summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
authorNadrieril Feneanar2020-02-19 17:25:57 +0000
committerGitHub2020-02-19 17:25:57 +0000
commitffbde252a850c7d96e1000e1be52792c41733a28 (patch)
treee668b7f764fb4981a802bc619e0b2ff62fa9ce16 /dhall/src/semantics/nze
parente4b3a879907b6dcc75d25847ae21a23d0201aae1 (diff)
parent7cbfc1a0d32766a383d1f48902502adaa2234d2f (diff)
Merge pull request #131 from Nadrieril/hir
Decouple main expression types
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/env.rs54
-rw-r--r--dhall/src/semantics/nze/mod.rs4
-rw-r--r--dhall/src/semantics/nze/nir.rs510
-rw-r--r--dhall/src/semantics/nze/normalize.rs413
-rw-r--r--dhall/src/semantics/nze/value.rs666
-rw-r--r--dhall/src/semantics/nze/var.rs2
6 files changed, 716 insertions, 933 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..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 {
@@ -9,18 +9,20 @@ pub(crate) enum NzVar {
}
#[derive(Debug, Clone)]
-enum NzEnvItem {
+enum EnvItem<Type> {
// Variable is bound with given type
- Kept(Value),
+ Kept(Type),
// Variable has been replaced by corresponding value
- Replaced(Value),
+ Replaced(Nir, Type),
}
#[derive(Debug, Clone)]
-pub(crate) struct NzEnv {
- items: Vec<NzEnvItem>,
+pub(crate) struct ValEnv<Type> {
+ items: Vec<EnvItem<Type>>,
}
+pub(crate) type NzEnv = ValEnv<()>;
+
impl NzVar {
pub fn new(idx: usize) -> Self {
NzVar::Bound(idx)
@@ -44,33 +46,49 @@ impl NzVar {
}
}
-impl NzEnv {
+impl<Type: Clone> ValEnv<Type> {
pub fn new() -> Self {
- NzEnv { items: Vec::new() }
+ ValEnv { items: Vec::new() }
+ }
+ pub fn discard_types(&self) -> ValEnv<()> {
+ let items = self
+ .items
+ .iter()
+ .map(|i| match i {
+ EnvItem::Kept(_) => EnvItem::Kept(()),
+ EnvItem::Replaced(val, _) => EnvItem::Replaced(val.clone(), ()),
+ })
+ .collect();
+ ValEnv { items }
}
- pub fn insert_type(&self, t: Value) -> Self {
+ pub fn insert_type(&self, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Kept(t));
+ env.items.push(EnvItem::Kept(ty));
env
}
- pub fn insert_value(&self, e: Value) -> Self {
+ pub fn insert_value(&self, e: Nir, ty: Type) -> Self {
let mut env = self.clone();
- env.items.push(NzEnvItem::Replaced(e));
+ 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] {
- NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
- NzEnvItem::Replaced(x) => x.kind().clone(),
+ EnvItem::Kept(_) => NirKind::Var(NzVar::new(idx)),
+ EnvItem::Replaced(x, _) => x.kind().clone(),
}
}
- pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+ pub fn lookup_ty(&self, var: &AlphaVar) -> Type {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) => ty.clone(),
- NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+ EnvItem::Kept(ty) | EnvItem::Replaced(_, ty) => ty.clone(),
}
}
}
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+ fn from(x: &'a NzEnv) -> Self {
+ x.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/nir.rs b/dhall/src/semantics/nze/nir.rs
new file mode 100644
index 0000000..4ed66b7
--- /dev/null
+++ b/dhall/src/semantics/nze/nir.rs
@@ -0,0 +1,510 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::semantics::nze::lazy;
+use crate::semantics::{
+ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder,
+ BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv,
+};
+use crate::syntax::{
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind,
+ Span,
+};
+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 `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 Nir(Rc<NirInternal>);
+
+#[derive(Debug)]
+struct NirInternal {
+ kind: lazy::Lazy<Thunk, NirKind>,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+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<Nir> },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+ /// Normal closure
+ Closure { env: NzEnv, body: Hir },
+ /// Closure that ignores the argument passed
+ 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<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 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 `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 NirKind {
+ /// Closures
+ LamClosure {
+ binder: Binder,
+ annot: Nir,
+ closure: Closure,
+ },
+ PiClosure {
+ binder: Binder,
+ annot: Nir,
+ closure: Closure,
+ },
+ AppliedBuiltin(BuiltinClosure<Nir>),
+
+ Var(NzVar),
+ Const(Const),
+ Lit(LitKind),
+ EmptyOptionalLit(Nir),
+ NEOptionalLit(Nir),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ 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(Nir, Nir),
+ /// Invariant: evaluation must not be able to progress with `normalize_one_layer`.
+ PartialExpr(ExprKind<Nir>),
+}
+
+impl Nir {
+ /// Construct a Nir from a completely unnormalized expression.
+ pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
+ NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
+ }
+ /// 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();
+ NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
+ }
+ /// Make a Nir from a NirKind
+ pub(crate) fn from_kind(v: NirKind) -> Nir {
+ NirInternal::from_whnf(v).into_nir()
+ }
+ pub(crate) fn from_const(c: Const) -> Self {
+ let v = NirKind::Const(c);
+ NirInternal::from_whnf(v).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 {
+ Nir::from_kind(NirKind::from_builtin_env(b, env.clone()))
+ }
+ pub(crate) fn from_text(txt: impl ToString) -> Self {
+ Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string())))
+ }
+
+ pub(crate) fn as_const(&self) -> Option<Const> {
+ match &*self.kind() {
+ 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) -> &NirKind {
+ self.0.kind()
+ }
+
+ pub(crate) fn to_type(&self, u: impl Into<Universe>) -> Type {
+ Type::new(self.clone(), u.into())
+ }
+ /// Converts a value back to the corresponding AST expression.
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ self.to_hir_noenv().to_expr(opts)
+ }
+ pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr {
+ self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv)
+ }
+
+ pub(crate) fn normalize(&self) {
+ self.0.normalize()
+ }
+
+ 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<Nir>>| {
+ ExprKind::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
+ })
+ .collect(),
+ )
+ };
+
+ let hir = match &*self.kind() {
+ NirKind::Var(v) => HirKind::Var(venv.lookup(v)),
+ NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+ self_kind => HirKind::Expr(match self_kind {
+ NirKind::Var(..) | NirKind::AppliedBuiltin(..) => {
+ unreachable!()
+ }
+ NirKind::LamClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Lam(
+ binder.to_label(),
+ annot.to_hir(venv),
+ closure.to_hir(venv),
+ ),
+ NirKind::PiClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Pi(
+ binder.to_label(),
+ annot.to_hir(venv),
+ closure.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),
+ ),
+ NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)),
+ NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+ HirKind::Expr(ExprKind::App(
+ Nir::from_builtin(Builtin::List).to_hir(venv),
+ n.to_hir(venv),
+ )),
+ Span::Artificial,
+ )),
+ NirKind::NEListLit(elts) => ExprKind::NEListLit(
+ elts.iter().map(|v| v.to_hir(venv)).collect(),
+ ),
+ NirKind::TextLit(elts) => ExprKind::TextLit(
+ elts.iter()
+ .map(|t| t.map_ref(|v| v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::RecordLit(kvs) => ExprKind::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::RecordType(kts) => ExprKind::RecordType(
+ kts.iter()
+ .map(|(k, v)| (k.clone(), v.to_hir(venv)))
+ .collect(),
+ ),
+ NirKind::UnionType(kts) => map_uniontype(kts),
+ NirKind::UnionConstructor(l, kts) => ExprKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ),
+ NirKind::UnionLit(l, v, kts) => ExprKind::App(
+ Hir::new(
+ HirKind::Expr(ExprKind::Field(
+ Hir::new(
+ HirKind::Expr(map_uniontype(kts)),
+ Span::Artificial,
+ ),
+ l.clone(),
+ )),
+ Span::Artificial,
+ ),
+ v.to_hir(venv),
+ ),
+ NirKind::Equivalence(x, y) => ExprKind::BinOp(
+ BinOp::Equivalence,
+ x.to_hir(venv),
+ y.to_hir(venv),
+ ),
+ NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
+ }),
+ };
+
+ Hir::new(hir, Span::Artificial)
+ }
+ pub fn to_hir_noenv(&self) -> Hir {
+ self.to_hir(VarEnv::new())
+ }
+}
+
+impl NirInternal {
+ fn from_whnf(k: NirKind) -> Self {
+ NirInternal {
+ kind: lazy::Lazy::new_completed(k),
+ }
+ }
+ fn from_thunk(th: Thunk) -> Self {
+ NirInternal {
+ kind: lazy::Lazy::new(th),
+ }
+ }
+ fn into_nir(self) -> Nir {
+ Nir(Rc::new(self))
+ }
+
+ fn kind(&self) -> &NirKind {
+ &self.kind
+ }
+ fn normalize(&self) {
+ self.kind().normalize();
+ }
+}
+
+impl NirKind {
+ pub(crate) fn into_nir(self) -> Nir {
+ Nir::from_kind(self)
+ }
+
+ pub(crate) fn normalize(&self) {
+ match self {
+ NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {}
+
+ NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => {
+ tth.normalize();
+ }
+
+ NirKind::NEOptionalLit(th) => {
+ th.normalize();
+ }
+ NirKind::LamClosure { annot, closure, .. }
+ | NirKind::PiClosure { annot, closure, .. } => {
+ annot.normalize();
+ closure.normalize();
+ }
+ NirKind::AppliedBuiltin(closure) => closure.normalize(),
+ NirKind::NEListLit(elts) => {
+ for x in elts.iter() {
+ x.normalize();
+ }
+ }
+ NirKind::RecordLit(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ NirKind::RecordType(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => {
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ NirKind::UnionLit(_, v, kts) => {
+ v.normalize();
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ NirKind::TextLit(tlit) => tlit.normalize(),
+ NirKind::Equivalence(x, y) => {
+ x.normalize();
+ y.normalize();
+ }
+ NirKind::PartialExpr(e) => {
+ e.map_ref(Nir::normalize);
+ }
+ }
+ }
+
+ 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) -> NirKind {
+ NirKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ }
+}
+
+impl Thunk {
+ fn new(env: NzEnv, body: Hir) -> Self {
+ Thunk::Thunk { env, body }
+ }
+ fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self {
+ Thunk::PartialExpr { env, expr }
+ }
+ fn eval(self) -> NirKind {
+ match self {
+ Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
+ Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
+ }
+ }
+}
+
+impl Closure {
+ pub fn new(env: &NzEnv, body: Hir) -> Self {
+ Closure::Closure {
+ env: env.clone(),
+ body,
+ }
+ }
+ /// New closure that ignores its argument
+ pub fn new_constant(body: Nir) -> Self {
+ Closure::ConstantClosure { body }
+ }
+
+ pub fn apply(&self, val: Nir) -> Nir {
+ match self {
+ Closure::Closure { env, body, .. } => {
+ body.eval(env.insert_value(val, ()))
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+ fn apply_var(&self, var: NzVar) -> Nir {
+ match self {
+ Closure::Closure { .. } => {
+ self.apply(Nir::from_kind(NirKind::Var(var)))
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+
+ // TODO: somehow normalize the body. Might require to pass an env.
+ pub fn normalize(&self) {}
+
+ /// Convert this closure to a Hir expression
+ pub fn to_hir(&self, venv: VarEnv) -> Hir {
+ self.apply_var(NzVar::new(venv.size()))
+ .to_hir(venv.insert())
+ }
+ /// 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<Nir, ()> {
+ match self {
+ Closure::Closure { .. } => {
+ let v = NzVar::fresh();
+ // TODO: handle case where variable is used in closure
+ // TODO: return information about where the variable is used
+ Ok(self.apply_var(v))
+ }
+ Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+ }
+ }
+}
+
+impl TextLit {
+ pub fn new(
+ elts: impl Iterator<Item = InterpolatedTextContents<Nir>>,
+ ) -> Self {
+ TextLit(squash_textlit(elts))
+ }
+ pub fn interpolate(v: Nir) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Expr(v)])
+ }
+ pub fn from_text(s: String) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ }
+
+ pub fn concat(&self, other: &TextLit) -> TextLit {
+ TextLit::new(self.iter().chain(other.iter()).cloned())
+ }
+ pub fn is_empty(&self) -> bool {
+ self.0.is_empty()
+ }
+ /// If the literal consists of only one interpolation and not text, return the interpolated
+ /// value.
+ pub fn as_single_expr(&self) -> Option<&Nir> {
+ use InterpolatedTextContents::Expr;
+ if let [Expr(v)] = self.0.as_slice() {
+ Some(v)
+ } else {
+ None
+ }
+ }
+ /// If there are no interpolations, return the corresponding text value.
+ pub fn as_text(&self) -> Option<String> {
+ use InterpolatedTextContents::Text;
+ if self.is_empty() {
+ Some(String::new())
+ } else if let [Text(s)] = self.0.as_slice() {
+ Some(s.clone())
+ } else {
+ None
+ }
+ }
+ 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(Nir::normalize);
+ }
+ }
+}
+
+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 Nir {
+ fn eq(&self, other: &Self) -> bool {
+ Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+ }
+}
+impl std::cmp::Eq for Nir {}
+
+impl std::cmp::PartialEq for Thunk {
+ fn eq(&self, _other: &Self) -> bool {
+ unreachable!(
+ "Trying to compare thunks but we should only compare WHNFs"
+ )
+ }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+ fn eq(&self, other: &Self) -> bool {
+ let v = NzVar::fresh();
+ self.apply_var(v) == other.apply_var(v)
+ }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Nir {
+ fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ let vint: &NirInternal = &self.0;
+ let kind = vint.kind();
+ if let NirKind::Const(c) = kind {
+ return write!(fmt, "{:?}", c);
+ }
+ 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 a00b7ff..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,49 +3,39 @@ use std::collections::HashMap;
use crate::semantics::NzEnv;
use crate::semantics::{
- Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
- ValueKind,
+ Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, NirKind, TextLit,
};
use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
+ BinOp, Builtin, ExprKind, InterpolatedTextContents, LitKind,
};
-use crate::Normalized;
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Nir, a: Nir) -> NirKind {
match f.kind() {
- ValueKind::LamClosure { closure, .. } => {
- closure.apply(a).to_whnf_check_type(ty)
+ 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, f.get_type().unwrap(), ty)
- }
- ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
- l.clone(),
- a,
- kts.clone(),
- uniont.clone(),
- f.get_type().unwrap(),
- ),
- _ => 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)
}
_ => {
@@ -96,86 +86,77 @@ where
// Small helper enum to avoid repetition
enum Ret<'a> {
- ValueKind(ValueKind),
- Value(Value),
- ValueRef(&'a Value),
- Expr(ExprKind<Value, Normalized>),
+ NirKind(NirKind),
+ Nir(Nir),
+ NirRef(&'a Nir),
+ Expr(ExprKind<Nir>),
}
-fn apply_binop<'a>(
- o: BinOp,
- x: &'a Value,
- y: &'a Value,
- ty: &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 ValueKind::{
- BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
- };
+ use LitKind::{Bool, Natural};
+ use NirKind::{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, _, _) 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, _, _) 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)),
+ (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, NaturalLit(0), _) => Ret::ValueRef(y),
- (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
- (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- Ret::ValueKind(NaturalLit(x + y))
+ (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)))
}
- (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))
+ (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)))
}
- (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, 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, 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), _) => 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();
@@ -183,32 +164,25 @@ fn apply_binop<'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 kts = match ty.kind() {
- RecordType(kts) => kts,
- _ => unreachable!("Internal type error"),
- };
- let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
- Ok(Value::from_partial_expr(
- ExprKind::BinOp(
- RecursiveRecordMerge,
- v1.clone(),
- v2.clone(),
- ),
- kts.get(k).expect("Internal type error").clone(),
- ))
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+ 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)) => {
@@ -216,118 +190,107 @@ fn apply_binop<'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(
- RecursiveRecordTypeMerge,
- l.clone(),
- r.clone(),
- ),
- ty.clone(),
- ))
+ |_, 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, Normalized>,
- ty: &Value,
- env: &NzEnv,
-) -> ValueKind {
- use ValueKind::{
- BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
- NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
- RecordType, UnionConstructor, UnionLit, UnionType,
+pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
+ use LitKind::Bool;
+ use NirKind::{
+ EmptyListLit, EmptyOptionalLit, Lit, NEListLit, NEOptionalLit,
+ PartialExpr, RecordLit, RecordType, UnionConstructor, UnionLit,
+ UnionType,
};
let ret = match expr {
- ExprKind::Import(_) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
- // Those cases have already been completely handled in the typechecking phase (using
- // `RetWhole`), so they won't appear here.
- ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
- | ExprKind::Embed(_)
- | ExprKind::Var(_) => {
- unreachable!("This case should have been handled in typecheck")
+ ExprKind::Import(..) | ExprKind::Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
}
- 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::Var(..)
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..) => unreachable!(
+ "This case should have been handled in normalize_hir_whnf"
+ ),
+
+ 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::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::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() {
- BoolLit(true) => Ret::ValueRef(e1),
- BoolLit(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`
- (BoolLit(true), BoolLit(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),
}
}
}
}
- ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
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(),
@@ -335,7 +298,6 @@ pub(crate) fn normalize_one_layer(
PartialExpr(ExprKind::Projection(v2, _)) => {
return normalize_one_layer(
ExprKind::Projection(v2.clone(), ls.clone()),
- ty,
env,
)
}
@@ -343,63 +305,42 @@ 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(),
- v.get_type().unwrap(),
- )),
+ UnionType(kts) => {
+ Ret::NirKind(UnionConstructor(l.clone(), kts.clone()))
+ }
PartialExpr(ExprKind::BinOp(
BinOp::RightBiasedRecordMerge,
x,
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()),
- ty,
env,
)
}
},
(RecordLit(kvs), _) => match kvs.get(l) {
Some(r) => Ret::Expr(ExprKind::Field(
- Value::from_kind_and_type(
- PartialExpr(ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- Value::from_kind_and_type(
- RecordLit({
- let mut kvs = HashMap::new();
- kvs.insert(l.clone(), r.clone());
- kvs
- }),
- Value::from_kind_and_type(
- RecordType({
- let mut kvs = HashMap::new();
- kvs.insert(
- l.clone(),
- r.get_type_not_sort(),
- );
- kvs
- }),
- r.get_type_not_sort()
- .get_type_not_sort(),
- ),
- ),
- y.clone(),
- )),
- v.get_type_not_sort(),
- ),
+ Nir::from_kind(PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ Nir::from_kind(RecordLit({
+ let mut kvs = HashMap::new();
+ kvs.insert(l.clone(), r.clone());
+ kvs
+ })),
+ y.clone(),
+ ))),
l.clone(),
)),
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -416,7 +357,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -426,7 +366,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(x.clone(), l.clone()),
- ty,
env,
)
}
@@ -438,25 +377,24 @@ pub(crate) fn normalize_one_layer(
ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
match handlers.kind() {
RecordLit(kvs) => match variant.kind() {
- UnionConstructor(l, _, _) => match kvs.get(l) {
- Some(h) => Ret::Value(h.clone()),
+ UnionConstructor(l, _) => match kvs.get(l) {
+ 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())),
+ UnionLit(l, v, _) => match kvs.get(l) {
+ 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),
@@ -467,37 +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();
- let mut rec_ty = HashMap::new();
- rec.insert("mapKey".into(), Value::from_text(k));
+ rec.insert("mapKey".into(), Nir::from_text(k));
rec.insert("mapValue".into(), v.clone());
- rec_ty.insert(
- "mapKey".into(),
- Value::from_builtin(Builtin::Text),
- );
- rec_ty.insert("mapValue".into(), v.get_type_not_sort());
-
- Value::from_kind_and_type(
- ValueKind::RecordLit(rec),
- Value::from_kind_and_type(
- ValueKind::RecordType(rec_ty),
- Value::from_const(Const::Type),
- ),
- )
+ Nir::from_kind(NirKind::RecordLit(rec))
})
.collect(),
)),
@@ -506,45 +431,41 @@ pub(crate) fn normalize_one_layer(
};
match ret {
- Ret::ValueKind(v) => v,
- Ret::Value(v) => v.to_whnf_check_type(ty),
- Ret::ValueRef(v) => v.to_whnf_check_type(ty),
- 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 a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
- match tye.kind() {
- TyExprKind::Var(var) => env.lookup_val(var),
- TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
+ match hir.kind() {
+ HirKind::Var(var) => env.lookup_val(var),
+ HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
+ HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
let annot = annot.eval(env);
- ValueKind::LamClosure {
+ NirKind::LamClosure {
binder: Binder::new(binder.clone()),
- annot: annot.clone(),
- closure: Closure::new(annot, env, body.clone()),
+ annot: annot,
+ closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
let annot = annot.eval(env);
- let closure = Closure::new(annot.clone(), env, body.clone());
- ValueKind::PiClosure {
+ NirKind::PiClosure {
binder: Binder::new(binder.clone()),
annot,
- closure,
+ closure: Closure::new(env, body.clone()),
}
}
- TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ HirKind::Expr(ExprKind::Let(_, _, val, body)) => {
let val = val.eval(env);
- body.eval(&env.insert_value(val)).kind().clone()
+ body.eval(env.insert_value(val, ())).kind().clone()
}
- TyExprKind::Expr(e) => {
- let ty = match tye.get_type() {
- Ok(ty) => ty,
- Err(_) => return ValueKind::Const(Const::Sort),
- };
- let e = e.map_ref(|tye| tye.eval(env));
- normalize_one_layer(e, &ty, env)
+ HirKind::Expr(e) => {
+ let e = e.map_ref(|hir| hir.eval(env));
+ normalize_one_layer(e, env)
}
}
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
deleted file mode 100644
index 607aa0d..0000000
--- a/dhall/src/semantics/nze/value.rs
+++ /dev/null
@@ -1,666 +0,0 @@
-use std::collections::HashMap;
-use std::rc::Rc;
-
-use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
-use crate::semantics::{
- apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
- TyEnv,
-};
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
-use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
- NaiveDouble, Natural, Span,
-};
-use crate::{Normalized, 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
-/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
-/// normalize as needed.
-#[derive(Clone)]
-pub(crate) struct Value(Rc<ValueInternal>);
-
-#[derive(Debug)]
-struct ValueInternal {
- kind: lazy::Lazy<Thunk, ValueKind>,
- /// This is None if and only if `form` is `Sort` (which doesn't have a type)
- ty: Option<Value>,
- span: Span,
-}
-
-/// An unevaluated subexpression
-#[derive(Debug, Clone)]
-pub(crate) enum Thunk {
- /// A completely unnormalized expression.
- Thunk { env: NzEnv, body: TyExpr },
- /// A partially normalized expression that may need to go through `normalize_one_layer`.
- PartialExpr {
- env: NzEnv,
- expr: ExprKind<Value, Normalized>,
- ty: Value,
- },
-}
-
-/// An unevaluated subexpression that takes an argument.
-#[derive(Debug, Clone)]
-pub(crate) enum Closure {
- /// Normal closure
- Closure {
- arg_ty: Value,
- env: NzEnv,
- body: TyExpr,
- },
- /// Closure that ignores the argument passed
- ConstantClosure { body: Value },
-}
-
-/// 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>>);
-
-/// 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
-/// 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.
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum ValueKind {
- /// Closures
- LamClosure {
- binder: Binder,
- annot: Value,
- closure: Closure,
- },
- PiClosure {
- binder: Binder,
- annot: Value,
- closure: Closure,
- },
- AppliedBuiltin(BuiltinClosure<Value>),
-
- Var(NzVar),
- Const(Const),
- BoolLit(bool),
- NaturalLit(Natural),
- IntegerLit(Integer),
- DoubleLit(NaiveDouble),
- EmptyOptionalLit(Value),
- NEOptionalLit(Value),
- // 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>>),
- // Also keep the type of the uniontype around
- UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
- // Also keep the type of the uniontype and the constructor around
- UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
- TextLit(TextLit),
- Equivalence(Value, Value),
- /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
- PartialExpr(ExprKind<Value, Normalized>),
-}
-
-impl Value {
- pub(crate) fn const_sort() -> Value {
- ValueInternal::from_whnf(
- ValueKind::Const(Const::Sort),
- None,
- Span::Artificial,
- )
- .into_value()
- }
- /// Construct a Value from a completely unnormalized expression.
- pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
- ValueInternal::from_thunk(
- Thunk::new(env, tye.clone()),
- tye.get_type().ok(),
- tye.span().clone(),
- )
- .into_value()
- }
- /// Construct a Value from a partially normalized expression that's not in WHNF.
- pub(crate) fn from_partial_expr(
- e: ExprKind<Value, Normalized>,
- ty: Value,
- ) -> Value {
- // TODO: env
- let env = NzEnv::new();
- ValueInternal::from_thunk(
- Thunk::from_partial_expr(env, e, ty.clone()),
- Some(ty),
- Span::Artificial,
- )
- .into_value()
- }
- /// Make a Value from a ValueKind
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
- ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
- }
- pub(crate) fn from_const(c: Const) -> Self {
- let v = ValueKind::Const(c);
- match c {
- Const::Type => {
- Value::from_kind_and_type(v, Value::from_const(Const::Kind))
- }
- Const::Kind => {
- Value::from_kind_and_type(v, Value::from_const(Const::Sort))
- }
- Const::Sort => Value::const_sort(),
- }
- }
- 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_and_type(
- ValueKind::from_builtin_env(b, env.clone()),
- typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
- )
- }
- pub(crate) fn from_text(txt: impl ToString) -> Self {
- Value::from_kind_and_type(
- ValueKind::TextLit(TextLit::from_text(txt.to_string())),
- Value::from_builtin(Builtin::Text),
- )
- }
-
- pub(crate) fn as_const(&self) -> Option<Const> {
- match &*self.kind() {
- ValueKind::Const(c) => Some(*c),
- _ => None,
- }
- }
- // pub(crate) fn span(&self) -> Span {
- // self.0.span.clone()
- // }
-
- /// This is what you want if you want to pattern-match on the value.
- /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
- /// panics.
- pub(crate) fn kind(&self) -> &ValueKind {
- self.0.kind()
- }
-
- /// Converts a value back to the corresponding AST expression.
- pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
- if opts.normalize {
- self.normalize();
- }
-
- self.to_tyexpr_noenv().to_expr(opts)
- }
- pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
- self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
- }
- pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
- self.kind().clone()
- }
- /// Before discarding type information, check that it matches the expected return type.
- pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
- self.check_type(ty);
- self.to_whnf_ignore_type()
- }
-
- /// Normalizes contents to normal form; faster than `normalize` if
- /// no one else shares this.
- pub(crate) fn normalize_mut(&mut self) {
- match Rc::get_mut(&mut self.0) {
- // Mutate directly if sole owner
- Some(vint) => vint.normalize_mut(),
- // Otherwise mutate through the refcell
- None => self.normalize(),
- }
- }
- pub(crate) fn normalize(&self) {
- self.0.normalize()
- }
-
- pub(crate) fn app(&self, v: Value) -> Value {
- let body_t = match &*self.get_type_not_sort().kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- v.check_type(annot);
- closure.apply(v.clone())
- }
- _ => unreachable!("Internal type error"),
- };
- Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
- }
-
- /// In debug mode, panic if the provided type doesn't match the value's type.
- /// Otherwise does nothing.
- pub(crate) fn check_type(&self, _ty: &Value) {
- // TODO: reenable
- // debug_assert_eq!(
- // Some(ty),
- // self.get_type().ok().as_ref(),
- // "Internal type error"
- // );
- }
- pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
- Ok(self.0.get_type()?.clone())
- }
- /// When we know the value isn't `Sort`, this gets the type directly
- pub(crate) fn get_type_not_sort(&self) -> Value {
- self.get_type()
- .expect("Internal type error: value is `Sort` but shouldn't be")
- }
-
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
- let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
- ExprKind::UnionType(
- kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
- })
- .collect(),
- )
- };
-
- let tye = match &*self.kind() {
- ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
- ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
- self_kind => TyExprKind::Expr(match self_kind {
- ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
- unreachable!()
- }
- ValueKind::LamClosure {
- binder,
- annot,
- closure,
- } => ExprKind::Lam(
- binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(venv),
- ),
- ValueKind::PiClosure {
- binder,
- annot,
- closure,
- } => ExprKind::Pi(
- binder.to_label(),
- annot.to_tyexpr(venv),
- closure.to_tyexpr(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::EmptyOptionalLit(n) => ExprKind::App(
- Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
- n.to_tyexpr(venv),
- ),
- ValueKind::NEOptionalLit(n) => {
- ExprKind::SomeLit(n.to_tyexpr(venv))
- }
- ValueKind::EmptyListLit(n) => {
- ExprKind::EmptyListLit(TyExpr::new(
- TyExprKind::Expr(ExprKind::App(
- Value::from_builtin(Builtin::List).to_tyexpr(venv),
- n.to_tyexpr(venv),
- )),
- Some(Value::from_const(Const::Type)),
- Span::Artificial,
- ))
- }
- ValueKind::NEListLit(elts) => ExprKind::NEListLit(
- elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
- ),
- ValueKind::TextLit(elts) => ExprKind::TextLit(
- elts.iter()
- .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
- kvs.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::RecordType(kts) => ExprKind::RecordType(
- kts.iter()
- .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
- .collect(),
- ),
- ValueKind::UnionType(kts) => map_uniontype(kts),
- ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(t.clone()),
- Span::Artificial,
- ),
- l.clone(),
- ),
- ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
- TyExpr::new(
- TyExprKind::Expr(ExprKind::Field(
- TyExpr::new(
- TyExprKind::Expr(map_uniontype(kts)),
- Some(uniont.clone()),
- Span::Artificial,
- ),
- l.clone(),
- )),
- Some(ctort.clone()),
- Span::Artificial,
- ),
- v.to_tyexpr(venv),
- ),
- ValueKind::Equivalence(x, y) => ExprKind::BinOp(
- BinOp::Equivalence,
- x.to_tyexpr(venv),
- y.to_tyexpr(venv),
- ),
- ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
- }),
- };
-
- TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
- }
- pub fn to_tyexpr_noenv(&self) -> TyExpr {
- self.to_tyexpr(VarEnv::new())
- }
-}
-
-impl ValueInternal {
- fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
- ValueInternal {
- kind: lazy::Lazy::new_completed(k),
- ty,
- span,
- }
- }
- fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
- ValueInternal {
- kind: lazy::Lazy::new(th),
- ty,
- span,
- }
- }
- fn into_value(self) -> Value {
- Value(Rc::new(self))
- }
-
- fn kind(&self) -> &ValueKind {
- &self.kind
- }
- fn normalize(&self) {
- self.kind().normalize();
- }
- // TODO: deprecated
- fn normalize_mut(&mut self) {
- self.normalize();
- }
-
- fn get_type(&self) -> Result<&Value, TypeError> {
- match &self.ty {
- Some(t) => Ok(t),
- None => Err(TypeError::new(TypeMessage::Sort)),
- }
- }
-}
-
-impl ValueKind {
- pub(crate) fn into_value_with_type(self, t: Value) -> Value {
- Value::from_kind_and_type(self, t)
- }
-
- pub(crate) fn normalize(&self) {
- match self {
- ValueKind::Var(..)
- | ValueKind::Const(_)
- | ValueKind::BoolLit(_)
- | ValueKind::NaturalLit(_)
- | ValueKind::IntegerLit(_)
- | ValueKind::DoubleLit(_) => {}
-
- ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
- tth.normalize();
- }
-
- ValueKind::NEOptionalLit(th) => {
- th.normalize();
- }
- ValueKind::LamClosure { annot, closure, .. }
- | ValueKind::PiClosure { annot, closure, .. } => {
- annot.normalize();
- closure.normalize();
- }
- ValueKind::AppliedBuiltin(closure) => closure.normalize(),
- ValueKind::NEListLit(elts) => {
- for x in elts.iter() {
- x.normalize();
- }
- }
- ValueKind::RecordLit(kvs) => {
- for x in kvs.values() {
- x.normalize();
- }
- }
- ValueKind::RecordType(kvs) => {
- for x in kvs.values() {
- x.normalize();
- }
- }
- ValueKind::UnionType(kts)
- | ValueKind::UnionConstructor(_, kts, _) => {
- for x in kts.values().flat_map(|opt| opt) {
- x.normalize();
- }
- }
- ValueKind::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) => {
- x.normalize();
- y.normalize();
- }
- ValueKind::PartialExpr(e) => {
- e.map_ref(Value::normalize);
- }
- }
- }
-
- pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
- ValueKind::from_builtin_env(b, NzEnv::new())
- }
- pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
- ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
- }
-}
-
-impl Thunk {
- pub fn new(env: &NzEnv, body: TyExpr) -> Self {
- Thunk::Thunk {
- env: env.clone(),
- body,
- }
- }
- pub fn from_partial_expr(
- env: NzEnv,
- expr: ExprKind<Value, Normalized>,
- ty: Value,
- ) -> Self {
- Thunk::PartialExpr { env, expr, ty }
- }
- pub fn eval(self) -> ValueKind {
- match self {
- Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
- Thunk::PartialExpr { env, expr, ty } => {
- normalize_one_layer(expr, &ty, &env)
- }
- }
- }
-}
-
-impl Closure {
- pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
- Closure::Closure {
- arg_ty,
- env: env.clone(),
- body,
- }
- }
- /// New closure that ignores its argument
- pub fn new_constant(body: Value) -> Self {
- Closure::ConstantClosure { body }
- }
-
- pub fn apply(&self, val: Value) -> Value {
- match self {
- Closure::Closure { env, body, .. } => {
- body.eval(&env.insert_value(val))
- }
- Closure::ConstantClosure { body, .. } => body.clone(),
- }
- }
- fn apply_var(&self, var: NzVar) -> Value {
- match self {
- Closure::Closure { arg_ty, .. } => {
- let val = Value::from_kind_and_type(
- ValueKind::Var(var),
- arg_ty.clone(),
- );
- self.apply(val)
- }
- Closure::ConstantClosure { body, .. } => body.clone(),
- }
- }
-
- // TODO: somehow normalize the body. Might require to pass an env.
- pub fn normalize(&self) {}
- /// Convert this closure to a TyExpr
- pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
- self.apply_var(NzVar::new(venv.size()))
- .to_tyexpr(venv.insert())
- }
- /// 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, ()> {
- match self {
- Closure::Closure { .. } => {
- let v = NzVar::fresh();
- // TODO: handle case where variable is used in closure
- // TODO: return information about where the variable is used
- Ok(self.apply_var(v))
- }
- Closure::ConstantClosure { body, .. } => Ok(body.clone()),
- }
- }
-}
-
-impl TextLit {
- pub fn new(
- elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
- ) -> Self {
- TextLit(squash_textlit(elts))
- }
- pub fn interpolate(v: Value) -> TextLit {
- TextLit(vec![InterpolatedTextContents::Expr(v)])
- }
- pub fn from_text(s: String) -> TextLit {
- TextLit(vec![InterpolatedTextContents::Text(s)])
- }
-
- pub fn concat(&self, other: &TextLit) -> TextLit {
- TextLit::new(self.iter().chain(other.iter()).cloned())
- }
- pub fn is_empty(&self) -> bool {
- self.0.is_empty()
- }
- /// If the literal consists of only one interpolation and not text, return the interpolated
- /// value.
- pub fn as_single_expr(&self) -> Option<&Value> {
- use InterpolatedTextContents::Expr;
- if let [Expr(v)] = self.0.as_slice() {
- Some(v)
- } else {
- None
- }
- }
- /// If there are no interpolations, return the corresponding text value.
- pub fn as_text(&self) -> Option<String> {
- use InterpolatedTextContents::Text;
- if self.is_empty() {
- Some(String::new())
- } else if let [Text(s)] = self.0.as_slice() {
- Some(s.clone())
- } else {
- None
- }
- }
- pub fn iter(
- &self,
- ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
- 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);
- }
- }
-}
-
-impl lazy::Eval<ValueKind> for Thunk {
- fn eval(self) -> ValueKind {
- self.eval()
- }
-}
-
-/// Compare two values for equality modulo alpha/beta-equivalence.
-impl std::cmp::PartialEq for Value {
- 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::PartialEq for Thunk {
- fn eq(&self, _other: &Self) -> bool {
- unreachable!(
- "Trying to compare thunks but we should only compare WHNFs"
- )
- }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for Closure {
- fn eq(&self, other: &Self) -> bool {
- let v = NzVar::fresh();
- self.apply_var(v) == other.apply_var(v)
- }
-}
-impl std::cmp::Eq for Closure {}
-
-impl std::fmt::Debug for Value {
- fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let vint: &ValueInternal = &self.0;
- let kind = vint.kind();
- if let ValueKind::Const(c) = kind {
- return write!(fmt, "{:?}", c);
- }
- let mut x = fmt.debug_struct(&format!("Value@WHNF"));
- x.field("kind", kind);
- if let Some(ty) = vint.ty.as_ref() {
- x.field("type", &ty);
- } else {
- x.field("type", &None::<()>);
- }
- x.finish()
- }
-}
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,