Print.ml 1.72 KB
Newer Older
1 2 3 4 5 6 7
open PPrint
open PPrintAux
open F

let arrow =
  string "->"

POTTIER Francois's avatar
POTTIER Francois committed
8
let doublebackslash =
9
  string "\\\\"
POTTIER Francois's avatar
POTTIER Francois committed
10

11
let forall =
12
  string "forall"
13 14 15 16

let rec typ0 ty =
  match ty with
  | TyVar x ->
17
      string x
18 19 20
  | TyArrow _
  | TyProduct _
  | TyForall _ ->
POTTIER Francois's avatar
POTTIER Francois committed
21
      parens (typ ty)
22 23 24 25

and typ1 ty =
  match ty with
  | TyProduct (ty1, ty2) ->
26
      group (typ0 ty1 ^/^ star ^/^ typ1 ty2)
27 28 29 30 31 32
  | _ ->
      typ0 ty

and typ2 ty =
  match ty with
  | TyArrow (ty1, ty2) ->
33
      group (typ1 ty1 ^/^ arrow ^/^ typ2 ty2)
34
  | TyForall (x, ty) ->
POTTIER Francois's avatar
POTTIER Francois committed
35
      group (forall ^/^ string x ^^ dot ^/^ typ2 ty)
36
  | _ ->
POTTIER Francois's avatar
POTTIER Francois committed
37
      typ1 ty
38 39

and typ ty =
POTTIER Francois's avatar
POTTIER Francois committed
40
  typ2 ty
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68

let rec term0 t =
  match t with
  | TeVar x ->
      string x
  | TeAbs _
  | TeApp _
  | TeLet _
  | TeTyAbs _
  | TeTyApp _
  | TePair _
  | TeProj _ ->
      parens (term t)

and term1 t =
  match t with
  | TeApp (t1, t2) ->
      app (term1 t1) (term0 t2)
  | TeTyApp (t1, ty2) ->
      app (term1 t1) (brackets (typ ty2))
  | TeProj (i, t) ->
      app (string (Printf.sprintf "proj%d" i)) (term0 t)
  | _ ->
      term0 t

and term2 t =
  match t with
  | TePair (t1, t2) ->
69
      group (term1 t1 ^^ comma ^/^ term2 t2)
70 71 72 73 74 75
  | _ ->
      term1 t

and term3 t =
  match t with
  | TeAbs (x, ty, t) ->
POTTIER Francois's avatar
POTTIER Francois committed
76
      block
77 78
        (backslash ^^ lparen ^^ string x ^^ spacecolon)
        (break 1 ^^ typ ty ^^ rparen)
POTTIER Francois's avatar
POTTIER Francois committed
79 80 81
        (break 1 ^^ dot)
      ^/^
      term3 t
82 83
  | TeLet (x, t1, t2) ->
      block
POTTIER Francois's avatar
POTTIER Francois committed
84
        (string "let" ^/^ string x ^/^ equals ^^ space)
85
        (term t1)
POTTIER Francois's avatar
POTTIER Francois committed
86
        (string " in")
87 88 89
      ^/^
      term t2
  | TeTyAbs (a, t) ->
POTTIER Francois's avatar
POTTIER Francois committed
90 91 92 93 94
      group (
        doublebackslash ^^ string a ^^ space ^^ dot
        ^/^
        term3 t
      )
95 96 97 98 99 100
  | _ ->
      term2 t

and term t =
  term3 t

POTTIER Francois's avatar
POTTIER Francois committed
101 102 103 104 105
let typ =
  adapt typ

let term =
  adapt term