source: src/common/AST.ma @ 1224

Last change on this file since 1224 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File size: 23.8 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * This file defines a number of data types and operations used in
17  the abstract syntax trees of many of the intermediate languages. *)
18
19include "basics/types.ma".
20include "common/Integers.ma".
21include "common/Floats.ma".
22include "ASM/Arithmetic.ma".
23include "common/Identifiers.ma".
24
25
26(* * * Syntactic elements *)
27
28(* Global variables and functions are represented by identifiers with the
29   tag for symbols.  Note that Clight also uses them for locals due to
30   the ambiguous syntax. *)
31
32axiom SymbolTag : String.
33
34definition ident ≝ identifier SymbolTag.
35
36definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?.
37
38definition ident_of_nat : nat → ident ≝ identifier_of_nat ?.
39
40(* XXX backend is currently using untagged words as identifiers. *)
41definition Identifier ≝ Word.
42
43definition Immediate ≝ nat. (* XXX is this the best place to put this? *)
44
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: list ident → Type[0]) (V: Type[0]) : Type[0] := {
286  prog_vars: list (ident × region × V);
287  prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars)));
288  prog_main: ident
289}.
290
291
292definition prog_funct_names ≝ λF,V. λp: program F V.
293  map … \fst (prog_funct … p).
294
295definition prog_var_names ≝ λF,V. λp: program F V.
296  map … (λx. \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. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝
315λA,B,V,p,transf.
316  mk_program B V
317    (prog_vars A V p)
318    (transf_program ?? transf (prog_funct A V p))
319    (prog_main 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
349lemma map_partial_preserves_first:
350 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C).
351  map_partial … f l = OK ? l' →
352   map … \fst l = map … \fst l'.
353 #A #B #C #f #l elim l
354  [ #l' #E normalize in E; destruct %
355  | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?)
356    [2: #err #E destruct
357    | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?)
358      cases (map_partial … f tl) in IH ⊢ %
359      #x #IH normalize in ⊢ (??%? → ?) #ABS destruct
360      >(IH x) // ]]
361qed.
362
363(*
364Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
365  match l with
366  | nil => OK nil
367  | (a, b) :: rem =>
368      match f b with
369      | Error msg => Error (prefix_errmsg a ++ msg)%list
370      | OK c =>
371          do rem' <- map_partial rem;
372          OK ((a, c) :: rem')
373      end
374  end.
375
376Remark In_map_partial:
377  forall l l' a c,
378  map_partial l = OK l' ->
379  In (a, c) l' ->
380  exists b, In (a, b) l /\ f b = OK c.
381Proof.
382  induction l; simpl.
383  intros. inv H. elim H0.
384  intros until c. destruct a as [a1 b1].
385  caseEq (f b1); try congruence.
386  intro c1; intros. monadInv H0.
387  elim H1; intro. inv H0. exists b1; auto.
388  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
389Qed.
390
391Remark map_partial_forall2:
392  forall l l',
393  map_partial l = OK l' ->
394  list_forall2
395    (fun (a_b: A * B) (a_c: A * C) =>
396       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
397    l l'.
398Proof.
399  induction l; simpl.
400  intros. inv H. constructor.
401  intro l'. destruct a as [a b].
402  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
403  constructor. simpl. auto. auto.
404Qed.
405
406End MAP_PARTIAL.
407
408Remark map_partial_total:
409  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
410  map_partial prefix (fun b => OK (f b)) l =
411  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
412Proof.
413  induction l; simpl.
414  auto.
415  destruct a as [a1 b1]. rewrite IHl. reflexivity.
416Qed.
417
418Remark map_partial_identity:
419  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),cmp
420  map_partial prefix (fun b => OK b) l = OK l.
421Proof.
422  induction l; simpl.
423  auto.
424  destruct a as [a1 b1]. rewrite IHl. reflexivity.
425Qed.
426
427Section TRANSF_PARTIAL_PROGRAM.
428
429Variable A B V: Type.
430Variable transf_partial: A -> res B.
431
432Definition prefix_funct_name (id: ident) : errmsg :=
433  MSG "In function " :: CTX id :: MSG ": " :: nil.
434*)
435definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) →  res (program B V) ≝
436λA,B,V,p,transf_partial.
437  do fl ← map_partial … transf_partial (prog_funct … p);
438  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
439
440(*
441Lemma transform_partial_program_function:
442  forall p tp i tf,
443  transform_partial_program p = OK tp ->
444  In (i, tf) tp.(prog_funct) ->
445  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
446Proof.
447  intros. monadInv H. simpl in H0. 
448  eapply In_map_partial; eauto.
449Qed.
450
451Lemma transform_partial_program_main:
452  forall p tp,
453  transform_partial_program p = OK tp ->
454  tp.(prog_main) = p.(prog_main).
455Proof.
456  intros. monadInv H. reflexivity.
457Qed.
458
459Lemma transform_partial_program_vars:
460  forall p tp,
461  transform_partial_program p = OK tp ->
462  tp.(prog_vars) = p.(prog_vars).
463Proof.
464  intros. monadInv H. reflexivity.
465Qed.
466
467End TRANSF_PARTIAL_PROGRAM.
468
469(** The following is a variant of [transform_program_partial] where
470  both the program functions and the additional variable information
471  are transformed by functions that can fail. *)
472
473Section TRANSF_PARTIAL_PROGRAM2.
474
475Variable A B V W: Type.
476Variable transf_partial_function: A -> res B.
477Variable transf_partial_variable: V -> res W.
478
479Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
480  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
481*)
482
483(* CSC: ad hoc lemma, move away? *)
484lemma map_fst:
485 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C').
486  map … \fst l = map … \fst l' →
487  map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'.
488#A #B #C #C' #l elim l
489 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct
490 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ]
491   #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 //
492   >e0 in e1 normalize #H @H ]
493qed.
494
495definition transform_partial_program2 :
496 ∀A,B,V,W. ∀p: program A V.
497  (A (prog_var_names … p) → res (B (prog_var_names ?? p)))
498  →  (V → res W) → res (program B W) ≝
499λA,B,V,W,p, transf_partial_function, transf_partial_variable.
500  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?.
501  (*CSC: interactive mode because of dependent types *)
502  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p))
503  cases (map_partial … transf_partial_variable (prog_vars … p))
504  [ #vl #EQ
505    @(OK (program B W) (mk_program … vl … (prog_main … p)))
506    <(map_fst … (EQ vl (refl …))) @fl
507  | #err #_ @(Error … err)]
508qed.
509
510(*
511Lemma transform_partial_program2_function:
512  forall p tp i tf,
513  transform_partial_program2 p = OK tp ->
514  In (i, tf) tp.(prog_funct) ->
515  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
516Proof.
517  intros. monadInv H. 
518  eapply In_map_partial; eauto.
519Qed.
520
521Lemma transform_partial_program2_variable:
522  forall p tp i tv,
523  transform_partial_program2 p = OK tp ->
524  In (i, tv) tp.(prog_vars) ->
525  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
526Proof.
527  intros. monadInv H.
528  eapply In_map_partial; eauto.
529Qed.
530
531Lemma transform_partial_program2_main:
532  forall p tp,
533  transform_partial_program2 p = OK tp ->
534  tp.(prog_main) = p.(prog_main).
535Proof.
536  intros. monadInv H. reflexivity.
537Qed.
538
539End TRANSF_PARTIAL_PROGRAM2.
540
541(** The following is a relational presentation of
542  [transform_program_partial2].  Given relations between function
543  definitions and between variable information, it defines a relation
544  between programs stating that the two programs have the same shape
545  (same global names, etc) and that identically-named function definitions
546  are variable information are related. *)
547
548Section MATCH_PROGRAM.
549
550Variable A B V W: Type.
551Variable match_fundef: A -> B -> Prop.
552Variable match_varinfo: V -> W -> Prop.
553
554Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
555  match x1, x2 with
556  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
557  end.
558
559Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
560  match x1, x2 with
561  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
562  end.
563
564Definition match_program (p1: program A V) (p2: program B W) : Prop :=
565  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
566  /\ p1.(prog_main) = p2.(prog_main)
567  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
568
569End MATCH_PROGRAM.
570
571Remark transform_partial_program2_match:
572  forall (A B V W: Type)
573         (transf_partial_function: A -> res B)
574         (transf_partial_variable: V -> res W)
575         (p: program A V) (tp: program B W),
576  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
577  match_program
578    (fun fd tfd => transf_partial_function fd = OK tfd)
579    (fun info tinfo => transf_partial_variable info = OK tinfo)
580    p tp.
581Proof.
582  intros. monadInv H. split.
583  apply list_forall2_imply with
584    (fun (ab: ident * A) (ac: ident * B) =>
585       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
586  eapply map_partial_forall2. eauto.
587  intros. destruct v1; destruct v2; simpl in *. auto.
588  split. auto.
589  apply list_forall2_imply with
590    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
591       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
592  eapply map_partial_forall2. eauto.
593  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
594Qed.
595*)
596(* * * External functions *)
597
598(* * For most languages, the functions composing the program are either
599  internal functions, defined within the language, or external functions
600  (a.k.a. system calls) that emit an event when applied.  We define
601  a type for such functions and some generic transformation functions. *)
602
603record external_function : Type[0] ≝ {
604  ef_id: ident;
605  ef_sig: signature
606}.
607
608definition ExternalFunction ≝ external_function.
609definition external_function_tag ≝ ef_id.
610definition external_function_sig ≝ ef_sig.
611
612inductive fundef (F: Type[0]): Type[0] ≝
613  | Internal: F → fundef F
614  | External: external_function → fundef F.
615
616(* Implicit Arguments External [F]. *)
617(*
618Section TRANSF_FUNDEF.
619
620Variable A B: Type.
621Variable transf: A -> B.
622*)
623definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
624λA,B,transf,fd.
625  match fd with
626  [ Internal f ⇒ Internal ? (transf f)
627  | External ef ⇒ External ? ef
628  ].
629
630(*
631End TRANSF_FUNDEF.
632
633Section TRANSF_PARTIAL_FUNDEF.
634
635Variable A B: Type.
636Variable transf_partial: A -> res B.
637*)
638
639definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
640λA,B,transf_partial,fd.
641  match fd with
642  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
643  | External ef ⇒ OK ? (External ? ef)
644  ].
645(*
646End TRANSF_PARTIAL_FUNDEF.
647*)
648
649
650
651(* Partially merged stuff derived from the prototype cerco compiler. *)
652
653(*
654definition bool_to_Prop ≝
655 λb. match b with [ true ⇒ True | false ⇒ False ].
656
657coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
658*)
659
660(* dpm: should go to standard library *)
661let rec member (i: ident) (eq_i: ident → ident → bool)
662               (g: list ident) on g: Prop ≝
663  match g with
664  [ nil ⇒ False
665  | cons hd tl ⇒
666      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
667  ].
668
669(* TODO: merge in comparison definitions from Integers.ma. *)
670inductive Compare: Type[0] ≝
671  Compare_Equal: Compare
672| Compare_NotEqual: Compare
673| Compare_Less: Compare
674| Compare_Greater: Compare
675| Compare_LessEqual: Compare
676| Compare_GreaterEqual: Compare.
677
678(* XXX unused definitions
679inductive Cast: Type[0] ≝
680  Cast_Int: Byte → Cast
681| Cast_AddrSymbol: Identifier → Cast
682| Cast_StackOffset: Immediate → Cast.
683
684inductive Data: Type[0] ≝
685  Data_Reserve: nat → Data
686| Data_Int8: Byte → Data
687| Data_Int16: Word → Data.
688
689inductive DataSize: Type[0] ≝
690  DataSize_Byte: DataSize
691| DataSize_HalfWord: DataSize
692| DataSize_Word: DataSize.
693*)
694
695definition Trace ≝ list Identifier.
696
697inductive op1: Type[0] ≝
698  | op_cast: nat → signedness → nat → op1
699  | op_neg_int: op1          (**r integer opposite *)
700  | op_not_bool: op1         (**r boolean negation  *)
701  | op_not_int: op1          (**r bitwise complement  *)
702  | op_id: op1               (**r identity *)
703  | op_ptr_of_int: op1       (**r int to pointer *)
704  | op_int_of_ptr: op1.      (**r pointer to int *)
705
706inductive op2: Type[0] ≝
707  | op_add: op2         (**r integer addition *)
708  | op_sub: op2         (**r integer subtraction *)
709  | op_mul: op2         (**r integer multiplication *)
710  | op_div: op2         (**r integer signed division *)
711  | op_divu: op2        (**r integer unsigned division *)
712  | op_mod: op2         (**r integer signed modulus *)
713  | op_modu: op2        (**r integer unsigned modulus *)
714  | op_and: op2         (**r bitwise ``and'' *)
715  | op_or: op2          (**r bitwise ``or'' *)
716  | op_xor: op2         (**r bitwise ``xor'' *)
717  | op_shl: op2         (**r left shift *)
718  | op_shr: op2         (**r right signed shift *)
719  | op_shru: op2        (**r right unsigned shift *)
720  | op_cmp: Compare → op2   (**r integer signed comparison *)
721  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
722  | op_addp: op2        (**r addition for a pointer and an integer *)
723  | op_subp: op2        (**r substraction for a pointer and a integer *)
724  | op_subpp: op2
725  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.