let pp fmt s = 
  let rec sym s =
    match s with 
      | Uninterp(f) -> Name.pp fmt f
      | Arith(op) -> arith op
      | Pair(op) -> pair op
      | Bv(op) -> bv op
      | Coproduct(op) -> coproduct op
      | Arrays(op) -> array op
      | Pp(op) -> pprod op
      | Fun(op) -> apply op
      | Bvarith(op) -> interp op

  and arith op =
    match op with
      | Num(q) -> Mpa.Q.pp fmt q 
      | Add -> Format.fprintf fmt "+"
      | Multq(q) ->  Mpa.Q.pp fmt q; Format.fprintf fmt "*" 

  and pair op =
    match op with
      | Cons -> Format.fprintf fmt "cons"
      | Car -> Format.fprintf fmt "car"
      | Cdr -> Format.fprintf fmt "cdr"

  and coproduct op =
    match op with
      | InL -> Format.fprintf fmt "inl"
      | InR ->  Format.fprintf fmt "inr"
      | OutL -> Format.fprintf fmt "outl"
      | OutR -> Format.fprintf fmt "outr"

  and bv op =
    match op with
      | Const(b) -> Format.fprintf fmt "0b%s" (Bitv.to_string b)
      | Conc(n,m) -> Format.fprintf fmt "conc[%d,%d]" n m
      | Sub(n,i,j) -> Format.fprintf fmt "sub[%d,%d,%d]" n i j
      | Bitwise(n) -> Format.fprintf fmt "ite[%d]" n

  and array op =
    match op with
      | Create -> Format.fprintf fmt "create"
      | Select -> Format.fprintf fmt "select"  
      | Update -> Format.fprintf fmt "update"

  and interp op =
    match op with
      | Unsigned -> Format.fprintf fmt "unsigned"

  and apply op =
    match op with
      | Apply(Some(c)) -> 
          Pretty.string fmt ("apply[" ^ Pretty.to_string Dom.pp c ^ "]")
      | Apply(None) ->
          Pretty.string fmt "apply"
      | Abs -> 
          Pretty.string fmt "lambda"

  and pprod op =
    match op with
      | Mult ->
          Format.fprintf fmt "."
      | Expt(n) ->
          Format.fprintf fmt "^%d" n
  in
  sym s