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/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
Note: See TracChangeset for help on using the changeset viewer.