locate_in_term generalized to locate_in_conjecture

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index b2ccf8e0cd1b6fdb0af721b13a7f397d25356c10..0817b75c15ed3a60db24ea5ff95cf2fd5fb9ae07 100644 (file)
--- a/helm/ocaml/tactics/.depend
+++ b/helm/ocaml/tactics/.depend
@@ -15,12 +15,13 @@ ring.cmi: proofEngineTypes.cmi
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
+tactics.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
 proofEngineReduction.cmo: proofEngineReduction.cmi 
 proofEngineReduction.cmx: proofEngineReduction.cmi 
-proofEngineHelpers.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi 
-proofEngineHelpers.cmx: proofEngineReduction.cmx proofEngineHelpers.cmi 
+proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
+proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi 
 tacticals.cmo: proofEngineTypes.cmi tacticals.cmi 
 tacticals.cmx: proofEngineTypes.cmx tacticals.cmi 
 reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
@@ -56,21 +57,23 @@ introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     introductionTactics.cmi 
 eliminationTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
-    proofEngineStructuralRules.cmi primitiveTactics.cmi \
-    eliminationTactics.cmi 
+    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi metadataQuery.cmi eliminationTactics.cmi 
 eliminationTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
-    proofEngineStructuralRules.cmx primitiveTactics.cmx \
-    eliminationTactics.cmi 
+    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx metadataQuery.cmx eliminationTactics.cmi 
 negationTactics.cmo: variousTactics.cmi tacticals.cmi proofEngineTypes.cmi \
     primitiveTactics.cmi eliminationTactics.cmi negationTactics.cmi 
 negationTactics.cmx: variousTactics.cmx tacticals.cmx proofEngineTypes.cmx \
     primitiveTactics.cmx eliminationTactics.cmx negationTactics.cmi 
 equalityTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
-    introductionTactics.cmi equalityTactics.cmi 
+    proofEngineStructuralRules.cmi proofEngineReduction.cmi \
+    proofEngineHelpers.cmi primitiveTactics.cmi introductionTactics.cmi \
+    equalityTactics.cmi 
 equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
-    introductionTactics.cmx equalityTactics.cmi 
+    proofEngineStructuralRules.cmx proofEngineReduction.cmx \
+    proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
+    equalityTactics.cmi 
 discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
     proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \
     equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi 
@@ -90,11 +93,11 @@ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \
     proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     fourier.cmx equalityTactics.cmx fourierR.cmi 
 fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \
-    proofEngineStructuralRules.cmi primitiveTactics.cmi metadataQuery.cmi \
-    fwdSimplTactic.cmi 
+    proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
+    primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi 
 fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \
-    proofEngineStructuralRules.cmx primitiveTactics.cmx metadataQuery.cmx \
-    fwdSimplTactic.cmi 
+    proofEngineStructuralRules.cmx proofEngineHelpers.cmx \
+    primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi 
 history.cmo: history.cmi 
 history.cmx: history.cmi 
 statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 4bb46fc4c011c491abfd316271b6e2b968137413..c24ccc773cf35f14138464bb639a9e5015e19739 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -557,7 +557,7 @@ exception Fail of string
 (** 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 =
+let locate_in_term what ~where context =
   let add_ctx context name entry =
       (Some (name, entry)) :: context
   in
@@ -603,7 +603,32 @@ let locate_in_term what ~where =
   and auxs context tl =  (* as aux for list of terms *)
     List.concat (List.map (fun t -> aux context t) tl)
   in
-   aux [] where
+   aux context where
+
+(** 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) =
+ 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 context' = entry::context in
+          context',res
+      | Some (_, Cic.Def (bo,ty)) ->
+         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
+         let context' = entry::context in
+          context',res
+   ) context ([],[])
+ in
+  res @ locate_in_term what ~where:ty context
 
 
 (* saturate_term newmeta metasenv context ty                                  *)

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index 78dc22c1c2e6b0dff0edc6a614bc6f9acf46b77d..f71574aef4bf67d560b8df8a0a6bee6b7e469f9f 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -80,10 +80,10 @@ val select:
   ] option list *
   (Cic.context * Cic.term) list
 
-(** locate_in_term what where
+(** locate_in_conjecture what where
 * [what] must be a physical pointer to a subterm of [where]
 * It returns the context of [what] in [where] *)
-val locate_in_term: Cic.term -> where:Cic.term -> Cic.context
+val locate_in_conjecture: Cic.term -> Cic.conjecture -> Cic.context
 
 (* saturate_term newmeta metasenv context ty                                  *)
 (* Given a type [ty] (a backbone), it returns its head and a new metasenv in  *)