From 015b76ce47af5b1b31661a934aee13843215c6b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 16:48:33 +0000 Subject: Construct T/Build closures in Expr space --- dhall/src/semantics/phase/normalize.rs | 113 +++++++++++++++++---------------- 1 file changed, 57 insertions(+), 56 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index bf0c626..0c581fe 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,7 +3,8 @@ use std::convert::TryInto; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::core::var::Subst; +use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; use crate::syntax; use crate::syntax::Const::Type; @@ -14,60 +15,51 @@ use crate::syntax::{ // Ad-hoc macro to help construct closures macro_rules! make_closure { - (#$var:ident) => { $var.clone() }; - (var($var:ident, $n:expr, $($ty:tt)*)) => {{ - let var = AlphaVar::from_var_and_alpha( + (var($var:ident)) => {{ + rc(ExprKind::Var(syntax::V( Label::from(stringify!($var)).into(), - $n - ); - ValueKind::Var(var) - .into_value_with_type(make_closure!($($ty)*)) + 0 + ))) }}; - // Warning: assumes that $ty, as a dhall value, has type `Type` (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var: AlphaLabel = Label::from(stringify!($var)).into(); + let var = Label::from(stringify!($var)); let ty = make_closure!($($ty)*); let body = make_closure!($($body)*); - let body_ty = body.get_type_not_sort(); - let lam_ty = ValueKind::Pi(var.clone(), ty.clone(), body_ty) - .into_value_with_type(Value::from_const(Type)); - ValueKind::Lam(var, ty, body).into_value_with_type(lam_ty) + rc(ExprKind::Lam(var, ty, body)) }}; - (Natural) => { - Value::from_builtin(Builtin::Natural) + (Type) => { + rc(ExprKind::Const(Type)) }; - (List $($rest:tt)*) => { - Value::from_builtin(Builtin::List) - .app(make_closure!($($rest)*)) + (Natural) => { + rc(ExprKind::Builtin(Builtin::Natural)) }; - (Some($($rest:tt)*)) => {{ - let v = make_closure!($($rest)*); - let v_type = v.get_type_not_sort(); - let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type); - ValueKind::NEOptionalLit(v).into_value_with_type(opt_v_type) + (List $($ty:tt)*) => {{ + let ty = make_closure!($($ty)*); + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + ty + )) }}; - (1 + $($rest:tt)*) => { - ValueKind::PartialExpr(ExprKind::BinOp( + (Some($($v:tt)*)) => { + rc(ExprKind::SomeLit( + make_closure!($($v)*) + )) + }; + (1 + $($v:tt)*) => { + rc(ExprKind::BinOp( syntax::BinOp::NaturalPlus, - make_closure!($($rest)*), - Value::from_kind_and_type( - ValueKind::NaturalLit(1), - make_closure!(Natural) - ), - )).into_value_with_type( - make_closure!(Natural) - ) + make_closure!($($v)*), + rc(ExprKind::NaturalLit(1)) + )) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ let head = make_closure!($($head)*); let tail = make_closure!($($tail)*); - let list_type = tail.get_type_not_sort(); - ValueKind::PartialExpr(ExprKind::BinOp( + rc(ExprKind::BinOp( syntax::BinOp::ListAppend, - ValueKind::NEListLit(vec![head]) - .into_value_with_type(list_type.clone()), + rc(ExprKind::NEListLit(vec![head])), tail, - )).into_value_with_type(list_type) + )) }}; } @@ -274,16 +266,16 @@ pub(crate) fn apply_builtin( let list_t = Value::from_builtin(List).app(t.clone()); Ret::Value( f.app(list_t.clone()) - .app({ - // Move `t` under new variables - let t1 = t.under_binder(Label::from("a")); - let t2 = t1.under_binder(Label::from("as")); - make_closure!( - λ(a : #t) -> - λ(as : List #t1) -> - [ var(a, 1, #t2) ] # var(as, 0, List #t2) - ) - }) + .app( + typecheck(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)), ) } @@ -302,10 +294,15 @@ pub(crate) fn apply_builtin( let optional_t = Value::from_builtin(Optional).app(t.clone()); Ret::Value( f.app(optional_t.clone()) - .app({ - let t1 = t.under_binder(Label::from("a")); - make_closure!(λ(a: #t) -> Some(var(a, 0, #t1))) - }) + .app( + typecheck(make_closure!( + λ(T : Type) -> + λ(a : var(T)) -> + Some(var(a)) + )) + .unwrap() + .app(t.clone()), + ) .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), @@ -324,9 +321,13 @@ pub(crate) fn apply_builtin( }, (NaturalBuild, [f]) => Ret::Value( f.app(Value::from_builtin(Natural)) - .app(make_closure!( - λ(x : Natural) -> 1 + var(x, 0, Natural) - )) + .app( + typecheck(make_closure!( + λ(x : Natural) -> + 1 + var(x) + )) + .unwrap(), + ) .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), -- cgit v1.2.3 From 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 14:26:40 +0000 Subject: Parameterize ValueKind by its subnodes --- dhall/src/semantics/phase/normalize.rs | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 0c581fe..7b4b37f 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -68,13 +68,13 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, -) -> ValueKind { +) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; // Small helper enum enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), Value(Value), // For applications that can return a function, it's important to keep the remaining // arguments to apply them to the resulting function. @@ -365,7 +365,7 @@ pub(crate) fn apply_builtin( } } -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { +pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { ValueKind::Lam(x, _, e) => { @@ -456,7 +456,7 @@ where // Small helper enum to avoid repetition enum Ret<'a> { - ValueKind(ValueKind), + ValueKind(ValueKind), Value(Value), ValueRef(&'a Value), Expr(ExprKind), @@ -589,7 +589,7 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, ty: &Value, -) -> ValueKind { +) -> ValueKind { use ValueKind::{ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, @@ -779,7 +779,10 @@ pub(crate) fn normalize_one_layer( } /// Normalize a ValueKind into WHNF -pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind { +pub(crate) fn normalize_whnf( + v: ValueKind, + ty: &Value, +) -> ValueKind { match v { ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), -- cgit v1.2.3 From 72d1e3c339cf550fa5af9981af6078a813feb80a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 11:03:40 +0000 Subject: Remove Shift/Subst traits --- dhall/src/semantics/phase/normalize.rs | 1 - 1 file changed, 1 deletion(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7b4b37f..615b2ff 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,7 +3,6 @@ use std::convert::TryInto; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::Subst; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; use crate::syntax; -- cgit v1.2.3 From 37acac4b972b38e8dbe2d174dae1031e5a8eda67 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 16:09:35 +0000 Subject: Tweak: handle empty lists in typeck --- dhall/src/semantics/phase/normalize.rs | 20 ++++---------------- 1 file changed, 4 insertions(+), 16 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 615b2ff..8f9a58a 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -590,9 +590,9 @@ pub(crate) fn normalize_one_layer( ty: &Value, ) -> ValueKind { use ValueKind::{ - AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, - IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit, - UnionConstructor, UnionLit, UnionType, + BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, + NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, + UnionLit, UnionType, }; let ret = match expr { @@ -609,6 +609,7 @@ pub(crate) fn normalize_one_layer( | ExprKind::Builtin(_) | ExprKind::Var(_) | ExprKind::Annot(_, _) + | ExprKind::EmptyListLit(_) | ExprKind::RecordType(_) | ExprKind::UnionType(_) => { unreachable!("This case should have been handled in typecheck") @@ -620,19 +621,6 @@ pub(crate) fn normalize_one_layer( ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), - ExprKind::EmptyListLit(ref t) => { - // Check if the type is of the form `List x` - let t_borrow = t.as_whnf(); - match &*t_borrow { - AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueKind(EmptyListLit(args[0].clone())) - } - _ => { - drop(t_borrow); - Ret::Expr(expr) - } - } - } ExprKind::NEListLit(elts) => { Ret::ValueKind(NEListLit(elts.into_iter().collect())) } -- cgit v1.2.3 From b7d847cc812e6a7ce52354b15a9ed6b41ffeb3b4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 18:57:52 +0000 Subject: Simplify --- dhall/src/semantics/phase/normalize.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f9a58a..541a196 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; +use crate::semantics::{AlphaVar, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -367,9 +366,9 @@ pub(crate) fn apply_builtin( pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueKind::Lam(x, _, e) => { - e.subst_shift(&x.into(), &a).to_whnf_check_type(ty) - } + ValueKind::Lam(_, _, e) => e + .subst_shift(&AlphaVar::default(), &a) + .to_whnf_check_type(ty), ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); -- cgit v1.2.3 From aec80599f161096b68cac88ffb8852a61b62fcfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 19 Jan 2020 18:30:13 +0000 Subject: Restore more types in value_to_tyexpr --- dhall/src/semantics/phase/normalize.rs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 541a196..f0a6a8c 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -374,9 +374,13 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let args = args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(*b, args, ty) } - ValueKind::UnionConstructor(l, kts) => { - ValueKind::UnionLit(l.clone(), a, kts.clone()) - } + ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( + l.clone(), + a, + kts.clone(), + uniont.clone(), + f.get_type().unwrap(), + ), _ => { drop(f_borrow); ValueKind::PartialExpr(ExprKind::App(f, a)) @@ -692,9 +696,11 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - UnionType(kts) => { - Ret::ValueKind(UnionConstructor(l.clone(), kts.clone())) - } + UnionType(kts) => Ret::ValueKind(UnionConstructor( + l.clone(), + kts.clone(), + v.get_type().unwrap(), + )), _ => { drop(v_borrow); Ret::Expr(expr) @@ -710,7 +716,8 @@ pub(crate) fn normalize_one_layer( let handlers_borrow = handlers.as_whnf(); let variant_borrow = variant.as_whnf(); match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) + { Some(h) => Ret::Value(h.clone()), None => { drop(handlers_borrow); @@ -718,7 +725,7 @@ pub(crate) fn normalize_one_layer( Ret::Expr(expr) } }, - (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { + (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { Some(h) => Ret::Value(h.app(v.clone())), None => { drop(handlers_borrow); -- cgit v1.2.3 From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 Jan 2020 22:22:01 +0000 Subject: Implement basic env-based normalization for Value-based TyExpr --- dhall/src/semantics/phase/normalize.rs | 85 +++++++++++++++++++++++++++++++++- 1 file changed, 84 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f0a6a8c..7fd76df 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,9 +1,12 @@ use std::collections::HashMap; use std::convert::TryInto; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{rc, typecheck}; use crate::semantics::phase::Normalized; -use crate::semantics::{AlphaVar, Value, ValueKind}; +use crate::semantics::{ + AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -786,3 +789,83 @@ pub(crate) fn normalize_whnf( v => v, } } + +#[derive(Debug, Clone)] +enum NzEnvItem { + // Variable is bound with given type + Kept(Value), + // Variable has been replaced by corresponding value + Replaced(Value), +} + +#[derive(Debug, Clone)] +pub(crate) struct NzEnv { + items: Vec, +} + +impl NzEnv { + pub fn new() -> Self { + NzEnv { items: Vec::new() } + } + + pub fn insert_type(&self, t: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Kept(t)); + env + } + pub fn insert_value(&self, e: Value) -> Self { + let mut env = self.clone(); + env.items.push(NzEnvItem::Replaced(e)); + env + } + pub fn lookup_val(&self, var: &AlphaVar) -> Value { + let idx = self.items.len() - 1 - var.idx(); + match &self.items[idx] { + NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( + ValueKind::Var(var.clone(), NzVar::new(idx)), + ty.clone(), + ), + NzEnvItem::Replaced(x) => x.clone(), + } + } +} + +/// Normalize a TyExpr into WHNF +pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { + let kind = match e.kind() { + TyExprKind::Var(var) => return env.lookup_val(var), + TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + ValueKind::LamClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + ValueKind::PiClosure { + binder: Binder::new(binder.clone()), + annot: annot.normalize_whnf(env), + closure: Closure::new(env, body.clone()), + } + } + TyExprKind::Expr(e) => { + let e = e.map_ref(|tye| tye.normalize_whnf(env)); + match e { + ExprKind::App(f, arg) => { + let f_borrow = f.as_whnf(); + match &*f_borrow { + ValueKind::LamClosure { closure, .. } => { + return closure.apply(arg) + } + _ => { + drop(f_borrow); + ValueKind::PartialExpr(ExprKind::App(f, arg)) + } + } + } + _ => ValueKind::PartialExpr(e), + } + } + }; + Value::from_kind_and_type_whnf(kind, e.get_type().unwrap()) +} -- cgit v1.2.3 From fccccac6463cb3ca91206d5c41bbf51fc2ec4e0f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 16:01:08 +0000 Subject: Reuse normalize_one_layer in new eval flow --- dhall/src/semantics/phase/normalize.rs | 68 ++++++++++++++++++++-------------- 1 file changed, 41 insertions(+), 27 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7fd76df..75d61d5 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -2,7 +2,9 @@ use std::collections::HashMap; use std::convert::TryInto; use crate::semantics::nze::NzVar; -use crate::semantics::phase::typecheck::{rc, typecheck}; +use crate::semantics::phase::typecheck::{ + builtin_to_value, const_to_value, rc, typecheck, +}; use crate::semantics::phase::Normalized; use crate::semantics::{ AlphaVar, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, @@ -372,6 +374,9 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::Lam(_, _, e) => e .subst_shift(&AlphaVar::default(), &a) .to_whnf_check_type(ty), + ValueKind::LamClosure { closure, .. } => { + closure.apply(a).to_whnf_check_type(ty) + } ValueKind::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); @@ -597,8 +602,8 @@ pub(crate) fn normalize_one_layer( ) -> ValueKind { use ValueKind::{ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor, - UnionLit, UnionType, + NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, + UnionConstructor, UnionLit, UnionType, }; let ret = match expr { @@ -611,15 +616,12 @@ pub(crate) fn normalize_one_layer( | ExprKind::Pi(_, _, _) | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Const(_) - | ExprKind::Builtin(_) | ExprKind::Var(_) - | ExprKind::Annot(_, _) - | ExprKind::EmptyListLit(_) - | ExprKind::RecordType(_) - | ExprKind::UnionType(_) => { + | ExprKind::Annot(_, _) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Const(c) => Ret::Value(const_to_value(c)), + ExprKind::Builtin(b) => Ret::Value(builtin_to_value(b)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), @@ -627,12 +629,29 @@ pub(crate) fn normalize_one_layer( ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), 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() + } + _ => panic!("internal type error"), + }; + Ret::ValueKind(ValueKind::EmptyListLit(arg)) + } ExprKind::NEListLit(elts) => { Ret::ValueKind(NEListLit(elts.into_iter().collect())) } ExprKind::RecordLit(kvs) => { Ret::ValueKind(RecordLit(kvs.into_iter().collect())) } + ExprKind::RecordType(kvs) => { + Ret::ValueKind(RecordType(kvs.into_iter().collect())) + } + ExprKind::UnionType(kvs) => { + Ret::ValueKind(UnionType(kvs.into_iter().collect())) + } ExprKind::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); @@ -665,6 +684,13 @@ pub(crate) fn normalize_one_layer( } } } + // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { } + // ExprKind::BinOp(Equivalence, l, r) => { + // RetWhole(Value::from_kind_and_type( + // ValueKind::Equivalence(l.clone(), r.clone()), + // Value::from_const(Type), + // )) + // } ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), @@ -831,8 +857,9 @@ impl NzEnv { } /// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { - let kind = match e.kind() { +pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { + let ty = tye.get_type().unwrap(); + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { ValueKind::LamClosure { @@ -850,22 +877,9 @@ pub(crate) fn normalize_tyexpr_whnf(e: &TyExpr, env: &NzEnv) -> Value { } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); - match e { - ExprKind::App(f, arg) => { - let f_borrow = f.as_whnf(); - match &*f_borrow { - ValueKind::LamClosure { closure, .. } => { - return closure.apply(arg) - } - _ => { - drop(f_borrow); - ValueKind::PartialExpr(ExprKind::App(f, arg)) - } - } - } - _ => ValueKind::PartialExpr(e), - } + normalize_one_layer(e, &ty) } }; - Value::from_kind_and_type_whnf(kind, e.get_type().unwrap()) + + Value::from_kind_and_type_whnf(kind, ty) } -- cgit v1.2.3 From bd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 16:29:25 +0000 Subject: Restore all types in Value::to_tyexpr --- dhall/src/semantics/phase/normalize.rs | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 75d61d5..8f3953d 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -71,6 +71,7 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, + types: Vec, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -364,7 +365,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args), + Ret::DoneAsIs => AppliedBuiltin(b, args, types), } } @@ -377,10 +378,15 @@ 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) => { + ValueKind::AppliedBuiltin(b, args, types) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args, ty) + let types = types + .iter() + .cloned() + .chain(once(f.get_type().unwrap())) + .collect(); + apply_builtin(*b, args, ty, types) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -631,7 +637,7 @@ 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) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => { args[0].clone() @@ -806,7 +812,9 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueKind::AppliedBuiltin(b, args, types) => { + apply_builtin(b, args, ty, types) + } ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) -- cgit v1.2.3 From 700ff482fbff8960bc0e792fec6fd538c5428d70 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 17:07:56 +0000 Subject: Normalize more expressions --- dhall/src/semantics/phase/normalize.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 8f3953d..ac60ce0 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -594,10 +594,14 @@ fn apply_binop<'a>( Ret::ValueKind(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) | (Equivalence, _, _) => { + (RecursiveRecordTypeMerge, _, _) => { unreachable!("This case should have been handled in typecheck") } + (Equivalence, _, _) => { + Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) + } + _ => return None, }) } @@ -690,13 +694,6 @@ pub(crate) fn normalize_one_layer( } } } - // ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => { } - // ExprKind::BinOp(Equivalence, l, r) => { - // RetWhole(Value::from_kind_and_type( - // ValueKind::Equivalence(l.clone(), r.clone()), - // Value::from_const(Type), - // )) - // } ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { Some(ret) => ret, None => Ret::Expr(expr), -- cgit v1.2.3 From a24f2d1367b2848779014c7bb3ecfe6bfbcff7d7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 18:38:30 +0000 Subject: Fix some variable shifting failures --- dhall/src/semantics/phase/normalize.rs | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ac60ce0..3ddfb84 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -12,8 +12,8 @@ use crate::semantics::{ use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, - Label, NaiveDouble, + BinOp, Builtin, Const, ExprKind, InterpolatedText, + InterpolatedTextContents, Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -822,7 +822,7 @@ pub(crate) fn normalize_whnf( } #[derive(Debug, Clone)] -enum NzEnvItem { +pub(crate) enum NzEnvItem { // Variable is bound with given type Kept(Value), // Variable has been replaced by corresponding value @@ -838,6 +838,9 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } + pub fn construct(items: Vec) -> Self { + NzEnv { items } + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -851,9 +854,16 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); + let var_idx = self.items[..idx] + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(var.clone(), NzVar::new(var_idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), @@ -863,7 +873,11 @@ impl NzEnv { /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = tye.get_type().unwrap(); + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return Value::from_const(Const::Sort), + }; + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { -- cgit v1.2.3 From b72f0968ac19058b9cc513ab0ed1785133232a3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 21:33:21 +0000 Subject: Implement basic typecheck with new approach --- dhall/src/semantics/phase/normalize.rs | 1 + 1 file changed, 1 insertion(+) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 3ddfb84..e848601 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,3 +1,4 @@ +#![allow(dead_code)] use std::collections::HashMap; use std::convert::TryInto; -- cgit v1.2.3 From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:15:17 +0000 Subject: Typecheck more cases --- dhall/src/semantics/phase/normalize.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index e848601..066a004 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -625,12 +625,14 @@ pub(crate) fn normalize_one_layer( // `RetWhole`), so they won't appear here. ExprKind::Lam(_, _, _) | ExprKind::Pi(_, _, _) - | ExprKind::Let(_, _, _, _) | ExprKind::Embed(_) - | ExprKind::Var(_) - | ExprKind::Annot(_, _) => { + | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } + ExprKind::Let(_, _, val, body) => { + Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) + } + 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::Assert(_) => Ret::Expr(expr), @@ -895,11 +897,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { closure: Closure::new(env, body.clone()), } } + TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { + let val = val.normalize_whnf(env); + return body.normalize_whnf(&env.insert_value(val)); + } TyExprKind::Expr(e) => { let e = e.map_ref(|tye| tye.normalize_whnf(env)); normalize_one_layer(e, &ty) } }; + // dbg!(tye.kind(), env, &kind); Value::from_kind_and_type_whnf(kind, ty) } -- cgit v1.2.3 From f2e8c414993d5c9fcc63f5c035f755712c01dad0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:20:53 +0000 Subject: Enable comparing Closures for equality --- dhall/src/semantics/phase/normalize.rs | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 066a004..7f547d7 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -884,17 +884,20 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { + let annot = annot.normalize_whnf(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), - annot: annot.normalize_whnf(env), - closure: Closure::new(env, body.clone()), + annot: annot.clone(), + closure: Closure::new(annot, env, body.clone()), } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { + let annot = annot.normalize_whnf(env); + let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), - annot: annot.normalize_whnf(env), - closure: Closure::new(env, body.clone()), + annot, + closure, } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { -- cgit v1.2.3 From 574fb56e87c1a71dc8d7efbff2789d3cfabdc529 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 13:51:24 +0000 Subject: More typecheck --- dhall/src/semantics/phase/normalize.rs | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 7f547d7..33e1f2b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -595,8 +595,23 @@ fn apply_binop<'a>( Ret::ValueKind(RecordLit(kvs)) } - (RecursiveRecordTypeMerge, _, _) => { - unreachable!("This case should have been handled in typecheck") + (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { + let kts = merge_maps::<_, _, _, !>( + kts_x, + kts_y, + // If the Label exists for both records, then we hit the recursive case. + |_, l: &Value, r: &Value| { + Ok(Value::from_kind_and_type( + ValueKind::PartialExpr(ExprKind::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + )), + ty.clone(), + )) + }, + )?; + Ret::ValueKind(RecordType(kts)) } (Equivalence, _, _) => { -- cgit v1.2.3 From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 Jan 2020 18:45:09 +0000 Subject: Fix a bunch of bugs and more tck --- dhall/src/semantics/phase/normalize.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/phase/normalize.rs') 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) -> 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(); -- cgit v1.2.3 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 ++++++++++++++++++++++------------ 1 file changed, 45 insertions(+), 25 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') 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 {} -- cgit v1.2.3 From 7683b0d762cf0df489ad4bc006e8db2358e81cf4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 21:50:04 +0000 Subject: Implement assert & merge and fix more bugs --- dhall/src/semantics/phase/normalize.rs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index a11cb75..532dae3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -855,17 +855,30 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, + vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { items: Vec::new() } + NzEnv { + items: Vec::new(), + vars: QuoteEnv::new(), + } } pub fn construct(items: Vec) -> Self { - NzEnv { items } + let vars = QuoteEnv::construct( + items + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(), + ); + NzEnv { items, vars } } pub fn as_quoteenv(&self) -> QuoteEnv { - QuoteEnv::construct(self.items.len()) + self.vars } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -874,6 +887,7 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); + env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { -- cgit v1.2.3 From f31ccaa40df77b1ca8b37db46a819460c831006e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:17:12 +0000 Subject: Fix more bugs --- dhall/src/semantics/phase/normalize.rs | 32 ++++---------------------------- 1 file changed, 4 insertions(+), 28 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 532dae3..f4e4099 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, QuoteEnv}; +use crate::semantics::nze::NzVar; use crate::semantics::phase::typecheck::{ builtin_to_value_env, const_to_value, rc, }; @@ -855,30 +855,14 @@ pub(crate) enum NzEnvItem { #[derive(Debug, Clone)] pub(crate) struct NzEnv { items: Vec, - vars: QuoteEnv, } impl NzEnv { pub fn new() -> Self { - NzEnv { - items: Vec::new(), - vars: QuoteEnv::new(), - } + NzEnv { items: Vec::new() } } pub fn construct(items: Vec) -> Self { - let vars = QuoteEnv::construct( - items - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(), - ); - NzEnv { items, vars } - } - pub fn as_quoteenv(&self) -> QuoteEnv { - self.vars + NzEnv { items } } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) @@ -887,7 +871,6 @@ impl NzEnv { pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); env.items.push(NzEnvItem::Kept(t)); - env.vars = env.vars.insert(); env } pub fn insert_value(&self, e: Value) -> Self { @@ -897,16 +880,9 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); - let var_idx = self.items[..idx] - .iter() - .filter(|i| match i { - NzEnvItem::Kept(_) => true, - NzEnvItem::Replaced(_) => false, - }) - .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(var_idx)), + ValueKind::Var(var.clone(), NzVar::new(idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), -- cgit v1.2.3 From db6c09f33c3c794e4b6ec8a7aa80978d945a9d7a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:26:42 +0000 Subject: Remove dead code --- dhall/src/semantics/phase/normalize.rs | 7 ------- 1 file changed, 7 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f4e4099..d40456b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,4 +1,3 @@ -#![allow(dead_code)] use std::collections::HashMap; use std::convert::TryInto; @@ -376,9 +375,6 @@ pub(crate) fn apply_builtin( pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueKind::Lam(_, _, e) => e - .subst_shift(&AlphaVar::default(), &a) - .to_whnf_check_type(ty), ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } @@ -861,9 +857,6 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } - pub fn construct(items: Vec) -> Self { - NzEnv { items } - } pub fn to_alpha_tyenv(&self) -> TyEnv { TyEnv::from_nzenv_alpha(self) } -- cgit v1.2.3 From 280b3174476ef8fe5a98f3614f4fe253fa243d8c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:35:28 +0000 Subject: Finally get rid of all of the shift/subst_shift ! --- dhall/src/semantics/phase/normalize.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d40456b..fa80b6e 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -638,15 +638,13 @@ pub(crate) fn normalize_one_layer( ), // Those cases have already been completely handled in the typechecking phase (using // `RetWhole`), so they won't appear here. - ExprKind::Lam(_, _, _) - | ExprKind::Pi(_, _, _) + ExprKind::Lam(..) + | ExprKind::Pi(..) + | ExprKind::Let(..) | ExprKind::Embed(_) | ExprKind::Var(_) => { unreachable!("This case should have been handled in typecheck") } - ExprKind::Let(_, _, val, body) => { - Ret::Value(body.subst_shift(&AlphaVar::default(), &val)) - } ExprKind::Annot(x, _) => Ret::Value(x), ExprKind::Const(c) => Ret::Value(const_to_value(c)), ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), -- cgit v1.2.3 From 489174a426e6057a68b6edd2e9b4387d09912a25 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 21:56:52 +0000 Subject: Move envs to their own files --- dhall/src/semantics/phase/normalize.rs | 62 ++-------------------------------- 1 file changed, 2 insertions(+), 60 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index fa80b6e..ce37993 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,16 +1,13 @@ use std::collections::HashMap; use std::convert::TryInto; -use crate::semantics::nze::NzVar; use crate::semantics::phase::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, -}; +use crate::semantics::NzEnv; +use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ @@ -838,53 +835,6 @@ pub(crate) fn normalize_whnf( } } -#[derive(Debug, Clone)] -pub(crate) enum NzEnvItem { - // Variable is bound with given type - Kept(Value), - // Variable has been replaced by corresponding value - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct NzEnv { - items: Vec, -} - -impl NzEnv { - pub fn new() -> Self { - NzEnv { items: Vec::new() } - } - 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(); - env.items.push(NzEnvItem::Kept(t)); - env - } - pub fn insert_value(&self, e: Value) -> Self { - let mut env = self.clone(); - env.items.push(NzEnvItem::Replaced(e)); - env - } - pub fn lookup_val(&self, var: &AlphaVar) -> Value { - let idx = self.items.len() - 1 - var.idx(); - match &self.items[idx] { - NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), - ty.clone(), - ), - NzEnvItem::Replaced(x) => x.clone(), - } - } - - pub fn size(&self) -> usize { - self.items.len() - } -} - /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let ty = match tye.get_type() { @@ -924,11 +874,3 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { // 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 {} -- cgit v1.2.3 From 655f67fb29ca847f86c3e19338757e7b031d4f50 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:09:39 +0000 Subject: Move builtins-related code to its own module --- dhall/src/semantics/phase/normalize.rs | 373 +-------------------------------- 1 file changed, 6 insertions(+), 367 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ce37993..2d4b4b3 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -1,373 +1,12 @@ use std::collections::HashMap; -use std::convert::TryInto; -use crate::semantics::phase::typecheck::{ - builtin_to_value_env, const_to_value, rc, -}; use crate::semantics::phase::Normalized; -use crate::semantics::tck::typecheck::type_with; use crate::semantics::NzEnv; -use crate::semantics::{Binder, Closure, TyExpr, TyExprKind, Value, ValueKind}; -use crate::syntax; -use crate::syntax::Const::Type; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, +use crate::semantics::{ + apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, }; - -// Ad-hoc macro to help construct closures -macro_rules! make_closure { - (var($var:ident)) => {{ - rc(ExprKind::Var(syntax::V( - Label::from(stringify!($var)).into(), - 0 - ))) - }}; - (λ($var:tt : $($ty:tt)*) -> $($body:tt)*) => {{ - let var = Label::from(stringify!($var)); - let ty = make_closure!($($ty)*); - let body = make_closure!($($body)*); - rc(ExprKind::Lam(var, ty, body)) - }}; - (Type) => { - rc(ExprKind::Const(Type)) - }; - (Natural) => { - rc(ExprKind::Builtin(Builtin::Natural)) - }; - (List $($ty:tt)*) => {{ - let ty = make_closure!($($ty)*); - rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - ty - )) - }}; - (Some($($v:tt)*)) => { - rc(ExprKind::SomeLit( - make_closure!($($v)*) - )) - }; - (1 + $($v:tt)*) => { - rc(ExprKind::BinOp( - syntax::BinOp::NaturalPlus, - make_closure!($($v)*), - rc(ExprKind::NaturalLit(1)) - )) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => {{ - let head = make_closure!($($head)*); - let tail = make_closure!($($tail)*); - rc(ExprKind::BinOp( - syntax::BinOp::ListAppend, - rc(ExprKind::NEListLit(vec![head])), - tail, - )) - }}; -} - -#[allow(clippy::cognitive_complexity)] -pub(crate) fn apply_builtin( - b: Builtin, - args: Vec, - ty: &Value, - types: Vec, - env: NzEnv, -) -> ValueKind { - use syntax::Builtin::*; - use ValueKind::*; - - // Small helper enum - enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - // For applications that can return a function, it's important to keep the remaining - // arguments to apply them to the resulting function. - 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())), - (NaturalIsZero, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalEven, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), - _ => Ret::DoneAsIs, - }, - (NaturalOdd, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), - _ => Ret::DoneAsIs, - }, - (NaturalToInteger, [n]) => match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), - _ => Ret::DoneAsIs, - }, - (NaturalShow, [n]) => { - match &*n.as_whnf() { - NaturalLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) - } - (NaturalLit(0), _) => Ret::Value(b.clone()), - (_, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), - _ if a == b => Ret::ValueKind(NaturalLit(0)), - _ => Ret::DoneAsIs, - }, - (IntegerShow, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - let s = if *n < 0 { - n.to_string() - } else { - format!("+{}", n) - }; - Ret::ValueKind(TextLit(vec![InterpolatedTextContents::Text(s)])) - } - _ => Ret::DoneAsIs, - }, - (IntegerToDouble, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) - } - _ => Ret::DoneAsIs, - }, - (IntegerNegate, [n]) => match &*n.as_whnf() { - IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), - _ => Ret::DoneAsIs, - }, - (IntegerClamp, [n]) => match &*n.as_whnf() { - IntegerLit(n) => { - Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) - } - _ => Ret::DoneAsIs, - }, - (DoubleShow, [n]) => { - match &*n.as_whnf() { - DoubleLit(n) => Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(n.to_string()), - ])), - _ => Ret::DoneAsIs, - } - } - (TextShow, [v]) => match &*v.as_whnf() { - TextLit(elts) => { - match elts.as_slice() { - // Empty string literal. - [] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = - std::iter::empty().collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - // If there are no interpolations (invariants ensure that when there are no - // interpolations, there is a single Text item) in the literal. - [InterpolatedTextContents::Text(s)] => { - // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = - std::iter::once(InterpolatedTextContents::Text( - s.clone(), - )) - .collect(); - let s = txt.to_string(); - Ret::ValueKind(TextLit(vec![ - InterpolatedTextContents::Text(s), - ])) - } - _ => Ret::DoneAsIs, - } - } - _ => Ret::DoneAsIs, - }, - (ListLength, [_, l]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), - NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), - _ => Ret::DoneAsIs, - }, - (ListHead, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) - } - _ => Ret::DoneAsIs, - }, - (ListLast, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( - xs.iter().rev().next().unwrap().clone(), - )), - _ => Ret::DoneAsIs, - }, - (ListReverse, [_, l]) => match &*l.as_whnf() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), - NEListLit(xs) => { - Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) - } - _ => Ret::DoneAsIs, - }, - (ListIndexed, [_, l]) => { - let l_whnf = l.as_whnf(); - match &*l_whnf { - EmptyListLit(_) | NEListLit(_) => { - // Extract the type of the list elements - let t = match &*l_whnf { - EmptyListLit(t) => t.clone(), - NEListLit(xs) => xs[0].get_type_not_sort(), - _ => unreachable!(), - }; - - // Construct the returned record type: { index: Natural, value: t } - let mut kts = HashMap::new(); - kts.insert("index".into(), Value::from_builtin(Natural)); - kts.insert("value".into(), t.clone()); - let t = Value::from_kind_and_type( - RecordType(kts), - Value::from_const(Type), - ); - - // Construct the new list, with added indices - let list = match &*l_whnf { - EmptyListLit(_) => EmptyListLit(t), - NEListLit(xs) => NEListLit( - xs.iter() - .enumerate() - .map(|(i, e)| { - let mut kvs = HashMap::new(); - kvs.insert( - "index".into(), - Value::from_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), - ); - kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) - }) - .collect(), - ), - _ => unreachable!(), - }; - Ret::ValueKind(list) - } - _ => Ret::DoneAsIs, - } - } - (ListBuild, [t, f]) => { - let list_t = Value::from_builtin(List).app(t.clone()); - Ret::Value( - f.app(list_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - λ(as : List var(T)) -> - [ var(a) ] # var(as) - )) - .app(t.clone()), - ) - .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), - ) - } - (ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() { - EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()), - NEListLit(xs) => { - let mut v = nil.clone(); - for x in xs.iter().cloned().rev() { - v = cons.app(x).app(v); - } - Ret::ValueWithRemainingArgs(r, v) - } - _ => Ret::DoneAsIs, - }, - (OptionalBuild, [t, f]) => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); - Ret::Value( - f.app(optional_t.clone()) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - Some(var(a)) - )) - .app(t.clone()), - ) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), - ) - } - (OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf() - { - EmptyOptionalLit(_) => { - Ret::ValueWithRemainingArgs(r, nothing.clone()) - } - NEOptionalLit(x) => { - Ret::ValueWithRemainingArgs(r, just.app(x.clone())) - } - _ => Ret::DoneAsIs, - }, - (NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Natural)) - .app(make_closure(make_closure!( - λ(x : Natural) -> - 1 + var(x) - ))) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), - ), - - (NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() { - NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()), - NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) - .app(t.clone()) - .app(succ.clone()) - .app(zero.clone()); - Ret::ValueWithRemainingArgs(r, succ.app(fold)) - } - _ => Ret::DoneAsIs, - }, - _ => Ret::DoneAsIs, - }; - match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueWithRemainingArgs(unconsumed_args, mut v) => { - let n_consumed_args = args.len() - unconsumed_args.len(); - for x in args.into_iter().skip(n_consumed_args) { - v = v.app(x); - } - v.to_whnf_check_type(ty) - } - Ret::DoneAsIs => AppliedBuiltin(b, args, types, env), - } -} +use crate::syntax; +use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents}; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); @@ -643,8 +282,8 @@ pub(crate) fn normalize_one_layer( unreachable!("This case should have been handled in typecheck") } ExprKind::Annot(x, _) => Ret::Value(x), - ExprKind::Const(c) => Ret::Value(const_to_value(c)), - ExprKind::Builtin(b) => Ret::Value(builtin_to_value_env(b, env)), + ExprKind::Const(c) => Ret::Value(Value::from_const(c)), + ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), ExprKind::Assert(_) => Ret::Expr(expr), ExprKind::App(v, a) => Ret::Value(v.app(a)), ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), -- cgit v1.2.3 From 17732b041dbd44f39ce3d04a289146db9882e865 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 11:53:37 +0000 Subject: Encapsulate partially applied builtin in a separate struct --- dhall/src/semantics/phase/normalize.rs | 31 +++++++++++-------------------- 1 file changed, 11 insertions(+), 20 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 2d4b4b3..d7720c7 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -3,10 +3,11 @@ use std::collections::HashMap; use crate::semantics::phase::Normalized; use crate::semantics::NzEnv; use crate::semantics::{ - apply_builtin, Binder, Closure, TyExpr, TyExprKind, Value, ValueKind, + Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, +}; +use crate::syntax::{ + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, }; -use crate::syntax; -use crate::syntax::{BinOp, Const, ExprKind, InterpolatedTextContents}; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { let f_borrow = f.as_whnf(); @@ -14,15 +15,8 @@ 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, env) => { - use std::iter::once; - let args = args.iter().cloned().chain(once(a.clone())).collect(); - let types = types - .iter() - .cloned() - .chain(once(f.get_type().unwrap())) - .collect(); - apply_builtin(*b, args, ty, types, env.clone()) + ValueKind::AppliedBuiltin(closure) => { + closure.apply(a, f.get_type().unwrap(), ty) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -293,12 +287,11 @@ 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, + ValueKind::AppliedBuiltin(BuiltinClosure { + b: Builtin::List, args, - _, - _, - ) if args.len() == 1 => args[0].clone(), + .. + }) if args.len() == 1 => args[0].clone(), _ => panic!("internal type error"), }; Ret::ValueKind(ValueKind::EmptyListLit(arg)) @@ -462,9 +455,7 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args, types, env) => { - apply_builtin(b, args, ty, types, env) - } + ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) -- cgit v1.2.3 From cb86493012b268ec32ad85a42b54fb1a2adab7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 14:20:01 +0000 Subject: s/as_whnf/kind/ --- dhall/src/semantics/phase/normalize.rs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index d7720c7..f36ec4a 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -10,7 +10,7 @@ use crate::syntax::{ }; pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.as_whnf(); + let f_borrow = f.kind(); match &*f_borrow { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) @@ -47,7 +47,7 @@ pub(crate) fn squash_textlit( match contents { Text(s) => crnt_str.push_str(&s), Expr(e) => { - let e_borrow = e.as_whnf(); + let e_borrow = e.kind(); match &*e_borrow { ValueKind::TextLit(elts2) => { inner(elts2.iter().cloned(), crnt_str, ret) @@ -123,8 +123,8 @@ fn apply_binop<'a>( BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, TextLit, }; - let x_borrow = x.as_whnf(); - let y_borrow = y.as_whnf(); + let x_borrow = x.kind(); + let y_borrow = y.kind(); Some(match (o, &*x_borrow, &*y_borrow) { (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), @@ -206,7 +206,7 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.as_whnf(); + let ty_borrow = ty.kind(); let kts = match &*ty_borrow { RecordType(kts) => kts, _ => unreachable!("Internal type error"), @@ -286,7 +286,7 @@ pub(crate) fn normalize_one_layer( ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { - let arg = match &*t.as_whnf() { + let arg = match &*t.kind() { ValueKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, @@ -319,13 +319,13 @@ pub(crate) fn normalize_one_layer( } } ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.as_whnf(); + let b_borrow = b.kind(); match &*b_borrow { BoolLit(true) => Ret::ValueRef(e1), BoolLit(false) => Ret::ValueRef(e2), _ => { - let e1_borrow = e1.as_whnf(); - let e2_borrow = e2.as_whnf(); + let e1_borrow = e1.kind(); + let e2_borrow = e2.kind(); match (&*e1_borrow, &*e2_borrow) { // Simplify `if b then True else False` (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), @@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer( Ret::ValueKind(RecordLit(HashMap::new())) } ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => Ret::ValueKind(RecordLit( ls.iter() @@ -365,7 +365,7 @@ pub(crate) fn normalize_one_layer( } } ExprKind::Field(ref v, ref l) => { - let v_borrow = v.as_whnf(); + let v_borrow = v.kind(); match &*v_borrow { RecordLit(kvs) => match kvs.get(l) { Some(r) => Ret::Value(r.clone()), @@ -391,8 +391,8 @@ pub(crate) fn normalize_one_layer( ExprKind::Completion(_, _) => unimplemented!("record completion"), ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.as_whnf(); - let variant_borrow = variant.as_whnf(); + let handlers_borrow = handlers.kind(); + let variant_borrow = variant.kind(); match (&*handlers_borrow, &*variant_borrow) { (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) { -- cgit v1.2.3 From 67bbbafbc9730d74e20e5ac082ae9a87bdf2234e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 16:39:25 +0000 Subject: Introduce Thunks and normalize lazily --- dhall/src/semantics/phase/normalize.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index f36ec4a..ea1a25b 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -457,6 +457,7 @@ pub(crate) fn normalize_whnf( match v { ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), + ValueKind::Thunk(th) => th.eval().kind().clone(), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) } @@ -475,7 +476,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), annot: annot.clone(), @@ -483,7 +484,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - let annot = annot.normalize_whnf(env); + let annot = annot.eval(env); let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), @@ -492,11 +493,11 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { - let val = val.normalize_whnf(env); - return body.normalize_whnf(&env.insert_value(val)); + let val = val.eval(env); + return body.eval(&env.insert_value(val)); } TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.normalize_whnf(env)); + let e = e.map_ref(|tye| tye.eval(env)); normalize_one_layer(e, &ty, env) } }; -- cgit v1.2.3 From 653cdb44cec4f54697d18f2c4ae9f67bbbc2fb3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:04:28 +0000 Subject: Move normalize under nze --- dhall/src/semantics/phase/normalize.rs | 507 --------------------------------- 1 file changed, 507 deletions(-) delete mode 100644 dhall/src/semantics/phase/normalize.rs (limited to 'dhall/src/semantics/phase/normalize.rs') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs deleted file mode 100644 index ea1a25b..0000000 --- a/dhall/src/semantics/phase/normalize.rs +++ /dev/null @@ -1,507 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::phase::Normalized; -use crate::semantics::NzEnv; -use crate::semantics::{ - Binder, BuiltinClosure, Closure, TyExpr, TyExprKind, Value, ValueKind, -}; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, -}; - -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { - let f_borrow = f.kind(); - match &*f_borrow { - ValueKind::LamClosure { closure, .. } => { - closure.apply(a).to_whnf_check_type(ty) - } - ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type().unwrap(), ty) - } - ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( - l.clone(), - a, - kts.clone(), - uniont.clone(), - f.get_type().unwrap(), - ), - _ => { - drop(f_borrow); - ValueKind::PartialExpr(ExprKind::App(f, a)) - } - } -} - -pub(crate) fn squash_textlit( - elts: impl Iterator>, -) -> Vec> { - use std::mem::replace; - use InterpolatedTextContents::{Expr, Text}; - - fn inner( - elts: impl Iterator>, - crnt_str: &mut String, - ret: &mut Vec>, - ) { - for contents in elts { - match contents { - Text(s) => crnt_str.push_str(&s), - Expr(e) => { - let e_borrow = e.kind(); - match &*e_borrow { - ValueKind::TextLit(elts2) => { - inner(elts2.iter().cloned(), crnt_str, ret) - } - _ => { - drop(e_borrow); - if !crnt_str.is_empty() { - ret.push(Text(replace(crnt_str, String::new()))) - } - ret.push(Expr(e.clone())) - } - } - } - } - } - } - - let mut crnt_str = String::new(); - let mut ret = Vec::new(); - inner(elts, &mut crnt_str, &mut ret); - if !crnt_str.is_empty() { - ret.push(Text(replace(&mut crnt_str, String::new()))) - } - ret -} - -pub(crate) fn merge_maps( - map1: &HashMap, - map2: &HashMap, - mut f: F, -) -> Result, Err> -where - F: FnMut(&K, &V, &V) -> Result, - K: std::hash::Hash + Eq + Clone, - V: Clone, -{ - let mut kvs = HashMap::new(); - for (x, v2) in map2 { - let newv = if let Some(v1) = map1.get(x) { - f(x, v1, v2)? - } else { - v2.clone() - }; - kvs.insert(x.clone(), newv); - } - for (x, v1) in map1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v1.clone()); - } - Ok(kvs) -} - -// Small helper enum to avoid repetition -enum Ret<'a> { - ValueKind(ValueKind), - Value(Value), - ValueRef(&'a Value), - Expr(ExprKind), -} - -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> Option> { - use BinOp::{ - BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, - NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, - RightBiasedRecordMerge, TextAppend, - }; - use ValueKind::{ - BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType, - TextLit, - }; - let x_borrow = x.kind(); - let y_borrow = y.kind(); - Some(match (o, &*x_borrow, &*y_borrow) { - (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y), - (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)), - (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)), - (BoolAnd, _, _) if x == y => Ret::ValueRef(x), - (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)), - (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)), - (BoolOr, BoolLit(false), _) => Ret::ValueRef(y), - (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolOr, _, _) if x == y => Ret::ValueRef(x), - (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y), - (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x), - (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)), - (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)), - (BoolNE, BoolLit(false), _) => Ret::ValueRef(y), - (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x), - (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)), - (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)), - - (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y), - (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(x + y)) - } - (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)), - (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)), - (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y), - (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { - Ret::ValueKind(NaturalLit(x * y)) - } - - (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y), - (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x), - (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind( - NEListLit(xs.iter().chain(ys.iter()).cloned().collect()), - ), - - (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y), - (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x), - (TextAppend, TextLit(x), TextLit(y)) => Ret::ValueKind(TextLit( - squash_textlit(x.iter().chain(y.iter()).cloned()), - )), - (TextAppend, TextLit(x), _) => { - use std::iter::once; - let y = InterpolatedTextContents::Expr(y.clone()); - Ret::ValueKind(TextLit(squash_textlit( - x.iter().cloned().chain(once(y)), - ))) - } - (TextAppend, _, TextLit(y)) => { - use std::iter::once; - let x = InterpolatedTextContents::Expr(x.clone()); - Ret::ValueKind(TextLit(squash_textlit( - once(x).chain(y.iter().cloned()), - ))) - } - - (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let mut kvs = kvs2.clone(); - for (x, v) in kvs1 { - // Insert only if key not already present - kvs.entry(x.clone()).or_insert_with(|| v.clone()); - } - Ret::ValueKind(RecordLit(kvs)) - } - - (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => { - Ret::ValueRef(x) - } - (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => { - Ret::ValueRef(y) - } - (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let ty_borrow = ty.kind(); - let kts = match &*ty_borrow { - RecordType(kts) => kts, - _ => unreachable!("Internal type error"), - }; - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - )), - kts.get(k).expect("Internal type error").clone(), - )) - })?; - Ret::ValueKind(RecordLit(kvs)) - } - - (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => { - let kts = merge_maps::<_, _, _, !>( - kts_x, - kts_y, - // If the Label exists for both records, then we hit the recursive case. - |_, l: &Value, r: &Value| { - Ok(Value::from_kind_and_type( - ValueKind::PartialExpr(ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - )), - ty.clone(), - )) - }, - )?; - Ret::ValueKind(RecordType(kts)) - } - - (Equivalence, _, _) => { - Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone())) - } - - _ => return None, - }) -} - -pub(crate) fn normalize_one_layer( - expr: ExprKind, - ty: &Value, - env: &NzEnv, -) -> ValueKind { - use ValueKind::{ - BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit, - NEOptionalLit, NaturalLit, RecordLit, RecordType, TextLit, - UnionConstructor, UnionLit, UnionType, - }; - - let ret = match expr { - ExprKind::Import(_) => unreachable!( - "There should remain no imports in a resolved expression" - ), - // Those cases have already been completely handled in the typechecking phase (using - // `RetWhole`), so they won't appear here. - ExprKind::Lam(..) - | ExprKind::Pi(..) - | ExprKind::Let(..) - | ExprKind::Embed(_) - | ExprKind::Var(_) => { - unreachable!("This case should have been handled in typecheck") - } - ExprKind::Annot(x, _) => Ret::Value(x), - ExprKind::Const(c) => Ret::Value(Value::from_const(c)), - ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)), - ExprKind::Assert(_) => Ret::Expr(expr), - ExprKind::App(v, a) => Ret::Value(v.app(a)), - ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)), - ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)), - ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)), - ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)), - ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), - ExprKind::EmptyListLit(t) => { - let arg = match &*t.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { - b: Builtin::List, - args, - .. - }) if args.len() == 1 => args[0].clone(), - _ => panic!("internal type error"), - }; - Ret::ValueKind(ValueKind::EmptyListLit(arg)) - } - ExprKind::NEListLit(elts) => { - Ret::ValueKind(NEListLit(elts.into_iter().collect())) - } - ExprKind::RecordLit(kvs) => { - Ret::ValueKind(RecordLit(kvs.into_iter().collect())) - } - ExprKind::RecordType(kvs) => { - Ret::ValueKind(RecordType(kvs.into_iter().collect())) - } - ExprKind::UnionType(kvs) => { - Ret::ValueKind(UnionType(kvs.into_iter().collect())) - } - ExprKind::TextLit(elts) => { - use InterpolatedTextContents::Expr; - let elts: Vec<_> = squash_textlit(elts.into_iter()); - // Simplify bare interpolation - if let [Expr(th)] = elts.as_slice() { - Ret::Value(th.clone()) - } else { - Ret::ValueKind(TextLit(elts)) - } - } - ExprKind::BoolIf(ref b, ref e1, ref e2) => { - let b_borrow = b.kind(); - match &*b_borrow { - BoolLit(true) => Ret::ValueRef(e1), - BoolLit(false) => Ret::ValueRef(e2), - _ => { - let e1_borrow = e1.kind(); - let e2_borrow = e2.kind(); - match (&*e1_borrow, &*e2_borrow) { - // Simplify `if b then True else False` - (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b), - _ if e1 == e2 => Ret::ValueRef(e1), - _ => { - drop(b_borrow); - drop(e1_borrow); - drop(e2_borrow); - Ret::Expr(expr) - } - } - } - } - } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { - Some(ret) => ret, - None => Ret::Expr(expr), - }, - - ExprKind::Projection(_, ref ls) if ls.is_empty() => { - Ret::ValueKind(RecordLit(HashMap::new())) - } - ExprKind::Projection(ref v, ref ls) => { - let v_borrow = v.kind(); - match &*v_borrow { - RecordLit(kvs) => Ret::ValueKind(RecordLit( - ls.iter() - .filter_map(|l| { - kvs.get(l).map(|x| (l.clone(), x.clone())) - }) - .collect(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::Field(ref v, ref l) => { - let v_borrow = v.kind(); - match &*v_borrow { - RecordLit(kvs) => match kvs.get(l) { - Some(r) => Ret::Value(r.clone()), - None => { - drop(v_borrow); - Ret::Expr(expr) - } - }, - UnionType(kts) => Ret::ValueKind(UnionConstructor( - l.clone(), - kts.clone(), - v.get_type().unwrap(), - )), - _ => { - drop(v_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::ProjectionByExpr(_, _) => { - unimplemented!("selection by expression") - } - ExprKind::Completion(_, _) => unimplemented!("record completion"), - - ExprKind::Merge(ref handlers, ref variant, _) => { - let handlers_borrow = handlers.kind(); - let variant_borrow = variant.kind(); - match (&*handlers_borrow, &*variant_borrow) { - (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l) - { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - }, - (RecordLit(kvs), EmptyOptionalLit(_)) => { - match kvs.get(&"None".into()) { - Some(h) => Ret::Value(h.clone()), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - (RecordLit(kvs), NEOptionalLit(v)) => { - match kvs.get(&"Some".into()) { - Some(h) => Ret::Value(h.app(v.clone())), - None => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - _ => { - drop(handlers_borrow); - drop(variant_borrow); - Ret::Expr(expr) - } - } - } - ExprKind::ToMap(_, _) => unimplemented!("toMap"), - }; - - match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueRef(v) => v.to_whnf_check_type(ty), - Ret::Expr(expr) => ValueKind::PartialExpr(expr), - } -} - -/// Normalize a ValueKind into WHNF -pub(crate) fn normalize_whnf( - v: ValueKind, - ty: &Value, -) -> ValueKind { - match v { - ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty), - ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()), - ValueKind::Thunk(th) => th.eval().kind().clone(), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(squash_textlit(elts.into_iter())) - } - // All other cases are already in WHNF - v => v, - } -} - -/// Normalize a TyExpr into WHNF -pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = match tye.get_type() { - Ok(ty) => ty, - Err(_) => return Value::from_const(Const::Sort), - }; - - let kind = match tye.kind() { - TyExprKind::Var(var) => return env.lookup_val(var), - TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { - let annot = annot.eval(env); - ValueKind::LamClosure { - binder: Binder::new(binder.clone()), - annot: annot.clone(), - closure: Closure::new(annot, env, body.clone()), - } - } - TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { - let annot = annot.eval(env); - let closure = Closure::new(annot.clone(), env, body.clone()); - ValueKind::PiClosure { - binder: Binder::new(binder.clone()), - annot, - closure, - } - } - TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { - let val = val.eval(env); - return body.eval(&env.insert_value(val)); - } - TyExprKind::Expr(e) => { - let e = e.map_ref(|tye| tye.eval(env)); - normalize_one_layer(e, &ty, env) - } - }; - - // dbg!(tye.kind(), env, &kind); - Value::from_kind_and_type_whnf(kind, ty) -} -- cgit v1.2.3