Changeset 913 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 9, 2011, 10:50:05 AM (8 years ago)
Author:
boender
Message:
  • temporary commit s.t. Assembly compiles
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r907 r913  
    509509   〈labels, policy, changed〉.
    510510
    511 (* let 〈new_labels, new_policy, ch〉 =
    512  jump_expansion_policy_internal program old_labels old_policy in
    513  if changed then recurse else stop *)
    514  
    515511definition expand_relative_jump_internal:
    516512 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
     
    641637qed.
    642638
     639(* let 〈new_labels, new_policy, ch〉 =
     640 jump_expansion_policy_internal program old_labels old_policy in
     641 if changed then recurse else stop *)
     642 
    643643definition assembly_1_pseudoinstruction ≝
    644   λprogram.
    645   λpc.
     644  λprogram: pseudo_assembly_program.
     645  λpc: Word.
    646646  λlookup_labels.
    647647  λlookup_datalabels.
    648648  λi.
    649   let expansion ≝ jump_expansion_policy policy_zero program pc in
     649  let expansion ≝ long_jump (* XXX temporarily, s.t. it compiles *) in
    650650    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    651651    [ None ⇒ None ?
     
    656656        Some ? (〈len, flattened〉)
    657657    ].
    658 
     658 
    659659definition construct_datalabels ≝
    660660  λpreamble.
Note: See TracChangeset for help on using the changeset viewer.