Ignore:
Timestamp:
Dec 5, 2010, 11:54:59 PM (9 years ago)
Author:
sacerdot
Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File:
1 edited

Legend:

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

    r372 r374  
    55ndefinition testmem ≝ assembly test.
    66ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.
     7ndefinition testfinal ≝ execute four (*(four * two_hundred_and_fifty_six)*) teststatus.
    88
    99notation "'STATUS'" with precedence 90 for @{ 'status }.
    1010interpretation "status" 'status = (mk_Status ??????????).
    1111
    12 (*
    13 nlemma xoo: testfinal = testfinal.
    14  nnormalize in ⊢ (??%?); @;
    15 nqed.
    16 *)
     12nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝
     13  match n with
     14    [ Z ⇒ []
     15    | S o ⇒
     16       first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
     17    ].
    1718
    18 (*
    19 nlemma test:
    20  (let status ≝
    21  load
    22   (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
    23    initialise_status
    24   in
    25    fetch (code_memory status) (program_counter status)
    26   ) = ?.
    27 ##[ nnormalize in ⊢ (??%?);
    28 *)
     19interpretation "left" 'left x = (Left ?? x).
     20interpretation "right" 'right x = (Right ?? x).
    2921
    30 (*
    31 nlemma xoo:
    32  (let testfinal ≝ testfinal in
    33  first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) =
    34  first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
    35  nnormalize in ⊢ (??%?);
    36 nqed.
     22notation < "'L' x" with precedence 70 for @{ 'left $x }.
     23notation < "'R' x" with precedence 70 for @{ 'right $x }.
    3724
    38 ndefinition is_JZ ≝
    39  λi: instruction.match i with
    40      [ Jump arg ⇒
    41         match arg with
    42          [ JZ arg ⇒
    43             match arg with
    44              [ RELATIVE arg ⇒ arg
    45              | _ ⇒ zero eight ]
    46          | _ ⇒ zero eight ]
    47      | _ ⇒ zero eight ].
     25notation < "𝟘" with precedence 90 for @{ 'zero }.
     26notation < "𝟙" with precedence 90 for @{ 'one }.
     27notation < "𝟚" with precedence 90 for @{ 'two }.
     28notation < "𝟛" with precedence 90 for @{ 'three }.
     29notation < "𝟜" with precedence 90 for @{ 'four }.
     30notation < "𝟝" with precedence 90 for @{ 'five }.
     31notation < "𝟞" with precedence 90 for @{ 'six }.
     32notation < "𝟟" with precedence 90 for @{ 'seven }.
     33notation < "𝟠" with precedence 90 for @{ 'eight }.
     34notation < "𝟡" with precedence 90 for @{ 'nine }.
     35notation < "𝔸" with precedence 90 for @{ 'a }.
     36notation < "𝔹" with precedence 90 for @{ 'b }.
     37notation < "∁" with precedence 90 for @{ 'c }.
     38notation < "𝔻" with precedence 90 for @{ 'd }.
     39notation < "𝔼" with precedence 90 for @{ 'e }.
     40notation < "𝔽" with precedence 90 for @{ 'f }.
     41
     42
     43interpretation "zero" 'zero = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
     44interpretation "one" 'one = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
     45interpretation "two" 'two = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
     46interpretation "three" 'three = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
     47interpretation "four" 'four = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
     48interpretation "five" 'five = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
     49interpretation "six" 'six = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
     50interpretation "seven" 'seven = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
     51interpretation "eight" 'eight = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
     52interpretation "nine" 'nine = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
     53interpretation "A" 'a = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
     54interpretation "B" 'b = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
     55interpretation "C" 'c = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
     56interpretation "D" 'd = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
     57interpretation "E" 'e = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
     58interpretation "F" 'f = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
     59
     60notation < "𝟘l" with precedence 90 for @{ 'zero4 $l }.
     61notation < "𝟙l" with precedence 90 for @{ 'one4 $l }.
     62notation < "𝟚l" with precedence 90 for @{ 'two4 $l }.
     63notation < "𝟛l" with precedence 90 for @{ 'three4 $l }.
     64notation < "𝟜l" with precedence 90 for @{ 'four4 $l }.
     65notation < "𝟝l" with precedence 90 for @{ 'five4 $l }.
     66notation < "𝟞l" with precedence 90 for @{ 'six4 $l }.
     67notation < "𝟟l" with precedence 90 for @{ 'seven4 $l }.
     68notation < "𝟠l" with precedence 90 for @{ 'eight4 $l }.
     69notation < "𝟡l" with precedence 90 for @{ 'nine4 $l }.
     70notation < "𝔸l" with precedence 90 for @{ 'a4 $l }.
     71notation < "𝔹l" with precedence 90 for @{ 'b4 $l }.
     72notation < "∁l" with precedence 90 for @{ 'c4 $l }.
     73notation < "𝔻l" with precedence 90 for @{ 'd4 $l }.
     74notation < "𝔼l" with precedence 90 for @{ 'e4 $l }.
     75notation < "𝔽l" with precedence 90 for @{ 'f4 $l }.
     76
     77interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     78interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     79interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     80interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     81interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     82interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     83interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     84interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     85interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     86interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     87interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     88interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     89interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     90interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     91interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     92interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     93
     94interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     95interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     96interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     97interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     98interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     99interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     100interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     101interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     102interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     103interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     104interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     105interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     106interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     107interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     108interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     109interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     110
     111interpretation "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)))).
     112interpretation "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)))).
     113interpretation "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)))).
     114interpretation "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)))).
     115interpretation "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)))).
     116interpretation "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)))).
     117interpretation "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)))).
     118interpretation "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)))).
     119interpretation "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)))).
     120interpretation "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)))).
     121interpretation "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)))).
     122interpretation "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)))).
     123interpretation "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)))).
     124interpretation "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)))).
     125interpretation "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)))).
     126interpretation "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)))).
     127
     128notation < "…" with precedence 90 for @{ 'hide }.
     129interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
    48130
    49131nlemma xoo:
    50  (let testfinal ≝ testfinal in
    51    is_JZ
    52     (first … (first … (fetch (code_memory testfinal) (program_counter testfinal))))
    53     )
    54   = zero eight.
     132 execute_trace one_hundred_and_twenty_eight teststatus =
     133 execute_trace four teststatus.
    55134 nnormalize in ⊢ (??%?);
    56 
    57 *)
    58 
     135(* nnormalize in ⊢ (???%);
     136 @.
     137nqed.
    59138
    60139nlemma xoo: program_counter testfinal = program_counter testfinal.
     
    63142 @.
    64143nqed.
     144*)
Note: See TracChangeset for help on using the changeset viewer.