From 8edbeadbd0dc06a75ffb8bf3b0a54a62e3acc5fc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 14:26:40 +0000 Subject: Parameterize ValueKind by its subnodes --- dhall/src/semantics/to_expr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/semantics/to_expr.rs') diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index b21fb29..9dee7b5 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -27,7 +27,7 @@ pub(crate) fn value_to_expr( /// Converts a value back to the corresponding AST expression. pub(crate) fn kind_to_expr( - kind: &ValueKind, + kind: &ValueKind, opts: ToExprOptions, ) -> NormalizedExpr { match kind { -- cgit v1.2.3 From 03da8fd6399f09c6282e0cd3930b6e39cc089043 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 21:14:45 +0000 Subject: Simplify Value::to_expr --- dhall/src/semantics/to_expr.rs | 112 ++++++++++++++++------------------------- 1 file changed, 43 insertions(+), 69 deletions(-) (limited to 'dhall/src/semantics/to_expr.rs') diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 9dee7b5..11e289f 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -5,8 +5,8 @@ use crate::semantics::phase::NormalizedExpr; use crate::syntax; use crate::syntax::{Builtin, ExprKind}; -#[derive(Copy, Clone)] /// Controls conversion from `Value` to `Expr` +#[derive(Copy, Clone)] pub(crate) struct ToExprOptions { /// Whether to convert all variables to `_` pub(crate) alpha: bool, @@ -22,84 +22,58 @@ pub(crate) fn value_to_expr( if opts.normalize { val.normalize_whnf(); } - val.as_kind().to_expr(opts) -} -/// Converts a value back to the corresponding AST expression. -pub(crate) fn kind_to_expr( - kind: &ValueKind, - opts: ToExprOptions, -) -> NormalizedExpr { - match kind { - ValueKind::Lam(x, t, e) => rc(ExprKind::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), + match val.as_kind().map_ref(|v| value_to_expr(v, opts)) { + ValueKind::Lam(x, t, e) => { + rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) + } ValueKind::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .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.to_expr(opts), - e.to_expr(opts), - )), + .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::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), - 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::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.to_expr(opts), + n, )), - ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => { - rc(ExprKind::EmptyListLit(rc(ExprKind::App( - rc(ExprKind::Builtin(Builtin::List)), - n.to_expr(opts), - )))) + 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::NEListLit(elts) => rc(ExprKind::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprKind::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprKind::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprKind::UnionType( - kts.iter() - .map(|(k, v)| (k.clone(), v.as_ref().map(|v| v.to_expr(opts)))) - .collect(), - )), ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field( - ValueKind::UnionType(kts.clone()).to_expr(opts), - l.clone(), + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, )), ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprKind::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprKind::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), + rc(ExprKind::Field( + rc(ExprKind::UnionType(kts.into_iter().collect())), + l, + )), + v, )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + 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), } } -- cgit v1.2.3 From a030560e60c4ff1c724216f4a5640722eb89b227 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 21:38:34 +0000 Subject: Use binder ids to reconstruct variables in expr output --- dhall/src/semantics/to_expr.rs | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/to_expr.rs') diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 11e289f..1ece1cc 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,9 +1,9 @@ -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; +use crate::semantics::core::context::VarCtx; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; +use crate::semantics::{Value, ValueKind}; use crate::syntax; -use crate::syntax::{Builtin, ExprKind}; +use crate::syntax::{Builtin, ExprKind, V}; /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -16,6 +16,7 @@ pub(crate) struct ToExprOptions { /// Converts a value back to the corresponding AST expression. pub(crate) fn value_to_expr( + ctx: &VarCtx, val: &Value, opts: ToExprOptions, ) -> NormalizedExpr { @@ -23,7 +24,27 @@ pub(crate) fn value_to_expr( val.normalize_whnf(); } - match val.as_kind().map_ref(|v| value_to_expr(v, opts)) { + let kind = val.as_kind(); + let kind = kind.map_ref_with_special_handling_of_binders( + |v| value_to_expr(ctx, v, opts), + |binder, v| value_to_expr(&ctx.insert(binder), v, opts), + ); + match kind { + ValueKind::Var(v) => { + let b = v.binder(); + let (idx, name) = if opts.alpha { + (ctx.lookup(&b), "_".into()) + } else { + (ctx.lookup_by_name(&b), b.name().clone()) + }; + match idx { + Some(idx) => rc(ExprKind::Var(V(name, idx))), + None => panic!( + "internal error: binder {:?} not found in environment", + b + ), + } + } ValueKind::Lam(x, t, e) => { rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) } @@ -33,7 +54,6 @@ pub(crate) fn value_to_expr( ValueKind::Pi(x, t, e) => { rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e)) } - ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), ValueKind::Const(c) => rc(ExprKind::Const(c)), ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)), ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)), -- cgit v1.2.3 From fc1d7b758008643447f17bc9d05adb128d1567cc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 10:25:28 +0000 Subject: Remove binder ids The underlying purpose of them turned out to be unsound --- dhall/src/semantics/to_expr.rs | 23 +++-------------------- 1 file changed, 3 insertions(+), 20 deletions(-) (limited to 'dhall/src/semantics/to_expr.rs') diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 1ece1cc..1adfd49 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,9 +1,8 @@ -use crate::semantics::core::context::VarCtx; 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}; +use crate::syntax::{Builtin, ExprKind}; /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -16,7 +15,6 @@ pub(crate) struct ToExprOptions { /// Converts a value back to the corresponding AST expression. pub(crate) fn value_to_expr( - ctx: &VarCtx, val: &Value, opts: ToExprOptions, ) -> NormalizedExpr { @@ -25,25 +23,10 @@ pub(crate) fn value_to_expr( } let kind = val.as_kind(); - let kind = kind.map_ref_with_special_handling_of_binders( - |v| value_to_expr(ctx, v, opts), - |binder, v| value_to_expr(&ctx.insert(binder), v, opts), - ); + let kind = kind.map_ref(|v| value_to_expr(v, opts)); match kind { ValueKind::Var(v) => { - let b = v.binder(); - let (idx, name) = if opts.alpha { - (ctx.lookup(&b), "_".into()) - } else { - (ctx.lookup_by_name(&b), b.name().clone()) - }; - match idx { - Some(idx) => rc(ExprKind::Var(V(name, idx))), - None => panic!( - "internal error: binder {:?} not found in environment", - b - ), - } + rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha))) } ValueKind::Lam(x, t, e) => { rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) -- cgit v1.2.3 From ab672506fd45e33f60b1b962c4757f912b6e27be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2020 18:31:45 +0000 Subject: Use alpha variables everywhere Don't bother keeping name around, it complicates matters --- dhall/src/semantics/to_expr.rs | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/to_expr.rs') diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 1adfd49..612f794 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,8 +1,9 @@ +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}; +use crate::syntax::{Builtin, ExprKind, V}; /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -14,19 +15,37 @@ pub(crate) struct ToExprOptions { } /// Converts a value back to the corresponding AST expression. -pub(crate) fn value_to_expr( - val: &Value, +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(|v| value_to_expr(v, opts)); + 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) => { - rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha))) + 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)) -- cgit v1.2.3 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/to_expr.rs | 101 ----------------------------------------- 1 file changed, 101 deletions(-) delete mode 100644 dhall/src/semantics/to_expr.rs (limited to 'dhall/src/semantics/to_expr.rs') 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), - } -} -- cgit v1.2.3