Module Reduction.Make

This module implements the reduction from ACG signatures and lexicons to datalog programs

Parameters

module Sg : module type of Signature.Data_Signature

Signature

val generate_and_add_rule : abs_cst:(string * Logic.Lambda.Lambda.stype) -> interpretation:(Logic.Lambda.Lambda.term * Logic.Lambda.Lambda.stype) -> 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:(name, dist_type) ~interpretation:(o_term, o_type) prog abs_sig obj_sig returns a pair (r,prog') where:

  • r is the generated rule
  • prog' is prog where the rule r has been added
  • name is the abstract constant name from the abstract signature abs_sig that triggers the rule generation, and dist_type is its type
  • o_term is the interpretation of name according to some lexicon
  • o_type is its type (and should be the image by the same lexicon of abs_cst
  • prog is the current datalog program
  • abs_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:Sg.stype -> 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.program

edb_and_query ~obj_term ~obj_type ~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 parse
  • prog' is prog where the extensional database resulting from the reduction of the object term obj_term has been added
  • obj_type is the type of obj_term (only used for debugging information)
  • dist_type is the distinguished type of the ACG
  • prog is the current datalog program
  • abs_sig and obj_sig are the abstract signature and the object signature of some ACG.