summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/mod.rs5
-rw-r--r--dhall/src/semantics/phase/normalize.rs5
-rw-r--r--dhall/src/semantics/phase/resolve.rs8
-rw-r--r--dhall/src/semantics/phase/typecheck.rs26
4 files changed, 31 insertions, 13 deletions
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 4dc91e7..67cdc91 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -89,6 +89,11 @@ impl Resolved {
pub fn to_expr(&self) -> ResolvedExpr {
self.0.clone()
}
+ pub fn tck_and_normalize_new_flow(&self) -> Result<Normalized, TypeError> {
+ let val = crate::semantics::tck::typecheck::typecheck(&self.0)?
+ .normalize_whnf_noenv();
+ Ok(Normalized(Typed(val)))
+ }
}
impl Typed {
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 33e1f2b..5fc72fc 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -2,7 +2,7 @@
use std::collections::HashMap;
use std::convert::TryInto;
-use crate::semantics::nze::NzVar;
+use crate::semantics::nze::{NzVar, QuoteEnv};
use crate::semantics::phase::typecheck::{
builtin_to_value, const_to_value, rc, typecheck,
};
@@ -859,6 +859,9 @@ impl NzEnv {
pub fn construct(items: Vec<NzEnvItem>) -> Self {
NzEnv { items }
}
+ pub fn as_quoteenv(&self) -> QuoteEnv {
+ QuoteEnv::construct(self.items.len())
+ }
pub fn insert_type(&self, t: Value) -> Self {
let mut env = self.clone();
diff --git a/dhall/src/semantics/phase/resolve.rs b/dhall/src/semantics/phase/resolve.rs
index cc4a024..64106aa 100644
--- a/dhall/src/semantics/phase/resolve.rs
+++ b/dhall/src/semantics/phase/resolve.rs
@@ -52,10 +52,14 @@ fn load_import(
import_cache: &mut ImportCache,
import_stack: &ImportStack,
) -> Result<Normalized, Error> {
+ // Ok(
+ // do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
+ // .typecheck()?
+ // .normalize(),
+ // )
Ok(
do_resolve_expr(Parsed::parse_file(f)?, import_cache, import_stack)?
- .typecheck()?
- .normalize(),
+ .tck_and_normalize_new_flow()?,
)
}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 1aab736..18e70e4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -280,7 +280,9 @@ pub(crate) fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
pub(crate) fn builtin_to_value(b: Builtin) -> Value {
Value::from_kind_and_type(
ValueKind::from_builtin(b),
- typecheck(type_of_builtin(b)).unwrap(),
+ crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b))
+ .unwrap()
+ .normalize_whnf_noenv(),
)
}
@@ -380,17 +382,21 @@ fn type_last_layer(
ExprKind::App(f, a) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
- let (tx, tb) = match &*tf_borrow {
- ValueKind::Pi(_, tx, tb) => (tx, tb),
+ match &*tf_borrow {
+ ValueKind::Pi(_, tx, tb) => {
+ if &a.get_type()? != tx {
+ return mkerr("TypeMismatch");
+ }
+
+ let ret = tb.subst_shift(&AlphaVar::default(), a);
+ ret.normalize_nf();
+ RetTypeOnly(ret)
+ }
+ ValueKind::PiClosure { closure, .. } => {
+ RetTypeOnly(closure.apply(a.clone()))
+ }
_ => return mkerr("NotAFunction"),
- };
- if &a.get_type()? != tx {
- return mkerr("TypeMismatch");
}
-
- let ret = tb.subst_shift(&AlphaVar::default(), a);
- ret.normalize_nf();
- RetTypeOnly(ret)
}
ExprKind::Annot(x, t) => {
if &x.get_type()? != t {