let rec pp fmt a =
  let str = Pretty.string fmt in
  let term = pp fmt in
  let args =  Pretty.tuple pp fmt in
  let app f l = Sym.pp fmt f; Pretty.tuple pp fmt l in
  let infixl x = Pretty.infixl pp x fmt in
  match a with
    | Var(x) -> Var.pp fmt x
    | App(f, l) when not(!pretty) -> app f l
    | App(f, l) ->
        (match f, l with
           | Arith(Num q), [] -> 
               Mpa.Q.pp fmt q
           | Arith(Add), _ -> 
               infixl " + " l
           | Arith(Multq(q)) , [x] -> 
               Pretty.infix Mpa.Q.pp "*" pp fmt (q, x)  
           | Pair(Car), [App(Coproduct(OutR), [x])] ->
               str "hd"; str "("; term x; str ")"
           | Pair(Cdr), [App(Coproduct(OutR), [x])] ->
               str "tl"; str "("; term x; str ")"
           | Pp(Mult), [] ->
               str "1"
           | Pp(Mult), xl ->
               infixl "*" xl
           | Pp(Expt _), [x] ->
               term x; Sym.pp fmt f
           | Bv(Const(b)), [] -> 
               str ("0b" ^ Bitv.to_string b)
           | Bv(Conc _), l -> 
               infixl " ++ " l
           | Bv(Sub(_,i,j)), [x] ->
               term x; Format.fprintf fmt "[%d:%d]" i j
           | Coproduct(InL), [App(Pair(Cons), [x; xl])] ->
               Pretty.infix pp "::" pp fmt (x, xl)
           | Coproduct(InR), [App(Pair(Cons), [])] ->
               str "[]"
           | Arrays(Update), [x;y;z] ->
               term x; str "["; term y; str " := "; term z; str "]"
           | Arrays(Select), [x; y] ->
               term x; str "["; term y; str "]"
           | _ -> 
               app f l)