summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
authorNadrieril2020-03-13 21:21:32 +0000
committerNadrieril2020-03-31 21:44:01 +0100
commitef3734a3e9381b2e91552089774126f58f560bc3 (patch)
tree6b1ff7e44feb23e333e8a1d4dadaff2d05a58881 /dhall/src/semantics/nze
parent1a0929b52af57d5963dd9da9e5cf85ffbed3a8f7 (diff)
Improve handling of builtin types in Nir
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/nze/nir.rs35
-rw-r--r--dhall/src/semantics/nze/normalize.rs22
2 files changed, 32 insertions, 25 deletions
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),
}