summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs54
-rw-r--r--dhall/src/semantics/nze/nir.rs10
-rw-r--r--dhall/src/semantics/nze/normalize.rs70
-rw-r--r--dhall/src/semantics/tck/typecheck.rs10
4 files changed, 72 insertions, 72 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 803630b..8d17aed 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -5,7 +5,7 @@ use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
- InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr,
+ InterpolatedTextContents, Label, NaiveDouble, NumKind, Span, UnspannedExpr,
V,
};
use crate::Normalized;
@@ -241,7 +241,7 @@ macro_rules! make_closure {
rc(ExprKind::BinOp(
BinOp::NaturalPlus,
make_closure!($($v)*),
- rc(ExprKind::Lit(LitKind::Natural(1)))
+ rc(ExprKind::Num(NumKind::Natural(1)))
))
};
([ $($head:tt)* ] # $($tail:tt)*) => {{
@@ -257,8 +257,8 @@ macro_rules! make_closure {
#[allow(clippy::cognitive_complexity)]
fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
- use LitKind::{Bool, Double, Integer, Natural};
use NirKind::*;
+ use NumKind::{Bool, Double, Integer, Natural};
// Small helper enum
enum Ret {
@@ -277,36 +277,36 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
Ret::NirKind(EmptyOptionalLit(t.clone()))
}
(Builtin::NaturalIsZero, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))),
+ Num(Natural(n)) => Ret::NirKind(Num(Bool(*n == 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalEven, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))),
+ Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 == 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalOdd, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))),
+ Num(Natural(n)) => Ret::NirKind(Num(Bool(*n % 2 != 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalToInteger, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))),
+ Num(Natural(n)) => Ret::NirKind(Num(Integer(*n as isize))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalShow, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)),
+ Num(Natural(n)) => Ret::Nir(Nir::from_text(n)),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
- (Lit(Natural(a)), Lit(Natural(b))) => {
- Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 })))
+ (Num(Natural(a)), Num(Natural(b))) => {
+ Ret::NirKind(Num(Natural(if b > a { b - a } else { 0 })))
}
- (Lit(Natural(0)), _) => Ret::Nir(b.clone()),
- (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
- _ if a == b => Ret::NirKind(Lit(Natural(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() {
- Lit(Integer(n)) => {
+ Num(Integer(n)) => {
let s = if *n < 0 {
n.to_string()
} else {
@@ -317,23 +317,23 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
_ => Ret::DoneAsIs,
},
(Builtin::IntegerToDouble, [n]) => match &*n.kind() {
- Lit(Integer(n)) => {
- Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64))))
+ Num(Integer(n)) => {
+ Ret::NirKind(Num(Double(NaiveDouble::from(*n as f64))))
}
_ => Ret::DoneAsIs,
},
(Builtin::IntegerNegate, [n]) => match &*n.kind() {
- Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))),
+ Num(Integer(n)) => Ret::NirKind(Num(Integer(-n))),
_ => Ret::DoneAsIs,
},
(Builtin::IntegerClamp, [n]) => match &*n.kind() {
- Lit(Integer(n)) => {
- Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0))))
+ Num(Integer(n)) => {
+ Ret::NirKind(Num(Natural((*n).try_into().unwrap_or(0))))
}
_ => Ret::DoneAsIs,
},
(Builtin::DoubleShow, [n]) => match &*n.kind() {
- Lit(Double(n)) => Ret::Nir(Nir::from_text(n)),
+ Num(Double(n)) => Ret::Nir(Nir::from_text(n)),
_ => Ret::DoneAsIs,
},
(Builtin::TextShow, [v]) => match &*v.kind() {
@@ -351,8 +351,8 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
_ => Ret::DoneAsIs,
},
(Builtin::ListLength, [_, l]) => match &*l.kind() {
- EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))),
- NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))),
+ EmptyListLit(_) => Ret::NirKind(Num(Natural(0))),
+ NEListLit(xs) => Ret::NirKind(Num(Natural(xs.len()))),
_ => Ret::DoneAsIs,
},
(Builtin::ListHead, [_, l]) => match &*l.kind() {
@@ -398,7 +398,7 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Nir::from_kind(Lit(Natural(i))),
+ Nir::from_kind(Num(Natural(i))),
);
kvs.insert("value".into(), e.clone());
Nir::from_kind(RecordLit(kvs))
@@ -466,14 +466,14 @@ fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
λ(x : Natural) ->
1 + var(x)
)))
- .app(Lit(Natural(0)).into_nir()),
+ .app(Num(Natural(0)).into_nir()),
),
(Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
- Lit(Natural(0)) => Ret::Nir(zero.clone()),
- Lit(Natural(n)) => {
+ Num(Natural(0)) => Ret::Nir(zero.clone()),
+ Num(Natural(n)) => {
let fold = Nir::from_builtin(Builtin::NaturalFold)
- .app(Lit(Natural(n - 1)).into_nir())
+ .app(Num(Natural(n - 1)).into_nir())
.app(t.clone())
.app(succ.clone())
.app(zero.clone());
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 4615b39..6f482a8 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -7,7 +7,7 @@ use crate::semantics::{
BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, NumKind,
Span,
};
use crate::{NormalizedExpr, ToExprOptions};
@@ -75,7 +75,7 @@ pub(crate) enum NirKind {
Var(NzVar),
Const(Const),
- Lit(LitKind),
+ Num(NumKind),
EmptyOptionalLit(Nir),
NEOptionalLit(Nir),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
@@ -145,7 +145,7 @@ impl Nir {
}
pub(crate) fn to_simple_value(&self) -> Option<SimpleValue> {
Some(SimpleValue::new(match self.kind() {
- NirKind::Lit(lit) => SValKind::Lit(lit.clone()),
+ NirKind::Num(lit) => SValKind::Num(lit.clone()),
NirKind::TextLit(x) => SValKind::Text(
x.as_text()
.expect("Normal form should ensure the text is a string"),
@@ -268,7 +268,7 @@ impl Nir {
closure.to_hir(venv),
),
NirKind::Const(c) => ExprKind::Const(*c),
- NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+ NirKind::Num(l) => ExprKind::Num(l.clone()),
NirKind::EmptyOptionalLit(n) => ExprKind::App(
Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
@@ -366,7 +366,7 @@ impl NirKind {
pub(crate) fn normalize(&self) {
match self {
- NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+ NirKind::Var(..) | NirKind::Const(_) | NirKind::Num(_) => {}
NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
tth.normalize();
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 79d55e8..c5e66a1 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,7 +6,7 @@ use crate::semantics::{
Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
};
use crate::syntax::{
- BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
+ BinOp, Builtin, ExprKind, InterpolatedTextContents, NumKind,
};
pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
@@ -99,40 +99,40 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use LitKind::{Bool, Natural};
- use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+ use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
+ use NumKind::{Bool, Natural};
Some(match (o, x.kind(), y.kind()) {
- (BoolAnd, Lit(Bool(true)), _) => Ret::NirRef(y),
- (BoolAnd, _, Lit(Bool(true))) => Ret::NirRef(x),
- (BoolAnd, Lit(Bool(false)), _) => Ret::NirKind(Lit(Bool(false))),
- (BoolAnd, _, Lit(Bool(false))) => Ret::NirKind(Lit(Bool(false))),
+ (BoolAnd, Num(Bool(true)), _) => Ret::NirRef(y),
+ (BoolAnd, _, Num(Bool(true))) => Ret::NirRef(x),
+ (BoolAnd, Num(Bool(false)), _) => Ret::NirKind(Num(Bool(false))),
+ (BoolAnd, _, Num(Bool(false))) => Ret::NirKind(Num(Bool(false))),
(BoolAnd, _, _) if x == y => Ret::NirRef(x),
- (BoolOr, Lit(Bool(true)), _) => Ret::NirKind(Lit(Bool(true))),
- (BoolOr, _, Lit(Bool(true))) => Ret::NirKind(Lit(Bool(true))),
- (BoolOr, Lit(Bool(false)), _) => Ret::NirRef(y),
- (BoolOr, _, Lit(Bool(false))) => Ret::NirRef(x),
+ (BoolOr, Num(Bool(true)), _) => Ret::NirKind(Num(Bool(true))),
+ (BoolOr, _, Num(Bool(true))) => Ret::NirKind(Num(Bool(true))),
+ (BoolOr, Num(Bool(false)), _) => Ret::NirRef(y),
+ (BoolOr, _, Num(Bool(false))) => Ret::NirRef(x),
(BoolOr, _, _) if x == y => Ret::NirRef(x),
- (BoolEQ, Lit(Bool(true)), _) => Ret::NirRef(y),
- (BoolEQ, _, Lit(Bool(true))) => Ret::NirRef(x),
- (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x == y))),
- (BoolEQ, _, _) if x == y => Ret::NirKind(Lit(Bool(true))),
- (BoolNE, Lit(Bool(false)), _) => Ret::NirRef(y),
- (BoolNE, _, Lit(Bool(false))) => Ret::NirRef(x),
- (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => Ret::NirKind(Lit(Bool(x != y))),
- (BoolNE, _, _) if x == y => Ret::NirKind(Lit(Bool(false))),
+ (BoolEQ, Num(Bool(true)), _) => Ret::NirRef(y),
+ (BoolEQ, _, Num(Bool(true))) => Ret::NirRef(x),
+ (BoolEQ, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x == y))),
+ (BoolEQ, _, _) if x == y => Ret::NirKind(Num(Bool(true))),
+ (BoolNE, Num(Bool(false)), _) => Ret::NirRef(y),
+ (BoolNE, _, Num(Bool(false))) => Ret::NirRef(x),
+ (BoolNE, Num(Bool(x)), Num(Bool(y))) => Ret::NirKind(Num(Bool(x != y))),
+ (BoolNE, _, _) if x == y => Ret::NirKind(Num(Bool(false))),
- (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
- (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
- (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
- Ret::NirKind(Lit(Natural(x + y)))
+ (NaturalPlus, Num(Natural(0)), _) => Ret::NirRef(y),
+ (NaturalPlus, _, Num(Natural(0))) => Ret::NirRef(x),
+ (NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
+ Ret::NirKind(Num(Natural(x + y)))
}
- (NaturalTimes, Lit(Natural(0)), _) => Ret::NirKind(Lit(Natural(0))),
- (NaturalTimes, _, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
- (NaturalTimes, Lit(Natural(1)), _) => Ret::NirRef(y),
- (NaturalTimes, _, Lit(Natural(1))) => Ret::NirRef(x),
- (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
- Ret::NirKind(Lit(Natural(x * y)))
+ (NaturalTimes, Num(Natural(0)), _) => Ret::NirKind(Num(Natural(0))),
+ (NaturalTimes, _, Num(Natural(0))) => Ret::NirKind(Num(Natural(0))),
+ (NaturalTimes, Num(Natural(1)), _) => Ret::NirRef(y),
+ (NaturalTimes, _, Num(Natural(1))) => Ret::NirRef(x),
+ (NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
+ Ret::NirKind(Num(Natural(x * y)))
}
(ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
@@ -212,12 +212,12 @@ fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
#[allow(clippy::cognitive_complexity)]
pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
- use LitKind::Bool;
use NirKind::{
- EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+ EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num,
PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
UnionType,
};
+ use NumKind::Bool;
let ret = match expr {
ExprKind::Import(..) | ExprKind::Completion(..) => {
@@ -235,7 +235,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
ExprKind::Assert(_) => Ret::Expr(expr),
ExprKind::App(v, a) => Ret::Nir(v.app(a)),
- ExprKind::Lit(l) => Ret::NirKind(Lit(l)),
+ ExprKind::Num(l) => Ret::NirKind(Num(l)),
ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
@@ -271,12 +271,12 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
match b.kind() {
- Lit(Bool(true)) => Ret::NirRef(e1),
- Lit(Bool(false)) => Ret::NirRef(e2),
+ Num(Bool(true)) => Ret::NirRef(e1),
+ Num(Bool(false)) => Ret::NirRef(e2),
_ => {
match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
- (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+ (Num(Bool(true)), Num(Bool(false))) => Ret::NirRef(b),
_ if e1 == e2 => Ret::NirRef(e1),
_ => Ret::Expr(expr),
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 9fa33f2..6951d62 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -9,7 +9,7 @@ use crate::semantics::{
NirKind, Tir, TyEnv, Type,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, NumKind, Span,
};
fn check_rectymerge(
@@ -96,14 +96,14 @@ fn type_one_layer(
let t_hir = type_of_builtin(*b);
typecheck(&t_hir)?.eval_to_type(env)?
}
- ExprKind::Lit(LitKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
- ExprKind::Lit(LitKind::Natural(_)) => {
+ ExprKind::Num(NumKind::Bool(_)) => Type::from_builtin(Builtin::Bool),
+ ExprKind::Num(NumKind::Natural(_)) => {
Type::from_builtin(Builtin::Natural)
}
- ExprKind::Lit(LitKind::Integer(_)) => {
+ ExprKind::Num(NumKind::Integer(_)) => {
Type::from_builtin(Builtin::Integer)
}
- ExprKind::Lit(LitKind::Double(_)) => {
+ ExprKind::Num(NumKind::Double(_)) => {
Type::from_builtin(Builtin::Double)
}
ExprKind::TextLit(interpolated) => {