Changeset 439 for Deliverables


Ignore:
Timestamp:
Dec 16, 2010, 6:17:14 PM (9 years ago)
Author:
mulligan
Message:

Changes to get everything to compile.

Location:
Deliverables/D4.1/Matita
Files:
1 added
4 edited

Legend:

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

    r437 r439  
    33include "Assembly.ma".
    44
    5 ndefinition steps ≝ one_hundred_and_twenty_eight.
     5ndefinition steps ≝ sixteen * two_hundred_and_fifty_six.
    66
    77ndefinition testmem ≝ assembly_unlabelled_program test.
     
    1515  | Just teststatus ⇒ Just … (execute steps teststatus)].
    1616
    17 notation "'STATUS'" with precedence 90 for @{ 'status }.
    18 interpretation "status" 'status = (mk_Status ??????????).
     17notation "'STATUS' pc sfr" with precedence 90 for @{ 'status $pc $sfr }.
     18interpretation "status" 'status pc sfr = (mk_Status ? ? ? ? pc sfr ? ? ? ?).
    1919
    2020nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝
     
    142142interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
    143143
     144ndefinition dbg ≝
     145  match teststatus with
     146    [ Nothing ⇒ Nothing ?
     147    | Just s ⇒
     148      let lk ≝ lookup ? seven ([[ false; false; false ]] @@ (max four)) (low_internal_ram s) (zero ?) in
     149        Just … 〈lk, program_counter s〉
     150    ].
     151   
     152nlemma test:
     153  dbg = dbg.
     154  nnormalize;
     155  @;
     156nqed.
     157
     158nlemma 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).
     163  nnormalize;
     164  @;
     165nqed.
     166
     167ndefinition instr ≝
     168  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)))
     172    ].
     173
     174ndefinition ftchtst ≝
     175  match testfinal with
     176    [ Nothing ⇒ Nothing …
     177    | Just teststatus ⇒ Just … (next (code_memory teststatus) (program_counter teststatus))
     178    ].
     179
     180(*   
     181nlemma test5:
     182  ftchtst = ftchtst.
     183  nnormalize;
     184
     185nlemma test4:
     186  instr = instr.
     187  nnormalize;
     188  @;
     189nqed.
     190
     191nlemma test2:
     192  get_arg_8 initialise_status false ACC_A =
     193  get_arg_8 initialise_status false ACC_A.
     194  nnormalize;
     195  @;
     196nqed.
     197*)
     198
    144199nlemma do_test: testtrace = testtrace.
    145200 nnormalize in ⊢ (??%?); (* STOP HERE TO SEE THE TRACE *)
  • Deliverables/D4.1/Matita/Interpret.ma

    r374 r439  
    33
    44ndefinition sign_extension: Byte → Word ≝
    5   λb.
    6     zero eight @@ b.
     5  λc.
     6    let b ≝ get_index_v ? eight c one ? in
     7      [[ b; b; b; b; b; b; b; b ]] @@ c.
     8  nnormalize;
     9  nrepeat (napply (less_than_or_equal_monotone ?));
     10  napply (less_than_or_equal_zero);
     11nqed.
    712   
    813nlemma inclusive_disjunction_true:
  • Deliverables/D4.1/Matita/Status.ma

    r362 r439  
    848848        λindirect: True.
    849849          let register ≝ get_register s [[ false; false; i ]] in
    850           let 〈 nu, nl 〉 ≝ split ? four four register in
     850          let 〈nu, nl〉 ≝ split ? four four register in
    851851          let bit_one ≝ get_index_v … nu one ? in
    852           let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
    853           match bit_one with
    854             [ true ⇒
    855               let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
    856                 set_low_internal_ram s memory
    857             | false ⇒
    858               let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
    859                 set_high_internal_ram s memory
    860             ]
     852          let 〈ignore, three_bits〉 ≝ split ? one three nu in
     853            match bit_one with
     854              [ true ⇒
     855                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
     856                  set_low_internal_ram s memory
     857              | false ⇒
     858                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
     859                  set_high_internal_ram s memory
     860              ]
    861861      | REGISTER r ⇒ λregister: True. set_register s r v
    862862      | ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
  • Deliverables/D4.1/Matita/depends

    r436 r439  
     1Exponential.ma Nat.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Arithmetic.ma BitVector.ma Exponential.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Exponential.ma Nat.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma logic/pts.ma
     
    88DoTest.ma Assembly.ma Interpret.ma Test.ma
    99ASM.ma BitVector.ma Either.ma String.ma
    10 Vector.ma List.ma Nat.ma
    1110Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1211Char.ma logic/pts.ma
    1312Test.ma ASM.ma
     13Vector.ma List.ma Nat.ma
    1414Connectives.ma Plogic/equality.ma
    1515Bool.ma logic/pts.ma
    1616Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
    1717List.ma Maybe.ma Util.ma
     18Interpret.ma Fetch.ma Status.ma
    1819Util.ma Nat.ma
    19 Interpret.ma Fetch.ma Status.ma
     20Compare.ma logic/pts.ma
    2021BitVector.ma String.ma Vector.ma
    2122String.ma Char.ma Compare.ma List.ma
    22 Compare.ma logic/pts.ma
    2323Nat.ma Bool.ma Cartesian.ma Connectives.ma
    2424Plogic/equality.ma
Note: See TracChangeset for help on using the changeset viewer.