summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/value.rs119
-rw-r--r--dhall/src/semantics/core/visitor.rs16
-rw-r--r--dhall/src/semantics/phase/normalize.rs18
-rw-r--r--dhall/src/semantics/phase/typecheck.rs12
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<Value> {
closure: Closure,
},
// Invariant: in whnf, the evaluation must not be able to progress further.
- AppliedBuiltin(Builtin, Vec<Value>),
+ // Keep types around to be able to recover the types of partial applications.
+ AppliedBuiltin(Builtin, Vec<Value>, Vec<Value>),
Var(AlphaVar, NzVar),
Const(Const),
@@ -92,9 +93,9 @@ pub(crate) enum ValueKind<Value> {
RecordLit(HashMap<Label, Value>),
UnionType(HashMap<Label, Option<Value>>),
// Also keep the type of the uniontype around
- UnionConstructor(Label, HashMap<Label, Option<Value>>, Type),
+ UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
// Also keep the type of the uniontype and the constructor around
- UnionLit(Label, Value, HashMap<Label, Option<Value>>, Type, Type),
+ UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
// Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
// contiguous text values must be merged.
TextLit(Vec<InterpolatedTextContents<Value>>),
@@ -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<Value> {
| 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<Value> {
}
pub(crate) fn from_builtin(b: Builtin) -> ValueKind<Value> {
- ValueKind::AppliedBuiltin(b, vec![])
+ ValueKind::AppliedBuiltin(b, vec![], vec![])
}
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
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<Value>,
ty: &Value,
+ types: Vec<Value>,
) -> ValueKind<Value> {
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<Value> {
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<Value> {
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);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 04:24:31 +0000