Ignore:
Timestamp:
Dec 13, 2011, 5:37:40 PM (8 years ago)
Author:
sacerdot
Message:

More proofs ported to new lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1516 r1603  
    235235
    236236(* TODO: perhaps should do a little type checking? *)
    237 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
     237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Sig ? (λen:env. All ? (λit. present ?? en (\fst it)) ids)) ≝
    238238match vs with
    239239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     
    249249[ @I
    250250| % [ whd >lookup_add_hit % #E destruct
    251     | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H
     251    | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H
    252252    ]
    253253] qed.
     
    318318        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    319319        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    320         ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     320        ! 〈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 ?;
    321321        ret ? 〈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);
    325         ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     325        ! 〈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 ?;
    326326        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327327       
     
    349349        [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
    350350        | Some e ⇒
    351             match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv.
     351            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;
    353353              ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉
     
    356356    | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
    357357    | St_goto l ⇒ λInv.
    358         match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒
     358        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
    359359          ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
    360360        ]
     
    405405| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    406406| % [ @Inv | @kInv ]
    407 | @(use_sig … k')
    408 | @(use_sig … k')
     407| @(pi2 … k')
     408| @(pi2 … k')
    409409| @(π1 Inv')
    410410| @(π2 Inv')
     
    415415  #s * #V #L %
    416416  [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
    417     [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en))
     417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
    418418      * #id' #ty * #E1 #H <E1 @H
    419419    | *: #H cases (Exists_All … H (init_locals_env … en …))
Note: See TracChangeset for help on using the changeset viewer.