summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
authorNadrieril2020-01-24 16:29:25 +0000
committerNadrieril2020-01-24 16:29:25 +0000
commitbd1eb36503aa6e03532fefcfd0c4f27eb62c99d2 (patch)
tree7af22057fb7938648a5bf527768218e565d5170f /dhall/src/semantics/phase
parentfccccac6463cb3ca91206d5c41bbf51fc2ec4e0f (diff)
Restore all types in Value::to_tyexpr
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/normalize.rs18
-rw-r--r--dhall/src/semantics/phase/typecheck.rs12
2 files changed, 20 insertions, 10 deletions
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);