From 5870a46d5ab5810901198f03ed461d5c3bb5aa8a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:58:48 +0000 Subject: Remove move type propagation through Value --- dhall/src/lib.rs | 32 +++------ dhall/src/semantics/builtins.rs | 41 +++--------- dhall/src/semantics/nze/normalize.rs | 124 ++++++++++------------------------- dhall/src/semantics/nze/value.rs | 84 ++++++------------------ dhall/src/semantics/tck/typecheck.rs | 42 ++++-------- 5 files changed, 86 insertions(+), 237 deletions(-) (limited to 'dhall') diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index d8eeb4a..48d4d96 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -24,7 +24,7 @@ use crate::semantics::resolve; use crate::semantics::resolve::ImportRoot; use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind}; use crate::syntax::binary; -use crate::syntax::{Builtin, Const, Expr}; +use crate::syntax::{Builtin, Expr}; pub type ParsedExpr = Expr; pub type DecodedExpr = Expr; @@ -148,18 +148,12 @@ impl Normalized { self.0 } - pub(crate) fn from_const(c: Const) -> Self { - Normalized(Value::from_const(c)) - } - pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self { - Normalized(Value::from_kind_and_type(v, t.into_value())) + pub(crate) fn from_kind(v: ValueKind) -> Self { + Normalized(Value::from_kind(v)) } pub(crate) fn from_value(th: Value) -> Self { Normalized(th) } - pub(crate) fn const_type() -> Self { - Normalized::from_const(Const::Type) - } pub fn make_builtin_type(b: Builtin) -> Self { Normalized::from_value(Value::from_builtin(b)) @@ -177,23 +171,17 @@ impl Normalized { pub fn make_record_type( kts: impl Iterator, ) -> Self { - Normalized::from_kind_and_type( - ValueKind::RecordType( - kts.map(|(k, t)| (k.into(), t.into_value())).collect(), - ), - Normalized::const_type(), - ) + Normalized::from_kind(ValueKind::RecordType( + kts.map(|(k, t)| (k.into(), t.into_value())).collect(), + )) } pub fn make_union_type( kts: impl Iterator)>, ) -> Self { - Normalized::from_kind_and_type( - ValueKind::UnionType( - kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) - .collect(), - ), - Normalized::const_type(), - ) + Normalized::from_kind(ValueKind::UnionType( + kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value()))) + .collect(), + )) } } diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs index 907d449..a513967 100644 --- a/dhall/src/semantics/builtins.rs +++ b/dhall/src/semantics/builtins.rs @@ -35,11 +35,11 @@ impl BuiltinClosure { } } - pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind { + pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind { use std::iter::once; let args = self.args.iter().cloned().chain(once(a.clone())).collect(); let types = self.types.iter().cloned().chain(once(f_ty)).collect(); - apply_builtin(self.b, args, ret_ty, types, self.env.clone()) + apply_builtin(self.b, args, types, self.env.clone()) } /// This doesn't break the invariant because we already checked that the appropriate arguments /// did not normalize to something that allows evaluation to proceed. @@ -267,7 +267,6 @@ macro_rules! make_closure { fn apply_builtin( b: Builtin, args: Vec, - ty: &Value, types: Vec, env: NzEnv, ) -> ValueKind { @@ -399,10 +398,7 @@ fn apply_builtin( let mut kts = HashMap::new(); kts.insert("index".into(), Value::from_builtin(Natural)); kts.insert("value".into(), t.clone()); - let t = Value::from_kind_and_type( - RecordType(kts), - Value::from_const(Type), - ); + let t = Value::from_kind(RecordType(kts)); // Construct the new list, with added indices let list = match &*l_whnf { @@ -414,18 +410,10 @@ fn apply_builtin( let mut kvs = HashMap::new(); kvs.insert( "index".into(), - Value::from_kind_and_type( - NaturalLit(i), - Value::from_builtin( - Builtin::Natural, - ), - ), + Value::from_kind(NaturalLit(i)), ); kvs.insert("value".into(), e.clone()); - Value::from_kind_and_type( - RecordLit(kvs), - t.clone(), - ) + Value::from_kind(RecordLit(kvs)) }) .collect(), ), @@ -449,7 +437,7 @@ fn apply_builtin( )) .app(t.clone()), ) - .app(EmptyListLit(t.clone()).into_value_with_type(list_t)), + .app(EmptyListLit(t.clone()).into_value()), ) } (ListFold, [_, l, _, cons, nil]) => match &*l.kind() { @@ -475,10 +463,7 @@ fn apply_builtin( )) .app(t.clone()), ) - .app( - EmptyOptionalLit(t.clone()) - .into_value_with_type(optional_t), - ), + .app(EmptyOptionalLit(t.clone()).into_value()), ) } (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { @@ -492,20 +477,14 @@ fn apply_builtin( λ(x : Natural) -> 1 + var(x) ))) - .app( - NaturalLit(0) - .into_value_with_type(Value::from_builtin(Natural)), - ), + .app(NaturalLit(0).into_value()), ), (NaturalFold, [n, t, succ, zero]) => match &*n.kind() { NaturalLit(0) => Ret::Value(zero.clone()), NaturalLit(n) => { let fold = Value::from_builtin(NaturalFold) - .app( - NaturalLit(n - 1) - .into_value_with_type(Value::from_builtin(Natural)), - ) + .app(NaturalLit(n - 1).into_value()) .app(t.clone()) .app(succ.clone()) .app(zero.clone()); @@ -517,7 +496,7 @@ fn apply_builtin( }; match ret { Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), + Ret::Value(v) => v.kind().clone(), Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure { b, args, diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index 3a981f4..c660fce 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -6,18 +6,16 @@ use crate::semantics::{ Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, ValueKind, }; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, -}; +use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; use crate::Normalized; -pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { +pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind { match f.kind() { ValueKind::LamClosure { closure, .. } => { - closure.apply(a).to_whnf_check_type(ty) + closure.apply(a).kind().clone() } ValueKind::AppliedBuiltin(closure) => { - closure.apply(a, f.get_type_not_sort(), ty) + closure.apply(a, f.get_type_not_sort()) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -102,12 +100,7 @@ enum Ret<'a> { Expr(ExprKind), } -fn apply_binop<'a>( - o: BinOp, - x: &'a Value, - y: &'a Value, - ty: &Value, -) -> Option> { +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { use BinOp::{ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus, NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge, @@ -194,19 +187,12 @@ fn apply_binop<'a>( Ret::ValueRef(y) } (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => { - let kts = match ty.kind() { - RecordType(kts) => kts, - _ => unreachable!("Internal type error"), - }; - let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| { - Ok(Value::from_partial_expr( - ExprKind::BinOp( - RecursiveRecordMerge, - v1.clone(), - v2.clone(), - ), - kts.get(k).expect("Internal type error").clone(), - )) + let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| { + Ok(Value::from_partial_expr(ExprKind::BinOp( + RecursiveRecordMerge, + v1.clone(), + v2.clone(), + ))) })?; Ret::ValueKind(RecordLit(kvs)) } @@ -217,14 +203,11 @@ fn apply_binop<'a>( kts_y, // If the Label exists for both records, then we hit the recursive case. |_, l: &Value, r: &Value| { - Ok(Value::from_partial_expr( - ExprKind::BinOp( - RecursiveRecordTypeMerge, - l.clone(), - r.clone(), - ), - ty.clone(), - )) + Ok(Value::from_partial_expr(ExprKind::BinOp( + RecursiveRecordTypeMerge, + l.clone(), + r.clone(), + ))) }, )?; Ret::ValueKind(RecordType(kts)) @@ -240,7 +223,6 @@ fn apply_binop<'a>( pub(crate) fn normalize_one_layer( expr: ExprKind, - ty: &Value, env: &NzEnv, ) -> ValueKind { use ValueKind::{ @@ -318,7 +300,7 @@ pub(crate) fn normalize_one_layer( } } } - ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) { + ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) { Some(ret) => ret, None => Ret::Expr(expr), }, @@ -335,7 +317,6 @@ pub(crate) fn normalize_one_layer( PartialExpr(ExprKind::Projection(v2, _)) => { return normalize_one_layer( ExprKind::Projection(v2.clone(), ls.clone()), - ty, env, ) } @@ -361,45 +342,26 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), - ty, env, ) } }, (RecordLit(kvs), _) => match kvs.get(l) { Some(r) => Ret::Expr(ExprKind::Field( - Value::from_kind_and_type( - PartialExpr(ExprKind::BinOp( - BinOp::RightBiasedRecordMerge, - Value::from_kind_and_type( - RecordLit({ - let mut kvs = HashMap::new(); - kvs.insert(l.clone(), r.clone()); - kvs - }), - Value::from_kind_and_type( - RecordType({ - let mut kvs = HashMap::new(); - kvs.insert( - l.clone(), - r.get_type_not_sort(), - ); - kvs - }), - r.get_type_not_sort() - .get_type_not_sort(), - ), - ), - y.clone(), - )), - v.get_type_not_sort(), - ), + Value::from_kind(PartialExpr(ExprKind::BinOp( + BinOp::RightBiasedRecordMerge, + Value::from_kind(RecordLit({ + let mut kvs = HashMap::new(); + kvs.insert(l.clone(), r.clone()); + kvs + })), + y.clone(), + ))), l.clone(), )), None => { return normalize_one_layer( ExprKind::Field(y.clone(), l.clone()), - ty, env, ) } @@ -416,7 +378,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(y.clone(), l.clone()), - ty, env, ) } @@ -426,7 +387,6 @@ pub(crate) fn normalize_one_layer( None => { return normalize_one_layer( ExprKind::Field(x.clone(), l.clone()), - ty, env, ) } @@ -482,22 +442,9 @@ pub(crate) fn normalize_one_layer( .sorted_by_key(|(k, _)| k.clone()) .map(|(k, v)| { let mut rec = HashMap::new(); - let mut rec_ty = HashMap::new(); rec.insert("mapKey".into(), Value::from_text(k)); rec.insert("mapValue".into(), v.clone()); - rec_ty.insert( - "mapKey".into(), - Value::from_builtin(Builtin::Text), - ); - rec_ty.insert("mapValue".into(), v.get_type_not_sort()); - - Value::from_kind_and_type( - ValueKind::RecordLit(rec), - Value::from_kind_and_type( - ValueKind::RecordType(rec_ty), - Value::from_const(Const::Type), - ), - ) + Value::from_kind(ValueKind::RecordLit(rec)) }) .collect(), )), @@ -507,8 +454,8 @@ pub(crate) fn normalize_one_layer( match ret { Ret::ValueKind(v) => v, - Ret::Value(v) => v.to_whnf_check_type(ty), - Ret::ValueRef(v) => v.to_whnf_check_type(ty), + Ret::Value(v) => v.kind().clone(), + Ret::ValueRef(v) => v.kind().clone(), Ret::Expr(expr) => ValueKind::PartialExpr(expr), } } @@ -521,17 +468,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { let annot = annot.eval(env); ValueKind::LamClosure { binder: Binder::new(binder.clone()), - annot: annot.clone(), - closure: Closure::new(annot, env, body.clone()), + annot: annot, + closure: Closure::new(env, body.clone()), } } TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => { let annot = annot.eval(env); - let closure = Closure::new(annot.clone(), env, body.clone()); ValueKind::PiClosure { binder: Binder::new(binder.clone()), annot, - closure, + closure: Closure::new(env, body.clone()), } } TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => { @@ -539,12 +485,8 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind { body.eval(&env.insert_value_noty(val)).kind().clone() } TyExprKind::Expr(e) => { - let ty = match tye.get_type() { - Ok(ty) => ty, - Err(_) => return ValueKind::Const(Const::Sort), - }; let e = e.map_ref(|tye| tye.eval(env)); - normalize_one_layer(e, &ty, env) + normalize_one_layer(e, env) } } } diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 203b479..47c50a4 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -5,8 +5,8 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, - type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv, - NzVar, TyEnv, TyExpr, TyExprKind, VarEnv, + type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind, + VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -39,7 +39,6 @@ pub(crate) enum Thunk { PartialExpr { env: NzEnv, expr: ExprKind, - ty: Value, }, } @@ -47,11 +46,7 @@ pub(crate) enum Thunk { #[derive(Debug, Clone)] pub(crate) enum Closure { /// Normal closure - Closure { - arg_ty: Value, - env: NzEnv, - body: TyExpr, - }, + Closure { env: NzEnv, body: TyExpr }, /// Closure that ignores the argument passed ConstantClosure { body: Value }, } @@ -130,21 +125,18 @@ impl Value { .into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr( - e: ExprKind, - ty: Value, - ) -> Value { + pub(crate) fn from_partial_expr(e: ExprKind) -> Value { // TODO: env let env = NzEnv::new(); ValueInternal::from_thunk( - Thunk::from_partial_expr(env, e, ty.clone()), + Thunk::from_partial_expr(env, e), Some(Value::const_kind()), Span::Artificial, ) .into_value() } /// Make a Value from a ValueKind - pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { + pub(crate) fn from_kind(v: ValueKind) -> Value { ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial) .into_value() } @@ -170,16 +162,12 @@ impl Value { Self::from_builtin_env(b, &NzEnv::new()) } pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { - Value::from_kind_and_type( - ValueKind::from_builtin_env(b, env.clone()), - typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(), - ) + Value::from_kind(ValueKind::from_builtin_env(b, env.clone())) } pub(crate) fn from_text(txt: impl ToString) -> Self { - Value::from_kind_and_type( - ValueKind::TextLit(TextLit::from_text(txt.to_string())), - Value::from_builtin(Builtin::Text), - ) + Value::from_kind(ValueKind::TextLit(TextLit::from_text( + txt.to_string(), + ))) } pub(crate) fn as_const(&self) -> Option { @@ -210,14 +198,6 @@ impl Value { pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env) } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { - self.kind().clone() - } - /// Before discarding type information, check that it matches the expected return type. - pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { - self.check_type(ty); - self.to_whnf_ignore_type() - } /// Normalizes contents to normal form; faster than `normalize` if /// no one else shares this. @@ -234,33 +214,19 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - Value::from_kind_and_type( - apply_any(self.clone(), v, &Value::const_kind()), - Value::const_kind(), - ) + Value::from_kind(apply_any(self.clone(), v)) } - /// In debug mode, panic if the provided type doesn't match the value's type. - /// Otherwise does nothing. - pub(crate) fn check_type(&self, _ty: &Value) { - // TODO: reenable - // debug_assert_eq!( - // Some(ty), - // self.get_type().ok().as_ref(), - // "Internal type error" - // ); - } pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result { let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv); type_with(tyenv, &expr).unwrap().get_type() } - pub(crate) fn get_type_noenv(&self) -> Result { - Ok(self.0.get_type()?.clone()) - } /// When we know the value isn't `Sort`, this gets the type directly pub(crate) fn get_type_not_sort(&self) -> Value { - self.get_type_noenv() + self.0 + .get_type() .expect("Internal type error: value is `Sort` but shouldn't be") + .clone() } pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { @@ -422,8 +388,8 @@ impl ValueInternal { } impl ValueKind { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_kind_and_type(self, t) + pub(crate) fn into_value(self) -> Value { + Value::from_kind(self) } pub(crate) fn normalize(&self) { @@ -504,24 +470,20 @@ impl Thunk { pub fn from_partial_expr( env: NzEnv, expr: ExprKind, - ty: Value, ) -> Self { - Thunk::PartialExpr { env, expr, ty } + Thunk::PartialExpr { env, expr } } pub fn eval(self) -> ValueKind { match self { Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), - Thunk::PartialExpr { env, expr, ty } => { - normalize_one_layer(expr, &ty, &env) - } + Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), } } } impl Closure { - pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self { + pub fn new(env: &NzEnv, body: TyExpr) -> Self { Closure::Closure { - arg_ty, env: env.clone(), body, } @@ -541,12 +503,8 @@ impl Closure { } fn apply_var(&self, var: NzVar) -> Value { match self { - Closure::Closure { arg_ty, .. } => { - let val = Value::from_kind_and_type( - ValueKind::Var(var), - arg_ty.clone(), - ); - self.apply(val) + Closure::Closure { .. } => { + self.apply(Value::from_kind(ValueKind::Var(var))) } Closure::ConstantClosure { body, .. } => body.clone(), } diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index ceb83de..810e483 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -183,11 +183,11 @@ fn type_one_layer( }; } - let ty = type_of_recordtype( + type_of_recordtype( span.clone(), kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; - Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::RecordType(kts) => { use std::collections::hash_map::Entry; @@ -247,22 +247,11 @@ fn type_one_layer( ValueKind::UnionType(kts) => match kts.get(x) { // Constructor has type T -> < x: T, ... > Some(Some(ty)) => { - // Can't fail because uniontypes must have type Const(_). - let kt = scrut.get_type()?.as_const().unwrap(); - // The type of the field must be Const smaller than `kt`, thus the - // function type has type `kt`. - let pi_ty = Value::from_const(kt); - - Value::from_kind_and_type( - ValueKind::PiClosure { - binder: Binder::new(x.clone()), - annot: ty.clone(), - closure: Closure::new_constant( - scrut_nf, - ), - }, - pi_ty, - ) + Value::from_kind(ValueKind::PiClosure { + binder: Binder::new(x.clone()), + annot: ty.clone(), + closure: Closure::new_constant(scrut_nf), + }) } Some(None) => scrut_nf, None => return span_err("MissingUnionField"), @@ -386,11 +375,11 @@ fn type_one_layer( })?; // Construct the final record type - let ty = type_of_recordtype( + type_of_recordtype( span.clone(), kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))), )?; - Value::from_kind_and_type(ValueKind::RecordType(kts), ty) + Value::from_kind(ValueKind::RecordType(kts)) } ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => { let ekind = ExprKind::BinOp( @@ -685,12 +674,8 @@ fn type_one_layer( let mut kts = HashMap::new(); kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text)); kts.insert("mapValue".into(), entry_type); - let output_type = Value::from_builtin(Builtin::List).app( - Value::from_kind_and_type( - ValueKind::RecordType(kts), - Value::from_const(Const::Type), - ), - ); + let output_type = Value::from_builtin(Builtin::List) + .app(Value::from_kind(ValueKind::RecordType(kts))); if let Some(annot) = annot { let annot_val = annot.eval(env.as_nzenv()); if output_type != annot_val { @@ -723,10 +708,7 @@ fn type_one_layer( }; } - Value::from_kind_and_type( - ValueKind::RecordType(new_kts), - record_type.get_type(env)?, - ) + Value::from_kind(ValueKind::RecordType(new_kts)) } ExprKind::ProjectionByExpr(record, selection) => { let record_type = record.get_type()?; -- cgit v1.2.3