source: src/common/AST.ma @ 1971

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

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

File size: 22.8 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
327definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
328λA,B,V,p,transf.
329  mk_program B V
330    (prog_vars A V p)
331    (transf_program ?? transf (prog_funct A V p))
332    (prog_main A V p).
333(*
334lemma transform_program_function:
335  ∀A,B,V,transf,p,i,tf.
336  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
337  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
338normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
339#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
340qed.
341*)
342(*
343End TRANSF_PROGRAM.
344
345(** The following is a variant of [transform_program] where the
346  code transformation function can fail and therefore returns an
347  option type. *)
348
349Open Local Scope error_monad_scope.
350Open Local Scope string_scope.
351
352Section MAP_PARTIAL.
353
354Variable A B C: Type.
355Variable prefix_errmsg: A -> errmsg.
356Variable f: B -> res C.
357*)
358definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
359                         list (A × B) → res (list (A × C)) ≝
360λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
361
362lemma map_partial_preserves_first:
363 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
364  map_partial … f l = OK ? l' →
365   map … \fst l = map … \fst l'.
366 #A #B #C #f #l elim l
367  [ #l' #E normalize in E; destruct %
368  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
369    [2: #err #E destruct
370    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
371      cases (map_partial … f tl) in IH ⊢ %;
372      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
373      >(IH x) // ]]
374qed.
375
376(*
377Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
378  match l with
379  | nil => OK nil
380  | (a, b) :: rem =>
381      match f b with
382      | Error msg => Error (prefix_errmsg a ++ msg)%list
383      | OK c =>
384          do rem' <- map_partial rem;
385          OK ((a, c) :: rem')
386      end
387  end.
388
389Remark In_map_partial:
390  forall l l' a c,
391  map_partial l = OK l' ->
392  In (a, c) l' ->
393  exists b, In (a, b) l /\ f b = OK c.
394Proof.
395  induction l; simpl.
396  intros. inv H. elim H0.
397  intros until c. destruct a as [a1 b1].
398  caseEq (f b1); try congruence.
399  intro c1; intros. monadInv H0.
400  elim H1; intro. inv H0. exists b1; auto.
401  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
402Qed.
403
404Remark map_partial_forall2:
405  forall l l',
406  map_partial l = OK l' ->
407  list_forall2
408    (fun (a_b: A * B) (a_c: A * C) =>
409       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
410    l l'.
411Proof.
412  induction l; simpl.
413  intros. inv H. constructor.
414  intro l'. destruct a as [a b].
415  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
416  constructor. simpl. auto. auto.
417Qed.
418
419End MAP_PARTIAL.
420
421Remark map_partial_total:
422  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
423  map_partial prefix (fun b => OK (f b)) l =
424  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
425Proof.
426  induction l; simpl.
427  auto.
428  destruct a as [a1 b1]. rewrite IHl. reflexivity.
429Qed.
430
431Remark map_partial_identity:
432  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
433  map_partial prefix (fun b => OK b) l = OK l.
434Proof.
435  induction l; simpl.
436  auto.
437  destruct a as [a1 b1]. rewrite IHl. reflexivity.
438Qed.
439
440Section TRANSF_PARTIAL_PROGRAM.
441
442Variable A B V: Type.
443Variable transf_partial: A -> res B.
444
445Definition prefix_funct_name (id: ident) : errmsg :=
446  MSG "In function " :: CTX id :: MSG ": " :: nil.
447*)
448definition 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) ≝
449λA,B,V,p,transf_partial.
450  do fl ← map_partial … transf_partial (prog_funct … p);
451  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
452
453(*
454Lemma transform_partial_program_function:
455  forall p tp i tf,
456  transform_partial_program p = OK tp ->
457  In (i, tf) tp.(prog_funct) ->
458  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
459Proof.
460  intros. monadInv H. simpl in H0. 
461  eapply In_map_partial; eauto.
462Qed.
463
464Lemma transform_partial_program_main:
465  forall p tp,
466  transform_partial_program p = OK tp ->
467  tp.(prog_main) = p.(prog_main).
468Proof.
469  intros. monadInv H. reflexivity.
470Qed.
471
472Lemma transform_partial_program_vars:
473  forall p tp,
474  transform_partial_program p = OK tp ->
475  tp.(prog_vars) = p.(prog_vars).
476Proof.
477  intros. monadInv H. reflexivity.
478Qed.
479
480End TRANSF_PARTIAL_PROGRAM.
481
482(** The following is a variant of [transform_program_partial] where
483  both the program functions and the additional variable information
484  are transformed by functions that can fail. *)
485
486Section TRANSF_PARTIAL_PROGRAM2.
487
488Variable A B V W: Type.
489Variable transf_partial_function: A -> res B.
490Variable transf_partial_variable: V -> res W.
491
492Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
493  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
494*)
495
496(* CSC: ad hoc lemma, move away? *)
497lemma map_fst:
498 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
499  map … \fst l = map … \fst l' →
500  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
501#A #B #C #C' #l elim l
502 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
503 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
504   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
505   >e0 in e1; normalize #H @H ]
506qed.
507
508definition transform_partial_program2 :
509 ∀A,B,V,W. ∀p: program A V.
510  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
511  →  (V → res W) → res (program B W) ≝
512λA,B,V,W,p, transf_partial_function, transf_partial_variable.
513  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
514  (*CSC: interactive mode because of dependent types *)
515  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
516  cases (map_partial … transf_partial_variable (prog_vars … p))
517  [ #vl #EQ
518    @(OK (program B W) (mk_program … vl … (prog_main … p)))
519    <(map_fst … (EQ vl (refl …))) @fl
520  | #err #_ @(Error … err)]
521qed.
522
523(*
524Lemma transform_partial_program2_function:
525  forall p tp i tf,
526  transform_partial_program2 p = OK tp ->
527  In (i, tf) tp.(prog_funct) ->
528  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
529Proof.
530  intros. monadInv H. 
531  eapply In_map_partial; eauto.
532Qed.
533
534Lemma transform_partial_program2_variable:
535  forall p tp i tv,
536  transform_partial_program2 p = OK tp ->
537  In (i, tv) tp.(prog_vars) ->
538  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
539Proof.
540  intros. monadInv H.
541  eapply In_map_partial; eauto.
542Qed.
543
544Lemma transform_partial_program2_main:
545  forall p tp,
546  transform_partial_program2 p = OK tp ->
547  tp.(prog_main) = p.(prog_main).
548Proof.
549  intros. monadInv H. reflexivity.
550Qed.
551
552End TRANSF_PARTIAL_PROGRAM2.
553
554(** The following is a relational presentation of
555  [transform_program_partial2].  Given relations between function
556  definitions and between variable information, it defines a relation
557  between programs stating that the two programs have the same shape
558  (same global names, etc) and that identically-named function definitions
559  are variable information are related. *)
560
561Section MATCH_PROGRAM.
562
563Variable A B V W: Type.
564Variable match_fundef: A -> B -> Prop.
565Variable match_varinfo: V -> W -> Prop.
566
567Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
568  match x1, x2 with
569  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
570  end.
571
572Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
573  match x1, x2 with
574  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
575  end.
576
577Definition match_program (p1: program A V) (p2: program B W) : Prop :=
578  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
579  /\ p1.(prog_main) = p2.(prog_main)
580  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
581
582End MATCH_PROGRAM.
583
584Remark transform_partial_program2_match:
585  forall (A B V W: Type)
586         (transf_partial_function: A -> res B)
587         (transf_partial_variable: V -> res W)
588         (p: program A V) (tp: program B W),
589  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
590  match_program
591    (fun fd tfd => transf_partial_function fd = OK tfd)
592    (fun info tinfo => transf_partial_variable info = OK tinfo)
593    p tp.
594Proof.
595  intros. monadInv H. split.
596  apply list_forall2_imply with
597    (fun (ab: ident * A) (ac: ident * B) =>
598       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
599  eapply map_partial_forall2. eauto.
600  intros. destruct v1; destruct v2; simpl in *. auto.
601  split. auto.
602  apply list_forall2_imply with
603    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
604       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
605  eapply map_partial_forall2. eauto.
606  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
607Qed.
608*)
609(* * * External functions *)
610
611(* * For most languages, the functions composing the program are either
612  internal functions, defined within the language, or external functions
613  (a.k.a. system calls) that emit an event when applied.  We define
614  a type for such functions and some generic transformation functions. *)
615
616record external_function : Type[0] ≝ {
617  ef_id: ident;
618  ef_sig: signature
619}.
620
621definition ExternalFunction ≝ external_function.
622definition external_function_tag ≝ ef_id.
623definition external_function_sig ≝ ef_sig.
624
625inductive fundef (F: Type[0]): Type[0] ≝
626  | Internal: F → fundef F
627  | External: external_function → fundef F.
628
629(* Implicit Arguments External [F]. *)
630(*
631Section TRANSF_FUNDEF.
632
633Variable A B: Type.
634Variable transf: A -> B.
635*)
636definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
637λA,B,transf,fd.
638  match fd with
639  [ Internal f ⇒ Internal ? (transf f)
640  | External ef ⇒ External ? ef
641  ].
642
643(*
644End TRANSF_FUNDEF.
645
646Section TRANSF_PARTIAL_FUNDEF.
647
648Variable A B: Type.
649Variable transf_partial: A -> res B.
650*)
651
652definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
653λA,B,transf_partial,fd.
654  match fd with
655  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
656  | External ef ⇒ OK ? (External ? ef)
657  ].
658(*
659End TRANSF_PARTIAL_FUNDEF.
660*)
661
662
663
664(* Partially merged stuff derived from the prototype cerco compiler. *)
665
666(*
667definition bool_to_Prop ≝
668 λb. match b with [ true ⇒ True | false ⇒ False ].
669
670coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
671*)
672
673(* dpm: should go to standard library *)
674let rec member (i: ident) (eq_i: ident → ident → bool)
675               (g: list ident) on g: Prop ≝
676  match g with
677  [ nil ⇒ False
678  | cons hd tl ⇒
679      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
680  ].
Note: See TracBrowser for help on using the repository browser.