Changeset 2286 for src/ASM


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r2275 r2286  
    33
    44include "ASM/String.ma".
    5 include "ASM/ASM.ma".
     5(*include "ASM/ASM.ma".*)
    66include "ASM/Arithmetic.ma". 
    77
     
    99definition ptr_size ≝ bitvector_of_nat 8 2.
    1010definition alignment ≝ None.
    11 
    12 (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
    13         not further back in the translation chain.                            *)
    14 inductive OpAccs: Type[0] ≝
    15   Mul: OpAccs
    16 | DivuModu: OpAccs.
    17 
    18 inductive Op1: Type[0] ≝
    19   Cmpl: Op1
    20 | Inc: Op1
    21 | Rl: Op1. (* TODO: implement left rotation *)
    22 
    23 inductive Op2: Type[0] ≝
    24   Add: Op2
    25 | Addc: Op2
    26 | Sub: Op2
    27 | And: Op2
    28 | Or: Op2
    29 | Xor: Op2.
    3011
    3112(* dpm: maybe useless? *)
     
    170151   Register31; Register32; Register33; Register34; Register35;
    171152   Register36; Register37].
    172 
    173 definition register_address: Register → [[ acc_a; direct; registr ]] ≝
    174   λr: Register.
    175     match r with
    176     [ Register00 ⇒ REGISTER [[ false; false; false ]]
    177     | Register01 ⇒ REGISTER [[ false; false; true ]]
    178     | Register02 ⇒ REGISTER [[ false; true; false ]]
    179     | Register03 ⇒ REGISTER [[ false; true; true ]]
    180     | Register04 ⇒ REGISTER [[ true; false; false ]]
    181     | Register05 ⇒ REGISTER [[ true; false; true ]]
    182     | Register06 ⇒ REGISTER [[ true; true; false ]]
    183     | Register07 ⇒ REGISTER [[ true; true; true ]]
    184     | RegisterA ⇒ ACC_A
    185     | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    186     | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    187     | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    188     | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
    189     ].
    190     [*: normalize
    191         @ I
    192     ]
    193 qed.
    194 
    195 record Eval: Type[0] ≝
    196 {
    197   opaccs: OpAccs → Byte → Byte → Byte × Byte;
    198   op1: Op1 → Byte → Byte;
    199   op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
    200 }.
    201 
    202 axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    203 axiom op1_implementation: Op1 → Byte → Byte.
    204 axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
    205 
    206 definition eval: Eval ≝
    207   mk_Eval opaccs_implementation
    208           op1_implementation
    209           op2_implementation.
  • src/ASM/Util.ma

    r2211 r2286  
    14371437interpretation "dependent if then else" 'if_then_else_safe b f g = (if_then_else_safe ? b f g).
    14381438
     1439lemma If_elim : ∀A.∀P : A → Prop.∀b : bool.∀f : b → A.∀g : Not (bool_to_Prop b) → A.
     1440  (∀prf.P (f prf)) → (∀prf.P (g prf)) → P (If b then with prf do f prf else with prf do g prf).
     1441#A #P * #f #g #H1 #H2 normalize // qed.
     1442
    14391443(* Also extracts an equality proof (useful when not using Russell). *)
    14401444notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
  • src/ASM/Vector.ma

    r2124 r2286  
    9292  @(dependent_rewrite_vectors A … E)
    9393  try assumption %
     94qed.
     95
     96lemma Vector_singl_elim : ∀A.∀P : Vector A 1 → Prop.∀v.
     97  (∀a.v = [[ a ]] → P [[ a ]]) → P v.
     98#A #P #v
     99elim (Vector_Sn … v) #a * #tl >(Vector_O … tl) #EQ >EQ #H @H % qed.
     100
     101lemma Vector_pair_elim : ∀A.∀P : Vector A 2 → Prop.∀v.
     102  (∀a,b.v = [[ a ; b ]] → P [[ a ; b ]]) → P v.
     103#A #P #v
     104elim (Vector_Sn … v) #a * #tl @(Vector_singl_elim … tl) #b #EQ1 #EQ2 destruct
     105#H @H %
     106qed.
     107
     108lemma Vector_triple_elim : ∀A.∀P : Vector A 3 → Prop.∀v.
     109  (∀a,b,c.v = [[ a ; b ; c ]] → P [[ a ; b ; c ]]) → P v.
     110#A #P #v
     111elim (Vector_Sn … v) #a * #tl @(Vector_pair_elim … tl) #b #c #EQ1 #EQ2 destruct
     112#H @H %
    94113qed.
    95114
     
    214233[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].
    215234
     235lemma tail_head' : ∀A,n,v.v = head' A n v ::: tail … v.
     236#A #n #v elim (Vector_Sn … v) #hd * #tl #EQ >EQ % qed.
     237
    216238let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
    217239 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
     
    421443qed.
    422444
     445lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v.
     446#A #n #v elim v -n [%]
     447#n #hd #tl change with (?→?:::(?@@?)≃?)
     448lapply (tl@@[[ ]])
     449<plus_n_O #v #EQ >EQ %
     450qed.
     451
    423452lemma vector_associative_append:
    424453  ∀A: Type[0].
     
    591620    //
    592621qed.
    593    
     622
     623lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m.
     624  v @@ u = v' @@ u' → v = v' ∧ u = u'.
     625#A #n #m #v elim v -n
     626[ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} %
     627| #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' -v'
     628  #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''}
     629  >EQ' %
     630]
     631qed.
     632
    594633(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    595634(* Other manipulations.                                                       *)
     
    761800  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
    762801] qed.
     802
     803lemma eq_v_append : ∀A,n,m,test,v1,v2,u1,u2.
     804  eq_v A (n+m) test (v1@@u1) (v2@@u2) =
     805  (eq_v A n test v1 v2 ∧ eq_v A m test u1 u2).
     806#A #n #m #test #v1 lapply m -m elim v1 -n
     807[ #m #v2 >(Vector_O … v2) #u1 #u2 % ]
     808#n #hd #tl #IH #m #v2
     809elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
     810#u1 #u2 whd in ⊢ (??%(?%?));
     811whd in match (head' ???);
     812whd in match (tail ???);
     813whd in match (tail ???);
     814elim (test ??) normalize nodelta [ @IH | % ]
     815qed.
    763816
    764817(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    881934  ]
    882935qed.
     936
     937(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     938(* Vector prefix and suffix relations.                                        *)
     939(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     940
     941(* n.b.: if n = m this is equivalent to equality, without n and m needing to be
     942   Leibniz-equal *)
     943let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝
     944match v1 with
     945[ VEmpty ⇒ true
     946| VCons n' hd1 tl1 ⇒
     947  match v2 with
     948  [ VEmpty ⇒ false
     949  | VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2
     950  ]
     951].
     952
     953let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝
     954If leb (S n) m then with prf do
     955  match v2 return λm.λv2:Vector A m.leb (S n) m → bool with
     956  [ VEmpty ⇒ Ⓧ
     957  | VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2
     958  ] prf
     959else (if eqb n m then
     960  vprefix A n m test v1 v2
     961else
     962  false).
     963
     964include alias "arithmetics/nat.ma".
     965
     966lemma prefix_to_le : ∀A,n,m,test,v1,v2.
     967  vprefix A n m test v1 v2 → n ≤ m.
     968#A #n #m #test #v1 lapply m -m elim v1 -n [//]
     969#n #hd #tl #IH #m * -m [*]
     970#m #hd' #tl'
     971whd in ⊢ (?%→?);
     972elim (test ??) [2: *]
     973whd in ⊢ (?%→?);
     974#H @le_S_S @(IH … H)
     975qed.
     976
     977lemma vprefix_ok : ∀A,n,m,test,v1,v2.
     978  vprefix A n m test v1 v2 → le n m ∧
     979  ∃pre.∃post : Vector A (m - n).v2 ≃ pre @@ post ∧
     980            bool_to_Prop (eq_v … test v1 pre).
     981#A #n #m #test #v1 #v2 #G %{(prefix_to_le … G)}
     982lapply G lapply v2 lapply m -m elim v1 -n
     983[ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ]
     984#n #hd1 #tl1 #IH #m * -m [*]
     985#m #hd2 #tl2 whd in ⊢ (?%→?);
     986elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *]
     987#G elim (IH … G) #pre * #post * #EQ #EQ'
     988%{(hd2:::pre)} %{post} %
     989[ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post)
     990  <(minus_to_plus m … (prefix_to_le … G) (refl …))
     991  #V #EQ'' >EQ'' %
     992| whd in ⊢ (?%);
     993  whd in match (head' ???); >H
     994  @EQ'
     995]
     996qed.
     997
     998lemma vprefix_to_eq : ∀A,n,test,v1,v2.
     999  vprefix A n n test v1 v2 = eq_v … test v1 v2.
     1000#A #n #test #v1 elim v1 -n
     1001[ #v2 >(Vector_O … v2) %
     1002| #n #hd1 #tl1 #IH
     1003  #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ)
     1004  normalize elim (test ??) [2: %]
     1005  normalize @IH
     1006]
     1007qed.
     1008
     1009lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m.
     1010  eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)).
     1011#A #n #m #test #v1 lapply m -m elim v1 -n
     1012[ #m #pre #post #_ %
     1013| #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre
     1014  #post
     1015  whd in ⊢ (?%→?%); whd in match (head' ???);
     1016  elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???);
     1017  @IH
     1018]
     1019qed.
     1020
     1021lemma vsuffix_to_le : ∀A,n,m,test,v1,v2.
     1022  vsuffix A n m test v1 v2 → n ≤ m.
     1023#A #n #m #test #v1 #v2 lapply v1 lapply n -n elim v2 -m
     1024[ #n * -n
     1025  [ * %
     1026  | #n #hd #tl *
     1027  ]
     1028| #m #hd2 #tl2 #IH
     1029  #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
     1030  @If_elim normalize nodelta @leb_elim #H *
     1031  [ #_ @(transitive_le … H) %2 %1
     1032  | #ABS elim (ABS I)
     1033  | #_ @eqb_elim #G normalize nodelta [2: *]
     1034    destruct #_ %
     1035  ]
     1036]
     1037qed.
     1038 
     1039lemma vsuffix_ok : ∀A,n,m,test,v1,v2.
     1040  vsuffix A n m test v1 v2 → le n m ∧
     1041  ∃pre : Vector A (m - n).∃post.v2 ≃ pre @@ post ∧
     1042            bool_to_Prop (eq_v … test v1 post).
     1043#A #n #m #test #v1 #v2 #G %{(vsuffix_to_le … G)}
     1044lapply G lapply v1 lapply n -n
     1045elim v2 -m
     1046[ #n #v1
     1047  whd in ⊢ (?%→?);
     1048  @eqb_elim #EQ1 [2: *]
     1049  normalize nodelta lapply v1 -v1 >EQ1 #v1
     1050  >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % %
     1051| #m #hd2 #tl2 #IH #n #v1
     1052  change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
     1053  @If_elim normalize nodelta #H
     1054  [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2
     1055    >minus_Sn_m
     1056    [ %{(hd2:::pre)} %{post} %{EQ2}
     1057      change with (?≃?:::(?@@?))
     1058      lapply EQ1 lapply (pre@@post)
     1059      <plus_minus_m_m
     1060      [ #v #EQ >EQ %]
     1061    ]
     1062    @(vsuffix_to_le … G)
     1063  | @eqb_elim #EQn [2: *] normalize nodelta
     1064    generalize in match (hd2:::tl2);
     1065    <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?)));
     1066    #v2' >vprefix_to_eq #G
     1067    <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?)));
     1068    <minus_n_n %{[[ ]]} %{v2'} %{G}
     1069    %
     1070  ]
     1071]
     1072qed.
     1073
     1074lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m.
     1075  eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)).
     1076#A #n #m #test #pre lapply m -m elim pre -n
     1077[ #m #v1 #post lapply v1 -v1 cases post -m
     1078  [ #v1 >(Vector_O … v1) * %
     1079  | #m #hd #tl #v1 #G
     1080    change with (bool_to_Prop (If ? then with prf do ? else ?))
     1081    @If_elim normalize nodelta
     1082    [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ]
     1083    #_ >eqb_n_n normalize nodelta
     1084    >vprefix_to_eq assumption
     1085  ]
     1086| #n #hd2 #tl2 #IH
     1087  #m #v1 #post #G
     1088  change with (bool_to_Prop (If ? then with prf do ? else ?))
     1089  @If_elim normalize nodelta
     1090  [ #H @IH @G
     1091  | @leb_elim [ #_ * #ABS elim (ABS I) ]
     1092    #H #_ @eqb_elim #K
     1093    [ @⊥ @(absurd ? K) @lt_to_not_eq // ]
     1094    normalize elim H -H #H @H normalize
     1095    >plus_n_Sm_fast //
     1096  ]
     1097]
     1098qed.
     1099
     1100(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     1101(* Vector flattening and recursive splitting.                                 *)
     1102(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     1103
     1104let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝
     1105match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with
     1106[ O ⇒ λ_.VEmpty ?
     1107| S k ⇒
     1108  λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in
     1109  pre ::: rvsplit … post
     1110].
     1111
     1112let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝
     1113match v return λn.λ_ : Vector ? n.Vector ? (n * m) with
     1114[ VEmpty ⇒ VEmpty ?
     1115| VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl
     1116].
     1117
     1118lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v.
     1119#A #n elim n -n
     1120[ #m #v >(Vector_O ? v) %
     1121| #n #IH #m #v
     1122  whd in match (rvsplit ????);
     1123  @vsplit_elim #pre #post #EQ
     1124  normalize nodelta
     1125  whd in match (vflatten ????); >IH >EQ %
     1126]
     1127qed.
     1128
     1129lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v.
     1130#A #n #m #v elim v -n
     1131[ %
     1132| #n #hd #tl #IH
     1133  whd in match (vflatten ????);
     1134  whd in match (rvsplit ????);
     1135  @vsplit_elim #pre #post #EQ
     1136  elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2
     1137  normalize nodelta >IH %
     1138]
     1139qed.
     1140
     1141(* Paolo: should'nt it be in the standard library? *)
     1142lemma sym_jmeq : ∀A,B.∀a : A.∀b : B.a≃b → b≃a.
     1143#A #B #a #b * % qed.
     1144
     1145lemma vflatten_append : ∀A,n,m,p,v1,v2.
     1146  vflatten A (n+m) p (v1 @@ v2) ≃ vflatten A n p v1 @@ vflatten A m p v2.
     1147#A #n #m #p #v1 lapply m -m elim v1
     1148[ #m #v2 %
     1149| #n #hd1 #tl1 #IH #m #v2
     1150  whd in ⊢ (??%?(????%?));
     1151  lapply (IH … v2)
     1152  lapply (vflatten … (tl1@@v2))
     1153  cut ((n+m)*p = n*p + m*p)
     1154  [ // ] #EQ whd in match (S n + m); whd in match (S ? * ?);
     1155  whd in match (S n * ?); >EQ in ⊢ (%→?%%??→?%%??); -EQ
     1156  #V #EQ >EQ -V @sym_jmeq @vector_associative_append
     1157]
     1158qed.
     1159
     1160lemma eq_v_vflatten : ∀A,n,m,test,v1,v2.
     1161  eq_v A ? test (vflatten A n m v1) (vflatten A n m v2) =
     1162  eq_v ?? (eq_v … test) v1 v2.
     1163#A #n #m #test #v1 elim v1 -n
     1164[ #v2 >(Vector_O … v2) % ]
     1165#n #hd #tl #IH #v2
     1166elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
     1167whd in ⊢ (??(????%%)%);
     1168whd in match (head' ???);
     1169whd in match (tail ???);
     1170>eq_v_append >IH %
     1171qed.
     1172
     1173lemma vprefix_vflatten : ∀A,n,m,p,test.∀v1,v2.
     1174  vprefix ? n m (eq_v ? p test) v1 v2 →
     1175  bool_to_Prop (vprefix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
     1176#A #n #m #p #test #v1 #v2 #G
     1177elim (vprefix_ok … G) #le_nm
     1178* #pre * #post *
     1179lapply (vflatten_append … pre post)
     1180lapply (pre @@ post)
     1181<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
     1182#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
     1183lapply (vflatten A m p v2')
     1184cut (m*p = n*p + (m-n)*p)
     1185[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
     1186  <distributive_times_plus <(minus_to_plus … le_nm (refl …)) % ]
     1187#EQ >EQ #v2' #EQ' >EQ' -v2' -v2'
     1188#G @vprefix_true
     1189>eq_v_vflatten @G
     1190qed.
     1191
     1192lemma vsuffix_vflatten : ∀A,n,m,p,test.∀v1,v2.
     1193  vsuffix ? n m (eq_v ? p test) v1 v2 →
     1194  bool_to_Prop (vsuffix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
     1195#A #n #m #p #test #v1 #v2 #G
     1196elim (vsuffix_ok … G) #le_nm * #pre * #post *
     1197lapply (vflatten_append … pre post)
     1198lapply (pre @@ post)
     1199>commutative_plus in ⊢ (%→?%%??→???%%→?);
     1200<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
     1201#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
     1202lapply (vflatten A m p v2')
     1203cut (m*p = (m-n)*p + n*p)
     1204[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
     1205  <distributive_times_plus <commutative_plus <(minus_to_plus … le_nm (refl …)) % ]
     1206#EQ >EQ #v2' #EQ' >EQ'
     1207#G @vsuffix_true
     1208>eq_v_vflatten @G
     1209qed.
Note: See TracChangeset for help on using the changeset viewer.