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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
open Utils
open Ast
let needs_parens (e : expr Marked.pos) : bool =
match Marked.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 (Marked.unmark v)
| SubScopeVar (_, subindex, subvar) ->
Format.fprintf fmt "%a.%a" SubScopeName.format_t (Marked.unmark subindex)
ScopeVar.format_t (Marked.unmark subvar)
let typ_needs_parens (e : typ Marked.pos) : bool =
match Marked.unmark e with TArrow _ -> true | _ -> false
let rec format_typ (fmt : Format.formatter) (typ : typ Marked.pos) : unit =
let format_typ_with_parens (fmt : Format.formatter) (t : typ Marked.pos) =
if typ_needs_parens t then
Format.fprintf fmt "%a%a%a" Dcalc.Print.format_punctuation "(" format_typ
t Dcalc.Print.format_punctuation ")"
else Format.fprintf fmt "%a" format_typ t
in
match Marked.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@ %a@]" format_typ_with_parens t1
Dcalc.Print.format_operator "→" format_typ t2
| TArray t1 ->
Format.fprintf fmt "@[%a@ %a@]" format_typ
(Marked.same_mark_as t1 typ)
Dcalc.Print.format_base_type "array"
| TAny -> Format.fprintf fmt "any"
let rec format_expr
?(debug : bool = false)
(fmt : Format.formatter)
(e : expr Marked.pos) : unit =
let format_expr = format_expr ~debug in
let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) =
if needs_parens e then Format.fprintf fmt "(%a)" format_expr e
else Format.fprintf fmt "%a" format_expr e
in
match Marked.unmark e with
| ELocation l -> Format.fprintf fmt "%a" format_location l
| EVar v -> Format.fprintf fmt "%a" format_var v
| ELit l -> Format.fprintf fmt "%a" Dcalc.Print.format_lit l
| EStruct (name, fields) ->
Format.fprintf fmt " @[<hov 2>%a@ %a@ %a@ %a@]" Ast.StructName.format_t name
Dcalc.Print.format_punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () ->
Format.fprintf fmt "%a@ " Dcalc.Print.format_punctuation ";")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "%a%a%a%a@ %a" Dcalc.Print.format_punctuation "\""
Ast.StructFieldName.format_t field_name
Dcalc.Print.format_punctuation "\"" Dcalc.Print.format_punctuation
"=" format_expr field_expr))
(Ast.StructFieldMap.bindings fields)
Dcalc.Print.format_punctuation "}"
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a%a%a%a%a" format_expr e1
Dcalc.Print.format_punctuation "." Dcalc.Print.format_punctuation "\""
Ast.StructFieldName.format_t field Dcalc.Print.format_punctuation "\""
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" Ast.EnumConstructor.format_t cons format_expr e1
| EMatch (e1, _, cases) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]"
Dcalc.Print.format_keyword "match" format_expr e1
Dcalc.Print.format_keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (cons_name, case_expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@]"
Dcalc.Print.format_punctuation "|"
Dcalc.Print.format_enum_constructor cons_name
Dcalc.Print.format_punctuation "→" 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>%a@ %a@ %a@ %a@ %a@ %a@ %a@\n@]"
Dcalc.Print.format_keyword "let" format_var x
Dcalc.Print.format_punctuation ":" format_typ tau
Dcalc.Print.format_punctuation "=" format_expr arg
Dcalc.Print.format_keyword "in"))
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@ %a@ %a@]"
Dcalc.Print.format_punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau) ->
Format.fprintf fmt "@[%a%a%a@ %a%a@]" Dcalc.Print.format_punctuation
"(" format_var x Dcalc.Print.format_punctuation ":" format_typ tau
Dcalc.Print.format_punctuation ")"))
xs_tau Dcalc.Print.format_punctuation "→" format_expr body
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1
Dcalc.Print.format_binop op format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
format_expr fmt arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[%a@ %a@]" Dcalc.Print.format_unop op
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 "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]"
Dcalc.Print.format_keyword "if" format_expr e1 Dcalc.Print.format_keyword
"then" format_expr e2 Dcalc.Print.format_keyword "else" format_expr e3
| EOp (Ternop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_ternop op
| EOp (Binop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_binop op
| EOp (Unop op) -> Format.fprintf fmt "%a" Dcalc.Print.format_unop op
| EDefault (excepts, just, cons) ->
if List.length excepts = 0 then
Format.fprintf fmt "@[%a%a %a@ %a%a@]" Dcalc.Print.format_punctuation "⟨"
format_expr just Dcalc.Print.format_punctuation "⊢" format_expr cons
Dcalc.Print.format_punctuation "⟩"
else
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a %a@ %a%a@]"
Dcalc.Print.format_punctuation "⟨"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
format_expr)
excepts Dcalc.Print.format_punctuation "|" format_expr just
Dcalc.Print.format_punctuation "⊢" format_expr cons
Dcalc.Print.format_punctuation "⟩"
| ErrorOnEmpty e' ->
Format.fprintf fmt "error_empty@ %a" format_with_parens e'
| EArray es ->
Format.fprintf fmt "%a%a%a" Dcalc.Print.format_punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Dcalc.Print.format_punctuation fmt ";")
(fun fmt e -> Format.fprintf fmt "@[%a@]" format_expr e))
es Dcalc.Print.format_punctuation "]"
let format_struct
(fmt : Format.formatter)
((name, fields) : StructName.t * (StructFieldName.t * typ Marked.pos) list)
: unit =
Format.fprintf fmt "%a %a %a %a@\n@[<hov 2> %a@]@\n%a"
Dcalc.Print.format_keyword "type" StructName.format_t name
Dcalc.Print.format_punctuation "=" Dcalc.Print.format_punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (field_name, typ) ->
Format.fprintf fmt "%a%a %a" StructFieldName.format_t field_name
Dcalc.Print.format_punctuation ":" format_typ typ))
fields Dcalc.Print.format_punctuation "}"
let format_enum
(fmt : Format.formatter)
((name, cases) : EnumName.t * (EnumConstructor.t * typ Marked.pos) list) :
unit =
Format.fprintf fmt "%a %a %a @\n@[<hov 2> %a@]" Dcalc.Print.format_keyword
"type" EnumName.format_t name Dcalc.Print.format_punctuation "="
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (field_name, typ) ->
Format.fprintf fmt "%a %a%a %a" Dcalc.Print.format_punctuation "|"
EnumConstructor.format_t field_name Dcalc.Print.format_punctuation
":" format_typ typ))
cases
let format_scope
?(debug : bool = false)
(fmt : Format.formatter)
((name, decl) : ScopeName.t * scope_decl) : unit =
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@]@\n@[<v 2> %a@]"
Dcalc.Print.format_keyword "let" Dcalc.Print.format_keyword "scope"
ScopeName.format_t name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(fun fmt (scope_var, (typ, vis)) ->
Format.fprintf fmt "%a%a%a %a%a%a%a%a" Dcalc.Print.format_punctuation
"(" ScopeVar.format_t scope_var Dcalc.Print.format_punctuation ":"
format_typ typ Dcalc.Print.format_punctuation "|"
Dcalc.Print.format_keyword
(match Marked.unmark vis.io_input with
| NoInput -> "internal"
| OnlyInput -> "input"
| Reentrant -> "context")
(if Marked.unmark vis.io_output then fun fmt () ->
Format.fprintf fmt "%a@,%a" Dcalc.Print.format_punctuation "|"
Dcalc.Print.format_keyword "output"
else fun fmt () -> Format.fprintf fmt "@<0>")
() Dcalc.Print.format_punctuation ")"))
(ScopeVarMap.bindings decl.scope_sig)
Dcalc.Print.format_punctuation "="
(Format.pp_print_list
~pp_sep:(fun fmt () ->
Format.fprintf fmt "%a@ " Dcalc.Print.format_punctuation ";")
(fun fmt rule ->
match rule with
| Definition (loc, typ, _, e) ->
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]"
Dcalc.Print.format_keyword "let" format_location
(Marked.unmark loc) Dcalc.Print.format_punctuation ":" format_typ
typ Dcalc.Print.format_punctuation "="
(fun fmt e ->
match Marked.unmark loc with
| SubScopeVar _ -> format_expr fmt e
| ScopeVar v -> (
match
Marked.unmark
(snd (ScopeVarMap.find (Marked.unmark v) decl.scope_sig))
.io_input
with
| Reentrant ->
Format.fprintf fmt "%a@ %a" Dcalc.Print.format_operator
"reentrant or by default" (format_expr ~debug) e
| _ -> Format.fprintf fmt "%a" (format_expr ~debug) e))
e
| Assertion e ->
Format.fprintf fmt "%a %a" Dcalc.Print.format_keyword "assert"
(format_expr ~debug) e
| Call (scope_name, subscope_name) ->
Format.fprintf fmt "%a %a%a%a%a" Dcalc.Print.format_keyword "call"
ScopeName.format_t scope_name Dcalc.Print.format_punctuation "["
SubScopeName.format_t subscope_name Dcalc.Print.format_punctuation
"]"))
decl.scope_decl_rules
let format_program
?(debug : bool = false)
(fmt : Format.formatter)
(p : program) : unit =
Format.fprintf fmt "%a%a%a%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
format_struct)
(StructMap.bindings p.program_structs)
(fun fmt () ->
if StructMap.is_empty p.program_structs then Format.fprintf fmt ""
else Format.fprintf fmt "\n\n")
()
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
format_enum)
(EnumMap.bindings p.program_enums)
(fun fmt () ->
if EnumMap.is_empty p.program_enums then Format.fprintf fmt ""
else Format.fprintf fmt "\n\n")
()
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
(format_scope ~debug))
(ScopeMap.bindings p.program_scopes)