Changeset 836 for src/ASM/Assembly.ma


Ignore:
Timestamp:
May 25, 2011, 11:43:42 AM (9 years ago)
Author:
mulligan
Message:

changes to assembly functions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r833 r836  
    544544  λi.
    545545  let expansion ≝ jump_expansion_policy program pc in
    546     match (expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i) with
     546    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
    547547    [ None ⇒ None ?
    548     | Some pseudos ⇒ Some ? (flatten ? (map ? ? assembly1 pseudos))
     548    | Some pseudos ⇒
     549      let mapped ≝ map ? ? assembly1 pseudos in
     550      let flattened ≝ flatten ? mapped in
     551      let len ≝ length ? flattened in
     552        Some ? (〈len, flattened〉)
    549553    ].
    550554
     
    588592  | _ ⇒
    589593    let pc_bv ≝ bitvector_of_nat ? program_counter in
    590     let assembled ≝ assembly_1_pseudoinstruction program pc_bv
    591                      lookup_labels lookup_datalabels i in
    592     match assembled with
     594    let pc_delta_assembled ≝
     595      assembly_1_pseudoinstruction program pc_bv
     596        lookup_labels lookup_datalabels i
     597    in
     598    match pc_delta_assembled with
    593599    [ None ⇒ None ?
    594     | Some assembled ⇒
     600    | Some pc_delta_assembled ⇒
     601      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
    595602      let code_memory ≝ load_code_memory assembled in
    596603      let pc ≝ foldr ? ? (λy. λpc.
     
    636643  ].
    637644
    638 definition assembly
     645definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16))
    639646  λp.
    640   λpc.
    641647    let 〈preamble, instr_list〉 ≝ p in
    642648    match build_maps p with
     
    651657        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    652658        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    653         let to_flatten ≝
    654          map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list
    655         in
    656          foldr ? ? (λx. λy.
     659        let result ≝ foldr ? ? (λx. λy.
    657660            match y with
    658661            [ None ⇒ None ?
    659662            | Some lst ⇒
     663              let 〈pc, y〉 ≝ lst in
     664              let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
    660665              match x with
    661666              [ None ⇒ None ?
    662               | Some x ⇒ Some ? (x @ lst)
     667              | Some x ⇒
     668                let 〈pc_delta, program〉 ≝ x in
     669                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
     670                  Some ? 〈new_pc, (program @ y)〉
    663671              ]
    664             ]) (Some ? [ ]) to_flatten ]].
     672            ]) (Some ? 〈(zero ?), [ ]〉) instr_list
     673        in
     674          match result with
     675          [ None ⇒ None ?
     676          | Some result ⇒ Some ? (〈\snd result, costs〉)
     677          ]
     678      ]
     679    ].
    665680
    666681definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.