Changeset 2032 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 8, 2012, 4:32:03 PM (8 years ago)
Author:
sacerdot
Message:

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

subaddressing_mode_elim redesigned from scratch and now also applied to
Policy.ma. Moreover, all daemons about that have been closed.
The new one is much simpler to apply since it behaves like a standard
elimination principle: @(subaddressing_mode_elim \ldots x) where x is
the thing to eliminate.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1946 r2032  
    693693    let c ≝ get_index_v … r 1 ? in
    694694    let d ≝ get_index_v … r 2 ? in
    695     let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     695    let 〈 un, ln 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    696696    let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
    697697    let offset ≝
     
    736736  λcode_memory:M.
    737737  λs: PreStatus M code_memory.
    738     let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in
     738    let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
    739739    let m ≝ get_index_v ?? nu O ? in
    740740    let r1 ≝ get_index_v ?? nu 1 ? in
     
    761761  λs: PreStatus M code_memory.
    762762  λv: Byte.
    763     let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in
     763    let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
    764764    let bit_zero ≝ get_index_v ?? nu O ? in
    765765    let bit_1 ≝ get_index_v ?? nu 1 ? in
     
    785785   match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with
    786786     [ DPTR ⇒ λ_:True.
    787        let 〈 bu, bl 〉 ≝ split … 8 8 v in
     787       let 〈 bu, bl 〉 ≝ vsplit … 8 8 v in
    788788       let status ≝ set_8051_sfr … s SFR_DPH bu in
    789789       let status ≝ set_8051_sfr … status SFR_DPL bl in
     
    850850      | DIRECT d ⇒
    851851        λdirect: True.
    852           let 〈 nu, nl 〉 ≝ split ? 4 4 d in
     852          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in
    853853          let bit_one ≝ get_index_v ? ? nu 0 ? in
    854           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     854          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    855855            match bit_one with
    856856              [ false ⇒
     
    861861      | INDIRECT i ⇒
    862862        λindirect: True.
    863           let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in
    864           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     863          let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in
     864          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    865865          let bit_1 ≝ get_index_v ?? bit_one_v O ? in
    866866          match  bit_1 with
     
    895895      [ DIRECT d ⇒
    896896        λdirect: True.
    897           let 〈 nu, nl 〉 ≝ split … 4 4 d in
     897          let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in
    898898          let bit_one ≝ get_index_v ? ? nu 0 ? in
    899           let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     899          let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in
    900900            match bit_one with
    901901              [ true ⇒ set_bit_addressable_sfr ?? s d v
     
    907907        λindirect: True.
    908908          let register ≝ get_register ?? s [[ false; false; i ]] in
    909           let 〈nu, nl〉 ≝ split ? 4 4 register in
     909          let 〈nu, nl〉 ≝ vsplit ? 4 4 register in
    910910          let bit_1 ≝ get_index_v … nu 0 ? in
    911           let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     911          let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    912912            match bit_1 with
    913913              [ false ⇒
     
    10041004      [ BIT_ADDR b ⇒
    10051005        λbit_addr: True.
    1006           let 〈 nu, nl 〉 ≝ split … 4 4 b in
     1006          let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in
    10071007          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1008           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     1008          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    10091009            match bit_1 with
    10101010              [ true ⇒
     
    10231023      | N_BIT_ADDR n ⇒
    10241024        λn_bit_addr: True.
    1025           let 〈 nu, nl 〉 ≝ split … 4 4 n in
     1025          let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in
    10261026          let bit_1 ≝ get_index_v ? ? nu 0 ? in
    1027           let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
     1027          let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in
    10281028            match bit_1 with
    10291029              [ true ⇒
     
    10611061    match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with
    10621062      [ BIT_ADDR b ⇒ λbit_addr: True.
    1063         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     1063        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10641064        let bit_1 ≝ get_index_v ?? nu 0 ? in
    1065         let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
     1065        let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in
    10661066        match bit_1 return λ_. ? with
    10671067          [ true ⇒
     
    10831083      | CARRY ⇒
    10841084        λcarry: True.
    1085         let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
     1085        let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in
    10861086        let bit_1 ≝ get_index_v… nu 1 ? in
    10871087        let bit_2 ≝ get_index_v… nu 2 ? in
Note: See TracChangeset for help on using the changeset viewer.