let output fmt = function
  | Term(t) -> Term.pp fmt t
  | Atom(a) -> Atom.pp fmt a
  | Cnstrnt(Some(c)) -> Sign.pp fmt c
  | Cnstrnt(None) -> Format.fprintf fmt "None"
  | Dom(Some(d)) -> Dom.pp fmt d
  | Dom(None) -> Format.fprintf fmt "None"
  | Optterm(Some(t)) -> Term.pp fmt t
  | Optterm(None) -> Format.fprintf fmt "None"
  | Name(n) -> Name.pp fmt n
  | Terms(ts) -> Pretty.set Term.pp fmt (Term.Set.elements ts)
  | Atoms(al) -> Pretty.set Atom.pp fmt (Atom.Set.elements al)
  | Unit() -> Format.fprintf fmt ""
  | Bool(x) -> Format.fprintf fmt "%s" (if x then "true" else "false")
  | Solution(sl) -> Pretty.list (Pretty.eqn Term.pp) fmt sl
  | Context(c) -> 
      Context.pp fmt c
  | Process(status) -> Context.Status.pp Name.pp fmt status
  | Sat(None) -> Pretty.string fmt ":unsat"
  | Sat(Some(rho, n)) ->
      Pretty.string fmt ":sat "; Prop.Assignment.pp fmt rho;
  | Symtab(sym) -> Symtab.pp fmt sym
  | Entry(e) -> Symtab.pp_entry fmt e
  | Int(i) -> Format.fprintf fmt "%d" i
  | String(s) -> Format.fprintf fmt "%s" s