include "ASM.ma".

ndefinition assembly1 ≝
 λi: instruction.match i with
  [ ACALL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
      [ ADDR11 w ⇒ λ_.
         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | ADD addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ]
      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | ADDC addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;true;true;r1;r2;r2]]) ]
      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | AJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
      [ ADDR11 w ⇒ λ_.
         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | ANL addrs ⇒
     match addrs with
      [ Left addrs ⇒ match addrs with
         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
            [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;true;true;r1;r2;r2]]) ]
            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
         | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
            let b1 ≝
             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
              [ DIRECT b1 ⇒ λ_.b1
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
         ]
      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
  | CLR addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[true; true; true; false; false; true; false; false]]) ]
      | CARRY ⇒ λ_.
         [ ([[true; true; false; false; false; false; true; true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | CPL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[true; true; true; true; false; true; false; false]]) ]
      | CARRY ⇒ λ_.
         [ ([[true; false; true; true; false; false; true; true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | DA addr ⇒
     [ ([[true; true; false; true; false; true; false; false]]) ]
  | DEC addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[false; false; false; true; false; true; false; false]]) ]
      | REGISTER r1 r2 r3 ⇒ λ_.
         [ ([[false; false; false; true; true; r1; r2; r3]]) ]
      | DIRECT b1 ⇒ λ_.
         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
      | INDIRECT i1 ⇒ λ_.
         [ ([[false; false; false; true; false; true; true; i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | DIV addr1 addr2 ⇒
     [ ([[true;false;false;false;false;true;false;false]]) ]
  | Jump j ⇒
     match j with
      [ DJNZ addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
          [ REGISTER r1 r2 r3 ⇒ λ_.
             [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ]
          | DIRECT b1 ⇒ λ_.
             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JC addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JNC addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JZ addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JNZ addr ⇒
         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
          [ RELATIVE b1 ⇒ λ_.
             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
      | JB addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JNB addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | JBC addr1 addr2 ⇒
         let b2 ≝
          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b2 ⇒ λ_. b2
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
      | CJNE addrs addr3 ⇒
         let b3 ≝
          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
           [ RELATIVE b3 ⇒ λ_. b3
           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
         match addrs with
          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
              [ DIRECT b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
              [ DATA b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
             let b2 ≝
              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
               [ DATA b2 ⇒ λ_. b2
               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
              [ DIRECT b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
              [ DATA b1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)

          ]
      | _ ⇒ [ ]
      ]
  | _ ⇒ [ ]].

(*
  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]


  | `INC `A ->
    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
  | `INC (`REG(r1,r2,r3)) ->
    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
  | `INC (`DIRECT b1) ->
    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
  | `INC (`INDIRECT i1) ->
    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
  | `INC `DPTR ->
    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
  | `JMP `IND_DPTR ->
    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
  | `LCALL (`ADDR16 w) ->
      let (b1,b2) = from_word w in
        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
  | `LJMP (`ADDR16 w) ->
      let (b1,b2) = from_word w in
        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
  | `MOV (`U1 (`A, `DIRECT b1)) ->
    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
  | `MOV (`U1 (`A, `INDIRECT i1)) ->
    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
  | `MOV (`U1 (`A, `DATA b1)) ->
    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
  | `MOV (`U3 (`DIRECT b1, `A)) ->
    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
  | `MOV (`U2 (`INDIRECT i1, `A)) ->
    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
  | `MOV (`U5 (`C, `BIT b1)) ->
    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
  | `MOV (`U6 (`BIT b1, `C)) ->
    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
    let (b1,b2) = from_word w in
      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
  | `MOVC (`A, `A_DPTR) ->
    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
  | `MOVC (`A, `A_PC) ->
    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
  | `MUL(`A, `B) ->
    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
  | `NOP ->
    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
  | `ORL (`U1(`A, `DIRECT b1)) ->
    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
  | `ORL (`U1(`A, `INDIRECT i1)) ->
    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
  | `ORL (`U1(`A, `DATA b1)) ->
    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
  | `ORL (`U2(`DIRECT b1, `A)) ->
    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
  | `ORL (`U3 (`C, `BIT b1)) ->
    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
  | `ORL (`U3 (`C, `NBIT b1)) ->
    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
  | `POP (`DIRECT b1) ->
    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
  | `PUSH (`DIRECT b1) ->
    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
  | `RET ->
    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
  | `RETI ->
    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
  | `RL `A ->
    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
  | `RLC `A ->
    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
  | `RR `A ->
    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
  | `RRC `A ->
    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
  | `SETB `C ->
    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
  | `SETB (`BIT b1) ->
    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
  | `SJMP (`REL b1) ->
    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
  | `SUBB (`A, `REG(r1,r2,r3)) ->
    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
  | `SUBB (`A, `DIRECT b1) ->
    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
  | `SUBB (`A, `INDIRECT i1) ->
    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
  | `SUBB (`A, `DATA b1) ->
    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
  | `SWAP `A ->
    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
  | `XCH (`A, `REG(r1,r2,r3)) ->
    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
  | `XCH (`A, `DIRECT b1) ->
    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
  | `XCH (`A, `INDIRECT i1) ->
    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
  | `XCHD(`A, `INDIRECT i1) ->
    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
  | `XRL(`U1(`A, `DIRECT b1)) ->
    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
  | `XRL(`U1(`A, `INDIRECT i1)) ->
    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
  | `XRL(`U1(`A, `DATA b1)) ->
    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
  | `XRL(`U2(`DIRECT b1, `A)) ->
    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
;;



nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
   elem:> A;
   witness: T elem
}.

interpretation "Sigma" 'sigma T = (Sigma ? T). 

naxiom daemon: False.

naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].

ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
 ≝
 [mk_Cartesian ??
   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
     (λl.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ?    (decode_register l) ?));
  mk_Cartesian ??
   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
     (λl.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
ncases daemon.
nqed.


naxiom decode_register: List Bool → [reg].
naxiom decode_direct: List Bool → [direct].

ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
 ≝
 [mk_Cartesian ??
   [ false; false; true; false; true]
     (λl.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ?    (decode_register l) ?));
  mk_Cartesian ??
   [ false; false; true; false; true]
     (λl.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
ncases daemon.
nqed.


ndefinition decode_tbl1:
 List (List Bool × Σaddr:all_types. [addr] → Instruction)
 ≝
 [mk_Cartesian ??
   [ false; false; true; false; true]
   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
     reg
     (λa.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ? a ?))) ].
ncases daemon.
nqed.
             
ndefinition decode_tbl2:
 List (List Bool × Σaddr:all_types. [addr] → Instruction)
 ≝
 [mk_Cartesian ??
   [ false; false; true; false; false; true; false; true]
   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
     direct
     (λa.
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ?     a ?))) ].
ncases daemon.
nqed.

ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.

decode_addr_mode; ∀addr:all_types. List Bool → [addr].

decode ≝
 λl:List Bit.
  List.iter
   (fun l0 addr mk_f →
     match split_prefix l l0 with
      [ None ⇒ ...
      | Some r ⇒ mk_f (decode_addr_mode r) ] 
      
   ) decode_tbl

encode ≝

ndefinition decode_tbl:
 List (List Bool × Σaddr:all_types. [addr] → Instruction)
 ≝
 [mk_Cartesian ??
   [ False; False; True; False; True]
   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
     reg
     (λa:subaddressing_mode ? [reg].
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ?     a ?)));
  mk_Cartesian ??
   [ False; False; True; False; False; True; False; True]
   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
     direct
     (λa:subaddressing_mode ? [direct].
       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
             (mk_subaddressing_mode ? ?     a ?)))
 ].
nnormalize; 
 
 ].
*)