summaryrefslogtreecommitdiff
path: root/contrib/subtac/eterm.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /contrib/subtac/eterm.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'contrib/subtac/eterm.ml')
-rw-r--r--contrib/subtac/eterm.ml121
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 *)