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

Changes to get everything to compile.

File:
1 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 *)
Note: See TracChangeset for help on using the changeset viewer.