Changeset 357


Ignore:
Timestamp:
Dec 1, 2010, 11:27:04 PM (9 years ago)
Author:
sacerdot
Message:
  • stupid bug fixed in BitVectorTrie?
  • dependencies minimized, dead code removed
Location:
Deliverables/D4.1/Matita
Files:
1 deleted
15 edited

Legend:

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

    r316 r357  
    11include "Either.ma".
    2 include "BitVectorTrie.ma".
     2include "BitVector.ma".
    33include "String.ma".
    44
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r351 r357  
    1 include "Universes.ma".
    2 include "Plogic/equality.ma".
    3 include "Connectives.ma".
    4 include "Nat.ma".
    51include "Exponential.ma".
    6 include "Bool.ma".
    72include "BitVector.ma".
    8 include "List.ma".
    93
    10 ndefinition one ≝ S Z.
    11 ndefinition two ≝ (S(S(Z))).
    12 ndefinition three ≝ two + one.
    13 ndefinition four ≝ two + two.
    14 ndefinition five ≝ three + two.
    15 ndefinition six ≝ three + three.
    16 ndefinition seven ≝ three + four.
    17 ndefinition eight ≝ four + four.
    18 ndefinition nine ≝ five + four.
    19 ndefinition ten ≝ five + five.
    20 ndefinition eleven ≝ six + five.
    21 ndefinition twelve ≝ six + six.
    22 ndefinition thirteen ≝ seven + six.
    23 ndefinition fourteen ≝ seven + seven.
    24 ndefinition fifteen ≝ eight + seven.
    25 ndefinition sixteen ≝ eight + eight.
    26 ndefinition seventeen ≝ nine + eight.
    27 ndefinition eighteen ≝ nine + nine.
    28 ndefinition nineteen ≝ ten + nine.
    29 ndefinition twenty_four ≝ sixteen + eight.
    30 ndefinition thirty_two ≝ sixteen + sixteen.
    31 ndefinition one_hundred ≝ ten * ten.
    32 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
    33 ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
    34 ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
    35 ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
    36 ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
    37 ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
    38 ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
    39 ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
    40 ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
    41 ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
    42 ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
    43 ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
    44 ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
    45 ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
    46 ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
    47 ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
    48 ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
    49 ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
    50 ndefinition two_hundred ≝ one_hundred + one_hundred.
    51 ndefinition two_hundred_and_two ≝ two_hundred + two.
    52 ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
    53 ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
    54 ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
    55 ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
    56 ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
    57 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    58 ndefinition two_hundred_and_fifty_six ≝
    59   one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
    60    
    614ndefinition nat_of_bool ≝
    625  λb: Bool.
  • Deliverables/D4.1/Matita/BitVector.ma

    r353 r357  
    66(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    77
    8 include "Universes.ma".
    9 
    108include "Vector.ma".
    11 include "List.ma".
    12 include "Nat.ma".
    13 include "Bool.ma".
    149
    1510(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r352 r357  
    11include "BitVector.ma".
    2 (*include "Compare.ma".*)
    32include "Bool.ma".
    43include "Maybe.ma".
     
    2423        | Node h l r ⇒
    2524           match hd with
    26              [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
    27              | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
     25             [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
     26             | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
    2827             ]
    2928        | Stub s ⇒ λ_. a
  • Deliverables/D4.1/Matita/DoTest.ma

    r355 r357  
    1515*)
    1616
     17(*
     18nlemma test:
     19 (let status ≝
     20 load
     21  (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
     22   initialise_status
     23  in
     24   fetch (code_memory status) (program_counter status)
     25  ) = ?.
     26##[ nnormalize in ⊢ (??%?);
     27*)
     28
     29
    1730nlemma xoo:
    18  fetch (code_mem testfinal) (program_counter testfinal) =
    19  fetch (code_mem testfinal) (program_counter testfinal).
     31 fetch (code_memory testfinal) (program_counter testfinal) =
     32 fetch (code_memory testfinal) (program_counter testfinal).
    2033 nnormalize in ⊢ (??%?); @;
    2134nqed.
    22 
     35*)
    2336
    2437nlemma xoo: program_counter testfinal = program_counter testfinal.
  • Deliverables/D4.1/Matita/Either.ma

    r268 r357  
    11include "Bool.ma".
    2 include "Maybe.ma".
    3 
    4 include "Universes.ma".
    52
    63ninductive Either (A: Type[0]) (B: Type[0]): Type[0] ≝
  • Deliverables/D4.1/Matita/Exponential.ma

    r351 r357  
    44
    55include "Nat.ma".
    6 
    7 include "Plogic/equality.ma".
    8 include "Connectives.ma".
    96
    107(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Interpret.ma

    r351 r357  
    11include "Status.ma".
    22include "Fetch.ma".
    3 include "Cartesian.ma".
    4 include "Arithmetic.ma".
    5 include "List.ma".
    63
    74ndefinition sign_extension: Byte → Word ≝
  • Deliverables/D4.1/Matita/List.ma

    r356 r357  
    44
    55include "Util.ma".
    6 include "Universes.ma".
    7 include "Bool.ma".
    8 include "Nat.ma".
    96include "Maybe.ma".
    10 include "Plogic/equality.ma".
    117
    128(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/Maybe.ma

    r260 r357  
    11include "Bool.ma".
    2 
    3 include "Universes.ma".
    42include "Plogic/equality.ma".
    53
  • Deliverables/D4.1/Matita/Nat.ma

    r352 r357  
    44include "Cartesian.ma".
    55include "Bool.ma".
    6 
    76include "Connectives.ma".
    87
     
    655654 #m n; napply less_than_b_elim.
    656655nqed.
     656
     657(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     658(* Numbers.                                                                   *)
     659(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     660
     661ndefinition one ≝ S Z.
     662ndefinition two ≝ (S(S(Z))).
     663ndefinition three ≝ two + one.
     664ndefinition four ≝ two + two.
     665ndefinition five ≝ three + two.
     666ndefinition six ≝ three + three.
     667ndefinition seven ≝ three + four.
     668ndefinition eight ≝ four + four.
     669ndefinition nine ≝ five + four.
     670ndefinition ten ≝ five + five.
     671ndefinition eleven ≝ six + five.
     672ndefinition twelve ≝ six + six.
     673ndefinition thirteen ≝ seven + six.
     674ndefinition fourteen ≝ seven + seven.
     675ndefinition fifteen ≝ eight + seven.
     676ndefinition sixteen ≝ eight + eight.
     677ndefinition seventeen ≝ nine + eight.
     678ndefinition eighteen ≝ nine + nine.
     679ndefinition nineteen ≝ ten + nine.
     680ndefinition twenty_four ≝ sixteen + eight.
     681ndefinition thirty_two ≝ sixteen + sixteen.
     682ndefinition one_hundred ≝ ten * ten.
     683ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
     684ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
     685ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
     686ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
     687ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
     688ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
     689ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
     690ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
     691ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
     692ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
     693ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
     694ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
     695ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
     696ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
     697ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
     698ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
     699ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
     700ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
     701ndefinition two_hundred ≝ one_hundred + one_hundred.
     702ndefinition two_hundred_and_two ≝ two_hundred + two.
     703ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
     704ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
     705ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
     706ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
     707ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
     708ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
     709ndefinition two_hundred_and_fifty_six ≝
     710  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
  • Deliverables/D4.1/Matita/Status.ma

    r354 r357  
    516516 
    517517naxiom not_implemented: False.
    518  
    519 include "Arithmetic.ma".
    520518 
    521519ndefinition get_bit_addressable_sfr ≝
  • Deliverables/D4.1/Matita/Test.ma

    r354 r357  
    1 include "Assembly.ma".
     1include "ASM.ma".
    22
    33ndefinition test: List instruction ≝
  • Deliverables/D4.1/Matita/Vector.ma

    r352 r357  
    44(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    55
    6 include "Util.ma".
    7 
    86include "Nat.ma".
    97include "List.ma".
    10 include "Cartesian.ma".
    11 include "Maybe.ma".
    12 include "Plogic/equality.ma".
    138
    149(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • Deliverables/D4.1/Matita/depends

    r355 r357  
    1 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
     1Arithmetic.ma BitVector.ma Exponential.ma
    22Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
     3Exponential.ma Nat.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
    6 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    7 Either.ma Bool.ma Maybe.ma Universes.ma
     6Maybe.ma Bool.ma Plogic/equality.ma
     7Either.ma Bool.ma
    88Universes.ma
    9 DoTest.ma Test.ma
    10 ASM.ma BitVectorTrie.ma Either.ma String.ma
    11 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
     9DoTest.ma Interpret.ma Test.ma
     10ASM.ma BitVector.ma Either.ma String.ma
     11Vector.ma List.ma Nat.ma
    1212Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1313Char.ma Universes.ma
    14 Test.ma Assembly.ma
     14Test.ma ASM.ma
    1515Connectives.ma Plogic/equality.ma
    1616Bool.ma Universes.ma
    1717Assembly.ma ASM.ma
    18 List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     18List.ma Maybe.ma Util.ma
    1919Util.ma Nat.ma
    20 Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma
    21 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    22 Compare.ma Universes.ma
     20Interpret.ma Fetch.ma Status.ma
     21BitVector.ma Vector.ma
    2322String.ma Char.ma List.ma
    2423Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.