From 084e81956e99bc759012be7c171f4095c2e59d22 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 19:34:11 +0000 Subject: Thread env through nztion to fix Foo/build closures --- dhall/src/semantics/phase/normalize.rs | 70 ++++++++++++++++++++++------------ dhall/src/semantics/phase/typecheck.rs | 20 ++++++---- 2 files changed, 58 insertions(+), 32 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 5fc72fc..a11cb75 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -4,9 +4,11 @@ use std::convert::TryInto; use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::typecheck::{ - builtin_to_value, const_to_value, rc, typecheck, + builtin_to_value_env, const_to_value, rc, }; use crate::semantics::phase::Normalized; +use crate::semantics::tck::typecheck::type_with; +use crate::semantics::tck::typecheck::TyEnv; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; @@ -73,6 +75,7 @@ pub(crate) fn apply_builtin( args: Vec, ty: &Value, types: Vec, + env: NzEnv, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -86,6 +89,11 @@ pub(crate) fn apply_builtin( ValueWithRemainingArgs(&'a [Value], Value), DoneAsIs, } + let make_closure = |e| { + type_with(&env.to_alpha_tyenv(), &e) + .unwrap() + .normalize_whnf(&env) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), @@ -272,13 +280,12 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(list_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> λ(as : List var(T)) -> [ var(a) ] # var(as) )) - .unwrap() .app(t.clone()), ) .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), @@ -300,12 +307,11 @@ pub(crate) fn apply_builtin( Ret::Value( f.app(optional_t.clone()) .app( - typecheck(make_closure!( + make_closure(make_closure!( λ(T : Type) -> λ(a : var(T)) -> Some(var(a)) )) - .unwrap() .app(t.clone()), ) .app( @@ -326,13 +332,10 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app( - typecheck(make_closure!( - λ(x : Natural) -> - 1 + var(x) - )) - .unwrap(), - ) + .app(make_closure(make_closure!( + λ(x : Natural) -> + 1 + var(x) + ))) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), @@ -366,7 +369,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args, types), + Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), } } @@ -379,7 +382,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args, types) => { + ValueKind::AppliedBuiltin(b, args, types, env) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); let types = types @@ -387,7 +390,7 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { .cloned() .chain(once(f.get_type().unwrap())) .collect(); - apply_builtin(*b, args, ty, types) + apply_builtin(*b, args, ty, types, env.clone()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -625,6 +628,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, + env: &NzEnv, ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, @@ -649,7 +653,7 @@ pub(crate) fn normalize_one_layer( } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -659,11 +663,12 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -827,10 +832,10 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types) => { - apply_builtin(b, args, ty, types) + ValueKind::AppliedBuiltin(b, args, types, env) => { + apply_builtin(b, args, ty, types, env) } - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), + ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -862,6 +867,9 @@ impl NzEnv { pub fn as_quoteenv(&self) -> QuoteEnv { QuoteEnv::construct(self.items.len()) } + pub fn to_alpha_tyenv(&self) -> TyEnv { + TyEnv::from_nzenv_alpha(self) + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -890,6 +898,10 @@ impl NzEnv { NzEnvItem::Replaced(x) => x.clone(), } } + + pub fn size(&self) -> usize { + self.items.len() + } } /// Normalize a TyExpr into WHNF @@ -924,10 +936,18 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - normalize_one_layer(e, &ty) + normalize_one_layer(e, &ty, env) } }; // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } + +/// Ignore NzEnv when comparing +impl std::cmp::PartialEq for NzEnv { + fn eq(&self, _other: &Self) -> bool { + true + } +} +impl std::cmp::Eq for NzEnv {} diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 18e70e4..f559323 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -5,6 +5,7 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TyCtx; use crate::semantics::phase::normalize::merge_maps; +use crate::semantics::phase::normalize::NzEnv; use crate::semantics::phase::Normalized; use crate::semantics::{AlphaVar, Binder, Value, ValueKind}; use crate::syntax; @@ -278,8 +279,11 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { } pub(crate) fn builtin_to_value(b: Builtin) -> Value { + builtin_to_value_env(b, &NzEnv::new()) +} +pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { Value::from_kind_and_type( - ValueKind::from_builtin(b), + ValueKind::from_builtin_env(b, env.clone()), crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) .unwrap() .normalize_whnf_noenv(), @@ -433,11 +437,12 @@ fn type_last_layer( } ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) - if args.len() == 1 => - { - args[0].clone() - } + ValueKind::AppliedBuiltin( + syntax::Builtin::List, + args, + _, + _, + ) if args.len() == 1 => args[0].clone(), _ => return mkerr("InvalidListType"), }; RetWhole(Value::from_kind_and_type( @@ -596,7 +601,7 @@ fn type_last_layer( } ExprKind::BinOp(ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _, _) => {} + ValueKind::AppliedBuiltin(List, _, _, _) => {} _ => return mkerr("BinOpTypeMismatch"), } @@ -666,6 +671,7 @@ fn type_last_layer( syntax::Builtin::Optional, args, _, + _, ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); -- cgit v1.2.3