module DDC.Driver.Command.Check
( cmdUniverse
, cmdUniverse1
, cmdUniverse2
, cmdUniverse3
, cmdShowKind
, cmdTypeEquiv
, cmdShowWType
, cmdShowType
, cmdExpRecon
, ShowTypeMode(..)
, cmdCheckModuleFromFile
, cmdCheckModuleFromString
, cmdParseCheckType
, cmdParseCheckExp)
where
import DDC.Driver.Output
import DDC.Interface.Source
import DDC.Build.Language
import DDC.Core.Fragment
import DDC.Core.Load
import DDC.Core.Parser
import DDC.Core.Lexer
import DDC.Core.Module
import DDC.Core.Exp
import DDC.Core.Pretty
import DDC.Core.Compounds
import DDC.Type.Transform.SpreadT
import DDC.Type.Universe
import DDC.Type.Equiv
import Control.Monad.Trans.Error
import Control.Monad.IO.Class
import qualified DDC.Base.Parser as BP
import qualified DDC.Type.Check as T
import Control.Monad
cmdUniverse :: Language -> Source -> String -> IO ()
cmdUniverse language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= do result <- cmdParseCheckType source fragment str
case result of
Just (t, _)
| Just u <- universeOfType (profilePrimKinds profile) t
-> outDocLn $ ppr u
_ -> outDocLn $ text "no universe"
cmdUniverse1 :: Language -> Source -> String -> IO ()
cmdUniverse1 language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= do result <- cmdParseCheckType source fragment str
case result of
Just (t, _)
| Just u <- universeFromType1 (profilePrimKinds profile) t
-> outDocLn $ ppr u
_ -> outDocLn $ text "no universe"
cmdUniverse2 :: Language -> Source -> String -> IO ()
cmdUniverse2 language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
= do result <- cmdParseCheckType source fragment str
case result of
Just (t, _)
| Just u <- universeFromType2 t
-> outDocLn $ ppr u
_ -> outDocLn $ text "no universe"
cmdUniverse3 :: Language -> Source -> String -> IO ()
cmdUniverse3 language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
kenv = profilePrimKinds profile
goParse toks
= case BP.runTokenParser describeTok srcName
(pType (contextOfProfile profile))
toks of
Left err -> outDocLn $ ppr err
Right t -> goUniverse3 (spreadT kenv t)
goUniverse3 tt
= case universeFromType3 tt of
Just u -> outDocLn $ ppr u
Nothing -> outDocLn $ text "no universe"
in goParse (fragmentLexExp fragment srcName srcLine str)
cmdShowKind :: Language -> Source -> String -> IO ()
cmdShowKind language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp fragment srcName srcLine str
eTK = loadType profile srcName toks
in case eTK of
Left err -> outDocLn $ ppr err
Right (t, k) -> outDocLn $ ppr t <+> text "::" <+> ppr k
cmdTypeEquiv :: Language -> Source -> String -> IO ()
cmdTypeEquiv language source ss
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
goParse toks
= case BP.runTokenParser describeTok (nameOfSource source)
(do t1 <- pTypeAtom (contextOfProfile profile)
t2 <- pTypeAtom (contextOfProfile profile)
return (t1, t2))
toks
of Left err -> outDocLn $ text "parse error " <> ppr err
Right tt -> goEquiv tt
goEquiv (t1, t2)
= do b1 <- checkT t1
b2 <- checkT t2
if b1 && b2
then outStrLn $ show $ equivT t1 t2
else return ()
config = T.configOfProfile profile
kenv = profilePrimKinds profile
checkT t
= case T.checkType config kenv (spreadT kenv t) of
Left err
-> do outDocLn $ ppr err
return False
Right{}
-> return True
in goParse (fragmentLexExp fragment srcName srcLine ss)
cmdShowWType :: Language -> Source -> String -> IO ()
cmdShowWType language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
, profile <- fragmentProfile fragment
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp fragment srcName srcLine str
eTK = loadWitness profile srcName toks
in case eTK of
Left err -> outDocLn $ ppr err
Right (t, k) -> outDocLn $ ppr t <+> text "::" <+> ppr k
data ShowTypeMode
= ShowTypeAll
| ShowTypeValue
| ShowTypeEffect
| ShowTypeClosure
deriving (Eq, Show)
cmdShowType :: Language -> ShowTypeMode -> Source -> String -> IO ()
cmdShowType language mode source ss
| Language bundle <- language
, fragment <- bundleFragment bundle
, modules <- bundleModules bundle
= cmdParseCheckExp fragment modules True source ss >>= goResult fragment
where
goResult _ Nothing
= return ()
goResult fragment (Just x)
= let
Just annot = takeAnnotOfExp x
t = annotType annot
eff = annotEffect annot
clo = annotClosure annot
in case mode of
ShowTypeAll
-> do outDocLn $ ppr x
outDocLn $ text ":*:" <+> ppr t
let features = profileFeatures $ fragmentProfile fragment
when (featuresTrackedEffects features)
$ outDocLn $ text ":!:" <+> ppr eff
when (featuresTrackedClosures features)
$ outDocLn $ text ":$:" <+> ppr clo
ShowTypeValue
-> outDocLn $ ppr x <+> text "::" <+> ppr t
ShowTypeEffect
-> outDocLn $ ppr x <+> text ":!:" <+> ppr eff
ShowTypeClosure
-> outDocLn $ ppr x <+> text ":$:" <+> ppr clo
cmdExpRecon :: Language -> Source -> String -> IO ()
cmdExpRecon language source ss
| Language bundle <- language
, fragment <- bundleFragment bundle
, modules <- bundleModules bundle
= cmdParseCheckExp fragment modules True source ss
>>= goResult
where
goResult Nothing
= return ()
goResult (Just x)
= outDocLn $ ppr x
cmdCheckModuleFromFile
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> FilePath
-> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
cmdCheckModuleFromFile fragment filePath
= goLoad
where lexModule = fragmentLexModule fragment filePath 1
goLoad
= do mModule <- liftIO
$ loadModuleFromFile
(fragmentProfile fragment) lexModule filePath
case mModule of
Left err -> throwError (renderIndent $ ppr err)
Right mm -> goCheckFragment mm
goCheckFragment mm
= case fragmentCheckModule fragment mm of
Just err -> throwError (renderIndent $ ppr err)
Nothing -> return mm
cmdCheckModuleFromString
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> Source
-> String
-> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
cmdCheckModuleFromString fragment source str
= goLoad
where lexModule = fragmentLexModule fragment
(nameOfSource source)
(lineStartOfSource source)
goLoad
= let mModule = loadModuleFromString
(fragmentProfile fragment) lexModule
(nameOfSource source)
str
in case mModule of
Left err -> throwError (renderIndent $ ppr err)
Right mm -> goCheckFragment mm
goCheckFragment mm
= case fragmentCheckModule fragment mm of
Just err -> throwError (renderIndent $ ppr err)
Nothing -> return mm
cmdParseCheckType
:: (Ord n, Show n, Pretty n)
=> Source
-> Fragment n err
-> String
-> IO (Maybe (Type n, Kind n))
cmdParseCheckType source frag str
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp frag srcName srcLine str
eTK = loadType (fragmentProfile frag) srcName toks
in case eTK of
Left err
-> do outDocLn $ ppr err
return Nothing
Right (t, k)
-> return $ Just (t, k)
cmdParseCheckExp
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> ModuleMap (AnTEC () n) n
-> Bool
-> Source
-> String
-> IO (Maybe ( Exp (AnTEC BP.SourcePos n) n))
cmdParseCheckExp frag modules permitPartialPrims source str
= goLoad (fragmentLexExp frag (nameOfSource source) (lineStartOfSource source) str)
where
profile = fragmentProfile frag
features = profileFeatures profile
features' = features { featuresPartialPrims
= featuresPartialPrims features || permitPartialPrims}
profile' = profile { profileFeatures = features' }
frag' = frag { fragmentProfile = profile' }
goLoad toks
= case loadExp (fragmentProfile frag') modules (nameOfSource source) toks of
Left err
-> do putStrLn $ renderIndent $ ppr err
return Nothing
Right result
-> goCheckFragment result
goCheckFragment x
= case fragmentCheckExp frag' x of
Just err
-> do putStrLn $ renderIndent $ ppr err
return Nothing
Nothing
-> do return (Just x)