1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
|
(**
- Get types of existentials ;
- Flatten dependency tree (prefix order) ;
- Replace existentials by De Bruijn indices in term, applied to the right arguments ;
- Apply term prefixed by quantification on "existentials".
*)
open Term
open Names
open Evd
open List
open Pp
open Util
open Subtac_utils
let trace s =
if !Options.debug then (msgnl s; msgerr s)
else ()
(** 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 evar_info id = List.assoc id evs in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
let (id, idstr), hyps, chop, _, _ =
try evar_info k
with Not_found ->
anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
in
seen := Intset.add id !seen;
(* Evar arguments are created in inverse order,
and we must not apply to defined ones (i.e. LetIn's)
*)
let args =
let n = match chop with None -> 0 | Some c -> c in
let (l, r) = list_chop n (List.rev (Array.to_list args)) in
List.rev r
in
let args =
let rec aux hyps args acc =
match hyps, args with
((_, None, _) :: tlh), (c :: tla) ->
aux tlh tla ((map_constr_with_binders succ substrec depth 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 _ -> ());
mkApp (mkVar idstr, Array.of_list args)
| _ -> map_constr_with_binders succ substrec depth c
in
let t' = substrec 0 t in
t', !seen
(** Substitute variable references in t using De Bruijn indices,
where n binders were passed through. *)
let subst_vars acc n t =
let var_index id = Util.list_index id acc in
let rec substrec depth c = match kind_of_term c with
| Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
| _ -> map_constr_with_binders succ substrec depth c
in
substrec 0 t
(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
to a product : forall H1 : t1, ..., forall Hn : tn, concl.
Changes evars and hypothesis references to variable references.
A little optimization: don't include unnecessary let-ins and their dependencies.
*)
let etype_of_evar evs hyps concl =
let rec aux acc n = function
(id, copt, t) :: tl ->
let t', s = subst_evar_constr evs n t in
let t'' = subst_vars acc 0 t' in
let rest, s' = aux (id :: acc) (succ n) tl in
let s' = Intset.union s s' in
(match copt with
Some c ->
if noccurn 1 rest then lift (-1) rest, s'
else
let c', s'' = subst_evar_constr evs n c in
let c' = subst_vars acc 0 c' in
mkNamedProd_or_LetIn (id, Some c', t'') rest, Intset.union s'' s'
| None ->
mkNamedProd_or_LetIn (id, None, t'') rest, s')
| [] ->
let t', s = subst_evar_constr evs n concl in
subst_vars acc 0 t', s
in aux [] 0 (rev hyps)
open Tacticals
let trunc_named_context n ctx =
let len = List.length ctx in
list_firstn (len - n) ctx
let rec chop_product n t =
if n = 0 then Some t
else
match kind_of_term t with
| Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
| _ -> None
let eterm_obligations name nclen isevars evm fs t tycon =
(* '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 evl = List.rev (to_list evm) in
let evn =
let i = ref (-1) in
List.rev_map (fun (id, ev) -> incr i;
(id, (!i, id_of_string
(string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
ev)) evl
in
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_right
(fun (id, (n, nstr), ev) l ->
let hyps = Environ.named_context_of_val ev.evar_hyps in
let hyps = trunc_named_context nclen hyps in
let evtyp, deps = 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
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, evtyp, deps)) in
y' :: l)
evn []
in
let t', _ = (* Substitute evar refs in the term by variables *)
subst_evar_constr evts 0 t
in
let evars =
List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None), 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'
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 *)
|
