From c736660f6dd26290773257d17ef909a77cd0a3f8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 26 Apr 2019 23:49:19 +0200 Subject: Lists and Optionals --- dhall/src/typecheck.rs | 136 ++++++++++++++++++++++++++++++++++--------------- 1 file changed, 94 insertions(+), 42 deletions(-) (limited to 'dhall') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 8088ef3..e7231e9 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -96,15 +96,6 @@ impl<'a> Type<'a> { &self, ) -> Result>, TypeError> { Ok(Cow::Owned(self.0.clone().into_normalized()?)) - // match &self.0 { - // TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), - // TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), - // TypeInternal::SuperType => Err(TypeError::new( - // &TypecheckContext::new(), - // rc(ExprF::Const(Const::Sort)), - // TypeMessage::Untyped, - // )), - // } } pub(crate) fn into_normalized(self) -> Result, TypeError> { self.0.into_normalized() @@ -165,6 +156,8 @@ pub(crate) enum TypeInternal<'a> { Const, BTreeMap>>, ), + ListType(TypecheckContext, Box>), + OptionalType(TypecheckContext, Box>), /// The type of `Sort` SuperType, /// This must not contain a value captured by one of the variants above. @@ -192,6 +185,30 @@ impl<'a> TypeInternal<'a> { TypeInternal::UnionType(ctx, c, kts) => { (ctx, ExprF::UnionType(kts), const_to_type(c)) } + TypeInternal::ListType(ctx, t) => { + return Ok(Typed( + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + t.embed()?, + )), + Some(Type::const_type()), + ctx, + PhantomData, + ) + .normalize()) + } + TypeInternal::OptionalType(ctx, t) => { + return Ok(Typed( + rc(ExprF::App( + rc(ExprF::Builtin(Builtin::Optional)), + t.embed()?, + )), + Some(Type::const_type()), + ctx, + PhantomData, + ) + .normalize()) + } }; let typed = Typed( rc(e.traverse_ref_simple(|e| e.clone().embed())?), @@ -231,6 +248,12 @@ impl<'a> TypeInternal<'a> { }) .collect(), ), + ListType(ctx, t) => { + ListType(ctx.clone(), Box::new(t.shift(delta, var))) + } + OptionalType(ctx, t) => { + OptionalType(ctx.clone(), Box::new(t.shift(delta, var))) + } Const(c) => Const(*c), SuperType => SuperType, } @@ -533,7 +556,7 @@ macro_rules! ensure_equal { macro_rules! ensure_simple_type { ($x:expr, $err:expr $(,)*) => {{ match $x.get_type()?.internal() { - TypeInternal::Const(Type) => {} + TypeInternal::Const(dhall_core::Const::Type) => {} _ => return Err($err), } }}; @@ -544,6 +567,8 @@ pub(crate) enum TypeIntermediate { Pi(TypecheckContext, Label, Type<'static>, Type<'static>), RecordType(TypecheckContext, BTreeMap>), UnionType(TypecheckContext, BTreeMap>>), + ListType(TypecheckContext, Type<'static>), + OptionalType(TypecheckContext, Type<'static>), } impl TypeIntermediate { @@ -661,6 +686,29 @@ impl TypeIntermediate { kts.clone(), )))) } + TypeIntermediate::ListType(ctx, t) => { + ensure_simple_type!( + t, + mkerr(ctx, InvalidListType(t.clone().into_normalized()?))?, + ); + Ok(TypedOrType::Type(Type(TypeInternal::ListType( + ctx.clone(), + Box::new(t.clone()), + )))) + } + TypeIntermediate::OptionalType(ctx, t) => { + ensure_simple_type!( + t, + mkerr( + ctx, + InvalidOptionalType(t.clone().into_normalized()?) + )?, + ); + Ok(TypedOrType::Type(Type(TypeInternal::OptionalType( + ctx.clone(), + Box::new(t.clone()), + )))) + } } } fn into_expr(self) -> Result>, TypeError> { @@ -668,6 +716,18 @@ impl TypeIntermediate { TypeIntermediate::Pi(_, x, t, e) => ExprF::Pi(x, t, e), TypeIntermediate::RecordType(_, kts) => ExprF::RecordType(kts), TypeIntermediate::UnionType(_, kts) => ExprF::UnionType(kts), + TypeIntermediate::ListType(_, t) => { + return Ok(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + t.embed()?, + ))) + } + TypeIntermediate::OptionalType(_, t) => { + return Ok(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::Optional)), + t.embed()?, + ))) + } } .traverse_ref_simple(|e| e.clone().embed())?)) } @@ -744,6 +804,17 @@ fn type_with( Ok(RetType(e.get_type_move()?)) } + OldOptionalLit(None, t) => { + let t = t.clone(); + let e = dhall::subexpr!(None t); + return type_with(ctx, e); + } + OldOptionalLit(Some(x), t) => { + let t = t.clone(); + let x = x.clone(); + let e = dhall::subexpr!(Some x : Optional t); + return type_with(ctx, e); + } Embed(p) => Ok(RetTypedOrType(TypedOrType::Typed(p.clone().into()))), _ => type_last_layer( ctx, @@ -779,7 +850,6 @@ fn type_last_layer( ) -> Result { use dhall_core::BinOp::*; use dhall_core::Builtin::*; - use dhall_core::Const::*; use dhall_core::ExprF::*; let mkerr = |msg: TypeMessage<'static>| { TypeError::new(ctx, original_e.clone(), msg) @@ -848,20 +918,15 @@ fn type_last_layer( } EmptyListLit(t) => { let t = t.normalize_to_type()?; - ensure_simple_type!( - t, - mkerr(InvalidListType(t.into_normalized()?)), - ); - let t = t.embed()?; - Ok(RetExpr(dhall::expr!(List t))) + Ok(RetType( + TypeIntermediate::ListType(ctx.clone(), t) + .typecheck()? + .normalize_to_type()?, + )) } NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); let (_, x) = iter.next().unwrap(); - ensure_simple_type!( - x.get_type()?, - mkerr(InvalidListType(x.get_type_move()?.into_normalized()?)), - ); for (i, y) in iter { ensure_equal!( x.get_type()?, @@ -874,33 +939,20 @@ fn type_last_layer( ); } let t = x.get_type_move()?; - let t = t.embed()?; - Ok(RetExpr(dhall::expr!(List t))) - } - OldOptionalLit(None, t) => { - let t = t.normalize()?.embed(); - let e = dhall::subexpr!(None t); Ok(RetType( - type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(), + TypeIntermediate::ListType(ctx.clone(), t) + .typecheck()? + .normalize_to_type()?, )) } - OldOptionalLit(Some(x), t) => { - let t = t.normalize()?.embed(); - let x = x.normalize()?.embed(); - let e = dhall::subexpr!(Some x : Optional t); + SomeLit(x) => { + let t = x.get_type_move()?; Ok(RetType( - type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(), + TypeIntermediate::OptionalType(ctx.clone(), t) + .typecheck()? + .normalize_to_type()?, )) } - SomeLit(x) => { - let tx = x.get_type_move()?; - ensure_simple_type!( - tx, - mkerr(InvalidOptionalType(tx.into_normalized()?)), - ); - let t = tx.embed()?; - Ok(RetExpr(dhall::expr!(Optional t))) - } RecordType(kts) => { let kts: BTreeMap<_, _> = kts .into_iter() -- cgit v1.2.3