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
|
(***********************************************************************)
(* 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 Ptype
open Past
open Penv
let cci_global id =
try
Declare.global_reference id
with
_ -> raise Not_found
let lookup_var ids locop id =
if List.mem id ids then
None
else begin
try Some (cci_global id)
with Not_found -> Perror.unbound_variable id locop
end
let check_ref idl loc id =
if (not (List.mem id idl)) & (not (Penv.is_global id)) then
Perror.unbound_reference id loc
(* db types : only check the references for the moment *)
let rec check_type_v refs = function
| Ref v ->
check_type_v refs v
| Array (c,v) ->
check_type_v refs v
| Arrow (bl,c) ->
check_binder refs c bl
| TypePure _ ->
()
and check_type_c refs ((_,v),e,_,_) =
check_type_v refs v;
List.iter (check_ref refs None) (Peffect.get_reads e);
List.iter (check_ref refs None) (Peffect.get_writes e)
(* TODO: check_condition on p and q *)
and check_binder refs c = function
| [] ->
check_type_c refs c
| (id, BindType (Ref _ | Array _ as v)) :: bl ->
check_type_v refs v;
check_binder (id :: refs) c bl
| (_, BindType v) :: bl ->
check_type_v refs v;
check_binder refs c bl
| _ :: bl ->
check_binder refs c bl
(* db binders *)
let rec db_binders ((tids,pids,refs) as idl) = function
| [] ->
idl, []
| (id, BindType (Ref _ | Array _ as v)) as b :: rem ->
check_type_v refs v;
let idl',rem' = db_binders (tids,pids,id::refs) rem in
idl', b :: rem'
| (id, BindType v) as b :: rem ->
check_type_v refs v;
let idl',rem' = db_binders (tids,id::pids,refs) rem in
idl', b :: rem'
| ((id, BindSet) as t) :: rem ->
let idl',rem' = db_binders (id::tids,pids,refs) rem in
idl', t :: rem'
| a :: rem ->
let idl',rem' = db_binders idl rem in idl', a :: rem'
(* db patterns *)
let rec db_pattern = function
| (PatVar id) as t ->
(try
(match Nametab.sp_of_id CCI id with
| ConstructRef (x,y) -> [], PatConstruct (id,(x,y))
| _ -> [id],t)
with Not_found -> [id],t)
| PatAlias (p,id) ->
let ids,p' = db_pattern p in ids,PatAlias (p',id)
| PatPair (p1,p2) ->
let ids1,p1' = db_pattern p1 in
let ids2,p2' = db_pattern p2 in
ids1@ids2, PatPair (p1',p2')
| PatApp pl ->
let ids,pl' =
List.fold_right
(fun p (ids,pl) ->
let ids',p' = db_pattern p in ids'@ids,p'::pl) pl ([],[]) in
ids,PatApp pl'
| PatConstruct _ ->
assert false (* constructor in a pattern after parsing ! *)
(* db programs *)
let db_prog e =
(* tids = type identifiers, ids = variables, refs = references and arrays *)
let rec db_desc ((tids,ids,refs) as idl) = function
| (Var x) as t ->
(match lookup_var ids (Some e.loc) x with
None -> t
| Some c -> Expression c)
| (Acc x) as t ->
check_ref refs (Some e.loc) x;
t
| Aff (x,e1) ->
check_ref refs (Some e.loc) x;
Aff (x, db idl e1)
| TabAcc (b,x,e1) ->
check_ref refs (Some e.loc) x;
TabAcc(b,x,db idl e1)
| TabAff (b,x,e1,e2) ->
check_ref refs (Some e.loc) x;
TabAff (b,x, db idl e1, db idl e2)
| Seq bl ->
Seq (List.map (function
Statement p -> Statement (db idl p)
| x -> x) bl)
| If (e1,e2,e3) ->
If (db idl e1, db idl e2, db idl e3)
| While (b,inv,var,bl) ->
let bl' = List.map (function
Statement p -> Statement (db idl p)
| x -> x) bl in
While (db idl b, inv, var, bl')
| Lam (bl,e) ->
let idl',bl' = db_binders idl bl in Lam(bl', db idl' e)
| App (e1,l) ->
App (db idl e1, List.map (db_arg idl) l)
| SApp (dl,l) ->
SApp (dl, List.map (db idl) l)
| LetRef (x,e1,e2) ->
LetRef (x, db idl e1, db (tids,ids,x::refs) e2)
| LetIn (x,e1,e2) ->
LetIn (x, db idl e1, db (tids,x::ids,refs) e2)
| LetRec (f,bl,v,var,e) ->
let (tids',ids',refs'),bl' = db_binders idl bl in
check_type_v refs' v;
LetRec (f, bl, v, var, db (tids',f::ids',refs') e)
| Debug (s,e1) ->
Debug (s, db idl e1)
| Expression _ as x -> x
| PPoint (s,d) -> PPoint (s, db_desc idl d)
and db_arg ((tids,_,refs) as idl) = function
| Term ({ desc = Var id } as t) ->
if List.mem id refs then Refarg id else Term (db idl t)
| Term t -> Term (db idl t)
| Type v as ty -> check_type_v refs v; ty
| Refarg _ -> assert false
and db idl e =
{ desc = db_desc idl e.desc ;
pre = e.pre; post = e.post;
loc = e.loc; info = e.info }
in
let ids = Sign.ids_of_named_context (Global.named_context ()) in
(* TODO: separer X:Set et x:V:Set
virer le reste (axiomes, etc.) *)
let vars,refs = all_vars (), all_refs () in
db ([],vars@ids,refs) e
;;
|
