source: src/common/AST.ma @ 1047

Last change on this file since 1047 was 1047, checked in by mulligan, 9 years ago

more work from today

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