source: src/common/AST.ma @ 1057

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

changes from today

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