diff options
author | Nadrieril | 2019-04-30 16:38:29 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-30 16:38:29 +0200 |
commit | 0ce663a74da1fbb87133b694f38d57b7086015f5 (patch) | |
tree | bc82eede5e943311dba6baa66eba930d713c1947 /dhall | |
parent | 77198a2833297289770867acdaf31db0e2011ea9 (diff) |
Pass references when possible
Diffstat (limited to '')
-rw-r--r-- | dhall/src/lib.rs | 1 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 151 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 59 |
3 files changed, 121 insertions, 90 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 3860890..6e4361f 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -5,6 +5,7 @@ #![feature(non_exhaustive)] #![feature(bind_by_move_pattern_guards)] #![feature(try_trait)] +#![feature(inner_deref)] #![cfg_attr(test, feature(custom_inner_attributes))] #![allow( clippy::type_complexity, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index f15eea4..26b23c2 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -25,7 +25,7 @@ impl<'a> Typed<'a> { /// leave ill-typed sub-expressions unevaluated. /// pub fn normalize(self) -> Normalized<'a> { - Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2) + Normalized(self.0.normalize_whnf().normalize_to_expr(), self.1, self.2) } pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { @@ -48,8 +48,8 @@ impl<'a> Typed<'a> { ) } - pub(crate) fn normalize_whnf(&self) -> Value { - self.0.as_whnf() + pub(crate) fn normalize_whnf(&self) -> std::cell::Ref<Value> { + self.0.normalize_whnf() } pub(crate) fn as_thunk(&self) -> Thunk { @@ -163,7 +163,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value { [_, NEListLit(xs), _, cons, nil] => { let mut v = nil; for x in xs.into_iter().rev() { - v = cons.clone().app(x.as_whnf()).app(v); + v = cons.clone().app(x.normalize_whnf().clone()).app(v); } v } @@ -197,7 +197,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>) -> Value { nothing }, [_, NEOptionalLit(x), _, just, _] => { - just.app(x.as_whnf()) + just.app(x.normalize_whnf().clone()) } ), NaturalBuild => improved_slice_patterns::match_vec!(args; @@ -298,7 +298,7 @@ impl NormalizationContext { fn lookup(&self, var: &V<Label>) -> Value { let V(x, n) = var; match self.0.lookup(x, *n) { - Some(EnvItem::Thunk(t)) => t.as_whnf(), + Some(EnvItem::Thunk(t)) => t.normalize_whnf().clone(), Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()), None => Value::Var(var.clone()), } @@ -374,33 +374,33 @@ impl Value { } /// Convert the value back to a (normalized) syntactic expression - pub(crate) fn normalize_to_expr(self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.clone(), - t.as_nf().normalize_to_expr(), - e.as_nf().normalize_to_expr(), + t.normalize_nf().normalize_to_expr(), + e.normalize_nf().normalize_to_expr(), )), Value::AppliedBuiltin(b, args) => { - let mut e = rc(ExprF::Builtin(b)); + let mut e = rc(ExprF::Builtin(*b)); for v in args { e = rc(ExprF::App(e, v.normalize_to_expr())); } e } Value::OptionalSomeClosure(n) => { - let a = n.as_nf().normalize_to_expr(); + let a = n.normalize_nf().normalize_to_expr(); dhall::subexpr!(λ(x: a) -> Some x) } Value::ListConsClosure(n, None) => { - let a = n.as_nf().normalize_to_expr(); + let a = n.normalize_nf().normalize_to_expr(); // Avoid accidental capture of the new `x` variable let a1 = a.shift0(1, &"x".into()); dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) } Value::ListConsClosure(n, Some(v)) => { - let v = v.as_nf().normalize_to_expr(); - let a = n.as_nf().normalize_to_expr(); + let v = v.normalize_nf().normalize_to_expr(); + let a = n.normalize_nf().normalize_to_expr(); // Avoid accidental capture of the new `xs` variable let v = v.shift0(1, &"xs".into()); dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) @@ -409,68 +409,90 @@ impl Value { dhall::subexpr!(λ(x : Natural) -> x + 1) } Value::Pi(x, t, e) => rc(ExprF::Pi( - x, - t.as_nf().normalize_to_expr(), - e.as_nf().normalize_to_expr(), + x.clone(), + t.normalize_nf().normalize_to_expr(), + e.normalize_nf().normalize_to_expr(), )), - Value::Var(v) => rc(ExprF::Var(v)), - 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::Var(v) => rc(ExprF::Var(v.clone())), + 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::EmptyOptionalLit(n) => rc(ExprF::App( rc(ExprF::Builtin(Builtin::OptionalNone)), - n.as_nf().normalize_to_expr(), + n.normalize_nf().normalize_to_expr(), )), Value::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.as_nf().normalize_to_expr())) + rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr())) } Value::EmptyListLit(n) => { - rc(ExprF::EmptyListLit(n.as_nf().normalize_to_expr())) + rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr())) } Value::NEListLit(elts) => rc(ExprF::NEListLit( elts.into_iter() - .map(|n| n.as_nf().normalize_to_expr()) + .map(|n| n.normalize_nf().normalize_to_expr()) .collect(), )), Value::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.into_iter() - .map(|(k, v)| (k, v.as_nf().normalize_to_expr())) + kvs.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_nf().normalize_to_expr()) + }) .collect(), )), Value::RecordType(kts) => rc(ExprF::RecordType( - kts.into_iter() - .map(|(k, v)| (k, v.as_nf().normalize_to_expr())) + kts.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_nf().normalize_to_expr()) + }) .collect(), )), Value::UnionType(kts) => rc(ExprF::UnionType( - kts.into_iter() - .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr()))) + kts.iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref() + .map(|v| v.normalize_nf().normalize_to_expr()), + ) + }) .collect(), )), Value::UnionConstructor(l, kts) => { let kts = kts - .into_iter() - .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr()))) + .iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref() + .map(|v| v.normalize_nf().normalize_to_expr()), + ) + }) .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l)) + rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit( - l, - v.as_nf().normalize_to_expr(), - kts.into_iter() - .map(|(k, v)| (k, v.map(|v| v.as_nf().normalize_to_expr()))) + l.clone(), + v.normalize_nf().normalize_to_expr(), + kts.iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref() + .map(|v| v.normalize_nf().normalize_to_expr()), + ) + }) .collect(), )), Value::TextLit(elts) => { fn normalize_textlit( - elts: Vec<InterpolatedTextContents<Thunk>>, + elts: &Vec<InterpolatedTextContents<Thunk>>, ) -> InterpolatedText<OutputSubExpr> { - elts.into_iter() + elts.iter() .flat_map(|contents| { use InterpolatedTextContents::{Expr, Text}; let new_interpolated = match contents { - Expr(n) => match n.as_nf() { + Expr(n) => match &*n.normalize_nf() { Value::TextLit(elts2) => { normalize_textlit(elts2) } @@ -482,7 +504,7 @@ impl Value { )], )), }, - Text(s) => InterpolatedText::from(s), + Text(s) => InterpolatedText::from(s.clone()), }; new_interpolated.into_iter() }) @@ -491,7 +513,7 @@ impl Value { rc(ExprF::TextLit(normalize_textlit(elts))) } - Value::Expr(e) => e, + Value::Expr(e) => e.clone(), } } @@ -586,7 +608,7 @@ impl Value { None, std::marker::PhantomData, ); - e.subst_shift(&V(x, 0), &val).as_whnf() + e.subst_shift(&V(x, 0), &val).normalize_whnf().clone() } (Value::AppliedBuiltin(b, mut args), val) => { args.push(val); @@ -741,7 +763,7 @@ impl Value { t.subst_shift(var, val), e.subst_shift(&var.shift0(1, x), val), ), - Value::Var(v) if v == var => val.normalize_whnf(), + Value::Var(v) if v == var => val.normalize_whnf().clone(), Value::Var(v) => Value::Var(v.shift(-1, var)), Value::Const(c) => Value::Const(*c), Value::BoolLit(b) => Value::BoolLit(*b), @@ -815,7 +837,7 @@ mod thunk { use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value}; use crate::expr::Typed; use dhall_core::{Label, V}; - use std::cell::RefCell; + use std::cell::{Ref, RefCell}; use std::rc::Rc; #[derive(Debug)] @@ -865,20 +887,20 @@ mod thunk { } // Always use normalize_whnf before - fn as_whnf(&self) -> Value { + fn as_whnf(&self) -> &Value { match self { ThunkInternal::Unnormalized(_, _) => unreachable!(), - ThunkInternal::WHNF(v) => v.as_ref().clone(), - ThunkInternal::NF(v) => v.as_ref().clone(), + ThunkInternal::WHNF(v) => v.as_ref(), + ThunkInternal::NF(v) => v.as_ref(), } } // Always use normalize_nf before - fn as_nf(&self) -> Value { + fn as_nf(&self) -> &Value { match self { ThunkInternal::Unnormalized(_, _) => unreachable!(), ThunkInternal::WHNF(_) => unreachable!(), - ThunkInternal::NF(v) => v.as_ref().clone(), + ThunkInternal::NF(v) => v.as_ref(), } } @@ -926,19 +948,20 @@ mod thunk { ThunkInternal::WHNF(Box::new(v)).into_thunk() } + // Deprecated pub(crate) fn normalize(&self) -> Thunk { - self.0.borrow_mut().normalize_nf(); + self.normalize_nf(); self.clone() } - pub(crate) fn as_whnf(&self) -> Value { + pub(crate) fn normalize_whnf(&self) -> Ref<Value> { self.0.borrow_mut().normalize_whnf(); - self.0.borrow().as_whnf() + Ref::map(self.0.borrow(), ThunkInternal::as_whnf) } - pub(crate) fn as_nf(&self) -> Value { + pub(crate) fn normalize_nf(&self) -> Ref<Value> { self.0.borrow_mut().normalize_nf(); - self.0.borrow().as_nf() + Ref::map(self.0.borrow(), ThunkInternal::as_nf) } pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { @@ -1006,9 +1029,9 @@ impl TypeThunk { } } - pub(crate) fn as_nf(&self) -> Value { + pub(crate) fn normalize_nf(&self) -> Value { match self { - TypeThunk::Thunk(th) => th.as_nf(), + TypeThunk::Thunk(th) => th.normalize_nf().clone(), // TODO: let's hope for the best with the unwrap TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(), } @@ -1177,7 +1200,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value { ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts), ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) { - Some(r) => r.as_whnf(), + Some(r) => r.normalize_whnf().clone(), None => { // Couldn't do anything useful, so just normalize subexpressions Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l))) @@ -1194,13 +1217,13 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value { ExprF::Merge(RecordLit(mut handlers), e, t) => { let e = match e { UnionConstructor(l, kts) => match handlers.remove(&l) { - Some(h) => return h.as_whnf(), + Some(h) => return h.normalize_whnf().clone(), None => UnionConstructor(l, kts), }, UnionLit(l, v, kts) => match handlers.remove(&l) { Some(h) => { - let h = h.as_whnf(); - let v = v.as_whnf(); + let h = h.normalize_whnf().clone(); + let v = v.normalize_whnf().clone(); return h.app(v); } None => UnionLit(l, v, kts), @@ -1211,7 +1234,7 @@ fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value { Expr(rc(ExprF::Merge( RecordLit(handlers).normalize_to_expr(), e.normalize_to_expr(), - t.map(<Value>::normalize_to_expr), + t.as_ref().map(Value::normalize_to_expr), ))) } // Couldn't do anything useful, so just normalize subexpressions diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index f22925a..8691945 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -87,11 +87,10 @@ impl Normalized<'static> { } } impl<'a> Typed<'a> { - fn normalize_to_type(self) -> Type<'a> { - // TODO: avoid cloning Value - match &self.normalize_whnf() { + fn normalize_to_type(&self) -> Type<'a> { + match &*self.normalize_whnf() { Value::Const(c) => Type(TypeInternal::Const(*c)), - _ => Type(TypeInternal::Typed(Box::new(self))), + _ => Type(TypeInternal::Typed(Box::new(self.clone()))), } } } @@ -105,7 +104,7 @@ impl<'a> Type<'a> { self.0.into_normalized() } pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> { - self.0.normalize_whnf() + Ok(self.0.normalize_whnf()?) } pub(crate) fn as_typed(&self) -> Result<Typed<'a>, TypeError> { self.0.as_typed() @@ -113,7 +112,7 @@ impl<'a> Type<'a> { fn internal(&self) -> &TypeInternal<'a> { &self.0 } - fn internal_whnf(&self) -> Option<Value> { + fn internal_whnf(&self) -> Option<std::cell::Ref<Value>> { self.0.whnf() } pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self { @@ -148,14 +147,17 @@ impl Type<'static> { impl TypeThunk { fn normalize_to_type( - self, + &self, ctx: &TypecheckContext, ) -> Result<Type<'static>, TypeError> { match self { - TypeThunk::Type(t) => Ok(t), + TypeThunk::Type(t) => Ok(t.clone()), TypeThunk::Thunk(th) => { // TODO: rule out statically - mktype(ctx, th.as_whnf().normalize_to_expr().embed_absurd()) + mktype( + ctx, + th.normalize_whnf().normalize_to_expr().embed_absurd(), + ) } } } @@ -179,7 +181,7 @@ impl<'a> TypeInternal<'a> { Ok(self.as_typed()?.normalize()) } fn normalize_whnf(&self) -> Result<Value, TypeError> { - Ok(self.as_typed()?.normalize_whnf()) + Ok(self.as_typed()?.normalize_whnf().clone()) } fn as_typed(&self) -> Result<Typed<'a>, TypeError> { Ok(match self { @@ -193,8 +195,7 @@ impl<'a> TypeInternal<'a> { } }) } - fn whnf(&self) -> Option<Value> { - // TODO: return reference + fn whnf(&self) -> Option<std::cell::Ref<Value>> { match self { TypeInternal::Typed(e) => Some(e.normalize_whnf()), _ => None, @@ -246,10 +247,10 @@ impl TypedOrType { TypedOrType::Type(t) => Ok(t.into_normalized()?.into()), } } - fn normalize_to_type(self) -> Type<'static> { + fn normalize_to_type(&self) -> Type<'static> { match self { TypedOrType::Typed(e) => e.normalize_to_type(), - TypedOrType::Type(t) => t, + TypedOrType::Type(t) => t.clone(), } } fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { @@ -845,7 +846,8 @@ fn type_last_layer( }, App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = match tf.internal_whnf() { + let tf_internal = tf.internal_whnf(); + let (x, tx, tb) = match tf_internal.deref() { Some(Value::Pi( x, TypeThunk::Type(tx), @@ -854,9 +856,9 @@ fn type_last_layer( Some(Value::Pi(_, _, _)) => { panic!("ICE: this should not have happened") } - _ => return Err(mkerr(NotAFunction(f))), + _ => return Err(mkerr(NotAFunction(f.clone()))), }; - ensure_equal!(a.get_type()?, &tx, { + ensure_equal!(a.get_type()?, tx, { mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a)) }); @@ -989,14 +991,16 @@ fn type_last_layer( .normalize_to_type(), )) } - Field(r, x) => match r.get_type()?.internal_whnf() { + Field(r, x) => match r.get_type()?.internal_whnf().deref() { Some(Value::RecordType(kts)) => match kts.get(&x) { Some(tth) => Ok(RetType(tth.clone().normalize_to_type(ctx)?)), - None => Err(mkerr(MissingRecordField(x, r))), + None => Err(mkerr(MissingRecordField(x, r.clone()))), }, + // TODO: branch here only when r.get_type() is a Const _ => { let r = r.normalize_to_type(); - match r.internal_whnf() { + let r_internal = r.internal_whnf(); + match r_internal.deref() { Some(Value::UnionType(kts)) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > // TODO: use "_" instead of x (i.e. compare types using equivalence in tests) @@ -1005,18 +1009,21 @@ fn type_last_layer( ctx.clone(), x.clone(), t.clone().normalize_to_type(ctx)?, - r, + r.clone(), ) .typecheck()? .normalize_to_type(), )), - Some(None) => Ok(RetType(r)), + Some(None) => Ok(RetType(r.clone())), None => Err(mkerr(MissingUnionField( x, - r.into_normalized()?, + r.clone().into_normalized()?, ))), }, - _ => Err(mkerr(NotARecord(x, r.into_normalized()?))), + _ => Err(mkerr(NotARecord( + x, + r.clone().into_normalized()? + ))), } } // _ => Err(mkerr(NotARecord( @@ -1033,9 +1040,9 @@ fn type_last_layer( // TODO: check type of interpolations TextLit(_) => Ok(RetType(builtin_to_type(Text)?)), BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.internal_whnf() { + match l.get_type()?.internal_whnf().deref() { Some(Value::AppliedBuiltin(List, _)) => {} - _ => return Err(mkerr(BinOpTypeMismatch(o, l))), + _ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))), } ensure_equal!( |