diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/phase/typecheck.rs (renamed from dhall/src/typecheck.rs) | 599 |
1 files changed, 148 insertions, 451 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/phase/typecheck.rs index 8d6b6eb..32c1531 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,361 +1,18 @@ #![allow(non_snake_case)] use std::borrow::Borrow; -use std::borrow::Cow; use std::collections::BTreeMap; -use std::fmt; -use crate::expr::*; -use crate::normalize::{ - AlphaVar, NormalizationContext, Thunk, TypeThunk, Value, -}; -use crate::traits::DynamicType; use dhall_proc_macros as dhall; -use dhall_syntax; -use dhall_syntax::context::Context; -use dhall_syntax::*; - -use self::TypeMessage::*; - -impl Resolved { - pub fn typecheck(self) -> Result<Typed, TypeError> { - type_of(self.0) - } - pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> { - let expr: SubExpr<_, _> = self.0; - let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd(); - type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) - } - /// Pretends this expression has been typechecked. Use with care. - #[allow(dead_code)] - pub fn skip_typecheck(self) -> Typed { - Typed::from_thunk_untyped(Thunk::new( - NormalizationContext::new(), - self.0, - )) - } -} - -impl Typed { - fn to_type(&self) -> Type { - match &self.to_value() { - Value::Const(c) => Type(TypeInternal::Const(*c)), - _ => Type(TypeInternal::Typed(Box::new(self.clone()))), - } - } -} - -impl Normalized { - fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - Normalized(self.0.shift(delta, var)) - } - pub(crate) fn to_type(self) -> Type { - self.0.to_type() - } -} - -impl Type { - pub(crate) fn to_normalized(&self) -> Normalized { - self.0.to_normalized() - } - pub(crate) fn to_expr(&self) -> SubExpr<X, X> { - self.0.to_expr() - } - pub(crate) fn to_value(&self) -> Value { - self.0.to_value() - } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { - self.0.get_type() - } - fn as_const(&self) -> Option<Const> { - self.0.as_const() - } - fn internal_whnf(&self) -> Option<Value> { - self.0.whnf() - } - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - Type(self.0.shift(delta, var)) - } - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Type(self.0.subst_shift(var, val)) - } - - fn const_sort() -> Self { - Type(TypeInternal::Const(Const::Sort)) - } - fn const_kind() -> Self { - Type(TypeInternal::Const(Const::Kind)) - } - pub(crate) fn const_type() -> Self { - Type(TypeInternal::Const(Const::Type)) - } -} - -impl TypeThunk { - fn to_type(&self, ctx: &TypecheckContext) -> Result<Type, TypeError> { - match self { - TypeThunk::Type(t) => Ok(t.clone()), - TypeThunk::Thunk(th) => { - // TODO: rule out statically - mktype(ctx, th.normalize_to_expr().embed_absurd().note_absurd()) - } - } - } -} - -/// A semantic type. This is partially redundant with `dhall_syntax::Expr`, on purpose. `TypeInternal` should -/// be limited to syntactic expressions: either written by the user or meant to be printed. -/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking, -/// but only construct `TypeInternal`s. -#[derive(Debug, Clone)] -pub(crate) enum TypeInternal { - Const(Const), - /// This must not contain a Const value. - Typed(Box<Typed>), -} - -impl TypeInternal { - fn to_typed(&self) -> Typed { - match self { - TypeInternal::Typed(e) => e.as_ref().clone(), - TypeInternal::Const(c) => const_to_typed(*c), - } - } - fn to_normalized(&self) -> Normalized { - self.to_typed().normalize() - } - fn to_expr(&self) -> SubExpr<X, X> { - self.to_normalized().to_expr() - } - fn to_value(&self) -> Value { - self.to_typed().to_value() - } - pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> { - Ok(match self { - TypeInternal::Typed(e) => e.get_type()?, - TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?), - }) - } - fn as_const(&self) -> Option<Const> { - match self { - TypeInternal::Const(c) => Some(*c), - _ => None, - } - } - fn whnf(&self) -> Option<Value> { - match self { - TypeInternal::Typed(e) => Some(e.to_value()), - _ => None, - } - } - fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - use TypeInternal::*; - match self { - Typed(e) => Typed(Box::new(e.shift(delta, var))), - Const(c) => Const(*c), - } - } - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - use TypeInternal::*; - match self { - Typed(e) => Typed(Box::new(e.subst_shift(var, val))), - Const(c) => Const(*c), - } - } -} - -impl Eq for TypeInternal {} -impl PartialEq for TypeInternal { - fn eq(&self, other: &Self) -> bool { - self.to_normalized() == other.to_normalized() - } -} - -#[derive(Debug, Clone)] -pub(crate) enum EnvItem { - Type(AlphaVar, Type), - Value(Normalized), -} - -impl EnvItem { - fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - use EnvItem::*; - match self { - Type(v, e) => Type(v.shift(delta, var), e.shift(delta, var)), - Value(e) => Value(e.shift(delta, var)), - } - } -} - -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(pub(crate) Context<Label, EnvItem>); - -impl TypecheckContext { - pub(crate) fn new() -> Self { - TypecheckContext(Context::new()) - } - pub(crate) fn insert_type(&self, x: &Label, t: Type) -> Self { - TypecheckContext( - self.0.map(|_, e| e.shift(1, &x.into())).insert( - x.clone(), - EnvItem::Type(x.into(), t.shift(1, &x.into())), - ), - ) - } - pub(crate) fn insert_value(&self, x: &Label, t: Normalized) -> Self { - TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t))) - } - pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> { - let V(x, n) = var; - match self.0.lookup(x, *n) { - Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)), - Some(EnvItem::Value(t)) => Some(t.get_type()?), - None => None, - } - } - fn to_normalization_ctx(&self) -> NormalizationContext { - NormalizationContext::from_typecheck_ctx(self) - } -} - -impl PartialEq for TypecheckContext { - fn eq(&self, _: &Self) -> bool { - // don't count contexts when comparing stuff - // this is dirty but needed for now - true - } -} -impl Eq for TypecheckContext {} - -fn function_check(a: Const, b: Const) -> Result<Const, ()> { - use dhall_syntax::Const::*; - match (a, b) { - (_, Type) => Ok(Type), - (Kind, Kind) => Ok(Kind), - (Sort, Sort) => Ok(Sort), - (Sort, Kind) => Ok(Sort), - _ => Err(()), - } -} - -// Equality up to alpha-equivalence (renaming of bound variables) -fn prop_equal<T, U>(eL0: T, eR0: U) -> bool -where - T: Borrow<Type>, - U: Borrow<Type>, -{ - eL0.borrow().to_value() == eR0.borrow().to_value() -} - -fn const_to_typed(c: Const) -> Typed { - match c { - Const::Sort => Typed::const_sort(), - _ => Typed::from_thunk_and_type( - Value::Const(c).into_thunk(), - type_of_const(c).unwrap(), - ), - } -} - -fn const_to_type(c: Const) -> Type { - Type(TypeInternal::Const(c)) -} - -fn type_of_const(c: Const) -> Result<Type, TypeError> { - match c { - Const::Type => Ok(Type::const_kind()), - Const::Kind => Ok(Type::const_sort()), - Const::Sort => { - return Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Sort, - )) - } - } -} - -fn type_of_builtin<E>(b: Builtin) -> Expr<X, E> { - use dhall_syntax::Builtin::*; - match b { - Bool | Natural | Integer | Double | Text => dhall::expr!(Type), - List | Optional => dhall::expr!( - Type -> Type - ), - - NaturalFold => dhall::expr!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - ), - NaturalBuild => dhall::expr!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - ), - NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!( - Natural -> Bool - ), - NaturalToInteger => dhall::expr!(Natural -> Integer), - NaturalShow => dhall::expr!(Natural -> Text), - - IntegerToDouble => dhall::expr!(Integer -> Double), - IntegerShow => dhall::expr!(Integer -> Text), - DoubleShow => dhall::expr!(Double -> Text), - TextShow => dhall::expr!(Text -> Text), - - ListBuild => dhall::expr!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - ), - ListFold => dhall::expr!( - forall (a: Type) -> - List a -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - ), - ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural), - ListHead | ListLast => { - dhall::expr!(forall (a: Type) -> List a -> Optional a) - } - ListIndexed => dhall::expr!( - forall (a: Type) -> - List a -> - List { index: Natural, value: a } - ), - ListReverse => dhall::expr!( - forall (a: Type) -> List a -> List a - ), +use dhall_syntax::{ + rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span, + SubExpr, X, +}; - OptionalBuild => dhall::expr!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => dhall::expr!( - forall (a: Type) -> - Optional a -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), - OptionalNone => dhall::expr!( - forall (a: Type) -> Optional a - ), - } -} +use crate::core::context::{NormalizationContext, TypecheckContext}; +use crate::core::thunk::{Thunk, TypeThunk}; +use crate::core::value::Value; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::{Normalized, Resolved, Type, Typed}; macro_rules! ensure_equal { ($x:expr, $y:expr, $err:expr $(,)*) => { @@ -386,6 +43,7 @@ pub(crate) enum TypeIntermediate { impl TypeIntermediate { fn typecheck(self) -> Result<Typed, TypeError> { + use crate::error::TypeMessage::*; let mkerr = |ctx, msg| TypeError::new(ctx, msg); Ok(match &self { TypeIntermediate::Pi(ctx, x, ta, tb) => { @@ -439,7 +97,7 @@ impl TypeIntermediate { TypeThunk::from_type(tb.clone()), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::RecordType(ctx, kts) => { @@ -469,7 +127,7 @@ impl TypeIntermediate { .collect(), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::UnionType(ctx, kts) => { @@ -508,7 +166,7 @@ impl TypeIntermediate { .collect(), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::ListType(ctx, t) => { @@ -520,7 +178,7 @@ impl TypeIntermediate { Value::from_builtin(Builtin::List) .app(t.to_value()) .into_thunk(), - const_to_type(Const::Type), + Type::from_const(Const::Type), ) } TypeIntermediate::OptionalType(ctx, t) => { @@ -532,23 +190,140 @@ impl TypeIntermediate { Value::from_builtin(Builtin::Optional) .app(t.to_value()) .into_thunk(), - const_to_type(Const::Type), + Type::from_const(Const::Type), ) } }) } } +fn function_check(a: Const, b: Const) -> Result<Const, ()> { + use dhall_syntax::Const::*; + match (a, b) { + (_, Type) => Ok(Type), + (Kind, Kind) => Ok(Kind), + (Sort, Sort) => Ok(Sort), + (Sort, Kind) => Ok(Sort), + _ => Err(()), + } +} + +// Equality up to alpha-equivalence (renaming of bound variables) +fn prop_equal<T, U>(eL0: T, eR0: U) -> bool +where + T: Borrow<Type>, + U: Borrow<Type>, +{ + eL0.borrow().to_value() == eR0.borrow().to_value() +} + +pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> { + match c { + Const::Type => Ok(Type::const_kind()), + Const::Kind => Ok(Type::const_sort()), + Const::Sort => { + return Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Sort, + )) + } + } +} + +fn type_of_builtin(b: Builtin) -> Expr<X, X> { + use dhall_syntax::Builtin::*; + match b { + Bool | Natural | Integer | Double | Text => dhall::expr!(Type), + List | Optional => dhall::expr!( + Type -> Type + ), + + NaturalFold => dhall::expr!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural + ), + NaturalBuild => dhall::expr!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural + ), + NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!( + Natural -> Bool + ), + NaturalToInteger => dhall::expr!(Natural -> Integer), + NaturalShow => dhall::expr!(Natural -> Text), + + IntegerToDouble => dhall::expr!(Integer -> Double), + IntegerShow => dhall::expr!(Integer -> Text), + DoubleShow => dhall::expr!(Double -> Text), + TextShow => dhall::expr!(Text -> Text), + + ListBuild => dhall::expr!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a + ), + ListFold => dhall::expr!( + forall (a: Type) -> + List a -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list + ), + ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural), + ListHead | ListLast => { + dhall::expr!(forall (a: Type) -> List a -> Optional a) + } + ListIndexed => dhall::expr!( + forall (a: Type) -> + List a -> + List { index: Natural, value: a } + ), + ListReverse => dhall::expr!( + forall (a: Type) -> List a -> List a + ), + + OptionalBuild => dhall::expr!( + forall (a: Type) -> + (forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional) -> + Optional a + ), + OptionalFold => dhall::expr!( + forall (a: Type) -> + Optional a -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + ), + OptionalNone => dhall::expr!( + forall (a: Type) -> Optional a + ), + } +} + /// Takes an expression that is meant to contain a Type /// and turn it into a type, typechecking it along the way. -fn mktype( +pub(crate) fn mktype( ctx: &TypecheckContext, e: SubExpr<Span, Normalized>, ) -> Result<Type, TypeError> { Ok(type_with(ctx, e)?.to_type()) } -fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> { +pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> { mktype( &TypecheckContext::new(), SubExpr::from_expr_no_note(ExprF::Builtin(b)), @@ -645,6 +420,7 @@ fn type_last_layer( ctx: &TypecheckContext, e: ExprF<Typed, Label, Normalized>, ) -> Result<Ret, TypeError> { + use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; use dhall_syntax::Builtin::*; use dhall_syntax::ExprF::*; @@ -857,9 +633,9 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetTyped(const_to_typed(c))), + Const(c) => Ok(RetTyped(Typed::from_const(c))), Builtin(b) => { - Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?)) + Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).absurd())?)) } BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)), NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)), @@ -927,99 +703,20 @@ fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> { Ok(e) } -/// The specific type error -#[derive(Debug)] -pub(crate) enum TypeMessage { - UnboundVariable(V<Label>), - InvalidInputType(Normalized), - InvalidOutputType(Normalized), - NotAFunction(Typed), - TypeMismatch(Typed, Normalized, Typed), - AnnotMismatch(Typed, Normalized), - Untyped, - InvalidListElement(usize, Normalized, Typed), - InvalidListType(Normalized), - InvalidOptionalType(Normalized), - InvalidPredicate(Typed), - IfBranchMismatch(Typed, Typed), - IfBranchMustBeTerm(bool, Typed), - InvalidFieldType(Label, Type), - NotARecord(Label, Normalized), - MissingRecordField(Label, Typed), - MissingUnionField(Label, Normalized), - BinOpTypeMismatch(BinOp, Typed), - NoDependentTypes(Normalized, Normalized), - InvalidTextInterpolation(Typed), - Sort, - Unimplemented, -} - -/// A structured type error that includes context -#[derive(Debug)] -pub struct TypeError { - type_message: TypeMessage, - context: TypecheckContext, -} - -impl TypeError { - pub(crate) fn new( - context: &TypecheckContext, - type_message: TypeMessage, - ) -> Self { - TypeError { - context: context.clone(), - type_message, - } - } -} - -impl From<TypeError> for std::option::NoneError { - fn from(_: TypeError) -> std::option::NoneError { - std::option::NoneError - } +pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> { + type_of(e.0) } -impl ::std::error::Error for TypeMessage { - fn description(&self) -> &str { - match *self { - // UnboundVariable => "Unbound variable", - InvalidInputType(_) => "Invalid function input", - InvalidOutputType(_) => "Invalid function output", - NotAFunction(_) => "Not a function", - TypeMismatch(_, _, _) => "Wrong type of function argument", - _ => "Unhandled error", - } - } +pub(crate) fn typecheck_with( + e: Resolved, + ty: &Type, +) -> Result<Typed, TypeError> { + let expr: SubExpr<_, _> = e.0; + let ty: SubExpr<_, _> = ty.to_expr().absurd(); + type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty))) } - -impl fmt::Display for TypeMessage { - fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - match self { - // UnboundVariable(_) => { - // f.write_str(include_str!("errors/UnboundVariable.txt")) - // } - // TypeMismatch(e0, e1, e2) => { - // let template = include_str!("errors/TypeMismatch.txt"); - // let s = template - // .replace("$txt0", &format!("{}", e0.as_expr())) - // .replace("$txt1", &format!("{}", e1.as_expr())) - // .replace("$txt2", &format!("{}", e2.as_expr())) - // .replace( - // "$txt3", - // &format!( - // "{}", - // e2.get_type() - // .unwrap() - // .as_normalized() - // .unwrap() - // .as_expr() - // ), - // ); - // f.write_str(&s) - // } - _ => f.write_str("Unhandled error message"), - } - } +pub(crate) fn skip_typecheck(e: Resolved) -> Typed { + Typed::from_thunk_untyped(Thunk::new(NormalizationContext::new(), e.0)) } #[cfg(test)] |