unpatched version for the new CamplP5

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 32573639b350a11d591e23cecdd5bf42003a433c..29341cb5dd72b3dcf6abd7d7e38d1d7c0a7e3142 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -292,10 +292,11 @@ let auto_eq_check eq_cache status =
 ;;
 
 let index_local_equations eq_cache status =
+  noprint (lazy "indexing equations");
   let open_goals = head_goals status#stack in
   let open_goal = List.hd open_goals in
-  debug_print (lazy ("indexing equations for " ^ string_of_int open_goal));
   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 c = ref 0 in
   List.fold_left 
@@ -303,12 +304,12 @@ let index_local_equations eq_cache status =
        c:= !c+1;
        let t = NCic.Rel !c in
          try
-           let ty = NCicTypeChecker.typeof status [] [] ctx t in
+           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 [] [] ty)));
-              NCicParamod.forward_infer_step eq_cache t 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 [] [] ty)));
+             (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
               eq_cache)
          with 
            | NCicTypeChecker.TypeCheckerFailure _
@@ -1018,7 +1019,7 @@ let perforate_small status subst metasenv context t =
   let rec aux = function
     | NCic.Appl (hd::tl) ->
        let map t =
-         let s = sort_of status subst metasenv context t in
+           let s = sort_of status subst metasenv context t in
            match s with
              | NCic.Sort(NCic.Type [`Type,u])
                  when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
@@ -1039,7 +1040,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
@@ -1064,7 +1065,7 @@ let get_candidates ?(smart=true) depth flags status cache signature gty =
             let raw_weak = 
               perforate_small status subst metasenv context raw_gty in
             let weak = mk_cic_term context raw_weak in
-            debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
+            noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
               Some raw_weak, Some (weak)
        | _ -> None,None
     else None,None
@@ -1109,10 +1110,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
@@ -1140,7 +1142,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
@@ -1156,7 +1158,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
@@ -1190,7 +1192,6 @@ let applicative_case depth signature status flags gty cache =
 exception Found
 ;;
 
-
 (* gty is supposed to be meta-closed *)
 let is_subsumed depth filter_depth status gty cache =
   if cache=[] then false else (
@@ -1361,7 +1362,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 +1385,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