Changeset 24


Ignore:
Timestamp:
Aug 27, 2010, 1:21:50 PM (9 years ago)
Author:
campbell
Message:

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

Location:
C-semantics
Files:
3 added
6 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/AST.ma

    r10 r24  
    149149Variable A B V: Type.
    150150Variable transf: A -> B.
    151 
    152 Definition transf_program (l: list (ident * A)) : list (ident * B) :=
    153   List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
    154 
    155 Definition transform_program (p: program A V) : program B V :=
    156   mkprogram
    157     (transf_program p.(prog_funct))
    158     p.(prog_main)
    159     p.(prog_vars).
    160 
    161 Lemma transform_program_function:
    162   forall p i tf,
    163   In (i, tf) (transform_program p).(prog_funct) ->
    164   exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
    165 Proof.
    166   simpl. unfold transf_program. intros.
    167   exploit list_in_map_inv; eauto.
    168   intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst.
    169   exists f; split; auto.
    170 Qed.
    171 
     151*)
     152
     153ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
     154λA,B,transf,l.
     155  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
     156
     157ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
     158λA,B,V,transf,p.
     159  mk_program B V
     160    (transf_program ?? transf (prog_funct A V p))
     161    (prog_main A V p)
     162    (prog_vars A V p).
     163
     164nlemma transform_program_function:
     165  ∀A,B,V,transf,p,i,tf.
     166  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
     167  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
     168nnormalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);
     169#x; nelim x; #i' tf'; *; #e H; ndestruct; @tf'; /2/;
     170nqed.
     171
     172(*
    172173End TRANSF_PROGRAM.
    173174
     
    413414Variable A B: Type.
    414415Variable transf: A -> B.
    415 
    416 Definition transf_fundef (fd: fundef A): fundef B :=
     416*)
     417ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
     418λA,B,transf,fd.
    417419  match fd with
    418   | Internal f => Internal (transf f)
    419   | External ef => External ef
    420   end.
    421 
     420  [ Internal f ⇒ Internal ? (transf f)
     421  | External ef ⇒ External ? ef
     422  ].
     423
     424(*
    422425End TRANSF_FUNDEF.
    423426
  • C-semantics/CexecIO.ma

    r20 r24  
    33
    44include "extralib.ma".
     5include "IOMonad.ma".
    56
    67(* Some experimental definitions for an executable semantics. *)
     
    611612(* IO monad *)
    612613
    613 ninductive IO (T:Type) : Type ≝
    614 | Interact : ident → list eventval → (eventval → IO T) → IO T
    615 | Value : T → IO T
    616 | Wrong : IO T.
    617 
    618 nlet rec bindIO (T,T':Type) (v:IO T) (f:T → IO T') on v : IO T' ≝
    619 match v with
    620 [ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO T T' (k res) f))
    621 | Value v' ⇒ (f v')
    622 | Wrong ⇒ Wrong T'
    623 ].
    624 
    625 nlet rec bindIO2 (T1,T2,T':Type) (v:IO (T1×T2)) (f:T1 → T2 → IO T') on v : IO T' ≝
    626 match v with
    627 [ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO2 T1 T2 T' (k res) f))
    628 | Value v' ⇒ match v' with [ mk_pair v1 v2 ⇒ f v1 v2 ]
    629 | Wrong ⇒ Wrong T'
    630 ].
    631 
    632 ndefinition do_io : ident → list eventval → IO eventval ≝
    633 λfn,args. Interact eventval fn args (λres. Value eventval res).
    634 
    635 ndefinition ret: ∀T. T → (IO T) ≝
    636 λT,x.(Value T x).
    637 
    638 ndefinition err_to_io : ∀T. res T → IO T ≝
    639 λT,v. match v with [ OK v' ⇒ Value T v' | Error ⇒ Wrong T ].
    640 (*ncoercion err_to_io : ∀A.∀c:res A.IO A ≝ err_to_io on _c:res ? to IO ?.*)
    641 ndefinition err_to_io_sig : ∀T.∀P:T → Prop. res (sigma T P) → IO (sigma T P) ≝
    642 λT,P,v. match v with [ OK v' ⇒ Value (sigma T P) v' | Error ⇒ Wrong (sigma T P) ].
    643 ncoercion err_to_io_sig : ∀A.∀P:A → Prop.∀c:res (sigma A P).IO (sigma A P) ≝ err_to_io_sig on _c:res ? to IO ?.
    644 
    645 
    646 (* If the original definitions are vague enough, do I need to do this? *)
    647 notation "! ident v ← e;: e'" right associative with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    648 notation "! 〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    649 interpretation "IO monad bind" 'bindIO e f = (bindIO ? ? e f).
    650 interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ??? e f).
    651 (**)
    652 nlet rec P_io (A:Type) (P:A → CProp[0]) (v:IO A) on v : CProp[0] ≝
    653 match v return λ_.CProp[0] with
    654 [ Wrong ⇒ True
    655 | Value z ⇒ P z
    656 | Interact fn args k ⇒ ∀v'.P_io A P (k v')
    657 ].
    658 
    659 ndefinition P_to_P_option_io : ∀A:Type[0].∀P:A → CProp[0].option (IO A) → CProp[0] ≝
    660   λA,P,a.match a with
    661    [ None ⇒ False
    662    | Some y ⇒ P_io A P y
    663    ].
    664 
    665 nlet rec io_inject_0 (A:Type) (P:A → Prop) (a:IO A) (p:P_io A P a) on a : IO (sigma A P) ≝
    666 (match a return λa'.a=a' → ? with
    667  [ Wrong ⇒ λ_. Wrong ?
    668  | Value c ⇒ λe2. Value ? (sig_intro A P c ?)
    669  | Interact fn args k ⇒ λe2. Interact ? fn args (λv. io_inject_0 A P (k v) ?)
    670  ]) (refl ? a).
    671  (* XXX: odd, can't do both cases at once. *)
    672 ##[ nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
    673 ##| nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
    674 ##] nqed.
    675 
    676 ndefinition io_inject : ∀A.∀P:A → Prop.∀a:option (IO A).∀p:P_to_P_option_io A P a.IO (sigma A P) ≝
    677   λA.λP:A → Prop.λa:option (IO A).λp:P_to_P_option_io A P a.
    678   (match a return λa'.a=a' → IO (sigma A P) with
    679    [ None ⇒ λe1.?
    680    | Some b ⇒ λe1. io_inject_0 A P b ?
    681    ]) (refl ? a).
    682 ##[ nrewrite > e1 in p; nnormalize; *;
    683 ##| nrewrite > e1 in p; nnormalize; //
    684 ##] nqed.
    685 
    686 nlet rec io_eject (A:Type) (P: A → Prop) (a:IO (sigma A P)) on a : IO A ≝
    687 match a with
    688 [ Wrong ⇒ Wrong ?
    689 | Value b ⇒ match b with [ sig_intro w p ⇒ Value ? w]
    690 | Interact fn args k ⇒ Interact ? fn args (λv. io_eject A P (k v))
    691 ].
    692 
    693 ncoercion io_inject :
    694   ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_io ? P a.IO (sigma A P) ≝ io_inject
    695   on a:option (IO ?) to IO (sigma ? ?).
    696 ncoercion io_eject : ∀A.∀P:A → Prop.∀c:IO (sigma A P).IO A ≝ io_eject
    697   on _c:IO (sigma ? ?) to IO ?.
    698 
    699 ndefinition opt_to_io : ∀T.option T → IO T ≝
    700 λT,v. match v with [ None ⇒ Wrong T | Some v' ⇒ Value T v' ].
    701 ncoercion opt_to_io : ∀T.∀v:option T. IO T ≝ opt_to_io on _v:option ? to IO ?.
    702 
    703 nlemma sig_bindIO_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO (sigma A P). ∀f:sigma A P → IO B.
    704   (∀v:A. ∀p:P v. P_io ? P' (f (sig_intro A P v p))) →
    705   P_io ? P' (bindIO (sigma A P) B e f).
    706 #A B P P' e f; nelim e;
    707 ##[ #fn args k IH; #IH'; nwhd; #res; napply IH; //;
    708 ##| #v0; nelim v0; #v Hv IH; nwhd; napply IH;
    709 ##| //;
    710 ##] nqed.
    711 
    712 nlemma sig_bindIO2_OK: ∀A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO (sigma (A×B) P). ∀f: A → B → IO C.
    713   (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io ? P' (f vA vB)) →
    714   P_io ? P' (bindIO2 A B C e f).
    715 #A B C P P' e f; nelim e;
    716 ##[ #fn args k IH; #IH'; nwhd; #res; napply IH; napply IH';
    717 ##| #v0; nelim v0; #v; nelim v; #vA vB Hv IH; napply IH; //;
    718 ##| //;
    719 ##] nqed.
    720 
    721 nlemma opt_bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO B.
    722   (∀v:A. e = Some A v → P_io ? P (f v)) →
    723   P_io ? P (bindIO A B e f).
    724 #A B P e; nelim e; //; #v f H; napply H; //;
    725 nqed.
    726 
    727 nlemma bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:IO A. ∀f: A → IO B.
    728   (∀v:A. P_io ? P (f v)) →
    729   P_io ? P (bindIO A B e f).
    730 #A B P e; nelim e;
    731 ##[ #fn args k IH; #f H; nwhd; #res; napply IH; //;
    732 ##| #v f H; napply H;
    733 ##| //;
    734 ##] nqed.
    735 (*
    736 nlemma bind_assoc_r: ∀A,B,C,e,f,g.
    737   bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g).
    738 #A B C e f g; nelim e;
    739 ##[ #fn args k IH; nwhd in ⊢ (???%);
    740 nnormalize;
    741 *)
    742 
    743 nlemma extract_subset_pair_io: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO C. ∀R:C→Prop.
    744   (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io ? R (Q a b)) →
    745   P_io ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
    746 #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
    747 ##[ *;
    748 ##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
    749 ##] nqed.
     614(* Interactions are function calls that return a value and do not change
     615   the rest of the Clight program's state. *)
     616ndefinition io ≝ mk_interaction (ident × (list eventval)) eventval.
     617
     618ndefinition do_io : ident → list eventval → IO io eventval ≝
     619λfn,args. Interact io eventval 〈fn,args〉 (λres. Value io eventval res).
     620
     621ndefinition ret: ∀T. T → (IO io T) ≝
     622λT,x.(Value io T x).
     623
     624(* Checking types of values given to / received from an external function call. *)
    750625
    751626ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
     
    784659(* execution *)
    785660
    786 nlet rec exec_step (ge:genv) (st:state) on st : (IO (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     661nlet rec exec_step (ge:genv) (st:state) on st : (IO io (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
    787662match st with
    788663[ State f s k e m ⇒
     
    820695          match fn_return f with
    821696          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    822           | _ ⇒ Some ? (Wrong ?)
     697          | _ ⇒ Some ? (Wrong ??)
    823698          ]
    824699      | Kcall _ _ _ _ ⇒
    825700          match fn_return f with
    826701          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
    827           | _ ⇒ Some ? (Wrong ?)
     702          | _ ⇒ Some ? (Wrong ??)
    828703          ]
    829704      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
     
    838713      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
    839714      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    840       | _ ⇒ Some ? (Wrong ?)
     715      | _ ⇒ Some ? (Wrong ??)
    841716      ]
    842717  | Scontinue ⇒
     
    853728      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
    854729      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
    855       | _ ⇒ Some ? (Wrong ?)
     730      | _ ⇒ Some ? (Wrong ??)
    856731      ]
    857732  | Sbreak ⇒
     
    862737      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    863738      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
    864       | _ ⇒ Some ? (Wrong ?)
     739      | _ ⇒ Some ? (Wrong ??)
    865740      ]
    866741  | Sifthenelse a s1 s2 ⇒ Some ? (
     
    886761    [ None ⇒ match fn_return f with
    887762      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
    888       | _ ⇒ Some ? (Wrong ?)
     763      | _ ⇒ Some ? (Wrong ??)
    889764      ]
    890765    | Some a ⇒ Some ? (
     
    896771      ! v ← exec_expr ge e m a;:
    897772      match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
    898                    | _ ⇒ Wrong ? ])
     773                   | _ ⇒ Wrong ?? ])
    899774  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
    900775  | Sgoto lbl ⇒
    901776      match find_label lbl (fn_body f) (call_cont k) with
    902777      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
    903       | None ⇒ Some ? (Wrong ?)
     778      | None ⇒ Some ? (Wrong ??)
    904779      ]
    905780  ]
     
    924799      match res with
    925800      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
    926       | _ ⇒ Some ? (Wrong ?)
     801      | _ ⇒ Some ? (Wrong ??)
    927802      ]
    928803    | Some r' ⇒
     
    934809      ]
    935810    ]
    936   | _ ⇒ Some ? (Wrong ?)
     811  | _ ⇒ Some ? (Wrong ??)
    937812  ]
    938813]. nwhd; //;
     
    1008883nqed.
    1009884
    1010 nlet rec make_initial_state (p:program) : IO (Σs:state. initial_state p s) ≝
     885nlet rec make_initial_state (p:program) : IO io (Σs:state. initial_state p s) ≝
    1011886  let ge ≝ globalenv Genv ?? p in
    1012887  let m0 ≝ init_mem Genv ?? p in
     
    1040915
    1041916nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
    1042  IO (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
     917 IO io (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
    1043918match is_final_state s with
    1044919[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
  • C-semantics/Coqlib.ma

    r10 r24  
    794794  induction l; simpl; congruence.
    795795Qed.
    796 
    797 Lemma list_in_map_inv:
    798   forall (A B: Type) (f: A -> B) (l: list A) (y: B),
    799   In y (List.map f l) -> exists x:A, y = f x /\ In x l.
    800 Proof.
    801   induction l; simpl; intros.
    802   contradiction.
    803   elim H; intro.
    804   exists a; intuition auto.
    805   generalize (IHl y H0). intros [x [EQ IN]].
    806   exists x; tauto.
    807 Qed.
    808 
     796*)
     797nlemma list_in_map_inv:
     798  ∀A,B: Type. ∀f: A -> B. ∀l: list A. ∀y: B.
     799  in_list ? y (map ?? f l) → ∃x:A. y = f x ∧ in_list ? x l.
     800#A B f l; nelim l;
     801##[ nnormalize; #y H; ninversion H;
     802  ##[ #x l' e1 e2; ndestruct;
     803  ##| #x z l' H1 H2 H3 H4; ndestruct;
     804  ##]
     805##| #x l' IH y H; ninversion H;
     806  ##[ nnormalize; #y' l'' e1 e2; ndestruct; @x; @; //;
     807  ##| nnormalize; #h h' t H1 H2 H3 H4; ndestruct;
     808      nelim (IH h H1); #x'; *; #IH1 IH2; @x'; @; /2/;
     809  ##]
     810##] nqed.
     811(*
    809812Lemma list_append_map:
    810813  forall (A B: Type) (f: A -> B) (l1 l2: list A),
  • C-semantics/Csyntax.ma

    r4 r24  
    224224  | LSdefault: statement → labeled_statements
    225225  | LScase: int → statement → labeled_statements → labeled_statements.
     226
     227nlet rec statement_ind2
     228  (P:statement → Prop) (Q:labeled_statements → Prop)
     229  (Ssk:P Sskip)
     230  (Sas:∀e1,e2. P (Sassign e1 e2))
     231  (Sca:∀eo,e,args. P (Scall eo e args))
     232  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     233  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     234  (Swh:∀e,s. P s → P (Swhile e s))
     235  (Sdo:∀e,s. P s → P (Sdowhile e s))
     236  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     237  (Sbr:P Sbreak)
     238  (Sco:P Scontinue)
     239  (Sre:∀eo. P (Sreturn eo))
     240  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     241  (Sla:∀l,s. P s → P (Slabel l s))
     242  (Sgo:∀l. P (Sgoto l))
     243  (LSd:∀s. P s → Q (LSdefault s))
     244  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     245  (s:statement) on s : P s ≝
     246match s with
     247[ Sskip ⇒ Ssk
     248| Sassign e1 e2 ⇒ Sas e1 e2
     249| Scall eo e args ⇒ Sca eo e args
     250| Ssequence s1 s2 ⇒ Ssq s1 s2
     251    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     253| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
     254    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     255    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     256| Swhile e s ⇒ Swh e s
     257    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     258| Sdowhile e s ⇒ Sdo e s
     259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     260| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
     261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
     262    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
     263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3)
     264| Sbreak ⇒ Sbr
     265| Scontinue ⇒ Sco
     266| Sreturn eo ⇒ Sre eo
     267| Sswitch e ls ⇒ Ssw e ls
     268    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls)
     269| Slabel l s ⇒ Sla l s
     270    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     271| Sgoto l ⇒ Sgo l
     272]
     273and labeled_statements_ind2
     274  (P:statement → Prop) (Q:labeled_statements → Prop)
     275  (Ssk:P Sskip)
     276  (Sas:∀e1,e2. P (Sassign e1 e2))
     277  (Sca:∀eo,e,args. P (Scall eo e args))
     278  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
     279  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
     280  (Swh:∀e,s. P s → P (Swhile e s))
     281  (Sdo:∀e,s. P s → P (Sdowhile e s))
     282  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
     283  (Sbr:P Sbreak)
     284  (Sco:P Scontinue)
     285  (Sre:∀eo. P (Sreturn eo))
     286  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
     287  (Sla:∀l,s. P s → P (Slabel l s))
     288  (Sgo:∀l. P (Sgoto l))
     289  (LSd:∀s. P s → Q (LSdefault s))
     290  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     291  (ls:labeled_statements) on ls : Q ls ≝
     292match ls with
     293[ LSdefault s ⇒ LSd s
     294    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     295| LScase i s t ⇒ LSc i s t
     296    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
     297    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t)
     298].
     299
     300ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo.
     301  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo
     302  (λ_,_. I) (λ_,_,_,_,_.I).
    226303
    227304(* * ** Functions *)
  • C-semantics/Globalenvs.ma

    r3 r24  
    4040
    4141(* FIXME: unimplemented stuff in AST.ma
    42 naxiom transform_program: ∀A,B,V:Type. (A → B) → program A V → program B V.
    4342naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V).
    4443naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W).
     
    4645*)
    4746
    48 nrecord GENV : Type[1] ≝ {
     47nrecord GENV : Type[2] ≝ {
    4948(* * ** Types and operations *)
    5049
     
    6766       a value, which must be a pointer with offset 0. *)
    6867
    69   find_symbol: ∀F: Type. genv_t F → ident → option block
     68  find_symbol: ∀F: Type. genv_t F → ident → option block;
    7069   (* * Return the address of the given global symbol, if any. *)
    71 }.
     70
    7271(* * ** Properties of the operations. *)
    7372(*
     
    143142(* * Commutation properties between program transformations
    144143  and operations over global environments. *)
    145 
     144*)*)
    146145  find_funct_ptr_transf:
    147146    ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     
    171170    ∀v : val. ∀tf : B.
    172171    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
    173     ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf;
    174 
     172    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ transf f = tf
     173(*
    175174(* * Commutation properties between partial program transformations
    176175  and operations over global environments. *)
     
    303302    init_mem ?? p' = init_mem ?? p*)
    304303}.
    305 *)
     304
     305
     306nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝
     307match l with
     308[ nil ⇒ a
     309| cons h t ⇒ foldl A B f (f a h) t
     310].
    306311
    307312(* XXX: temporary definition
     
    327332  (λF,ge,v. match v with [ Vptr b o ⇒ if eq o zero then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
    328333  (λF,ge. symbols ? ge) (* find_symbol *)
     334  ?
     335  ?
     336  ?
     337  ?
     338  ?
     339  ?
    329340.
    330 
     341##[ #A B C transf p b f; nelim p; #fns main vars;
     342    nelim fns;
     343    ##[ nnormalize; #H; ndestruct;
     344    ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);
     345        nrewrite > (?:nextfunction ?? = length ? t);
     346        ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
     347            nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     348        ##| nrewrite > (?:nextfunction ?? = length ? t);
     349          ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;
     350              nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     351          ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??%?);
     352            ##[ #H; ndestruct (H); //;
     353            ##| #H; napply IH; napply H;
     354            ##]
     355          ##]
     356        ##]
     357    ##]
     358##| #A B C transf p v f; nelim v;
     359    ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
     360    ##| ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
     361    ##| #b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
     362        nwhd in ⊢ (??%? → ??%?);
     363        ##[ nelim p; #fns main vars; nelim fns;
     364          ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
     365          ##| #h t; nelim h; #f fn IH;
     366              nwhd in ⊢ (??%? → ??%?);
     367              nrewrite > (?:nextfunction ?? = length ? t);
     368              ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
     369                nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     370              ##| nrewrite > (?:nextfunction ?? = length ? t);
     371                ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;
     372                nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     373                ##| napply eqZb_elim; #e; nwhd in ⊢ (??%? → ??%?); #H;
     374                  ##[ ndestruct (H); //;
     375                  ##| napply IH; napply H;
     376                  ##]
     377                ##]
     378              ##]
     379          ##]
     380       ##| #H; ndestruct;
     381       ##]
     382    ##]
     383##| #A B C transf p id; nelim p; #fns main vars;
     384    nelim fns;
     385    ##[ nnormalize; //
     386    ##| #h t; nelim h; #fid fd; nwhd in ⊢ (??%% → ??%%); #IH;
     387        nelim (ident_eq fid id); #e;
     388        ##[ nwhd in ⊢ (??%%);
     389          nrewrite > (?:nextfunction ?? = length ? t);
     390          ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
     391              nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     392          ##| nrewrite > (?:nextfunction ?? = length ? t);
     393            ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     394                nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     395            ##| //
     396            ##]
     397          ##]
     398        ##| nwhd in ⊢ (??%%); nrewrite > IH; napply refl;
     399        ##]
     400    ##]
     401##| //;
     402##| #A B C transf p b tf; nelim p; #fns main vars;
     403    nelim fns;
     404    ##[ nnormalize; #H; ndestruct;
     405    ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     406        nrewrite > (?:nextfunction ?? = length ? t);
     407        ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
     408            nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     409        ##| nrewrite > (?:nextfunction ?? = length ? t);
     410          ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     411              nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     412          ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     413            ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;
     414            ##| #H; napply IH; napply H;
     415            ##]
     416          ##]
     417        ##]
     418    ##]
     419##| #A B C transf p v tf; nelim p; #fns main vars; nelim v;
     420  ##[ nnormalize; #H; ndestruct;
     421  ##| ##2,3: #x; nnormalize; #H; ndestruct;
     422  ##| #b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
     423    ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     424      nelim fns;
     425      ##[ nnormalize; #H; ndestruct;
     426      ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     427          nrewrite > (?:nextfunction ?? = length ? t);
     428          ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
     429              nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     430          ##| nrewrite > (?:nextfunction ?? = length ? t);
     431            ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     432                nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     433            ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     434              ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;
     435              ##| #H; napply IH; napply H;
     436              ##]
     437            ##]
     438          ##]
     439      ##]
     440    ##| nnormalize; #H; ndestruct;
     441    ##]
     442 ##]
     443##] nqed.
     444         
    331445(*
    332446(** The rest of this library is a straightforward implementation of
  • C-semantics/Mem.ma

    r15 r24  
    15031503    nrewrite > (high_bound_free … ne);
    15041504    #Hval; #Hlo; #Hhi; #Hal;
    1505     @; /2/; @; //; napply (valid_block_free_2 … Hval);
     1505    @; ##[ @; //; napply (valid_block_free_2 … Hval); ##| /2/ ##]
    15061506##] nqed.
    15071507
Note: See TracChangeset for help on using the changeset viewer.