Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 74 insertions, 47 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9bfb33ea..00a69bba 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -1,3 +1,4 @@
+(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
@@ -6,12 +7,14 @@
 *)
 
 open Term
+open Sign
 open Names
 open Evd
 open List
 open Pp
 open Util
 open Subtac_utils
+open Proof_type
 
 let trace s = 
   if !Flags.debug then (msgnl s; msgerr s)
@@ -20,15 +23,27 @@ let trace s =
 let succfix (depth, fixrels) = 
   (succ depth, List.map succ fixrels)
 
+type oblinfo =
+  { ev_name: int * identifier;
+    ev_hyps: named_context;
+    ev_status: obligation_definition_status;
+    ev_chop: int option;
+    ev_loc: Util.loc;
+    ev_typ: types;
+    ev_tac: Tacexpr.raw_tactic_expr option;
+    ev_deps: Intset.t }
+    
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
+
 let subst_evar_constr evs n t = 
   let seen = ref Intset.empty in
   let transparent = ref Idset.empty in
   let evar_info id = List.assoc id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
-	let (id, idstr), hyps, chop, _, _, _ = 
+	let { ev_name = (id, idstr) ; 
+	      ev_hyps = hyps ; ev_chop = chop } =
 	  try evar_info k
 	  with Not_found -> 
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -46,17 +61,13 @@ let subst_evar_constr evs n t =
 	  let rec aux hyps args acc =
 	     match hyps, args with
 		 ((_, None, _) :: tlh), (c :: tla) -> 
-		   aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc)
+		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
 	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
 	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
 	  in aux hyps args [] 
 	in
-  	  (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (List.length args) ++ str "arguments," ++
-			int (List.length hyps) ++ str " hypotheses" ++ spc () ++
-			pp_list (fun x -> my_print_constr (Global.env ()) x) args);
- 	   with _ -> ());
 	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
 	    transparent := Idset.add idstr !transparent;
 	  mkApp (mkVar idstr, Array.of_list args)
@@ -93,8 +104,8 @@ let etype_of_evar evs hyps concl =
 	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
-		if noccurn 1 rest then lift (-1) rest, s', trans'
-		else
+(* 		if noccurn 1 rest then lift (-1) rest, s', trans' *)
+(* 		else *)
 		  let c', s'', trans'' = subst_evar_constr evs n c in
 		  let c' = subst_vars acc 0 c' in
 		    mkNamedProd_or_LetIn (id, Some c', t'') rest, 
@@ -121,15 +132,34 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let eterm_obligations env name isevars evm fs t ty = 
-  (* 'Serialize' the evars, we assume that the types of the existentials
-     refer to previous existentials in the list only *)
-  trace (str " In eterm: isevars: " ++ my_print_evardefs isevars);
-  trace (str "Term given to eterm" ++ spc () ++
-	    Termops.print_constr_env (Global.env ()) t);
+let evar_dependencies evm ev =
+  let one_step deps = 
+    Intset.fold (fun ev s -> 
+      let evi = Evd.find evm ev in
+	Intset.union (Evarutil.evars_of_evar_info evi) s)
+      deps deps
+  in 
+  let rec aux deps =
+    let deps' = one_step deps in
+      if Intset.equal deps deps' then deps
+      else aux deps'
+  in aux (Intset.singleton ev)
+
+let sort_dependencies evl =
+  List.sort (fun (_, _, deps) (_, _, deps') -> 
+    if Intset.subset deps deps' then (* deps' depends on deps *) -1
+    else if Intset.subset deps' deps then 1
+    else Intset.compare deps deps')
+    evl
+    
+let eterm_obligations env name isevars evm fs ?status t ty = 
+  (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
   let nc_len = Sign.named_context_length nc in
   let evl = List.rev (to_list evm) in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
   let evn = 
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i; 
@@ -146,20 +176,29 @@ let eterm_obligations env name isevars evm fs t ty =
 	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
 	 let evtyp, hyps, chop = 
 	   match chop_product fs evtyp with
-	       Some t -> 
-		 (try
-		    trace (str "Choped a product: " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) evtyp ++ str " to " ++ spc () ++
-			     Termops.print_constr_env (Global.env ()) t);
-		  with _ -> ());
-		 t, trunc_named_context fs hyps, fs
-	     | None -> evtyp, hyps, 0
+	   | Some t -> t, trunc_named_context fs hyps, fs
+	   | None -> evtyp, hyps, 0
 	 in
 	 let loc, k = evar_source id isevars in
-	 let opacity = match k with QuestionMark o -> o | _ -> true in
-	 let opaque = if not opacity || chop <> fs then None else Some chop in
-	 let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in
-	   y' :: l) 
+	 let status = match k with QuestionMark o -> Some o | _ -> status in
+	 let status, chop = match status with 
+	   | Some (Define true as stat) ->
+	       if chop <> fs then Define false, None 
+	       else stat, Some chop
+	   | Some s -> s, None
+	   | None -> Define true, None
+	 in
+	 let tac = match ev.evar_extra with 
+	   | Some t -> 
+	       if Dyn.tag t = "tactic" then 
+		 Some (Tacinterp.globTacticIn (Tacinterp.tactic_out t))
+	       else None
+	   | None -> None
+	 in
+	 let info = { ev_name = (n, nstr);
+		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
+		      ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
+	 in (id, info) :: l) 
       evn []
   in 
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
@@ -167,28 +206,16 @@ let eterm_obligations env name isevars evm fs t ty =
   in
   let ty, _, _ = subst_evar_constr evts 0 ty in
   let evars = 
-    List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) -> 
-      name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
-  in
-    (try
-       trace (str "Term constructed in eterm" ++ spc () ++
-		Termops.print_constr_env (Global.env ()) t');
-       ignore(iter
-		(fun (name, typ, _, _, deps) ->
-		   trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
-			    Termops.print_constr_env (Global.env ()) typ))
-		evars);
-     with _ -> ());
-    Array.of_list (List.rev evars), t', ty
+    List.map (fun (_, info) ->
+      let { ev_name = (_, name); ev_status = status;
+	    ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
+      in
+      let status = match status with
+	| Define true when Idset.mem name transparent -> Define false
+	| _ -> status
+      in name, typ, loc, status, deps, tac) evts
+  in Array.of_list (List.rev evars), t', ty
 
 let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n
 
-(* let eterm evm t (tycon : types option) =  *)
-(*   let t, tycon, evs = eterm_term evm t tycon in *)
-(*     match tycon with *)
-(* 	Some typ -> Tactics.apply_term (mkCast (t, DEFAULTcast, typ)) [] *)
-(*       | None -> Tactics.apply_term t (mkMetas (List.length evs)) *)
-     
-(* open Tacmach *)
-
 let etermtac (evm, t) = assert(false) (*eterm evm t None *)