source: src/common/AST.ma @ 3367

Last change on this file since 3367 was 2767, checked in by mckinna, 7 years ago

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

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