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 Z))) (S (S (S (S (S (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 r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
      | 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 r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
      | 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 Z))) (S (S (S (S (S (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 r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
            | 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 r ⇒ λ_.
         [ ([[false; false; false; true; true]]) @@ r ]
      | 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 r ⇒ λ_.
             [ ([[true; true; false; true; true]]) @@ r ; 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 addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
              [ REGISTER r⇒ λ_.
                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
              | INDIRECT i1 ⇒ λ_.
                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
  | INC addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
      [ ACC_A ⇒ λ_.
         [ ([[false;false;false;false;false;true;false;false]]) ]         
      | REGISTER r ⇒ λ_.
         [ ([[false;false;false;false;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
      | INDIRECT i1 ⇒ λ_.
        [ ([[false; false; false; false; false; true; true; i1]]) ]
      | DPTR ⇒ λ_.
        [ ([[true;false;true;false;false;false;true;true]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | JMP addr ⇒
     [ ([[false;true;true;true;false;false;true;true]]) ]
  | LCALL addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
      [ ADDR16 w ⇒ λ_.
         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | LJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
      [ ADDR16 w ⇒ λ_.
         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | MOV addrs ⇒
     match addrs with
      [ Left addrs ⇒
         match addrs with
          [ Left addrs ⇒
             match addrs with
              [ Left 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 r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
                          [ REGISTER r ⇒ λ_.
                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                          | INDIRECT i1 ⇒ λ_.
                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
                  | 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;register;direct;indirect;data]] x) → ? with
                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;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 ? [[data16]] x) → ? with
                  [ DATA16 w ⇒ λ_.
                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
                      [ ([[true;false;false;true;false;false;false;false]]); 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]] x) → ? with
              [ BIT_ADDR b1 ⇒ λ_.
                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
          [ BIT_ADDR b1 ⇒ λ_.
             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
  | MOVC addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
      [ ACC_DPTR ⇒ λ_.
         [ ([[true;false;false;true;false;false;true;true]]) ]
      | ACC_PC ⇒ λ_.
         [ ([[true;false;false;false;false;false;true;true]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | MOVX addrs ⇒
     match addrs with
      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
          [ EXT_INDIRECT i1 ⇒ λ_.
             [ ([[true;true;true;false;false;false;true;i1]]) ]
          | EXT_INDIRECT_DPTR ⇒ λ_.
             [ ([[true;true;true;false;false;false;false;false]]) ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
          [ EXT_INDIRECT i1 ⇒ λ_.
             [ ([[true;true;true;true;false;false;true;i1]]) ]
          | EXT_INDIRECT_DPTR ⇒ λ_.
             [ ([[true;true;true;true;false;false;false;false]]) ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
  | MUL addr1 addr2 ⇒
     [ ([[true;false;true;false;false;true;false;false]]) ]
  | NOP ⇒
     [ ([[false;false;false;false;false;false;false;false]]) ]
  | ORL 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;data;direct;indirect]] x) → ? with
             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;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;false;false;false;true;false]]); b1 ]
              | DATA b2 ⇒ λ_.
                 [ ([[false;true;false;false;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 ⇒ λ_.
             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
          | N_BIT_ADDR b1 ⇒ λ_.
             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
  | POP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
      [ DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | PUSH addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
      [ DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | RET ⇒
     [ ([[false;false;true;false;false;false;true;false]]) ]
  | RETI ⇒
     [ ([[false;false;true;true;false;false;true;false]]) ]
  | RL addr ⇒
     [ ([[false;false;true;false;false;false;true;true]]) ]
  | RLC addr ⇒
     [ ([[false;false;true;true;false;false;true;true]]) ]
  | RR addr ⇒
     [ ([[false;false;false;false;false;false;true;true]]) ]
  | RRC addr ⇒
     [ ([[false;false;false;true;false;false;true;true]]) ]
  | SETB addr ⇒     
     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
      [ CARRY ⇒ λ_.
         [ ([[true;true;false;true;false;false;true;true]]) ]
      | BIT_ADDR b1 ⇒ λ_.
         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | SJMP addr ⇒
     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
      [ RELATIVE b1 ⇒ λ_.
         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
  | SUBB addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
      [ REGISTER r ⇒ λ_.
         [ ([[true;false;false;true;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;false;true]]); b1]
      | INDIRECT i1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;true;i1]]) ]
      | DATA b1 ⇒ λ_.
         [ ([[true;false;false;true;false;true;false;false]]); b1]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | SWAP addr ⇒
     [ ([[true;true;false;false;false;true;false;false]]) ]
  | XCH addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
      [ REGISTER r ⇒ λ_.
         [ ([[true;true;false;false;true]]) @@ r ]
      | DIRECT b1 ⇒ λ_.
         [ ([[true;true;false;false;false;true;false;true]]); b1]
      | INDIRECT i1 ⇒ λ_.
         [ ([[true;true;false;false;false;true;true;i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | XCHD addr1 addr2 ⇒
     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
      [ INDIRECT i1 ⇒ λ_.
         [ ([[true;true;false;true;false;true;true;i1]]) ]
      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
  | XRL addrs ⇒
     match addrs with
      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
          [ REGISTER r ⇒ λ_.
             [ ([[false;true;true;false;true]]) @@ r ]
          | DIRECT b1 ⇒ λ_.
             [ ([[false;true;true;false;false;true;false;true]]); b1]
          | INDIRECT i1 ⇒ λ_.
             [ ([[false;true;true;false;false;true;true;i1]]) ]
          | DATA b1 ⇒ λ_.
             [ ([[false;true;true;false;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;true;false;false;false;true;false]]); b1 ]         
          | DATA b2 ⇒ λ_.
             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].

(*
let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty

let load_mem mem status = { status with code_memory = mem }
let load l = load_mem (load_code_memory l)

module StringMap = Map.Make(String);;
module IntMap = Map.Make(struct type t = int let compare = compare end);;


let assembly_jump addr_of =
 function
    `JC a1 -> `JC (addr_of a1)
  | `JNC a1 -> `JNC (addr_of a1)
  | `JB (a1,a2) -> `JB (a1,addr_of a2)
  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
  | `JZ a1 -> `JZ (addr_of a1)
  | `JNZ a1 -> `JNZ (addr_of a1)
  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
;;

let assembly (preamble,l) =
 let datalabels,_ =
  List.fold_left
   (fun (datalabels,addr) (name,size) ->
     let addr16 = vect_of_int addr `Sixteen in
      StringMap.add name addr16 datalabels, addr+size
   ) (StringMap.empty,0) preamble
 in
 let pc,labels,costs =
  List.fold_left
   (fun (pc,labels,costs) i ->
     match i with
        `Label s -> pc, StringMap.add s pc labels, costs
      | `Cost s -> pc, labels, IntMap.add pc s costs
      | `Mov (_,_) -> pc, labels, costs
      | `Jmp _ 
      | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
      | `WithLabel i ->
          let fake_addr _ = `REL (zero `Eight) in
          let fake_jump = assembly_jump fake_addr i in
          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
           assert (fake_jump = i');
           (pc + int_of_vect pc',labels, costs)
      | #instruction as i ->
        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
         assert (i = i');
         (pc + int_of_vect pc',labels, costs)
   ) (0,StringMap.empty,IntMap.empty) l
 in
  if pc >= 65536 then
   raise CodeTooLarge
  else
      List.flatten (List.map
         (function
            `Label _
          | `Cost _ -> []
          | `WithLabel i ->
              let addr_of (`Label s) =
               let addr = StringMap.find s labels in
               (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
                assert (addr < 256);
                `REL (vect_of_int addr `Eight)
              in
               assembly1 (assembly_jump addr_of i)
          | `Mov (`DPTR,s) ->
              let addrr16 = StringMap.find s datalabels in
               assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
          | `Jmp s ->
              let pc_offset = StringMap.find s labels in
                assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
          | `Call s ->
              let pc_offset = StringMap.find s labels in
                assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
          | #instruction as i -> assembly1 i) l), costs
;;
*)