X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.ml;h=b38512273081907ab6cff86c16cd56f35be304a1;hb=refs%2Ftags%2F0.4.95%407852;hp=2a637135351516703b6e83e8c500ef467e11687a;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 2a6371353..b38512273 100644
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -27,11 +27,11 @@
 
 exception Bad_pattern of string Lazy.t
 
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _) =
+let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
   CicMkImplicit.new_meta metasenv []
 
 let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty, attrs = proof in
+ let uri,metasenv,initial_subst,bo,ty, attrs = proof in
    (* empty context is ok for term since it wont be used by apply_subst *)
    (* hack: since we do not know the context and the type of term, we
       create a substitution with cc =[] and type = Implicit; they will be
@@ -62,7 +62,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
       * since the parser does not reject as statements terms with
       * metavariable therein *)
      let ty' = subst_in ty in
-      let newproof = uri,metasenv'',bo',ty', attrs in
+      let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -77,8 +77,9 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*CSC: ci ripasso sopra apply_subst!!!                                     *)
 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
 (*CSC: [newmetasenv].                                             *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty, attrs) = proof in
+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
   (* Metavariables can appear also in the *statement* of the theorem
    * since the parser does not reject as statements terms with
@@ -104,7 +105,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = uri,metasenv',bo',ty', attrs in
+  (* qui da capire se per la fase transitoria si fa initial_subst @ subst
+   * oppure subst *)
+   let newproof = uri,metasenv',subst,bo',ty', attrs in
     (newproof, metasenv')
 
 let compare_metasenvs ~oldmetasenv ~newmetasenv =
@@ -360,25 +363,25 @@ let pattern_of ?(equality=(==)) ~term terms =
         if b1||b2 then true,Cic.Cast (te, ty)
         else
          not_found
-    | Cic.Prod (name, s, t) ->
+    | Cic.Prod (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.Prod (name, s, t)
+         true, Cic.Prod (Cic.Anonymous, s, t)
         else
          not_found
-    | Cic.Lambda (name, s, t) ->
+    | Cic.Lambda (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.Lambda (name, s, t)
+         true, Cic.Lambda (Cic.Anonymous, s, t)
         else
          not_found
-    | Cic.LetIn (name, s, t) ->
+    | Cic.LetIn (_, s, t) ->
        let b1,s = aux s in
        let b2,t = aux t in
         if b1||b2 then
-         true, Cic.LetIn (name, s, t)
+         true, Cic.LetIn (Cic.Anonymous, s, t)
         else
          not_found
     | Cic.Appl terms ->
@@ -483,17 +486,33 @@ exception Fail of string Lazy.t
    let find_pattern_for name =
      try Some (snd (List.find (fun (n, pat) -> Cic.Name n = name) hyp_patterns))
      with Not_found -> None in
+   (* Multiple hypotheses with the same name can be in the context.
+      In this case we need to pick the last one, but we will perform
+      a fold_right on the context. Thus we pre-process hyp_patterns. *)
+   let full_hyp_pattern =
+    let rec aux blacklist =
+     function
+        [] -> []
+      | None::tl -> None::aux blacklist tl
+      | Some (name,_)::tl ->
+         if List.mem name blacklist then
+          None::aux blacklist tl
+         else
+          find_pattern_for name::aux (name::blacklist) tl
+    in
+     aux [] context
+   in
    let subst,metasenv,ugraph,ty_terms =
     select_in_term ~metasenv ~context ~ugraph ~term:ty
      ~pattern:(what,goal_pattern) in
    let subst,metasenv,ugraph,context_terms =
     let subst,metasenv,ugraph,res,_ =
      (List.fold_right
-      (fun entry (subst,metasenv,ugraph,res,context) ->
+      (fun (pattern,entry) (subst,metasenv,ugraph,res,context) ->
         match entry with
-          None -> subst,metasenv,ugraph,(None::res),(None::context)
+          None -> subst,metasenv,ugraph,None::res,None::context
         | Some (name,Cic.Decl term) ->
-            (match find_pattern_for name with
+            (match pattern with
             | None ->
                subst,metasenv,ugraph,((Some (`Decl []))::res),(entry::context)
             | Some pat ->
@@ -504,7 +523,7 @@ exception Fail of string Lazy.t
                  subst,metasenv,ugraph,((Some (`Decl terms))::res),
                   (entry::context))
         | Some (name,Cic.Def (bo, ty)) ->
-            (match find_pattern_for name with
+            (match pattern with
             | None ->
                let selected_ty=match ty with None -> None | Some _ -> Some [] in
                 subst,metasenv,ugraph,((Some (`Def ([],selected_ty)))::res),
@@ -525,7 +544,7 @@ exception Fail of string Lazy.t
                 in
                  subst,metasenv,ugraph,((Some (`Def (terms_bo,terms_ty)))::res),
                   (entry::context))
-      ) context (subst,metasenv,ugraph,[],[]))
+      ) (List.combine full_hyp_pattern context) (subst,metasenv,ugraph,[],[]))
     in
      subst,metasenv,ugraph,res
    in
@@ -649,6 +668,13 @@ let split_with_whd (c, t) =
     in
     aux false [] 0 c t
 
+let split_with_normalize (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux a n c = function
+      | Cic.Prod (s, v, t)  -> aux ((c, v) :: a) (succ n) (add s v c) t
+      | v                   -> (c, v) :: a, n
+    in
+    aux [] 0 c (CicReduction.normalize c t)
 
   (* menv sorting *)
 module OT = 
@@ -680,4 +706,3 @@ let relations_of_menv m c =
 let sort_metasenv (m : Cic.metasenv) =
   (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
 ;;
-