From bd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 16:29:25 +0000 Subject: Restore all types in Value::to_tyexpr --- dhall/src/semantics/core/value.rs | 119 ++++++++++++++++++++------------- dhall/src/semantics/core/visitor.rs | 16 +++-- dhall/src/semantics/phase/normalize.rs | 18 +++-- dhall/src/semantics/phase/typecheck.rs | 12 ++-- 4 files changed, 101 insertions(+), 64 deletions(-) diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 8beed24..3798053 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -75,7 +75,8 @@ pub(crate) enum ValueKind { closure: Closure, }, // Invariant: in whnf, the evaluation must not be able to progress further. - AppliedBuiltin(Builtin, Vec), + // Keep types around to be able to recover the types of partial applications. + AppliedBuiltin(Builtin, Vec, Vec), Var(AlphaVar, NzVar), Const(Const), @@ -92,9 +93,9 @@ pub(crate) enum ValueKind { RecordLit(HashMap), UnionType(HashMap>), // Also keep the type of the uniontype around - UnionConstructor(Label, HashMap>, Type), + UnionConstructor(Label, HashMap>, Value), // Also keep the type of the uniontype and the constructor around - UnionLit(Label, Value, HashMap>, Type, Type), + UnionLit(Label, Value, HashMap>, Value, Value), // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), @@ -309,8 +310,68 @@ impl Value { annot.to_tyexpr(qenv), closure.apply_ty(annot.clone()).to_tyexpr(qenv.insert()), )), + ValueKind::AppliedBuiltin(b, args, types) => { + TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold( + ExprKind::Builtin(*b), + |acc, (v, ty)| { + ExprKind::App( + TyExpr::new( + TyExprKind::Expr(acc), + Some(ty.clone()), + Span::Artificial, + ), + v.to_tyexpr(qenv), + ) + }, + )) + } + ValueKind::UnionConstructor(l, kts, t) => { + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| v.to_tyexpr(qenv)), + ) + }) + .collect(), + )), + Some(t.clone()), + Span::Artificial, + ), + l.clone(), + )) + } + ValueKind::UnionLit(l, v, kts, uniont, ctort) => { + TyExprKind::Expr(ExprKind::App( + TyExpr::new( + TyExprKind::Expr(ExprKind::Field( + TyExpr::new( + TyExprKind::Expr(ExprKind::UnionType( + kts.into_iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref() + .map(|v| v.to_tyexpr(qenv)), + ) + }) + .collect(), + )), + Some(uniont.clone()), + Span::Artificial, + ), + l.clone(), + )), + Some(ctort.clone()), + Span::Artificial, + ), + v.to_tyexpr(qenv), + )) + } 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), @@ -319,23 +380,14 @@ impl Value { let expr = match self_kind { ValueKind::Var(..) | ValueKind::LamClosure { .. } - | ValueKind::PiClosure { .. } => unreachable!(), + | ValueKind::PiClosure { .. } + | ValueKind::AppliedBuiltin(..) + | ValueKind::UnionConstructor(..) + | ValueKind::UnionLit(..) => 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), @@ -366,35 +418,6 @@ impl Value { 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( - 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()) } @@ -530,7 +553,7 @@ impl ValueKind { | ValueKind::PiClosure { annot, .. } => { annot.normalize_mut(); } - ValueKind::AppliedBuiltin(_, args) => { + ValueKind::AppliedBuiltin(_, args, _) => { for x in args.iter_mut() { x.normalize_mut(); } @@ -578,7 +601,7 @@ impl ValueKind { } pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![]) + ValueKind::AppliedBuiltin(b, vec![], vec![]) } fn shift(&self, delta: isize, var: &AlphaVar) -> Option { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index ee44ed7..64250b0 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -98,7 +98,9 @@ where annot: v.visit_val(annot)?, closure: closure.clone(), }, - AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), + AppliedBuiltin(b, xs, types) => { + AppliedBuiltin(*b, v.visit_vec(xs)?, v.visit_vec(types)?) + } Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), @@ -112,15 +114,17 @@ where RecordType(kts) => RecordType(v.visit_map(kts)?), RecordLit(kvs) => RecordLit(v.visit_map(kvs)?), UnionType(kts) => UnionType(v.visit_optmap(kts)?), - UnionConstructor(l, kts, t) => { - UnionConstructor(l.clone(), v.visit_optmap(kts)?, t.clone()) - } + UnionConstructor(l, kts, uniont) => UnionConstructor( + l.clone(), + v.visit_optmap(kts)?, + v.visit_val(uniont)?, + ), UnionLit(l, x, kts, uniont, ctort) => UnionLit( l.clone(), v.visit_val(x)?, v.visit_optmap(kts)?, - uniont.clone(), - ctort.clone(), + v.visit_val(uniont)?, + v.visit_val(ctort)?, ), TextLit(ts) => TextLit( ts.iter() diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index 75d61d5..8f3953d 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -71,6 +71,7 @@ pub(crate) fn apply_builtin( b: Builtin, args: Vec, ty: &Value, + types: Vec, ) -> ValueKind { use syntax::Builtin::*; use ValueKind::*; @@ -364,7 +365,7 @@ pub(crate) fn apply_builtin( } v.to_whnf_check_type(ty) } - Ret::DoneAsIs => AppliedBuiltin(b, args), + Ret::DoneAsIs => AppliedBuiltin(b, args, types), } } @@ -377,10 +378,15 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind { ValueKind::LamClosure { closure, .. } => { closure.apply(a).to_whnf_check_type(ty) } - ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(b, args, types) => { use std::iter::once; let args = args.iter().cloned().chain(once(a.clone())).collect(); - apply_builtin(*b, args, ty) + let types = types + .iter() + .cloned() + .chain(once(f.get_type().unwrap())) + .collect(); + apply_builtin(*b, args, ty, types) } ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit( l.clone(), @@ -631,7 +637,7 @@ pub(crate) fn normalize_one_layer( ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)), ExprKind::EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => { args[0].clone() @@ -806,7 +812,9 @@ pub(crate) fn normalize_whnf( ty: &Value, ) -> ValueKind { match v { - ValueKind::AppliedBuiltin(b, args) => apply_builtin(b, args, ty), + ValueKind::AppliedBuiltin(b, args, types) => { + apply_builtin(b, args, ty, types) + } ValueKind::PartialExpr(e) => normalize_one_layer(e, ty), ValueKind::TextLit(elts) => { ValueKind::TextLit(squash_textlit(elts.into_iter())) diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs index 9e41f1e..f2d1bf2 100644 --- a/dhall/src/semantics/phase/typecheck.rs +++ b/dhall/src/semantics/phase/typecheck.rs @@ -421,7 +421,7 @@ fn type_last_layer( } EmptyListLit(t) => { let arg = match &*t.as_whnf() { - ValueKind::AppliedBuiltin(syntax::Builtin::List, args) + ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _) if args.len() == 1 => { args[0].clone() @@ -613,7 +613,7 @@ fn type_last_layer( } BinOp(o @ ListAppend, l, r) => { match &*l.get_type()?.as_whnf() { - ValueKind::AppliedBuiltin(List, _) => {} + ValueKind::AppliedBuiltin(List, _, _) => {} _ => return mkerr(BinOpTypeMismatch(*o, l.clone())), } @@ -679,9 +679,11 @@ fn type_last_layer( let union_borrow = union_type.as_whnf(); let variants = match &*union_borrow { ValueKind::UnionType(kts) => Cow::Borrowed(kts), - ValueKind::AppliedBuiltin(syntax::Builtin::Optional, args) - if args.len() == 1 => - { + ValueKind::AppliedBuiltin( + syntax::Builtin::Optional, + args, + _, + ) if args.len() == 1 => { let ty = &args[0]; let mut kts = HashMap::new(); kts.insert("None".into(), None); -- cgit v1.2.3