summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/semantics/builtins.rs511
-rw-r--r--dhall/src/semantics/core/value.rs31
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/phase/normalize.rs373
-rw-r--r--dhall/src/semantics/phase/typecheck.rs177
-rw-r--r--dhall/src/semantics/tck/mod.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs22
8 files changed, 553 insertions, 568 deletions
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<E>(x: UnspannedExpr<E>) -> Expr<E> {
+ 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<E>(b: Builtin) -> Expr<E> {
+ 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<Value>,
+ ty: &Value,
+ types: Vec<Value>,
+ env: NzEnv,
+) -> ValueKind<Value> {
+ use syntax::Builtin::*;
+ use ValueKind::*;
+
+ // Small helper enum
+ enum Ret<'a> {
+ ValueKind(ValueKind<Value>),
+ 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<Normalized> =
+ 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<Normalized> =
+ 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<Const> {
@@ -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<Value>,
- ty: &Value,
- types: Vec<Value>,
- env: NzEnv,
-) -> ValueKind<Value> {
- use syntax::Builtin::*;
- use ValueKind::*;
-
- // Small helper enum
- enum Ret<'a> {
- ValueKind(ValueKind<Value>),
- 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<Normalized> =
- 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<Normalized> =
- 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<Value> {
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<E>(x: UnspannedExpr<E>) -> Expr<E> {
- 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<E>(b: Builtin) -> Expr<E> {
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:55:03 +0000