diff options
author | Nadrieril | 2019-05-06 23:52:15 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-06 23:52:15 +0200 |
commit | 55b5be3407a8528bc47482a591b168a7cb0ce91e (patch) | |
tree | 4ccd6a98d01e6436c7fdd51a77837b02847fc3a2 /dhall/src/phase/typecheck.rs | |
parent | 5b91eaa9d6b70a2ac72fe19f2d21871c8d94b017 (diff) |
Move main datatypes into their own modules
Diffstat (limited to 'dhall/src/phase/typecheck.rs')
-rw-r--r-- | dhall/src/phase/typecheck.rs | 345 |
1 files changed, 137 insertions, 208 deletions
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index aee9892..42a4540 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -1,220 +1,18 @@ #![allow(non_snake_case)] use std::borrow::Borrow; -use std::borrow::Cow; use std::collections::BTreeMap; use dhall_proc_macros as dhall; -use dhall_syntax::context::Context; use dhall_syntax::{ rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span, - SubExpr, V, X, + SubExpr, X, }; +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::normalize::{ - AlphaVar, NormalizationContext, Thunk, TypeThunk, Value, -}; use crate::phase::{Normalized, Resolved, Type, TypeInternal, Typed}; -use crate::traits::DynamicType; - -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()) - } - } - } -} - -#[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() -} - -pub(crate) 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)) -} - -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<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 - ), - - 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 - ), - } -} macro_rules! ensure_equal { ($x:expr, $y:expr, $err:expr $(,)*) => { @@ -399,16 +197,147 @@ impl TypeIntermediate { } } +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 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)) +} + +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<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 + ), + + 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)), |