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
|
use crate::builtins::Builtin;
use crate::error::{ErrorBuilder, TypeError};
use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
use crate::syntax::{Const, Expr, Span};
/// The type of a type. 0 is `Type`, 1 is `Kind`, etc...
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Default)]
pub struct Universe(u8);
/// An expression representing a type
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Type {
val: Nir,
univ: Universe,
}
/// A hir expression plus its inferred type.
/// Stands for "Typed intermediate representation"
#[derive(Debug, Clone)]
pub struct Tir<'hir> {
hir: &'hir Hir,
ty: Type,
}
impl Universe {
pub fn from_const(c: Const) -> Self {
Universe(match c {
Const::Type => 0,
Const::Kind => 1,
Const::Sort => 2,
})
}
pub fn as_const(self) -> Option<Const> {
match self.0 {
0 => Some(Const::Type),
1 => Some(Const::Kind),
2 => Some(Const::Sort),
_ => None,
}
}
pub fn next(self) -> Self {
Universe(self.0 + 1)
}
}
impl Type {
pub fn new(val: Nir, univ: Universe) -> Self {
Type { val, univ }
}
/// Creates a new Type and infers its universe by re-typechecking its value.
/// TODO: ideally avoid this function altogether. Would need to store types in RecordType and
/// PiClosure.
pub fn new_infer_universe(
env: &TyEnv,
val: Nir,
) -> Result<Self, TypeError> {
let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
let u = match c {
Some(c) => c.to_universe(),
None => unreachable!(
"internal type error: this is not a type: {:?}",
val
),
};
Ok(Type::new(val, u))
}
pub fn from_const(c: Const) -> Self {
Self::new(Nir::from_const(c), c.to_universe().next())
}
pub fn from_builtin(b: Builtin) -> Self {
use Builtin::*;
match b {
Bool | Natural | Integer | Double | Text => {}
_ => unreachable!("this builtin is not a type: {}", b),
}
Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
}
/// Get the type of this type
pub fn ty(&self) -> Universe {
self.univ
}
pub fn to_nir(&self) -> Nir {
self.val.clone()
}
pub fn as_nir(&self) -> &Nir {
&self.val
}
pub fn into_nir(self) -> Nir {
self.val
}
pub fn as_const(&self) -> Option<Const> {
self.val.as_const()
}
pub fn kind(&self) -> &NirKind {
self.val.kind()
}
pub fn to_hir(&self, venv: VarEnv) -> Hir {
self.val.to_hir(venv)
}
pub fn to_expr_tyenv(&self, tyenv: &TyEnv) -> Expr {
self.val.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
}
}
impl<'hir> Tir<'hir> {
pub fn from_hir(hir: &'hir Hir, ty: Type) -> Self {
Tir { hir, ty }
}
pub fn span(&self) -> Span {
self.as_hir().span()
}
pub fn ty(&self) -> &Type {
&self.ty
}
pub fn into_ty(self) -> Type {
self.ty
}
pub fn to_hir(&self) -> Hir {
self.as_hir().clone()
}
pub fn as_hir(&self) -> &Hir {
&self.hir
}
pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
self.as_hir().to_expr_tyenv(env)
}
/// Eval the Tir. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
self.as_hir().eval(env.into())
}
pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
if self.ty().as_const().is_none() {
return mkerr(
ErrorBuilder::new(format!(
"Expected a type, found: `{}`",
self.to_expr_tyenv(env),
))
.span_err(
self.span(),
format!(
"this has type: `{}`",
self.ty().to_expr_tyenv(env)
),
)
.help(format!(
"An expression in type position must have type `Type`, \
`Kind` or `Sort`",
))
.format(),
);
}
Ok(())
}
/// Evaluate to a Type.
pub fn eval_to_type(&self, env: &TyEnv) -> Result<Type, TypeError> {
self.ensure_is_type(env)?;
Ok(Type::new(
self.eval(env),
self.ty()
.as_const()
.expect("case handled in ensure_is_type")
.to_universe(),
))
}
}
impl From<Const> for Universe {
fn from(x: Const) -> Universe {
Universe::from_const(x)
}
}
|
