Changeset 2661


Ignore:
Timestamp:
Feb 12, 2013, 3:26:37 AM (6 years ago)
Author:
sacerdot
Message:

stacksize "repaired" by "considering" tailcalls
Some daemons added here and there since many are already in place.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/BACKEND_BROKEN_FILES

    r2660 r2661  
    44  joint/lineariseProof.ma
    55  LTL/LTLToLIN.ma
    6 joint/stacksize.ma:               mancano tailcall
    76
    87LIN/joint_LTL_LIN_semantics.ma:   parametri
  • src/joint/stacksize.ma

    r2601 r2661  
    5151    extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
    5252      (up ?? (lg (as_call_ident ? «s1p,cl»))::res)
     53  | tal_base_tailcall s1p s1s s2 ex cl tlr ⇒
     54     extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr
     55      (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res)
    5356  | tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒
    5457    let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr
     
    8891  | tal_base_return st1 st1' ex cl ⇒ ?
    8992  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
     93  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    9094  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    9195  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
     
    112116      normalize #abs destruct (abs)
    113117    ]
     118  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid *
     119    #taa * #H * #G * #K inversion taa in ⊢ ?;
     120    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     121    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     122      normalize #abs destruct (abs)
     123    ]
    114124  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize *
    115125    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
     
    130140  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    131141  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
     142  | #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs)
    132143  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    133144    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
     
    170181      destruct normalize * #abs destruct (abs)
    171182    ]
     183  | (* tail call case *) cases daemon
    172184  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize
    173185    * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *]
     
    192204      >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *)
    193205    ]
    194   ]
     206  ]
     207| (* tail call case *) cases daemon
    195208| cases t2
    196209  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa *
     
    218231      | #ss #sf #ex'' #cl'' normalize #abs cases abs
    219232      | #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs
     233      | #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs
    220234      | #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1'
    221235        normalize #abs cases abs
     
    226240      destruct normalize * * #abs destruct (abs)
    227241    ]
     242  | (* tail call case *) cases daemon
    228243  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    229244    normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * *
     
    249264  | #ss #fs #ex' #cl'
    250265  | #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co'
     266  | #st2p #st2s #st2' #ex' #cl' #tlr2
    251267  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2
    252268  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co'
     
    254270  normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    255271]
     272(* Another tailcall case escaped *) cases daemon
    256273qed.
    257274
     
    285302  | tal_base_return st1 st1' ex cl ⇒ ?
    286303  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
     304  | tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ?
    287305  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    288306  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
     
    292310|*: #Hsim >(tal_rel_extract_equal … Hsim []) %
    293311]
    294 qed.
    295      
    296      
    297      
    298            
     312qed.
Note: See TracChangeset for help on using the changeset viewer.