Changeset 465 for Deliverables


Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

Location:
Deliverables/D4.1/Matita
Files:
14 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/ASM.ma

    r410 r465  
    1 include "Either.ma".
    21include "BitVector.ma".
    32include "String.ma".
    … …  
    76| INDIRECT: Bit → addressing_mode
    87| EXT_INDIRECT: Bit → addressing_mode
    9 | REGISTER: BitVector (S (S (S Z))) → addressing_mode
     8| REGISTER: BitVector (S (S (S O))) → addressing_mode
    109| ACC_A: addressing_mode
    1110| ACC_B: addressing_mode
    … …  
    9392
    9493
    95 nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝
    96  match l return λm.λ_:Vector addressing_mode_tag m.Bool with
     94nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
     95 match l return λm.λ_:Vector addressing_mode_tag m.bool with
    9796  [ VEmpty ⇒ false
    9897  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    … …  
    198197 | WithLabel: jump String → labelled_instruction.
    199198
    200 ndefinition preamble ≝ List (String × Nat).
    201 
    202 ndefinition assembly_program ≝ preamble × (List labelled_instruction).
     199ndefinition preamble ≝ list (String × nat).
     200
     201ndefinition assembly_program ≝ preamble × (list labelled_instruction).

  • Deliverables/D4.1/Matita/Arithmetic.ma

    r462 r465  
    1 include "Exponential.ma".
    21include "BitVector.ma".
     2include "Util.ma".
    33
    44ndefinition nat_of_bool ≝
    5   λb: Bool.
     5  λb: bool.
    66    match b with
    7       [ false ⇒ Z
    8       | true ⇒ S Z
     7      [ false ⇒ O
     8      | true ⇒ S O
    99      ].
    1010   
    1111ndefinition add_n_with_carry:
    12       ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
    13   λn: Nat.
     12      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     13  λn: nat.
    1414  λb: BitVector n.
    1515  λc: BitVector n.
    16   λcarry: Bool.
     16  λcarry: bool.
    1717    let b_as_nat ≝ nat_of_bitvector n b in
    1818    let c_as_nat ≝ nat_of_bitvector n c in
    1919    let carry_as_nat ≝ nat_of_bool carry in
    2020    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
    21     let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
    22                   (modulus c_as_nat ((S (S Z)) * n)) +
    23                   c_as_nat) ≳ ((S (S Z)) * n) in
    24     let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
    25                   (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
    26                   c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in
    27     let result ≝ modulus result_old ((S (S Z))^n) in
    28     let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
     21    let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
     22                  (modulus c_as_nat (2 * n)) +
     23                  c_as_nat) (2 * n) in
     24    let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
     25                  (modulus c_as_nat (2^(n - 1))) +
     26                  c_as_nat) (2^(n - 1)) in
     27    let result ≝ modulus result_old (2^n) in
     28    let cy_flag ≝ geb result_old (2^n) in
    2929    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
    30       mk_Cartesian ? ? (bitvector_of_nat n result)
     30      mk_pair ? ? (bitvector_of_nat n result)
    3131                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
    3232
    33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
    34   λn: Nat.
     33ndefinition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
     34  λn: nat.
    3535  λb: BitVector n.
    3636  λc: BitVector n.
    37   λcarry: Bool.
     37  λcarry: bool.
    3838     let b_as_nat ≝ nat_of_bitvector n b in
    3939     let c_as_nat ≝ nat_of_bitvector n c in
    4040     let carry_as_nat ≝ nat_of_bool carry in
    41      let temporary ≝ (b_as_nat mod (two * n)) - (c_as_nat mod (two * n)) in
    42      let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in
    43      let bit_six ≝ less_than_b (b_as_nat mod (two^(n - one))) ((c_as_nat mod (two^(n - one))) + carry_as_nat) in
     41     let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
     42     let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
     43     let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
    4444     let 〈b',cy_flag〉 ≝
    45        if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then
     45       if geb b_as_nat (c_as_nat + carry_as_nat) then
    4646         〈b_as_nat, false〉
    4747       else
    48          〈b_as_nat + (two^n), true〉
     48         〈b_as_nat + (2^n), true〉
    4949     in
    5050       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
    5151         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
    5252         
    53 ndefinition add_8_with_carry ≝ add_n_with_carry eight.
    54 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
    55 ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.
    56 ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.
     53ndefinition add_8_with_carry ≝ add_n_with_carry 8.
     54ndefinition add_16_with_carry ≝ add_n_with_carry 16.
     55ndefinition sub_8_with_carry ≝ sub_n_with_carry 8.
     56ndefinition sub_16_with_carry ≝ sub_n_with_carry 16.
    5757
    5858ndefinition increment ≝
    59   λn: Nat.
    60   λb: BitVector n.
    61     let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
    62     let overflow ≝ b_as_nat ≳ (S (S Z))^n in
     59  λn: nat.
     60  λb: BitVector n.
     61    let b_as_nat ≝ (nat_of_bitvector n b) + (S O) in
     62    let overflow ≝ geb b_as_nat (S (S O))^n in
    6363      match overflow with
    6464        [ false ⇒ bitvector_of_nat n b_as_nat
    … …  
    6767       
    6868ndefinition decrement ≝
    69   λn: Nat.
     69  λn: nat.
    7070  λb: BitVector n.
    7171    let b_as_nat ≝ nat_of_bitvector n b in
    7272      match b_as_nat with
    73         [ Z ⇒ max n
     73        [ O ⇒ max n
    7474        | S o ⇒ bitvector_of_nat n o
    7575        ].
    7676   
    7777ndefinition two_complement_negation ≝
    78   λn: Nat.
     78  λn: nat.
    7979  λb: BitVector n.
    8080    let new_b ≝ negation_bv n b in
    … …  
    8282   
    8383ndefinition addition_n ≝
    84   λn: Nat.
     84  λn: nat.
    8585  λb, c: BitVector n.
    8686    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
    … …  
    8888   
    8989ndefinition subtraction ≝
    90   λn: Nat.
     90  λn: nat.
    9191  λb, c: BitVector n.
    9292    addition_n n b (two_complement_negation n c).
    9393   
    9494ndefinition multiplication ≝
    95   λn: Nat.
     95  λn: nat.
    9696  λb, c: BitVector n.
    9797    let b_nat ≝ nat_of_bitvector ? b in
    … …  
    101101     
    102102ndefinition division_u ≝
    103   λn: Nat.
     103  λn: nat.
    104104  λb, c: BitVector n.
    105105    let b_nat ≝ nat_of_bitvector ? b in
    106106    let c_nat ≝ nat_of_bitvector ? c in
    107107    match c_nat with
    108     [ Z ⇒ Nothing ?
     108    [ O ⇒ None ?
    109109    | _ ⇒
    110110      let result ≝ b_nat ÷ c_nat in
    111         Just ? (bitvector_of_nat n result)
     111        Some ? (bitvector_of_nat n result)
    112112    ].
    113113     
    114 ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe (BitVector n) ≝
     114ndefinition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
    115115  λn.
    116116    match n with
    117     [ Z ⇒ λb, c. Nothing ?
     117    [ O ⇒ λb, c. None ?
    118118    | S p ⇒ λb, c: BitVector (S p).
    119         let b_sign_bit ≝ get_index_v ? ? b Z ? in
    120         let c_sign_bit ≝ get_index_v ? ? c Z ? in
     119        let b_sign_bit ≝ get_index_v ? ? b O ? in
     120        let c_sign_bit ≝ get_index_v ? ? c O ? in
    121121        let b_as_nat ≝ nat_of_bitvector ? b in
    122122        let c_as_nat ≝ nat_of_bitvector ? c in
    123123        match c_as_nat with
    124         [ Z ⇒ Nothing ?
     124        [ O ⇒ None ?
    125125        | S o ⇒
    126126          match b_sign_bit with
    127127          [ true ⇒
    128             let temp_b ≝ (b_as_nat - (two^((S p)-one))) in
     128            let temp_b ≝ b_as_nat - (2^p) in
    129129            match c_sign_bit with
    130130            [ true ⇒
    131               let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
    132                 Just ? (bitvector_of_nat ? (temp_b ÷ temp_c))
     131              let temp_c ≝ c_as_nat - (2^p) in
     132                Some ? (bitvector_of_nat ? (temp_b ÷ temp_c))
    133133            | false ⇒
    134               let result ≝ (temp_b ÷ c_as_nat) + (two^((S p)-one)) in
    135                 Just ? (bitvector_of_nat ? result)
     134              let result ≝ (temp_b ÷ c_as_nat) + (2^p) in
     135                Some ? (bitvector_of_nat ? result)
    136136            ]
    137137          | false ⇒
    138138            match c_sign_bit with
    139139            [ true ⇒
    140               let temp_c ≝ (c_as_nat - (two^((S p)-one))) in
    141               let result ≝ (b_as_nat ÷ temp_c) + (two^((S p)-one)) in
    142                 Just ? (bitvector_of_nat ? result)
    143             | false ⇒ Just ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
     140              let temp_c ≝ c_as_nat - (2^p) in
     141              let result ≝ (b_as_nat ÷ temp_c) + (2^p) in
     142                Some ? (bitvector_of_nat ? result)
     143            | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))
    144144            ]
    145145          ]
    … …  
    161161  λb, c: BitVector n.
    162162    match division_s n b c with
    163       [ Nothing ⇒ Nothing ?
    164       | Just result ⇒
    165           let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in
    166             Just ? (subtraction n b low_bits)
     163      [ None ⇒ None ?
     164      | Some result ⇒
     165          let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in
     166            Some ? (subtraction n b low_bits)
    167167      ].
    168168     
    … …  
    172172    let b_nat ≝ nat_of_bitvector ? b in
    173173    let c_nat ≝ nat_of_bitvector ? c in
    174       less_than_b b_nat c_nat.
     174      ltb b_nat c_nat.
    175175     
    176176ndefinition gt_u ≝ λn, b, c. lt_u n c b.
    177177
    178 ndefinition lte_u ≝ λn, b, c. negation (gt_u n b c).
    179 
    180 ndefinition gte_u ≝ λn, b, c. negation (lt_u n b c).
     178ndefinition lte_u ≝ λn, b, c. ¬(gt_u n b c).
     179
     180ndefinition gte_u ≝ λn, b, c. ¬(lt_u n b c).
    181181     
    182182ndefinition lt_s ≝
    … …  
    184184  λb, c: BitVector n.
    185185    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
    186     let ov_flag ≝ get_index_v ? ? flags two ? in
     186    let ov_flag ≝ get_index_v ? ? flags 2 ? in
    187187     if ov_flag then
    188188       true
    189189     else
    190        ((match n return λn'.BitVector n' → Bool with
    191        [ Z ⇒ λ_.false
     190       ((match n return λn'.BitVector n' → bool with
     191       [ O ⇒ λ_.false
    192192       | S o ⇒
    193          λresult'.(get_index_v ? ? result' Z ?)
     193         λresult'.(get_index_v ? ? result' O ?)
    194194       ]) result).
    195195      //;
    … …  
    198198ndefinition gt_s ≝ λn,b,c. lt_s n c b.
    199199
    200 ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c).
    201 
    202 ndefinition gte_s ≝ λn. λb, c.
    203   negation (lt_s n b c).
    204      
    205 alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
     200ndefinition lte_s ≝ λn,b,c. ¬(gt_s n b c).
     201
     202ndefinition gte_s ≝ λn. λb, c. ¬(lt_s n b c).
     203     
     204alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
    206205
    207206ndefinition bitvector_of_bool:
    208       ∀n: Nat. ∀b: Bool. BitVector (S n) ≝
    209   λn: Nat.
    210   λb: Bool.
    211    (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z ↦ S n⌉.
     207      ∀n: nat. ∀b: bool. BitVector (S n) ≝
     208  λn: nat.
     209  λb: bool.
     210   (pad (S n - (S O)) (S O) [[b]])⌈(S n - (S O)) + S O ↦ S n⌉.
    212211 /2/.
    213212nqed.
    214213
    215214ndefinition full_add ≝
    216   λn: Nat.
     215  λn: nat.
    217216  λb, c: BitVector n.
    218217  λd: Bit.
    219218    fold_right2_i ? ? ? (
    220219      λn.
    221        λb1, b2: Bool.
     220       λb1, b2: bool.
    222221        λd: Bit × (BitVector n).
    223222        let 〈c1,r〉 ≝ d in
    224           〈inclusive_disjunction (conjunction b1 b2)
    225                                  (conjunction c1 (inclusive_disjunction b1 b2)),
     223          〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)),
    226224           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
    227225     〈d, [[ ]]〉 ? b c.
    228226   
    229227ndefinition half_add ≝
    230   λn: Nat.
     228  λn: nat.
    231229  λb, c: BitVector n.
    232230    full_add n b c false.

  • Deliverables/D4.1/Matita/Assembly.ma

    r437 r465  
    1010     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    1111      [ ADDR11 w ⇒ λ_.
    12          let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
     12         let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in
    1313          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    1414      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    … …  
    3030     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    3131      [ ADDR11 w ⇒ λ_.
    32          let 〈v1,v2〉 ≝ split ?  (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
     32         let 〈v1,v2〉 ≝ split ?  (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in
    3333          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    3434      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    3535  | ANL addrs ⇒
    3636     match addrs with
    37       [ Left addrs ⇒ match addrs with
    38          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     37      [ inl addrs ⇒ match addrs with
     38         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    3939           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    4040            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    … …  
    4343            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
    4444            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    45          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     45         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    4646            let b1 ≝
    4747             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    … …  
    5353             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    5454         ]
    55       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     55      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    5656         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    5757          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
    … …  
    157157           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
    158158         match addrs with
    159           [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     159          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    160160             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
    161161              [ DIRECT b1 ⇒ λ_.
    … …  
    164164                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
    165165              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    166           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     166          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    167167             let b2 ≝
    168168              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
    169169               [ DATA b2 ⇒ λ_. b2
    170170               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    171              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
     171             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
    172172              [ REGISTER r⇒ λ_.
    173173                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
    … …  
    193193     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    194194      [ ADDR16 w ⇒ λ_.
    195          let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     195         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    196196          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    197197      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    … …  
    199199     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    200200      [ ADDR16 w ⇒ λ_.
    201          let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     201         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    202202          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    203203      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    204204  | MOV addrs ⇒
    205205     match addrs with
    206       [ Left addrs ⇒
     206      [ inl addrs ⇒
    207207         match addrs with
    208           [ Left addrs ⇒
     208          [ inl addrs ⇒
    209209             match addrs with
    210               [ Left addrs ⇒
     210              [ inl addrs ⇒
    211211                 match addrs with
    212                   [ Left addrs ⇒
     212                  [ inl addrs ⇒
    213213                     match addrs with
    214                       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     214                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    215215                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    216216                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    … …  
    219219                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
    220220                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    221                       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     221                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    222222                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
    223223                          [ REGISTER r ⇒ λ_.
    … …  
    234234                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    235235                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    236                   | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     236                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    237237                     let b1 ≝
    238238                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    … …  
    246246                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
    247247                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    248               | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     248              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    249249                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    250250                  [ DATA16 w ⇒ λ_.
    251                      let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     251                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
    252252                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
    253253                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    254           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     254          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    255255             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    256256              [ BIT_ADDR b1 ⇒ λ_.
    257257                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
    258258              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    259       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     259      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    260260         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
    261261          [ BIT_ADDR b1 ⇒ λ_.
    … …  
    271271  | MOVX addrs ⇒
    272272     match addrs with
    273       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     273      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    274274         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    275275          [ EXT_INDIRECT i1 ⇒ λ_.
    … …  
    278278             [ ([[true;true;true;false;false;false;false;false]]) ]
    279279          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    280       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     280      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    281281         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
    282282          [ EXT_INDIRECT i1 ⇒ λ_.
    … …  
    291291  | ORL addrs ⇒
    292292     match addrs with
    293       [ Left addrs ⇒
     293      [ inl addrs ⇒
    294294         match addrs with
    295           [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     295          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    296296             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
    297297             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    … …  
    300300             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
    301301             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    302           | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     302          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    303303            let b1 ≝
    304304              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    … …  
    311311                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
    312312              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    313       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
     313      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
    314314         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    315315          [ BIT_ADDR b1 ⇒ λ_.
    … …  
    381381  | XRL addrs ⇒
    382382     match addrs with
    383       [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     383      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    384384         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
    385385          [ REGISTER r ⇒ λ_.
    … …  
    392392             [ ([[false;true;true;false;false;true;false;false]]); b1]
    393393          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    394       | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     394      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    395395         let b1 ≝
    396396          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
    … …  
    419419      ].
    420420
    421 ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝
    422     λmap: BitVectorTrie (BitVector eight) eight.
     421ndefinition address_of: BitVectorTrie (BitVector 8) 8 → String → addressing_mode ≝
     422    λmap: BitVectorTrie (BitVector 8) 8.
    423423    λstring: String.
    424424      let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in
    425425      let address_bv ≝ nat_of_bitvector ? address in
    426         if less_than_b address_bv two_hundred_and_fifty_six then
     426        if leb address_bv 256 then
    427427          RELATIVE address
    428428        else
    … …  
    431431nqed.
    432432
    433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly: assembly_program → option (list Byte × (BitVectorTrie String 16)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
    436436    let 〈datalabels, ignore〉 ≝
    437       fold_left ((BitVectorTrie (BitVector sixteen) sixteen) × Nat) ? (
     437      foldl ((BitVectorTrie (BitVector 16) 16) × nat) ? (
    438438        λt. λpreamble.
    439439          let 〈datalabels, addr〉 ≝ t in
    440440          let 〈name, size〉 ≝ preamble in
    441           let addr_sixteen ≝ bitvector_of_nat sixteen addr in
     441          let addr_sixteen ≝ bitvector_of_nat 16 addr in
    442442            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
    443               〈(Stub ? ?), Z〉 preamble in
     443              〈(Stub ? ?), O〉 preamble in
    444444    let 〈pc_labels, costs〉 ≝
    445       fold_left ((Nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (
     445      foldl ((nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (
    446446        λt. λi.
    447447          let 〈pc_labels, costs〉 ≝ t in
    … …  
    450450              [ Instruction instr ⇒
    451451                let code_memory ≝ load_code_memory (assembly1 instr) in
    452                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
     452                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    453453                let 〈instr', program_counter'〉 ≝ instr_pc' in
    454454                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
    … …  
    456456              | Label label ⇒
    457457                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    458                   〈〈program_counter, (insert ? ? (bitvector_of_string eight label) program_counter_bv labels)〉, costs〉
     458                  〈〈program_counter, (insert ? ? (bitvector_of_string 8 label) program_counter_bv labels)〉, costs〉
    459459              | Cost cost ⇒
    460460                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    461461                  〈pc_labels, (insert ? ? program_counter_bv cost costs)〉
    462462              | Jmp jmp ⇒
    463                   〈〈program_counter + three, labels〉, costs〉
     463                  〈〈program_counter + 3, labels〉, costs〉
    464464              | Call call ⇒
    465                   〈〈program_counter + three, labels〉, costs〉
     465                  〈〈program_counter + 3, labels〉, costs〉
    466466              | Mov dptr trgt ⇒ t
    467467              | WithLabel jmp ⇒
    468                 let fake_addr ≝ RELATIVE (zero eight) in
     468                let fake_addr ≝ RELATIVE (zero 8) in
    469469                let fake_jump ≝ assembly_jump jmp (λx: String. fake_addr) in
    470470                let code_memory ≝ load_code_memory (assembly1 fake_jump) in
    471                 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
     471                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
    472472                let 〈instr', program_counter'〉 ≝ instr_pc' in
    473                 let program_counter_n' ≝ nat_of_bitvector sixteen program_counter' in
     473                let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in
    474474                  〈〈program_counter + program_counter_n', labels〉, costs〉
    475475              ]
    476           ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
     476          ) 〈〈O, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
    477477    let 〈program_counter, labels〉 ≝ pc_labels in
    478       if greater_than_b program_counter
    479                         sixty_five_thousand_five_hundred_and_thirty_six then
    480         Nothing ?
     478      if gtb program_counter (2^16) then
     479        None ?
    481480      else
    482481        let flat_list ≝
    … …  
    489488                  | Call call ⇒
    490489                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
    491                     let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     490                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
    492491                    let address ≝ ADDR16 pc_offset_pad in
    493492                      assembly1 (LCALL ? address)
    … …  
    495494                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
    496495                    let address ≝ DATA16 pc_offset in
    497                       assembly1 (MOV ? (Left ? ? (Left ? ? (Right ? ? 〈DPTR, address〉))))
     496                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
    498497                  | Instruction instr ⇒ assembly1 instr
    499498                  | Jmp jmp ⇒
    500499                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
    501                     let pc_offset_pad ≝ (zero eight) @@ pc_offset in
     500                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
    502501                    let address ≝ ADDR16 pc_offset_pad in
    503502                      assembly1 (LJMP ? address)
    … …  
    507506            ) instr_list
    508507          ) in
    509         Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
     508        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
    510509  ##[##2,3,4,5,6: nnormalize; @;
    511510  ##| nwhd in ⊢ (? (? ? ? %));
    512       ncases (less_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)
     511      ncases (leb (nat_of_bitvector 8 ?) 256)
    513512        [ nnormalize; @;
    514513      ##| nnormalize;
    … …  
    518517nqed.
    519518
    520 ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    521  λp.Just ? (〈fold_right ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
     519ndefinition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie String 16)) ≝
     520 λp.Some ? (〈foldr ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).

  • Deliverables/D4.1/Matita/BitVector.ma

    r462 r465  
    22(* BitVector.ma: Fixed length bitvectors, and common operations on them.      *)
    33(*               Most functions are specialised versions of those found in    *)
    4 (*               Vector.ma as a courtesy, or Boolean functions lifted into    *)
     4(*               Vector.ma as a courtesy, or boolean functions lifted into    *)
    55(*               BitVector variants.                                          *)
    66(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    77
     8include "arithmetics/nat.ma".
     9
     10include "Util.ma".
    811include "Vector.ma".
    912include "String.ma".
    … …  
    1316(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1417
    15 ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    16 ndefinition Bit ≝ Bool.
    17 ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).
    18 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).
    19 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).
    20 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).
    21 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).
     18ndefinition BitVector ≝ λn: nat. Vector bool n.
     19ndefinition Bit ≝ bool.
     20ndefinition Nibble ≝ BitVector (S (S (S (S O)))).
     21ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S O))))))).
     22ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S O)))))))).
     23ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).
     24ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S O))))))))))).
    2225
    2326(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    2730(*
    2831ndefinition get_index_bv ≝
    29   λn: Nat.
    30   λb: BitVector n.
    31   λm: Nat.
     32  λn: nat.
     33  λb: BitVector n.
     34  λm: nat.
    3235  λp: m < n.
    33     get_index_bv Bool n b m p.
     36    get_index_bv bool n b m p.
    3437   
    3538interpretation "BitVector get_index" 'get_index b n = (get_index ? b n).
    3639   
    3740ndefinition set_index_bv ≝
    38   λn: Nat.
    39   λb: BitVector n.
    40   λm: Nat.
     41  λn: nat.
     42  λb: BitVector n.
     43  λm: nat.
    4144  λp: m < n.
    42   λc: Bool.
    43     set_index Bool n b m c.
     45  λc: bool.
     46    set_index bool n b m c.
    4447   
    4548ndefinition drop ≝
    46   λn: Nat.
    47   λb: BitVector n.
    48   λm: Nat.
    49     drop Bool n b m.
     49  λn: nat.
     50  λb: BitVector n.
     51  λm: nat.
     52    drop bool n b m.
    5053*)
    5154
    … …  
    5457(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    5558
    56 ndefinition zero: ∀n:Nat. BitVector n ≝
    57   λn: Nat. replicate Bool n false.
    58    
    59 ndefinition max: ∀n:Nat. BitVector n ≝
    60   λn: Nat. replicate Bool n true.
     59ndefinition zero: ∀n:nat. BitVector n ≝
     60  λn: nat. replicate bool n false.
     61   
     62ndefinition max: ∀n:nat. BitVector n ≝
     63  λn: nat. replicate bool n true.
    6164
    6265(*
    6366ndefinition append ≝
    64   λm, n: Nat.
     67  λm, n: nat.
    6568  λb: BitVector m.
    6669  λc: BitVector n.
    67     append Bool m n b c.
     70    append bool m n b c.
    6871*)
    6972 
    7073ndefinition pad ≝
    71   λm, n: Nat.
    72   λb: BitVector n.
    73     let padding ≝ replicate Bool m false in
    74       append Bool m n padding b.
     74  λm, n: nat.
     75  λb: BitVector n.
     76    let padding ≝ replicate bool m false in
     77      append bool m n padding b.
    7578     
    7679(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    8083(*
    8184ndefinition reverse ≝
    82   λn: Nat.
    83   λb: BitVector n.
    84     reverse Bool n b.
     85  λn: nat.
     86  λb: BitVector n.
     87    reverse bool n b.
    8588
    8689ndefinition length ≝
    87   λn: Nat.
    88   λb: BitVector n.
    89     length Bool n b.
     90  λn: nat.
     91  λb: BitVector n.
     92    length bool n b.
    9093*)
    9194
    … …  
    9497(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9598   
    96 ndefinition conjunction_bv ≝
    97   λn: Nat.
    98   λb: BitVector n.
    99   λc: BitVector n.
    100     zip_with Bool Bool Bool n conjunction b c.
    101    
    102 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).
     99ndefinition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝
     100  λn: nat.
     101  λb: BitVector n.
     102  λc: BitVector n.
     103    zip_with ? ? ? n (andb) b c.
     104   
     105interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c).
    103106   
    104107ndefinition inclusive_disjunction_bv ≝
    105   λn: Nat.
    106   λb: BitVector n.
    107   λc: BitVector n.
    108     zip_with Bool Bool Bool n inclusive_disjunction b c.
     108  λn: nat.
     109  λb: BitVector n.
     110  λc: BitVector n.
     111    zip_with ? ? ? n (orb) b c.
    109112   
    110113interpretation "BitVector inclusive disjunction"
    111   'inclusive_disjunction b c = (inclusive_disjunction ? b c).
     114  'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c).
    112115         
    113116ndefinition exclusive_disjunction_bv ≝
    114   λn: Nat.
    115   λb: BitVector n.
    116   λc: BitVector n.
    117     zip_with Bool Bool Bool n exclusive_disjunction b c.
     117  λn: nat.
     118  λb: BitVector n.
     119  λc: BitVector n.
     120    zip_with ? ? ? n (exclusive_disjunction) b c.
    118121   
    119122interpretation "BitVector exclusive disjunction"
    … …  
    121124   
    122125ndefinition negation_bv ≝
    123   λn: Nat.
    124   λb: BitVector n.
    125     map Bool Bool n (negation) b.
    126    
    127 interpretation "BitVector negation" 'negation b c = (negation ? b c).
     126  λn: nat.
     127  λb: BitVector n.
     128    map bool bool n (notb) b.
     129   
     130interpretation "BitVector negation" 'negation b c = (negation_bv ? b c).
    128131
    129132(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    133136(*
    134137ndefinition rotate_left_bv ≝
    135   λn, m: Nat.
    136   λb: BitVector n.
    137     rotate_left Bool n m b.
     138  λn, m: nat.
     139  λb: BitVector n.
     140    rotate_left bool n m b.
    138141
    139142ndefinition rotate_right_bv ≝
    140   λn, m: Nat.
    141   λb: BitVector n.
    142     rotate_right Bool n m b.
     143  λn, m: nat.
     144  λb: BitVector n.
     145    rotate_right bool n m b.
    143146   
    144147ndefinition shift_left_bv ≝
    145   λn, m: Nat.
    146   λb: BitVector n.
    147   λc: Bool.
    148     shift_left Bool n m b c.
     148  λn, m: nat.
     149  λb: BitVector n.
     150  λc: bool.
     151    shift_left bool n m b c.
    149152   
    150153ndefinition shift_right_bv ≝
    151   λn, m: Nat.
    152   λb: BitVector n.
    153   λc: Bool.
    154     shift_right Bool n m b c.
     154  λn, m: nat.
     155  λb: BitVector n.
     156  λc: bool.
     157    shift_right bool n m b c.
    155158*)
    156159 
    … …  
    161164(*
    162165ndefinition list_of_bitvector ≝
    163   λn: Nat.
    164   λb: BitVector n.
    165     list_of_vector Bool n b.
     166  λn: nat.
     167  λb: BitVector n.
     168    list_of_vector bool n b.
    166169   
    167170ndefinition bitvector_of_list ≝
    168   λl: List Bool.
    169     vector_of_list Bool l.
    170 *)
    171 
    172 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
     171  λl: List bool.
     172    vector_of_list bool l.
     173*)
     174
     175nlet rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝
    173176 match bound with
    174   [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
    175   | S bound ⇒
    176     let divrem ≝ divide_with_remainder n (S (S Z)) in
    177     let div ≝ first Nat Nat divrem in
    178     let rem ≝ second Nat Nat divrem in
     177  [ O ⇒ [ ] (* IT WILL NOT HAPPEN *)
     178  | S bound' ⇒
     179    let divrem ≝ divide_with_remainder n (S (S O)) in
     180    let div ≝ fst nat nat divrem in
     181    let rem ≝ snd nat nat divrem in
    179182      match div with
    180         [ Z ⇒
     183        [ O ⇒
    181184          match rem with
    182             [ Z ⇒ Empty Bool
    183             | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
     185            [ O ⇒ [ ]
     186            | S r ⇒ true :: (bitvector_of_nat_aux O bound')
    184187            ]
    185188        | S d ⇒
    186189          match rem with
    187             [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
    188             | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
     190            [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound')
     191            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound')
    189192            ]
    190193        ]].
    191194
    192195ndefinition eq_bv ≝
    193   λn: Nat.
     196  λn: nat.
    194197  λb, c: BitVector n.
    195     eq_v Bool n (λd, e.
    196       if inclusive_disjunction (conjunction d e) (conjunction (negation d)
    197                                                               (negation e)) then
     198    eq_v bool n (λd, e.
     199      if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
    198200        true
    199201      else
    200202        false) b c.
    201203
    202 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
    203   let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
     204nlet rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝
     205  let biglist ≝ rev ? (bitvector_of_nat_aux m m) in
    204206  let size ≝ length ? biglist in
    205207  let bitvector ≝ vector_of_list ? biglist in
    … …  
    208210    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
    209211    (λH:¬(size ≤ n). max n).
    210  nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
     212    nrewrite < plus_minus_m_m; //; nassumption;
    211213nqed.
    212214
    213 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
     215nlet rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝
    214216  match b with
    215     [ VEmpty ⇒ Z
     217    [ VEmpty ⇒ O
    216218    | VCons o hd tl ⇒
    217       let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
    218         ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
     219      let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in
     220        plus ((2^o) * hdval) (nat_of_bitvector o tl)
    219221    ].
    220222   
    221223naxiom bitvector_of_string:
    222   ∀n: Nat.
     224  ∀n: nat.
    223225  ∀s: String.
    224226    BitVector n.
    225227   
    226228naxiom string_of_bitvector:
    227   ∀n: Nat.
     229  ∀n: nat.
    228230  ∀b: BitVector n.
    229231    String.

  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r464 r465  
    11include "BitVector.ma".
    2 include "Bool.ma".
    3 include "Maybe.ma".
    42
    5 ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝
    6   Leaf: A → BitVectorTrie A Z
    7 | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    8 | Stub: ∀n: Nat. BitVectorTrie A n.
     3include "basics/bool.ma".
     4include "datatypes/sums.ma".
    95
    10 nlet rec lookup (A: Type[0]) (n: Nat)
     6ninductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
     7  Leaf: A → BitVectorTrie A O
     8| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
     9| Stub: ∀n: nat. BitVectorTrie A n.
     10
     11nlet rec lookup (A: Type[0]) (n: nat)
    1112                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
    1213       : A ≝
    1314  (match b return λx.λ_. x = n → A with
    1415    [ VEmpty ⇒
    15       (match t return λx.λ_. Z = x → A with
     16      (match t return λx.λ_. O = x → A with
    1617        [ Leaf l ⇒ λ_.l
    1718        | Node h l r ⇒ λK.⊥
    … …  
    2829        | Stub s ⇒ λ_. a]
    2930    ]) (refl ? n).
    30  ##[##1,2: ndestruct |##*: napply S_inj; //]
     31 ##[##1,2: ndestruct |##*: napply injective_S; //]
    3132nqed.
    3233
    33 nlet rec prepare_trie_for_insertion (A: Type[0]) (n: Nat)
     34nlet rec prepare_trie_for_insertion (A: Type[0]) (n: nat)
    3435                                    (b: BitVector n) (a:A) on b
    3536       : BitVectorTrie A n ≝
    … …  
    4344    ].
    4445
    45 nlet rec insert (A: Type[0]) (n: Nat)
     46nlet rec insert (A: Type[0]) (n: nat)
    4647                (b: BitVector n) (a: A) on b:
    4748                 BitVectorTrie A n → BitVectorTrie A n ≝
    … …  
    6061    ]).
    6162    ##[ ndestruct;
    62     ##|##*: napply S_inj; // ]
     63    ##|##*: napply injective_S; // ]
    6364nqed.
    6465
    … …  
    6667nlemma insert_lookup_stub:
    6768  ∀A: Type[0].
    68   ∀n: Nat.
     69  ∀n: nat.
    6970  ∀b: BitVector n.
    7071  ∀t: BitVectorTrie A n.
    … …  
    8182(*
    8283nlemma test:
    83   ∀n: Nat.
     84  ∀n: nat.
    8485  ∀b: BitVector n.
    8586    length n b = n.
    … …  
    9293nlemma insert_lookup_leaf:
    9394  ∀A: Type[0].
    94   ∀n: Nat.
     95  ∀n: nat.
    9596  ∀b: BitVector n.
    9697  ∀a, c: A.

  • Deliverables/D4.1/Matita/DoTest.ma

    r463 r465  
    88ndefinition teststatus ≝
    99 match testmem with
    10   [ Nothing ⇒ Nothing …
    11   | Just testmem ⇒ Just … (load (first … testmem) initialise_status)].
     10  [ None ⇒ None …
     11  | Some testmem ⇒ Some … (load (first … testmem) initialise_status)].
    1212ndefinition testfinal ≝
    1313 match teststatus with
    14   [ Nothing ⇒ Nothing …
    15   | Just teststatus ⇒ Just … (execute steps teststatus)].
     14  [ None ⇒ None …
     15  | Some teststatus ⇒ Some … (execute steps teststatus)].
    1616
    1717notation "'STATUS' pc sfr" with precedence 90 for @{ 'status $pc $sfr }.
    1818interpretation "status" 'status pc sfr = (mk_Status ? ? ? ? pc sfr ? ? ? ?).
    1919
    20 nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝
     20nlet rec execute_trace (n: nat) (s: Status) on n: list ? ≝
    2121  match n with
    22     [ Z ⇒ []
     22    [ O ⇒ []
    2323    | S o ⇒
    2424       first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
    … …  
    2727ndefinition testtrace ≝
    2828 match teststatus with
    29   [ Nothing ⇒ Nothing …
    30   | Just teststatus ⇒ Just … (execute_trace steps teststatus)].
    31 
    32 interpretation "left" 'left x = (Left ?? x).
    33 interpretation "right" 'right x = (Right ?? x).
     29  [ None ⇒ None …
     30  | Some teststatus ⇒ Some … (execute_trace steps teststatus)].
     31
     32interpretation "left" 'left x = (inl ?? x).
     33interpretation "right" 'right x = (inr ?? x).
    3434
    3535notation < "'L' x" with precedence 70 for @{ 'left $x }.
    … …  
    144144ndefinition dbg ≝
    145145  match teststatus with
    146     [ Nothing ⇒ Nothing ?
    147     | Just s ⇒
     146    [ None ⇒ None ?
     147    | Some s ⇒
    148148      let lk ≝ lookup ? seven ([[ false; false; false ]] @@ (max four)) (low_internal_ram s) (zero ?) in
    149         Just … 〈lk, program_counter s〉
     149        Some … 〈lk, program_counter s〉
    150150    ].
    151151   
    … …  
    167167ndefinition instr ≝
    168168  match teststatus with
    169     [ Nothing ⇒ Nothing …   
    170     | Just teststatus ⇒
    171         Just … (fetch (code_memory teststatus) (bitvector_of_nat ? (two_hundred_and_fifty_six + thirty_two + twenty_four)))
     169    [ None ⇒ None …   
     170    | Some teststatus ⇒
     171        Some … (fetch (code_memory teststatus) (bitvector_of_nat ? (two_hundred_and_fifty_six + thirty_two + twenty_four)))
    172172    ].
    173173
    174174ndefinition ftchtst ≝
    175175  match testfinal with
    176     [ Nothing ⇒ Nothing …
    177     | Just teststatus ⇒ Just … (next (code_memory teststatus) (program_counter teststatus))
     176    [ None ⇒ None …
     177    | Some teststatus ⇒ Some … (next (code_memory teststatus) (program_counter teststatus))
    178178    ].
    179179

  • Deliverables/D4.1/Matita/Fetch.ma

    r332 r465  
    33include "ASM.ma".
    44
    5 ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝
     5ndefinition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝
    66 λpmem,pc.
    7   let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in
    8    〈res, lookup … pc pmem (zero eight)〉.
     7  let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in
     8   〈res, lookup … pc pmem (zero 8)〉.
    99
    1010(* timings taken from SIEMENS *)
    1111
    12 ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝
     12ndefinition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝
    1313 λpmem,pc.
    1414  let 〈pc,v〉 ≝ next pmem pc in
    … …  
    1818      let 〈b,v〉≝  head … v in if b then
    1919       let 〈b,v〉≝  head … v in if b then
    20         〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,ACC_A〉))))), pc〉, one〉
    21        else
    22         let 〈b,v〉≝  head … v in if b then
    23          let 〈b,v〉≝  head … v in if b then
    24           〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, one〉
    25          else
    26           let 〈b,v〉≝  head … v in if b then
    27            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,ACC_A〉)))), pc〉, one〉
    28           else
    29            〈〈CPL … ACC_A, pc〉, one〉
    30         else
    31          let 〈b,v〉≝  head … v in if b then
    32           〈〈MOVX … (Right … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, two〉
    33          else
    34           let 〈b,v〉≝  head … v in if b then
    35            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
    36           else
    37            〈〈MOVX … (Right … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, two〉
    38       else
    39        let 〈b,v〉≝  head … v in if b then
    40         〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉))))), pc〉, one〉
    41        else
    42         let 〈b,v〉≝  head … v in if b then
    43          let 〈b,v〉≝  head … v in if b then
    44           〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, one〉
    45          else
    46           let 〈b,v〉≝  head … v in if b then
    47            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DIRECT b1〉))))), pc〉, one〉
    48           else
    49            〈〈CLR … ACC_A, pc〉, one〉
    50         else
    51          let 〈b,v〉≝  head … v in if b then
    52           〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, two〉
    53          else
    54           let 〈b,v〉≝  head … v in if b then
    55            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
    56           else
    57            〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, two〉
     20        〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉
     21       else
     22        let 〈b,v〉≝  head … v in if b then
     23         let 〈b,v〉≝  head … v in if b then
     24          〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉
     25         else
     26          let 〈b,v〉≝  head … v in if b then
     27           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉
     28          else
     29           〈〈CPL … ACC_A, pc〉, 1〉
     30        else
     31         let 〈b,v〉≝  head … v in if b then
     32          〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉
     33         else
     34          let 〈b,v〉≝  head … v in if b then
     35           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     36          else
     37           〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉
     38      else
     39       let 〈b,v〉≝  head … v in if b then
     40        〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉
     41       else
     42        let 〈b,v〉≝  head … v in if b then
     43         let 〈b,v〉≝  head … v in if b then
     44          〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉
     45         else
     46          let 〈b,v〉≝  head … v in if b then
     47           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉
     48          else
     49           〈〈CLR … ACC_A, pc〉, 1〉
     50        else
     51         let 〈b,v〉≝  head … v in if b then
     52          〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉
     53         else
     54          let 〈b,v〉≝  head … v in if b then
     55           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     56          else
     57           〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉
    5858     else
    5959      let 〈b,v〉≝  head … v in if b then
    6060       let 〈b,v〉≝  head … v in if b then
    61         let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉
    62        else
    63         let 〈b,v〉≝  head … v in if b then
    64          let 〈b,v〉≝  head … v in if b then
    65           〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    66          else
    67           let 〈b,v〉≝  head … v in if b then
    68            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉
    69           else
    70            〈〈DA … ACC_A, pc〉, one〉
    71         else
    72          let 〈b,v〉≝  head … v in if b then
    73           let 〈b,v〉≝  head … v in if b then
    74            〈〈SETB … CARRY, pc〉, one〉
    75           else
    76            let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉
    77          else
    78           let 〈b,v〉≝  head … v in if b then
    79            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉
    80           else
    81            let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, two〉
    82       else
    83        let 〈b,v〉≝  head … v in if b then
    84         〈〈XCH … ACC_A (REGISTER v), pc〉, one〉
    85        else
    86         let 〈b,v〉≝  head … v in if b then
    87          let 〈b,v〉≝  head … v in if b then
    88           〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    89          else
    90           let 〈b,v〉≝  head … v in if b then
    91            let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, one〉
    92           else
    93            〈〈SWAP … ACC_A, pc〉, one〉
    94         else
    95          let 〈b,v〉≝  head … v in if b then
    96           let 〈b,v〉≝  head … v in if b then
    97            〈〈CLR … CARRY, pc〉, one〉
    98           else
    99            let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉
    100          else
    101           let 〈b,v〉≝  head … v in if b then
    102            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉
    103           else
    104            let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, two〉
     61        let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     62       else
     63        let 〈b,v〉≝  head … v in if b then
     64         let 〈b,v〉≝  head … v in if b then
     65          〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
     66         else
     67          let 〈b,v〉≝  head … v in if b then
     68           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     69          else
     70           〈〈DA … ACC_A, pc〉, 1〉
     71        else
     72         let 〈b,v〉≝  head … v in if b then
     73          let 〈b,v〉≝  head … v in if b then
     74           〈〈SETB … CARRY, pc〉, 1〉
     75          else
     76           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉
     77         else
     78          let 〈b,v〉≝  head … v in if b then
     79           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     80          else
     81           let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉
     82      else
     83       let 〈b,v〉≝  head … v in if b then
     84        〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉
     85       else
     86        let 〈b,v〉≝  head … v in if b then
     87         let 〈b,v〉≝  head … v in if b then
     88          〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
     89         else
     90          let 〈b,v〉≝  head … v in if b then
     91           let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉
     92          else
     93           〈〈SWAP … ACC_A, pc〉, 1〉
     94        else
     95         let 〈b,v〉≝  head … v in if b then
     96          let 〈b,v〉≝  head … v in if b then
     97           〈〈CLR … CARRY, pc〉, 1〉
     98          else
     99           let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉
     100         else
     101          let 〈b,v〉≝  head … v in if b then
     102           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     103          else
     104           let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉
    105105    else
    106106     let 〈b,v〉≝  head … v in if b then
    107107      let 〈b,v〉≝  head … v in if b then
    108108       let 〈b,v〉≝  head … v in if b then
    109         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (Right … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, two〉
    110        else
    111         let 〈b,v〉≝  head … v in if b then
    112          let 〈b,v〉≝  head … v in if b then
    113           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Right … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, two〉
    114          else
    115           let 〈b,v〉≝  head … v in if b then
    116            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (Left … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, two〉
    117           else
    118            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Left … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, two〉
    119         else
    120          let 〈b,v〉≝  head … v in if b then
    121           let 〈b,v〉≝  head … v in if b then
    122            〈〈CPL … CARRY, pc〉, one〉
    123           else
    124            let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉
    125          else
    126           let 〈b,v〉≝  head … v in if b then
    127            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
    128           else
    129            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉
    130       else
    131        let 〈b,v〉≝  head … v in if b then
    132         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DIRECT b1〉))))), pc〉, two〉
    133        else
    134         let 〈b,v〉≝  head … v in if b then
    135          let 〈b,v〉≝  head … v in if b then
    136           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, two〉
    137          else
    138           〈〈MUL … ACC_A ACC_B, pc〉, four〉
    139         else
    140          let 〈b,v〉≝  head … v in if b then
    141           let 〈b,v〉≝  head … v in if b then
    142            〈〈INC … DPTR, pc〉, two〉
    143           else
    144            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Right … 〈CARRY,BIT_ADDR b1〉)), pc〉, one〉
    145          else
    146           let 〈b,v〉≝  head … v in if b then
    147            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
    148           else
    149            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉
     109        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     110       else
     111        let 〈b,v〉≝  head … v in if b then
     112         let 〈b,v〉≝  head … v in if b then
     113          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     114         else
     115          let 〈b,v〉≝  head … v in if b then
     116           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     117          else
     118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     119        else
     120         let 〈b,v〉≝  head … v in if b then
     121          let 〈b,v〉≝  head … v in if b then
     122           〈〈CPL … CARRY, pc〉, 1〉
     123          else
     124           let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉
     125         else
     126          let 〈b,v〉≝  head … v in if b then
     127           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     128          else
     129           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
     130      else
     131       let 〈b,v〉≝  head … v in if b then
     132        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉
     133       else
     134        let 〈b,v〉≝  head … v in if b then
     135         let 〈b,v〉≝  head … v in if b then
     136          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉
     137         else
     138          〈〈MUL … ACC_A ACC_B, pc〉, 4〉
     139        else
     140         let 〈b,v〉≝  head … v in if b then
     141          let 〈b,v〉≝  head … v in if b then
     142           〈〈INC … DPTR, pc〉, 2〉
     143          else
     144           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉
     145         else
     146          let 〈b,v〉≝  head … v in if b then
     147           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     148          else
     149           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
    150150     else
    151151      let 〈b,v〉≝  head … v in if b then
    152152       let 〈b,v〉≝  head … v in if b then
    153         〈〈SUBB … ACC_A (REGISTER v), pc〉, one〉
    154        else
    155         let 〈b,v〉≝  head … v in if b then
    156          let 〈b,v〉≝  head … v in if b then
    157           〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    158          else
    159           let 〈b,v〉≝  head … v in if b then
    160            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, one〉
    161           else
    162            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉
    163         else
    164          let 〈b,v〉≝  head … v in if b then
    165           let 〈b,v〉≝  head … v in if b then
    166            〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉
    167           else
    168            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Right … 〈BIT_ADDR b1,CARRY〉), pc〉, two〉
    169          else
    170           let 〈b,v〉≝  head … v in if b then
    171            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉
    172           else
    173            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Right … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, two〉
    174       else
    175        let 〈b,v〉≝  head … v in if b then
    176         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,REGISTER v〉)))), pc〉, two〉
    177        else
    178         let 〈b,v〉≝  head … v in if b then
    179          let 〈b,v〉≝  head … v in if b then
    180           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, two〉
    181          else
    182           let 〈b,v〉≝  head … v in if b then
    183            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DIRECT b2〉)))), pc〉, two〉
    184           else
    185            〈〈DIV … ACC_A ACC_B, pc〉, four〉
    186         else
    187          let 〈b,v〉≝  head … v in if b then
    188           let 〈b,v〉≝  head … v in if b then
    189            〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉
    190           else
    191            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉
    192          else
    193           let 〈b,v〉≝  head … v in if b then
    194            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉
    195           else
    196            let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉
     153        〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉
     154       else
     155        let 〈b,v〉≝  head … v in if b then
     156         let 〈b,v〉≝  head … v in if b then
     157          〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
     158         else
     159          let 〈b,v〉≝  head … v in if b then
     160           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉
     161          else
     162           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉
     163        else
     164         let 〈b,v〉≝  head … v in if b then
     165          let 〈b,v〉≝  head … v in if b then
     166           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
     167          else
     168           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉
     169         else
     170          let 〈b,v〉≝  head … v in if b then
     171           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     172          else
     173           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉
     174      else
     175       let 〈b,v〉≝  head … v in if b then
     176        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉
     177       else
     178        let 〈b,v〉≝  head … v in if b then
     179         let 〈b,v〉≝  head … v in if b then
     180          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉
     181         else
     182          let 〈b,v〉≝  head … v in if b then
     183           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉
     184          else
     185           〈〈DIV … ACC_A ACC_B, pc〉, 4〉
     186        else
     187         let 〈b,v〉≝  head … v in if b then
     188          let 〈b,v〉≝  head … v in if b then
     189           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
     190          else
     191           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     192         else
     193          let 〈b,v〉≝  head … v in if b then
     194           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     195          else
     196           let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
    197197   else
    198198    let 〈b,v〉≝  head … v in if b then
    … …  
    200200      let 〈b,v〉≝  head … v in if b then
    201201       let 〈b,v〉≝  head … v in if b then
    202         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DATA b1〉))))), pc〉, one〉
    203        else
    204         let 〈b,v〉≝  head … v in if b then
    205          let 〈b,v〉≝  head … v in if b then
    206           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, one〉
    207          else
    208           let 〈b,v〉≝  head … v in if b then
    209            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DATA b2〉)))), pc〉, three〉
    210           else
    211            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DATA b1〉))))), pc〉, one〉
    212         else
    213          let 〈b,v〉≝  head … v in if b then
    214           let 〈b,v〉≝  head … v in if b then
    215            〈〈JMP … INDIRECT_DPTR, pc〉, two〉
    216           else
    217            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉
    218          else
    219           let 〈b,v〉≝  head … v in if b then
    220            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    221           else
    222            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, two〉
    223       else
    224        let 〈b,v〉≝  head … v in if b then
    225         〈〈XRL … (Left … 〈ACC_A,REGISTER v〉), pc〉, one〉
    226        else
    227         let 〈b,v〉≝  head … v in if b then
    228          let 〈b,v〉≝  head … v in if b then
    229           〈〈XRL … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, one〉
    230          else
    231           let 〈b,v〉≝  head … v in if b then
    232            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DIRECT b1〉), pc〉, one〉
    233           else
    234            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DATA b1〉), pc〉, one〉
    235         else
    236          let 〈b,v〉≝  head … v in if b then
    237           let 〈b,v〉≝  head … v in if b then
    238            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,DATA b2〉), pc〉, two〉
    239           else
    240            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,ACC_A〉), pc〉, one〉
    241          else
    242           let 〈b,v〉≝  head … v in if b then
    243            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    244           else
    245            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉
     202        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉
     203       else
     204        let 〈b,v〉≝  head … v in if b then
     205         let 〈b,v〉≝  head … v in if b then
     206          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉
     207         else
     208          let 〈b,v〉≝  head … v in if b then
     209           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉
     210          else
     211           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉
     212        else
     213         let 〈b,v〉≝  head … v in if b then
     214          let 〈b,v〉≝  head … v in if b then
     215           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
     216          else
     217           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     218         else
     219          let 〈b,v〉≝  head … v in if b then
     220           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     221          else
     222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉
     223      else
     224       let 〈b,v〉≝  head … v in if b then
     225        〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉
     226       else
     227        let 〈b,v〉≝  head … v in if b then
     228         let 〈b,v〉≝  head … v in if b then
     229          〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉
     230         else
     231          let 〈b,v〉≝  head … v in if b then
     232           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉
     233          else
     234           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉
     235        else
     236         let 〈b,v〉≝  head … v in if b then
     237          let 〈b,v〉≝  head … v in if b then
     238           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉
     239          else
     240           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉
     241         else
     242          let 〈b,v〉≝  head … v in if b then
     243           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     244          else
     245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉
    246246     else
    247247      let 〈b,v〉≝  head … v in if b then
    248248       let 〈b,v〉≝  head … v in if b then
    249         〈〈ANL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉
    250        else
    251         let 〈b,v〉≝  head … v in if b then
    252          let 〈b,v〉≝  head … v in if b then
    253           〈〈ANL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉
    254          else
    255           let 〈b,v〉≝  head … v in if b then
    256            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉
    257           else
    258            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉
    259         else
    260          let 〈b,v〉≝  head … v in if b then
    261           let 〈b,v〉≝  head … v in if b then
    262            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉
    263           else
    264            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉
    265          else
    266           let 〈b,v〉≝  head … v in if b then
    267            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    268           else
    269            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, two〉
    270       else
    271        let 〈b,v〉≝  head … v in if b then
    272         〈〈ORL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉
    273        else
    274         let 〈b,v〉≝  head … v in if b then
    275          let 〈b,v〉≝  head … v in if b then
    276           〈〈ORL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉
    277          else
    278           let 〈b,v〉≝  head … v in if b then
    279            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉
    280           else
    281            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉
    282         else
    283          let 〈b,v〉≝  head … v in if b then
    284           let 〈b,v〉≝  head … v in if b then
    285            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉
    286           else
    287            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉
    288          else
    289           let 〈b,v〉≝  head … v in if b then
    290            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    291           else
    292            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉
     249        〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
     250       else
     251        let 〈b,v〉≝  head … v in if b then
     252         let 〈b,v〉≝  head … v in if b then
     253          〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
     254         else
     255          let 〈b,v〉≝  head … v in if b then
     256           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     257          else
     258           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     259        else
     260         let 〈b,v〉≝  head … v in if b then
     261          let 〈b,v〉≝  head … v in if b then
     262           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     263          else
     264           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     265         else
     266          let 〈b,v〉≝  head … v in if b then
     267           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     268          else
     269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉
     270      else
     271       let 〈b,v〉≝  head … v in if b then
     272        〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
     273       else
     274        let 〈b,v〉≝  head … v in if b then
     275         let 〈b,v〉≝  head … v in if b then
     276          〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
     277         else
     278          let 〈b,v〉≝  head … v in if b then
     279           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     280          else
     281           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     282        else
     283         let 〈b,v〉≝  head … v in if b then
     284          let 〈b,v〉≝  head … v in if b then
     285           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     286          else
     287           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     288         else
     289          let 〈b,v〉≝  head … v in if b then
     290           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     291          else
     292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉
    293293    else
    294294     let 〈b,v〉≝  head … v in if b then
    295295      let 〈b,v〉≝  head … v in if b then
    296296       let 〈b,v〉≝  head … v in if b then
    297         〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉
    298        else
    299         let 〈b,v〉≝  head … v in if b then
    300          let 〈b,v〉≝  head … v in if b then
    301           〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    302          else
    303           let 〈b,v〉≝  head … v in if b then
    304            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, one〉
    305           else
    306            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉
    307         else
    308          let 〈b,v〉≝  head … v in if b then
    309           let 〈b,v〉≝  head … v in if b then
    310            〈〈RLC … ACC_A, pc〉, one〉
    311           else
    312            〈〈RETI …, pc〉, two〉
    313          else
    314           let 〈b,v〉≝  head … v in if b then
    315            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    316           else
    317            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    318       else
    319        let 〈b,v〉≝  head … v in if b then
    320         〈〈ADD … ACC_A (REGISTER v), pc〉, one〉
    321        else
    322         let 〈b,v〉≝  head … v in if b then
    323          let 〈b,v〉≝  head … v in if b then
    324           〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    325          else
    326           let 〈b,v〉≝  head … v in if b then
    327            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, one〉
    328           else
    329            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉
    330         else
    331          let 〈b,v〉≝  head … v in if b then
    332           let 〈b,v〉≝  head … v in if b then
    333            〈〈RL … ACC_A, pc〉, one〉
    334           else
    335            〈〈RET …, pc〉, two〉
    336          else
    337           let 〈b,v〉≝  head … v in if b then
    338            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    339           else
    340            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     297        〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉
     298       else
     299        let 〈b,v〉≝  head … v in if b then
     300         let 〈b,v〉≝  head … v in if b then
     301          〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
     302         else
     303          let 〈b,v〉≝  head … v in if b then
     304           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉
     305          else
     306           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉
     307        else
     308         let 〈b,v〉≝  head … v in if b then
     309          let 〈b,v〉≝  head … v in if b then
     310           〈〈RLC … ACC_A, pc〉, 1〉
     311          else
     312           〈〈RETI …, pc〉, 2〉
     313         else
     314          let 〈b,v〉≝  head … v in if b then
     315           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     316          else
     317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     318      else
     319       let 〈b,v〉≝  head … v in if b then
     320        〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉
     321       else
     322        let 〈b,v〉≝  head … v in if b then
     323         let 〈b,v〉≝  head … v in if b then
     324          〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
     325         else
     326          let 〈b,v〉≝  head … v in if b then
     327           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉
     328          else
     329           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉
     330        else
     331         let 〈b,v〉≝  head … v in if b then
     332          let 〈b,v〉≝  head … v in if b then
     333           〈〈RL … ACC_A, pc〉, 1〉
     334          else
     335           〈〈RET …, pc〉, 2〉
     336         else
     337          let 〈b,v〉≝  head … v in if b then
     338           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     339          else
     340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    341341     else
    342342      let 〈b,v〉≝  head … v in if b then
    343343       let 〈b,v〉≝  head … v in if b then
    344         〈〈DEC … (REGISTER v), pc〉, one〉
    345        else
    346         let 〈b,v〉≝  head … v in if b then
    347          let 〈b,v〉≝  head … v in if b then
    348           〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉
    349          else
    350           let 〈b,v〉≝  head … v in if b then
    351            let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, one〉
    352           else
    353            〈〈DEC … ACC_A, pc〉, one〉
    354         else
    355          let 〈b,v〉≝  head … v in if b then
    356           let 〈b,v〉≝  head … v in if b then
    357            〈〈RRC … ACC_A, pc〉, one〉
    358           else
    359            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉
    360          else
    361           let 〈b,v〉≝  head … v in if b then
    362            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
    363           else
    364            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    365       else
    366        let 〈b,v〉≝  head … v in if b then
    367         〈〈INC … (REGISTER v), pc〉, one〉
    368        else
    369         let 〈b,v〉≝  head … v in if b then
    370          let 〈b,v〉≝  head … v in if b then
    371           〈〈INC … (INDIRECT (from_singl … v)), pc〉, one〉
    372          else
    373           let 〈b,v〉≝  head … v in if b then
    374            let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, one〉
    375           else
    376            〈〈INC … ACC_A, pc〉, one〉
    377         else
    378          let 〈b,v〉≝  head … v in if b then
    379           let 〈b,v〉≝  head … v in if b then
    380            〈〈RR … ACC_A, pc〉, one〉
    381           else
    382            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉
    383          else
    384           let 〈b,v〉≝  head … v in if b then
    385            let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
    386           else
    387            〈〈NOP …, pc〉, one〉.
     344        〈〈DEC … (REGISTER v), pc〉, 1〉
     345       else
     346        let 〈b,v〉≝  head … v in if b then
     347         let 〈b,v〉≝  head … v in if b then
     348          〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉
     349         else
     350          let 〈b,v〉≝  head … v in if b then
     351           let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉
     352          else
     353           〈〈DEC … ACC_A, pc〉, 1〉
     354        else
     355         let 〈b,v〉≝  head … v in if b then
     356          let 〈b,v〉≝  head … v in if b then
     357           〈〈RRC … ACC_A, pc〉, 1〉
     358          else
     359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     360         else
     361          let 〈b,v〉≝  head … v in if b then
     362           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     363          else
     364           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     365      else
     366       let 〈b,v〉≝  head … v in if b then
     367        〈〈INC … (REGISTER v), pc〉, 1〉
     368       else
     369        let 〈b,v〉≝  head … v in if b then
     370         let 〈b,v〉≝  head … v in if b then
     371          〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉
     372         else
     373          let 〈b,v〉≝  head … v in if b then
     374           let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉
     375          else
     376           〈〈INC … ACC_A, pc〉, 1〉
     377        else
     378         let 〈b,v〉≝  head … v in if b then
     379          let 〈b,v〉≝  head … v in if b then
     380           〈〈RR … ACC_A, pc〉, 1〉
     381          else
     382           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     383         else
     384          let 〈b,v〉≝  head … v in if b then
     385           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     386          else
     387           〈〈NOP …, pc〉, 1〉.
    388388 @.
    389389nqed.

  • Deliverables/D4.1/Matita/Interpret.ma

    r439 r465  
    5353
    5454nlemma execute_1_technical:
    55   ∀n,m: Nat.
     55  ∀n,m: nat.
    5656  ∀v: Vector addressing_mode_tag (S n).
    5757  ∀q: Vector addressing_mode_tag (S m).
    … …  
    9494            let ov_flag ≝ get_index' ? two ? flags in
    9595            let s ≝ set_arg_8 s ACC_A result in
    96               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     96              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    9797        | ADDC addr1 addr2 ⇒
    9898            let old_cy_flag ≝ get_cy_flag s in
    … …  
    103103            let ov_flag ≝ get_index' ? two ? flags in
    104104            let s ≝ set_arg_8 s ACC_A result in
    105               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     105              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    106106        | SUBB addr1 addr2 ⇒
    107107            let old_cy_flag ≝ get_cy_flag s in
    … …  
    112112            let ov_flag ≝ get_index' ? two ? flags in
    113113            let s ≝ set_arg_8 s ACC_A result in
    114               set_flags s cy_flag (Just Bit ac_flag) ov_flag
     114              set_flags s cy_flag (Some Bit ac_flag) ov_flag
    115115        | ANL addr ⇒
    116116          match addr with
    117             [ Left l ⇒
     117            [ inl l ⇒
    118118              match l with
    119                 [ Left l' ⇒
     119                [ inl l' ⇒
    120120                  let 〈addr1, addr2〉 ≝ l' in
    121121                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    122122                    set_arg_8 s addr1 and_val
    123                 | Right r ⇒
     123                | right r ⇒
    124124                  let 〈addr1, addr2〉 ≝ r in
    125125                  let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    126126                    set_arg_8 s addr1 and_val
    127127                ]
    128             | Right r ⇒
     128            | right r ⇒
    129129              let 〈addr1, addr2〉 ≝ r in
    130130              let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
    131                 set_flags s and_val (Nothing ?) (get_ov_flag s)
     131                set_flags s and_val (None ?) (get_ov_flag s)
    132132            ]
    133133        | ORL addr ⇒
    134134          match addr with
    135             [ Left l ⇒
     135            [ inl l ⇒
    136136              match l with
    137                 [ Left l' ⇒
     137                [ inl l' ⇒
    138138                  let 〈addr1, addr2〉 ≝ l' in
    139139                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    140140                    set_arg_8 s addr1 or_val
    141                 | Right r ⇒
     141                | right r ⇒
    142142                  let 〈addr1, addr2〉 ≝ r in
    143143                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    144144                    set_arg_8 s addr1 or_val
    145145                ]
    146             | Right r ⇒
     146            | right r ⇒
    147147              let 〈addr1, addr2〉 ≝ r in
    148148              let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in
    149                 set_flags s or_val (Nothing ?) (get_ov_flag s)
     149                set_flags s or_val (None ?) (get_ov_flag s)
    150150            ]
    151151        | XRL addr ⇒
    152152          match addr with
    153             [ Left l' ⇒
     153            [ inl l' ⇒
    154154              let 〈addr1, addr2〉 ≝ l' in
    155155              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    156156                set_arg_8 s addr1 xor_val
    157             | Right r ⇒
     157            | right r ⇒
    158158              let 〈addr1, addr2〉 ≝ r in
    159159              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in
    … …  
    201201           let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in
    202202             match acc_b_nat with
    203                [ Z ⇒ set_flags s false (Nothing Bit) true
     203               [ Z ⇒ set_flags s false (None Bit) true
    204204               | S o ⇒
    205205                 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in
    … …  
    207207                 let s ≝ set_8051_sfr s SFR_ACC_A q in
    208208                 let s ≝ set_8051_sfr s SFR_ACC_B r in
    209                    set_flags s false (Nothing Bit) false
     209                   set_flags s false (None Bit) false
    210210               ]
    211211        | DA addr ⇒
    … …  
    219219                    let new_acc ≝ nu @@ acc_nl' in
    220220                    let s ≝ set_8051_sfr s SFR_ACC_A new_acc in
    221                       set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s)
     221                      set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s)
    222222                  else
    223223                    s
    … …  
    395395                [ RELATIVE r ⇒ λrelative: True.
    396396                  match addr1 with
    397                     [ Left l ⇒
     397                    [ inl l ⇒
    398398                        let 〈addr1, addr2〉 ≝ l in
    399399                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
    … …  
    402402                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    403403                            let s ≝ set_program_counter s new_pc in
    404                               set_flags s new_cy (Nothing ?) (get_ov_flag s)
     404                              set_flags s new_cy (None ?) (get_ov_flag s)
    405405                          else
    406                             (set_flags s new_cy (Nothing ?) (get_ov_flag s))
    407                     | Right r' ⇒
     406                            (set_flags s new_cy (None ?) (get_ov_flag s))
     407                    | right r' ⇒
    408408                        let 〈addr1, addr2〉 ≝ r' in
    409409                        let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1))
    … …  
    412412                            let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    413413                            let s ≝ set_program_counter s new_pc in
    414                               set_flags s new_cy (Nothing ?) (get_ov_flag s)
     414                              set_flags s new_cy (None ?) (get_ov_flag s)
    415415                          else
    416                             (set_flags s new_cy (Nothing ?) (get_ov_flag s))
     416                            (set_flags s new_cy (None ?) (get_ov_flag s))
    417417                    ]
    418418                | _ ⇒ λother: False. ⊥
    … …  
    484484          (* DPM: only copies --- doesn't affect I/O *)
    485485          match addr with
    486             [ Left l ⇒
     486            [ inl l ⇒
    487487              let 〈addr1, addr2〉 ≝ l in
    488488                set_arg_8 s addr1 (get_arg_8 s false addr2)
    489             | Right r ⇒
     489            | right r ⇒
    490490              let 〈addr1, addr2〉 ≝ r in
    491491                set_arg_8 s addr1 (get_arg_8 s false addr2)
    … …  
    493493        | MOV addr ⇒
    494494          match addr with
    495             [ Left l ⇒
     495            [ inl l ⇒
    496496              match l with
    497                 [ Left l' ⇒
     497                [ inl l' ⇒
    498498                  match l' with
    499                     [ Left l'' ⇒
     499                    [ inl l'' ⇒
    500500                      match l'' with
    501                         [ Left l''' ⇒
     501                        [ inl l''' ⇒
    502502                          match l''' with
    503                             [ Left l'''' ⇒
     503                            [ inl l'''' ⇒
    504504                              let 〈addr1, addr2〉 ≝ l'''' in
    505505                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    506                             | Right r'''' ⇒
     506                            | right r'''' ⇒
    507507                              let 〈addr1, addr2〉 ≝ r'''' in
    508508                                set_arg_8 s addr1 (get_arg_8 s false addr2)
    509509                            ]
    510                         | Right r''' ⇒
     510                        | right r''' ⇒
    511511                          let 〈addr1, addr2〉 ≝ r''' in
    512512                            set_arg_8 s addr1 (get_arg_8 s false addr2)
    513513                        ]
    514                     | Right r'' ⇒
     514                    | right r'' ⇒
    515515                      let 〈addr1, addr2〉 ≝ r'' in
    516516                        set_arg_16 s (get_arg_16 s addr2) addr1
    517517                    ]
    518                 | Right r ⇒
     518                | right r ⇒
    519519                  let 〈addr1, addr2〉 ≝ r in
    520520                    set_arg_1 s addr1 (get_arg_1 s addr2 false)
    521521                ]
    522             | Right r ⇒
     522            | right r ⇒
    523523              let 〈addr1, addr2〉 ≝ r in
    524524                set_arg_1 s addr1 (get_arg_1 s addr2 false)
    … …  
    573573nqed.
    574574
    575 nlet rec execute (n: Nat) (s: Status) on n: Status ≝
     575nlet rec execute (n: nat) (s: Status) on n: Status ≝
    576576  match n with
    577577    [ Z ⇒ s

  • Deliverables/D4.1/Matita/Status.ma

    r439 r465  
    77include "BitVectorTrie.ma".
    88
    9 ndefinition Time ≝ Nat.
     9ndefinition Time ≝ nat.
    1010
    1111ninductive SerialBufferType: Type[0] ≝
    … …  
    4444  λs: SFR8051.
    4545    match s with
    46       [ SFR_SP ⇒ Z
    47       | SFR_DPL ⇒ S Z
    48       | SFR_DPH ⇒ two
    49       | SFR_PCON ⇒ three
    50       | SFR_TCON ⇒ four
    51       | SFR_TMOD ⇒ five
    52       | SFR_TL0 ⇒ six
    53       | SFR_TL1 ⇒ seven
    54       | SFR_TH0 ⇒ eight
    55       | SFR_TH1 ⇒ nine
    56       | SFR_P1 ⇒ ten
    57       | SFR_SCON ⇒ eleven
    58       | SFR_SBUF ⇒ twelve
    59       | SFR_IE ⇒ thirteen
    60       | SFR_P3 ⇒ fourteen
    61       | SFR_IP ⇒ fifteen
    62       | SFR_PSW ⇒ sixteen
    63       | SFR_ACC_A ⇒ seventeen
    64       | SFR_ACC_B ⇒ eighteen
     46      [ SFR_SP ⇒ O
     47      | SFR_DPL ⇒ 1
     48      | SFR_DPH ⇒ 2
     49      | SFR_PCON ⇒ 3
     50      | SFR_TCON ⇒ 4
     51      | SFR_TMOD ⇒ 5
     52      | SFR_TL0 ⇒ 6
     53      | SFR_TL1 ⇒ 7
     54      | SFR_TH0 ⇒ 8
     55      | SFR_TH1 ⇒ 9
     56      | SFR_P1 ⇒ 10
     57      | SFR_SCON ⇒ 11
     58      | SFR_SBUF ⇒ 12
     59      | SFR_IE ⇒ 13
     60      | SFR_P3 ⇒ 14
     61      | SFR_IP ⇒ 15
     62      | SFR_PSW ⇒ 16
     63      | SFR_ACC_A ⇒ 17
     64      | SFR_ACC_B ⇒ 18
    6565      ].
    6666     
    … …  
    7575  λs: SFR8052.
    7676    match s with
    77       [ SFR_T2CON ⇒ Z
    78       | SFR_RCAP2L ⇒ S Z
    79       | SFR_RCAP2H ⇒ two
    80       | SFR_TL2 ⇒ three
    81       | SFR_TH2 ⇒ four
     77      [ SFR_T2CON ⇒ O
     78      | SFR_RCAP2L ⇒ 1
     79      | SFR_RCAP2H ⇒ 2
     80      | SFR_TL2 ⇒ 3
     81      | SFR_TH2 ⇒ 4
    8282      ].
    8383
    … …  
    8787nrecord Status: Type[0] ≝
    8888{
    89   code_memory: BitVectorTrie Byte sixteen;
    90   low_internal_ram: BitVectorTrie Byte seven;
    91   high_internal_ram: BitVectorTrie Byte seven;
    92   external_ram: BitVectorTrie Byte sixteen;
     89  code_memory: BitVectorTrie Byte 16;
     90  low_internal_ram: BitVectorTrie Byte 7;
     91  high_internal_ram: BitVectorTrie Byte 7;
     92  external_ram: BitVectorTrie Byte 16;
    9393 
    9494  program_counter: Word;
    9595 
    96   special_function_registers_8051: Vector Byte nineteen;
    97   special_function_registers_8052: Vector Byte five;
     96  special_function_registers_8051: Vector Byte 19;
     97  special_function_registers_8052: Vector Byte 5;
    9898 
    9999  p1_latch: Byte;
    … …  
    103103}.
    104104
    105 nlemma sfr8051_index_nineteen:
     105nlemma sfr8051_index_19:
    106106  ∀i: SFR8051.
    107     sfr_8051_index i < nineteen.
    108  #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
    109  napply less_than_or_equal_zero.
     107    sfr_8051_index i < 19.
     108 #i; ncases i; nnormalize; nrepeat (napply le_S_S);
     109 napply le_O_n.
    110110nqed.
    111111   
    112 nlemma sfr8052_index_five:
     112nlemma sfr8052_index_5:
    113113  ∀i: SFR8052.
    114     sfr_8052_index i < five.
    115  #i; ncases i; nnormalize; nrepeat (napply less_than_or_equal_monotone);
    116  napply less_than_or_equal_zero.
     114    sfr_8052_index i < 5.
     115 #i; ncases i; nnormalize; nrepeat (napply le_S_S);
     116 napply le_O_n.
    117117nqed.
    118118   
    … …  
    192192    let index ≝ sfr_8051_index i in
    193193      get_index_v … sfr index ?.
    194     napply sfr8051_index_nineteen.
     194    napply sfr8051_index_19.
    195195nqed.
    196196
    … …  
    201201    let index ≝ sfr_8052_index i in
    202202      get_index_v … sfr index ?.
    203     napply sfr8052_index_five.
     203    napply sfr8052_index_5.
    204204nqed.
    205205
    … …  
    217217    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    218218    let new_special_function_registers_8051 ≝
    219       set_index Byte nineteen old_special_function_registers_8051 index b ? in
     219      set_index Byte 19 old_special_function_registers_8051 index b ? in
    220220    let old_p1_latch ≝ p1_latch s in
    221221    let old_p3_latch ≝ p3_latch s in
    … …  
    231231                old_p3_latch
    232232                old_clock.
    233     napply (sfr8051_index_nineteen i).
     233    napply (sfr8051_index_19 i).
    234234nqed.
    235235
    … …  
    247247    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    248248    let new_special_function_registers_8052 ≝
    249       set_index Byte five old_special_function_registers_8052 index b ? in
     249      set_index Byte 5 old_special_function_registers_8052 index b ? in
    250250    let old_p1_latch ≝ p1_latch s in
    251251    let old_p3_latch ≝ p3_latch s in
    … …  
    261261                old_p3_latch
    262262                old_clock.
    263     napply (sfr8052_index_five i).
     263    napply (sfr8052_index_5 i).
    264264nqed.
    265265
    … …  
    289289ndefinition set_code_memory ≝
    290290  λs: Status.
    291   λr: BitVectorTrie Byte sixteen.
     291  λr: BitVectorTrie Byte 16.
    292292    let old_low_internal_ram ≝ low_internal_ram s in
    293293    let old_high_internal_ram ≝ high_internal_ram s in
    … …  
    312312ndefinition set_low_internal_ram ≝
    313313  λs: Status.
    314   λr: BitVectorTrie Byte seven.
     314  λr: BitVectorTrie Byte 7.
    315315    let old_code_memory ≝ code_memory s in
    316316    let old_high_internal_ram ≝ high_internal_ram s in
    … …  
    335335ndefinition set_high_internal_ram ≝
    336336  λs: Status.
    337   λr: BitVectorTrie Byte seven.
     337  λr: BitVectorTrie Byte 7.
    338338    let old_code_memory ≝ code_memory s in
    339339    let old_low_internal_ram ≝ low_internal_ram s in
    … …  
    359359ndefinition set_external_ram ≝
    360360  λs: Status.
    361   λr: BitVectorTrie Byte sixteen.
     361  λr: BitVectorTrie Byte 16.
    362362    let old_code_memory ≝ code_memory s in
    363363    let old_low_internal_ram ≝ low_internal_ram s in
    … …  
    383383  λs: Status.
    384384    let sfr ≝ special_function_registers_8051 s in
    385     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    386       get_index_v Bool eight psw Z ?.
    387     nnormalize.
    388     napply (less_than_or_equal_monotone ? ?).
    389     napply (less_than_or_equal_zero).
    390     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    391     napply (less_than_or_equal_zero).
     385    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     386      get_index_v bool 8 psw O ?.
     387    nnormalize;
     388    napply (le_S_S ? ?);
     389    ##[ napply le_O_n;
     390    ##| nrepeat (napply (le_S_S));
     391        //;
     392    ##]
    392393nqed.
    393394
    … …  
    395396  λs: Status.
    396397    let sfr ≝ special_function_registers_8051 s in
    397     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    398       get_index_v Bool eight psw (S Z) ?.
    399     nnormalize.
    400     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    401     napply (less_than_or_equal_zero).
    402     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    403     napply (less_than_or_equal_zero).
     398    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     399      get_index_v bool 8 psw (S O) ?.
     400    nnormalize;
     401    nrepeat (napply (le_S_S ? ?));
     402    napply le_O_n;
    404403nqed.
    405404
    … …  
    407406  λs: Status.
    408407    let sfr ≝ special_function_registers_8051 s in
    409     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    410       get_index_v Bool eight psw two ?.
    411     nnormalize.
    412     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    413     napply (less_than_or_equal_zero).
    414     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    415     napply (less_than_or_equal_zero).
     408    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     409      get_index_v bool 8 psw 2 ?.
     410    nnormalize;
     411    nrepeat (napply (le_S_S ? ?));
     412    napply le_O_n;
    416413nqed.
    417414
    … …  
    419416  λs: Status.
    420417    let sfr ≝ special_function_registers_8051 s in
    421     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    422       get_index_v Bool eight psw three ?.
    423     nnormalize.
    424     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    425     napply (less_than_or_equal_zero).
    426     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    427     napply (less_than_or_equal_zero).
     418    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     419      get_index_v bool 8 psw 3 ?.
     420    nnormalize;
     421    nrepeat (napply (le_S_S ? ?));
     422    napply le_O_n;
    428423nqed.
    429424
    … …  
    431426  λs: Status.
    432427    let sfr ≝ special_function_registers_8051 s in
    433     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    434       get_index_v Bool eight psw four ?.
    435     nnormalize.
    436     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    437     napply (less_than_or_equal_zero).
    438     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    439     napply (less_than_or_equal_zero).
     428    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     429      get_index_v bool 8 psw 4 ?.
     430    nnormalize;
     431    nrepeat (napply (le_S_S ? ?));
     432    napply le_O_n;
    440433nqed.
    441434
    … …  
    443436  λs: Status.
    444437    let sfr ≝ special_function_registers_8051 s in
    445     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    446       get_index_v Bool eight psw five ?.
    447     nnormalize.
    448     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    449     napply (less_than_or_equal_zero).
    450     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    451     napply (less_than_or_equal_zero).
     438    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     439      get_index_v bool 8 psw 5 ?.
     440    nnormalize;
     441    nrepeat (napply (le_S_S ? ?));
     442    napply le_O_n;
    452443nqed.
    453444
    … …  
    455446  λs: Status.
    456447    let sfr ≝ special_function_registers_8051 s in
    457     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    458       get_index_v Bool eight psw six ?.
    459     nnormalize.
    460     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    461     napply (less_than_or_equal_zero).
    462     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    463     napply (less_than_or_equal_zero).
     448    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     449      get_index_v bool 8 psw 6 ?.
     450    nnormalize;
     451    nrepeat (napply (le_S_S ? ?));
     452    napply le_O_n;
    464453nqed.
    465454
    … …  
    467456  λs: Status.
    468457    let sfr ≝ special_function_registers_8051 s in
    469     let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
    470       get_index_v Bool eight psw seven ?.
    471     nnormalize.
    472     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    473     napply (less_than_or_equal_zero).
    474     nrepeat (napply (less_than_or_equal_monotone ? ?)).
    475     napply (less_than_or_equal_zero).
     458    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
     459      get_index_v bool 8 psw 7 ?.
     460    nnormalize;
     461    nrepeat (napply (le_S_S ? ?));
     462    napply le_O_n;
    476463nqed.
    477464
    … …  
    479466  λs: Status.
    480467  λcy: Bit.
    481   λac: Maybe Bit.
     468  λac: option Bit.
    482469  λov: Bit.
    483     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
    484     let old_cy ≝ get_index_v… nu Z ? in
    485     let old_ac ≝ get_index_v… nu one ? in
    486     let old_fo ≝ get_index_v… nu two ? in
    487     let old_rs1 ≝ get_index_v… nu three ? in
    488     let old_rs0 ≝ get_index_v… nl Z ? in
    489     let old_ov ≝ get_index_v… nl one ? in
    490     let old_ud ≝ get_index_v… nl two ? in
    491     let old_p ≝ get_index_v… nl three ? in
    492     let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in
     470    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in
     471    let old_cy ≝ get_index_v… nu O ? in
     472    let old_ac ≝ get_index_v… nu 1 ? in
     473    let old_fo ≝ get_index_v… nu 2 ? in
     474    let old_rs1 ≝ get_index_v… nu 3 ? in
     475    let old_rs0 ≝ get_index_v… nl O ? in
     476    let old_ov ≝ get_index_v… nl 1 ? in
     477    let old_ud ≝ get_index_v… nl 2 ? in
     478    let old_p ≝ get_index_v… nl 3 ? in
     479    let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in
    493480    let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
    494481                     old_rs0 ; old_ov ; old_ud ; old_p ]] in
    … …  
    496483    ##[##1,2,3,4,5,6,7,8:
    497484        nnormalize;
    498         nrepeat (napply less_than_or_equal_monotone);
    499         napply (less_than_or_equal_zero);
     485        nrepeat (napply le_S_S);
     486        napply (le_O_n);
    500487    ##]
    501488nqed.
    502489
    503490ndefinition initialise_status ≝
    504   let status ≝ mk_Status (Stub Byte sixteen)                    (* Code mem. *)
    505                          (Stub Byte seven)                      (* Low mem.  *)
    506                          (Stub Byte seven)                      (* High mem. *)
    507                          (Stub Byte sixteen)                    (* Ext mem.  *)
    508                          (zero sixteen)                         (* PC.       *)
    509                          (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
    510                          (replicate Byte five (zero eight))     (* 8052 SFR. *)
    511                          (zero eight)                           (* P1 latch. *)
    512                          (zero eight)                           (* P3 latch. *)
    513                          Z                                      (* Clock.    *)
     491  let status ≝ mk_Status (Stub Byte 16)                    (* Code mem. *)
     492                         (Stub Byte 7)                      (* Low mem.  *)
     493                         (Stub Byte 7)                      (* High mem. *)
     494                         (Stub Byte 16)                    (* Ext mem.  *)
     495                         (zero 16)                         (* PC.       *)
     496                         (replicate Byte 19 (zero 8)) (* 8051 SFR. *)
     497                         (replicate Byte 5 (zero 8))     (* 8052 SFR. *)
     498                         (zero 8)                           (* P1 latch. *)
     499                         (zero 8)                           (* P3 latch. *)
     500                         O                                      (* Clock.    *)
    514501  in
    515     set_8051_sfr status SFR_SP (bitvector_of_nat eight seven).
     502    set_8051_sfr status SFR_SP (bitvector_of_nat 8 7).
    516503 
    517504naxiom not_implemented: False.
    … …  
    519506ndefinition get_bit_addressable_sfr ≝
    520507  λs: Status.
    521   λn: Nat.
     508  λn: nat.
    522509  λb: BitVector n.
    523   λl: Bool.
     510  λl: bool.
    524511    let address ≝ nat_of_bitvector … b in
    525       if (eq_n address one_hundred_and_twenty_eight) then
     512      if (eqb address 128) then
    526513        ?
    527       else if (eq_n address one_hundred_and_forty_four) then
     514      else if (eqb address 144) then
    528515        if l then
    529516          (p1_latch s)
    530517        else
    531518          (get_8051_sfr s SFR_P1)
    532       else if (eq_n address one_hundred_and_sixty) then
     519      else if (eqb address 160) then
    533520        ?
    534       else if (eq_n address one_hundred_and_seventy_six) then
     521      else if (eqb address 176) then
    535522        if l then
    536523          (p3_latch s)
    537524        else
    538525          (get_8051_sfr s SFR_P3)
    539       else if (eq_n address one_hundred_and_fifty_three) then
     526      else if (eqb address 153) then
    540527        get_8051_sfr s SFR_SBUF
    541       else if (eq_n address one_hundred_and_thirty_eight) then
     528      else if (eqb address 138) then
    542529        get_8051_sfr s SFR_TL0
    543       else if (eq_n address one_hundred_and_thirty_nine) then
     530      else if (eqb address 139) then
    544531        get_8051_sfr s SFR_TL1
    545       else if (eq_n address one_hundred_and_forty) then
     532      else if (eqb address 140) then
    546533        get_8051_sfr s SFR_TH0
    547       else if (eq_n address one_hundred_and_forty_one) then
     534      else if (eqb address 141) then
    548535        get_8051_sfr s SFR_TH1
    549       else if (eq_n address two_hundred) then
     536      else if (eqb address 200) then
    550537        get_8052_sfr s SFR_T2CON
    551       else if (eq_n address two_hundred_and_two) then
     538      else if (eqb address 202) then
    552539        get_8052_sfr s SFR_RCAP2L
    553       else if (eq_n address two_hundred_and_three) then
     540      else if (eqb address 203) then
    554541        get_8052_sfr s SFR_RCAP2H
    555       else if (eq_n address two_hundred_and_four) then
     542      else if (eqb address 204) then
    556543        get_8052_sfr s SFR_TL2
    557       else if (eq_n address two_hundred_and_five) then
     544      else if (eqb address 205) then
    558545        get_8052_sfr s SFR_TH2
    559       else if (eq_n address one_hundred_and_thirty_five) then
     546      else if (eqb address 135) then
    560547        get_8051_sfr s SFR_PCON
    561       else if (eq_n address one_hundred_and_thirty_six) then
     548      else if (eqb address 136) then
    562549        get_8051_sfr s SFR_TCON
    563       else if (eq_n address one_hundred_and_thirty_seven) then
     550      else if (eqb address 137) then
    564551        get_8051_sfr s SFR_TMOD
    565       else if (eq_n address one_hundred_and_fifty_two) then
     552      else if (eqb address 152) then
    566553        get_8051_sfr s SFR_SCON
    567       else if (eq_n address one_hundred_and_sixty_eight) then
     554      else if (eqb address 168) then
    568555        get_8051_sfr s SFR_IE
    569       else if (eq_n address one_hundred_and_eighty_four) then
     556      else if (eqb address 184) then
    570557        get_8051_sfr s SFR_IP
    571       else if (eq_n address one_hundred_and_twenty_nine) then
     558      else if (eqb address 129) then
    572559        get_8051_sfr s SFR_SP
    573       else if (eq_n address one_hundred_and_thirty) then
     560      else if (eqb address 130) then
    574561        get_8051_sfr s SFR_DPL
    575       else if (eq_n address one_hundred_and_thirty_one) then
     562      else if (eqb address 131) then
    576563        get_8051_sfr s SFR_DPH
    577       else if (eq_n address two_hundred_and_eight) then
     564      else if (eqb address 208) then
    578565        get_8051_sfr s SFR_PSW
    579       else if (eq_n address two_hundred_and_twenty_four) then
     566      else if (eqb address 224) then
    580567        get_8051_sfr s SFR_ACC_A
    581       else if (eq_n address two_hundred_and_forty) then
     568      else if (eqb address 240) then
    582569        get_8051_sfr s SFR_ACC_B
    583570      else
    … …  
    591578  λv: Byte.
    592579    let address ≝ nat_of_bitvector … b in
    593       if (eq_n address one_hundred_and_twenty_eight) then
     580      if (eqb address 128) then
    594581        ?
    595       else if (eq_n address one_hundred_and_forty_four) then
     582      else if (eqb address 144) then
    596583        let status_1 ≝ set_8051_sfr s SFR_P1 v in
    597584        let status_2 ≝ set_p1_latch s v in
    598585          status_2
    599       else if (eq_n address one_hundred_and_sixty) then
     586      else if (eqb address 160) then
    600587        ?
    601       else if (eq_n address one_hundred_and_seventy_six) then
     588      else if (eqb address 176) then
    602589        let status_1 ≝ set_8051_sfr s SFR_P3 v in
    603590        let status_2 ≝ set_p3_latch s v in
    604591          status_2
    605       else if (eq_n address one_hundred_and_fifty_three) then
     592      else if (eqb address 153) then
    606593        set_8051_sfr s SFR_SBUF v
    607       else if (eq_n address one_hundred_and_thirty_eight) then
     594      else if (eqb address 138) then
    608595        set_8051_sfr s SFR_TL0 v
    609       else if (eq_n address one_hundred_and_thirty_nine) then
     596      else if (eqb address 139) then
    610597        set_8051_sfr s SFR_TL1 v
    611       else if (eq_n address one_hundred_and_forty) then
     598      else if (eqb address 140) then
    612599        set_8051_sfr s SFR_TH0 v
    613       else if (eq_n address one_hundred_and_forty_one) then
     600      else if (eqb address 141) then
    614601        set_8051_sfr s SFR_TH1 v
    615       else if (eq_n address two_hundred) then
     602      else if (eqb address 200) then
    616603        set_8052_sfr s SFR_T2CON v
    617       else if (eq_n address two_hundred_and_two) then
     604      else if (eqb address 202) then
    618605        set_8052_sfr s SFR_RCAP2L v
    619       else if (eq_n address two_hundred_and_three) then
     606      else if (eqb address 203) then
    620607        set_8052_sfr s SFR_RCAP2H v
    621       else if (eq_n address two_hundred_and_four) then
     608      else if (eqb address 204) then
    622609        set_8052_sfr s SFR_TL2 v
    623       else if (eq_n address two_hundred_and_five) then
     610      else if (eqb address 205) then
    624611        set_8052_sfr s SFR_TH2 v
    625       else if (eq_n address one_hundred_and_thirty_five) then
     612      else if (eqb address 135) then
    626613        set_8051_sfr s SFR_PCON v
    627       else if (eq_n address one_hundred_and_thirty_six) then
     614      else if (eqb address 136) then
    628615        set_8051_sfr s SFR_TCON v
    629       else if (eq_n address one_hundred_and_thirty_seven) then
     616      else if (eqb address 137) then
    630617        set_8051_sfr s SFR_TMOD v
    631       else if (eq_n address one_hundred_and_fifty_two) then
     618      else if (eqb address 152) then
    632619        set_8051_sfr s SFR_SCON v
    633       else if (eq_n address one_hundred_and_sixty_eight) then
     620      else if (eqb address 168) then
    634621        set_8051_sfr s SFR_IE v
    635       else if (eq_n address one_hundred_and_eighty_four) then
     622      else if (eqb address 184) then
    636623        set_8051_sfr s SFR_IP v
    637       else if (eq_n address one_hundred_and_twenty_nine) then
     624      else if (eqb address 129) then
    638625        set_8051_sfr s SFR_SP v
    639       else if (eq_n address one_hundred_and_thirty) then
     626      else if (eqb address 130) then
    640627        set_8051_sfr s SFR_DPL v
    641       else if (eq_n address one_hundred_and_thirty_one) then
     628      else if (eqb address 131) then
    642629        set_8051_sfr s SFR_DPH v
    643       else if (eq_n address two_hundred_and_eight) then
     630      else if (eqb address 208) then
    644631        set_8051_sfr s SFR_PSW v
    645       else if (eq_n address two_hundred_and_twenty_four) then
     632      else if (eqb address 224) then
    646633        set_8051_sfr s SFR_ACC_A v
    647       else if (eq_n address two_hundred_and_forty) then
     634      else if (eqb address 240) then
    648635        set_8051_sfr s SFR_ACC_B v
    649636      else
    … …  
    654641ndefinition bit_address_of_register ≝
    655642  λs: Status.
    656   λr: BitVector three.
    657     let b ≝ get_index_v … r Z ? in
    658     let c ≝ get_index_v … r one ? in
    659     let d ≝ get_index_v … r two ? in
    660     let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    661     let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in
     643  λr: BitVector 3.
     644    let b ≝ get_index_v … r O ? in
     645    let c ≝ get_index_v … r 1 ? in
     646    let d ≝ get_index_v … r 2 ? in
     647    let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     648    let 〈 r1, r0 〉 ≝ mk_pair … (get_index_v … 4 un 2 ?) (get_index_v … 4 un 3 ?) in
    662649    let offset ≝
    663       if conjunction (negation r1) (negation r0) then
    664         Z
    665       else if conjunction (negation r1) r0 then
    666         eight
    667       else if conjunction r1 r0 then
    668         twenty_four
     650      if ¬r1 ∧ ¬r0 then
     651        O
     652      else if ¬r1 ∧ r0 then
     653        8
     654      else if r1 ∧ r0 then
     655        24
    669656      else
    670         sixteen
     657        16
    671658    in
    672       bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
     659      bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
    673660  ##[##1,2,3,4,5:
    674661      nnormalize;
    675       nrepeat (napply less_than_or_equal_monotone);
    676       napply less_than_or_equal_zero;
     662      nrepeat (napply le_S_S);
     663      napply le_O_n;
    677664  ##]
    678665nqed.
    … …  
    680667ndefinition get_register ≝
    681668  λs: Status.
    682   λr: BitVector three.
     669  λr: BitVector 3.
    683670    let address ≝ bit_address_of_register s r in
    684       lookup … address (low_internal_ram s) (zero eight).
     671      lookup … address (low_internal_ram s) (zero 8).
    685672     
    686673ndefinition set_register ≝
    687674  λs: Status.
    688   λr: BitVector three.
     675  λr: BitVector 3.
    689676  λv: Byte.
    690677    let address ≝ bit_address_of_register s r in
    … …  
    695682ndefinition read_at_stack_pointer ≝
    696683  λs: Status.
    697     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    698     let m ≝ get_index_v … nu Z ? in
    699     let r1 ≝ get_index_v … nu one ? in
    700     let r2 ≝ get_index_v … nu two ? in
    701     let r3 ≝ get_index_v … nu three ? in
     684    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
     685    let m ≝ get_index_v … nu O ? in
     686    let r1 ≝ get_index_v … nu 1 ? in
     687    let r2 ≝ get_index_v … nu 2 ? in
     688    let r3 ≝ get_index_v … nu 3 ? in
    702689    let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
    703690    let memory ≝
    … …  
    707694        (high_internal_ram s)
    708695    in
    709       lookup … address memory (zero eight).
    710     ##[##1,2,3,4:
    711         nnormalize;
    712         nrepeat (napply less_than_or_equal_monotone);
    713         napply less_than_or_equal_zero;
    714     ##]
     696      lookup … address memory (zero 8).
     697  ##[##1,2,3,4:
     698      nnormalize;
     699      nrepeat (napply le_S_S);
     700      napply le_O_n;
     701  ##]
    715702nqed.
    716703
    … …  
    718705  λs: Status.
    719706  λv: Byte.
    720     let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
    721     let bit_zero ≝ get_index_v… nu Z ? in
    722     let bit_one ≝ get_index_v… nu one ? in
    723     let bit_two ≝ get_index_v… nu two ? in
    724     let bit_three ≝ get_index_v… nu three ? in
     707    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
     708    let bit_zero ≝ get_index_v… nu O ? in
     709    let bit_1 ≝ get_index_v… nu 1 ? in
     710    let bit_2 ≝ get_index_v… nu 2 ? in
     711    let bit_3 ≝ get_index_v… nu 3 ? in
    725712      if bit_zero then
    726         let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     713        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    727714                              v (low_internal_ram s) in
    728715          set_low_internal_ram s memory
    729716      else
    730         let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
     717        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    731718                              v (high_internal_ram s) in
    732719          set_high_internal_ram s memory.
    733     ##[##1,2,3,4:
    734         nnormalize;
    735         nrepeat (napply less_than_or_equal_monotone);
    736         napply less_than_or_equal_zero;
    737     ##]
     720  ##[##1,2,3,4:
     721      nnormalize;
     722      nrepeat (napply le_S_S);
     723      napply le_O_n;
     724  ##]
    738725nqed.
    739726
    … …  
    742729   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
    743730     [ DPTR ⇒ λ_:True.
    744        let 〈 bu, bl 〉 ≝ split … eight eight v in
     731       let 〈 bu, bl 〉 ≝ split … 8 8 v in
    745732       let status ≝ set_8051_sfr s SFR_DPH bu in
    746733       let status ≝ set_8051_sfr status SFR_DPL bl in
    … …  
    762749      ] (subaddressing_modein … a).
    763750     
    764 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
     751ndefinition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
    765752                                          acc_a ; acc_b ; data ; acc_dptr ;
    766753                                          acc_pc ; ext_indirect ;
    … …  
    778765        λext_indirect_dptr: True.
    779766          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    780             lookup … sixteen address (external_ram s) (zero eight)
     767            lookup … 16 address (external_ram s) (zero 8)
    781768      | EXT_INDIRECT e ⇒
    782769        λext_indirect: True.
    783770          let address ≝ get_register s [[ false; false; e ]]  in
    784           let padded_address ≝ pad eight eight address in
    785             lookup … sixteen padded_address (external_ram s) (zero eight)
     771          let padded_address ≝ pad 8 8 address in
     772            lookup … 16 padded_address (external_ram s) (zero 8)
    786773      | ACC_DPTR ⇒
    787774        λacc_dptr: True.
    788775          let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    789           let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    790           let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
    791             lookup … sixteen address (external_ram s) (zero eight)
     776          let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
     777          let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
     778            lookup … 16 address (external_ram s) (zero 8)
    792779      | ACC_PC ⇒
    793780        λacc_pc: True.
    794           let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
    795           let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
    796             lookup … sixteen address (external_ram s) (zero eight)
     781          let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
     782          let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in
     783            lookup … 16 address (external_ram s) (zero 8)
    797784      | DIRECT d ⇒
    798785        λdirect: True.
    799           let 〈 nu, nl 〉 ≝ split … four four d in
    800           let bit_one ≝ get_index_v … nu one ? in
    801             match bit_one with
     786          let 〈 nu, nl 〉 ≝ split … 4 4 d in
     787          let bit_1 ≝ get_index_v … nu 1 ? in
     788            match bit_1 with
    802789              [ true ⇒
    803                   let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
     790                  let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
    804791                  let address ≝ three_bits @@ nl in
    805                     lookup ? seven address (low_internal_ram s) (zero eight)
    806               | false ⇒ get_bit_addressable_sfr s eight d l
     792                    lookup ? 7 address (low_internal_ram s) (zero 8)
     793              | false ⇒ get_bit_addressable_sfr s 8 d l
    807794              ]
    808795      | INDIRECT i ⇒
    809796        λindirect: True.
    810           let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
    811           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    812           let bit_one ≝ get_index_v … bit_one_v Z ? in
    813           match bit_one with
     797          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in
     798          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     799          let bit_1 ≝ get_index_v … bit_one_v O ? in
     800          match bit_1 with
    814801            [ true ⇒
    815                 lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
     802                lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8)
    816803            | false ⇒
    817                 lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
     804                lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8)
    818805            ]
    819806      | _ ⇒ λother.
    … …  
    822809      ##[##1,2:
    823810          nnormalize;
    824           nrepeat (napply less_than_or_equal_monotone);
    825           napply less_than_or_equal_zero;
     811          nrepeat (napply le_S_S);
     812          napply le_O_n;
    826813      ##]
    827814nqed.
    … …  
    836823      [ DIRECT d ⇒
    837824        λdirect: True.
    838           let 〈 nu, nl 〉 ≝ split … four four d in
    839           let bit_one ≝ get_index_v … nu one ? in
    840           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    841             match bit_one with
     825          let 〈 nu, nl 〉 ≝ split … 4 4 d in
     826          let bit_1 ≝ get_index_v … nu 1 ? in
     827          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     828            match bit_1 with
    842829              [ true ⇒ set_bit_addressable_sfr s d v
    843830              | false ⇒
    844                 let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
     831                let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in
    845832                  set_low_internal_ram s memory
    846833              ]
    … …  
    848835        λindirect: True.
    849836          let register ≝ get_register s [[ false; false; i ]] in
    850           let 〈nu, nl〉 ≝ split ? four four register in
    851           let bit_one ≝ get_index_v … nu one ? in
    852           let 〈ignore, three_bits〉 ≝ split ? one three nu in
    853             match bit_one with
     837          let 〈nu, nl〉 ≝ split ? 4 4 register in
     838          let bit_1 ≝ get_index_v … nu 1 ? in
     839          let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     840            match bit_1 with
    854841              [ true ⇒
    855842                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
    … …  
    865852        λext_indirect: True.
    866853          let address ≝ get_register s [[ false; false; e ]] in
    867           let padded_address ≝ pad eight eight address in
    868           let memory ≝ insert ? sixteen padded_address v (external_ram s) in
     854          let padded_address ≝ pad 8 8 address in
     855          let memory ≝ insert ? 16 padded_address v (external_ram s) in
    869856            set_external_ram s memory
    870857      | EXT_INDIRECT_DPTR ⇒
    871858        λext_indirect_dptr: True.
    872859          let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
    873           let memory ≝ insert ? sixteen address v (external_ram s) in
     860          let memory ≝ insert ? 16 address v (external_ram s) in
    874861            set_external_ram s memory
    875862      | _ ⇒
    … …  
    879866      ##[##1,2:
    880867          nnormalize;
    881           nrepeat (napply less_than_or_equal_monotone);
    882           napply less_than_or_equal_zero
     868          nrepeat (napply le_S_S);
     869          napply le_O_n
    883870      ##]
    884871nqed.
    885872
    886873ntheorem modulus_less_than:
    887   ∀m,n: Nat. (m mod (S n)) < S n.
    888  #n m; nnormalize; napply less_than_or_equal_monotone;
    889  nlapply (ltoe_refl n);
     874  ∀m,n: nat. (m mod (S n)) < S n.
     875 #n m; nnormalize; napply le_S_S;
     876 nlapply (le_n n);
    890877 ngeneralize in ⊢ (?%? → ?(??%?)?);
    891878 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?)
    … …  
    895882     [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/;
    896883       ncases n; nnormalize; //;
    897        #x K1; nlapply (less_than_or_equal_injective … K1); ngeneralize in match m;
     884       #x K1; nlapply (le_S_S_to_le … K1); ngeneralize in match m;
    898885       nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //;
    899886       #q K2; napply H; /3/]
    … …  
    901888
    902889ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
    903                        Bool → Bool ≝
     890                       bool → bool ≝
    904891  λs, a, l.
    905892    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
    … …  
    908895      [ BIT_ADDR b ⇒
    909896        λbit_addr: True.
    910           let 〈 nu, nl 〉 ≝ split … four four b in
    911           let bit_one ≝ get_index_v … nu one ? in
    912           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    913             match bit_one with
     897          let 〈 nu, nl 〉 ≝ split … 4 4 b in
     898          let bit_1 ≝ get_index_v … nu 1 ? in
     899          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     900            match bit_1 with
    914901              [ true ⇒
    915902                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    916                 let d ≝ address ÷ eight in
    917                 let m ≝ address mod eight in
    918                 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     903                let d ≝ address ÷ 8 in
     904                let m ≝ address mod 8 in
     905                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    919906                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    920907                  get_index_v … sfr m ?
    921908              | false ⇒
    922909                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    923                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    924                 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    925                   get_index_v … t (modulus address eight) ?
     910                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     911                let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     912                  get_index_v … t (modulus address 8) ?
    926913              ]
    927914      | N_BIT_ADDR n ⇒
    928915        λn_bit_addr: True.
    929           let 〈 nu, nl 〉 ≝ split … four four n in
    930           let bit_one ≝ get_index_v … nu one ? in
    931           let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
    932             match bit_one with
     916          let 〈 nu, nl 〉 ≝ split … 4 4 n in
     917          let bit_1 ≝ get_index_v … nu 1 ? in
     918          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     919            match bit_1 with
    933920              [ true ⇒
    934921                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    935                 let d ≝ address ÷ eight in
    936                 let m ≝ address mod eight in
    937                 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     922                let d ≝ address ÷ 8 in
     923                let m ≝ address mod 8 in
     924                let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    938925                let sfr ≝ get_bit_addressable_sfr s ? trans l in
    939                   negation (get_index_v … sfr m ?)
     926                  ¬(get_index_v … sfr m ?)
    940927              | false ⇒
    941928                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    942                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    943                 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    944                   negation (get_index_v … trans (modulus address eight) ?)
     929                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     930                let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     931                  ¬(get_index_v … trans (modulus address 8) ?)
    945932              ]
    946933      | CARRY ⇒ λcarry: True. get_cy_flag s
    … …  
    950937      ##[##3,6:
    951938          nnormalize;
    952           nrepeat (napply less_than_or_equal_monotone);
    953           napply less_than_or_equal_zero;
     939          nrepeat (napply le_S_S);
     940          napply le_O_n;
    954941      ##|##1,2,4,5:
    955942          napply modulus_less_than;
    … …  
    962949    match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
    963950      [ BIT_ADDR b ⇒ λbit_addr: True.
    964           let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    965           let bit_one ≝ get_index_v … nu one ? in
    966           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    967           match bit_one with
     951          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     952          let bit_1 ≝ get_index_v … nu 1 ? in
     953          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     954          match bit_1 with
    968955            [ true ⇒
    969956                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    970                 let d ≝ address ÷ eight in
    971                 let m ≝ address mod eight in
    972                 let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
     957                let d ≝ address ÷ 8 in
     958                let m ≝ address mod 8 in
     959                let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    973960                let sfr ≝ get_bit_addressable_sfr s ? t true in
    974961                let new_sfr ≝ set_index … sfr m v ? in
    … …  
    976963            | false ⇒
    977964                let address ≝ nat_of_bitvector … (three_bits @@ nl) in
    978                 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
    979                 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
    980                 let n_bit ≝ set_index … t (modulus address eight) v ? in
    981                 let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
     965                let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     966                let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
     967                let n_bit ≝ set_index … t (modulus address 8) v ? in
     968                let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in
    982969                  set_low_internal_ram s memory
    983970            ]
    984971      | CARRY ⇒
    985972        λcarry: True.
    986           let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
    987           let bit_one ≝ get_index_v… nu one ? in
    988           let bit_two ≝ get_index_v… nu two ? in
    989           let bit_three ≝ get_index_v… nu three ? in
    990           let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
     973          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
     974          let bit_1 ≝ get_index_v… nu 1 ? in
     975          let bit_2 ≝ get_index_v… nu 2 ? in
     976          let bit_3 ≝ get_index_v… nu 3 ? in
     977          let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
    991978            set_8051_sfr s SFR_PSW new_psw
    992979      | _ ⇒
    … …  
    997984      ##[##1,2,3,6:
    998985          nnormalize;
    999           nrepeat (napply less_than_or_equal_monotone);
    1000           napply less_than_or_equal_zero;
     986          nrepeat (napply le_S_S);
     987          napply le_O_n;
    1001988      ##|##4,5:
    1002989          napply modulus_less_than;
    … …  
    1005992
    1006993ndefinition load_code_memory ≝
    1007  fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).
     994 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
    1008995
    1009996ndefinition load ≝

  • Deliverables/D4.1/Matita/String.ma

    r414 r465  
    11include "Char.ma".
    2 include "List.ma".
    3 include "Compare.ma".
    42
    5 ndefinition String ≝ List Char.
     3include "datatypes/list.ma".
    64
    7 naxiom string_lexicographic_ordering: String → String → Compare.
     5ndefinition String ≝ list Char.

  • Deliverables/D4.1/Matita/Test.ma

    r437 r465  
    11include "ASM.ma".
    22
    3 ndefinition test: List instruction ≝
     3ndefinition test: list instruction ≝
    44 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
    55  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
    66  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
    7   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
     7  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
    88  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
    9   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
     9  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    1010  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    1111  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    12   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    13   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
    14   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     12  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     13  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
     14  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    1515  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
    16   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    17   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
    18   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    19   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     16  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     17  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
     18  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     19  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    2020  CLR … (ACC_A);
    2121  MOVC … (ACC_A) (ACC_DPTR);
    22   MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
     22  MOVX … (inr … 〈(EXT_INDIRECT false),(ACC_A)〉);
    2323  INC … (DPTR);
    2424  INC … (REGISTER [[false;false;false]]);
    25   Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
     25  Jump … (CJNE … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
    2626  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
    2727  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
    2828  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
    29   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
     29  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
    3030  CLR … (ACC_A);
    31   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
    32   MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
     31  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
     32  MOV … (inl … (inl … (inl … (inl … (inr … 〈(INDIRECT false),(ACC_A)〉)))));
    3333  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
    34   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    35   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    36   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     34  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     35  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
     36  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    3737  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
    38   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    39   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     38  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     39  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    4040  CLR … (ACC_A);
    41   MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
     41  MOVX … (inr … 〈(EXT_INDIRECT true),(ACC_A)〉);
    4242  INC … (REGISTER [[false;false;true]]);
    4343  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    44   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    45   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    46   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     44  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     45  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
     46  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    4747  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
    48   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    49   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
     48  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     49  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    5050  CLR … (ACC_A);
    51   MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
     51  MOVX … (inr … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
    5252  INC … (DPTR);
    5353  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    5454  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
    5555  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    56   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
    57   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
     56  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
     57  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
    5858  XCHD … (ACC_A) (INDIRECT false);
    59   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
     59  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    6060  RET … ;
    61   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     61  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    6262  RET … ;
    6363  NOP … ;

  • Deliverables/D4.1/Matita/Util.ma

    r246 r465  
    1 include "Nat.ma".
     1include "arithmetics/nat.ma".
     2include "datatypes/pairs.ma".
     3include "datatypes/sums.ma".
     4include "datatypes/list.ma".
     5
     6nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0])
     7                         (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
     8  match l with
     9    [ nil ⇒ x
     10    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
     11    ].
     12
     13ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
     14
    215
    316ndefinition function_apply ≝
    … …  
    1326interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
    1427
    15 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝
     28nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
    1629  match n with
    17     [ Z ⇒ a
     30    [ O ⇒ a
    1831    | S o ⇒ f (iterate A f a o)
    1932    ].
     33   
     34notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     35 with precedence 10
     36for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }.
     37
     38
     39notation "⊥" with precedence 90
     40  for @{ match ? in False with [ ] }.
     41
     42nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝
     43  match b with
     44    [ true ⇒ t
     45    | false ⇒ f
     46    ].
     47   
     48notation "hvbox('if' b 'then' t 'else' f)"
     49  non associative with precedence 83
     50  for @{ 'if_then_else $b $t $f }.
     51
     52interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
     53
     54nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝
     55  match b with
     56    [ true ⇒
     57      match c with
     58        [ false ⇒ true
     59        | true ⇒ false
     60        ]
     61    | false ⇒
     62      match c with
     63        [ false ⇒ false
     64        | true ⇒ true
     65        ]
     66    ].
     67
     68ndefinition ltb ≝
     69  λm, n: nat.
     70    leb (S m) n.
     71   
     72ndefinition geb ≝
     73  λm, n: nat.
     74    ltb n m.
     75
     76ndefinition gtb ≝
     77  λm, n: nat.
     78    leb n m.
     79
     80interpretation "Nat less than" 'lt m n = (ltb m n).
     81interpretation "Nat greater than" 'gt m n = (gtb m n).
     82interpretation "Nat greater than eq" 'geq m n = (geb m n).
     83
     84nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝
     85  match ltb n p with
     86    [ true ⇒ O
     87    | false ⇒
     88      match m with
     89        [ O ⇒ O
     90        | (S q) ⇒ S (division_aux q (n - (S p)) p)
     91        ]
     92    ].
     93   
     94ndefinition division ≝
     95  λm, n: nat.
     96    match n with
     97      [ O ⇒ S m
     98      | S o ⇒ division_aux m m o
     99      ].
     100     
     101notation "hvbox(n break ÷ m)"
     102  right associative with precedence 47
     103  for @{ 'division $n $m }.
     104 
     105interpretation "Nat division" 'division n m = (division n m).
     106
     107nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
     108  match leb n p with
     109    [ true ⇒ n
     110    | false ⇒
     111      match m with
     112        [ O ⇒ n
     113        | S o ⇒ modulus_aux o (n - (S p)) p
     114        ]
     115    ].
     116   
     117ndefinition modulus ≝
     118  λm, n: nat.
     119    match n with
     120      [ O ⇒ m
     121      | S o ⇒ modulus_aux m m o
     122      ].
     123   
     124notation "hvbox(n break 'mod' m)"
     125  right associative with precedence 47
     126  for @{ 'modulus $n $m }.
     127 
     128interpretation "Nat modulus" 'modulus m n = (modulus m n).
     129
     130ndefinition divide_with_remainder ≝
     131  λm, n: nat.
     132    mk_pair ? ? (m ÷ n) (modulus m n).
     133   
     134nlet rec exponential (m: nat) (n: nat) on n ≝
     135  match n with
     136    [ O ⇒ S O
     137    | S o ⇒ m * exponential m o
     138    ].
     139
     140interpretation "Nat exponential" 'exp n m = (exponential n m).
     141   
     142notation "hvbox(a break ⊎ b)"
     143 left associative with precedence 50
     144for @{ 'disjoint_union $a $b }.
     145interpretation "sum" 'disjoint_union A B = (Sum A B).
     146
     147ntheorem less_than_or_equal_monotone:
     148  ∀m, n: nat.
     149    m ≤ n → (S m) ≤ (S n).
     150 #m n H; nelim H; /2/.
     151nqed.
     152
     153ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n).
     154 #m; nelim m; nnormalize
     155  [ #n H; ndestruct | #y H1 z; ncases z; nnormalize
     156    [ #H; /2/ | /3/ ]
     157nqed.
     158
     159ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n.
     160 #m; nelim m; //; #y H1 z; ncases z; nnormalize
     161  [ #H; ndestruct | /3/ ]
     162nqed.
     163
     164ndefinition less_than_or_equal_b_elim:
     165 ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) →
     166  P (leb m n).
     167 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n);
     168 nlapply (less_than_or_equal_b_complete m n);
     169 ncases (leb m n); /3/.
     170nqed.

  • Deliverables/D4.1/Matita/Vector.ma

    r374 r465  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "Nat.ma".
    7 include "List.ma".
     6include "datatypes/list.ma".
     7include "basics/bool.ma".
     8include "datatypes/sums.ma".
     9
     10include "Util.ma".
     11
     12include "arithmetics/nat.ma".
     13
    814
    915(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    1117(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    1218
    13 ninductive Vector (A: Type[0]): Nat → Type[0] ≝
    14   VEmpty: Vector A Z
    15 | VCons: ∀n: Nat. A → Vector A n → Vector A (S n).
     19ninductive Vector (A: Type[0]): nat → Type[0] ≝
     20  VEmpty: Vector A O
     21| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
    1622
    1723(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    3844(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    3945
    40 nlet rec get_index_v (A: Type[0]) (n: Nat)
    41                    (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝
     46nlet rec get_index_v (A: Type[0]) (n: nat)
     47                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
    4248  (match m with
    43     [ Z ⇒
    44       match v return λx.λ_. Z < x → A with
    45         [ VEmpty ⇒ λabsd1: Z < Z. ?
    46         | VCons p hd tl ⇒ λprf1: Z < S p. hd
     49    [ O ⇒
     50      match v return λx.λ_. O < x → A with
     51        [ VEmpty ⇒ λabsd1: O < O. ?
     52        | VCons p hd tl ⇒ λprf1: O < S p. hd
    4753        ]
    4854    | S o ⇒
    4955      (match v return λx.λ_. S o < x → A with
    50         [ VEmpty ⇒ λprf: S o < Z. ?
     56        [ VEmpty ⇒ λprf: S o < O. ?
    5157        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    5258        ])
    5359    ]) lt.
    54     ##[ ncases (nothing_less_than_Z Z); #K; ncases (K absd1)
    55     ##| ncases (nothing_less_than_Z (S o)); #K; ncases (K prf)
    56     ##| napply succ_less_than_injective; nassumption
     60    ##[ ncases (not_le_Sn_O O); nnormalize in absd1; #H; ncases (H absd1);
     61    ##| ncases (not_le_Sn_O (S o)); nnormalize in prf; #H; ncases (H prf);
     62    ##| nnormalize; nnormalize in prf; napply le_S_S_to_le; nassumption;
    5763    ##]
    5864nqed.
    … …  
    6066ndefinition get_index' ≝
    6167  λA: Type[0].
    62   λn, m: Nat.
     68  λn, m: nat.
    6369  λb: Vector A (S (n + m)).
    6470    get_index_v A (S (n + m)) b n ?.
    6571  nnormalize;
    66   napply less_than_or_equal_monotone;
    67   napply less_than_or_equal_plus;
    68 nqed.
    69 
    70 nlet rec get_index_weak_v (A: Type[0]) (n: Nat)
    71                           (v: Vector A n) (m: Nat) on m ≝
     72  //;
     73nqed.
     74
     75nlet rec get_index_weak_v (A: Type[0]) (n: nat)
     76                          (v: Vector A n) (m: nat) on m ≝
    7277  match m with
    73     [ Z ⇒
     78    [ O ⇒
    7479      match v with
    75         [ VEmpty ⇒ Nothing A
    76         | VCons p hd tl ⇒ Just A hd
     80        [ VEmpty ⇒ None A
     81        | VCons p hd tl ⇒ Some A hd
    7782        ]
    7883    | S o ⇒
    7984      match v with
    80         [ VEmpty ⇒ Nothing A
     85        [ VEmpty ⇒ None A
    8186        | VCons p hd tl ⇒ get_index_weak_v A p tl o
    8287        ]
    … …  
    8590interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).
    8691
    87 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝
     92nlet rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
    8893  (match m with
    89     [ Z ⇒
    90       match v return λx.λ_. Z < x → Vector A x with
    91         [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]
    92         | VCons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
     94    [ O ⇒
     95      match v return λx.λ_. O < x → Vector A x with
     96        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
     97        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
    9398        ]
    9499    | S o ⇒
    95100      (match v return λx.λ_. S o < x → Vector A x with
    96         [ VEmpty ⇒ λprf: S o < Z. [[ ]]
     101        [ VEmpty ⇒ λprf: S o < O. [[ ]]
    97102        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
    98103        ])
    99104    ]) lt.
    100     napply succ_less_than_injective.
    101     nassumption.
    102 nqed.
    103    
    104 nlet rec set_index_weak (A: Type[0]) (n: Nat)
    105                         (v: Vector A n) (m: Nat) (a: A) on m ≝
     105    nnormalize in prf ⊢ %;
     106    /2/;
     107nqed.
     108   
     109nlet rec set_index_weak (A: Type[0]) (n: nat)
     110                        (v: Vector A n) (m: nat) (a: A) on m ≝
    106111  match m with
    107     [ Z ⇒
     112    [ O ⇒
    108113      match v with
    109         [ VEmpty ⇒ Nothing (Vector A n)
    110         | VCons o hd tl ⇒ Just (Vector A n) (? (VCons A o a tl))
     114        [ VEmpty ⇒ None (Vector A n)
     115        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
    111116        ]
    112117    | S o ⇒
    113118      match v with
    114         [ VEmpty ⇒ Nothing (Vector A n)
     119        [ VEmpty ⇒ None (Vector A n)
    115120        | VCons p hd tl ⇒
    116121            let settail ≝ set_index_weak A p tl o a in
    117122              match settail with
    118                 [ Nothing ⇒ Nothing (Vector A n)
    119                 | Just j ⇒ Just (Vector A n) (? (VCons A p hd j))
     123                [ None ⇒ None (Vector A n)
     124                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
    120125                ]
    121126        ]
    … …  
    124129nqed.
    125130
    126 nlet rec drop (A: Type[0]) (n: Nat)
    127               (v: Vector A n) (m: Nat) on m ≝
     131nlet rec drop (A: Type[0]) (n: nat)
     132              (v: Vector A n) (m: nat) on m ≝
    128133  match m with
    129     [ Z ⇒ Just (Vector A n) v
     134    [ O ⇒ Some (Vector A n) v
    130135    | S o ⇒
    131136      match v with
    132         [ VEmpty ⇒ Nothing (Vector A n)
     137        [ VEmpty ⇒ None (Vector A n)
    133138        | VCons p hd tl ⇒ ? (drop A p tl o)
    134139        ]
    … …  
    137142nqed.
    138143
    139 nlet rec split (A: Type[0]) (m,n: Nat) on m
    140              : Vector A (m+n) → (Vector A m) × (Vector A n)
     144nlet rec split (A: Type[0]) (m,n: nat) on m
     145             : Vector A (plus m n) → (Vector A m) × (Vector A n)
    141146≝
    142  match m return λm. Vector A (m+n) → (Vector A m) × (Vector A n) with
    143   [ Z ⇒ λv.〈[[ ]], v〉
     147 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
     148  [ O ⇒ λv.〈[[ ]], v〉
    144149  | S m' ⇒ λv.
    145      match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
     150     match v return λl.λ_:Vector A l.l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with
    146151      [ VEmpty ⇒ λK.⊥
    147152      | VCons o he tl ⇒ λK.
    148153         match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with
    149           [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    150 // [ ndestruct | nlapply (S_inj … K); //]
     154          [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
     155// [ ndestruct | nlapply (injective_S … K); //]
    151156nqed.
    152157
    … …  
    157162  | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉
    158163  ] (? : S ? = S ?).
    159 // [ ndestruct | nlapply (S_inj … K); //]
    160 nqed.
    161 
    162 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝
    163  λA,v. first … (head … v).
     164// [ ndestruct | nlapply (injective_S … K); //]
     165nqed.
     166
     167ndefinition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
     168 λA,v. fst … (head … v).
    164169   
    165170(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    167172(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    168173   
    169 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)
     174nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
    170175                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    171176  match v with
    … …  
    174179    ].
    175180
    176 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])
    177                       (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)
     181nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
     182                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
    178183                      (v: Vector A n) (q: Vector B n) on v : C n ≝
    179184  (match v return λx.λ_. x = n → C n with
    180185    [ VEmpty ⇒
    181       match q return λx.λ_. Z = x → C x with
    182         [ VEmpty ⇒ λprf: Z = Z. c
     186      match q return λx.λ_. O = x → C x with
     187        [ VEmpty ⇒ λprf: O = O. c
    183188        | VCons o hd tl ⇒ λabsd. ⊥
    184189        ]
    185190    | VCons o hd tl ⇒
    186191      match q return λx.λ_. S o = x → C x with
    187         [ VEmpty ⇒ λabsd: S o = Z. ⊥
     192        [ VEmpty ⇒ λabsd: S o = O. ⊥
    188193        | VCons p hd' tl' ⇒ λprf: S o = S p.
    189194           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
    190195        ]
    191196    ]) (refl ? n).
    192 ##[##1,2: ndestruct | ##3,4: nlapply (S_inj … prf); // ]
     197##[##1,2: ndestruct | ##3,4: nlapply (injective_S … prf); // ]
    193198nqed.
    194199 
    195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
     200nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
    196201                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    197202  match v with
    … …  
    204209(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    205210
    206 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)
     211nlet rec map (A: Type[0]) (B: Type[0]) (n: nat)
    207212             (f: A → B) (v: Vector A n) on v ≝
    208213  match v with
    … …  
    211216    ].
    212217
    213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)
     218nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
    214219             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
    215220  (match v return (λx.λr. x = n → Vector C x) with
    … …  
    228233          ndestruct(e);
    229234          ##
    230         | nlapply (S_inj … e); #H; nrewrite > H;
     235        | nlapply (injective_S … e); #H; nrewrite > H;
    231236          napply tl'
    232237          ##
    … …  
    236241ndefinition zip ≝
    237242  λA, B: Type[0].
    238   λn: Nat.
     243  λn: nat.
    239244  λv: Vector A n.
    240245  λq: Vector B n.
    241     zip_with A B (Cartesian A B) n (mk_Cartesian A B) v q.
     246    zip_with A B (A × B) n (mk_pair A B) v q.
    242247
    243248(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    245250(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    246251
    247 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
     252nlet rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
    248253  match n return λn. Vector A n with
    249     [ Z ⇒ [[ ]]
     254    [ O ⇒ [[ ]]
    250255    | S m ⇒ h ::: (replicate A m h)
    251256    ].
    252257
    253 nlet rec append (A: Type[0]) (n: Nat) (m: Nat)
     258(* DPM: fixme.  Weird matita bug in base case. *)
     259nlet rec append (A: Type[0]) (n: nat) (m: nat)
    254260                (v: Vector A n) (q: Vector A m) on v ≝
    255261  match v return (λn.λv. Vector A (n + m)) with
    256     [ VEmpty ⇒ q
     262    [ VEmpty ⇒ (? q)
    257263    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
    258264    ].
     265    #H; nassumption;
     266nqed.
    259267   
    260268notation "hvbox(l break @@ r)"
    … …  
    264272interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
    265273   
    266 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
     274nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
    267275                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
    268276  a :::
    … …  
    272280       ]).
    273281
    274 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)
     282nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
    275283                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
    276284  match v with
    … …  
    285293(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286294
    287 nlet rec reverse (A: Type[0]) (n: Nat)
     295nlet rec reverse (A: Type[0]) (n: nat)
    288296                 (v: Vector A n) on v ≝
    289297  match v return (λm.λv. Vector A m) with
    … …  
    291299    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    292300    ].
    293     nrewrite < (succ_plus ? ?).
    294     nrewrite > (plus_zero ?).
    295     //.
     301    //;
    296302nqed.
    297303
    … …  
    300306(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    301307
    302 nlet rec list_of_vector (A: Type[0]) (n: Nat)
     308nlet rec list_of_vector (A: Type[0]) (n: nat)
    303309                        (v: Vector A n) on v ≝
    304   match v return λn.λv. List A with
     310  match v return λn.λv. list A with
    305311    [ VEmpty ⇒ []
    306312    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
    307313    ].
    308314
    309 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
     315nlet rec vector_of_list (A: Type[0]) (l: list A) on l ≝
    310316  match l return λl. Vector A (length A l) with
    311     [ Empty ⇒ [[ ]]
    312     | Cons hd tl ⇒ hd ::: (vector_of_list A tl)
     317    [ nil ⇒ [[ ]]
     318    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
    313319    ].
    314320
    … …  
    317323(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    318324   
    319 nlet rec rotate_left (A: Type[0]) (n: Nat)
    320                      (m: Nat) (v: Vector A n) on m: Vector A n ≝
     325nlet rec rotate_left (A: Type[0]) (n: nat)
     326                     (m: nat) (v: Vector A n) on m: Vector A n ≝
    321327  match m with
    322     [ Z ⇒ v
     328    [ O ⇒ v
    323329    | S o ⇒
    324330        match v with
    325331          [ VEmpty ⇒ [[ ]]
    326332          | VCons p hd tl ⇒
    327              rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S Z) ↦ Vector A (S p)⌉)
     333             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
    328334          ]
    329335    ].
    … …  
    333339ndefinition rotate_right ≝
    334340  λA: Type[0].
    335   λn, m: Nat.
     341  λn, m: nat.
    336342  λv: Vector A n.
    337343    reverse A n (rotate_left A n m (reverse A n v)).
    … …  
    339345ndefinition shift_left_1 ≝
    340346  λA: Type[0].
    341   λn: Nat.
     347  λn: nat.
    342348  λv: Vector A (S n).
    343349  λa: A.
    … …  
    351357ndefinition shift_right_1 ≝
    352358  λA: Type[0].
    353   λn: Nat.
     359  λn: nat.
    354360  λv: Vector A (S n).
    355361  λa: A.
    … …  
    358364ndefinition shift_left ≝
    359365  λA: Type[0].
    360   λn, m: Nat.
     366  λn, m: nat.
    361367  λv: Vector A (S n).
    362368  λa: A.
    … …  
    365371ndefinition shift_right ≝
    366372  λA: Type[0].
    367   λn, m: Nat.
     373  λn, m: nat.
    368374  λv: Vector A (S n).
    369375  λa: A.
    … …  
    374380(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    375381
    376 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool ≝
    377   (match b return λx.λ_. n = x → Bool with
     382nlet rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
     383  (match b return λx.λ_. n = x → bool with
    378384    [ VEmpty ⇒
    379       match c return λx.λ_. x = Z → Bool with
     385      match c return λx.λ_. x = O → bool with
    380386        [ VEmpty ⇒ λ_. true
    381387        | VCons p hd tl ⇒ λabsd.⊥
    382388        ]
    383389    | VCons o hd tl ⇒
    384         match c return λx.λ_. x = S o → Bool with
     390        match c return λx.λ_. x = S o → bool with
    385391          [ VEmpty ⇒ λabsd.⊥
    386392          | VCons p hd' tl' ⇒
    … …  
    393399    ]) (refl ? n).
    394400    ##[##1,2: ndestruct
    395       | nlapply (S_inj … prf); #X; nrewrite < X; @]
     401      | nlapply (injective_S … prf); #X; nrewrite < X; @]
    396402nqed.
    397403
    … …  
    402408ndefinition mem ≝
    403409 λA: Type[0].
    404  λeq_a : A → A → Bool.
    405  λn: Nat.
     410 λeq_a : A → A → bool.
     411 λn: nat.
    406412 λl: Vector A n.
    407413 λx: A.
    408   fold_right … (λy,v. inclusive_disjunction (eq_a x y) v) false l.
     414  fold_right … (λy,v. (eq_a x y) ∨ v) false l.
    409415
    410416ndefinition subvector_with ≝
    411417  λA: Type[0].
    412   λn: Nat.
    413   λm: Nat.
    414   λf: A → A → Bool.
     418  λn: nat.
     419  λm: nat.
     420  λf: A → A → bool.
    415421  λv: Vector A n.
    416422  λq: Vector A m.
    417     fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x) v) true v.
     423    fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v.
    418424   
    419425(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    … …  
    423429nlemma map_fusion:
    424430  ∀A, B, C: Type[0].
    425   ∀n: Nat.
     431  ∀n: nat.
    426432  ∀v: Vector A n.
    427433  ∀f: A → B.

  • Deliverables/D4.1/Matita/depends

    r462 r465  
    1 Exponential.ma Nat.ma
     1Vector.ma Util.ma arithmetics/nat.ma basics/bool.ma datatypes/list.ma datatypes/sums.ma
     2Interpret.ma Fetch.ma Status.ma
     3ASM.ma BitVector.ma String.ma
     4BitVector.ma String.ma Util.ma Vector.ma arithmetics/nat.ma
     5Debug.ma Interpret.ma Status.ma
     6Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
     7BitVectorTrie.ma BitVector.ma datatypes/bool.ma datatypes/sums.ma
     8Arithmetic.ma BitVector.ma Util.ma
     9Test.ma ASM.ma
     10String.ma Char.ma datatypes/list.ma
     11Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
     12Char.ma logic/pts.ma
    213Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Arithmetic.ma BitVector.ma Exponential.ma
    4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    5 Cartesian.ma logic/pts.ma
    6 Maybe.ma Bool.ma Plogic/equality.ma
    7 Either.ma Bool.ma
    814DoTest.ma Assembly.ma Interpret.ma Test.ma
    9 Debug.ma Interpret.ma Status.ma
    10 ASM.ma BitVector.ma Either.ma String.ma
    11 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    12 Char.ma logic/pts.ma
    13 Test.ma ASM.ma
    14 Vector.ma List.ma Nat.ma
    15 Connectives.ma Plogic/equality.ma
    16 Bool.ma logic/pts.ma
    17 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    18 List.ma Maybe.ma Util.ma
    19 Interpret.ma Fetch.ma Status.ma
    20 Util.ma Nat.ma
    21 Compare.ma logic/pts.ma
    22 BitVector.ma String.ma Vector.ma
    23 String.ma Char.ma Compare.ma List.ma
    24 Nat.ma Bool.ma Cartesian.ma Connectives.ma
    25 Plogic/equality.ma
     15Util.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma
     16arithmetics/nat.ma
     17basics/bool.ma
     18datatypes/bool.ma
     19datatypes/list.ma
     20datatypes/pairs.ma
     21datatypes/sums.ma
    2622logic/pts.ma
Note: See TracChangeset for help on using the changeset viewer.