This module implements the reduction from ACG signatures and lexicons to datalog programs
module Sg :
Interface.Signature_sig
with type term = Logic.Lambda.Lambda.term
and type stype = Logic.Lambda.Lambda.stypeval generate_and_add_rule :
abs_cst:(string * Logic.Lambda.Lambda.stype) ->
obj_princ_type:Logic.Lambda.Lambda.stype ->
obj_typing_env:
(Logic.Lambda.Lambda.term * Logic.Lambda.Lambda.stype)
UtilsLib.Utils.IntMap.t ->
DatalogLib.Datalog.Datalog.Program.program ->
abs_sig:Sg.t ->
obj_sig:Sg.t ->
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Rule.rule
* DatalogLib.Datalog.Datalog.Program.programgenerate_and_add_rule ~abs_cst ~obj_princ_type ~obj_typing_env
prog abs_sig obj_sig returns a pair (r,prog') where:
r is the generated ruleprog' is prog where the rule r has been addedabs_cst is the abstract constant from the abstract signature abs_sig that triggers the rule generationobj_princ_type is the principal type of the image by the lexicon of abs_cstobj_typing_env is its typing environment. The latter maps the position of the object constants in the realisation of abs_cst to a pair (t,ty) where t is the object constant itself, and ty the type associated by the principal typing environment.prog is the current datalog programabs_sig and obj_sig are the abstract signature and the object signature of some ACG.val edb_and_query :
obj_term:Logic.Lambda.Lambda.term ->
obj_type:Logic.Lambda.Lambda.stype ->
obj_typing_env:
(Logic.Lambda.Lambda.term * Logic.Lambda.Lambda.stype)
UtilsLib.Utils.IntMap.t ->
dist_type:Sg.stype ->
DatalogLib.Datalog.Datalog.Program.program ->
abs_sig:Sg.t ->
obj_sig:Sg.t ->
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate
* DatalogLib.Datalog.Datalog.Program.programedb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type
prog ~abs_sig ~obj_sig returns a pair (q,prog') where:
q is the predicate corresponding to the query generated by the object term obj_term to parseprog' is prog where the extensional database resulting from the reduction of the object term obj_termobj_type is the principal type of obj_termobj_typing_env is its typing environment. The latter maps the position of the object constants in the realisation of abs_cst to a pair (t,ty) where t is the object constant itself, and ty the type associated by the principal typing environment.dist_type is the distinguished type of the ACGprog is the current datalog programabs_sig and obj_sig are the abstract signature and the object signature of some ACG.