source: src/common/AST.ma @ 2474

Last change on this file since 2474 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File size: 29.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
40(* dpm: not needed
41inductive quantity: Type[0] ≝
42  | q_int: Byte → quantity
43  | q_offset: quantity
44  | q_ptr: quantity.
45 
46inductive abstract_size: Type[0] ≝
47  | size_q: quantity → abstract_size
48  | size_prod: list abstract_size → abstract_size
49  | size_sum: list abstract_size → abstract_size
50  | size_array: nat → abstract_size → abstract_size.
51*)
52
53
54(* Memory spaces
55
56   For full 8051 memory spaces support we have internal memory pointers,
57   PData pointers which are 8 bit pointers to the first page of XData, and
58   a tagged Any pointer for any of the spaces.
59   
60   We only support the 16 bit XData and Code pointers for now.  Some commented
61   out code is still present to suggest how to add the rest, which includes
62   having pointers and pointer types contain a region field to indicate what
63   kind of pointer they are (in addition to the region in the block which
64   indicates where the pointer points to).
65
66 *)
67
68inductive region : Type[0] ≝
69(*  | Any : region
70  | Data : region
71  | IData : region
72  | PData : region*)
73  | XData : region
74  | Code : region.
75
76definition eq_region : region → region → bool ≝
77λr1,r2.
78  match r1 with
79  [ (*Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
80  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
81  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
82  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
83  |*) XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
84  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
85  ].
86
87lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
88  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
89  P (eq_region r1 r2).
90#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
91try ( @Ptrue // )
92@Pfalse % #E destruct
93qed.
94
95lemma reflexive_eq_region: ∀r. eq_region r r = true.
96 * //
97qed.
98
99definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
100#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
101
102(*
103(* Carefully defined to be convertably nonzero *)
104definition size_pointer : region → nat ≝
105λsp. S match sp with [ Data ⇒ 0 | IData ⇒ 0 | PData ⇒ 0 | XData ⇒ 1 | Code ⇒ 1 | Any ⇒ 2 ].
106*)
107definition size_pointer : nat ≝ 2.
108
109(* We maintain some reasonable type information through the front end of the
110   compiler. *)
111
112inductive signedness : Type[0] ≝
113  | Signed: signedness
114  | Unsigned: signedness.
115
116inductive intsize : Type[0] ≝
117  | I8: intsize
118  | I16: intsize
119  | I32: intsize.
120
121(* * Float types come in two sizes: 32 bits (single precision)
122  and 64-bit (double precision). *)
123
124inductive floatsize : Type[0] ≝
125  | F32: floatsize
126  | F64: floatsize.
127
128inductive typ : Type[0] ≝
129  | ASTint : intsize → signedness → typ
130  | ASTptr : (*region →*) typ.
131(*  | ASTfloat : floatsize → typ. *)
132
133(* XXX aliases *)
134definition SigType ≝ typ.
135definition SigType_Int ≝ ASTint I32 Unsigned.
136(*
137| SigType_Float: SigType
138*)
139definition SigType_Ptr ≝ ASTptr (*Any*).
140
141(* Define these carefully so that we always know that the result is nonzero,
142   and can be used in dependent types of the form (S n).
143   (At the time of writing this is only used for bitsize_of_intsize.) *)
144
145definition pred_size_intsize : intsize → nat ≝
146λsz. match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
147
148definition size_intsize : intsize → nat ≝
149λsz. S (pred_size_intsize sz).
150
151definition bitsize_of_intsize : intsize → nat ≝
152λsz. size_intsize sz * 8.
153
154definition eq_intsize : intsize → intsize → bool ≝
155λsz1,sz2.
156  match sz1 with
157  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
158  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
159  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
160  ].
161
162lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
163  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
164* * #P #Hne #Heq whd in ⊢ (?%); try (@Heq @refl) @Hne % #E destruct
165qed.
166
167lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
168* @refl
169qed.
170
171lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
172* * * #NE try @refl @False_ind @NE @refl
173qed.
174
175definition signedness_check : ∀sg1,sg2:signedness. ∀P:signedness → signedness → Type[0].
176 P sg1 sg1 → P sg1 sg2 → P sg1 sg2 ≝
177λsg1,sg2,P.
178match sg1 return λsg1. P sg1 sg1 → P sg1 sg2 → P sg1 sg2 with
179[ Signed ⇒ λx. match sg2 return λsg2. P ? sg2 → P Signed sg2 with [ Signed ⇒ λd. x | _ ⇒ λd. d ]
180| Unsigned ⇒ λx. match sg2 return λsg2. P ? sg2 → P Unsigned sg2 with [ Unsigned ⇒ λd. x | _ ⇒ λd. d ]
181].
182
183let rec inttyp_eq_elim' (sz1,sz2:intsize) (sg1,sg2:signedness) (P:intsize → signedness → intsize → signedness → Type[0]) on sz1 :
184  P sz1 sg1 sz1 sg1 → P sz1 sg1 sz2 sg2 → P sz1 sg1 sz2 sg2 ≝
185match sz1 return λsz. P sz sg1 sz sg1 → P sz sg1 sz2 sg2 → P sz sg1 sz2 sg2 with
186[ 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 ]
187| 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 ]
188| 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 ]
189].
190
191let rec intsize_eq_elim' (sz1,sz2:intsize) (P:intsize → intsize → Type[0]) on sz1 :
192  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
193match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
194[ I8  ⇒ λx. match sz2 return λsz. P ? sz → P I8 sz with [ I8  ⇒ λd. x | _ ⇒ λd. d ]
195| I16 ⇒ λx. match sz2 return λsz. P ? sz → P I16 sz with [ I16 ⇒ λd. x | _ ⇒ λd. d ]
196| I32 ⇒ λx. match sz2 return λsz. P ? sz → P I32 sz with [ I32 ⇒ λd. x | _ ⇒ λd. d ]
197].
198
199(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
200   if it is returns [e1] where the type of [n] has its dependency on [sz1]
201   changed to [sz2], and if not returns [e2]. *)
202let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
203  P sz1 → (P sz2 → A) → A → A ≝
204match sz1 return λsz. P sz → (P sz2 → A) → A → A with
205[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
206| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
207| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
208].
209
210lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
211  intsize_eq_elim A sz sz P p f d = f p.
212#A * //
213qed.
214
215lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
216  (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).
217#A * * #P #p #f #d #Q #Hne #Heq
218[ 1,5,9: whd in ⊢ (?%); @(Heq (refl ??))
219| *: whd in ⊢ (?%); @Hne % #E destruct
220] qed.
221
222lemma intsize_eq_elim_false : ∀A,sz,sz',P,p,f,d.
223  sz ≠ sz' →
224  intsize_eq_elim A sz sz' P p f d = d.
225#A * * // #P #p #f #d * #H cases (H (refl ??))
226qed.
227
228(* A type for the integers that appear in the semantics. *)
229definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
230
231definition repr : ∀sz:intsize. nat → bvint sz ≝
232λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
233
234definition size_floatsize : floatsize → nat ≝
235λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
236
237let rec floatsize_eq_elim (sz1,sz2:floatsize) (P:floatsize → floatsize → Type[0]) on sz1 :
238  P sz1 sz1 → P sz1 sz2 → P sz1 sz2 ≝
239match sz1 return λsz. P sz sz → P sz sz2 → P sz sz2 with
240[ F32 ⇒ λx. match sz2 return λsz. P ? sz → P F32 sz with [ F32 ⇒ λd. x | _ ⇒ λd. d ]
241| F64 ⇒ λx. match sz2 return λsz. P ? sz → P F64 sz with [ F64 ⇒ λd. x | _ ⇒ λd. d ]
242].
243
244
245definition typesize : typ → nat ≝ λty.
246  match ty with
247  [ ASTint sz _ ⇒ size_intsize sz
248  | ASTptr  ⇒ size_pointer ].
249(*  | ASTfloat sz ⇒ size_floatsize sz ].*)
250
251lemma typesize_pos: ∀ty. typesize ty > 0.
252*; try *; try * /2 by le_n/ qed.
253
254lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
255* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
256qed.
257
258lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
259#t1 #t2 cases t1 cases t2
260[ %1 @refl
261| 2,3: #ty %2 % #H destruct
262| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
263]
264qed.
265
266(* * Additionally, function definitions and function calls are annotated
267  by function signatures indicating the number and types of arguments,
268  as well as the type of the returned value if any.  These signatures
269  are used in particular to determine appropriate calling conventions
270  for the function. *)
271
272record signature : Type[0] ≝ {
273  sig_args: list typ;
274  sig_res: option typ
275}.
276
277(* XXX aliases *)
278definition Signature ≝ signature.
279definition signature_args ≝ sig_args.
280definition signature_return ≝ sig_res.
281
282definition proj_sig_res : signature → typ ≝ λs.
283  match sig_res s with
284  [ None ⇒ ASTint I32 Unsigned
285  | Some t ⇒ t
286  ].
287
288(* * Initialization data for global variables. *)
289
290inductive init_data: Type[0] ≝
291  | Init_int8: bvint I8 → init_data
292  | Init_int16: bvint I16 → init_data
293  | Init_int32: bvint I32 → init_data
294  | Init_float32: float → init_data
295  | Init_float64: float → init_data
296  | Init_space: nat → init_data
297  | Init_null: (*region →*) init_data
298  | Init_addrof: (*region →*) ident → nat → init_data.   (*r address of symbol + offset *)
299
300(* * Whole programs consist of:
301- a collection of function definitions (name and description);
302- the name of the ``main'' function that serves as entry point in the program;
303- a collection of global variable declarations, consisting of
304  a name, initialization data, and additional information.
305
306The type of function descriptions and that of additional information
307for variables vary among the various intermediate languages and are
308taken as parameters to the [program] type.  The other parts of whole
309programs are common to all languages. *)
310
311record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
312  prog_vars: list (ident × region × V);
313  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
314  prog_main: ident
315}.
316
317
318definition prog_funct_names ≝ λF,V. λp: program F V.
319  map ?? \fst (prog_funct … p).
320
321definition prog_var_names ≝ λF,V. λp: program F V.
322  map ?? (λx. \fst (\fst x)) (prog_vars … p).
323
324(* * * Generic transformations over programs *)
325
326(* * We now define a general iterator over programs that applies a given
327  code transformation function to all function descriptions and leaves
328  the other parts of the program unchanged. *)
329(*
330Section TRANSF_PROGRAM.
331
332Variable A B V: Type.
333Variable transf: A -> B.
334*)
335
336definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
337λA,B,transf,l.
338  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
339
340(* In principle we could allow the transformation to be specialised to a
341   particular set of variable names, but that makes it much harder to state
342   and prove properties. *)
343
344definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝
345λA,B,V,p,transf.
346  mk_program B V
347    (prog_vars A V p)
348    (transf_program ?? (transf ?) (prog_funct A V p))
349    (prog_main A V p).
350
351(* Versions of the above that thread a fresh name generator through the
352   transformation. *)
353
354definition transf_program_gen : ∀tag,A,B. universe tag →
355  (universe tag → A → B × (universe tag)) →
356  list (ident × A) →
357  list (ident × B) × (universe tag) ≝
358λtag,A,B,gen,transf,l.
359  foldr ?? (λid_fn,bs_gen. let 〈fn',gen'〉 ≝ transf (\snd bs_gen) (\snd id_fn) in
360                      〈〈\fst id_fn, fn'〉::(\fst bs_gen), gen'〉) 〈[ ], gen〉 l.
361
362lemma transf_program_gen_step : ∀tag,A,B,gen,transf,id,fn,tl.
363  ∃gen'.
364    \fst (transf_program_gen tag A B gen transf (〈id,fn〉::tl)) =
365    〈id, \fst (transf gen' fn)〉::(\fst (transf_program_gen tag A B gen transf tl)).
366#tag #A #B #gen #transf #id #fn #tl
367whd in ⊢ (??(λ_.??(???%)?));
368change with (transf_program_gen ??????) in match (foldr ?????);
369cases (transf_program_gen ??????) #tl' #gen'
370%{gen'} cases (transf gen' fn) //
371qed.
372
373definition transform_program_gen : ∀tag,A,B,V. universe tag → ∀p:program A V.
374  (∀varnames. universe tag → A varnames → B varnames × (universe tag)) →
375  program B V × (universe tag) ≝
376λtag,A,B,V,gen,p,trans.
377  let fsg ≝ transf_program_gen tag ?? gen (trans ?) (prog_funct A V p) in
378  〈mk_program B V
379    (prog_vars A V p)
380    (\fst fsg)
381    (prog_main A V p), \snd fsg〉.
382
383
384(*
385lemma transform_program_function:
386  ∀A,B,V,transf,p,i,tf.
387  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
388  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
389normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
390#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
391qed.
392*)
393(*
394End TRANSF_PROGRAM.
395
396(** The following is a variant of [transform_program] where the
397  code transformation function can fail and therefore returns an
398  option type. *)
399
400Open Local Scope error_monad_scope.
401Open Local Scope string_scope.
402
403Section MAP_PARTIAL.
404
405Variable A B C: Type.
406Variable prefix_errmsg: A -> errmsg.
407Variable f: B -> res C.
408*)
409definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
410                         list (A × B) → res (list (A × C)) ≝
411λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
412
413lemma map_partial_preserves_first:
414 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
415  map_partial … f l = OK ? l' →
416   map … \fst l = map … \fst l'.
417 #A #B #C #f #l elim l
418  [ #l' #E normalize in E; destruct %
419  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
420    [2: #err #E destruct
421    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
422      cases (map_partial … f tl) in IH ⊢ %;
423      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
424      >(IH x) // ]]
425qed.
426
427lemma map_partial_All2 : ∀A,B,C,f. ∀P:A×B → A×C → Prop.
428  (∀i,x,y. f x = OK ? y → P 〈i,x〉 〈i,y〉) →
429  ∀l,l'.
430  map_partial A B C f l = OK ? l' →
431  All2 (A×B) (A×C) P l l'.
432#A #B #C #f #P #H #l elim l
433[ * [ // | #h #t #E normalize in E; destruct ]
434| * #a #b #tl #IH #l' #M
435  cases (bind_inversion ????? M) -M * #a' #c * #AC #M
436  cases (bind_inversion ????? M) -M #tl' * #TL #M
437  cases (bind_inversion ????? AC) -AC #c' * #C #C'
438  normalize in C C' M; destruct %
439  [ @H @C
440  | @IH @TL
441  ]
442] qed.
443
444(*
445Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
446  match l with
447  | nil => OK nil
448  | (a, b) :: rem =>
449      match f b with
450      | Error msg => Error (prefix_errmsg a ++ msg)%list
451      | OK c =>
452          do rem' <- map_partial rem;
453          OK ((a, c) :: rem')
454      end
455  end.
456
457Remark In_map_partial:
458  forall l l' a c,
459  map_partial l = OK l' ->
460  In (a, c) l' ->
461  exists b, In (a, b) l /\ f b = OK c.
462Proof.
463  induction l; simpl.
464  intros. inv H. elim H0.
465  intros until c. destruct a as [a1 b1].
466  caseEq (f b1); try congruence.
467  intro c1; intros. monadInv H0.
468  elim H1; intro. inv H0. exists b1; auto.
469  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
470Qed.
471
472Remark map_partial_forall2:
473  forall l l',
474  map_partial l = OK l' ->
475  list_forall2
476    (fun (a_b: A * B) (a_c: A * C) =>
477       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
478    l l'.
479Proof.
480  induction l; simpl.
481  intros. inv H. constructor.
482  intro l'. destruct a as [a b].
483  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
484  constructor. simpl. auto. auto.
485Qed.
486
487End MAP_PARTIAL.
488
489Remark map_partial_total:
490  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
491  map_partial prefix (fun b => OK (f b)) l =
492  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
493Proof.
494  induction l; simpl.
495  auto.
496  destruct a as [a1 b1]. rewrite IHl. reflexivity.
497Qed.
498
499Remark map_partial_identity:
500  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
501  map_partial prefix (fun b => OK b) l = OK l.
502Proof.
503  induction l; simpl.
504  auto.
505  destruct a as [a1 b1]. rewrite IHl. reflexivity.
506Qed.
507
508Section TRANSF_PARTIAL_PROGRAM.
509
510Variable A B V: Type.
511Variable transf_partial: A -> res B.
512
513Definition prefix_funct_name (id: ident) : errmsg :=
514  MSG "In function " :: CTX id :: MSG ": " :: nil.
515*)
516definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
517λA,B,V,p,transf_partial.
518  do fl ← map_partial … (transf_partial ?) (prog_funct … p);
519  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
520
521(*
522Lemma transform_partial_program_function:
523  forall p tp i tf,
524  transform_partial_program p = OK tp ->
525  In (i, tf) tp.(prog_funct) ->
526  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
527Proof.
528  intros. monadInv H. simpl in H0. 
529  eapply In_map_partial; eauto.
530Qed.
531
532Lemma transform_partial_program_main:
533  forall p tp,
534  transform_partial_program p = OK tp ->
535  tp.(prog_main) = p.(prog_main).
536Proof.
537  intros. monadInv H. reflexivity.
538Qed.
539
540Lemma transform_partial_program_vars:
541  forall p tp,
542  transform_partial_program p = OK tp ->
543  tp.(prog_vars) = p.(prog_vars).
544Proof.
545  intros. monadInv H. reflexivity.
546Qed.
547
548End TRANSF_PARTIAL_PROGRAM.
549
550(** The following is a variant of [transform_program_partial] where
551  both the program functions and the additional variable information
552  are transformed by functions that can fail. *)
553
554Section TRANSF_PARTIAL_PROGRAM2.
555
556Variable A B V W: Type.
557Variable transf_partial_function: A -> res B.
558Variable transf_partial_variable: V -> res W.
559
560Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
561  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
562*)
563
564(* CSC: ad hoc lemma, move away? *)
565lemma map_fst:
566 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
567  map … \fst l = map … \fst l' →
568  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
569#A #B #C #C' #l elim l
570 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
571 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
572   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
573   >e0 in e1; normalize #H @H ]
574qed.
575
576definition transform_partial_program2 :
577 ∀A,B,V,W. ∀p: program A V.
578  (∀varnames. A varnames → res (B varnames))
579  →  (V → res W) → res (program B W) ≝
580λA,B,V,W,p, transf_partial_function, transf_partial_variable.
581  do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?.
582  (*CSC: interactive mode because of dependent types *)
583  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
584  cases (map_partial … transf_partial_variable (prog_vars … p))
585  [ #vl #EQ
586    @(OK (program B W) (mk_program … vl … (prog_main … p)))
587    <(map_fst … (EQ vl (refl …))) @fl
588  | #err #_ @(Error … err)]
589qed.
590
591lemma transform_partial_program2_preserves_var_names : ∀A,B,V,W,p,tf,tv,p'.
592  transform_partial_program2 A B V W p tf tv = OK ? p' →
593  prog_var_names … p = prog_var_names … p'.
594#A #B #V #W * #vars #fns #main #tf #tv * #vars' #fns' #main'
595#T cases (bind_inversion ????? T) -T #vars1 * #Evars1
596generalize in match (map_partial_preserves_first ?????); #MPPF
597lapply (refl ? (map_partial ??? tv vars))
598cases (map_partial ?????) in ⊢ (???% → ?);
599[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
600#vs #VS >VS in MPPF ⊢ %; #MPPF
601whd in ⊢ (??%% → ?);
602generalize in match (map_fst ???????); #MF
603#E destruct
604whd in ⊢ (??%%); @MF
605qed.
606
607
608(*
609Lemma transform_partial_program2_function:
610  forall p tp i tf,
611  transform_partial_program2 p = OK tp ->
612  In (i, tf) tp.(prog_funct) ->
613  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
614Proof.
615  intros. monadInv H. 
616  eapply In_map_partial; eauto.
617Qed.
618
619Lemma transform_partial_program2_variable:
620  forall p tp i tv,
621  transform_partial_program2 p = OK tp ->
622  In (i, tv) tp.(prog_vars) ->
623  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
624Proof.
625  intros. monadInv H.
626  eapply In_map_partial; eauto.
627Qed.
628
629Lemma transform_partial_program2_main:
630  forall p tp,
631  transform_partial_program2 p = OK tp ->
632  tp.(prog_main) = p.(prog_main).
633Proof.
634  intros. monadInv H. reflexivity.
635Qed.
636
637End TRANSF_PARTIAL_PROGRAM2.
638
639(** The following is a relational presentation of
640  [transform_program_partial2].  Given relations between function
641  definitions and between variable information, it defines a relation
642  between programs stating that the two programs have the same shape
643  (same global names, etc) and that identically-named function definitions
644  are variable information are related. *)
645
646Section MATCH_PROGRAM.
647
648Variable A B V W: Type.
649Variable match_fundef: A -> B -> Prop.
650Variable match_varinfo: V -> W -> Prop.
651
652*)
653
654record matching : Type[1] ≝ {
655  m_A : list ident → Type[0];  m_B : list ident → Type[0];  (* function types *)
656  m_V : Type[0];  m_W : Type[0];  (* variable types *)
657  match_fundef : ∀vs. m_A vs → m_B vs → Prop;
658  match_varinfo : m_V → m_W → Prop
659}.
660
661(* When defining a matching between function entries, quietly enforce equality
662   of the list of global variables (vs and vs'). *)
663
664inductive match_funct_entry (M:matching) : ∀vs,vs'. ident × (m_A M vs) → ident × (m_B M vs') → Prop ≝
665| mfe_intro : ∀vs,id,f1,f2. match_fundef M vs f1 f2 → match_funct_entry M vs vs 〈id,f1〉 〈id,f2〉.
666
667(* but we'll need some care to usefully invert it *)
668
669definition mfe_cast_fn_type : ∀M,vs,vs'. ∀E:vs'=vs. m_B M vs' → m_B M vs ≝
670λM,vs,vs',E. ?.
671>E #m @m
672qed.
673
674let rec match_funct_entry_inv (M:matching)
675  (P:∀vs,id,f,id',f'. Prop)
676  (H:∀vs,id,f,f'. match_fundef M vs f f' → P vs id f id f')
677  vs id f id' f'
678  (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝
679match MFE return λvs,vs',idf,idf',MFE. ∀E:vs'=vs. P vs (\fst idf) (\snd idf) (\fst idf') (mfe_cast_fn_type … E (\snd idf')) with
680[ mfe_intro vs id f1 f2 MF ⇒ ?
681] (refl ??).
682#E >(K ?? E) @H @MF
683qed.
684
685(* and continue as before *)
686
687inductive match_var_entry (M:matching) : ident × region × (m_V M) → ident × region × (m_W M) → Prop ≝
688| mve_intro : ∀id,r,v1,v2. match_varinfo M v1 v2 → match_var_entry M 〈id,r,v1〉 〈id,r,v2〉.
689
690lemma matching_vars : ∀M.∀p1:program (m_A M) (m_V M).∀p2:program (m_B M) (m_W M).
691  All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2) →
692  prog_var_names … p1 = prog_var_names … p2.
693#M * #vs1 #mn1 #fn1 * #vs2 #mn2 #fn2
694normalize generalize in match vs2;
695elim vs1
696[ * [ // | #h #t * ]
697| * * #id1 #r1 #v1 #tl1 #IH * [ * ]
698  * * #id2 #r2 #v2 #tl2 * *
699  #id #r #v1' #v2' #_ #H
700  whd in ⊢ (??%%); >(IH … H) %
701] qed.
702
703record match_program (M:matching) (p1: program (m_A M) (m_V M)) (p2: program (m_B M) (m_W M)) : Prop ≝ {
704  mp_vars : All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2);
705  mp_funct : All2 ?? … (match_funct_entry M (prog_var_names … p1) (prog_var_names … p2)) (prog_funct … p1) (prog_funct ??… p2);
706  mp_main : prog_main … p1 = prog_main … p2
707}.
708
709(*
710End MATCH_PROGRAM.
711*)
712
713(* Now show that all the transformations are instances of match_program. *)
714
715lemma transform_partial_program2_match:
716  ∀A,B,V,W.
717         ∀transf_partial_function: ∀vs. A vs -> res (B vs).
718         ∀transf_partial_variable: V -> res W.
719         ∀p: program A V. ∀tp: program B W.
720  transform_partial_program2 … p transf_partial_function transf_partial_variable = OK ? tp →
721  match_program (mk_matching A B V W
722    (λvs,fd,tfd. transf_partial_function vs … fd = OK ? tfd)
723    (λinfo,tinfo. transf_partial_variable info = OK ? tinfo))
724    p tp.
725#A #B #V #W #transf_partial_function #transf_partial_variable
726* #vars #main #functs * #vars' #main' #functs'
727#T cases (bind_inversion ????? T) -T #fl * #Efl
728generalize in match (map_partial_preserves_first ?????); #MPPF
729lapply (refl ? (map_partial ??? transf_partial_variable vars))
730cases (map_partial ?????) in ⊢ (???% → ?);
731[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
732#vs #VS >VS in MPPF ⊢ %; #MPPF
733whd in ⊢ (??%% → ?);
734generalize in match (map_fst ???????); #MF
735#E destruct
736%
737[ @(map_partial_All2 … VS) * /2/
738| whd in match (prog_var_names ???);
739  whd in match (prog_var_names ???);
740  <MF @(map_partial_All2 … Efl) #id #f1 #f2 /2/
741| //
742] qed.
743
744lemma transform_partial_program_match:
745  ∀A,B,V.
746    ∀trans_partial_function: ∀vs. A vs → res (B vs).
747    ∀p: program A V. ∀tp: program B V.
748  transform_partial_program … p trans_partial_function = OK ? tp →
749  match_program (mk_matching A B V V
750    (λvs,fd,tfd. trans_partial_function vs fd = OK ? tfd)
751    (λv,w. v = w))
752    p tp.
753#A #B #V #tpf
754* #vars #fns #main * #vars' #fns' #main'
755#TPP cases (bind_inversion ????? TPP) -TPP #fns'' * #MAP
756#E normalize in E; destruct
757%
758[ elim vars' // * * #id #r #v #tl #H % /2/
759| @(map_partial_All2 … MAP) #i #f #f' #TPF % @TPF
760| //
761] qed.
762
763lemma transform_program_match:
764  ∀A,B,V.
765    ∀trans_function: ∀vs. A vs → B vs.
766    ∀p: program A V.
767  match_program (mk_matching A B V V
768    (λvs,fd,tfd. trans_function vs fd = tfd)
769    (λv,w. v = w))
770    p (transform_program … p trans_function).
771#A #B #V #tf
772* #vars #fns #main
773%
774[ normalize elim vars // * * #id #r #v #tl #H % /2/
775| whd in match (prog_var_names ???);
776  whd in match (prog_vars ???);
777  elim fns
778  [ //
779  | * #id #f #tl #IH % // % //
780  ]
781| //
782] qed.
783
784lemma transform_program_gen_match:
785  ∀A,B,V,tag,gen.
786    ∀trans_function: ∀vs. universe tag → A vs → B vs × (universe tag).
787    ∀p: program A V.
788  match_program (mk_matching A B V V
789    (λvs,fd,tfd. ∃g,g'. trans_function vs g fd = 〈tfd,g'〉)
790    (λv,w. v = w))
791    p (\fst (transform_program_gen … gen p trans_function)).
792#A #B #V #tag #gen #tf
793* #vars #fns #main
794%
795[ normalize elim vars // * * #id #r #v #tl #H % /2/
796| whd in match (prog_var_names ???);
797  whd in match (prog_vars ???);
798  whd in match (transform_program_gen ???????);
799  generalize in match gen;
800  elim fns
801  [ //
802  | * #id #f #tl #IH #g
803    cases (transf_program_gen_step tag (A ?) (B ?) g (tf ?) id f tl)
804    #g' #E >E % /4/
805  ]
806| //
807] qed.
808
809(* * * External functions *)
810
811(* * For most languages, the functions composing the program are either
812  internal functions, defined within the language, or external functions
813  (a.k.a. system calls) that emit an event when applied.  We define
814  a type for such functions and some generic transformation functions. *)
815
816record external_function : Type[0] ≝ {
817  ef_id: ident;
818  ef_sig: signature
819}.
820
821definition ExternalFunction ≝ external_function.
822definition external_function_tag ≝ ef_id.
823definition external_function_sig ≝ ef_sig.
824
825inductive fundef (F: Type[0]): Type[0] ≝
826  | Internal: F → fundef F
827  | External: external_function → fundef F.
828
829(* Implicit Arguments External [F]. *)
830(*
831Section TRANSF_FUNDEF.
832
833Variable A B: Type.
834Variable transf: A -> B.
835*)
836definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
837λA,B,transf,fd.
838  match fd with
839  [ Internal f ⇒ Internal ? (transf f)
840  | External ef ⇒ External ? ef
841  ].
842
843(*
844End TRANSF_FUNDEF.
845
846Section TRANSF_PARTIAL_FUNDEF.
847
848Variable A B: Type.
849Variable transf_partial: A -> res B.
850*)
851
852definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
853λA,B,transf_partial,fd.
854  match fd with
855  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
856  | External ef ⇒ OK ? (External ? ef)
857  ].
858(*
859End TRANSF_PARTIAL_FUNDEF.
860*)
861
862
863
864(* Partially merged stuff derived from the prototype cerco compiler. *)
865
866(*
867definition bool_to_Prop ≝
868 λb. match b with [ true ⇒ True | false ⇒ False ].
869
870coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
871*)
872
873(* dpm: should go to standard library *)
874let rec member (i: ident) (eq_i: ident → ident → bool)
875               (g: list ident) on g: Prop ≝
876  match g with
877  [ nil ⇒ False
878  | cons hd tl ⇒
879      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
880  ].
Note: See TracBrowser for help on using the repository browser.