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::semantics::{NzEnv, Value, ValueKind};
use crate::syntax;
use crate::syntax::{
Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr,
};
pub(crate) fn const_to_value(c: Const) -> Value {
let v = ValueKind::Const(c);
match c {
Const::Type => {
Value::from_kind_and_type(v, const_to_value(Const::Kind))
}
Const::Kind => {
Value::from_kind_and_type(v, const_to_value(Const::Sort))
}
Const::Sort => Value::const_sort(),
}
}
pub fn rc<E>(x: UnspannedExpr<E>) -> Expr<E> {
Expr::new(x, Span::Artificial)
}
// Ad-hoc macro to help construct the types of builtins
macro_rules! make_type {
(Type) => { ExprKind::Const(Const::Type) };
(Bool) => { ExprKind::Builtin(Builtin::Bool) };
(Natural) => { ExprKind::Builtin(Builtin::Natural) };
(Integer) => { ExprKind::Builtin(Builtin::Integer) };
(Double) => { ExprKind::Builtin(Builtin::Double) };
(Text) => { ExprKind::Builtin(Builtin::Text) };
($var:ident) => {
ExprKind::Var(syntax::V(stringify!($var).into(), 0))
};
(Optional $ty:ident) => {
ExprKind::App(
rc(ExprKind::Builtin(Builtin::Optional)),
rc(make_type!($ty))
)
};
(List $($rest:tt)*) => {
ExprKind::App(
rc(ExprKind::Builtin(Builtin::List)),
rc(make_type!($($rest)*))
)
};
({ $($label:ident : $ty:ident),* }) => {{
let mut kts = syntax::map::DupTreeMap::new();
$(
kts.insert(
Label::from(stringify!($label)),
rc(make_type!($ty)),
);
)*
ExprKind::RecordType(kts)
}};
($ty:ident -> $($rest:tt)*) => {
ExprKind::Pi(
"_".into(),
rc(make_type!($ty)),
rc(make_type!($($rest)*))
)
};
(($($arg:tt)*) -> $($rest:tt)*) => {
ExprKind::Pi(
"_".into(),
rc(make_type!($($arg)*)),
rc(make_type!($($rest)*))
)
};
(forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
ExprKind::Pi(
stringify!($var).into(),
rc(make_type!($($ty)*)),
rc(make_type!($($rest)*))
)
};
}
pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
use syntax::Builtin::*;
rc(match b {
Bool | Natural | Integer | Double | Text => make_type!(Type),
List | Optional => make_type!(
Type -> Type
),
NaturalFold => make_type!(
Natural ->
forall (natural: Type) ->
forall (succ: natural -> natural) ->
forall (zero: natural) ->
natural
),
NaturalBuild => make_type!(
(forall (natural: Type) ->
forall (succ: natural -> natural) ->
forall (zero: natural) ->
natural) ->
Natural
),
NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
Natural -> Bool
),
NaturalToInteger => make_type!(Natural -> Integer),
NaturalShow => make_type!(Natural -> Text),
NaturalSubtract => make_type!(Natural -> Natural -> Natural),
IntegerToDouble => make_type!(Integer -> Double),
IntegerShow => make_type!(Integer -> Text),
IntegerNegate => make_type!(Integer -> Integer),
IntegerClamp => make_type!(Integer -> Natural),
DoubleShow => make_type!(Double -> Text),
TextShow => make_type!(Text -> Text),
ListBuild => make_type!(
forall (a: Type) ->
(forall (list: Type) ->
forall (cons: a -> list -> list) ->
forall (nil: list) ->
list) ->
List a
),
ListFold => make_type!(
forall (a: Type) ->
(List a) ->
forall (list: Type) ->
forall (cons: a -> list -> list) ->
forall (nil: list) ->
list
),
ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
ListHead | ListLast => {
make_type!(forall (a: Type) -> (List a) -> Optional a)
}
ListIndexed => make_type!(
forall (a: Type) ->
(List a) ->
List { index: Natural, value: a }
),
ListReverse => make_type!(
forall (a: Type) -> (List a) -> List a
),
OptionalBuild => make_type!(
forall (a: Type) ->
(forall (optional: Type) ->
forall (just: a -> optional) ->
forall (nothing: optional) ->
optional) ->
Optional a
),
OptionalFold => make_type!(
forall (a: Type) ->
(Optional a) ->
forall (optional: Type) ->
forall (just: a -> optional) ->
forall (nothing: optional) ->
optional
),
OptionalNone => make_type!(
forall (A: Type) -> Optional A
),
})
}
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
builtin_to_value_env(b, &NzEnv::new())
}
pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value {
Value::from_kind_and_type(
ValueKind::from_builtin_env(b, env.clone()),
crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
.unwrap()
.normalize_whnf_noenv(),
)
}
|
