module Calculi.Lambda.Cube.TH (
sf
, stlc
) where
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Quote as TH
import qualified Language.Haskell.TH.Syntax as TH
import qualified Compiler.Typesystem.SystemFOmega as SFO
import qualified Compiler.Typesystem.SystemF as SF
import qualified Compiler.Typesystem.SimplyTyped as STLC
import Text.Megaparsec
import Text.Megaparsec.Error
import Calculi.Lambda.Cube
import Data.List
import Control.Monad
#if __GLASGOW_HASKELL__ >= 800
type LCParsec = Parsec Dec String
#else
type LCParsec = Parsec String
#endif
type StringSF = SF.SystemF String String
type StringSTLC = STLC.SimplyTyped String
lamcsymbol :: String -> LCParsec String
lamcsymbol = lamctoken . string
lamctoken :: LCParsec a -> LCParsec a
lamctoken p = do
pval <- p
void $ many (char ' ')
return pval
paren :: LCParsec a -> LCParsec a
paren = between (lamcsymbol "(") (lamcsymbol ")")
wrapped :: LCParsec a -> LCParsec a
wrapped p = do
void $ many (lamcsymbol " ")
p' <- p
eof
return p'
variable :: LCParsec String
variable = lamctoken ((:) <$> lowerChar <*> many (lowerChar <|> upperChar)) <?> "variable"
constant :: LCParsec String
constant = lamctoken ((:) <$> upperChar <*> many (lowerChar <|> upperChar)) <?> "constant"
quant :: (Polymorphic t, String ~ PolyType t) => LCParsec t -> LCParsec t
quant pexpr = label "quantification" $ do
void $ lamcsymbol "∀" <|> lamcsymbol "forall"
tvars <- some variable
void $ lamcsymbol "."
expr <- pexpr
return (foldr quantify expr tvars)
exprsequence :: SimpleType t => LCParsec t -> LCParsec t
exprsequence subexpr = label "expression sequence" $ do
expr <- subexpr
funApply <- optional $ do
void $ lamcsymbol "->" <|> lamcsymbol "→"
exprsequence subexpr
return (maybe expr (expr /->) funApply)
sfexpr :: LCParsec StringSF
sfexpr = label "System-F expression" $
quant sfexpr
<|> exprsequence (poly <$> variable
<|> mono <$> constant
<|> paren sfexpr)
stlcexpr :: LCParsec StringSTLC
stlcexpr = label "Simply-typed expression" $ exprsequence (mono <$> constant <|> paren stlcexpr)
sf :: TH.QuasiQuoter
sf = mkqq "sf" sfexpr
stlc :: TH.QuasiQuoter
stlc = mkqq "stlc" stlcexpr
mkqq :: TH.Lift t => String -> LCParsec t -> TH.QuasiQuoter
mkqq pname p = TH.QuasiQuoter {
TH.quoteExp = \str -> do
loc <- TH.location
let fname = intercalate ":" [pname
, TH.loc_filename loc
, show $ TH.loc_start loc
, show $ TH.loc_end loc
]
case runParser (wrapped p) fname str of
Left err -> fail . show $ err
Right val -> TH.lift val
, TH.quotePat = error $ pname ++ " doesn't implement quotePat for this QuasiQuoter"
, TH.quoteType = error $ pname ++ " doesn't implement quoteType for this QuasiQuoter"
, TH.quoteDec = error $ pname ++ " doesn't implement quoteDec for this QuasiQuoter"
}