From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:58:48 +0000 Subject: Remove move type propagation through Value --- dhall/src/semantics/builtins.rs | 41 ++++++++++------------------------------- 1 file changed, 10 insertions(+), 31 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 907d449..a513967 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -35,11 +35,11 @@ impl BuiltinClosure { } } - pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind { + pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); let types = self.types.iter().cloned().chain(once(f_ty)).collect(); - apply_builtin(self.b, args, ret_ty, types, self.env.clone()) + apply_builtin(self.b, args, types, self.env.clone()) } /// This doesn't break the invariant because we already checked that the appropriate arguments /// did not normalize to something that allows evaluation to proceed. @@ -267,7 +267,6 @@ macro_rules! make_closure { fn apply_builtin( b: Builtin, args: Vec, - ty: &Value, types: Vec, env: NzEnv, ) -> ValueKind { @@ -399,10 +398,7 @@ fn apply_builtin( 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), - ); + let t = Value::from_kind(RecordType(kts)); // Construct the new list, with added indices let list = match &*l_whnf { @@ -414,18 +410,10 @@ fn apply_builtin( let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), + Value::from_kind(NaturalLit(i)), ); kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) + Value::from_kind(RecordLit(kvs)) }) .collect(), ), @@ -449,7 +437,7 @@ fn apply_builtin( )) .app(t.clone()), ) - .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), + .app(EmptyListLit(t.clone()).into_value()), ) } (ListFold, [_, l, _, cons, nil]) => match &*l.kind() { @@ -475,10 +463,7 @@ fn apply_builtin( )) .app(t.clone()), ) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), + .app(EmptyOptionalLit(t.clone()).into_value()), ) } (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { @@ -492,20 +477,14 @@ fn apply_builtin( λ(x : Natural) -> 1 + var(x) ))) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), + .app(NaturalLit(0).into_value()), ), (NaturalFold, [n, t, succ, zero]) => match &*n.kind() { NaturalLit(0) => Ret::Value(zero.clone()), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) + .app(NaturalLit(n - 1).into_value()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); @@ -517,7 +496,7 @@ fn apply_builtin( }; match ret { Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), + Ret::Value(v) => v.kind().clone(), Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, -- cgit v1.2.3 From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- dhall/src/semantics/builtins.rs | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index a513967..423364d 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv, + typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -48,17 +48,13 @@ impl BuiltinClosure { x.normalize(); } } - pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind { - TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold( + pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { + HirKind::Expr(self.args.iter().zip(self.types.iter()).fold( ExprKind::Builtin(self.b), |acc, (v, ty)| { ExprKind::App( - TyExpr::new( - TyExprKind::Expr(acc), - Some(ty.clone()), - Span::Artificial, - ), - v.to_tyexpr(venv), + Hir::new(HirKind::Expr(acc), Span::Artificial), + v.to_hir(venv), ) }, )) -- cgit v1.2.3 From 5688ed654eee258bf8ffc8761ce693c73a0242d5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:58:11 +0000 Subject: Remove extra types stored in Value --- dhall/src/semantics/builtins.rs | 28 ++++++---------------------- 1 file changed, 6 insertions(+), 22 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 423364d..715e045 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -19,10 +19,6 @@ pub(crate) struct BuiltinClosure { pub b: Builtin, /// Arguments applied to the closure so far. pub args: Vec, - /// Keeps the types of the partial applications around to be able to convert back to TyExpr. - /// If the args so far are `x_1`, ..., `x_n`, this contains the types of `b`, `b x1`, ..., - /// `b x_1 x_2 ... x_(n-1)`. - pub types: Vec, } impl BuiltinClosure { @@ -31,15 +27,13 @@ impl BuiltinClosure { env, b, args: Vec::new(), - types: Vec::new(), } } - pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind { + pub fn apply(&self, a: Value) -> ValueKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); - let types = self.types.iter().cloned().chain(once(f_ty)).collect(); - apply_builtin(self.b, args, types, self.env.clone()) + apply_builtin(self.b, args, self.env.clone()) } /// This doesn't break the invariant because we already checked that the appropriate arguments /// did not normalize to something that allows evaluation to proceed. @@ -49,9 +43,9 @@ impl BuiltinClosure { } } pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { - HirKind::Expr(self.args.iter().zip(self.types.iter()).fold( + HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), - |acc, (v, ty)| { + |acc, v| { ExprKind::App( Hir::new(HirKind::Expr(acc), Span::Artificial), v.to_hir(venv), @@ -260,12 +254,7 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -fn apply_builtin( - b: Builtin, - args: Vec, - types: Vec, - env: NzEnv, -) -> ValueKind { +fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { use Builtin::*; use ValueKind::*; @@ -493,12 +482,7 @@ fn apply_builtin( match ret { Ret::ValueKind(v) => v, Ret::Value(v) => v.kind().clone(), - Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { - b, - args, - types, - env, - }), + Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }), } } -- cgit v1.2.3 From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:58:28 +0000 Subject: Take Hir for typecheck --- dhall/src/semantics/builtins.rs | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 715e045..b1d12aa 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, + skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -115,9 +115,9 @@ macro_rules! make_type { }; } -pub(crate) fn type_of_builtin(b: Builtin) -> Expr { +pub(crate) fn type_of_builtin(b: Builtin) -> Hir { use Builtin::*; - match b { + let expr = match b { Bool | Natural | Integer | Double | Text => make_type!(Type), List | Optional => make_type!( Type -> Type @@ -200,7 +200,8 @@ pub(crate) fn type_of_builtin(b: Builtin) -> Expr { OptionalNone => make_type!( forall (A: Type) -> Optional A ), - } + }; + skip_resolve(&expr).unwrap() } // Ad-hoc macro to help construct closures @@ -264,7 +265,8 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { Value(Value), DoneAsIs, } - let make_closure = |e| typecheck(&e).unwrap().eval(&env); + let make_closure = + |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env); let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), -- cgit v1.2.3 From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:07:03 +0000 Subject: Remove all types from Value --- dhall/src/semantics/builtins.rs | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index b1d12aa..9d4f8a2 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -370,17 +370,9 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } _ => Ret::DoneAsIs, }, - (ListIndexed, [_, l]) => { - let l_whnf = l.kind(); - match &*l_whnf { + (ListIndexed, [t, l]) => { + match l.kind() { 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)); @@ -388,7 +380,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let t = Value::from_kind(RecordType(kts)); // Construct the new list, with added indices - let list = match &*l_whnf { + let list = match l.kind() { EmptyListLit(_) => EmptyListLit(t), NEListLit(xs) => NEListLit( xs.iter() -- cgit v1.2.3 From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/builtins.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 9d4f8a2..d9a3599 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -265,8 +265,11 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { Value(Value), DoneAsIs, } - let make_closure = - |e| typecheck(&skip_resolve(&e).unwrap()).unwrap().eval(&env); + let make_closure = |e| { + typecheck(&skip_resolve(&e).unwrap()) + .unwrap() + .eval(env.clone()) + }; let ret = match (b, args.as_slice()) { (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/builtins.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index d9a3599..cbb5a6e 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -55,7 +55,7 @@ impl BuiltinClosure { } } -pub(crate) fn rc(x: UnspannedExpr) -> Expr { +pub(crate) fn rc(x: UnspannedExpr) -> Expr { Expr::new(x, Span::Artificial) } -- cgit v1.2.3 From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 19:04:44 +0000 Subject: Introduce LitKind to factor out common enum nodes --- dhall/src/semantics/builtins.rs | 119 +++++++++++++++++++++------------------- 1 file changed, 63 insertions(+), 56 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index cbb5a6e..752b25c 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -5,7 +5,8 @@ use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V, + InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr, + V, }; use crate::Normalized; use std::collections::HashMap; @@ -240,7 +241,7 @@ macro_rules! make_closure { rc(ExprKind::BinOp( BinOp::NaturalPlus, make_closure!($($v)*), - rc(ExprKind::NaturalLit(1)) + rc(ExprKind::Lit(LitKind::Natural(1))) )) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ @@ -256,7 +257,7 @@ macro_rules! make_closure { #[allow(clippy::cognitive_complexity)] fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { - use Builtin::*; + use LitKind::{Bool, Double, Integer, Natural}; use ValueKind::*; // Small helper enum @@ -272,38 +273,40 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { }; let ret = match (b, args.as_slice()) { - (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())), - (NaturalIsZero, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)), + (Builtin::OptionalNone, [t]) => { + Ret::ValueKind(EmptyOptionalLit(t.clone())) + } + (Builtin::NaturalIsZero, [n]) => match &*n.kind() { + Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))), _ => Ret::DoneAsIs, }, - (NaturalEven, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)), + (Builtin::NaturalEven, [n]) => match &*n.kind() { + Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))), _ => Ret::DoneAsIs, }, - (NaturalOdd, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)), + (Builtin::NaturalOdd, [n]) => match &*n.kind() { + Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))), _ => Ret::DoneAsIs, }, - (NaturalToInteger, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)), + (Builtin::NaturalToInteger, [n]) => match &*n.kind() { + Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))), _ => Ret::DoneAsIs, }, - (NaturalShow, [n]) => match &*n.kind() { - NaturalLit(n) => Ret::Value(Value::from_text(n)), + (Builtin::NaturalShow, [n]) => match &*n.kind() { + Lit(Natural(n)) => Ret::Value(Value::from_text(n)), _ => Ret::DoneAsIs, }, - (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { - (NaturalLit(a), NaturalLit(b)) => { - Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 })) + (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { + (Lit(Natural(a)), Lit(Natural(b))) => { + Ret::ValueKind(Lit(Natural(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)), + (Lit(Natural(0)), _) => Ret::Value(b.clone()), + (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))), + _ if a == b => Ret::ValueKind(Lit(Natural(0))), _ => Ret::DoneAsIs, }, - (IntegerShow, [n]) => match &*n.kind() { - IntegerLit(n) => { + (Builtin::IntegerShow, [n]) => match &*n.kind() { + Lit(Integer(n)) => { let s = if *n < 0 { n.to_string() } else { @@ -313,27 +316,27 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } _ => Ret::DoneAsIs, }, - (IntegerToDouble, [n]) => match &*n.kind() { - IntegerLit(n) => { - Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64))) + (Builtin::IntegerToDouble, [n]) => match &*n.kind() { + Lit(Integer(n)) => { + Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64)))) } _ => Ret::DoneAsIs, }, - (IntegerNegate, [n]) => match &*n.kind() { - IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)), + (Builtin::IntegerNegate, [n]) => match &*n.kind() { + Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))), _ => Ret::DoneAsIs, }, - (IntegerClamp, [n]) => match &*n.kind() { - IntegerLit(n) => { - Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0))) + (Builtin::IntegerClamp, [n]) => match &*n.kind() { + Lit(Integer(n)) => { + Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0)))) } _ => Ret::DoneAsIs, }, - (DoubleShow, [n]) => match &*n.kind() { - DoubleLit(n) => Ret::Value(Value::from_text(n)), + (Builtin::DoubleShow, [n]) => match &*n.kind() { + Lit(Double(n)) => Ret::Value(Value::from_text(n)), _ => Ret::DoneAsIs, }, - (TextShow, [v]) => match &*v.kind() { + (Builtin::TextShow, [v]) => match &*v.kind() { TextLit(tlit) => { if let Some(s) = tlit.as_text() { // Printing InterpolatedText takes care of all the escaping @@ -347,38 +350,41 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } _ => Ret::DoneAsIs, }, - (ListLength, [_, l]) => match &*l.kind() { - EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)), - NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())), + (Builtin::ListLength, [_, l]) => match &*l.kind() { + EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))), + NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))), _ => Ret::DoneAsIs, }, - (ListHead, [_, l]) => match &*l.kind() { + (Builtin::ListHead, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) } _ => Ret::DoneAsIs, }, - (ListLast, [_, l]) => match &*l.kind() { + (Builtin::ListLast, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => Ret::ValueKind(NEOptionalLit( xs.iter().rev().next().unwrap().clone(), )), _ => Ret::DoneAsIs, }, - (ListReverse, [_, l]) => match &*l.kind() { + (Builtin::ListReverse, [_, l]) => match &*l.kind() { EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), NEListLit(xs) => { Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) } _ => Ret::DoneAsIs, }, - (ListIndexed, [t, l]) => { + (Builtin::ListIndexed, [t, l]) => { match l.kind() { EmptyListLit(_) | NEListLit(_) => { // Construct the returned record type: { index: Natural, value: t } let mut kts = HashMap::new(); - kts.insert("index".into(), Value::from_builtin(Natural)); + kts.insert( + "index".into(), + Value::from_builtin(Builtin::Natural), + ); kts.insert("value".into(), t.clone()); let t = Value::from_kind(RecordType(kts)); @@ -392,7 +398,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_kind(NaturalLit(i)), + Value::from_kind(Lit(Natural(i))), ); kvs.insert("value".into(), e.clone()); Value::from_kind(RecordLit(kvs)) @@ -406,8 +412,8 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { _ => Ret::DoneAsIs, } } - (ListBuild, [t, f]) => { - let list_t = Value::from_builtin(List).app(t.clone()); + (Builtin::ListBuild, [t, f]) => { + let list_t = Value::from_builtin(Builtin::List).app(t.clone()); Ret::Value( f.app(list_t.clone()) .app( @@ -422,7 +428,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { .app(EmptyListLit(t.clone()).into_value()), ) } - (ListFold, [_, l, _, cons, nil]) => match &*l.kind() { + (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() { EmptyListLit(_) => Ret::Value(nil.clone()), NEListLit(xs) => { let mut v = nil.clone(); @@ -433,8 +439,9 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } _ => Ret::DoneAsIs, }, - (OptionalBuild, [t, f]) => { - let optional_t = Value::from_builtin(Optional).app(t.clone()); + (Builtin::OptionalBuild, [t, f]) => { + let optional_t = + Value::from_builtin(Builtin::Optional).app(t.clone()); Ret::Value( f.app(optional_t.clone()) .app( @@ -448,25 +455,25 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { .app(EmptyOptionalLit(t.clone()).into_value()), ) } - (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { + (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { EmptyOptionalLit(_) => Ret::Value(nothing.clone()), NEOptionalLit(x) => Ret::Value(just.app(x.clone())), _ => Ret::DoneAsIs, }, - (NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Natural)) + (Builtin::NaturalBuild, [f]) => Ret::Value( + f.app(Value::from_builtin(Builtin::Natural)) .app(make_closure(make_closure!( λ(x : Natural) -> 1 + var(x) ))) - .app(NaturalLit(0).into_value()), + .app(Lit(Natural(0)).into_value()), ), - (NaturalFold, [n, t, succ, zero]) => match &*n.kind() { - NaturalLit(0) => Ret::Value(zero.clone()), - NaturalLit(n) => { - let fold = Value::from_builtin(NaturalFold) - .app(NaturalLit(n - 1).into_value()) + (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() { + Lit(Natural(0)) => Ret::Value(zero.clone()), + Lit(Natural(n)) => { + let fold = Value::from_builtin(Builtin::NaturalFold) + .app(Lit(Natural(n - 1)).into_value()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/builtins.rs | 118 ++++++++++++++++++++-------------------- 1 file changed, 59 insertions(+), 59 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 752b25c..61de0c7 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, + skip_resolve, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -15,14 +15,14 @@ use std::convert::TryInto; /// A partially applied builtin. /// Invariant: the evaluation of the given args must not be able to progress further #[derive(Debug, Clone)] -pub(crate) struct BuiltinClosure { +pub(crate) struct BuiltinClosure { pub env: NzEnv, pub b: Builtin, /// Arguments applied to the closure so far. - pub args: Vec, + pub args: Vec, } -impl BuiltinClosure { +impl BuiltinClosure { pub fn new(b: Builtin, env: NzEnv) -> Self { BuiltinClosure { env, @@ -31,7 +31,7 @@ impl BuiltinClosure { } } - pub fn apply(&self, a: Value) -> ValueKind { + pub fn apply(&self, a: Nir) -> NirKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(self.b, args, self.env.clone()) @@ -256,14 +256,14 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { +fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { use LitKind::{Bool, Double, Integer, Natural}; - use ValueKind::*; + use NirKind::*; // Small helper enum enum Ret { - ValueKind(ValueKind), - Value(Value), + NirKind(NirKind), + Nir(Nir), DoneAsIs, } let make_closure = |e| { @@ -274,35 +274,35 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let ret = match (b, args.as_slice()) { (Builtin::OptionalNone, [t]) => { - Ret::ValueKind(EmptyOptionalLit(t.clone())) + Ret::NirKind(EmptyOptionalLit(t.clone())) } (Builtin::NaturalIsZero, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalEven, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalOdd, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalToInteger, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))), + Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))), _ => Ret::DoneAsIs, }, (Builtin::NaturalShow, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::Value(Value::from_text(n)), + Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)), _ => Ret::DoneAsIs, }, (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { (Lit(Natural(a)), Lit(Natural(b))) => { - Ret::ValueKind(Lit(Natural(if b > a { b - a } else { 0 }))) + Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 }))) } - (Lit(Natural(0)), _) => Ret::Value(b.clone()), - (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))), - _ if a == b => Ret::ValueKind(Lit(Natural(0))), + (Lit(Natural(0)), _) => Ret::Nir(b.clone()), + (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))), + _ if a == b => Ret::NirKind(Lit(Natural(0))), _ => Ret::DoneAsIs, }, (Builtin::IntegerShow, [n]) => match &*n.kind() { @@ -312,28 +312,28 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } else { format!("+{}", n) }; - Ret::Value(Value::from_text(s)) + Ret::Nir(Nir::from_text(s)) } _ => Ret::DoneAsIs, }, (Builtin::IntegerToDouble, [n]) => match &*n.kind() { Lit(Integer(n)) => { - Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64)))) + Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64)))) } _ => Ret::DoneAsIs, }, (Builtin::IntegerNegate, [n]) => match &*n.kind() { - Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))), + Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))), _ => Ret::DoneAsIs, }, (Builtin::IntegerClamp, [n]) => match &*n.kind() { Lit(Integer(n)) => { - Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0)))) + Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0)))) } _ => Ret::DoneAsIs, }, (Builtin::DoubleShow, [n]) => match &*n.kind() { - Lit(Double(n)) => Ret::Value(Value::from_text(n)), + Lit(Double(n)) => Ret::Nir(Nir::from_text(n)), _ => Ret::DoneAsIs, }, (Builtin::TextShow, [v]) => match &*v.kind() { @@ -343,7 +343,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let txt: InterpolatedText = std::iter::once(InterpolatedTextContents::Text(s)) .collect(); - Ret::Value(Value::from_text(txt)) + Ret::Nir(Nir::from_text(txt)) } else { Ret::DoneAsIs } @@ -351,28 +351,28 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { _ => Ret::DoneAsIs, }, (Builtin::ListLength, [_, l]) => match &*l.kind() { - EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))), - NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))), + EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))), + NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))), _ => Ret::DoneAsIs, }, (Builtin::ListHead, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), + EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) + Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone())) } _ => Ret::DoneAsIs, }, (Builtin::ListLast, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( + EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), + NEListLit(xs) => Ret::NirKind(NEOptionalLit( xs.iter().rev().next().unwrap().clone(), )), _ => Ret::DoneAsIs, }, (Builtin::ListReverse, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), + EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())), NEListLit(xs) => { - Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) + Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect())) } _ => Ret::DoneAsIs, }, @@ -383,10 +383,10 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let mut kts = HashMap::new(); kts.insert( "index".into(), - Value::from_builtin(Builtin::Natural), + Nir::from_builtin(Builtin::Natural), ); kts.insert("value".into(), t.clone()); - let t = Value::from_kind(RecordType(kts)); + let t = Nir::from_kind(RecordType(kts)); // Construct the new list, with added indices let list = match l.kind() { @@ -398,23 +398,23 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_kind(Lit(Natural(i))), + Nir::from_kind(Lit(Natural(i))), ); kvs.insert("value".into(), e.clone()); - Value::from_kind(RecordLit(kvs)) + Nir::from_kind(RecordLit(kvs)) }) .collect(), ), _ => unreachable!(), }; - Ret::ValueKind(list) + Ret::NirKind(list) } _ => Ret::DoneAsIs, } } (Builtin::ListBuild, [t, f]) => { - let list_t = Value::from_builtin(Builtin::List).app(t.clone()); - Ret::Value( + let list_t = Nir::from_builtin(Builtin::List).app(t.clone()); + Ret::Nir( f.app(list_t.clone()) .app( make_closure(make_closure!( @@ -425,24 +425,24 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { )) .app(t.clone()), ) - .app(EmptyListLit(t.clone()).into_value()), + .app(EmptyListLit(t.clone()).into_nir()), ) } (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() { - EmptyListLit(_) => Ret::Value(nil.clone()), + EmptyListLit(_) => Ret::Nir(nil.clone()), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().cloned().rev() { v = cons.app(x).app(v); } - Ret::Value(v) + Ret::Nir(v) } _ => Ret::DoneAsIs, }, (Builtin::OptionalBuild, [t, f]) => { let optional_t = - Value::from_builtin(Builtin::Optional).app(t.clone()); - Ret::Value( + Nir::from_builtin(Builtin::Optional).app(t.clone()); + Ret::Nir( f.app(optional_t.clone()) .app( make_closure(make_closure!( @@ -452,47 +452,47 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { )) .app(t.clone()), ) - .app(EmptyOptionalLit(t.clone()).into_value()), + .app(EmptyOptionalLit(t.clone()).into_nir()), ) } (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { - EmptyOptionalLit(_) => Ret::Value(nothing.clone()), - NEOptionalLit(x) => Ret::Value(just.app(x.clone())), + EmptyOptionalLit(_) => Ret::Nir(nothing.clone()), + NEOptionalLit(x) => Ret::Nir(just.app(x.clone())), _ => Ret::DoneAsIs, }, - (Builtin::NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Builtin::Natural)) + (Builtin::NaturalBuild, [f]) => Ret::Nir( + f.app(Nir::from_builtin(Builtin::Natural)) .app(make_closure(make_closure!( λ(x : Natural) -> 1 + var(x) ))) - .app(Lit(Natural(0)).into_value()), + .app(Lit(Natural(0)).into_nir()), ), (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() { - Lit(Natural(0)) => Ret::Value(zero.clone()), + Lit(Natural(0)) => Ret::Nir(zero.clone()), Lit(Natural(n)) => { - let fold = Value::from_builtin(Builtin::NaturalFold) - .app(Lit(Natural(n - 1)).into_value()) + let fold = Nir::from_builtin(Builtin::NaturalFold) + .app(Lit(Natural(n - 1)).into_nir()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); - Ret::Value(succ.app(fold)) + Ret::Nir(succ.app(fold)) } _ => Ret::DoneAsIs, }, _ => Ret::DoneAsIs, }; match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.kind().clone(), + Ret::NirKind(v) => v, + Ret::Nir(v) => v.kind().clone(), Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }), } } -impl std::cmp::PartialEq for BuiltinClosure { +impl std::cmp::PartialEq for BuiltinClosure { fn eq(&self, other: &Self) -> bool { self.b == other.b && self.args == other.args } } -impl std::cmp::Eq for BuiltinClosure {} +impl std::cmp::Eq for BuiltinClosure {} -- cgit v1.2.3