Reduction.MakeSourceThis module implements the reduction from ACG signatures and lexicons to datalog programs
module Sg : module type of Signature.Data_Signatureval 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 ->
abs_sig:Sg.t ->
obj_sig:Sg.t ->
update_fct:
(Logic.Lambda.Lambda.term ->
(string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.t) ->
string * (string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.t)) ->
syms:(string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.t) ->
DatalogLib.Datalog.Datalog.Program.program ->
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Rule.rule
* DatalogLib.Datalog.Datalog.Program.program
* (string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.t)generate_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 ->
?adornment:MagicRewriting.Adornment.status list ->
DatalogLib.Datalog.Datalog.Program.program ->
abs_sig:Sg.t ->
obj_sig:Sg.t ->
syms:(string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.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_term has been addedobj_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.val only_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 ->
syms:(string UtilsLib.Utils.IntMap.t * UtilsLib.Utils.StringSet.t) ->
DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate
* DatalogLib.Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate list
* DatalogLib.Datalog.Datalog.Program.programonly_edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type prog ~abs_sig ~obj_sig returns a triple (q,edb,prog') where:
q is the predicate corresponding to the query generated by the object term obj_term to parseedb is the extensional database (as a list of predicates) resulting from the reduction of the object term obj_termprog' is prog with the const_table updated from the queryobj_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.