source: src/common/AST.ma @ 1139

Last change on this file since 1139 was 1139, checked in by campbell, 9 years ago

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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