diff options
Diffstat (limited to 'dhall/src/core')
-rw-r--r-- | dhall/src/core/context.rs | 34 | ||||
-rw-r--r-- | dhall/src/core/thunk.rs | 48 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 23 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 16 |
4 files changed, 54 insertions, 67 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 328bfdc..62affcf 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -10,25 +10,25 @@ use crate::error::TypeError; use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] -pub(crate) enum CtxItem<T> { +pub enum CtxItem<T> { Kept(AlphaVar, T), Replaced(Thunk, T), } #[derive(Debug, Clone)] -pub(crate) struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>); +pub struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>); #[derive(Debug, Clone)] -pub(crate) struct NormalizationContext(Context<()>); +pub struct NormalizationContext(Context<()>); #[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Context<Type>); +pub struct TypecheckContext(Context<Type>); impl<T> Context<T> { - pub(crate) fn new() -> Self { + pub fn new() -> Self { Context(Rc::new(Vec::new())) } - pub(crate) fn insert_kept(&self, x: &Label, t: T) -> Self + pub fn insert_kept(&self, x: &Label, t: T) -> Self where T: Shift + Clone, { @@ -36,7 +36,7 @@ impl<T> Context<T> { vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); Context(Rc::new(vec)) } - pub(crate) fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self + pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self where T: Clone, { @@ -44,7 +44,7 @@ impl<T> Context<T> { vec.push((x.clone(), CtxItem::Replaced(th, t))); Context(Rc::new(vec)) } - pub(crate) fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>> + pub fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>> where T: Clone + Shift, { @@ -109,13 +109,13 @@ impl<T> Context<T> { } impl NormalizationContext { - pub(crate) fn new() -> Self { + pub fn new() -> Self { NormalizationContext(Context::new()) } - pub(crate) fn skip(&self, x: &Label) -> Self { + pub fn skip(&self, x: &Label) -> Self { NormalizationContext(self.0.insert_kept(x, ())) } - pub(crate) fn lookup(&self, var: &V<Label>) -> Value { + pub fn lookup(&self, var: &V<Label>) -> Value { match self.0.lookup(var) { Ok(CtxItem::Replaced(t, ())) => t.to_value(), Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()), @@ -125,24 +125,20 @@ impl NormalizationContext { } impl TypecheckContext { - pub(crate) fn new() -> Self { + pub fn new() -> Self { TypecheckContext(Context::new()) } - pub(crate) fn insert_type(&self, x: &Label, t: Type) -> Self { + pub fn insert_type(&self, x: &Label, t: Type) -> Self { TypecheckContext(self.0.insert_kept(x, t)) } - pub(crate) fn insert_value( - &self, - x: &Label, - e: Typed, - ) -> Result<Self, TypeError> { + pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> { Ok(TypecheckContext(self.0.insert_replaced( x, e.to_thunk(), e.get_type()?.into_owned(), ))) } - pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Typed> { + pub fn lookup(&self, var: &V<Label>) -> Option<Typed> { match self.0.lookup(var) { Ok(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type( Thunk::from_value(Value::Var(newvar.clone())), diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 2d4c34d..0e4f2d5 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -42,7 +42,7 @@ pub struct Thunk(Rc<RefCell<ThunkInternal>>); /// 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(crate) struct TypeThunk(Typed); +pub struct TypeThunk(Typed); impl ThunkInternal { fn into_thunk(self) -> Thunk { @@ -103,25 +103,25 @@ impl ThunkInternal { } impl Thunk { - pub(crate) fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { + pub fn new(ctx: NormalizationContext, e: InputSubExpr) -> Thunk { ThunkInternal::Unnormalized(ctx, e).into_thunk() } - pub(crate) fn from_value(v: Value) -> Thunk { + pub fn from_value(v: Value) -> Thunk { ThunkInternal::Value(WHNF, v).into_thunk() } - pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk { + pub fn from_normalized_expr(e: OutputSubExpr) -> Thunk { Thunk::new(NormalizationContext::new(), e.absurd()) } - pub(crate) fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk { + pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk { ThunkInternal::PartialExpr(e).into_thunk() } // Normalizes contents to normal form; faster than `normalize_nf` if // no one else shares this thunk - pub(crate) fn normalize_mut(&mut self) { + pub 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(), @@ -159,75 +159,69 @@ impl 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<Value> { + pub fn normalize_nf(&self) -> Ref<Value> { 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<Value> { + pub fn as_value(&self) -> Ref<Value> { self.do_normalize_whnf(); Ref::map(self.0.borrow(), ThunkInternal::as_whnf) } - pub(crate) fn to_value(&self) -> Value { + pub fn to_value(&self) -> Value { self.as_value().clone() } - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { + pub 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: Value) -> Value { + pub fn app_val(&self, val: Value) -> Value { self.app_thunk(val.into_thunk()) } - pub(crate) fn app_thunk(&self, th: Thunk) -> Value { + pub fn app_thunk(&self, th: Thunk) -> Value { apply_any(self.clone(), th) } } impl TypeThunk { - pub(crate) fn from_value(v: Value) -> TypeThunk { + pub fn from_value(v: Value) -> TypeThunk { TypeThunk::from_thunk(Thunk::from_value(v)) } - pub(crate) fn from_thunk(th: Thunk) -> TypeThunk { + pub fn from_thunk(th: Thunk) -> TypeThunk { TypeThunk(Typed::from_thunk_untyped(th)) } - pub(crate) fn from_type(t: Type) -> TypeThunk { + pub fn from_type(t: Type) -> TypeThunk { TypeThunk(t.to_typed()) } - pub(crate) fn normalize_mut(&mut self) { + pub fn normalize_mut(&mut self) { self.0.normalize_mut() } - pub(crate) fn normalize_nf(&self) -> Value { + pub fn normalize_nf(&self) -> Value { self.0.to_value().normalize() } - pub(crate) fn to_value(&self) -> Value { + pub fn to_value(&self) -> Value { self.0.to_value() } - pub(crate) fn to_thunk(&self) -> Thunk { + pub fn to_thunk(&self) -> Thunk { self.0.to_thunk() } - pub(crate) fn to_type(&self) -> Type { + pub fn to_type(&self) -> Type { self.0.to_type() } - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { + pub fn normalize_to_expr_maybe_alpha(&self, alpha: bool) -> OutputSubExpr { self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) } } diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 799cfac..cff599b 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -25,7 +25,7 @@ use crate::phase::Typed; /// 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(crate) enum Value { +pub enum Value { /// Closures Lam(AlphaLabel, TypeThunk, Thunk), Pi(AlphaLabel, TypeThunk, TypeThunk), @@ -62,20 +62,17 @@ pub(crate) enum Value { } impl Value { - pub(crate) fn into_thunk(self) -> Thunk { + pub fn into_thunk(self) -> Thunk { Thunk::from_value(self) } /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + pub 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(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { + pub 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), @@ -213,13 +210,13 @@ impl Value { } // Deprecated - pub(crate) fn normalize(&self) -> Value { + pub fn normalize(&self) -> Value { let mut v = self.clone(); v.normalize_mut(); v } - pub(crate) fn normalize_mut(&mut self) { + pub fn normalize_mut(&mut self) { match self { Value::NaturalSuccClosure | Value::Var(_) @@ -302,21 +299,21 @@ impl Value { } /// Apply to a value - pub(crate) fn app(self, val: Value) -> Value { + pub fn app(self, val: Value) -> Value { self.app_val(val) } /// Apply to a value - pub(crate) fn app_val(self, val: Value) -> Value { + pub fn app_val(self, val: Value) -> Value { self.app_thunk(val.into_thunk()) } /// Apply to a thunk - pub(crate) fn app_thunk(self, th: Thunk) -> Value { + pub fn app_thunk(self, th: Thunk) -> Value { Thunk::from_value(self).app_thunk(th) } - pub(crate) fn from_builtin(b: Builtin) -> Value { + pub fn from_builtin(b: Builtin) -> Value { Value::AppliedBuiltin(b, vec![]) } } diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs index ea7e55f..e474e44 100644 --- a/dhall/src/core/var.rs +++ b/dhall/src/core/var.rs @@ -6,7 +6,7 @@ use dhall_syntax::{Label, V}; /// that corresponds to the alpha-normalized version of the first one. /// Equality is up to alpha-equivalence. #[derive(Debug, Clone, Eq)] -pub(crate) struct AlphaVar { +pub struct AlphaVar { normal: V<Label>, alpha: Option<V<()>>, } @@ -14,9 +14,9 @@ pub(crate) struct AlphaVar { // Exactly like a Label, but equality returns always true. // This is so that Value equality is exactly alpha-equivalence. #[derive(Debug, Clone, Eq)] -pub(crate) struct AlphaLabel(Label); +pub struct AlphaLabel(Label); -pub(crate) trait Shift: Sized { +pub trait Shift: Sized { // Shift an expression to move it around binders without changing the meaning of its free // variables. Shift by 1 to move an expression under a binder. Shift by -1 to extract an // expression from under a binder, if the expression does not refer to that bound variable. @@ -50,18 +50,18 @@ pub(crate) trait Shift: Sized { } } -pub(crate) trait Subst<T> { +pub trait Subst<T> { fn subst_shift(&self, var: &AlphaVar, val: &T) -> Self; } impl AlphaVar { - pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { + pub fn to_var(&self, alpha: bool) -> V<Label> { match (alpha, &self.alpha) { (true, Some(x)) => V("_".into(), x.1), _ => self.normal.clone(), } } - pub(crate) fn from_var(normal: V<Label>) -> Self { + pub fn from_var(normal: V<Label>) -> Self { AlphaVar { normal, alpha: None, @@ -70,14 +70,14 @@ impl AlphaVar { } impl AlphaLabel { - pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { + pub fn to_label_maybe_alpha(&self, alpha: bool) -> Label { if alpha { "_".into() } else { self.to_label() } } - pub(crate) fn to_label(&self) -> Label { + pub fn to_label(&self) -> Label { self.clone().into() } } |