source: src/common/AST.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 6 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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