diff options
author | Nadrieril | 2019-08-23 18:53:46 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-23 18:53:46 +0200 |
commit | d5bdd48d4c34b4e213e3e2431936c160e4320a80 (patch) | |
tree | 2685d76c9ea37d98a541af83b7e939f695b1193c /dhall/src/phase/normalize.rs | |
parent | d9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 (diff) |
Clarify which syntax elements are completely handled in the tck phase
Diffstat (limited to 'dhall/src/phase/normalize.rs')
-rw-r--r-- | dhall/src/phase/normalize.rs | 40 |
1 files changed, 18 insertions, 22 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()); |