From 814c22dfe44a7ff896187cc87f212eb7de28a10a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 23 Apr 2019 22:51:29 +0200 Subject: RecordTypes --- dhall/src/typecheck.rs | 170 +++++++++++++++++++++++++++++++------------------ 1 file changed, 108 insertions(+), 62 deletions(-) (limited to 'dhall') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 0ee481f..f006ec6 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,6 +1,7 @@ #![allow(non_snake_case)] use std::borrow::Borrow; use std::borrow::Cow; +use std::collections::BTreeMap; use std::fmt; use std::marker::PhantomData; @@ -32,12 +33,6 @@ impl<'a> Resolved<'a> { } } impl<'a> Typed<'a> { - fn normalize_to_type( - self, - ctx: &TypecheckContext, - ) -> Result, TypeError> { - Ok(self.normalize().into_type_ctx(ctx)?) - } fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); ty.ok_or_else(|| { @@ -71,14 +66,13 @@ impl<'a> Normalized<'a> { self, ctx: &TypecheckContext, ) -> Result, TypeError> { - Ok(Type(match self.0.as_ref() { - ExprF::Const(c) => TypeInternal::Const(*c), + Ok(match self.0.as_ref() { + ExprF::Const(c) => Type(TypeInternal::Const(*c)), ExprF::Pi(_, _, _) => { - return Ok(type_with(ctx, self.0.embed_absurd())? - .normalize_to_type(ctx)?) + type_with(ctx, self.0.embed_absurd())?.normalize_to_type(ctx)? } - _ => TypeInternal::Expr(Box::new(self)), - })) + _ => Type(TypeInternal::Expr(Box::new(self))), + }) } fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); @@ -161,6 +155,7 @@ pub(crate) enum TypeInternal<'a> { Box>, Box>, ), + RecordType(TypecheckContext, Const, BTreeMap>), /// The type of `Sort` SuperType, /// This must not contain a value captured by one of the variants above. @@ -172,11 +167,16 @@ impl<'a> TypeInternal<'a> { match self { TypeInternal::Expr(e) => Ok(*e), TypeInternal::Pi(ctx, c, x, t, e) => Ok(Typed( - rc(ExprF::Pi( - x, - t.into_normalized()?.embed(), - e.into_normalized()?.embed(), - )), + rc(ExprF::Pi(x, t, e) + .traverse_ref_simple(|e| e.clone().embed())?), + Some(const_to_type(c)), + ctx, + PhantomData, + ) + .normalize()), + TypeInternal::RecordType(ctx, c, kts) => Ok(Typed( + rc(ExprF::RecordType(kts) + .traverse_ref_simple(|e| e.clone().embed())?), Some(const_to_type(c)), ctx, PhantomData, @@ -204,6 +204,13 @@ impl<'a> TypeInternal<'a> { Box::new(t.shift(delta, var)), Box::new(e.shift(delta, &var.shift0(1, x))), ), + RecordType(ctx, c, kts) => RecordType( + ctx.clone(), + *c, + kts.iter() + .map(|(k, v)| (k.clone(), v.shift(delta, var))) + .collect(), + ), Const(c) => Const(*c), SuperType => SuperType, } @@ -228,7 +235,7 @@ impl TypedOrType { ctx: &TypecheckContext, ) -> Result, TypeError> { match self { - TypedOrType::Typed(e) => Ok(e.normalize_to_type(ctx)?), + TypedOrType::Typed(e) => Ok(e.normalize().into_type_ctx(ctx)?), TypedOrType::Type(t) => Ok(t), } } @@ -531,43 +538,43 @@ macro_rules! ensure_is_const { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum TypeIntermediate { Pi(TypecheckContext, Label, Type<'static>, Type<'static>), + RecordType(TypecheckContext, BTreeMap>), } impl TypeIntermediate { fn typecheck(self) -> Result { + let mkerr = + |ctx, msg| Ok(TypeError::new(ctx, self.clone().into_expr()?, msg)); match &self { TypeIntermediate::Pi(ctx, x, ta, tb) => { let ctx2 = ctx.insert_type(x, ta.clone()); let kA = ensure_is_const!( &ta.get_type()?, - TypeError::new( + mkerr( ctx, - self.clone().into_expr()?, InvalidInputType(ta.clone().into_normalized()?), - ), + )?, ); let kB = ensure_is_const!( &tb.get_type()?, - TypeError::new( + mkerr( &ctx2, - self.clone().into_expr()?, InvalidOutputType( tb.clone() .into_normalized()? .get_type_move()? .into_normalized()? ), - ), + )?, ); let k = match function_check(kA, kB) { Ok(k) => k, Err(()) => { - return Err(TypeError::new( + return Err(mkerr( ctx, - self.clone().into_expr()?, NoDependentTypes( ta.clone().into_normalized()?, tb.clone() @@ -575,7 +582,7 @@ impl TypeIntermediate { .get_type_move()? .into_normalized()?, ), - )) + )?) } }; @@ -587,16 +594,51 @@ impl TypeIntermediate { Box::new(tb.clone()), )))) } + TypeIntermediate::RecordType(ctx, kts) => { + // Check that all types are the same const + let mut k = None; + for (x, t) in kts { + let k2 = ensure_is_const!( + t.get_type()?, + mkerr( + ctx, + InvalidFieldType( + x.clone(), + TypedOrType::Type(t.clone()) + ) + )? + ); + match k { + None => k = Some(k2), + Some(k1) if k1 != k2 => { + return Err(mkerr( + ctx, + InvalidFieldType( + x.clone(), + TypedOrType::Type(t.clone()), + ), + )?) + } + Some(_) => {} + } + } + // An empty record type has type Type + let k = k.unwrap_or(dhall_core::Const::Type); + + Ok(TypedOrType::Type(Type(TypeInternal::RecordType( + ctx.clone(), + k, + kts.clone(), + )))) + } } } fn into_expr(self) -> Result>, TypeError> { - match self { - TypeIntermediate::Pi(_, x, t, e) => Ok(rc(ExprF::Pi( - x, - t.into_normalized()?.embed(), - e.into_normalized()?.embed(), - ))), + Ok(rc(match self { + TypeIntermediate::Pi(_, x, t, e) => ExprF::Pi(x, t, e), + TypeIntermediate::RecordType(_, kts) => ExprF::RecordType(kts), } + .traverse_ref_simple(|e| e.clone().embed())?)) } } @@ -619,7 +661,9 @@ fn simple_type_from_builtin<'a>(b: Builtin) -> Type<'a> { /// Intermediary return type enum Ret { - /// Returns the contained Type as is + /// Returns the contained value as is + RetTypedOrType(TypedOrType), + /// Use the contained Type as the type of the input expression RetType(Type<'static>), /// Returns an expression that must be typechecked and /// turned into a Type first. @@ -651,8 +695,10 @@ fn type_with( let ta = mktype(ctx, ta.clone())?; let ctx2 = ctx.insert_type(x, ta.clone()); let tb = mktype(&ctx2, tb.clone())?; - return TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb) - .typecheck(); + Ok(RetTypedOrType( + TypeIntermediate::Pi(ctx.clone(), x.clone(), ta, tb) + .typecheck()?, + )) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -667,7 +713,7 @@ fn type_with( Ok(RetType(e.get_type_move()?)) } - Embed(p) => return Ok(TypedOrType::Typed(p.clone().into())), + Embed(p) => Ok(RetTypedOrType(TypedOrType::Typed(p.clone().into()))), _ => type_last_layer( ctx, // Typecheck recursively all subexpressions @@ -689,6 +735,7 @@ fn type_with( ctx.clone(), PhantomData, ))), + RetTypedOrType(tt) => Ok(tt), } } @@ -732,6 +779,10 @@ fn type_last_layer( a.normalize()?.embed(), tb.into_normalized()?.into_expr().embed_absurd(), ))) + // Ok(RetType(mktype( + // &ctx.insert_value(&x, a), + // tb.into_normalized()?.into_expr().embed_absurd(), + // )?)) } Annot(x, t) => { let t = t.normalize_to_type(ctx)?; @@ -823,24 +874,13 @@ fn type_last_layer( Ok(RetExpr(dhall::expr!(Optional t))) } RecordType(kts) => { - // Check that all types are the same const - let mut k = None; - for (x, t) in kts { - let k2 = ensure_is_const!( - t.get_type()?, - mkerr(InvalidFieldType(x, t)) - ); - match k { - None => k = Some(k2), - Some(k1) if k1 != k2 => { - return Err(mkerr(InvalidFieldType(x, t))) - } - Some(_) => {} - } - } - // An empty record type has type Type - let k = k.unwrap_or(dhall_core::Const::Type); - Ok(RetType(const_to_type(k))) + let kts: BTreeMap<_, _> = kts + .into_iter() + .map(|(x, t)| Ok((x, t.normalize_to_type(ctx)?))) + .collect::>()?; + Ok(RetTypedOrType( + TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?, + )) } UnionType(kts) => { // Check that all types are the same const @@ -860,20 +900,21 @@ fn type_last_layer( } } } - // An empty union type has type Type - // An union type with only unary variants has type Type + // An empty union type has type Type; + // an union type with only unary variants also has type Type let k = k.unwrap_or(dhall_core::Const::Type); Ok(RetType(const_to_type(k))) } RecordLit(kvs) => { let kts = kvs .into_iter() - .map(|(x, v)| { - let t = v.get_type_move()?.embed()?; - Ok((x, t)) - }) + .map(|(x, v)| Ok((x, v.get_type_move()?))) .collect::>()?; - Ok(RetExpr(RecordType(kts))) + Ok(RetType( + TypeIntermediate::RecordType(ctx.clone(), kts) + .typecheck()? + .normalize_to_type(ctx)?, + )) } UnionLit(x, v, kvs) => { let mut kts: std::collections::BTreeMap<_, _> = kvs @@ -890,6 +931,11 @@ fn type_last_layer( kts.insert(x, Some(t)); Ok(RetExpr(UnionType(kts))) } + // Field(r, x) => match &r.get_type()?.0 { + // TypeInternal::RecordType(_, _, kts) => match kts.get(&x) { + // Some(t) => Ok(RetType(t.clone())), + // None => Err(mkerr(MissingRecordField(x, r))), + // }, Field(r, x) => match r.get_type()?.unroll_ref()?.as_ref() { RecordType(kts) => match kts.get(&x) { Some(t) => Ok(RetExpr(t.unroll().embed_absurd())), -- cgit v1.2.3