source: src/common/AST.ma @ 2103

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

Make transform_*program take a more general transformation to make
properties easier to state.

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