Changeset 1885


Ignore:
Timestamp:
Apr 11, 2012, 10:06:50 AM (8 years ago)
Author:
boender
Message:
  • updated assembler with new definition of occurs_exactly_once
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1870 r1885  
    11241124  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
    11251125   let 〈labels, costs〉 ≝ res in
    1126     ∀id. occurs_exactly_once id (\snd pseudo_program) →
     1126    ∀id. occurs_exactly_once ?? id (\snd pseudo_program) →
    11271127     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id) ≝
    11281128  λpseudo_program.
     
    11391139                (ppc' = length … pre)) (*∧ *)
    11401140                (tech_pc_sigma00 pseudo_program (pi1 … pol) pre = 〈ppc',pc'〉)) (*∧*)
    1141                 (∀id. occurs_exactly_once id pre →
     1141                (∀id. occurs_exactly_once ?? id pre →
    11421142                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
    11431143                (\snd pseudo_program)
     
    11921192 ∀pseudo_program.∀pol:policy pseudo_program.
    11931193   let 〈labels, costs〉 ≝ build_maps pseudo_program pol in
    1194     ∀id. occurs_exactly_once id (\snd pseudo_program) →
     1194    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    11951195     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id).
    11961196 #pseudo_program #pol @(pi2 … (build_maps0 … pol))
Note: See TracChangeset for help on using the changeset viewer.