(** This module defines parameterized arithmetic expressions, i.e. arithmetic
    expressions mixed with any other type. For instance, one can define
    arithmetic expressions with function calls, arithmetic expressions with top
    and bottom (the abstract interpretation constants), etc. *)

(* Note: the feature 'mixed with any other type' is not used anymore. It would
   make the code clearer to remove it. *)


module P = struct

  type relation = Lt | Gt | Le | Ge

  let is_large = function
    | Le | Ge -> true
    | Lt | Gt -> false

  let has_lower_type = function
    | Lt | Le -> true
    | Gt | Ge -> false

  let string_of_relation = function
    | Lt -> "<"
    | Le -> "<="
    | Gt -> ">"
    | Ge -> ">="

  let mk_strict = function
    | Lt | Le -> Lt
    | Gt | Ge -> Gt

  let mk_large = function
    | Lt | Le -> Le
    | Gt | Ge -> Ge

  let opposite = function
    | Lt -> Ge
    | Le -> Gt
    | Gt -> Le
    | Ge -> Lt

  type unop = Neg

  type binop = Add | Sub | Div | Mul | Mod | Max

  let string_of_unop = function
    | Neg -> "-"

  let string_of_binop = function
    | Add -> "+"
    | Sub -> "-"
    | Div -> "/"
    | Mul -> "*"
    | Mod -> "%"
    | Max -> "max"

  type 'a tt =
    | A of 'a
    | Int of int
    | Var of string
    | UnOp of unop * 'a tt
    | BinOp of binop * 'a tt * 'a tt
    | Cond of 'a tt * relation * 'a tt * 'a tt * 'a tt (* ternary expressions *)

  let compare compare_a v1 v2 = match v1, v2 with
    | A a1, A a2 -> compare_a a1 a2
    | A _, _ -> -1
    | _, A _ -> 1
    | _ -> Pervasives.compare v1 v2

  let rec map f = function
    | A a -> A (f a)
    | Int i -> Int i
    | Var x -> Var x
    | UnOp (unop, v) -> UnOp (unop, map f v)
    | BinOp (binop, v1, v2) -> BinOp (binop, map f v1, map f v2)
    | Cond (v1, rel, v2, v3, v4) ->
      Cond (map f v1, rel, map f v2, map f v3, map f v4)

  let fill_subs v subs = match v, subs with
    | A _, _ | Int _, _ | Var _, _ -> v
    | UnOp (unop, _), v :: _ -> UnOp (unop, v)
    | BinOp (binop, _, _), v1 :: v2 :: _ -> BinOp (binop, v1, v2)
    | Cond (_, rel, _, _, _), t1 :: t2 :: tif :: telse :: _ ->
      Cond (t1, rel, t2, tif, telse)
    | _ -> raise (Failure "ArithSig.fill_subs") (* wrong number of arguments *)

  let subs = function
    | A _ | Int _ | Var _ -> []
    | UnOp (_, v) -> [v]
    | BinOp (_, v1, v2) -> [v1 ; v2]
    | Cond (t1, _, t2, tif, telse) -> [t1 ; t2 ; tif ; telse]

  let rec fold f v =
    let subs_res = List.map (fold f) (subs v) in
    f v subs_res

  let f_is_independent v subs_res =
    let b = match v with A _ -> false | _ -> true in
    List.fold_left (&&) true (b :: subs_res)

  (** [is_independent v] returns true if and only if the arithmetic expression
      [v] does not mention a value of its parameter type. *)

  let is_independent v = fold f_is_independent v

  let f_replace replacements v subs_res =
    let v = match v with
      | Var x when List.mem_assoc x replacements -> List.assoc x replacements
      | _ -> v in
    fill_subs v subs_res

  let replace replacements v = fold (f_replace replacements) v

end

include P


module type S = sig
  type t

  val to_string : t -> string
  val to_cil_term : t -> Cil_types.term

  val compute : t -> t
  val neg : t -> t tt
  val addl : t -> t tt -> t tt
  val addr : t tt -> t -> t tt
  val minusl : t -> t tt -> t tt
  val minusr : t tt -> t -> t tt
  val mull : t -> t tt -> t tt
  val mulr : t tt -> t -> t tt
  val divl : t -> t tt -> t tt
  val divr : t tt -> t -> t tt
  val modl : t -> t tt -> t tt
  val modr : t tt -> t -> t tt
  val maxl : t -> t tt -> t tt
  val maxr : t tt -> t -> t tt
  val lel : t -> t tt -> bool
  val ler : t tt -> t -> bool
  val ltl : t -> t tt -> bool
  val ltr : t tt -> t -> bool
  val gel : t -> t tt -> bool
  val ger : t tt -> t -> bool
  val gtl : t -> t tt -> bool
  val gtr : t tt -> t -> bool

  val compare : t -> t -> int
end