diff options
author | Nadrieril | 2020-02-17 18:22:06 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-17 18:22:06 +0000 |
commit | cd5e172002ce724be7bdd52883e121efa8817f20 (patch) | |
tree | b90ed1b2a0fcbec7bc26119596ac25d98918949a /dhall/src/semantics/nze/value.rs | |
parent | 2f65c02a995f6b6d4c755197fc074782f6bb100d (diff) |
Rename Value to Nir
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/nze/nir.rs (renamed from dhall/src/semantics/nze/value.rs) | 237 |
1 files changed, 116 insertions, 121 deletions
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/nir.rs index 7084af6..a6dafa2 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/nir.rs @@ -14,15 +14,16 @@ use crate::{NormalizedExpr, ToExprOptions}; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a Rc<RefCell> to share computation. -/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence +/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence /// (renaming of bound variables) and beta-equivalence (normalization). It will recursively /// normalize as needed. +/// Stands for "Normalized intermediate representation" #[derive(Clone)] -pub(crate) struct Value(Rc<ValueInternal>); +pub(crate) struct Nir(Rc<NirInternal>); #[derive(Debug)] -struct ValueInternal { - kind: lazy::Lazy<Thunk, ValueKind>, +struct NirInternal { + kind: lazy::Lazy<Thunk, NirKind>, span: Span, } @@ -32,7 +33,7 @@ pub(crate) enum Thunk { /// A completely unnormalized expression. Thunk { env: NzEnv, body: Hir }, /// A partially normalized expression that may need to go through `normalize_one_layer`. - PartialExpr { env: NzEnv, expr: ExprKind<Value> }, + PartialExpr { env: NzEnv, expr: ExprKind<Nir> }, } /// An unevaluated subexpression that takes an argument. @@ -41,101 +42,99 @@ pub(crate) enum Closure { /// Normal closure Closure { env: NzEnv, body: Hir }, /// Closure that ignores the argument passed - ConstantClosure { body: Value }, + ConstantClosure { body: Nir }, } /// A text literal with interpolations. // Invariant: this must not contain interpolations that are themselves TextLits, and contiguous // text values must be merged. #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>); +pub(crate) struct TextLit(Vec<InterpolatedTextContents<Nir>>); /// This represents a value in Weak Head Normal Form (WHNF). This means that the value is /// normalized up to the first constructor, but subexpressions may not be fully normalized. -/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in +/// When all the Nirs in a NirKind are in WHNF, and recursively so, then the NirKind is in /// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so /// if we have the first constructor of the NF at all levels, we actually have the NF. -/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and -/// we only need to recursively normalize its sub-`Value`s to get to the NF. +/// In particular, this means that once we get a `NirKind`, it can be considered immutable, and +/// we only need to recursively normalize its sub-`Nir`s to get to the NF. #[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { +pub(crate) enum NirKind { /// Closures LamClosure { binder: Binder, - annot: Value, + annot: Nir, closure: Closure, }, PiClosure { binder: Binder, - annot: Value, + annot: Nir, closure: Closure, }, - AppliedBuiltin(BuiltinClosure<Value>), + AppliedBuiltin(BuiltinClosure<Nir>), Var(NzVar), Const(Const), Lit(LitKind), - EmptyOptionalLit(Value), - NEOptionalLit(Value), + EmptyOptionalLit(Nir), + NEOptionalLit(Nir), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec<Value>), - RecordType(HashMap<Label, Value>), - RecordLit(HashMap<Label, Value>), - UnionType(HashMap<Label, Option<Value>>), - UnionConstructor(Label, HashMap<Label, Option<Value>>), - UnionLit(Label, Value, HashMap<Label, Option<Value>>), + EmptyListLit(Nir), + NEListLit(Vec<Nir>), + RecordType(HashMap<Label, Nir>), + RecordLit(HashMap<Label, Nir>), + UnionType(HashMap<Label, Option<Nir>>), + UnionConstructor(Label, HashMap<Label, Option<Nir>>), + UnionLit(Label, Nir, HashMap<Label, Option<Nir>>), TextLit(TextLit), - Equivalence(Value, Value), + Equivalence(Nir, Nir), /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. - PartialExpr(ExprKind<Value>), + PartialExpr(ExprKind<Nir>), } -impl Value { - /// Construct a Value from a completely unnormalized expression. - pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value { +impl Nir { + /// Construct a Nir from a completely unnormalized expression. + pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Nir { let span = hir.span(); - ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() + NirInternal::from_thunk(Thunk::new(env, hir), span).into_nir() } - /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind<Value>) -> Value { + /// Construct a Nir from a partially normalized expression that's not in WHNF. + pub(crate) fn from_partial_expr(e: ExprKind<Nir>) -> Nir { // TODO: env let env = NzEnv::new(); - ValueInternal::from_thunk( + NirInternal::from_thunk( Thunk::from_partial_expr(env, e), Span::Artificial, ) - .into_value() + .into_nir() } - /// Make a Value from a ValueKind - pub(crate) fn from_kind(v: ValueKind) -> Value { - ValueInternal::from_whnf(v, Span::Artificial).into_value() + /// Make a Nir from a NirKind + pub(crate) fn from_kind(v: NirKind) -> Nir { + NirInternal::from_whnf(v, Span::Artificial).into_nir() } pub(crate) fn from_const(c: Const) -> Self { - let v = ValueKind::Const(c); - ValueInternal::from_whnf(v, Span::Artificial).into_value() + let v = NirKind::Const(c); + NirInternal::from_whnf(v, Span::Artificial).into_nir() } pub(crate) fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) } pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { - Value::from_kind(ValueKind::from_builtin_env(b, env.clone())) + Nir::from_kind(NirKind::from_builtin_env(b, env.clone())) } pub(crate) fn from_text(txt: impl ToString) -> Self { - Value::from_kind(ValueKind::TextLit(TextLit::from_text( - txt.to_string(), - ))) + Nir::from_kind(NirKind::TextLit(TextLit::from_text(txt.to_string()))) } pub(crate) fn as_const(&self) -> Option<Const> { match &*self.kind() { - ValueKind::Const(c) => Some(*c), + NirKind::Const(c) => Some(*c), _ => None, } } /// This is what you want if you want to pattern-match on the value. - pub(crate) fn kind(&self) -> &ValueKind { + pub(crate) fn kind(&self) -> &NirKind { self.0.kind() } @@ -157,12 +156,12 @@ impl Value { self.0.normalize() } - pub(crate) fn app(&self, v: Value) -> Value { - Value::from_kind(apply_any(self.clone(), v)) + pub(crate) fn app(&self, v: Nir) -> Nir { + Nir::from_kind(apply_any(self.clone(), v)) } pub fn to_hir(&self, venv: VarEnv) -> Hir { - let map_uniontype = |kts: &HashMap<Label, Option<Value>>| { + let map_uniontype = |kts: &HashMap<Label, Option<Nir>>| { ExprKind::UnionType( kts.iter() .map(|(k, v)| { @@ -173,13 +172,13 @@ impl Value { }; let hir = match &*self.kind() { - ValueKind::Var(v) => HirKind::Var(venv.lookup(v)), - ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv), + NirKind::Var(v) => HirKind::Var(venv.lookup(v)), + NirKind::AppliedBuiltin(closure) => closure.to_hirkind(venv), self_kind => HirKind::Expr(match self_kind { - ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { + NirKind::Var(..) | NirKind::AppliedBuiltin(..) => { unreachable!() } - ValueKind::LamClosure { + NirKind::LamClosure { binder, annot, closure, @@ -188,7 +187,7 @@ impl Value { annot.to_hir(venv), closure.to_hir(venv), ), - ValueKind::PiClosure { + NirKind::PiClosure { binder, annot, closure, @@ -197,49 +196,47 @@ impl Value { annot.to_hir(venv), closure.to_hir(venv), ), - ValueKind::Const(c) => ExprKind::Const(*c), - ValueKind::Lit(l) => ExprKind::Lit(l.clone()), - ValueKind::EmptyOptionalLit(n) => ExprKind::App( - Value::from_builtin(Builtin::OptionalNone).to_hir(venv), + NirKind::Const(c) => ExprKind::Const(*c), + NirKind::Lit(l) => ExprKind::Lit(l.clone()), + NirKind::EmptyOptionalLit(n) => ExprKind::App( + Nir::from_builtin(Builtin::OptionalNone).to_hir(venv), n.to_hir(venv), ), - ValueKind::NEOptionalLit(n) => { - ExprKind::SomeLit(n.to_hir(venv)) - } - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( + NirKind::NEOptionalLit(n) => ExprKind::SomeLit(n.to_hir(venv)), + NirKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( HirKind::Expr(ExprKind::App( - Value::from_builtin(Builtin::List).to_hir(venv), + Nir::from_builtin(Builtin::List).to_hir(venv), n.to_hir(venv), )), Span::Artificial, )), - ValueKind::NEListLit(elts) => ExprKind::NEListLit( + NirKind::NEListLit(elts) => ExprKind::NEListLit( elts.iter().map(|v| v.to_hir(venv)).collect(), ), - ValueKind::TextLit(elts) => ExprKind::TextLit( + NirKind::TextLit(elts) => ExprKind::TextLit( elts.iter() .map(|t| t.map_ref(|v| v.to_hir(venv))) .collect(), ), - ValueKind::RecordLit(kvs) => ExprKind::RecordLit( + NirKind::RecordLit(kvs) => ExprKind::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.to_hir(venv))) .collect(), ), - ValueKind::RecordType(kts) => ExprKind::RecordType( + NirKind::RecordType(kts) => ExprKind::RecordType( kts.iter() .map(|(k, v)| (k.clone(), v.to_hir(venv))) .collect(), ), - ValueKind::UnionType(kts) => map_uniontype(kts), - ValueKind::UnionConstructor(l, kts) => ExprKind::Field( + NirKind::UnionType(kts) => map_uniontype(kts), + NirKind::UnionConstructor(l, kts) => ExprKind::Field( Hir::new( HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), ), - ValueKind::UnionLit(l, v, kts) => ExprKind::App( + NirKind::UnionLit(l, v, kts) => ExprKind::App( Hir::new( HirKind::Expr(ExprKind::Field( Hir::new( @@ -252,12 +249,12 @@ impl Value { ), v.to_hir(venv), ), - ValueKind::Equivalence(x, y) => ExprKind::BinOp( + NirKind::Equivalence(x, y) => ExprKind::BinOp( BinOp::Equivalence, x.to_hir(venv), y.to_hir(venv), ), - ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)), + NirKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)), }), }; @@ -268,24 +265,24 @@ impl Value { } } -impl ValueInternal { - fn from_whnf(k: ValueKind, span: Span) -> Self { - ValueInternal { +impl NirInternal { + fn from_whnf(k: NirKind, span: Span) -> Self { + NirInternal { kind: lazy::Lazy::new_completed(k), span, } } fn from_thunk(th: Thunk, span: Span) -> Self { - ValueInternal { + NirInternal { kind: lazy::Lazy::new(th), span, } } - fn into_value(self) -> Value { - Value(Rc::new(self)) + fn into_nir(self) -> Nir { + Nir(Rc::new(self)) } - fn kind(&self) -> &ValueKind { + fn kind(&self) -> &NirKind { &self.kind } fn normalize(&self) { @@ -293,70 +290,70 @@ impl ValueInternal { } } -impl ValueKind { - pub(crate) fn into_value(self) -> Value { - Value::from_kind(self) +impl NirKind { + pub(crate) fn into_nir(self) -> Nir { + Nir::from_kind(self) } pub(crate) fn normalize(&self) { match self { - ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {} + NirKind::Var(..) | NirKind::Const(_) | NirKind::Lit(_) => {} - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + NirKind::EmptyOptionalLit(tth) | NirKind::EmptyListLit(tth) => { tth.normalize(); } - ValueKind::NEOptionalLit(th) => { + NirKind::NEOptionalLit(th) => { th.normalize(); } - ValueKind::LamClosure { annot, closure, .. } - | ValueKind::PiClosure { annot, closure, .. } => { + NirKind::LamClosure { annot, closure, .. } + | NirKind::PiClosure { annot, closure, .. } => { annot.normalize(); closure.normalize(); } - ValueKind::AppliedBuiltin(closure) => closure.normalize(), - ValueKind::NEListLit(elts) => { + NirKind::AppliedBuiltin(closure) => closure.normalize(), + NirKind::NEListLit(elts) => { for x in elts.iter() { x.normalize(); } } - ValueKind::RecordLit(kvs) => { + NirKind::RecordLit(kvs) => { for x in kvs.values() { x.normalize(); } } - ValueKind::RecordType(kvs) => { + NirKind::RecordType(kvs) => { for x in kvs.values() { x.normalize(); } } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + NirKind::UnionType(kts) | NirKind::UnionConstructor(_, kts) => { for x in kts.values().flat_map(|opt| opt) { x.normalize(); } } - ValueKind::UnionLit(_, v, kts) => { + NirKind::UnionLit(_, v, kts) => { v.normalize(); for x in kts.values().flat_map(|opt| opt) { x.normalize(); } } - ValueKind::TextLit(tlit) => tlit.normalize(), - ValueKind::Equivalence(x, y) => { + NirKind::TextLit(tlit) => tlit.normalize(), + NirKind::Equivalence(x, y) => { x.normalize(); y.normalize(); } - ValueKind::PartialExpr(e) => { - e.map_ref(Value::normalize); + NirKind::PartialExpr(e) => { + e.map_ref(Nir::normalize); } } } - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::from_builtin_env(b, NzEnv::new()) + pub(crate) fn from_builtin(b: Builtin) -> NirKind { + NirKind::from_builtin_env(b, NzEnv::new()) } - pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { - ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env)) + pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> NirKind { + NirKind::AppliedBuiltin(BuiltinClosure::new(b, env)) } } @@ -364,10 +361,10 @@ impl Thunk { fn new(env: NzEnv, body: Hir) -> Self { Thunk::Thunk { env, body } } - fn from_partial_expr(env: NzEnv, expr: ExprKind<Value>) -> Self { + fn from_partial_expr(env: NzEnv, expr: ExprKind<Nir>) -> Self { Thunk::PartialExpr { env, expr } } - fn eval(self) -> ValueKind { + fn eval(self) -> NirKind { match self { Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body), Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), @@ -383,11 +380,11 @@ impl Closure { } } /// New closure that ignores its argument - pub fn new_constant(body: Value) -> Self { + pub fn new_constant(body: Nir) -> Self { Closure::ConstantClosure { body } } - pub fn apply(&self, val: Value) -> Value { + pub fn apply(&self, val: Nir) -> Nir { match self { Closure::Closure { env, body, .. } => { body.eval(env.insert_value(val, ())) @@ -395,10 +392,10 @@ impl Closure { Closure::ConstantClosure { body, .. } => body.clone(), } } - fn apply_var(&self, var: NzVar) -> Value { + fn apply_var(&self, var: NzVar) -> Nir { match self { Closure::Closure { .. } => { - self.apply(Value::from_kind(ValueKind::Var(var))) + self.apply(Nir::from_kind(NirKind::Var(var))) } Closure::ConstantClosure { body, .. } => body.clone(), } @@ -414,7 +411,7 @@ impl Closure { } /// If the closure variable is free in the closure, return Err. Otherwise, return the value /// with that free variable remove. - pub fn remove_binder(&self) -> Result<Value, ()> { + pub fn remove_binder(&self) -> Result<Nir, ()> { match self { Closure::Closure { .. } => { let v = NzVar::fresh(); @@ -429,11 +426,11 @@ impl Closure { impl TextLit { pub fn new( - elts: impl Iterator<Item = InterpolatedTextContents<Value>>, + elts: impl Iterator<Item = InterpolatedTextContents<Nir>>, ) -> Self { TextLit(squash_textlit(elts)) } - pub fn interpolate(v: Value) -> TextLit { + pub fn interpolate(v: Nir) -> TextLit { TextLit(vec![InterpolatedTextContents::Expr(v)]) } pub fn from_text(s: String) -> TextLit { @@ -448,7 +445,7 @@ impl TextLit { } /// If the literal consists of only one interpolation and not text, return the interpolated /// value. - pub fn as_single_expr(&self) -> Option<&Value> { + pub fn as_single_expr(&self) -> Option<&Nir> { use InterpolatedTextContents::Expr; if let [Expr(v)] = self.0.as_slice() { Some(v) @@ -467,33 +464,31 @@ impl TextLit { None } } - pub fn iter( - &self, - ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> { + pub fn iter(&self) -> impl Iterator<Item = &InterpolatedTextContents<Nir>> { self.0.iter() } /// Normalize the contained values. This does not break the invariant because we have already /// ensured that no contained values normalize to a TextLit. pub fn normalize(&self) { for x in self.0.iter() { - x.map_ref(Value::normalize); + x.map_ref(Nir::normalize); } } } -impl lazy::Eval<ValueKind> for Thunk { - fn eval(self) -> ValueKind { +impl lazy::Eval<NirKind> for Thunk { + fn eval(self) -> NirKind { self.eval() } } /// Compare two values for equality modulo alpha/beta-equivalence. -impl std::cmp::PartialEq for Value { +impl std::cmp::PartialEq for Nir { fn eq(&self, other: &Self) -> bool { Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind() } } -impl std::cmp::Eq for Value {} +impl std::cmp::Eq for Nir {} impl std::cmp::PartialEq for Thunk { fn eq(&self, _other: &Self) -> bool { @@ -512,14 +507,14 @@ impl std::cmp::PartialEq for Closure { } impl std::cmp::Eq for Closure {} -impl std::fmt::Debug for Value { +impl std::fmt::Debug for Nir { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let vint: &ValueInternal = &self.0; + let vint: &NirInternal = &self.0; let kind = vint.kind(); - if let ValueKind::Const(c) = kind { + if let NirKind::Const(c) = kind { return write!(fmt, "{:?}", c); } - let mut x = fmt.debug_struct(&format!("Value@WHNF")); + let mut x = fmt.debug_struct(&format!("Nir@WHNF")); x.field("kind", kind); x.finish() } |