Changeset 329


Ignore:
Timestamp:
Nov 29, 2010, 1:42:00 PM (9 years ago)
Author:
mulligan
Message:

Commit to restore deleted file.

Location:
Deliverables/D4.1/Matita
Files:
8 edited

Legend:

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

    r264 r329  
    5656| Z: Char.
    5757*)
     58
     59naxiom Char: Type[0].
  • Deliverables/D4.1/Matita/Interpret.ma

    r328 r329  
     1include "Status.ma".
     2include "Fetch.ma".
     3include "Cartesian.ma".
     4include "Arithmetic.ma".
     5include "List.ma".
     6
     7ndefinition execute_1: Status → Status ≝
     8  λs.
     9    let 〈 instr_pc, ticks 〉 ≝ fetch (code_memory s) (program_counter s) in
     10    let 〈 instr, pc 〉 ≝ 〈 first … instr_pc, second … instr_pc 〉 in
     11    let s ≝ set_clock s (clock s + ticks) in
     12    let s ≝ set_program_counter s pc in
     13    let s ≝
     14      match instr with
     15        [ ADD addr1 addr2 ⇒
     16            match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
     17              [ ACC_A ⇒ λacc_a: True.
     18                match addr2 return λx. bool_to_Prop (is_in … [[ register;
     19                                                                direct;
     20                                                                indirect;
     21                                                                data ]] x) → ? with
     22                  [ REGISTER r ⇒ λregister: True.
     23                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     24                                                           (get_arg_8 s false (REGISTER r)) false in
     25                    let cy_flag ≝ get_index ? flags Z in
     26                    let ac_flag ≝ get_index ? flags one in
     27                    let ov_flag ≝ get_index ? flags two in
     28                    let s ≝ set_arg_8 s ACC_A result in
     29                      set_flags s cy_flag (Just? ac_flag) ov_flag
     30                  | DIRECT d ⇒ λdirect: True. ?
     31                  | INDIRECT i ⇒ λindirect: True. ?
     32                  | DATA d ⇒ λdata: True. ?
     33                  | _ ⇒ λother: False. ?
     34                  ] (subaddressing_modein … addr2)
     35            | _ ⇒ λother: False. ?
     36            ] (subaddressing_modein … addr1)
     37        | _ ⇒ s
     38        ]
     39    in
     40      s.
     41   
     42   
  • Deliverables/D4.1/Matita/List.ma

    r260 r329  
    77include "Bool.ma".
    88include "Nat.ma".
    9 (* include "Maybe.ma". *)
     9include "Maybe.ma".
    1010include "Plogic/equality.ma".
    1111
     
    3838 
    3939(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     40(* Building lists from scratch                                                *)
     41(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     42
     43nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
     44  match n with
     45    [ Z ⇒ Empty A
     46    | S o ⇒ a :: replicate A o a
     47    ].
     48   
     49nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
     50  match l with
     51    [ Empty ⇒ m
     52    | Cons hd tl ⇒ hd :: (append A tl m)
     53    ].
     54   
     55notation "hvbox(l break @ r)"
     56  right associative with precedence 47
     57  for @{ 'append $l $r }.   
     58 
     59interpretation "List append" 'append = (append ?). 
     60 
     61(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     62(* Other manipulations.                                                       *)
     63(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     64
     65nlet rec length (A: Type[0]) (l: List A) on l ≝
     66  match l with
     67    [ Empty ⇒ Z
     68    | Cons hd tl ⇒ S $ length A tl
     69    ].
     70   
     71nlet rec reverse (A: Type[0]) (l: List A) on l ≝
     72  match l with
     73    [ Empty ⇒ Empty A
     74    | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
     75    ].
     76 
     77(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    4078(* Lookup.                                                                    *)
    4179(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    42    
    43 (*   
    44 nlet rec get_index (A: Type[0]) (l: List A) (n: Nat) on n ≝
     80
     81nlet rec get_index (A: Type[0]) (l: List A)
     82                   (n: Nat) (lt: n < length ? l) on n: A ≝
     83  match n return λx. x < length ? l → A with
     84    [ Z ⇒
     85      match l return λx. Z < length ? x → A with
     86        [ Empty ⇒ λabsd: Z < Z. ?
     87        | Cons hd tl ⇒ λp. hd
     88        ]
     89    | S o ⇒
     90      match l return λx. S o < length ? x → A with
     91        [ Empty ⇒ λabsd: S o < Z. ?
     92        | Cons hd tl ⇒ λp. get_index A tl o ?
     93        ]
     94    ] ?.
     95    ##[##1:
     96        nassumption;
     97    ##|##2:
     98        ncases (nothing_less_than_Z Z);
     99        #K;
     100        ncases (K absd);
     101    ##|##3:
     102        ncases (nothing_less_than_Z (S o));
     103        #K;
     104        ncases (K absd);
     105    ##| ncases (less_than_monoton);
     106   
     107   
     108nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝
    45109  match n with
    46110    [ Z ⇒
     
    58122interpretation "List get_index" 'get_index l n = (get_index ? l n).
    59123
    60 nlet rec set_index (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
     124nlet rec set_index_weak (A: Type[0]) (l: List A) (n: Nat) (a: A) on n ≝
    61125  match n with
    62126    [ Z ⇒
     
    85149          | Cons hd tl ⇒ drop A tl o
    86150          ]
    87     ].
    88 *)
    89    
    90 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    91 (* Building lists from scratch                                                *)
    92 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    93 
    94 nlet rec replicate (A: Type[0]) (n: Nat) (a: A) on n ≝
    95   match n with
    96     [ Z ⇒ Empty A
    97     | S o ⇒ a :: replicate A o a
    98     ].
    99    
    100 nlet rec append (A: Type[0]) (l: List A) (m: List A) on l ≝
    101   match l with
    102     [ Empty ⇒ m
    103     | Cons hd tl ⇒ hd :: (append A tl m)
    104     ].
    105    
    106 notation "hvbox(l break @ r)"
    107   right associative with precedence 47
    108   for @{ 'append $l $r }.   
    109  
    110 interpretation "List append" 'append = (append ?).   
    111 
    112 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    113 (* Other manipulations.                                                       *)
    114 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    115 
    116 nlet rec length (A: Type[0]) (l: List A) on l ≝
    117   match l with
    118     [ Empty ⇒ Z
    119     | Cons hd tl ⇒ S $ length A tl
    120     ].
    121    
    122 nlet rec reverse (A: Type[0]) (l: List A) on l ≝
    123   match l with
    124     [ Empty ⇒ Empty A
    125     | Cons hd tl ⇒ reverse A tl @ (hd :: Empty A)
    126     ].
     151    ]. 
    127152
    128153(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Nat.ma

    r277 r329  
    212212(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    213213
     214naxiom succ_less_than_injective:
     215  ∀m, n: Nat.
     216    less_than_p (S m) (S n) → m < n.
     217   
     218naxiom nothing_less_than_Z:
     219  ∀m: Nat.
     220    ¬(m < Z).
     221   
    214222nlemma less_than_or_equal_zero:
    215223  ∀n: Nat.
  • Deliverables/D4.1/Matita/Status.ma

    r317 r329  
    9898 
    9999  p1_latch: Byte;
    100   p3_latch: Byte
     100  p3_latch: Byte;
     101 
     102  clock: Time
    101103}.
    102104
     
    108110  ∀i: SFR8052.
    109111    sfr_8052_index i < five.
     112   
     113ndefinition set_clock ≝
     114  λs: Status.
     115  λt: Time.
     116    let old_code_memory ≝ code_memory s in
     117    let old_low_internal_ram ≝ low_internal_ram s in
     118    let old_high_internal_ram ≝ high_internal_ram s in
     119    let old_external_ram ≝ external_ram s in
     120    let old_program_counter ≝ program_counter s in
     121    let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
     122    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
     123    let old_p1_latch ≝ p1_latch s in   
     124    let old_p3_latch ≝ p3_latch s in
     125      mk_Status old_code_memory
     126                old_low_internal_ram
     127                old_high_internal_ram
     128                old_external_ram
     129                old_program_counter
     130                old_special_function_registers_8051
     131                old_special_function_registers_8052
     132                old_p1_latch
     133                old_p3_latch
     134                t.
    110135   
    111136ndefinition set_p1_latch ≝
     
    120145    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    121146    let old_p3_latch ≝ p3_latch s in
     147    let old_clock ≝ clock s in
    122148      mk_Status old_code_memory
    123149                old_low_internal_ram
     
    128154                old_special_function_registers_8052
    129155                b
    130                 old_p3_latch.
     156                old_p3_latch
     157                old_clock.
    131158
    132159ndefinition set_p3_latch ≝
     
    141168    let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
    142169    let old_p1_latch ≝ p1_latch s in
     170    let old_clock ≝ clock s in
    143171      mk_Status old_code_memory
    144172                old_low_internal_ram
     
    149177                old_special_function_registers_8052
    150178                old_p1_latch
    151                 b.
     179                b
     180                old_clock.
    152181
    153182ndefinition get_8051_sfr ≝
     
    185214    let old_p1_latch ≝ p1_latch s in
    186215    let old_p3_latch ≝ p3_latch s in
     216    let old_clock ≝ clock s in
    187217      mk_Status old_code_memory
    188218                old_low_internal_ram
     
    193223                old_special_function_registers_8052
    194224                old_p1_latch
    195                 old_p3_latch.
     225                old_p3_latch
     226                old_clock.
    196227    napply (sfr8051_index_nineteen i).
    197228nqed.
     
    213244    let old_p1_latch ≝ p1_latch s in
    214245    let old_p3_latch ≝ p3_latch s in
     246    let old_clock ≝ clock s in
    215247      mk_Status old_code_memory
    216248                old_low_internal_ram
     
    221253                new_special_function_registers_8052
    222254                old_p1_latch
    223                 old_p3_latch.
     255                old_p3_latch
     256                old_clock.
    224257    napply (sfr8052_index_five i).
    225258nqed.
     
    236269    let old_p1_latch ≝ p1_latch s in
    237270    let old_p3_latch ≝ p3_latch s in
     271    let old_clock ≝ clock s in
    238272      mk_Status old_code_memory
    239273                old_low_internal_ram
     
    244278                old_special_function_registers_8052
    245279                old_p1_latch
    246                 old_p3_latch.
     280                old_p3_latch
     281                old_clock.
    247282               
    248283ndefinition set_code_memory ≝
     
    257292    let old_p1_latch ≝ p1_latch s in
    258293    let old_p3_latch ≝ p3_latch s in
     294    let old_clock ≝ clock s in
    259295      mk_Status r
    260296                old_low_internal_ram
     
    265301                old_special_function_registers_8052
    266302                old_p1_latch
    267                 old_p3_latch.
     303                old_p3_latch
     304                old_clock.
    268305               
    269306ndefinition set_low_internal_ram ≝
     
    278315    let old_p1_latch ≝ p1_latch s in
    279316    let old_p3_latch ≝ p3_latch s in
     317    let old_clock ≝ clock s in
    280318      mk_Status old_code_memory
    281319                r
     
    286324                old_special_function_registers_8052
    287325                old_p1_latch
    288                 old_p3_latch.
     326                old_p3_latch
     327                old_clock.
    289328               
    290329ndefinition set_high_internal_ram ≝
     
    300339    let old_p1_latch ≝ p1_latch s in
    301340    let old_p3_latch ≝ p3_latch s in
     341    let old_clock ≝ clock s in
    302342      mk_Status old_code_memory
    303343                old_low_internal_ram
     
    308348                old_special_function_registers_8052
    309349                old_p1_latch
    310                 old_p3_latch.
     350                old_p3_latch
     351                old_clock.
    311352               
    312353ndefinition set_external_ram ≝
     
    321362    let old_p1_latch ≝ p1_latch s in
    322363    let old_p3_latch ≝ p3_latch s in
     364    let old_clock ≝ clock s in
    323365      mk_Status old_code_memory
    324366                old_low_internal_ram
     
    329371                old_special_function_registers_8052
    330372                old_p1_latch
    331                 old_p3_latch.
     373                old_p3_latch
     374                old_clock.
    332375               
    333376naxiom less_than_or_equal_monotone:
     
    467510                         (replicate Byte five (zero eight))     (* 8052 SFR. *)
    468511                         (zero eight)                           (* P1 latch. *)
    469                          (zero eight) in                        (* P3 latch. *)
    470   set_program_counter status (bitvector_of_nat sixteen seven).
     512                         (zero eight)                           (* P3 latch. *)
     513                         Z                                      (* Clock.    *)
     514  in
     515    set_program_counter status (bitvector_of_nat sixteen seven).
    471516 
    472517naxiom not_implemented: False.
     
    650695      set_low_internal_ram s new_low_internal_ram.
    651696     
     697alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".
    652698ndefinition read_at_stack_pointer ≝
    653699  λs: Status.
  • Deliverables/D4.1/Matita/String.ma

    r264 r329  
    22include "List.ma".
    33
    4 (*ndefinition String ≝ List Char.*)
    5 naxiom String: Type[0].
     4ndefinition String ≝ List Char.
  • Deliverables/D4.1/Matita/Vector.ma

    r328 r329  
    3535(* Lookup.                                                                    *)
    3636(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    37 
    38 naxiom succ_less_than_injective:
    39   ∀m, n: Nat.
    40     less_than_p (S m) (S n) → m < n.
    41    
    42 naxiom nothing_less_than_Z:
    43   ∀m: Nat.
    44     ¬(m < Z).
    4537
    4638nlet rec get_index (A: Type[0]) (n: Nat)
  • Deliverables/D4.1/Matita/depends

    r328 r329  
    1414Bool.ma Universes.ma
    1515Assembly.ma ASM.ma
    16 List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     16List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     17Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma
    1718Util.ma Nat.ma
    1819Compare.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.