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
open Domain.Lib
module Atom = Domain.Atom
module Mixfix = Domain.Mixfix
module Mixop = Domain.Mixop
open Lang
module Value = Runtime.Value
open Util.Source
module F = Format
module HEnv = MakeCaseIdEnv (Hints.Alter)
let hintid = "print"
let hints_of_typcase (henv : HEnv.t) (tid : TId.t) (typcase : Il.typcase) :
HEnv.t =
let nottyp, _, hints = typcase in
let hint_opt =
List.find_opt (fun hint -> El.(hint.hintid.it = hintid)) hints
|> Option.map (fun hint -> El.(hint.hintexp))
in
let hint_alter_opt = Option.bind hint_opt Hints.Alter.init in
match hint_alter_opt with
| Some hint_alter ->
let mixop, _ = Mixfix.split nottyp.it in
let cid = (tid, mixop) in
HEnv.add cid hint_alter henv
| None -> henv
let hints_of_typcases (henv : HEnv.t) (tid : TId.t) (typcases : Il.typcase list)
: HEnv.t =
List.fold_left
(fun henv typcase -> hints_of_typcase henv tid typcase)
henv typcases
let hints_of_deftyp (henv : HEnv.t) (tid : TId.t) (deftyp : Il.deftyp) : HEnv.t
=
match deftyp.it with
| VariantT typcases -> hints_of_typcases henv tid typcases
| _ -> henv
let hints_of_def_al (henv : HEnv.t) (def_al : Al.def) : HEnv.t =
match def_al.it with
| TypD (id, _, deftyp, _) -> hints_of_deftyp henv id deftyp
| _ -> henv
let hints_of_def_sl (henv : HEnv.t) (def_sl : Sl.def) : HEnv.t =
match def_sl.it with
| TypD (id, _, deftyp, _) -> hints_of_deftyp henv id deftyp
| _ -> henv
let hints_of_def_pl (henv : HEnv.t) (def_pl : Pl.def) : HEnv.t =
let open Pl in
match def_pl.Annot.node.it with
| TypD (id, _, deftyp) -> hints_of_deftyp henv id deftyp
| _ -> henv
let hints_of_spec_al (spec_al : Al.spec) : HEnv.t =
List.fold_left hints_of_def_al HEnv.empty spec_al
let hints_of_spec_sl (spec_sl : Sl.spec) : HEnv.t =
List.fold_left hints_of_def_sl HEnv.empty spec_sl
let hints_of_spec_pl (spec_pl : Pl.spec) : HEnv.t =
List.fold_left hints_of_def_pl HEnv.empty spec_pl
let pp_num fmt (num : Il.num) : unit =
match num with
| `Nat n -> F.fprintf fmt "%s" (Bigint.to_string n)
| `Int i ->
F.fprintf fmt "%s"
((if i >= Bigint.zero then "" else "-")
^ Bigint.to_string (Bigint.abs i))
let pp_atom fmt (atom : Il.atom) : unit =
match atom.it with
| Atom.Tag _ -> ()
| _ ->
atom.it |> Atom.render_atom |> String.lowercase_ascii
|> F.fprintf fmt "%s"
let pp_atoms fmt (atoms : Il.atom list) : unit =
match atoms with
| [] -> F.fprintf fmt ""
| _ ->
let atoms =
atoms
|> List.map (fun atom -> F.asprintf "%a" pp_atom atom)
|> List.filter (fun str -> str <> String.empty)
in
F.fprintf fmt "%s" (String.concat " " atoms)
let rec pp_value (henv : HEnv.t) fmt (value : Value.t) : unit =
let note = value.note in
match value.it with
| BoolV b -> F.fprintf fmt "%b" b
| NumV n -> F.fprintf fmt "%a" pp_num n
| TextV _ -> pp_text_v fmt value
| StructV _ -> failwith "@pp_value: StructV not implemented"
| CaseV valuecase -> pp_case_v note henv fmt valuecase
| TupleV values ->
F.fprintf fmt "(%s)"
(String.concat ", "
(List.map (fun v -> F.asprintf "%a" (pp_value henv) v) values))
| OptV _ -> pp_opt_v henv fmt value
| ListV _ -> pp_list_v henv fmt value
| _ -> failwith "@pp_value: TODO"
and pp_text_v fmt (value : Value.t) : unit =
match value.it with
| TextV text -> F.fprintf fmt "%s" (String.escaped text)
| _ -> failwith "@pp_text_v: expected TextV value"
and pp_case_v (note : Il.vnote) (henv : HEnv.t) fmt (valuecase : Il.valuecase) :
unit =
let mixop, values = Mixfix.split valuecase in
let cid_opt =
match note.typ with VarT (tid, _) -> Some (tid, mixop) | _ -> None
in
let hint_alter_opt =
Option.bind cid_opt (fun cid -> HEnv.find_opt cid henv)
in
match hint_alter_opt with
| Some hint_alter -> pp_hint_case_v henv hint_alter fmt values
| None -> pp_default_case_v henv fmt valuecase
and pp_hint_case_v (henv : HEnv.t) (hint : Hints.Alter.t) fmt
(values : Value.t list) : unit =
let str =
Hints.Alter.alternate ~empty:""
~text:(fun s -> match s with "" -> None | s -> Some s)
~atom:(fun (atom : Il.atom) -> F.asprintf "%a" pp_atom atom)
~join:(fun (docs : string list) -> String.concat " " docs)
~fuse:(fun (a : string) (b : string) -> a ^ b)
~other:(fun (hintexp : El.exp) -> El.Print.string_of_exp hintexp)
hint
(fun value -> F.asprintf "%a" (pp_value henv) value)
values
in
F.fprintf fmt "%s" str
and pp_default_case_v (henv : HEnv.t) fmt (valuecase : Il.valuecase) : unit =
F.fprintf fmt "%s"
(Mixfix.render
~string_of_atom:(fun atom -> F.asprintf "%a" pp_atom atom)
~string_of_arg:(F.asprintf "%a" (pp_value henv))
valuecase)
and pp_opt_v (henv : HEnv.t) fmt (value : Value.t) : unit =
match value.it with
| OptV (Some v) -> F.fprintf fmt "%a" (pp_value henv) v
| OptV None -> ()
| _ -> failwith "@pp_opt_v: expected OptV value"
and pp_list_v (henv : HEnv.t) fmt (value : Value.t) : unit =
let values =
match value.it with
| ListV values -> values
| _ ->
failwith
(F.asprintf "@pp_list_v: expected ListV, got %a" (pp_value henv) value)
in
let ss = List.map (F.asprintf "%a" (pp_value henv)) values in
F.fprintf fmt "%s" (String.concat " " ss)