diff options
| -rw-r--r-- | dhall/src/core/thunk.rs | 13 | ||||
| -rw-r--r-- | dhall/src/phase/mod.rs | 7 | ||||
| -rw-r--r-- | dhall/src/phase/normalize.rs | 54 | ||||
| -rw-r--r-- | serde_dhall/src/lib.rs | 24 |
4 files changed, 57 insertions, 41 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) => { diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs index f400206..a277977 100644 --- a/serde_dhall/src/lib.rs +++ b/serde_dhall/src/lib.rs @@ -160,20 +160,21 @@ pub mod value { self.0.to_type() } - pub(crate) fn from_dhall_value(v: DhallValue) -> Self { - Value(Typed::from_value_untyped(v)) + /// Assumes that the given value has type `Type`. + pub(crate) fn make_simple_type(v: DhallValue) -> Self { + Value(Typed::from_value_and_type(v, Type::const_type())) } pub(crate) fn make_builtin_type(b: Builtin) -> Self { - Self::from_dhall_value(DhallValue::from_builtin(b)) + Self::make_simple_type(DhallValue::from_builtin(b)) } pub(crate) fn make_optional_type(t: Value) -> Self { - Self::from_dhall_value( + Self::make_simple_type( DhallValue::from_builtin(Builtin::Optional) .app_thunk(t.to_thunk()), ) } pub(crate) fn make_list_type(t: Value) -> Self { - Self::from_dhall_value( + Self::make_simple_type( DhallValue::from_builtin(Builtin::List).app_thunk(t.to_thunk()), ) } @@ -182,9 +183,9 @@ pub mod value { pub fn make_record_type( kts: impl Iterator<Item = (String, Value)>, ) -> Self { - Self::from_dhall_value(DhallValue::RecordType( + Self::make_simple_type(DhallValue::RecordType( kts.map(|(k, t)| { - (k.into(), TypedThunk::from_thunk(t.to_thunk())) + (k.into(), TypedThunk::from_thunk_simple_type(t.to_thunk())) }) .collect(), )) @@ -193,9 +194,14 @@ pub mod value { pub fn make_union_type( kts: impl Iterator<Item = (String, Option<Value>)>, ) -> Self { - Self::from_dhall_value(DhallValue::UnionType( + Self::make_simple_type(DhallValue::UnionType( kts.map(|(k, t)| { - (k.into(), t.map(|t| TypedThunk::from_thunk(t.to_thunk()))) + ( + k.into(), + t.map(|t| { + TypedThunk::from_thunk_simple_type(t.to_thunk()) + }), + ) }) .collect(), )) |