summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/builtins.rs119
-rw-r--r--dhall/src/semantics/nze/normalize.rs86
-rw-r--r--dhall/src/semantics/nze/value.rs21
-rw-r--r--dhall/src/semantics/tck/typecheck.rs16
-rw-r--r--dhall/src/syntax/ast/expr.rs22
-rw-r--r--dhall/src/syntax/ast/visitor.rs5
-rw-r--r--dhall/src/syntax/binary/decode.rs18
-rw-r--r--dhall/src/syntax/binary/encode.rs9
-rw-r--r--dhall/src/syntax/text/parser.rs11
-rw-r--r--dhall/src/syntax/text/printer.rs30
10 files changed, 179 insertions, 158 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index cbb5a6e..752b25c 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -5,7 +5,8 @@ use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
use crate::syntax::{
BinOp, Builtin, Const, Expr, ExprKind, InterpolatedText,
- InterpolatedTextContents, Label, NaiveDouble, Span, UnspannedExpr, V,
+ InterpolatedTextContents, Label, LitKind, NaiveDouble, Span, UnspannedExpr,
+ V,
};
use crate::Normalized;
use std::collections::HashMap;
@@ -240,7 +241,7 @@ macro_rules! make_closure {
rc(ExprKind::BinOp(
BinOp::NaturalPlus,
make_closure!($($v)*),
- rc(ExprKind::NaturalLit(1))
+ rc(ExprKind::Lit(LitKind::Natural(1)))
))
};
([ $($head:tt)* ] # $($tail:tt)*) => {{
@@ -256,7 +257,7 @@ macro_rules! make_closure {
#[allow(clippy::cognitive_complexity)]
fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
- use Builtin::*;
+ use LitKind::{Bool, Double, Integer, Natural};
use ValueKind::*;
// Small helper enum
@@ -272,38 +273,40 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
};
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
- (NaturalIsZero, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
+ (Builtin::OptionalNone, [t]) => {
+ Ret::ValueKind(EmptyOptionalLit(t.clone()))
+ }
+ (Builtin::NaturalIsZero, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))),
_ => Ret::DoneAsIs,
},
- (NaturalEven, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
+ (Builtin::NaturalEven, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))),
_ => Ret::DoneAsIs,
},
- (NaturalOdd, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
+ (Builtin::NaturalOdd, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))),
_ => Ret::DoneAsIs,
},
- (NaturalToInteger, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
+ (Builtin::NaturalToInteger, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))),
_ => Ret::DoneAsIs,
},
- (NaturalShow, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::Value(Value::from_text(n)),
+ (Builtin::NaturalShow, [n]) => match &*n.kind() {
+ Lit(Natural(n)) => Ret::Value(Value::from_text(n)),
_ => Ret::DoneAsIs,
},
- (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
- (NaturalLit(a), NaturalLit(b)) => {
- Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
+ (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
+ (Lit(Natural(a)), Lit(Natural(b))) => {
+ Ret::ValueKind(Lit(Natural(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)),
+ (Lit(Natural(0)), _) => Ret::Value(b.clone()),
+ (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
+ _ if a == b => Ret::ValueKind(Lit(Natural(0))),
_ => Ret::DoneAsIs,
},
- (IntegerShow, [n]) => match &*n.kind() {
- IntegerLit(n) => {
+ (Builtin::IntegerShow, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
let s = if *n < 0 {
n.to_string()
} else {
@@ -313,27 +316,27 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
}
_ => Ret::DoneAsIs,
},
- (IntegerToDouble, [n]) => match &*n.kind() {
- IntegerLit(n) => {
- Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
+ (Builtin::IntegerToDouble, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
+ Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64))))
}
_ => Ret::DoneAsIs,
},
- (IntegerNegate, [n]) => match &*n.kind() {
- IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+ (Builtin::IntegerNegate, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))),
_ => Ret::DoneAsIs,
},
- (IntegerClamp, [n]) => match &*n.kind() {
- IntegerLit(n) => {
- Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+ (Builtin::IntegerClamp, [n]) => match &*n.kind() {
+ Lit(Integer(n)) => {
+ Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0))))
}
_ => Ret::DoneAsIs,
},
- (DoubleShow, [n]) => match &*n.kind() {
- DoubleLit(n) => Ret::Value(Value::from_text(n)),
+ (Builtin::DoubleShow, [n]) => match &*n.kind() {
+ Lit(Double(n)) => Ret::Value(Value::from_text(n)),
_ => Ret::DoneAsIs,
},
- (TextShow, [v]) => match &*v.kind() {
+ (Builtin::TextShow, [v]) => match &*v.kind() {
TextLit(tlit) => {
if let Some(s) = tlit.as_text() {
// Printing InterpolatedText takes care of all the escaping
@@ -347,38 +350,41 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
}
_ => Ret::DoneAsIs,
},
- (ListLength, [_, l]) => match &*l.kind() {
- EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
- NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
+ (Builtin::ListLength, [_, l]) => match &*l.kind() {
+ EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))),
+ NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))),
_ => Ret::DoneAsIs,
},
- (ListHead, [_, l]) => match &*l.kind() {
+ (Builtin::ListHead, [_, l]) => match &*l.kind() {
EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
_ => Ret::DoneAsIs,
},
- (ListLast, [_, l]) => match &*l.kind() {
+ (Builtin::ListLast, [_, l]) => match &*l.kind() {
EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
xs.iter().rev().next().unwrap().clone(),
)),
_ => Ret::DoneAsIs,
},
- (ListReverse, [_, l]) => match &*l.kind() {
+ (Builtin::ListReverse, [_, l]) => match &*l.kind() {
EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
}
_ => Ret::DoneAsIs,
},
- (ListIndexed, [t, l]) => {
+ (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(), Value::from_builtin(Natural));
+ kts.insert(
+ "index".into(),
+ Value::from_builtin(Builtin::Natural),
+ );
kts.insert("value".into(), t.clone());
let t = Value::from_kind(RecordType(kts));
@@ -392,7 +398,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_kind(NaturalLit(i)),
+ Value::from_kind(Lit(Natural(i))),
);
kvs.insert("value".into(), e.clone());
Value::from_kind(RecordLit(kvs))
@@ -406,8 +412,8 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
_ => Ret::DoneAsIs,
}
}
- (ListBuild, [t, f]) => {
- let list_t = Value::from_builtin(List).app(t.clone());
+ (Builtin::ListBuild, [t, f]) => {
+ let list_t = Value::from_builtin(Builtin::List).app(t.clone());
Ret::Value(
f.app(list_t.clone())
.app(
@@ -422,7 +428,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
.app(EmptyListLit(t.clone()).into_value()),
)
}
- (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
+ (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
EmptyListLit(_) => Ret::Value(nil.clone()),
NEListLit(xs) => {
let mut v = nil.clone();
@@ -433,8 +439,9 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
}
_ => Ret::DoneAsIs,
},
- (OptionalBuild, [t, f]) => {
- let optional_t = Value::from_builtin(Optional).app(t.clone());
+ (Builtin::OptionalBuild, [t, f]) => {
+ let optional_t =
+ Value::from_builtin(Builtin::Optional).app(t.clone());
Ret::Value(
f.app(optional_t.clone())
.app(
@@ -448,25 +455,25 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
.app(EmptyOptionalLit(t.clone()).into_value()),
)
}
- (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
+ (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
_ => Ret::DoneAsIs,
},
- (NaturalBuild, [f]) => Ret::Value(
- f.app(Value::from_builtin(Natural))
+ (Builtin::NaturalBuild, [f]) => Ret::Value(
+ f.app(Value::from_builtin(Builtin::Natural))
.app(make_closure(make_closure!(
λ(x : Natural) ->
1 + var(x)
)))
- .app(NaturalLit(0).into_value()),
+ .app(Lit(Natural(0)).into_value()),
),
- (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
- NaturalLit(0) => Ret::Value(zero.clone()),
- NaturalLit(n) => {
- let fold = Value::from_builtin(NaturalFold)
- .app(NaturalLit(n - 1).into_value())
+ (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
+ Lit(Natural(0)) => Ret::Value(zero.clone()),
+ Lit(Natural(n)) => {
+ let fold = Value::from_builtin(Builtin::NaturalFold)
+ .app(Lit(Natural(n - 1)).into_value())
.app(t.clone())
.app(succ.clone())
.app(zero.clone());
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 03b91a5..4111190 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -5,7 +5,9 @@ use crate::semantics::NzEnv;
use crate::semantics::{
Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
};
-use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
+use crate::syntax::{
+ BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
+};
pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
match f.kind() {
@@ -98,40 +100,44 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
- use ValueKind::{
- BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
- };
+ use LitKind::{Bool, Natural};
+ use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+
Some(match (o, x.kind(), y.kind()) {
- (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
- (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
- (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
+ (BoolAnd, Lit(Bool(true)), _) => Ret::ValueRef(y),
+ (BoolAnd, _, Lit(Bool(true))) => Ret::ValueRef(x),
+ (BoolAnd, Lit(Bool(false)), _) => Ret::ValueKind(Lit(Bool(false))),
+ (BoolAnd, _, Lit(Bool(false))) => Ret::ValueKind(Lit(Bool(false))),
(BoolAnd, _, _) if x == y => Ret::ValueRef(x),
- (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
- (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
- (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
- (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+ (BoolOr, Lit(Bool(true)), _) => Ret::ValueKind(Lit(Bool(true))),
+ (BoolOr, _, Lit(Bool(true))) => Ret::ValueKind(Lit(Bool(true))),
+ (BoolOr, Lit(Bool(false)), _) => Ret::ValueRef(y),
+ (BoolOr, _, Lit(Bool(false))) => Ret::ValueRef(x),
(BoolOr, _, _) if x == y => Ret::ValueRef(x),
- (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
- (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
- (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
- (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
- (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
- (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
- (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
- (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+ (BoolEQ, Lit(Bool(true)), _) => Ret::ValueRef(y),
+ (BoolEQ, _, Lit(Bool(true))) => Ret::ValueRef(x),
+ (BoolEQ, Lit(Bool(x)), Lit(Bool(y))) => {
+ Ret::ValueKind(Lit(Bool(x == y)))
+ }
+ (BoolEQ, _, _) if x == y => Ret::ValueKind(Lit(Bool(true))),
+ (BoolNE, Lit(Bool(false)), _) => Ret::ValueRef(y),
+ (BoolNE, _, Lit(Bool(false))) => Ret::ValueRef(x),
+ (BoolNE, Lit(Bool(x)), Lit(Bool(y))) => {
+ Ret::ValueKind(Lit(Bool(x != y)))
+ }
+ (BoolNE, _, _) if x == y => Ret::ValueKind(Lit(Bool(false))),
- (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
- (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
- (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueKind(NaturalLit(x + y))
- }
- (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
- (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
- (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
- (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
- (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueKind(NaturalLit(x * y))
+ (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y),
+ (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x),
+ (NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
+ Ret::ValueKind(Lit(Natural(x + y)))
+ }
+ (NaturalTimes, Lit(Natural(0)), _) => Ret::ValueKind(Lit(Natural(0))),
+ (NaturalTimes, _, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
+ (NaturalTimes, Lit(Natural(1)), _) => Ret::ValueRef(y),
+ (NaturalTimes, _, Lit(Natural(1))) => Ret::ValueRef(x),
+ (NaturalTimes, Lit(Natural(x)), Lit(Natural(y))) => {
+ Ret::ValueKind(Lit(Natural(x * y)))
}
(ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
@@ -217,10 +223,11 @@ pub(crate) fn normalize_one_layer(
expr: ExprKind<Value>,
env: &NzEnv,
) -> ValueKind {
+ use LitKind::Bool;
use ValueKind::{
- BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
- NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
- RecordType, UnionConstructor, UnionLit, UnionType,
+ EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+ PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+ UnionType,
};
let ret = match expr {
@@ -240,10 +247,7 @@ pub(crate) fn normalize_one_layer(
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)),
- ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
- ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
- ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+ ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())),
ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
@@ -279,12 +283,12 @@ pub(crate) fn normalize_one_layer(
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
match b.kind() {
- BoolLit(true) => Ret::ValueRef(e1),
- BoolLit(false) => Ret::ValueRef(e2),
+ Lit(Bool(true)) => Ret::ValueRef(e1),
+ Lit(Bool(false)) => Ret::ValueRef(e2),
_ => {
match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
- (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b),
_ if e1 == e2 => Ret::ValueRef(e1),
_ => Ret::Expr(expr),
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 0df3c74..2ae6852 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -9,8 +9,8 @@ use crate::semantics::{
TyExpr, VarEnv,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural, Span,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+ Span,
};
use crate::{NormalizedExpr, ToExprOptions};
@@ -76,10 +76,7 @@ pub(crate) enum ValueKind {
Var(NzVar),
Const(Const),
- BoolLit(bool),
- NaturalLit(Natural),
- IntegerLit(Integer),
- DoubleLit(NaiveDouble),
+ Lit(LitKind),
EmptyOptionalLit(Value),
NEOptionalLit(Value),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
@@ -205,10 +202,7 @@ impl Value {
closure.to_hir(venv),
),
ValueKind::Const(c) => ExprKind::Const(*c),
- ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
- ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n),
- ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
- ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
+ ValueKind::Lit(l) => ExprKind::Lit(l.clone()),
ValueKind::EmptyOptionalLit(n) => ExprKind::App(
Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
@@ -317,12 +311,7 @@ impl ValueKind {
pub(crate) fn normalize(&self) {
match self {
- ValueKind::Var(..)
- | ValueKind::Const(_)
- | ValueKind::BoolLit(_)
- | ValueKind::NaturalLit(_)
- | ValueKind::IntegerLit(_)
- | ValueKind::DoubleLit(_) => {}
+ ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
tth.normalize();
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index f9ff3d3..c52cfda 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -9,7 +9,7 @@ use crate::semantics::{
TyExpr, TyExprKind, Type, Value, ValueKind,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Span,
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
};
fn type_of_recordtype<'a>(
@@ -115,10 +115,16 @@ fn type_one_layer(
let t_tyexpr = typecheck(&t_hir)?;
t_tyexpr.eval(env)
}
- 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::Lit(LitKind::Bool(_)) => Value::from_builtin(Builtin::Bool),
+ ExprKind::Lit(LitKind::Natural(_)) => {
+ Value::from_builtin(Builtin::Natural)
+ }
+ ExprKind::Lit(LitKind::Integer(_)) => {
+ Value::from_builtin(Builtin::Integer)
+ }
+ ExprKind::Lit(LitKind::Double(_)) => {
+ Value::from_builtin(Builtin::Double)
+ }
ExprKind::TextLit(interpolated) => {
let text_type = Value::from_builtin(Builtin::Text);
for contents in interpolated.iter() {
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 512010a..18ec9fd 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -103,6 +103,19 @@ pub struct Expr {
pub type UnspannedExpr = ExprKind<Expr>;
+/// Simple literals
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+pub enum LitKind {
+ /// `True`
+ Bool(bool),
+ /// `1`
+ Natural(Natural),
+ /// `+2`
+ Integer(Integer),
+ /// `3.24`
+ Double(Double),
+}
+
/// Syntax tree for expressions
// Having the recursion out of the enum definition enables writing
// much more generic code and improves pattern-matching behind
@@ -110,6 +123,7 @@ pub type UnspannedExpr = ExprKind<Expr>;
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum ExprKind<SubExpr> {
Const(Const),
+ Lit(LitKind),
/// `x`
/// `x@n`
Var(V),
@@ -131,16 +145,8 @@ pub enum ExprKind<SubExpr> {
Builtin(Builtin),
// Binary operations
BinOp(BinOp, SubExpr, SubExpr),
- /// `True`
- BoolLit(bool),
/// `if x then y else z`
BoolIf(SubExpr, SubExpr, SubExpr),
- /// `1`
- NaturalLit(Natural),
- /// `+2`
- IntegerLit(Integer),
- /// `3.24`
- DoubleLit(Double),
/// `"Some ${interpolated} text"`
TextLit(InterpolatedText<SubExpr>),
/// `[] : t`
diff --git a/dhall/src/syntax/ast/visitor.rs b/dhall/src/syntax/ast/visitor.rs
index 39959ac..c361bc1 100644
--- a/dhall/src/syntax/ast/visitor.rs
+++ b/dhall/src/syntax/ast/visitor.rs
@@ -91,10 +91,7 @@ where
Annot(x, t) => Annot(expr!(x)?, expr!(t)?),
Const(k) => Const(*k),
Builtin(v) => Builtin(*v),
- BoolLit(b) => BoolLit(*b),
- NaturalLit(n) => NaturalLit(*n),
- IntegerLit(n) => IntegerLit(*n),
- DoubleLit(n) => DoubleLit(*n),
+ Lit(l) => Lit(l.clone()),
TextLit(t) => TextLit(t.traverse_ref(|e| expr!(e))?),
BinOp(o, x, y) => BinOp(*o, expr!(x)?, expr!(y)?),
BoolIf(b, t, f) => BoolIf(expr!(b)?, expr!(t)?, expr!(f)?),
diff --git a/dhall/src/syntax/binary/decode.rs b/dhall/src/syntax/binary/decode.rs
index 6fbcc10..2e50d61 100644
--- a/dhall/src/syntax/binary/decode.rs
+++ b/dhall/src/syntax/binary/decode.rs
@@ -6,8 +6,8 @@ use crate::error::DecodeError;
use crate::syntax;
use crate::syntax::{
Expr, ExprKind, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
- Integer, InterpolatedText, Label, Natural, Scheme, Span, UnspannedExpr,
- URL, V,
+ Integer, InterpolatedText, Label, LitKind, Natural, Scheme, Span,
+ UnspannedExpr, URL, V,
};
use crate::DecodedExpr;
@@ -31,8 +31,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
String(s) => match Builtin::parse(s) {
Some(b) => ExprKind::Builtin(b),
None => match s.as_str() {
- "True" => BoolLit(true),
- "False" => BoolLit(false),
+ "True" => Lit(LitKind::Bool(true)),
+ "False" => Lit(LitKind::Bool(false)),
"Type" => Const(Const::Type),
"Kind" => Const(Const::Kind),
"Sort" => Const(Const::Sort),
@@ -40,8 +40,8 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
},
},
U64(n) => Var(V(Label::from("_"), *n as usize)),
- F64(x) => DoubleLit((*x).into()),
- Bool(b) => BoolLit(*b),
+ F64(x) => Lit(LitKind::Double((*x).into())),
+ Bool(b) => Lit(LitKind::Bool(*b)),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
if l.as_str() == "_" {
@@ -216,9 +216,9 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
let z = cbor_value_to_dhall(&z)?;
BoolIf(x, y, z)
}
- [U64(15), U64(x)] => NaturalLit(*x as Natural),
- [U64(16), U64(x)] => IntegerLit(*x as Integer),
- [U64(16), I64(x)] => IntegerLit(*x as Integer),
+ [U64(15), U64(x)] => Lit(LitKind::Natural(*x as Natural)),
+ [U64(16), U64(x)] => Lit(LitKind::Integer(*x as Integer)),
+ [U64(16), I64(x)] => Lit(LitKind::Integer(*x as Integer)),
[U64(18), String(first), rest @ ..] => {
TextLit(InterpolatedText::from((
first.clone(),
diff --git a/dhall/src/syntax/binary/encode.rs b/dhall/src/syntax/binary/encode.rs
index 686f737..291ac4a 100644
--- a/dhall/src/syntax/binary/encode.rs
+++ b/dhall/src/syntax/binary/encode.rs
@@ -46,6 +46,7 @@ where
use std::iter::once;
use syntax::Builtin;
use syntax::ExprKind::*;
+ use syntax::LitKind::*;
use self::Serialize::{RecordMap, UnionMap};
fn expr(x: &Expr) -> self::Serialize<'_> {
@@ -60,10 +61,10 @@ where
match e.as_ref() {
Const(c) => ser.serialize_str(&c.to_string()),
Builtin(b) => ser.serialize_str(&b.to_string()),
- BoolLit(b) => ser.serialize_bool(*b),
- NaturalLit(n) => ser_seq!(ser; tag(15), U64(*n as u64)),
- IntegerLit(n) => ser_seq!(ser; tag(16), I64(*n as i64)),
- DoubleLit(n) => {
+ Lit(Bool(b)) => ser.serialize_bool(*b),
+ Lit(Natural(n)) => ser_seq!(ser; tag(15), U64(*n as u64)),
+ Lit(Integer(n)) => ser_seq!(ser; tag(16), I64(*n as i64)),
+ Lit(Double(n)) => {
let n: f64 = (*n).into();
ser.serialize_f64(n)
}
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 0ff1363..f3ebd2b 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -7,6 +7,7 @@ use pest_consume::{match_nodes, Parser};
use crate::syntax::map::{DupTreeMap, DupTreeSet};
use crate::syntax::ExprKind::*;
+use crate::syntax::LitKind::*;
use crate::syntax::{
Double, Expr, FilePath, FilePrefix, Hash, ImportLocation, ImportMode,
Integer, InterpolatedText, InterpolatedTextContents, Label, NaiveDouble,
@@ -344,8 +345,8 @@ impl DhallParser {
let e = match crate::syntax::Builtin::parse(s) {
Some(b) => Builtin(b),
None => match s {
- "True" => BoolLit(true),
- "False" => BoolLit(false),
+ "True" => Lit(Bool(true)),
+ "False" => Lit(Bool(false)),
"Type" => Const(crate::syntax::Const::Type),
"Kind" => Const(crate::syntax::Const::Kind),
"Sort" => Const(crate::syntax::Const::Sort),
@@ -833,9 +834,9 @@ impl DhallParser {
#[alias(expression, shortcut = true)]
fn primitive_expression(input: ParseInput) -> ParseResult<Expr> {
Ok(match_nodes!(input.children();
- [double_literal(n)] => spanned(input, DoubleLit(n)),
- [natural_literal(n)] => spanned(input, NaturalLit(n)),
- [integer_literal(n)] => spanned(input, IntegerLit(n)),
+ [double_literal(n)] => spanned(input, Lit(Double(n))),
+ [natural_literal(n)] => spanned(input, Lit(Natural(n))),
+ [integer_literal(n)] => spanned(input, Lit(Integer(n))),
[double_quote_literal(s)] => spanned(input, TextLit(s)),
[single_quote_literal(s)] => spanned(input, TextLit(s)),
[record_type_or_literal(e)] => spanned(input, e),
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index d1c9588..8891d41 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -196,15 +196,7 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
Var(a) => a.fmt(f)?,
Const(k) => k.fmt(f)?,
Builtin(v) => v.fmt(f)?,
- BoolLit(true) => f.write_str("True")?,
- BoolLit(false) => f.write_str("False")?,
- NaturalLit(a) => a.fmt(f)?,
- IntegerLit(a) if *a >= 0 => {
- f.write_str("+")?;
- a.fmt(f)?;
- }
- IntegerLit(a) => a.fmt(f)?,
- DoubleLit(a) => a.fmt(f)?,
+ Lit(a) => a.fmt(f)?,
TextLit(a) => a.fmt(f)?,
RecordType(a) if a.is_empty() => f.write_str("{}")?,
RecordType(a) => fmt_list("{ ", ", ", " }", a, f, |(k, t), f| {
@@ -239,7 +231,25 @@ impl<SE: Display + Clone> Display for ExprKind<SE> {
impl Display for Expr {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
- self.as_ref().fmt_phase(f, PrintPhase::Base)
+ self.kind().fmt_phase(f, PrintPhase::Base)
+ }
+}
+
+impl Display for LitKind {
+ fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
+ use LitKind::*;
+ match self {
+ Bool(true) => f.write_str("True")?,
+ Bool(false) => f.write_str("False")?,
+ Natural(a) => a.fmt(f)?,
+ Integer(a) if *a >= 0 => {
+ f.write_str("+")?;
+ a.fmt(f)?;
+ }
+ Integer(a) => a.fmt(f)?,
+ Double(a) => a.fmt(f)?,
+ }
+ Ok(())
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 17:36:58 +0000