open import Pervasives
open import Interp
open import Interp_ast
import Assert_extra Maybe_extra (* For failwith for error reporting while debugging; and for fromJust when we know it's not Nothing *)
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 zeroi = integerFromNat 0
let onei = integerFromNat 1
let twoi = integerFromNat 2

let rec sparse_walker update ni processed_length length ls df =
  if processed_length = length 
  then []
  else match ls with
  | [] -> replicate (natFromInteger (length - processed_length)) df
  | (i,v)::ls -> 
    if ni = i 
    then v::(sparse_walker update (update ni) (processed_length + 1) length ls df)
    else df::(sparse_walker update (update ni) (processed_length + 1) length ((i,v)::ls) df)
end

let fill_in_sparse v = match v with
  | V_vector_sparse first length inc ls df -> 
    V_vector first inc (sparse_walker (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
end    

let is_one v = match v with 
  | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_true else L_false) lb)
  | V_unknown -> V_unknown
end ;;

let lt_range (V_tuple[v1;v2]) = match (v1,v2) with 
  | (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)
  | (V_unknown,_) -> V_unknown
  | (_,V_unknown) -> V_unknown
end ;;

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 (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
  let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
  V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
  let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
  V_vector 0 false (map bool_to_bit l) ;;
let to_vec ord len n =
  if ord
  then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
  else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
;;

let exts len ((V_vector _ inc _) as v) =
  to_vec inc len (to_num true v)
;;

let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
(* XXX interpret vectors as unsigned numbers for equality *)
let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num false v; r]) ;;
let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num false v]) ;;

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 arith_op op (V_tuple args) = match args with
  | [V_unknown;_] -> V_unknown
  | [_;V_unknown] -> V_unknown
  | [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 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 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 ord (List.length cs) n)])
end ;;

let arith_op_range_vec_range op (V_tuple args) = match args with
  | [n;(V_vector _ _ _ as l2)] ->
    arith_op op (V_tuple [n;(to_num true l2)])
end ;;
let arith_op_vec_range_range op (V_tuple args) = match args with
  | [(V_vector _ _ _ as l1);n] ->
    arith_op op (V_tuple [(to_num true l1);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_vec_range_range", arith_op_vec_range_range (+));
  ("add_range_vec", arith_op_range_vec (+));
  ("add_range_vec_range", arith_op_range_vec_range (+));
  ("minus", arith_op (-));
  ("minus_vec", arith_op_vec (-));
  ("mod", arith_op (mod));
  ("mod_vec", arith_op_vec (mod));
  ("mod_vec_range", arith_op_vec_range (mod));
  ("eq", eq);
  ("eq_vec_range", eq_vec_range);
  ("eq_range_vec", eq_range_vec);
  ("neq", neq);
  ("vec_concat", vec_concat);
  ("is_one", is_one);
  ("to_num_inc", to_num false);
  ("to_num_dec", to_num false);
  ("EXTS", exts 64);
  ("to_vec_inc", to_vec_inc);
  ("to_vec_dec", to_vec_dec);
  ("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 = match List.lookup name function_map with
  | Just f -> f v
  | Nothing -> Assert_extra.failwith ("missing library function " ^ name)
  end