source: src/common/AST.ma @ 2305

Last change on this file since 2305 was 2286, checked in by tranquil, 8 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 27.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(*
351lemma transform_program_function:
352  ∀A,B,V,transf,p,i,tf.
353  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
354  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
355normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
356#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
357qed.
358*)
359(*
360End TRANSF_PROGRAM.
361
362(** The following is a variant of [transform_program] where the
363  code transformation function can fail and therefore returns an
364  option type. *)
365
366Open Local Scope error_monad_scope.
367Open Local Scope string_scope.
368
369Section MAP_PARTIAL.
370
371Variable A B C: Type.
372Variable prefix_errmsg: A -> errmsg.
373Variable f: B -> res C.
374*)
375definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
376                         list (A × B) → res (list (A × C)) ≝
377λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
378
379lemma map_partial_preserves_first:
380 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
381  map_partial … f l = OK ? l' →
382   map … \fst l = map … \fst l'.
383 #A #B #C #f #l elim l
384  [ #l' #E normalize in E; destruct %
385  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?); cases (f b) normalize in ⊢ (? → ??%? → ?);
386    [2: #err #E destruct
387    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
388      cases (map_partial … f tl) in IH ⊢ %;
389      #x #IH normalize in ⊢ (??%? → ?); #ABS destruct normalize
390      >(IH x) // ]]
391qed.
392
393lemma map_partial_All2 : ∀A,B,C,f. ∀P:A×B → A×C → Prop.
394  (∀i,x,y. f x = OK ? y → P 〈i,x〉 〈i,y〉) →
395  ∀l,l'.
396  map_partial A B C f l = OK ? l' →
397  All2 (A×B) (A×C) P l l'.
398#A #B #C #f #P #H #l elim l
399[ * [ // | #h #t #E normalize in E; destruct ]
400| * #a #b #tl #IH #l' #M
401  cases (bind_inversion ????? M) -M * #a' #c * #AC #M
402  cases (bind_inversion ????? M) -M #tl' * #TL #M
403  cases (bind_inversion ????? AC) -AC #c' * #C #C'
404  normalize in C C' M; destruct %
405  [ @H @C
406  | @IH @TL
407  ]
408] qed.
409
410(*
411Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
412  match l with
413  | nil => OK nil
414  | (a, b) :: rem =>
415      match f b with
416      | Error msg => Error (prefix_errmsg a ++ msg)%list
417      | OK c =>
418          do rem' <- map_partial rem;
419          OK ((a, c) :: rem')
420      end
421  end.
422
423Remark In_map_partial:
424  forall l l' a c,
425  map_partial l = OK l' ->
426  In (a, c) l' ->
427  exists b, In (a, b) l /\ f b = OK c.
428Proof.
429  induction l; simpl.
430  intros. inv H. elim H0.
431  intros until c. destruct a as [a1 b1].
432  caseEq (f b1); try congruence.
433  intro c1; intros. monadInv H0.
434  elim H1; intro. inv H0. exists b1; auto.
435  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
436Qed.
437
438Remark map_partial_forall2:
439  forall l l',
440  map_partial l = OK l' ->
441  list_forall2
442    (fun (a_b: A * B) (a_c: A * C) =>
443       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
444    l l'.
445Proof.
446  induction l; simpl.
447  intros. inv H. constructor.
448  intro l'. destruct a as [a b].
449  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
450  constructor. simpl. auto. auto.
451Qed.
452
453End MAP_PARTIAL.
454
455Remark map_partial_total:
456  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
457  map_partial prefix (fun b => OK (f b)) l =
458  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
459Proof.
460  induction l; simpl.
461  auto.
462  destruct a as [a1 b1]. rewrite IHl. reflexivity.
463Qed.
464
465Remark map_partial_identity:
466  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
467  map_partial prefix (fun b => OK b) l = OK l.
468Proof.
469  induction l; simpl.
470  auto.
471  destruct a as [a1 b1]. rewrite IHl. reflexivity.
472Qed.
473
474Section TRANSF_PARTIAL_PROGRAM.
475
476Variable A B V: Type.
477Variable transf_partial: A -> res B.
478
479Definition prefix_funct_name (id: ident) : errmsg :=
480  MSG "In function " :: CTX id :: MSG ": " :: nil.
481*)
482definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
483λA,B,V,p,transf_partial.
484  do fl ← map_partial … (transf_partial ?) (prog_funct … p);
485  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
486
487(*
488Lemma transform_partial_program_function:
489  forall p tp i tf,
490  transform_partial_program p = OK tp ->
491  In (i, tf) tp.(prog_funct) ->
492  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
493Proof.
494  intros. monadInv H. simpl in H0. 
495  eapply In_map_partial; eauto.
496Qed.
497
498Lemma transform_partial_program_main:
499  forall p tp,
500  transform_partial_program p = OK tp ->
501  tp.(prog_main) = p.(prog_main).
502Proof.
503  intros. monadInv H. reflexivity.
504Qed.
505
506Lemma transform_partial_program_vars:
507  forall p tp,
508  transform_partial_program p = OK tp ->
509  tp.(prog_vars) = p.(prog_vars).
510Proof.
511  intros. monadInv H. reflexivity.
512Qed.
513
514End TRANSF_PARTIAL_PROGRAM.
515
516(** The following is a variant of [transform_program_partial] where
517  both the program functions and the additional variable information
518  are transformed by functions that can fail. *)
519
520Section TRANSF_PARTIAL_PROGRAM2.
521
522Variable A B V W: Type.
523Variable transf_partial_function: A -> res B.
524Variable transf_partial_variable: V -> res W.
525
526Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
527  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
528*)
529
530(* CSC: ad hoc lemma, move away? *)
531lemma map_fst:
532 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
533  map … \fst l = map … \fst l' →
534  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
535#A #B #C #C' #l elim l
536 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
537 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
538   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%); >(IH tl2) destruct normalize in e1 ⊢ %; >e0 //
539   >e0 in e1; normalize #H @H ]
540qed.
541
542definition transform_partial_program2 :
543 ∀A,B,V,W. ∀p: program A V.
544  (∀varnames. A varnames → res (B varnames))
545  →  (V → res W) → res (program B W) ≝
546λA,B,V,W,p, transf_partial_function, transf_partial_variable.
547  do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?.
548  (*CSC: interactive mode because of dependent types *)
549  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
550  cases (map_partial … transf_partial_variable (prog_vars … p))
551  [ #vl #EQ
552    @(OK (program B W) (mk_program … vl … (prog_main … p)))
553    <(map_fst … (EQ vl (refl …))) @fl
554  | #err #_ @(Error … err)]
555qed.
556
557lemma transform_partial_program2_preserves_var_names : ∀A,B,V,W,p,tf,tv,p'.
558  transform_partial_program2 A B V W p tf tv = OK ? p' →
559  prog_var_names … p = prog_var_names … p'.
560#A #B #V #W * #vars #fns #main #tf #tv * #vars' #fns' #main'
561#T cases (bind_inversion ????? T) -T #vars1 * #Evars1
562generalize in match (map_partial_preserves_first ?????); #MPPF
563lapply (refl ? (map_partial ??? tv vars))
564cases (map_partial ?????) in ⊢ (???% → ?);
565[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
566#vs #VS >VS in MPPF ⊢ %; #MPPF
567whd in ⊢ (??%% → ?);
568generalize in match (map_fst ???????); #MF
569#E destruct
570whd in ⊢ (??%%); @MF
571qed.
572
573
574(*
575Lemma transform_partial_program2_function:
576  forall p tp i tf,
577  transform_partial_program2 p = OK tp ->
578  In (i, tf) tp.(prog_funct) ->
579  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
580Proof.
581  intros. monadInv H. 
582  eapply In_map_partial; eauto.
583Qed.
584
585Lemma transform_partial_program2_variable:
586  forall p tp i tv,
587  transform_partial_program2 p = OK tp ->
588  In (i, tv) tp.(prog_vars) ->
589  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
590Proof.
591  intros. monadInv H.
592  eapply In_map_partial; eauto.
593Qed.
594
595Lemma transform_partial_program2_main:
596  forall p tp,
597  transform_partial_program2 p = OK tp ->
598  tp.(prog_main) = p.(prog_main).
599Proof.
600  intros. monadInv H. reflexivity.
601Qed.
602
603End TRANSF_PARTIAL_PROGRAM2.
604
605(** The following is a relational presentation of
606  [transform_program_partial2].  Given relations between function
607  definitions and between variable information, it defines a relation
608  between programs stating that the two programs have the same shape
609  (same global names, etc) and that identically-named function definitions
610  are variable information are related. *)
611
612Section MATCH_PROGRAM.
613
614Variable A B V W: Type.
615Variable match_fundef: A -> B -> Prop.
616Variable match_varinfo: V -> W -> Prop.
617
618*)
619
620record matching : Type[1] ≝ {
621  m_A : list ident → Type[0];  m_B : list ident → Type[0];  (* function types *)
622  m_V : Type[0];  m_W : Type[0];  (* variable types *)
623  match_fundef : ∀vs. m_A vs → m_B vs → Prop;
624  match_varinfo : m_V → m_W → Prop
625}.
626
627(* When defining a matching between function entries, quietly enforce equality
628   of the list of global variables (vs and vs'). *)
629
630inductive match_funct_entry (M:matching) : ∀vs,vs'. ident × (m_A M vs) → ident × (m_B M vs') → Prop ≝
631| mfe_intro : ∀vs,id,f1,f2. match_fundef M vs f1 f2 → match_funct_entry M vs vs 〈id,f1〉 〈id,f2〉.
632
633(* but we'll need some care to usefully invert it *)
634
635definition mfe_cast_fn_type : ∀M,vs,vs'. ∀E:vs'=vs. m_B M vs' → m_B M vs ≝
636λM,vs,vs',E. ?.
637>E #m @m
638qed.
639
640let rec match_funct_entry_inv (M:matching)
641  (P:∀vs,id,f,id',f'. Prop)
642  (H:∀vs,id,f,id',f'. match_fundef M vs f f' → P vs id f id' f')
643  vs id f id' f'
644  (MFE:match_funct_entry M vs vs 〈id,f〉 〈id',f'〉) on MFE : P vs id f id' f' ≝
645match 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
646[ mfe_intro vs id f1 f2 MF ⇒ ?
647] (refl ??).
648#E >(K ?? E) @H @MF
649qed.
650
651(* and continue as before *)
652
653inductive match_var_entry (M:matching) : ident × region × (m_V M) → ident × region × (m_W M) → Prop ≝
654| mve_intro : ∀id,r,v1,v2. match_varinfo M v1 v2 → match_var_entry M 〈id,r,v1〉 〈id,r,v2〉.
655
656lemma matching_vars : ∀M.∀p1:program (m_A M) (m_V M).∀p2:program (m_B M) (m_W M).
657  All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2) →
658  prog_var_names … p1 = prog_var_names … p2.
659#M * #vs1 #mn1 #fn1 * #vs2 #mn2 #fn2
660normalize generalize in match vs2;
661elim vs1
662[ * [ // | #h #t * ]
663| * * #id1 #r1 #v1 #tl1 #IH * [ * ]
664  * * #id2 #r2 #v2 #tl2 * *
665  #id #r #v1' #v2' #_ #H
666  whd in ⊢ (??%%); >(IH … H) %
667] qed.
668
669record match_program (M:matching) (p1: program (m_A M) (m_V M)) (p2: program (m_B M) (m_W M)) : Prop ≝ {
670  mp_vars : All2 … (match_var_entry M) (prog_vars … p1) (prog_vars … p2);
671  mp_funct : All2 ?? … (match_funct_entry M (prog_var_names … p1) (prog_var_names … p2)) (prog_funct … p1) (prog_funct ??… p2);
672  mp_main : prog_main … p1 = prog_main … p2
673}.
674
675(*
676End MATCH_PROGRAM.
677*)
678
679(* Now show that all the transformations are instances of match_program. *)
680
681lemma transform_partial_program2_match:
682  ∀A,B,V,W.
683         ∀transf_partial_function: ∀vs. A vs -> res (B vs).
684         ∀transf_partial_variable: V -> res W.
685         ∀p: program A V. ∀tp: program B W.
686  transform_partial_program2 … p transf_partial_function transf_partial_variable = OK ? tp →
687  match_program (mk_matching A B V W
688    (λvs,fd,tfd. transf_partial_function vs … fd = OK ? tfd)
689    (λinfo,tinfo. transf_partial_variable info = OK ? tinfo))
690    p tp.
691#A #B #V #W #transf_partial_function #transf_partial_variable
692* #vars #main #functs * #vars' #main' #functs'
693#T cases (bind_inversion ????? T) -T #fl * #Efl
694generalize in match (map_partial_preserves_first ?????); #MPPF
695lapply (refl ? (map_partial ??? transf_partial_variable vars))
696cases (map_partial ?????) in ⊢ (???% → ?);
697[ 2: #m #M >M in MPPF ⊢ %; #MPPF #E normalize in E; destruct ]
698#vs #VS >VS in MPPF ⊢ %; #MPPF
699whd in ⊢ (??%% → ?);
700generalize in match (map_fst ???????); #MF
701#E destruct
702%
703[ @(map_partial_All2 … VS) * /2/
704| whd in match (prog_var_names ???);
705  whd in match (prog_var_names ???);
706  <MF @(map_partial_All2 … Efl) #id #f1 #f2 /2/
707| //
708] qed.
709
710lemma transform_partial_program_match:
711  ∀A,B,V.
712    ∀trans_partial_function: ∀vs. A vs → res (B vs).
713    ∀p: program A V. ∀tp: program B V.
714  transform_partial_program … p trans_partial_function = OK ? tp →
715  match_program (mk_matching A B V V
716    (λvs,fd,tfd. trans_partial_function vs fd = OK ? tfd)
717    (λv,w. v = w))
718    p tp.
719#A #B #V #tpf
720* #vars #fns #main * #vars' #fns' #main'
721#TPP cases (bind_inversion ????? TPP) -TPP #fns'' * #MAP
722#E normalize in E; destruct
723%
724[ elim vars' // * * #id #r #v #tl #H % /2/
725| @(map_partial_All2 … MAP) #i #f #f' #TPF % @TPF
726| //
727] qed.
728
729lemma transform_program_match:
730  ∀A,B,V.
731    ∀trans_function: ∀vs. A vs → B vs.
732    ∀p: program A V.
733  match_program (mk_matching A B V V
734    (λvs,fd,tfd. trans_function vs fd = tfd)
735    (λv,w. v = w))
736    p (transform_program … p trans_function).
737#A #B #V #tf
738* #vars #fns #main
739%
740[ normalize elim vars // * * #id #r #v #tl #H % /2/
741| whd in match (prog_var_names ???);
742  whd in match (prog_vars ???);
743  elim fns
744  [ //
745  | * #id #f #tl #IH % // % //
746  ]
747| //
748] qed.
749
750(* * * External functions *)
751
752(* * For most languages, the functions composing the program are either
753  internal functions, defined within the language, or external functions
754  (a.k.a. system calls) that emit an event when applied.  We define
755  a type for such functions and some generic transformation functions. *)
756
757record external_function : Type[0] ≝ {
758  ef_id: ident;
759  ef_sig: signature
760}.
761
762definition ExternalFunction ≝ external_function.
763definition external_function_tag ≝ ef_id.
764definition external_function_sig ≝ ef_sig.
765
766inductive fundef (F: Type[0]): Type[0] ≝
767  | Internal: F → fundef F
768  | External: external_function → fundef F.
769
770(* Implicit Arguments External [F]. *)
771(*
772Section TRANSF_FUNDEF.
773
774Variable A B: Type.
775Variable transf: A -> B.
776*)
777definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
778λA,B,transf,fd.
779  match fd with
780  [ Internal f ⇒ Internal ? (transf f)
781  | External ef ⇒ External ? ef
782  ].
783
784(*
785End TRANSF_FUNDEF.
786
787Section TRANSF_PARTIAL_FUNDEF.
788
789Variable A B: Type.
790Variable transf_partial: A -> res B.
791*)
792
793definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
794λA,B,transf_partial,fd.
795  match fd with
796  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
797  | External ef ⇒ OK ? (External ? ef)
798  ].
799(*
800End TRANSF_PARTIAL_FUNDEF.
801*)
802
803
804
805(* Partially merged stuff derived from the prototype cerco compiler. *)
806
807(*
808definition bool_to_Prop ≝
809 λb. match b with [ true ⇒ True | false ⇒ False ].
810
811coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
812*)
813
814(* dpm: should go to standard library *)
815let rec member (i: ident) (eq_i: ident → ident → bool)
816               (g: list ident) on g: Prop ≝
817  match g with
818  [ nil ⇒ False
819  | cons hd tl ⇒
820      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
821  ].
Note: See TracBrowser for help on using the repository browser.