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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
[@@@ocaml.text "/*"]
(** Copyright 2021-2024, Kakadu and contributors *)
(** SPDX-License-Identifier: LGPL-3.0-or-later *)
[@@@ocaml.text "/*"]
(* Pretty printer goes here *)
open Ast
open Utils
let pp ?(compact = true) =
let open Format in
let mangle t fmt x =
if is_free_in x t || not compact then fprintf fmt "%s" x else fprintf fmt "_"
in
let rec pp fmt = function
| Var s -> Format.fprintf fmt "%s" s
| App (l, r) -> Format.fprintf fmt "(%a %a)" pp l pp r
| Abs (x, Abs (y, Var z)) when x = z && y <> z && compact ->
if compact then Format.fprintf fmt "⊤"
| Abs (x, Abs (y, Var z)) when y = z && x <> z && compact -> Format.fprintf fmt "⊥"
| Abs (f, Abs (x, Var z)) when x = z && x <> f && compact -> Format.fprintf fmt "0"
| Abs (f, Abs (x, App (Var g, Var z))) when x = z && x <> f && g = f && compact ->
Format.fprintf fmt "1"
| Abs (f, Abs (x, App (Var g, App (Var h, Var z))))
when x = z && x <> f && g = f && h = g && compact -> Format.fprintf fmt "2"
| Abs (v1, Abs (v2, Abs (v3, Abs (v4, t)))) when compact ->
Format.fprintf
fmt
"(λ %a %a %a %a -> %a)"
(mangle t)
v1
(mangle t)
v2
(mangle t)
v3
(mangle t)
v4
pp
t
| Abs (v1, Abs (v2, Abs (v3, t))) when compact ->
Format.fprintf
fmt
"(λ %a %a %a -> %a)"
(mangle t)
v1
(mangle t)
v2
(mangle t)
v3
pp
t
| Abs (v1, Abs (v2, t)) when compact ->
Format.fprintf fmt "(λ %a %a -> %a)" (mangle t) v1 (mangle t) v2 pp t
| Abs (x, t) -> Format.fprintf fmt "(λ %a . %a)" (mangle t) x pp t
in
pp
;;
let pp_hum = pp ~compact:true
let pp = pp ~compact:false