module Ermine.Parser.Data
( constr
, dataType
) where
import Bound
import Bound.Var (unvar)
import Control.Applicative
import Control.Lens
import Data.List
import Data.Maybe
import Data.Text (Text)
import Ermine.Parser.Global
import Ermine.Parser.Style
import Ermine.Parser.Type
import Ermine.Syntax.Constructor
import Ermine.Syntax.Data
import Ermine.Syntax.Kind (HasKindVars(..))
import Ermine.Syntax.Type
import Text.Parser.Combinators
import Text.Parser.Token
abstractSimple :: Eq v => [v] -> v -> Var Int v
abstractSimple l v = maybe (F v) B $ elemIndex v l
constr :: (Monad m, TokenParsing m) => m (Constructor (Maybe Text) (Var Text Text))
constr = build . fromMaybe ([], [])
<$> optional (quantifier "forall")
<*> globalIdent termCon
<*> many typ0
where
build (ks, ts) g as = Constructor g (map Just ks) ts' as'
where
ts' = map (bimap (unvar Just Just) (abstract (`elemIndex` map Just ks))) ts
as' = abstract (`elemIndex` map fst ts) . abstractKinds (`elemIndex` map Just ks) <$> as
dataType :: (Monad m, TokenParsing m) => m (DataType () Text)
dataType = build <$ symbol "data"
<*> globalIdent typeCon
<*> typVarBindings
<*> (fromMaybe [] <$> optional (symbolic '=' *> sepBy constr (symbolic '|')))
where
build nm ts cs = bimap semiClosedKind semiClosedType $ DataType nm (map Just ks) ts' cs'
where
ks = nub . catMaybes $ toListOf kindVars (snd <$> ts, cs)
jks = Just <$> ks
ts' = map (bimap (unvar Just Just) (abstract (`elemIndex` jks))) ts
cs' = bimap (abstractSimple jks) (abstractSimple $ map fst ts) <$> cs
semiClosedKind (Just _) = error "dataType: Impossible kind"
semiClosedKind Nothing = ()
semiClosedType (B _) = error "dataType: Impossible type"
semiClosedType (F x) = x