summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/nze/env.rs23
-rw-r--r--dhall/src/semantics/nze/normalize.rs8
-rw-r--r--dhall/src/semantics/nze/value.rs60
-rw-r--r--dhall/src/semantics/tck/env.rs8
-rw-r--r--dhall/src/semantics/tck/typecheck.rs56
5 files changed, 88 insertions, 67 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..261e0b6 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Type, Value, ValueKind};
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum NzVar {
@@ -11,9 +11,9 @@ pub(crate) enum NzVar {
#[derive(Debug, Clone)]
enum NzEnvItem {
// Variable is bound with given type
- Kept(Value),
+ Kept(Type),
// Variable has been replaced by corresponding value
- Replaced(Value),
+ Replaced(Value, Type),
}
#[derive(Debug, Clone)]
@@ -49,28 +49,31 @@ impl NzEnv {
NzEnv { items: Vec::new() }
}
- pub fn insert_type(&self, t: Value) -> Self {
+ pub fn insert_type(&self, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Kept(t));
+ env.items.push(NzEnvItem::Kept(ty));
env
}
- pub fn insert_value(&self, e: Value) -> Self {
+ pub fn insert_value(&self, e: Value, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Replaced(e));
+ env.items.push(NzEnvItem::Replaced(e, ty));
env
}
+ pub fn insert_value_noty(&self, e: Value) -> Self {
+ let ty = e.get_type_not_sort();
+ self.insert_value(e, ty)
+ }
pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
- NzEnvItem::Replaced(x) => x.kind().clone(),
+ NzEnvItem::Replaced(x, _) => x.kind().clone(),
}
}
pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) => ty.clone(),
- NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+ NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(),
}
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index a00b7ff..3a981f4 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -17,14 +17,14 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
closure.apply(a).to_whnf_check_type(ty)
}
ValueKind::AppliedBuiltin(closure) => {
- closure.apply(a, f.get_type().unwrap(), ty)
+ closure.apply(a, f.get_type_not_sort(), ty)
}
ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
l.clone(),
a,
kts.clone(),
uniont.clone(),
- f.get_type().unwrap(),
+ f.get_type_not_sort(),
),
_ => ValueKind::PartialExpr(ExprKind::App(f, a)),
}
@@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer(
UnionType(kts) => Ret::ValueKind(UnionConstructor(
l.clone(),
kts.clone(),
- v.get_type().unwrap(),
+ v.get_type_not_sort(),
)),
PartialExpr(ExprKind::BinOp(
BinOp::RightBiasedRecordMerge,
@@ -536,7 +536,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
}
TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
let val = val.eval(env);
- body.eval(&env.insert_value(val)).kind().clone()
+ body.eval(&env.insert_value_noty(val)).kind().clone()
}
TyExprKind::Expr(e) => {
let ty = match tye.get_type() {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 607aa0d..203b479 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -3,13 +3,11 @@ use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
use crate::semantics::{
apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
- TyEnv,
+ type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
+ NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
};
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
NaiveDouble, Natural, Span,
@@ -119,11 +117,14 @@ impl Value {
)
.into_value()
}
+ pub(crate) fn const_kind() -> Value {
+ Value::from_const(Const::Kind)
+ }
/// Construct a Value from a completely unnormalized expression.
pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
ValueInternal::from_thunk(
Thunk::new(env, tye.clone()),
- tye.get_type().ok(),
+ Some(Value::const_kind()),
tye.span().clone(),
)
.into_value()
@@ -137,24 +138,31 @@ impl Value {
let env = NzEnv::new();
ValueInternal::from_thunk(
Thunk::from_partial_expr(env, e, ty.clone()),
- Some(ty),
+ Some(Value::const_kind()),
Span::Artificial,
)
.into_value()
}
/// Make a Value from a ValueKind
pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
- ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
+ ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
+ .into_value()
}
pub(crate) fn from_const(c: Const) -> Self {
let v = ValueKind::Const(c);
match c {
- Const::Type => {
- Value::from_kind_and_type(v, Value::from_const(Const::Kind))
- }
- Const::Kind => {
- Value::from_kind_and_type(v, Value::from_const(Const::Sort))
- }
+ Const::Type => ValueInternal::from_whnf(
+ v,
+ Some(Value::from_const(Const::Kind)),
+ Span::Artificial,
+ )
+ .into_value(),
+ Const::Kind => ValueInternal::from_whnf(
+ v,
+ Some(Value::const_sort()),
+ Span::Artificial,
+ )
+ .into_value(),
Const::Sort => Value::const_sort(),
}
}
@@ -226,14 +234,10 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- let body_t = match &*self.get_type_not_sort().kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- v.check_type(annot);
- closure.apply(v.clone())
- }
- _ => unreachable!("Internal type error"),
- };
- Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
+ Value::from_kind_and_type(
+ apply_any(self.clone(), v, &Value::const_kind()),
+ Value::const_kind(),
+ )
}
/// In debug mode, panic if the provided type doesn't match the value's type.
@@ -246,12 +250,16 @@ impl Value {
// "Internal type error"
// );
}
- pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+ 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()
+ }
+ pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> {
Ok(self.0.get_type()?.clone())
}
/// When we know the value isn't `Sort`, this gets the type directly
pub(crate) fn get_type_not_sort(&self) -> Value {
- self.get_type()
+ self.get_type_noenv()
.expect("Internal type error: value is `Sort` but shouldn't be")
}
@@ -366,6 +374,10 @@ impl Value {
TyExpr::new(tye, self.0.ty.clone(), 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);
+ type_with(tyenv, &expr).unwrap()
+ }
pub fn to_tyexpr_noenv(&self) -> TyExpr {
self.to_tyexpr(VarEnv::new())
}
@@ -522,7 +534,7 @@ impl Closure {
pub fn apply(&self, val: Value) -> Value {
match self {
Closure::Closure { env, body, .. } => {
- body.eval(&env.insert_value(val))
+ body.eval(&env.insert_value_noty(val))
}
Closure::ConstantClosure { body, .. } => body.clone(),
}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 1fc711c..b3e7895 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -104,16 +104,16 @@ impl TyEnv {
&self.names
}
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+ pub fn insert_type(&self, x: &Label, ty: Type) -> Self {
TyEnv {
names: self.names.insert(x),
- items: self.items.insert_type(t),
+ items: self.items.insert_type(ty),
}
}
- pub fn insert_value(&self, x: &Label, e: Value) -> Self {
+ pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
TyEnv {
names: self.names.insert(x),
- items: self.items.insert_value(e),
+ items: self.items.insert_value(e, ty),
}
}
pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index dd9a8fa..ceb83de 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -72,7 +72,9 @@ fn type_one_layer(
ExprKind::Lam(binder, annot, body) => {
let body_ty = body.get_type()?;
- let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
+ let body_ty = body_ty.to_tyexpr_tyenv(
+ &env.insert_type(&binder.clone(), annot.eval(env.as_nzenv())),
+ );
let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
type_one_layer(env, pi_ekind, Span::Artificial)?
.eval(env.as_nzenv())
@@ -154,7 +156,7 @@ fn type_one_layer(
}
}
let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
+ if t.get_type(env)?.as_const() != Some(Const::Type) {
return span_err("InvalidListType");
}
@@ -162,7 +164,7 @@ fn type_one_layer(
}
ExprKind::SomeLit(x) => {
let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Const::Type) {
+ if t.get_type(env)?.as_const() != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
@@ -183,8 +185,7 @@ fn type_one_layer(
let ty = type_of_recordtype(
span.clone(),
- kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
+ kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
}
@@ -278,13 +279,13 @@ fn type_one_layer(
return span_err(&format!(
"annot mismatch: ({} : {}) : {}",
x.to_expr_tyenv(env),
- x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+ 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_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- // t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+ // 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,));
}
@@ -352,10 +353,9 @@ fn type_one_layer(
if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
- if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
- return span_err("IfBranchMustBeTerm");
- }
- if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ let y_ty = y.get_type()?;
+ let y_ty = y_ty.to_tyexpr_tyenv(env);
+ if y_ty.get_type()?.as_const() != Some(Const::Type) {
return span_err("IfBranchMustBeTerm");
}
if y.get_type()? != z.get_type()? {
@@ -388,16 +388,15 @@ fn type_one_layer(
// Construct the final record type
let ty = type_of_recordtype(
span.clone(),
- kts.iter()
- .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
+ kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
let ekind = ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
- x.get_type()?.to_tyexpr(env.as_varenv()),
- y.get_type()?.to_tyexpr(env.as_varenv()),
+ x.get_type()?.to_tyexpr_tyenv(env),
+ y.get_type()?.to_tyexpr_tyenv(env),
);
type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
}
@@ -418,8 +417,8 @@ fn type_one_layer(
env,
ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
- tx.to_tyexpr(env.as_varenv()),
- ty.to_tyexpr(env.as_varenv()),
+ tx.to_tyexpr_tyenv(env),
+ ty.to_tyexpr_tyenv(env),
),
Span::Artificial,
)?;
@@ -451,7 +450,9 @@ fn type_one_layer(
if l.get_type()? != r.get_type()? {
return span_err("EquivalenceTypeMismatch");
}
- if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ if l.get_type()?.to_tyexpr_tyenv(env).get_type()?.as_const()
+ != Some(Const::Type)
+ {
return span_err("EquivalenceArgumentsMustBeTerms");
}
@@ -668,7 +669,7 @@ fn type_one_layer(
annot_val
} else {
let entry_type = kts.iter().next().unwrap().1.clone();
- if entry_type.get_type()?.as_const() != Some(Const::Type) {
+ if entry_type.get_type(env)?.as_const() != Some(Const::Type) {
return span_err(
"`toMap` only accepts records of type `Type`",
);
@@ -724,7 +725,7 @@ fn type_one_layer(
Value::from_kind_and_type(
ValueKind::RecordType(new_kts),
- record_type.get_type()?,
+ record_type.get_type(env)?,
)
}
ExprKind::ProjectionByExpr(record, selection) => {
@@ -804,7 +805,12 @@ pub(crate) fn type_with(
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
ExprKind::Embed(p) => {
- return Ok(p.clone().into_value().to_tyexpr_noenv())
+ let val = p.clone().into_value();
+ (
+ val.to_tyexpr_noenv().kind().clone(),
+ Some(val.get_type(&TyEnv::new())?),
+ )
+ // return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
let ekind = match ekind {
@@ -829,9 +835,9 @@ pub(crate) fn type_with(
val.clone()
};
let val = type_with(env, &val)?;
- val.get_type()?; // Ensure val is not Sort
+ let val_ty = val.get_type()?;
let val_nf = val.eval(&env.as_nzenv());
- let body_env = env.insert_value(&binder, val_nf);
+ let body_env = env.insert_value(&binder, val_nf, val_ty);
let body = type_with(&body_env, body)?;
ExprKind::Let(binder.clone(), None, val, body)
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 11:27:37 +0000