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

let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;

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 value_eq x y then L_one else L_zero) Unknown) ;;

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

let neq = compose neg eq ;;

let lt_range (V_tuple[V_lit (L_aux (L_num l1) lr);V_lit (L_aux (L_num l2) ll);]) =
  if l1 < l2
  then V_lit (L_aux L_one Unknown)
  else V_lit (L_aux L_zero Unknown)

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 ;;

let bitwise_not (V_vector idx inc v) =
  let apply x = bool_to_bit(not (bit_to_bool x)) in
  V_vector idx inc (List.map apply v)

let bitwise_not_bit (V_lit (L_aux l loc)) = match l with
  | L_zero -> (V_lit (L_aux L_one loc))
  | L_one  -> (V_lit (L_aux L_zero loc))
end;; 

let bitwise_binop_bit op (V_tuple [x; y]) =
  bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
;;

let bitwise_binop op (V_tuple [V_vector idx inc v; V_vector idx' inc' v']) =
  (* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
  let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
  V_vector idx inc (List.map apply (List.zip v v'))

(* 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 signed (V_vector idx inc l) =
  (* Word library in Lem expects bitseq with LSB first *)
  let l = if inc then reverse l else l in
  (* Make sure the last bit is a zero to force unsigned numbers *)
  let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;

let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
  let l = boolListFrombitSeq len (bitSeqFromInteger 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 (bitSeqFromInteger Nothing n) in
  V_vector 0 false (map bool_to_bit l) ;;
let to_vec ord len v =
  if ord
  then to_vec_inc len v
  else to_vec_dec len v
;;

(* XXX work-around to avoid truncating *)
let to_vec_safe o l v = to_vec o 64 v ;;

let arith_op op (V_tuple args) = match args with
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
  end ;;
let arith_op_vec op (V_tuple args) = match args with
  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
    let (l1',l2') = (to_num false l1,to_num false l2) in
    let n = arith_op op (V_tuple [l1';l2']) in
    to_vec_safe ord (List.length cs) n
end ;;
let arith_op_range_vec op (V_tuple args) = match args with
  | [n; (V_vector _ ord cs as l2)] ->
    arith_op_vec op (V_tuple [(to_vec_safe ord (List.length cs) n);l2])
end ;;
let arith_op_vec_range op (V_tuple args) = match args with
  | [(V_vector _ ord cs as l1);n] ->
  arith_op_vec op (V_tuple [l1;(to_vec_safe ord (List.length cs) n)])
end ;;

let compare_op op (V_tuple args) = match args with
  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
    if (op x y)
    then V_lit(L_aux L_one lx)
    else V_lit(L_aux L_zero lx)
end ;;
let compare_op_vec op (V_tuple args) = match args with
  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
    let (l1',l2') = (to_num true l1, to_num true l2) in
    compare_op op (V_tuple[l1';l2'])
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 = [
  ("ignore", ignore_sail);            
  ("add", arith_op (+));
  ("add_vec", arith_op_vec (+));
  ("add_vec_range", arith_op_vec_range (+));
  ("add_range_vec", arith_op_range_vec (+));
  ("minus", arith_op (-));
  ("minus_vec", arith_op_vec (-));
  ("eq", eq);
  ("neq", neq);
  ("vec_concat", vec_concat);
  ("is_one", is_one);
  ("to_num_inc", to_num false);
  ("to_num_dec", to_num false);
  ("exts", to_num true);
  (* 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);
  ("bitwise_not", bitwise_not);
  ("bitwise_not_bit", bitwise_not_bit);
  ("bitwise_and", bitwise_binop (&&));
  ("bitwise_or", bitwise_binop (||));
  ("bitwise_xor", bitwise_binop xor);
  ("bitwise_and_bit", bitwise_binop_bit (&&));
  ("bitwise_or_bit", bitwise_binop_bit (||));
  ("bitwise_xor_bit", bitwise_binop_bit xor);
  ("lt", compare_op (<));
  ("gt", compare_op (>));
  ("lt_vec", compare_op_vec (<));
  ("gt_vec", compare_op_vec (>));
] ;;

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