Changeset 1096 for Deliverables/D3.3
 Timestamp:
 Aug 3, 2011, 1:04:48 PM (9 years ago)
 Location:
 Deliverables/D3.3/idlookupbranch
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Clight/toCminor.ma
r1087 r1096 741 741 ]. 742 742 *) 743 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 743 744 definition lenv ≝ identifier_map SymbolTag (identifier Label). 745 746 definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l. 747 748 definition stmt_inv ≝ 749 λvars. λlbls:lenv. 750 stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s). 751 752 definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝ 744 753 λvars,e1,e2. 745 754 do e2' ← translate_expr vars e2; … … 749 758  MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» 750 759 ]. 751 whd 760 #ls whd % 752 761 [ % // @sig_ok 762  @I 753 763  % @sig_ok 764  @I 754 765 ] qed. 755 766 … … 783 794 ] qed. 784 795 785 let rec translate_statement (vars:var_types) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_vars s (local_id vars)) ≝ 796 axiom MissingLabel : String. 797 798 definition lookup_label ≝ 799 λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). 800 801 lemma lookup_label_hit : ∀lbls,l,l'. 802 lookup_label lbls l = OK ? l' → 803 lpresent lbls l'. 804 #lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ % 805 normalize #x try #y destruct /2/ 806 qed. 807 808 let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs:stmt.stmt_inv vars lbls s) ≝ 786 809 match s with 787 810 [ Sskip ⇒ OK ? «St_skip, ?» 788  Sassign e1 e2 ⇒ translate_assign vars e1 e2 811  Sassign e1 e2 ⇒ 812 do s' ← translate_assign vars e1 e2; 813 OK ? «eject ?? s', ?» 789 814  Scall ret ef args ⇒ 790 815 do ef' ← translate_expr vars ef; … … 803 828 ] 804 829  Ssequence s1 s2 ⇒ 805 do s1' ← translate_statement vars tmp tmpp s1;806 do s2' ← translate_statement vars tmp tmpp s2;830 do s1' ← translate_statement vars lbls tmp tmpp s1; 831 do s2' ← translate_statement vars lbls tmp tmpp s2; 807 832 OK ? «St_seq s1' s2', ?» 808 833  Sifthenelse e1 s1 s2 ⇒ … … 810 835 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 811 836 [ ASTint _ _ ⇒ λe1'. 812 do s1' ← translate_statement vars tmp tmpp s1;813 do s2' ← translate_statement vars tmp tmpp s2;837 do s1' ← translate_statement vars lbls tmp tmpp s1; 838 do s2' ← translate_statement vars lbls tmp tmpp s2; 814 839 OK ? «St_ifthenelse ?? e1' s1' s2', ?» 815 840  _ ⇒ λ_.Error ? (msg TypeMismatch) … … 819 844 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 820 845 [ ASTint _ _ ⇒ λe1'. 821 do s1' ← translate_statement vars tmp tmpp s1;846 do s1' ← translate_statement vars lbls tmp tmpp s1; 822 847 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 823 848 OK ? «St_block … … 830 855 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 831 856 [ ASTint _ _ ⇒ λe1'. 832 do s1' ← translate_statement vars tmp tmpp s1;857 do s1' ← translate_statement vars lbls tmp tmpp s1; 833 858 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 834 859 OK ? «St_block … … 841 866 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 842 867 [ ASTint _ _ ⇒ λe1'. 843 do s1' ← translate_statement vars tmp tmpp s1;844 do s2' ← translate_statement vars tmp tmpp s2;845 do s3' ← translate_statement vars tmp tmpp s3;868 do s1' ← translate_statement vars lbls tmp tmpp s1; 869 do s2' ← translate_statement vars lbls tmp tmpp s2; 870 do s3' ← translate_statement vars lbls tmp tmpp s3; 846 871 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 847 872 OK ? «St_seq s1' … … 862 887  Sswitch e1 ls ⇒ Error ? (msg FIXME) 863 888  Slabel l s1 ⇒ 864 do s1' ← translate_statement vars tmp tmpp s1; 865 OK ? «St_label l s1', ?» 866  Sgoto l ⇒ OK ? «St_goto l, ?» 889 do l' as E ← lookup_label lbls l; 890 do s1' ← translate_statement vars lbls tmp tmpp s1; 891 OK ? «St_label l' s1', ?» 892  Sgoto l ⇒ 893 do l' as E ← lookup_label lbls l; 894 OK ? «St_goto l', ?» 867 895  Scost l s1 ⇒ 868 do s1' ← translate_statement vars tmp tmpp s1;896 do s1' ← translate_statement vars lbls tmp tmpp s1; 869 897 OK ? «St_cost l s1', ?» 870 898 ]. 871 whd try @I 872 [ % [ % [ @p  @sig_ok ]  @(sig_ok ? (All ??)) ] 873  % [ whd % [ % [ @sig_ok  @sig_ok ]  @(sig_ok ? (All ??)) ]  whd % @sig_ok ] 874  % [ % [ @I  @sig_ok ]  @(sig_ok ? (All ??)) ] 875  % @sig_ok 876  % [ % @sig_ok  @sig_ok ] 877  % [ % @sig_ok  whd @I ] 878  % [ @sig_ok  whd % [ % [ @sig_ok  @I ]  @I ] ] 879  % [ @sig_ok  whd % [ % [ @sig_ok  whd % @sig_ok ]  @I ] ] 880  @sig_ok 881  @sig_ok 882  @sig_ok 899 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 900 try @I 901 try @(sig_ok ? (λs.stmt_inv ?? s)) 902 try @(sig_ok ? (λe.expr_vars ? e ?)) 903 try @(sig_ok ? (λs.stmt_vars ?? s)) 904 try @(sig_ok ? (λs.stmt_labels ?? s)) 905 try @(sig_ok ? (All ??)) 906 try @(sig_ok ? (local_id vars)) 907 try @(lookup_label_hit … E) 908 [ @(sig_ok ?? s') 909  @p 910 ] qed. 911 912 let rec labels_defined (s:statement) : list ident ≝ 913 match s with 914 [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 915  Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 916  Swhile _ s ⇒ labels_defined s 917  Sdowhile _ s ⇒ labels_defined s 918  Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 919  Sswitch _ ls ⇒ labels_defined_switch ls 920  Slabel l s ⇒ l::(labels_defined s) 921  Scost _ s ⇒ labels_defined s 922  _ ⇒ [ ] 923 ] 924 and labels_defined_switch (ls:labeled_statements) : list ident ≝ 925 match ls with 926 [ LSdefault s ⇒ labels_defined s 927  LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls 928 ]. 929 930 lemma OK_sig_eq : ∀A,P,x,xp,y,yp. OK (Σx:A.P x) «x,xp» = OK (Σx:A.P x) «y,yp» → x = y. 931 #A #P #x #xp #y #yp #E destruct @refl 932 qed. 933 934 definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). 935 936 lemma Exists_append : ∀A,P,l1,l2. 937 Exists A P (l1@l2) → 938 Exists A P l1 ∨ Exists A P l2. 939 #A #P #l1 elim l1 940 [ #l2 #H %2 @H 941  #h #t #IH #l2 whd in ⊢ (% → ?) * 942 [ #H %1 %1 @H 943  #H cases (IH l2 H) /4/ 944 ] 945 ] qed. 946 947 lemma Exists_append_l : ∀A,P,l1,l2. 948 Exists A P l1 → Exists A P (l1@l2). 949 #A #P #l1 #l2 elim l1 950 [ * 951  #h #t #IH * 952 [ #H %1 @H 953  #H %2 @IH @H 954 ] 955 ] qed. 956 957 lemma Exists_append_r : ∀A,P,l1,l2. 958 Exists A P l2 → Exists A P (l1@l2). 959 #A #P #l1 #l2 elim l1 960 [ #H @H 961  #h #t #IH #H %2 @IH @H 962 ] qed. 963 964 lemma reflmatch : ∀A,B,e.∀P:∀v:A. e = OK ? v → res B.∀x. 965 match e return λx.e = x → ? with [ OK v ⇒ P v  Error m ⇒ λ_.Error ? m ] (refl ? e) = OK ? x → 966 ∃v,p. P v p = OK ? x. 967 #A #B * 968 [ #v #P #x normalize #H %{v} % [ @refl  @H ] 969  #m #P #x normalize #H destruct 970 ] qed. 971 972 lemma labels_translated : ∀vars,lbls,tmp,tmpp,s,l,s',p. 973 (Exists ? (λl'.l' = l) (labels_defined s)) → 974 translate_statement vars lbls tmp tmpp s = OK ? «s', p» → 975 ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'. 976 #vars #lbls #tmp #tmpp #s #l @(statement_ind … s) (* FIXME: once switch is done we'll need something else here *) 977 [ #s' #p * 978  #e1 #e2 #s' #p * 979  #eo #e #args #s' #p * 980  #s1 #s2 #IH1 #IH2 #s' #p #H #E 981 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 982 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 983 <(OK_sig_eq ?????? E) E; 984 cases (Exists_append ???? H) 985 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 986  #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @L2 ] 987 ] 988  #e #s1 #s2 #IH1 #IH2 #s' #p #H #E 989 (* Carefully get rid of the equality that will screw up the case analysis *) 990 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 991 [ #sz #sg #e' #E 992 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 993 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 994 <(OK_sig_eq ?????? E) E; 995 cases (Exists_append ???? H) 996 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 997  #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @L2 ] 998 ] 999  *: #x #e' normalize #E destruct 1000 ] 1001  #e #s #IH #s' #p #H #E 1002 (* Carefully get rid of the equality that will screw up the case analysis *) 1003 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1004 [ #sz #sg #e' #E 1005 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1006 <(OK_sig_eq ?????? E) E; 1007 cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La  whd; normalize in ⊢ (???%) >append_nil @Lb ] 1008  *: #x #e' normalize #E destruct 1009 ] 1010  #e #s #IH #s' #p #H #E 1011 (* Carefully get rid of the equality that will screw up the case analysis *) 1012 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1013 [ #sz #sg #e' #E 1014 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1015 <(OK_sig_eq ?????? E) E; 1016 cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La  whd; normalize in ⊢ (???%) >append_nil @Lb ] 1017  *: #x #e' normalize #E destruct 1018 ] 1019  #s1 #e #s1 #s2 #IH1 #IH2 #IH3 #s' #p #H #E 1020 (* Carefully get rid of the equality that will screw up the case analysis *) 1021 cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ % 1022 [ #sz #sg #e' #E 1023 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1024 cases (bind_inversion ????? E) * #s2' #I2 * #E2 E #E 1025 cases (bind_inversion ????? E) * #s3' #I3 * #E3 E #E 1026 <(OK_sig_eq ?????? E) E; 1027 cases (Exists_append ???? H) 1028 [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_l @L2 ] 1029  H #H cases (Exists_append ???? H) 1030 [ #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @Exists_append_l @Exists_append_r @L2 ] 1031  #H3 cases (IH3 s3' I3 H3 E3) #l' * #L1 #L2 %{l'} % [ @L1  @Exists_append_r @Exists_append_l @Exists_append_l @L2 ] 1032 ] 1033 ] 1034  *: #x #e' normalize #E destruct 1035 ] 1036  #s' #p * 1037  #s' #p * 1038  #eo #s' #p * 1039  #e #ls #IH #s' #p #H #E whd in E:(??%?); destruct (* FIXME once switch is implemented ... *) 1040  #l0 #s0 #IH #s' #p #H 1041 whd in ⊢ (??%? → ?) #E cases (reflmatch ????? E) E #l1 * #El #E 1042 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1043 <(OK_sig_eq ?????? E) E; 1044 cases H 1045 [ #El' %{l1} <El' % [ @El  %1 @refl ] 1046  #H1 cases (IH s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1  %2 @L2 ] 1047 ] 1048  #l0 #s' #p * 1049  #l0 #s0 #IH #s' #p #H #E 1050 cases (bind_inversion ????? E) * #s1' #I1 * #E1 E #E 1051 <(OK_sig_eq ?????? E) E; 1052 @(IH s1' I1 H E1) 883 1053 ] qed. 884 1054 885 1055 axiom ParamGlobalMixup : String. 886 1056 887 definition alloc_params : ∀vars:var_types. list (ident×type) → (Σs:stmt.stmt_vars s (local_id vars)) → res (Σs:stmt.stmt_vars s (local_id vars)) ≝888 λvars, params,s. foldl ?? (λs,it.1057 definition alloc_params : ∀vars:var_types.∀ls. list (ident×type) → (Σs:stmt. stmt_inv vars ls s) → res (Σs:stmt.stmt_inv vars ls s) ≝ 1058 λvars,ls,params,s. foldl ?? (λs,it. 889 1059 let 〈id,ty〉 ≝ it in 890 1060 do s ← s; … … 901 1071  Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] 902 1072 ] E) (OK ? s) params. 903 whd % [ whd % [ @I  whd >E @I ]  @sig_ok ] 904 qed. 1073 try @conj try @conj try @conj try @conj try @conj 1074 try @I 1075 [ whd >E @I 1076  @(sig_ok … s) 1077 ] qed. 905 1078 906 1079 definition bigid1 ≝ an_identifier SymbolTag [[ … … 948 1121 ] qed. 949 1122 1123 (* We only record labels from Slabel, not Sgoto, so that we detect badly formed 1124 programs. *) 1125 let rec extend_label_env (s:statement) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝ 1126 match s with 1127 [ Ssequence s1 s2 ⇒ 1128 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in 1129 extend_label_env s2 lbls u 1130  Sifthenelse _ s1 s2 ⇒ 1131 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in 1132 extend_label_env s2 lbls u 1133  Swhile _ s ⇒ extend_label_env s lbls u 1134  Sdowhile _ s ⇒ extend_label_env s lbls u 1135  Sfor s1 _ s2 s3 ⇒ 1136 let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in 1137 let 〈lbls,u〉 ≝ extend_label_env s2 lbls u in 1138 extend_label_env s3 lbls u 1139  Sswitch _ ls ⇒ extend_label_env' ls lbls u 1140  Slabel l s ⇒ 1141 let 〈l',u〉 ≝ fresh ? u in 1142 extend_label_env s (add … lbls l l') u 1143  Scost _ s ⇒ extend_label_env s lbls u 1144  _ ⇒ 〈lbls,u〉 1145 ] 1146 and extend_label_env' (ls:labeled_statements) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝ 1147 match ls with 1148 [ LSdefault s ⇒ extend_label_env s lbls u 1149  LScase _ _ s ls ⇒ 1150 let 〈lbls,u〉 ≝ extend_label_env s lbls u in 1151 extend_label_env' ls lbls u 1152 ]. 1153 1154 definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?). 1155 950 1156 (* FIXME: the temporary handling is nonsense, I'm afraid. *) 951 1157 definition translate_function : list (ident×region) → function → res internal_function ≝ 952 1158 λglobals, f. 1159 let 〈lbls, label_universe〉 ≝ build_label_env (fn_body f) in 953 1160 let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in 954 1161 let tmp ≝ bigid1 in (* FIXME *) 955 1162 let tmpp ≝ bigid2 in (* FIXME *) 956 1163 let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in 957 do s ← translate_statement vartypes tmp tmpp (fn_body f);958 do s ← alloc_params vartypes (fn_params f) s;1164 do s as E1 ← translate_statement vartypes lbls tmp tmpp (fn_body f); 1165 do s as E2 ← alloc_params vartypes lbls (fn_params f) s; 959 1166 OK ? (mk_internal_function 960 1167 (opttyp_of_type (fn_return f)) … … 965 1172 [ whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_hit % 966 1173  whd whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit % % ] 967  @stmt_vars_mp [ 3: @sig_ok  skip ] 1174  @(stmt_P_mp ???? (sig_ok ?? s)) 1175 #s1 * #H1 #H2 % [ 2: @H2 ] 1176 @stmt_vars_mp [ 3: @sig_ok  skip ] 968 1177 #i #H cases (identifier_eq ? tmp i) 969 1178 [ #E <E @Exists_mid @refl 
Deliverables/D3.3/idlookupbranch/Cminor/syntax.ma
r1087 r1096 39 39 ] qed. 40 40 41 axiom Label : String. 42 41 43 inductive stmt : Type[0] ≝ 42 44  St_skip : stmt … … 54 56  St_switch : ∀sz,sg. expr (ASTint sz sg) → list (bvint sz × nat) → nat → stmt 55 57  St_return : option (Σt. expr t) → stmt 56  St_label : ident → stmt → stmt57  St_goto : ident → stmt58  St_label : identifier Label → stmt → stmt 59  St_goto : identifier Label → stmt 58 60  St_cost : costlabel → stmt → stmt. 59 61 62 let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝ 63 match s with 64 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 65  St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2 66  St_loop s' ⇒ P s ∧ stmt_P P s' 67  St_block s' ⇒ P s ∧ stmt_P P s' 68  St_label _ s' ⇒ P s ∧ stmt_P P s' 69  St_cost _ s' ⇒ P s ∧ stmt_P P s' 70  _ ⇒ P s 71 ]. 72 73 lemma stmt_P_P : ∀P,s. stmt_P P s → P s. 74 #P * normalize /2/ 75 [ #s1 #s2 * * /2/ 76  #sz #sg #e #s1 #s2 * * /2/ 77  3,4: #s * /2/ 78  5,6: #i #s normalize * /2/ 79 ] qed. 80 60 81 (* Assert a predicate on every variable or parameter identifier. *) 61 let rec stmt_vars (s:stmt) (P:ident → Prop) on s : Prop ≝ 82 definition stmt_vars : (ident → Prop) → stmt → Prop ≝ 83 λP,s. 62 84 match s with 63 [ St_skip ⇒ True 64  St_assign _ i e ⇒ P i ∧ expr_vars ? e P 85 [ St_assign _ i e ⇒ P i ∧ expr_vars ? e P 65 86  St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P 66 87  St_call oi e es ⇒ match oi with [ None ⇒ True  Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es 67 88  St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es 68  St_seq s1 s2 ⇒ stmt_vars s1 P ∧ stmt_vars s2 P 69  St_ifthenelse _ _ e s1 s2 ⇒ expr_vars ? e P ∧ stmt_vars s1 P ∧ stmt_vars s2 P 70  St_loop s ⇒ stmt_vars s P 71  St_block s ⇒ stmt_vars s P 72  St_exit _ ⇒ True 89  St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P 73 90  St_switch _ _ e _ _ ⇒ expr_vars ? e P 74 91  St_return oe ⇒ match oe with [ None ⇒ True  Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ] 75  St_label _ s ⇒ stmt_vars s P 76  St_goto _ ⇒ True 77  St_cost _ s ⇒ stmt_vars s P 92  _ ⇒ True 78 93 ]. 79 94 80 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars s P → stmt_vars s Q. 95 definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝ 96 λP,s. 97 match s with 98 [ St_label l _ ⇒ P l 99  St_goto l ⇒ P l 100  _ ⇒ True 101 ]. 102 103 lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s. 104 #P #Q #H #s elim s /2/ 105 [ #s1 #s2 #H1 #H2 normalize * * /4/ 106  #sz #sg #e #s1 #s2 #H1 #H2 * * /5/ 107  #s #H * /5/ 108  #s #H * /5/ 109  #l #s #H * /5/ 110  #l #s #H * /5/ 111 ] qed. 112 113 lemma stmt_vars_mp : ∀P,Q. (∀i. P i → Q i) → ∀s. stmt_vars P s → stmt_vars Q s. 81 114 #P #Q #H #s elim s normalize 82 115 [ // … … 86 119  #e #es * #H1 #H2 % [ /3/  @(All_mp … H2) * /3/ ] 87 120  #s1 #s2 #H1 #H2 * /3/ 88  #sz #sg #e #s1 #s2 #H1 #H2 * */5/121  #sz #sg #e #s1 #s2 #H1 #H2 /5/ 89 122  8,9: #s #H1 #H2 /2/ 90 123  // … … 96 129 ] qed. 97 130 131 (* Get labels from a Cminor statement. *) 132 let rec labels_of (s:stmt) : list (identifier Label) ≝ 133 match s with 134 [ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 135  St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2) 136  St_loop s ⇒ labels_of s 137  St_block s ⇒ labels_of s 138  St_label l s ⇒ l::(labels_of s) 139  St_cost _ s ⇒ labels_of s 140  _ ⇒ [ ] 141 ]. 142 98 143 record internal_function : Type[0] ≝ 99 144 { f_return : option typ … … 102 147 ; f_stacksize : nat 103 148 ; f_body : stmt 104 ; f_bound : stmt_vars f_body (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) 149 ; f_inv : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧ 150 stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body 105 151 }. 106 152
Note: See TracChangeset
for help on using the changeset viewer.