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
|
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 Subtac_utils
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 abs c bl =
List.fold_right (fun (n, t) c -> abs ([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 before, after = 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) as lnid, ntyp), after = match after with
hd :: tl -> hd, tl
| _ -> assert(false) (* Rec arg must be in after *)
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 wf_prop = (mkAppC (wfrel, [ mkIdentC nid'; mkIdentC nid ])) in
let lam_wf_prop = mkLambdaC ([lnid'], ntyp, wf_prop) in
let typnid' = mkSubset lnid' ntyp wf_prop in
let internal_type =
abstract_constr_expr_bl mkProdC
(mkProdC ([lnid'], typnid',
mkLetInC (lnid, mkProj1 ntyp lam_wf_prop (mkIdentC nid'),
abstract_constr_expr_bl mkProdC typ after)))
before
in
let body' =
let body =
(* cast or we will loose some info at pretyping time as body
is a function *)
CCast (dummy_loc, body, CastConv DEFAULTcast, typ)
in
let body' = (* body abstracted by rec call *)
mkLambdaC ([(dummy_loc, Name id)], internal_type, body)
in
mkAppC (body',
[mkLambdaC
([lnid'], typnid',
mkAppC (mkIdentC id,
[mkProj1 ntyp lam_wf_prop (mkIdentC nid');
(mkAppExplC (acc_inv_ref,
[ ntyp; wfrel;
mkIdentC nid;
mkIdentC accproofid;
mkProj1 ntyp lam_wf_prop (mkIdentC nid');
mkProj2 ntyp lam_wf_prop (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
(if tl = [] then [] else [LocalRawAssum (tl, typ)]) @
LocalRawAssum ([(dummy_loc, Name accproofid)], acctyp) ::
[LocalRawAssum (List.rev (x :: bl'), typ)]
else aux' (x :: bl') tl
| [] -> [assum]
in aux (aux' [] bl @ acc) 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
*)
|
