Source file errors.ml
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
open UtilsLib
open Logic.Lambda
open Logic.Abstract_syntax
open Error
module Environment_l =
struct
type t =
| EntryNotFound of string
| NotALexicon of string
| NotASignature of string
| DuplicatedEntry of string
| Other
let kind = "ACG"
let pp fmt = function
| EntryNotFound e -> Format.fprintf fmt "Entry@ \"%s\"@ not@ found@ in@ current@ environment" e
| NotALexicon e -> Format.fprintf fmt "Entry@ \"%s\"@ is@ not@ a@ lexicon,@ but@ a@ lexicon@ is@ required" e
| NotASignature e -> Format.fprintf fmt "Entry@ \"%s\"@ is@ not@ a@ signature,@ but@ a@ signature@ is@ required" e
| DuplicatedEntry e -> Format.fprintf fmt "Entry@ \"%s\"@ already@ exists@ in@ the@ environment" e
| Other -> Format.fprintf fmt "Unknown@ error"
end
module EnvironmentErrors = ErrorManager(Environment_l)
module Lexicon_l =
struct
type t =
| MissingInterpretations of string * string * string list
| BadInterpretationOfMacro of string * string * string
| NotComposable of string * string * string
| UnavailableSignature of (string * string * string)
| NotCompatibleSignature of (string * string * string * string)
let kind = "Lexicon"
let pp fmt err =
match err with
| MissingInterpretations (lex_name, abs_name, lst) ->
UtilsLib.PPUtils.(
Format.fprintf fmt
"Lexicon@ %a@ is@ missing@ the@ interpretations@ of@ \
the@ following@ terms@ of@ the@ abstract@ signature@ \
%a:@[<v2>@,@[%a@]@]"
PPUtils.lex_pp
lex_name
PPUtils.sig_pp
abs_name
(pp_list Format.pp_print_string)
lst)
| BadInterpretationOfMacro (lex_name, sig_name, macro_name) ->
Format.fprintf fmt
"The@ term@ \"%s\"@ is@ not@ a@ constant@ but@ a@ macro@ \
of@ the@ abstract@ signature@ %a.@ It@ thus@ should@ \
not@ be@ given@ an@ interpretation@ by@ the@ lexicon@ \
%a"
macro_name
PPUtils.sig_pp
sig_name
PPUtils.lex_pp
lex_name
| NotComposable (lex_name, l1_name, l2_name) ->
Format.fprintf
fmt
"Lexicon@ %a@ is@ defined@ using@ the@ composition@ \
%a∘%a.@ However,@ the@ abstract@ vocabulary@ of@ \
%a@ is@ not@ the@ same@ as@ the@ object@ \
vocabulary@ of@ %a"
PPUtils.lex_pp
lex_name
PPUtils.lex_pp
l2_name
PPUtils.lex_pp
l1_name
PPUtils.lex_pp
l2_name
PPUtils.lex_pp
l1_name
| UnavailableSignature (lex_name, sig_name, file_name) ->
Format.fprintf
fmt
"No@ signature@ %a@ available@ for@ lexicon@ %a@ defined@ in@ the@ object@ file@ \"%s\".@ Maybe@ an@ object@ file@ defining@ %a@ is@ missing"
PPUtils.sig_pp
sig_name
PPUtils.lex_pp
lex_name
file_name
PPUtils.sig_pp
sig_name
| NotCompatibleSignature (lex_name, lex_filename, sig_name, sig_filename) ->
Format.fprintf
fmt
"A@ signature@ %a@ is@ available@ for@ lexicon@ \
%a@ defined@ in@ the@ object@ file@ \"%s\".@ \
However,@ it@ seems@ it@ is@ not@ against@ that@ \
signature@ (from@ file@ \"%s\",@ or@ possibly@ a@ later@ \
version)@ that@ lexicon@ %a@ was@ compiled"
PPUtils.sig_pp
sig_name
PPUtils.lex_pp
lex_name
lex_filename
sig_filename
PPUtils.lex_pp
lex_name
end
module LexiconErrors = ErrorManager(Lexicon_l)
module Type_l =
struct
type t =
| AlreadyDefinedVar of string
| NotDefinedVar of string
| NotDefinedConst of string
| NotWellTypedTerm of string * string
| NotWellTypedTermPlus of string * string * string
| NotWellKindedType of string
| NonLinearVar of string
| LinearVar of string
| IsUsed of string * string
| TwoOccurrencesOfLinearVariable of UtilsLib.Error.pos
| NonEmptyContext of string * UtilsLib.Error.pos * UtilsLib.Error.pos * string
| NotNormal
| VacuousAbstraction of string * UtilsLib.Error.pos
| BadBinderType of (string * ((Format.formatter -> Lambda.stype -> unit) * Lambda.stype))
| Other
let kind = "Type"
let arrow_pp fmt = function
| Abstract_syntax.Non_linear -> Format.fprintf fmt "⇒"
| Abstract_syntax.Linear -> Format.fprintf fmt "→"
[@@warning "-unused-value-declaration"]
let pp fmt err =
match err with
| AlreadyDefinedVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ already@ defined" s
| NotDefinedVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ not@ defined" s
| NotDefinedConst s -> Format.fprintf fmt "Const@ \"%s\"@ is@ not@ defined" s
| NotWellTypedTerm (s, typ) ->
Format.fprintf fmt "Term@ \"%s\"@ not@ well@ typed.@;Expected@ type:@ %s" s typ
| NotWellTypedTermPlus (s, typ, wrong_typ) ->
Format.fprintf fmt
"Term@ \"%s\"@ not@ well@ typed.@;\"%s\"@ is@ of@ type@ %s@ but@ is@ here@ used@ with@ type@ %s"
s s typ wrong_typ
| NotWellKindedType s -> Format.fprintf fmt "Type@ \"%s\"@ not@ well@ kinded" s
| NonLinearVar s ->
Format.fprintf fmt "Var@ \"%s\"@ is@ supposed@ to@ be@ non-linear" s
| LinearVar s -> Format.fprintf fmt "Var@ \"%s\"@ is@ supposed@ to@ be@ linear" s
| IsUsed (s1, s2) ->
Format.fprintf fmt
"The@ type@ of@ this@ expression@ is@ \"%s\"@ but@ is@ used@ with@ type@ %s" s1 s2
| TwoOccurrencesOfLinearVariable (s, e) ->
Format.fprintf fmt "This@ linear@ variable@ was@ already@ used:@ %s"
(UtilsLib.Error.compute_comment_for_location (s, e))
| NonEmptyContext (x, (s, e), funct_pos, funct_type) ->
Format.fprintf fmt
"This@ term@ contains@ a@ free@ linear@ variable@ \"%s\"@ at@ %s@ and@ is@ \
argument@ of@ the@ term@ of@ type@ \"%s\"@ at@ %s"
x
(UtilsLib.Error.compute_comment_for_location (s, e))
funct_type
(UtilsLib.Error.compute_comment_for_location funct_pos)
| NotNormal -> Format.fprintf fmt "This@ term@ is@ not@ in@ normal@ form"
| VacuousAbstraction (x, (s, e)) ->
Format.fprintf fmt
"This@ linear@ variable@ \"%s\"@ is@ abstracted@ over@ but@ not@ used@ in@ term@ %s"
x
(UtilsLib.Error.compute_comment_for_location (s, e))
| BadBinderType (s, (pp,t)) -> Format.fprintf fmt "Term@ \"%s\"@ is@ declared@ as@ binder@ of@ type@ \"%a\",@ but@ its@ type@ should@ match@ \"('a → 'b) → 'c\"@ (or@ with@ \"⇒\"@ anywhere@ instead@ of@ \"→\")" s pp t
| Other -> Format.fprintf fmt "Not@ yet@ implemented"
end
module TypeErrors = ErrorManager(Type_l)
module Cmd_l =
struct
type t =
| TypeMismatch of (Format.formatter -> unit) * (Format.formatter -> unit) * (Format.formatter -> unit) * (Format.formatter -> unit)
let kind = ""
let pp fmt = function
| TypeMismatch (obj, abs, inter_abs, lex) ->
Format.fprintf
fmt
"The@ object@ type@ \"%t\"@ is@ not@ the@ interpretation@ of@ the@ abstract@ type@ \"%t\"@ by@ the@ lexicon@ %t@ (type@ \"%t\"@ was@ expected)"
obj
abs
lex
inter_abs
end
module CmdErrors = ErrorManager(Cmd_l)