From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 Jan 2020 22:22:01 +0000 Subject: Implement basic env-based normalization for Value-based TyExpr --- dhall/src/semantics/core/value.rs | 267 +++++++++++++++++++++--------------- dhall/src/semantics/core/visitor.rs | 18 +++ 2 files changed, 177 insertions(+), 108 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index a7c207d..8beed24 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -5,7 +5,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::nze::{NzVar, QuoteEnv}; -use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; +use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, @@ -53,11 +53,27 @@ pub(crate) enum Form { NF, } +#[derive(Debug, Clone)] +pub(crate) struct Closure { + env: NzEnv, + body: TyExpr, +} + #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum ValueKind { /// Closures Lam(Binder, Value, Value), Pi(Binder, Value, Value), + LamClosure { + binder: Binder, + annot: Value, + closure: Closure, + }, + PiClosure { + binder: Binder, + annot: Value, + closure: Closure, + }, // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), @@ -267,128 +283,136 @@ impl Value { _ => self.as_internal().subst_shift(var, val).into_value(), } } - // pub(crate) fn subst_ctx(&self, ctx: &TyCtx) -> Self { - // match &*self.as_kind() { - // ValueKind::Var(var) => match ctx.lookup_alpha(var) { - // Some(val) => val, - // None => unreachable!("Internal type error"), - // }, - // kind => { - // let kind = kind.map_ref_with_special_handling_of_binders( - // |x| x.subst_ctx(ctx), - // |b, t, x| x.subst_ctx(&ctx.insert_type(b, t.clone())), - // ); - // ValueInternal { - // form: Unevaled, - // kind, - // ty: self.as_internal().ty.clone(), - // span: self.as_internal().span.clone(), - // } - // .into_value() - // } - // } - // } pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { - let self_kind = self.as_kind(); - let self_ty = self.as_internal().ty.clone(); - let self_span = self.as_internal().span.clone(); - if let ValueKind::Var(v, _w) = &*self_kind { - return TyExpr::new( + let tye = match &*self.as_kind() { + ValueKind::Var(v, _w) => { + TyExprKind::Var(*v) // TODO: Only works when we don't normalize under lambdas - // TyExprKind::Var(qenv.lookup(w)), - TyExprKind::Var(*v), - self_ty, - self_span, - ); - } - - // TODO: properly recover intermediate types; `None` is a time-bomb here. - let self_kind = self_kind.map_ref_with_special_handling_of_binders( - |v| v.to_tyexpr(qenv), - |_, _, v| v.to_tyexpr(qenv.insert()), - ); - let expr = match self_kind { - ValueKind::Var(..) => unreachable!(), - ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e), - ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), - ValueKind::AppliedBuiltin(b, args) => { - args.into_iter().fold(ExprKind::Builtin(b), |acc, v| { - ExprKind::App( - TyExpr::new( - TyExprKind::Expr(acc), - None, // TODO - Span::Artificial, - ), - v, - ) - }) + // TyExprKind::Var(qenv.lookup(w)) } - 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::EmptyOptionalLit(n) => ExprKind::App( - builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), - n, - ), - ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( - TyExprKind::Expr(ExprKind::App( - builtin_to_value(Builtin::List).to_tyexpr(qenv), - n, - )), - Some(const_to_value(Const::Type)), - Span::Artificial, + ValueKind::LamClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Lam( + binder.to_label(), + annot.to_tyexpr(qenv), + closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()), )), - ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), - ValueKind::RecordLit(kvs) => { - ExprKind::RecordLit(kvs.into_iter().collect()) - } - ValueKind::RecordType(kts) => { - ExprKind::RecordType(kts.into_iter().collect()) - } - ValueKind::UnionType(kts) => { - ExprKind::UnionType(kts.into_iter().collect()) - } - ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( - TyExpr::new( - TyExprKind::Expr(ExprKind::UnionType( - kts.into_iter().collect(), - )), - Some(t), - Span::Artificial, - ), - l, - ), - ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App( - TyExpr::new( - TyExprKind::Expr(ExprKind::Field( + ValueKind::PiClosure { + binder, + annot, + closure, + } => TyExprKind::Expr(ExprKind::Pi( + binder.to_label(), + annot.to_tyexpr(qenv), + closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()), + )), + self_kind => { + // TODO: properly recover intermediate types; `None` is a time-bomb here. + let self_kind = self_kind + .map_ref_with_special_handling_of_binders( + |v| v.to_tyexpr(qenv), + |_, _, v| v.to_tyexpr(qenv.insert()), + ); + let expr = match self_kind { + ValueKind::Var(..) + | ValueKind::LamClosure { .. } + | ValueKind::PiClosure { .. } => unreachable!(), + ValueKind::Lam(x, t, e) => { + ExprKind::Lam(x.to_label(), t, e) + } + ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), + ValueKind::AppliedBuiltin(b, args) => { + args.into_iter().fold(ExprKind::Builtin(b), |acc, v| { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(acc), + None, // TODO + Span::Artificial, + ), + v, + ) + }) + } + 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::EmptyOptionalLit(n) => ExprKind::App( + builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), + n, + ), + ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), + ValueKind::EmptyListLit(n) => { + ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + builtin_to_value(Builtin::List).to_tyexpr(qenv), + n, + )), + Some(const_to_value(Const::Type)), + Span::Artificial, + )) + } + ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), + ValueKind::RecordLit(kvs) => { + ExprKind::RecordLit(kvs.into_iter().collect()) + } + ValueKind::RecordType(kts) => { + ExprKind::RecordType(kts.into_iter().collect()) + } + ValueKind::UnionType(kts) => { + ExprKind::UnionType(kts.into_iter().collect()) + } + ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field( TyExpr::new( TyExprKind::Expr(ExprKind::UnionType( kts.into_iter().collect(), )), - Some(uniont), + Some(t), Span::Artificial, ), l, - )), - Some(ctort), - Span::Artificial, - ), - v, - ), - ValueKind::TextLit(elts) => { - ExprKind::TextLit(elts.into_iter().collect()) - } - ValueKind::Equivalence(x, y) => { - ExprKind::BinOp(BinOp::Equivalence, x, y) + ), + ValueKind::UnionLit(l, v, kts, uniont, ctort) => { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter().collect(), + )), + Some(uniont), + Span::Artificial, + ), + l, + )), + Some(ctort), + Span::Artificial, + ), + v, + ) + } + ValueKind::TextLit(elts) => { + ExprKind::TextLit(elts.into_iter().collect()) + } + ValueKind::Equivalence(x, y) => { + ExprKind::BinOp(BinOp::Equivalence, x, y) + } + ValueKind::PartialExpr(e) => e, + }; + TyExprKind::Expr(expr) } - ValueKind::PartialExpr(e) => e, }; - TyExpr::new(TyExprKind::Expr(expr), self_ty, self_span) + let self_ty = self.as_internal().ty.clone(); + let self_span = self.as_internal().span.clone(); + TyExpr::new(tye, self_ty, self_span) + } + pub fn to_tyexpr_noenv(&self) -> TyExpr { + self.to_tyexpr(QuoteEnv::new()) } } @@ -502,6 +526,10 @@ impl ValueKind { t.normalize_mut(); e.normalize_mut(); } + ValueKind::LamClosure { annot, .. } + | ValueKind::PiClosure { annot, .. } => { + annot.normalize_mut(); + } ValueKind::AppliedBuiltin(_, args) => { for x in args.iter_mut() { x.normalize_mut(); @@ -620,6 +648,21 @@ impl ValueKind { } } +impl Closure { + pub fn new(env: &NzEnv, body: TyExpr) -> Self { + Closure { + env: env.clone(), + body: body, + } + } + pub fn apply(&self, val: Value) -> Value { + self.body.normalize_whnf(&self.env.insert_value(val)) + } + pub fn apply_ty(&self, ty: Value) -> Value { + self.body.normalize_whnf(&self.env.insert_type(ty)) + } +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { @@ -628,6 +671,14 @@ impl std::cmp::PartialEq for Value { } impl std::cmp::Eq for Value {} +// TODO: panics +impl std::cmp::PartialEq for Closure { + fn eq(&self, _other: &Self) -> bool { + panic!("comparing closures for equality seems like a bad idea") + } +} +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.as_internal(); diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index 5a04747..ee44ed7 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -80,6 +80,24 @@ where let (t, e) = v.visit_binder(l, t, e)?; Pi(l.clone(), t, e) } + LamClosure { + binder, + annot, + closure, + } => LamClosure { + binder: binder.clone(), + annot: v.visit_val(annot)?, + closure: closure.clone(), + }, + PiClosure { + binder, + annot, + closure, + } => PiClosure { + binder: binder.clone(), + annot: v.visit_val(annot)?, + closure: closure.clone(), + }, AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), -- cgit v1.2.3