Changeset 2221 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 20, 2012, 10:46:29 AM (7 years ago)
Author:
boender
Message:
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2199 r2221  
    624624    let 〈labels,costs〉 ≝ labels_costs in
    625625    ∀l.occurs_exactly_once ?? l program →
    626     bitvector_of_nat ? (lookup_def ?? labels l 0) =
    627      address_of_word_labels_code_mem program l
     626    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     627     address_of_word_labels_code_mem program l)
     628     (lookup_def ?? labels l 0 < |program|)
    628629  ) ≝
    629630  λprogram.
     
    633634    ppc = |prefix| ∧
    634635    ∀l.occurs_exactly_once ?? l prefix →
    635     bitvector_of_nat ? (lookup_def ?? labels l 0) =
     636    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
    636637     address_of_word_labels_code_mem prefix l)
     638     (lookup_def ?? labels l 0 < |program|))
    637639  program
    638640  (λprefix.λx.λtl.λprf.λlabels_costs_ppc.
     
    656658   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
    657659 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
    658    [ #Heq #Hocc >(eq_identifier_eq … Heq)
    659      >address_of_word_labels_code_mem_Some_hit
    660      [ >IH1 >lookup_def_add_hit %
    661      | <(eq_identifier_eq … Heq) in Hocc; //
     660   [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj
     661     [ >address_of_word_labels_code_mem_Some_hit
     662       [ >IH1 >lookup_def_add_hit %
     663       | <(eq_identifier_eq … Heq) in Hocc; //
     664       ]
     665     | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    662666     ]
    663    | #Hneq #Hocc
    664      <address_of_word_labels_code_mem_Some_miss
    665      [ >lookup_def_add_miss
    666        [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
    667        | % @neq_identifier_neq @Hneq
     667   | #Hneq #Hocc lapply (IH2 lbl ?)
     668     [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //
     669     | #IH3 @conj
     670       [ <address_of_word_labels_code_mem_Some_miss
     671         [ >lookup_def_add_miss
     672           [ @(proj1 ?? IH3)
     673           | % @neq_identifier_neq @Hneq
     674           ] 
     675         | @Hocc
     676         | >eq_identifier_sym @Hneq
     677         ]
     678       | >lookup_def_add_miss
     679         [ @(proj2 ?? IH3)
     680         | % @neq_identifier_neq @Hneq
     681         ]
    668682       ]
    669      | @Hocc
    670      | >eq_identifier_sym @Hneq
    671683     ]
    672684   ]
     
    688700 ∀pseudo_program: pseudo_assembly_program.
    689701   let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in
    690     ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    691      bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
     702    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) → And
     703     (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)
     704     (lookup_def ?? labels id 0 < |\snd pseudo_program|).
    692705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2
    693706qed.
Note: See TracChangeset for help on using the changeset viewer.