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

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.