X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=1b1132dee8a90e0d06684d05b843d6bb4dfc6f9d;hb=90293a04a41156a66b381a867714d3563b4c2594;hp=bc6730376640e654753258dd48a5ef252799f8a7;hpb=99d8a9f4c5d6e3b3052ec03189e02db6b817bc55;p=helm.git

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index bc6730376..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
@@ -306,7 +307,7 @@ let index_local_equations eq_cache status =
          try
            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
            if is_a_fact status (mk_cic_term ctx ty) then
-             (noprint(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+             (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)));
@@ -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
 ;;
 
@@ -1040,7 +1084,7 @@ let get_cands retrieve_for diff empty gty weak_gty =
             cands, diff more_cands cands
 ;;
 
-let get_candidates ?(smart=true) depth flags status cache signature gty =
+let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
   let universe = status#auto_cache in
   let _,_,metasenv,subst,_ = status#obj in
   let context = ctx_of gty in
@@ -1110,10 +1154,11 @@ let get_candidates ?(smart=true) depth flags status cache signature gty =
   let candidates_facts,candidates_other =
     let gl1,gl2 = List.partition test global_cands in
     let ll1,ll2 = List.partition test local_cands in
-    (* if the goal is an equation we avoid to apply unit equalities,
-     since superposition should take care of them; refl is an
+    (* if the goal is an equation and paramodulation did not fail
+     we avoid to apply unit equalities; refl is an
      exception since it prompts for convertibility *)
-    let l1 = if is_eq then [Ast.Ident("refl",None)] else gl1@ll1 in 
+    let l1 = if is_eq && (not pfailed) 
+      then [Ast.Ident("refl",None)] else gl1@ll1 in 
     let l2 = 
       (* if smart given candidates are applied in smart mode *)
       if by && smart then ll2
@@ -1141,7 +1186,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty =
   sort_candidates status context (smart_candidates_other)
 ;;
 
-let applicative_case depth signature status flags gty cache =
+let applicative_case ~pfailed depth signature status flags gty cache =
   app_counter:= !app_counter+1; 
   let _,_,metasenv,subst,_ = status#obj in
   let context = ctx_of gty in
@@ -1157,7 +1202,7 @@ let applicative_case depth signature status flags gty cache =
   (* new *)
   let candidates_facts, smart_candidates_facts, 
       candidates_other, smart_candidates_other = 
-    get_candidates ~smart:true depth 
+    get_candidates ~smart:true ~pfailed depth 
       flags status tcache signature gty 
   in
   let sm = if is_eq || is_prod then 0 else 2 in
@@ -1361,7 +1406,7 @@ let is_meta status gty =
 
 let do_something signature flags status g depth gty cache =
   (* if the goal is meta we close it with I:True. This should work
-    thnaks to the toplogical sorting of goals. *)
+    thanks to the toplogical sorting of goals. *)
   if is_meta status gty then
     let t = Ast.Ident("I",None) in
     debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
@@ -1384,7 +1429,7 @@ let do_something signature flags status g depth gty cache =
   in
   let l2 = 
     if ((l1 <> []) && flags.last) then [] else
-    applicative_case depth signature status flags gty cache 
+    applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache 
   in
   (* statistics *)
   List.iter