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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
module Pos = Utils.Pos
open Ast
let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ -> true | _ -> false
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let format_location (fmt : Format.formatter) (l : location) : unit =
match l with
| ScopeVar v -> Format.fprintf fmt "%a" ScopeVar.format_t (Pos.unmark v)
| SubScopeVar (_, subindex, subvar) ->
Format.fprintf fmt "%a.%a" SubScopeName.format_t (Pos.unmark subindex) ScopeVar.format_t
(Pos.unmark subvar)
let typ_needs_parens (e : typ Pos.marked) : bool =
match Pos.unmark e with TArrow _ -> true | _ -> false
let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked) : unit =
let format_typ_with_parens (fmt : Format.formatter) (t : typ Pos.marked) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" format_typ t
else Format.fprintf fmt "%a" format_typ t
in
match Pos.unmark typ with
| TLit l -> Dcalc.Print.format_tlit fmt l
| TStruct s -> Format.fprintf fmt "%a" Ast.StructName.format_t s
| TEnum e -> Format.fprintf fmt "%a" Ast.EnumName.format_t e
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1 format_typ t2
let rec format_expr (fmt : Format.formatter) (e : expr Pos.marked) : unit =
let format_with_parens (fmt : Format.formatter) (e : expr Pos.marked) =
if needs_parens e then Format.fprintf fmt "(%a)" format_expr e
else Format.fprintf fmt "%a" format_expr e
in
match Pos.unmark e with
| ELocation l -> Format.fprintf fmt "%a" format_location l
| EVar v -> Format.fprintf fmt "%a" format_var (Pos.unmark v)
| ELit l -> Format.fprintf fmt "%a" Dcalc.Print.format_lit (Pos.same_pos_as l e)
| EStruct (name, fields) ->
Format.fprintf fmt "@[%a @[<hov 2>{@ %a@ }@]@]" Ast.StructName.format_t name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "%a = %a" Ast.StructFieldName.format_t field_name format_expr
field_expr))
(Ast.StructFieldMap.bindings fields)
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a.%a" format_expr e1 Ast.StructFieldName.format_t field
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" Ast.EnumConstructor.format_t cons format_expr e1
| EMatch (e1, _, cases) ->
Format.fprintf fmt "@[<hov 2>@[match@ %a@ with@]@ %a@]" format_expr e1
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ |@ ")
(fun fmt (cons_name, case_expr) ->
Format.fprintf fmt "@[<hov 2>%a@ →@ %a@]" Ast.EnumConstructor.format_t cons_name
format_expr case_expr))
(Ast.EnumConstructorMap.bindings cases)
| EApp ((EAbs (_, binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> (x, tau, arg)) xs_tau args in
Format.fprintf fmt "@[%a%a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau, arg) ->
Format.fprintf fmt "@[@[<hov 2>let@ %a@ :@ %a@ =@ %a@]@ in@\n@]" format_var x
format_typ tau format_expr arg))
xs_tau_arg format_expr body
| EAbs (_, binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> (x, tau)) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>λ@ %a@ →@ %a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau) -> Format.fprintf fmt "@[(%a:@ %a)@]" format_var x format_typ tau))
xs_tau format_expr body
| EApp ((EOp (Binop op), _), [ arg1; arg2 ]) ->
Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 Dcalc.Print.format_binop
(op, Pos.no_pos) format_with_parens arg2
| EApp ((EOp (Unop op), _), [ arg1 ]) ->
Format.fprintf fmt "@[%a@ %a@]" Dcalc.Print.format_unop (op, Pos.no_pos) format_with_parens
arg1
| EApp (f, args) ->
Format.fprintf fmt "@[%a@ %a@]" format_expr f
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens)
args
| EIfThenElse (e1, e2, e3) ->
Format.fprintf fmt "if@ @[<hov 2>%a@]@ then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]" format_expr
e1 format_expr e2 format_expr e3
| EOp (Binop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_binop (op, Pos.no_pos)
| EOp (Unop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_unop (op, Pos.no_pos)
| EDefault (excepts, just, cons) ->
if List.length excepts = 0 then
Format.fprintf fmt "@[⟨%a ⊢ %a⟩@]" format_expr just format_expr cons
else
Format.fprintf fmt "@[<hov 2>⟨%a@ |@ %a ⊢ %a⟩@]"
(Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") format_expr)
excepts format_expr just format_expr cons