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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
(* $Id$ *)
open Util
open Names
open Nameops
open Libnames
open Term
open Termops
open Nametab
open Declarations
open Indtypes
open Sign
open Rawterm
open Typeops
open Entries
open Topconstr
open Pmisc
open Past
(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *)
let make_hole c = mkCast (isevar, c)
(* Tuples are defined in file Tuples.v
* and their constructors are called Build_tuple_n or exists_n,
* wether they are dependant (last element only) or not.
* If necessary, tuples are generated ``on the fly''. *)
let tuple_exists id =
try let _ = Nametab.locate (make_short_qualid id) in true
with Not_found -> false
let ast_set = CSort (dummy_loc,RProp Pos)
let tuple_n n =
let id = make_ident "tuple_" (Some n) in
let l1n = Util.interval 1 n in
let params =
List.map (fun i ->
(LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set)))
l1n in
let fields =
List.map
(fun i ->
let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
let id' = make_ident "T" (Some i) in
(false, Vernacexpr.AssumExpr (id, mkIdentC id')))
l1n
in
let cons = make_ident "Build_tuple_" (Some n) in
Record.definition_structure ((false, id), params, fields, cons, mk_Set)
(*s [(sig_n n)] generates the inductive
\begin{verbatim}
Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set :=
exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P).
\end{verbatim} *)
let sig_n n =
let id = make_ident "sig_" (Some n) in
let l1n = Util.interval 1 n in
let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in
let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in
let idp = make_ident "P" None in
let params =
let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in
(idp, LocalAssum typ) ::
(List.rev_map (fun id -> (id, LocalAssum mkSet)) lT)
in
let lc =
let app_sig = mkApp(mkRel (2*n+3),
Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in
let app_p = mkApp(mkRel (n+1),
Array.init n (fun i -> mkRel (n-i))) in
let c = mkArrow app_p app_sig in
List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c
in
let cname = make_ident "exist_" (Some n) in
Declare.declare_mind
{ mind_entry_finite = true;
mind_entry_inds =
[ { mind_entry_params = params;
mind_entry_typename = id;
mind_entry_arity = mkSet;
mind_entry_consnames = [ cname ];
mind_entry_lc = [ lc ] } ] }
(*s On the fly generation of needed (possibly dependent) tuples. *)
let check_product_n n =
if n > 2 then
let s = Printf.sprintf "tuple_%d" n in
if not (tuple_exists (id_of_string s)) then tuple_n n
let check_dep_product_n n =
if n > 1 then
let s = Printf.sprintf "sig_%d" n in
if not (tuple_exists (id_of_string s)) then ignore (sig_n n)
(*s Constructors for the tuples. *)
let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1)
let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1)
let tuple_ref dep n =
if n = 2 & not dep then
pair
else
let n = n - (if dep then 1 else 0) in
if dep then
if n = 1 then
exist
else begin
let id = make_ident "exist_" (Some n) in
if not (tuple_exists id) then ignore (sig_n n);
Nametab.locate (make_short_qualid id)
end
else begin
let id = make_ident "Build_tuple_" (Some n) in
if not (tuple_exists id) then tuple_n n;
Nametab.locate (make_short_qualid id)
end
(* Binders. *)
let trad_binder avoid nenv id = function
| CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
| CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
let rec push_vars avoid nenv = function
| [] -> ([],avoid,nenv)
| (id,b) :: bl ->
let b' = trad_binder avoid nenv id b in
let bl',avoid',nenv' =
push_vars (id :: avoid) (add_name (Name id) nenv) bl
in
((id,b') :: bl', avoid', nenv')
let rec raw_lambda bl v = match bl with
| [] ->
v
| (id,ty) :: bl' ->
RLambda (dummy_loc, Name id, ty, raw_lambda bl' v)
(* The translation itself is quite easy.
letin are translated into Cases constructions *)
let rawconstr_of_prog p =
let rec trad avoid nenv = function
| CC_var id ->
RVar (dummy_loc, id)
(*i optimisation : let x = <constr> in e2 => e2[x<-constr]
| CC_letin (_,_,[id,_],CC_expr c,e2) ->
real_subst_in_constr [id,c] (trad e2)
| CC_letin (_,_,([_] as b),CC_expr e1,e2) ->
let (b',avoid',nenv') = push_vars avoid nenv b in
let c1 = Detyping.detype avoid nenv e1
and c2 = trad avoid' nenv' e2 in
let id = Name (fst (List.hd b')) in
RLetIn (dummy_loc, id, c1, c2)
i*)
| CC_letin (_,_,([_] as b),e1,e2) ->
let (b',avoid',nenv') = push_vars avoid nenv b in
let c1 = trad avoid nenv e1
and c2 = trad avoid' nenv' e2 in
RApp (dummy_loc, raw_lambda b' c2, [c1])
| CC_letin (dep,ty,bl,e1,e2) ->
let (bl',avoid',nenv') = push_vars avoid nenv bl in
let c1 = trad avoid nenv e1
and c2 = trad avoid' nenv' e2 in
ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None)
| CC_lam (bl,e) ->
let bl',avoid',nenv' = push_vars avoid nenv bl in
let c = trad avoid' nenv' e in
raw_lambda bl' c
| CC_app (f,args) ->
let c = trad avoid nenv f
and cargs = List.map (trad avoid nenv) args in
RApp (dummy_loc, c, cargs)
| CC_tuple (_,_,[e]) ->
trad avoid nenv e
| CC_tuple (false,_,[e1;e2]) ->
let c1 = trad avoid nenv e1
and c2 = trad avoid nenv e2 in
RApp (dummy_loc, RRef (dummy_loc,pair),
[RHole (dummy_loc,ImplicitArg (pair,1));
RHole (dummy_loc,ImplicitArg (pair,2));c1;c2])
| CC_tuple (dep,tyl,l) ->
let n = List.length l in
let cl = List.map (trad avoid nenv) l in
let tuple = tuple_ref dep n in
let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
let args = tyl @ cl in
RApp (dummy_loc, RRef (dummy_loc, tuple), args)
| CC_case (ty,b,el) ->
let c = trad avoid nenv b in
let cl = List.map (trad avoid nenv) el in
let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
| CC_expr c ->
Detyping.detype (false,Global.env()) avoid nenv c
| CC_hole c ->
RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
Detyping.detype (false,Global.env()) avoid nenv c)
in
trad [] empty_names_context p
|
