From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 17:08:01 +0200 Subject: Naming tweaks --- dhall/src/core/value.rs | 6 ++--- dhall/src/core/valuef.rs | 11 +++++----- dhall/src/phase/normalize.rs | 52 ++++++++++++++++++++------------------------ dhall/src/phase/typecheck.rs | 5 ++--- serde_dhall/src/lib.rs | 6 ++--- 5 files changed, 35 insertions(+), 45 deletions(-) diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f897f16..5055ac2 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -8,7 +8,7 @@ use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; +use crate::phase::normalize::{apply_any, normalize_whnf}; use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; @@ -208,11 +208,11 @@ impl Value { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> OutputSubExpr { + ) -> NormalizedSubExpr { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_value(&self, th: Value) -> ValueF { + pub(crate) fn app(&self, th: Value) -> ValueF { apply_any(self.clone(), th) } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index da03cbd..e9049c7 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -7,8 +7,7 @@ use dhall_syntax::{ use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::OutputSubExpr; -use crate::phase::Normalized; +use crate::phase::{Normalized, NormalizedSubExpr}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. @@ -59,7 +58,7 @@ impl ValueF { } /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { self.normalize_to_expr_maybe_alpha(false) } /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize @@ -67,7 +66,7 @@ impl ValueF { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> OutputSubExpr { + ) -> NormalizedSubExpr { match self { ValueF::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -258,8 +257,8 @@ impl ValueF { } /// Apply to a value - pub fn app_value(self, th: Value) -> ValueF { - Value::from_valuef_untyped(self).app_value(th) + pub fn app(self, th: Value) -> ValueF { + Value::from_valuef_untyped(self).app(th) } pub fn from_builtin(b: Builtin) -> ValueF { diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index f943171..afc2e7f 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -8,9 +8,7 @@ use dhall_syntax::{ use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr}; - -pub(crate) type OutputSubExpr = NormalizedSubExpr; +use crate::phase::Normalized; // Ad-hoc macro to help construct closures macro_rules! make_closure { @@ -35,7 +33,7 @@ macro_rules! make_closure { }; (List $($rest:tt)*) => { Value::from_builtin(Builtin::List) - .app_value(make_closure!($($rest)*)) + .app(make_closure!($($rest)*)) .into_value_simple_type() }; (Some($($rest:tt)*)) => { @@ -229,12 +227,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => { let list_t = Value::from_builtin(List) - .app_value(t.clone()) + .app(t.clone()) .into_value_simple_type(); Ok(( r, - f.app_value(list_t.clone()) - .app_value({ + f.app(list_t.clone()) + .app({ // Move `t` under new `x` variable let t1 = t.under_binder(Label::from("x")); make_closure!( @@ -243,7 +241,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { [ var(x, 1) ] # var(xs, 0) ) }) - .app_value( + .app( EmptyListLit(t.clone()) .into_value_with_type(list_t), ), @@ -255,11 +253,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { NEListLit(xs) => { let mut v = nil.clone(); for x in xs.iter().rev() { - v = cons - .clone() - .app_value(x.clone()) - .app_value(v) - .into_value_untyped(); + v = cons.clone().app(x.clone()).app(v).into_value_untyped(); } Ok((r, v.to_whnf())) } @@ -277,13 +271,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => { let optional_t = Value::from_builtin(Optional) - .app_value(t.clone()) + .app(t.clone()) .into_value_simple_type(); Ok(( r, - f.app_value(optional_t.clone()) - .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) - .app_value( + f.app(optional_t.clone()) + .app(make_closure!(λ(x: #t) -> Some(var(x, 0)))) + .app( EmptyOptionalLit(t.clone()) .into_value_with_type(optional_t), ), @@ -292,7 +286,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())), - NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))), + NEOptionalLit(x) => Ok((r, just.app(x.clone()))), _ => Err(()), }, (NaturalBuild, [f, r..]) => match &*f.as_whnf() { @@ -307,9 +301,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { } _ => Ok(( r, - f.app_value(Value::from_builtin(Natural)) - .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) - .app_value( + f.app(Value::from_builtin(Natural)) + .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app( NaturalLit(0) .into_value_with_type(Value::from_builtin(Natural)), ), @@ -319,15 +313,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) - .app_value( + .app( NaturalLit(n - 1) .into_value_with_type(Value::from_builtin(Natural)), ) - .app_value(t.clone()) - .app_value(succ.clone()) - .app_value(zero.clone()) + .app(t.clone()) + .app(succ.clone()) + .app(zero.clone()) .into_value_with_type(t.clone()); - Ok((r, succ.app_value(fold))) + Ok((r, succ.app(fold))) } _ => Err(()), }, @@ -337,7 +331,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { Ok((unconsumed_args, mut v)) => { let n_consumed_args = args.len() - unconsumed_args.len(); for x in args.into_iter().skip(n_consumed_args) { - v = v.app_value(x); + v = v.app(x); } v } @@ -621,7 +615,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)), ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)), ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)), - ExprF::App(v, a) => Ret::ValueF(v.app_value(a)), + ExprF::App(v, a) => Ret::ValueF(v.app(a)), ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)), @@ -743,7 +737,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { } }, (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) { - Some(h) => Ret::ValueF(h.app_value(v.clone())), + Some(h) => Ret::ValueF(h.app(v.clone())), None => { drop(handlers_borrow); drop(variant_borrow); diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 1ea87d1..440d694 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -457,7 +457,7 @@ fn type_last_layer( RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) - .app_value(t.into_owned()), + .app(t.into_owned()), Value::from_const(Type), )) } @@ -468,8 +468,7 @@ fn type_last_layer( } RetTypeOnly(Value::from_valuef_and_type( - ValueF::from_builtin(dhall_syntax::Builtin::Optional) - .app_value(t), + ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t), Value::from_const(Type), )) } diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index cef11dd..4171fab 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -169,14 +169,12 @@ pub mod value { } pub(crate) fn make_optional_type(t: Value) -> Self { Self::make_simple_type( - DhallValueF::from_builtin(Builtin::Optional) - .app_value(t.to_value()), + DhallValueF::from_builtin(Builtin::Optional).app(t.to_value()), ) } pub(crate) fn make_list_type(t: Value) -> Self { Self::make_simple_type( - DhallValueF::from_builtin(Builtin::List) - .app_value(t.to_value()), + DhallValueF::from_builtin(Builtin::List).app(t.to_value()), ) } // Made public for the StaticType derive macro -- cgit v1.2.3