Mercurial > urweb

comparison src/elab_err.sig @ 1719:0bafdfae2ac7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Saving proper environments, to use in displaying nested error messages
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Apr 2012 14:57:00 -0400
parents 6c00d8af6239
children 799be3911ce3
comparison
equal deleted inserted replaced
1718:dd12d6d9e9a7 1719:0bafdfae2ac7
41 41
42 datatype con_error = 42 datatype con_error =
43 UnboundCon of ErrorMsg.span * string 43 UnboundCon of ErrorMsg.span * string
44 | UnboundDatatype of ErrorMsg.span * string 44 | UnboundDatatype of ErrorMsg.span * string
45 | UnboundStrInCon of ErrorMsg.span * string 45 | UnboundStrInCon of ErrorMsg.span * string
46 | WrongKind of Elab.con * Elab.kind * Elab.kind * kunify_error 46 | WrongKind of Elab.con * Elab.kind * Elab.kind * ElabEnv.env * kunify_error
47 | DuplicateField of ErrorMsg.span * string 47 | DuplicateField of ErrorMsg.span * string
48 | ProjBounds of Elab.con * int 48 | ProjBounds of Elab.con * int
49 | ProjMismatch of Elab.con * Elab.kind 49 | ProjMismatch of Elab.con * Elab.kind
50 50
51 val conError : ElabEnv.env -> con_error -> unit 51 val conError : ElabEnv.env -> con_error -> unit
52 52
53 datatype cunify_error = 53 datatype cunify_error =
54 CKind of Elab.kind * Elab.kind * kunify_error 54 CKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
55 | COccursCheckFailed of Elab.con * Elab.con 55 | COccursCheckFailed of Elab.con * Elab.con
56 | CIncompatible of Elab.con * Elab.con 56 | CIncompatible of Elab.con * Elab.con
57 | CExplicitness of Elab.con * Elab.con 57 | CExplicitness of Elab.con * Elab.con
58 | CKindof of Elab.kind * Elab.con * string 58 | CKindof of Elab.kind * Elab.con * string
59 | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option 59 | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * (ElabEnv.env * cunify_error) option) option
60 | TooLifty of ErrorMsg.span * ErrorMsg.span 60 | TooLifty of ErrorMsg.span * ErrorMsg.span
61 | TooUnify of Elab.con * Elab.con 61 | TooUnify of Elab.con * Elab.con
62 | TooDeep 62 | TooDeep
63 | CScope of Elab.con * Elab.con 63 | CScope of Elab.con * Elab.con
64 64
65 val cunifyError : ElabEnv.env -> cunify_error -> unit 65 val cunifyError : ElabEnv.env -> cunify_error -> unit
66 66
67 datatype exp_error = 67 datatype exp_error =
68 UnboundExp of ErrorMsg.span * string 68 UnboundExp of ErrorMsg.span * string
69 | UnboundStrInExp of ErrorMsg.span * string 69 | UnboundStrInExp of ErrorMsg.span * string
70 | Unify of Elab.exp * Elab.con * Elab.con * cunify_error 70 | Unify of Elab.exp * Elab.con * Elab.con * ElabEnv.env * cunify_error
71 | Unif of string * ErrorMsg.span * Elab.con 71 | Unif of string * ErrorMsg.span * Elab.con
72 | WrongForm of string * Elab.exp * Elab.con 72 | WrongForm of string * Elab.exp * Elab.con
73 | IncompatibleCons of Elab.con * Elab.con 73 | IncompatibleCons of Elab.con * Elab.con
74 | DuplicatePatternVariable of ErrorMsg.span * string 74 | DuplicatePatternVariable of ErrorMsg.span * string
75 | PatUnify of Elab.pat * Elab.con * Elab.con * cunify_error 75 | PatUnify of Elab.pat * Elab.con * Elab.con * ElabEnv.env * cunify_error
76 | UnboundConstructor of ErrorMsg.span * string list * string 76 | UnboundConstructor of ErrorMsg.span * string list * string
77 | PatHasArg of ErrorMsg.span 77 | PatHasArg of ErrorMsg.span
78 | PatHasNoArg of ErrorMsg.span 78 | PatHasNoArg of ErrorMsg.span
79 | Inexhaustive of ErrorMsg.span * Elab.pat 79 | Inexhaustive of ErrorMsg.span * Elab.pat
80 | DuplicatePatField of ErrorMsg.span * string 80 | DuplicatePatField of ErrorMsg.span * string
92 val declError : ElabEnv.env -> decl_error -> unit 92 val declError : ElabEnv.env -> decl_error -> unit
93 93
94 datatype sgn_error = 94 datatype sgn_error =
95 UnboundSgn of ErrorMsg.span * string 95 UnboundSgn of ErrorMsg.span * string
96 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item 96 | UnmatchedSgi of ErrorMsg.span * Elab.sgn_item
97 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * kunify_error 97 | SgiWrongKind of ErrorMsg.span * Elab.sgn_item * Elab.kind * Elab.sgn_item * Elab.kind * ElabEnv.env * kunify_error
98 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * cunify_error 98 | SgiWrongCon of ErrorMsg.span * Elab.sgn_item * Elab.con * Elab.sgn_item * Elab.con * ElabEnv.env * cunify_error
99 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item 99 | SgiMismatchedDatatypes of ErrorMsg.span * Elab.sgn_item * Elab.sgn_item
100 * (Elab.con * Elab.con * cunify_error) option 100 * (Elab.con * Elab.con * ElabEnv.env * cunify_error) option
101 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn 101 | SgnWrongForm of ErrorMsg.span * Elab.sgn * Elab.sgn
102 | UnWhereable of Elab.sgn * string 102 | UnWhereable of Elab.sgn * string
103 | WhereWrongKind of Elab.kind * Elab.kind * kunify_error 103 | WhereWrongKind of Elab.kind * Elab.kind * ElabEnv.env * kunify_error
104 | NotIncludable of Elab.sgn 104 | NotIncludable of Elab.sgn
105 | DuplicateCon of ErrorMsg.span * string 105 | DuplicateCon of ErrorMsg.span * string
106 | DuplicateVal of ErrorMsg.span * string 106 | DuplicateVal of ErrorMsg.span * string
107 | DuplicateSgn of ErrorMsg.span * string 107 | DuplicateSgn of ErrorMsg.span * string
108 | DuplicateStr of ErrorMsg.span * string 108 | DuplicateStr of ErrorMsg.span * string
113 datatype str_error = 113 datatype str_error =
114 UnboundStr of ErrorMsg.span * string 114 UnboundStr of ErrorMsg.span * string
115 | NotFunctor of Elab.sgn 115 | NotFunctor of Elab.sgn
116 | FunctorRebind of ErrorMsg.span 116 | FunctorRebind of ErrorMsg.span
117 | UnOpenable of Elab.sgn 117 | UnOpenable of Elab.sgn
118 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error) 118 | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * ElabEnv.env * kunify_error)
119 | DuplicateConstructor of string * ErrorMsg.span 119 | DuplicateConstructor of string * ErrorMsg.span
120 | NotDatatype of ErrorMsg.span 120 | NotDatatype of ErrorMsg.span
121 121
122 val strError : ElabEnv.env -> str_error -> unit 122 val strError : ElabEnv.env -> str_error -> unit
123 123