Changeset 2232 for src/Cminor


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

Remove unused block structure in Cminor.

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r2176 r2232  
    6868| #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?);
    6969  >(IH1 H1) >(IH2 H2) @refl
    70 | #s #IH * * #_ #_ #H @(IH H)
    71 | #s #IH * * #_ #_ #H @(IH H)
    7270| #l #s #IH * * #_ *
    7371| #l #s #IH * * #_ #_ #H @(IH H)
  • src/Cminor/semantics.ma

    r2176 r2232  
    159159    | Some sk ⇒ Some ? sk
    160160    ]
    161 | St_loop s' ⇒ λInv. find_label l s' (Kseq (St_loop s') k) f en ??
    162 | St_block s' ⇒ λInv. find_label l s' (Kblock k) f en ??
    163161| St_label l' s' ⇒ λInv.
    164162    match identifier_eq ? l l' with
     
    173171try @(π2 (π1 Inv))
    174172[ % [ @(π2 Inv) | @kInv ]
    175 | % [ @Inv | @kInv ]
    176173| % [ @(π2 Inv) | @kInv ]
    177174] qed.
     
    208205  | #sk #_ #E whd in E:(??%?); destruct
    209206  ]
    210 | #s1 #IH #k #f #en #Inv #kInv @IH
    211 | #s1 #IH #k #f #en #Inv #kInv @IH
    212207| #E whd in i:(??%?); cases (identifier_eq Label l a) in i;
    213208  whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ]
     
    286281axiom FailedStore : String.
    287282axiom BadFunctionValue : String.
    288 axiom BadSwitchValue : String.
    289 axiom UnknownLabel : String.
    290283axiom ReturnMismatch : String.
    291284
     
    329322        ! b ← eval_bool_of_val v;
    330323        return 〈tr, State f (if b then strue else sfalse) en fInv ? m sp k ? st〉
    331     | St_loop s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kseq (St_loop s) k) ? st〉
    332     | St_block s ⇒ λInv. return 〈E0, State f s en fInv ? m sp (Kblock k) ? st〉
    333     | St_exit n ⇒ λInv.
    334         ! k' ← k_exit n k ?? kInv;
    335         return 〈E0, State f St_skip en fInv ? m sp k' ? st〉
    336     | St_switch sz _ e cs default ⇒ λInv.
    337         ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    338         match v with
    339         [ Vint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.
    340             ! k' ← k_exit (find_case ?? i cs default) k ?? kInv;
    341             return 〈tr, State f St_skip en fInv ? m sp k' ? st〉)
    342             (Error ? (msg BadSwitchValue))
    343         | _ ⇒ Error ? (msg BadSwitchValue)
    344         ]
    345324    | St_return eo ⇒
    346325        match eo return λeo. stmt_inv f en (St_return eo) → ? with
     
    411390| @(π2 Inv')
    412391| @(π1 Inv')
    413 | @(pi2 … k')
    414 | @(pi2 … k')
    415 | % [ @Inv | @kInv ]
    416392| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    417393| % [ @(π2 Inv) | @kInv ]
    418394| @stmt_inv_update @fInv
    419 | 10,11:
     395| 7,8:
    420396  @(stmt_P_mp … (f_inv f))
    421397  #s * #V #L %
  • src/Cminor/syntax.ma

    r2176 r2232  
    4646| St_seq : stmt → stmt → stmt
    4747| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
    48 | St_loop : stmt → stmt
    49 | St_block : stmt → stmt
    50 | St_exit : nat → stmt
    51 (* expr to switch on, table of 〈switch value, #blocks to exit〉, default *)
    52 | St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt
    5348| St_return : option (𝚺t. expr t) → stmt
    5449| St_label : identifier Label → stmt → stmt
     
    6055[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    6156| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    62 | St_loop s' ⇒ P s ∧ stmt_P P s'
    63 | St_block s' ⇒ P s ∧ stmt_P P s'
    6457| St_label _ s' ⇒ P s ∧ stmt_P P s'
    6558| St_cost _ s' ⇒ P s ∧ stmt_P P s'
     
    7164[ #s1 #s2 * * /2/
    7265| #sz #sg #e #s1 #s2 * * /2/
    73 | 3,4: #s * /2/
    74 | 5,6: #i #s normalize * /2/
     66| *: #i #s normalize * /2/
    7567] qed.
    7668
     
    8678*)
    8779| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    88 | St_switch _ _ e _ _ ⇒ expr_vars ? e P
    8980| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
    9081| _ ⇒ True
     
    10394[ #s1 #s2 #H1 #H2 normalize * * /4/
    10495| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
    105 | #s #H * /5/
    106 | #s #H * /5/
    10796| #l #s #H * /5/
    10897| #l #s #H * /5/
     
    120109| #s1 #s2 #H1 #H2 * /3/
    121110| #sz #sg #e #s1 #s2 #H1 #H2 /5/
    122 | 7,8: #s #H1 #H2 /2/
    123 | //
    124 | /5/
    125111| * normalize [ // | *; normalize /3/ ]
    126112| /2/
     
    137123[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    138124| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
    139 | St_loop s ⇒ labels_of s
    140 | St_block s ⇒ labels_of s
    141125| St_label l s ⇒ l::(labels_of s)
    142126| St_cost _ s ⇒ labels_of s
  • 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.