summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze/nir.rs
diff options
context:
space:
mode:
authorNadrieril2020-02-17 18:22:06 +0000
committerNadrieril2020-02-17 18:22:06 +0000
commitcd5e172002ce724be7bdd52883e121efa8817f20 (patch)
treeb90ed1b2a0fcbec7bc26119596ac25d98918949a /dhall/src/semantics/nze/nir.rs
parent2f65c02a995f6b6d4c755197fc074782f6bb100d (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()
}