From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/nze/env.rs | 10 +- dhall/src/semantics/nze/mod.rs | 4 +- dhall/src/semantics/nze/nir.rs | 521 ++++++++++++++++++++++++++++++++++ dhall/src/semantics/nze/normalize.rs | 243 ++++++++-------- dhall/src/semantics/nze/value.rs | 526 ----------------------------------- dhall/src/semantics/nze/var.rs | 2 +- 6 files changed, 644 insertions(+), 662 deletions(-) create mode 100644 dhall/src/semantics/nze/nir.rs delete mode 100644 dhall/src/semantics/nze/value.rs (limited to 'dhall/src/semantics/nze') 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 { // 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 ValEnv { 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/nir.rs b/dhall/src/semantics/nze/nir.rs new file mode 100644 index 0000000..a6dafa2 --- /dev/null +++ b/dhall/src/semantics/nze/nir.rs @@ -0,0 +1,521 @@ +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 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); + +#[derive(Debug)] +struct NirInternal { + kind: lazy::Lazy, + span: Span, +} + +/// 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 }, +} + +/// 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>); + +/// 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), + + Var(NzVar), + Const(Const), + Lit(LitKind), + EmptyOptionalLit(Nir), + NEOptionalLit(Nir), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Nir), + NEListLit(Vec), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Nir, HashMap>), + TextLit(TextLit), + Equivalence(Nir, Nir), + /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. + PartialExpr(ExprKind), +} + +impl Nir { + /// Construct a Nir from a completely unnormalized expression. + pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir { + let span = hir.span(); + NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir() + } + /// Construct a Nir from a partially normalized expression that's not in WHNF. + pub(crate) fn from_partial_expr(e: ExprKind) -> Nir { + // TODO: env + let env = NzEnv::new(); + NirInternal::from_thunk( + Thunk::from_partial_expr(env, e), + Span::Artificial, + ) + .into_nir() + } + /// 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 = 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 { + 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 { + 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) -> 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 { + if opts.normalize { + self.normalize(); + } + 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>| { + 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, self.0.span.clone()) + } + pub fn to_hir_noenv(&self) -> Hir { + self.to_hir(VarEnv::new()) + } +} + +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 { + NirInternal { + kind: lazy::Lazy::new(th), + span, + } + } + 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) -> 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 { + 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>, + ) -> 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 { + 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> { + 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 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 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>, -) -> Vec> { + elts: impl Iterator>, +) -> Vec> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator>, + elts: impl Iterator>, crnt_str: &mut String, - ret: &mut Vec>, + ret: &mut Vec>, ) { 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), + NirKind(NirKind), + Nir(Nir), + NirRef(&'a Nir), + Expr(ExprKind), } -fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { +fn apply_binop<'a>(o: BinOp, x: &'a Nir, y: &'a Nir) -> Option> { 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> { // 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> { 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, - env: &NzEnv, -) -> ValueKind { +pub(crate) fn normalize_one_layer(expr: ExprKind, 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/value.rs b/dhall/src/semantics/nze/value.rs deleted file mode 100644 index 7084af6..0000000 --- a/dhall/src/semantics/nze/value.rs +++ /dev/null @@ -1,526 +0,0 @@ -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 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); - -#[derive(Debug)] -struct ValueInternal { - kind: lazy::Lazy, - span: Span, -} - -/// 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 }, -} - -/// 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: 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>); - -/// 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), - - Var(NzVar), - Const(Const), - Lit(LitKind), - EmptyOptionalLit(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - TextLit(TextLit), - Equivalence(Value, Value), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. - PartialExpr(ExprKind), -} - -impl Value { - /// Construct a Value from a completely unnormalized expression. - pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value { - let span = hir.span(); - ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() - } - /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind) -> Value { - // TODO: env - let env = NzEnv::new(); - ValueInternal::from_thunk( - Thunk::from_partial_expr(env, e), - Span::Artificial, - ) - .into_value() - } - /// Make a Value from a ValueKind - pub(crate) fn from_kind(v: ValueKind) -> Value { - ValueInternal::from_whnf(v, Span::Artificial).into_value() - } - pub(crate) fn from_const(c: Const) -> Self { - let v = ValueKind::Const(c); - ValueInternal::from_whnf(v, Span::Artificial).into_value() - } - 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())) - } - pub(crate) fn from_text(txt: impl ToString) -> Self { - Value::from_kind(ValueKind::TextLit(TextLit::from_text( - txt.to_string(), - ))) - } - - pub(crate) fn as_const(&self) -> Option { - match &*self.kind() { - ValueKind::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 { - self.0.kind() - } - - pub(crate) fn to_type(&self, u: impl Into) -> 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 { - if opts.normalize { - self.normalize(); - } - 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: Value) -> Value { - Value::from_kind(apply_any(self.clone(), v)) - } - - pub fn to_hir(&self, venv: VarEnv) -> Hir { - let map_uniontype = |kts: &HashMap>| { - ExprKind::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_hir(venv))) - }) - .collect(), - ) - }; - - let hir = match &*self.kind() { - ValueKind::Var(v) => HirKind::Var(venv.lookup(v)), - ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv), - self_kind => HirKind::Expr(match self_kind { - ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { - unreachable!() - } - ValueKind::LamClosure { - binder, - annot, - closure, - } => ExprKind::Lam( - binder.to_label(), - annot.to_hir(venv), - closure.to_hir(venv), - ), - ValueKind::PiClosure { - binder, - annot, - closure, - } => ExprKind::Pi( - binder.to_label(), - 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), - n.to_hir(venv), - ), - ValueKind::NEOptionalLit(n) => { - ExprKind::SomeLit(n.to_hir(venv)) - } - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( - HirKind::Expr(ExprKind::App( - Value::from_builtin(Builtin::List).to_hir(venv), - n.to_hir(venv), - )), - Span::Artificial, - )), - ValueKind::NEListLit(elts) => ExprKind::NEListLit( - elts.iter().map(|v| v.to_hir(venv)).collect(), - ), - ValueKind::TextLit(elts) => ExprKind::TextLit( - elts.iter() - .map(|t| t.map_ref(|v| v.to_hir(venv))) - .collect(), - ), - ValueKind::RecordLit(kvs) => ExprKind::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_hir(venv))) - .collect(), - ), - ValueKind::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( - Hir::new( - HirKind::Expr(map_uniontype(kts)), - Span::Artificial, - ), - l.clone(), - ), - ValueKind::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), - ), - ValueKind::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)), - }), - }; - - Hir::new(hir, self.0.span.clone()) - } - pub fn to_hir_noenv(&self) -> Hir { - self.to_hir(VarEnv::new()) - } -} - -impl ValueInternal { - fn from_whnf(k: ValueKind, span: Span) -> Self { - ValueInternal { - kind: lazy::Lazy::new_completed(k), - span, - } - } - fn from_thunk(th: Thunk, span: Span) -> Self { - ValueInternal { - kind: lazy::Lazy::new(th), - span, - } - } - fn into_value(self) -> Value { - Value(Rc::new(self)) - } - - fn kind(&self) -> &ValueKind { - &self.kind - } - fn normalize(&self) { - self.kind().normalize(); - } -} - -impl ValueKind { - pub(crate) fn into_value(self) -> Value { - Value::from_kind(self) - } - - pub(crate) fn normalize(&self) { - match self { - ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {} - - 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 { - fn new(env: NzEnv, body: Hir) -> Self { - Thunk::Thunk { env, body } - } - fn from_partial_expr(env: NzEnv, expr: ExprKind) -> Self { - Thunk::PartialExpr { env, expr } - } - fn eval(self) -> ValueKind { - 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: 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 { .. } => { - self.apply(Value::from_kind(ValueKind::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 { - 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>, - ) -> 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 { - 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> { - 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 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); - 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, -- cgit v1.2.3