Ignore:
Timestamp:
Feb 9, 2012, 1:22:28 PM (9 years ago)
Author:
campbell
Message:

Comment out unused tailcalls in Cminor and RTLabs.
(They would be a little tricky to deal with in RTLabs/Traces.ma, and we
don't currently generate them.)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1631 r1680  
    606606(* XXX Work around odd disambiguation errors. *)
    607607alias id "R_skip" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,1,0)".
    608 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,14,0)".
     608(* If reenabling tailcalls, change 12 to 14. *)
     609alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
    609610
    610611definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
     
    703704      ] in
    704705    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
     706(*
    705707| St_tailcall e args ⇒ λEnv.
    706708    let ❬f, args_regs❭ ≝ choose_regs ? env args f (π2 (π1 Env)) in
     
    714716      ] in
    715717    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f ?), ?»
     718*)
    716719| St_seq s1 s2 ⇒ λEnv.
    717720    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
     
    795798| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
    796799| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
    797 | 4,8: @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
    798 | 5,9: @sym_eq @(All2_length … (pi2 ?? args_regs))
    799 | 6,10: @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
     800| (*4,8:*) @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
     801| (*5,9:*) @sym_eq @(All2_length … (pi2 ?? args_regs))
     802| (*6,10:*) @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
    800803| @(π1 (π1 (π1 Env)))
    801 | 11,13,14,19,20: (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
     804| 8,10,11,16,17: (*11,13,14,19,20:*) (@(All_mp … (pi2 ?? exits))) #i #H @(fn_con_graph … H) repeat @fn_contains_step @I
    802805| #l #H cases (Exists_append … H)
    803806  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
Note: See TracChangeset for help on using the changeset viewer.