open import Interp_ast
open import Pervasives

type tannot = maybe (t * tag * list nec * effect)

let get_exp_l (E_aux e (l,annot)) = l

val pure : effect
let pure = Effect_aux(Effect_set []) Unknown
let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown

(* Workaround Lem's inability to scrap my (type classes) boilerplate.
 * Implementing only Eq, and only for literals - hopefully this will
 * be enough, but we should in principle implement ordering for everything in
 * Interp_ast *)

val lit_eq: lit -> lit -> bool
let lit_eq (L_aux left _) (L_aux right _) =
   match (left, right) with
   | (L_unit, L_unit) -> true
   | (L_zero, L_zero) -> true
   | (L_one, L_one) -> true
   | (L_true, L_true) -> true
   | (L_false, L_false) -> true
   | (L_num n, L_num m) -> n = m
   | (L_hex h, L_hex h') -> h = h'
   | (L_bin b, L_bin b') -> b = b'
   | (L_undef, L_undef) -> true
   | (L_string s, L_string s') -> s = s'
   | (_, _) -> false
end

instance (Eq lit)
  let (=) = lit_eq
  let (<>) n1 n2 = not (lit_eq n1 n2)
end

let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end

let rec list_to_string format sep lst = match lst with 
  | [] -> ""
  | [last] -> format last
  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
end 

val has_rmem_effect : list base_effect -> bool
val has_barr_effect : list base_effect -> bool
val has_wmem_effect : list base_effect -> bool
let rec has_effect which efcts =
  match efcts with
  | [] -> false
  | (BE_aux e _)::efcts ->
    match (which,e) with
    | (BE_rreg,BE_rreg)    -> true 
    | (BE_wreg,BE_wreg)    -> true 
    | (BE_rmem,BE_rmem)    -> true 
    | (BE_wmem,BE_wmem)    -> true 
    | (BE_barr,BE_barr)    -> true 
    | (BE_undef,BE_undef)  -> true 
    | (BE_unspec,BE_unspec) -> true 
    | (BE_nondet,BE_nondet) -> true 
    | _ -> has_effect which efcts
    end 
  end
let has_rmem_effect = has_effect BE_rmem
let has_barr_effect = has_effect BE_barr
let has_wmem_effect = has_effect BE_wmem

let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
let get_effects (Typ_aux t _) =
  match t with
    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
    | _ -> []
  end

val find_type_def : defs tannot -> id -> maybe (type_def tannot)
val find_function : defs tannot -> id -> maybe (list (funcl tannot))

let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls

let rec find_function (Defs defs) id =
  match defs with 
  | [] -> Nothing
  | def::defs -> 
    match def with
    | DEF_fundef f -> match get_funcls id f with
      | [] -> find_function (Defs defs) id
      | funcs -> Just funcs end
    | _ -> find_function (Defs defs) id
    end end


let rec get_first_index_range (BF_aux i _) = match i with
  | BF_single i -> i
  | BF_range i j -> i
  | BF_concat s _ -> get_first_index_range s
end 

let rec get_index_range_size (BF_aux i _) = match i with
  | BF_single _ -> 1
  | BF_range i j -> (abs (i-j)) + 1
  | BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
end