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/semantics/nze/normalize.rs | 124 ++++++++++------------------------- dhall/src/semantics/nze/value.rs | 84 ++++++------------------ 2 files changed, 54 insertions(+), 154 deletions(-) (limited to 'dhall/src/semantics/nze') 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(), } -- cgit v1.2.3