added homepage URL, now we have one

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index f390b0e42c92dabf2e2b6c48ebc612eacce2e889..22b6c8487a8348d74a80f896c501a26f3263aba1 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -194,26 +194,32 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
            ) (subst,metasenv,ugraph,[]) patterns
          in
           subst,metasenv,ugraph,resoutty @ resindterm @ respatterns
-(*CSC: c'e' ancora un problema: il caso vs Meta puo' alterare il goal ==>
-       bisogna ricominciare da capo sul nuovo goal per preservare i puntatori
-       fisici
       | Cic.Fix (_, funl) -> 
          let tys =
           List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
          in
           List.fold_left (
-            fun acc (_, _, ty, bo) ->
-             find context w ty @ find (tys @ context) w bo @ acc
-          ) [] funl
+            fun (subst,metasenv,ugraph,acc) (_, _, ty, bo) ->
+             let subst,metasenv,ugraph,resty =
+              find subst metasenv ugraph context w ty in
+             let subst,metasenv,ugraph,resbo =
+              find subst metasenv ugraph (tys @ context) w bo
+             in
+              subst,metasenv,ugraph, resty @ resbo @ acc
+          ) (subst,metasenv,ugraph,[]) funl
       | Cic.CoFix (_, funl) ->
          let tys =
           List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funl
          in
           List.fold_left (
-            fun acc (_, ty, bo) ->
-             find context w ty @ find (tys @ context) w bo @ acc
-          ) [] funl
-*)
+            fun (subst,metasenv,ugraph,acc) (_, ty, bo) ->
+             let subst,metasenv,ugraph,resty =
+              find subst metasenv ugraph context w ty in
+             let subst,metasenv,ugraph,resbo =
+              find subst metasenv ugraph (tys @ context) w bo
+             in
+              subst,metasenv,ugraph, resty @ resbo @ acc
+          ) (subst,metasenv,ugraph,[]) funl
   in
   find subst metasenv ugraph context wanted t
   
@@ -548,6 +554,88 @@ exception Fail of string
    in
     subst,metasenv,ugraph,context_terms, ty_terms
 
+(** 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
+* [context] must be the context of [where]
+*)
+let locate_in_term ?(equality=(==))what ~where context =
+  let add_ctx context name entry =
+      (Some (name, entry)) :: context in
+  let rec aux context where =
+   if equality what where then [context,where]
+   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.LetIn (name, s, 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
+    | Cic.Fix (_, funs) ->
+       let tys =
+        List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs
+       in
+        List.concat
+          (List.map
+            (fun (_, _, ty, 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.map
+            (fun (_, ty, 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)
+  in
+   aux context 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
+* [context] must be the context of [where]
+*)
+let locate_in_conjecture ?(equality=(==)) 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                                  *)
 (* 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 *)
@@ -601,3 +689,13 @@ let saturate_term newmeta metasenv context ty =
    let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
     res,metasenv @ newmetasenv,arguments,lastmeta
 
+let lookup_type metasenv context hyp =
+   let rec aux p = function
+      | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
+      | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
+      | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
+         p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+      | _ :: tail -> aux (succ p) tail
+      | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+   in
+   aux 1 context