From fb0120dffe8e9552c3da7b994ad850f66dc612a3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:21:54 +0200 Subject: s/TypeThunk/TypedThunk/g --- dhall/src/core/value.rs | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0b68bf6..8486d6e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, X, }; -use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::thunk::{Thunk, TypedThunk}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, @@ -26,15 +26,15 @@ use crate::phase::Typed; #[derive(Debug, Clone, PartialEq, Eq)] pub enum Value { /// Closures - Lam(AlphaLabel, TypeThunk, Thunk), - Pi(AlphaLabel, TypeThunk, TypeThunk), + Lam(AlphaLabel, TypedThunk, Thunk), + Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypeThunk), + OptionalSomeClosure(TypedThunk), /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypeThunk, Option), + ListConsClosure(TypedThunk, Option), /// `λ(x : Natural) -> x + 1` NaturalSuccClosure, @@ -44,20 +44,20 @@ pub enum Value { NaturalLit(Natural), IntegerLit(Integer), DoubleLit(NaiveDouble), - EmptyOptionalLit(TypeThunk), + EmptyOptionalLit(TypedThunk), NEOptionalLit(Thunk), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypeThunk), + EmptyListLit(TypedThunk), NEListLit(Vec), RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Thunk, HashMap>), // Invariant: this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), - Equivalence(TypeThunk, TypeThunk), + Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } -- cgit v1.2.3 From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 20:54:15 +0200 Subject: Stop tracking the absence of Embed values at the type level --- dhall/src/core/value.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8486d6e..88d7a20 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use dhall_syntax::{ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, X, + NaiveDouble, Natural, }; use crate::core::thunk::{Thunk, TypedThunk}; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::{ apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, }; -use crate::phase::Typed; +use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the @@ -59,7 +59,7 @@ pub enum Value { TextLit(Vec>), Equivalence(TypedThunk, TypedThunk), // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprF), } impl Value { @@ -475,7 +475,7 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(X::clone(x)), + |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +500,7 @@ impl Subst for Value { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, )) } // Retry normalizing since substituting may allow progress -- cgit v1.2.3 From 51dbaa0b66089bca63aa9cf69a1e0ec59df053b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 21:10:59 +0200 Subject: Considerably simplify Embed handling --- dhall/src/core/value.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 88d7a20..20a6021 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -243,7 +243,7 @@ impl Value { y.normalize_to_expr_maybe_alpha(alpha), )), Value::PartialExpr(e) => { - rc(e.map_ref_simple(|v| v.normalize_to_expr_maybe_alpha(alpha))) + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } } @@ -333,8 +333,8 @@ impl Value { y.normalize_mut(); } Value::PartialExpr(e) => { - // TODO: need map_mut_simple - e.map_ref_simple(|v| { + // TODO: need map_mut + e.map_ref(|v| { v.normalize_nf(); }); } @@ -475,7 +475,6 @@ impl Shift for Value { e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - |x| Ok(Normalized::clone(x)), )?, ), }) @@ -500,7 +499,6 @@ impl Subst for Value { &val.under_binder(x), ) }, - Normalized::clone, )) } // Retry normalizing since substituting may allow progress -- cgit v1.2.3 From 67cdda53d95057174b86878f22dbc0efc0255fd9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 14 Aug 2019 22:55:00 +0200 Subject: Fix typo in normalization --- dhall/src/core/value.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 20a6021..845596b 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -107,7 +107,7 @@ impl Value { )) }; (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - rc(ExprF::Pi( + rc(ExprF::Lam( stringify!($var).into(), make_expr!($($ty)*), make_expr!($($rest)*) -- cgit v1.2.3 From aabca76a62256aa7cad66c2016ed504e49651d5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 13:06:56 +0200 Subject: Remove special closures from Value Instead construct their values directly --- dhall/src/core/value.rs | 95 +------------------------------------------------ 1 file changed, 1 insertion(+), 94 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 845596b..036a20c 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -30,13 +30,6 @@ pub enum Value { Pi(AlphaLabel, TypedThunk, TypedThunk), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), - /// `λ(x: a) -> Some x` - OptionalSomeClosure(TypedThunk), - /// `λ(x : a) -> λ(xs : List a) -> [ x ] # xs` - /// `λ(xs : List a) -> [ x ] # xs` - ListConsClosure(TypedThunk, Option), - /// `λ(x : Natural) -> x + 1` - NaturalSuccClosure, Var(AlphaVar), Const(Const), @@ -74,47 +67,6 @@ impl Value { /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - // Ad-hoc macro to help construct the unapplied closures - macro_rules! make_expr { - (Natural) => { rc(ExprF::Builtin(Builtin::Natural)) }; - (var($var:ident)) => { - rc(ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))) - }; - ($var:ident) => { $var }; - (List $($rest:tt)*) => { - rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - make_expr!($($rest)*) - )) - }; - (Some $($rest:tt)*) => { - rc(ExprF::SomeLit( - make_expr!($($rest)*) - )) - }; - (1 + $($rest:tt)*) => { - rc(ExprF::BinOp( - dhall_syntax::BinOp::NaturalPlus, - rc(ExprF::NaturalLit(1)), - make_expr!($($rest)*) - )) - }; - ([ $($head:tt)* ] # $($tail:tt)*) => { - rc(ExprF::BinOp( - dhall_syntax::BinOp::ListAppend, - rc(ExprF::NEListLit(vec![make_expr!($($head)*)])), - make_expr!($($tail)*) - )) - }; - (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { - rc(ExprF::Lam( - stringify!($var).into(), - make_expr!($($ty)*), - make_expr!($($rest)*) - )) - }; - } - match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -131,27 +83,6 @@ impl Value { } e } - Value::OptionalSomeClosure(n) => { - let a = n.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(x: a) -> Some var(x)) - } - Value::ListConsClosure(a, None) => { - // Avoid accidental capture of the new `x` variable - let a1 = a.under_binder(Label::from("x")); - let a1 = a1.normalize_to_expr_maybe_alpha(alpha); - let a = a.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(x : a) -> λ(xs : List a1) -> [ var(x) ] # var(xs)) - } - Value::ListConsClosure(n, Some(v)) => { - // Avoid accidental capture of the new `xs` variable - let v = v.under_binder(Label::from("xs")); - let v = v.normalize_to_expr_maybe_alpha(alpha); - let a = n.normalize_to_expr_maybe_alpha(alpha); - make_expr!(λ(xs : List a) -> [ v ] # var(xs)) - } - Value::NaturalSuccClosure => { - make_expr!(λ(x : Natural) -> 1 + var(x)) - } Value::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), t.normalize_to_expr_maybe_alpha(alpha), @@ -257,8 +188,7 @@ impl Value { pub fn normalize_mut(&mut self) { match self { - Value::NaturalSuccClosure - | Value::Var(_) + Value::Var(_) | Value::Const(_) | Value::BoolLit(_) | Value::NaturalLit(_) @@ -266,7 +196,6 @@ impl Value { | Value::DoubleLit(_) => {} Value::EmptyOptionalLit(tth) - | Value::OptionalSomeClosure(tth) | Value::EmptyListLit(tth) => { tth.normalize_mut(); } @@ -287,12 +216,6 @@ impl Value { x.normalize_mut(); } } - Value::ListConsClosure(t, v) => { - t.normalize_mut(); - for x in v.iter_mut() { - x.normalize_mut(); - } - } Value::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); @@ -375,14 +298,6 @@ impl Shift for Value { .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.shift(delta, var)?) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.shift(delta, var)?, - v.as_ref().map(|v| Ok(v.shift(delta, var)?)).transpose()?, - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.shift(delta, var)?, @@ -516,14 +431,6 @@ impl Subst for Value { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::NaturalSuccClosure => Value::NaturalSuccClosure, - Value::OptionalSomeClosure(tth) => { - Value::OptionalSomeClosure(tth.subst_shift(var, val)) - } - Value::ListConsClosure(t, v) => Value::ListConsClosure( - t.subst_shift(var, val), - v.as_ref().map(|v| v.subst_shift(var, val)), - ), Value::Pi(x, t, e) => Value::Pi( x.clone(), t.subst_shift(var, val), -- cgit v1.2.3 From 9e38d92bf481da8e34081c81c813acd802efa016 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 22:03:41 +0200 Subject: Fix variable substitution I have no idea how this didn't get caught before --- dhall/src/core/value.rs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 036a20c..75ef5a5 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -436,10 +436,8 @@ impl Subst for Value { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::Var(v) => match v.shift(-1, var) { - None => val.to_value().clone(), - Some(newvar) => Value::Var(newvar), - }, + Value::Var(v) if v == var => val.to_value(), + Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()), Value::Const(c) => Value::Const(*c), Value::BoolLit(b) => Value::BoolLit(*b), Value::NaturalLit(n) => Value::NaturalLit(*n), -- cgit v1.2.3 From 91ba644fa47c29feb57dba957ee8aa115ed95fef Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 22:12:25 +0200 Subject: rustfmt --- dhall/src/core/value.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 75ef5a5..19be56a 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -195,8 +195,7 @@ impl Value { | Value::IntegerLit(_) | Value::DoubleLit(_) => {} - Value::EmptyOptionalLit(tth) - | Value::EmptyListLit(tth) => { + Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => { tth.normalize_mut(); } -- cgit v1.2.3 From 88ebc0f9d561a2541aad84a3152511a0439db8b4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 17:56:19 +0200 Subject: Reduce api surface of dhall crate Helps detect unused code --- dhall/src/core/value.rs | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 19be56a..61a8eea 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -56,17 +56,17 @@ pub enum Value { } impl Value { - pub fn into_thunk(self) -> Thunk { + pub(crate) fn into_thunk(self) -> Thunk { Thunk::from_value(self) } /// Convert the value to a fully normalized syntactic expression - pub fn normalize_to_expr(&self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { self.normalize_to_expr_maybe_alpha(false) } /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -179,14 +179,7 @@ impl Value { } } - // Deprecated - pub fn normalize(&self) -> Value { - let mut v = self.clone(); - v.normalize_mut(); - v - } - - pub fn normalize_mut(&mut self) { + pub(crate) fn normalize_mut(&mut self) { match self { Value::Var(_) | Value::Const(_) @@ -264,12 +257,12 @@ impl Value { } /// Apply to a value - pub fn app(self, val: Value) -> Value { + pub(crate) fn app(self, val: Value) -> Value { self.app_val(val) } /// Apply to a value - pub fn app_val(self, val: Value) -> Value { + pub(crate) fn app_val(self, val: Value) -> Value { self.app_thunk(val.into_thunk()) } -- cgit v1.2.3 From 5f0d69671b44ba1dff6becb9ebc7f6e74241e3e2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 18:14:55 +0200 Subject: Remove dead code --- dhall/src/core/value.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 61a8eea..d3d017d 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -66,7 +66,10 @@ impl Value { } /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize /// if alpha is `true` - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), -- cgit v1.2.3 From e0f5216215ccb7a4df85d80e11dd265cdb52a44f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:47:36 +0200 Subject: s/Value/ValueF/ --- dhall/src/core/value.rs | 212 ++++++++++++++++++++++++------------------------ 1 file changed, 106 insertions(+), 106 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index d3d017d..0f2ef00 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -15,16 +15,16 @@ use crate::phase::{Normalized, Typed}; /// A semantic value. The invariants ensure this value represents a Weak-Head /// Normal Form (WHNF). This means that this first constructor is the first constructor of the /// final Normal Form (NF). -/// This WHNF must be preserved by operations on `Value`s. In particular, `subst_shift` could break +/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break /// the invariants so need to be careful to reevaluate as needed. /// Subexpressions are Thunks, which are partially evaluated expressions that are normalized -/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the -/// Value is in NF. This is because WHNF ensures that we have the first constructor of the NF; so +/// on-demand. When all the Thunks in a ValueF are at least in WHNF, and recursively so, then the +/// ValueF is in 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. /// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence /// (normalization). Equality will normalize only as needed. #[derive(Debug, Clone, PartialEq, Eq)] -pub enum Value { +pub enum ValueF { /// Closures Lam(AlphaLabel, TypedThunk, Thunk), Pi(AlphaLabel, TypedThunk, TypedThunk), @@ -55,9 +55,9 @@ pub enum Value { PartialExpr(ExprF), } -impl Value { +impl ValueF { pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_value(self) + Thunk::from_valuef(self) } /// Convert the value to a fully normalized syntactic expression @@ -71,12 +71,12 @@ impl Value { alpha: bool, ) -> OutputSubExpr { match self { - Value::Lam(x, t, e) => rc(ExprF::Lam( + ValueF::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), t.normalize_to_expr_maybe_alpha(alpha), e.normalize_to_expr_maybe_alpha(alpha), )), - Value::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(b, args) => { let mut e = rc(ExprF::Builtin(*b)); for v in args { e = rc(ExprF::App( @@ -86,48 +86,48 @@ impl Value { } e } - Value::Pi(x, t, e) => rc(ExprF::Pi( + ValueF::Pi(x, t, e) => rc(ExprF::Pi( x.to_label_maybe_alpha(alpha), t.normalize_to_expr_maybe_alpha(alpha), e.normalize_to_expr_maybe_alpha(alpha), )), - Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))), - Value::Const(c) => rc(ExprF::Const(*c)), - Value::BoolLit(b) => rc(ExprF::BoolLit(*b)), - Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - Value::EmptyOptionalLit(n) => rc(ExprF::App( + ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), + ValueF::Const(c) => rc(ExprF::Const(*c)), + ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueF::EmptyOptionalLit(n) => rc(ExprF::App( rc(ExprF::Builtin(Builtin::OptionalNone)), n.normalize_to_expr_maybe_alpha(alpha), )), - Value::NEOptionalLit(n) => { + ValueF::NEOptionalLit(n) => { rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) } - Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( rc(ExprF::Builtin(Builtin::List)), n.normalize_to_expr_maybe_alpha(alpha), )))), - Value::NEListLit(elts) => rc(ExprF::NEListLit( + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( elts.iter() .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) .collect(), )), - Value::RecordLit(kvs) => rc(ExprF::RecordLit( + ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( kvs.iter() .map(|(k, v)| { (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) }) .collect(), )), - Value::RecordType(kts) => rc(ExprF::RecordType( + ValueF::RecordType(kts) => rc(ExprF::RecordType( kts.iter() .map(|(k, v)| { (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) }) .collect(), )), - Value::UnionType(kts) => rc(ExprF::UnionType( + ValueF::UnionType(kts) => rc(ExprF::UnionType( kts.iter() .map(|(k, v)| { ( @@ -139,7 +139,7 @@ impl Value { }) .collect(), )), - Value::UnionConstructor(l, kts) => { + ValueF::UnionConstructor(l, kts) => { let kts = kts .iter() .map(|(k, v)| { @@ -153,12 +153,12 @@ impl Value { .collect(); rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } - Value::UnionLit(l, v, kts) => rc(ExprF::App( - Value::UnionConstructor(l.clone(), kts.clone()) + ValueF::UnionLit(l, v, kts) => rc(ExprF::App( + ValueF::UnionConstructor(l.clone(), kts.clone()) .normalize_to_expr_maybe_alpha(alpha), v.normalize_to_expr_maybe_alpha(alpha), )), - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { use InterpolatedTextContents::{Expr, Text}; rc(ExprF::TextLit( elts.iter() @@ -171,12 +171,12 @@ impl Value { .collect(), )) } - Value::Equivalence(x, y) => rc(ExprF::BinOp( + ValueF::Equivalence(x, y) => rc(ExprF::BinOp( dhall_syntax::BinOp::Equivalence, x.normalize_to_expr_maybe_alpha(alpha), y.normalize_to_expr_maybe_alpha(alpha), )), - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } @@ -184,60 +184,60 @@ impl Value { pub(crate) fn normalize_mut(&mut self) { match self { - Value::Var(_) - | Value::Const(_) - | Value::BoolLit(_) - | Value::NaturalLit(_) - | Value::IntegerLit(_) - | Value::DoubleLit(_) => {} + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} - Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => { + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { tth.normalize_mut(); } - Value::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th) => { th.normalize_mut(); } - Value::Lam(_, t, e) => { + ValueF::Lam(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::Pi(_, t, e) => { + ValueF::Pi(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::AppliedBuiltin(_, args) => { + ValueF::AppliedBuiltin(_, args) => { for x in args.iter_mut() { x.normalize_mut(); } } - Value::NEListLit(elts) => { + ValueF::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); } } - Value::RecordLit(kvs) => { + ValueF::RecordLit(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::RecordType(kvs) => { + ValueF::RecordType(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::UnionType(kts) | Value::UnionConstructor(_, kts) => { + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::UnionLit(_, v, kts) => { + ValueF::UnionLit(_, v, kts) => { v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { for x in elts.iter_mut() { use InterpolatedTextContents::{Expr, Text}; match x { @@ -246,11 +246,11 @@ impl Value { } } } - Value::Equivalence(x, y) => { + ValueF::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); } - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { // TODO: need map_mut e.map_ref(|v| { v.normalize_nf(); @@ -260,75 +260,75 @@ impl Value { } /// Apply to a value - pub(crate) fn app(self, val: Value) -> Value { + pub(crate) fn app(self, val: ValueF) -> ValueF { self.app_val(val) } /// Apply to a value - pub(crate) fn app_val(self, val: Value) -> Value { + pub(crate) fn app_val(self, val: ValueF) -> ValueF { self.app_thunk(val.into_thunk()) } /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> Value { - Thunk::from_value(self).app_thunk(th) + pub fn app_thunk(self, th: Thunk) -> ValueF { + Thunk::from_valuef(self).app_thunk(th) } - pub fn from_builtin(b: Builtin) -> Value { - Value::AppliedBuiltin(b, vec![]) + pub fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) } } -impl Shift for Value { +impl Shift for ValueF { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - Value::Lam(x, t, e) => Value::Lam( + ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin( *b, args.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::Pi(x, t, e) => Value::Pi( + ValueF::Pi(x, t, e) => ValueF::Pi( x.clone(), t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - Value::Var(v) => Value::Var(v.shift(delta, var)?), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.shift(delta, var)?) + ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.shift(delta, var)?) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.shift(delta, var)?) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.shift(delta, var)?) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::UnionType( kts.iter() .map(|(k, v)| { Ok(( @@ -340,7 +340,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -353,7 +353,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.shift(delta, var)?, kts.iter() @@ -367,7 +367,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::TextLit(elts) => Value::TextLit( + ValueF::TextLit(elts) => ValueF::TextLit( elts.iter() .map(|contents| { use InterpolatedTextContents::{Expr, Text}; @@ -378,10 +378,10 @@ impl Shift for Value { }) .collect::>()?, ), - Value::Equivalence(x, y) => { - Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) } - Value::PartialExpr(e) => Value::PartialExpr( + ValueF::PartialExpr(e) => ValueF::PartialExpr( e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), @@ -391,16 +391,16 @@ impl Shift for Value { } } -impl Subst for Value { +impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { // Retry normalizing since substituting may allow progress - Value::AppliedBuiltin(b, args) => apply_builtin( + ValueF::AppliedBuiltin(b, args) => apply_builtin( *b, args.iter().map(|v| v.subst_shift(var, val)).collect(), ), // Retry normalizing since substituting may allow progress - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { normalize_one_layer(e.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), |x, v| { @@ -412,8 +412,8 @@ impl Subst for Value { )) } // Retry normalizing since substituting may allow progress - Value::TextLit(elts) => { - Value::TextLit(squash_textlit(elts.iter().map(|contents| { + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.iter().map(|contents| { use InterpolatedTextContents::{Expr, Text}; match contents { Expr(th) => Expr(th.subst_shift(var, val)), @@ -421,53 +421,53 @@ impl Subst for Value { } }))) } - Value::Lam(x, t, e) => Value::Lam( + ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::Pi(x, t, e) => Value::Pi( + ValueF::Pi(x, t, e) => ValueF::Pi( x.clone(), t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - Value::Var(v) if v == var => val.to_value(), - Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.subst_shift(var, val)) + ValueF::Var(v) if v == var => val.to_valuef(), + ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.subst_shift(var, val)) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.subst_shift(var, val)) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter().map(|v| v.subst_shift(var, val)).collect(), ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::UnionType( kts.iter() .map(|(k, v)| { (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) }) .collect(), ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -475,7 +475,7 @@ impl Subst for Value { }) .collect(), ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.subst_shift(var, val), kts.iter() @@ -484,7 +484,7 @@ impl Subst for Value { }) .collect(), ), - Value::Equivalence(x, y) => Value::Equivalence( + ValueF::Equivalence(x, y) => ValueF::Equivalence( x.subst_shift(var, val), y.subst_shift(var, val), ), -- cgit v1.2.3 From cc0c6cc420ca8019665e745797758c997cc35358 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 22:33:16 +0200 Subject: Use generic Shift/Subst impls --- dhall/src/core/value.rs | 168 ++++++++++++------------------------------------ 1 file changed, 40 insertions(+), 128 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0f2ef00..da70118 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -287,12 +287,9 @@ impl Shift for ValueF { t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin( - *b, - args.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::>()?, - ), + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) + } ValueF::Pi(x, t, e) => ValueF::Pi( x.clone(), t.shift(delta, var)?, @@ -313,80 +310,27 @@ impl Shift for ValueF { ValueF::EmptyListLit(tth) => { ValueF::EmptyListLit(tth.shift(delta, var)?) } - ValueF::NEListLit(elts) => ValueF::NEListLit( - elts.iter() - .map(|v| Ok(v.shift(delta, var)?)) - .collect::>()?, - ), - ValueF::RecordLit(kvs) => ValueF::RecordLit( - kvs.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::>()?, - ), - ValueF::RecordType(kvs) => ValueF::RecordType( - kvs.iter() - .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) - .collect::>()?, - ), - ValueF::UnionType(kts) => ValueF::UnionType( - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::>()?, - ), - ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( - x.clone(), - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::>()?, - ), + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.shift(delta, var)?) + } + ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.shift(delta, var)?) + } + ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.shift(delta, var)?, - kts.iter() - .map(|(k, v)| { - Ok(( - k.clone(), - v.as_ref() - .map(|v| Ok(v.shift(delta, var)?)) - .transpose()?, - )) - }) - .collect::>()?, - ), - ValueF::TextLit(elts) => ValueF::TextLit( - elts.iter() - .map(|contents| { - use InterpolatedTextContents::{Expr, Text}; - Ok(match contents { - Expr(th) => Expr(th.shift(delta, var)?), - Text(s) => Text(s.clone()), - }) - }) - .collect::>()?, + kts.shift(delta, var)?, ), + ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), ValueF::Equivalence(x, y) => { ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) } - ValueF::PartialExpr(e) => ValueF::PartialExpr( - e.traverse_ref_with_special_handling_of_binders( - |v| Ok(v.shift(delta, var)?), - |x, v| Ok(v.shift(delta, &var.under_binder(x))?), - )?, - ), + ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), }) } } @@ -395,32 +339,17 @@ impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { // Retry normalizing since substituting may allow progress - ValueF::AppliedBuiltin(b, args) => apply_builtin( - *b, - args.iter().map(|v| v.subst_shift(var, val)).collect(), - ), + ValueF::AppliedBuiltin(b, args) => { + apply_builtin(*b, args.subst_shift(var, val)) + } // Retry normalizing since substituting may allow progress ValueF::PartialExpr(e) => { - normalize_one_layer(e.map_ref_with_special_handling_of_binders( - |v| v.subst_shift(var, val), - |x, v| { - v.subst_shift( - &var.under_binder(x), - &val.under_binder(x), - ) - }, - )) + normalize_one_layer(e.subst_shift(var, val)) } // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => { - ValueF::TextLit(squash_textlit(elts.iter().map(|contents| { - use InterpolatedTextContents::{Expr, Text}; - match contents { - Expr(th) => Expr(th.subst_shift(var, val)), - Text(s) => Text(s.clone()), - } - }))) - } + ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( + elts.iter().map(|contents| contents.subst_shift(var, val)), + )), ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.subst_shift(var, val), @@ -447,42 +376,25 @@ impl Subst for ValueF { ValueF::EmptyListLit(tth) => { ValueF::EmptyListLit(tth.subst_shift(var, val)) } - ValueF::NEListLit(elts) => ValueF::NEListLit( - elts.iter().map(|v| v.subst_shift(var, val)).collect(), - ), - ValueF::RecordLit(kvs) => ValueF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect(), - ), - ValueF::RecordType(kvs) => ValueF::RecordType( - kvs.iter() - .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) - .collect(), - ), - ValueF::UnionType(kts) => ValueF::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), - ), - ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( - x.clone(), - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), - ), + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.subst_shift(var, val)) + } + ValueF::RecordLit(kvs) => { + ValueF::RecordLit(kvs.subst_shift(var, val)) + } + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.subst_shift(var, val)) + } + ValueF::UnionType(kts) => { + ValueF::UnionType(kts.subst_shift(var, val)) + } + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + } ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.subst_shift(var, val), - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) - }) - .collect(), + kts.subst_shift(var, val), ), ValueF::Equivalence(x, y) => ValueF::Equivalence( x.subst_shift(var, val), -- cgit v1.2.3 From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Aug 2019 19:00:43 +0200 Subject: s/Thunk/Value/ --- dhall/src/core/value.rs | 723 ++++++++++++++++++++++++------------------------ 1 file changed, 362 insertions(+), 361 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index da70118..5c29bf0 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,405 +1,406 @@ -use std::collections::HashMap; - -use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -use crate::core::thunk::{Thunk, TypedThunk}; -use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::{ - apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, -}; -use crate::phase::{Normalized, Typed}; - -/// A semantic value. The invariants ensure this value represents a Weak-Head -/// Normal Form (WHNF). This means that this first constructor is the first constructor of the -/// final Normal Form (NF). -/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break -/// the invariants so need to be careful to reevaluate as needed. -/// Subexpressions are Thunks, which are partially evaluated expressions that are normalized -/// on-demand. When all the Thunks in a ValueF are at least in WHNF, and recursively so, then the -/// ValueF is in 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. -/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize only as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum ValueF { - /// Closures - Lam(AlphaLabel, TypedThunk, Thunk), - Pi(AlphaLabel, TypedThunk, TypedThunk), - // Invariant: the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec), - - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(TypedThunk), - NEOptionalLit(Thunk), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedThunk), - NEListLit(Vec), - RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), - // Invariant: this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(TypedThunk, TypedThunk), - // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), +use std::borrow::Cow; +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; + +use dhall_syntax::{Const, ExprF}; + +use crate::core::context::TypecheckContext; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; + +#[derive(Debug, Clone, Copy)] +enum Marker { + /// Weak Head Normal Form, i.e. subexpressions may not be normalized + WHNF, + /// Normal form, i.e. completely normalized + NF, } +use Marker::{NF, WHNF}; -impl ValueF { - pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_valuef(self) - } +#[derive(Debug, Clone)] +enum ValueInternal { + /// Partially normalized value whose subexpressions have been thunked (this is returned from + /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no + /// requirement of WHNF here. + PartialExpr(ExprF), + /// Partially normalized value. + /// Invariant: if the marker is `NF`, the value must be fully normalized + ValueF(Marker, ValueF), +} - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) +#[derive(Debug)] +struct TypedValueInternal { + internal: ValueInternal, + typ: Option, +} + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a Type from typechecking to preserve type information through +/// normalization. +#[derive(Clone)] +pub struct Value(Rc>); + +#[derive(Debug, Clone)] +pub struct TypedValue(Value); + +impl ValueInternal { + fn into_value(self, t: Option) -> Value { + TypedValueInternal { + internal: self, + typ: t, + } + .into_value() } - /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize - /// if alpha is `true` - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { + + fn normalize_whnf(&mut self) { match self { - ValueF::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::AppliedBuiltin(b, args) => { - let mut e = rc(ExprF::Builtin(*b)); - for v in args { - e = rc(ExprF::App( - e, - v.normalize_to_expr_maybe_alpha(alpha), - )); - } - e + ValueInternal::PartialExpr(e) => { + *self = + ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } - ValueF::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), - ValueF::Const(c) => rc(ExprF::Const(*c)), - ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueF::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} + } + } + + fn normalize_nf(&mut self) { + match self { + ValueInternal::PartialExpr(_) => { + self.normalize_whnf(); + self.normalize_nf(); } - ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.normalize_to_expr_maybe_alpha(alpha), - )))), - ValueF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter() - .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) - .collect(), - )), - ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - ValueF::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - ValueF::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(), - )), - ValueF::UnionConstructor(l, kts) => { - let kts = kts - .iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) + ValueInternal::ValueF(m @ WHNF, v) => { + v.normalize_mut(); + *m = NF; } - ValueF::UnionLit(l, v, kts) => rc(ExprF::App( - ValueF::UnionConstructor(l.clone(), kts.clone()) - .normalize_to_expr_maybe_alpha(alpha), - v.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::TextLit(elts) => { - use InterpolatedTextContents::{Expr, Text}; - rc(ExprF::TextLit( - elts.iter() - .map(|contents| match contents { - Expr(e) => { - Expr(e.normalize_to_expr_maybe_alpha(alpha)) - } - Text(s) => Text(s.clone()), - }) - .collect(), - )) + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } + } + + // Always use normalize_whnf before + fn as_whnf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(_, v) => v, + } + } + + // Always use normalize_nf before + fn as_nf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + unreachable!() } - ValueF::Equivalence(x, y) => rc(ExprF::BinOp( - dhall_syntax::BinOp::Equivalence, - x.normalize_to_expr_maybe_alpha(alpha), - y.normalize_to_expr_maybe_alpha(alpha), + ValueInternal::ValueF(NF, v) => v, + } + } +} + +impl TypedValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_internal(&self) -> &ValueInternal { + &self.internal + } + fn as_internal_mut(&mut self) -> &mut ValueInternal { + &mut self.internal + } + + fn get_type(&self) -> Result { + match &self.typ { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, )), - ValueF::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } } } +} +impl Value { + pub(crate) fn from_valuef(v: ValueF) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(None) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + } + pub(crate) fn from_partial_expr(e: ExprF) -> Value { + ValueInternal::PartialExpr(e).into_value(None) + } + pub(crate) fn with_type(self, t: Type) -> Value { + self.as_internal().clone().into_value(Some(t)) + } + + /// Mutates the contents. If no one else shares this thunk, + /// mutates directly, thus avoiding a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) { + match Rc::get_mut(&mut self.0) { + // Mutate directly if sole owner + Some(refcell) => f(RefCell::get_mut(refcell)), + // Otherwise mutate through the refcell + None => f(&mut self.as_tinternal_mut()), + } + } + + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this thunk pub(crate) fn normalize_mut(&mut self) { - match self { - ValueF::Var(_) - | ValueF::Const(_) - | ValueF::BoolLit(_) - | ValueF::NaturalLit(_) - | ValueF::IntegerLit(_) - | ValueF::DoubleLit(_) => {} - - ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { - tth.normalize_mut(); - } + self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) + } - ValueF::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueF::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueF::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueF::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::TextLit(elts) => { - for x in elts.iter_mut() { - use InterpolatedTextContents::{Expr, Text}; - match x { - Expr(n) => n.normalize_mut(), - Text(_) => {} - } - } - } - ValueF::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueF::PartialExpr(e) => { - // TODO: need map_mut - e.map_ref(|v| { - v.normalize_nf(); - }); - } + fn as_tinternal(&self) -> Ref { + self.0.borrow() + } + fn as_tinternal_mut(&mut self) -> RefMut { + self.0.borrow_mut() + } + fn as_internal(&self) -> Ref { + Ref::map(self.as_tinternal(), TypedValueInternal::as_internal) + } + fn as_internal_mut(&self) -> RefMut { + RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut) + } + + fn do_normalize_whnf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); + } + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} } } - /// Apply to a value - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_val(val) + fn do_normalize_nf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + drop(borrow); + self.as_internal_mut().normalize_nf(); + } + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } } - /// Apply to a value - pub(crate) fn app_val(self, val: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn normalize_nf(&self) -> Ref { + self.do_normalize_nf(); + Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> ValueF { - Thunk::from_valuef(self).app_thunk(th) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn as_valuef(&self) -> Ref { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) } - pub fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) + pub(crate) fn to_valuef(&self) -> ValueF { + self.as_valuef().clone() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + pub(crate) fn app_value(&self, th: Value) -> ValueF { + apply_any(self.clone(), th) + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + Ok(Cow::Owned(self.as_tinternal().get_type()?)) } } -impl Shift for ValueF { +impl TypedValue { + pub(crate) fn from_valuef(v: ValueF) -> TypedValue { + TypedValue::from_value_untyped(Value::from_valuef(v)) + } + + pub(crate) fn from_type(t: Type) -> TypedValue { + t.into_typedvalue() + } + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.normalize_nf().clone() + } + + pub(crate) fn to_typed(&self) -> Typed { + self.clone().into_typed() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { + TypedValue(th.with_type(t)) + } + pub fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value_and_type(th, Type::const_type()) + } + pub(crate) fn from_value_untyped(th: Value) -> Self { + TypedValue(th) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + } + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) + } + + pub(crate) fn to_valuef(&self) -> ValueF { + self.0.to_valuef() + } + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr_maybe_alpha(true) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn to_type(&self) -> Type { + self.clone().into_typed().into_type() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_typedvalue(self) + } + pub(crate) fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + pub(crate) fn normalize_mut(&mut self) { + self.0.normalize_mut() + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + self.0.get_type() + } +} + +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Value(self.0.shift(delta, var)?)) + } +} + +impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::AppliedBuiltin(b, args) => { - ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.shift(delta, var)?) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.shift(delta, var)?) } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.shift(delta, var)?) + ValueInternal::ValueF(m, v) => { + ValueInternal::ValueF(*m, v.shift(delta, var)?) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.shift(delta, var)?) - } - ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.shift(delta, var)?) - } - ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), - ValueF::Equivalence(x, y) => { - ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) - } - ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), }) } } -impl Subst for ValueF { +impl Shift for TypedValue { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValue(self.0.shift(delta, var)?)) + } +} + +impl Shift for TypedValueInternal { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValueInternal { + internal: self.internal.shift(delta, var)?, + typ: self.typ.shift(delta, var)?, + }) + } +} + +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + Value(self.0.subst_shift(var, val)) + } +} + +impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - // Retry normalizing since substituting may allow progress - ValueF::AppliedBuiltin(b, args) => { - apply_builtin(*b, args.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::PartialExpr(e) => { - normalize_one_layer(e.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( - elts.iter().map(|contents| contents.subst_shift(var, val)), - )), - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Var(v) if v == var => val.to_valuef(), - ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.subst_shift(var, val)) - } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.subst_shift(var, val)) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.subst_shift(var, val)) + ValueInternal::ValueF(_, v) => { + // The resulting value may not stay in normal form after substitution + ValueInternal::ValueF(WHNF, v.subst_shift(var, val)) } - ValueF::RecordLit(kvs) => { - ValueF::RecordLit(kvs.subst_shift(var, val)) - } - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.subst_shift(var, val)) - } - ValueF::UnionType(kts) => { - ValueF::UnionType(kts.subst_shift(var, val)) + } + } +} + +impl Subst for TypedValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValueInternal { + internal: self.internal.subst_shift(var, val), + typ: self.typ.subst_shift(var, val), + } + } +} + +impl Subst for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValue(self.0.subst_shift(var, val)) + } +} + +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.as_valuef() == *other.as_valuef() + } +} +impl std::cmp::Eq for Value {} + +impl std::cmp::PartialEq for TypedValue { + fn eq(&self, other: &Self) -> bool { + self.to_valuef() == other.to_valuef() + } +} +impl std::cmp::Eq for TypedValue {} + +impl std::fmt::Debug for Value { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let b: &ValueInternal = &self.as_internal(); + match b { + ValueInternal::ValueF(m, v) => { + f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + f.debug_tuple("Value@PartialExpr").field(e).finish() } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueF::Equivalence(x, y) => ValueF::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), } } } -- cgit v1.2.3 From c7d9a8659214a228963ea40d76e361bbc08129bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 18 Aug 2019 15:24:13 +0200 Subject: Rework ValueInternal and clarify invariants around ValueF --- dhall/src/core/value.rs | 103 +++++++++++++++++++++++++----------------------- 1 file changed, 54 insertions(+), 49 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5c29bf0..19976af 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -8,28 +8,32 @@ use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; +use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; use crate::phase::typecheck::type_of_const; use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] -enum Marker { - /// Weak Head Normal Form, i.e. subexpressions may not be normalized +enum Form { + /// No constraints; expression may not be normalized at all. + Unevaled, + /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may + /// not be normalized. This means that the first constructor of the contained ValueF is the first + /// constructor of the final Normal Form (NF). WHNF, - /// Normal form, i.e. completely normalized + /// Normal Form, i.e. completely normalized. + /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the + /// ValueF is in 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. NF, } -use Marker::{NF, WHNF}; +use Form::{Unevaled, NF, WHNF}; #[derive(Debug, Clone)] enum ValueInternal { - /// Partially normalized value whose subexpressions have been thunked (this is returned from - /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no - /// requirement of WHNF here. - PartialExpr(ExprF), /// Partially normalized value. + /// Invariant: if the marker is `WHNF`, the value must be in Weak Head Normal Form /// Invariant: if the marker is `NF`, the value must be fully normalized - ValueF(Marker, ValueF), + ValueF(Form, ValueF), } #[derive(Debug)] @@ -45,6 +49,8 @@ struct TypedValueInternal { #[derive(Clone)] pub struct Value(Rc>); +/// A value that needs to carry a type for typechecking to work. +/// TODO: actually enforce this. #[derive(Debug, Clone)] pub struct TypedValue(Value); @@ -58,25 +64,25 @@ impl ValueInternal { } fn normalize_whnf(&mut self) { - match self { - ValueInternal::PartialExpr(e) => { - *self = - ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) + take_mut::take(self, |vint| match vint { + ValueInternal::ValueF(Unevaled, v) => { + ValueInternal::ValueF(WHNF, normalize_whnf(v)) } - // Already at least in WHNF - ValueInternal::ValueF(_, _) => {} - } + // Already in WHNF + vint @ ValueInternal::ValueF(WHNF, _) + | vint @ ValueInternal::ValueF(NF, _) => vint, + }) } fn normalize_nf(&mut self) { match self { - ValueInternal::PartialExpr(_) => { + ValueInternal::ValueF(Unevaled, _) => { self.normalize_whnf(); self.normalize_nf(); } - ValueInternal::ValueF(m @ WHNF, v) => { + ValueInternal::ValueF(f @ WHNF, v) => { v.normalize_mut(); - *m = NF; + *f = NF; } // Already in NF ValueInternal::ValueF(NF, _) => {} @@ -86,7 +92,7 @@ impl ValueInternal { // Always use normalize_whnf before fn as_whnf(&self) -> &ValueF { match self { - ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(Unevaled, _) => unreachable!(), ValueInternal::ValueF(_, v) => v, } } @@ -94,9 +100,8 @@ impl ValueInternal { // Always use normalize_nf before fn as_nf(&self) -> &ValueF { match self { - ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { - unreachable!() - } + ValueInternal::ValueF(Unevaled, _) + | ValueInternal::ValueF(WHNF, _) => unreachable!(), ValueInternal::ValueF(NF, v) => v, } } @@ -126,13 +131,13 @@ impl TypedValueInternal { impl Value { pub(crate) fn from_valuef(v: ValueF) -> Value { - ValueInternal::ValueF(WHNF, v).into_value(None) + ValueInternal::ValueF(Unevaled, v).into_value(None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { - ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + ValueInternal::ValueF(Unevaled, v).into_value(Some(t)) } pub(crate) fn from_partial_expr(e: ExprF) -> Value { - ValueInternal::PartialExpr(e).into_value(None) + Value::from_valuef(ValueF::PartialExpr(e)) } pub(crate) fn with_type(self, t: Type) -> Value { self.as_internal().clone().into_value(Some(t)) @@ -150,7 +155,7 @@ impl Value { } /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this thunk + /// no one else shares this thunk. pub(crate) fn normalize_mut(&mut self) { self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) } @@ -171,19 +176,20 @@ impl Value { fn do_normalize_whnf(&self) { let borrow = self.as_internal(); match &*borrow { - ValueInternal::PartialExpr(_) => { + ValueInternal::ValueF(Unevaled, _) => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already at least in WHNF - ValueInternal::ValueF(_, _) => {} + ValueInternal::ValueF(WHNF, _) | ValueInternal::ValueF(NF, _) => {} } } fn do_normalize_nf(&self) { let borrow = self.as_internal(); match &*borrow { - ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + ValueInternal::ValueF(Unevaled, _) + | ValueInternal::ValueF(WHNF, _) => { drop(borrow); self.as_internal_mut().normalize_nf(); } @@ -199,13 +205,21 @@ impl Value { Ref::map(self.as_internal(), ValueInternal::as_nf) } - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + /// TODO: deprecated because of misleading name pub(crate) fn as_valuef(&self) -> Ref { + self.as_whnf() + } + + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + pub(crate) fn as_whnf(&self) -> Ref { self.do_normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_whnf) } + /// TODO: deprecated because of misleading name pub(crate) fn to_valuef(&self) -> ValueF { self.as_valuef().clone() } @@ -317,11 +331,8 @@ impl Shift for Value { impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueInternal::PartialExpr(e) => { - ValueInternal::PartialExpr(e.shift(delta, var)?) - } - ValueInternal::ValueF(m, v) => { - ValueInternal::ValueF(*m, v.shift(delta, var)?) + ValueInternal::ValueF(f, v) => { + ValueInternal::ValueF(*f, v.shift(delta, var)?) } }) } @@ -351,12 +362,9 @@ impl Subst for Value { impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - ValueInternal::PartialExpr(e) => { - ValueInternal::PartialExpr(e.subst_shift(var, val)) - } ValueInternal::ValueF(_, v) => { - // The resulting value may not stay in normal form after substitution - ValueInternal::ValueF(WHNF, v.subst_shift(var, val)) + // The resulting value may not stay in wnhf after substitution + ValueInternal::ValueF(Unevaled, v.subst_shift(var, val)) } } } @@ -392,14 +400,11 @@ impl std::cmp::PartialEq for TypedValue { impl std::cmp::Eq for TypedValue {} impl std::fmt::Debug for Value { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let b: &ValueInternal = &self.as_internal(); match b { - ValueInternal::ValueF(m, v) => { - f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() - } - ValueInternal::PartialExpr(e) => { - f.debug_tuple("Value@PartialExpr").field(e).finish() + ValueInternal::ValueF(f, v) => { + fmt.debug_tuple(&format!("Value@{:?}", f)).field(v).finish() } } } -- cgit v1.2.3 From e70da4c0e9ee2354d757f19f1712f5b04f7acc99 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 18 Aug 2019 23:17:03 +0200 Subject: Merge ValueInternal and TypedValueInternal --- dhall/src/core/value.rs | 190 ++++++++++++++++++++---------------------------- 1 file changed, 79 insertions(+), 111 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 19976af..ef43e3e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -29,17 +29,13 @@ enum Form { use Form::{Unevaled, NF, WHNF}; #[derive(Debug, Clone)] -enum ValueInternal { - /// Partially normalized value. - /// Invariant: if the marker is `WHNF`, the value must be in Weak Head Normal Form - /// Invariant: if the marker is `NF`, the value must be fully normalized - ValueF(Form, ValueF), -} - -#[derive(Debug)] -struct TypedValueInternal { - internal: ValueInternal, - typ: Option, +/// Partially normalized value. +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +/// Invariant: if `form` is `NF`, `value` must be fully normalized +struct ValueInternal { + form: Form, + value: ValueF, + ty: Option, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -47,7 +43,7 @@ struct TypedValueInternal { /// Can optionally store a Type from typechecking to preserve type information through /// normalization. #[derive(Clone)] -pub struct Value(Rc>); +pub struct Value(Rc>); /// A value that needs to carry a type for typechecking to work. /// TODO: actually enforce this. @@ -55,72 +51,54 @@ pub struct Value(Rc>); pub struct TypedValue(Value); impl ValueInternal { - fn into_value(self, t: Option) -> Value { - TypedValueInternal { - internal: self, - typ: t, - } - .into_value() + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) } fn normalize_whnf(&mut self) { - take_mut::take(self, |vint| match vint { - ValueInternal::ValueF(Unevaled, v) => { - ValueInternal::ValueF(WHNF, normalize_whnf(v)) - } + take_mut::take(self, |vint| match &vint.form { + Unevaled => ValueInternal { + form: WHNF, + value: normalize_whnf(vint.value), + ty: vint.ty, + }, // Already in WHNF - vint @ ValueInternal::ValueF(WHNF, _) - | vint @ ValueInternal::ValueF(NF, _) => vint, + WHNF | NF => vint, }) } - fn normalize_nf(&mut self) { - match self { - ValueInternal::ValueF(Unevaled, _) => { + match self.form { + Unevaled => { self.normalize_whnf(); self.normalize_nf(); } - ValueInternal::ValueF(f @ WHNF, v) => { - v.normalize_mut(); - *f = NF; + WHNF => { + self.value.normalize_mut(); + self.form = NF; } // Already in NF - ValueInternal::ValueF(NF, _) => {} + NF => {} } } - // Always use normalize_whnf before + /// Always use normalize_whnf before fn as_whnf(&self) -> &ValueF { - match self { - ValueInternal::ValueF(Unevaled, _) => unreachable!(), - ValueInternal::ValueF(_, v) => v, + match self.form { + Unevaled => unreachable!(), + _ => &self.value, } } - - // Always use normalize_nf before + /// Always use normalize_nf before fn as_nf(&self) -> &ValueF { - match self { - ValueInternal::ValueF(Unevaled, _) - | ValueInternal::ValueF(WHNF, _) => unreachable!(), - ValueInternal::ValueF(NF, v) => v, + match self.form { + Unevaled | WHNF => unreachable!(), + NF => &self.value, } } -} -impl TypedValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_internal(&self) -> &ValueInternal { - &self.internal - } - fn as_internal_mut(&mut self) -> &mut ValueInternal { - &mut self.internal - } - - fn get_type(&self) -> Result { - match &self.typ { - Some(t) => Ok(t.clone()), + fn get_type(&self) -> Result<&Type, TypeError> { + match &self.ty { + Some(t) => Ok(t), None => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, @@ -131,70 +109,80 @@ impl TypedValueInternal { impl Value { pub(crate) fn from_valuef(v: ValueF) -> Value { - ValueInternal::ValueF(Unevaled, v).into_value(None) + ValueInternal { + form: Unevaled, + value: v, + ty: None, + } + .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { - ValueInternal::ValueF(Unevaled, v).into_value(Some(t)) + ValueInternal { + form: Unevaled, + value: v, + ty: Some(t), + } + .into_value() } pub(crate) fn from_partial_expr(e: ExprF) -> Value { Value::from_valuef(ValueF::PartialExpr(e)) } + // TODO: avoid using this function pub(crate) fn with_type(self, t: Type) -> Value { - self.as_internal().clone().into_value(Some(t)) + let vint = self.as_internal(); + ValueInternal { + form: vint.form, + value: vint.value.clone(), + ty: Some(t), + } + .into_value() } /// Mutates the contents. If no one else shares this thunk, /// mutates directly, thus avoiding a RefCell lock. - fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) { + fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner Some(refcell) => f(RefCell::get_mut(refcell)), // Otherwise mutate through the refcell - None => f(&mut self.as_tinternal_mut()), + None => f(&mut self.as_internal_mut()), } } /// Normalizes contents to normal form; faster than `normalize_nf` if /// no one else shares this thunk. pub(crate) fn normalize_mut(&mut self) { - self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) + self.mutate_internal(|vint| vint.normalize_nf()) } - fn as_tinternal(&self) -> Ref { - self.0.borrow() - } - fn as_tinternal_mut(&mut self) -> RefMut { - self.0.borrow_mut() - } fn as_internal(&self) -> Ref { - Ref::map(self.as_tinternal(), TypedValueInternal::as_internal) + self.0.borrow() } fn as_internal_mut(&self) -> RefMut { - RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut) + self.0.borrow_mut() } fn do_normalize_whnf(&self) { let borrow = self.as_internal(); - match &*borrow { - ValueInternal::ValueF(Unevaled, _) => { + match borrow.form { + Unevaled => { drop(borrow); self.as_internal_mut().normalize_whnf(); } // Already at least in WHNF - ValueInternal::ValueF(WHNF, _) | ValueInternal::ValueF(NF, _) => {} + WHNF | NF => {} } } fn do_normalize_nf(&self) { let borrow = self.as_internal(); - match &*borrow { - ValueInternal::ValueF(Unevaled, _) - | ValueInternal::ValueF(WHNF, _) => { + match borrow.form { + Unevaled | WHNF => { drop(borrow); self.as_internal_mut().normalize_nf(); } // Already in NF - ValueInternal::ValueF(NF, _) => {} + NF => {} } } @@ -240,7 +228,7 @@ impl Value { } pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(Cow::Owned(self.as_tinternal().get_type()?)) + Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } } @@ -330,10 +318,10 @@ impl Shift for Value { impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ValueInternal::ValueF(f, v) => { - ValueInternal::ValueF(*f, v.shift(delta, var)?) - } + Some(ValueInternal { + form: self.form, + value: self.value.shift(delta, var)?, + ty: self.ty.shift(delta, var)?, }) } } @@ -344,15 +332,6 @@ impl Shift for TypedValue { } } -impl Shift for TypedValueInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedValueInternal { - internal: self.internal.shift(delta, var)?, - typ: self.typ.shift(delta, var)?, - }) - } -} - impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { Value(self.0.subst_shift(var, val)) @@ -361,20 +340,11 @@ impl Subst for Value { impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - ValueInternal::ValueF(_, v) => { - // The resulting value may not stay in wnhf after substitution - ValueInternal::ValueF(Unevaled, v.subst_shift(var, val)) - } - } - } -} - -impl Subst for TypedValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypedValueInternal { - internal: self.internal.subst_shift(var, val), - typ: self.typ.subst_shift(var, val), + ValueInternal { + // The resulting value may not stay in wnhf after substitution + form: Unevaled, + value: self.value.subst_shift(var, val), + ty: self.ty.subst_shift(var, val), } } } @@ -401,11 +371,9 @@ impl std::cmp::Eq for TypedValue {} impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let b: &ValueInternal = &self.as_internal(); - match b { - ValueInternal::ValueF(f, v) => { - fmt.debug_tuple(&format!("Value@{:?}", f)).field(v).finish() - } - } + let vint: &ValueInternal = &self.as_internal(); + fmt.debug_tuple(&format!("Value@{:?}", &vint.form)) + .field(&vint.value) + .finish() } } -- cgit v1.2.3 From 29016b78736dca857e4e7f7c4dc68ed5e30c28bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 12:25:09 +0200 Subject: s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible --- dhall/src/core/value.rs | 38 ++++++++++++++++++-------------------- 1 file changed, 18 insertions(+), 20 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index ef43e3e..213a2bd 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -193,23 +193,17 @@ impl Value { Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// WARNING: avoid normalizing any thunk while holding on to this ref - /// or you could run into BorrowMut panics - /// TODO: deprecated because of misleading name - pub(crate) fn as_valuef(&self) -> Ref { - self.as_whnf() - } - - /// WARNING: avoid normalizing any thunk while holding on to this ref - /// or you could run into BorrowMut panics + /// This is what you want if you want to pattern-match on the value. + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. pub(crate) fn as_whnf(&self) -> Ref { self.do_normalize_whnf(); Ref::map(self.as_internal(), ValueInternal::as_whnf) } - /// TODO: deprecated because of misleading name - pub(crate) fn to_valuef(&self) -> ValueF { - self.as_valuef().clone() + /// TODO: cloning a valuef can often be avoided + pub(crate) fn to_whnf(&self) -> ValueF { + self.as_whnf().clone() } pub(crate) fn normalize_to_expr_maybe_alpha( @@ -275,14 +269,19 @@ impl TypedValue { TypedValue(Value::from_valuef_and_type(v, t)) } - pub(crate) fn to_valuef(&self) -> ValueF { - self.0.to_valuef() + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref { + self.0.as_whnf() + } + pub(crate) fn to_whnf(&self) -> ValueF { + self.0.to_whnf() } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr() + self.as_whnf().normalize_to_expr() } pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_valuef().normalize_to_expr_maybe_alpha(true) + self.as_whnf().normalize_to_expr_maybe_alpha(true) } pub(crate) fn to_value(&self) -> Value { self.0.clone() @@ -294,8 +293,7 @@ impl TypedValue { Typed::from_typedvalue(self) } pub(crate) fn as_const(&self) -> Option { - // TODO: avoid clone - match &self.to_valuef() { + match &*self.as_whnf() { ValueF::Const(c) => Some(*c), _ => None, } @@ -357,14 +355,14 @@ impl Subst for TypedValue { impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { - *self.as_valuef() == *other.as_valuef() + *self.as_whnf() == *other.as_whnf() } } impl std::cmp::Eq for Value {} impl std::cmp::PartialEq for TypedValue { fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() + &*self.as_whnf() == &*other.as_whnf() } } impl std::cmp::Eq for TypedValue {} -- cgit v1.2.3 From 26a1fd0f0861038a76a0f9b09eaef16d808d4139 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 21:52:26 +0200 Subject: Use TypedValue instead of Typed in normalize and typecheck Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized --- dhall/src/core/value.rs | 48 ++++++++++++++++++++---------------------------- 1 file changed, 20 insertions(+), 28 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 213a2bd..f4cb6b6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -10,7 +10,7 @@ use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; use crate::phase::typecheck::type_of_const; -use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] enum Form { @@ -35,12 +35,12 @@ use Form::{Unevaled, NF, WHNF}; struct ValueInternal { form: Form, value: ValueF, - ty: Option, + ty: Option, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, /// sharing computation automatically. Uses a RefCell to share computation. -/// Can optionally store a Type from typechecking to preserve type information through +/// Can optionally store a type from typechecking to preserve type information through /// normalization. #[derive(Clone)] pub struct Value(Rc>); @@ -96,7 +96,7 @@ impl ValueInternal { } } - fn get_type(&self) -> Result<&Type, TypeError> { + fn get_type(&self) -> Result<&TypedValue, TypeError> { match &self.ty { Some(t) => Ok(t), None => Err(TypeError::new( @@ -116,7 +116,7 @@ impl Value { } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value { ValueInternal { form: Unevaled, value: v, @@ -128,7 +128,7 @@ impl Value { Value::from_valuef(ValueF::PartialExpr(e)) } // TODO: avoid using this function - pub(crate) fn with_type(self, t: Type) -> Value { + pub(crate) fn with_type(self, t: TypedValue) -> Value { let vint = self.as_internal(); ValueInternal { form: vint.form, @@ -221,7 +221,7 @@ impl Value { apply_any(self.clone(), th) } - pub(crate) fn get_type(&self) -> Result, TypeError> { + pub(crate) fn get_type(&self) -> Result, TypeError> { Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } } @@ -231,18 +231,10 @@ impl TypedValue { TypedValue::from_value_untyped(Value::from_valuef(v)) } - pub(crate) fn from_type(t: Type) -> TypedValue { - t.into_typedvalue() - } - pub(crate) fn normalize_nf(&self) -> ValueF { self.0.normalize_nf().clone() } - pub(crate) fn to_typed(&self) -> Typed { - self.clone().into_typed() - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, @@ -250,11 +242,11 @@ impl TypedValue { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { + pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self { TypedValue(th.with_type(t)) } pub fn from_value_simple_type(th: Value) -> Self { - TypedValue::from_value_and_type(th, Type::const_type()) + TypedValue::from_value_and_type(th, TypedValue::const_type()) } pub(crate) fn from_value_untyped(th: Value) -> Self { TypedValue(th) @@ -265,7 +257,10 @@ impl TypedValue { Err(_) => TypedValue::from_valuef(ValueF::Const(c)), } } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + pub fn const_type() -> Self { + TypedValue::from_const(Const::Type) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { TypedValue(Value::from_valuef_and_type(v, t)) } @@ -286,9 +281,6 @@ impl TypedValue { pub(crate) fn to_value(&self) -> Value { self.0.clone() } - pub(crate) fn to_type(&self) -> Type { - self.clone().into_typed().into_type() - } pub(crate) fn into_typed(self) -> Typed { Typed::from_typedvalue(self) } @@ -303,7 +295,7 @@ impl TypedValue { self.0.normalize_mut() } - pub(crate) fn get_type(&self) -> Result, TypeError> { + pub(crate) fn get_type(&self) -> Result, TypeError> { self.0.get_type() } } @@ -330,14 +322,14 @@ impl Shift for TypedValue { } } -impl Subst for Value { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { Value(self.0.subst_shift(var, val)) } } -impl Subst for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst for ValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, @@ -347,8 +339,8 @@ impl Subst for ValueInternal { } } -impl Subst for TypedValue { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { TypedValue(self.0.subst_shift(var, val)) } } -- cgit v1.2.3 From 07a276c1d6ee892b93abbd7a73c78c96d56f4fe7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 22:26:17 +0200 Subject: Reduce untyped construction of Values --- dhall/src/core/value.rs | 68 ++++++++++++++++++++----------------------------- 1 file changed, 28 insertions(+), 40 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f4cb6b6..c4e3831 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF}; +use dhall_syntax::Const; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; @@ -10,7 +10,7 @@ use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; use crate::phase::typecheck::type_of_const; -use crate::phase::{Normalized, NormalizedSubExpr, Typed}; +use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] enum Form { @@ -28,7 +28,7 @@ enum Form { } use Form::{Unevaled, NF, WHNF}; -#[derive(Debug, Clone)] +#[derive(Debug)] /// Partially normalized value. /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form /// Invariant: if `form` is `NF`, `value` must be fully normalized @@ -108,7 +108,7 @@ impl ValueInternal { } impl Value { - pub(crate) fn from_valuef(v: ValueF) -> Value { + pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { ValueInternal { form: Unevaled, value: v, @@ -124,18 +124,8 @@ impl Value { } .into_value() } - pub(crate) fn from_partial_expr(e: ExprF) -> Value { - Value::from_valuef(ValueF::PartialExpr(e)) - } - // TODO: avoid using this function - pub(crate) fn with_type(self, t: TypedValue) -> Value { - let vint = self.as_internal(); - ValueInternal { - form: vint.form, - value: vint.value.clone(), - ty: Some(t), - } - .into_value() + pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { + Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type)) } /// Mutates the contents. If no one else shares this thunk, @@ -214,7 +204,7 @@ impl Value { } pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { - self.app_value(val.into_value()) + self.app_value(val.into_value_untyped()) } pub(crate) fn app_value(&self, th: Value) -> ValueF { @@ -227,41 +217,39 @@ impl Value { } impl TypedValue { - pub(crate) fn from_valuef(v: ValueF) -> TypedValue { - TypedValue::from_value_untyped(Value::from_valuef(v)) - } - - pub(crate) fn normalize_nf(&self) -> ValueF { - self.0.normalize_nf().clone() - } - - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + pub fn from_value(th: Value) -> Self { + TypedValue(th) } - - pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self { - TypedValue(th.with_type(t)) + pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue { + TypedValue::from_value(Value::from_valuef_untyped(v)) } - pub fn from_value_simple_type(th: Value) -> Self { - TypedValue::from_value_and_type(th, TypedValue::const_type()) + pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) } - pub(crate) fn from_value_untyped(th: Value) -> Self { - TypedValue(th) + // TODO: do something with the info that the type is Type. Maybe check + // is a type is present ? + pub(crate) fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value(th) } pub(crate) fn from_const(c: Const) -> Self { match type_of_const(c) { Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)), } } pub fn const_type() -> Self { TypedValue::from_const(Const::Type) } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { - TypedValue(Value::from_valuef_and_type(v, t)) + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.normalize_nf().clone() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut -- cgit v1.2.3 From 730f2ebb146792994c7492b6c05f7d09d42cbccf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 23:00:49 +0200 Subject: Merge TypedValue and Value --- dhall/src/core/value.rs | 192 ++++++++++++++++-------------------------------- 1 file changed, 63 insertions(+), 129 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index c4e3831..8573d11 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -35,7 +35,7 @@ use Form::{Unevaled, NF, WHNF}; struct ValueInternal { form: Form, value: ValueF, - ty: Option, + ty: Option, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -45,11 +45,6 @@ struct ValueInternal { #[derive(Clone)] pub struct Value(Rc>); -/// A value that needs to carry a type for typechecking to work. -/// TODO: actually enforce this. -#[derive(Debug, Clone)] -pub struct TypedValue(Value); - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -96,7 +91,7 @@ impl ValueInternal { } } - fn get_type(&self) -> Result<&TypedValue, TypeError> { + fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), None => Err(TypeError::new( @@ -116,7 +111,7 @@ impl Value { } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Value { + pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { ValueInternal { form: Unevaled, value: v, @@ -125,7 +120,57 @@ impl Value { .into_value() } pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { - Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type)) + Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => Value::from_valuef_untyped(ValueF::Const(c)), + } + } + pub fn const_type() -> Self { + Value::from_const(Const::Type) + } + + pub(crate) fn as_const(&self) -> Option { + match &*self.as_whnf() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + fn as_internal(&self) -> Ref { + self.0.borrow() + } + fn as_internal_mut(&self) -> RefMut { + self.0.borrow_mut() + } + /// This is what you want if you want to pattern-match on the value. + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_whnf(&self) -> Ref { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) + } + + // TODO: rename `normalize_to_expr` + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr() + } + // TODO: rename `normalize_to_expr_maybe_alpha` + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.as_whnf().normalize_to_expr_maybe_alpha(true) + } + // TODO: deprecated + pub(crate) fn to_value(&self) -> Value { + self.clone() + } + /// TODO: cloning a valuef can often be avoided + pub(crate) fn to_whnf(&self) -> ValueF { + self.as_whnf().clone() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_value(self) } /// Mutates the contents. If no one else shares this thunk, @@ -138,20 +183,12 @@ impl Value { None => f(&mut self.as_internal_mut()), } } - /// Normalizes contents to normal form; faster than `normalize_nf` if /// no one else shares this thunk. pub(crate) fn normalize_mut(&mut self) { self.mutate_internal(|vint| vint.normalize_nf()) } - fn as_internal(&self) -> Ref { - self.0.borrow() - } - fn as_internal_mut(&self) -> RefMut { - self.0.borrow_mut() - } - fn do_normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { @@ -163,7 +200,6 @@ impl Value { WHNF | NF => {} } } - fn do_normalize_nf(&self) { let borrow = self.as_internal(); match borrow.form { @@ -176,26 +212,14 @@ impl Value { } } - // WARNING: avoid normalizing any thunk while holding on to this ref - // or you could run into BorrowMut panics + /// WARNING: avoid normalizing any thunk while holding on to this ref + /// or you could run into BorrowMut panics + // TODO: rename to `as_nf` pub(crate) fn normalize_nf(&self) -> Ref { self.do_normalize_nf(); Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// This is what you want if you want to pattern-match on the value. - /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut - /// panics. - pub(crate) fn as_whnf(&self) -> Ref { - self.do_normalize_whnf(); - Ref::map(self.as_internal(), ValueInternal::as_whnf) - } - - /// TODO: cloning a valuef can often be avoided - pub(crate) fn to_whnf(&self) -> ValueF { - self.as_whnf().clone() - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, @@ -211,83 +235,11 @@ impl Value { apply_any(self.clone(), th) } - pub(crate) fn get_type(&self) -> Result, TypeError> { + pub(crate) fn get_type(&self) -> Result, TypeError> { Ok(Cow::Owned(self.as_internal().get_type()?.clone())) } } -impl TypedValue { - pub fn from_value(th: Value) -> Self { - TypedValue(th) - } - pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue { - TypedValue::from_value(Value::from_valuef_untyped(v)) - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self { - TypedValue(Value::from_valuef_and_type(v, t)) - } - // TODO: do something with the info that the type is Type. Maybe check - // is a type is present ? - pub(crate) fn from_value_simple_type(th: Value) -> Self { - TypedValue::from_value(th) - } - pub(crate) fn from_const(c: Const) -> Self { - match type_of_const(c) { - Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)), - } - } - pub fn const_type() -> Self { - TypedValue::from_const(Const::Type) - } - - pub(crate) fn normalize_nf(&self) -> ValueF { - self.0.normalize_nf().clone() - } - - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) - } - - /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut - /// panics. - pub(crate) fn as_whnf(&self) -> Ref { - self.0.as_whnf() - } - pub(crate) fn to_whnf(&self) -> ValueF { - self.0.to_whnf() - } - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.as_whnf().normalize_to_expr() - } - pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.as_whnf().normalize_to_expr_maybe_alpha(true) - } - pub(crate) fn to_value(&self) -> Value { - self.0.clone() - } - pub(crate) fn into_typed(self) -> Typed { - Typed::from_typedvalue(self) - } - pub(crate) fn as_const(&self) -> Option { - match &*self.as_whnf() { - ValueF::Const(c) => Some(*c), - _ => None, - } - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result, TypeError> { - self.0.get_type() - } -} - impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) @@ -304,20 +256,14 @@ impl Shift for ValueInternal { } } -impl Shift for TypedValue { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedValue(self.0.shift(delta, var)?)) - } -} - -impl Subst for Value { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { Value(self.0.subst_shift(var, val)) } } -impl Subst for ValueInternal { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst for ValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, @@ -327,12 +273,7 @@ impl Subst for ValueInternal { } } -impl Subst for TypedValue { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { - TypedValue(self.0.subst_shift(var, val)) - } -} - +// TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { *self.as_whnf() == *other.as_whnf() @@ -340,13 +281,6 @@ impl std::cmp::PartialEq for Value { } impl std::cmp::Eq for Value {} -impl std::cmp::PartialEq for TypedValue { - fn eq(&self, other: &Self) -> bool { - &*self.as_whnf() == &*other.as_whnf() - } -} -impl std::cmp::Eq for TypedValue {} - impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); -- cgit v1.2.3 From 88a3b5efb2cf4b8ebb3743389e5666deae5f8962 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 23:09:08 +0200 Subject: Tweak Value API --- dhall/src/core/value.rs | 47 +++++++++++++++++++---------------------------- 1 file changed, 19 insertions(+), 28 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 8573d11..87816c4 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -49,6 +49,9 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } + fn as_valuef(&self) -> &ValueF { + &self.value + } fn normalize_whnf(&mut self) { take_mut::take(self, |vint| match &vint.form { @@ -76,21 +79,6 @@ impl ValueInternal { } } - /// Always use normalize_whnf before - fn as_whnf(&self) -> &ValueF { - match self.form { - Unevaled => unreachable!(), - _ => &self.value, - } - } - /// Always use normalize_nf before - fn as_nf(&self) -> &ValueF { - match self.form { - Unevaled | WHNF => unreachable!(), - NF => &self.value, - } - } - fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), @@ -145,12 +133,23 @@ impl Value { fn as_internal_mut(&self) -> RefMut { self.0.borrow_mut() } + /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an + /// unevaled PartialExpr. You probably want to use `as_whnf`. + fn as_valuef(&self) -> Ref { + Ref::map(self.as_internal(), ValueInternal::as_valuef) + } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. pub(crate) fn as_whnf(&self) -> Ref { - self.do_normalize_whnf(); - Ref::map(self.as_internal(), ValueInternal::as_whnf) + self.normalize_whnf(); + self.as_valuef() + } + /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut + /// panics. + pub(crate) fn as_nf(&self) -> Ref { + self.normalize_nf(); + self.as_valuef() } // TODO: rename `normalize_to_expr` @@ -189,7 +188,7 @@ impl Value { self.mutate_internal(|vint| vint.normalize_nf()) } - fn do_normalize_whnf(&self) { + pub(crate) fn normalize_whnf(&self) { let borrow = self.as_internal(); match borrow.form { Unevaled => { @@ -200,7 +199,7 @@ impl Value { WHNF | NF => {} } } - fn do_normalize_nf(&self) { + pub(crate) fn normalize_nf(&self) { let borrow = self.as_internal(); match borrow.form { Unevaled | WHNF => { @@ -212,19 +211,11 @@ impl Value { } } - /// WARNING: avoid normalizing any thunk while holding on to this ref - /// or you could run into BorrowMut panics - // TODO: rename to `as_nf` - pub(crate) fn normalize_nf(&self) -> Ref { - self.do_normalize_nf(); - Ref::map(self.as_internal(), ValueInternal::as_nf) - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, ) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + self.as_nf().normalize_to_expr_maybe_alpha(alpha) } pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { -- cgit v1.2.3 From caf36246a517b884d7cfcf7c31e1b5d8fce60dfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 13:49:13 +0200 Subject: Cleanup --- dhall/src/core/value.rs | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 87816c4..0af7c8c 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -40,8 +40,7 @@ struct ValueInternal { /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, /// sharing computation automatically. Uses a RefCell to share computation. -/// Can optionally store a type from typechecking to preserve type information through -/// normalization. +/// Can optionally store a type from typechecking to preserve type information. #[derive(Clone)] pub struct Value(Rc>); @@ -160,10 +159,6 @@ impl Value { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.as_whnf().normalize_to_expr_maybe_alpha(true) } - // TODO: deprecated - pub(crate) fn to_value(&self) -> Value { - self.clone() - } /// TODO: cloning a valuef can often be avoided pub(crate) fn to_whnf(&self) -> ValueF { self.as_whnf().clone() @@ -172,8 +167,7 @@ impl Value { Typed::from_value(self) } - /// Mutates the contents. If no one else shares this thunk, - /// mutates directly, thus avoiding a RefCell lock. + /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner @@ -183,7 +177,7 @@ impl Value { } } /// Normalizes contents to normal form; faster than `normalize_nf` if - /// no one else shares this thunk. + /// no one else shares this. pub(crate) fn normalize_mut(&mut self) { self.mutate_internal(|vint| vint.normalize_nf()) } @@ -218,10 +212,6 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { - self.app_value(val.into_value_untyped()) - } - pub(crate) fn app_value(&self, th: Value) -> ValueF { apply_any(self.clone(), th) } -- cgit v1.2.3 From 38a82c53ef45e802cf5816a8afcbf36a69c91174 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 14:12:27 +0200 Subject: Clarify conversion of Const/Builtin to Value --- dhall/src/core/value.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 0af7c8c..5367c86 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -9,7 +9,7 @@ use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; -use crate::phase::typecheck::type_of_const; +use crate::phase::typecheck::const_to_value; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] @@ -110,10 +110,7 @@ impl Value { Value::from_valuef_and_type(v, Value::from_const(Const::Type)) } pub(crate) fn from_const(c: Const) -> Self { - match type_of_const(c) { - Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => Value::from_valuef_untyped(ValueF::Const(c)), - } + const_to_value(c) } pub fn const_type() -> Self { Value::from_const(Const::Type) -- cgit v1.2.3 From 04438824db21fb5d9d3a2abdb3fa167875bda892 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 16:39:27 +0200 Subject: Add Value::from_builtin --- dhall/src/core/value.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5367c86..f897f16 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,14 +2,14 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::Const; +use dhall_syntax::{Builtin, Const}; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; -use crate::phase::typecheck::const_to_value; +use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] @@ -115,6 +115,9 @@ impl Value { pub fn const_type() -> Self { Value::from_const(Const::Type) } + pub fn from_builtin(b: Builtin) -> Self { + builtin_to_value(b) + } pub(crate) fn as_const(&self) -> Option { match &*self.as_whnf() { -- cgit v1.2.3 From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 17:08:01 +0200 Subject: Naming tweaks --- dhall/src/core/value.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f897f16..5055ac2 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -8,7 +8,7 @@ use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; +use crate::phase::normalize::{apply_any, normalize_whnf}; use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; @@ -208,11 +208,11 @@ impl Value { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> OutputSubExpr { + ) -> NormalizedSubExpr { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_value(&self, th: Value) -> ValueF { + pub(crate) fn app(&self, th: Value) -> ValueF { apply_any(self.clone(), th) } -- cgit v1.2.3 From 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:03:59 +0200 Subject: Introduce a new enum to store either a Value or a ValueF --- dhall/src/core/value.rs | 54 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 51 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5055ac2..25fcaae 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,6 +44,14 @@ struct ValueInternal { #[derive(Clone)] pub struct Value(Rc>); +/// When a function needs to return either a freshly created ValueF or an existing Value, but +/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to +/// avoid loss of typ information. +pub enum VoVF { + Value(Value), + ValueF(ValueF), +} + impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -56,7 +64,8 @@ impl ValueInternal { take_mut::take(self, |vint| match &vint.form { Unevaled => ValueInternal { form: WHNF, - value: normalize_whnf(vint.value), + // TODO: thunk chaining + value: normalize_whnf(vint.value).into_whnf(), ty: vint.ty, }, // Already in WHNF @@ -166,6 +175,9 @@ impl Value { pub(crate) fn into_typed(self) -> Typed { Typed::from_value(self) } + pub(crate) fn into_vovf(self) -> VoVF { + VoVF::Value(self) + } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { @@ -212,8 +224,8 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app(&self, th: Value) -> ValueF { - apply_any(self.clone(), th) + pub(crate) fn app(&self, v: Value) -> VoVF { + apply_any(self.clone(), v) } pub(crate) fn get_type(&self) -> Result, TypeError> { @@ -221,6 +233,42 @@ impl Value { } } +impl VoVF { + pub fn into_whnf(self) -> ValueF { + match self { + VoVF::Value(v) => v.to_whnf(), + VoVF::ValueF(v) => v, + } + } + pub(crate) fn into_value_untyped(self) -> Value { + match self { + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_untyped(), + } + } + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + match self { + // TODO: check type with debug_assert ? + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_with_type(t), + } + } + pub(crate) fn into_value_simple_type(self) -> Value { + match self { + // TODO: check type with debug_assert ? + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_simple_type(), + } + } + + pub(crate) fn app(self, x: Value) -> Self { + match self { + VoVF::Value(v) => v.app(x), + VoVF::ValueF(v) => v.into_value_untyped().app(x), + } + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) -- cgit v1.2.3 From c157df5e66fb80ff6184cb3934e5b0883f0fdbf0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:11:05 +0200 Subject: No need for Cow in return type of get_type --- dhall/src/core/value.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 25fcaae..64a4842 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,4 +1,3 @@ -use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; @@ -228,8 +227,8 @@ impl Value { apply_any(self.clone(), v) } - pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(Cow::Owned(self.as_internal().get_type()?.clone())) + pub(crate) fn get_type(&self) -> Result { + Ok(self.as_internal().get_type()?.clone()) } } -- cgit v1.2.3 From f70e45daef2570259eccd227a0126493c015d7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 21:50:47 +0200 Subject: Track evaluation status alongside ValueF in VoVF --- dhall/src/core/value.rs | 44 ++++++++++++++++++-------------------------- 1 file changed, 18 insertions(+), 26 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 64a4842..b44dad6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] -enum Form { +pub enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -46,9 +46,10 @@ pub struct Value(Rc>); /// When a function needs to return either a freshly created ValueF or an existing Value, but /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to /// avoid loss of typ information. +#[derive(Debug, Clone)] pub enum VoVF { Value(Value), - ValueF(ValueF), + ValueF { val: ValueF, form: Form }, } impl ValueInternal { @@ -98,24 +99,14 @@ impl ValueInternal { } impl Value { + pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { + ValueInternal { form, value, ty }.into_value() + } pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: None, - } - .into_value() + Value::new(v, Unevaled, None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: Some(t), - } - .into_value() - } - pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { - Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + Value::new(v, Unevaled, Some(t)) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -236,34 +227,35 @@ impl VoVF { pub fn into_whnf(self) -> ValueF { match self { VoVF::Value(v) => v.to_whnf(), - VoVF::ValueF(v) => v, + VoVF::ValueF { + val, + form: Unevaled, + } => normalize_whnf(val).into_whnf(), + // Already at lest in WHNF + VoVF::ValueF { val, .. } => val, } } pub(crate) fn into_value_untyped(self) -> Value { match self { VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_untyped(), + VoVF::ValueF { val, form } => Value::new(val, form, None), } } pub(crate) fn into_value_with_type(self, t: Value) -> Value { match self { // TODO: check type with debug_assert ? VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_with_type(t), + VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), } } pub(crate) fn into_value_simple_type(self) -> Value { - match self { - // TODO: check type with debug_assert ? - VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_simple_type(), - } + self.into_value_with_type(Value::from_const(Const::Type)) } pub(crate) fn app(self, x: Value) -> Self { match self { VoVF::Value(v) => v.app(x), - VoVF::ValueF(v) => v.into_value_untyped().app(x), + VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), } } } -- cgit v1.2.3 From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:20:59 +0200 Subject: Propagate type information in Value::app() --- dhall/src/core/value.rs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index b44dad6..24e2803 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -214,8 +214,18 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app(&self, v: Value) -> VoVF { - apply_any(self.clone(), v) + pub(crate) fn app(&self, v: Value) -> Value { + let vovf = apply_any(self.clone(), v.clone()); + match self.as_internal().get_type() { + Err(_) => vovf.into_value_untyped(), + Ok(t) => match &*t.as_whnf() { + ValueF::Pi(x, _, e) => { + let t = e.subst_shift(&x.into(), &v); + vovf.into_value_with_type(t) + } + _ => unreachable!("Internal type error"), + }, + } } pub(crate) fn get_type(&self) -> Result { @@ -248,15 +258,12 @@ impl VoVF { VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), } } - pub(crate) fn into_value_simple_type(self) -> Value { - self.into_value_with_type(Value::from_const(Const::Type)) - } - pub(crate) fn app(self, x: Value) -> Self { - match self { + pub(crate) fn app(self, x: Value) -> VoVF { + VoVF::Value(match self { VoVF::Value(v) => v.app(x), VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), - } + }) } } -- cgit v1.2.3 From 6c006e122a050ebbe76c8c566e559bbf9f2301a7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 23:06:14 +0200 Subject: Reduce API surface of dhall crate --- dhall/src/core/value.rs | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 24e2803..e1623a8 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] -pub enum Form { +pub(crate) enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -41,13 +41,13 @@ struct ValueInternal { /// sharing computation automatically. Uses a RefCell to share computation. /// Can optionally store a type from typechecking to preserve type information. #[derive(Clone)] -pub struct Value(Rc>); +pub(crate) struct Value(Rc>); /// When a function needs to return either a freshly created ValueF or an existing Value, but /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to /// avoid loss of typ information. #[derive(Debug, Clone)] -pub enum VoVF { +pub(crate) enum VoVF { Value(Value), ValueF { val: ValueF, form: Form }, } @@ -111,10 +111,7 @@ impl Value { pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) } - pub fn const_type() -> Self { - Value::from_const(Const::Type) - } - pub fn from_builtin(b: Builtin) -> Self { + pub(crate) fn from_builtin(b: Builtin) -> Self { builtin_to_value(b) } @@ -234,7 +231,7 @@ impl Value { } impl VoVF { - pub fn into_whnf(self) -> ValueF { + pub(crate) fn into_whnf(self) -> ValueF { match self { VoVF::Value(v) => v.to_whnf(), VoVF::ValueF { -- cgit v1.2.3 From e8a9178ebe4860a8a00a6ec8f77b661fdad84890 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 21 Aug 2019 17:40:56 +0200 Subject: Don't use take_mut::take lightly since normalize_whnf might panic --- dhall/src/core/value.rs | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index e1623a8..69d372a 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -61,16 +61,25 @@ impl ValueInternal { } fn normalize_whnf(&mut self) { - take_mut::take(self, |vint| match &vint.form { - Unevaled => ValueInternal { - form: WHNF, - // TODO: thunk chaining - value: normalize_whnf(vint.value).into_whnf(), - ty: vint.ty, + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + value: ValueF::Const(Const::Type), + ty: None, }, - // Already in WHNF - WHNF | NF => vint, - }) + |vint| match &vint.form { + Unevaled => ValueInternal { + form: WHNF, + // TODO: thunk chaining + value: normalize_whnf(vint.value).into_whnf(), + ty: vint.ty, + }, + // Already in WHNF + WHNF | NF => vint, + }, + ) } fn normalize_nf(&mut self) { match self.form { -- cgit v1.2.3 From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:09:55 +0200 Subject: Keep type information through normalization --- dhall/src/core/value.rs | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 69d372a..6f9f78a 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -70,12 +70,25 @@ impl ValueInternal { ty: None, }, |vint| match &vint.form { - Unevaled => ValueInternal { - form: WHNF, - // TODO: thunk chaining - value: normalize_whnf(vint.value).into_whnf(), - ty: vint.ty, - }, + Unevaled => { + let (value, ty) = (vint.value, vint.ty); + let vovf = normalize_whnf(value, ty.as_ref()); + // let was_value = if let VoVF::Value(_) = &vovf { + // true + // } else { + // false + // }; + let (new_val, _new_ty) = + vovf.into_whnf_and_type(ty.as_ref()); + // if was_value { + // debug_assert_eq!(ty, new_ty); + // } + ValueInternal { + form: WHNF, + value: new_val, + ty: ty, + } + } // Already in WHNF WHNF | NF => vint, }, @@ -221,7 +234,8 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let vovf = apply_any(self.clone(), v.clone()); + let ty = self.get_type().ok(); + let vovf = apply_any(self.clone(), v.clone(), ty.as_ref()); match self.as_internal().get_type() { Err(_) => vovf.into_value_untyped(), Ok(t) => match &*t.as_whnf() { @@ -240,15 +254,18 @@ impl Value { } impl VoVF { - pub(crate) fn into_whnf(self) -> ValueF { + pub(crate) fn into_whnf_and_type( + self, + ty: Option<&Value>, + ) -> (ValueF, Option) { match self { - VoVF::Value(v) => v.to_whnf(), VoVF::ValueF { val, form: Unevaled, - } => normalize_whnf(val).into_whnf(), + } => normalize_whnf(val, ty).into_whnf_and_type(ty), // Already at lest in WHNF - VoVF::ValueF { val, .. } => val, + VoVF::ValueF { val, .. } => (val, None), + VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()), } } pub(crate) fn into_value_untyped(self) -> Value { -- cgit v1.2.3 From 80fb5355ea90377492b9863f632c01a808f8aade Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:33:12 +0200 Subject: Check consistency of type information --- dhall/src/core/value.rs | 53 ++++++++++++++++++++++++++----------------------- 1 file changed, 28 insertions(+), 25 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 6f9f78a..7f98826 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -71,22 +71,13 @@ impl ValueInternal { }, |vint| match &vint.form { Unevaled => { - let (value, ty) = (vint.value, vint.ty); - let vovf = normalize_whnf(value, ty.as_ref()); - // let was_value = if let VoVF::Value(_) = &vovf { - // true - // } else { - // false - // }; - let (new_val, _new_ty) = - vovf.into_whnf_and_type(ty.as_ref()); - // if was_value { - // debug_assert_eq!(ty, new_ty); - // } + let new_value = + normalize_whnf(vint.value, vint.ty.as_ref()) + .into_whnf(vint.ty.as_ref()); ValueInternal { form: WHNF, - value: new_val, - ty: ty, + value: new_value, + ty: vint.ty, } } // Already in WHNF @@ -254,18 +245,23 @@ impl Value { } impl VoVF { - pub(crate) fn into_whnf_and_type( - self, - ty: Option<&Value>, - ) -> (ValueF, Option) { + pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF { match self { VoVF::ValueF { val, form: Unevaled, - } => normalize_whnf(val, ty).into_whnf_and_type(ty), + } => normalize_whnf(val, ty).into_whnf(ty), // Already at lest in WHNF - VoVF::ValueF { val, .. } => (val, None), - VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()), + VoVF::ValueF { val, .. } => val, + VoVF::Value(v) => { + let v_ty = v.get_type().ok(); + debug_assert_eq!( + ty, + v_ty.as_ref(), + "The type recovered from normalization doesn't match the stored type." + ); + v.to_whnf() + } } } pub(crate) fn into_value_untyped(self) -> Value { @@ -274,11 +270,18 @@ impl VoVF { VoVF::ValueF { val, form } => Value::new(val, form, None), } } - pub(crate) fn into_value_with_type(self, t: Value) -> Value { + pub(crate) fn into_value_with_type(self, ty: Value) -> Value { match self { - // TODO: check type with debug_assert ? - VoVF::Value(v) => v, - VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), + VoVF::Value(v) => { + let v_ty = v.get_type().ok(); + debug_assert_eq!( + Some(&ty), + v_ty.as_ref(), + "The type recovered from normalization doesn't match the stored type." + ); + v + } + VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)), } } -- cgit v1.2.3 From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 17:07:59 +0200 Subject: Enforce type information almost everywhere --- dhall/src/core/value.rs | 66 +++++++++++++++++++++++++++---------------------- 1 file changed, 36 insertions(+), 30 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 7f98826..4a78b05 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -27,13 +27,14 @@ pub(crate) enum Form { } use Form::{Unevaled, NF, WHNF}; -#[derive(Debug)] /// Partially normalized value. /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form /// Invariant: if `form` is `NF`, `value` must be fully normalized +#[derive(Debug)] struct ValueInternal { form: Form, value: ValueF, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, } @@ -69,11 +70,15 @@ impl ValueInternal { value: ValueF::Const(Const::Type), ty: None, }, - |vint| match &vint.form { - Unevaled => { + |vint| match (&vint.form, &vint.ty) { + (Unevaled, None) => ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + }, + (Unevaled, Some(ty)) => { let new_value = - normalize_whnf(vint.value, vint.ty.as_ref()) - .into_whnf(vint.ty.as_ref()); + normalize_whnf(vint.value, &ty).into_whnf(&ty); ValueInternal { form: WHNF, value: new_value, @@ -81,7 +86,7 @@ impl ValueInternal { } } // Already in WHNF - WHNF | NF => vint, + (WHNF, _) | (NF, _) => vint, }, ) } @@ -103,10 +108,9 @@ impl ValueInternal { fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), + None => { + Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) + } } } } @@ -115,9 +119,13 @@ impl Value { pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { ValueInternal { form, value, ty }.into_value() } + // TODO: this is very wrong pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { Value::new(v, Unevaled, None) } + pub(crate) fn const_sort() -> Value { + Value::new(ValueF::Const(Const::Sort), NF, None) + } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { Value::new(v, Unevaled, Some(t)) } @@ -225,27 +233,30 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let ty = self.get_type().ok(); - let vovf = apply_any(self.clone(), v.clone(), ty.as_ref()); - match self.as_internal().get_type() { - Err(_) => vovf.into_value_untyped(), - Ok(t) => match &*t.as_whnf() { - ValueF::Pi(x, _, e) => { - let t = e.subst_shift(&x.into(), &v); - vovf.into_value_with_type(t) - } - _ => unreachable!("Internal type error"), - }, + let t = self.get_type_not_sort(); + let vovf = apply_any(self.clone(), v.clone(), &t); + let t_borrow = t.as_whnf(); + match &*t_borrow { + ValueF::Pi(x, _, e) => { + let t = e.subst_shift(&x.into(), &v); + vovf.into_value_with_type(t) + } + _ => unreachable!("Internal type error"), } } pub(crate) fn get_type(&self) -> Result { Ok(self.as_internal().get_type()?.clone()) } + /// When we know the value isn't `Sort`, this gets the type directly + pub(crate) fn get_type_not_sort(&self) -> Value { + self.get_type() + .expect("Internal type error: value is `Sort` but shouldn't be") + } } impl VoVF { - pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF { + pub(crate) fn into_whnf(self, ty: &Value) -> ValueF { match self { VoVF::ValueF { val, @@ -256,7 +267,7 @@ impl VoVF { VoVF::Value(v) => { let v_ty = v.get_type().ok(); debug_assert_eq!( - ty, + Some(ty), v_ty.as_ref(), "The type recovered from normalization doesn't match the stored type." ); @@ -264,12 +275,6 @@ impl VoVF { } } } - pub(crate) fn into_value_untyped(self) -> Value { - match self { - VoVF::Value(v) => v, - VoVF::ValueF { val, form } => Value::new(val, form, None), - } - } pub(crate) fn into_value_with_type(self, ty: Value) -> Value { match self { VoVF::Value(v) => { @@ -288,7 +293,8 @@ impl VoVF { pub(crate) fn app(self, x: Value) -> VoVF { VoVF::Value(match self { VoVF::Value(v) => v.app(x), - VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), + // TODO: this is very wrong + VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x), }) } } -- cgit v1.2.3 From bf37fd9da3782134ca4bca9567c34bbee81784b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:16:38 +0200 Subject: Rework apply_builtin to enforce preservation of type information --- dhall/src/core/value.rs | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 4a78b05..2554da1 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -116,18 +116,24 @@ impl ValueInternal { } impl Value { - pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { - ValueInternal { form, value, ty }.into_value() - } - // TODO: this is very wrong - pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - Value::new(v, Unevaled, None) + fn new(value: ValueF, form: Form, ty: Value) -> Value { + ValueInternal { + form, + value, + ty: Some(ty), + } + .into_value() } pub(crate) fn const_sort() -> Value { - Value::new(ValueF::Const(Const::Sort), NF, None) + ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + } + .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, Some(t)) + Value::new(v, Unevaled, t) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -286,17 +292,9 @@ impl VoVF { ); v } - VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)), + VoVF::ValueF { val, form } => Value::new(val, form, ty), } } - - pub(crate) fn app(self, x: Value) -> VoVF { - VoVF::Value(match self { - VoVF::Value(v) => v.app(x), - // TODO: this is very wrong - VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x), - }) - } } impl Shift for Value { -- cgit v1.2.3 From 906cbf5fc4c3bee65f24df1604497e33c6a20833 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:52:59 +0200 Subject: Remove now unnecessary VoVF enum --- dhall/src/core/value.rs | 95 ++++++++++++++----------------------------------- 1 file changed, 27 insertions(+), 68 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 2554da1..13f8e59 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,15 +44,6 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc>); -/// When a function needs to return either a freshly created ValueF or an existing Value, but -/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to -/// avoid loss of typ information. -#[derive(Debug, Clone)] -pub(crate) enum VoVF { - Value(Value), - ValueF { val: ValueF, form: Form }, -} - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -76,15 +67,11 @@ impl ValueInternal { value: ValueF::Const(Const::Sort), ty: None, }, - (Unevaled, Some(ty)) => { - let new_value = - normalize_whnf(vint.value, &ty).into_whnf(&ty); - ValueInternal { - form: WHNF, - value: new_value, - ty: vint.ty, - } - } + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + value: normalize_whnf(vint.value, &ty), + ty: vint.ty, + }, // Already in WHNF (WHNF, _) | (NF, _) => vint, }, @@ -135,6 +122,9 @@ impl Value { pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { Value::new(v, Unevaled, t) } + pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { + Value::new(v, WHNF, t) + } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) } @@ -182,16 +172,22 @@ impl Value { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.as_whnf().normalize_to_expr_maybe_alpha(true) } - /// TODO: cloning a valuef can often be avoided - pub(crate) fn to_whnf(&self) -> ValueF { + pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { self.as_whnf().clone() } + /// Before discarding type information, check that it matches the expected return type. + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { + let self_ty = self.get_type().ok(); + debug_assert_eq!( + Some(ty), + self_ty.as_ref(), + "The value returned from normalization doesn't have the expected type." + ); + self.to_whnf_ignore_type() + } pub(crate) fn into_typed(self) -> Typed { Typed::from_value(self) } - pub(crate) fn into_vovf(self) -> VoVF { - VoVF::Value(self) - } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { @@ -239,16 +235,14 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let t = self.get_type_not_sort(); - let vovf = apply_any(self.clone(), v.clone(), &t); - let t_borrow = t.as_whnf(); - match &*t_borrow { - ValueF::Pi(x, _, e) => { - let t = e.subst_shift(&x.into(), &v); - vovf.into_value_with_type(t) - } + let body_t = match &*self.get_type_not_sort().as_whnf() { + ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v), _ => unreachable!("Internal type error"), - } + }; + Value::from_valuef_and_type_whnf( + apply_any(self.clone(), v, &body_t), + body_t, + ) } pub(crate) fn get_type(&self) -> Result { @@ -261,42 +255,6 @@ impl Value { } } -impl VoVF { - pub(crate) fn into_whnf(self, ty: &Value) -> ValueF { - match self { - VoVF::ValueF { - val, - form: Unevaled, - } => normalize_whnf(val, ty).into_whnf(ty), - // Already at lest in WHNF - VoVF::ValueF { val, .. } => val, - VoVF::Value(v) => { - let v_ty = v.get_type().ok(); - debug_assert_eq!( - Some(ty), - v_ty.as_ref(), - "The type recovered from normalization doesn't match the stored type." - ); - v.to_whnf() - } - } - } - pub(crate) fn into_value_with_type(self, ty: Value) -> Value { - match self { - VoVF::Value(v) => { - let v_ty = v.get_type().ok(); - debug_assert_eq!( - Some(&ty), - v_ty.as_ref(), - "The type recovered from normalization doesn't match the stored type." - ); - v - } - VoVF::ValueF { val, form } => Value::new(val, form, ty), - } - } -} - impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) @@ -324,6 +282,7 @@ impl Subst for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, + // TODO: check type info if self.value if Var(v) and v == var value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), } -- cgit v1.2.3 From 829fff5bd3e2115c0a16d40a4dc266747d622b08 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 26 Aug 2019 18:54:29 +0200 Subject: Check correctness of type info in a few more places --- dhall/src/core/value.rs | 60 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 43 insertions(+), 17 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 13f8e59..21ac288 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -62,16 +62,17 @@ impl ValueInternal { ty: None, }, |vint| match (&vint.form, &vint.ty) { - (Unevaled, None) => ValueInternal { - form: NF, - value: ValueF::Const(Const::Sort), - ty: None, - }, (Unevaled, Some(ty)) => ValueInternal { form: WHNF, value: normalize_whnf(vint.value, &ty), ty: vint.ty, }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + }, // Already in WHNF (WHNF, _) | (NF, _) => vint, }, @@ -177,12 +178,7 @@ impl Value { } /// Before discarding type information, check that it matches the expected return type. pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { - let self_ty = self.get_type().ok(); - debug_assert_eq!( - Some(ty), - self_ty.as_ref(), - "The value returned from normalization doesn't have the expected type." - ); + self.check_type(ty); self.to_whnf_ignore_type() } pub(crate) fn into_typed(self) -> Typed { @@ -236,7 +232,10 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v), + ValueF::Pi(x, t, e) => { + v.check_type(t); + e.subst_shift(&x.into(), &v) + } _ => unreachable!("Internal type error"), }; Value::from_valuef_and_type_whnf( @@ -245,6 +244,15 @@ impl Value { ) } + /// In debug mode, panic if the provided type doesn't match the value's type. + /// Otherwise does nothing. + pub(crate) fn check_type(&self, ty: &Value) { + debug_assert_eq!( + Some(ty), + self.get_type().ok().as_ref(), + "Internal type error" + ); + } pub(crate) fn get_type(&self) -> Result { Ok(self.as_internal().get_type()?.clone()) } @@ -273,7 +281,17 @@ impl Shift for ValueInternal { impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Value(self.0.subst_shift(var, val)) + match &*self.as_valuef() { + // If the var matches, we can just reuse the provided value instead of copying it. + // We also check that the types match, if in debug mode. + ValueF::Var(v) if v == var => { + if let Ok(self_ty) = self.get_type() { + val.check_type(&self_ty.subst_shift(var, val)); + } + val.clone() + } + _ => Value(self.0.subst_shift(var, val)), + } } } @@ -282,7 +300,6 @@ impl Subst for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, - // TODO: check type info if self.value if Var(v) and v == var value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), } @@ -300,8 +317,17 @@ impl std::cmp::Eq for Value {} impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); - fmt.debug_tuple(&format!("Value@{:?}", &vint.form)) - .field(&vint.value) - .finish() + if let ValueF::Const(c) = &vint.value { + write!(fmt, "{:?}", c) + } else { + let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); + x.field("value", &vint.value); + if let Some(ty) = vint.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } } } -- cgit v1.2.3 From a7363042a16364a6dafdd545f4069dcf04a4197e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 27 Aug 2019 23:18:13 +0200 Subject: Rename SubExpr to Expr, and Expr to RawExpr For clarity, and consistency with Value --- dhall/src/core/value.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 21ac288..49e30cd 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -9,7 +9,7 @@ use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf}; use crate::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::phase::{NormalizedSubExpr, Typed}; +use crate::phase::{NormalizedExpr, Typed}; #[derive(Debug, Clone, Copy)] pub(crate) enum Form { @@ -166,11 +166,11 @@ impl Value { } // TODO: rename `normalize_to_expr` - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + pub(crate) fn to_expr(&self) -> NormalizedExpr { self.as_whnf().normalize_to_expr() } // TODO: rename `normalize_to_expr_maybe_alpha` - pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { self.as_whnf().normalize_to_expr_maybe_alpha(true) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { @@ -226,7 +226,7 @@ impl Value { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> NormalizedSubExpr { + ) -> NormalizedExpr { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } -- cgit v1.2.3 From 55c127e70eb484df486a45b25bcf03479eebda10 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2019 13:49:27 +0200 Subject: Cleanup conversion of `Value` to `Expr` --- dhall/src/core/value.rs | 34 ++++++++++++++-------------------- 1 file changed, 14 insertions(+), 20 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 49e30cd..3cccb1d 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,6 +44,15 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc>); +#[derive(Copy, Clone)] +/// Controls conversion from `Value` to `Expr` +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -158,20 +167,12 @@ impl Value { self.normalize_whnf(); self.as_valuef() } - /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut - /// panics. - pub(crate) fn as_nf(&self) -> Ref { - self.normalize_nf(); - self.as_valuef() - } - // TODO: rename `normalize_to_expr` - pub(crate) fn to_expr(&self) -> NormalizedExpr { - self.as_whnf().normalize_to_expr() - } - // TODO: rename `normalize_to_expr_maybe_alpha` - pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr { - self.as_whnf().normalize_to_expr_maybe_alpha(true) + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + if opts.normalize { + self.normalize_whnf(); + } + self.as_valuef().to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { self.as_whnf().clone() @@ -223,13 +224,6 @@ impl Value { } } - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> NormalizedExpr { - self.as_nf().normalize_to_expr_maybe_alpha(alpha) - } - pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { ValueF::Pi(x, t, e) => { -- cgit v1.2.3