source: src/common/AST.ma @ 1059

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

work from today, bit of a mess at the moment

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