Changeset 2260 for src/ASM


Ignore:
Timestamp:
Jul 25, 2012, 4:52:44 PM (7 years ago)
Author:
sacerdot
Message:

Now we use the efficient lookup_address.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2259 r2260  
    488488  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
    489489  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    490   ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
     490  ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
    491491  ∀s: PreStatus pseudo_assembly_program cm.
    492492  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
     
    943943        |3,7:
    944944          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    945           @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     945          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    946946        |2,6:
    947947          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
     
    949949        |4,8:
    950950          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
    951           @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     951          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    952952        ]
    953953      |3:
     
    15801580            |3,7:
    15811581              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1582               [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1582              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    15831583            |2,6:
    15841584              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     
    15861586            |4,8:
    15871587              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1588               [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1588              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    15891589            ]
    15901590          |*:
     
    16301630            |3,7:
    16311631              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1632               [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1632              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    16331633            |2,6:
    16341634              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     
    16361636            |4,8:
    16371637              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1638               [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1638              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    16391639            ]
    16401640          |*:
     
    16991699          |3:
    17001700            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1701             [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1701            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    17021702          |2:
    17031703            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
     
    17051705          |4:
    17061706            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1707             [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1707            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    17081708          ]
    17091709        |*:
     
    17491749          |3:
    17501750            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    1751             [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1751            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    17521752          |2:
    17531753            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     
    17551755          |4:
    17561756            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    1757             [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     1757            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    17581758          ]
    17591759        |*:
     
    20092009                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
    20102010                [1:
    2011                   @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2011                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    20122012                |2,3:
    20132013                  %
     
    20502050              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
    20512051              [1:
    2052                 @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2052                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    20532053              |2,3:
    20542054                %
     
    20612061                |2:
    20622062                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    2063                   [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2063                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    20642064                ]
    20652065              ]
     
    21612161      |2:
    21622162        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
    2163         [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2163        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    21642164      |3:
    21652165        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
    2166         [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try %
     2166        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
    21672167        @(pose … (set_clock ????)) #status #status_refl
    21682168        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    21692169        [1:
    21702170          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
    2171           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2171          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    21722172        |2:
    21732173          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
    2174           [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2174          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    21752175        ]
    21762176      ]
     
    21922192      [1:
    21932193        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
    2194         [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
     2194        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    21952195      |2:
    21962196        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
    21972197        [1:
    2198           /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
     2198          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    21992199        |2,3:
    22002200          %
     
    23142314      [1:
    23152315        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2316         [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     2316        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    23172317      |2:
    23182318        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2319         [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     2319        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    23202320      ]
    23212321    |2:
    23222322      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    23232323      [1:
    2324         @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2324        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    23252325      |*:
    23262326        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     
    23322332      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    23332333      [1:
    2334         @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2334        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    23352335      |2:
    23362336        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     
    23722372        [1:
    23732373          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
    2374           [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     2374          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    23752375        |2:
    23762376          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    2377           [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]
     2377          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
    23782378        ]
    23792379      |2:
     
    23952395              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
    23962396              [1:
    2397                 @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2397                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    23982398              |2:
    23992399                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     
    24052405              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
    24062406              [1:
    2407                 @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
     2407                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
    24082408              |2:
    24092409                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
     
    25772577    [1,3:
    25782578      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
    2579       [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2579      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
    25802580      >(get_arg_8_set_program_counter … true addr1)
    2581       [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2581      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
    25822582      @get_arg_8_pseudo_addressing_mode_ok assumption
    25832583    |2,4:
     
    25892589      [1,10:
    25902590        whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2591         [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2591        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    25922592        >low_internal_ram_set_program_counter
    25932593        [1:
     
    26002600      |2,11:
    26012601        whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2602         [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2602        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    26032603        >high_internal_ram_set_program_counter
    26042604        [1:
     
    26112611      |3,12:
    26122612        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
    2613         [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2613        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    26142614        >(external_ram_set_arg_8 ??? addr1)
    26152615        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
     
    26192619          >program_counter_set_program_counter
    26202620          >set_arg_8_set_program_counter
    2621           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2621          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    26222622          >set_clock_set_program_counter >program_counter_set_program_counter
    26232623          change with (add ??? = ?)
     
    26252625        |2:
    26262626          >set_arg_8_set_program_counter
    2627           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
     2627          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    26282628          >program_counter_set_program_counter
    26292629          >set_arg_8_set_program_counter
Note: See TracChangeset for help on using the changeset viewer.