X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=4224eb5b154ba117ca0c2c2093adb601507afd55;hb=0409d6974224ddfc00a5f3d9918651c6d99aa661;hp=ea797481c4edf96b0f550f60fa0c9fb9cc6e510b;hpb=c5b08eb60c8ede80fad4f44abd8439cef9b339c1;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index ea797481c..4224eb5b1 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -111,62 +111,119 @@ let compare_metasenvs ~oldmetasenv ~newmetasenv =
 ;;
 
 (** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
-let find_subterms ~wanted ~context t =
-  let rec find context w t =
-    if ProofEngineReduction.alpha_equivalence w t then 
-      [context,t]
-    else
+let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
+  let rec find subst metasenv ugraph context w t =
+   try
+    let subst,metasenv,ugraph =
+     CicUnification.fo_unif_subst subst context metasenv w t ugraph
+    in
+      subst,metasenv,ugraph,[context,t]
+   with
+     CicUnification.UnificationFailure _
+   | CicUnification.Uncertain _ ->
       match t with
       | Cic.Sort _ 
-      | Cic.Rel _ -> []
+      | Cic.Rel _ -> subst,metasenv,ugraph,[]
       | Cic.Meta (_, ctx) -> 
           List.fold_left (
-            fun acc e -> 
+            fun (subst,metasenv,ugraph,acc) e -> 
               match e with 
-              | None -> acc 
-              | Some t -> find context w t @ acc
-          ) [] ctx
+              | None -> subst,metasenv,ugraph,acc 
+              | Some t ->
+                 let subst,metasenv,ugraph,res =
+                  find subst metasenv ugraph context w t
+                 in
+                  subst,metasenv,ugraph, res @ acc
+          ) (subst,metasenv,ugraph,[]) ctx
       | Cic.Lambda (name, t1, t2) 
       | Cic.Prod (name, t1, t2) ->
-          find context w t1 @
-          find (Some (name, Cic.Decl t1)::context)
+         let subst,metasenv,ugraph,rest1 =
+          find subst metasenv ugraph context w t1 in
+         let subst,metasenv,ugraph,rest2 =
+          find subst metasenv ugraph (Some (name, Cic.Decl t1)::context)
            (CicSubstitution.lift 1 w) t2
+         in
+          subst,metasenv,ugraph,rest1 @ rest2
       | Cic.LetIn (name, t1, t2) -> 
-          find context w t1 @
-          find (Some (name, Cic.Def (t1,None))::context)
+         let subst,metasenv,ugraph,rest1 =
+          find subst metasenv ugraph context w t1 in
+         let subst,metasenv,ugraph,rest2 =
+          find subst metasenv ugraph (Some (name, Cic.Def (t1,None))::context)
            (CicSubstitution.lift 1 w) t2
+         in
+          subst,metasenv,ugraph,rest1 @ rest2
       | Cic.Appl l -> 
-          List.fold_left (fun acc t -> find context w t @ acc) [] l
-      | Cic.Cast (t, ty) -> find context w t @ find context w ty
+          List.fold_left
+           (fun (subst,metasenv,ugraph,acc) t ->
+             let subst,metasenv,ugraph,res =
+              find subst metasenv ugraph context w t
+             in
+              subst,metasenv,ugraph,res @ acc)
+           (subst,metasenv,ugraph,[]) l
+      | Cic.Cast (t, ty) ->
+         let subst,metasenv,ugraph,rest =
+          find subst metasenv ugraph context w t in
+         let subst,metasenv,ugraph,resty =
+          find subst metasenv ugraph context w ty
+         in
+          subst,metasenv,ugraph,rest @ resty
       | Cic.Implicit _ -> assert false
       | Cic.Const (_, esubst)
       | Cic.Var (_, esubst) 
       | Cic.MutInd (_, _, esubst) 
       | Cic.MutConstruct (_, _, _, esubst) -> 
-          List.fold_left (fun acc (_, t) -> find context w t @ acc) [] esubst
+          List.fold_left
+           (fun (subst,metasenv,ugraph,acc) (_, t) ->
+             let subst,metasenv,ugraph,res =
+              find subst metasenv ugraph context w t
+             in
+              subst,metasenv,ugraph,res @ acc)
+           (subst,metasenv,ugraph,[]) esubst
       | Cic.MutCase (_, _, outty, indterm, patterns) -> 
-          find context w outty @ find context w indterm @ 
-            List.fold_left (fun acc p -> find context w p @ acc) [] patterns
+         let subst,metasenv,ugraph,resoutty =
+          find subst metasenv ugraph context w outty in
+         let subst,metasenv,ugraph,resindterm =
+          find subst metasenv ugraph context w indterm in
+         let subst,metasenv,ugraph,respatterns =
+          List.fold_left
+           (fun (subst,metasenv,ugraph,acc) p ->
+             let subst,metaseng,ugraph,res =
+              find subst metasenv ugraph context w p
+             in
+              subst,metasenv,ugraph,res @ acc
+           ) (subst,metasenv,ugraph,[]) patterns
+         in
+          subst,metasenv,ugraph,resoutty @ resindterm @ respatterns
       | 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 context wanted t
+  find subst metasenv ugraph context wanted t
   
-let select_in_term ~context ~term ~pattern:(wanted,where) =
+let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
   let add_ctx context name entry =
       (Some (name, entry)) :: context
   in
@@ -238,21 +295,21 @@ let select_in_term ~context ~term ~pattern:(wanted,where) =
    let context_len = List.length context in
    let roots = aux context where term in
     match wanted with
-       None -> roots
+       None -> [],metasenv,ugraph,roots
      | Some wanted ->
         let rec find_in_roots =
          function
-            [] -> []
+            [] -> [],metasenv,ugraph,[]
           | (context',where)::tl ->
-             let tl' = find_in_roots tl in
+             let subst,metasenv,ugraph,tl' = find_in_roots tl in
              let context'_len = List.length context' in
-             let found =
+             let subst,metasenv,ugraph,found =
               let wanted =
                CicSubstitution.lift (context'_len - context_len) wanted
               in
-               find_subterms ~wanted ~context where
+               find_subterms ~subst ~metasenv ~ugraph ~wanted ~context where
              in
-              found @ tl'
+              subst,metasenv,ugraph,found @ tl'
         in
          find_in_roots roots
 
@@ -406,21 +463,26 @@ exception Fail of string
   * has an entry for each entry in the context and in the same order.
   * Of course the list of terms (with their context) associated to the
   * hypothesis name may be empty. *)
-  let select ~metasenv ~conjecture:(_,context,ty) ~pattern:(what,hyp_patterns,goal_pattern) =
+  let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
+       ~pattern:(what,hyp_patterns,goal_pattern)
+  =
    let find_pattern_for name =
      try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
      with Not_found -> None in
-   let ty_terms = select_in_term ~context ~term:ty ~pattern:(what,goal_pattern) in
+   let subst,metasenv,ugraph,ty_terms =
+    select_in_term ~metasenv ~context ~ugraph ~term:ty
+     ~pattern:(what,goal_pattern) in
    let context_len = List.length context in
-   let context_terms =
-    fst
+   let subst,metasenv,ugraph,context_terms =
+    let subst,metasenv,ugraph,res,_ =
      (List.fold_right
-      (fun entry (res,context) ->
+      (fun entry (subst,metasenv,ugraph,res,context) ->
         match entry with
-          None -> (None::res),(None::context)
+          None -> subst,metasenv,ugraph,(None::res),(None::context)
         | Some (name,Cic.Decl term) ->
             (match find_pattern_for name with
-            | None -> ((Some (`Decl []))::res),(entry::context)
+            | None ->
+               subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
                try
                 let what =
@@ -434,8 +496,12 @@ exception Fail of string
                       assert (subst' = []);
                       assert (metasenv' = metasenv);
                       Some what in
-                let terms = select_in_term ~context ~term ~pattern:(what,pat) in
-                 ((Some (`Decl terms))::res),(entry::context)
+                let subst,metasenv,ugraph,terms =
+                 select_in_term ~metasenv ~context ~ugraph ~term
+                  ~pattern:(what,pat)
+                in
+                 subst,metasenv,ugraph,((Some (`Decl terms))::res),
+                  (entry::context)
                with
                 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                  raise
@@ -445,8 +511,9 @@ exception Fail of string
         | Some (name,Cic.Def (bo, ty)) ->
             (match find_pattern_for name with
             | None ->
-               let selected_ty= match ty with None -> None | Some _ -> Some [] in
-                ((Some (`Def ([],selected_ty)))::res),(entry::context)
+               let selected_ty=match ty with None -> None | Some _ -> Some [] in
+                subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
+                 (entry::context)
             | Some pat -> 
                try
                 let what =
@@ -460,21 +527,153 @@ exception Fail of string
                       assert (subst' = []);
                       assert (metasenv' = metasenv);
                       Some what in
-                let terms_bo =
-                 select_in_term ~context ~term:bo ~pattern:(what,pat) in
-                let terms_ty =
+                let subst,metasenv,ugraph,terms_bo =
+                 select_in_term ~metasenv ~context ~ugraph ~term:bo
+                  ~pattern:(what,pat) in
+                let subst,metasenv,ugraph,terms_ty =
                  match ty with
-                    None -> None
+                    None -> subst,metasenv,ugraph,None
                   | Some ty ->
-                     Some (select_in_term ~context ~term:ty ~pattern:(what,pat))
+                     let subst,metasenv,ugraph,res =
+                      select_in_term ~metasenv ~context ~ugraph ~term:ty
+                       ~pattern:(what,pat)
+                     in
+                      subst,metasenv,ugraph,Some res
                 in
-                 ((Some (`Def (terms_bo,terms_ty)))::res),(entry::context)
+                 subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
+                  (entry::context)
                with
                 CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
                  raise
                   (Fail
                     ("The term the user wants to convert is not closed " ^
                      "in the context of the position of the substitution.")))
-      ) context ([],[]))
+      ) context (subst,metasenv,ugraph,[],[]))
+    in
+     subst,metasenv,ugraph,res
+   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 *)
+(* new applications and the index of the last new META introduced. The nth    *)
+(* argument in the list of arguments is just the nth new META.                *)
+let saturate_term newmeta metasenv context ty =
+ let module C = Cic in
+ let module S = CicSubstitution in
+  let rec aux newmeta ty =
+   let ty' = ty in
+   match ty' with
+      C.Cast (he,_) -> aux newmeta he
+(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
+      (* If the expected type is a Type, then also Set is OK ==>
+      *  we accept any term of type Type *)
+      (*CSC: BUG HERE: in this way it is possible for the term of
+      * type Type to be different from a Sort!!! *)
+    | C.Prod (name,(C.Sort (C.Type _) as s),t) ->
+       (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *)
+       let irl =
+         CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        let newargument = C.Meta (newmeta+1,irl) in
+         let (res,newmetasenv,arguments,lastmeta) =
+          aux (newmeta + 2) (S.subst newargument t)
+         in
+          res,
+           (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
+           newargument::arguments,lastmeta
+*)
+    | C.Prod (name,s,t) ->
+       let irl =
+         CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        let newargument = C.Meta (newmeta,irl) in
+         let (res,newmetasenv,arguments,lastmeta) =
+          aux (newmeta + 1) (S.subst newargument t)
+         in
+         let s' = CicReduction.normalize ~delta:false context s in
+          res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
+          (** NORMALIZE RATIONALE 
+           * we normalize the target only NOW since we may be in this case:
+           * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k  
+           * and we want a mesasenv with ?1:A1 and ?2:A2 and not
+           * ?1, ?2, ?3 (that is the one we whould get if we start from the
+           * beta-normalized A1 -> A2 -> A3 -> P **)
+    | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
+  in
+   (* WARNING: here we are using the invariant that above the most *)
+   (* recente new_meta() there are no used metas.                  *)
+   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
-    context_terms, ty_terms
+   aux 1 context