Ignore:
Timestamp:
Jan 23, 2012, 6:31:27 PM (7 years ago)
Author:
campbell
Message:

Update Cminor and RTLabs semantics to use new monad definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1601 r1655  
    8989definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
    9090λge,st.
    91 match st with
     91match st return λ_. IO ??? with
    9292[ State f fs m ⇒
    9393  let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in
    94   match s return λs. labels_present ? s → ? with
    95   [ St_skip l ⇒ λH. ret ? 〈E0, build_state f fs m l ?〉
    96   | St_cost cl l ⇒ λH. ret ? 〈Echarge cl, build_state f fs m l ?〉
     94  match s return λs. labels_present ? s → IO ??? with
     95  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
     96  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
    9797  | St_const r cst l ⇒ λH.
    9898      ! v ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) (sp f) cst);
    9999      ! locals ← reg_store r v (locals f);
    100       ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     100      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    101101  | St_op1 _ _ op dst src l ⇒ λH.
    102102      ! v ← reg_retrieve (locals f) src;
    103103      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    104104      ! locals ← reg_store dst v' (locals f);
    105       ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     105      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    106106  | St_op2 op dst src1 src2 l ⇒ λH.
    107107      ! v1 ← reg_retrieve (locals f) src1;
     
    109109      ! v' ← opt_to_res … (msg FailedOp) (eval_binop op v1 v2);
    110110      ! locals ← reg_store dst v' (locals f);
    111       ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     111      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    112112  | St_load chunk addr dst l ⇒ λH.
    113113      ! vaddr ← reg_retrieve (locals f) addr;
    114114      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    115115      ! locals ← reg_store dst v (locals f);
    116       ret ? 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
     116      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
    117117  | St_store chunk addr src l ⇒ λH.
    118118      ! vaddr ← reg_retrieve (locals f) addr;
    119119      ! v ← reg_retrieve (locals f) src;
    120120      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    121       ret ? 〈E0, build_state f fs m' l ?〉
     121      return 〈E0, build_state f fs m' l ?〉
    122122  | St_call_id id args dst l ⇒ λH.
    123123      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    124124      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    125       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    126       ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     125      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     126      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    127127  | St_call_ptr frs args dst l ⇒ λH.
    128128      ! fv ← reg_retrieve (locals f) frs;
    129129      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    130       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    131       ret ? 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     130      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     131      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
    132132  | St_tailcall_id id args ⇒ λH.
    133133      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    134134      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    135       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    136       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
     135      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     136      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    137137  | St_tailcall_ptr frs args ⇒ λH.
    138138      ! fv ← reg_retrieve (locals f) frs;
    139139      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    140       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    141       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
     140      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
     141      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    142142
    143143  | St_cond src ltrue lfalse ⇒ λH.
    144144      ! v ← reg_retrieve (locals f) src;
    145145      ! b ← eval_bool_of_val v;
    146       ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
     146      return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
    147147
    148148  | St_jumptable r ls ⇒ λH.
     
    151151      [ Vint _ i ⇒
    152152          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
    153           [ None ⇒ λ_. Wrong ??? (msg BadJumpTable)
    154           | Some l ⇒ λE. ret ? 〈E0, build_state f fs m l ?〉
     153          [ None ⇒ λ_. Error ? (msg BadJumpTable)
     154          | Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉
    155155          ] (refl ??)
    156       | _ ⇒ Wrong ??? (msg BadJumpValue)
     156      | _ ⇒ Error ? (msg BadJumpValue)
    157157      ]
    158158
    159159  | St_return ⇒ λH.
    160160      ! v ← match f_result (func f) with
    161             [ None ⇒ ret ? (None ?)
     161            [ None ⇒ return (None ?)
    162162            | Some rt ⇒
    163163                let 〈r,ty〉 ≝ rt in
    164164                ! v ← reg_retrieve (locals f) r;
    165                 ret ? (Some ? v)
     165                return (Some ? v)
    166166            ];
    167       ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
     167      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    168168  ] (f_closed (func f) (next f) s ?)
    169169| Callstate fd params dst fs m ⇒
    170     match fd with
     170    match fd return λ_. IO ??? with
    171171    [ Internal fn ⇒
    172172        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
     
    174174           here *)
    175175        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    176         ret ? 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
     176        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
    177177    | External fn ⇒
    178         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     178        ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn)));
    179179        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    180         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
     180        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    181181    ]
    182182| Returnstate v dst fs m ⇒
     
    189189                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
    190190                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
    191         ret ? 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
     191        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
    192192    ]
    193193]. try @(next_ok f) try @lookup_lookup_present try @H
     
    250250.
    251251
     252lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.
     253  (∀a. e = OK A a → f a = OK ? v → P v) →
     254  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
     255#A #B *
     256[ #a #f #v #P #H #E whd in E:(??%?); @(H a) //
     257| #m #f #v #P #H #E whd in E:(??%?); destruct
     258] qed.
     259
     260lemma bind_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
     261  (∀a. e = OK A a → f a = OK B v → P v) →
     262  (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     263#O #I #A #B *
     264[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
     265  [ #v' #E normalize in E; destruct @refl | #m #E normalize in E; destruct ] ]
     266| #m #f #v #P #H #E whd in E:(??%?); destruct
     267] qed.
     268
    252269lemma bindIO_value : ∀O,I,A,B,e,f,v. ∀P:B → Prop.
    253270  (∀a. e = Value ??? a → f a = Value ??? v → P v) →
     
    270287  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    271288  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
    272   | #r #c #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #locals' #Eloc #E whd in E:(??%?); destruct % %
    273   | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
    274   | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v1 #Ev1 @bindIO_value #v2 #Ev2 @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
    275   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
    276   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #v' #Ev'  @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct % %
    277   | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
    278   | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    279   | #id #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #b #Eb @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    280   | #r #rs #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #fd #Efd  @bindIO_value #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
    281   | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev @bindIO_value #b #Eb #E whd in E:(??%?); destruct % %
    282   | #r #ls #LP whd in ⊢ (??%? → ?); @bindIO_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
    283   | #LP whd in ⊢ (??%? → ?); @bindIO_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bindIO_value #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
     289  | #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
     290  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     291  | #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     292  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     293  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
     294  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ????) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
     295  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     296  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     297  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
     298  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
     299  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ]
     300  | #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5
    284301  ]
    285302| * #fn #args #retdst #stk #m #tr #s'
    286303  whd in ⊢ (??%? → ?);
    287   [ @bindIO_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
     304  [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
    288305    #E destruct %4
    289   | @bindIO_value #evargs #Eargs @bindIO_value #evres #Eres whd in Eres:(??%?);
    290     destruct
     306  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
    291307  ]
    292308| #v #r * [2: #f #fs ] #m #tr #s'
    293309  whd in ⊢ (??%? → ?);
    294   [ @bindIO_value #loc #Eloc #E whd in E:(??%?); destruct
     310  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
    295311    %6 cases f #func #locals #next #next_ok #sp #retdst %
    296312  | #E destruct
Note: See TracChangeset for help on using the changeset viewer.