diff options
author | Nadrieril | 2019-08-20 16:39:27 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-20 16:39:27 +0200 |
commit | 04438824db21fb5d9d3a2abdb3fa167875bda892 (patch) | |
tree | a146443659088dd7330e4456f7c01c2c701ef4bf | |
parent | 38a82c53ef45e802cf5816a8afcbf36a69c91174 (diff) |
Add Value::from_builtin
-rw-r--r-- | dhall/src/core/value.rs | 7 | ||||
-rw-r--r-- | dhall/src/core/valuef.rs | 10 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 44 |
3 files changed, 24 insertions, 37 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5367c86..f897f16 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,14 +2,14 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::Const; +use dhall_syntax::{Builtin, Const}; 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::typecheck::const_to_value; +use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] @@ -115,6 +115,9 @@ impl Value { pub fn const_type() -> Self { Value::from_const(Const::Type) } + pub fn from_builtin(b: Builtin) -> Self { + builtin_to_value(b) + } pub(crate) fn as_const(&self) -> Option<Const> { match &*self.as_whnf() { diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 0c3058d..da03cbd 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -257,16 +257,6 @@ impl ValueF { } } - /// Apply to a valuef - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_valuef(val) - } - - /// Apply to a valuef - pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { - self.app_value(val.into_value_untyped()) - } - /// Apply to a value pub fn app_value(self, th: Value) -> ValueF { Value::from_valuef_untyped(self).app_value(th) diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index a379a4b..f943171 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -31,11 +31,10 @@ macro_rules! make_closure { ).into_value_untyped() }; (Natural) => { - ValueF::from_builtin(Builtin::Natural) - .into_value_simple_type() + Value::from_builtin(Builtin::Natural) }; (List $($rest:tt)*) => { - ValueF::from_builtin(Builtin::List) + Value::from_builtin(Builtin::List) .app_value(make_closure!($($rest)*)) .into_value_simple_type() }; @@ -192,10 +191,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { (ListIndexed, [_, l, r..]) => match &*l.as_whnf() { EmptyListLit(t) => { let mut kts = HashMap::new(); - kts.insert( - "index".into(), - Value::from_valuef_untyped(ValueF::from_builtin(Natural)), - ); + kts.insert("index".into(), Value::from_builtin(Natural)); kts.insert("value".into(), t.clone()); Ok(( r, @@ -232,7 +228,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } } _ => { - let list_t = ValueF::from_builtin(List) + let list_t = Value::from_builtin(List) .app_value(t.clone()) .into_value_simple_type(); Ok(( @@ -280,7 +276,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { } } _ => { - let optional_t = ValueF::from_builtin(Optional) + let optional_t = Value::from_builtin(Optional) .app_value(t.clone()) .into_value_simple_type(); Ok(( @@ -309,26 +305,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF { unimplemented!() } } - _ => { - let nat_type = - ValueF::from_builtin(Natural).into_value_simple_type(); - Ok(( - r, - f.app_value(nat_type.clone()) - .app_value( - make_closure!(λ(x : Natural) -> 1 + var(x, 0)), - ) - .app_value( - NaturalLit(0).into_value_with_type(nat_type), - ), - )) - } + _ => Ok(( + r, + f.app_value(Value::from_builtin(Natural)) + .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0))) + .app_value( + NaturalLit(0) + .into_value_with_type(Value::from_builtin(Natural)), + ), + )), }, (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() { NaturalLit(0) => Ok((r, zero.to_whnf())), NaturalLit(n) => { - let fold = ValueF::from_builtin(NaturalFold) - .app(NaturalLit(n - 1)) + let fold = Value::from_builtin(NaturalFold) + .app_value( + NaturalLit(n - 1) + .into_value_with_type(Value::from_builtin(Natural)), + ) .app_value(t.clone()) .app_value(succ.clone()) .app_value(zero.clone()) |