Ignore:
Timestamp:
Mar 26, 2013, 3:34:30 PM (7 years ago)
Author:
campbell
Message:

Fix silly label handling bug I realised was there during my talk...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2877 r2953  
    15221522
    15231523(* params and statement aren't real parameters, they're just there for giving the invariant. *)
    1524 definition alloc_params :
     1524definition alloc_params_main :
    15251525 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
    15261526   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝   
     
    15441544@(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl
    15451545qed.
     1546
     1547(* For a soundly-labelled program there will be a cost label at the start of the
     1548   function.  We should keep it there to keep it soundly-labelled. *)
     1549
     1550definition alloc_params :
     1551 ∀vars:var_types.∀lbls,statement,uv,flag,rettyp. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag rettyp su)
     1552   → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝
     1553λvars,lbls,statement,uv,ul,rettyp,params,su.
     1554  match su return λsu. trans_inv vars lbls statement uv ul rettyp su → ? with
     1555  [ mk_Prod tl s0 ⇒
     1556    match s0 return λs. trans_inv vars lbls statement uv ul rettyp 〈tl, s〉 → ? with
     1557    [ St_cost cl s' ⇒ λinv.
     1558      ! tls ← alloc_params_main vars lbls statement uv ul rettyp params «〈tl,s'〉,?»;
     1559      return «〈\fst tls,St_cost cl (\snd tls)〉, ?»
     1560    | _ ⇒ λ_. alloc_params_main vars lbls statement uv ul rettyp params su
     1561    ]
     1562  ] (pi2 ?? su).
     1563[ cases tl in inv ⊢ %;
     1564  #tg #lg * * * * * #SV #SP #LT #TP * #_ #RO * #_ #LW whd
     1565  % [ % [ % [ % [ @SP | @LT ]| @TP ]| @RO ]| @LW ]
     1566| cases tls * * #tg #lb #s * * * * #SI #LT #TP #RO #LW whd
     1567  % [ % [ % [ % [ % [ // | @SI ] | @LT ]| @TP ]| % // ]| % // ]
     1568] qed.
     1569
    15461570
    15471571definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
Note: See TracChangeset for help on using the changeset viewer.