summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/builtins.rs31
-rw-r--r--dhall/src/semantics/nze/nir.rs35
-rw-r--r--dhall/src/semantics/nze/normalize.rs22
-rw-r--r--dhall/src/semantics/tck/typecheck.rs28
-rw-r--r--dhall/src/simple.rs36
5 files changed, 66 insertions, 86 deletions
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<Nir> {
- pub env: NzEnv,
- pub b: Builtin,
+pub(crate) struct BuiltinClosure {
+ env: NzEnv,
+ b: Builtin,
/// Arguments applied to the closure so far.
- pub args: Vec<Nir>,
+ args: Vec<Nir>,
}
-impl BuiltinClosure<Nir> {
- 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<Nir>, 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<Nir>, env: NzEnv) -> NirKind {
}
}
-impl<Nir: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Nir> {
+impl std::cmp::PartialEq for BuiltinClosure {
fn eq(&self, other: &Self) -> bool {
self.b == other.b && self.args == other.args
}
}
-impl<Nir: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Nir> {}
+impl std::cmp::Eq for BuiltinClosure {}
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 1148e31..e6482fc 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -70,13 +70,17 @@ pub(crate) enum NirKind {
annot: Nir,
closure: Closure,
},
- AppliedBuiltin(BuiltinClosure<Nir>),
+ AppliedBuiltin(BuiltinClosure),
Var(NzVar),
Const(Const),
+ // Must be a number type, Bool or Text
+ BuiltinType(Builtin),
Num(NumKind),
+ OptionalType(Nir),
EmptyOptionalLit(Nir),
NEOptionalLit(Nir),
+ ListType(Nir),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
EmptyListLit(Nir),
NEListLit(Vec<Nir>),
@@ -187,12 +191,21 @@ impl Nir {
closure.to_hir(venv),
),
NirKind::Const(c) => ExprKind::Const(*c),
+ NirKind::BuiltinType(b) => ExprKind::Builtin(*b),
NirKind::Num(l) => ExprKind::Num(l.clone()),
+ NirKind::OptionalType(t) => ExprKind::App(
+ Nir::from_builtin(Builtin::Optional).to_hir(venv),
+ t.to_hir(venv),
+ ),
NirKind::EmptyOptionalLit(n) => ExprKind::App(
Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
),
NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+ NirKind::ListType(t) => ExprKind::App(
+ Nir::from_builtin(Builtin::List).to_hir(venv),
+ t.to_hir(venv),
+ ),
NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
HirKind::Expr(ExprKind::App(
Nir::from_builtin(Builtin::List).to_hir(venv),
@@ -285,14 +298,20 @@ impl NirKind {
pub(crate) fn normalize(&self) {
match self {
- NirKind::Var(..) | NirKind::Const(_) | NirKind::Num(_) => {}
-
- NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
- tth.normalize();
+ NirKind::Var(..)
+ | NirKind::Const(_)
+ | NirKind::Num(_)
+ | NirKind::BuiltinType(..) => {}
+
+ NirKind::EmptyOptionalLit(v)
+ | NirKind::EmptyListLit(v)
+ | NirKind::OptionalType(v)
+ | NirKind::ListType(v) => {
+ v.normalize();
}
- NirKind::NEOptionalLit(th) => {
- th.normalize();
+ NirKind::NEOptionalLit(v) => {
+ v.normalize();
}
NirKind::LamClosure { annot, closure, .. }
| NirKind::PiClosure { annot, closure, .. } => {
@@ -341,7 +360,7 @@ impl NirKind {
NirKind::from_builtin_env(b, NzEnv::new())
}
pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
- NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ BuiltinClosure::new(b, env)
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c5e66a1..46d8fb5 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -2,12 +2,8 @@ use itertools::Itertools;
use std::collections::HashMap;
use crate::semantics::NzEnv;
-use crate::semantics::{
- Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
-};
-use crate::syntax::{
- BinOp, Builtin, ExprKind, InterpolatedTextContents, NumKind,
-};
+use crate::semantics::{Binder, Closure, Hir, HirKind, Nir, NirKind, TextLit};
+use crate::syntax::{BinOp, ExprKind, InterpolatedTextContents, NumKind};
pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
match f.kind() {
@@ -239,11 +235,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => args[0].clone(),
+ NirKind::ListType(t) => t.clone(),
_ => panic!("internal type error"),
};
Ret::NirKind(NirKind::EmptyListLit(arg))
@@ -442,12 +434,8 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
ExprKind::ToMap(ref v, ref annot) => match v.kind() {
RecordLit(kvs) if kvs.is_empty() => {
match annot.as_ref().map(|v| v.kind()) {
- Some(NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- })) if args.len() == 1 => {
- Ret::NirKind(EmptyListLit(args[0].clone()))
+ Some(NirKind::ListType(t)) => {
+ Ret::NirKind(EmptyListLit(t.clone()))
}
_ => Ret::Expr(expr),
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 6951d62..880ab22 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -5,8 +5,8 @@ use std::collections::HashMap;
use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::semantics::merge_maps;
use crate::semantics::{
- type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
- NirKind, Tir, TyEnv, Type,
+ type_of_builtin, Binder, Closure, Hir, HirKind, Nir, NirKind, Tir, TyEnv,
+ Type,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
@@ -121,11 +121,7 @@ fn type_one_layer(
ExprKind::EmptyListLit(t) => {
let t = t.eval_to_type(env)?;
match t.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => {}
+ NirKind::ListType(..) => {}
_ => return span_err("InvalidListType"),
};
t
@@ -376,10 +372,7 @@ fn type_one_layer(
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
match l.ty().kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- ..
- }) => {}
+ NirKind::ListType(..) => {}
_ => return span_err("BinOpTypeMismatch"),
}
@@ -435,12 +428,7 @@ fn type_one_layer(
let union_type = union.ty();
let variants = match union_type.kind() {
NirKind::UnionType(kts) => Cow::Borrowed(kts),
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::Optional,
- args,
- ..
- }) if args.len() == 1 => {
- let ty = &args[0];
+ NirKind::OptionalType(ty) => {
let mut kts = HashMap::new();
kts.insert("None".into(), None);
kts.insert("Some".into(), Some(ty.clone()));
@@ -595,11 +583,7 @@ fn type_one_layer(
let err_msg = "The type of `toMap x` must be of the form \
`List { mapKey : Text, mapValue : T }`";
let arg = match annot_val.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => &args[0],
+ NirKind::ListType(t) => t,
_ => return span_err(err_msg),
};
let kts = match arg.kind() {
diff --git a/dhall/src/simple.rs b/dhall/src/simple.rs
index 2e5d3c4..45fa656 100644
--- a/dhall/src/simple.rs
+++ b/dhall/src/simple.rs
@@ -1,6 +1,6 @@
use std::collections::BTreeMap;
-use crate::semantics::{BuiltinClosure, Hir, HirKind, Nir, NirKind};
+use crate::semantics::{Hir, HirKind, Nir, NirKind};
use crate::syntax::{Builtin, ExprKind, NumKind, Span};
use crate::Value;
@@ -90,30 +90,16 @@ impl SimpleType {
}
pub(crate) fn from_nir(nir: &Nir) -> Option<Self> {
Some(SimpleType::new(match nir.kind() {
- NirKind::AppliedBuiltin(BuiltinClosure { b, args, .. })
- if args.is_empty() =>
- {
- match b {
- Builtin::Bool => STyKind::Bool,
- Builtin::Natural => STyKind::Natural,
- Builtin::Integer => STyKind::Integer,
- Builtin::Double => STyKind::Double,
- Builtin::Text => STyKind::Text,
- _ => return None,
- }
- }
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::Optional,
- args,
- ..
- }) if args.len() == 1 => {
- STyKind::Optional(Self::from_nir(&args[0])?)
- }
- NirKind::AppliedBuiltin(BuiltinClosure {
- b: Builtin::List,
- args,
- ..
- }) if args.len() == 1 => STyKind::List(Self::from_nir(&args[0])?),
+ NirKind::BuiltinType(b) => match b {
+ Builtin::Bool => STyKind::Bool,
+ Builtin::Natural => STyKind::Natural,
+ Builtin::Integer => STyKind::Integer,
+ Builtin::Double => STyKind::Double,
+ Builtin::Text => STyKind::Text,
+ _ => unreachable!(),
+ },
+ NirKind::OptionalType(t) => STyKind::Optional(Self::from_nir(t)?),
+ NirKind::ListType(t) => STyKind::List(Self::from_nir(t)?),
NirKind::RecordType(kts) => STyKind::Record(
kts.iter()
.map(|(k, v)| Some((k.into(), Self::from_nir(v)?)))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 08:33:56 +0000