source: src/common/AST.ma @ 1213

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

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

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