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
|
(**
- 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
let reverse_array arr =
Array.of_list (List.rev (Array.to_list arr))
(** Utilities to find indices in lists *)
let list_index x l =
let rec aux i = function
k :: tl -> if k = x then i else aux (succ i) tl
| [] -> raise Not_found
in aux 0 l
let list_assoc_index x l =
let rec aux i = function
(k, v) :: tl -> if k = x then i else aux (succ i) tl
| [] -> raise Not_found
in aux 0 l
(** 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
(* Evar arguments are created in inverse order *)
let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in
mkApp (ex, Array.of_list 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 by 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 t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts)
open Tacmach
let etermtac (evm, t) = eterm evm t
|
