Ignore:
Timestamp:
Jul 23, 2012, 2:05:10 PM (7 years ago)
Author:
campbell
Message:

Remove unused block structure in Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2178 r2232  
    610610alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)".
    611611
    612 definition nth_sig : ∀A. ∀P:A → Prop. errmsg → (Σl:list A. All A P l) → nat → res (Σa:A. P a) ≝
    613 λA,P,m,l,n.
    614   match nth_opt A n l return λx.(∀_.x = ? → ?) → ? with
    615   [ None ⇒ λ_. Error ? m
    616   | Some a ⇒ λH'. OK ? «a, ?»
    617   ] (All_nth A P n l (pi2 … l)).
    618 @H' @refl qed.
    619 
    620612lemma lookup_label_rev : ∀lenv,l,l',p.
    621613  lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'.
     
    677669qed.
    678670
    679 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) (exits:Σls:list label. All ? (present ?? (pf_graph … f)) ls) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
     671let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env env) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝
    680672match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with
    681673[ St_skip ⇒ λ_. OK ? «f, ?»
     
    719711*)
    720712| St_seq s1 s2 ⇒ λEnv.
    721     do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
    722     do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
     713    do f2 ← add_stmt env label_env s2 ? f;
     714    do f1 ← add_stmt env label_env s1 ? f2;
    723715      OK ? «pi1 … f1, ?»
    724716| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    725717    let l_next ≝ pf_entry … f in
    726     do f2 ← add_stmt env label_env s2 (π2 Env) f «exits, ?»;
     718    do f2 ← add_stmt env label_env s2 (π2 Env) f;
    727719    let l2 ≝ pf_entry … f2 in
    728720    let f ≝ add_fresh_to_graph … (λ_. R_skip l_next) f2 ?? in
    729     do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f «exits, ?»;
     721    do f1 ← add_stmt env label_env s1 (π2 (π1 Env)) f;
    730722    let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in
    731723    let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in
    732724    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) f «r, ?»), ?»
    733 | St_loop s ⇒ λEnv.
    734     let f ≝ add_fresh_to_graph … R_skip f ?? in (* dummy statement, fill in afterwards *)
    735     let l_loop ≝ pf_entry … f in
    736     do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
    737     OK ? «pi1 … (fill_in_statement … l_loop (R_skip (pf_entry … f)) f ??), ?»
    738 | St_block s ⇒ λEnv.
    739     do f ← add_stmt env label_env s (π2 Env) f («pf_entry … f::exits, ?»);
    740     OK ? «pi1 … f, ?»
    741 | St_exit n ⇒ λEnv.
    742     do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    743     OK ? «pi1 … (add_fresh_to_graph … (λ_. R_skip l) f ??), ?»
    744 | St_switch sz sg e tab n ⇒ λEnv.
    745     let ❬f,r❭ ≝ choose_reg … e f ? in
    746     do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;
    747     let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in
    748     do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.
    749       do f ← f;
    750       let 〈i,n〉 ≝ cs in
    751       let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in
    752       let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in
    753       do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    754       let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    755       let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
    756       let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
    757         OK ? «pi1 … f, ?») (OK ? f) tab;
    758     OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
    759725| St_return opt_e ⇒ let f0 ≝ f in
    760726    let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in
     
    776742    ]
    777743| St_label l s' ⇒ λEnv.
    778     do f ← add_stmt env label_env s' (π2 Env) f exits;
     744    do f ← add_stmt env label_env s' (π2 Env) f;
    779745    let l' ≝ lookup_label label_env l ? in
    780746    OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?»
     
    783749    OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?»
    784750| St_cost l s' ⇒ λEnv.
    785     do f ← add_stmt env label_env s' (π2 Env) f exits;
     751    do f ← add_stmt env label_env s' (π2 Env) f;
    786752    OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?»
    787753] Env.
     
    799765| @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I
    800766| @(fn_con_env … (pi2 ?? addr_reg)) repeat @fn_contains_step @I
    801 | (*4,8:*) @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
    802 | (*5,9:*) @sym_eq @(All2_length … (pi2 ?? args_regs))
    803 | (*6,10:*) @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
     767| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
     768| @sym_eq @(All2_length … (pi2 ?? args_regs))
     769| @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
    804770| @(π1 (π1 (π1 Env)))
    805 | 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
    806771| #l #H cases (Exists_append … H)
    807772  [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1)
     
    815780| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    816781| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
    817 | @(pi2 … (pf_entry …))
    818 | @Cminor_labels_sig @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
    819 | % [ @pi2 | @(pi2 ?? exits) ]
    820 | @(equal_Cminor_labels_added ??? s) [ @refl | @(stmt_labels_added ????? (pi2 ?? f)) ]
    821 | #l' #H @(pi2 … l)
    822 | #l #H @(fn_con_graph … (pi2 ?? l_default)) repeat @fn_contains_step @I
    823 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    824 | #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
    825 | #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
    826 | #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
    827782| #_ (* see above *) <E @(pi2 ?? r)
    828783| @(pi2 … (pf_entry …))
     
    867822    l
    868823    l in
    869 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];
     824do f ← add_stmt env label_env (f_body f) ? emptyfn;
    870825OK ? (mk_internal_function
    871826    (pf_labgen … f)
     
    881836    (pf_exit … f)
    882837  ).
    883 [ @I
    884 | -emptyfn @(stmt_P_mp … (f_inv f))
     838[ -emptyfn @(stmt_P_mp … (f_inv f))
    885839  #s * #V #L %
    886840  [ @(stmt_vars_mp … V)
     
    925879  | whd in ⊢ (??%? → ?); #E' destruct (E')
    926880  ]
    927 | 7,8: whd >lookup_add_hit % #E destruct
     881| 6,7: whd >lookup_add_hit % #E destruct
    928882| % @refl
    929883]
Note: See TracChangeset for help on using the changeset viewer.