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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn
open Topconstr
open Subtac_coercion
open Scoq
open Coqlib
open Printer
open Subtac_errors
open Context
open Eterm
let mkAppExplC (f, args) = CAppExpl (dummy_loc, (None, f), args)
let mkSubset name typ prop =
mkAppExplC (sig_ref,
[ typ; mkLambdaC ([name], typ, prop) ])
let mkProj1 u p x =
mkAppExplC (proj1_sig_ref, [ u; p; x ])
let mkProj2 u p x =
mkAppExplC (proj2_sig_ref, [ u; p; x ])
let list_of_local_binders l =
let rec aux acc = function
Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, c) :: acc) tl
| Topconstr.LocalRawAssum (nl, c) :: tl ->
aux (List.fold_left (fun acc n -> (n, c) :: acc) acc nl) tl
| [] -> List.rev acc
in aux [] l
let abstract_constr_expr_bl c bl =
List.fold_right (fun (n, t) c -> mkLambdaC ([n], t, c)) bl c
let pr_binder_list b =
List.fold_right (fun ((loc, name), t) acc -> Nameops.pr_name name ++ str " : " ++
Ppconstr.pr_constr_expr t ++ spc () ++ acc) b (mt ())
let rec rewrite_rec_calls l c = c
let rewrite_fixpoint env l (f, decl) =
let (id, (n, ro), bl, typ, body) = f in
let body = rewrite_rec_calls l body in
match ro with
CStructRec -> ((id, (n, ro), bl, typ, body), decl)
| CWfRec wfrel ->
let bls = list_of_local_binders bl in
let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id id ++
Ppconstr.pr_binders bl ++ str " : " ++
Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
Ppconstr.pr_constr_expr body)
in
let after, before = list_chop n bls in
let _ = trace (str "Binders before the recursion arg: " ++ spc () ++
pr_binder_list before ++ str "; after the recursion arg: " ++
pr_binder_list after)
in
let ((locn, name), ntyp), before = match before with
hd :: tl -> hd, tl
| _ -> assert(false) (* Rec arg must be in before *)
in
let nid = match name with
Name id -> id
| Anonymous -> assert(false) (* Rec arg _must_ be named *)
in
let _wfproof =
let _wf_rel = mkAppExplC (well_founded_ref, [ntyp; wfrel]) in
(*make_existential_expr dummy_loc before wf_rel*)
mkRefC lt_wf_ref
in
let nid', accproofid =
let nid = string_of_id nid in
id_of_string (nid ^ "'"), id_of_string ("Acc_" ^ nid)
in
let lnid', laccproofid = (dummy_loc, Name nid'), (dummy_loc, Name accproofid) in
let coqP = abstract_constr_expr_bl typ after in
let body' =
let prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
let lamprop = mkLambdaC ([lnid'], ntyp, prop) in
let typnid' = mkSubset lnid' ntyp prop in
let body' = (* body abstracted by rec call *)
mkLambdaC ([(dummy_loc, Name id)],
mkProdC ([lnid'], typnid', coqP),
body)
in
mkAppC (body',
[mkLambdaC
([lnid'], typnid',
mkAppC (mkIdentC id,
[mkProj1 ntyp lamprop (mkIdentC nid');
(mkAppExplC (acc_inv_ref,
[ ntyp; wfrel;
mkIdentC nid;
mkIdentC accproofid;
mkProj1 ntyp lamprop (mkIdentC nid');
mkProj2 ntyp lamprop (mkIdentC nid') ])) ]))])
in
let acctyp = mkAppExplC (acc_ref, [ ntyp; wfrel; mkIdentC nid ]) in
let bl' =
let rec aux acc = function
Topconstr.LocalRawDef _ as x :: tl ->
aux (x :: acc) tl
| Topconstr.LocalRawAssum (bl, typ) as assum :: tl ->
let rec aux' bl' = function
((loc, name') as x) :: tl ->
if name' = name then
LocalRawAssum (List.rev (x :: bl'), typ) ::
LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
if tl = [] then [] else [LocalRawAssum (tl, typ)]
else aux' (x :: bl') tl
| [] -> [assum]
in aux (acc @ List.rev (aux' [] bl)) tl
| [] -> List.rev acc
in aux [] bl
in
let _ = trace (str "Rewrote fixpoint: " ++ Ppconstr.pr_id id ++
Ppconstr.pr_binders bl' ++ str " : " ++
Ppconstr.pr_constr_expr typ ++ str " := " ++ spc () ++
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
let list_mapi f =
let rec aux i = function
hd :: tl -> f i hd :: aux (succ i) tl
| [] -> []
in aux 0
let rewrite_cases_aux (loc, po, tml, eqns) =
let tml = list_mapi (fun i (c, (n, opt)) -> c,
((match n with
Name id -> (match c with
| RVar (_, id') when id = id' ->
Name (id_of_string (string_of_id id ^ "'"))
| _ -> n)
| Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
opt)) tml
in
let mkHole = RHole (dummy_loc, InternalHole) in
let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
[mkHole; c; n])
in
let eqs_types =
List.map
(fun (c, (n, _)) ->
let id = match n with Name id -> id | _ -> assert false in
let heqid = id_of_string ("Heq" ^ string_of_id id) in
Name heqid, mkeq c (RVar (dummy_loc, id)))
tml
in
let po =
List.fold_right
(fun (n,t) acc ->
RProd (dummy_loc, n, t, acc))
eqs_types (match po with
Some e -> e
| None -> mkHole)
in
let eqns =
List.map (fun (loc, idl, cpl, c) ->
let c' =
List.fold_left
(fun acc (n, t) ->
RLambda (dummy_loc, n, t, acc))
c eqs_types
in (loc, idl, cpl, c'))
eqns
in
let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
[mkHole; c])
in
let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
let case = RCases (loc,Some po,tml,eqns) in
let app = RApp (dummy_loc, case, refls) in
app
let rec rewrite_cases c =
match c with
RCases _ -> let c' = map_rawconstr rewrite_cases c in
(match c' with
| RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
| _ -> assert(false))
| _ -> map_rawconstr rewrite_cases c
|
