Ignore:
Timestamp:
Dec 15, 2010, 6:38:59 PM (9 years ago)
Author:
mulligan
Message:
  • README updated
  • Test and DoTest? fixed to work on assembly_program
  • assembly function for labelled programs avoided because of efficiency issues
File:
1 edited

Legend:

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

    r403 r431  
    33include "Assembly.ma".
    44
    5 ndefinition testmem ≝ assembly test.
    6 ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute four (*(four * two_hundred_and_fifty_six)*) teststatus.
     5ndefinition steps ≝ one_hundred_and_twenty_eight.
     6
     7ndefinition testmem ≝ assembly 〈[ ], test〉.
     8ndefinition teststatus ≝
     9 match testmem with
     10  [ Nothing ⇒ Nothing …
     11  | Just testmem ⇒ Just … (load (first … testmem) initialise_status)].
     12ndefinition testfinal ≝
     13 match teststatus with
     14  [ Nothing ⇒ Nothing …
     15  | Just teststatus ⇒ Just … (execute steps teststatus)].
    816
    917notation "'STATUS'" with precedence 90 for @{ 'status }.
     
    1624       first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
    1725    ].
     26
     27ndefinition testtrace ≝
     28 match teststatus with
     29  [ Nothing ⇒ Nothing …
     30  | Just teststatus ⇒ Just … (execute_trace steps teststatus)].
    1831
    1932interpretation "left" 'left x = (Left ?? x).
     
    129142interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
    130143
    131 nlemma xoo:
    132  execute_trace one_hundred_and_twenty_eight teststatus =
    133  execute_trace eight teststatus.
    134  nnormalize in ⊢ (??%?);
    135 (* nnormalize in ⊢ (???%);
     144nlemma do_test: testtrace = testtrace.
     145 nnormalize in ⊢ (??%?); (* STOP HERE TO SEE THE TRACE *)
     146 nnormalize;
    136147 @.
    137148nqed.
    138 
    139 nlemma xoo: program_counter testfinal = program_counter testfinal.
    140  nnormalize in ⊢ (??%?);
    141  nnormalize in ⊢ (???%);
    142  @.
    143 nqed.
    144 *)
Note: See TracChangeset for help on using the changeset viewer.