Changeset 281


Ignore:
Timestamp:
Nov 24, 2010, 6:29:12 PM (9 years ago)
Author:
mulligan
Message:

Resolved conflicts.

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

Legend:

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

    r277 r281  
    2727ndefinition eighteen ≝ nine + nine.
    2828ndefinition nineteen ≝ ten + nine.
     29ndefinition one_hundred ≝ ten * ten.
    2930ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
     31ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
     32ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
     33ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
     34ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
     35ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
     36ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
     37ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
     38ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
     39ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
     40ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
     41ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
     42ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
     43ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
     44ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
     45ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
     46ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
     47ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
     48ndefinition two_hundred ≝ one_hundred + one_hundred.
     49ndefinition two_hundred_and_two ≝ two_hundred + two.
     50ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
     51ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
     52ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
     53ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
     54ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
     55ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    3056ndefinition two_hundred_and_fifty_six ≝
    31   one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                        
     57  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
    3258   
    3359ndefinition nat_of_bool ≝
  • Deliverables/D4.1/Matita/Assembly.ma

    r279 r281  
    1818  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
    1919
    20 
     20(*
    2121  | `ADDC (`A, `REG(r1,r2,r3)) ->
    2222     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
     
    349349 
    350350 ].
    351 
     351*)
  • Deliverables/D4.1/Matita/Bool.ma

    r268 r281  
    1111    ].
    1212   
    13 notation "hvbox(b ? t : f)"
     13notation "hvbox('if' b 'then' t 'else' f)"
    1414  non associative with precedence 83
    1515  for @{ 'if_then_else $b $t $f }.
     
    5050    [ true ⇒ false
    5151    | false ⇒ true
    52     ]. 
     52    ].
    5353 
  • Deliverables/D4.1/Matita/Cartesian.ma

    r279 r281  
    1212 with precedence 10
    1313for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
    14 
    15 (*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*)
    16 
  • Deliverables/D4.1/Matita/Status.ma

    r276 r281  
    9595 
    9696  special_function_registers_8051: Vector Byte nineteen;
    97   special_function_registers_8052: Vector Byte five
     97  special_function_registers_8052: Vector Byte five;
     98 
     99  p1_latch: Byte;
     100  p3_latch: Byte
    98101}.
    99102
     
    174177ndefinition set_program_counter ≝
    175178  λs: Status.
    176   λi: SFR8052.
    177179  λw: Word.
    178     let index ≝ sfr_8052_index i in
    179180    let old_code_memory ≝ code_memory s in
    180181    let old_low_internal_ram ≝ low_internal_ram s in
     
    358359                         (zero sixteen)
    359360                         (replicate Byte nineteen (zero eight))
    360                          (replicate Byte five (zero eight)) in
    361   status.
     361                         (replicate Byte five (zero eight))
     362                         (zero eight)
     363                         (zero eight) in
     364  set_program_counter status (bitvector_of_nat sixteen seven).
     365 
     366naxiom not_implemented: False.
     367 
     368include "Arithmetic.ma".
     369 
     370ndefinition get_bit_addressable_sfr ≝
     371  λs: Status.
     372  λn: Nat.
     373  λb: BitVector n.
     374  λl: Bool.
     375    let address ≝ nat_of_bitvector … b in
     376      if (decidable_equality address one_hundred_and_twenty_eight) then
     377        ?
     378      else if (decidable_equality address one_hundred_and_forty_four) then
     379        if l then
     380          (p1_latch s)
     381        else
     382          (get_8051_sfr s SFR_P1)
     383      else if (decidable_equality address one_hundred_and_sixty) then
     384        ?
     385      else if (decidable_equality address one_hundred_and_seventy_six) then
     386        if l then
     387          (p3_latch s)
     388        else
     389          (get_8051_sfr s SFR_P3)
     390      else if (decidable_equality address one_hundred_and_fifty_three) then
     391        get_8051_sfr s SFR_SBUF
     392      else if (decidable_equality address one_hundred_and_thirty_eight) then
     393        get_8051_sfr s SFR_TL0
     394      else if (decidable_equality address one_hundred_and_thirty_nine) then
     395        get_8051_sfr s SFR_TL1
     396      else if (decidable_equality address one_hundred_and_forty) then
     397        get_8051_sfr s SFR_TH0
     398      else if (decidable_equality address one_hundred_and_forty_one) then
     399        get_8051_sfr s SFR_TH1
     400      else if (decidable_equality address two_hundred) then
     401        get_8052_sfr s SFR_T2CON
     402      else if (decidable_equality address two_hundred_and_two) then
     403        get_8052_sfr s SFR_RCAP2L
     404      else if (decidable_equality address two_hundred_and_three) then
     405        get_8052_sfr s SFR_RCAP2H
     406      else if (decidable_equality address two_hundred_and_four) then
     407        get_8052_sfr s SFR_TL2
     408      else if (decidable_equality address two_hundred_and_five) then
     409        get_8052_sfr s SFR_TH2
     410      else if (decidable_equality address one_hundred_and_thirty_five) then
     411        get_8051_sfr s SFR_PCON
     412      else if (decidable_equality address one_hundred_and_thirty_six) then
     413        get_8051_sfr s SFR_TCON
     414      else if (decidable_equality address one_hundred_and_thirty_seven) then
     415        get_8051_sfr s SFR_TMOD
     416      else if (decidable_equality address one_hundred_and_fifty_two) then
     417        get_8051_sfr s SFR_SCON
     418      else if (decidable_equality address one_hundred_and_sixty_eight) then
     419        get_8051_sfr s SFR_IE
     420      else if (decidable_equality address one_hundred_and_eighty_four) then
     421        get_8051_sfr s SFR_IP
     422      else if (decidable_equality address one_hundred_and_twenty_nine) then
     423        get_8051_sfr s SFR_SP
     424      else if (decidable_equality address one_hundred_and_thirty) then
     425        get_8051_sfr s SFR_DPL
     426      else if (decidable_equality address one_hundred_and_thirty_one) then
     427        get_8051_sfr s SFR_DPH
     428      else if (decidable_equality address two_hundred_and_eight) then
     429        get_8051_sfr s SFR_PSW
     430      else if (decidable_equality address two_hundred_and_twenty_four) then
     431        get_8051_sfr s SFR_ACC_A
     432      else if (decidable_equality address two_hundred_and_forty) then
     433        get_8051_sfr s SFR_ACC_B
     434      else
     435        ?.
     436      ncases not_implemented.
     437nqed.
  • Deliverables/D4.1/Matita/depends

    r271 r281  
    1 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    21Status.ma Arithmetic.ma BitVectorTrie.ma
    32Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
     3Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
     6Universes.ma
    67Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    78Either.ma Bool.ma Maybe.ma Universes.ma
    8 Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
     10Char.ma Universes.ma
    1011Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    11 Char.ma Universes.ma
    1212Connectives.ma Plogic/equality.ma
    1313Bool.ma Universes.ma
     
    1515List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1616Util.ma Nat.ma
     17String.ma Char.ma List.ma
    1718BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1819Compare.ma Universes.ma
    19 String.ma Char.ma List.ma
    2020Plogic/equality.ma Universes.ma
    2121Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset for help on using the changeset viewer.