Changeset 1351 for src/Clight
 Timestamp:
 Oct 11, 2011, 12:24:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r1316 r1351 137 137 qed. 138 138 139 include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)140 141 139 lemma characterise_vars_all : ∀l,f,vars,n. 142 140 characterise_vars l f = 〈vars,n〉 → … … 146 144 whd in ⊢ (∀_.∀_.??%? → ?) 147 145 elim (fn_params f @ fn_vars f) 148 [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) E;#i #H @False_ind146 [ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind 149 147 elim globals in H 150 148 [ normalize // … … 160 158 @(IH m0 n0) 161 159 [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ 162  2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE160  2,4: destruct (EQ2) @(local_id_add_miss … H) @NE 163 161 ] 164 162 ] … … 724 722 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 725 723 * #tmp' #u whd in ⊢ (???% → ?) #E 726 >(pair_eq2 ?????? E) 724 destruct 727 725 #id #H 728 726 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ] … … 780 778 generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?) 781 779 * #tmp' #u' whd in ⊢ (???% → ?) #E 782 >(pair_eq1 ?????? E) >(pair_eq2 ?????? E) 780 destruct 783 781 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ?  _ ⇒ ? ] >lookup_add_hit 784 782 @I 785 783 qed. 786 787 lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x.788 #A #P #P' #H1 * #x #H2 @H1 @H2789 qed.790 791 definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝792 λA,B,C,P,e,f.793 match e with794 [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ]795  Error msg ⇒ Error ? msg796 ].797 798 notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.799 (*800 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.801 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.802 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.803 *)804 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).805 784 806 785 let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝ … … 826 805 ] 827 806  Ssequence s1 s2 ⇒ 828 do 〈s1', u1〉 with H1← translate_statement vars lbls u s1;829 do 〈s2', u2〉 with H2← translate_statement vars lbls u1 s2;807 do «s1', u1, H1» ← translate_statement vars lbls u s1; 808 do «s2', u2, H2» ← translate_statement vars lbls u1 s2; 830 809 OK ? «〈St_seq s1' s2', u2〉, ?» 831 810  Sifthenelse e1 s1 s2 ⇒ … … 833 812 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 834 813 [ ASTint _ _ ⇒ λe1'. 835 do 〈s1', u〉 with H1← translate_statement vars lbls u s1;836 do 〈s2', u〉 with H2← translate_statement vars lbls u s2;814 do «s1', u, H1» ← translate_statement vars lbls u s1; 815 do «s2', u, H2» ← translate_statement vars lbls u s2; 837 816 OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?» 838 817  _ ⇒ λ_.Error ? (msg TypeMismatch) … … 842 821 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 843 822 [ ASTint _ _ ⇒ λe1'. 844 do 〈s1', u〉 with H1← translate_statement vars lbls u s1;823 do «s1', u, H1» ← translate_statement vars lbls u s1; 845 824 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 846 825 OK ? «〈St_block … … 853 832 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 854 833 [ ASTint _ _ ⇒ λe1'. 855 do 〈s1',u〉 with H1← translate_statement vars lbls u s1;834 do «s1',u, H1» ← translate_statement vars lbls u s1; 856 835 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 857 836 OK ? «〈St_block … … 864 843 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with 865 844 [ ASTint _ _ ⇒ λe1'. 866 do 〈s1', u〉 with H1← translate_statement vars lbls u s1;867 do 〈s2', u〉 with H2← translate_statement vars lbls u s2;868 do 〈s3', u〉 with H3← translate_statement vars lbls u s3;845 do «s1', u, H1» ← translate_statement vars lbls u s1; 846 do «s2', u, H2» ← translate_statement vars lbls u s2; 847 do «s3', u, H3» ← translate_statement vars lbls u s3; 869 848 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 870 849 OK ? «〈St_seq s1' … … 886 865  Slabel l s1 ⇒ 887 866 do l' as E ← lookup_label lbls l; 888 do 〈s1', u〉 with H1← translate_statement vars lbls u s1;867 do «s1', u, H1» ← translate_statement vars lbls u s1; 889 868 OK ? «〈St_label l' s1', u〉, ?» 890 869  Sgoto l ⇒ … … 892 871 OK ? «〈St_goto l', u〉, ?» 893 872  Scost l s1 ⇒ 894 do 〈s1', u〉 with H1← translate_statement vars lbls u s1;873 do «s1', u, H1» ← translate_statement vars lbls u s1; 895 874 OK ? «〈St_cost l s1', u〉, ?» 896 875 ]. … … 954 933 λvars,ls,s0,u,params,s. foldl ?? (λsu,it. 955 934 let 〈id,ty〉 ≝ it in 956 do 〈s,u〉 with Is← su;935 do «s,u, Is» ← su; 957 936 do t as E ← lookup' vars id; 958 937 match t return λx.? → ? with … … 1074 1053 let tmp ≝ mk_tmpgen tmpuniverse [ ] in 1075 1054 do s ← translate_statement vartypes lbls tmp (fn_body f); 1076 do 〈s,tmp〉 with Is← alloc_params vartypes lbls ?? (fn_params f) s;1055 do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s; 1077 1056 OK ? (mk_internal_function 1078 1057 (opttyp_of_type (fn_return f))
Note: See TracChangeset
for help on using the changeset viewer.