removing extra spaces

[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 25bc6376119ebcaff753212c7ba11aa4666ea929..b77c633694404c00e155d6d102cbaca41645355d 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -28,7 +28,7 @@ module RHT = struct
   type t = NReference.reference
   let equal = NReference.eq
   let compare = NReference.compare
-  let hash = NReferece.hash
+  let hash = NReference.hash
 end;;
 
 module RefHash = Hashtbl.Make(RHT);;
@@ -145,7 +145,7 @@ let is_a_fact_obj s uri =
 let is_a_fact_ast status subst metasenv ctx cand = 
  noprint ~depth:0 
    (lazy ("checking facts " ^ NotationPp.pp_term status cand)); 
- let status, t = disambiguate status ctx ("",0,cand) None in
+ let status, t = disambiguate status ctx ("",0,cand) `XTNone in
  let status,t = term_of_cic_term status t ctx in
  let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
    is_a_fact status (mk_cic_term ctx ty)
@@ -247,7 +247,7 @@ let solve f status eq_cache goal =
             NCicUnification.unify status metasenv subst ctx gty pty *)
         NCicRefiner.typeof 
           (status#set_coerc_db NCicCoercion.empty_db) 
-          metasenv subst ctx pt (Some gty) 
+          metasenv subst ctx pt (`XTSome gty) 
         in 
           noprint (lazy (Printf.sprintf "Refined in %fs"
                      (Unix.gettimeofday() -. stamp))); 
@@ -318,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 `XTNone 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
@@ -341,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
 ;;
 
 (*
@@ -549,7 +590,7 @@ let smart_apply t unit_eq status g =
   let n,h,metasenv,subst,o = status#obj in
   let gname, ctx, gty = List.assoc g metasenv in
   (* let ggty = mk_cic_term context gty in *)
-  let status, t = disambiguate status ctx t None in
+  let status, t = disambiguate status ctx t `XTNone in
   let status,t = term_of_cic_term status t ctx in
   let _,_,metasenv,subst,_ = status#obj in
   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
@@ -591,6 +632,10 @@ let smart_apply t unit_eq status g =
       | NCicEnvironment.ObjectNotFound s as e ->
           raise (Error (lazy "eq_coerc non yet defined",Some e))
       | Error _ as e -> debug_print (lazy "error"); raise e
+(* FG: for now we catch TypeCheckerFailure; to be understood *)  
+      | NCicTypeChecker.TypeCheckerFailure _ ->
+          debug_print (lazy "TypeCheckerFailure");
+          raise (Error (lazy "no proof found",None))
 ;;
 
 let compare_statuses ~past ~present =
@@ -933,7 +978,7 @@ let openg_no status = List.length (head_goals status#stack)
 let sort_candidates status ctx candidates =
  let _,_,metasenv,subst,_ = status#obj in
   let branch cand =
-    let status,ct = disambiguate status ctx ("",0,cand) None in
+    let status,ct = disambiguate status ctx ("",0,cand) `XTNone in
     let status,t = term_of_cic_term status ct ctx in
     let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
     let res = branch status (mk_cic_term ctx ty) in
@@ -1770,7 +1815,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
       | None -> None 
       | Some l -> 
          let to_Ast t =
-           let status, res = disambiguate status [] t None in 
+(* FG: `XTSort here? *)          
+           let status, res = disambiguate status [] t `XTNone in 
            let _,res = term_of_cic_term status res (ctx_of res) 
            in Ast.NCic res 
           in Some (List.map to_Ast l) 
@@ -1841,23 +1887,3 @@ let auto_tac ~params:(_,flags as params) ?trace_ref =
     fast_eq_check_tac ~params  
   else auto_tac ~params ?trace_ref
 ;;
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-