source: src/common/AST.ma @ 1060

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

work from this morning and yesterday

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