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/builtins.rs | 118 ++++---- 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 +- dhall/src/semantics/resolve/hir.rs | 6 +- dhall/src/semantics/tck/env.rs | 4 +- dhall/src/semantics/tck/tir.rs | 26 +- dhall/src/semantics/tck/typecheck.rs | 90 +++--- 11 files changed, 764 insertions(+), 786 deletions(-) create mode 100644 dhall/src/semantics/nze/nir.rs delete mode 100644 dhall/src/semantics/nze/value.rs (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 752b25c..61de0c7 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -1,5 +1,5 @@ use crate::semantics::{ - skip_resolve, typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv, + skip_resolve, typecheck, Hir, HirKind, Nir, NirKind, NzEnv, VarEnv, }; use crate::syntax::map::DupTreeMap; use crate::syntax::Const::Type; @@ -15,14 +15,14 @@ use std::convert::TryInto; /// A partially applied builtin. /// Invariant: the evaluation of the given args must not be able to progress further #[derive(Debug, Clone)] -pub(crate) struct BuiltinClosure { +pub(crate) struct BuiltinClosure { pub env: NzEnv, pub b: Builtin, /// Arguments applied to the closure so far. - pub args: Vec, + pub args: Vec, } -impl BuiltinClosure { +impl BuiltinClosure { pub fn new(b: Builtin, env: NzEnv) -> Self { BuiltinClosure { env, @@ -31,7 +31,7 @@ impl BuiltinClosure { } } - pub fn apply(&self, a: Value) -> ValueKind { + pub fn apply(&self, a: Nir) -> NirKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); apply_builtin(self.b, args, self.env.clone()) @@ -256,14 +256,14 @@ macro_rules! make_closure { } #[allow(clippy::cognitive_complexity)] -fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { +fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { use LitKind::{Bool, Double, Integer, Natural}; - use ValueKind::*; + use NirKind::*; // Small helper enum enum Ret { - ValueKind(ValueKind), - Value(Value), + NirKind(NirKind), + Nir(Nir), DoneAsIs, } let make_closure = |e| { @@ -274,35 +274,35 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let ret = match (b, args.as_slice()) { (Builtin::OptionalNone, [t]) => { - Ret::ValueKind(EmptyOptionalLit(t.clone())) + Ret::NirKind(EmptyOptionalLit(t.clone())) } (Builtin::NaturalIsZero, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n == 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalEven, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 == 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 == 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalOdd, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Bool(*n % 2 != 0))), + Lit(Natural(n)) => Ret::NirKind(Lit(Bool(*n % 2 != 0))), _ => Ret::DoneAsIs, }, (Builtin::NaturalToInteger, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::ValueKind(Lit(Integer(*n as isize))), + Lit(Natural(n)) => Ret::NirKind(Lit(Integer(*n as isize))), _ => Ret::DoneAsIs, }, (Builtin::NaturalShow, [n]) => match &*n.kind() { - Lit(Natural(n)) => Ret::Value(Value::from_text(n)), + Lit(Natural(n)) => Ret::Nir(Nir::from_text(n)), _ => Ret::DoneAsIs, }, (Builtin::NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) { (Lit(Natural(a)), Lit(Natural(b))) => { - Ret::ValueKind(Lit(Natural(if b > a { b - a } else { 0 }))) + Ret::NirKind(Lit(Natural(if b > a { b - a } else { 0 }))) } - (Lit(Natural(0)), _) => Ret::Value(b.clone()), - (_, Lit(Natural(0))) => Ret::ValueKind(Lit(Natural(0))), - _ if a == b => Ret::ValueKind(Lit(Natural(0))), + (Lit(Natural(0)), _) => Ret::Nir(b.clone()), + (_, Lit(Natural(0))) => Ret::NirKind(Lit(Natural(0))), + _ if a == b => Ret::NirKind(Lit(Natural(0))), _ => Ret::DoneAsIs, }, (Builtin::IntegerShow, [n]) => match &*n.kind() { @@ -312,28 +312,28 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { } else { format!("+{}", n) }; - Ret::Value(Value::from_text(s)) + Ret::Nir(Nir::from_text(s)) } _ => Ret::DoneAsIs, }, (Builtin::IntegerToDouble, [n]) => match &*n.kind() { Lit(Integer(n)) => { - Ret::ValueKind(Lit(Double(NaiveDouble::from(*n as f64)))) + Ret::NirKind(Lit(Double(NaiveDouble::from(*n as f64)))) } _ => Ret::DoneAsIs, }, (Builtin::IntegerNegate, [n]) => match &*n.kind() { - Lit(Integer(n)) => Ret::ValueKind(Lit(Integer(-n))), + Lit(Integer(n)) => Ret::NirKind(Lit(Integer(-n))), _ => Ret::DoneAsIs, }, (Builtin::IntegerClamp, [n]) => match &*n.kind() { Lit(Integer(n)) => { - Ret::ValueKind(Lit(Natural((*n).try_into().unwrap_or(0)))) + Ret::NirKind(Lit(Natural((*n).try_into().unwrap_or(0)))) } _ => Ret::DoneAsIs, }, (Builtin::DoubleShow, [n]) => match &*n.kind() { - Lit(Double(n)) => Ret::Value(Value::from_text(n)), + Lit(Double(n)) => Ret::Nir(Nir::from_text(n)), _ => Ret::DoneAsIs, }, (Builtin::TextShow, [v]) => match &*v.kind() { @@ -343,7 +343,7 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let txt: InterpolatedText = std::iter::once(InterpolatedTextContents::Text(s)) .collect(); - Ret::Value(Value::from_text(txt)) + Ret::Nir(Nir::from_text(txt)) } else { Ret::DoneAsIs } @@ -351,28 +351,28 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { _ => Ret::DoneAsIs, }, (Builtin::ListLength, [_, l]) => match &*l.kind() { - EmptyListLit(_) => Ret::ValueKind(Lit(Natural(0))), - NEListLit(xs) => Ret::ValueKind(Lit(Natural(xs.len()))), + EmptyListLit(_) => Ret::NirKind(Lit(Natural(0))), + NEListLit(xs) => Ret::NirKind(Lit(Natural(xs.len()))), _ => Ret::DoneAsIs, }, (Builtin::ListHead, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), + EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), NEListLit(xs) => { - Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone())) + Ret::NirKind(NEOptionalLit(xs.iter().next().unwrap().clone())) } _ => Ret::DoneAsIs, }, (Builtin::ListLast, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())), - NEListLit(xs) => Ret::ValueKind(NEOptionalLit( + EmptyListLit(n) => Ret::NirKind(EmptyOptionalLit(n.clone())), + NEListLit(xs) => Ret::NirKind(NEOptionalLit( xs.iter().rev().next().unwrap().clone(), )), _ => Ret::DoneAsIs, }, (Builtin::ListReverse, [_, l]) => match &*l.kind() { - EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())), + EmptyListLit(n) => Ret::NirKind(EmptyListLit(n.clone())), NEListLit(xs) => { - Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect())) + Ret::NirKind(NEListLit(xs.iter().rev().cloned().collect())) } _ => Ret::DoneAsIs, }, @@ -383,10 +383,10 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let mut kts = HashMap::new(); kts.insert( "index".into(), - Value::from_builtin(Builtin::Natural), + Nir::from_builtin(Builtin::Natural), ); kts.insert("value".into(), t.clone()); - let t = Value::from_kind(RecordType(kts)); + let t = Nir::from_kind(RecordType(kts)); // Construct the new list, with added indices let list = match l.kind() { @@ -398,23 +398,23 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_kind(Lit(Natural(i))), + Nir::from_kind(Lit(Natural(i))), ); kvs.insert("value".into(), e.clone()); - Value::from_kind(RecordLit(kvs)) + Nir::from_kind(RecordLit(kvs)) }) .collect(), ), _ => unreachable!(), }; - Ret::ValueKind(list) + Ret::NirKind(list) } _ => Ret::DoneAsIs, } } (Builtin::ListBuild, [t, f]) => { - let list_t = Value::from_builtin(Builtin::List).app(t.clone()); - Ret::Value( + let list_t = Nir::from_builtin(Builtin::List).app(t.clone()); + Ret::Nir( f.app(list_t.clone()) .app( make_closure(make_closure!( @@ -425,24 +425,24 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { )) .app(t.clone()), ) - .app(EmptyListLit(t.clone()).into_value()), + .app(EmptyListLit(t.clone()).into_nir()), ) } (Builtin::ListFold, [_, l, _, cons, nil]) => match &*l.kind() { - EmptyListLit(_) => Ret::Value(nil.clone()), + EmptyListLit(_) => Ret::Nir(nil.clone()), NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().cloned().rev() { v = cons.app(x).app(v); } - Ret::Value(v) + Ret::Nir(v) } _ => Ret::DoneAsIs, }, (Builtin::OptionalBuild, [t, f]) => { let optional_t = - Value::from_builtin(Builtin::Optional).app(t.clone()); - Ret::Value( + Nir::from_builtin(Builtin::Optional).app(t.clone()); + Ret::Nir( f.app(optional_t.clone()) .app( make_closure(make_closure!( @@ -452,47 +452,47 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> ValueKind { )) .app(t.clone()), ) - .app(EmptyOptionalLit(t.clone()).into_value()), + .app(EmptyOptionalLit(t.clone()).into_nir()), ) } (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { - EmptyOptionalLit(_) => Ret::Value(nothing.clone()), - NEOptionalLit(x) => Ret::Value(just.app(x.clone())), + EmptyOptionalLit(_) => Ret::Nir(nothing.clone()), + NEOptionalLit(x) => Ret::Nir(just.app(x.clone())), _ => Ret::DoneAsIs, }, - (Builtin::NaturalBuild, [f]) => Ret::Value( - f.app(Value::from_builtin(Builtin::Natural)) + (Builtin::NaturalBuild, [f]) => Ret::Nir( + f.app(Nir::from_builtin(Builtin::Natural)) .app(make_closure(make_closure!( λ(x : Natural) -> 1 + var(x) ))) - .app(Lit(Natural(0)).into_value()), + .app(Lit(Natural(0)).into_nir()), ), (Builtin::NaturalFold, [n, t, succ, zero]) => match &*n.kind() { - Lit(Natural(0)) => Ret::Value(zero.clone()), + Lit(Natural(0)) => Ret::Nir(zero.clone()), Lit(Natural(n)) => { - let fold = Value::from_builtin(Builtin::NaturalFold) - .app(Lit(Natural(n - 1)).into_value()) + let fold = Nir::from_builtin(Builtin::NaturalFold) + .app(Lit(Natural(n - 1)).into_nir()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); - Ret::Value(succ.app(fold)) + Ret::Nir(succ.app(fold)) } _ => Ret::DoneAsIs, }, _ => Ret::DoneAsIs, }; match ret { - Ret::ValueKind(v) => v, - Ret::Value(v) => v.kind().clone(), + Ret::NirKind(v) => v, + Ret::Nir(v) => v.kind().clone(), Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, env }), } } -impl std::cmp::PartialEq for BuiltinClosure { +impl std::cmp::PartialEq for BuiltinClosure { fn eq(&self, other: &Self) -> bool { self.b == other.b && self.args == other.args } } -impl std::cmp::Eq for BuiltinClosure {} +impl std::cmp::Eq for BuiltinClosure {} 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, diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index ae65fff..346abbf 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,5 +1,5 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value}; +use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -75,8 +75,8 @@ impl Hir { } /// Eval the Hir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: impl Into) -> Value { - Value::new_thunk(env.into(), self.clone()) + pub fn eval(&self, env: impl Into) -> Nir { + Nir::new_thunk(env.into(), self.clone()) } } diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs index f290c02..17b3cfe 100644 --- a/dhall/src/semantics/tck/env.rs +++ b/dhall/src/semantics/tck/env.rs @@ -1,4 +1,4 @@ -use crate::semantics::{AlphaVar, NameEnv, NzEnv, NzVar, Type, ValEnv, Value}; +use crate::semantics::{AlphaVar, NameEnv, Nir, NzEnv, NzVar, Type, ValEnv}; use crate::syntax::Label; /// Environment for indexing variables. @@ -61,7 +61,7 @@ impl TyEnv { items: self.items.insert_type(ty), } } - pub fn insert_value(&self, x: &Label, e: Value, ty: Type) -> Self { + pub fn insert_value(&self, x: &Label, e: Nir, ty: Type) -> Self { TyEnv { names: self.names.insert(x), items: self.items.insert_value(e, ty), diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs index 800d1b7..908bf8f 100644 --- a/dhall/src/semantics/tck/tir.rs +++ b/dhall/src/semantics/tck/tir.rs @@ -1,5 +1,5 @@ use crate::error::{ErrorBuilder, TypeError}; -use crate::semantics::{mkerr, Hir, NzEnv, TyEnv, Value, ValueKind, VarEnv}; +use crate::semantics::{mkerr, Hir, Nir, NirKind, NzEnv, TyEnv, VarEnv}; use crate::syntax::{Builtin, Const, Span}; use crate::{NormalizedExpr, ToExprOptions}; @@ -10,7 +10,7 @@ pub(crate) struct Universe(u8); /// An expression representing a type #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) struct Type { - val: Value, + val: Nir, univ: Universe, } @@ -44,7 +44,7 @@ impl Universe { } impl Type { - pub fn new(val: Value, univ: Universe) -> Self { + pub fn new(val: Nir, univ: Universe) -> Self { Type { val, univ } } /// Creates a new Type and infers its universe by re-typechecking its value. @@ -52,7 +52,7 @@ impl Type { /// PiClosure. pub fn new_infer_universe( env: &TyEnv, - val: Value, + val: Nir, ) -> Result { let c = val.to_hir(env.as_varenv()).typecheck(env)?.ty().as_const(); let u = match c { @@ -65,7 +65,7 @@ impl Type { Ok(Type::new(val, u)) } pub fn from_const(c: Const) -> Self { - Self::new(Value::from_const(c), c.to_universe().next()) + Self::new(Nir::from_const(c), c.to_universe().next()) } pub fn from_builtin(b: Builtin) -> Self { use Builtin::*; @@ -74,7 +74,7 @@ impl Type { _ => unreachable!("this builtin is not a type: {}", b), } - Self::new(Value::from_builtin(b), Universe::from_const(Const::Type)) + Self::new(Nir::from_builtin(b), Universe::from_const(Const::Type)) } /// Get the type of this type @@ -82,19 +82,19 @@ impl Type { self.univ } - pub fn to_value(&self) -> Value { + pub fn to_nir(&self) -> Nir { self.val.clone() } - pub fn as_value(&self) -> &Value { + pub fn as_nir(&self) -> &Nir { &self.val } - pub fn into_value(self) -> Value { + pub fn into_nir(self) -> Nir { self.val } pub fn as_const(&self) -> Option { self.val.as_const() } - pub fn kind(&self) -> &ValueKind { + pub fn kind(&self) -> &NirKind { self.val.kind() } @@ -136,7 +136,7 @@ impl Tir { } /// Eval the Tir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: impl Into) -> Value { + pub fn eval(&self, env: impl Into) -> Nir { self.as_hir().eval(env.into()) } pub fn ensure_is_type(&self, env: &TyEnv) -> Result<(), TypeError> { @@ -175,11 +175,11 @@ impl Tir { } /// Eval a closed Tir (i.e. without free variables). It will actually get evaluated only as /// needed on demand. - pub fn eval_closed_expr(&self) -> Value { + pub fn eval_closed_expr(&self) -> Nir { self.eval(NzEnv::new()) } /// Eval a closed Tir fully and recursively; - pub fn rec_eval_closed_expr(&self) -> Value { + pub fn rec_eval_closed_expr(&self) -> Nir { let val = self.eval_closed_expr(); val.normalize(); val diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 7bf15af..42a9165 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -5,8 +5,8 @@ use std::collections::HashMap; use crate::error::{ErrorBuilder, TypeError, TypeMessage}; use crate::semantics::merge_maps; use crate::semantics::{ - type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Tir, TyEnv, - Type, Value, ValueKind, + type_of_builtin, Binder, BuiltinClosure, Closure, Hir, HirKind, Nir, + NirKind, Tir, TyEnv, Type, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, LitKind, Span, @@ -15,11 +15,11 @@ use crate::syntax::{ fn check_rectymerge( span: &Span, env: &TyEnv, - x: Value, - y: Value, + x: Nir, + y: Nir, ) -> Result<(), TypeError> { let kts_x = match x.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -28,7 +28,7 @@ fn check_rectymerge( } }; let kts_y = match y.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return mk_span_err( span.clone(), @@ -118,7 +118,7 @@ fn type_one_layer( ExprKind::EmptyListLit(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -139,18 +139,16 @@ fn type_one_layer( return span_err("InvalidListType"); } - let t = x.ty().to_value(); - Value::from_builtin(Builtin::List) - .app(t) - .to_type(Const::Type) + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::List).app(t).to_type(Const::Type) } ExprKind::SomeLit(x) => { if x.ty().ty().as_const() != Some(Const::Type) { return span_err("InvalidOptionalType"); } - let t = x.ty().to_value(); - Value::from_builtin(Builtin::Optional) + let t = x.ty().to_nir(); + Nir::from_builtin(Builtin::Optional) .app(t) .to_type(Const::Type) } @@ -165,7 +163,7 @@ fn type_one_layer( Entry::Occupied(_) => { return span_err("RecordTypeDuplicateField") } - Entry::Vacant(e) => e.insert(v.ty().to_value()), + Entry::Vacant(e) => e.insert(v.ty().to_nir()), }; // Check that the fields have a valid kind @@ -175,7 +173,7 @@ fn type_one_layer( } } - Value::from_kind(ValueKind::RecordType(kts)).to_type(k) + Nir::from_kind(NirKind::RecordType(kts)).to_type(k) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -230,21 +228,21 @@ fn type_one_layer( } ExprKind::Field(scrut, x) => { match scrut.ty().kind() { - ValueKind::RecordType(kts) => match kts.get(&x) { + NirKind::RecordType(kts) => match kts.get(&x) { Some(val) => Type::new_infer_universe(env, val.clone())?, None => return span_err("MissingRecordField"), }, - ValueKind::Const(_) => { + NirKind::Const(_) => { let scrut = scrut.eval_to_type(env)?; match scrut.kind() { - ValueKind::UnionType(kts) => match kts.get(x) { + NirKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - Value::from_kind(ValueKind::PiClosure { + Nir::from_kind(NirKind::PiClosure { binder: Binder::new(x.clone()), annot: ty.clone(), closure: Closure::new_constant( - scrut.to_value(), + scrut.to_nir(), ), }) .to_type(scrut.ty()) @@ -261,10 +259,8 @@ fn type_one_layer( ExprKind::Assert(t) => { let t = t.eval_to_type(env)?; match t.kind() { - ValueKind::Equivalence(x, y) if x == y => {} - ValueKind::Equivalence(..) => { - return span_err("AssertMismatch") - } + NirKind::Equivalence(x, y) if x == y => {} + NirKind::Equivalence(..) => return span_err("AssertMismatch"), _ => return span_err("AssertMustTakeEquivalence"), } t @@ -272,8 +268,8 @@ fn type_one_layer( ExprKind::App(f, arg) => { match f.ty().kind() { // TODO: store Type in closure - ValueKind::PiClosure { annot, closure, .. } => { - if arg.ty().as_value() != annot { + NirKind::PiClosure { annot, closure, .. } => { + if arg.ty().as_nir() != annot { return mkerr( ErrorBuilder::new(format!( "wrong type of function argument" @@ -318,7 +314,7 @@ fn type_one_layer( } } ExprKind::BoolIf(x, y, z) => { - if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) { + if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) { return span_err("InvalidPredicate"); } if y.ty().ty().as_const() != Some(Const::Type) { @@ -336,12 +332,12 @@ fn type_one_layer( // Extract the LHS record type let kts_x = match x_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; // Extract the RHS record type let kts_y = match y_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("MustCombineRecord"), }; @@ -352,10 +348,10 @@ fn type_one_layer( })?; let u = max(x.ty().ty(), y.ty().ty()); - Value::from_kind(ValueKind::RecordType(kts)).to_type(u) + Nir::from_kind(NirKind::RecordType(kts)).to_type(u) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { - check_rectymerge(&span, env, x.ty().to_value(), y.ty().to_value())?; + check_rectymerge(&span, env, x.ty().to_nir(), y.ty().to_nir())?; let hir = Hir::new( HirKind::Expr(ExprKind::BinOp( @@ -379,7 +375,7 @@ fn type_one_layer( } ExprKind::BinOp(BinOp::ListAppend, l, r) => { match l.ty().kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, .. }) => {} @@ -431,14 +427,14 @@ fn type_one_layer( ExprKind::Merge(record, union, type_annot) => { let record_type = record.ty(); let handlers = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("Merge1ArgMustBeRecord"), }; let union_type = union.ty(); let variants = match union_type.kind() { - ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::UnionType(kts) => Cow::Borrowed(kts), + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::Optional, args, .. @@ -457,7 +453,7 @@ fn type_one_layer( let handler_return_type: Type = match variants.get(x) { // Union alternative with type Some(Some(variant_type)) => match handler_type.kind() { - ValueKind::PiClosure { closure, annot, .. } => { + NirKind::PiClosure { closure, annot, .. } => { if variant_type != annot { return mkerr( ErrorBuilder::new(format!( @@ -578,7 +574,7 @@ fn type_one_layer( } let record_t = record.ty(); let kts = match record_t.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => { return span_err("The argument to `toMap` must be a record") } @@ -598,7 +594,7 @@ fn type_one_layer( let err_msg = "The type of `toMap x` must be of the form \ `List { mapKey : Text, mapValue : T }`"; let arg = match annot_val.kind() { - ValueKind::AppliedBuiltin(BuiltinClosure { + NirKind::AppliedBuiltin(BuiltinClosure { b: Builtin::List, args, .. @@ -606,14 +602,14 @@ fn type_one_layer( _ => return span_err(err_msg), }; let kts = match arg.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err(err_msg), }; if kts.len() != 2 { return span_err(err_msg); } match kts.get(&"mapKey".into()) { - Some(t) if *t == Value::from_builtin(Builtin::Text) => {} + Some(t) if *t == Nir::from_builtin(Builtin::Text) => {} _ => return span_err(err_msg), } match kts.get(&"mapValue".into()) { @@ -632,10 +628,10 @@ fn type_one_layer( } let mut kts = HashMap::new(); - kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); + kts.insert("mapKey".into(), Nir::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type: Type = Value::from_builtin(Builtin::List) - .app(Value::from_kind(ValueKind::RecordType(kts))) + let output_type: Type = Nir::from_builtin(Builtin::List) + .app(Nir::from_kind(NirKind::RecordType(kts))) .to_type(Const::Type); if let Some(annot) = annot { let annot_val = annot.eval_to_type(env)?; @@ -649,7 +645,7 @@ fn type_one_layer( ExprKind::Projection(record, labels) => { let record_type = record.ty(); let kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; @@ -671,19 +667,19 @@ fn type_one_layer( Type::new_infer_universe( env, - Value::from_kind(ValueKind::RecordType(new_kts)), + Nir::from_kind(NirKind::RecordType(new_kts)), )? } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.ty(); let rec_kts = match record_type.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionMustBeRecord"), }; let selection_val = selection.eval_to_type(env)?; let sel_kts = match selection_val.kind() { - ValueKind::RecordType(kts) => kts, + NirKind::RecordType(kts) => kts, _ => return span_err("ProjectionByExprTakesRecordType"), }; -- cgit v1.2.3