source: src/common/AST.ma @ 1872

Last change on this file since 1872 was 1872, checked in by campbell, 8 years ago

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

File size: 22.6 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * This file defines a number of data types and operations used in
17  the abstract syntax trees of many of the intermediate languages. *)
18
19include "basics/types.ma".
20include "common/Integers.ma".
21include "common/Floats.ma".
22include "ASM/Arithmetic.ma".
23include "common/Identifiers.ma".
24
25
26(* * * Syntactic elements *)
27
28(* Global variables and functions are represented by identifiers with the
29   tag for symbols.  Note that Clight also uses them for locals due to
30   the ambiguous syntax. *)
31
32axiom SymbolTag : String.
33
34definition ident ≝ identifier SymbolTag.
35
36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
37
38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
39
40definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
41
42(* dpm: not needed
43inductive quantity: Type[0] ≝
44  | q_int: Byte → quantity
45  | q_offset: quantity
46  | q_ptr: quantity.
47 
48inductive abstract_size: Type[0] ≝
49  | size_q: quantity → abstract_size
50  | size_prod: list abstract_size → abstract_size
51  | size_sum: list abstract_size → abstract_size
52  | size_array: nat → abstract_size → abstract_size.
53*)
54
55
56(* Memory spaces *)
57
58inductive region : Type[0] ≝
59  | Any : region
60  | Data : region
61  | IData : region
62  | PData : region
63  | XData : region
64  | Code : region.
65
66definition eq_region : region → region → bool ≝
67λr1,r2.
68  match r1 with
69  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
70  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
71  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
72  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
73  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
74  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
75  ].
76
77lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
78  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
79  P (eq_region r1 r2).
80#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
81try ( @Ptrue // )
82@Pfalse % #E destruct
83qed.
84
85lemma reflexive_eq_region: ∀r. eq_region r r = true.
86 * //
87qed.
88
89definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
90#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
91
92(* Carefully defined to be convertably nonzero *)
93definition size_pointer : region → nat ≝
94λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
95
96(* We maintain some reasonable type information through the front end of the
97   compiler. *)
98
99inductive signedness : Type[0] ≝
100  | Signed: signedness
101  | Unsigned: signedness.
102
103inductive intsize : Type[0] ≝
104  | I8: intsize
105  | I16: intsize
106  | I32: intsize.
107
108(* * Float types come in two sizes: 32 bits (single precision)
109  and 64-bit (double precision). *)
110
111inductive floatsize : Type[0] ≝
112  | F32: floatsize
113  | F64: floatsize.
114
115inductive typ : Type[0] ≝
116  | ASTint : intsize → signedness → typ
117  | ASTptr : region → typ
118  | ASTfloat : floatsize → typ.
119
120(* XXX aliases *)
121definition SigType ≝ typ.
122definition SigType_Int ≝ ASTint I32 Unsigned.
123(*
124| SigType_Float: SigType
125*)
126definition SigType_Ptr ≝ ASTptr Any.
127
128(* Define these carefully so that we always know that the result is nonzero,
129   and can be used in dependent types of the form (S n).
130   (At the time of writing this is only used for bitsize_of_intsize.) *)
131
132definition size_intsize : intsize → nat ≝
133λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
134
135definition bitsize_of_intsize : intsize → nat ≝
136λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
137
138definition eq_intsize : intsize → intsize → bool ≝
139λsz1,sz2.
140  match sz1 with
141  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
142  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
143  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
144  ].
145
146lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
147  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
148* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
149qed.
150
151lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
152* @refl
153qed.
154
155lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
156* * * #NE try @refl @False_ind @NE @refl
157qed.
158
159definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
160 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
161λsg1,sg2,P.
162match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
163[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
164| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
165].
166
167let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
168  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
169match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
170[ I8  ⇒ λx. match sz2 return λsz. P ?? sz ? → P I8 ? sz ? with [ I8  ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
171| I16 ⇒ λx. match sz2 return λsz. P I16 sg1 sz sg2 → P I16 sg1 sz sg2 with [ I16 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
172| I32 ⇒ λx. match sz2 return λsz. P I32 sg1 sz sg2 → P I32 sg1 sz sg2 with [ I32 ⇒ signedness_check sg1 sg2 (λs1,s2. P ? s1 ? s2) x | _ ⇒ λd. d ]
173].
174
175let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
176  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
177match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
178[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
179| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
180| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
181].
182
183(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
184   if it is returns [e1] where the type of [n] has its dependency on [sz1]
185   changed to [sz2], and if not returns [e2]. *)
186let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
187  P sz1 → (P sz2 → A) → A → A ≝
188match sz1 return λsz. P sz → (P sz2 → A) → A → A with
189[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
190| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
191| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
192].
193
194lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
195  intsize_eq_elim A sz sz P p f d = f p.
196#A * //
197qed.
198
199lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
200  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
201#A * * #P #p #f #d #Q #Hne #Heq
202[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
203| *: whd in ⊢ (?%); @Hne % #E destruct
204] qed.
205
206
207(* A type for the integers that appear in the semantics. *)
208definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
209
210definition repr : ∀sz:intsize. nat → bvint sz ≝
211λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
212
213definition size_floatsize : floatsize → nat ≝
214λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
215
216let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
217  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
218match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
219[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
220| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
221].
222
223
224definition typesize : typ → nat ≝ λty.
225  match ty with
226  [ ASTint sz _ ⇒ size_intsize sz
227  | ASTptr r ⇒ size_pointer r
228  | ASTfloat sz ⇒ size_floatsize sz ].
229
230lemma typesize_pos: ∀ty. typesize ty > 0.
231*; try *; try * /2 by le_n/ qed.
232
233lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
234* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
235qed.
236
237lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
238#t1 #t2 cases t1 cases t2
239[ %1 @refl
240| 2,3: #ty %2 % #H destruct
241| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
242]
243qed.
244
245(* * Additionally, function definitions and function calls are annotated
246  by function signatures indicating the number and types of arguments,
247  as well as the type of the returned value if any.  These signatures
248  are used in particular to determine appropriate calling conventions
249  for the function. *)
250
251record signature : Type[0] ≝ {
252  sig_args: list typ;
253  sig_res: option typ
254}.
255
256(* XXX aliases *)
257definition Signature ≝ signature.
258definition signature_args ≝ sig_args.
259definition signature_return ≝ sig_res.
260
261definition proj_sig_res : signature → typ ≝ λs.
262  match sig_res s with
263  [ None ⇒ ASTint I32 Unsigned
264  | Some t ⇒ t
265  ].
266
267(* * Initialization data for global variables. *)
268
269inductive init_data: Type[0] ≝
270  | Init_int8: bvint I8 → init_data
271  | Init_int16: bvint I16 → init_data
272  | Init_int32: bvint I32 → init_data
273  | Init_float32: float → init_data
274  | Init_float64: float → init_data
275  | Init_space: nat → init_data
276  | Init_null: region → init_data
277  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
278
279(* * Whole programs consist of:
280- a collection of function definitions (name and description);
281- the name of the ``main'' function that serves as entry point in the program;
282- a collection of global variable declarations, consisting of
283  a name, initialization data, and additional information.
284
285The type of function descriptions and that of additional information
286for variables vary among the various intermediate languages and are
287taken as parameters to the [program] type.  The other parts of whole
288programs are common to all languages. *)
289
290record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
291  prog_vars: list (ident × region × V);
292  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
293  prog_main: ident
294}.
295
296
297definition prog_funct_names ≝ λF,V. λp: program F V.
298  map ?? \fst (prog_funct … p).
299
300definition prog_var_names ≝ λF,V. λp: program F V.
301  map ?? (λx. \fst (\fst x)) (prog_vars … p).
302
303(* * * Generic transformations over programs *)
304
305(* * We now define a general iterator over programs that applies a given
306  code transformation function to all function descriptions and leaves
307  the other parts of the program unchanged. *)
308(*
309Section TRANSF_PROGRAM.
310
311Variable A B V: Type.
312Variable transf: A -> B.
313*)
314
315definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
316λA,B,transf,l.
317  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
318
319definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
320λA,B,V,p,transf.
321  mk_program B V
322    (prog_vars A V p)
323    (transf_program ?? transf (prog_funct A V p))
324    (prog_main A V p).
325(*
326lemma transform_program_function:
327  ∀A,B,V,transf,p,i,tf.
328  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
329  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
330normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
331#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
332qed.
333*)
334(*
335End TRANSF_PROGRAM.
336
337(** The following is a variant of [transform_program] where the
338  code transformation function can fail and therefore returns an
339  option type. *)
340
341Open Local Scope error_monad_scope.
342Open Local Scope string_scope.
343
344Section MAP_PARTIAL.
345
346Variable A B C: Type.
347Variable prefix_errmsg: A -> errmsg.
348Variable f: B -> res C.
349*)
350definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
351                         list (A × B) → res (list (A × C)) ≝
352λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
353
354lemma map_partial_preserves_first:
355 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
356  map_partial … f l = OK ? l' →
357   map … \fst l = map … \fst l'.
358 #A #B #C #f #l elim l
359  [ #l' #E normalize in E; destruct %
360  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
361    [2: #err #E destruct
362    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
363      cases (map_partial … f tl) in IH ⊢ %;
364      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
365      >(IH x) // ]]
366qed.
367
368(*
369Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
370  match l with
371  | nil => OK nil
372  | (a, b) :: rem =>
373      match f b with
374      | Error msg => Error (prefix_errmsg a ++ msg)%list
375      | OK c =>
376          do rem' <- map_partial rem;
377          OK ((a, c) :: rem')
378      end
379  end.
380
381Remark In_map_partial:
382  forall l l' a c,
383  map_partial l = OK l' ->
384  In (a, c) l' ->
385  exists b, In (a, b) l /\ f b = OK c.
386Proof.
387  induction l; simpl.
388  intros. inv H. elim H0.
389  intros until c. destruct a as [a1 b1].
390  caseEq (f b1); try congruence.
391  intro c1; intros. monadInv H0.
392  elim H1; intro. inv H0. exists b1; auto.
393  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
394Qed.
395
396Remark map_partial_forall2:
397  forall l l',
398  map_partial l = OK l' ->
399  list_forall2
400    (fun (a_b: A * B) (a_c: A * C) =>
401       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
402    l l'.
403Proof.
404  induction l; simpl.
405  intros. inv H. constructor.
406  intro l'. destruct a as [a b].
407  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
408  constructor. simpl. auto. auto.
409Qed.
410
411End MAP_PARTIAL.
412
413Remark map_partial_total:
414  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
415  map_partial prefix (fun b => OK (f b)) l =
416  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
417Proof.
418  induction l; simpl.
419  auto.
420  destruct a as [a1 b1]. rewrite IHl. reflexivity.
421Qed.
422
423Remark map_partial_identity:
424  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
425  map_partial prefix (fun b => OK b) l = OK l.
426Proof.
427  induction l; simpl.
428  auto.
429  destruct a as [a1 b1]. rewrite IHl. reflexivity.
430Qed.
431
432Section TRANSF_PARTIAL_PROGRAM.
433
434Variable A B V: Type.
435Variable transf_partial: A -> res B.
436
437Definition prefix_funct_name (id: ident) : errmsg :=
438  MSG "In function " :: CTX id :: MSG ": " :: nil.
439*)
440definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
441λA,B,V,p,transf_partial.
442  do fl ← map_partial … transf_partial (prog_funct … p);
443  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
444
445(*
446Lemma transform_partial_program_function:
447  forall p tp i tf,
448  transform_partial_program p = OK tp ->
449  In (i, tf) tp.(prog_funct) ->
450  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
451Proof.
452  intros. monadInv H. simpl in H0. 
453  eapply In_map_partial; eauto.
454Qed.
455
456Lemma transform_partial_program_main:
457  forall p tp,
458  transform_partial_program p = OK tp ->
459  tp.(prog_main) = p.(prog_main).
460Proof.
461  intros. monadInv H. reflexivity.
462Qed.
463
464Lemma transform_partial_program_vars:
465  forall p tp,
466  transform_partial_program p = OK tp ->
467  tp.(prog_vars) = p.(prog_vars).
468Proof.
469  intros. monadInv H. reflexivity.
470Qed.
471
472End TRANSF_PARTIAL_PROGRAM.
473
474(** The following is a variant of [transform_program_partial] where
475  both the program functions and the additional variable information
476  are transformed by functions that can fail. *)
477
478Section TRANSF_PARTIAL_PROGRAM2.
479
480Variable A B V W: Type.
481Variable transf_partial_function: A -> res B.
482Variable transf_partial_variable: V -> res W.
483
484Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
485  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
486*)
487
488(* CSC: ad hoc lemma, move away? *)
489lemma map_fst:
490 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
491  map … \fst l = map … \fst l' →
492  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
493#A #B #C #C' #l elim l
494 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
495 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
496   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
497   >e0 in e1; normalize #H @H ]
498qed.
499
500definition transform_partial_program2 :
501 ∀A,B,V,W. ∀p: program A V.
502  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
503  →  (V → res W) → res (program B W) ≝
504λA,B,V,W,p, transf_partial_function, transf_partial_variable.
505  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
506  (*CSC: interactive mode because of dependent types *)
507  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
508  cases (map_partial … transf_partial_variable (prog_vars … p))
509  [ #vl #EQ
510    @(OK (program B W) (mk_program … vl … (prog_main … p)))
511    <(map_fst … (EQ vl (refl …))) @fl
512  | #err #_ @(Error … err)]
513qed.
514
515(*
516Lemma transform_partial_program2_function:
517  forall p tp i tf,
518  transform_partial_program2 p = OK tp ->
519  In (i, tf) tp.(prog_funct) ->
520  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
521Proof.
522  intros. monadInv H. 
523  eapply In_map_partial; eauto.
524Qed.
525
526Lemma transform_partial_program2_variable:
527  forall p tp i tv,
528  transform_partial_program2 p = OK tp ->
529  In (i, tv) tp.(prog_vars) ->
530  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
531Proof.
532  intros. monadInv H.
533  eapply In_map_partial; eauto.
534Qed.
535
536Lemma transform_partial_program2_main:
537  forall p tp,
538  transform_partial_program2 p = OK tp ->
539  tp.(prog_main) = p.(prog_main).
540Proof.
541  intros. monadInv H. reflexivity.
542Qed.
543
544End TRANSF_PARTIAL_PROGRAM2.
545
546(** The following is a relational presentation of
547  [transform_program_partial2].  Given relations between function
548  definitions and between variable information, it defines a relation
549  between programs stating that the two programs have the same shape
550  (same global names, etc) and that identically-named function definitions
551  are variable information are related. *)
552
553Section MATCH_PROGRAM.
554
555Variable A B V W: Type.
556Variable match_fundef: A -> B -> Prop.
557Variable match_varinfo: V -> W -> Prop.
558
559Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
560  match x1, x2 with
561  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
562  end.
563
564Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
565  match x1, x2 with
566  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
567  end.
568
569Definition match_program (p1: program A V) (p2: program B W) : Prop :=
570  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
571  /\ p1.(prog_main) = p2.(prog_main)
572  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
573
574End MATCH_PROGRAM.
575
576Remark transform_partial_program2_match:
577  forall (A B V W: Type)
578         (transf_partial_function: A -> res B)
579         (transf_partial_variable: V -> res W)
580         (p: program A V) (tp: program B W),
581  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
582  match_program
583    (fun fd tfd => transf_partial_function fd = OK tfd)
584    (fun info tinfo => transf_partial_variable info = OK tinfo)
585    p tp.
586Proof.
587  intros. monadInv H. split.
588  apply list_forall2_imply with
589    (fun (ab: ident * A) (ac: ident * B) =>
590       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
591  eapply map_partial_forall2. eauto.
592  intros. destruct v1; destruct v2; simpl in *. auto.
593  split. auto.
594  apply list_forall2_imply with
595    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
596       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
597  eapply map_partial_forall2. eauto.
598  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
599Qed.
600*)
601(* * * External functions *)
602
603(* * For most languages, the functions composing the program are either
604  internal functions, defined within the language, or external functions
605  (a.k.a. system calls) that emit an event when applied.  We define
606  a type for such functions and some generic transformation functions. *)
607
608record external_function : Type[0] ≝ {
609  ef_id: ident;
610  ef_sig: signature
611}.
612
613definition ExternalFunction ≝ external_function.
614definition external_function_tag ≝ ef_id.
615definition external_function_sig ≝ ef_sig.
616
617inductive fundef (F: Type[0]): Type[0] ≝
618  | Internal: F → fundef F
619  | External: external_function → fundef F.
620
621(* Implicit Arguments External [F]. *)
622(*
623Section TRANSF_FUNDEF.
624
625Variable A B: Type.
626Variable transf: A -> B.
627*)
628definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
629λA,B,transf,fd.
630  match fd with
631  [ Internal f ⇒ Internal ? (transf f)
632  | External ef ⇒ External ? ef
633  ].
634
635(*
636End TRANSF_FUNDEF.
637
638Section TRANSF_PARTIAL_FUNDEF.
639
640Variable A B: Type.
641Variable transf_partial: A -> res B.
642*)
643
644definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
645λA,B,transf_partial,fd.
646  match fd with
647  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
648  | External ef ⇒ OK ? (External ? ef)
649  ].
650(*
651End TRANSF_PARTIAL_FUNDEF.
652*)
653
654
655
656(* Partially merged stuff derived from the prototype cerco compiler. *)
657
658(*
659definition bool_to_Prop ≝
660 λb. match b with [ true ⇒ True | false ⇒ False ].
661
662coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
663*)
664
665(* dpm: should go to standard library *)
666let rec member (i: ident) (eq_i: ident → ident → bool)
667               (g: list ident) on g: Prop ≝
668  match g with
669  [ nil ⇒ False
670  | cons hd tl ⇒
671      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
672  ].
Note: See TracBrowser for help on using the repository browser.