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
|
(**
- 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 Sutils
open Evd
open List
open Pp
(** Substitute evar references in t using De Bruijn indices,
where n binders were passed through. *)
let subst_evars evs n t =
let evar_index id =
let idx = list_assoc_index id evs in
idx + 1
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
(try
msgnl (str "Evar " ++ int k ++ str " found");
let ex =
(* mkVar (id_of_string ("Evar" ^ string_of_int k));*)
mkRel (evar_index k + depth)
in
let args = Array.map (map_constr_with_binders succ substrec depth) args in
mkApp (ex, args)
with Not_found ->
msgnl (str "Evar " ++ int k ++ str " not found!!!");
c)
| _ -> map_constr_with_binders succ substrec depth c
in
substrec 0 t
(** 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 =
let idx = list_index id acc in
idx + 1
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 De Bruijn indices.
*)
let etype_of_evar evs ev =
let rec aux acc n = function
(id, copt, t) :: tl ->
let t' = subst_evars evs n t in
let t'' = subst_vars acc 0 t' in
mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
| [] ->
let t' = subst_evars evs n ev.evar_concl in
subst_vars acc 0 t'
in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps))
open Tacticals
let eterm evm t =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
let evl = to_list evm in
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_left
(fun l (id, y) ->
let y' = (id, etype_of_evar l y) in
y' :: l)
[] evl
in
let t' = (* Substitute evar refs in the term to De Bruijn indices *)
subst_evars evts 0 t
in
let t'' =
(* Make the lambdas 'generalizing' the existential variables *)
fold_left
(fun acc (id, c) ->
mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
c, acc))
t' evts
in
let declare_evar (id, c) =
let id = id_of_string ("Evar" ^ string_of_int id) in
ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
Decl_kinds.IsAssumption Decl_kinds.Definitional))
in
let declare_assert acc (id, c) =
let id = id_of_string ("Evar" ^ string_of_int id) in
tclTHEN acc (Tactics.assert_tac false (Name id) c)
in
msgnl (str "Term constructed in Eterm" ++
Termops.print_constr_env (Global.env ()) t'');
Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts)
(* t'' *)
(* Hack: push evars as assumptions in the global env *)
(* iter declare_evar evts; *)
(* Tactics.apply t' *)
(*tclTHEN (fold_left declare_assert tclIDTAC evts) (Tactics.apply t')*)
open Tacmach
let etermtac (evm, t) =
let t' = eterm evm t in
t'
(* Tactics.apply (Reduction.nf_betaiota t')
Tactics.exact (Reduction.nf_betaiota t')*)
|
