Added a fol operation

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

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0ff4ddbe5358b82e7c27782c4e5974b6693d6e2e..827c1dc46f06a67146cf6d3b1a053971776231bf 100644 (file)
--- 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