summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs239
1 files changed, 231 insertions, 8 deletions
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 01:21:43 +0000