include "Universes.ma".
include "Equality.ma".
include "Either.ma".
include "BitVector.ma".
include "BitVectorTrie.ma".

ninductive all_types : Type[0] ≝
   reg: all_types | direct: all_types | indirect:all_types | data:all_types
   | acc: all_types | rel: all_types.

interpretation "Cartesian" 'product A B = (Cartesian A B).
interpretation "Either" 'plus A B = (Either A B).

ninductive addressing_mode: Type[0] ≝
  DIRECT: Byte → addressing_mode
| INDIRECT: Bit → addressing_mode
| EXTINDIRECT: Bit → addressing_mode
| REGISTER: Bit → Bit → Bit → addressing_mode
| ACCUMULATORA: addressing_mode
| ACCUMULATORB: addressing_mode
| DPOINTER: addressing_mode
| DATA: Byte → addressing_mode
| DATA16: Word → addressing_mode
| ACCUMULATORDPOINTER: addressing_mode
| ACCUMULATORPROGRAMCOUNTER: addressing_mode
| EXTERNALINDIRECTDPOINTER: addressing_mode
| INDIRECTDPOINTER: addressing_mode
| CARRY: addressing_mode
| BIT: Bit → addressing_mode
| COMPLEMENTBITADDRESS: Bit → addressing_mode
| RELATIVE: Byte → addressing_mode
| ADDRESS11: Word11 → addressing_mode
| ADDRESS16: Word → addressing_mode.

(* to avoid expansion... *)
nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
  match d with
   [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True | _ ⇒ False ]
   | data ⇒ match A with [ DATA _ ⇒ True | _ ⇒ False ]
   | rel ⇒ match A with [ RELATIVE _ ⇒ True | _ ⇒ False ]
   | acc ⇒ match A with [ ACCUMULATORA ⇒ True | _ ⇒ False ]
   | direct ⇒ match A with [ DIRECT _ ⇒ True | _ ⇒ False ]
   | indirect ⇒ match A with [ INDIRECT _ ⇒ True | _ ⇒ False ]].

interpretation "Bool" 'or a b = (inclusive_disjunction a b).

nlet rec is_in n (l: Vector all_types (S n)) (A:addressing_mode) on l : Bool ≝
 match l return λm.λ_:Vector all_types m .∀K:m=S n.Bool with
  [ Empty ⇒ λK.⊥
  | Cons m he (tl: Vector all_types m) ⇒ λ_.
     match m return λz.m = z → Bool with
      [ Z ⇒ λ_.is_a he A
      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
##[##4: #x; ncases K; napply x ]
//; ndestruct.
nqed.

nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝
 { subaddressing_modeel:> addressing_mode;
   subaddressing_modein:
    match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop) | False ⇒ (? : Prop) ]
 }.
##[ napply True | napply False ]
nqed.

ncoercion subaddressing_mode : ∀n.∀l:Vector all_types (S n).Type[0]
 ≝ subaddressing_mode on _l: Vector all_types (S ?) to Type[0].

(*
ncoercion mk_subaddressing_mode :
 ∀n.∀l:Vector all_types (S n).∀a:addressing_mode.
  ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True | False ⇒ False]*).subaddressing_mode n l
 ≝ mk_subaddressing_mode on _a:addressing_mode to subaddressing_mode ? ?.
*)

ninductive Jump (A: Type[0]): Type[0] ≝
  JC: A → Jump A
| JNC: A → Jump A
| JB: Bit → A → Jump A
| JNB: Bit → A → Jump A
| JBC: Bit → A → Jump A
| JZ: A → Jump A
| JNZ: A → Jump A
| CJNE: (([acc] × [direct; data]) + [reg; indirect] × [data]) → A → Jump A
| DJNZ: [reg ; direct] → A → Jump A
| ADD: [acc] → [reg; direct; indirect; data] → Jump A.

ndefinition xxx: Jump Nat.
 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [True] [True] [True]) ?) (Z: Nat)).
 napply I;
nqed.

naxiom bar: addressing_mode → Nat.

ndefinition barj ≝
 λA.λf:A → Nat.λJ:Jump A.
  match J with
   [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
   | _ ⇒ (Z: Nat)].
   
ndefinition PreInstruction ≝ λA: Type[0]. Jump A.

ndefinition Instruction ≝ PreInstruction [rel].

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

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

ndefinition true: Bool ≝ True.
ndefinition false: Bool ≝ False.
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; 
 
 ].