Indexing local context for paramod.

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index ef100f74278ae34f9aada60f15445ea10a5c015b..587b29a3aa997b8d8d8d1613d62bb9c5e1345eb4 100644 (file)
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,5 +1,6 @@
 nTactics.cmi: nTacStatus.cmi 
 andOrTree.cmi: zipTree.cmi 
+nnAuto.cmi: nTacStatus.cmi 
 nAuto.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
 nDestructTac.cmi: nTacStatus.cmi 
@@ -15,8 +16,12 @@ zipTree.cmo: zipTree.cmi
 zipTree.cmx: zipTree.cmi 
 andOrTree.cmo: zipTree.cmi andOrTree.cmi 
 andOrTree.cmx: zipTree.cmx andOrTree.cmi 
-nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi 
-nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi 
+nnAuto.cmo: nTactics.cmi nTacStatus.cmi nnAuto.cmi 
+nnAuto.cmx: nTactics.cmx nTacStatus.cmx nnAuto.cmi 
+nAuto.cmo: zipTree.cmi nnAuto.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi \
+    nAuto.cmi 
+nAuto.cmx: zipTree.cmx nnAuto.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx \
+    nAuto.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 
 nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi 

diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile
index 6bb0ac3eee918af564f94ebb8332237346fc7362..e83858e7e6d790a6a52aad047c05ae3d37432c13 100644 (file)
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -7,6 +7,7 @@ INTERFACE_FILES = \
        nTactics.mli \
        zipTree.mli \
        andOrTree.mli \
+        nnAuto.mli \
        nAuto.mli \
        nInversion.mli \
        nDestructTac.mli

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 640128616719fdbeb76aa7eead5beed334e15e40..25f4e0fc70ff52c85f4e49f7630605fcae456bcc 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -13,7 +13,7 @@
 
 open Printf
 
-let debug = ref false
+let debug = ref true
 let debug_print ?(depth=0) s = 
   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
 let debug_do f = if !debug then f () else ()
@@ -1499,7 +1499,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
                  status pos cache 
 
   and attack pos cache and_item =
-    show pos; (* uncomment to show the tree *)
+    (* show pos; uncomment to show the tree *)
     match and_item with
     | _, S _ -> assert false (* next would close the proof or give a D *) 
     | _, L _ -> assert false (* L is a final solution *)
@@ -1618,6 +1618,40 @@ let auto_tac ~params:(_univ,flags) status =
     up_to depth depth
 ;;
 
+let rec rm_assoc n = function
+  | [] -> assert false
+  | (x,i)::tl when n=x -> i,tl
+  | p::tl -> let i,tl = rm_assoc n tl in i,p::tl
+;;
+
+let merge canonicals elements n m =
+  let cn,canonicals = rm_assoc n canonicals in
+  let cm,canonicals = rm_assoc m canonicals in
+  let ln,elements = rm_assoc cn elements in
+  let lm,elements = rm_assoc cm elements in
+  let canonicals = 
+    (n,cm)::(m,cm)::List.map 
+      (fun (x,xc) as p  -> 
+        if xc = cn then (x,cm) else p) canonicals
+  in 
+  let elements = (cn,ln@lm)::elements 
+  in
+    canonicals,elements
+;;
+
+let clusters f l =
+  let canonicals = List.map (fun x -> (x,x)) l in
+  let elements = List.map (fun x -> (x,[x])) l in
+   List.fold_left 
+     (fun (canonicals,elements) x ->
+       let dep = f x in
+        List.fold_left 
+          (fun (canonicals,elements) d ->
+             merge canonicals elements d x) 
+          (canonicals,elements) dep)
+     (canonicals,elements) l
+;;
+
 let group_by_tac ~eq_predicate ~action:tactic status = 
  let goals = head_goals status#stack in
  if List.length goals < 2 then tactic status 
@@ -1674,7 +1708,11 @@ let auto_tac ~params =
 (* ========================= dispatching of auto/auto_paramod ============ *)
 let auto_tac ~params:(_,flags as params) =
   if List.mem_assoc "paramodulation" flags then 
-    auto_paramod_tac ~params  
+    auto_paramod_tac ~params 
+  else if List.mem_assoc "fast_paramod" flags then 
+    NnAuto.fast_eq_check_tac ~params  
+  else if List.mem_assoc "slir" flags then 
+    NnAuto.auto_tac ~params  
   else 
     auto_tac ~params
 ;;

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 4af0c3fb7a0d14f01672ad7d6a20c91e3fe7f124..efb4e843c99a2e91da86a04144f657c666370c55 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -74,6 +74,7 @@ val atomic_tac :
       [> `NoTag ])
      list NTacStatus.status ->
      (< auto_cache : NCicLibrary.automation_cache;
+        eq_cache : NCicLibrary.unit_eq_cache;
         coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list;
         lstatus : LexiconEngine.lexicon_status; obj : NCic.obj;
         set_coerc_db : NCicCoercion.db -> 'c;

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0ff4ddbe5358b82e7c27782c4e5974b6693d6e2e..827c1dc46f06a67146cf6d3b1a053971776231bf 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -53,6 +53,25 @@ let auto_paramod_tac ~params status =
   NTactics.distribute_tac (auto_paramod ~params) status
 ;;
 
+let fast_eq_check ~params status goal =
+  let gty = get_goalty status goal in
+  let n,h,metasenv,subst,o = status#obj in
+  let eq_cache = status#eq_cache in
+  let status,t = term_of_cic_term status gty (ctx_of gty) in 
+  match
+    NCicParamod.fast_eq_check status metasenv subst (ctx_of gty) 
+      eq_cache (NCic.Rel ~-1,t) 
+  with
+  | [] -> raise (Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (mk_cic_term (ctx_of gty) pt)
+;;
+
+let fast_eq_check_tac  ~params = 
+  NTactics.distribute_tac (fast_eq_check ~params)
+;;
+
 (*************** subsumption ****************)
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 (* exceptions *)
@@ -1367,6 +1386,22 @@ let equational_and_applicative_case
  elems, cache
 ;;
 
+(* warning: ctx is supposed to be already instantiated w.r.t subst *)
+let index_local_equations eq_cache ctx =
+  let c = ref 0 in
+  List.fold_left 
+    (fun cache _ ->
+       c:= !c+1;
+       let t = NCic.Rel 1 in
+        try
+          let ty = NCicTypeChecker.typeof [] [] ctx t in
+            NCicParamod.forward_infer_step eq_cache t ty
+        with 
+          | NCicTypeChecker.TypeCheckerFailure _
+          | NCicTypeChecker.AssertFailure _ -> eq_cache) 
+    eq_cache ctx
+;;
+
 let rec guess_name name ctx = 
   if name = "_" then guess_name "auto" ctx else
   if not (List.mem_assoc name ctx) then name else