X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.ml;h=d95d37d8ca53090771a8f10a7f1068d0eb0f3677;hb=765eb07cafb8a06a5027f4569ad06d805aba2488;hp=b38512273081907ab6cff86c16cd56f35be304a1;hpb=61d82f6f49845fe5111969156945accf21fb5a70;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml
index b38512273..d95d37d8c 100644
--- a/helm/software/components/tactics/proofEngineHelpers.ml
+++ b/helm/software/components/tactics/proofEngineHelpers.ml
@@ -27,8 +27,8 @@
 
 exception Bad_pattern of string Lazy.t
 
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
-  CicMkImplicit.new_meta metasenv []
+let new_meta_of_proof ~proof:(_, metasenv, subst, _, _, _) =
+  CicMkImplicit.new_meta metasenv subst
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,initial_subst,bo,ty, attrs = proof in
@@ -48,16 +48,15 @@ let subst_meta_in_proof proof meta term newmetasenv =
          List.map
           (function
               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def (subst_in s,None))
             | None -> None
-            | Some (n,Cic.Def (bo,Some ty)) ->
-               Some (n,Cic.Def (subst_in bo,Some (subst_in ty)))
+            | Some (n,Cic.Def (bo,ty)) ->
+               Some (n,Cic.Def (subst_in bo,subst_in ty))
           ) canonical_context
         in
          i,canonical_context',(subst_in ty)
       ) metasenv'
     in
-     let bo' = subst_in bo in
+     let bo' = lazy (subst_in (Lazy.force bo)) in
      (* Metavariables can appear also in the *statement* of the theorem
       * since the parser does not reject as statements terms with
       * metavariable therein *)
@@ -80,7 +79,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
  let (uri,_,initial_subst,bo,ty, attrs) = proof in
   let subst_in = CicMetaSubst.apply_subst subst in
-  let bo' = subst_in bo in
+  let bo' = lazy (subst_in (Lazy.force bo)) in
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
    * metavariable therein *)
@@ -95,10 +94,8 @@ let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
              (function
                  None -> None
                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
-               | Some (i,Cic.Def (t,None))  ->
-                  Some (i,Cic.Def (subst_in t,None))
-               | Some (i,Cic.Def (bo,Some ty)) ->
-                  Some (i,Cic.Def (subst_in bo,Some (subst_in ty)))
+               | Some (i,Cic.Def (bo,ty)) ->
+                  Some (i,Cic.Def (subst_in bo,subst_in ty))
              ) canonical_context
            in
             (m,canonical_context',subst_in ty)::i
@@ -151,14 +148,16 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
            (CicSubstitution.lift 1 w) t2
          in
           subst,metasenv,ugraph,rest1 @ rest2
-      | Cic.LetIn (name, t1, t2) -> 
+      | Cic.LetIn (name, t1, t2, t3) -> 
          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
+          find subst metasenv ugraph context w t2 in
+         let subst,metasenv,ugraph,rest3 =
+          find subst metasenv ugraph (Some (name, Cic.Def (t1,t2))::context)
+           (CicSubstitution.lift 1 w) t3
          in
-          subst,metasenv,ugraph,rest1 @ rest2
+          subst,metasenv,ugraph,rest1 @ rest2 @ rest3
       | Cic.Appl l -> 
           List.fold_left
            (fun (subst,metasenv,ugraph,acc) t ->
@@ -230,7 +229,9 @@ let find_subterms ~subst ~metasenv ~ugraph ~wanted ~context t =
   in
   find subst metasenv ugraph context wanted t
   
-let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
+let select_in_term 
+  ~metasenv ~subst ~context ~ugraph ~term ~pattern:(wanted,where) 
+=
   let add_ctx context name entry = (Some (name, entry)) :: context in
   let map2 error_msg f l1 l2 = 
     try 
@@ -263,12 +264,16 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
         aux context s1 s2 @ aux (add_ctx context name (Cic.Decl s2)) t1 t2
     | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
     | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
-    | 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.LetIn (Cic.Anonymous, s1, ty1, t1), Cic.LetIn (name, s2, ty2, t2) -> 
+        aux context s1 s2 @
+        aux context ty1 ty2 @
+        aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+    | Cic.LetIn (Cic.Name n1, s1, ty1, t1), 
+      Cic.LetIn ((Cic.Name n2) as name, s2, ty2, t2) when n1 = n2-> 
+        aux context s1 s2 @
+        aux context ty1 ty2 @
+        aux (add_ctx context name (Cic.Def (s2,ty2))) t1 t2
+    | Cic.LetIn (name1, s1, ty1, t1), Cic.LetIn (name2, s2, ty2, t2) -> []
     | Cic.Appl terms1, Cic.Appl terms2 -> auxs context terms1 terms2
     | Cic.Var (_, subst1), Cic.Var (_, subst2)
     | Cic.Const (_, subst1), Cic.Const (_, subst2)
@@ -310,13 +315,13 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
      | Some where -> aux context where term
    in
     match wanted with
-       None -> [],metasenv,ugraph,roots
+       None -> subst,metasenv,ugraph,roots
      | Some wanted ->
-        let rec find_in_roots =
+        let rec find_in_roots subst =
          function
-            [] -> [],metasenv,ugraph,[]
+            [] -> subst,metasenv,ugraph,[]
           | (context',where)::tl ->
-             let subst,metasenv,ugraph,tl' = find_in_roots tl in
+             let subst,metasenv,ugraph,tl' = find_in_roots subst tl in
              let subst,metasenv,ugraph,found =
               let wanted, metasenv, ugraph = wanted context' metasenv ugraph in
                find_subterms ~subst ~metasenv ~ugraph ~wanted ~context:context'
@@ -324,7 +329,8 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
              in
               subst,metasenv,ugraph,found @ tl'
         in
-         find_in_roots roots
+         find_in_roots subst roots
+;;
 
 (** create a pattern from a term and a list of subterms.
 * the pattern is granted to have a ? for every subterm that has no selected
@@ -377,11 +383,12 @@ let pattern_of ?(equality=(==)) ~term terms =
          true, Cic.Lambda (Cic.Anonymous, s, t)
         else
          not_found
-    | Cic.LetIn (_, s, t) ->
+    | Cic.LetIn (_, s, ty, t) ->
        let b1,s = aux s in
-       let b2,t = aux t in
-        if b1||b2 then
-         true, Cic.LetIn (Cic.Anonymous, s, t)
+       let b2,ty = aux ty in
+       let b3,t = aux t in
+        if b1||b2||b3 then
+         true, Cic.LetIn (Cic.Anonymous, s, ty, t)
         else
          not_found
     | Cic.Appl terms ->
@@ -479,7 +486,7 @@ exception Fail of string Lazy.t
   *
   * @raise Bad_pattern
   * *)
-  let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
+  let select ~metasenv ~subst ~ugraph ~conjecture:(_,context,ty)
        ~(pattern: (Cic.term, Cic.lazy_term) ProofEngineTypes.pattern)
   =
    let what, hyp_patterns, goal_pattern = pattern in
@@ -503,8 +510,9 @@ exception Fail of string Lazy.t
      aux [] context
    in
    let subst,metasenv,ugraph,ty_terms =
-    select_in_term ~metasenv ~context ~ugraph ~term:ty
-     ~pattern:(what,goal_pattern) in
+    select_in_term ~metasenv ~subst ~context ~ugraph ~term:ty
+     ~pattern:(what,goal_pattern) 
+   in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
@@ -517,7 +525,7 @@ exception Fail of string Lazy.t
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
                 let subst,metasenv,ugraph,terms =
-                 select_in_term ~metasenv ~context ~ugraph ~term
+                 select_in_term ~subst ~metasenv ~context ~ugraph ~term
                   ~pattern:(what, Some pat)
                 in
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
@@ -525,22 +533,19 @@ exception Fail of string Lazy.t
         | Some (name,Cic.Def (bo, ty)) ->
             (match pattern with
             | None ->
-               let selected_ty=match ty with None -> None | Some _ -> Some [] in
+               let selected_ty = [] in
                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
                  (entry::context)
             | Some pat -> 
                 let subst,metasenv,ugraph,terms_bo =
-                 select_in_term ~metasenv ~context ~ugraph ~term:bo
+                 select_in_term ~subst ~metasenv ~context ~ugraph ~term:bo
                   ~pattern:(what, Some pat) in
                 let subst,metasenv,ugraph,terms_ty =
-                 match ty with
-                    None -> subst,metasenv,ugraph,None
-                  | Some ty ->
-                     let subst,metasenv,ugraph,res =
-                      select_in_term ~metasenv ~context ~ugraph ~term:ty
-                       ~pattern:(what, Some pat)
-                     in
-                      subst,metasenv,ugraph,Some res
+                 let subst,metasenv,ugraph,res =
+                  select_in_term ~subst ~metasenv ~context ~ugraph ~term:ty
+                   ~pattern:(what, Some pat)
+                 in
+                  subst,metasenv,ugraph,res
                 in
                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
                   (entry::context))
@@ -549,6 +554,7 @@ exception Fail of string Lazy.t
      subst,metasenv,ugraph,res
    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]
@@ -575,8 +581,10 @@ let locate_in_term ?(equality=(fun _ -> (==))) what ~where context =
     | 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.LetIn (name, s, ty, t) -> 
+        aux context s @
+        aux context ty @
+        aux (add_ctx context name (Cic.Def (s,ty))) t
     | Cic.Appl tl -> auxs context tl
     | Cic.MutCase (_, _, out, t, pat) ->
         aux context out @ aux context t @ auxs context pat
@@ -621,11 +629,7 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
           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 res = res @ locate_in_term what ~where:ty context in
          let context' = entry::context in
           context',res
    ) context ([],[])
@@ -635,14 +639,38 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
 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)
+      | Some (Cic.Name name, Cic.Def (_,t)) :: _ when name = hyp -> p, t
       | _ :: tail -> aux (succ p) tail
       | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
    in
    aux 1 context
 
+let find_hyp name =
+ let rec find_hyp n =
+  function
+     [] -> assert false
+   | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
+      Cic.Rel n, CicSubstitution.lift n ty
+   | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
+   | _::tl -> find_hyp (n+1) tl
+ in
+  find_hyp 1
+;;
+
+(* sort pattern hypotheses from the smallest to the highest Rel *)
+let sort_pattern_hyps context (t,hpatterns,cpattern) =
+ let hpatterns =
+  List.sort
+   (fun (id1,_) (id2,_) ->
+     let t1,_ = find_hyp id1 context in
+     let t2,_ = find_hyp id2 context in
+     match t1,t2 with
+        Cic.Rel n1, Cic.Rel n2 -> compare n1 n2
+      | _,_ -> assert false) hpatterns
+ in
+  t,hpatterns,cpattern
+;;
+
 (* FG: **********************************************************************)
 
 let get_name context index =
@@ -692,10 +720,9 @@ let relations_of_menv m c =
       (List.map 
         (function 
          | None -> []
-         | Some (_,Cic.Decl t)
-         | Some (_,Cic.Def (t,None)) -> 
+         | Some (_,Cic.Decl t) ->
              List.map fst (CicUtil.metas_of_term ty)
-         | Some (_,Cic.Def (t,Some ty)) -> 
+         | Some (_,Cic.Def (t,ty)) -> 
              List.map fst (CicUtil.metas_of_term ty) @
              List.map fst (CicUtil.metas_of_term t))
         ctx)