Skip to content

Commit f3d17d8

Browse files
committed
Move typing messages into submodule
1 parent 43085c1 commit f3d17d8

File tree

2 files changed

+58
-51
lines changed

2 files changed

+58
-51
lines changed

pikelet/src/lang/core/typing.rs

Lines changed: 4 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,10 @@ use crate::lang::core::{
1313
Constant, Globals, LocalLevel, Locals, Term, UniverseLevel, UniverseOffset,
1414
};
1515

16+
pub mod reporting;
17+
18+
pub use self::reporting::*;
19+
1620
/// The state of the type checker.
1721
pub struct State<'me> {
1822
/// Global definition environment.
@@ -108,57 +112,6 @@ impl<'me> State<'me> {
108112
}
109113
}
110114

111-
#[derive(Clone, Debug)]
112-
pub enum Message {
113-
MaximumUniverseLevelReached,
114-
UnboundGlobal {
115-
name: String,
116-
},
117-
UnboundLocal,
118-
InvalidRecordType {
119-
duplicate_labels: Vec<String>,
120-
},
121-
InvalidRecordTerm {
122-
missing_labels: Vec<String>,
123-
unexpected_labels: Vec<String>,
124-
},
125-
LabelNotFound {
126-
expected_label: String,
127-
head_type: Arc<Value>,
128-
},
129-
TooManyParameters,
130-
TooManyArguments {
131-
head_type: Arc<Value>,
132-
},
133-
MismatchedSequenceLength {
134-
found_len: usize,
135-
expected_len: Arc<Value>,
136-
},
137-
NoSequenceConversion {
138-
expected_type: Arc<Value>,
139-
},
140-
AmbiguousTerm {
141-
term: AmbiguousTerm,
142-
},
143-
MismatchedTypes {
144-
found_type: Arc<Value>,
145-
expected_type: ExpectedType,
146-
},
147-
}
148-
149-
#[derive(Clone, Debug)]
150-
pub enum AmbiguousTerm {
151-
Sequence,
152-
FunctionTerm,
153-
RecordTerm,
154-
}
155-
156-
#[derive(Clone, Debug)]
157-
pub enum ExpectedType {
158-
Universe,
159-
Type(Arc<Value>),
160-
}
161-
162115
/// Check that a term is a type and return the universe level it inhabits.
163116
pub fn is_type(state: &mut State<'_>, term: &Term) -> Option<UniverseLevel> {
164117
let r#type = synth_type(state, term);
Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
use std::sync::Arc;
2+
3+
use crate::lang::core::semantics::Value;
4+
5+
#[derive(Clone, Debug)]
6+
pub enum Message {
7+
MaximumUniverseLevelReached,
8+
UnboundGlobal {
9+
name: String,
10+
},
11+
UnboundLocal,
12+
InvalidRecordType {
13+
duplicate_labels: Vec<String>,
14+
},
15+
InvalidRecordTerm {
16+
missing_labels: Vec<String>,
17+
unexpected_labels: Vec<String>,
18+
},
19+
LabelNotFound {
20+
expected_label: String,
21+
head_type: Arc<Value>,
22+
},
23+
TooManyParameters,
24+
TooManyArguments {
25+
head_type: Arc<Value>,
26+
},
27+
MismatchedSequenceLength {
28+
found_len: usize,
29+
expected_len: Arc<Value>,
30+
},
31+
NoSequenceConversion {
32+
expected_type: Arc<Value>,
33+
},
34+
AmbiguousTerm {
35+
term: AmbiguousTerm,
36+
},
37+
MismatchedTypes {
38+
found_type: Arc<Value>,
39+
expected_type: ExpectedType,
40+
},
41+
}
42+
43+
#[derive(Clone, Debug)]
44+
pub enum AmbiguousTerm {
45+
Sequence,
46+
FunctionTerm,
47+
RecordTerm,
48+
}
49+
50+
#[derive(Clone, Debug)]
51+
pub enum ExpectedType {
52+
Universe,
53+
Type(Arc<Value>),
54+
}

0 commit comments

Comments
 (0)