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

let arrow =
  string "->"

8
let backslash =
9
  string "\\"
10

POTTIER Francois's avatar
POTTIER Francois committed
11
let doublebackslash =
12
  string "\\\\"
POTTIER Francois's avatar
POTTIER Francois committed
13

14
let forall =
15
  string "forall"
16 17 18 19

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

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

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

and typ ty =
POTTIER Francois's avatar
POTTIER Francois committed
43
  typ2 ty
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 69 70 71

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) ->
72
      group (lparen ^^ term1 t1 ^^ comma ^/^ term2 t2 ^^ rparen)
73 74 75 76 77 78
  | _ ->
      term1 t

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

and term t =
  term3 t

POTTIER Francois's avatar
POTTIER Francois committed
104 105 106 107 108
let typ =
  adapt typ

let term =
  adapt term