datalog.mli 6.28 KB
Newer Older
1 2
open UtilsLib

3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
module ASPred:module type of Datalog_AbstractSyntax.AbstractSyntax.Predicate 
  with type pred_id=Datalog_AbstractSyntax.AbstractSyntax.Predicate.pred_id 
  and type PredIdTable.table = Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table

module ASRule:module type of Datalog_AbstractSyntax.AbstractSyntax.Rule
  with type rule=Datalog_AbstractSyntax.AbstractSyntax.Rule.rule

module ASProg:module type of Datalog_AbstractSyntax.AbstractSyntax.Program
  with type program = Datalog_AbstractSyntax.AbstractSyntax.Program.program


module type Datalog_Sig=
sig
  exception Fails
  module UF:UnionFind.S
    
  module Predicate :
  sig
    type predicate = { p_id : ASPred.pred_id; arity : int; }
    val make_predicate : Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate -> predicate
    module PredMap : Map.S with type key = ASPred.pred_id
    module FactSet :Set.S with type elt = ASPred.predicate
    val conditionnal_add :
      FactSet.elt -> FactSet.t -> FactSet.t -> FactSet.t -> FactSet.t
    val facts_to_string : FactSet.t PredMap.t -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> string
    module PredicateMap : Map.S with type key = ASPred.predicate
    module Premise :
    sig
      type t = ASPred.predicate list * int * int (* the first int parameter is meant to be the rule id and the second one to be the number of intensional predicates occurring in it*)
      val to_string : t -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> string
    end
    module PremiseSet : Set.S with type elt = Premise.t
    val add_map_to_premises_to_buffer : Buffer.t -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> PremiseSet.t PredicateMap.t -> unit
    val format_derivations2 : ?query:Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> PremiseSet.t PredicateMap.t -> unit




    val add_pred_arguments_to_content :
      ASPred.term list ->
      Datalog_AbstractSyntax.ConstGen.id UF.content list * int *
        int Datalog_AbstractSyntax.VarGen.IdMap.t ->
      Datalog_AbstractSyntax.ConstGen.id UF.content list * int *
        int Datalog_AbstractSyntax.VarGen.IdMap.t
	
  end
    
  module Rule :
  sig
    type rule = {
      id : int;
      lhs : Predicate.predicate;
      e_rhs : (Predicate.predicate*int) list;
      i_rhs : (Predicate.predicate*int) list;
      i_rhs_num:int;
      content : Datalog_AbstractSyntax.ConstGen.id UF.t;
    }
    val make_rule : ASRule.rule -> rule
    val cyclic_unify : int -> int -> 'a UF.t -> 'a UF.t
    val extract_consequence :
      rule -> Datalog_AbstractSyntax.ConstGen.id UF.t -> ASPred.predicate
    module FactArray :
    sig
      type row = Predicate.FactSet.t
      type array = row list
      val collect_results :
        ('a -> (int * Datalog_AbstractSyntax.ConstGen.id UF.t) * Predicate.FactSet.elt list -> 'a) ->
        'a ->
        (int * Datalog_AbstractSyntax.ConstGen.id UF.t) * Predicate.FactSet.elt list -> array -> 'a
    end
    val immediate_consequence_of_rule :
      rule -> FactArray.row Predicate.PredMap.t -> ASPred.predicate list
      
    module Rules:Set.S with type elt=rule
  end
    
  module Program :
  sig
    type program = {
82 83
      (*      rules : Rule.rule list Predicate.PredMap.t; *)
      rules : Rule.Rules.t Predicate.PredMap.t;
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
      edb : ASPred.pred_id list;
      edb_facts:Predicate.FactSet.t Predicate.PredMap.t;
      idb : ASPred.pred_id list;
      pred_table: ASPred.PredIdTable.table;
      const_table: Datalog_AbstractSyntax.ConstGen.Table.table;
      rule_id_gen:IdGenerator.IntIdGen.t;
    }
    val empty : program
    val make_program : ASProg.program -> program
    val temp_facts :
      Rule.rule ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t ->
      (ASPred.predicate * Predicate.FactSet.elt list -> Rule.rule -> 'a -> 'a) -> 'a -> ASPred.PredIdTable.table -> Datalog_AbstractSyntax.ConstGen.Table.table -> 'a
    val p_semantics_for_predicate :
      Predicate.PredMap.key ->
      program ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t ->
      Rule.FactArray.row Predicate.PredMap.t -> Predicate.PremiseSet.t Predicate.PredicateMap.t -> Predicate.FactSet.t * Predicate.PremiseSet.t Predicate.PredicateMap.t 
    val seminaive : program -> Rule.FactArray.row Predicate.PredMap.t * Predicate.PremiseSet.t Predicate.PredicateMap.t
    val to_abstract : program -> ASProg.program
      
    val extend : program -> ASProg.modifier -> program
      
    val add_e_facts : program -> (ASRule.rule list*Datalog_AbstractSyntax.ConstGen.Table.table*IdGenerator.IntIdGen.t) -> program
      
    (** [add_rule i r p] adds a [ASRule.rule] to a [Datalog.Program]
115
	with the assumption that it will not change the {e nature} of
116 117 118 119 120 121 122
	any predicate (that is making it change from extensional to
	intensional). If [i] is set to true, then the rule concerns an
	intensional predicate. If it is set to [false] then it
	concerns an extensional predicate and the rhs of the rule
	should be empty.*)
      
    val add_rule : intensional:bool -> ASRule.rule -> program -> program
123 124 125 126 127 128 129 130 131 132 133

    (** [remove_rule id p] returns the program [p] from which the rule
	with id [id] has been removed.
	
	IMPORTANT: This function only deals with rules introducing
	intensional predicate, because it is used when a constant is
	given several interpretations in a lexicon.
	
    *)
    val remove_rule : int -> ASPred.pred_id -> program -> program

134 135 136 137 138 139 140 141
      
    val get_fresh_rule_id : program -> (int * program)
    val get_fresh_cst_id : string -> program -> (Datalog_AbstractSyntax.ConstGen.id * program)
    val add_pred_sym : string -> program -> (ASPred.pred_id*program)

    val build_forest : ?query:Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate -> Predicate.PremiseSet.t Predicate.PredicateMap.t -> program -> int SharedForest.SharedForest.tree list list

    val edb_to_buffer : program -> Buffer.t
142
    val edb_to_log : Logs.src -> Logs.level -> program -> unit
143 144 145 146 147 148 149 150 151 152

  end
end
  
  

module Make :
  functor (S : UnionFind.Store) -> Datalog_Sig

module Datalog:Datalog_Sig