From db1375eccd1e6943b504cd54ed17eb8f4d19c25f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 6 Feb 2020 17:35:54 +0000 Subject: Remove most reliance on types stored in Value --- dhall/src/semantics/nze/value.rs | 60 ++++++++++++++++++++++++---------------- 1 file changed, 36 insertions(+), 24 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 607aa0d..203b479 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -3,13 +3,11 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::lazy; -use crate::semantics::Binder; use crate::semantics::{ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, - TyEnv, + type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv, + NzVar, TyEnv, TyExpr, TyExprKind, VarEnv, }; -use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind}; -use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, @@ -119,11 +117,14 @@ impl Value { ) .into_value() } + pub(crate) fn const_kind() -> Value { + Value::from_const(Const::Kind) + } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { ValueInternal::from_thunk( Thunk::new(env, tye.clone()), - tye.get_type().ok(), + Some(Value::const_kind()), tye.span().clone(), ) .into_value() @@ -137,24 +138,31 @@ impl Value { let env = NzEnv::new(); ValueInternal::from_thunk( Thunk::from_partial_expr(env, e, ty.clone()), - Some(ty), + 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 { - ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value() + ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial) + .into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); match c { - Const::Type => { - Value::from_kind_and_type(v, Value::from_const(Const::Kind)) - } - Const::Kind => { - Value::from_kind_and_type(v, Value::from_const(Const::Sort)) - } + Const::Type => ValueInternal::from_whnf( + v, + Some(Value::from_const(Const::Kind)), + Span::Artificial, + ) + .into_value(), + Const::Kind => ValueInternal::from_whnf( + v, + Some(Value::const_sort()), + Span::Artificial, + ) + .into_value(), Const::Sort => Value::const_sort(), } } @@ -226,14 +234,10 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let body_t = match &*self.get_type_not_sort().kind() { - ValueKind::PiClosure { annot, closure, .. } => { - v.check_type(annot); - closure.apply(v.clone()) - } - _ => unreachable!("Internal type error"), - }; - Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t) + Value::from_kind_and_type( + apply_any(self.clone(), v, &Value::const_kind()), + Value::const_kind(), + ) } /// In debug mode, panic if the provided type doesn't match the value's type. @@ -246,12 +250,16 @@ impl Value { // "Internal type error" // ); } - pub(crate) fn get_type(&self) -> Result { + 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() + self.get_type_noenv() .expect("Internal type error: value is `Sort` but shouldn't be") } @@ -366,6 +374,10 @@ impl Value { TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone()) } + pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { + let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv); + type_with(tyenv, &expr).unwrap() + } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr(VarEnv::new()) } @@ -522,7 +534,7 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { - body.eval(&env.insert_value(val)) + body.eval(&env.insert_value_noty(val)) } Closure::ConstantClosure { body, .. } => body.clone(), } -- cgit v1.2.3 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/value.rs | 84 ++++++++++------------------------------ 1 file changed, 21 insertions(+), 63 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') 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 From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:23:59 +0000 Subject: Add Hir as untyped alternative to TyExpr --- dhall/src/semantics/nze/value.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 47c50a4..d4213bc 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_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind, - VarEnv, + type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr, + TyExprKind, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -461,19 +461,19 @@ impl ValueKind { } impl Thunk { - pub fn new(env: &NzEnv, body: TyExpr) -> Self { + fn new(env: &NzEnv, body: TyExpr) -> Self { Thunk::Thunk { env: env.clone(), body, } } - pub fn from_partial_expr( + fn from_partial_expr( env: NzEnv, expr: ExprKind, ) -> Self { Thunk::PartialExpr { env, expr } } - pub fn eval(self) -> ValueKind { + fn eval(self) -> ValueKind { match self { Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), -- cgit v1.2.3 From 6c90d356c9a4a5bbeb88f25ad0ab499ba1503eae Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:53:55 +0000 Subject: Remove most TyExpr from normalization --- dhall/src/semantics/nze/value.rs | 120 ++++++++++++++++++--------------------- 1 file changed, 55 insertions(+), 65 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d4213bc..d05c545 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,9 +4,9 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, - type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr, - TyExprKind, VarEnv, + apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, + type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, + TyExpr, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -34,7 +34,7 @@ struct ValueInternal { #[derive(Debug, Clone)] pub(crate) enum Thunk { /// A completely unnormalized expression. - Thunk { env: NzEnv, body: TyExpr }, + Thunk { env: NzEnv, body: Hir }, /// A partially normalized expression that may need to go through `normalize_one_layer`. PartialExpr { env: NzEnv, @@ -46,7 +46,7 @@ pub(crate) enum Thunk { #[derive(Debug, Clone)] pub(crate) enum Closure { /// Normal closure - Closure { env: NzEnv, body: TyExpr }, + Closure { env: NzEnv, body: Hir }, /// Closure that ignores the argument passed ConstantClosure { body: Value }, } @@ -116,11 +116,12 @@ impl Value { Value::from_const(Const::Kind) } /// Construct a Value from a completely unnormalized expression. - pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value { + pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value { + let span = hir.span(); ValueInternal::from_thunk( - Thunk::new(env, tye.clone()), + Thunk::new(env, hir), Some(Value::const_kind()), - tye.span().clone(), + span, ) .into_value() } @@ -176,13 +177,8 @@ impl Value { _ => None, } } - // pub(crate) fn span(&self) -> Span { - // self.0.span.clone() - // } /// This is what you want if you want to pattern-match on the value. - /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut - /// panics. pub(crate) fn kind(&self) -> &ValueKind { self.0.kind() } @@ -196,7 +192,7 @@ impl Value { self.to_tyexpr_noenv().to_expr(opts) } pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { - self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env) + self.to_hir(env.as_varenv()).to_expr_tyenv(env) } /// Normalizes contents to normal form; faster than `normalize` if @@ -218,8 +214,7 @@ impl Value { } 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() + self.to_tyexpr_tyenv(tyenv).get_type() } /// When we know the value isn't `Sort`, this gets the type directly pub(crate) fn get_type_not_sort(&self) -> Value { @@ -229,21 +224,21 @@ impl Value { .clone() } - pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + pub fn to_hir(&self, venv: VarEnv) -> Hir { let map_uniontype = |kts: &HashMap>| { ExprKind::UnionType( kts.iter() .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv))) + (k.clone(), v.as_ref().map(|v| v.to_hir(venv))) }) .collect(), ) }; - let tye = match &*self.kind() { - ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)), - ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv), - self_kind => TyExprKind::Expr(match self_kind { + let hir = match &*self.kind() { + ValueKind::Var(v) => HirKind::Var(venv.lookup(v)), + ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv), + self_kind => HirKind::Expr(match self_kind { ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { unreachable!() } @@ -253,8 +248,8 @@ impl Value { closure, } => ExprKind::Lam( binder.to_label(), - annot.to_tyexpr(venv), - closure.to_tyexpr(venv), + annot.to_hir(venv), + closure.to_hir(venv), ), ValueKind::PiClosure { binder, @@ -262,8 +257,8 @@ impl Value { closure, } => ExprKind::Pi( binder.to_label(), - annot.to_tyexpr(venv), - closure.to_tyexpr(venv), + annot.to_hir(venv), + closure.to_hir(venv), ), ValueKind::Const(c) => ExprKind::Const(*c), ValueKind::BoolLit(b) => ExprKind::BoolLit(*b), @@ -271,81 +266,75 @@ impl Value { ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n), ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n), ValueKind::EmptyOptionalLit(n) => ExprKind::App( - Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv), - n.to_tyexpr(venv), + Value::from_builtin(Builtin::OptionalNone).to_hir(venv), + n.to_hir(venv), ), ValueKind::NEOptionalLit(n) => { - ExprKind::SomeLit(n.to_tyexpr(venv)) - } - ValueKind::EmptyListLit(n) => { - ExprKind::EmptyListLit(TyExpr::new( - TyExprKind::Expr(ExprKind::App( - Value::from_builtin(Builtin::List).to_tyexpr(venv), - n.to_tyexpr(venv), - )), - Some(Value::from_const(Const::Type)), - Span::Artificial, - )) + ExprKind::SomeLit(n.to_hir(venv)) } + ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( + HirKind::Expr(ExprKind::App( + Value::from_builtin(Builtin::List).to_hir(venv), + n.to_hir(venv), + )), + Span::Artificial, + )), ValueKind::NEListLit(elts) => ExprKind::NEListLit( - elts.iter().map(|v| v.to_tyexpr(venv)).collect(), + elts.iter().map(|v| v.to_hir(venv)).collect(), ), ValueKind::TextLit(elts) => ExprKind::TextLit( elts.iter() - .map(|t| t.map_ref(|v| v.to_tyexpr(venv))) + .map(|t| t.map_ref(|v| v.to_hir(venv))) .collect(), ), ValueKind::RecordLit(kvs) => ExprKind::RecordLit( kvs.iter() - .map(|(k, v)| (k.clone(), v.to_tyexpr(venv))) + .map(|(k, v)| (k.clone(), v.to_hir(venv))) .collect(), ), ValueKind::RecordType(kts) => ExprKind::RecordType( kts.iter() - .map(|(k, v)| (k.clone(), v.to_tyexpr(venv))) + .map(|(k, v)| (k.clone(), v.to_hir(venv))) .collect(), ), ValueKind::UnionType(kts) => map_uniontype(kts), ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( - TyExpr::new( - TyExprKind::Expr(map_uniontype(kts)), - Some(t.clone()), + Hir::new( + HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), ), ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( - TyExpr::new( - TyExprKind::Expr(ExprKind::Field( - TyExpr::new( - TyExprKind::Expr(map_uniontype(kts)), - Some(uniont.clone()), + Hir::new( + HirKind::Expr(ExprKind::Field( + Hir::new( + HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), )), - Some(ctort.clone()), Span::Artificial, ), - v.to_tyexpr(venv), + v.to_hir(venv), ), ValueKind::Equivalence(x, y) => ExprKind::BinOp( BinOp::Equivalence, - x.to_tyexpr(venv), - y.to_tyexpr(venv), + x.to_hir(venv), + y.to_hir(venv), ), - ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)), + ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)), }), }; - TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone()) + Hir::new(hir, self.0.span.clone()) } pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { - let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv); + let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv); type_with(tyenv, &expr).unwrap() } pub fn to_tyexpr_noenv(&self) -> TyExpr { - self.to_tyexpr(VarEnv::new()) + self.to_tyexpr_tyenv(&TyEnv::new()) } } @@ -461,7 +450,7 @@ impl ValueKind { } impl Thunk { - fn new(env: &NzEnv, body: TyExpr) -> Self { + fn new(env: &NzEnv, body: Hir) -> Self { Thunk::Thunk { env: env.clone(), body, @@ -475,14 +464,14 @@ impl Thunk { } fn eval(self) -> ValueKind { match self { - Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), + Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body), Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), } } } impl Closure { - pub fn new(env: &NzEnv, body: TyExpr) -> Self { + pub fn new(env: &NzEnv, body: Hir) -> Self { Closure::Closure { env: env.clone(), body, @@ -512,10 +501,11 @@ impl Closure { // TODO: somehow normalize the body. Might require to pass an env. pub fn normalize(&self) {} - /// Convert this closure to a TyExpr - pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr { + + /// Convert this closure to a Hir expression + pub fn to_hir(&self, venv: VarEnv) -> Hir { self.apply_var(NzVar::new(venv.size())) - .to_tyexpr(venv.insert()) + .to_hir(venv.insert()) } /// If the closure variable is free in the closure, return Err. Otherwise, return the value /// with that free variable remove. -- cgit v1.2.3 From 5688ed654eee258bf8ffc8761ce693c73a0242d5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:58:11 +0000 Subject: Remove extra types stored in Value --- dhall/src/semantics/nze/value.rs | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index d05c545..a771b91 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -93,10 +93,8 @@ pub(crate) enum ValueKind { RecordType(HashMap), RecordLit(HashMap), UnionType(HashMap>), - // Also keep the type of the uniontype around - UnionConstructor(Label, HashMap>, Value), - // Also keep the type of the uniontype and the constructor around - UnionLit(Label, Value, HashMap>, Value, Value), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), TextLit(TextLit), Equivalence(Value, Value), /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? @@ -298,14 +296,14 @@ impl Value { .collect(), ), ValueKind::UnionType(kts) => map_uniontype(kts), - ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( + ValueKind::UnionConstructor(l, kts) => ExprKind::Field( Hir::new( HirKind::Expr(map_uniontype(kts)), Span::Artificial, ), l.clone(), ), - ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( + ValueKind::UnionLit(l, v, kts) => ExprKind::App( Hir::new( HirKind::Expr(ExprKind::Field( Hir::new( @@ -418,13 +416,12 @@ impl ValueKind { x.normalize(); } } - ValueKind::UnionType(kts) - | ValueKind::UnionConstructor(_, kts, _) => { + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { for x in kts.values().flat_map(|opt| opt) { x.normalize(); } } - ValueKind::UnionLit(_, v, kts, _, _) => { + ValueKind::UnionLit(_, v, kts) => { v.normalize(); for x in kts.values().flat_map(|opt| opt) { x.normalize(); -- cgit v1.2.3 From 21db63d3e614554f258526182c7ed89a2c244b65 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 21:58:28 +0000 Subject: Take Hir for typecheck --- dhall/src/semantics/nze/value.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index a771b91..48acdb5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -327,9 +327,12 @@ impl Value { Hir::new(hir, self.0.span.clone()) } + pub fn to_hir_noenv(&self) -> Hir { + self.to_hir(VarEnv::new()) + } pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { - let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv); - type_with(tyenv, &expr).unwrap() + let hir = self.to_hir(tyenv.as_varenv()); + type_with(tyenv, &hir).unwrap() } pub fn to_tyexpr_noenv(&self) -> TyExpr { self.to_tyexpr_tyenv(&TyEnv::new()) -- cgit v1.2.3 From ad085a20bc257d03a52708d920cfc65f0e9051e6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:07:03 +0000 Subject: Remove all types from Value --- dhall/src/semantics/nze/value.rs | 80 ++++------------------------------------ 1 file changed, 7 insertions(+), 73 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 48acdb5..5a7b558 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,7 +1,7 @@ use std::collections::HashMap; use std::rc::Rc; -use crate::error::{TypeError, TypeMessage}; +use crate::error::TypeError; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, @@ -25,8 +25,6 @@ pub(crate) struct Value(Rc); #[derive(Debug)] struct ValueInternal { kind: lazy::Lazy, - /// This is None if and only if `form` is `Sort` (which doesn't have a type) - ty: Option, span: Span, } @@ -103,25 +101,12 @@ pub(crate) enum ValueKind { impl Value { pub(crate) fn const_sort() -> Value { - ValueInternal::from_whnf( - ValueKind::Const(Const::Sort), - None, - Span::Artificial, - ) - .into_value() - } - pub(crate) fn const_kind() -> Value { - Value::from_const(Const::Kind) + Value::from_const(Const::Sort) } /// Construct a Value from a completely unnormalized expression. pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value { let span = hir.span(); - ValueInternal::from_thunk( - Thunk::new(env, hir), - Some(Value::const_kind()), - span, - ) - .into_value() + ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. pub(crate) fn from_partial_expr(e: ExprKind) -> Value { @@ -129,33 +114,17 @@ impl Value { let env = NzEnv::new(); ValueInternal::from_thunk( 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(v: ValueKind) -> Value { - ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial) - .into_value() + ValueInternal::from_whnf(v, Span::Artificial).into_value() } pub(crate) fn from_const(c: Const) -> Self { let v = ValueKind::Const(c); - match c { - Const::Type => ValueInternal::from_whnf( - v, - Some(Value::from_const(Const::Kind)), - Span::Artificial, - ) - .into_value(), - Const::Kind => ValueInternal::from_whnf( - v, - Some(Value::const_sort()), - Span::Artificial, - ) - .into_value(), - Const::Sort => Value::const_sort(), - } + ValueInternal::from_whnf(v, Span::Artificial).into_value() } pub(crate) fn from_builtin(b: Builtin) -> Self { Self::from_builtin_env(b, &NzEnv::new()) @@ -193,16 +162,6 @@ impl Value { self.to_hir(env.as_varenv()).to_expr_tyenv(env) } - /// Normalizes contents to normal form; faster than `normalize` if - /// no one else shares this. - pub(crate) fn normalize_mut(&mut self) { - match Rc::get_mut(&mut self.0) { - // Mutate directly if sole owner - Some(vint) => vint.normalize_mut(), - // Otherwise mutate through the refcell - None => self.normalize(), - } - } pub(crate) fn normalize(&self) { self.0.normalize() } @@ -214,13 +173,6 @@ impl Value { pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result { self.to_tyexpr_tyenv(tyenv).get_type() } - /// When we know the value isn't `Sort`, this gets the type directly - pub(crate) fn get_type_not_sort(&self) -> Value { - self.0 - .get_type() - .expect("Internal type error: value is `Sort` but shouldn't be") - .clone() - } pub fn to_hir(&self, venv: VarEnv) -> Hir { let map_uniontype = |kts: &HashMap>| { @@ -340,17 +292,15 @@ impl Value { } impl ValueInternal { - fn from_whnf(k: ValueKind, ty: Option, span: Span) -> Self { + fn from_whnf(k: ValueKind, span: Span) -> Self { ValueInternal { kind: lazy::Lazy::new_completed(k), - ty, span, } } - fn from_thunk(th: Thunk, ty: Option, span: Span) -> Self { + fn from_thunk(th: Thunk, span: Span) -> Self { ValueInternal { kind: lazy::Lazy::new(th), - ty, span, } } @@ -364,17 +314,6 @@ impl ValueInternal { fn normalize(&self) { self.kind().normalize(); } - // TODO: deprecated - fn normalize_mut(&mut self) { - self.normalize(); - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => Err(TypeError::new(TypeMessage::Sort)), - } - } } impl ValueKind { @@ -616,11 +555,6 @@ impl std::fmt::Debug for Value { } let mut x = fmt.debug_struct(&format!("Value@WHNF")); x.field("kind", kind); - if let Some(ty) = vint.ty.as_ref() { - x.field("type", &ty); - } else { - x.field("type", &None::<()>); - } x.finish() } } -- cgit v1.2.3 From 35cc98dc767247f4881866de40c7d8dd82eba8a5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 22:30:32 +0000 Subject: Remove types from NzEnv --- dhall/src/semantics/nze/value.rs | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 5a7b558..a60be9d 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -100,11 +100,8 @@ pub(crate) enum ValueKind { } impl Value { - pub(crate) fn const_sort() -> Value { - Value::from_const(Const::Sort) - } /// Construct a Value from a completely unnormalized expression. - pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value { + pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value { let span = hir.span(); ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() } @@ -158,8 +155,8 @@ impl Value { self.to_tyexpr_noenv().to_expr(opts) } - pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { - self.to_hir(env.as_varenv()).to_expr_tyenv(env) + pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { + self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) } pub(crate) fn normalize(&self) { @@ -389,11 +386,8 @@ impl ValueKind { } impl Thunk { - fn new(env: &NzEnv, body: Hir) -> Self { - Thunk::Thunk { - env: env.clone(), - body, - } + fn new(env: NzEnv, body: Hir) -> Self { + Thunk::Thunk { env, body } } fn from_partial_expr( env: NzEnv, @@ -424,7 +418,7 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { - body.eval(&env.insert_value_noty(val)) + body.eval(&env.insert_value(val, ())) } Closure::ConstantClosure { body, .. } => body.clone(), } -- cgit v1.2.3 From 5a2538d174fd36a8ed7f4fa344b9583fc48bd977 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 13:12:13 +0000 Subject: Remove the Embed variant from ExprKind --- dhall/src/semantics/nze/value.rs | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index a60be9d..0df3c74 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -12,7 +12,7 @@ use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; -use crate::{Normalized, NormalizedExpr, ToExprOptions}; +use crate::{NormalizedExpr, ToExprOptions}; /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation /// automatically. Uses a Rc to share computation. @@ -34,10 +34,7 @@ pub(crate) enum Thunk { /// A completely unnormalized expression. Thunk { env: NzEnv, body: Hir }, /// A partially normalized expression that may need to go through `normalize_one_layer`. - PartialExpr { - env: NzEnv, - expr: ExprKind, - }, + PartialExpr { env: NzEnv, expr: ExprKind }, } /// An unevaluated subexpression that takes an argument. @@ -96,7 +93,7 @@ pub(crate) enum ValueKind { TextLit(TextLit), Equivalence(Value, Value), /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? - PartialExpr(ExprKind), + PartialExpr(ExprKind), } impl Value { @@ -106,7 +103,7 @@ impl Value { ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() } /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind) -> Value { + pub(crate) fn from_partial_expr(e: ExprKind) -> Value { // TODO: env let env = NzEnv::new(); ValueInternal::from_thunk( @@ -389,10 +386,7 @@ impl Thunk { fn new(env: NzEnv, body: Hir) -> Self { Thunk::Thunk { env, body } } - fn from_partial_expr( - env: NzEnv, - expr: ExprKind, - ) -> Self { + fn from_partial_expr(env: NzEnv, expr: ExprKind) -> Self { Thunk::PartialExpr { env, expr } } fn eval(self) -> ValueKind { -- cgit v1.2.3 From 40bee3cdcb9ac0c76996feeceb6ca160a6bd8b42 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 11 Feb 2020 19:04:44 +0000 Subject: Introduce LitKind to factor out common enum nodes --- dhall/src/semantics/nze/value.rs | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 0df3c74..2ae6852 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -9,8 +9,8 @@ use crate::semantics::{ TyExpr, VarEnv, }; use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, Span, + BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, + Span, }; use crate::{NormalizedExpr, ToExprOptions}; @@ -76,10 +76,7 @@ pub(crate) enum ValueKind { Var(NzVar), Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), + Lit(LitKind), EmptyOptionalLit(Value), NEOptionalLit(Value), // EmptyListLit(t) means `[] : List t`, not `[] : t` @@ -205,10 +202,7 @@ impl Value { closure.to_hir(venv), ), ValueKind::Const(c) => ExprKind::Const(*c), - ValueKind::BoolLit(b) => ExprKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ExprKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n), + ValueKind::Lit(l) => ExprKind::Lit(l.clone()), ValueKind::EmptyOptionalLit(n) => ExprKind::App( Value::from_builtin(Builtin::OptionalNone).to_hir(venv), n.to_hir(venv), @@ -317,12 +311,7 @@ impl ValueKind { pub(crate) fn normalize(&self) { match self { - ValueKind::Var(..) - | ValueKind::Const(_) - | ValueKind::BoolLit(_) - | ValueKind::NaturalLit(_) - | ValueKind::IntegerLit(_) - | ValueKind::DoubleLit(_) => {} + ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {} ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { tth.normalize(); -- cgit v1.2.3 From f29a40fb55b898b3a3cc51f198e8522eaecf0777 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 13 Feb 2020 20:17:41 +0000 Subject: Simplify conversions to/from TyExpr --- dhall/src/semantics/nze/value.rs | 20 +++----------------- 1 file changed, 3 insertions(+), 17 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 2ae6852..0603fb5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -1,12 +1,10 @@ use std::collections::HashMap; use std::rc::Rc; -use crate::error::TypeError; use crate::semantics::nze::lazy; use crate::semantics::{ - apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, - type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, - TyExpr, VarEnv, + apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, + BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, @@ -146,8 +144,7 @@ impl Value { if opts.normalize { self.normalize(); } - - self.to_tyexpr_noenv().to_expr(opts) + self.to_hir_noenv().to_expr(opts) } pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) @@ -161,10 +158,6 @@ impl Value { Value::from_kind(apply_any(self.clone(), v)) } - pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result { - self.to_tyexpr_tyenv(tyenv).get_type() - } - pub fn to_hir(&self, venv: VarEnv) -> Hir { let map_uniontype = |kts: &HashMap>| { ExprKind::UnionType( @@ -270,13 +263,6 @@ impl Value { pub fn to_hir_noenv(&self) -> Hir { self.to_hir(VarEnv::new()) } - pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr { - let hir = self.to_hir(tyenv.as_varenv()); - type_with(tyenv, &hir).unwrap() - } - pub fn to_tyexpr_noenv(&self) -> TyExpr { - self.to_tyexpr_tyenv(&TyEnv::new()) - } } impl ValueInternal { -- cgit v1.2.3 From d65d639ff93691adbf0a208edb99736003bc64bd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:05:26 +0000 Subject: Factor some tck code to avoid needing get_type_tyexpr --- dhall/src/semantics/nze/value.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 0603fb5..3a5b5b5 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -87,7 +87,7 @@ pub(crate) enum ValueKind { UnionLit(Label, Value, HashMap>), TextLit(TextLit), Equivalence(Value, Value), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`? + /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. PartialExpr(ExprKind), } @@ -387,7 +387,7 @@ impl Closure { pub fn apply(&self, val: Value) -> Value { match self { Closure::Closure { env, body, .. } => { - body.eval(&env.insert_value(val, ())) + body.eval(env.insert_value(val, ())) } Closure::ConstantClosure { body, .. } => body.clone(), } -- cgit v1.2.3 From aa867b21f57f9bef2ec2b9d8450736f9111189ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 15 Feb 2020 19:44:40 +0000 Subject: Introduce proper Type struct --- dhall/src/semantics/nze/value.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 3a5b5b5..f31fd6c 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, - BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, VarEnv, + BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, @@ -139,6 +139,9 @@ impl Value { self.0.kind() } + pub(crate) fn to_type(&self) -> Type { + self.clone().into() + } /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { if opts.normalize { -- cgit v1.2.3 From c451c18103b871e563b12c524bc3feec5451154c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 16 Feb 2020 19:48:35 +0000 Subject: Avoid recomputing universes in tck --- dhall/src/semantics/nze/value.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index f31fd6c..7084af6 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -4,7 +4,7 @@ use std::rc::Rc; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, - BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, VarEnv, + BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, @@ -139,8 +139,8 @@ impl Value { self.0.kind() } - pub(crate) fn to_type(&self) -> Type { - self.clone().into() + pub(crate) fn to_type(&self, u: impl Into) -> Type { + Type::new(self.clone(), u.into()) } /// Converts a value back to the corresponding AST expression. pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/nze/value.rs | 526 --------------------------------------- 1 file changed, 526 deletions(-) delete mode 100644 dhall/src/semantics/nze/value.rs (limited to 'dhall/src/semantics/nze/value.rs') diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs deleted file mode 100644 index 7084af6..0000000 --- a/dhall/src/semantics/nze/value.rs +++ /dev/null @@ -1,526 +0,0 @@ -use std::collections::HashMap; -use std::rc::Rc; - -use crate::semantics::nze::lazy; -use crate::semantics::{ - apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit, Binder, - BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv, Type, Universe, VarEnv, -}; -use crate::syntax::{ - BinOp, Builtin, Const, ExprKind, InterpolatedTextContents, Label, LitKind, - Span, -}; -use crate::{NormalizedExpr, ToExprOptions}; - -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation -/// automatically. Uses a Rc to share computation. -/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence -/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively -/// normalize as needed. -#[derive(Clone)] -pub(crate) struct Value(Rc); - -#[derive(Debug)] -struct ValueInternal { - kind: lazy::Lazy, - span: Span, -} - -/// An unevaluated subexpression -#[derive(Debug, Clone)] -pub(crate) enum Thunk { - /// A completely unnormalized expression. - Thunk { env: NzEnv, body: Hir }, - /// A partially normalized expression that may need to go through `normalize_one_layer`. - PartialExpr { env: NzEnv, expr: ExprKind }, -} - -/// An unevaluated subexpression that takes an argument. -#[derive(Debug, Clone)] -pub(crate) enum Closure { - /// Normal closure - Closure { env: NzEnv, body: Hir }, - /// Closure that ignores the argument passed - ConstantClosure { body: Value }, -} - -/// A text literal with interpolations. -// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous -// text values must be merged. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) struct TextLit(Vec>); - -/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is -/// normalized up to the first constructor, but subexpressions may not be fully normalized. -/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in -/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so -/// if we have the first constructor of the NF at all levels, we actually have the NF. -/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and -/// we only need to recursively normalize its sub-`Value`s to get to the NF. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { - /// Closures - LamClosure { - binder: Binder, - annot: Value, - closure: Closure, - }, - PiClosure { - binder: Binder, - annot: Value, - closure: Closure, - }, - AppliedBuiltin(BuiltinClosure), - - Var(NzVar), - Const(Const), - Lit(LitKind), - EmptyOptionalLit(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - TextLit(TextLit), - Equivalence(Value, Value), - /// Invariant: evaluation must not be able to progress with `normalize_one_layer`. - PartialExpr(ExprKind), -} - -impl Value { - /// Construct a Value from a completely unnormalized expression. - pub(crate) fn new_thunk(env: NzEnv, hir: Hir) -> Value { - let span = hir.span(); - ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value() - } - /// Construct a Value from a partially normalized expression that's not in WHNF. - pub(crate) fn from_partial_expr(e: ExprKind) -> Value { - // TODO: env - let env = NzEnv::new(); - ValueInternal::from_thunk( - Thunk::from_partial_expr(env, e), - Span::Artificial, - ) - .into_value() - } - /// Make a Value from a ValueKind - pub(crate) fn from_kind(v: ValueKind) -> Value { - ValueInternal::from_whnf(v, Span::Artificial).into_value() - } - pub(crate) fn from_const(c: Const) -> Self { - let v = ValueKind::Const(c); - ValueInternal::from_whnf(v, Span::Artificial).into_value() - } - pub(crate) fn from_builtin(b: Builtin) -> Self { - Self::from_builtin_env(b, &NzEnv::new()) - } - pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self { - Value::from_kind(ValueKind::from_builtin_env(b, env.clone())) - } - pub(crate) fn from_text(txt: impl ToString) -> Self { - Value::from_kind(ValueKind::TextLit(TextLit::from_text( - txt.to_string(), - ))) - } - - pub(crate) fn as_const(&self) -> Option { - match &*self.kind() { - ValueKind::Const(c) => Some(*c), - _ => None, - } - } - - /// This is what you want if you want to pattern-match on the value. - pub(crate) fn kind(&self) -> &ValueKind { - self.0.kind() - } - - pub(crate) fn to_type(&self, u: impl Into) -> Type { - Type::new(self.clone(), u.into()) - } - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.normalize { - self.normalize(); - } - self.to_hir_noenv().to_expr(opts) - } - pub(crate) fn to_expr_tyenv(&self, tyenv: &TyEnv) -> NormalizedExpr { - self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv) - } - - pub(crate) fn normalize(&self) { - self.0.normalize() - } - - pub(crate) fn app(&self, v: Value) -> Value { - Value::from_kind(apply_any(self.clone(), v)) - } - - pub fn to_hir(&self, venv: VarEnv) -> Hir { - let map_uniontype = |kts: &HashMap>| { - ExprKind::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_hir(venv))) - }) - .collect(), - ) - }; - - let hir = match &*self.kind() { - ValueKind::Var(v) => HirKind::Var(venv.lookup(v)), - ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv), - self_kind => HirKind::Expr(match self_kind { - ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => { - unreachable!() - } - ValueKind::LamClosure { - binder, - annot, - closure, - } => ExprKind::Lam( - binder.to_label(), - annot.to_hir(venv), - closure.to_hir(venv), - ), - ValueKind::PiClosure { - binder, - annot, - closure, - } => ExprKind::Pi( - binder.to_label(), - annot.to_hir(venv), - closure.to_hir(venv), - ), - ValueKind::Const(c) => ExprKind::Const(*c), - ValueKind::Lit(l) => ExprKind::Lit(l.clone()), - ValueKind::EmptyOptionalLit(n) => ExprKind::App( - Value::from_builtin(Builtin::OptionalNone).to_hir(venv), - n.to_hir(venv), - ), - ValueKind::NEOptionalLit(n) => { - ExprKind::SomeLit(n.to_hir(venv)) - } - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new( - HirKind::Expr(ExprKind::App( - Value::from_builtin(Builtin::List).to_hir(venv), - n.to_hir(venv), - )), - Span::Artificial, - )), - ValueKind::NEListLit(elts) => ExprKind::NEListLit( - elts.iter().map(|v| v.to_hir(venv)).collect(), - ), - ValueKind::TextLit(elts) => ExprKind::TextLit( - elts.iter() - .map(|t| t.map_ref(|v| v.to_hir(venv))) - .collect(), - ), - ValueKind::RecordLit(kvs) => ExprKind::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_hir(venv))) - .collect(), - ), - ValueKind::RecordType(kts) => ExprKind::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_hir(venv))) - .collect(), - ), - ValueKind::UnionType(kts) => map_uniontype(kts), - ValueKind::UnionConstructor(l, kts) => ExprKind::Field( - Hir::new( - HirKind::Expr(map_uniontype(kts)), - Span::Artificial, - ), - l.clone(), - ), - ValueKind::UnionLit(l, v, kts) => ExprKind::App( - Hir::new( - HirKind::Expr(ExprKind::Field( - Hir::new( - HirKind::Expr(map_uniontype(kts)), - Span::Artificial, - ), - l.clone(), - )), - Span::Artificial, - ), - v.to_hir(venv), - ), - ValueKind::Equivalence(x, y) => ExprKind::BinOp( - BinOp::Equivalence, - x.to_hir(venv), - y.to_hir(venv), - ), - ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)), - }), - }; - - Hir::new(hir, self.0.span.clone()) - } - pub fn to_hir_noenv(&self) -> Hir { - self.to_hir(VarEnv::new()) - } -} - -impl ValueInternal { - fn from_whnf(k: ValueKind, span: Span) -> Self { - ValueInternal { - kind: lazy::Lazy::new_completed(k), - span, - } - } - fn from_thunk(th: Thunk, span: Span) -> Self { - ValueInternal { - kind: lazy::Lazy::new(th), - span, - } - } - fn into_value(self) -> Value { - Value(Rc::new(self)) - } - - fn kind(&self) -> &ValueKind { - &self.kind - } - fn normalize(&self) { - self.kind().normalize(); - } -} - -impl ValueKind { - pub(crate) fn into_value(self) -> Value { - Value::from_kind(self) - } - - pub(crate) fn normalize(&self) { - match self { - ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::Lit(_) => {} - - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize(); - } - - ValueKind::NEOptionalLit(th) => { - th.normalize(); - } - ValueKind::LamClosure { annot, closure, .. } - | ValueKind::PiClosure { annot, closure, .. } => { - annot.normalize(); - closure.normalize(); - } - ValueKind::AppliedBuiltin(closure) => closure.normalize(), - ValueKind::NEListLit(elts) => { - for x in elts.iter() { - x.normalize(); - } - } - ValueKind::RecordLit(kvs) => { - for x in kvs.values() { - x.normalize(); - } - } - ValueKind::RecordType(kvs) => { - for x in kvs.values() { - x.normalize(); - } - } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { - for x in kts.values().flat_map(|opt| opt) { - x.normalize(); - } - } - ValueKind::UnionLit(_, v, kts) => { - v.normalize(); - for x in kts.values().flat_map(|opt| opt) { - x.normalize(); - } - } - ValueKind::TextLit(tlit) => tlit.normalize(), - ValueKind::Equivalence(x, y) => { - x.normalize(); - y.normalize(); - } - ValueKind::PartialExpr(e) => { - e.map_ref(Value::normalize); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::from_builtin_env(b, NzEnv::new()) - } - pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind { - ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env)) - } -} - -impl Thunk { - fn new(env: NzEnv, body: Hir) -> Self { - Thunk::Thunk { env, body } - } - fn from_partial_expr(env: NzEnv, expr: ExprKind) -> Self { - Thunk::PartialExpr { env, expr } - } - fn eval(self) -> ValueKind { - match self { - Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body), - Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), - } - } -} - -impl Closure { - pub fn new(env: &NzEnv, body: Hir) -> Self { - Closure::Closure { - env: env.clone(), - body, - } - } - /// New closure that ignores its argument - pub fn new_constant(body: Value) -> Self { - Closure::ConstantClosure { body } - } - - pub fn apply(&self, val: Value) -> Value { - match self { - Closure::Closure { env, body, .. } => { - body.eval(env.insert_value(val, ())) - } - Closure::ConstantClosure { body, .. } => body.clone(), - } - } - fn apply_var(&self, var: NzVar) -> Value { - match self { - Closure::Closure { .. } => { - self.apply(Value::from_kind(ValueKind::Var(var))) - } - Closure::ConstantClosure { body, .. } => body.clone(), - } - } - - // TODO: somehow normalize the body. Might require to pass an env. - pub fn normalize(&self) {} - - /// Convert this closure to a Hir expression - pub fn to_hir(&self, venv: VarEnv) -> Hir { - self.apply_var(NzVar::new(venv.size())) - .to_hir(venv.insert()) - } - /// If the closure variable is free in the closure, return Err. Otherwise, return the value - /// with that free variable remove. - pub fn remove_binder(&self) -> Result { - match self { - Closure::Closure { .. } => { - let v = NzVar::fresh(); - // TODO: handle case where variable is used in closure - // TODO: return information about where the variable is used - Ok(self.apply_var(v)) - } - Closure::ConstantClosure { body, .. } => Ok(body.clone()), - } - } -} - -impl TextLit { - pub fn new( - elts: impl Iterator>, - ) -> Self { - TextLit(squash_textlit(elts)) - } - pub fn interpolate(v: Value) -> TextLit { - TextLit(vec![InterpolatedTextContents::Expr(v)]) - } - pub fn from_text(s: String) -> TextLit { - TextLit(vec![InterpolatedTextContents::Text(s)]) - } - - pub fn concat(&self, other: &TextLit) -> TextLit { - TextLit::new(self.iter().chain(other.iter()).cloned()) - } - pub fn is_empty(&self) -> bool { - self.0.is_empty() - } - /// If the literal consists of only one interpolation and not text, return the interpolated - /// value. - pub fn as_single_expr(&self) -> Option<&Value> { - use InterpolatedTextContents::Expr; - if let [Expr(v)] = self.0.as_slice() { - Some(v) - } else { - None - } - } - /// If there are no interpolations, return the corresponding text value. - pub fn as_text(&self) -> Option { - use InterpolatedTextContents::Text; - if self.is_empty() { - Some(String::new()) - } else if let [Text(s)] = self.0.as_slice() { - Some(s.clone()) - } else { - None - } - } - pub fn iter( - &self, - ) -> impl Iterator> { - self.0.iter() - } - /// Normalize the contained values. This does not break the invariant because we have already - /// ensured that no contained values normalize to a TextLit. - pub fn normalize(&self) { - for x in self.0.iter() { - x.map_ref(Value::normalize); - } - } -} - -impl lazy::Eval for Thunk { - fn eval(self) -> ValueKind { - self.eval() - } -} - -/// Compare two values for equality modulo alpha/beta-equivalence. -impl std::cmp::PartialEq for Value { - fn eq(&self, other: &Self) -> bool { - Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind() - } -} -impl std::cmp::Eq for Value {} - -impl std::cmp::PartialEq for Thunk { - fn eq(&self, _other: &Self) -> bool { - unreachable!( - "Trying to compare thunks but we should only compare WHNFs" - ) - } -} -impl std::cmp::Eq for Thunk {} - -impl std::cmp::PartialEq for Closure { - fn eq(&self, other: &Self) -> bool { - let v = NzVar::fresh(); - self.apply_var(v) == other.apply_var(v) - } -} -impl std::cmp::Eq for Closure {} - -impl std::fmt::Debug for Value { - fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - let vint: &ValueInternal = &self.0; - let kind = vint.kind(); - if let ValueKind::Const(c) = kind { - return write!(fmt, "{:?}", c); - } - let mut x = fmt.debug_struct(&format!("Value@WHNF")); - x.field("kind", kind); - x.finish() - } -} -- cgit v1.2.3