diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/phase/typecheck.rs | 87 |
1 files changed, 28 insertions, 59 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index bfe85b9..b163af6 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -35,19 +35,19 @@ macro_rules! ensure_simple_type { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum TypeIntermediate { - Pi(TypecheckContext, Label, Type, Type), - RecordType(TypecheckContext, BTreeMap<Label, Type>), - UnionType(TypecheckContext, BTreeMap<Label, Option<Type>>), - ListType(TypecheckContext, Type), - OptionalType(TypecheckContext, Type), + Pi(Label, Type, Type), + RecordType(BTreeMap<Label, Type>), + UnionType(BTreeMap<Label, Option<Type>>), + ListType(Type), + OptionalType(Type), } impl TypeIntermediate { - fn typecheck(self) -> Result<Typed, TypeError> { + fn typecheck(self, ctx: &TypecheckContext) -> Result<Typed, TypeError> { use crate::error::TypeMessage::*; - let mkerr = |ctx, msg| TypeError::new(ctx, msg); + let mkerr = |ctx: &TypecheckContext, msg| TypeError::new(ctx, msg); Ok(match &self { - TypeIntermediate::Pi(ctx, x, ta, tb) => { + TypeIntermediate::Pi(x, ta, tb) => { let ctx2 = ctx.insert_type(x, ta.clone()); let kA = match ta.get_type()?.as_const() { @@ -101,7 +101,7 @@ impl TypeIntermediate { Type::from_const(k), ) } - TypeIntermediate::RecordType(ctx, kts) => { + TypeIntermediate::RecordType(kts) => { // Check that all types are the same const let mut k = None; for (x, t) in kts { @@ -131,7 +131,7 @@ impl TypeIntermediate { Type::from_const(k), ) } - TypeIntermediate::UnionType(ctx, kts) => { + TypeIntermediate::UnionType(kts) => { // Check that all types are the same const let mut k = None; for (x, t) in kts { @@ -170,7 +170,7 @@ impl TypeIntermediate { Type::from_const(k), ) } - TypeIntermediate::ListType(ctx, t) => { + TypeIntermediate::ListType(t) => { ensure_simple_type!( t, mkerr(ctx, InvalidListType(t.clone().to_normalized())), @@ -182,7 +182,7 @@ impl TypeIntermediate { Type::from_const(Const::Type), ) } - TypeIntermediate::OptionalType(ctx, t) => { + TypeIntermediate::OptionalType(t) => { ensure_simple_type!( t, mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())), @@ -337,6 +337,7 @@ enum Ret { RetTyped(Typed), /// Use the contained Type as the type of the input expression RetType(Type), + RetTypeIntermediate(TypeIntermediate), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -356,20 +357,13 @@ fn type_with( let ctx2 = ctx.insert_type(x, tx.clone()); let b = type_with(&ctx2, b.clone())?; let tb = b.get_type()?.into_owned(); - Ok(RetType( - TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::Pi(x.clone(), tx, tb))) } Pi(x, ta, tb) => { let ta = mktype(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); let tb = mktype(&ctx2, tb.clone())?; - Ok(RetTyped( - TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb) - .typecheck()?, - )) + return TypeIntermediate::Pi(x.clone(), ta, tb).typecheck(ctx); } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -379,9 +373,7 @@ fn type_with( }; let v = type_with(ctx, v)?; - let e = type_with(&ctx.insert_value(x, v.clone())?, e.clone())?; - - Ok(RetType(e.get_type()?.into_owned())) + return type_with(&ctx.insert_value(x, v.clone())?, e.clone()); } OldOptionalLit(None, t) => { let none = SubExpr::from_expr_no_note(ExprF::Builtin( @@ -411,6 +403,10 @@ fn type_with( Thunk::new(ctx.to_normalization_ctx(), e), typ, ), + RetTypeIntermediate(ti) => Typed::from_thunk_and_type( + Thunk::new(ctx.to_normalization_ctx(), e), + ti.typecheck(ctx)?.to_type(), + ), RetTyped(tt) => tt, }) } @@ -493,11 +489,7 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.to_type(); - Ok(RetType( - TypeIntermediate::ListType(ctx.clone(), t) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::ListType(t))) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); @@ -514,28 +506,18 @@ fn type_last_layer( ); } let t = x.get_type()?.into_owned(); - Ok(RetType( - TypeIntermediate::ListType(ctx.clone(), t) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::ListType(t))) } SomeLit(x) => { let t = x.get_type()?.into_owned(); - Ok(RetType( - TypeIntermediate::OptionalType(ctx.clone(), t) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::OptionalType(t))) } RecordType(kts) => { let kts: BTreeMap<_, _> = kts .into_iter() .map(|(x, t)| Ok((x, t.to_type()))) .collect::<Result<_, _>>()?; - Ok(RetTyped( - TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?, - )) + Ok(RetTyped(TypeIntermediate::RecordType(kts).typecheck(ctx)?)) } UnionType(kts) => { let kts: BTreeMap<_, _> = kts @@ -550,20 +532,14 @@ fn type_last_layer( )) }) .collect::<Result<_, _>>()?; - Ok(RetTyped( - TypeIntermediate::UnionType(ctx.clone(), kts).typecheck()?, - )) + Ok(RetTyped(TypeIntermediate::UnionType(kts).typecheck(ctx)?)) } RecordLit(kvs) => { let kts = kvs .into_iter() .map(|(x, v)| Ok((x, v.get_type()?.into_owned()))) .collect::<Result<_, _>>()?; - Ok(RetType( - TypeIntermediate::RecordType(ctx.clone(), kts) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::RecordType(kts))) } UnionLit(x, v, kvs) => { let mut kts: std::collections::BTreeMap<_, _> = kvs @@ -578,11 +554,7 @@ fn type_last_layer( .collect::<Result<_, _>>()?; let t = v.get_type()?.into_owned(); kts.insert(x, Some(t)); - Ok(RetType( - TypeIntermediate::UnionType(ctx.clone(), kts) - .typecheck()? - .to_type(), - )) + Ok(RetTypeIntermediate(TypeIntermediate::UnionType(kts))) } Field(r, x) => { match &r.get_type()?.internal_whnf() { @@ -599,15 +571,12 @@ fn type_last_layer( Some(Value::UnionType(kts)) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { - Ok(RetType( + Ok(RetTypeIntermediate( TypeIntermediate::Pi( - ctx.clone(), "_".into(), t.to_type(ctx)?, r.clone(), ) - .typecheck()? - .to_type(), )) }, Some(None) => { |