Merge branch 'lazy-dtree' of github.com:Deducteam/Dedukti into lazy-d…

…tree
GuillaumeGen · Apr 3, 2019 · 9434399 · 9434399
2 parents 7bc9a51 + a980044
commit 9434399
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 12 deletions.
diff --git a/kernel/rule.ml b/kernel/rule.ml
@@ -40,18 +40,19 @@ type constr =
   | Linearity of int * int
   | Bracket   of int * term
 
-type rule_infos = {
-  l           : loc;
-  name        : rule_name;
-  cst         : name;
-  args        : pattern list;
-  rhs         : term;
-  ctx_size    : int;
-  esize       : int;
-  pats        : wf_pattern array;
-  arity       : int array;
-  constraints : constr list;
-}
+type rule_infos =
+  {
+    l           : loc;
+    name        : rule_name;
+    cst         : name;
+    args        : pattern list;
+    rhs         : term;
+    ctx_size    : int;
+    esize       : int;
+    pats        : wf_pattern array;
+    arity       : int array;
+    constraints : constr list;
+  }
 
 let infer_rule_context ri =
   let res = Array.make ri.ctx_size (mk_ident "_") in

diff --git a/kernel/signature.ml b/kernel/signature.ml
@@ -69,7 +69,12 @@ type t =
   {
     name   : mident;
     file   : string;
+    (** [tables] maps module ident to the hastable of their symbols.
+        It should only contain a single entry for each module.
+        Each module's hashtable should only contain a single entry
+        for each of its symbols. *)
     tables : (rw_infos HId.t) HMd.t;
+
     mutable external_rules:rule_infos list list;
   }