Changeset 24 for C-semantics/CexecIO.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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〉)
Note: See TracChangeset for help on using the changeset viewer.