acw/bang
1
0
Fork 0
Code Issues Pull Requests 1 Actions Packages Projects Releases Wiki Activity

Checkpoint.

Browse Source
This commit is contained in:
Adam Wick
2016-07-02 19:11:43 -07:00
parent 40c0517dd3
commit ad016f9dcf
7 changed files with 170 additions and 198 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
src/Bang/Monad.hs
View File

@@ -10,7 +10,7 @@ module Bang.Monad(
, runCompiler
, runPass
, getPassState, setPassState, overPassState, viewPassState
, genName, genTypeRef, genVarRef
, registerNewName, genName, genTypeRef, genVarRef
, warn, err
)
where
@@ -83,13 +83,14 @@ runCompiler cmd opts action =
Left _ -> exit ("Unable to open file '" ++ path ++ "'")
Right txt -> snd `fmap` unCompiler (action orig txt) (initialState cmd)
runPass :: s2 -> (Compiler s2 a) -> Compiler s1 a
runPass :: s2 -> (Compiler s2 a) -> Compiler s1 (s2, a)
runPass s2 action =
Compiler (\ cst1 ->
do let cst2 = set csPassState s2 cst1
s1 = view csPassState cst1
(cst2', v) <- unCompiler action cst2
return (set csPassState s1 cst2', v))
let retval = (view csPassState cst2', v)
return (set csPassState s1 cst2', retval))
getPassState :: Compiler s s
getPassState = Compiler (\ st -> return (st, view csPassState st))
@@ -105,6 +106,13 @@ viewPassState l = Compiler (\ st -> return (st, view (csPassState . l) st))
-- -----------------------------------------------------------------------------
registerNewName :: NameEnvironment -> Text -> Compiler s Name
registerNewName env name =
Compiler (\ st ->
do let current = view csNextIdent st
res = Name unknownLocation env current name
return (over csNextIdent (+1) st, res))
genName :: NameEnvironment -> Compiler s Name
genName env = Compiler (\ st ->
do let current = view csNextIdent st

5
src/Bang/Syntax/AST.hs
View File

@@ -47,9 +47,8 @@ data ConstantValue = ConstantInt Word Text
data Type = TypeUnit Location Kind
| TypePrim Location Kind Text
| TypeRef Location Kind Name
| TypeLambda Location Kind Type Type
| TypeLambda Location Kind [Type] Type
| TypeApp Location Kind Type Type
| TypeForAll [Name] Type
deriving (Show)
instance Eq Type where
@@ -58,7 +57,6 @@ instance Eq Type where
(TypeRef _ _ n) == (TypeRef _ _ m) = n == m
(TypeLambda _ _ at et) == (TypeLambda _ _ bt ft) = (at == bt) && (et == ft)
(TypeApp _ _ at bt) == (TypeApp _ _ ct dt) = (at == ct) && (bt == dt)
(TypeForAll ns t) == (TypeForAll ms u) = (ns == ms) && (t == u)
_ == _ = False
kind :: Type -> Kind
@@ -67,7 +65,6 @@ kind (TypePrim _ k _) = k
kind (TypeRef _ k _) = k
kind (TypeLambda _ k _ _) = k
kind (TypeApp _ k _ _) = k
kind (TypeForAll _ t) = kind t
data Kind = Star
| KindArrow Kind Kind

4
src/Bang/Syntax/Parser.y
View File

@@ -181,14 +181,14 @@ Type :: { Type }
[] -> return result
xs ->
do unregisterNames TypeEnv xs
return (TypeForAll xs result)
return result
}
RawType :: { (Type, [Name]) }
: RawType '->' BaseType {%
do let (p1, names1) = $1
(p2, names2) = $3
return (TypeLambda $2 (Star `KindArrow` Star) p1 p2, union names1 names2)
return (TypeLambda $2 (Star `KindArrow` Star) [p1] p2, union names1 names2)
}
| BaseType { $1 }

10
src/Bang/Syntax/ParserMonad.hs
View File

@@ -2,6 +2,7 @@
{-# LANGUAGE TemplateHaskell #-}
module Bang.Syntax.ParserMonad(
Parser
, NameDatabase
, runParser
, addFixities
, registerName
@@ -21,7 +22,7 @@ import Bang.Syntax.Location(Location(..), Located(..),
advanceWith', locatedAt)
import Bang.Syntax.ParserError(ParserError(..))
import Bang.Syntax.Token(Token(..), Fixity)
import Control.Lens(view, set, over)
import Control.Lens(view, set, over, _1)
import Control.Lens.TH(makeLenses)
import Control.Monad(forM_)
import Data.Char(digitToInt, isSpace)
@@ -30,6 +31,8 @@ import qualified Data.Map.Strict as Map
import Data.Text.Lazy(Text)
import qualified Data.Text.Lazy as T
type NameDatabase = Map (NameEnvironment, Text) Name
data ParserState = ParserState {
_psPrecTable :: Map Text Fixity
, _psNameDatabase :: Map (NameEnvironment, Text) Name
@@ -42,8 +45,9 @@ makeLenses ''ParserState
type Parser a = Compiler ParserState a
runParser :: Origin -> Text -> Parser a -> Compiler ps a
runParser origin stream action = runPass pstate action
runParser :: Origin -> Text -> Parser a -> Compiler ps (NameDatabase, a)
runParser origin stream action =
over _1 (view psNameDatabase) `fmap` runPass pstate action
where
initInput = AlexInput initialPosition stream
pstate = ParserState Map.empty Map.empty 1 origin initInput

9
src/Bang/Syntax/Pretty.hs
View File

@@ -1,5 +1,9 @@
module Bang.Syntax.Pretty(
ppModule
, ppDeclaration
, ppExpression
, ppType
, ppName
)
where
@@ -53,11 +57,8 @@ ppType t =
TypeUnit _ _ -> text "()"
TypePrim _ _ n -> text (unpack n)
TypeRef _ _ n -> ppName n
TypeLambda _ _ a b -> ppType a <> space <> text "->" <> space <> ppType b
TypeLambda _ _ as b -> hsep (map ppType as) <> space <> text "->" <> space <> ppType b
TypeApp _ _ a b -> ppType a <> space <> ppType b
TypeForAll ns s ->
text "∀" <> space <> hsep (punctuate comma (map ppName ns)) <>
space <> text "." <> space <> ppType s
text' :: Text -> Doc a
text' = text . unpack

296
src/Bang/TypeInfer.hs
View File

@@ -1,191 +1,169 @@
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
module Bang.TypeInfer
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
module Bang.TypeInfer(runTypeInference)
where
import Bang.Monad(Compiler, BangError(..), err,
getPassState, setPassState)
runPass, getPassState, setPassState,
viewPassState, overPassState,
registerNewName, genName)
import Bang.Syntax.AST
import Bang.Syntax.Location(unknownLocation)
import Control.Lens(view, over)
import Bang.Syntax.Location(Location, unknownLocation)
import Bang.Syntax.ParserMonad(NameDatabase(..))
import Bang.Syntax.Pretty(ppName)
import Bang.Utils.Pretty(BangDoc)
import Control.Lens(set, view, over)
import Control.Lens.TH(makeLenses)
import Data.List(union, nub, concat)
import Data.Map.Strict(Map)
import qualified Data.Map.Strict as Map
import Data.Text.Lazy(pack)
-- -----------------------------------------------------------------------------
type Substitution = Map Name Type
class Types t where
apply :: Substitution -> t -> t
tv :: t -> [Name]
nullSubstitution :: Substitution
nullSubstitution = Map.empty
(⟼) :: Name -> Type -> Substitution
(⟼) = Map.singleton
infixr 4 @@
(@@) :: Substitution -> Substitution -> Substitution
(@@) s1 s2 =
let s2' = Map.map (\ t -> apply s1 t) s2
in Map.union s2' s1
-- -----------------------------------------------------------------------------
data InferenceError = UnificationError Type Type
| OccursCheckFails Name Type
| KindCheckFails Name Type
| MatchFailure Type Type
| UnboundIdentifier Name
| MergeFailure Substitution Substitution
deriving (Show)
instance BangError InferenceError where
ppError = undefined
import Data.Set(Set)
import qualified Data.Set as Set
import Data.Text.Lazy(Text, pack)
import Text.PrettyPrint.Annotated(text, (<+>), quotes)
data InferenceState = InferenceState {
_istCurrentSubstitution :: Substitution
, _istNextIdentifier :: Word
_nameDatabase :: NameDatabase
}
makeLenses ''InferenceState
type Infer a = Compiler InferenceState a
runInfer :: NameDatabase -> Infer a -> Compiler ps a
runInfer ndb action = snd `fmap` runPass initial action
where initial = InferenceState ndb
-- -----------------------------------------------------------------------------
merge :: Substitution -> Substitution -> Infer Substitution
merge s1 s2 | agree = return (Map.union s1 s2)
| otherwise = err (MergeFailure s1 s2)
where
names = Map.keys (Map.intersection s1 s2)
agree = all (\ v ->
let refv = TypeRef (error "Internal error, TypeInfer") Star v
in apply s1 refv == apply s2 refv)
names
data InferError = UnboundVariable Location Name
deriving (Show)
mostGeneralUnifier :: Type -> Type -> Infer Substitution
mostGeneralUnifier t1 t2 =
case (t1, t2) of
(TypeApp _ _ l r, TypeApp _ _ l' r') ->
do s1 <- mostGeneralUnifier l l'
s2 <- mostGeneralUnifier (apply s1 r) (apply s1 r')
return (s2 @@ s1)
(u@(TypeRef _ _ _), t) -> varBind u t
(t, u@(TypeRef _ _ _)) -> varBind u t
(TypePrim _ _ tc1, TypePrim _ _ tc2) | tc1 == tc2 -> return nullSubstitution
_ -> err (UnificationError t1 t2)
instance BangError InferError where
ppError = prettyError
varBind :: Type -> Type -> Infer Substitution
varBind = undefined
-- | TypeRef _ _ u' <- t, u' == u = return nullSubstitution
-- | u `elem` tv t = err (OccursCheckFails u t)
-- | k /= kind t = err (KindCheckFails u t)
-- | otherwise = return (u ⟼ t)
--
match :: Type -> Type -> Infer Substitution
match t1 t2 =
case (t1, t2) of
(TypeApp _ _ l r, TypeApp _ _ l' r') ->
do sl <- match l l'
sr <- match r r'
merge sl sr
(TypeRef _ k u, t) | k == kind t -> return (u ⟼ t)
(TypePrim _ _ tc1, TypePrim _ _ tc2) | tc1 == tc2 -> return nullSubstitution
_ -> err (MatchFailure t1 t2)
prettyError :: InferError -> (Maybe Location, BangDoc)
prettyError e =
case e of
UnboundVariable l n ->
(Just l, text "Unbound variable '" <+> quotes (ppName n))
data Scheme = Forall [Kind] Type
-- -----------------------------------------------------------------------------
instance Types Scheme where
apply s (Forall ks t) = Forall ks (apply s t)
tv (Forall _ qt) = tv qt
type Substitutions = Map Name Type
data Assumption = Name :>: Scheme
noSubstitutions :: Substitutions
noSubstitutions = Map.empty
instance Types Assumption where
apply s (i :>: sc) = i :>: (apply s sc)
tv (_ :>: sc) = tv sc
composeSubstitutions :: Substitutions -> Substitutions -> Substitutions
composeSubstitutions s1 s2 = Map.map (apply s1) s2 `Map.union` s1
find :: Name -> [Assumption] -> Infer Scheme
find i [] = err (UnboundIdentifier i)
find i ((i' :>: sc) : as) | i == i' = return sc
| otherwise = find i as
class Types a where
freeTypeVariables :: a -> Set Name
apply :: Substitutions -> a -> a
instance Types Type where
apply s v@(TypeRef _ _ n) = case Map.lookup n s of
Just t -> t
Nothing -> v
apply s (TypeApp l k t u) = TypeApp l k (apply s t) (apply s u)
apply _ t = t
--
tv (TypeRef _ _ n) = [n]
tv (TypeApp _ _ t u) = tv t `union` tv u
tv _ = []
freeTypeVariables t =
case t of
TypeUnit _ _ -> Set.empty
TypePrim _ _ _ -> Set.empty
TypeRef _ _ n -> Set.singleton n
TypeLambda _ _ ns e -> Set.unions (map freeTypeVariables ns) `Set.union`
freeTypeVariables e
TypeApp _ _ a b -> freeTypeVariables a `Set.union` freeTypeVariables b
apply substs t =
case t of
TypeRef _ _ n -> case Map.lookup n substs of
Nothing -> t
Just t' -> t'
TypeLambda l k ns e -> TypeLambda l k (apply substs ns) (apply substs e)
TypeApp l k a b -> TypeApp l k (apply substs a) (apply substs b)
_ -> t
instance Types [Type] where
apply s = map (apply s)
tv = nub . concat . map tv
instance Types a => Types [a] where
freeTypeVariables l = Set.unions (map freeTypeVariables l)
apply s = map (apply s)
getSubstitution :: Infer Substitution
getSubstitution = view istCurrentSubstitution `fmap` getPassState
-- -----------------------------------------------------------------------------
extendSubstitution :: Substitution -> Infer ()
extendSubstitution s' =
do s <- getPassState
setPassState (over istCurrentSubstitution (s' @@) s)
inferModule :: Module -> Infer Module
inferModule = undefined
unify :: Type -> Type -> Infer ()
unify t1 t2 =
do s <- getSubstitution
u <- mostGeneralUnifier (apply s t1) (apply s t2)
extendSubstitution u
runTypeInference :: NameDatabase -> Module -> Compiler ps Module
runTypeInference ndb mod = runInfer ndb (inferModule mod)
gensym :: Kind -> Infer Type
gensym k =
do s <- getPassState
setPassState (over istNextIdentifier (+1) s)
let num = view istNextIdentifier s
str = "gensym:" ++ show num
name = Name unknownLocation TypeEnv num (pack str)
return (TypeRef unknownLocation k name)
data Predicate = IsIn String Type
deriving (Eq)
inferConstant :: ConstantValue -> Infer ([Predicate], Type)
inferConstant c =
do v <- gensym Star
let constraint | ConstantInt _ _ <- c = IsIn "IntLike" v
| ConstantChar _ <- c = IsIn "CharLake" v
| ConstantString _ <- c = IsIn "StringLike" v
| ConstantFloat _ <- c = IsIn "FloatLike" v
return ([constraint], v)
data ClassEnvironment = [Predicate] :=> Type
freshInst :: Scheme -> Infer ClassEnvironment
freshInst = undefined
inferExpression :: ClassEnvironment -> [Assumption] ->
Expression ->
Infer ([Predicate], Type)
inferExpression _classEnv assumpts expr =
case expr of
ConstantExp _ cv -> inferConstant cv
ReferenceExp _ n -> do sc <- find n assumpts
(ps :=> t) <- freshInst sc
return (ps, t)
LambdaExp _ _ _ -> error "FIXME, here"
infer :: Module -> Infer Module
infer = undefined
typeInfer :: Word -> Module -> Either InferenceError Module
typeInfer = undefined
-- data Scheme = Scheme [Name] Type
--
-- getName :: NameEnvironment -> Text -> Infer Name
-- getName env nameText =
-- do namedb <- viewPassState nameDatabase
-- let key = (env, nameText)
-- case Map.lookup key namedb of
-- Nothing ->
-- do name <- registerNewName env nameText
-- overPassState (set nameDatabase (Map.insert key name namedb))
-- return name
-- Just name ->
-- return name
--
-- runTypeInference :: NameDatabase -> Module -> Compiler ps Module
-- runTypeInference nameDB mod =
-- snd `fmap` (runPass initialState (inferModule mod))
-- where initialState = InferenceState nameDB
--
-- type Substitutions = Map Name Type
--
-- nullSubst :: Substitutions
-- nullSubst = Map.empty
--
-- type TypeEnv = Map Name Scheme
--
-- class Substitutable a where
-- apply :: Substitutions -> a -> Type
--
-- instance Substitutable Type where
-- apply subs t =
-- case t of
-- TypeUnit _ _ -> t
-- TypePrim _ _ _ -> t
-- TypeRef _ _ n -> case Map.lookup n subs of
-- Nothing -> t
-- Just t' -> t'
-- TypeLambda l k ats bt ->
-- TypeLambda l k (map (apply subs) ats) (apply subs bt)
-- TypeApp l k a b ->
-- TypeApp l k (apply subs a) (apply subs b)
-- TypeForAll ns t ->
-- TypeForAll ns (apply subs t)
--
-- instance Substitutable Name where
-- apply subs n =
-- case Map.lookup n subs of
-- Nothing -> TypeRef unknownLocation Star n
-- Just t -> t
--
-- instantiate :: Scheme -> Infer Type
-- instantiate =
-- do
--
-- inferExpression :: TypeEnv -> Expression ->
-- Infer (Substitutions, Type)
-- inferExpression typeEnv expr =
-- case expr of
-- ConstantExp s cv -> do memName <- getName TypeEnv "Memory"
-- return (nullSubst, TypeRef s Star memName)
-- ReferenceExp s n -> case Map.lookup n typeEnv of
-- Nothing -> err (UnboundVariable s n)
-- Just t -> do t' <- instantiate t
-- return (nullSubst, t')
-- LambdaExp s ns e -> do localTypeNames <- mapM (const (genName TypeEnv)) ns
-- let localSchemes = map (Scheme [] . TypeRef s Star) localTypeNames
-- localEnv = Map.fromList (zip ns localSchemes)
-- typeEnv' = typeEnv `Map.union` localEnv
-- (s1, t1) <- inferExpression typeEnv' e
-- return (s1, TypeLambda s (Star `KindArrow` Star)
-- (map (apply s1) localTypeNames)
-- t1)
--
-- inferModule :: Module -> Infer Module
-- inferModule = undefined

28
src/Main.hs
View File

@@ -3,6 +3,7 @@ import Bang.Monad
import Bang.Syntax.Lexer()
import Bang.Syntax.Parser(runParser, parseModule)
import Bang.Syntax.Pretty(ppModule)
import Bang.TypeInfer(runTypeInference)
import Data.Version(showVersion)
import Paths_bang(version)
import Text.PrettyPrint.Annotated(render)
@@ -10,28 +11,11 @@ import Text.PrettyPrint.Annotated(render)
main :: IO ()
main = getCommand >>= \ cmd ->
case cmd of
Parse o -> do mdl <- runCompiler cmd o (\ r t -> runParser r t parseModule)
Parse o -> do (_, mdl) <- runCompiler cmd o (\ r t -> runParser r t parseModule)
putStrLn (render (ppModule mdl))
TypeCheck o -> do mdl <- runCompiler cmd o (\ r t ->
do (ndb, mdl) <- runParser r t parseModule
runTypeInference ndb mdl)
putStrLn (render (ppModule mdl))
TypeCheck _ -> undefined
Help -> putStrLn helpString
Version -> putStrLn ("Bang tool, version " ++ showVersion version)
-- run :: CommandsWithInputFile o => o -> (FilePath -> Text -> IO ()) -> IO ()
-- run opts action =
-- do let path = view inputFile opts
-- mtxt <- tryJust (guard . isDoesNotExistError) (T.readFile path)
-- case mtxt of
-- Left _ -> exit ("Unable to open file '" ++ path ++ "'")
-- Right txt -> action path txt
--
-- withParsed :: (Module -> IO ()) -> FilePath -> Text -> IO ()
-- withParsed action path body =
-- case parseModule (File path) body of
-- Left err -> exit (show err)
-- Right mdl -> action mdl
--
-- withInferred :: (Module -> IO ()) -> Module -> IO ()
-- withInferred action mdl =
-- case typeInfer 0 mdl of
-- Left err -> exit (show err)
-- Right mdl' -> action mdl'