Changeset 1655


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

Update Cminor and RTLabs semantics to use new monad definitions.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1626 r1655  
    295295definition eval_step : genv → state → IO io_out io_in (trace × state) ≝
    296296λge,st.
    297 match st with
    298 [ State f s en fInv Inv m sp k kInv st ⇒
    299     match s return λs. stmt_inv f en s → ? with
     297match st return λ_. IO ??? with
     298[ State f s en fInv Inv m sp k kInv st ⇒ err_to_io ??? (
     299    match s return λs. stmt_inv f en s → res (trace × state) with
    300300    [ St_skip ⇒ λInv.
    301         match k return λk. cont_inv f en k → ? with
    302         [ Kseq s' k' ⇒ λkInv. ret ? 〈E0, State f s' en fInv ? m sp k' ? st〉
    303         | Kblock k' ⇒ λkInv. ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
     301        match k return λk. cont_inv f en k → res ? with
     302        [ Kseq s' k' ⇒ λkInv. return 〈E0, State f s' en fInv ? m sp k' ? st〉
     303        | Kblock k' ⇒ λkInv. return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    304304          (* cminor allows functions without an explicit return statement *)
    305         | Kend ⇒ λkInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
     305        | Kend ⇒ λkInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    306306        ] kInv
    307307    | St_assign _ id e ⇒ λInv.
    308308        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    309309        let en' ≝ update_present ?? en id ? v in
    310         ret ? 〈tr, State f St_skip en' ? ? m sp k ? st〉
     310        return 〈tr, State f St_skip en' ? ? m sp k ? st〉
    311311    | St_store _ _ chunk edst e ⇒ λInv.
    312312        ! 〈tr,vdst〉 ← eval_expr ge ? edst en ? sp m;
    313313        ! 〈tr',v〉 ← eval_expr ge ? e en ? sp m;
    314314        ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vdst v);
    315         ret ? 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
     315        return 〈tr ⧺ tr', State f St_skip en fInv ? m' sp k ? st〉
    316316
    317317    | St_call dst ef args ⇒ λInv.
     
    319319        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    320320        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    321         ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     321        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    322322    | St_tailcall ef args ⇒ λInv.
    323323        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    324324        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    325325        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    326         ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
     326        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327327       
    328     | St_seq s1 s2 ⇒ λInv. ret ? 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
     328    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
    329329    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
    330330        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    331331        ! b ← eval_bool_of_val v;
    332         ret ? 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
    333     | St_loop s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
    334     | St_block s ⇒ λInv. ret ? 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
     332        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
     333    | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
     334    | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
    335335    | St_exit n ⇒ λInv.
    336336        ! k' ← k_exit n k ?? kInv;
    337         ret ? 〈E0, State f St_skip en fInv ? m sp k' ? st〉
     337        return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    338338    | St_switch sz _ e cs default ⇒ λInv.
    339339        ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
     
    341341        [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    342342            ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
    343             ret ? 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    344             (Wrong ??? (msg BadSwitchValue))
    345         | _ ⇒ Wrong ??? (msg BadSwitchValue)
     343            return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
     344            (Error ? (msg BadSwitchValue))
     345        | _ ⇒ Error ? (msg BadSwitchValue)
    346346        ]
    347347    | St_return eo ⇒
    348348        match eo return λeo. stmt_inv f en (St_return eo) → ? with
    349         [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
     349        [ None ⇒ λInv. return 〈E0, Returnstate (None ?) (free m sp) st〉
    350350        | Some e ⇒
    351351            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    352352              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    353               ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉
     353              return 〈tr, Returnstate (Some ? v) (free m sp) st〉
    354354            ]
    355355        ]
    356     | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
     356    | St_label l s' ⇒ λInv. return 〈E0, State f s' en fInv ? m sp k ? st〉
    357357    | St_goto l ⇒ λInv.
    358358        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
    359           ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
     359          return 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
    360360        ]
    361361    | St_cost l s' ⇒ λInv.
    362         ret ? 〈Echarge l, State f s' en fInv ? m sp k ? st〉
    363     ] Inv
     362        return 〈Echarge l, State f s' en fInv ? m sp k ? st〉
     363    ] Inv)
    364364| Callstate fd args m st ⇒
    365365    match fd with
    366     [ Internal f ⇒
     366    [ Internal f ⇒ err_to_io ?? (trace × state) (
    367367        let 〈m',sp〉 ≝ alloc m 0 (f_stacksize f) Any in
    368368        ! en ← bind_params args (f_params f);
    369         ret ? 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉
     369        return 〈E0, State f (f_body f) (init_locals en (f_vars f)) ? ? m' sp Kend ? st〉)
    370370    | External fn ⇒
    371         ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
     371        ! evargs ← err_to_io ??? (check_eventval_list args (sig_args (ef_sig fn)));
    372372        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    373373        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    374         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
    375     ]
    376 | Returnstate res m st ⇒
     374        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m st〉
     375    ]
     376| Returnstate result m st ⇒ err_to_io ??? (
    377377    match st with
    378378    [ Scall dst f sp en dstP fInv k Inv st' ⇒
    379         match res with
     379        match result with
    380380        [ None ⇒ match dst with
    381                  [ None ⇒ ret ? 〈E0, State f St_skip en ? ? m sp k ? st'〉
    382                  | Some _ ⇒ Wrong ??? (msg ReturnMismatch)]
    383         | Some v ⇒ match dst return λdst. match dst with [ None ⇒ ? | Some _ ⇒ ?] → ? with
    384                    [ None ⇒ λ_. Wrong ??? (msg ReturnMismatch)
    385                    | Some idty ⇒ λdstP. ret ? 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
     381                 [ None ⇒ return 〈E0, State f St_skip en ? ? m sp k ? st'〉
     382                 | Some _ ⇒ Error ? (msg ReturnMismatch)]
     383        | Some v ⇒ match dst return λdst. match dst with [ None ⇒ True | Some idty ⇒ present ?? en (\fst idty) ] → res (trace × state) with
     384                   [ None ⇒ λ_. Error ? (msg ReturnMismatch)
     385                   | Some idty ⇒ λdstP. return 〈E0, State f St_skip (update_present ?? en (\fst idty) dstP v) ? ? m sp k ? st'〉
    386386                   ] dstP
    387387        ]
    388     | _ ⇒ Wrong ??? (msg BadState)
    389     ]
     388    | _ ⇒ Error ? (msg BadState)
     389    ])
    390390].
    391391try @(π1 kInv)
     
    401401try @(π1 Inv)
    402402try @(π2 Inv)
    403 [ @stmt_inv_update @fInv
    404 | % [ @(π2 Inv) | @kInv ]
    405 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    406 | % [ @Inv | @kInv ]
     403[ @fInv
     404| @(π2 Inv')
     405| @(π1 Inv')
    407406| @(pi2 … k')
    408407| @(pi2 … k')
    409 | @(π1 Inv')
    410 | @(π2 Inv')
    411 | @fInv
    412 | @I
    413 | 11,12:
     408| % [ @Inv | @kInv ]
     409| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
     410| % [ @(π2 Inv) | @kInv ]
     411| @stmt_inv_update @fInv
     412| 10,11:
    414413  @(stmt_P_mp … (f_inv f))
    415414  #s * #V #L %
     
    422421  | 2,4: @L
    423422  ]
     423| @I
     424| @cont_inv_update @Inv
     425| @stmt_inv_update @fInv
     426| @Inv
    424427| @fInv
    425 | @Inv
    426 | @stmt_inv_update @fInv
    427 | @cont_inv_update @Inv
    428428] qed.
    429429
  • 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.