summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-08-16 19:16:40 +0200
committerNadrieril2019-08-16 19:16:40 +0200
commit45fb07f74f19919f742be6fe7793dc72d4022f26 (patch)
treefffab6fdb5b59e6e32eec60b3c4adfa5835e4778 /dhall
parentfcc9afb3624883c4f99320c37678b7f9d338630d (diff)
Try to minimize untyped TypedThunks
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/thunk.rs13
-rw-r--r--dhall/src/phase/mod.rs7
-rw-r--r--dhall/src/phase/normalize.rs54
3 files changed, 42 insertions, 32 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 87541d3..5f96ec8 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -182,11 +182,7 @@ impl Thunk {
impl TypedThunk {
pub(crate) fn from_value(v: Value) -> TypedThunk {
- TypedThunk::from_thunk(Thunk::from_value(v))
- }
-
- pub fn from_thunk(th: Thunk) -> TypedThunk {
- TypedThunk::from_thunk_untyped(th)
+ TypedThunk::from_thunk_untyped(Thunk::from_value(v))
}
pub(crate) fn from_type(t: Type) -> TypedThunk {
@@ -216,14 +212,17 @@ impl TypedThunk {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
TypedThunk::Typed(th, Box::new(t))
}
+ pub fn from_thunk_simple_type(th: Thunk) -> Self {
+ TypedThunk::from_thunk_and_type(th, Type::const_type())
+ }
pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
TypedThunk::Untyped(th)
}
pub(crate) fn from_const(c: Const) -> Self {
TypedThunk::Const(c)
}
- pub(crate) fn from_value_untyped(v: Value) -> Self {
- TypedThunk::from_thunk_untyped(Thunk::from_value(v))
+ pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self {
+ TypedThunk::from_thunk_and_type(Thunk::from_value(v), t)
}
// TODO: Avoid cloning if possible
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 5a6d4db..adf749c 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -101,12 +101,15 @@ impl Typed {
pub(crate) fn from_const(c: Const) -> Self {
Typed(TypedThunk::from_const(c))
}
- pub fn from_value_untyped(v: Value) -> Self {
- Typed(TypedThunk::from_value_untyped(v))
+ pub fn from_value_and_type(v: Value, t: Type) -> Self {
+ Typed(TypedThunk::from_value_and_type(v, t))
}
pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
Typed(th)
}
+ pub fn const_type() -> Self {
+ Typed::from_const(Const::Type)
+ }
pub(crate) fn to_value(&self) -> Value {
self.0.to_value()
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 2a2bf3e..02b705d 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -22,10 +22,13 @@ macro_rules! make_closure {
);
Value::Var(var).into_thunk()
}};
+ // Warning: assumes that $ty, as a dhall value, has type `Type`
(λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
Value::Lam(
Label::from(stringify!($var)).into(),
- TypedThunk::from_thunk_untyped(make_closure!($($ty)*)),
+ TypedThunk::from_thunk_simple_type(
+ make_closure!($($ty)*),
+ ),
make_closure!($($rest)*),
).into_thunk()
};
@@ -61,9 +64,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
// Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
let ret = match (b, args.as_slice()) {
- (OptionalNone, [t, r..]) => {
- Ok((r, EmptyOptionalLit(TypedThunk::from_thunk(t.clone()))))
- }
+ (OptionalNone, [t, r..]) => Ok((
+ r,
+ EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())),
+ )),
(NaturalIsZero, [n, r..]) => match &*n.as_value() {
NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
_ => Err(()),
@@ -228,7 +232,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
[ var(x, 1) ] # var(xs, 0)
)
})
- .app_val(EmptyListLit(TypedThunk::from_thunk(t.clone()))),
+ .app_val(EmptyListLit(TypedThunk::from_thunk_simple_type(
+ t.clone(),
+ ))),
)),
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
@@ -260,9 +266,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
r,
f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
.app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
- .app_val(EmptyOptionalLit(TypedThunk::from_thunk(
- t.clone(),
- ))),
+ .app_val(EmptyOptionalLit(
+ TypedThunk::from_thunk_simple_type(t.clone()),
+ )),
)),
},
(OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
@@ -611,18 +617,20 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- TypedThunk::from_thunk(Thunk::from_partial_expr(ExprF::BinOp(
- RecursiveRecordTypeMerge,
- v1.to_thunk(),
- v2.to_thunk(),
- )))
+ TypedThunk::from_thunk_untyped(Thunk::from_partial_expr(
+ ExprF::BinOp(
+ RecursiveRecordTypeMerge,
+ v1.to_thunk(),
+ v2.to_thunk(),
+ ),
+ ))
});
Ret::Value(RecordType(kvs))
}
(Equivalence, _, _) => Ret::Value(Value::Equivalence(
- TypedThunk::from_thunk(x.clone()),
- TypedThunk::from_thunk(y.clone()),
+ TypedThunk::from_thunk_simple_type(x.clone()),
+ TypedThunk::from_thunk_simple_type(y.clone()),
)),
_ => return None,
@@ -645,12 +653,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
ExprF::Annot(x, _) => Ret::Thunk(x),
ExprF::Assert(_) => Ret::Expr(expr),
ExprF::Lam(x, t, e) => {
- Ret::Value(Lam(x.into(), TypedThunk::from_thunk(t), e))
+ Ret::Value(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e))
}
ExprF::Pi(x, t, e) => Ret::Value(Pi(
x.into(),
- TypedThunk::from_thunk(t),
- TypedThunk::from_thunk(e),
+ TypedThunk::from_thunk_untyped(t),
+ TypedThunk::from_thunk_untyped(e),
)),
ExprF::Let(x, _, v, b) => {
let v = Typed::from_thunk_untyped(v);
@@ -669,9 +677,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
let t_borrow = t.as_value();
match &*t_borrow {
AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
- Ret::Value(EmptyListLit(TypedThunk::from_thunk(
- args[0].clone(),
- )))
+ Ret::Value(EmptyListLit(
+ TypedThunk::from_thunk_simple_type(args[0].clone()),
+ ))
}
_ => {
drop(t_borrow);
@@ -687,12 +695,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> Value {
}
ExprF::RecordType(kts) => Ret::Value(RecordType(
kts.into_iter()
- .map(|(k, t)| (k, TypedThunk::from_thunk(t)))
+ .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t)))
.collect(),
)),
ExprF::UnionType(kts) => Ret::Value(UnionType(
kts.into_iter()
- .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk(t))))
+ .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t))))
.collect(),
)),
ExprF::TextLit(elts) => {