X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.ml;h=ec2e1919c456bf2f807c865d3f5e5cff8b48d2d1;hb=5717dca7637e00f6f82e462619ee0e07d99cf289;hp=177471c7403a4d9eb2da538289f76e5e718f0681;hpb=2a39b3fe15889f379932c642f4775a5f8e756022;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 177471c74..ec2e1919c 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 =
@@ -648,3 +651,43 @@ let split_with_whd (c, t) =
       | v                   -> aux true a n c (CicReduction.whd c v)
     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 = 
+  struct 
+    type t = Cic.conjecture
+    let compare (i,_,_) (j,_,_) = Pervasives.compare i j
+  end
+module MS = HTopoSort.Make(OT)
+let relations_of_menv m c =
+  let i, ctx, ty = c in
+  let m = List.filter (fun (j,_,_) -> j <> i) m in
+  let m_ty = List.map fst (CicUtil.metas_of_term ty) in
+  let m_ctx = 
+    List.flatten
+      (List.map 
+        (function 
+         | None -> []
+         | Some (_,Cic.Decl t)
+         | Some (_,Cic.Def (t,None)) -> 
+             List.map fst (CicUtil.metas_of_term ty)
+         | Some (_,Cic.Def (t,Some ty)) -> 
+             List.map fst (CicUtil.metas_of_term ty) @
+             List.map fst (CicUtil.metas_of_term t))
+        ctx)
+  in
+  let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
+  List.filter (fun (i,_,_) -> List.exists ((=) i) metas) m
+;;
+let sort_metasenv (m : Cic.metasenv) =
+  (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
+;;
+