From 0409d6974224ddfc00a5f3d9918651c6d99aa661 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 26 Jul 2005 14:56:19 +0000
Subject: [PATCH] draft version of locate_in_term

---
 helm/ocaml/tactics/proofEngineHelpers.ml  | 60 +++++++++++++++++++++++
 helm/ocaml/tactics/proofEngineHelpers.mli |  2 +
 2 files changed, 62 insertions(+)

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ae6c7ef50..4224eb5b1 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -554,6 +554,66 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
+let locate_in_term what ~where =
+  let add_ctx context name entry =
+      (Some (name, entry)) :: context
+  in
+  let rec aux context where =
+   if what == where then context
+   else
+    match where with
+    | Cic.Implicit _
+    | Cic.Meta _
+    | Cic.Rel _
+    | Cic.Sort _
+    | Cic.Var _
+    | Cic.Const _
+    | Cic.MutInd _
+    | 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
+    | Cic.Appl tl -> auxs context tl
+(*
+    | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> 
+        aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
+    | Cic.LetIn (Cic.Name n1, s1, t1), 
+      Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> 
+        aux context s1 s2 @ aux (add_ctx context name (Cic.Def (s2,None))) t1 t2
+    | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
+    | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
+        aux context out1 out2 @ aux context t1 t2 @ auxs context pat1 pat2
+    | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
+       let tys =
+        List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+       in
+        List.concat
+          (List.map2
+            (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
+              aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
+            funs1 funs2)
+    | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
+       let tys =
+        List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
+       in
+        List.concat
+          (List.map2
+            (fun (_, ty1, bo1) (_, ty2, bo2) ->
+              aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
+            funs1 funs2)
+    | x,y -> 
+        raise (Bad_pattern 
+                (Printf.sprintf "Pattern %s versus term %s" 
+                  (CicPp.ppterm x)
+                  (CicPp.ppterm y)))
+*)
+  and auxs context tl =  (* as aux for list of terms *)
+    List.concat (List.map (fun t -> aux context t) tl)
+  in
+   aux [] where
+
+
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)
 (* which there is new a META for each hypothesis, a list of arguments for the *)
diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index 013d6292a..b04f13139 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -80,6 +80,8 @@ val select:
   ] option list *
   (Cic.context * Cic.term) list
 
+val locate_in_term: Cic.term -> where:Cic.term -> Cic.context
+
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)
 (* which there is new a META for each hypothesis, a list of arguments for the *)
-- 
2.39.2