source: src/common/AST.ma @ 1046

Last change on this file since 1046 was 1046, checked in by mulligan, 8 years ago

syntax of rtlabs was wrong: cast not const. more added to rtlabs --> rtl pass

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