From 1ed3123aeb3c9272b6810605a7ee781c42095f09 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:20:35 +0200 Subject: Swap Typed and TypeThunk --- dhall/src/core/thunk.rs | 125 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 104 insertions(+), 21 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index f41579c..740ecbc 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -1,15 +1,18 @@ +use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{ExprF, X}; +use dhall_syntax::{Const, ExprF, X}; -use crate::core::context::NormalizationContext; +use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; -use crate::phase::{Type, Typed}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -42,7 +45,16 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub struct TypeThunk(Typed); +pub enum TypeThunk { + // Any value, along with (optionally) its type + Untyped(Thunk), + Typed(Thunk, Box), + // One of the base higher-kinded typed. + // Used to avoid storing the same tower ot Type->Kind->Sort + // over and over again. Also enables having Sort as a type + // even though it doesn't itself have a type. + Const(Const), +} impl ThunkInternal { fn into_thunk(self) -> Thunk { @@ -190,39 +202,94 @@ impl TypeThunk { } pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk(Typed::from_thunk_untyped(th)) + TypeThunk::from_thunk_untyped(th) } pub fn from_type(t: Type) -> TypeThunk { - TypeThunk(t) + t.into_typethunk() } - pub fn normalize_mut(&mut self) { - self.0.normalize_mut() + pub fn normalize_nf(&self) -> Value { + match self { + TypeThunk::Const(c) => Value::Const(*c), + TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + thunk.normalize_nf().clone() + } + } } - pub fn normalize_nf(&self) -> Value { - self.0.to_value().normalize() + pub fn to_typed(&self) -> Typed { + self.clone().into_typed() } - pub fn to_value(&self) -> Value { - self.0.to_value() + pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub fn to_thunk(&self) -> Thunk { - self.0.to_thunk() + pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + TypeThunk::Typed(th, Box::new(t)) + } + pub fn from_thunk_untyped(th: Thunk) -> Self { + TypeThunk::Untyped(th) + } + pub fn from_const(c: Const) -> Self { + TypeThunk::Const(c) + } + pub fn from_value_untyped(v: Value) -> Self { + TypeThunk::from_thunk_untyped(Thunk::from_value(v)) } + // TODO: Avoid cloning if possible + pub fn to_value(&self) -> Value { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), + TypeThunk::Const(c) => Value::Const(*c), + } + } + pub fn to_expr(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr() + } + pub fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_value().normalize_to_expr_maybe_alpha(true) + } + pub fn to_thunk(&self) -> Thunk { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), + TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + } + } pub fn to_type(&self) -> Type { - self.0.to_type() + self.clone().into_typed().into_type() + } + pub fn into_typed(self) -> Typed { + Typed::from_typethunk(self) + } + pub fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_value() { + Value::Const(c) => Some(*c), + _ => None, + } } - pub fn to_typed(&self) -> Typed { - self.0.clone() + pub fn normalize_mut(&mut self) { + match self { + TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + th.normalize_mut() + } + TypeThunk::Const(_) => {} + } } - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { - self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + pub fn get_type(&self) -> Result, TypeError> { + match self { + TypeThunk::Untyped(_) => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, + )), + TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + } } } @@ -254,7 +321,14 @@ impl Shift for ThunkInternal { impl Shift for TypeThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypeThunk(self.0.shift(delta, var)?)) + Some(match self { + TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.shift(delta, var)?, + Box::new(t.shift(delta, var)?), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + }) } } @@ -293,7 +367,16 @@ impl Subst for ThunkInternal { impl Subst for TypeThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypeThunk(self.0.subst_shift(var, val)) + match self { + TypeThunk::Untyped(th) => { + TypeThunk::Untyped(th.subst_shift(var, val)) + } + TypeThunk::Typed(th, t) => TypeThunk::Typed( + th.subst_shift(var, val), + Box::new(t.subst_shift(var, val)), + ), + TypeThunk::Const(c) => TypeThunk::Const(*c), + } } } -- cgit v1.2.3 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/thunk.rs | 68 +++++++++++++++++++++++++------------------------ 1 file changed, 35 insertions(+), 33 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 740ecbc..38c54f7 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -45,7 +45,7 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub enum TypeThunk { +pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), @@ -196,23 +196,23 @@ impl Thunk { } } -impl TypeThunk { - pub fn from_value(v: Value) -> TypeThunk { - TypeThunk::from_thunk(Thunk::from_value(v)) +impl TypedThunk { + pub fn from_value(v: Value) -> TypedThunk { + TypedThunk::from_thunk(Thunk::from_value(v)) } - pub fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk::from_thunk_untyped(th) + pub fn from_thunk(th: Thunk) -> TypedThunk { + TypedThunk::from_thunk_untyped(th) } - pub fn from_type(t: Type) -> TypeThunk { + pub fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } pub fn normalize_nf(&self) -> Value { match self { - TypeThunk::Const(c) => Value::Const(*c), - TypeThunk::Untyped(thunk) | TypeThunk::Typed(thunk, _) => { + TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } } @@ -227,23 +227,23 @@ impl TypeThunk { } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - TypeThunk::Typed(th, Box::new(t)) + TypedThunk::Typed(th, Box::new(t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - TypeThunk::Untyped(th) + TypedThunk::Untyped(th) } pub fn from_const(c: Const) -> Self { - TypeThunk::Const(c) + TypedThunk::Const(c) } pub fn from_value_untyped(v: Value) -> Self { - TypeThunk::from_thunk_untyped(Thunk::from_value(v)) + TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.to_value(), - TypeThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), + TypedThunk::Const(c) => Value::Const(*c), } } pub fn to_expr(&self) -> NormalizedSubExpr { @@ -254,8 +254,8 @@ impl TypeThunk { } pub fn to_thunk(&self) -> Thunk { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => th.clone(), - TypeThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), + TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), } } pub fn to_type(&self) -> Type { @@ -274,21 +274,21 @@ impl TypeThunk { pub fn normalize_mut(&mut self) { match self { - TypeThunk::Untyped(th) | TypeThunk::Typed(th, _) => { + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.normalize_mut() } - TypeThunk::Const(_) => {} + TypedThunk::Const(_) => {} } } pub fn get_type(&self) -> Result, TypeError> { match self { - TypeThunk::Untyped(_) => Err(TypeError::new( + TypedThunk::Untyped(_) => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, )), - TypeThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), - TypeThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), + TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), + TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } } @@ -319,15 +319,17 @@ impl Shift for ThunkInternal { } } -impl Shift for TypeThunk { +impl Shift for TypedThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - TypeThunk::Untyped(th) => TypeThunk::Untyped(th.shift(delta, var)?), - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.shift(delta, var)?) + } + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.shift(delta, var)?, Box::new(t.shift(delta, var)?), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), }) } } @@ -365,17 +367,17 @@ impl Subst for ThunkInternal { } } -impl Subst for TypeThunk { +impl Subst for TypedThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - TypeThunk::Untyped(th) => { - TypeThunk::Untyped(th.subst_shift(var, val)) + TypedThunk::Untyped(th) => { + TypedThunk::Untyped(th.subst_shift(var, val)) } - TypeThunk::Typed(th, t) => TypeThunk::Typed( + TypedThunk::Typed(th, t) => TypedThunk::Typed( th.subst_shift(var, val), Box::new(t.subst_shift(var, val)), ), - TypeThunk::Const(c) => TypeThunk::Const(*c), + TypedThunk::Const(c) => TypedThunk::Const(*c), } } } @@ -387,9 +389,9 @@ impl std::cmp::PartialEq for Thunk { } impl std::cmp::Eq for Thunk {} -impl std::cmp::PartialEq for TypeThunk { +impl std::cmp::PartialEq for TypedThunk { fn eq(&self, other: &Self) -> bool { self.to_value() == other.to_value() } } -impl std::cmp::Eq for TypeThunk {} +impl std::cmp::Eq for TypedThunk {} -- cgit v1.2.3 From cbd62bb57bcc94e0133c57437488a5af22a0b1c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 Aug 2019 17:34:38 +0200 Subject: Typos --- dhall/src/core/thunk.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 38c54f7..c18014e 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -49,9 +49,9 @@ pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), - // One of the base higher-kinded typed. + // One of the base higher-kinded types. // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a type + // over and over again. Also enables having Sort as a value // even though it doesn't itself have a type. Const(Const), } -- 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/thunk.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index c18014e..4d193f9 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -2,7 +2,7 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell}; use std::rc::Rc; -use dhall_syntax::{Const, ExprF, X}; +use dhall_syntax::{Const, ExprF}; use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::value::Value; @@ -12,7 +12,7 @@ use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; use crate::phase::typecheck::type_of_const; -use crate::phase::{NormalizedSubExpr, Type, Typed}; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; #[derive(Debug, Clone, Copy)] enum Marker { @@ -30,7 +30,7 @@ enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. - PartialExpr(ExprF), + PartialExpr(ExprF), /// Partially normalized value. /// Invariant: if the marker is `NF`, the value must be fully normalized Value(Marker, Value), @@ -123,7 +123,7 @@ impl Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF) -> Thunk { + pub fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } @@ -309,7 +309,7 @@ impl Shift for ThunkInternal { 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)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +356,7 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - X::clone, + Normalized::clone, ), ), ThunkInternal::Value(_, v) => { -- 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/thunk.rs | 2 -- 1 file changed, 2 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 4d193f9..7c5c537 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -309,7 +309,6 @@ impl Shift for ThunkInternal { 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)), )?, ), ThunkInternal::Value(m, v) => { @@ -356,7 +355,6 @@ impl Subst for ThunkInternal { &val.under_binder(x), ) }, - Normalized::clone, ), ), ThunkInternal::Value(_, v) => { -- cgit v1.2.3 From a9804009f405be7e8a89e301f280ee9d51b57e5e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 15 Aug 2019 13:08:25 +0200 Subject: Custom Debug impls to improve debug legibility --- dhall/src/core/thunk.rs | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 7c5c537..14d8792 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -39,7 +39,7 @@ enum ThunkInternal { /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, /// sharing computation automatically. /// Uses a RefCell to share computation. -#[derive(Debug, Clone)] +#[derive(Clone)] pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve @@ -393,3 +393,22 @@ impl std::cmp::PartialEq for TypedThunk { } } impl std::cmp::Eq for TypedThunk {} + +impl std::fmt::Debug for Thunk { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let b: &ThunkInternal = &self.0.borrow(); + match b { + ThunkInternal::Value(m, v) => { + f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() + } + ThunkInternal::PartialExpr(e) => { + f.debug_tuple("Thunk@PartialExpr").field(e).finish() + } + ThunkInternal::Unnormalized(ctx, e) => f + .debug_tuple("Thunk@Unnormalized") + .field(ctx) + .field(e) + .finish(), + } + } +} -- 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/thunk.rs | 56 ++++++++++++++++++++++++------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 14d8792..54a5442 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -115,21 +115,21 @@ impl ThunkInternal { } impl Thunk { - pub fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { + pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { ThunkInternal::Unnormalized(ctx, e).into_thunk() } - pub fn from_value(v: Value) -> Thunk { + pub(crate) fn from_value(v: Value) -> Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub fn from_partial_expr(e: ExprF) -> Thunk { + pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } // Normalizes contents to normal form; faster than `normalize_nf` if // no one else shares this thunk - pub fn normalize_mut(&mut self) { + pub(crate) fn normalize_mut(&mut self) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner Some(refcell) => RefCell::get_mut(refcell).normalize_nf(), @@ -167,37 +167,37 @@ impl Thunk { // WARNING: avoid normalizing any thunk while holding on to this ref // or you could run into BorrowMut panics - pub fn normalize_nf(&self) -> Ref { + pub(crate) fn normalize_nf(&self) -> Ref { self.do_normalize_nf(); Ref::map(self.0.borrow(), ThunkInternal::as_nf) } // WARNING: avoid normalizing any thunk while holding on to this ref // or you could run into BorrowMut panics - pub fn as_value(&self) -> Ref { + pub(crate) fn as_value(&self) -> Ref { self.do_normalize_whnf(); Ref::map(self.0.borrow(), ThunkInternal::as_whnf) } - pub fn to_value(&self) -> Value { + pub(crate) fn to_value(&self) -> Value { self.as_value().clone() } - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub fn app_val(&self, val: Value) -> Value { + pub(crate) fn app_val(&self, val: Value) -> Value { self.app_thunk(val.into_thunk()) } - pub fn app_thunk(&self, th: Thunk) -> Value { + pub(crate) fn app_thunk(&self, th: Thunk) -> Value { apply_any(self.clone(), th) } } impl TypedThunk { - pub fn from_value(v: Value) -> TypedThunk { + pub(crate) fn from_value(v: Value) -> TypedThunk { TypedThunk::from_thunk(Thunk::from_value(v)) } @@ -205,11 +205,11 @@ impl TypedThunk { TypedThunk::from_thunk_untyped(th) } - pub fn from_type(t: Type) -> TypedThunk { + pub(crate) fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } - pub fn normalize_nf(&self) -> Value { + pub(crate) fn normalize_nf(&self) -> Value { match self { TypedThunk::Const(c) => Value::Const(*c), TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { @@ -218,53 +218,53 @@ impl TypedThunk { } } - pub fn to_typed(&self) -> Typed { + pub(crate) fn to_typed(&self) -> Typed { self.clone().into_typed() } - pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { + pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { TypedThunk::Typed(th, Box::new(t)) } - pub fn from_thunk_untyped(th: Thunk) -> Self { + pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { TypedThunk::Untyped(th) } - pub fn from_const(c: Const) -> Self { + pub(crate) fn from_const(c: Const) -> Self { TypedThunk::Const(c) } - pub fn from_value_untyped(v: Value) -> Self { + pub(crate) fn from_value_untyped(v: Value) -> Self { TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } // TODO: Avoid cloning if possible - pub fn to_value(&self) -> Value { + pub(crate) fn to_value(&self) -> Value { match self { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), TypedThunk::Const(c) => Value::Const(*c), } } - pub fn to_expr(&self) -> NormalizedSubExpr { + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { self.to_value().normalize_to_expr() } - pub fn to_expr_alpha(&self) -> NormalizedSubExpr { + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.to_value().normalize_to_expr_maybe_alpha(true) } - pub fn to_thunk(&self) -> Thunk { + pub(crate) fn to_thunk(&self) -> Thunk { match self { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), } } - pub fn to_type(&self) -> Type { + pub(crate) fn to_type(&self) -> Type { self.clone().into_typed().into_type() } - pub fn into_typed(self) -> Typed { + pub(crate) fn into_typed(self) -> Typed { Typed::from_typethunk(self) } - pub fn as_const(&self) -> Option { + pub(crate) fn as_const(&self) -> Option { // TODO: avoid clone match &self.to_value() { Value::Const(c) => Some(*c), @@ -272,7 +272,7 @@ impl TypedThunk { } } - pub fn normalize_mut(&mut self) { + pub(crate) fn normalize_mut(&mut self) { match self { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.normalize_mut() @@ -281,7 +281,7 @@ impl TypedThunk { } } - pub fn get_type(&self) -> Result, TypeError> { + pub(crate) fn get_type(&self) -> Result, TypeError> { match self { TypedThunk::Untyped(_) => Err(TypeError::new( &TypecheckContext::new(), -- 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/thunk.rs | 59 ++++++++++++++----------------------------------- 1 file changed, 17 insertions(+), 42 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 54a5442..87541d3 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -4,13 +4,11 @@ use std::rc::Rc; use dhall_syntax::{Const, ExprF}; -use crate::core::context::{NormalizationContext, TypecheckContext}; +use crate::core::context::TypecheckContext; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{ - apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, -}; +use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; use crate::phase::typecheck::type_of_const; use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; @@ -25,8 +23,6 @@ use Marker::{NF, WHNF}; #[derive(Debug)] enum ThunkInternal { - /// Non-normalized value alongside a normalization context - Unnormalized(NormalizationContext, InputSubExpr), /// Partially normalized value whose subexpressions have been thunked (this is returned from /// typechecking). Note that this is different from `Value::PartialExpr` because there is no /// requirement of WHNF here. @@ -63,12 +59,6 @@ impl ThunkInternal { fn normalize_whnf(&mut self) { match self { - ThunkInternal::Unnormalized(ctx, e) => { - *self = ThunkInternal::Value( - WHNF, - normalize_whnf(ctx.clone(), e.clone()), - ) - } ThunkInternal::PartialExpr(e) => { *self = ThunkInternal::Value(WHNF, normalize_one_layer(e.clone())) @@ -80,8 +70,7 @@ impl ThunkInternal { fn normalize_nf(&mut self) { match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => { + ThunkInternal::PartialExpr(_) => { self.normalize_whnf(); self.normalize_nf(); } @@ -97,8 +86,7 @@ impl ThunkInternal { // Always use normalize_whnf before fn as_whnf(&self) -> &Value { match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => unreachable!(), + ThunkInternal::PartialExpr(_) => unreachable!(), ThunkInternal::Value(_, v) => v, } } @@ -106,19 +94,15 @@ impl ThunkInternal { // Always use normalize_nf before fn as_nf(&self) -> &Value { match self { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) - | ThunkInternal::Value(WHNF, _) => unreachable!(), + ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { + unreachable!() + } ThunkInternal::Value(NF, v) => v, } } } impl Thunk { - pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { - ThunkInternal::Unnormalized(ctx, e).into_thunk() - } - pub(crate) fn from_value(v: Value) -> Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } @@ -141,8 +125,7 @@ impl Thunk { fn do_normalize_whnf(&self) { let borrow = self.0.borrow(); match &*borrow { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) => { + ThunkInternal::PartialExpr(_) => { drop(borrow); self.0.borrow_mut().normalize_whnf(); } @@ -154,9 +137,7 @@ impl Thunk { fn do_normalize_nf(&self) { let borrow = self.0.borrow(); match &*borrow { - ThunkInternal::Unnormalized(_, _) - | ThunkInternal::PartialExpr(_) - | ThunkInternal::Value(WHNF, _) => { + ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { drop(borrow); self.0.borrow_mut().normalize_nf(); } @@ -183,7 +164,10 @@ impl Thunk { self.as_value().clone() } - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } @@ -222,7 +206,10 @@ impl TypedThunk { self.clone().into_typed() } - pub(crate) fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } @@ -302,9 +289,6 @@ impl Shift for Thunk { impl Shift for ThunkInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ThunkInternal::Unnormalized(ctx, e) => { - ThunkInternal::Unnormalized(ctx.shift(delta, var)?, e.clone()) - } ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr( e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -342,10 +326,6 @@ impl Subst for Thunk { impl Subst for ThunkInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - ThunkInternal::Unnormalized(ctx, e) => ThunkInternal::Unnormalized( - ctx.subst_shift(var, val), - e.clone(), - ), ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr( e.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), @@ -404,11 +384,6 @@ impl std::fmt::Debug for Thunk { ThunkInternal::PartialExpr(e) => { f.debug_tuple("Thunk@PartialExpr").field(e).finish() } - ThunkInternal::Unnormalized(ctx, e) => f - .debug_tuple("Thunk@Unnormalized") - .field(ctx) - .field(e) - .finish(), } } } -- cgit v1.2.3 From 45fb07f74f19919f742be6fe7793dc72d4022f26 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:16:40 +0200 Subject: Try to minimize untyped TypedThunks --- dhall/src/core/thunk.rs | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 87541d3..5f96ec8 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -182,11 +182,7 @@ impl Thunk { impl TypedThunk { pub(crate) fn from_value(v: Value) -> TypedThunk { - TypedThunk::from_thunk(Thunk::from_value(v)) - } - - pub fn from_thunk(th: Thunk) -> TypedThunk { - TypedThunk::from_thunk_untyped(th) + TypedThunk::from_thunk_untyped(Thunk::from_value(v)) } pub(crate) fn from_type(t: Type) -> TypedThunk { @@ -216,14 +212,17 @@ impl TypedThunk { pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { TypedThunk::Typed(th, Box::new(t)) } + pub fn from_thunk_simple_type(th: Thunk) -> Self { + TypedThunk::from_thunk_and_type(th, Type::const_type()) + } pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { TypedThunk::Untyped(th) } pub(crate) fn from_const(c: Const) -> Self { TypedThunk::Const(c) } - pub(crate) fn from_value_untyped(v: Value) -> Self { - TypedThunk::from_thunk_untyped(Thunk::from_value(v)) + pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self { + TypedThunk::from_thunk_and_type(Thunk::from_value(v), t) } // TODO: Avoid cloning if possible -- 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/thunk.rs | 90 +++++++++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 44 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 5f96ec8..cf7c097 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use dhall_syntax::{Const, ExprF}; use crate::core::context::TypecheckContext; -use crate::core::value::Value; +use crate::core::value::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; @@ -24,12 +24,12 @@ use Marker::{NF, WHNF}; #[derive(Debug)] enum ThunkInternal { /// Partially normalized value whose subexpressions have been thunked (this is returned from - /// typechecking). Note that this is different from `Value::PartialExpr` because there is no + /// 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 - Value(Marker, Value), + ValueF(Marker, ValueF), } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -61,10 +61,10 @@ impl ThunkInternal { match self { ThunkInternal::PartialExpr(e) => { *self = - ThunkInternal::Value(WHNF, normalize_one_layer(e.clone())) + ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } // Already at least in WHNF - ThunkInternal::Value(_, _) => {} + ThunkInternal::ValueF(_, _) => {} } } @@ -74,37 +74,37 @@ impl ThunkInternal { self.normalize_whnf(); self.normalize_nf(); } - ThunkInternal::Value(m @ WHNF, v) => { + ThunkInternal::ValueF(m @ WHNF, v) => { v.normalize_mut(); *m = NF; } // Already in NF - ThunkInternal::Value(NF, _) => {} + ThunkInternal::ValueF(NF, _) => {} } } // Always use normalize_whnf before - fn as_whnf(&self) -> &Value { + fn as_whnf(&self) -> &ValueF { match self { ThunkInternal::PartialExpr(_) => unreachable!(), - ThunkInternal::Value(_, v) => v, + ThunkInternal::ValueF(_, v) => v, } } // Always use normalize_nf before - fn as_nf(&self) -> &Value { + fn as_nf(&self) -> &ValueF { match self { - ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { + ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { unreachable!() } - ThunkInternal::Value(NF, v) => v, + ThunkInternal::ValueF(NF, v) => v, } } } impl Thunk { - pub(crate) fn from_value(v: Value) -> Thunk { - ThunkInternal::Value(WHNF, v).into_thunk() + pub(crate) fn from_valuef(v: ValueF) -> Thunk { + ThunkInternal::ValueF(WHNF, v).into_thunk() } pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { @@ -130,38 +130,38 @@ impl Thunk { self.0.borrow_mut().normalize_whnf(); } // Already at least in WHNF - ThunkInternal::Value(_, _) => {} + ThunkInternal::ValueF(_, _) => {} } } fn do_normalize_nf(&self) { let borrow = self.0.borrow(); match &*borrow { - ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => { + ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { drop(borrow); self.0.borrow_mut().normalize_nf(); } // Already in NF - ThunkInternal::Value(NF, _) => {} + ThunkInternal::ValueF(NF, _) => {} } } // 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 { + pub(crate) fn normalize_nf(&self) -> Ref { self.do_normalize_nf(); Ref::map(self.0.borrow(), ThunkInternal::as_nf) } // WARNING: avoid normalizing any thunk while holding on to this ref // or you could run into BorrowMut panics - pub(crate) fn as_value(&self) -> Ref { + pub(crate) fn as_valuef(&self) -> Ref { self.do_normalize_whnf(); Ref::map(self.0.borrow(), ThunkInternal::as_whnf) } - pub(crate) fn to_value(&self) -> Value { - self.as_value().clone() + pub(crate) fn to_valuef(&self) -> ValueF { + self.as_valuef().clone() } pub(crate) fn normalize_to_expr_maybe_alpha( @@ -171,27 +171,27 @@ impl Thunk { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_val(&self, val: Value) -> Value { + pub(crate) fn app_val(&self, val: ValueF) -> ValueF { self.app_thunk(val.into_thunk()) } - pub(crate) fn app_thunk(&self, th: Thunk) -> Value { + pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF { apply_any(self.clone(), th) } } impl TypedThunk { - pub(crate) fn from_value(v: Value) -> TypedThunk { - TypedThunk::from_thunk_untyped(Thunk::from_value(v)) + pub(crate) fn from_valuef(v: ValueF) -> TypedThunk { + TypedThunk::from_thunk_untyped(Thunk::from_valuef(v)) } pub(crate) fn from_type(t: Type) -> TypedThunk { t.into_typethunk() } - pub(crate) fn normalize_nf(&self) -> Value { + pub(crate) fn normalize_nf(&self) -> ValueF { match self { - TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Const(c) => ValueF::Const(*c), TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } @@ -221,27 +221,29 @@ impl TypedThunk { pub(crate) fn from_const(c: Const) -> Self { TypedThunk::Const(c) } - pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self { - TypedThunk::from_thunk_and_type(Thunk::from_value(v), t) + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t) } // TODO: Avoid cloning if possible - pub(crate) fn to_value(&self) -> Value { + pub(crate) fn to_valuef(&self) -> ValueF { match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(), - TypedThunk::Const(c) => Value::Const(*c), + TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { + th.to_valuef() + } + TypedThunk::Const(c) => ValueF::Const(*c), } } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr() + self.to_valuef().normalize_to_expr() } pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr_maybe_alpha(true) + self.to_valuef().normalize_to_expr_maybe_alpha(true) } pub(crate) fn to_thunk(&self) -> Thunk { match self { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), - TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)), + TypedThunk::Const(c) => Thunk::from_valuef(ValueF::Const(*c)), } } pub(crate) fn to_type(&self) -> Type { @@ -252,8 +254,8 @@ impl TypedThunk { } pub(crate) fn as_const(&self) -> Option { // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), _ => None, } } @@ -294,8 +296,8 @@ impl Shift for ThunkInternal { |x, v| Ok(v.shift(delta, &var.under_binder(x))?), )?, ), - ThunkInternal::Value(m, v) => { - ThunkInternal::Value(*m, v.shift(delta, var)?) + ThunkInternal::ValueF(m, v) => { + ThunkInternal::ValueF(*m, v.shift(delta, var)?) } }) } @@ -336,9 +338,9 @@ impl Subst for ThunkInternal { }, ), ), - ThunkInternal::Value(_, v) => { + ThunkInternal::ValueF(_, v) => { // The resulting value may not stay in normal form after substitution - ThunkInternal::Value(WHNF, v.subst_shift(var, val)) + ThunkInternal::ValueF(WHNF, v.subst_shift(var, val)) } } } @@ -361,14 +363,14 @@ impl Subst for TypedThunk { impl std::cmp::PartialEq for Thunk { fn eq(&self, other: &Self) -> bool { - *self.as_value() == *other.as_value() + *self.as_valuef() == *other.as_valuef() } } impl std::cmp::Eq for Thunk {} impl std::cmp::PartialEq for TypedThunk { fn eq(&self, other: &Self) -> bool { - self.to_value() == other.to_value() + self.to_valuef() == other.to_valuef() } } impl std::cmp::Eq for TypedThunk {} @@ -377,7 +379,7 @@ impl std::fmt::Debug for Thunk { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let b: &ThunkInternal = &self.0.borrow(); match b { - ThunkInternal::Value(m, v) => { + ThunkInternal::ValueF(m, v) => { f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() } ThunkInternal::PartialExpr(e) => { -- cgit v1.2.3 From 9383d55718b86faf4c1734fe8fee3f99730499d4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 20:05:23 +0200 Subject: Remove Const-optimization for now --- dhall/src/core/thunk.rs | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index cf7c097..db68169 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -45,11 +45,6 @@ pub enum TypedThunk { // Any value, along with (optionally) its type Untyped(Thunk), Typed(Thunk, Box), - // One of the base higher-kinded types. - // Used to avoid storing the same tower ot Type->Kind->Sort - // over and over again. Also enables having Sort as a value - // even though it doesn't itself have a type. - Const(Const), } impl ThunkInternal { @@ -191,7 +186,6 @@ impl TypedThunk { pub(crate) fn normalize_nf(&self) -> ValueF { match self { - TypedThunk::Const(c) => ValueF::Const(*c), TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { thunk.normalize_nf().clone() } @@ -219,7 +213,10 @@ impl TypedThunk { TypedThunk::Untyped(th) } pub(crate) fn from_const(c: Const) -> Self { - TypedThunk::Const(c) + match type_of_const(c) { + Ok(t) => TypedThunk::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => TypedThunk::from_valuef(ValueF::Const(c)), + } } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t) @@ -231,7 +228,6 @@ impl TypedThunk { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.to_valuef() } - TypedThunk::Const(c) => ValueF::Const(*c), } } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { @@ -243,7 +239,6 @@ impl TypedThunk { pub(crate) fn to_thunk(&self) -> Thunk { match self { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), - TypedThunk::Const(c) => Thunk::from_valuef(ValueF::Const(*c)), } } pub(crate) fn to_type(&self) -> Type { @@ -265,18 +260,16 @@ impl TypedThunk { TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { th.normalize_mut() } - TypedThunk::Const(_) => {} } } pub(crate) fn get_type(&self) -> Result, TypeError> { match self { - TypedThunk::Untyped(_) => Err(TypeError::new( + TypedThunk::Untyped(th) => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, )), TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), - TypedThunk::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } } @@ -313,7 +306,6 @@ impl Shift for TypedThunk { th.shift(delta, var)?, Box::new(t.shift(delta, var)?), ), - TypedThunk::Const(c) => TypedThunk::Const(*c), }) } } @@ -356,7 +348,6 @@ impl Subst for TypedThunk { th.subst_shift(var, val), Box::new(t.subst_shift(var, val)), ), - TypedThunk::Const(c) => TypedThunk::Const(*c), } } } -- cgit v1.2.3 From 961dbc0e9d52691de590568c01a22d28c04fe2f5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 21:59:11 +0200 Subject: Store type in Thunk --- dhall/src/core/thunk.rs | 94 +++++++++++++++++++++---------------------------- 1 file changed, 40 insertions(+), 54 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index db68169..e315a90 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -33,23 +33,18 @@ enum ThunkInternal { } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, -/// sharing computation automatically. -/// Uses a RefCell to share computation. +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a Type from the typechecking phase to preserve type information through +/// the normalization phase. #[derive(Clone)] -pub struct Thunk(Rc>); +pub struct Thunk(Rc>, Option>); -/// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve -/// type information through the normalization phase. #[derive(Debug, Clone)] -pub enum TypedThunk { - // Any value, along with (optionally) its type - Untyped(Thunk), - Typed(Thunk, Box), -} +pub struct TypedThunk(Thunk); impl ThunkInternal { - fn into_thunk(self) -> Thunk { - Thunk(Rc::new(RefCell::new(self))) + fn into_thunk(self, t: Option>) -> Thunk { + Thunk(Rc::new(RefCell::new(self)), t) } fn normalize_whnf(&mut self) { @@ -99,11 +94,16 @@ impl ThunkInternal { impl Thunk { pub(crate) fn from_valuef(v: ValueF) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk() + ThunkInternal::ValueF(WHNF, v).into_thunk(None) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk { + ThunkInternal::ValueF(WHNF, v).into_thunk(Some(Box::new(t))) } - pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { - ThunkInternal::PartialExpr(e).into_thunk() + ThunkInternal::PartialExpr(e).into_thunk(None) + } + pub(crate) fn with_type(self, t: Type) -> Thunk { + Thunk(self.0, Some(Box::new(t))) } // Normalizes contents to normal form; faster than `normalize_nf` if @@ -186,9 +186,7 @@ impl TypedThunk { pub(crate) fn normalize_nf(&self) -> ValueF { match self { - TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => { - thunk.normalize_nf().clone() - } + TypedThunk(thunk) => thunk.normalize_nf().clone(), } } @@ -204,13 +202,13 @@ impl TypedThunk { } pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - TypedThunk::Typed(th, Box::new(t)) + TypedThunk(th.with_type(t)) } pub fn from_thunk_simple_type(th: Thunk) -> Self { TypedThunk::from_thunk_and_type(th, Type::const_type()) } pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - TypedThunk::Untyped(th) + TypedThunk(th) } pub(crate) fn from_const(c: Const) -> Self { match type_of_const(c) { @@ -219,16 +217,14 @@ impl TypedThunk { } } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t) + TypedThunk::from_thunk_and_type( + Thunk::from_valuef_and_type(v, t.clone()), + t, + ) } - // TODO: Avoid cloning if possible pub(crate) fn to_valuef(&self) -> ValueF { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { - th.to_valuef() - } - } + self.0.to_valuef() } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { self.to_valuef().normalize_to_expr() @@ -237,9 +233,7 @@ impl TypedThunk { self.to_valuef().normalize_to_expr_maybe_alpha(true) } pub(crate) fn to_thunk(&self) -> Thunk { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(), - } + self.0.clone() } pub(crate) fn to_type(&self) -> Type { self.clone().into_typed().into_type() @@ -256,27 +250,28 @@ impl TypedThunk { } pub(crate) fn normalize_mut(&mut self) { - match self { - TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => { - th.normalize_mut() - } - } + self.0.normalize_mut() } pub(crate) fn get_type(&self) -> Result, TypeError> { - match self { - TypedThunk::Untyped(th) => Err(TypeError::new( + match &(self.0).1 { + Some(t) => Ok(Cow::Borrowed(&*t)), + None => Err(TypeError::new( &TypecheckContext::new(), TypeMessage::Untyped, )), - TypedThunk::Typed(_, t) => Ok(Cow::Borrowed(t)), } } } impl Shift for Thunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(self.0.borrow().shift(delta, var)?.into_thunk()) + Some( + self.0 + .borrow() + .shift(delta, var)? + .into_thunk(self.1.shift(delta, var)?), + ) } } @@ -299,20 +294,17 @@ impl Shift for ThunkInternal { impl Shift for TypedThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - TypedThunk::Untyped(th) => { - TypedThunk::Untyped(th.shift(delta, var)?) - } - TypedThunk::Typed(th, t) => TypedThunk::Typed( - th.shift(delta, var)?, - Box::new(t.shift(delta, var)?), - ), + TypedThunk(th) => TypedThunk(th.shift(delta, var)?), }) } } impl Subst for Thunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - self.0.borrow().subst_shift(var, val).into_thunk() + self.0 + .borrow() + .subst_shift(var, val) + .into_thunk(self.1.subst_shift(var, val)) } } @@ -341,13 +333,7 @@ impl Subst for ThunkInternal { impl Subst for TypedThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - TypedThunk::Untyped(th) => { - TypedThunk::Untyped(th.subst_shift(var, val)) - } - TypedThunk::Typed(th, t) => TypedThunk::Typed( - th.subst_shift(var, val), - Box::new(t.subst_shift(var, val)), - ), + TypedThunk(th) => TypedThunk(th.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/thunk.rs | 35 ++++++++--------------------------- 1 file changed, 8 insertions(+), 27 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index e315a90..b6358ef 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -266,24 +266,16 @@ impl TypedThunk { impl Shift for Thunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some( - self.0 - .borrow() - .shift(delta, var)? - .into_thunk(self.1.shift(delta, var)?), - ) + Some(Thunk(self.0.shift(delta, var)?, self.1.shift(delta, var)?)) } } impl Shift for ThunkInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ThunkInternal::PartialExpr(e) => ThunkInternal::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))?), - )?, - ), + ThunkInternal::PartialExpr(e) => { + ThunkInternal::PartialExpr(e.shift(delta, var)?) + } ThunkInternal::ValueF(m, v) => { ThunkInternal::ValueF(*m, v.shift(delta, var)?) } @@ -301,27 +293,16 @@ impl Shift for TypedThunk { impl Subst for Thunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - self.0 - .borrow() - .subst_shift(var, val) - .into_thunk(self.1.subst_shift(var, val)) + Thunk(self.0.subst_shift(var, val), self.1.subst_shift(var, val)) } } impl Subst for ThunkInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr( - 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), - ) - }, - ), - ), + ThunkInternal::PartialExpr(e) => { + ThunkInternal::PartialExpr(e.subst_shift(var, val)) + } ThunkInternal::ValueF(_, v) => { // The resulting value may not stay in normal form after substitution ThunkInternal::ValueF(WHNF, v.subst_shift(var, val)) -- cgit v1.2.3 From 8dec798929f35df15a7bc3a6caa4f0c7954c4ffc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 23:17:46 +0200 Subject: Share type alongside the value in a thunk --- dhall/src/core/thunk.rs | 138 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 98 insertions(+), 40 deletions(-) (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index b6358ef..325a410 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -1,5 +1,5 @@ use std::borrow::Cow; -use std::cell::{Ref, RefCell}; +use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; use dhall_syntax::{Const, ExprF}; @@ -21,7 +21,7 @@ enum Marker { } use Marker::{NF, WHNF}; -#[derive(Debug)] +#[derive(Debug, Clone)] enum ThunkInternal { /// 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 @@ -32,19 +32,29 @@ enum ThunkInternal { ValueF(Marker, ValueF), } +#[derive(Debug)] +struct TypedThunkInternal { + internal: ThunkInternal, + 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 the typechecking phase to preserve type information through /// the normalization phase. #[derive(Clone)] -pub struct Thunk(Rc>, Option>); +pub struct Thunk(Rc>); #[derive(Debug, Clone)] pub struct TypedThunk(Thunk); impl ThunkInternal { - fn into_thunk(self, t: Option>) -> Thunk { - Thunk(Rc::new(RefCell::new(self)), t) + fn into_thunk(self, t: Option) -> Thunk { + TypedThunkInternal { + internal: self, + typ: t, + } + .into_thunk() } fn normalize_whnf(&mut self) { @@ -92,37 +102,78 @@ impl ThunkInternal { } } +impl TypedThunkInternal { + fn into_thunk(self) -> Thunk { + Thunk(Rc::new(RefCell::new(self))) + } + fn as_internal(&self) -> &ThunkInternal { + &self.internal + } + fn as_internal_mut(&mut self) -> &mut ThunkInternal { + &mut self.internal + } + + fn get_type(&self) -> Result { + match &self.typ { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, + )), + } + } +} + impl Thunk { pub(crate) fn from_valuef(v: ValueF) -> Thunk { ThunkInternal::ValueF(WHNF, v).into_thunk(None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk(Some(Box::new(t))) + ThunkInternal::ValueF(WHNF, v).into_thunk(Some(t)) } pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk(None) } pub(crate) fn with_type(self, t: Type) -> Thunk { - Thunk(self.0, Some(Box::new(t))) + self.as_internal().clone().into_thunk(Some(t)) } - // Normalizes contents to normal form; faster than `normalize_nf` if - // no one else shares this thunk - pub(crate) fn normalize_mut(&mut self) { + /// 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 TypedThunkInternal)) { match Rc::get_mut(&mut self.0) { // Mutate directly if sole owner - Some(refcell) => RefCell::get_mut(refcell).normalize_nf(), + Some(refcell) => f(RefCell::get_mut(refcell)), // Otherwise mutate through the refcell - None => self.0.borrow_mut().normalize_nf(), + 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) { + self.mutate_internal(|i| i.as_internal_mut().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(), TypedThunkInternal::as_internal) + } + fn as_internal_mut(&self) -> RefMut { + RefMut::map(self.0.borrow_mut(), TypedThunkInternal::as_internal_mut) + } + fn do_normalize_whnf(&self) { - let borrow = self.0.borrow(); + let borrow = self.as_internal(); match &*borrow { ThunkInternal::PartialExpr(_) => { drop(borrow); - self.0.borrow_mut().normalize_whnf(); + self.as_internal_mut().normalize_whnf(); } // Already at least in WHNF ThunkInternal::ValueF(_, _) => {} @@ -130,11 +181,11 @@ impl Thunk { } fn do_normalize_nf(&self) { - let borrow = self.0.borrow(); + let borrow = self.as_internal(); match &*borrow { ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { drop(borrow); - self.0.borrow_mut().normalize_nf(); + self.as_internal_mut().normalize_nf(); } // Already in NF ThunkInternal::ValueF(NF, _) => {} @@ -145,14 +196,14 @@ impl Thunk { // or you could run into BorrowMut panics pub(crate) fn normalize_nf(&self) -> Ref { self.do_normalize_nf(); - Ref::map(self.0.borrow(), ThunkInternal::as_nf) + Ref::map(self.as_internal(), ThunkInternal::as_nf) } // 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.0.borrow(), ThunkInternal::as_whnf) + Ref::map(self.as_internal(), ThunkInternal::as_whnf) } pub(crate) fn to_valuef(&self) -> ValueF { @@ -173,6 +224,10 @@ impl Thunk { pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF { apply_any(self.clone(), th) } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + Ok(Cow::Owned(self.as_tinternal().get_type()?)) + } } impl TypedThunk { @@ -185,9 +240,7 @@ impl TypedThunk { } pub(crate) fn normalize_nf(&self) -> ValueF { - match self { - TypedThunk(thunk) => thunk.normalize_nf().clone(), - } + self.0.normalize_nf().clone() } pub(crate) fn to_typed(&self) -> Typed { @@ -217,10 +270,7 @@ impl TypedThunk { } } pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - TypedThunk::from_thunk_and_type( - Thunk::from_valuef_and_type(v, t.clone()), - t, - ) + TypedThunk(Thunk::from_valuef_and_type(v, t)) } pub(crate) fn to_valuef(&self) -> ValueF { @@ -254,19 +304,13 @@ impl TypedThunk { } pub(crate) fn get_type(&self) -> Result, TypeError> { - match &(self.0).1 { - Some(t) => Ok(Cow::Borrowed(&*t)), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - } + self.0.get_type() } } impl Shift for Thunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Thunk(self.0.shift(delta, var)?, self.1.shift(delta, var)?)) + Some(Thunk(self.0.shift(delta, var)?)) } } @@ -285,15 +329,22 @@ impl Shift for ThunkInternal { impl Shift for TypedThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - TypedThunk(th) => TypedThunk(th.shift(delta, var)?), + Some(TypedThunk(self.0.shift(delta, var)?)) + } +} + +impl Shift for TypedThunkInternal { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedThunkInternal { + internal: self.internal.shift(delta, var)?, + typ: self.typ.shift(delta, var)?, }) } } impl Subst for Thunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Thunk(self.0.subst_shift(var, val), self.1.subst_shift(var, val)) + Thunk(self.0.subst_shift(var, val)) } } @@ -311,14 +362,21 @@ impl Subst for ThunkInternal { } } -impl Subst for TypedThunk { +impl Subst for TypedThunkInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - TypedThunk(th) => TypedThunk(th.subst_shift(var, val)), + TypedThunkInternal { + internal: self.internal.subst_shift(var, val), + typ: self.typ.subst_shift(var, val), } } } +impl Subst for TypedThunk { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedThunk(self.0.subst_shift(var, val)) + } +} + impl std::cmp::PartialEq for Thunk { fn eq(&self, other: &Self) -> bool { *self.as_valuef() == *other.as_valuef() @@ -335,7 +393,7 @@ impl std::cmp::Eq for TypedThunk {} impl std::fmt::Debug for Thunk { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let b: &ThunkInternal = &self.0.borrow(); + let b: &ThunkInternal = &self.as_internal(); match b { ThunkInternal::ValueF(m, v) => { f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() -- 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/thunk.rs | 406 ------------------------------------------------ 1 file changed, 406 deletions(-) delete mode 100644 dhall/src/core/thunk.rs (limited to 'dhall/src/core/thunk.rs') diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs deleted file mode 100644 index 325a410..0000000 --- a/dhall/src/core/thunk.rs +++ /dev/null @@ -1,406 +0,0 @@ -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::value::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}; - -#[derive(Debug, Clone)] -enum ThunkInternal { - /// 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), -} - -#[derive(Debug)] -struct TypedThunkInternal { - internal: ThunkInternal, - 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 the typechecking phase to preserve type information through -/// the normalization phase. -#[derive(Clone)] -pub struct Thunk(Rc>); - -#[derive(Debug, Clone)] -pub struct TypedThunk(Thunk); - -impl ThunkInternal { - fn into_thunk(self, t: Option) -> Thunk { - TypedThunkInternal { - internal: self, - typ: t, - } - .into_thunk() - } - - fn normalize_whnf(&mut self) { - match self { - ThunkInternal::PartialExpr(e) => { - *self = - ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone())) - } - // Already at least in WHNF - ThunkInternal::ValueF(_, _) => {} - } - } - - fn normalize_nf(&mut self) { - match self { - ThunkInternal::PartialExpr(_) => { - self.normalize_whnf(); - self.normalize_nf(); - } - ThunkInternal::ValueF(m @ WHNF, v) => { - v.normalize_mut(); - *m = NF; - } - // Already in NF - ThunkInternal::ValueF(NF, _) => {} - } - } - - // Always use normalize_whnf before - fn as_whnf(&self) -> &ValueF { - match self { - ThunkInternal::PartialExpr(_) => unreachable!(), - ThunkInternal::ValueF(_, v) => v, - } - } - - // Always use normalize_nf before - fn as_nf(&self) -> &ValueF { - match self { - ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { - unreachable!() - } - ThunkInternal::ValueF(NF, v) => v, - } - } -} - -impl TypedThunkInternal { - fn into_thunk(self) -> Thunk { - Thunk(Rc::new(RefCell::new(self))) - } - fn as_internal(&self) -> &ThunkInternal { - &self.internal - } - fn as_internal_mut(&mut self) -> &mut ThunkInternal { - &mut self.internal - } - - fn get_type(&self) -> Result { - match &self.typ { - Some(t) => Ok(t.clone()), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - } - } -} - -impl Thunk { - pub(crate) fn from_valuef(v: ValueF) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk(None) - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk { - ThunkInternal::ValueF(WHNF, v).into_thunk(Some(t)) - } - pub(crate) fn from_partial_expr(e: ExprF) -> Thunk { - ThunkInternal::PartialExpr(e).into_thunk(None) - } - pub(crate) fn with_type(self, t: Type) -> Thunk { - self.as_internal().clone().into_thunk(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 TypedThunkInternal)) { - 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) { - self.mutate_internal(|i| i.as_internal_mut().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(), TypedThunkInternal::as_internal) - } - fn as_internal_mut(&self) -> RefMut { - RefMut::map(self.0.borrow_mut(), TypedThunkInternal::as_internal_mut) - } - - fn do_normalize_whnf(&self) { - let borrow = self.as_internal(); - match &*borrow { - ThunkInternal::PartialExpr(_) => { - drop(borrow); - self.as_internal_mut().normalize_whnf(); - } - // Already at least in WHNF - ThunkInternal::ValueF(_, _) => {} - } - } - - fn do_normalize_nf(&self) { - let borrow = self.as_internal(); - match &*borrow { - ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => { - drop(borrow); - self.as_internal_mut().normalize_nf(); - } - // Already in NF - ThunkInternal::ValueF(NF, _) => {} - } - } - - // 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(), ThunkInternal::as_nf) - } - - // 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(), ThunkInternal::as_whnf) - } - - 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_val(&self, val: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) - } - - pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF { - apply_any(self.clone(), th) - } - - pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(Cow::Owned(self.as_tinternal().get_type()?)) - } -} - -impl TypedThunk { - pub(crate) fn from_valuef(v: ValueF) -> TypedThunk { - TypedThunk::from_thunk_untyped(Thunk::from_valuef(v)) - } - - pub(crate) fn from_type(t: Type) -> TypedThunk { - t.into_typethunk() - } - - 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_thunk_and_type(th: Thunk, t: Type) -> Self { - TypedThunk(th.with_type(t)) - } - pub fn from_thunk_simple_type(th: Thunk) -> Self { - TypedThunk::from_thunk_and_type(th, Type::const_type()) - } - pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { - TypedThunk(th) - } - pub(crate) fn from_const(c: Const) -> Self { - match type_of_const(c) { - Ok(t) => TypedThunk::from_valuef_and_type(ValueF::Const(c), t), - Err(_) => TypedThunk::from_valuef(ValueF::Const(c)), - } - } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { - TypedThunk(Thunk::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_thunk(&self) -> Thunk { - 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_typethunk(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 Thunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Thunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for ThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ThunkInternal::PartialExpr(e) => { - ThunkInternal::PartialExpr(e.shift(delta, var)?) - } - ThunkInternal::ValueF(m, v) => { - ThunkInternal::ValueF(*m, v.shift(delta, var)?) - } - }) - } -} - -impl Shift for TypedThunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedThunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for TypedThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedThunkInternal { - internal: self.internal.shift(delta, var)?, - typ: self.typ.shift(delta, var)?, - }) - } -} - -impl Subst for Thunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Thunk(self.0.subst_shift(var, val)) - } -} - -impl Subst for ThunkInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - ThunkInternal::PartialExpr(e) => { - ThunkInternal::PartialExpr(e.subst_shift(var, val)) - } - ThunkInternal::ValueF(_, v) => { - // The resulting value may not stay in normal form after substitution - ThunkInternal::ValueF(WHNF, v.subst_shift(var, val)) - } - } - } -} - -impl Subst for TypedThunkInternal { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypedThunkInternal { - internal: self.internal.subst_shift(var, val), - typ: self.typ.subst_shift(var, val), - } - } -} - -impl Subst for TypedThunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - TypedThunk(self.0.subst_shift(var, val)) - } -} - -impl std::cmp::PartialEq for Thunk { - fn eq(&self, other: &Self) -> bool { - *self.as_valuef() == *other.as_valuef() - } -} -impl std::cmp::Eq for Thunk {} - -impl std::cmp::PartialEq for TypedThunk { - fn eq(&self, other: &Self) -> bool { - self.to_valuef() == other.to_valuef() - } -} -impl std::cmp::Eq for TypedThunk {} - -impl std::fmt::Debug for Thunk { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let b: &ThunkInternal = &self.as_internal(); - match b { - ThunkInternal::ValueF(m, v) => { - f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish() - } - ThunkInternal::PartialExpr(e) => { - f.debug_tuple("Thunk@PartialExpr").field(e).finish() - } - } - } -} -- cgit v1.2.3