New tactic unfold.

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index c24ccc773cf35f14138464bb639a9e5015e19739..c9dc6c2c611194760e24bc42b17f0039904da959 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -554,15 +554,23 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
-(** locate_in_term what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_term what ~where context =
+exception TermNotFound
+exception TermFoundMultipleTimes
+
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched term together with its context in [where]
+* [equality] defaults to physical equality
+* [context] must be the context of [where]
+* It may raise TermNotFound or TermFoundMultipleTimes
+*)
+let locate_in_term ?(equality=(==))what ~where context =
+  let (@@) (l1,l2) (l1',l2') = l1 @ l1', l2 @ l2' in
+  let list_concat l = List.fold_right (@@) l ([],[]) in
   let add_ctx context name entry =
-      (Some (name, entry)) :: context
-  in
+      (Some (name, entry)) :: context in
   let rec aux context where =
-   if what == where then context
+   if equality what where then context,[where]
    else
     match where with
     | Cic.Implicit _
@@ -572,64 +580,75 @@ let locate_in_term what ~where context =
     | Cic.Var _
     | Cic.Const _
     | Cic.MutInd _
-    | Cic.MutConstruct _ -> []
-    | Cic.Cast (te, ty) -> aux context te @ aux context ty
+    | Cic.MutConstruct _ -> [],[]
+    | Cic.Cast (te, ty) -> aux context te @@ aux context ty
     | Cic.Prod (name, s, t)
     | Cic.Lambda (name, s, t) ->
-        aux context s @ aux (add_ctx context name (Cic.Decl s)) t
+        aux context s @@ aux (add_ctx context name (Cic.Decl s)) t
     | Cic.LetIn (name, s, t) -> 
-        aux context s @ aux (add_ctx context name (Cic.Def (s,None))) t
+        aux context s @@ aux (add_ctx context name (Cic.Def (s,None))) t
     | Cic.Appl tl -> auxs context tl
     | Cic.MutCase (_, _, out, t, pat) ->
-        aux context out @ aux context t @ auxs context pat
+        aux context out @@ aux context t @@ auxs context pat
     | Cic.Fix (_, funs) ->
        let tys =
         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
-        List.concat
+        list_concat
           (List.map
             (fun (_, _, ty, bo) -> 
-              aux context ty @ aux (tys @ context) bo)
+              aux context ty @@ aux (tys @ context) bo)
             funs)
     | Cic.CoFix (_, funs) ->
        let tys =
         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
        in
-        List.concat
+        list_concat
           (List.map
             (fun (_, ty, bo) ->
-              aux context ty @ aux (tys @ context) bo)
+              aux context ty @@ aux (tys @ context) bo)
             funs)
   and auxs context tl =  (* as aux for list of terms *)
-    List.concat (List.map (fun t -> aux context t) tl)
+    list_concat (List.map (fun t -> aux context t) tl)
   in
-   aux context where
+   match aux context where with
+      context,[] -> raise TermNotFound
+    | context,[t] -> context,t
+    | context,_ -> raise TermFoundMultipleTimes
 
-(** locate_in_conjecture what where
-* [what] must be a physical pointer to a subterm of [where]
-* It returns the context of [what] in [where] *)
-let locate_in_conjecture what (_,context,ty) =
+(** locate_in_term equality what where
+* [what] must be a subterm of [where] according to [equality]
+* It returns the context of [what] in [where]
+* [equality] defaults to physical equality
+* It may raise TermNotFound or TermFoundMultipleTimes
+*)
+let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
+ let (@@) (l1,l2) (l1',t) = l1 @ l1', l2 @ [t] in
  let context,res =
   List.fold_right
    (fun entry (context,res) ->
      match entry with
         None -> entry::context, res
       | Some (_, Cic.Decl ty) ->
-         let res = res @ locate_in_term what ~where:ty context in
+         let res = res @@ locate_in_term ~equality what ~where:ty context in
          let context' = entry::context in
           context',res
       | Some (_, Cic.Def (bo,ty)) ->
-         let res = res @ locate_in_term what ~where:bo context in
+         let res = res @@ locate_in_term ~equality what ~where:bo context in
          let res =
           match ty with
              None -> res
-           | Some ty -> res @ locate_in_term what ~where:ty context in
+           | Some ty ->
+              res @@ locate_in_term ~equality what ~where:ty context in
          let context' = entry::context in
           context',res
-   ) context ([],[])
+   ) context ([],([],[]))
  in
-  res @ locate_in_term what ~where:ty context
-
+ let res = res @@ locate_in_term ~equality what ~where:ty context in
+  match res with
+     context,[] -> raise TermNotFound
+   | context,[_] -> context
+   | context,_ -> raise TermFoundMultipleTimes
 
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)