X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=1b1132dee8a90e0d06684d05b843d6bb4dfc6f9d;hb=4bea40e6589ce21c15ecf99bdd5bd2a1c62f6809;hp=29341cb5dd72b3dcf6abd7d7e38d1d7c0a7e3142;hpb=e356b6fba9e8fd1e757e7589f01fb9b51979f76c;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 29341cb5d..1b1132dee 100644
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -26,9 +26,9 @@ let app_counter = ref 0
 
 module RHT = struct
   type t = NReference.reference
-  let equal = (==)
-  let compare = Pervasives.compare
-  let hash = Hashtbl.hash
+  let equal = NReference.eq
+  let compare = NReference.compare
+  let hash = NReference.hash
 end;;
 
 module RefHash = Hashtbl.Make(RHT);;
@@ -267,6 +267,7 @@ let solve f status eq_cache goal =
                         Lazy.force msg ^
 			"\n in the environment\n" ^ 
 			status#ppmetasenv subst metasenv)); None
+      | Sys.Break as e -> raise e
       | _ -> None
     in
     HExtlib.filter_map build_status
@@ -317,6 +318,44 @@ let index_local_equations eq_cache status =
     eq_cache ctx
 ;;
 
+let index_local_equations2 eq_cache status open_goal lemmas nohyps =
+  noprint (lazy "indexing equations");
+  let eq_cache,lemmas =
+   match lemmas with
+      None -> eq_cache,[]
+    | Some l -> NCicParamod.empty_state,l
+  in
+  let ngty = get_goalty status open_goal in
+  let _,_,metasenv,subst,_ = status#obj in
+  let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
+  let status,lemmas =
+   List.fold_left
+    (fun (status,lemmas) l ->
+      let status,l = NTacStatus.disambiguate status ctx l None in
+      let status,l = NTacStatus.term_of_cic_term status l ctx in
+       status,l::lemmas)
+    (status,[]) lemmas in
+  let local_equations =
+   if nohyps then [] else
+    List.map (fun i -> NCic.Rel (i + 1))
+     (HExtlib.list_seq 1 (List.length ctx)) in
+  let lemmas = lemmas @ local_equations in
+  List.fold_left 
+    (fun eq_cache t ->
+         try
+           let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
+           if is_a_fact status (mk_cic_term ctx ty) then
+             (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+              NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
+           else 
+             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
+              eq_cache)
+         with 
+           | NCicTypeChecker.TypeCheckerFailure _
+           | NCicTypeChecker.AssertFailure _ -> eq_cache)
+    eq_cache lemmas
+;;
+
 let fast_eq_check_tac ~params s = 
   let unit_eq = index_local_equations s#eq_cache s in   
   dist_fast_eq_check unit_eq s
@@ -340,8 +379,11 @@ let demod eq_cache status goal =
 ;;
 
 let demod_tac ~params s = 
-  let unit_eq = index_local_equations s#eq_cache s in   
-  NTactics.distribute_tac (demod unit_eq) s
+  let unit_eq s i =
+   index_local_equations2 s#eq_cache s i (fst params)
+    (List.mem_assoc "nohyps" (snd params))
+  in   
+   NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s
 ;;
 
 (*
@@ -436,7 +478,9 @@ let close_metasenv status metasenv subst =
            (* prerr_endline (status#ppterm ctx [] [] iterm); *)
            let s_entry = i, ([], ctx, iterm, ty)
            in s_entry::subst,okind::objs
-         with _ -> assert false)
+         with
+            Sys.Break as e -> raise e
+          | _ -> assert false)
       (subst,[]) metasenv
 ;;