open import Pervasives
open import Interp
open import Interp_ast
import Maybe_extra
open import Num
open import List
open import Word

let compose f g x = f (V_tuple [g x]) ;;

let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;

let eq (V_tuple [x; y]) = V_lit (L_aux (if x = y then L_true else L_false) Unknown) ;;

let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
  | L_true -> L_false
  | L_false -> L_true end) la) ;;

let neq = compose neg eq ;;

let bit_to_bool b = match b with
    V_lit (L_aux L_zero _) -> false
  | V_lit (L_aux L_one _) -> true
  end ;;
let bool_to_bit b = match b with
    false -> V_lit (L_aux L_zero Unknown)
  | true -> V_lit (L_aux L_one Unknown)
  end ;;

(* BitSeq expects LSB first.
 * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
 * hence MSB first.
 * http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num_inc (V_vector idx true l) =
  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
let to_num_dec (V_vector idx false l) =
  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;

let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
  let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
  V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
  let l = boolListFrombitSeq len (bitSeqFromNatural Nothing n) in
  V_vector 0 false (map bool_to_bit l) ;;

let rec add (V_tuple args) = match args with
  (* vector case *)
  | [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
      let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
      let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
      (* XXX how shall I decide this? max? max+1? *)
      let len = max (List.length l) (List.length l') in
      (* XXX assume d = d' *)
      (if d then to_vec_inc else to_vec_dec) len (V_lit (L_aux (L_num (x+y)) lx))
  (* integer case *)
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
  (* assume other literals are L_bin or L_hex, ie. vectors *)
  | [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
  | [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
  end ;;

let rec vec_concat (V_tuple args) = match args with
  | [V_vector n d l; V_vector n' d' l'] ->
      (* XXX d = d' ? droping n' ? *)
      V_vector n d (l ++ l')
  | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
  | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
  end ;;

let function_map = [
  ("add", add);
  ("eq", eq);
  ("vec_concat", vec_concat);
  ("is_one", is_one);
  ("to_num_inc", to_num_inc);
  ("to_num_dec", to_num_dec);
  (* XXX the size of the target vector should be given by the interpreter *)
  ("to_vec_inc", to_vec_inc 64);
  ("to_vec_dec", to_vec_dec 64);
] ;;

let eval_external name v = (Maybe_extra.fromJust (List.lookup name function_map)) v ;;