From a594e3aa376aa4bfef3456d336630f7520f3c28b Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 28 Apr 2019 01:03:12 +0200 Subject: Use PartiallyNormalized throughout typechecking --- dhall/src/expr.rs | 3 - dhall/src/normalize.rs | 12 ++-- dhall/src/typecheck.rs | 173 +++++++++++++++++++++++++------------------------ 3 files changed, 95 insertions(+), 93 deletions(-) (limited to 'dhall') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index d1729a5..bde4fe0 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -133,9 +133,6 @@ impl<'a> Normalized<'a> { pub(crate) fn as_expr(&self) -> &SubExpr { &self.0 } - pub(crate) fn into_expr(self) -> SubExpr { - self.0 - } #[allow(dead_code)] pub(crate) fn unnote<'b>(self) -> Normalized<'b> { Normalized(self.0, self.1, PhantomData) diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 2dc4cab..88a55a1 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use dhall_core::context::Context; use dhall_core::{ - rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText, + rc, shift, shift0, Builtin, Const, ExprF, Integer, InterpolatedText, InterpolatedTextContents, Label, Natural, SubExpr, V, X, }; use dhall_generator as dhall; @@ -347,6 +347,7 @@ pub(crate) enum WHNF { NaturalSuccClosure, Pi(Label, TypeThunk, TypeThunk), + Const(Const), BoolLit(bool), NaturalLit(Natural), IntegerLit(Integer), @@ -406,6 +407,7 @@ impl WHNF { t.normalize().normalize_to_expr(), e.normalize().normalize_to_expr(), )), + WHNF::Const(c) => rc(ExprF::Const(c)), WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)), WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)), WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)), @@ -494,7 +496,7 @@ impl WHNF { } /// Apply to a value - fn app(self, val: WHNF) -> WHNF { + pub(crate) fn app(self, val: WHNF) -> WHNF { match (self, val) { (WHNF::Lam(x, _, (ctx, e)), val) => { let ctx2 = ctx.insert(&x, val); @@ -531,13 +533,14 @@ impl WHNF { } } - fn from_builtin(b: Builtin) -> WHNF { + pub(crate) fn from_builtin(b: Builtin) -> WHNF { WHNF::AppliedBuiltin(b, vec![]) } fn shift(&mut self, delta: isize, var: &V