source: src/common/AST.ma @ 2624

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

Properly evict unused and axiomatised Floats.

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