From 2f5c45fd2f712f7befe6f7c92b62dc76d5f77538 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 16:50:49 +0000 Subject: Rename LitKind to NumKind --- dhall/src/semantics/builtins.rs | 54 ++++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 27 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 803630b..8d17aed 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -5,7 +5,7 @@ use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; use crate::syntax::{ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText, - InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr, + InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, V, }; use crate::Normalized; @@ -241,7 +241,7 @@ macro_rules! make_closure { rc(ExprKind::BinOp( BinOp::NaturalPlus, make_closure!($($v)*), - rc(ExprKind::Lit(LitKind::Natural(1))) + rc(ExprKind::Num(NumKind::Natural(1))) )) }; ([ $($head:tt)* ] # $($tail:tt)*) => {{ @@ -257,8 +257,8 @@ macro_rules! make_closure { #[allow(clippy::cognitive_complexity)] fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { - use LitKind::{Bool, Double, Integer, Natural}; use NirKind::*; + use NumKind::{Bool, Double, Integer, Natural}; // Small helper enum enum Ret { @@ -277,36 +277,36 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { Ret::NirKind(EmptyOptionalLit(t.clone())) } (Builtin::NaturalIsZero, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))), + Num(Natural(n)) => Ret::NirKind(Num(Bool(*n == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalEven, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))), + Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalOdd, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))), + Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 != 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalToInteger, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))), + Num(Natural(n)) => Ret::NirKind(Num(Integer(*n as isize))), _ => Ret::DoneAsIs, }, (Builtin::NaturalShow, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)), + Num(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::NirKind(Lit(Natural(if b > a { b - a } else { 0 }))) + (Num(Natural(a)), Num(Natural(b))) => { + Ret::NirKind(Num(Natural(if b > a { b - a } else { 0 }))) } - (Lit(Natural(0)), _) => Ret::Nir(b.clone()), - (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))), - _ if a == b => Ret::NirKind(Lit(Natural(0))), + (Num(Natural(0)), _) => Ret::Nir(b.clone()), + (_, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))), + _ if a == b => Ret::NirKind(Num(Natural(0))), _ => Ret::DoneAsIs, }, (Builtin::IntegerShow, [n]) => match &*n.kind() { - Lit(Integer(n)) => { + Num(Integer(n)) => { let s = if *n < 0 { n.to_string() } else { @@ -317,23 +317,23 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { _ => Ret::DoneAsIs, }, (Builtin::IntegerToDouble, [n]) => match &*n.kind() { - Lit(Integer(n)) => { - Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64)))) + Num(Integer(n)) => { + Ret::NirKind(Num(Double(NaiveDouble::from(*n as f64)))) } _ => Ret::DoneAsIs, }, (Builtin::IntegerNegate, [n]) => match &*n.kind() { - Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))), + Num(Integer(n)) => Ret::NirKind(Num(Integer(-n))), _ => Ret::DoneAsIs, }, (Builtin::IntegerClamp, [n]) => match &*n.kind() { - Lit(Integer(n)) => { - Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0)))) + Num(Integer(n)) => { + Ret::NirKind(Num(Natural((*n).try_into().unwrap_or(0)))) } _ => Ret::DoneAsIs, }, (Builtin::DoubleShow, [n]) => match &*n.kind() { - Lit(Double(n)) => Ret::Nir(Nir::from_text(n)), + Num(Double(n)) => Ret::Nir(Nir::from_text(n)), _ => Ret::DoneAsIs, }, (Builtin::TextShow, [v]) => match &*v.kind() { @@ -351,8 +351,8 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { _ => Ret::DoneAsIs, }, (Builtin::ListLength, [_, l]) => match &*l.kind() { - EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))), - NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))), + EmptyListLit(_) => Ret::NirKind(Num(Natural(0))), + NEListLit(xs) => Ret::NirKind(Num(Natural(xs.len()))), _ => Ret::DoneAsIs, }, (Builtin::ListHead, [_, l]) => match &*l.kind() { @@ -398,7 +398,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Nir::from_kind(Lit(Natural(i))), + Nir::from_kind(Num(Natural(i))), ); kvs.insert("value".into(), e.clone()); Nir::from_kind(RecordLit(kvs)) @@ -466,14 +466,14 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { λ(x : Natural) -> 1 + var(x) ))) - .app(Lit(Natural(0)).into_nir()), + .app(Num(Natural(0)).into_nir()), ), (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() { - Lit(Natural(0)) => Ret::Nir(zero.clone()), - Lit(Natural(n)) => { + Num(Natural(0)) => Ret::Nir(zero.clone()), + Num(Natural(n)) => { let fold = Nir::from_builtin(Builtin::NaturalFold) - .app(Lit(Natural(n - 1)).into_nir()) + .app(Num(Natural(n - 1)).into_nir()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); -- cgit v1.2.3 From 35db1b4b54dba8b0cafe661329e0099dfabd8073 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 17:04:47 +0000 Subject: Remove top-level Expr aliases --- dhall/src/semantics/builtins.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 8d17aed..eb50612 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -8,7 +8,6 @@ use crate::syntax::{ InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr, V, }; -use crate::Normalized; use std::collections::HashMap; use std::convert::TryInto; @@ -340,7 +339,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { TextLit(tlit) => { if let Some(s) = tlit.as_text() { // Printing InterpolatedText takes care of all the escaping - let txt: InterpolatedText = + let txt: InterpolatedText = std::iter::once(InterpolatedTextContents::Text(s)) .collect(); Ret::Nir(Nir::from_text(txt)) -- cgit v1.2.3 From ef3734a3e9381b2e91552089774126f58f560bc3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 21:21:32 +0000 Subject: Improve handling of builtin types in Nir --- dhall/src/semantics/builtins.rs | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index eb50612..7fbb933 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -14,22 +14,17 @@ 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 env: NzEnv, - pub b: Builtin, +pub(crate) struct BuiltinClosure { + env: NzEnv, + b: Builtin, /// Arguments applied to the closure so far. - pub args: Vec, + args: Vec, } -impl BuiltinClosure { - pub fn new(b: Builtin, env: NzEnv) -> Self { - BuiltinClosure { - env, - b, - args: Vec::new(), - } +impl BuiltinClosure { + pub fn new(b: Builtin, env: NzEnv) -> NirKind { + apply_builtin(b, Vec::new(), env) } - pub fn apply(&self, a: Nir) -> NirKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a)).collect(); @@ -272,6 +267,14 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { }; let ret = match (b, args.as_slice()) { + (Builtin::Bool, []) + | (Builtin::Natural, []) + | (Builtin::Integer, []) + | (Builtin::Double, []) + | (Builtin::Text, []) => Ret::NirKind(BuiltinType(b)), + (Builtin::Optional, [t]) => Ret::NirKind(OptionalType(t.clone())), + (Builtin::List, [t]) => Ret::NirKind(ListType(t.clone())), + (Builtin::OptionalNone, [t]) => { Ret::NirKind(EmptyOptionalLit(t.clone())) } @@ -489,9 +492,9 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { } } -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 From f4a1a6b8d4de5f83649b2ddd90d65f6e6d76e5e1 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 13 Mar 2020 21:29:08 +0000 Subject: Nir::normalize isn't useful It pretends to normalize but actually can't normalize under lambdas. The correct way to normalize a Nir is to convert it to Hir. --- dhall/src/semantics/builtins.rs | 7 ------- 1 file changed, 7 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 7fbb933..ef375b8 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -30,13 +30,6 @@ impl BuiltinClosure { let args = self.args.iter().cloned().chain(once(a)).collect(); 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. - pub fn normalize(&self) { - for x in self.args.iter() { - x.normalize(); - } - } pub fn to_hirkind(&self, venv: VarEnv) -> HirKind { HirKind::Expr(self.args.iter().fold( ExprKind::Builtin(self.b), -- cgit v1.2.3 From 7848c8e8d3147ebe428290558aa6c0efcbf59ee5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 18 Mar 2020 18:58:51 +0000 Subject: Brutally make all of dhall pub --- dhall/src/semantics/builtins.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index ef375b8..fa22bd0 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -14,7 +14,7 @@ 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 struct BuiltinClosure { env: NzEnv, b: Builtin, /// Arguments applied to the closure so far. @@ -43,7 +43,7 @@ impl BuiltinClosure { } } -pub(crate) fn rc(x: UnspannedExpr) -> Expr { +pub fn rc(x: UnspannedExpr) -> Expr { Expr::new(x, Span::Artificial) } @@ -103,7 +103,7 @@ macro_rules! make_type { }; } -pub(crate) fn type_of_builtin(b: Builtin) -> Hir { +pub fn type_of_builtin(b: Builtin) -> Hir { use Builtin::*; let expr = match b { Bool | Natural | Integer | Double | Text => make_type!(Type), -- cgit v1.2.3 From 85e2e8ee5e83dadd05b6974ba6c951350cb97a61 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 21 Mar 2020 21:30:30 +0000 Subject: Introduce option builder --- dhall/src/semantics/builtins.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/builtins.rs') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index fa22bd0..6007a92 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, Nir, NirKind, NzEnv, VarEnv, + skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -189,7 +189,7 @@ pub fn type_of_builtin(b: Builtin) -> Hir { forall (A: Type) -> Optional A ), }; - skip_resolve(&expr).unwrap() + skip_resolve_expr(&expr).unwrap() } // Ad-hoc macro to help construct closures @@ -254,7 +254,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { DoneAsIs, } let make_closure = |e| { - typecheck(&skip_resolve(&e).unwrap()) + typecheck(&skip_resolve_expr(&e).unwrap()) .unwrap() .eval(env.clone()) }; -- cgit v1.2.3