diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 19 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/typecheck.rs | 101 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 239 |
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)) } }; |