X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2FproofEngineHelpers.ml;h=2a637135351516703b6e83e8c500ef467e11687a;hb=a1c4c601850c71e094a4703af00f02ca2026d8ed;hp=6e7b5a8e74aa90deb24642ad3184f562233b18fb;hpb=9e18c7f8aa6c5b905598521c769c1a2f58c13262;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 6e7b5a8e7..2a6371353 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 = proof in
+ let uri,metasenv,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' in
+      let newproof = uri,metasenv'',bo',ty', attrs in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -78,7 +78,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*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) = proof in
+ let (uri,_,bo,ty, attrs) = proof 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 +104,7 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = uri,metasenv',bo',ty' in
+   let newproof = uri,metasenv',bo',ty', attrs in
     (newproof, metasenv')
 
 let compare_metasenvs ~oldmetasenv ~newmetasenv =
@@ -613,69 +613,6 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) =
  in
   res @ locate_in_term what ~where:ty context
 
-(* saturate_term newmeta metasenv context ty goal_arity                       *)
-(* Given a type [ty] (a backbone), it returns its suffix of length            *)
-(* [goal_arity] 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 goal_arity =
- let module C = Cic in
- let module S = CicSubstitution in
- assert (goal_arity >= 0);
-  let rec aux newmeta ty =
-   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,prod_no =
-          aux (newmeta + 1) (S.subst newargument t)
-         in
-          if prod_no + 1 = goal_arity then
-           let head = CicReduction.normalize ~delta:false context ty in
-            head,[],[],lastmeta,goal_arity + 1
-          else
-           (** 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 **)
-           let s' = CicReduction.normalize ~delta:false context s in
-            res,(newmeta,context,s')::newmetasenv,newargument::arguments,
-             lastmeta,prod_no + 1
-    | t ->
-       let head = CicReduction.normalize ~delta:false context t in
-        match CicReduction.whd context head with
-           C.Prod _ as head' -> aux newmeta head'
-         | _ -> head,[],[],newmeta,0
-  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
@@ -689,17 +626,6 @@ let lookup_type metasenv context hyp =
 
 (* FG: **********************************************************************)
 
-let list_rev_map_filter f l =
-   let rec aux a = function
-      | []       -> a
-      | hd :: tl -> 
-         begin match f hd with
-	    | None   -> aux a tl
-	    | Some b -> aux (b :: a) tl 
-         end
-   in 
-   aux [] l
-
 let get_name context index =
    try match List.nth context (pred index) with
       | Some (Cic.Name name, _)     -> Some name
@@ -713,3 +639,45 @@ let get_rel context name =
       | _ :: tl                                 -> aux (succ i) tl
    in
    aux 1 context
+
+let split_with_whd (c, t) =
+   let add s v c = Some (s, Cic.Decl v) :: c in
+   let rec aux whd a n c = function
+      | Cic.Prod (s, v, t)  -> aux false ((c, v) :: a) (succ n) (add s v c) t
+      | v when whd          -> (c, v) :: a, n
+      | v                   -> aux true a n c (CicReduction.whd c v)
+    in
+    aux false [] 0 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)
+;;
+