Browse Source

it, it works?

master
depsterr 9 months ago
parent
commit
1175881339
  1. 1
      TODO
  2. 11
      app/Main.hs
  3. 15
      readme.simple.txt
  4. 101
      src/Simple/TC.hs

1
TODO

@ -1,5 +1,6 @@
short term:
non-empty list type
check stuff is not already in scope for top levels
long term:
floats?

11
app/Main.hs

@ -6,13 +6,16 @@ import Parser.SanityCheck (sanityCheck)
import Parser.Parser (parse)
import Lexer.Lexer (runAlex')
import Simple.Convert
import Simple.TC
import System.Environment
import System.Exit
main :: IO ()
main = getArgs >>= \case
[] -> exitSuccess
(f:_) -> readFile f >>= \t -> case runAlex' parse f t >>= sanityCheck f t >>= convert f t of
(Left s) -> putStrLn s
(Right r) -> print r
[] -> exitSuccess
f:_ -> readFile f >>= \t -> case runAlex' parse f t >>= sanityCheck f t >>= convert f t of
Right r -> runChecks r >>= \case
Right (_, env) -> print env
Left err -> print err
Left e -> putStrLn e

15
readme.simple.txt

@ -5,3 +5,18 @@
[Bool -> Bool]
(def (((not True) False)
((not False) True)))
[Integer -> Bool]
(def (((is1 1) True)
((is1 _) False)))
(data IntList ([IntList] IEmpty)
([Integer -> IntList -> IntList] ICons))
(data BoolList ([BoolList] BEmpty)
([Bool -> BoolList -> BoolList] BCons))
[IntList -> BoolList]
(def (((is1l IEmpty) BEmpty)
((is1l (ICons x xs)) (BCons (is1 x) (is1l xs)))))

101
src/Simple/TC.hs

@ -3,9 +3,11 @@ Module: Simple.TC
Description: Simple type checker.
A type checker for a simple subset of the language.
TODO: major refactor, split code accros modules
-}
{-# LANGUAGE GeneralizedNewtypeDeriving, LambdaCase, TupleSections, TemplateHaskell #-}
module Simple.TC where
module Simple.TC (runChecks) where
import Simple.AST
import Types
@ -28,18 +30,28 @@ data TypeError
| NoCase PN
| UnknownPattern PN
| UndefinedType PN Identifier
| InvalidRecordField PN Identifier
| IncompleteInstance PN Identifier
deriving (Show)
type Env a = Map Identifier a
data CheckEnv = CheckEnv { _defs :: Env Type
, _types :: Set Identifier
, _rec :: Env (Env Type)
} deriving Show
makeLenses ''CheckEnv
newtype Check a = Check { getCheck :: StateT CheckEnv (ExceptT TypeError IO) a }
initialState :: CheckEnv
initialState = CheckEnv M.empty S.empty M.empty
newtype Check a = Check { runCheck :: StateT CheckEnv (ExceptT TypeError IO) a }
deriving (Functor, Applicative, Monad, MonadError TypeError, MonadState CheckEnv)
swap :: (a,b) -> (b,a)
swap (a,b) = (b,a)
local :: (CheckEnv -> CheckEnv) -> Check a -> Check a
local f ca = get >>= \s -> put (f s) >> ca >>= \r -> put s >> pure r
@ -58,15 +70,25 @@ modifyEnv f = modState (\env -> env & defs %~ f)
modifyTypeEnv :: (Set Identifier -> Set Identifier) -> Check ()
modifyTypeEnv f = modState (\env -> env & types %~ f)
modifyRecEnv :: (Env (Env Type) -> Env (Env Type)) -> Check ()
modifyRecEnv f = modState (\env -> env & rec %~ f)
getTypeEnv :: Check (Set Identifier)
getTypeEnv = (^. types) <$> get
getRecEnv :: Check (Env (Env Type))
getRecEnv = (^. rec) <$> get
localTypeEnv :: (Set Identifier -> Set Identifier) -> Check a -> Check a
localTypeEnv f = local (\env -> env & types %~ f)
guard :: Type -> TypeError -> Bool -> Check Type
guard t _ True = pure t
guard _ e False = throwError e
guard :: TypeError -> Bool -> Check ()
guard _ True = pure ()
guard e False = throwError e
guardt :: Type -> TypeError -> Bool -> Check Type
guardt t _ True = pure t
guardt _ e False = throwError e
withBindings :: [(Type, Identifier)] -> Check a -> Check a
withBindings = localEnv . (flip insertMapBindings)
@ -83,6 +105,9 @@ insertMapBindings = foldr (uncurry (flip M.insert))
insertSetTypes :: Ord a => Set a -> [a] -> Set a
insertSetTypes = foldr S.insert
insertRecCons :: Identifier -> [(Type, Identifier)] -> Check ()
insertRecCons i = modifyRecEnv . M.insert i . M.fromList . map swap
iesTotis :: [(Identifier, Expr)] -> Check [(Type, Identifier)]
iesTotis ies = getEnv >>= \env -> traverse (\(i,e) -> (,i) <$> inferExpr e) ies
@ -93,10 +118,8 @@ tsToFunc p (t:ts) b = FuncType p t (tsToFunc p ts b)
-- ^ Constructors of.. maybe I don't need this lol
consOf :: Type -> Check [(Type, Identifier)]
consOf t = pure . filter (constructs t . fst) . map flip2 . M.toList =<< getEnv
consOf t = pure . filter (constructs t . fst) . map swap . M.toList =<< getEnv
where
flip2 :: (a,b) -> (b,a)
flip2 (a,b) = (b,a)
-- ^ checks if second arg constructs first arg
constructs :: Type -> Type -> Bool
constructs t1 t2 | t1 == t2 = True
@ -105,7 +128,7 @@ consOf t = pure . filter (constructs t . fst) . map flip2 . M.toList =<< getEnv
checkExpr :: Expr -> Type -> Check Type
checkExpr expr t = checkType t >> inferExpr expr >>=
\t2 -> guard t (TypeMismatch (pos expr) t t2) (t == t2)
\t2 -> guardt t (TypeMismatch (pos expr) t t2) (t == t2)
inferExpr :: Expr -> Check Type
inferExpr = \case
@ -114,7 +137,7 @@ inferExpr = \case
checkExpr1 :: Expr1 -> Type -> Check Type
checkExpr1 expr t = checkType t >> inferExpr1 expr >>=
\t2 -> guard t (TypeMismatch (pos expr) t t2) (t == t2)
\t2 -> guardt t (TypeMismatch (pos expr) t t2) (t == t2)
inferFunc :: PN -> Expr -> [Expr] -> Check Type
inferFunc p _ [] = throwError (ArityMismatch p)
@ -132,12 +155,20 @@ inferExpr1 = \case
Apply p e es -> inferFunc p e es
Case p e pes -> inferExpr e >>= \t -> inferCase p t pes
Let _ ies e -> iesTotis ies >>= \tis -> withBindings tis (inferExpr e)
Inst p i ies -> undefined -- TODO: check type of each constructor and that all constructors are there
Inst p i ies -> getRecEnv >>= \renv ->
case M.lookup i renv of
Just rcons -> guard (IncompleteInstance p i) (M.size rcons == length ies)
>> mapM_ (\(i',e) -> case M.lookup i' rcons of
Just t -> checkExpr e t
Nothing -> throwError (InvalidRecordField p i')) ies
Nothing -> throwError (UndefinedType p i)
>> pure (UsrType p i)
Term t -> inferTerm t
checkTerm :: Term -> Type -> Check Type
checkTerm term t = checkType t >> inferTerm term >>=
\t2 -> guard t (TypeMismatch (pos term) t t2) (t == t2)
\t2 -> guardt t (TypeMismatch (pos term) t t2) (t == t2)
inferTerm :: Term -> Check Type
inferTerm = \case
@ -150,7 +181,7 @@ inferTerm = \case
checkLiteral :: Literal -> Type -> Check Type
checkLiteral lit t = checkType t >> inferLiteral lit >>=
\t2 -> guard t (TypeMismatch (pos lit) t t2) (t == t2)
\t2 -> guardt t (TypeMismatch (pos lit) t t2) (t == t2)
inferLiteral :: Literal -> Check Type
inferLiteral = \case
@ -191,7 +222,7 @@ patternBindings target = \case
checkPattern :: Pattern -> Type -> Check Type
checkPattern pt t = checkType t >> inferPattern t pt >>=
\t2 -> guard t (TypeMismatch (pos pt) t t2) (t == t2)
\t2 -> guardt t (TypeMismatch (pos pt) t t2) (t == t2)
inferPattern :: Type -> Pattern -> Check Type
inferPattern target = \case
@ -214,10 +245,11 @@ inferPattern target = \case
-- This goes on the users given declerations, if they've been wrong it'll error out later
withTlBinding :: TopLevel -> Check ()
withTlBinding (Def _ t i _ ) = checkType t >> insertBindings [(t,i)]
withTlBinding (Dat _ i tis) = insertTypes [i] >> checkTypes tis >> insertBindings tis
withTlBinding (Rec p i tis) = insertTypes [i] >> insertBindings (constructor : deconstructors)
insertTLBinding :: TopLevel -> Check ()
insertTLBinding (Def _ t i _ ) = insertBindings [(t,i)]
insertTLBinding (Dat _ i tis) = insertTypes [i] >> insertBindings tis
insertTLBinding (Rec p i tis) = insertTypes [i] >> insertBindings (constructor : deconstructors)
>> insertRecCons i tis
where
constructor :: (Type, Identifier)
constructor = (tsToFunc p (fst <$> tis) curType, i)
@ -234,19 +266,38 @@ withTlBinding (Rec p i tis) = insertTypes [i] >> insertBindings (constructor :
go1 :: Type -> Type -> Type
go1 t1 t2 = FuncType (pos t2) t1 t2
checkTopLevel :: TopLevel -> Check Type
checkTopLevel tl t = checkType t >> inferTopLevel tl >>=
\t2 -> guard t (TypeMismatch (pos tl) t t2) (t == t2)
-- Assumes you've already bound all top levels
checkTopLevel :: TopLevel -> Check ()
checkTopLevel (Def _ _ _ []) = throwError Urk -- this should not be able to be (use non-empty lists you fool)
checkTopLevel (Def p _ i pes) = getEnv >>= \env ->
case M.lookup i env of
Just t -> mapM_ (checkCases p t) pes
Nothing -> throwError Urk -- should be in env at this point
checkTopLevel (Dat p i tis) = checkTypes tis
checkTopLevel (Rec p i tis) = checkTypes tis
-- if we have no patterns, simply check type, otherwise match pattern with function type and recurse
checkCases :: PN -> Type -> ([Pattern], Expr) -> Check Type
checkCases _ t ([],e) = checkExpr e t
checkCases p (FuncType _ t1 t2) (pe:ps,e) = checkPattern pe t1 >>
patternBindings t1 pe >>= \b -> withBindings b (checkCases p t2 (ps,e))
checkCases p _ _ = throwError (ArityMismatch p)
inferTopLevel :: TopLevel -> Check Type
inferTopLevel = undefined -- use patterns to see how much is matched away and then go on expr
-- make sure it matches what's in the environment
-- checkPattern :: Pattern -> Type -> Check Type
-- checkPattern pt t = checkType t >> inferPattern t pt >>=
-- check that shit is in scope
checkType :: Type -> Check Type
checkType (FuncType p t1 t2) = FuncType p <$> checkType t1 <*> checkType t2
checkType t@(UsrType p i) = getTypeEnv >>= guard t (UndefinedType p i) . S.member i
checkType t@(UsrType p i) = getTypeEnv >>= guardt t (UndefinedType p i) . S.member i
checkType t = pure t
checkTypes :: [(Type, a)] -> Check ()
checkTypes = mapM_ (checkType . fst)
checkAST :: [TopLevel] -> Check ()
checkAST tls = mapM_ insertTLBinding tls >> mapM_ checkTopLevel tls
runChecks :: [TopLevel] -> IO (Either TypeError ((), CheckEnv))
runChecks tls = runExceptT (runStateT (runCheck (checkAST tls)) initialState)

Loading…
Cancel
Save