summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs14
-rw-r--r--dhall/src/semantics/hir.rs3
-rw-r--r--dhall/src/semantics/nze/normalize.rs21
-rw-r--r--dhall/src/semantics/nze/value.rs120
-rw-r--r--dhall/src/semantics/tck/env.rs6
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs11
-rw-r--r--dhall/src/semantics/tck/typecheck.rs13
7 files changed, 80 insertions, 108 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index a513967..423364d 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
use crate::semantics::{
- typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+ typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv,
};
use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
@@ -48,17 +48,13 @@ impl BuiltinClosure<Value> {
x.normalize();
}
}
- pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind {
- TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold(
+ pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+ HirKind::Expr(self.args.iter().zip(self.types.iter()).fold(
ExprKind::Builtin(self.b),
|acc, (v, ty)| {
ExprKind::App(
- TyExpr::new(
- TyExprKind::Expr(acc),
- Some(ty.clone()),
- Span::Artificial,
- ),
- v.to_tyexpr(venv),
+ Hir::new(HirKind::Expr(acc), Span::Artificial),
+ v.to_hir(venv),
)
},
))
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 2784ecb..683dbbb 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -62,8 +62,7 @@ impl Hir {
/// Eval the Hir. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: &NzEnv) -> Value {
- // Value::new_thunk(env, self.clone())
- todo!()
+ Value::new_thunk(env, self.clone())
}
/// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index b5949f5..acb2e51 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,8 +3,7 @@ use std::collections::HashMap;
use crate::semantics::NzEnv;
use crate::semantics::{
- Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind,
- Value, ValueKind,
+ Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
};
use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
use crate::Normalized;
@@ -460,11 +459,11 @@ pub(crate) fn normalize_one_layer(
}
}
-/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
- match tye.kind() {
- TyExprKind::Var(var) => env.lookup_val(var),
- TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+ match hir.kind() {
+ HirKind::Var(var) => env.lookup_val(var),
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
ValueKind::LamClosure {
binder: Binder::new(binder.clone()),
@@ -472,7 +471,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
let annot = annot.eval(env);
ValueKind::PiClosure {
binder: Binder::new(binder.clone()),
@@ -480,12 +479,12 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
body.eval(&env.insert_value_noty(val)).kind().clone()
}
- TyExprKind::Expr(e) => {
- let e = e.map_ref(|tye| tye.eval(env));
+ HirKind::Expr(e) => {
+ let e = e.map_ref(|hir| hir.eval(env));
normalize_one_layer(e, env)
}
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d4213bc..d05c545 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,9 +4,9 @@ use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::nze::lazy;
use crate::semantics::{
- apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
- type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr,
- TyExprKind, VarEnv,
+ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
+ type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv,
+ TyExpr, VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -34,7 +34,7 @@ struct ValueInternal {
#[derive(Debug, Clone)]
pub(crate) enum Thunk {
/// A completely unnormalized expression.
- Thunk { env: NzEnv, body: TyExpr },
+ Thunk { env: NzEnv, body: Hir },
/// A partially normalized expression that may need to go through `normalize_one_layer`.
PartialExpr {
env: NzEnv,
@@ -46,7 +46,7 @@ pub(crate) enum Thunk {
#[derive(Debug, Clone)]
pub(crate) enum Closure {
/// Normal closure
- Closure { env: NzEnv, body: TyExpr },
+ Closure { env: NzEnv, body: Hir },
/// Closure that ignores the argument passed
ConstantClosure { body: Value },
}
@@ -116,11 +116,12 @@ impl Value {
Value::from_const(Const::Kind)
}
/// Construct a Value from a completely unnormalized expression.
- pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+ pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
+ let span = hir.span();
ValueInternal::from_thunk(
- Thunk::new(env, tye.clone()),
+ Thunk::new(env, hir),
Some(Value::const_kind()),
- tye.span().clone(),
+ span,
)
.into_value()
}
@@ -176,13 +177,8 @@ impl Value {
_ => None,
}
}
- // pub(crate) fn span(&self) -> Span {
- // self.0.span.clone()
- // }
/// This is what you want if you want to pattern-match on the value.
- /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
- /// panics.
pub(crate) fn kind(&self) -> &ValueKind {
self.0.kind()
}
@@ -196,7 +192,7 @@ impl Value {
self.to_tyexpr_noenv().to_expr(opts)
}
pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+ self.to_hir(env.as_varenv()).to_expr_tyenv(env)
}
/// Normalizes contents to normal form; faster than `normalize` if
@@ -218,8 +214,7 @@ impl Value {
}
pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
- let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
- type_with(tyenv, &expr).unwrap().get_type()
+ self.to_tyexpr_tyenv(tyenv).get_type()
}
/// When we know the value isn't `Sort`, this gets the type directly
pub(crate) fn get_type_not_sort(&self) -> Value {
@@ -229,21 +224,21 @@ impl Value {
.clone()
}
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
ExprKind::UnionType(
kts.iter()
.map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+ (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
})
.collect(),
)
};
- let tye = match &*self.kind() {
- ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
- ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
- self_kind => TyExprKind::Expr(match self_kind {
+ let hir = match &*self.kind() {
+ ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
+ ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+ self_kind => HirKind::Expr(match self_kind {
ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
unreachable!()
}
@@ -253,8 +248,8 @@ impl Value {
closure,
} => ExprKind::Lam(
binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(venv),
+ annot.to_hir(venv),
+ closure.to_hir(venv),
),
ValueKind::PiClosure {
binder,
@@ -262,8 +257,8 @@ impl Value {
closure,
} => ExprKind::Pi(
binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(venv),
+ annot.to_hir(venv),
+ closure.to_hir(venv),
),
ValueKind::Const(c) => ExprKind::Const(*c),
ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
@@ -271,81 +266,75 @@ impl Value {
ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
ValueKind::EmptyOptionalLit(n) => ExprKind::App(
- Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
- n.to_tyexpr(venv),
+ Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
+ n.to_hir(venv),
),
ValueKind::NEOptionalLit(n) => {
- ExprKind::SomeLit(n.to_tyexpr(venv))
- }
- ValueKind::EmptyListLit(n) => {
- ExprKind::EmptyListLit(TyExpr::new(
- TyExprKind::Expr(ExprKind::App(
- Value::from_builtin(Builtin::List).to_tyexpr(venv),
- n.to_tyexpr(venv),
- )),
- Some(Value::from_const(Const::Type)),
- Span::Artificial,
- ))
+ ExprKind::SomeLit(n.to_hir(venv))
}
+ ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+ HirKind::Expr(ExprKind::App(
+ Value::from_builtin(Builtin::List).to_hir(venv),
+ n.to_hir(venv),
+ )),
+ Span::Artificial,
+ )),
ValueKind::NEListLit(elts) => ExprKind::NEListLit(
- elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+ elts.iter().map(|v| v.to_hir(venv)).collect(),
),
ValueKind::TextLit(elts) => ExprKind::TextLit(
elts.iter()
- .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+ .map(|t| t.map_ref(|v| v.to_hir(venv)))
.collect(),
),
ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
kvs.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
.collect(),
),
ValueKind::RecordType(kts) => ExprKind::RecordType(
kts.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
.collect(),
),
ValueKind::UnionType(kts) => map_uniontype(kts),
ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(t.clone()),
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
Span::Artificial,
),
l.clone(),
),
ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
- TyExpr::new(
- TyExprKind::Expr(ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(uniont.clone()),
+ Hir::new(
+ HirKind::Expr(ExprKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
Span::Artificial,
),
l.clone(),
)),
- Some(ctort.clone()),
Span::Artificial,
),
- v.to_tyexpr(venv),
+ v.to_hir(venv),
),
ValueKind::Equivalence(x, y) => ExprKind::BinOp(
BinOp::Equivalence,
- x.to_tyexpr(venv),
- y.to_tyexpr(venv),
+ x.to_hir(venv),
+ y.to_hir(venv),
),
- ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+ ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
}),
};
- TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
+ Hir::new(hir, self.0.span.clone())
}
pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
- let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+ let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv);
type_with(tyenv, &expr).unwrap()
}
pub fn to_tyexpr_noenv(&self) -> TyExpr {
- self.to_tyexpr(VarEnv::new())
+ self.to_tyexpr_tyenv(&TyEnv::new())
}
}
@@ -461,7 +450,7 @@ impl ValueKind {
}
impl Thunk {
- fn new(env: &NzEnv, body: TyExpr) -> Self {
+ fn new(env: &NzEnv, body: Hir) -> Self {
Thunk::Thunk {
env: env.clone(),
body,
@@ -475,14 +464,14 @@ impl Thunk {
}
fn eval(self) -> ValueKind {
match self {
- Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
+ Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
}
}
}
impl Closure {
- pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+ pub fn new(env: &NzEnv, body: Hir) -> Self {
Closure::Closure {
env: env.clone(),
body,
@@ -512,10 +501,11 @@ impl Closure {
// TODO: somehow normalize the body. Might require to pass an env.
pub fn normalize(&self) {}
- /// Convert this closure to a TyExpr
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+
+ /// Convert this closure to a Hir expression
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
self.apply_var(NzVar::new(venv.size()))
- .to_tyexpr(venv.insert())
+ .to_hir(venv.insert())
}
/// If the closure variable is free in the closure, return Err. Otherwise, return the value
/// with that free variable remove.
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index b3e7895..af955f4 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
}
impl VarEnv {
- pub fn new() -> Self {
- VarEnv { size: 0 }
- }
+ // pub fn new() -> Self {
+ // VarEnv { size: 0 }
+ // }
pub fn size(&self) -> usize {
self.size
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index fa578c0..29099c5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,6 @@
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{
- rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
-};
-use crate::syntax::{ExprKind, Span, V};
+use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
+use crate::syntax::{ExprKind, Span};
use crate::Normalized;
use crate::{NormalizedExpr, ToExprOptions};
@@ -56,13 +54,10 @@ impl TyExpr {
pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
self.to_hir().to_expr(opts)
}
- pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- self.to_hir().to_expr_tyenv(env)
- }
/// Eval the TyExpr. It will actually get evaluated only as needed on demand.
pub fn eval(&self, env: &NzEnv) -> Value {
- Value::new_thunk(env, self.clone())
+ Value::new_thunk(env, self.to_hir())
}
/// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 810e483..5b233f8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -266,17 +266,10 @@ fn type_one_layer(
let x_ty = x.get_type()?;
if x_ty != t {
return span_err(&format!(
- "annot mismatch: ({} : {}) : {}",
- x.to_expr_tyenv(env),
- x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
- t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
+ "annot mismatch: {} != {}",
+ x_ty.to_expr_tyenv(env),
+ t.to_expr_tyenv(env)
));
- // return span_err(format!(
- // "annot mismatch: {} != {}",
- // x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
- // t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
- // ));
- // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
}
x_ty
}