summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
authorNadrieril2019-08-23 18:53:46 +0200
committerNadrieril2019-08-23 18:53:46 +0200
commitd5bdd48d4c34b4e213e3e2431936c160e4320a80 (patch)
tree2685d76c9ea37d98a541af83b7e939f695b1193c /dhall/src/phase
parentd9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 (diff)
Clarify which syntax elements are completely handled in the tck phase
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/normalize.rs40
-rw-r--r--dhall/src/phase/typecheck.rs9
2 files changed, 24 insertions, 25 deletions
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 28dc0f6..c8f5bc2 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -578,39 +578,41 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
Ret::ValueF(RecordLit(kvs))
}
- (RecursiveRecordTypeMerge, _, _) => {
+ (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => {
unreachable!("This case should have been handled in typecheck")
}
- (Equivalence, _, _) => {
- Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone()))
- }
-
_ => return None,
})
}
pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
use ValueF::{
- AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
- NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
- TextLit, UnionConstructor, UnionLit, UnionType,
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
+ NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+ UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
ExprF::Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
- ExprF::Embed(_) => unreachable!(),
- ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => Ret::Value(x),
+ // Those cases have already been completely handled in the typechecking phase (using
+ // `RetWhole`), so they won't appear here.
+ ExprF::Lam(_, _, _)
+ | ExprF::Pi(_, _, _)
+ | ExprF::Let(_, _, _, _)
+ | ExprF::Embed(_)
+ | ExprF::Const(_)
+ | ExprF::Builtin(_)
+ | ExprF::Var(_)
+ | ExprF::Annot(_, _)
+ | ExprF::RecordType(_)
+ | ExprF::UnionType(_) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
ExprF::Assert(_) => Ret::Expr(expr),
- ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
- ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
- ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
ExprF::App(v, a) => Ret::Value(v.app(a)),
- ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
- ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
ExprF::NaturalLit(n) => Ret::ValueF(NaturalLit(n)),
ExprF::IntegerLit(n) => Ret::ValueF(IntegerLit(n)),
@@ -635,12 +637,6 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
ExprF::RecordLit(kvs) => {
Ret::ValueF(RecordLit(kvs.into_iter().collect()))
}
- ExprF::RecordType(kts) => {
- Ret::ValueF(RecordType(kts.into_iter().collect()))
- }
- ExprF::UnionType(kts) => {
- Ret::ValueF(UnionType(kts.into_iter().collect()))
- }
ExprF::TextLit(elts) => {
use InterpolatedTextContents::Expr;
let elts: Vec<_> = squash_textlit(elts.into_iter());
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 363d733..0268b80 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -291,7 +291,7 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
let ctx = TypecheckContext::new();
Value::from_valuef_and_type(
- ValueF::PartialExpr(ExprF::Builtin(b)),
+ ValueF::from_builtin(b),
type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
)
}
@@ -399,7 +399,7 @@ fn type_last_layer(
if &x.get_type()? != t {
return mkerr(AnnotMismatch(x.clone(), t.clone()));
}
- RetTypeOnly(x.get_type()?)
+ RetWhole(x.clone())
}
Assert(t) => {
match &*t.as_whnf() {
@@ -649,7 +649,10 @@ fn type_last_layer(
return mkerr(EquivalenceTypeMismatch(r.clone(), l.clone()));
}
- RetTypeOnly(Value::from_const(Type))
+ RetWhole(Value::from_valuef_and_type(
+ ValueF::Equivalence(l.clone(), r.clone()),
+ Value::from_const(Type),
+ ))
}
BinOp(o, l, r) => {
let t = builtin_to_value(match o {