source: src/common/AST.ma @ 1268

Last change on this file since 1268 was 1268, checked in by sacerdot, 9 years ago

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

File size: 23.3 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * This file defines a number of data types and operations used in
17  the abstract syntax trees of many of the intermediate languages. *)
18
19include "basics/types.ma".
20include "common/Integers.ma".
21include "common/Floats.ma".
22include "ASM/Arithmetic.ma".
23include "common/Identifiers.ma".
24
25
26(* * * Syntactic elements *)
27
28(* Global variables and functions are represented by identifiers with the
29   tag for symbols.  Note that Clight also uses them for locals due to
30   the ambiguous syntax. *)
31
32axiom SymbolTag : String.
33
34definition ident ≝ identifier SymbolTag.
35
36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
37
38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
39
40definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
41
42(* dpm: not needed
43inductive quantity: Type[0] ≝
44  | q_int: Byte → quantity
45  | q_offset: quantity
46  | q_ptr: quantity.
47 
48inductive abstract_size: Type[0] ≝
49  | size_q: quantity → abstract_size
50  | size_prod: list abstract_size → abstract_size
51  | size_sum: list abstract_size → abstract_size
52  | size_array: nat → abstract_size → abstract_size.
53*)
54
55
56(* Memory spaces *)
57
58inductive region : Type[0] ≝
59  | Any : region
60  | Data : region
61  | IData : region
62  | PData : region
63  | XData : region
64  | Code : region.
65
66definition eq_region : region → region → bool ≝
67λr1,r2.
68  match r1 with
69  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
70  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
71  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
72  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
73  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
74  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
75  ].
76
77lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
78  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
79  P (eq_region r1 r2).
80#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
81try ( @Ptrue // )
82@Pfalse % #E destruct
83qed.
84
85lemma reflexive_eq_region: ∀r. eq_region r r = true.
86 * //
87qed.
88
89definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
90#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
91
92definition size_pointer : region → nat ≝
93λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
94
95(* We maintain some reasonable type information through the front end of the
96   compiler. *)
97
98inductive signedness : Type[0] ≝
99  | Signed: signedness
100  | Unsigned: signedness.
101
102inductive intsize : Type[0] ≝
103  | I8: intsize
104  | I16: intsize
105  | I32: intsize.
106
107(* * Float types come in two sizes: 32 bits (single precision)
108  and 64-bit (double precision). *)
109
110inductive floatsize : Type[0] ≝
111  | F32: floatsize
112  | F64: floatsize.
113
114inductive typ : Type[0] ≝
115  | ASTint : intsize → signedness → typ
116  | ASTptr : region → typ
117  | ASTfloat : floatsize → typ.
118
119(* XXX aliases *)
120definition SigType ≝ typ.
121definition SigType_Int ≝ ASTint I32 Unsigned.
122(*
123| SigType_Float: SigType
124*)
125definition SigType_Ptr ≝ ASTptr Any.
126
127(* Define these carefully so that we always know that the result is nonzero,
128   and can be used in dependent types of the form (S n).
129   (At the time of writing this is only used for bitsize_of_intsize.) *)
130
131definition size_intsize : intsize → nat ≝
132λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
133
134definition bitsize_of_intsize : intsize → nat ≝
135λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
136
137definition eq_intsize : intsize → intsize → bool ≝
138λsz1,sz2.
139  match sz1 with
140  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
141  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
142  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
143  ].
144
145lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
146  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
147* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
148qed.
149
150lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
151* @refl
152qed.
153
154lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
155* * * #NE try @refl @False_ind @NE @refl
156qed.
157
158(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
159   if it is returns [e1] where the type of [n] has its dependency on [sz1]
160   changed to [sz2], and if not returns [e2]. *)
161let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
162  P sz1 → (P sz2 → A) → A → A ≝
163match sz1 return λsz. P sz → (P sz2 → A) → A → A with
164[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
165| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
166| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
167].
168
169lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
170  intsize_eq_elim A sz sz P p f d = f p.
171#A * //
172qed.
173
174lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
175  (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).
176#A * * #P #p #f #d #Q #Hne #Heq
177[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
178| *: whd in ⊢ (?%) @Hne % #E destruct
179] qed.
180
181
182(* A type for the integers that appear in the semantics. *)
183definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
184
185definition repr : ∀sz:intsize. nat → bvint sz ≝
186λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
187
188definition size_floatsize : floatsize → nat ≝
189λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
190
191definition typesize : typ → nat ≝ λty.
192  match ty with
193  [ ASTint sz _ ⇒ size_intsize sz
194  | ASTptr r ⇒ size_pointer r
195  | ASTfloat sz ⇒ size_floatsize sz ].
196
197lemma typesize_pos: ∀ty. typesize ty > 0.
198*; try *; try * /2/ qed.
199
200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
201* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
202
203lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
204#t1 #t2 cases t1 cases t2
205[ %1 @refl
206| 2,3: #ty %2 % #H destruct
207| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
208]
209qed.
210
211(* * Additionally, function definitions and function calls are annotated
212  by function signatures indicating the number and types of arguments,
213  as well as the type of the returned value if any.  These signatures
214  are used in particular to determine appropriate calling conventions
215  for the function. *)
216
217record signature : Type[0] ≝ {
218  sig_args: list typ;
219  sig_res: option typ
220}.
221
222(* XXX aliases *)
223definition Signature ≝ signature.
224definition signature_args ≝ sig_args.
225definition signature_return ≝ sig_res.
226
227definition proj_sig_res : signature → typ ≝ λs.
228  match sig_res s with
229  [ None ⇒ ASTint I32 Unsigned
230  | Some t ⇒ t
231  ].
232
233(* * Memory accesses (load and store instructions) are annotated by
234  a ``memory chunk'' indicating the type, size and signedness of the
235  chunk of memory being accessed. *)
236
237inductive memory_chunk : Type[0] ≝
238  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
239  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
240  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
241  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
242  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
243  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
244  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
245  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
246
247definition typ_of_memory_chunk : memory_chunk → typ ≝
248λc. match c with
249[ Mint8signed ⇒ ASTint I8 Signed
250| Mint8unsigned ⇒ ASTint I8 Unsigned
251| Mint16signed ⇒ ASTint I16 Signed
252| Mint16unsigned ⇒ ASTint I16 Unsigned
253| Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
254| Mfloat32 ⇒ ASTfloat F32
255| Mfloat64 ⇒ ASTfloat F64
256| Mpointer r ⇒ ASTptr r
257].
258
259(* * Initialization data for global variables. *)
260
261inductive init_data: Type[0] ≝
262  | Init_int8: bvint I8 → init_data
263  | Init_int16: bvint I16 → init_data
264  | Init_int32: bvint I32 → init_data
265  | Init_float32: float → init_data
266  | Init_float64: float → init_data
267  | Init_space: nat → init_data
268  | Init_null: region → init_data
269  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
270
271(* * Whole programs consist of:
272- a collection of function definitions (name and description);
273- the name of the ``main'' function that serves as entry point in the program;
274- a collection of global variable declarations, consisting of
275  a name, initialization data, and additional information.
276
277The type of function descriptions and that of additional information
278for variables vary among the various intermediate languages and are
279taken as parameters to the [program] type.  The other parts of whole
280programs are common to all languages. *)
281
282record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := {
283  prog_vars: list (ident × region × V);
284  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
285  prog_main: ident
286}.
287
288
289definition prog_funct_names ≝ λF,V. λp: program F V.
290  map … \fst (prog_funct … p).
291
292definition prog_var_names ≝ λF,V. λp: program F V.
293  map … (λx. \fst (\fst x)) (prog_vars … p).
294
295(* * * Generic transformations over programs *)
296
297(* * We now define a general iterator over programs that applies a given
298  code transformation function to all function descriptions and leaves
299  the other parts of the program unchanged. *)
300(*
301Section TRANSF_PROGRAM.
302
303Variable A B V: Type.
304Variable transf: A -> B.
305*)
306
307definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
308λA,B,transf,l.
309  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
310
311definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
312λA,B,V,p,transf.
313  mk_program B V
314    (prog_vars A V p)
315    (transf_program ?? transf (prog_funct A V p))
316    (prog_main A V p).
317(*
318lemma transform_program_function:
319  ∀A,B,V,transf,p,i,tf.
320  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
321  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
322normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
323#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
324qed.
325*)
326(*
327End TRANSF_PROGRAM.
328
329(** The following is a variant of [transform_program] where the
330  code transformation function can fail and therefore returns an
331  option type. *)
332
333Open Local Scope error_monad_scope.
334Open Local Scope string_scope.
335
336Section MAP_PARTIAL.
337
338Variable A B C: Type.
339Variable prefix_errmsg: A -> errmsg.
340Variable f: B -> res C.
341*)
342definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
343                         list (A × B) → res (list (A × C)) ≝
344λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
345
346lemma map_partial_preserves_first:
347 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
348  map_partial … f l = OK ? l' →
349   map … \fst l = map … \fst l'.
350 #A #B #C #f #l elim l
351  [ #l' #E normalize in E; destruct %
352  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
353    [2: #err #E destruct
354    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
355      cases (map_partial … f tl) in IH ⊢ %
356      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
357      >(IH x) // ]]
358qed.
359
360(*
361Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
362  match l with
363  | nil => OK nil
364  | (a, b) :: rem =>
365      match f b with
366      | Error msg => Error (prefix_errmsg a ++ msg)%list
367      | OK c =>
368          do rem' <- map_partial rem;
369          OK ((a, c) :: rem')
370      end
371  end.
372
373Remark In_map_partial:
374  forall l l' a c,
375  map_partial l = OK l' ->
376  In (a, c) l' ->
377  exists b, In (a, b) l /\ f b = OK c.
378Proof.
379  induction l; simpl.
380  intros. inv H. elim H0.
381  intros until c. destruct a as [a1 b1].
382  caseEq (f b1); try congruence.
383  intro c1; intros. monadInv H0.
384  elim H1; intro. inv H0. exists b1; auto.
385  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
386Qed.
387
388Remark map_partial_forall2:
389  forall l l',
390  map_partial l = OK l' ->
391  list_forall2
392    (fun (a_b: A * B) (a_c: A * C) =>
393       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
394    l l'.
395Proof.
396  induction l; simpl.
397  intros. inv H. constructor.
398  intro l'. destruct a as [a b].
399  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
400  constructor. simpl. auto. auto.
401Qed.
402
403End MAP_PARTIAL.
404
405Remark map_partial_total:
406  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
407  map_partial prefix (fun b => OK (f b)) l =
408  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
409Proof.
410  induction l; simpl.
411  auto.
412  destruct a as [a1 b1]. rewrite IHl. reflexivity.
413Qed.
414
415Remark map_partial_identity:
416  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
417  map_partial prefix (fun b => OK b) l = OK l.
418Proof.
419  induction l; simpl.
420  auto.
421  destruct a as [a1 b1]. rewrite IHl. reflexivity.
422Qed.
423
424Section TRANSF_PARTIAL_PROGRAM.
425
426Variable A B V: Type.
427Variable transf_partial: A -> res B.
428
429Definition prefix_funct_name (id: ident) : errmsg :=
430  MSG "In function " :: CTX id :: MSG ": " :: nil.
431*)
432definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
433λA,B,V,p,transf_partial.
434  do fl ← map_partial … transf_partial (prog_funct … p);
435  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
436
437(*
438Lemma transform_partial_program_function:
439  forall p tp i tf,
440  transform_partial_program p = OK tp ->
441  In (i, tf) tp.(prog_funct) ->
442  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
443Proof.
444  intros. monadInv H. simpl in H0. 
445  eapply In_map_partial; eauto.
446Qed.
447
448Lemma transform_partial_program_main:
449  forall p tp,
450  transform_partial_program p = OK tp ->
451  tp.(prog_main) = p.(prog_main).
452Proof.
453  intros. monadInv H. reflexivity.
454Qed.
455
456Lemma transform_partial_program_vars:
457  forall p tp,
458  transform_partial_program p = OK tp ->
459  tp.(prog_vars) = p.(prog_vars).
460Proof.
461  intros. monadInv H. reflexivity.
462Qed.
463
464End TRANSF_PARTIAL_PROGRAM.
465
466(** The following is a variant of [transform_program_partial] where
467  both the program functions and the additional variable information
468  are transformed by functions that can fail. *)
469
470Section TRANSF_PARTIAL_PROGRAM2.
471
472Variable A B V W: Type.
473Variable transf_partial_function: A -> res B.
474Variable transf_partial_variable: V -> res W.
475
476Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
477  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
478*)
479
480(* CSC: ad hoc lemma, move away? *)
481lemma map_fst:
482 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
483  map … \fst l = map … \fst l' →
484  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
485#A #B #C #C' #l elim l
486 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
487 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
488   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
489   >e0 in e1; normalize #H @H ]
490qed.
491
492definition transform_partial_program2 :
493 ∀A,B,V,W. ∀p: program A V.
494  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
495  →  (V → res W) → res (program B W) ≝
496λA,B,V,W,p, transf_partial_function, transf_partial_variable.
497  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
498  (*CSC: interactive mode because of dependent types *)
499  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
500  cases (map_partial … transf_partial_variable (prog_vars … p))
501  [ #vl #EQ
502    @(OK (program B W) (mk_program … vl … (prog_main … p)))
503    <(map_fst … (EQ vl (refl …))) @fl
504  | #err #_ @(Error … err)]
505qed.
506
507(*
508Lemma transform_partial_program2_function:
509  forall p tp i tf,
510  transform_partial_program2 p = OK tp ->
511  In (i, tf) tp.(prog_funct) ->
512  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
513Proof.
514  intros. monadInv H. 
515  eapply In_map_partial; eauto.
516Qed.
517
518Lemma transform_partial_program2_variable:
519  forall p tp i tv,
520  transform_partial_program2 p = OK tp ->
521  In (i, tv) tp.(prog_vars) ->
522  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
523Proof.
524  intros. monadInv H.
525  eapply In_map_partial; eauto.
526Qed.
527
528Lemma transform_partial_program2_main:
529  forall p tp,
530  transform_partial_program2 p = OK tp ->
531  tp.(prog_main) = p.(prog_main).
532Proof.
533  intros. monadInv H. reflexivity.
534Qed.
535
536End TRANSF_PARTIAL_PROGRAM2.
537
538(** The following is a relational presentation of
539  [transform_program_partial2].  Given relations between function
540  definitions and between variable information, it defines a relation
541  between programs stating that the two programs have the same shape
542  (same global names, etc) and that identically-named function definitions
543  are variable information are related. *)
544
545Section MATCH_PROGRAM.
546
547Variable A B V W: Type.
548Variable match_fundef: A -> B -> Prop.
549Variable match_varinfo: V -> W -> Prop.
550
551Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
552  match x1, x2 with
553  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
554  end.
555
556Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
557  match x1, x2 with
558  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
559  end.
560
561Definition match_program (p1: program A V) (p2: program B W) : Prop :=
562  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
563  /\ p1.(prog_main) = p2.(prog_main)
564  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
565
566End MATCH_PROGRAM.
567
568Remark transform_partial_program2_match:
569  forall (A B V W: Type)
570         (transf_partial_function: A -> res B)
571         (transf_partial_variable: V -> res W)
572         (p: program A V) (tp: program B W),
573  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
574  match_program
575    (fun fd tfd => transf_partial_function fd = OK tfd)
576    (fun info tinfo => transf_partial_variable info = OK tinfo)
577    p tp.
578Proof.
579  intros. monadInv H. split.
580  apply list_forall2_imply with
581    (fun (ab: ident * A) (ac: ident * B) =>
582       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
583  eapply map_partial_forall2. eauto.
584  intros. destruct v1; destruct v2; simpl in *. auto.
585  split. auto.
586  apply list_forall2_imply with
587    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
588       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
589  eapply map_partial_forall2. eauto.
590  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
591Qed.
592*)
593(* * * External functions *)
594
595(* * For most languages, the functions composing the program are either
596  internal functions, defined within the language, or external functions
597  (a.k.a. system calls) that emit an event when applied.  We define
598  a type for such functions and some generic transformation functions. *)
599
600record external_function : Type[0] ≝ {
601  ef_id: ident;
602  ef_sig: signature
603}.
604
605definition ExternalFunction ≝ external_function.
606definition external_function_tag ≝ ef_id.
607definition external_function_sig ≝ ef_sig.
608
609inductive fundef (F: Type[0]): Type[0] ≝
610  | Internal: F → fundef F
611  | External: external_function → fundef F.
612
613(* Implicit Arguments External [F]. *)
614(*
615Section TRANSF_FUNDEF.
616
617Variable A B: Type.
618Variable transf: A -> B.
619*)
620definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
621λA,B,transf,fd.
622  match fd with
623  [ Internal f ⇒ Internal ? (transf f)
624  | External ef ⇒ External ? ef
625  ].
626
627(*
628End TRANSF_FUNDEF.
629
630Section TRANSF_PARTIAL_FUNDEF.
631
632Variable A B: Type.
633Variable transf_partial: A -> res B.
634*)
635
636definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
637λA,B,transf_partial,fd.
638  match fd with
639  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
640  | External ef ⇒ OK ? (External ? ef)
641  ].
642(*
643End TRANSF_PARTIAL_FUNDEF.
644*)
645
646
647
648(* Partially merged stuff derived from the prototype cerco compiler. *)
649
650(*
651definition bool_to_Prop ≝
652 λb. match b with [ true ⇒ True | false ⇒ False ].
653
654coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
655*)
656
657(* dpm: should go to standard library *)
658let rec member (i: ident) (eq_i: ident → ident → bool)
659               (g: list ident) on g: Prop ≝
660  match g with
661  [ nil ⇒ False
662  | cons hd tl ⇒
663      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
664  ].
665
666(* TODO: merge in comparison definitions from Integers.ma. *)
667inductive Compare: Type[0] ≝
668  Compare_Equal: Compare
669| Compare_NotEqual: Compare
670| Compare_Less: Compare
671| Compare_Greater: Compare
672| Compare_LessEqual: Compare
673| Compare_GreaterEqual: Compare.
674
675inductive op1: Type[0] ≝
676  | op_cast: nat → signedness → nat → op1
677  | op_neg_int: op1          (**r integer opposite *)
678  | op_not_bool: op1         (**r boolean negation  *)
679  | op_not_int: op1          (**r bitwise complement  *)
680  | op_id: op1               (**r identity *)
681  | op_ptr_of_int: op1       (**r int to pointer *)
682  | op_int_of_ptr: op1.      (**r pointer to int *)
683
684inductive op2: Type[0] ≝
685  | op_add: op2         (**r integer addition *)
686  | op_sub: op2         (**r integer subtraction *)
687  | op_mul: op2         (**r integer multiplication *)
688  | op_div: op2         (**r integer signed division *)
689  | op_divu: op2        (**r integer unsigned division *)
690  | op_mod: op2         (**r integer signed modulus *)
691  | op_modu: op2        (**r integer unsigned modulus *)
692  | op_and: op2         (**r bitwise ``and'' *)
693  | op_or: op2          (**r bitwise ``or'' *)
694  | op_xor: op2         (**r bitwise ``xor'' *)
695  | op_shl: op2         (**r left shift *)
696  | op_shr: op2         (**r right signed shift *)
697  | op_shru: op2        (**r right unsigned shift *)
698  | op_cmp: Compare → op2   (**r integer signed comparison *)
699  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
700  | op_addp: op2        (**r addition for a pointer and an integer *)
701  | op_subp: op2        (**r substraction for a pointer and a integer *)
702  | op_subpp: op2
703  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.