Changeset 1943


Ignore:
Timestamp:
May 14, 2012, 6:45:01 PM (8 years ago)
Author:
boender
Message:
  • changed 'labels okay' part of create_label_cost_map
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1942 r1943  
    10871087   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉. *)
    10881088
    1089 (*axiom eq_identifier_eq:
     1089axiom eq_identifier_eq:
    10901090  ∀tag: String.
    10911091  ∀l.
     
    10971097  ∀l, r: identifier tag.
    10981098    eq_identifier tag l r = false → (l = r → False).
    1099 *)
    11001099
    11011100(* label_map: identifier ↦ pseudo program counter *)
     
    11401139  (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)
    11411140    let 〈labels,costs〉 ≝ labels_costs in
    1142     ∀i:ℕ.lt i (|program|) →
     1141    (*∀i:ℕ.lt i (|program|) → *)
    11431142    ∀l.occurs_exactly_once ?? l program →
    1144     is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    1145     lookup ?? labels l = Some ? i
     1143    (*is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
     1144    lookup ?? labels l = Some ? i*)
     1145    bitvector_of_nat ? (lookup_def ?? labels l 0) =
     1146     address_of_word_labels_code_mem program l
    11461147  ) ≝
    11471148  λprogram.
     
    11501151    let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in
    11511152    ppc = |prefix| ∧
     1153    ∀l.occurs_exactly_once ?? l prefix →
     1154    bitvector_of_nat ? (lookup_def ?? labels l 0) =
     1155     address_of_word_labels_code_mem prefix l
     1156    (*
    11521157    ∀i:ℕ.lt i (|prefix|) →
    11531158    ∀l.occurs_exactly_once ?? l prefix →
    11541159    is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    1155     lookup … labels l = Some ? i
     1160    lookup … labels l = Some ? i *)
    11561161  )
    11571162  program
     
    11731178  -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]
    11741179 inversion label [#EQ | #l #EQ]
     1180 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta
     1181   >occurs_exactly_once_None in Hocc; @(IH2 lbl)
     1182 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)
     1183   [ #Heq #Hocc >(eq_identifier_eq … Heq)
     1184     >address_of_word_labels_code_mem_Some_hit
     1185     [ >IH1 >lookup_def_add_hit %
     1186     | <(eq_identifier_eq … Heq) in Hocc; //
     1187     ]
     1188   | #Hneq #Hocc
     1189     <address_of_word_labels_code_mem_Some_miss
     1190     [ >lookup_def_add_miss
     1191       [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq //
     1192       | % @neq_identifier_neq @Hneq
     1193       ]
     1194     | @Hocc
     1195     | >eq_identifier_sym @Hneq
     1196     ]
     1197   ]
     1198 ]
     1199(*  |       
     1200    [ @Hocc
     1201    | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
     1202    ]
    11751203 [1,2: normalize nodelta
    1176    #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    1177   [3: #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
     1204   (* #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     1205  [3: #Hi *) #lbl #Hocc (*#Hlbl*) lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
    11781206    @eq_identifier_elim
    11791207    [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
     
    12011229    ]
    12021230  ]
    1203  ]
     1231 ] *)
    12041232| @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %
    1205   #i #Hi normalize in Hi; cases (not_le_Sn_O i) #abs cases (abs Hi)
     1233  #l #abs cases (abs)
    12061234| cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *
    12071235  #_ #H @H
     
    12141242    ∀id. occurs_exactly_once ??  id (\snd pseudo_program) →
    12151243     bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id.
    1216  #pseudo_program
    1217  cases (create_label_cost_map (\snd pseudo_program)) * #label_map #cost_map
    1218  normalize nodelta elim (\snd pseudo_program)
    1219  [1:
    1220    #_ #id #absurd normalize in absurd; cases absurd
    1221  |2:
    1222    #hd #tl #inductive_hypothesis #H #id
    1223    whd in match (occurs_exactly_once ????);
    1224    whd in ⊢ (? → ???%);
    1225    whd in match (index_of ???);
    1226    inversion (instruction_matches_identifier ????) normalize nodelta
    1227    [1:
    1228      whd in ⊢ (??%? → ?); #G
    1229      lapply (H 0 ? id ??)
    1230      [1:
    1231        normalize cases hd in G; #lbl #instr normalize
    1232        cases lbl normalize try (#absurd destruct(absurd) @I)
    1233        #id' change with (eq_identifier ??? = true → ?)
    1234        @(eq_identifier_elim ? ? id id') #assm
    1235        [1:
    1236          //
    1237        |2:
    1238          lapply (eq_identifier_false … assm)
    1239          check eq_identifier
    1240          #absurd1 >eq_identifier_sym >absurd1 #absurd2 destruct(absurd2)
    1241        ]
    1242      |2:
    1243      |3:
    1244        normalize @le_S_S //
    1245      |4:
    1246        #H whd in match (lookup_def ?????);
    1247        >H normalize nodelta #_ %
    1248      ]
    1249    |2:
    1250      
    1251    ]
    1252    cases daemon
    1253 qed.
    1254 
     1244 #p @pi2
     1245qed.
     1246 
    12551247definition assembly:
    12561248 ∀p:pseudo_assembly_program.∀sigma:Word → Word × bool.list Byte × (BitVectorTrie costlabel 16) ≝
Note: See TracChangeset for help on using the changeset viewer.