Changeset 1680


Ignore:
Timestamp:
Feb 9, 2012, 1:22:28 PM (6 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.)

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1655 r1680  
    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 ?;
    321321        return 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
     322(*
    322323    | St_tailcall ef args ⇒ λInv.
    323324        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
     
    325326        ! 〈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 ?;
    326327        return 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327        
     328*)       
    328329    | St_seq s1 s2 ⇒ λInv. return 〈E0, State f s1 en fInv ? m sp (Kseq s2 k) ? st〉
    329330    | St_ifthenelse _ _ e strue sfalse ⇒ λInv.
  • src/Cminor/syntax.ma

    r1631 r1680  
    4343(* ident for returned value, expression to identify fn, args. *)
    4444| St_call : option (ident × typ) → expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     45(* We don't use these at the moment, and they're getting in the way.
    4546| St_tailcall : expr (ASTptr Code) → list (𝚺t. expr t) → stmt
     47*)
    4648| St_seq : stmt → stmt → stmt
    4749| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
     
    8284| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    8385| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     86(*
    8487| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     88*)
    8589| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    8690| St_switch _ _ e _ _ ⇒ expr_vars ? e P
     
    113117| #t #r #q #e1 #e2 * /4/
    114118| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
     119(*
    115120| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
     121*)
    116122| #s1 #s2 #H1 #H2 * /3/
    117123| #sz #sg #e #s1 #s2 #H1 #H2 /5/
    118 | 8,9: #s #H1 #H2 /2/
     124| 7,8: #s #H1 #H2 /2/
    119125| //
    120126| /5/
  • 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)
  • src/RTLabs/semantics.ma

    r1655 r1680  
    130130      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
    131131      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     132(*
    132133  | St_tailcall_id id args ⇒ λH.
    133134      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    140141      ! vs ← m_mmap … (reg_retrieve (locals f)) args;
    141142      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    142 
     143*)
    143144  | St_cond src ltrue lfalse ⇒ λH.
    144145      ! v ← reg_retrieve (locals f) src;
     
    294295  | #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 ]
    295296  | #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 ]
     297(*
    296298  | #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 ]
    297299  | #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 ]
     300*)
    298301  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    299302  | #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 ]
  • src/RTLabs/syntax.ma

    r1675 r1680  
    1919| St_call_id : ident → list register → option register → label → statement
    2020| St_call_ptr : register → list register → option register → label → statement
     21(* We're not using these just now, and they'd make the Traces.ma proofs more difficult.
    2122| St_tailcall_id : ident → list register → statement
    2223| St_tailcall_ptr : register → list register → statement
     24*)
    2325| St_cond : register → label → label → statement
    2426| St_jumptable : register → list label → statement
     
    4648| St_call_id _ _ _ l ⇒ P l
    4749| St_call_ptr _ _ _ l ⇒ P l
     50(*
    4851| St_tailcall_id _ _ ⇒ True
    4952| St_tailcall_ptr _ _ ⇒ True
     53*)
    5054| St_cond _ l1 l2 ⇒ P l1 ∧ P l2
    5155| St_jumptable _ ls ⇒ All ? P ls
     
    105109| St_call_id _ _ _ l ⇒ [l]
    106110| St_call_ptr _ _ _ l ⇒ [l]
     111(*
    107112| St_tailcall_id _ _ ⇒ [ ]
    108113| St_tailcall_ptr _ _ ⇒ [ ]
     114*)
    109115| St_cond _ l1 l2 ⇒ [l1; l2]
    110116| St_jumptable _ ls ⇒ ls
Note: See TracChangeset for help on using the changeset viewer.