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 | |
parent | d9e3bcca9b4350cbc1db2545d7ed28dde4e12be4 (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.rs | 40 | ||||
-rw-r--r-- | dhall/src/phase/typecheck.rs | 9 |
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 { |