source: src/common/AST.ma @ 1465

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

Dead code removed.

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