first snapshot of the night-profiling

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index aec43abc373750a42f8edbe26c807950e68d516b..c1f4ebc3c7ac58466066cbf25e7001802226b756 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -24,11 +24,16 @@
  *)
 
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
-  CicMkImplicit.new_meta metasenv
+  CicMkImplicit.new_meta metasenv []
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,bo,ty = proof in
-  let subst_in = CicMetaSubst.apply_subst [meta,term] in
+   (* empty context is ok for term since it wont be used by apply_subst *)
+   (* hack: since we do not know the context and the type of term, we
+      create a substitution with cc =[] and type = Implicit; they will be
+      in  any case dropped by apply_subst, but it would be better to rewrite
+      the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
+  let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
    in
@@ -48,7 +53,11 @@ let subst_meta_in_proof proof meta term newmetasenv =
       ) metasenv'
     in
      let bo' = subst_in bo in
-      let newproof = uri,metasenv'',bo',ty in
+     (* Metavariables can appear also in the *statement* of the theorem
+      * since the parser does not reject as statements terms with
+      * metavariable therein *)
+     let ty' = subst_in ty in
+      let newproof = uri,metasenv'',bo',ty' in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -66,6 +75,10 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
  let (uri,_,bo,ty) = proof in
   let bo' = subst_in bo in
+  (* Metavariables can appear also in the *statement* of the theorem
+   * since the parser does not reject as statements terms with
+   * metavariable therein *)
+  let ty' = subst_in ty in
   let metasenv' =
    List.fold_right
     (fun metasenv_entry i ->
@@ -85,6 +98,55 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = uri,metasenv',bo',ty in
+   let newproof = uri,metasenv',bo',ty' in
     (newproof, metasenv')
 
+let compare_metasenvs ~oldmetasenv ~newmetasenv =
+ List.map (function (i,_,_) -> i)
+  (List.filter
+   (function (i,_,_) ->
+     not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
+;;
+
+(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
+let find_subterms ~eq ~wanted t =
+  let rec find wanted t =
+    if eq wanted t then 
+      [t]
+    else
+      match t with
+      | Cic.Sort _ 
+      | Cic.Rel _ -> []
+      | Cic.Meta (_, ctx) -> 
+          List.fold_left (
+            fun acc e -> 
+              match e with 
+              | None -> acc 
+              | Some t -> find wanted t @ acc
+          ) [] ctx
+      | Cic.Lambda (_, t1, t2) 
+      | Cic.Prod (_, t1, t2) 
+      | Cic.LetIn (_, t1, t2) -> 
+          find wanted t1 @ find (CicSubstitution.lift 1 wanted) t2
+      | Cic.Appl l -> 
+          List.fold_left (fun acc t -> find wanted t @ acc) [] l
+      | Cic.Cast (t, ty) -> find wanted t @ find wanted ty
+      | Cic.Implicit _ -> assert false
+      | Cic.Const (_, esubst)
+      | Cic.Var (_, esubst) 
+      | Cic.MutInd (_, _, esubst) 
+      | Cic.MutConstruct (_, _, _, esubst) -> 
+          List.fold_left (fun acc (_, t) -> find wanted t @ acc) [] esubst
+      | Cic.MutCase (_, _, outty, indterm, patterns) -> 
+          find wanted outty @ find wanted indterm @ 
+            List.fold_left (fun acc p -> find wanted p @ acc) [] patterns
+      | Cic.Fix (_, funl) -> 
+          List.fold_left (
+            fun acc (_, _, ty, bo) -> find wanted ty @ find wanted bo @ acc
+          ) [] funl
+      | Cic.CoFix (_, funl) ->
+          List.fold_left (
+            fun acc (_, ty, bo) -> find wanted ty @ find wanted bo @ acc
+          ) [] funl
+  in
+  find wanted t