summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-01-19 18:30:13 +0000
committerNadrieril2020-01-19 18:30:13 +0000
commitaec80599f161096b68cac88ffb8852a61b62fcfa (patch)
tree945a87f97f062dcc7b0f4ec2f04dd8bc2da431ef /dhall/src/semantics
parent2f19fe1978c0fc8c456563c68ca08eb5b48ef0cd (diff)
Restore more types in value_to_tyexpr
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/value.rs77
-rw-r--r--dhall/src/semantics/core/visitor.rs14
-rw-r--r--dhall/src/semantics/phase/normalize.rs23
-rw-r--r--dhall/src/semantics/tck/mod.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs14
5 files changed, 93 insertions, 37 deletions
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<Value> {
RecordType(HashMap<Label, Value>),
RecordLit(HashMap<Label, Value>),
UnionType(HashMap<Label, Option<Value>>),
- UnionConstructor(Label, HashMap<Label, Option<Value>>),
- UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+ // Also keep the type of the uniontype around
+ UnionConstructor(Label, HashMap<Label, Option<Value>>, Type),
+ // Also keep the type of the uniontype and the constructor around
+ UnionLit(Label, Value, HashMap<Label, Option<Value>>, Type, Type),
// Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Value>>),
@@ -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<Value> {
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)))
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 541a196..f0a6a8c 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -374,9 +374,13 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args, ty)
}
- ValueKind::UnionConstructor(l, kts) => {
- ValueKind::UnionLit(l.clone(), a, kts.clone())
- }
+ ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
+ l.clone(),
+ a,
+ kts.clone(),
+ uniont.clone(),
+ f.get_type().unwrap(),
+ ),
_ => {
drop(f_borrow);
ValueKind::PartialExpr(ExprKind::App(f, a))
@@ -692,9 +696,11 @@ pub(crate) fn normalize_one_layer(
Ret::Expr(expr)
}
},
- UnionType(kts) => {
- Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
- }
+ UnionType(kts) => Ret::ValueKind(UnionConstructor(
+ l.clone(),
+ kts.clone(),
+ v.get_type().unwrap(),
+ )),
_ => {
drop(v_borrow);
Ret::Expr(expr)
@@ -710,7 +716,8 @@ pub(crate) fn normalize_one_layer(
let handlers_borrow = handlers.as_whnf();
let variant_borrow = variant.as_whnf();
match (&*handlers_borrow, &*variant_borrow) {
- (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
+ (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l)
+ {
Some(h) => Ret::Value(h.clone()),
None => {
drop(handlers_borrow);
@@ -718,7 +725,7 @@ pub(crate) fn normalize_one_layer(
Ret::Expr(expr)
}
},
- (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
+ (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) {
Some(h) => Ret::Value(h.app(v.clone())),
None => {
drop(handlers_borrow);
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 407605d..ba95847 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,2 +1,4 @@
+pub mod context;
pub mod tyexpr;
+pub mod typecheck;
pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index f0fcdd1..36cae04 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,6 @@
#![allow(dead_code)]
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::core::context::TyCtx;
use crate::semantics::core::var::AlphaVar;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::Normalized;
@@ -33,11 +35,21 @@ impl TyExpr {
pub fn kind(&self) -> &TyExprKind {
&*self.kind
}
+ pub fn get_type(&self) -> Result<Type, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t.clone()),
+ None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+ }
+ }
/// Converts a value back to the corresponding AST expression.
- pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+ pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
tyexpr_to_expr(self, opts, &mut Vec::new())
}
+ // TODO: temporary hack
+ pub fn to_value(&self) -> Value {
+ todo!()
+ }
}
fn tyexpr_to_expr<'a>(