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/builtins.rs | 511 +++++++++++++++++++++++++++++++++ dhall/src/semantics/core/value.rs | 31 +- dhall/src/semantics/mod.rs | 2 + dhall/src/semantics/phase/normalize.rs | 373 +----------------------- dhall/src/semantics/phase/typecheck.rs | 177 ------------ dhall/src/semantics/tck/mod.rs | 2 +- dhall/src/semantics/tck/tyexpr.rs | 3 +- dhall/src/semantics/tck/typecheck.rs | 22 +- 8 files changed, 553 insertions(+), 568 deletions(-) create mode 100644 dhall/src/semantics/builtins.rs diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs new file mode 100644 index 0000000..58cf0d6 --- /dev/null +++ b/dhall/src/semantics/builtins.rs @@ -0,0 +1,511 @@ +use crate::semantics::phase::Normalized; +use crate::semantics::{type_with, NzEnv, Value, ValueKind}; +use crate::syntax::Const::Type; +use crate::syntax::{ + self, Builtin, Const, Expr, ExprKind, InterpolatedText, + InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V, +}; +use std::collections::HashMap; +use std::convert::TryInto; + +pub(crate) fn rc(x: UnspannedExpr) -> Expr { + Expr::new(x, Span::Artificial) +} + +// Ad-hoc macro to help construct the types of builtins +macro_rules! make_type { + (Type) => { rc(ExprKind::Const(Const::Type)) }; + (Bool) => { rc(ExprKind::Builtin(Builtin::Bool)) }; + (Natural) => { rc(ExprKind::Builtin(Builtin::Natural)) }; + (Integer) => { rc(ExprKind::Builtin(Builtin::Integer)) }; + (Double) => { rc(ExprKind::Builtin(Builtin::Double)) }; + (Text) => { rc(ExprKind::Builtin(Builtin::Text)) }; + ($var:ident) => { + rc(ExprKind::Var(V(stringify!($var).into(), 0))) + }; + (Optional $ty:ident) => { + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::Optional)), + make_type!($ty) + )) + }; + (List $($rest:tt)*) => { + rc(ExprKind::App( + rc(ExprKind::Builtin(Builtin::List)), + make_type!($($rest)*) + )) + }; + ({ $($label:ident : $ty:ident),* }) => {{ + let mut kts = syntax::map::DupTreeMap::new(); + $( + kts.insert( + Label::from(stringify!($label)), + make_type!($ty), + ); + )* + rc(ExprKind::RecordType(kts)) + }}; + ($ty:ident -> $($rest:tt)*) => { + rc(ExprKind::Pi( + "_".into(), + make_type!($ty), + make_type!($($rest)*) + )) + }; + (($($arg:tt)*) -> $($rest:tt)*) => { + rc(ExprKind::Pi( + "_".into(), + make_type!($($arg)*), + make_type!($($rest)*) + )) + }; + (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { + rc(ExprKind::Pi( + stringify!($var).into(), + make_type!($($ty)*), + make_type!($($rest)*) + )) + }; +} + +pub(crate) fn type_of_builtin(b: Builtin) -> Expr { + use Builtin::*; + match b { + Bool | Natural | Integer | Double | Text => make_type!(Type), + List | Optional => make_type!( + Type -> Type + ), + + NaturalFold => make_type!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural + ), + NaturalBuild => make_type!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural + ), + NaturalIsZero | NaturalEven | NaturalOdd => make_type!( + Natural -> Bool + ), + NaturalToInteger => make_type!(Natural -> Integer), + NaturalShow => make_type!(Natural -> Text), + NaturalSubtract => make_type!(Natural -> Natural -> Natural), + + IntegerToDouble => make_type!(Integer -> Double), + IntegerShow => make_type!(Integer -> Text), + IntegerNegate => make_type!(Integer -> Integer), + IntegerClamp => make_type!(Integer -> Natural), + + DoubleShow => make_type!(Double -> Text), + TextShow => make_type!(Text -> Text), + + ListBuild => make_type!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a + ), + ListFold => make_type!( + forall (a: Type) -> + (List a) -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list + ), + ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), + ListHead | ListLast => { + make_type!(forall (a: Type) -> (List a) -> Optional a) + } + ListIndexed => make_type!( + forall (a: Type) -> + (List a) -> + List { index: Natural, value: a } + ), + ListReverse => make_type!( + forall (a: Type) -> (List a) -> List a + ), + + OptionalBuild => make_type!( + forall (a: Type) -> + (forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional) -> + Optional a + ), + OptionalFold => make_type!( + forall (a: Type) -> + (Optional a) -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + ), + OptionalNone => make_type!( + forall (A: Type) -> Optional A + ), + } +} + +// 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), + } +} diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 918826b..7ecb2bf 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -5,12 +5,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::Binder; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; -use crate::semantics::phase::typecheck::{ - builtin_to_value, builtin_to_value_env, const_to_value, -}; use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::semantics::{type_of_builtin, TyExpr, TyExprKind}; use crate::semantics::{NzEnv, NzVar, VarEnv}; -use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, @@ -138,13 +135,27 @@ impl Value { Value::new(v, WHNF, t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { - const_to_value(c) + let v = ValueKind::Const(c); + match c { + Const::Type => { + Value::from_kind_and_type(v, Value::from_const(Const::Kind)) + } + Const::Kind => { + Value::from_kind_and_type(v, Value::from_const(Const::Sort)) + } + Const::Sort => Value::const_sort(), + } } pub(crate) fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) } pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { - builtin_to_value_env(b, env) + Value::from_kind_and_type( + ValueKind::from_builtin_env(b, env.clone()), + crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) + .unwrap() + .normalize_whnf_noenv(), + ) } pub(crate) fn as_const(&self) -> Option { @@ -361,17 +372,19 @@ impl Value { ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), ValueKind::EmptyOptionalLit(n) => ExprKind::App( - builtin_to_value(Builtin::OptionalNone).to_tyexpr(venv), + Value::from_builtin(Builtin::OptionalNone) + .to_tyexpr(venv), n, ), ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), ValueKind::EmptyListLit(n) => { ExprKind::EmptyListLit(TyExpr::new( TyExprKind::Expr(ExprKind::App( - builtin_to_value(Builtin::List).to_tyexpr(venv), + Value::from_builtin(Builtin::List) + .to_tyexpr(venv), n, )), - Some(const_to_value(Const::Type)), + Some(Value::from_const(Const::Type)), Span::Artificial, )) } diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index ce08334..01bbd39 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,7 +1,9 @@ +pub mod builtins; pub mod core; pub mod nze; pub mod phase; pub mod tck; +pub(crate) use self::builtins::*; pub(crate) use self::core::*; pub(crate) use self::nze::*; pub(crate) use self::tck::*; 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)), diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 2e22ad2..8b13789 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -1,178 +1 @@ -use crate::semantics::{NzEnv, Value, ValueKind}; -use crate::syntax; -use crate::syntax::{ - Builtin, Const, Expr, ExprKind, Label, Span, UnspannedExpr, -}; -pub(crate) fn const_to_value(c: Const) -> Value { - let v = ValueKind::Const(c); - match c { - Const::Type => { - Value::from_kind_and_type(v, const_to_value(Const::Kind)) - } - Const::Kind => { - Value::from_kind_and_type(v, const_to_value(Const::Sort)) - } - Const::Sort => Value::const_sort(), - } -} - -pub fn rc(x: UnspannedExpr) -> Expr { - Expr::new(x, Span::Artificial) -} - -// Ad-hoc macro to help construct the types of builtins -macro_rules! make_type { - (Type) => { ExprKind::Const(Const::Type) }; - (Bool) => { ExprKind::Builtin(Builtin::Bool) }; - (Natural) => { ExprKind::Builtin(Builtin::Natural) }; - (Integer) => { ExprKind::Builtin(Builtin::Integer) }; - (Double) => { ExprKind::Builtin(Builtin::Double) }; - (Text) => { ExprKind::Builtin(Builtin::Text) }; - ($var:ident) => { - ExprKind::Var(syntax::V(stringify!($var).into(), 0)) - }; - (Optional $ty:ident) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::Optional)), - rc(make_type!($ty)) - ) - }; - (List $($rest:tt)*) => { - ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - rc(make_type!($($rest)*)) - ) - }; - ({ $($label:ident : $ty:ident),* }) => {{ - let mut kts = syntax::map::DupTreeMap::new(); - $( - kts.insert( - Label::from(stringify!($label)), - rc(make_type!($ty)), - ); - )* - ExprKind::RecordType(kts) - }}; - ($ty:ident -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($ty)), - rc(make_type!($($rest)*)) - ) - }; - (($($arg:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - "_".into(), - rc(make_type!($($arg)*)), - rc(make_type!($($rest)*)) - ) - }; - (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - ExprKind::Pi( - stringify!($var).into(), - rc(make_type!($($ty)*)), - rc(make_type!($($rest)*)) - ) - }; -} - -pub(crate) fn type_of_builtin(b: Builtin) -> Expr { - use syntax::Builtin::*; - rc(match b { - Bool | Natural | Integer | Double | Text => make_type!(Type), - List | Optional => make_type!( - Type -> Type - ), - - NaturalFold => make_type!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => make_type!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => make_type!( - Natural -> Bool - ), - NaturalToInteger => make_type!(Natural -> Integer), - NaturalShow => make_type!(Natural -> Text), - NaturalSubtract => make_type!(Natural -> Natural -> Natural), - - IntegerToDouble => make_type!(Integer -> Double), - IntegerShow => make_type!(Integer -> Text), - IntegerNegate => make_type!(Integer -> Integer), - IntegerClamp => make_type!(Integer -> Natural), - - DoubleShow => make_type!(Double -> Text), - TextShow => make_type!(Text -> Text), - - ListBuild => make_type!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => make_type!( - forall (a: Type) -> - (List a) -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => make_type!(forall (a: Type) -> (List a) -> Natural), - ListHead | ListLast => { - make_type!(forall (a: Type) -> (List a) -> Optional a) - } - ListIndexed => make_type!( - forall (a: Type) -> - (List a) -> - List { index: Natural, value: a } - ), - ListReverse => make_type!( - forall (a: Type) -> (List a) -> List a - ), - - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => make_type!( - forall (A: Type) -> Optional A - ), - }) -} - -pub(crate) fn builtin_to_value(b: Builtin) -> Value { - builtin_to_value_env(b, &NzEnv::new()) -} -pub(crate) fn builtin_to_value_env(b: Builtin, env: &NzEnv) -> Value { - Value::from_kind_and_type( - ValueKind::from_builtin_env(b, env.clone()), - crate::semantics::tck::typecheck::typecheck(&type_of_builtin(b)) - .unwrap() - .normalize_whnf_noenv(), - ) -} diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index 28974af..1df2a48 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,6 +1,6 @@ -pub mod context; pub mod env; pub mod tyexpr; pub mod typecheck; pub(crate) use env::*; pub(crate) use tyexpr::*; +pub(crate) use typecheck::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 114bb14..bf7c130 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,9 +1,8 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::normalize_tyexpr_whnf; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; -use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; +use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 789105f..22ba72d 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -4,12 +4,10 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::merge_maps; -use crate::semantics::phase::typecheck::{ - builtin_to_value, const_to_value, type_of_builtin, -}; use crate::semantics::phase::Normalized; use crate::semantics::{ - Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind, + type_of_builtin, Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, + Value, ValueKind, }; use crate::syntax; use crate::syntax::{ @@ -72,19 +70,19 @@ fn type_one_layer( | ExprKind::Const(Const::Sort) | ExprKind::Embed(..) => unreachable!(), // Handled in type_with - ExprKind::Const(Const::Type) => const_to_value(Const::Kind), - ExprKind::Const(Const::Kind) => const_to_value(Const::Sort), + ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_expr = type_of_builtin(*b); let t_tyexpr = type_with(env, &t_expr)?; t_tyexpr.normalize_whnf(env.as_nzenv()) } - ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool), - ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural), - ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer), - ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double), + ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), + ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural), + ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer), + ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double), ExprKind::TextLit(interpolated) => { - let text_type = builtin_to_value(Builtin::Text); + let text_type = Value::from_builtin(Builtin::Text); for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { @@ -388,7 +386,7 @@ fn type_one_layer( Value::from_const(Const::Type) } ExprKind::BinOp(o, l, r) => { - let t = builtin_to_value(match o { + let t = Value::from_builtin(match o { BinOp::BoolAnd | BinOp::BoolOr | BinOp::BoolEQ -- cgit v1.2.3