summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/var.rs6
-rw-r--r--dhall/src/semantics/phase/normalize.rs113
-rw-r--r--dhall/src/semantics/phase/typecheck.rs3
3 files changed, 58 insertions, 64 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 1548713..017a689 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -62,12 +62,6 @@ impl AlphaVar {
self.normal.clone()
}
}
- pub(crate) fn from_var_and_alpha(normal: V<Label>, alpha: usize) -> Self {
- AlphaVar {
- normal,
- alpha: V((), alpha),
- }
- }
}
impl AlphaLabel {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index bf0c626..0c581fe 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -3,7 +3,8 @@ use std::convert::TryInto;
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
-use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
+use crate::semantics::core::var::Subst;
+use crate::semantics::phase::typecheck::{rc, typecheck};
use crate::semantics::phase::Normalized;
use crate::syntax;
use crate::syntax::Const::Type;
@@ -14,60 +15,51 @@ use crate::syntax::{
// Ad-hoc macro to help construct closures
macro_rules! make_closure {
- (#$var:ident) => { $var.clone() };
- (var($var:ident, $n:expr, $($ty:tt)*)) => {{
- let var = AlphaVar::from_var_and_alpha(
+ (var($var:ident)) => {{
+ rc(ExprKind::Var(syntax::V(
Label::from(stringify!($var)).into(),
- $n
- );
- ValueKind::Var(var)
- .into_value_with_type(make_closure!($($ty)*))
+ 0
+ )))
}};
- // Warning: assumes that $ty, as a dhall value, has type `Type`
(λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{
- let var: AlphaLabel = Label::from(stringify!($var)).into();
+ let var = Label::from(stringify!($var));
let ty = make_closure!($($ty)*);
let body = make_closure!($($body)*);
- let body_ty = body.get_type_not_sort();
- let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty)
- .into_value_with_type(Value::from_const(Type));
- ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty)
+ rc(ExprKind::Lam(var, ty, body))
}};
- (Natural) => {
- Value::from_builtin(Builtin::Natural)
+ (Type) => {
+ rc(ExprKind::Const(Type))
};
- (List $($rest:tt)*) => {
- Value::from_builtin(Builtin::List)
- .app(make_closure!($($rest)*))
+ (Natural) => {
+ rc(ExprKind::Builtin(Builtin::Natural))
};
- (Some($($rest:tt)*)) => {{
- let v = make_closure!($($rest)*);
- let v_type = v.get_type_not_sort();
- let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
- ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type)
+ (List $($ty:tt)*) => {{
+ let ty = make_closure!($($ty)*);
+ rc(ExprKind::App(
+ rc(ExprKind::Builtin(Builtin::List)),
+ ty
+ ))
}};
- (1 + $($rest:tt)*) => {
- ValueKind::PartialExpr(ExprKind::BinOp(
+ (Some($($v:tt)*)) => {
+ rc(ExprKind::SomeLit(
+ make_closure!($($v)*)
+ ))
+ };
+ (1 + $($v:tt)*) => {
+ rc(ExprKind::BinOp(
syntax::BinOp::NaturalPlus,
- make_closure!($($rest)*),
- Value::from_kind_and_type(
- ValueKind::NaturalLit(1),
- make_closure!(Natural)
- ),
- )).into_value_with_type(
- make_closure!(Natural)
- )
+ make_closure!($($v)*),
+ rc(ExprKind::NaturalLit(1))
+ ))
};
([ $($head:tt)* ] # $($tail:tt)*) => {{
let head = make_closure!($($head)*);
let tail = make_closure!($($tail)*);
- let list_type = tail.get_type_not_sort();
- ValueKind::PartialExpr(ExprKind::BinOp(
+ rc(ExprKind::BinOp(
syntax::BinOp::ListAppend,
- ValueKind::NEListLit(vec![head])
- .into_value_with_type(list_type.clone()),
+ rc(ExprKind::NEListLit(vec![head])),
tail,
- )).into_value_with_type(list_type)
+ ))
}};
}
@@ -274,16 +266,16 @@ pub(crate) fn apply_builtin(
let list_t = Value::from_builtin(List).app(t.clone());
Ret::Value(
f.app(list_t.clone())
- .app({
- // Move `t` under new variables
- let t1 = t.under_binder(Label::from("a"));
- let t2 = t1.under_binder(Label::from("as"));
- make_closure!(
- λ(a : #t) ->
- λ(as : List #t1) ->
- [ var(a, 1, #t2) ] # var(as, 0, List #t2)
- )
- })
+ .app(
+ typecheck(make_closure!(
+ λ(T : Type) ->
+ λ(a : var(T)) ->
+ λ(as : List var(T)) ->
+ [ var(a) ] # var(as)
+ ))
+ .unwrap()
+ .app(t.clone()),
+ )
.app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
)
}
@@ -302,10 +294,15 @@ pub(crate) fn apply_builtin(
let optional_t = Value::from_builtin(Optional).app(t.clone());
Ret::Value(
f.app(optional_t.clone())
- .app({
- let t1 = t.under_binder(Label::from("a"));
- make_closure!(λ(a: #t) -> Some(var(a, 0, #t1)))
- })
+ .app(
+ typecheck(make_closure!(
+ λ(T : Type) ->
+ λ(a : var(T)) ->
+ Some(var(a))
+ ))
+ .unwrap()
+ .app(t.clone()),
+ )
.app(
EmptyOptionalLit(t.clone())
.into_value_with_type(optional_t),
@@ -324,9 +321,13 @@ pub(crate) fn apply_builtin(
},
(NaturalBuild, [f]) => Ret::Value(
f.app(Value::from_builtin(Natural))
- .app(make_closure!(
- λ(x : Natural) -> 1 + var(x, 0, Natural)
- ))
+ .app(
+ typecheck(make_closure!(
+ λ(x : Natural) ->
+ 1 + var(x)
+ ))
+ .unwrap(),
+ )
.app(
NaturalLit(0)
.into_value_with_type(Value::from_builtin(Natural)),
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c8d934d..2e1cc02 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -291,10 +291,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
}
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
- let ctx = TyCtx::new();
Value::from_kind_and_type(
ValueKind::from_builtin(b),
- type_with(&ctx, type_of_builtin(b)).unwrap(),
+ typecheck(type_of_builtin(b)).unwrap(),
)
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 17:28:40 +0000