summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/lib.rs36
-rw-r--r--dhall/src/semantics/builtins.rs118
-rw-r--r--dhall/src/semantics/nze/env.rs10
-rw-r--r--dhall/src/semantics/nze/mod.rs4
-rw-r--r--dhall/src/semantics/nze/nir.rs (renamed from dhall/src/semantics/nze/value.rs)237
-rw-r--r--dhall/src/semantics/nze/normalize.rs243
-rw-r--r--dhall/src/semantics/nze/var.rs2
-rw-r--r--dhall/src/semantics/resolve/hir.rs6
-rw-r--r--dhall/src/semantics/tck/env.rs4
-rw-r--r--dhall/src/semantics/tck/tir.rs26
-rw-r--r--dhall/src/semantics/tck/typecheck.rs90
-rw-r--r--dhall/src/tests.rs2
12 files changed, 377 insertions, 401 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 3fbc251..a4987c6 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -22,7 +22,7 @@ use crate::error::{EncodeError, Error, TypeError};
use crate::semantics::parse;
use crate::semantics::resolve;
use crate::semantics::resolve::ImportRoot;
-use crate::semantics::{typecheck, typecheck_with, Hir, Tir, Value, ValueKind};
+use crate::semantics::{typecheck, typecheck_with, Hir, Nir, NirKind, Tir};
use crate::syntax::binary;
use crate::syntax::{Builtin, Expr};
@@ -48,9 +48,9 @@ pub struct Typed(Tir);
///
/// Invariant: the contained Typed expression must be in normal form,
#[derive(Debug, Clone)]
-pub struct Normalized(Value);
+pub struct Normalized(Nir);
-/// Controls conversion from `Value` to `Expr`
+/// Controls conversion from `Nir` to `Expr`
#[derive(Copy, Clone)]
pub(crate) struct ToExprOptions {
/// Whether to convert all variables to `_`
@@ -118,7 +118,7 @@ impl Typed {
}
pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
- Ok(Normalized(self.0.ty().clone().into_value()))
+ Ok(Normalized(self.0.ty().clone().into_nir()))
}
}
@@ -145,45 +145,43 @@ impl Normalized {
normalize: false,
})
}
- pub(crate) fn to_value(&self) -> Value {
+ pub(crate) fn to_nir(&self) -> Nir {
self.0.clone()
}
- pub(crate) fn into_value(self) -> Value {
+ pub(crate) fn into_nir(self) -> Nir {
self.0
}
- pub(crate) fn from_kind(v: ValueKind) -> Self {
- Normalized(Value::from_kind(v))
+ pub(crate) fn from_kind(v: NirKind) -> Self {
+ Normalized(Nir::from_kind(v))
}
- pub(crate) fn from_value(th: Value) -> Self {
+ pub(crate) fn from_nir(th: Nir) -> Self {
Normalized(th)
}
pub fn make_builtin_type(b: Builtin) -> Self {
- Normalized::from_value(Value::from_builtin(b))
+ Normalized::from_nir(Nir::from_builtin(b))
}
pub fn make_optional_type(t: Normalized) -> Self {
- Normalized::from_value(
- Value::from_builtin(Builtin::Optional).app(t.to_value()),
+ Normalized::from_nir(
+ Nir::from_builtin(Builtin::Optional).app(t.to_nir()),
)
}
pub fn make_list_type(t: Normalized) -> Self {
- Normalized::from_value(
- Value::from_builtin(Builtin::List).app(t.to_value()),
- )
+ Normalized::from_nir(Nir::from_builtin(Builtin::List).app(t.to_nir()))
}
pub fn make_record_type(
kts: impl Iterator<Item = (String, Normalized)>,
) -> Self {
- Normalized::from_kind(ValueKind::RecordType(
- kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+ Normalized::from_kind(NirKind::RecordType(
+ kts.map(|(k, t)| (k.into(), t.into_nir())).collect(),
))
}
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Normalized>)>,
) -> Self {
- Normalized::from_kind(ValueKind::UnionType(
- kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+ Normalized::from_kind(NirKind::UnionType(
+ kts.map(|(k, t)| (k.into(), t.map(|t| t.into_nir())))
.collect(),
))
}
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 752b25c..61de0c7 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
use crate::semantics::{
- skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv,
+ skip_resolve, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv,
};
use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
@@ -15,14 +15,14 @@ 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<Value> {
+pub(crate) struct BuiltinClosure<Nir> {
pub env: NzEnv,
pub b: Builtin,
/// Arguments applied to the closure so far.
- pub args: Vec<Value>,
+ pub args: Vec<Nir>,
}
-impl BuiltinClosure<Value> {
+impl BuiltinClosure<Nir> {
pub fn new(b: Builtin, env: NzEnv) -> Self {
BuiltinClosure {
env,
@@ -31,7 +31,7 @@ impl BuiltinClosure<Value> {
}
}
- pub fn apply(&self, a: Value) -> ValueKind {
+ pub fn apply(&self, a: Nir) -> NirKind {
use std::iter::once;
let args = self.args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(self.b, args, self.env.clone())
@@ -256,14 +256,14 @@ macro_rules! make_closure {
}
#[allow(clippy::cognitive_complexity)]
-fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
+fn apply_builtin(b: Builtin, args: Vec<Nir>, env: NzEnv) -> NirKind {
use LitKind::{Bool, Double, Integer, Natural};
- use ValueKind::*;
+ use NirKind::*;
// Small helper enum
enum Ret {
- ValueKind(ValueKind),
- Value(Value),
+ NirKind(NirKind),
+ Nir(Nir),
DoneAsIs,
}
let make_closure = |e| {
@@ -274,35 +274,35 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let ret = match (b, args.as_slice()) {
(Builtin::OptionalNone, [t]) => {
- Ret::ValueKind(EmptyOptionalLit(t.clone()))
+ Ret::NirKind(EmptyOptionalLit(t.clone()))
}
(Builtin::NaturalIsZero, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))),
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalEven, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))),
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalOdd, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))),
+ Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalToInteger, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))),
+ Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))),
_ => Ret::DoneAsIs,
},
(Builtin::NaturalShow, [n]) => match &*n.kind() {
- Lit(Natural(n)) => Ret::Value(Value::from_text(n)),
+ Lit(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::ValueKind(Lit(Natural(if b > a { b - a } else { 0 })))
+ Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 })))
}
- (Lit(Natural(0)), _) => Ret::Value(b.clone()),
- (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))),
- _ if a == b => Ret::ValueKind(Lit(Natural(0))),
+ (Lit(Natural(0)), _) => Ret::Nir(b.clone()),
+ (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))),
+ _ if a == b => Ret::NirKind(Lit(Natural(0))),
_ => Ret::DoneAsIs,
},
(Builtin::IntegerShow, [n]) => match &*n.kind() {
@@ -312,28 +312,28 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
} else {
format!("+{}", n)
};
- Ret::Value(Value::from_text(s))
+ Ret::Nir(Nir::from_text(s))
}
_ => Ret::DoneAsIs,
},
(Builtin::IntegerToDouble, [n]) => match &*n.kind() {
Lit(Integer(n)) => {
- Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64))))
+ Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64))))
}
_ => Ret::DoneAsIs,
},
(Builtin::IntegerNegate, [n]) => match &*n.kind() {
- Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))),
+ Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))),
_ => Ret::DoneAsIs,
},
(Builtin::IntegerClamp, [n]) => match &*n.kind() {
Lit(Integer(n)) => {
- Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0))))
+ Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0))))
}
_ => Ret::DoneAsIs,
},
(Builtin::DoubleShow, [n]) => match &*n.kind() {
- Lit(Double(n)) => Ret::Value(Value::from_text(n)),
+ Lit(Double(n)) => Ret::Nir(Nir::from_text(n)),
_ => Ret::DoneAsIs,
},
(Builtin::TextShow, [v]) => match &*v.kind() {
@@ -343,7 +343,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let txt: InterpolatedText<Normalized> =
std::iter::once(InterpolatedTextContents::Text(s))
.collect();
- Ret::Value(Value::from_text(txt))
+ Ret::Nir(Nir::from_text(txt))
} else {
Ret::DoneAsIs
}
@@ -351,28 +351,28 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
_ => Ret::DoneAsIs,
},
(Builtin::ListLength, [_, l]) => match &*l.kind() {
- EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))),
- NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))),
+ EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))),
+ NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))),
_ => Ret::DoneAsIs,
},
(Builtin::ListHead, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
+ EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
+ Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
}
_ => Ret::DoneAsIs,
},
(Builtin::ListLast, [_, l]) => match &*l.kind() {
- EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
- NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
+ 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::ValueKind(EmptyListLit(n.clone())),
+ EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())),
NEListLit(xs) => {
- Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
+ Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect()))
}
_ => Ret::DoneAsIs,
},
@@ -383,10 +383,10 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let mut kts = HashMap::new();
kts.insert(
"index".into(),
- Value::from_builtin(Builtin::Natural),
+ Nir::from_builtin(Builtin::Natural),
);
kts.insert("value".into(), t.clone());
- let t = Value::from_kind(RecordType(kts));
+ let t = Nir::from_kind(RecordType(kts));
// Construct the new list, with added indices
let list = match l.kind() {
@@ -398,23 +398,23 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_kind(Lit(Natural(i))),
+ Nir::from_kind(Lit(Natural(i))),
);
kvs.insert("value".into(), e.clone());
- Value::from_kind(RecordLit(kvs))
+ Nir::from_kind(RecordLit(kvs))
})
.collect(),
),
_ => unreachable!(),
};
- Ret::ValueKind(list)
+ Ret::NirKind(list)
}
_ => Ret::DoneAsIs,
}
}
(Builtin::ListBuild, [t, f]) => {
- let list_t = Value::from_builtin(Builtin::List).app(t.clone());
- Ret::Value(
+ let list_t = Nir::from_builtin(Builtin::List).app(t.clone());
+ Ret::Nir(
f.app(list_t.clone())
.app(
make_closure(make_closure!(
@@ -425,24 +425,24 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
))
.app(t.clone()),
)
- .app(EmptyListLit(t.clone()).into_value()),
+ .app(EmptyListLit(t.clone()).into_nir()),
)
}
(Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
- EmptyListLit(_) => Ret::Value(nil.clone()),
+ 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::Value(v)
+ Ret::Nir(v)
}
_ => Ret::DoneAsIs,
},
(Builtin::OptionalBuild, [t, f]) => {
let optional_t =
- Value::from_builtin(Builtin::Optional).app(t.clone());
- Ret::Value(
+ Nir::from_builtin(Builtin::Optional).app(t.clone());
+ Ret::Nir(
f.app(optional_t.clone())
.app(
make_closure(make_closure!(
@@ -452,47 +452,47 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
))
.app(t.clone()),
)
- .app(EmptyOptionalLit(t.clone()).into_value()),
+ .app(EmptyOptionalLit(t.clone()).into_nir()),
)
}
(Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
- EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
- NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
+ EmptyOptionalLit(_) => Ret::Nir(nothing.clone()),
+ NEOptionalLit(x) => Ret::Nir(just.app(x.clone())),
_ => Ret::DoneAsIs,
},
- (Builtin::NaturalBuild, [f]) => Ret::Value(
- f.app(Value::from_builtin(Builtin::Natural))
+ (Builtin::NaturalBuild, [f]) => Ret::Nir(
+ f.app(Nir::from_builtin(Builtin::Natural))
.app(make_closure(make_closure!(
λ(x : Natural) ->
1 + var(x)
)))
- .app(Lit(Natural(0)).into_value()),
+ .app(Lit(Natural(0)).into_nir()),
),
(Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
- Lit(Natural(0)) => Ret::Value(zero.clone()),
+ Lit(Natural(0)) => Ret::Nir(zero.clone()),
Lit(Natural(n)) => {
- let fold = Value::from_builtin(Builtin::NaturalFold)
- .app(Lit(Natural(n - 1)).into_value())
+ let fold = Nir::from_builtin(Builtin::NaturalFold)
+ .app(Lit(Natural(n - 1)).into_nir())
.app(t.clone())
.app(succ.clone())
.app(zero.clone());
- Ret::Value(succ.app(fold))
+ Ret::Nir(succ.app(fold))
}
_ => Ret::DoneAsIs,
},
_ => Ret::DoneAsIs,
};
match ret {
- Ret::ValueKind(v) => v,
- Ret::Value(v) => v.kind().clone(),
+ Ret::NirKind(v) => v,
+ Ret::Nir(v) => v.kind().clone(),
Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }),
}
}
-impl<Value: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Value> {
+impl<Nir: std::cmp::PartialEq> std::cmp::PartialEq for BuiltinClosure<Nir> {
fn eq(&self, other: &Self) -> bool {
self.b == other.b && self.args == other.args
}
}
-impl<Value: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Value> {}
+impl<Nir: std::cmp::Eq> std::cmp::Eq for BuiltinClosure<Nir> {}
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 241af40..55050ed 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Nir, NirKind};
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum NzVar {
@@ -13,7 +13,7 @@ enum EnvItem<Type> {
// Variable is bound with given type
Kept(Type),
// Variable has been replaced by corresponding value
- Replaced(Value, Type),
+ Replaced(Nir, Type),
}
#[derive(Debug, Clone)]
@@ -67,15 +67,15 @@ impl<Type: Clone> ValEnv<Type> {
env.items.push(EnvItem::Kept(ty));
env
}
- pub fn insert_value(&self, e: Value, ty: Type) -> Self {
+ pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
let mut env = self.clone();
env.items.push(EnvItem::Replaced(e, ty));
env
}
- pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+ pub fn lookup_val(&self, var: &AlphaVar) -> NirKind {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- EnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+ EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
EnvItem::Replaced(x, _) => x.kind().clone(),
}
}
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
index 2c8d907..2648339 100644
--- a/dhall/src/semantics/nze/mod.rs
+++ b/dhall/src/semantics/nze/mod.rs
@@ -1,9 +1,9 @@
pub mod env;
pub mod lazy;
+pub mod nir;
pub mod normalize;
-pub mod value;
pub mod var;
pub(crate) use env::*;
+pub(crate) use nir::*;
pub(crate) use normalize::*;
-pub(crate) use value::*;
pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/nir.rs
index 7084af6..a6dafa2 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -14,15 +14,16 @@ use crate::{NormalizedExpr, ToExprOptions};
/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
/// automatically. Uses a Rc<RefCell> to share computation.
-/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
+/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence
/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
/// normalize as needed.
+/// Stands for "Normalized intermediate representation"
#[derive(Clone)]
-pub(crate) struct Value(Rc<ValueInternal>);
+pub(crate) struct Nir(Rc<NirInternal>);
#[derive(Debug)]
-struct ValueInternal {
- kind: lazy::Lazy<Thunk, ValueKind>,
+struct NirInternal {
+ kind: lazy::Lazy<Thunk, NirKind>,
span: Span,
}
@@ -32,7 +33,7 @@ pub(crate) enum Thunk {
/// A completely unnormalized expression.
Thunk { env: NzEnv, body: Hir },
/// A partially normalized expression that may need to go through `normalize_one_layer`.
- PartialExpr { env: NzEnv, expr: ExprKind<Value> },
+ PartialExpr { env: NzEnv, expr: ExprKind<Nir> },
}
/// An unevaluated subexpression that takes an argument.
@@ -41,101 +42,99 @@ pub(crate) enum Closure {
/// Normal closure
Closure { env: NzEnv, body: Hir },
/// Closure that ignores the argument passed
- ConstantClosure { body: Value },
+ ConstantClosure { body: Nir },
}
/// A text literal with interpolations.
// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
// text values must be merged.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>);
/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
/// normalized up to the first constructor, but subexpressions may not be fully normalized.
-/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// When all the Nirs in a NirKind are in WHNF, and recursively so, then the NirKind is in
/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
/// if we have the first constructor of the NF at all levels, we actually have the NF.
-/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
-/// we only need to recursively normalize its sub-`Value`s to get to the NF.
+/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Nir`s to get to the NF.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
+pub(crate) enum NirKind {
/// Closures
LamClosure {
binder: Binder,
- annot: Value,
+ annot: Nir,
closure: Closure,
},
PiClosure {
binder: Binder,
- annot: Value,
+ annot: Nir,
closure: Closure,
},
- AppliedBuiltin(BuiltinClosure<Value>),
+ AppliedBuiltin(BuiltinClosure<Nir>),
Var(NzVar),
Const(Const),
Lit(LitKind),
- EmptyOptionalLit(Value),
- NEOptionalLit(Value),
+ EmptyOptionalLit(Nir),
+ NEOptionalLit(Nir),
// EmptyListLit(t) means `[] : List t`, not `[] : t`
- EmptyListLit(Value),
- NEListLit(Vec<Value>),
- RecordType(HashMap<Label, Value>),
- RecordLit(HashMap<Label, Value>),
- UnionType(HashMap<Label, Option<Value>>),
- UnionConstructor(Label, HashMap<Label, Option<Value>>),
- UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+ EmptyListLit(Nir),
+ NEListLit(Vec<Nir>),
+ RecordType(HashMap<Label, Nir>),
+ RecordLit(HashMap<Label, Nir>),
+ UnionType(HashMap<Label, Option<Nir>>),
+ UnionConstructor(Label, HashMap<Label, Option<Nir>>),
+ UnionLit(Label, Nir, HashMap<Label, Option<Nir>>),
TextLit(TextLit),
- Equivalence(Value, Value),
+ Equivalence(Nir, Nir),
/// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
- PartialExpr(ExprKind<Value>),
+ PartialExpr(ExprKind<Nir>),
}
-impl Value {
- /// Construct a Value from a completely unnormalized expression.
- pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value {
+impl Nir {
+ /// Construct a Nir from a completely unnormalized expression.
+ pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
let span = hir.span();
- ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
+ NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir()
}
- /// Construct a Value from a partially normalized expression that's not in WHNF.
- pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value {
+ /// Construct a Nir from a partially normalized expression that's not in WHNF.
+ pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
// TODO: env
let env = NzEnv::new();
- ValueInternal::from_thunk(
+ NirInternal::from_thunk(
Thunk::from_partial_expr(env, e),
Span::Artificial,
)
- .into_value()
+ .into_nir()
}
- /// Make a Value from a ValueKind
- pub(crate) fn from_kind(v: ValueKind) -> Value {
- ValueInternal::from_whnf(v, Span::Artificial).into_value()
+ /// Make a Nir from a NirKind
+ pub(crate) fn from_kind(v: NirKind) -> Nir {
+ NirInternal::from_whnf(v, Span::Artificial).into_nir()
}
pub(crate) fn from_const(c: Const) -> Self {
- let v = ValueKind::Const(c);
- ValueInternal::from_whnf(v, Span::Artificial).into_value()
+ let v = NirKind::Const(c);
+ NirInternal::from_whnf(v, Span::Artificial).into_nir()
}
pub(crate) fn from_builtin(b: Builtin) -> Self {
Self::from_builtin_env(b, &NzEnv::new())
}
pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
- Value::from_kind(ValueKind::from_builtin_env(b, env.clone()))
+ Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
}
pub(crate) fn from_text(txt: impl ToString) -> Self {
- Value::from_kind(ValueKind::TextLit(TextLit::from_text(
- txt.to_string(),
- )))
+ Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
}
pub(crate) fn as_const(&self) -> Option<Const> {
match &*self.kind() {
- ValueKind::Const(c) => Some(*c),
+ NirKind::Const(c) => Some(*c),
_ => None,
}
}
/// This is what you want if you want to pattern-match on the value.
- pub(crate) fn kind(&self) -> &ValueKind {
+ pub(crate) fn kind(&self) -> &NirKind {
self.0.kind()
}
@@ -157,12 +156,12 @@ impl Value {
self.0.normalize()
}
- pub(crate) fn app(&self, v: Value) -> Value {
- Value::from_kind(apply_any(self.clone(), v))
+ pub(crate) fn app(&self, v: Nir) -> Nir {
+ Nir::from_kind(apply_any(self.clone(), v))
}
pub fn to_hir(&self, venv: VarEnv) -> Hir {
- let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
+ let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| {
ExprKind::UnionType(
kts.iter()
.map(|(k, v)| {
@@ -173,13 +172,13 @@ impl Value {
};
let hir = match &*self.kind() {
- ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
- ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+ NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+ NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
self_kind => HirKind::Expr(match self_kind {
- ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
+ NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
unreachable!()
}
- ValueKind::LamClosure {
+ NirKind::LamClosure {
binder,
annot,
closure,
@@ -188,7 +187,7 @@ impl Value {
annot.to_hir(venv),
closure.to_hir(venv),
),
- ValueKind::PiClosure {
+ NirKind::PiClosure {
binder,
annot,
closure,
@@ -197,49 +196,47 @@ impl Value {
annot.to_hir(venv),
closure.to_hir(venv),
),
- ValueKind::Const(c) => ExprKind::Const(*c),
- ValueKind::Lit(l) => ExprKind::Lit(l.clone()),
- ValueKind::EmptyOptionalLit(n) => ExprKind::App(
- Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
+ NirKind::Const(c) => ExprKind::Const(*c),
+ NirKind::Lit(l) => ExprKind::Lit(l.clone()),
+ NirKind::EmptyOptionalLit(n) => ExprKind::App(
+ Nir::from_builtin(Builtin::OptionalNone).to_hir(venv),
n.to_hir(venv),
),
- ValueKind::NEOptionalLit(n) => {
- ExprKind::SomeLit(n.to_hir(venv))
- }
- ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+ NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+ NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
HirKind::Expr(ExprKind::App(
- Value::from_builtin(Builtin::List).to_hir(venv),
+ Nir::from_builtin(Builtin::List).to_hir(venv),
n.to_hir(venv),
)),
Span::Artificial,
)),
- ValueKind::NEListLit(elts) => ExprKind::NEListLit(
+ NirKind::NEListLit(elts) => ExprKind::NEListLit(
elts.iter().map(|v| v.to_hir(venv)).collect(),
),
- ValueKind::TextLit(elts) => ExprKind::TextLit(
+ NirKind::TextLit(elts) => ExprKind::TextLit(
elts.iter()
.map(|t| t.map_ref(|v| v.to_hir(venv)))
.collect(),
),
- ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
+ NirKind::RecordLit(kvs) => ExprKind::RecordLit(
kvs.iter()
.map(|(k, v)| (k.clone(), v.to_hir(venv)))
.collect(),
),
- ValueKind::RecordType(kts) => ExprKind::RecordType(
+ NirKind::RecordType(kts) => ExprKind::RecordType(
kts.iter()
.map(|(k, v)| (k.clone(), v.to_hir(venv)))
.collect(),
),
- ValueKind::UnionType(kts) => map_uniontype(kts),
- ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
+ NirKind::UnionType(kts) => map_uniontype(kts),
+ NirKind::UnionConstructor(l, kts) => ExprKind::Field(
Hir::new(
HirKind::Expr(map_uniontype(kts)),
Span::Artificial,
),
l.clone(),
),
- ValueKind::UnionLit(l, v, kts) => ExprKind::App(
+ NirKind::UnionLit(l, v, kts) => ExprKind::App(
Hir::new(
HirKind::Expr(ExprKind::Field(
Hir::new(
@@ -252,12 +249,12 @@ impl Value {
),
v.to_hir(venv),
),
- ValueKind::Equivalence(x, y) => ExprKind::BinOp(
+ NirKind::Equivalence(x, y) => ExprKind::BinOp(
BinOp::Equivalence,
x.to_hir(venv),
y.to_hir(venv),
),
- ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+ NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
}),
};
@@ -268,24 +265,24 @@ impl Value {
}
}
-impl ValueInternal {
- fn from_whnf(k: ValueKind, span: Span) -> Self {
- ValueInternal {
+impl NirInternal {
+ fn from_whnf(k: NirKind, span: Span) -> Self {
+ NirInternal {
kind: lazy::Lazy::new_completed(k),
span,
}
}
fn from_thunk(th: Thunk, span: Span) -> Self {
- ValueInternal {
+ NirInternal {
kind: lazy::Lazy::new(th),
span,
}
}
- fn into_value(self) -> Value {
- Value(Rc::new(self))
+ fn into_nir(self) -> Nir {
+ Nir(Rc::new(self))
}
- fn kind(&self) -> &ValueKind {
+ fn kind(&self) -> &NirKind {
&self.kind
}
fn normalize(&self) {
@@ -293,70 +290,70 @@ impl ValueInternal {
}
}
-impl ValueKind {
- pub(crate) fn into_value(self) -> Value {
- Value::from_kind(self)
+impl NirKind {
+ pub(crate) fn into_nir(self) -> Nir {
+ Nir::from_kind(self)
}
pub(crate) fn normalize(&self) {
match self {
- ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {}
+ NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
- ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+ NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
tth.normalize();
}
- ValueKind::NEOptionalLit(th) => {
+ NirKind::NEOptionalLit(th) => {
th.normalize();
}
- ValueKind::LamClosure { annot, closure, .. }
- | ValueKind::PiClosure { annot, closure, .. } => {
+ NirKind::LamClosure { annot, closure, .. }
+ | NirKind::PiClosure { annot, closure, .. } => {
annot.normalize();
closure.normalize();
}
- ValueKind::AppliedBuiltin(closure) => closure.normalize(),
- ValueKind::NEListLit(elts) => {
+ NirKind::AppliedBuiltin(closure) => closure.normalize(),
+ NirKind::NEListLit(elts) => {
for x in elts.iter() {
x.normalize();
}
}
- ValueKind::RecordLit(kvs) => {
+ NirKind::RecordLit(kvs) => {
for x in kvs.values() {
x.normalize();
}
}
- ValueKind::RecordType(kvs) => {
+ NirKind::RecordType(kvs) => {
for x in kvs.values() {
x.normalize();
}
}
- ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+ NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
for x in kts.values().flat_map(|opt| opt) {
x.normalize();
}
}
- ValueKind::UnionLit(_, v, kts) => {
+ NirKind::UnionLit(_, v, kts) => {
v.normalize();
for x in kts.values().flat_map(|opt| opt) {
x.normalize();
}
}
- ValueKind::TextLit(tlit) => tlit.normalize(),
- ValueKind::Equivalence(x, y) => {
+ NirKind::TextLit(tlit) => tlit.normalize(),
+ NirKind::Equivalence(x, y) => {
x.normalize();
y.normalize();
}
- ValueKind::PartialExpr(e) => {
- e.map_ref(Value::normalize);
+ NirKind::PartialExpr(e) => {
+ e.map_ref(Nir::normalize);
}
}
}
- pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
- ValueKind::from_builtin_env(b, NzEnv::new())
+ pub(crate) fn from_builtin(b: Builtin) -> NirKind {
+ NirKind::from_builtin_env(b, NzEnv::new())
}
- pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
- ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind {
+ NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
}
}
@@ -364,10 +361,10 @@ impl Thunk {
fn new(env: NzEnv, body: Hir) -> Self {
Thunk::Thunk { env, body }
}
- fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self {
+ fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
Thunk::PartialExpr { env, expr }
}
- fn eval(self) -> ValueKind {
+ fn eval(self) -> NirKind {
match self {
Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
@@ -383,11 +380,11 @@ impl Closure {
}
}
/// New closure that ignores its argument
- pub fn new_constant(body: Value) -> Self {
+ pub fn new_constant(body: Nir) -> Self {
Closure::ConstantClosure { body }
}
- pub fn apply(&self, val: Value) -> Value {
+ pub fn apply(&self, val: Nir) -> Nir {
match self {
Closure::Closure { env, body, .. } => {
body.eval(env.insert_value(val, ()))
@@ -395,10 +392,10 @@ impl Closure {
Closure::ConstantClosure { body, .. } => body.clone(),
}
}
- fn apply_var(&self, var: NzVar) -> Value {
+ fn apply_var(&self, var: NzVar) -> Nir {
match self {
Closure::Closure { .. } => {
- self.apply(Value::from_kind(ValueKind::Var(var)))
+ self.apply(Nir::from_kind(NirKind::Var(var)))
}
Closure::ConstantClosure { body, .. } => body.clone(),
}
@@ -414,7 +411,7 @@ impl Closure {
}
/// If the closure variable is free in the closure, return Err. Otherwise, return the value
/// with that free variable remove.
- pub fn remove_binder(&self) -> Result<Value, ()> {
+ pub fn remove_binder(&self) -> Result<Nir, ()> {
match self {
Closure::Closure { .. } => {
let v = NzVar::fresh();
@@ -429,11 +426,11 @@ impl Closure {
impl TextLit {
pub fn new(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
) -> Self {
TextLit(squash_textlit(elts))
}
- pub fn interpolate(v: Value) -> TextLit {
+ pub fn interpolate(v: Nir) -> TextLit {
TextLit(vec![InterpolatedTextContents::Expr(v)])
}
pub fn from_text(s: String) -> TextLit {
@@ -448,7 +445,7 @@ impl TextLit {
}
/// If the literal consists of only one interpolation and not text, return the interpolated
/// value.
- pub fn as_single_expr(&self) -> Option<&Value> {
+ pub fn as_single_expr(&self) -> Option<&Nir> {
use InterpolatedTextContents::Expr;
if let [Expr(v)] = self.0.as_slice() {
Some(v)
@@ -467,33 +464,31 @@ impl TextLit {
None
}
}
- pub fn iter(
- &self,
- ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
+ pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> {
self.0.iter()
}
/// Normalize the contained values. This does not break the invariant because we have already
/// ensured that no contained values normalize to a TextLit.
pub fn normalize(&self) {
for x in self.0.iter() {
- x.map_ref(Value::normalize);
+ x.map_ref(Nir::normalize);
}
}
}
-impl lazy::Eval<ValueKind> for Thunk {
- fn eval(self) -> ValueKind {
+impl lazy::Eval<NirKind> for Thunk {
+ fn eval(self) -> NirKind {
self.eval()
}
}
/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
+impl std::cmp::PartialEq for Nir {
fn eq(&self, other: &Self) -> bool {
Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
}
}
-impl std::cmp::Eq for Value {}
+impl std::cmp::Eq for Nir {}
impl std::cmp::PartialEq for Thunk {
fn eq(&self, _other: &Self) -> bool {
@@ -512,14 +507,14 @@ impl std::cmp::PartialEq for Closure {
}
impl std::cmp::Eq for Closure {}
-impl std::fmt::Debug for Value {
+impl std::fmt::Debug for Nir {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let vint: &ValueInternal = &self.0;
+ let vint: &NirInternal = &self.0;
let kind = vint.kind();
- if let ValueKind::Const(c) = kind {
+ if let NirKind::Const(c) = kind {
return write!(fmt, "{:?}", c);
}
- let mut x = fmt.debug_struct(&format!("Value@WHNF"));
+ let mut x = fmt.debug_struct(&format!("Nir@WHNF"));
x.field("kind", kind);
x.finish()
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c2d2dc2..4c2aa33 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,41 +3,39 @@ use std::collections::HashMap;
use crate::semantics::NzEnv;
use crate::semantics::{
- Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
+ Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
};
use crate::syntax::{
BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
};
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
+pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
match f.kind() {
- ValueKind::LamClosure { closure, .. } => {
- closure.apply(a).kind().clone()
+ NirKind::LamClosure { closure, .. } => closure.apply(a).kind().clone(),
+ NirKind::AppliedBuiltin(closure) => closure.apply(a),
+ NirKind::UnionConstructor(l, kts) => {
+ NirKind::UnionLit(l.clone(), a, kts.clone())
}
- ValueKind::AppliedBuiltin(closure) => closure.apply(a),
- ValueKind::UnionConstructor(l, kts) => {
- ValueKind::UnionLit(l.clone(), a, kts.clone())
- }
- _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
+ _ => NirKind::PartialExpr(ExprKind::App(f, a)),
}
}
pub(crate) fn squash_textlit(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
-) -> Vec<InterpolatedTextContents<Value>> {
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+) -> Vec<InterpolatedTextContents<Nir>> {
use std::mem::replace;
use InterpolatedTextContents::{Expr, Text};
fn inner(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
crnt_str: &mut String,
- ret: &mut Vec<InterpolatedTextContents<Value>>,
+ ret: &mut Vec<InterpolatedTextContents<Nir>>,
) {
for contents in elts {
match contents {
Text(s) => crnt_str.push_str(&s),
Expr(e) => match e.kind() {
- ValueKind::TextLit(elts2) => {
+ NirKind::TextLit(elts2) => {
inner(elts2.iter().cloned(), crnt_str, ret)
}
_ => {
@@ -88,85 +86,77 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueKind(ValueKind),
- Value(Value),
- ValueRef(&'a Value),
- Expr(ExprKind<Value>),
+ NirKind(NirKind),
+ Nir(Nir),
+ NirRef(&'a Nir),
+ Expr(ExprKind<Nir>),
}
-fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
RightBiasedRecordMerge, TextAppend,
};
use LitKind::{Bool, Natural};
- use ValueKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
+ use NirKind::{EmptyListLit, Lit, NEListLit, RecordLit, RecordType};
Some(match (o, x.kind(), y.kind()) {
- (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, 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, 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))),
+ (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, _, _) 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, _, _) 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))),
- (NaturalPlus, Lit(Natural(0)), _) => Ret::ValueRef(y),
- (NaturalPlus, _, Lit(Natural(0))) => Ret::ValueRef(x),
+ (NaturalPlus, Lit(Natural(0)), _) => Ret::NirRef(y),
+ (NaturalPlus, _, Lit(Natural(0))) => Ret::NirRef(x),
(NaturalPlus, Lit(Natural(x)), Lit(Natural(y))) => {
- Ret::ValueKind(Lit(Natural(x + y)))
+ Ret::NirKind(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(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::ValueKind(Lit(Natural(x * y)))
+ Ret::NirKind(Lit(Natural(x * y)))
}
- (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
- (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
- (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
- NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
- ),
+ (ListAppend, EmptyListLit(_), _) => Ret::NirRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::NirRef(x),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::NirKind(NEListLit(
+ xs.iter().chain(ys.iter()).cloned().collect(),
+ )),
- (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
- Ret::ValueRef(y)
- }
- (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
- Ret::ValueRef(x)
- }
- (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
- Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
- }
- (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
- ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
- ),
- (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
- ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
- ),
+ (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => Ret::NirRef(y),
+ (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => Ret::NirRef(x),
+ (TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
+ Ret::NirKind(NirKind::TextLit(x.concat(y)))
+ }
+ (TextAppend, NirKind::TextLit(x), _) => Ret::NirKind(NirKind::TextLit(
+ x.concat(&TextLit::interpolate(y.clone())),
+ )),
+ (TextAppend, _, NirKind::TextLit(y)) => Ret::NirKind(NirKind::TextLit(
+ TextLit::interpolate(x.clone()).concat(y),
+ )),
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
+ Ret::NirRef(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
+ Ret::NirRef(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -174,25 +164,25 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
// Insert only if key not already present
kvs.entry(x.clone()).or_insert_with(|| v.clone());
}
- Ret::ValueKind(RecordLit(kvs))
+ Ret::NirKind(RecordLit(kvs))
}
- (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
+ (RightBiasedRecordMerge, _, _) if x == y => Ret::NirRef(y),
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ValueRef(x)
+ Ret::NirRef(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ValueRef(y)
+ Ret::NirRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
- Ok(Value::from_partial_expr(ExprKind::BinOp(
+ Ok(Nir::from_partial_expr(ExprKind::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
)))
})?;
- Ret::ValueKind(RecordLit(kvs))
+ Ret::NirKind(RecordLit(kvs))
}
(RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
@@ -200,31 +190,28 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
kts_x,
kts_y,
// If the Label exists for both records, then we hit the recursive case.
- |_, l: &Value, r: &Value| {
- Ok(Value::from_partial_expr(ExprKind::BinOp(
+ |_, l: &Nir, r: &Nir| {
+ Ok(Nir::from_partial_expr(ExprKind::BinOp(
RecursiveRecordTypeMerge,
l.clone(),
r.clone(),
)))
},
)?;
- Ret::ValueKind(RecordType(kts))
+ Ret::NirKind(RecordType(kts))
}
(Equivalence, _, _) => {
- Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+ Ret::NirKind(NirKind::Equivalence(x.clone(), y.clone()))
}
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(
- expr: ExprKind<Value>,
- env: &NzEnv,
-) -> ValueKind {
+pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
use LitKind::Bool;
- use ValueKind::{
+ use NirKind::{
EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
UnionType,
@@ -241,54 +228,54 @@ pub(crate) fn normalize_one_layer(
"This case should have been handled in normalize_hir_whnf"
),
- ExprKind::Annot(x, _) => Ret::Value(x),
- ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
- ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+ ExprKind::Annot(x, _) => Ret::Nir(x),
+ ExprKind::Const(c) => Ret::Nir(Nir::from_const(c)),
+ ExprKind::Builtin(b) => Ret::Nir(Nir::from_builtin_env(b, env)),
ExprKind::Assert(_) => Ret::Expr(expr),
- ExprKind::App(v, a) => Ret::Value(v.app(a)),
- ExprKind::Lit(l) => Ret::ValueKind(Lit(l.clone())),
- ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+ ExprKind::App(v, a) => Ret::Nir(v.app(a)),
+ ExprKind::Lit(l) => Ret::NirKind(Lit(l.clone())),
+ ExprKind::SomeLit(e) => Ret::NirKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
let arg = match t.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
}) if args.len() == 1 => args[0].clone(),
_ => panic!("internal type error"),
};
- Ret::ValueKind(ValueKind::EmptyListLit(arg))
+ Ret::NirKind(NirKind::EmptyListLit(arg))
}
ExprKind::NEListLit(elts) => {
- Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+ Ret::NirKind(NEListLit(elts.into_iter().collect()))
}
ExprKind::RecordLit(kvs) => {
- Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+ Ret::NirKind(RecordLit(kvs.into_iter().collect()))
}
ExprKind::RecordType(kvs) => {
- Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+ Ret::NirKind(RecordType(kvs.into_iter().collect()))
}
ExprKind::UnionType(kvs) => {
- Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+ Ret::NirKind(UnionType(kvs.into_iter().collect()))
}
ExprKind::TextLit(elts) => {
let tlit = TextLit::new(elts.into_iter());
// Simplify bare interpolation
if let Some(v) = tlit.as_single_expr() {
- Ret::Value(v.clone())
+ Ret::Nir(v.clone())
} else {
- Ret::ValueKind(ValueKind::TextLit(tlit))
+ Ret::NirKind(NirKind::TextLit(tlit))
}
}
ExprKind::BoolIf(ref b, ref e1, ref e2) => {
match b.kind() {
- Lit(Bool(true)) => Ret::ValueRef(e1),
- Lit(Bool(false)) => Ret::ValueRef(e2),
+ Lit(Bool(true)) => Ret::NirRef(e1),
+ Lit(Bool(false)) => Ret::NirRef(e2),
_ => {
match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
- (Lit(Bool(true)), Lit(Bool(false))) => Ret::ValueRef(b),
- _ if e1 == e2 => Ret::ValueRef(e1),
+ (Lit(Bool(true)), Lit(Bool(false))) => Ret::NirRef(b),
+ _ if e1 == e2 => Ret::NirRef(e1),
_ => Ret::Expr(expr),
}
}
@@ -300,10 +287,10 @@ pub(crate) fn normalize_one_layer(
},
ExprKind::Projection(_, ref ls) if ls.is_empty() => {
- Ret::ValueKind(RecordLit(HashMap::new()))
+ Ret::NirKind(RecordLit(HashMap::new()))
}
ExprKind::Projection(ref v, ref ls) => match v.kind() {
- RecordLit(kvs) => Ret::ValueKind(RecordLit(
+ RecordLit(kvs) => Ret::NirKind(RecordLit(
ls.iter()
.filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
.collect(),
@@ -318,11 +305,11 @@ pub(crate) fn normalize_one_layer(
},
ExprKind::Field(ref v, ref l) => match v.kind() {
RecordLit(kvs) => match kvs.get(l) {
- Some(r) => Ret::Value(r.clone()),
+ Some(r) => Ret::Nir(r.clone()),
None => Ret::Expr(expr),
},
UnionType(kts) => {
- Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
+ Ret::NirKind(UnionConstructor(l.clone(), kts.clone()))
}
PartialExpr(ExprKind::BinOp(
BinOp::RightBiasedRecordMerge,
@@ -330,7 +317,7 @@ pub(crate) fn normalize_one_layer(
y,
)) => match (x.kind(), y.kind()) {
(_, RecordLit(kvs)) => match kvs.get(l) {
- Some(r) => Ret::Value(r.clone()),
+ Some(r) => Ret::Nir(r.clone()),
None => {
return normalize_one_layer(
ExprKind::Field(x.clone(), l.clone()),
@@ -340,9 +327,9 @@ pub(crate) fn normalize_one_layer(
},
(RecordLit(kvs), _) => match kvs.get(l) {
Some(r) => Ret::Expr(ExprKind::Field(
- Value::from_kind(PartialExpr(ExprKind::BinOp(
+ Nir::from_kind(PartialExpr(ExprKind::BinOp(
BinOp::RightBiasedRecordMerge,
- Value::from_kind(RecordLit({
+ Nir::from_kind(RecordLit({
let mut kvs = HashMap::new();
kvs.insert(l.clone(), r.clone());
kvs
@@ -395,19 +382,19 @@ pub(crate) fn normalize_one_layer(
match handlers.kind() {
RecordLit(kvs) => match variant.kind() {
UnionConstructor(l, _) => match kvs.get(l) {
- Some(h) => Ret::Value(h.clone()),
+ Some(h) => Ret::Nir(h.clone()),
None => Ret::Expr(expr),
},
UnionLit(l, v, _) => match kvs.get(l) {
- Some(h) => Ret::Value(h.app(v.clone())),
+ Some(h) => Ret::Nir(h.app(v.clone())),
None => Ret::Expr(expr),
},
EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
- Some(h) => Ret::Value(h.clone()),
+ Some(h) => Ret::Nir(h.clone()),
None => Ret::Expr(expr),
},
NEOptionalLit(v) => match kvs.get(&"Some".into()) {
- Some(h) => Ret::Value(h.app(v.clone())),
+ Some(h) => Ret::Nir(h.app(v.clone())),
None => Ret::Expr(expr),
},
_ => Ret::Expr(expr),
@@ -418,24 +405,24 @@ pub(crate) fn normalize_one_layer(
ExprKind::ToMap(ref v, ref annot) => match v.kind() {
RecordLit(kvs) if kvs.is_empty() => {
match annot.as_ref().map(|v| v.kind()) {
- Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+ Some(NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
})) if args.len() == 1 => {
- Ret::ValueKind(EmptyListLit(args[0].clone()))
+ Ret::NirKind(EmptyListLit(args[0].clone()))
}
_ => Ret::Expr(expr),
}
}
- RecordLit(kvs) => Ret::ValueKind(NEListLit(
+ RecordLit(kvs) => Ret::NirKind(NEListLit(
kvs.iter()
.sorted_by_key(|(k, _)| k.clone())
.map(|(k, v)| {
let mut rec = HashMap::new();
- rec.insert("mapKey".into(), Value::from_text(k));
+ rec.insert("mapKey".into(), Nir::from_text(k));
rec.insert("mapValue".into(), v.clone());
- Value::from_kind(ValueKind::RecordLit(rec))
+ Nir::from_kind(NirKind::RecordLit(rec))
})
.collect(),
)),
@@ -444,20 +431,20 @@ pub(crate) fn normalize_one_layer(
};
match ret {
- Ret::ValueKind(v) => v,
- Ret::Value(v) => v.kind().clone(),
- Ret::ValueRef(v) => v.kind().clone(),
- Ret::Expr(expr) => ValueKind::PartialExpr(expr),
+ Ret::NirKind(v) => v,
+ Ret::Nir(v) => v.kind().clone(),
+ Ret::NirRef(v) => v.kind().clone(),
+ Ret::Expr(expr) => NirKind::PartialExpr(expr),
}
}
/// Normalize Hir into WHNF
-pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
match hir.kind() {
HirKind::Var(var) => env.lookup_val(var),
HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
- ValueKind::LamClosure {
+ NirKind::LamClosure {
binder: Binder::new(binder.clone()),
annot: annot,
closure: Closure::new(env, body.clone()),
@@ -465,7 +452,7 @@ pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
}
HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
let annot = annot.eval(env);
- ValueKind::PiClosure {
+ NirKind::PiClosure {
binder: Binder::new(binder.clone()),
annot,
closure: Closure::new(env, body.clone()),
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
index 264b81d..413c759 100644
--- a/dhall/src/semantics/nze/var.rs
+++ b/dhall/src/semantics/nze/var.rs
@@ -1,7 +1,7 @@
use crate::syntax::Label;
// Exactly like a Label, but equality returns always true.
-// This is so that ValueKind equality is exactly alpha-equivalence.
+// This is so that NirKind equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct Binder {
name: Label,
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index ae65fff..346abbf 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,5 +1,5 @@
use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value};
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::{NormalizedExpr, ToExprOptions};
@@ -75,8 +75,8 @@ impl Hir {
}
/// Eval the Hir. It will actually get evaluated only as needed on demand.
- pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
- Value::new_thunk(env.into(), self.clone())
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
+ Nir::new_thunk(env.into(), self.clone())
}
}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index f290c02..17b3cfe 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value};
+use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv};
use crate::syntax::Label;
/// Environment for indexing variables.
@@ -61,7 +61,7 @@ impl TyEnv {
items: self.items.insert_type(ty),
}
}
- pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self {
+ pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self {
TyEnv {
names: self.names.insert(x),
items: self.items.insert_value(e, ty),
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index 800d1b7..908bf8f 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -1,5 +1,5 @@
use crate::error::{ErrorBuilder, TypeError};
-use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv};
+use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv};
use crate::syntax::{Builtin, Const, Span};
use crate::{NormalizedExpr, ToExprOptions};
@@ -10,7 +10,7 @@ pub(crate) struct Universe(u8);
/// An expression representing a type
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) struct Type {
- val: Value,
+ val: Nir,
univ: Universe,
}
@@ -44,7 +44,7 @@ impl Universe {
}
impl Type {
- pub fn new(val: Value, univ: Universe) -> Self {
+ pub fn new(val: Nir, univ: Universe) -> Self {
Type { val, univ }
}
/// Creates a new Type and infers its universe by re-typechecking its value.
@@ -52,7 +52,7 @@ impl Type {
/// PiClosure.
pub fn new_infer_universe(
env: &TyEnv,
- val: Value,
+ val: Nir,
) -> Result<Self, TypeError> {
let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const();
let u = match c {
@@ -65,7 +65,7 @@ impl Type {
Ok(Type::new(val, u))
}
pub fn from_const(c: Const) -> Self {
- Self::new(Value::from_const(c), c.to_universe().next())
+ Self::new(Nir::from_const(c), c.to_universe().next())
}
pub fn from_builtin(b: Builtin) -> Self {
use Builtin::*;
@@ -74,7 +74,7 @@ impl Type {
_ => unreachable!("this builtin is not a type: {}", b),
}
- Self::new(Value::from_builtin(b), Universe::from_const(Const::Type))
+ Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type))
}
/// Get the type of this type
@@ -82,19 +82,19 @@ impl Type {
self.univ
}
- pub fn to_value(&self) -> Value {
+ pub fn to_nir(&self) -> Nir {
self.val.clone()
}
- pub fn as_value(&self) -> &Value {
+ pub fn as_nir(&self) -> &Nir {
&self.val
}
- pub fn into_value(self) -> Value {
+ pub fn into_nir(self) -> Nir {
self.val
}
pub fn as_const(&self) -> Option<Const> {
self.val.as_const()
}
- pub fn kind(&self) -> &ValueKind {
+ pub fn kind(&self) -> &NirKind {
self.val.kind()
}
@@ -136,7 +136,7 @@ impl Tir {
}
/// Eval the Tir. It will actually get evaluated only as needed on demand.
- pub fn eval(&self, env: impl Into<NzEnv>) -> Value {
+ pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
self.as_hir().eval(env.into())
}
pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> {
@@ -175,11 +175,11 @@ impl Tir {
}
/// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as
/// needed on demand.
- pub fn eval_closed_expr(&self) -> Value {
+ pub fn eval_closed_expr(&self) -> Nir {
self.eval(NzEnv::new())
}
/// Eval a closed Tir fully and recursively;
- pub fn rec_eval_closed_expr(&self) -> Value {
+ pub fn rec_eval_closed_expr(&self) -> Nir {
let val = self.eval_closed_expr();
val.normalize();
val
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7bf15af..42a9165 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, Tir, TyEnv,
- Type, Value, ValueKind,
+ type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir,
+ NirKind, Tir, TyEnv, Type,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span,
@@ -15,11 +15,11 @@ use crate::syntax::{
fn check_rectymerge(
span: &Span,
env: &TyEnv,
- x: Value,
- y: Value,
+ x: Nir,
+ y: Nir,
) -> Result<(), TypeError> {
let kts_x = match x.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => {
return mk_span_err(
span.clone(),
@@ -28,7 +28,7 @@ fn check_rectymerge(
}
};
let kts_y = match y.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => {
return mk_span_err(
span.clone(),
@@ -118,7 +118,7 @@ fn type_one_layer(
ExprKind::EmptyListLit(t) => {
let t = t.eval_to_type(env)?;
match t.kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
@@ -139,18 +139,16 @@ fn type_one_layer(
return span_err("InvalidListType");
}
- let t = x.ty().to_value();
- Value::from_builtin(Builtin::List)
- .app(t)
- .to_type(Const::Type)
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type)
}
ExprKind::SomeLit(x) => {
if x.ty().ty().as_const() != Some(Const::Type) {
return span_err("InvalidOptionalType");
}
- let t = x.ty().to_value();
- Value::from_builtin(Builtin::Optional)
+ let t = x.ty().to_nir();
+ Nir::from_builtin(Builtin::Optional)
.app(t)
.to_type(Const::Type)
}
@@ -165,7 +163,7 @@ fn type_one_layer(
Entry::Occupied(_) => {
return span_err("RecordTypeDuplicateField")
}
- Entry::Vacant(e) => e.insert(v.ty().to_value()),
+ Entry::Vacant(e) => e.insert(v.ty().to_nir()),
};
// Check that the fields have a valid kind
@@ -175,7 +173,7 @@ fn type_one_layer(
}
}
- Value::from_kind(ValueKind::RecordType(kts)).to_type(k)
+ Nir::from_kind(NirKind::RecordType(kts)).to_type(k)
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
@@ -230,21 +228,21 @@ fn type_one_layer(
}
ExprKind::Field(scrut, x) => {
match scrut.ty().kind() {
- ValueKind::RecordType(kts) => match kts.get(&x) {
+ NirKind::RecordType(kts) => match kts.get(&x) {
Some(val) => Type::new_infer_universe(env, val.clone())?,
None => return span_err("MissingRecordField"),
},
- ValueKind::Const(_) => {
+ NirKind::Const(_) => {
let scrut = scrut.eval_to_type(env)?;
match scrut.kind() {
- ValueKind::UnionType(kts) => match kts.get(x) {
+ NirKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- Value::from_kind(ValueKind::PiClosure {
+ Nir::from_kind(NirKind::PiClosure {
binder: Binder::new(x.clone()),
annot: ty.clone(),
closure: Closure::new_constant(
- scrut.to_value(),
+ scrut.to_nir(),
),
})
.to_type(scrut.ty())
@@ -261,10 +259,8 @@ fn type_one_layer(
ExprKind::Assert(t) => {
let t = t.eval_to_type(env)?;
match t.kind() {
- ValueKind::Equivalence(x, y) if x == y => {}
- ValueKind::Equivalence(..) => {
- return span_err("AssertMismatch")
- }
+ NirKind::Equivalence(x, y) if x == y => {}
+ NirKind::Equivalence(..) => return span_err("AssertMismatch"),
_ => return span_err("AssertMustTakeEquivalence"),
}
t
@@ -272,8 +268,8 @@ fn type_one_layer(
ExprKind::App(f, arg) => {
match f.ty().kind() {
// TODO: store Type in closure
- ValueKind::PiClosure { annot, closure, .. } => {
- if arg.ty().as_value() != annot {
+ NirKind::PiClosure { annot, closure, .. } => {
+ if arg.ty().as_nir() != annot {
return mkerr(
ErrorBuilder::new(format!(
"wrong type of function argument"
@@ -318,7 +314,7 @@ fn type_one_layer(
}
}
ExprKind::BoolIf(x, y, z) => {
- if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
+ if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
}
if y.ty().ty().as_const() != Some(Const::Type) {
@@ -336,12 +332,12 @@ fn type_one_layer(
// Extract the LHS record type
let kts_x = match x_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("MustCombineRecord"),
};
// Extract the RHS record type
let kts_y = match y_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("MustCombineRecord"),
};
@@ -352,10 +348,10 @@ fn type_one_layer(
})?;
let u = max(x.ty().ty(), y.ty().ty());
- Value::from_kind(ValueKind::RecordType(kts)).to_type(u)
+ Nir::from_kind(NirKind::RecordType(kts)).to_type(u)
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
- check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?;
+ check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?;
let hir = Hir::new(
HirKind::Expr(ExprKind::BinOp(
@@ -379,7 +375,7 @@ fn type_one_layer(
}
ExprKind::BinOp(BinOp::ListAppend, l, r) => {
match l.ty().kind() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
..
}) => {}
@@ -431,14 +427,14 @@ fn type_one_layer(
ExprKind::Merge(record, union, type_annot) => {
let record_type = record.ty();
let handlers = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("Merge1ArgMustBeRecord"),
};
let union_type = union.ty();
let variants = match union_type.kind() {
- ValueKind::UnionType(kts) => Cow::Borrowed(kts),
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::UnionType(kts) => Cow::Borrowed(kts),
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::Optional,
args,
..
@@ -457,7 +453,7 @@ fn type_one_layer(
let handler_return_type: Type = match variants.get(x) {
// Union alternative with type
Some(Some(variant_type)) => match handler_type.kind() {
- ValueKind::PiClosure { closure, annot, .. } => {
+ NirKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
return mkerr(
ErrorBuilder::new(format!(
@@ -578,7 +574,7 @@ fn type_one_layer(
}
let record_t = record.ty();
let kts = match record_t.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => {
return span_err("The argument to `toMap` must be a record")
}
@@ -598,7 +594,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() {
- ValueKind::AppliedBuiltin(BuiltinClosure {
+ NirKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
..
@@ -606,14 +602,14 @@ fn type_one_layer(
_ => return span_err(err_msg),
};
let kts = match arg.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err(err_msg),
};
if kts.len() != 2 {
return span_err(err_msg);
}
match kts.get(&"mapKey".into()) {
- Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+ Some(t) if *t == Nir::from_builtin(Builtin::Text) => {}
_ => return span_err(err_msg),
}
match kts.get(&"mapValue".into()) {
@@ -632,10 +628,10 @@ fn type_one_layer(
}
let mut kts = HashMap::new();
- kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+ kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text));
kts.insert("mapValue".into(), entry_type);
- let output_type: Type = Value::from_builtin(Builtin::List)
- .app(Value::from_kind(ValueKind::RecordType(kts)))
+ let output_type: Type = Nir::from_builtin(Builtin::List)
+ .app(Nir::from_kind(NirKind::RecordType(kts)))
.to_type(Const::Type);
if let Some(annot) = annot {
let annot_val = annot.eval_to_type(env)?;
@@ -649,7 +645,7 @@ fn type_one_layer(
ExprKind::Projection(record, labels) => {
let record_type = record.ty();
let kts = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
@@ -671,19 +667,19 @@ fn type_one_layer(
Type::new_infer_universe(
env,
- Value::from_kind(ValueKind::RecordType(new_kts)),
+ Nir::from_kind(NirKind::RecordType(new_kts)),
)?
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.ty();
let rec_kts = match record_type.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionMustBeRecord"),
};
let selection_val = selection.eval_to_type(env)?;
let sel_kts = match selection_val.kind() {
- ValueKind::RecordType(kts) => kts,
+ NirKind::RecordType(kts) => kts,
_ => return span_err("ProjectionByExprTakesRecordType"),
};
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ad5fee5..482f9ae 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -208,7 +208,7 @@ impl TestFile {
from_slice::<Value>(&expr_data).unwrap(),
from_slice::<Value>(&expected_data).unwrap()
);
- // If difference was not visible in the cbor::Value, compare normally.
+ // If difference was not visible in the cbor::Nir, compare normally.
assert_eq!(expr_data, expected_data);
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 21:49:20 +0000