source: src/common/AST.ma @ 1881

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

Fix up earlier front-end value conversion work.

File size: 22.7 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 pred_size_intsize : intsize → nat ≝
133λsz. match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
134
135definition size_intsize : intsize → nat ≝
136λsz. S (pred_size_intsize sz).
137
138definition bitsize_of_intsize : intsize → nat ≝
139λsz. size_intsize sz * 8.
140
141definition eq_intsize : intsize → intsize → bool ≝
142λsz1,sz2.
143  match sz1 with
144  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
145  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
146  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
147  ].
148
149lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
150  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
151* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
152qed.
153
154lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
155* @refl
156qed.
157
158lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
159* * * #NE try @refl @False_ind @NE @refl
160qed.
161
162definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
163 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
164λsg1,sg2,P.
165match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
166[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
167| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
168].
169
170let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
171  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
172match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
173[ 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 ]
174| 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 ]
175| 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 ]
176].
177
178let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
179  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
180match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
181[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
182| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
183| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
184].
185
186(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
187   if it is returns [e1] where the type of [n] has its dependency on [sz1]
188   changed to [sz2], and if not returns [e2]. *)
189let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
190  P sz1 → (P sz2 → A) → A → A ≝
191match sz1 return λsz. P sz → (P sz2 → A) → A → A with
192[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
193| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
194| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
195].
196
197lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
198  intsize_eq_elim A sz sz P p f d = f p.
199#A * //
200qed.
201
202lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
203  (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).
204#A * * #P #p #f #d #Q #Hne #Heq
205[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
206| *: whd in ⊢ (?%); @Hne % #E destruct
207] qed.
208
209
210(* A type for the integers that appear in the semantics. *)
211definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
212
213definition repr : ∀sz:intsize. nat → bvint sz ≝
214λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
215
216definition size_floatsize : floatsize → nat ≝
217λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
218
219let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
220  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
221match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
222[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
223| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
224].
225
226
227definition typesize : typ → nat ≝ λty.
228  match ty with
229  [ ASTint sz _ ⇒ size_intsize sz
230  | ASTptr r ⇒ size_pointer r
231  | ASTfloat sz ⇒ size_floatsize sz ].
232
233lemma typesize_pos: ∀ty. typesize ty > 0.
234*; try *; try * /2 by le_n/ qed.
235
236lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
237* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
238qed.
239
240lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
241#t1 #t2 cases t1 cases t2
242[ %1 @refl
243| 2,3: #ty %2 % #H destruct
244| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
245]
246qed.
247
248(* * Additionally, function definitions and function calls are annotated
249  by function signatures indicating the number and types of arguments,
250  as well as the type of the returned value if any.  These signatures
251  are used in particular to determine appropriate calling conventions
252  for the function. *)
253
254record signature : Type[0] ≝ {
255  sig_args: list typ;
256  sig_res: option typ
257}.
258
259(* XXX aliases *)
260definition Signature ≝ signature.
261definition signature_args ≝ sig_args.
262definition signature_return ≝ sig_res.
263
264definition proj_sig_res : signature → typ ≝ λs.
265  match sig_res s with
266  [ None ⇒ ASTint I32 Unsigned
267  | Some t ⇒ t
268  ].
269
270(* * Initialization data for global variables. *)
271
272inductive init_data: Type[0] ≝
273  | Init_int8: bvint I8 → init_data
274  | Init_int16: bvint I16 → init_data
275  | Init_int32: bvint I32 → init_data
276  | Init_float32: float → init_data
277  | Init_float64: float → init_data
278  | Init_space: nat → init_data
279  | Init_null: region → init_data
280  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
281
282(* * Whole programs consist of:
283- a collection of function definitions (name and description);
284- the name of the ``main'' function that serves as entry point in the program;
285- a collection of global variable declarations, consisting of
286  a name, initialization data, and additional information.
287
288The type of function descriptions and that of additional information
289for variables vary among the various intermediate languages and are
290taken as parameters to the [program] type.  The other parts of whole
291programs are common to all languages. *)
292
293record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
294  prog_vars: list (ident × region × V);
295  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
296  prog_main: ident
297}.
298
299
300definition prog_funct_names ≝ λF,V. λp: program F V.
301  map ?? \fst (prog_funct … p).
302
303definition prog_var_names ≝ λF,V. λp: program F V.
304  map ?? (λx. \fst (\fst x)) (prog_vars … p).
305
306(* * * Generic transformations over programs *)
307
308(* * We now define a general iterator over programs that applies a given
309  code transformation function to all function descriptions and leaves
310  the other parts of the program unchanged. *)
311(*
312Section TRANSF_PROGRAM.
313
314Variable A B V: Type.
315Variable transf: A -> B.
316*)
317
318definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
319λA,B,transf,l.
320  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
321
322definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
323λA,B,V,p,transf.
324  mk_program B V
325    (prog_vars A V p)
326    (transf_program ?? transf (prog_funct A V p))
327    (prog_main A V p).
328(*
329lemma transform_program_function:
330  ∀A,B,V,transf,p,i,tf.
331  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
332  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
333normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
334#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
335qed.
336*)
337(*
338End TRANSF_PROGRAM.
339
340(** The following is a variant of [transform_program] where the
341  code transformation function can fail and therefore returns an
342  option type. *)
343
344Open Local Scope error_monad_scope.
345Open Local Scope string_scope.
346
347Section MAP_PARTIAL.
348
349Variable A B C: Type.
350Variable prefix_errmsg: A -> errmsg.
351Variable f: B -> res C.
352*)
353definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
354                         list (A × B) → res (list (A × C)) ≝
355λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
356
357lemma map_partial_preserves_first:
358 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
359  map_partial … f l = OK ? l' →
360   map … \fst l = map … \fst l'.
361 #A #B #C #f #l elim l
362  [ #l' #E normalize in E; destruct %
363  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
364    [2: #err #E destruct
365    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
366      cases (map_partial … f tl) in IH ⊢ %;
367      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
368      >(IH x) // ]]
369qed.
370
371(*
372Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
373  match l with
374  | nil => OK nil
375  | (a, b) :: rem =>
376      match f b with
377      | Error msg => Error (prefix_errmsg a ++ msg)%list
378      | OK c =>
379          do rem' <- map_partial rem;
380          OK ((a, c) :: rem')
381      end
382  end.
383
384Remark In_map_partial:
385  forall l l' a c,
386  map_partial l = OK l' ->
387  In (a, c) l' ->
388  exists b, In (a, b) l /\ f b = OK c.
389Proof.
390  induction l; simpl.
391  intros. inv H. elim H0.
392  intros until c. destruct a as [a1 b1].
393  caseEq (f b1); try congruence.
394  intro c1; intros. monadInv H0.
395  elim H1; intro. inv H0. exists b1; auto.
396  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
397Qed.
398
399Remark map_partial_forall2:
400  forall l l',
401  map_partial l = OK l' ->
402  list_forall2
403    (fun (a_b: A * B) (a_c: A * C) =>
404       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
405    l l'.
406Proof.
407  induction l; simpl.
408  intros. inv H. constructor.
409  intro l'. destruct a as [a b].
410  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
411  constructor. simpl. auto. auto.
412Qed.
413
414End MAP_PARTIAL.
415
416Remark map_partial_total:
417  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
418  map_partial prefix (fun b => OK (f b)) l =
419  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
420Proof.
421  induction l; simpl.
422  auto.
423  destruct a as [a1 b1]. rewrite IHl. reflexivity.
424Qed.
425
426Remark map_partial_identity:
427  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
428  map_partial prefix (fun b => OK b) l = OK l.
429Proof.
430  induction l; simpl.
431  auto.
432  destruct a as [a1 b1]. rewrite IHl. reflexivity.
433Qed.
434
435Section TRANSF_PARTIAL_PROGRAM.
436
437Variable A B V: Type.
438Variable transf_partial: A -> res B.
439
440Definition prefix_funct_name (id: ident) : errmsg :=
441  MSG "In function " :: CTX id :: MSG ": " :: nil.
442*)
443definition 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) ≝
444λA,B,V,p,transf_partial.
445  do fl ← map_partial … transf_partial (prog_funct … p);
446  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
447
448(*
449Lemma transform_partial_program_function:
450  forall p tp i tf,
451  transform_partial_program p = OK tp ->
452  In (i, tf) tp.(prog_funct) ->
453  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
454Proof.
455  intros. monadInv H. simpl in H0. 
456  eapply In_map_partial; eauto.
457Qed.
458
459Lemma transform_partial_program_main:
460  forall p tp,
461  transform_partial_program p = OK tp ->
462  tp.(prog_main) = p.(prog_main).
463Proof.
464  intros. monadInv H. reflexivity.
465Qed.
466
467Lemma transform_partial_program_vars:
468  forall p tp,
469  transform_partial_program p = OK tp ->
470  tp.(prog_vars) = p.(prog_vars).
471Proof.
472  intros. monadInv H. reflexivity.
473Qed.
474
475End TRANSF_PARTIAL_PROGRAM.
476
477(** The following is a variant of [transform_program_partial] where
478  both the program functions and the additional variable information
479  are transformed by functions that can fail. *)
480
481Section TRANSF_PARTIAL_PROGRAM2.
482
483Variable A B V W: Type.
484Variable transf_partial_function: A -> res B.
485Variable transf_partial_variable: V -> res W.
486
487Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
488  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
489*)
490
491(* CSC: ad hoc lemma, move away? *)
492lemma map_fst:
493 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
494  map … \fst l = map … \fst l' →
495  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
496#A #B #C #C' #l elim l
497 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
498 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
499   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
500   >e0 in e1; normalize #H @H ]
501qed.
502
503definition transform_partial_program2 :
504 ∀A,B,V,W. ∀p: program A V.
505  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
506  →  (V → res W) → res (program B W) ≝
507λA,B,V,W,p, transf_partial_function, transf_partial_variable.
508  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
509  (*CSC: interactive mode because of dependent types *)
510  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
511  cases (map_partial … transf_partial_variable (prog_vars … p))
512  [ #vl #EQ
513    @(OK (program B W) (mk_program … vl … (prog_main … p)))
514    <(map_fst … (EQ vl (refl …))) @fl
515  | #err #_ @(Error … err)]
516qed.
517
518(*
519Lemma transform_partial_program2_function:
520  forall p tp i tf,
521  transform_partial_program2 p = OK tp ->
522  In (i, tf) tp.(prog_funct) ->
523  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
524Proof.
525  intros. monadInv H. 
526  eapply In_map_partial; eauto.
527Qed.
528
529Lemma transform_partial_program2_variable:
530  forall p tp i tv,
531  transform_partial_program2 p = OK tp ->
532  In (i, tv) tp.(prog_vars) ->
533  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
534Proof.
535  intros. monadInv H.
536  eapply In_map_partial; eauto.
537Qed.
538
539Lemma transform_partial_program2_main:
540  forall p tp,
541  transform_partial_program2 p = OK tp ->
542  tp.(prog_main) = p.(prog_main).
543Proof.
544  intros. monadInv H. reflexivity.
545Qed.
546
547End TRANSF_PARTIAL_PROGRAM2.
548
549(** The following is a relational presentation of
550  [transform_program_partial2].  Given relations between function
551  definitions and between variable information, it defines a relation
552  between programs stating that the two programs have the same shape
553  (same global names, etc) and that identically-named function definitions
554  are variable information are related. *)
555
556Section MATCH_PROGRAM.
557
558Variable A B V W: Type.
559Variable match_fundef: A -> B -> Prop.
560Variable match_varinfo: V -> W -> Prop.
561
562Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
563  match x1, x2 with
564  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
565  end.
566
567Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
568  match x1, x2 with
569  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
570  end.
571
572Definition match_program (p1: program A V) (p2: program B W) : Prop :=
573  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
574  /\ p1.(prog_main) = p2.(prog_main)
575  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
576
577End MATCH_PROGRAM.
578
579Remark transform_partial_program2_match:
580  forall (A B V W: Type)
581         (transf_partial_function: A -> res B)
582         (transf_partial_variable: V -> res W)
583         (p: program A V) (tp: program B W),
584  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
585  match_program
586    (fun fd tfd => transf_partial_function fd = OK tfd)
587    (fun info tinfo => transf_partial_variable info = OK tinfo)
588    p tp.
589Proof.
590  intros. monadInv H. split.
591  apply list_forall2_imply with
592    (fun (ab: ident * A) (ac: ident * B) =>
593       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
594  eapply map_partial_forall2. eauto.
595  intros. destruct v1; destruct v2; simpl in *. auto.
596  split. auto.
597  apply list_forall2_imply with
598    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
599       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
600  eapply map_partial_forall2. eauto.
601  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
602Qed.
603*)
604(* * * External functions *)
605
606(* * For most languages, the functions composing the program are either
607  internal functions, defined within the language, or external functions
608  (a.k.a. system calls) that emit an event when applied.  We define
609  a type for such functions and some generic transformation functions. *)
610
611record external_function : Type[0] ≝ {
612  ef_id: ident;
613  ef_sig: signature
614}.
615
616definition ExternalFunction ≝ external_function.
617definition external_function_tag ≝ ef_id.
618definition external_function_sig ≝ ef_sig.
619
620inductive fundef (F: Type[0]): Type[0] ≝
621  | Internal: F → fundef F
622  | External: external_function → fundef F.
623
624(* Implicit Arguments External [F]. *)
625(*
626Section TRANSF_FUNDEF.
627
628Variable A B: Type.
629Variable transf: A -> B.
630*)
631definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
632λA,B,transf,fd.
633  match fd with
634  [ Internal f ⇒ Internal ? (transf f)
635  | External ef ⇒ External ? ef
636  ].
637
638(*
639End TRANSF_FUNDEF.
640
641Section TRANSF_PARTIAL_FUNDEF.
642
643Variable A B: Type.
644Variable transf_partial: A -> res B.
645*)
646
647definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
648λA,B,transf_partial,fd.
649  match fd with
650  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
651  | External ef ⇒ OK ? (External ? ef)
652  ].
653(*
654End TRANSF_PARTIAL_FUNDEF.
655*)
656
657
658
659(* Partially merged stuff derived from the prototype cerco compiler. *)
660
661(*
662definition bool_to_Prop ≝
663 λb. match b with [ true ⇒ True | false ⇒ False ].
664
665coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
666*)
667
668(* dpm: should go to standard library *)
669let rec member (i: ident) (eq_i: ident → ident → bool)
670               (g: list ident) on g: Prop ≝
671  match g with
672  [ nil ⇒ False
673  | cons hd tl ⇒
674      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
675  ].
Note: See TracBrowser for help on using the repository browser.