Changeset 472


Ignore:
Timestamp:
Jan 21, 2011, 11:08:00 AM (7 years ago)
Author:
mulligan
Message:

More changes to debug and testing files to get them to work with the standard library.

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

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Debug.ma

    r439 r472  
    1010
    1111nlemma test2:
    12   sub_8_with_carry (bitvector_of_nat eight two_hundred_and_fifty_six)
    13                (bitvector_of_nat eight one) false =
    14   sub_8_with_carry (bitvector_of_nat eight two_hundred_and_fifty_six)
    15                (bitvector_of_nat eight one) false.
     12  sub_8_with_carry (bitvector_of_nat 8 256)
     13               (bitvector_of_nat 8 1) false =
     14  sub_8_with_carry (bitvector_of_nat 8 256)
     15               (bitvector_of_nat 8 1) false.
    1616  nnormalize;
    1717  @;
  • Deliverables/D4.1/Matita/DoTest.ma

    r465 r472  
    33include "Assembly.ma".
    44
    5 ndefinition steps ≝ sixteen.
     5ndefinition steps ≝ 1.
    66
    77ndefinition testmem ≝ assembly_unlabelled_program test.
     
    99 match testmem with
    1010  [ None ⇒ None …
    11   | Some testmem ⇒ Some … (load (first … testmem) initialise_status)].
     11  | Some testmem ⇒ Some … (load (fst … testmem) initialise_status)].
    1212ndefinition testfinal ≝
    1313 match teststatus with
     
    2222    [ O ⇒ []
    2323    | S o ⇒
    24        first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
     24       fst … (fst … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
    2525    ].
    2626
     
    8888notation < "𝔽l" with precedence 90 for @{ 'f4 $l }.
    8989
    90 interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
    91 interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
    92 interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
    93 interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
    94 interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
    95 interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
    96 interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
    97 interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
    98 interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
    99 interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
    100 interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
    101 interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
    102 interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
    103 interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
    104 interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
    105 interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
    106 
    107 interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    108 interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    109 interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    110 interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    111 interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    112 interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    113 interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    114 interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    115 interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    116 interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    117 interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    118 interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    119 interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    120 interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    121 interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
    122 interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
    123 
    124 interpretation "zero16" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    125 interpretation "one16" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    126 interpretation "two16" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    127 interpretation "three16" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    128 interpretation "four16" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    129 interpretation "five16" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    130 interpretation "six16" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    131 interpretation "seven16" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    132 interpretation "eight16" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    133 interpretation "nine16" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    134 interpretation "A16" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    135 interpretation "B16" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    136 interpretation "C16" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    137 interpretation "D16" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
    138 interpretation "E16" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
    139 interpretation "F16" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     90interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
     91interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
     92interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
     93interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
     94interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
     95interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
     96interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
     97interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
     98interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
     99interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
     100interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
     101interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
     102interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) false l)))).
     103interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S O)))) true l)))).
     104interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) false l)))).
     105interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S O)))) true l)))).
     106
     107interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     108interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     109interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     110interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     111interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     112interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     113interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     114interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     115interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     116interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     117interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     118interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     119interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     120interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     121interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) false l)))).
     122interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S O)))))))) true l)))).
     123
     124interpretation "zero16" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     125interpretation "one16" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     126interpretation "two16" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     127interpretation "three16" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     128interpretation "four16" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     129interpretation "five16" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     130interpretation "six16" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     131interpretation "seven16" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     132interpretation "eight16" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     133interpretation "nine16" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     134interpretation "A16" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     135interpretation "B16" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     136interpretation "C16" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     137interpretation "D16" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
     138interpretation "E16" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) false l)))).
     139interpretation "F16" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))) true l)))).
    140140
    141141notation < "…" with precedence 90 for @{ 'hide }.
     
    146146    [ None ⇒ None ?
    147147    | Some s ⇒
    148       let lk ≝ lookup ? seven ([[ false; false; false ]] @@ (max four)) (low_internal_ram s) (zero ?) in
     148      let lk ≝ lookup ? 7 ([[ false; false; false ]] @@ (max 4)) (low_internal_ram s) (zero ?) in
    149149        Some … 〈lk, program_counter s〉
    150150    ].
     
    157157
    158158nlemma test3:
    159   half_add ? (sign_extension (bitvector_of_nat eight (two_hundred_and_fifty_six - three)))
    160                                      (bitvector_of_nat sixteen thirty_two) =
    161   half_add ? (sign_extension (bitvector_of_nat eight (two_hundred_and_fifty_six - three)))
    162                                      (bitvector_of_nat sixteen thirty_two).
     159  half_add ? (sign_extension (bitvector_of_nat 8 (256 - 3)))
     160                                     (bitvector_of_nat 16 32) =
     161  half_add ? (sign_extension (bitvector_of_nat 8 (256 - 3)))
     162                                     (bitvector_of_nat 16 32).
    163163  nnormalize;
    164164  @;
     
    169169    [ None ⇒ None …   
    170170    | Some teststatus ⇒
    171         Some … (fetch (code_memory teststatus) (bitvector_of_nat ? (two_hundred_and_fifty_six + thirty_two + twenty_four)))
     171        Some … (fetch (code_memory teststatus) (bitvector_of_nat ? (256 + 32 + 24)))
    172172    ].
    173173
  • Deliverables/D4.1/Matita/depends

    r465 r472  
     1Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
     2Arithmetic.ma BitVector.ma Util.ma
     3BitVectorTrie.ma BitVector.ma basics/bool.ma datatypes/sums.ma
     4DoTest.ma Assembly.ma Interpret.ma Test.ma
     5Debug.ma Interpret.ma Status.ma
     6ASM.ma BitVector.ma String.ma
     7Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
     8Char.ma logic/pts.ma
     9Test.ma ASM.ma
    110Vector.ma Util.ma arithmetics/nat.ma basics/bool.ma datatypes/list.ma datatypes/sums.ma
     11Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    212Interpret.ma Fetch.ma Status.ma
    3 ASM.ma BitVector.ma String.ma
     13Util.ma arithmetics/nat.ma datatypes/list.ma datatypes/pairs.ma datatypes/sums.ma
    414BitVector.ma String.ma Util.ma Vector.ma arithmetics/nat.ma
    5 Debug.ma Interpret.ma Status.ma
    6 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    7 BitVectorTrie.ma BitVector.ma datatypes/bool.ma datatypes/sums.ma
    8 Arithmetic.ma BitVector.ma Util.ma
    9 Test.ma ASM.ma
    1015String.ma Char.ma datatypes/list.ma
    11 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    12 Char.ma logic/pts.ma
    13 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    14 DoTest.ma Assembly.ma Interpret.ma Test.ma
    15 Util.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma
    1616arithmetics/nat.ma
    1717basics/bool.ma
    18 datatypes/bool.ma
    1918datatypes/list.ma
    2019datatypes/pairs.ma
Note: See TracChangeset for help on using the changeset viewer.