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 ++++++++++++++++++++++++++++++++++++++++-------- dhall/src/phase/mod.rs | 95 ++++++++++-------------------------- 2 files changed, 129 insertions(+), 91 deletions(-) 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), + } } } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index ccedff2..0b05227 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -4,14 +4,12 @@ use std::path::Path; use dhall_syntax::{Const, Import, Span, SubExpr, X}; -use crate::core::context::TypecheckContext; -use crate::core::thunk::Thunk; +use crate::core::thunk::{Thunk, TypeThunk}; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::{EncodeError, Error, ImportError, TypeError, TypeMessage}; +use crate::error::{EncodeError, Error, ImportError, TypeError}; use resolve::ImportRoot; -use typecheck::type_of_const; pub(crate) mod binary; pub(crate) mod normalize; @@ -33,16 +31,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub enum Typed { - // 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), -} +pub struct Typed(TypeThunk); /// A normalized expression. /// @@ -105,83 +94,63 @@ impl Typed { /// /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. - pub fn normalize(self) -> Normalized { - match &self { - Typed::Const(_) => {} - Typed::Untyped(thunk) | Typed::Typed(thunk, _) => { - thunk.normalize_nf(); - } - } + pub fn normalize(mut self) -> Normalized { + self.normalize_mut(); Normalized(self) } pub fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - Typed::Typed(th, Box::new(t)) + Typed(TypeThunk::from_thunk_and_type(th, t)) } pub fn from_thunk_untyped(th: Thunk) -> Self { - Typed::Untyped(th) + Typed(TypeThunk::from_thunk_untyped(th)) } pub fn from_const(c: Const) -> Self { - Typed::Const(c) + Typed(TypeThunk::from_const(c)) } pub fn from_value_untyped(v: Value) -> Self { - Typed::from_thunk_untyped(Thunk::from_value(v)) + Typed(TypeThunk::from_value_untyped(v)) + } + pub fn from_typethunk(th: TypeThunk) -> Self { + Typed(th) } - // TODO: Avoid cloning if possible pub fn to_value(&self) -> Value { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.to_value(), - Typed::Const(c) => Value::Const(*c), - } + self.0.to_value() } pub fn to_expr(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr() + self.0.to_expr() } pub fn to_expr_alpha(&self) -> NormalizedSubExpr { - self.to_value().normalize_to_expr_maybe_alpha(true) + self.0.to_expr_alpha() } pub fn to_thunk(&self) -> Thunk { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.clone(), - Typed::Const(c) => Thunk::from_value(Value::Const(*c)), - } + self.0.to_thunk() } // Deprecated pub fn to_type(&self) -> Type { - self.clone().into_type() + self.clone() } // Deprecated pub fn into_type(self) -> Type { self } + pub fn into_typethunk(self) -> TypeThunk { + self.0 + } pub fn to_normalized(&self) -> Normalized { self.clone().normalize() } pub fn as_const(&self) -> Option { - // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), - _ => None, - } + self.0.as_const() } pub fn normalize_mut(&mut self) { - match self { - Typed::Untyped(th) | Typed::Typed(th, _) => th.normalize_mut(), - Typed::Const(_) => {} - } + self.0.normalize_mut() } pub fn get_type(&self) -> Result, TypeError> { - match self { - Typed::Untyped(_) => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - Typed::Typed(_, t) => Ok(Cow::Borrowed(t)), - Typed::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), - } + self.0.get_type() } } @@ -208,14 +177,7 @@ impl Normalized { impl Shift for Typed { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - Typed::Untyped(th) => Typed::Untyped(th.shift(delta, var)?), - Typed::Typed(th, t) => Typed::Typed( - th.shift(delta, var)?, - Box::new(t.shift(delta, var)?), - ), - Typed::Const(c) => Typed::Const(*c), - }) + Some(Typed(self.0.shift(delta, var)?)) } } @@ -227,14 +189,7 @@ impl Shift for Normalized { impl Subst for Typed { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - Typed::Untyped(th) => Typed::Untyped(th.subst_shift(var, val)), - Typed::Typed(th, t) => Typed::Typed( - th.subst_shift(var, val), - Box::new(t.subst_shift(var, val)), - ), - Typed::Const(c) => Typed::Const(*c), - } + Typed(self.0.subst_shift(var, val)) } } -- cgit v1.2.3