summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-08-20 16:39:27 +0200
committerNadrieril2019-08-20 16:39:27 +0200
commit04438824db21fb5d9d3a2abdb3fa167875bda892 (patch)
treea146443659088dd7330e4456f7c01c2c701ef4bf /dhall
parent38a82c53ef45e802cf5816a8afcbf36a69c91174 (diff)
Add Value::from_builtin
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/value.rs7
-rw-r--r--dhall/src/core/valuef.rs10
-rw-r--r--dhall/src/phase/normalize.rs44
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())