Browse files

Remove redundancy and prevent a nasty error message for ill-kinded th…

…ings

Ignore-this: bc5cdbcea244ef7b3ddb098c916361a5

darcs-hash:20111028145051-e29d1-ce44893b9e77bae52eefaab96facbaf5f8874473.gz
  • Loading branch information...
1 parent 4fea7e0 commit e24efa820e8cdb3061279bcb4748adce93422cf6 @adamgundry committed Oct 28, 2011
Showing with 16 additions and 22 deletions.
  1. +0 −1 src/Language/Inch/File.lhs
  2. +12 −9 src/Language/Inch/KindCheck.lhs
  3. +0 −8 src/Language/Inch/Main.lhs
  4. +4 −4 src/Language/Inch/TypeCheck.lhs
View
1 src/Language/Inch/File.lhs
@@ -5,7 +5,6 @@
> import Prelude hiding (catch)
> import Control.Exception
> import Control.Monad.State
-> import System.Environment
> import System.Exit
> import System.FilePath
> import System.IO
View
21 src/Language/Inch/KindCheck.lhs
@@ -52,17 +52,13 @@
> inferKind _ _ (SBinOp o) = return $ TK (BinOp o) (KNum :-> KNum :-> KNum)
> inferKind b g (SBind c a SKNat t) = do
> v <- freshVar (UserVar All) a KNum
-> TK ty l <- inferKind b (g :< Ex v) t
-> case l of
-> KSet -> return $ TK (Bind c a KNum (bindTy v (Qual (P LE 0 (TyVar v)) ty))) KSet
-> _ -> erk "inferKind: forall/pi must have kind *"
+> ty <- checkKindSet b (g :< Ex v) t
+> return $ TK (Bind c a KNum (bindTy v (Qual (P LE 0 (TyVar v)) ty))) KSet
> inferKind b g (SBind c a k t) = case kindKind k of
> Ex k' -> do
> v <- freshVar (UserVar All) a k'
-> TK ty l <- inferKind b (g :< Ex v) t
-> case l of
-> KSet -> return $ TK (Bind c a k' (bindTy v ty)) KSet
-> _ -> erk "inferKind: forall/pi must have kind *"
+> ty <- checkKindSet b (g :< Ex v) t
+> return $ TK (Bind c a k' (bindTy v ty)) KSet
> inferKind b g (SQual p t) = do
> p' <- checkPredKind b g p
> TK t' KSet <- inferKind b g t
@@ -73,9 +69,16 @@
> TK t' k <- inferKind b g t
> case k of
> KNum -> return t'
-> _ -> erk "checkNumKind: ill-kinded!"
+> _ -> errKindMismatch (fogTy t' ::: fogKind k) SKNum
> checkPredKind :: Binder -> Bwd (Ex (Var ())) -> SPredicate -> Contextual Predicate
> checkPredKind b g = traverse (checkNumKind b g)
+
+> checkKindSet :: Binder -> Bwd (Ex (Var ())) -> SType -> Contextual (Type KSet)
+> checkKindSet b g t = do
+> TK t' k <- inferKind b g t
+> case k of
+> KSet -> return t'
+> _ -> errKindNotSet (fogKind k)
View
8 src/Language/Inch/Main.lhs
@@ -3,19 +3,11 @@
> module Main where
> import Prelude hiding (catch)
-> import Control.Exception
-> import Control.Monad.State
> import System.Environment
-> import System.Exit
> import System.FilePath
-> import System.IO
-> import Language.Inch.Context
> import Language.Inch.Syntax
-> import Language.Inch.Parser
> import Language.Inch.PrettyPrinter
-> import Language.Inch.ProgramCheck
-> import Language.Inch.Erase
> import Language.Inch.File
View
8 src/Language/Inch/TypeCheck.lhs
@@ -324,9 +324,9 @@ status.
> return $ Let ds' t' ::: ty
> checkInfer mty (t :? xty) = do
-> TK sc KSet <- inferKind All B0 xty
-> t' <- checkSigma sc t
-> r <- instSigma sc mty
+> sc <- checkKindSet All B0 xty
+> t' <- checkSigma sc t
+> r <- instSigma sc mty
> return $ (t' :? sc) ::: r
> checkInfer (Just r) (Case t as) = do
@@ -337,7 +337,7 @@ status.
> checkInfer Nothing (Case t as) = do
> t' ::: ty <- inferRho t
> as' ::: tys <- unzipAsc <$> traverse (inferCaseAlt ty) as
-> r <- unifyList tys
+> r <- unifyList tys
> return (Case t' as' ::: r)
> checkInfer _ (TmBrace _) = erk "Braces aren't cool"

0 comments on commit e24efa8

Please sign in to comment.