source: src/common/AST.ma @ 2105

Last change on this file since 2105 was 2105, checked in by campbell, 7 years ago

Show some results about globalenvs and program transformations.

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