From ec28905d32c23109da17696faefab284fde3e103 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 18 Jan 2020 18:46:09 +0000 Subject: Introduce intermediate representation that stores typed expr --- dhall/src/semantics/core/value.rs | 87 +++++++++++++++++++++++++++++--- dhall/src/semantics/core/var.rs | 18 +------ dhall/src/semantics/mod.rs | 3 +- dhall/src/semantics/phase/mod.rs | 10 +++- dhall/src/semantics/tck/mod.rs | 2 + dhall/src/semantics/tck/tyexpr.rs | 83 +++++++++++++++++++++++++++++++ dhall/src/semantics/to_expr.rs | 101 -------------------------------------- dhall/src/syntax/ast/expr.rs | 2 +- 8 files changed, 177 insertions(+), 129 deletions(-) create mode 100644 dhall/src/semantics/tck/mod.rs create mode 100644 dhall/src/semantics/tck/tyexpr.rs delete mode 100644 dhall/src/semantics/to_expr.rs diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 8b3ada1..a1125cd 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -7,10 +7,12 @@ use crate::semantics::core::context::TyCtx; use crate::semantics::core::var::{AlphaVar, Binder}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; -use crate::semantics::to_expr; +use crate::semantics::phase::{ + Normalized, NormalizedExpr, ToExprOptions, Typed, +}; +use crate::semantics::{TyExpr, TyExprKind}; use crate::syntax::{ - Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, }; @@ -159,11 +161,12 @@ impl Value { } /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::value_to_expr(self, opts, &vec![]) + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + if opts.normalize { + self.normalize_nf(); + } + + self.to_tyexpr().to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() @@ -283,6 +286,10 @@ impl Value { // } // } // } + + pub fn to_tyexpr(&self) -> TyExpr { + value_to_tyexpr(self) + } } impl ValueInternal { @@ -510,6 +517,70 @@ impl ValueKind { } } +fn value_to_tyexpr(val: &Value) -> TyExpr { + let val_kind = val.as_kind(); + let val_ty = val.as_internal().ty.clone(); + let val_span = val.as_internal().span.clone(); + if let ValueKind::Var(v) = &*val_kind { + return TyExpr::new(TyExprKind::Var(*v), val_ty, val_span); + } + + // TODO: properly recover intermediate types; `None` is a time-bomb here. + let rc = |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial); + + let val_kind = val_kind.map_ref(|v| v.to_tyexpr()); + let expr = match val_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(rc(acc), 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(rc(ExprKind::Builtin(Builtin::OptionalNone)), n) + } + ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), + ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc( + ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n), + )), + 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) => ExprKind::Field( + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, + ), + ValueKind::UnionLit(l, v, kts) => ExprKind::App( + rc(ExprKind::Field( + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, + )), + v, + ), + ValueKind::TextLit(elts) => { + ExprKind::TextLit(elts.into_iter().collect()) + } + ValueKind::Equivalence(x, y) => { + ExprKind::BinOp(BinOp::Equivalence, x, y) + } + ValueKind::PartialExpr(e) => e, + }; + + TyExpr::new(TyExprKind::Expr(expr), val_ty, val_span) +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index b336c66..0aa86d5 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,7 +1,7 @@ use crate::syntax::{Label, V}; /// Stores an alpha-normalized variable. -#[derive(Clone, Eq)] +#[derive(Clone, Copy, PartialEq, Eq)] pub struct AlphaVar { alpha: V<()>, } @@ -36,27 +36,11 @@ impl Binder { pub(crate) fn new(name: Label) -> Self { Binder { name } } - pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label { - if alpha { - "_".into() - } else { - self.to_label() - } - } pub(crate) fn to_label(&self) -> Label { self.clone().into() } - pub(crate) fn name(&self) -> &Label { - &self.name - } } -/// Equality up to alpha-equivalence -impl std::cmp::PartialEq for AlphaVar { - fn eq(&self, other: &Self) -> bool { - self.alpha == other.alpha - } -} /// Equality up to alpha-equivalence impl std::cmp::PartialEq for Binder { fn eq(&self, _other: &Self) -> bool { diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 3ef1aba..63f74ee 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,4 +1,5 @@ pub mod core; pub mod phase; -pub mod to_expr; +pub mod tck; pub(crate) use self::core::*; +pub(crate) use self::tck::*; diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 6afed88..4dc91e7 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,6 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; use resolve::ImportRoot; @@ -38,6 +37,15 @@ pub struct Typed(Value); #[derive(Debug, Clone)] pub struct Normalized(Typed); +/// Controls conversion from `Value` to `Expr` +#[derive(Copy, Clone)] +pub(crate) struct ToExprOptions { + /// Whether to convert all variables to `_` + pub(crate) alpha: bool, + /// Whether to normalize before converting + pub(crate) normalize: bool, +} + impl Parsed { pub fn parse_file(f: &Path) -> Result { parse::parse_file(f) diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs new file mode 100644 index 0000000..407605d --- /dev/null +++ b/dhall/src/semantics/tck/mod.rs @@ -0,0 +1,2 @@ +pub mod tyexpr; +pub(crate) use tyexpr::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs new file mode 100644 index 0000000..a8b8e58 --- /dev/null +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -0,0 +1,83 @@ +#![allow(dead_code)] +use crate::semantics::core::var::AlphaVar; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::Normalized; +use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; +use crate::semantics::Value; +use crate::syntax::{ExprKind, Label, Span, V}; + +pub(crate) type Type = Value; + +// An expression with inferred types at every node and resolved variables. +pub(crate) struct TyExpr { + kind: Box, + ty: Option, + span: Span, +} + +pub(crate) enum TyExprKind { + Var(AlphaVar), + // Forbidden ExprKind variants: Var + Expr(ExprKind), +} + +impl TyExpr { + pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { + TyExpr { + kind: Box::new(kind), + ty, + span, + } + } + + pub fn kind(&self) -> &TyExprKind { + &*self.kind + } + + /// Converts a value back to the corresponding AST expression. + pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr { + tyexpr_to_expr(self, opts, &Vec::new()) + } +} + +// TODO: mutate context once map_ref gets simplified +fn tyexpr_to_expr<'a>( + tyexpr: &'a TyExpr, + opts: ToExprOptions, + ctx: &Vec<&'a Label>, +) -> NormalizedExpr { + rc(match tyexpr.kind() { + TyExprKind::Var(v) if opts.alpha => { + ExprKind::Var(V("_".into(), v.idx())) + } + TyExprKind::Var(v) => { + let name = ctx[ctx.len() - 1 - v.idx()]; + let mut idx = 0; + for l in ctx.iter().rev().take(v.idx()) { + if *l == name { + idx += 1; + } + } + ExprKind::Var(V(name.clone(), idx)) + } + TyExprKind::Expr(e) => { + let e = e.map_ref_with_special_handling_of_binders( + |tye| tyexpr_to_expr(tye, opts, ctx), + |l, tye| { + let ctx = ctx.iter().copied().chain(Some(l)).collect(); + tyexpr_to_expr(tye, opts, &ctx) + }, + ); + + match e { + ExprKind::Lam(_, t, e) if opts.alpha => { + ExprKind::Lam("_".into(), t, e) + } + ExprKind::Pi(_, t, e) if opts.alpha => { + ExprKind::Pi("_".into(), t, e) + } + e => e, + } + } + }) +} diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs deleted file mode 100644 index 612f794..0000000 --- a/dhall/src/semantics/to_expr.rs +++ /dev/null @@ -1,101 +0,0 @@ -use crate::semantics::core::var::Binder; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::NormalizedExpr; -use crate::semantics::{Value, ValueKind}; -use crate::syntax; -use crate::syntax::{Builtin, ExprKind, V}; - -/// Controls conversion from `Value` to `Expr` -#[derive(Copy, Clone)] -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - -/// Converts a value back to the corresponding AST expression. -pub(crate) fn value_to_expr<'a>( - val: &'a Value, - opts: ToExprOptions, - ctx: &Vec<&'a Binder>, -) -> NormalizedExpr { - if opts.normalize { - val.normalize_whnf(); - } - - let kind = val.as_kind(); - let kind = kind.map_ref_with_special_handling_of_binders( - |v| value_to_expr(v, opts, ctx), - |b, _, v| { - let mut ctx = ctx.clone(); - ctx.push(b); - value_to_expr(v, opts, &ctx) - }, - ); - match kind { - ValueKind::Var(v) if opts.alpha => { - rc(ExprKind::Var(V("_".into(), v.idx()))) - } - ValueKind::Var(v) => { - let name = ctx[ctx.len() - 1 - v.idx()].to_label(); - let mut idx = 0; - for b in ctx.iter().rev().take(v.idx()) { - if b.name() == &name { - idx += 1; - } - } - rc(ExprKind::Var(V(name, idx))) - } - ValueKind::Lam(x, t, e) => { - rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) - } - ValueKind::AppliedBuiltin(b, args) => args - .into_iter() - .fold(rc(ExprKind::Builtin(b)), |acc, v| rc(ExprKind::App(acc, v))), - ValueKind::Pi(x, t, e) => { - rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e)) - } - ValueKind::Const(c) => rc(ExprKind::Const(c)), - ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)), - ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)), - ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(n)), - ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::OptionalNone)), - n, - )), - ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n)), - ValueKind::EmptyListLit(n) => rc(ExprKind::EmptyListLit(rc( - ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n), - ))), - ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(elts)), - ValueKind::RecordLit(kvs) => { - rc(ExprKind::RecordLit(kvs.into_iter().collect())) - } - ValueKind::RecordType(kts) => { - rc(ExprKind::RecordType(kts.into_iter().collect())) - } - ValueKind::UnionType(kts) => { - rc(ExprKind::UnionType(kts.into_iter().collect())) - } - ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( - rc(ExprKind::UnionType(kts.into_iter().collect())), - l, - )), - ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( - rc(ExprKind::Field( - rc(ExprKind::UnionType(kts.into_iter().collect())), - l, - )), - v, - )), - ValueKind::TextLit(elts) => { - rc(ExprKind::TextLit(elts.into_iter().collect())) - } - ValueKind::Equivalence(x, y) => { - rc(ExprKind::BinOp(syntax::BinOp::Equivalence, x, y)) - } - ValueKind::PartialExpr(e) => rc(e), - } -} diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs index 170cbe7..f22a279 100644 --- a/dhall/src/syntax/ast/expr.rs +++ b/dhall/src/syntax/ast/expr.rs @@ -23,7 +23,7 @@ pub enum Const { /// The `Label` field is the variable's name (i.e. \"`x`\"). /// The `Int` field is a DeBruijn index. /// See dhall-lang/standard/semantics.md for details -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] pub struct V