summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs494
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/nze/nir.rs5
-rw-r--r--dhall/src/semantics/tck/typecheck.rs5
4 files changed, 5 insertions, 501 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
deleted file mode 100644
index f65e8d1..0000000
--- a/dhall/src/semantics/builtins.rs
+++ /dev/null
@@ -1,494 +0,0 @@
-use crate::operations::OpKind;
-use crate::semantics::{
- skip_resolve_expr, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
-};
-use crate::syntax::map::DupTreeMap;
-use crate::syntax::Const::Type;
-use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
- InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr,
- V,
-};
-use std::collections::HashMap;
-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 struct BuiltinClosure {
- env: NzEnv,
- b: Builtin,
- /// Arguments applied to the closure so far.
- args: Vec<Nir>,
-}
-
-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();
- apply_builtin(self.b, args, self.env.clone())
- }
- pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
- HirKind::Expr(self.args.iter().fold(
- ExprKind::Builtin(self.b),
- |acc, v| {
- ExprKind::Op(OpKind::App(
- Hir::new(HirKind::Expr(acc), Span::Artificial),
- v.to_hir(venv),
- ))
- },
- ))
- }
-}
-
-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) => { 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::Op(OpKind::App(
- rc(ExprKind::Builtin(Builtin::Optional)),
- make_type!($ty)
- )))
- };
- (List $($rest:tt)*) => {
- rc(ExprKind::Op(OpKind::App(
- rc(ExprKind::Builtin(Builtin::List)),
- make_type!($($rest)*)
- )))
- };
- ({ $($label:ident : $ty:ident),* }) => {{
- let mut kts = 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 fn type_of_builtin(b: Builtin) -> Hir {
- use Builtin::*;
- let expr = 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
- ),
- };
- skip_resolve_expr(&expr).unwrap()
-}
-
-// Ad-hoc macro to help construct closures
-macro_rules! make_closure {
- (var($var:ident)) => {{
- rc(ExprKind::Var(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::Op(OpKind::App(
- rc(ExprKind::Builtin(Builtin::List)),
- ty
- )))
- }};
- (Some($($v:tt)*)) => {
- rc(ExprKind::SomeLit(
- make_closure!($($v)*)
- ))
- };
- (1 + $($v:tt)*) => {
- rc(ExprKind::Op(OpKind::BinOp(
- BinOp::NaturalPlus,
- make_closure!($($v)*),
- rc(ExprKind::Num(NumKind::Natural(1)))
- )))
- };
- ([ $($head:tt)* ] # $($tail:tt)*) => {{
- let head = make_closure!($($head)*);
- let tail = make_closure!($($tail)*);
- rc(ExprKind::Op(OpKind::BinOp(
- BinOp::ListAppend,
- rc(ExprKind::NEListLit(vec![head])),
- tail,
- )))
- }};
-}
-
-#[allow(clippy::cognitive_complexity)]
-fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
- use NirKind::*;
- use NumKind::{Bool, Double, Integer, Natural};
-
- // Small helper enum
- enum Ret {
- NirKind(NirKind),
- Nir(Nir),
- DoneAsIs,
- }
- let make_closure = |e| {
- typecheck(&skip_resolve_expr(&e).unwrap())
- .unwrap()
- .eval(env.clone())
- };
-
- 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()))
- }
- (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
- Num(Natural(n)) => Ret::NirKind(Num(Bool(*n == 0))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalEven, [n]) => match &*n.kind() {
- Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 == 0))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalOdd, [n]) => match &*n.kind() {
- Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 != 0))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
- Num(Natural(n)) => Ret::NirKind(Num(Integer(*n as isize))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalShow, [n]) => match &*n.kind() {
- Num(Natural(n)) => Ret::Nir(Nir::from_text(n)),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
- (Num(Natural(a)), Num(Natural(b))) => {
- Ret::NirKind(Num(Natural(if b > a { b - a } else { 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() {
- Num(Integer(n)) => {
- let s = if *n < 0 {
- n.to_string()
- } else {
- format!("+{}", n)
- };
- Ret::Nir(Nir::from_text(s))
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
- Num(Integer(n)) => {
- Ret::NirKind(Num(Double(NaiveDouble::from(*n as f64))))
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::IntegerNegate, [n]) => match &*n.kind() {
- Num(Integer(n)) => Ret::NirKind(Num(Integer(-n))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::IntegerClamp, [n]) => match &*n.kind() {
- Num(Integer(n)) => {
- Ret::NirKind(Num(Natural((*n).try_into().unwrap_or(0))))
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::DoubleShow, [n]) => match &*n.kind() {
- Num(Double(n)) => Ret::Nir(Nir::from_text(n)),
- _ => Ret::DoneAsIs,
- },
- (Builtin::TextShow, [v]) => match &*v.kind() {
- TextLit(tlit) => {
- if let Some(s) = tlit.as_text() {
- // Printing InterpolatedText takes care of all the escaping
- let txt: InterpolatedText<Expr> =
- std::iter::once(InterpolatedTextContents::Text(s))
- .collect();
- Ret::Nir(Nir::from_text(txt))
- } else {
- Ret::DoneAsIs
- }
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::ListLength, [_, l]) => match &*l.kind() {
- EmptyListLit(_) => Ret::NirKind(Num(Natural(0))),
- NEListLit(xs) => Ret::NirKind(Num(Natural(xs.len()))),
- _ => Ret::DoneAsIs,
- },
- (Builtin::ListHead, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
- NEListLit(xs) => {
- Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::ListLast, [_, l]) => match &*l.kind() {
- 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::NirKind(EmptyListLit(n.clone())),
- NEListLit(xs) => {
- Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect()))
- }
- _ => Ret::DoneAsIs,
- },
- (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(),
- Nir::from_builtin(Builtin::Natural),
- );
- kts.insert("value".into(), t.clone());
- let t = Nir::from_kind(RecordType(kts));
-
- // Construct the new list, with added indices
- let list = match l.kind() {
- EmptyListLit(_) => EmptyListLit(t),
- NEListLit(xs) => NEListLit(
- xs.iter()
- .enumerate()
- .map(|(i, e)| {
- let mut kvs = HashMap::new();
- kvs.insert(
- "index".into(),
- Nir::from_kind(Num(Natural(i))),
- );
- kvs.insert("value".into(), e.clone());
- Nir::from_kind(RecordLit(kvs))
- })
- .collect(),
- ),
- _ => unreachable!(),
- };
- Ret::NirKind(list)
- }
- _ => Ret::DoneAsIs,
- }
- }
- (Builtin::ListBuild, [t, f]) => {
- let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
- Ret::Nir(
- f.app(list_t)
- .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_nir()),
- )
- }
- (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
- 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::Nir(v)
- }
- _ => Ret::DoneAsIs,
- },
- (Builtin::OptionalBuild, [t, f]) => {
- let optional_t =
- Nir::from_builtin(Builtin::Optional).app(t.clone());
- Ret::Nir(
- f.app(optional_t)
- .app(
- make_closure(make_closure!(
- λ(T : Type) ->
- λ(a : var(T)) ->
- Some(var(a))
- ))
- .app(t.clone()),
- )
- .app(EmptyOptionalLit(t.clone()).into_nir()),
- )
- }
- (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
- EmptyOptionalLit(_) => Ret::Nir(nothing.clone()),
- NEOptionalLit(x) => Ret::Nir(just.app(x.clone())),
- _ => Ret::DoneAsIs,
- },
- (Builtin::NaturalBuild, [f]) => Ret::Nir(
- f.app(Nir::from_builtin(Builtin::Natural))
- .app(make_closure(make_closure!(
- λ(x : Natural) ->
- 1 + var(x)
- )))
- .app(Num(Natural(0)).into_nir()),
- ),
-
- (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
- Num(Natural(0)) => Ret::Nir(zero.clone()),
- Num(Natural(n)) => {
- let fold = Nir::from_builtin(Builtin::NaturalFold)
- .app(Num(Natural(n - 1)).into_nir())
- .app(t.clone())
- .app(succ.clone())
- .app(zero.clone());
- Ret::Nir(succ.app(fold))
- }
- _ => Ret::DoneAsIs,
- },
- _ => Ret::DoneAsIs,
- };
- match ret {
- Ret::NirKind(v) => v,
- Ret::Nir(v) => v.kind().clone(),
- Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
- }
-}
-
-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 {}
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 468d8b1..a488c31 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,9 +1,7 @@
-pub mod builtins;
pub mod nze;
pub mod parse;
pub mod resolve;
pub mod tck;
-pub use self::builtins::*;
pub use self::nze::*;
pub use self::resolve::*;
pub use self::tck::*;
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 5c67c02..e2a0113 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -1,11 +1,12 @@
use std::collections::HashMap;
use std::rc::Rc;
+use crate::builtins::BuiltinClosure;
use crate::operations::OpKind;
use crate::semantics::nze::lazy;
use crate::semantics::{
- apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder,
- BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+ apply_any, normalize_hir, normalize_one_layer, squash_textlit, Binder, Hir,
+ HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7481f07..a31f15c 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -1,11 +1,10 @@
use std::cmp::max;
use std::collections::HashMap;
+use crate::builtins::type_of_builtin;
use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::operations::typecheck_operation;
-use crate::semantics::{
- type_of_builtin, Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type,
-};
+use crate::semantics::{Hir, HirKind, Nir, NirKind, Tir, TyEnv, Type};
use crate::syntax::{
Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 13:48:34 +0000