Changeset 2232 for src/Cminor
- Timestamp:
- Jul 23, 2012, 2:05:10 PM (9 years ago)
- Location:
- src/Cminor
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/initialisation.ma
r2176 r2232 68 68 | #sz #sg #e #s1 #s2 #IH1 #IH2 * * * #_ #_ #H1 #H2 whd in ⊢ (??%?); 69 69 >(IH1 H1) >(IH2 H2) @refl 70 | #s #IH * * #_ #_ #H @(IH H)71 | #s #IH * * #_ #_ #H @(IH H)72 70 | #l #s #IH * * #_ * 73 71 | #l #s #IH * * #_ #_ #H @(IH H) -
src/Cminor/semantics.ma
r2176 r2232 159 159 | Some sk ⇒ Some ? sk 160 160 ] 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 ??163 161 | St_label l' s' ⇒ λInv. 164 162 match identifier_eq ? l l' with … … 173 171 try @(π2 (π1 Inv)) 174 172 [ % [ @(π2 Inv) | @kInv ] 175 | % [ @Inv | @kInv ]176 173 | % [ @(π2 Inv) | @kInv ] 177 174 ] qed. … … 208 205 | #sk #_ #E whd in E:(??%?); destruct 209 206 ] 210 | #s1 #IH #k #f #en #Inv #kInv @IH211 | #s1 #IH #k #f #en #Inv #kInv @IH212 207 | #E whd in i:(??%?); cases (identifier_eq Label l a) in i; 213 208 whd in ⊢ (? → ??%? → ?); [ #_ #E2 destruct | *; #H cases (H (sym_eq … E)) ] … … 286 281 axiom FailedStore : String. 287 282 axiom BadFunctionValue : String. 288 axiom BadSwitchValue : String.289 axiom UnknownLabel : String.290 283 axiom ReturnMismatch : String. 291 284 … … 329 322 ! b ← eval_bool_of_val v; 330 323 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 with339 [ 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 ]345 324 | St_return eo ⇒ 346 325 match eo return λeo. stmt_inv f en (St_return eo) → ? with … … 411 390 | @(π2 Inv') 412 391 | @(π1 Inv') 413 | @(pi2 … k')414 | @(pi2 … k')415 | % [ @Inv | @kInv ]416 392 | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ] 417 393 | % [ @(π2 Inv) | @kInv ] 418 394 | @stmt_inv_update @fInv 419 | 10,11:395 | 7,8: 420 396 @(stmt_P_mp … (f_inv f)) 421 397 #s * #V #L % -
src/Cminor/syntax.ma
r2176 r2232 46 46 | St_seq : stmt → stmt → stmt 47 47 | St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt 48 | St_loop : stmt → stmt49 | St_block : stmt → stmt50 | St_exit : nat → stmt51 (* 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 → stmt53 48 | St_return : option (𝚺t. expr t) → stmt 54 49 | St_label : identifier Label → stmt → stmt … … 60 55 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 61 56 | 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'64 57 | St_label _ s' ⇒ P s ∧ stmt_P P s' 65 58 | St_cost _ s' ⇒ P s ∧ stmt_P P s' … … 71 64 [ #s1 #s2 * * /2/ 72 65 | #sz #sg #e #s1 #s2 * * /2/ 73 | 3,4: #s * /2/ 74 | 5,6: #i #s normalize * /2/ 66 | *: #i #s normalize * /2/ 75 67 ] qed. 76 68 … … 86 78 *) 87 79 | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P 88 | St_switch _ _ e _ _ ⇒ expr_vars ? e P89 80 | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ] 90 81 | _ ⇒ True … … 103 94 [ #s1 #s2 #H1 #H2 normalize * * /4/ 104 95 | #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 105 | #s #H * /5/106 | #s #H * /5/107 96 | #l #s #H * /5/ 108 97 | #l #s #H * /5/ … … 120 109 | #s1 #s2 #H1 #H2 * /3/ 121 110 | #sz #sg #e #s1 #s2 #H1 #H2 /5/ 122 | 7,8: #s #H1 #H2 /2/123 | //124 | /5/125 111 | * normalize [ // | *; normalize /3/ ] 126 112 | /2/ … … 137 123 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 138 124 | St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 139 | St_loop s ⇒ labels_of s140 | St_block s ⇒ labels_of s141 125 | St_label l s ⇒ l::(labels_of s) 142 126 | St_cost _ s ⇒ labels_of s -
src/Cminor/toRTLabs.ma
r2178 r2232 610 610 alias id "R_return" = "cic:/matita/cerco/RTLabs/syntax/statement.con(0,12,0)". 611 611 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 = ? → ?) → ? with615 [ None ⇒ λ_. Error ? m616 | Some a ⇒ λH'. OK ? «a, ?»617 ] (All_nth A P n l (pi2 … l)).618 @H' @refl qed.619 620 612 lemma lookup_label_rev : ∀lenv,l,l',p. 621 613 lookup_label lenv l p = l' → lookup ?? lenv l = Some ? l'. … … 677 669 qed. 678 670 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') ≝671 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) on s : res (Σf':partial_fn label_env env. add_stmt_inv label_env env s f f') ≝ 680 672 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env env. add_stmt_inv … s f f') with 681 673 [ St_skip ⇒ λ_. OK ? «f, ?» … … 719 711 *) 720 712 | 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; 723 715 OK ? «pi1 … f1, ?» 724 716 | St_ifthenelse _ _ e s1 s2 ⇒ λEnv. 725 717 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; 727 719 let l2 ≝ pf_entry … f2 in 728 720 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; 730 722 let ❬f,r❭ ≝ choose_reg … e f1 (π1 (π1 (π1 Env))) in 731 723 let f ≝ add_fresh_to_graph … (λl1. St_cond r l1 l2) f ?? in 732 724 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 in736 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 ? in746 do l_default ← nth_sig ?? (msg BadCminorProgram) exits n;747 let f ≝ add_fresh_to_graph … (λ_. R_skip l_default) f ?? in748 do f ← foldr ? (res (Σf':partial_fn ??. ?)) (λcs,f.749 do f ← f;750 let 〈i,n〉 ≝ cs in751 let ❬f,cr❭ ≝ fresh_reg … f (ASTint sz sg) in752 let ❬f,br❭ ≝ fresh_reg … f (ASTint I8 Unsigned) in753 do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;754 let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in755 let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in756 let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in757 OK ? «pi1 … f, ?») (OK ? f) tab;758 OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»759 725 | St_return opt_e ⇒ let f0 ≝ f in 760 726 let f ≝ add_fresh_to_graph … (λ_. R_return) f ?? in … … 776 742 ] 777 743 | 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; 779 745 let l' ≝ lookup_label label_env l ? in 780 746 OK ? «pi1 … (add_to_graph … l' (R_skip (pf_entry … f)) f ??), ?» … … 783 749 OK ? «pi1 … (add_fresh_to_graph' … (λ_.R_skip l') f ??), ?» 784 750 | 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; 786 752 OK ? «pi1 … (add_fresh_to_graph … (St_cost l) f ??), ?» 787 753 ] Env. … … 799 765 | @(fn_con_env … (pi2 ?? val_reg)) repeat @fn_contains_step @I 800 766 | @(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 @I802 | (*5,9:*)@sym_eq @(All2_length … (pi2 ?? args_regs))803 | (*6,10:*)@(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I767 | @(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 804 770 | @(π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 @I806 771 | #l #H cases (Exists_append … H) 807 772 [ #H1 @(stmt_labels_added ????? (pi2 ?? f1) ? H1) … … 815 780 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I 816 781 | #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 @I823 | @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I824 | #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 @I826 | #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I827 782 | #_ (* see above *) <E @(pi2 ?? r) 828 783 | @(pi2 … (pf_entry …)) … … 867 822 l 868 823 l in 869 do f ← add_stmt env label_env (f_body f) ? emptyfn [ ];824 do f ← add_stmt env label_env (f_body f) ? emptyfn; 870 825 OK ? (mk_internal_function 871 826 (pf_labgen … f) … … 881 836 (pf_exit … f) 882 837 ). 883 [ @I 884 | -emptyfn @(stmt_P_mp … (f_inv f)) 838 [ -emptyfn @(stmt_P_mp … (f_inv f)) 885 839 #s * #V #L % 886 840 [ @(stmt_vars_mp … V) … … 925 879 | whd in ⊢ (??%? → ?); #E' destruct (E') 926 880 ] 927 | 7,8: whd >lookup_add_hit % #E destruct881 | 6,7: whd >lookup_add_hit % #E destruct 928 882 | % @refl 929 883 ]
Note: See TracChangeset
for help on using the changeset viewer.