she-0.0: src/TypesToKinds.lhs

> module TypesToKinds where

> import Control.Applicative

> import HaLay
> import Parsley

> dataGrok :: [Tok] -> [[Tok]]
> dataGrok cs@(KW "newtype" : T Ty _ : ds)
>    = map blat (fillet ds)
> dataGrok cs@(KW "data" : T Ty _ : ds)
>    = map blat (fillet ds)
> dataGrok cs = []

> blat :: (Tok, Int) -> [Tok]
> blat (c, j) =
>     [KW "data", T Ty (cxs ++ [Spc " "]), Sym "=", T Ty cxs] where
>   cxs = Spc " " : c : ([1 .. j] >>= (\k -> [Spc " ", Lid ("x" ++ show k)]))

> fillet :: [Tok] -> [(Tok, Int)]
> fillet [] = []
> fillet (Sym "=" : [T Ty cs]) =
>   case parse (pSep (spc *> teq (Sym "|")) (spc *> pOldSyn)) cs of
>     Just sis -> sis
>     _ -> []
> fillet (L "where" css : _)     = css >>= gadtSyn
> fillet (_ : cs) = fillet cs

> pOldSyn :: P Tok (Tok, Int)
> pOldSyn = (\s -> (jig s, 2)) <$ pArg <*> infC <* pArg
>       <|> (,) <$> pCId
>               <*> (length <$> many pArg <|> pBr Crl pFields)
>               <* spc

> jig :: String -> Tok
> jig s = (B Rnd [Sym (":$#$#$#" ++ s)])

> pArg :: P Tok ()
> pArg = spc <* (
>   () <$ lid <|>
>   () <$ uid <|>
>   pBr Rnd (() <$ pRest) <|>
>   pBr Sqr (() <$ pRest) <|>
>   teq (Sym "!") *> pArg
>   )

> pFields :: P Tok Int
> pFields = 0 <$ pEnd <|> (1 +) <$ lid <*> pFields <|> next *> pFields

> gadtSyn :: [Tok] -> [(Tok, Int)]
> gadtSyn cs = case parse pGDecl cs of
>   Just (ss, i) -> map (flip (,) i) ss
>   _ -> []

> pGDecl :: P Tok ([Tok], Int)
> pGDecl = (,) <$> pSep (spc *> teq (Sym ",")) pCId <* spc <* teq (Sym "::")
>              <*> pTag Ty pArity <* pRest

> pCId :: P Tok Tok
> pCId = Uid <$> (("SheTy" ++) <$> uid)
>    <|> jig <$> pBr Rnd (spc *> infC <* spc)

> pArity :: P Tok Int
> pArity = 0 <$ pEnd
>      <|> (1 +) <$ teq (Sym "->") <*> pArity
>      <|> next *> pArity

> tyTTK :: [Tok] -> Maybe [Tok]
> tyTTK (B Crl [T Ex us] : ts) =
>   Just $ B Rnd (munge exTTK us) : munge tyTTK ts
> tyTTK (B Crl [T Ty us] : ts) =
>   Just $ Sym "*" : munge tyTTK ts
> tyTTK _ = Nothing

> ttkMu :: [Tok] -> Maybe [Tok]
> ttkMu (T Ty us : ts) = Just $ T Ty (munge tyTTK us) : munge ttkMu ts
> ttkMu _ = Nothing

> exTTK :: [Tok] -> Maybe [Tok]
> exTTK (Uid s : ts) = Just $ Uid ("SheTy" ++ s) : munge exTTK ts
> exTTK (Sym (':' : s) : ts) = Just $ Sym (":$#$#$#:" ++ s) : munge exTTK ts
> exTTK _ = Nothing

> typesToKinds :: [[Tok]] -> [[Tok]]
> typesToKinds = map (munge ttkMu)