From 730f2ebb146792994c7492b6c05f7d09d42cbccf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 23:00:49 +0200 Subject: Merge TypedValue and Value --- dhall/src/phase/mod.rs | 16 ++-- dhall/src/phase/normalize.rs | 90 +++++++--------------- dhall/src/phase/typecheck.rs | 177 ++++++++++++++++++++----------------------- 3 files changed, 117 insertions(+), 166 deletions(-) (limited to 'dhall/src/phase') diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index e58e689..91d64c3 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -4,7 +4,7 @@ use std::path::Path; use dhall_syntax::{Const, SubExpr}; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{EncodeError, Error, ImportError, TypeError}; @@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] -pub struct Typed(TypedValue); +pub struct Typed(Value); /// A normalized expression. /// @@ -91,12 +91,12 @@ impl Typed { } pub(crate) fn from_const(c: Const) -> Self { - Typed(TypedValue::from_const(c)) + Typed(Value::from_const(c)) } pub fn from_valuef_and_type(v: ValueF, t: Typed) -> Self { - Typed(TypedValue::from_valuef_and_type(v, t.into_typedvalue())) + Typed(Value::from_valuef_and_type(v, t.into_value())) } - pub(crate) fn from_typedvalue(th: TypedValue) -> Self { + pub(crate) fn from_value(th: Value) -> Self { Typed(th) } pub fn const_type() -> Self { @@ -112,7 +112,7 @@ impl Typed { pub fn to_value(&self) -> Value { self.0.to_value() } - pub(crate) fn into_typedvalue(self) -> TypedValue { + pub(crate) fn into_value(self) -> Value { self.0 } @@ -155,8 +155,8 @@ impl Shift for Normalized { } } -impl Subst for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst for Typed { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { Typed(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs index 27858d8..821c5fd 100644 --- a/dhall/src/phase/normalize.rs +++ b/dhall/src/phase/normalize.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, }; -use crate::core::value::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -26,9 +26,7 @@ macro_rules! make_closure { (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => { ValueF::Lam( Label::from(stringify!($var)).into(), - TypedValue::from_value_simple_type( - make_closure!($($ty)*), - ), + make_closure!($($ty)*), make_closure!($($rest)*), ).into_value_untyped() }; @@ -51,10 +49,10 @@ macro_rules! make_closure { make_closure!($($rest)*), Value::from_valuef_and_type( ValueF::NaturalLit(1), - TypedValue::from_value(make_closure!(Natural)) + make_closure!(Natural) ), )).into_value_with_type( - TypedValue::from_value(make_closure!(Natural)) + make_closure!(Natural) ) }; ([ $($head:tt)* ] # $($tail:tt)*) => { @@ -74,10 +72,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { // 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(TypedValue::from_value_simple_type(t.clone())), - )), + (OptionalNone, [t, r..]) => Ok((r, EmptyOptionalLit(t.clone()))), (NaturalIsZero, [n, r..]) => match &*n.as_whnf() { NaturalLit(n) => Ok((r, BoolLit(*n == 0))), _ => Err(()), @@ -199,16 +194,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { let mut kts = HashMap::new(); kts.insert( "index".into(), - TypedValue::from_valuef_untyped(ValueF::from_builtin( - Natural, - )), + Value::from_valuef_untyped(ValueF::from_builtin(Natural)), ); kts.insert("value".into(), t.clone()); Ok(( r, - EmptyListLit(TypedValue::from_valuef_untyped(RecordType( - kts, - ))), + EmptyListLit(Value::from_valuef_untyped(RecordType(kts))), )) } NEListLit(xs) => { @@ -252,9 +243,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { [ var(x, 1) ] # var(xs, 0) ) }) - .app_valuef(EmptyListLit( - TypedValue::from_value_simple_type(t.clone()), - )), + .app_valuef(EmptyListLit(t.clone())), )), }, (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() { @@ -288,9 +277,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { ValueF::from_builtin(Optional).app_value(t.clone()), ) .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0)))) - .app_valuef(EmptyOptionalLit( - TypedValue::from_value_simple_type(t.clone()), - )), + .app_valuef(EmptyOptionalLit(t.clone())), )), }, (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() { @@ -346,10 +333,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueF { let f_borrow = f.as_whnf(); match &*f_borrow { - ValueF::Lam(x, _, e) => { - let val = TypedValue::from_value(a); - e.subst_shift(&x.into(), &val).to_whnf() - } + ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(), ValueF::AppliedBuiltin(b, args) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); @@ -639,21 +623,18 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { } (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => { let kvs = merge_maps(kvs1, kvs2, |v1, v2| { - TypedValue::from_valuef_untyped(ValueF::PartialExpr( - ExprF::BinOp( - RecursiveRecordTypeMerge, - v1.to_value(), - v2.to_value(), - ), - )) + Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp( + RecursiveRecordTypeMerge, + v1.to_value(), + v2.to_value(), + ))) }); Ret::ValueF(RecordType(kvs)) } - (Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence( - TypedValue::from_value_simple_type(x.clone()), - TypedValue::from_value_simple_type(y.clone()), - )), + (Equivalence, _, _) => { + Ret::ValueF(ValueF::Equivalence(x.clone(), y.clone())) + } _ => return None, }) @@ -674,18 +655,9 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { ExprF::Var(_) => unreachable!(), ExprF::Annot(x, _) => Ret::Value(x), ExprF::Assert(_) => Ret::Expr(expr), - ExprF::Lam(x, t, e) => { - Ret::ValueF(Lam(x.into(), TypedValue::from_value(t), e)) - } - ExprF::Pi(x, t, e) => Ret::ValueF(Pi( - x.into(), - TypedValue::from_value(t), - TypedValue::from_value(e), - )), - ExprF::Let(x, _, v, b) => { - let v = TypedValue::from_value(v); - Ret::Value(b.subst_shift(&x.into(), &v)) - } + 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::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)), ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)), @@ -699,9 +671,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { let t_borrow = t.as_whnf(); match &*t_borrow { AppliedBuiltin(Builtin::List, args) if args.len() == 1 => { - Ret::ValueF(EmptyListLit( - TypedValue::from_value_simple_type(args[0].clone()), - )) + Ret::ValueF(EmptyListLit(args[0].clone())) } _ => { drop(t_borrow); @@ -715,16 +685,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF) -> ValueF { ExprF::RecordLit(kvs) => { Ret::ValueF(RecordLit(kvs.into_iter().collect())) } - ExprF::RecordType(kts) => Ret::ValueF(RecordType( - kts.into_iter() - .map(|(k, t)| (k, TypedValue::from_value(t))) - .collect(), - )), - ExprF::UnionType(kts) => Ret::ValueF(UnionType( - kts.into_iter() - .map(|(k, t)| (k, t.map(|t| TypedValue::from_value(t)))) - .collect(), - )), + ExprF::RecordType(kts) => { + Ret::ValueF(RecordType(kts.into_iter().collect())) + } + ExprF::UnionType(kts) => { + Ret::ValueF(UnionType(kts.into_iter().collect())) + } ExprF::TextLit(elts) => { use InterpolatedTextContents::Expr; let elts: Vec<_> = squash_textlit(elts.into_iter()); diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index e24f5a3..e65881e 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ }; use crate::core::context::TypecheckContext; -use crate::core::value::TypedValue; +use crate::core::value::Value; use crate::core::valuef::ValueF; use crate::core::var::{Shift, Subst}; use crate::error::{TypeError, TypeMessage}; @@ -14,9 +14,9 @@ use crate::phase::Normalized; fn tck_pi_type( ctx: &TypecheckContext, x: Label, - tx: TypedValue, - te: TypedValue, -) -> Result { + tx: Value, + te: Value, +) -> Result { use crate::error::TypeMessage::*; let ctx2 = ctx.insert_type(&x, tx.clone()); @@ -37,16 +37,16 @@ fn tck_pi_type( let k = function_check(ka, kb); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::Pi(x.into(), tx, te), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_record_type( ctx: &TypecheckContext, - kts: impl IntoIterator>, -) -> Result { + kts: impl IntoIterator>, +) -> Result { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; let mut new_kts = HashMap::new(); @@ -70,18 +70,18 @@ fn tck_record_type( // An empty record type has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::RecordType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } fn tck_union_type( ctx: &TypecheckContext, kts: Iter, -) -> Result +) -> Result where - Iter: IntoIterator), TypeError>>, + Iter: IntoIterator), TypeError>>, { use crate::error::TypeMessage::*; use std::collections::hash_map::Entry; @@ -115,9 +115,9 @@ where // an union type with only unary variants also has type Type let k = k.unwrap_or(Const::Type); - Ok(TypedValue::from_valuef_and_type( + Ok(Value::from_valuef_and_type( ValueF::UnionType(new_kts), - TypedValue::from_const(k), + Value::from_const(k), )) } @@ -130,10 +130,10 @@ fn function_check(a: Const, b: Const) -> Const { } } -pub(crate) fn type_of_const(c: Const) -> Result { +pub(crate) fn type_of_const(c: Const) -> Result { match c { - Const::Type => Ok(TypedValue::from_const(Const::Kind)), - Const::Kind => Ok(TypedValue::from_const(Const::Sort)), + Const::Type => Ok(Value::from_const(Const::Kind)), + Const::Kind => Ok(Value::from_const(Const::Sort)), Const::Sort => { Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) } @@ -282,16 +282,16 @@ fn type_of_builtin(b: Builtin) -> Expr { } // TODO: this can't fail in practise -pub(crate) fn builtin_to_type(b: Builtin) -> Result { +pub(crate) fn builtin_to_type(b: Builtin) -> Result { type_with(&TypecheckContext::new(), SubExpr::from_builtin(b)) } /// Intermediary return type enum Ret { /// Returns the contained value as is - RetWhole(TypedValue), - /// Use the contained TypedValue as the type of the input expression - RetTypeOnly(TypedValue), + RetWhole(Value), + /// Use the contained Value as the type of the input expression + RetTypeOnly(Value), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -301,7 +301,7 @@ enum Ret { fn type_with( ctx: &TypecheckContext, e: SubExpr, -) -> Result { +) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; use Ret::*; @@ -313,7 +313,7 @@ fn type_with( let v = ValueF::Lam(x.clone().into(), tx.clone(), b.to_value()); let tb = b.get_type()?.into_owned(); let t = tck_pi_type(ctx, x.clone(), tx, tb)?; - TypedValue::from_valuef_and_type(v, t) + Value::from_valuef_and_type(v, t) } Pi(x, ta, tb) => { let ta = type_with(ctx, ta.clone())?; @@ -331,7 +331,7 @@ fn type_with( let v = type_with(ctx, v)?; return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } - Embed(p) => p.clone().into_typed().into_typedvalue(), + Embed(p) => p.clone().into_typed().into_value(), Var(var) => match ctx.lookup(&var) { Some(typed) => typed.clone(), None => { @@ -352,10 +352,7 @@ fn type_with( match ret { RetTypeOnly(typ) => { let expr = expr.map_ref(|typed| typed.to_value()); - TypedValue::from_valuef_and_type( - ValueF::PartialExpr(expr), - typ, - ) + Value::from_valuef_and_type(ValueF::PartialExpr(expr), typ) } RetWhole(tt) => tt, } @@ -367,7 +364,7 @@ fn type_with( /// layer. fn type_last_layer( ctx: &TypecheckContext, - e: &ExprF, + e: &ExprF, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -466,10 +463,10 @@ fn type_last_layer( )); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::List) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } SomeLit(x) => { @@ -478,10 +475,10 @@ fn type_last_layer( return Err(TypeError::new(ctx, InvalidOptionalType(t))); } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::from_builtin(dhall_syntax::Builtin::Optional) .app_value(t.to_value()), - TypedValue::from_const(Type), + Value::from_const(Type), ))) } RecordType(kts) => Ok(RetWhole(tck_record_type( @@ -545,7 +542,7 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetWhole(TypedValue::from_const(*c))), + Const(c) => Ok(RetWhole(Value::from_const(*c))), Builtin(b) => Ok(RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?)), BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), @@ -607,43 +604,38 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { + kts_l: &HashMap, + kts_r: &HashMap, + ) -> Result { use crate::phase::normalize::outer_join; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - inner_l: &TypedValue, - inner_r: &TypedValue| - -> Result { - match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { - ( - ValueF::RecordType(inner_l_kvs), - ValueF::RecordType(inner_r_kvs), - ) => combine_record_types( - ctx, - inner_l_kvs, - inner_r_kvs, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + inner_l: &Value, + inner_r: &Value| + -> Result { + match (&*inner_l.as_whnf(), &*inner_r.as_whnf()) { + ( + ValueF::RecordType(inner_l_kvs), + ValueF::RecordType(inner_r_kvs), + ) => { + combine_record_types(ctx, inner_l_kvs, inner_r_kvs) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; - let kts: HashMap> = - outer_join( - |l| Ok(l.clone()), - |r| Ok(r.clone()), - combine, - kts_l, - kts_r, - ); + let kts: HashMap> = outer_join( + |l| Ok(l.clone()), + |r| Ok(r.clone()), + combine, + kts_l, + kts_r, + ); Ok(tck_record_type( ctx, @@ -684,35 +676,30 @@ fn type_last_layer( // records of records when merging. fn combine_record_types( ctx: &TypecheckContext, - kts_l: &HashMap, - kts_r: &HashMap, - ) -> Result { + kts_l: &HashMap, + kts_r: &HashMap, + ) -> Result { use crate::phase::normalize::intersection_with_key; // If the Label exists for both records and the values // are records themselves, then we hit the recursive case. // Otherwise we have a field collision. - let combine = - |k: &Label, - kts_l_inner: &TypedValue, - kts_r_inner: &TypedValue| - -> Result { - match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) - { - ( - ValueF::RecordType(kvs_l_inner), - ValueF::RecordType(kvs_r_inner), - ) => combine_record_types( - ctx, - kvs_l_inner, - kvs_r_inner, - ), - (_, _) => Err(TypeError::new( - ctx, - FieldCollision(k.clone()), - )), + let combine = |k: &Label, + kts_l_inner: &Value, + kts_r_inner: &Value| + -> Result { + match (&*kts_l_inner.as_whnf(), &*kts_r_inner.as_whnf()) { + ( + ValueF::RecordType(kvs_l_inner), + ValueF::RecordType(kvs_r_inner), + ) => { + combine_record_types(ctx, kvs_l_inner, kvs_r_inner) } - }; + (_, _) => { + Err(TypeError::new(ctx, FieldCollision(k.clone()))) + } + } + }; let kts = intersection_with_key(combine, kts_l, kts_r); @@ -747,8 +734,8 @@ fn type_last_layer( k_l } else { return Err(mkerr(RecordTypeMismatch( - TypedValue::from_const(k_l), - TypedValue::from_const(k_r), + Value::from_const(k_l), + Value::from_const(k_r), l.clone(), r.clone(), ))); @@ -779,7 +766,7 @@ fn type_last_layer( // Ensure that the records combine without a type error // and if not output the final Const value. combine_record_types(ctx, kts_x, kts_y) - .and(Ok(RetTypeOnly(TypedValue::from_const(k)))) + .and(Ok(RetTypeOnly(Value::from_const(k)))) } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { @@ -814,7 +801,7 @@ fn type_last_layer( ))); } - Ok(RetTypeOnly(TypedValue::from_const(Type))) + Ok(RetTypeOnly(Value::from_const(Type))) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -941,7 +928,7 @@ fn type_last_layer( }; } - Ok(RetTypeOnly(TypedValue::from_valuef_and_type( + Ok(RetTypeOnly(Value::from_valuef_and_type( ValueF::RecordType(new_kts), record_type.get_type()?.into_owned(), ))) @@ -952,15 +939,13 @@ fn type_last_layer( /// `type_of` is the same as `type_with` with an empty context, meaning that the /// expression must be closed (i.e. no free variables), otherwise type-checking /// will fail. -pub(crate) fn typecheck( - e: SubExpr, -) -> Result { +pub(crate) fn typecheck(e: SubExpr) -> Result { type_with(&TypecheckContext::new(), e) } pub(crate) fn typecheck_with( expr: SubExpr, ty: SubExpr, -) -> Result { +) -> Result { typecheck(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } -- cgit v1.2.3