X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=827c1dc46f06a67146cf6d3b1a053971776231bf;hb=3ca99dabf7d136ebd58fa61e7a2d7134c8dc365c;hp=0ff4ddbe5358b82e7c27782c4e5974b6693d6e2e;hpb=711a06aebcd4f8e1127a56d82dd1fc4de22d5ea2;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0ff4ddbe5..827c1dc46 100644
--- 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