Mercurial > urweb
comparison src/elab_err.sig @ 1719:0bafdfae2ac7
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 |