From aec80599f161096b68cac88ffb8852a61b62fcfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 19 Jan 2020 18:30:13 +0000 Subject: Restore more types in value_to_tyexpr --- dhall/src/semantics/core/value.rs | 77 ++++++++++++++++++++++++++----------- dhall/src/semantics/core/visitor.rs | 14 ++++--- 2 files changed, 63 insertions(+), 28 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7086616..f470019 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -10,7 +10,7 @@ use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ Normalized, NormalizedExpr, ToExprOptions, Typed, }; -use crate::semantics::{TyExpr, TyExprKind}; +use crate::semantics::{TyExpr, TyExprKind, Type}; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, Span, @@ -75,8 +75,10 @@ pub(crate) enum ValueKind { RecordType(HashMap), RecordLit(HashMap), UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), + // Also keep the type of the uniontype around + UnionConstructor(Label, HashMap>, Type), + // Also keep the type of the uniontype and the constructor around + UnionLit(Label, Value, HashMap>, Type, Type), // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), @@ -296,28 +298,40 @@ impl Value { } // TODO: properly recover intermediate types; `None` is a time-bomb here. - let rc = - |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial); - let self_kind = self_kind.map_ref(|v| v.to_tyexpr()); 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(rc(acc), v)), + 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(rc(ExprKind::Builtin(Builtin::OptionalNone)), n) - } + ValueKind::EmptyOptionalLit(n) => ExprKind::App( + builtin_to_value(Builtin::OptionalNone).to_tyexpr(), + n, + ), ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), - ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc( - ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n), + ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( + TyExprKind::Expr(ExprKind::App( + builtin_to_value(Builtin::List).to_tyexpr(), + n, + )), + Some(const_to_value(Const::Type)), + Span::Artificial, )), ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts), ValueKind::RecordLit(kvs) => { @@ -329,15 +343,31 @@ impl Value { ValueKind::UnionType(kts) => { ExprKind::UnionType(kts.into_iter().collect()) } - ValueKind::UnionConstructor(l, kts) => ExprKind::Field( - rc(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) => ExprKind::App( - rc(ExprKind::Field( - rc(ExprKind::UnionType(kts.into_iter().collect())), - 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) => { @@ -483,12 +513,13 @@ impl ValueKind { x.normalize_mut(); } } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + ValueKind::UnionType(kts) + | ValueKind::UnionConstructor(_, kts, _) => { for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - ValueKind::UnionLit(_, v, kts) => { + ValueKind::UnionLit(_, v, kts, _, _) => { v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index e61a649..a449f6c 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -94,12 +94,16 @@ 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) => { - UnionConstructor(l.clone(), v.visit_optmap(kts)?) - } - UnionLit(l, t, kts) => { - UnionLit(l.clone(), v.visit_val(t)?, v.visit_optmap(kts)?) + UnionConstructor(l, kts, t) => { + UnionConstructor(l.clone(), v.visit_optmap(kts)?, t.clone()) } + UnionLit(l, x, kts, uniont, ctort) => UnionLit( + l.clone(), + v.visit_val(x)?, + v.visit_optmap(kts)?, + uniont.clone(), + ctort.clone(), + ), TextLit(ts) => TextLit( ts.iter() .map(|t| t.traverse_ref(|e| v.visit_val(e))) -- cgit v1.2.3