Print.ml 530 Bytes
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
open PPrint
open PPrintAux
open Term

let rec term0 t =
  match t with
  | TVar x ->
      string x
  | TLambda _
  | TApp (_, _) ->
      parens (term t)

and term1 t =
  match t with
  | TApp (t1, t2) ->
      app (term1 t1) (term0 t2)
  | _ ->
      term0 t

and term2 t =
  match t with
  | TLambda (x, t) ->
      block
        (backslash ^^ string x ^^ dot)
        (term2 t)
        empty
  | _ ->
      term1 t

and term t =
  term2 t

33
let term (oc : out_channel) (t : (string, string) term) : unit =
POTTIER Francois's avatar
POTTIER Francois committed
34
  output oc (term t)