summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-02-06 17:35:54 +0000
committerNadrieril2020-02-09 20:13:23 +0000
commitdb1375eccd1e6943b504cd54ed17eb8f4d19c25f (patch)
treee83455535ba5af82159aafc8d14cdba8eee6c1a7 /dhall/src/semantics/tck
parente4b3a879907b6dcc75d25847ae21a23d0201aae1 (diff)
Remove most reliance on types stored in Value
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/env.rs8
-rw-r--r--dhall/src/semantics/tck/typecheck.rs56
2 files changed, 35 insertions, 29 deletions
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)
}