summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/phase/normalize.rs19
-rw-r--r--dhall/src/semantics/phase/typecheck.rs101
-rw-r--r--dhall/src/semantics/tck/typecheck.rs239
3 files changed, 301 insertions, 58 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 7f547d7..33e1f2b 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -595,8 +595,23 @@ fn apply_binop<'a>(
Ret::ValueKind(RecordLit(kvs))
}
- (RecursiveRecordTypeMerge, _, _) => {
- unreachable!("This case should have been handled in typecheck")
+ (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
+ let kts = merge_maps::<_, _, _, !>(
+ kts_x,
+ kts_y,
+ // If the Label exists for both records, then we hit the recursive case.
+ |_, l: &Value, r: &Value| {
+ Ok(Value::from_kind_and_type(
+ ValueKind::PartialExpr(ExprKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ )),
+ ty.clone(),
+ ))
+ },
+ )?;
+ Ret::ValueKind(RecordType(kts))
}
(Equivalence, _, _) => {
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 44678cd..1aab736 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -356,7 +356,6 @@ fn type_last_layer(
use syntax::BinOp::*;
use syntax::Builtin::*;
use syntax::Const::Type;
- use syntax::ExprKind::*;
let mkerr =
|msg: &str| Err(TypeError::new(TypeMessage::Custom(msg.to_string())));
@@ -370,13 +369,15 @@ fn type_last_layer(
use Ret::*;
let ret = match &e {
- Import(_) => unreachable!(
+ ExprKind::Import(_) => unreachable!(
"There should remain no imports in a resolved expression"
),
- Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
- unreachable!()
- }
- App(f, a) => {
+ ExprKind::Lam(_, _, _)
+ | ExprKind::Pi(_, _, _)
+ | ExprKind::Let(_, _, _, _)
+ | ExprKind::Embed(_)
+ | ExprKind::Var(_) => unreachable!(),
+ ExprKind::App(f, a) => {
let tf = f.get_type()?;
let tf_borrow = tf.as_whnf();
let (tx, tb) = match &*tf_borrow {
@@ -391,13 +392,13 @@ fn type_last_layer(
ret.normalize_nf();
RetTypeOnly(ret)
}
- Annot(x, t) => {
+ ExprKind::Annot(x, t) => {
if &x.get_type()? != t {
return mkerr("AnnotMismatch");
}
RetWhole(x.clone())
}
- Assert(t) => {
+ ExprKind::Assert(t) => {
match &*t.as_whnf() {
ValueKind::Equivalence(x, y) if x == y => {}
ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
@@ -405,16 +406,16 @@ fn type_last_layer(
}
RetTypeOnly(t.clone())
}
- BoolIf(x, y, z) => {
+ ExprKind::BoolIf(x, y, z) => {
if *x.get_type()?.as_whnf() != ValueKind::from_builtin(Bool) {
return mkerr("InvalidPredicate");
}
- if y.get_type()?.get_type()?.as_const() != Some(Type) {
+ if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
return mkerr("IfBranchMustBeTerm");
}
- if z.get_type()?.get_type()?.as_const() != Some(Type) {
+ if z.get_type()?.get_type()?.as_const() != Some(Const::Type) {
return mkerr("IfBranchMustBeTerm");
}
@@ -424,7 +425,7 @@ fn type_last_layer(
RetTypeOnly(y.get_type()?)
}
- EmptyListLit(t) => {
+ ExprKind::EmptyListLit(t) => {
let arg = match &*t.as_whnf() {
ValueKind::AppliedBuiltin(syntax::Builtin::List, args, _)
if args.len() == 1 =>
@@ -438,7 +439,7 @@ fn type_last_layer(
t.clone(),
))
}
- NEListLit(xs) => {
+ ExprKind::NEListLit(xs) => {
let mut iter = xs.iter().enumerate();
let (_, x) = iter.next().unwrap();
for (_, y) in iter {
@@ -447,30 +448,30 @@ fn type_last_layer(
}
}
let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Type) {
+ if t.get_type()?.as_const() != Some(Const::Type) {
return mkerr("InvalidListType");
}
RetTypeOnly(Value::from_builtin(syntax::Builtin::List).app(t))
}
- SomeLit(x) => {
+ ExprKind::SomeLit(x) => {
let t = x.get_type()?;
- if t.get_type()?.as_const() != Some(Type) {
+ if t.get_type()?.as_const() != Some(Const::Type) {
return mkerr("InvalidOptionalType");
}
RetTypeOnly(Value::from_builtin(syntax::Builtin::Optional).app(t))
}
- RecordType(kts) => RetWhole(tck_record_type(
+ ExprKind::RecordType(kts) => RetWhole(tck_record_type(
kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
)?),
- UnionType(kts) => RetWhole(tck_union_type(
+ ExprKind::UnionType(kts) => RetWhole(tck_union_type(
kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
)?),
- RecordLit(kvs) => RetTypeOnly(tck_record_type(
+ ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
)?),
- Field(r, x) => {
+ ExprKind::Field(r, x) => {
match &*r.get_type()?.as_whnf() {
ValueKind::RecordType(kts) => match kts.get(&x) {
Some(tth) => RetTypeOnly(tth.clone()),
@@ -494,13 +495,13 @@ fn type_last_layer(
} // _ => mkerr("NotARecord"),
}
}
- Const(c) => RetWhole(const_to_value(*c)),
- Builtin(b) => RetWhole(builtin_to_value(*b)),
- BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
- NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
- IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
- DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
- TextLit(interpolated) => {
+ ExprKind::Const(c) => RetWhole(const_to_value(*c)),
+ ExprKind::Builtin(b) => RetWhole(builtin_to_value(*b)),
+ ExprKind::BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
+ ExprKind::NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
+ ExprKind::IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
+ ExprKind::DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
+ ExprKind::TextLit(interpolated) => {
let text_type = builtin_to_value(Text);
for contents in interpolated.iter() {
use InterpolatedTextContents::Expr;
@@ -512,7 +513,7 @@ fn type_last_layer(
}
RetTypeOnly(text_type)
}
- BinOp(RightBiasedRecordMerge, l, r) => {
+ ExprKind::BinOp(RightBiasedRecordMerge, l, r) => {
let l_type = l.get_type()?;
let r_type = r.get_type()?;
@@ -541,16 +542,18 @@ fn type_last_layer(
kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
)?)
}
- BinOp(RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
- ctx,
- ExprKind::BinOp(
- RecursiveRecordTypeMerge,
- l.get_type()?,
- r.get_type()?,
- ),
- Span::Artificial,
- )?),
- BinOp(RecursiveRecordTypeMerge, l, r) => {
+ ExprKind::BinOp(RecursiveRecordMerge, l, r) => {
+ RetTypeOnly(type_last_layer(
+ ctx,
+ ExprKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.get_type()?,
+ r.get_type()?,
+ ),
+ Span::Artificial,
+ )?)
+ }
+ ExprKind::BinOp(RecursiveRecordTypeMerge, l, r) => {
// Extract the LHS record type
let borrow_l = l.as_whnf();
let kts_x = match &*borrow_l {
@@ -585,7 +588,7 @@ fn type_last_layer(
RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
}
- BinOp(ListAppend, l, r) => {
+ ExprKind::BinOp(ListAppend, l, r) => {
match &*l.get_type()?.as_whnf() {
ValueKind::AppliedBuiltin(List, _, _) => {}
_ => return mkerr("BinOpTypeMismatch"),
@@ -597,11 +600,11 @@ fn type_last_layer(
RetTypeOnly(l.get_type()?)
}
- BinOp(Equivalence, l, r) => {
- if l.get_type()?.get_type()?.as_const() != Some(Type) {
+ ExprKind::BinOp(Equivalence, l, r) => {
+ if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
return mkerr("EquivalenceArgumentMustBeTerm");
}
- if r.get_type()?.get_type()?.as_const() != Some(Type) {
+ if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
return mkerr("EquivalenceArgumentMustBeTerm");
}
@@ -614,7 +617,7 @@ fn type_last_layer(
Value::from_const(Type),
))
}
- BinOp(o, l, r) => {
+ ExprKind::BinOp(o, l, r) => {
let t = builtin_to_value(match o {
BoolAnd => Bool,
BoolOr => Bool,
@@ -641,7 +644,7 @@ fn type_last_layer(
RetTypeOnly(t)
}
- Merge(record, union, type_annot) => {
+ ExprKind::Merge(record, union, type_annot) => {
let record_type = record.get_type()?;
let record_borrow = record_type.as_whnf();
let handlers = match &*record_borrow {
@@ -723,8 +726,8 @@ fn type_last_layer(
(None, None) => return mkerr("MergeEmptyNeedsAnnotation"),
}
}
- ToMap(_, _) => unimplemented!("toMap"),
- Projection(record, labels) => {
+ ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+ ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
let record_type_borrow = record_type.as_whnf();
let kts = match &*record_type_borrow {
@@ -753,8 +756,10 @@ fn type_last_layer(
record_type.get_type()?,
))
}
- ProjectionByExpr(_, _) => unimplemented!("selection by expression"),
- Completion(_, _) => unimplemented!("record completion"),
+ ExprKind::ProjectionByExpr(_, _) => {
+ unimplemented!("selection by expression")
+ }
+ ExprKind::Completion(_, _) => unimplemented!("record completion"),
};
Ok(match ret {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 52c7ac7..1687185 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -19,8 +19,8 @@ use crate::semantics::{
};
use crate::syntax;
use crate::syntax::{
- Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span,
- UnspannedExpr, V,
+ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
+ Span, UnspannedExpr, V,
};
#[derive(Debug, Clone)]
@@ -46,7 +46,7 @@ impl TyEnv {
&self.names
}
- pub fn insert_type(&self, x: &Label, t: Value) -> Self {
+ pub fn insert_type(&self, x: &Label, t: Type) -> Self {
TyEnv {
names: self.names.insert(x),
items: self.items.insert_type(t),
@@ -58,7 +58,7 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Value)> {
+ pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
let var = self.names.unlabel_var(var)?;
let ty = self.items.lookup_val(&var).get_type().unwrap();
Some((TyExprKind::Var(var), ty))
@@ -72,10 +72,10 @@ fn mkerr<T>(x: impl ToString) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
-fn type_last_layer(
+fn type_one_layer(
env: &TyEnv,
kind: &ExprKind<TyExpr, Normalized>,
-) -> Result<Value, TypeError> {
+) -> Result<Type, TypeError> {
Ok(match &kind {
ExprKind::Import(..) => unreachable!(
"There should remain no imports in a resolved expression"
@@ -85,7 +85,7 @@ fn type_last_layer(
| ExprKind::Pi(..)
| ExprKind::Let(..)
| ExprKind::Const(Const::Sort)
- | ExprKind::Embed(..) => unreachable!(),
+ | ExprKind::Embed(..) => unreachable!(), // Handled in type_with
ExprKind::Const(Const::Type) => const_to_value(Const::Kind),
ExprKind::Const(Const::Kind) => const_to_value(Const::Sort),
@@ -96,7 +96,99 @@ fn type_last_layer(
ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural),
ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer),
ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double),
+ ExprKind::TextLit(interpolated) => {
+ let text_type = builtin_to_value(Builtin::Text);
+ for contents in interpolated.iter() {
+ use InterpolatedTextContents::Expr;
+ if let Expr(x) = contents {
+ if x.get_type()? != text_type {
+ return mkerr("InvalidTextInterpolation");
+ }
+ }
+ }
+ text_type
+ }
+
+ // ExprKind::EmptyListLit(t) => {
+ // let arg = match &*t.as_whnf() {
+ // ValueKind::AppliedBuiltin(Builtin::List, args, _)
+ // if args.len() == 1 =>
+ // {
+ // args[0].clone()
+ // }
+ // _ => return mkerr("InvalidListType"),
+ // };
+ // RetWhole(Value::from_kind_and_type(
+ // ValueKind::EmptyListLit(arg),
+ // t.clone(),
+ // ))
+ // }
+ ExprKind::NEListLit(xs) => {
+ let mut iter = xs.iter().enumerate();
+ let (_, x) = iter.next().unwrap();
+ for (i, y) in iter {
+ if x.get_type()? != y.get_type()? {
+ return mkerr("InvalidListElement");
+ }
+ }
+ let t = x.get_type()?;
+ if t.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("InvalidListType");
+ }
+
+ Value::from_builtin(Builtin::List).app(t)
+ }
+ ExprKind::SomeLit(x) => {
+ let t = x.get_type()?;
+ if t.get_type()?.as_const() != Some(Const::Type) {
+ return mkerr("InvalidOptionalType");
+ }
+ Value::from_builtin(Builtin::Optional).app(t)
+ }
+ // ExprKind::RecordType(kts) => RetWhole(tck_record_type(
+ // kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+ // )?),
+ // ExprKind::UnionType(kts) => RetWhole(tck_union_type(
+ // kts.iter().map(|(x, t)| Ok((x.clone(), t.clone()))),
+ // )?),
+ // ExprKind::RecordLit(kvs) => RetTypeOnly(tck_record_type(
+ // kvs.iter().map(|(x, v)| Ok((x.clone(), v.get_type()?))),
+ // )?),
+ ExprKind::Field(r, x) => {
+ match &*r.get_type()?.as_whnf() {
+ ValueKind::RecordType(kts) => match kts.get(&x) {
+ Some(tth) => tth.clone(),
+ None => return mkerr("MissingRecordField"),
+ },
+ // TODO: branch here only when r.get_type() is a Const
+ _ => {
+ let r_nf = r.normalize_whnf(env.as_nzenv());
+ let r_nf_borrow = r_nf.as_whnf();
+ match &*r_nf_borrow {
+ ValueKind::UnionType(kts) => match kts.get(x) {
+ // Constructor has type T -> < x: T, ... >
+ // TODO: check pi type properly
+ Some(Some(t)) => Value::from_kind_and_type(
+ ValueKind::PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: t.clone(),
+ closure: Closure::new(
+ t.clone(),
+ env.as_nzenv(),
+ r.clone(),
+ ),
+ },
+ Value::from_const(Const::Type),
+ ),
+ Some(None) => r_nf.clone(),
+ None => return mkerr("MissingUnionField"),
+ },
+ _ => return mkerr("NotARecord"),
+ }
+ } // _ => mkerr("NotARecord"),
+ }
+ }
ExprKind::Annot(x, t) => {
if x.get_type()? != t.normalize_whnf(env.as_nzenv()) {
return mkerr("annot mismatch");
@@ -139,7 +231,138 @@ fn type_last_layer(
y.get_type()?
}
+ // ExprKind::BinOp(BinOp::RightBiasedRecordMerge, l, r) => {
+ // let l_type = l.get_type()?;
+ // let r_type = r.get_type()?;
+
+ // // Extract the LHS record type
+ // let l_type_borrow = l_type.as_whnf();
+ // let kts_x = match &*l_type_borrow {
+ // ValueKind::RecordType(kts) => kts,
+ // _ => return mkerr("MustCombineRecord"),
+ // };
+
+ // // Extract the RHS record type
+ // let r_type_borrow = r_type.as_whnf();
+ // let kts_y = match &*r_type_borrow {
+ // ValueKind::RecordType(kts) => kts,
+ // _ => return mkerr("MustCombineRecord"),
+ // };
+ // // Union the two records, prefering
+ // // the values found in the RHS.
+ // let kts = merge_maps::<_, _, _, !>(kts_x, kts_y, |_, _, r_t| {
+ // Ok(r_t.clone())
+ // })?;
+
+ // // Construct the final record type from the union
+ // RetTypeOnly(tck_record_type(
+ // kts.into_iter().map(|(x, v)| Ok((x.clone(), v))),
+ // )?)
+ // }
+ // ExprKind::BinOp(BinOp::RecursiveRecordMerge, l, r) => RetTypeOnly(type_last_layer(
+ // ctx,
+ // ExprKind::BinOp(
+ // RecursiveRecordTypeMerge,
+ // l.get_type()?,
+ // r.get_type()?,
+ // ),
+ // Span::Artificial,
+ // )?),
+ // ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, l, r) => {
+ // // Extract the LHS record type
+ // let borrow_l = l.as_whnf();
+ // let kts_x = match &*borrow_l {
+ // ValueKind::RecordType(kts) => kts,
+ // _ => {
+ // return mkerr("RecordTypeMergeRequiresRecordType")
+ // }
+ // };
+
+ // // Extract the RHS record type
+ // let borrow_r = r.as_whnf();
+ // let kts_y = match &*borrow_r {
+ // ValueKind::RecordType(kts) => kts,
+ // _ => {
+ // return mkerr("RecordTypeMergeRequiresRecordType")
+ // }
+ // };
+
+ // // Ensure that the records combine without a type error
+ // let kts = merge_maps(
+ // kts_x,
+ // kts_y,
+ // // If the Label exists for both records, then we hit the recursive case.
+ // |_, l: &Value, r: &Value| {
+ // type_last_layer(
+ // ctx,
+ // ExprKind::BinOp(
+ // RecursiveRecordTypeMerge,
+ // l.clone(),
+ // r.clone(),
+ // ),
+ // Span::Artificial,
+ // )
+ // },
+ // )?;
+
+ // RetWhole(tck_record_type(kts.into_iter().map(Ok))?)
+ // }
+ // ExprKind::BinOp(o @ BinOp::ListAppend, l, r) => {
+ // match &*l.get_type()?.as_whnf() {
+ // ValueKind::AppliedBuiltin(List, _, _) => {}
+ // _ => return mkerr("BinOpTypeMismatch"),
+ // }
+
+ // if l.get_type()? != r.get_type()? {
+ // return mkerr("BinOpTypeMismatch");
+ // }
+
+ // l.get_type()?
+ // }
+ // ExprKind::BinOp(BinOp::Equivalence, l, r) => {
+ // if l.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ // return mkerr("EquivalenceArgumentMustBeTerm");
+ // }
+ // if r.get_type()?.get_type()?.as_const() != Some(Const::Type) {
+ // return mkerr("EquivalenceArgumentMustBeTerm");
+ // }
+
+ // if l.get_type()? != r.get_type()? {
+ // return mkerr("EquivalenceTypeMismatch");
+ // }
+
+ // RetWhole(Value::from_kind_and_type(
+ // ValueKind::Equivalence(l.clone(), r.clone()),
+ // Value::from_const(Type),
+ // ))
+ // }
+ ExprKind::BinOp(o, l, r) => {
+ let t = builtin_to_value(match o {
+ BinOp::BoolAnd
+ | BinOp::BoolOr
+ | BinOp::BoolEQ
+ | BinOp::BoolNE => Builtin::Bool,
+ BinOp::NaturalPlus | BinOp::NaturalTimes => Builtin::Natural,
+ BinOp::TextAppend => Builtin::Text,
+ BinOp::ListAppend
+ | BinOp::RightBiasedRecordMerge
+ | BinOp::RecursiveRecordMerge
+ | BinOp::RecursiveRecordTypeMerge
+ | BinOp::Equivalence => unreachable!(),
+ BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
+ });
+
+ if l.get_type()? != t {
+ return mkerr("BinOpTypeMismatch");
+ }
+
+ if r.get_type()? != t {
+ return mkerr("BinOpTypeMismatch");
+ }
+
+ t
+ }
_ => Value::from_const(Const::Type), // TODO
})
}
@@ -216,7 +439,7 @@ fn type_with(
}
ekind => {
let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
- let ty = type_last_layer(env, &ekind)?;
+ let ty = type_one_layer(env, &ekind)?;
(TyExprKind::Expr(ekind), Some(ty))
}
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 16:15:25 +0000