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
|
(***********************************************************************)
(* 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 Names
open Term
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.sp_of_id CCI id in true with Not_found -> false
let ast_set = Ast.ope ("PROP", [ Ast.ide "Pos" ])
let tuple_n n =
let name = "tuple_" ^ string_of_int n in
let id = id_of_string name in
let l1n = Util.interval 1 n in
let params =
List.map
(fun i -> let id = id_of_string ("T" ^ string_of_int i) in (id, ast_set))
l1n
in
let fields =
List.map
(fun i ->
let id = id_of_string
("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
(false, (id, true, Ast.nvar ("T" ^ string_of_int i))))
l1n
in
let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
Record.definition_structure (false, id, params, fields, cons, mk_Set)
let sig_n n =
let name = "sig_" ^ string_of_int n in
let id = id_of_string name in
let l1n = Util.interval 1 n in
let lT =
List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in
let lx =
List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in
let ty_p = List.fold_right (fun ti c -> mkArrow (mkVar ti) c) lT mkProp in
let arity =
let ar =
List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT
(mkArrow ty_p mkSet) in
mkCast (ar, mkType Univ.prop_univ)
in
let idp = id_of_string "P" in
let lc =
let app_sig =
let l =
(mkRel (2*n+3)) :: (List.map (fun id -> (mkVar id)) lT) @ [mkVar idp]
in
mkAppA (Array.of_list l) in
let app_p =
let l = (mkVar idp) :: (List.map (fun id -> mkVar id) lx) in
mkAppA (Array.of_list l) in
let c = mkArrow app_p app_sig in
let c = List.fold_right (fun (x,tx) c -> mkNamedProd x (mkVar tx) c)
(List.combine lx lT) c in
let c = mkNamedProd idp ty_p c in
let c = List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT c in
DLAMV (Name id, [| c |])
in
let cname = id_of_string ("exist_" ^ string_of_int n) in
Declare.machine_minductive (Termenv.initial_assumptions()) (succ n)
[| id, Anonymous, arity, lc, [| cname |] |] true
let tuple_name 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 name = Printf.sprintf "exist_%d" n in
if not (tuple_exists (id_of_string name)) then sig_n n;
name
end
else begin
let name = Printf.sprintf "Build_tuple_%d" n in
if not (tuple_exists (id_of_string name)) then tuple_n n;
name
end
(* Binders. *)
let trad_binding bl =
List.map (function
(id,CC_untyped_binder) -> (id,isevar)
| (id,CC_typed_binder ty) -> (id,ty)) bl
let lambda_of_bl bl c =
let b = trad_binding bl in n_lambda c (List.rev b)
(* The translation itself is quite easy.
letin are translated into Cases construtions *)
let constr_of_prog p =
let rec trad = function
CC_var id -> VAR id
(* 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),(e1,_),e2) ->
let c = trad e1 and c2 = trad e2 in
Term.applist (lambda_of_bl b c2, [c])
| CC_letin (dep,ty,bl,(e,info),e1) ->
let c1 = trad e1
and c = trad e in
let l = [ lambda_of_bl bl c1 ] in
Term.mkMutCase (Term.ci_of_mind info) ty c l
| CC_lam (bl,e) ->
let c = trad e in lambda_of_bl bl c
| CC_app (f,args) ->
let c = trad f
and cargs = List.map trad args in
Term.applist (c,cargs)
| CC_tuple (_,_,[e]) -> trad e
| CC_tuple (false,_,[e1;e2]) ->
let c1 = trad e1
and c2 = trad e2 in
Term.applist (constant "pair", [isevar;isevar;c1;c2])
| CC_tuple (dep,tyl,l) ->
let n = List.length l in
let cl = List.map trad l in
let name = tuple_name dep n in
let args = tyl @ cl in
Term.applist (constant name,args)
| CC_case (ty,(b,info),el) ->
let c = trad b in
let cl = List.map trad el in
mkMutCase (Term.ci_of_mind info) ty c cl
| CC_expr c -> c
| CC_hole c -> make_hole c
in
trad p
|
