1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index b9ee8bb8fc8d72eb00e231ad0b9f531d6b6cd9ad..22b6c8487a8348d74a80f896c501a26f3263aba1 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -554,23 +554,17 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
-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]
+* It returns the matched terms together with their contexts 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
   let rec aux context where =
-   if equality what where then context,[where]
+   if equality what where then [context,where]
    else
     match where with
     | Cic.Implicit _
@@ -580,83 +574,67 @@ let locate_in_term ?(equality=(==))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
-   match aux context where with
-      context,[] -> raise TermNotFound
-    | context,[t] -> context,t
-    | context,_ -> raise TermFoundMultipleTimes
+   aux context where
 
-(** locate_in_term equality what where
-* [what] must be a subterm of [where] according to [equality]
-* It returns the context of [what] in [where]
+(** locate_in_term equality what where context
+* [what] must match a subterm of [where] according to [equality]
+* It returns the matched terms together with their contexts in [where]
 * [equality] defaults to physical equality
-* It may raise TermNotFound or TermFoundMultipleTimes
+* [context] must be the context of [where]
 *)
 let locate_in_conjecture ?(equality=(==)) what (_,context,ty) =
- let (@@) (l1,l2) =
-  function
-     None -> l1,l2
-   | Some (l1',t) -> l1 @ l1', l2 @ [t] in
- let locate_in_term what ~where context =
-  try
-   Some (locate_in_term ~equality what ~where context)
-  with
-     TermNotFound -> None 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 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 what ~where:bo context in
          let res =
           match ty with
              None -> res
            | Some ty ->
-              res @@ locate_in_term what ~where:ty context in
+              res @ locate_in_term what ~where:ty context in
          let context' = entry::context in
           context',res
-   ) context ([],([],[]))
+   ) context ([],[])
  in
- let res = res @@ locate_in_term what ~where:ty context in
-  match res with
-     context,[] -> raise TermNotFound
-   | context,[_] -> context
-   | context,_ -> raise TermFoundMultipleTimes
+  res @ locate_in_term what ~where:ty context
 
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)