module DDC.Driver.Command.Check
(
cmdCheckFromFile
, cmdCheckSourceTetraFromFile
, cmdCheckSourceTetraFromString
, cmdCheckCoreFromFile
, cmdCheckCoreFromString
, cmdShowType
, cmdTypeEquiv
, cmdParseCheckType
, Mode(..)
, ShowSpecMode(..)
, cmdShowSpec
, cmdExpRecon
, cmdParseCheckExp
, cmdShowWType)
where
import DDC.Driver.Stage
import DDC.Driver.Output
import DDC.Driver.Config
import DDC.Interface.Source
import DDC.Build.Language
import DDC.Build.Pipeline
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 qualified DDC.Core.Check as C
import Control.Monad
import System.FilePath
import System.Directory
cmdCheckFromFile
:: Config
-> FilePath
-> ErrorT String IO ()
cmdCheckFromFile config filePath
| ".dst" <- takeExtension filePath
= cmdCheckSourceTetraFromFile config filePath
| Just language <- languageOfExtension (takeExtension filePath)
= cmdCheckCoreFromFile config language filePath
| otherwise
= let ext = takeExtension filePath
in throwError $ "Cannot check '" ++ ext ++ "'files."
cmdCheckSourceTetraFromFile
:: Config
-> FilePath
-> ErrorT String IO ()
cmdCheckSourceTetraFromFile config filePath
= do
exists <- liftIO $ doesFileExist filePath
when (not exists)
$ throwError $ "No such file " ++ show filePath
src <- liftIO $ readFile filePath
cmdCheckSourceTetraFromString config (SourceFile filePath) src
cmdCheckSourceTetraFromString
:: Config
-> Source
-> String
-> ErrorT String IO ()
cmdCheckSourceTetraFromString config source str
= let
pmode = prettyModeOfConfig $ configPretty config
pipeLoad
= pipeText (nameOfSource source) (lineStartOfSource source) str
$ stageSourceTetraLoad config source
[ PipeCoreOutput pmode SinkDiscard ]
in do
errs <- liftIO pipeLoad
case errs of
[] -> return ()
es -> throwError $ renderIndent $ vcat $ map ppr es
cmdCheckCoreFromFile
:: Config
-> Language
-> FilePath
-> ErrorT String IO ()
cmdCheckCoreFromFile config language filePath
| Language bundle <- language
, fragment <- bundleFragment bundle
= do
mModule <- liftIO
$ loadModuleFromFile fragment filePath
$ (if configInferTypes config then C.Synth else C.Recon)
case mModule of
(Left err, _ct) -> throwError (renderIndent $ ppr err)
(Right _, _ct) -> return ()
cmdCheckCoreFromString
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> Source
-> String
-> C.Mode n
-> ErrorT String IO (Module (AnTEC BP.SourcePos n) n)
cmdCheckCoreFromString fragment source str mode
= do
let mModule = loadModuleFromString fragment
(nameOfSource source) (lineStartOfSource source)
mode str
case mModule of
(Left err, _ct) -> throwError (renderIndent $ ppr err)
(Right mm, _ct) -> return mm
cmdParseCheckType
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> Universe
-> Source
-> String
-> IO (Maybe (Type n, Kind n))
cmdParseCheckType fragment uni source str
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp fragment srcName srcLine str
eTK = loadTypeFromTokens fragment uni srcName toks
in case eTK of
Left err
-> do outDocLn $ ppr err
return Nothing
Right (t, k)
-> return $ Just (t, k)
cmdShowType :: Language -> Universe -> Source -> String -> IO ()
cmdShowType language uni source str
| Language bundle <- language
, fragment <- bundleFragment bundle
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp fragment srcName srcLine str
eTK = loadTypeFromTokens fragment uni 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.checkSpec config kenv (spreadT kenv t) of
Left err
-> do outDocLn $ ppr err
return False
Right{}
-> return True
in goParse (fragmentLexExp fragment srcName srcLine ss)
cmdParseCheckExp
:: (Ord n, Show n, Pretty n, Pretty (err (AnTEC BP.SourcePos n)))
=> Fragment n err
-> ModuleMap (AnTEC () n) n
-> Mode n
-> Bool
-> Bool
-> Source
-> String
-> IO ( Maybe (Exp (AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
cmdParseCheckExp
fragment modules
mode printTrace permitPartialPrims
source str
= goLex
where
profile = fragmentProfile fragment
features = profileFeatures profile
features' = features { featuresPartialPrims
= featuresPartialPrims features || permitPartialPrims}
profile' = profile { profileFeatures = features' }
fragment' = fragment { fragmentProfile = profile' }
goLex
= goLoad (fragmentLexExp fragment'
(nameOfSource source)
(lineStartOfSource source)
str)
goLoad toks
= case loadExpFromTokens fragment' modules
(nameOfSource source) mode toks of
(Left err, mct)
-> do outDocLn $ ppr err
case mct of
Just ct
| printTrace -> outDocLn $ ppr ct
_ -> return ()
return (Nothing, mct)
(Right result, mct)
-> return (Just result, mct)
data ShowSpecMode
= ShowSpecAll
| ShowSpecData
| ShowSpecEffect
| ShowSpecClosure
deriving (Eq, Show)
cmdShowSpec
:: Language
-> ShowSpecMode
-> Bool
-> Bool
-> Source
-> String
-> IO ()
cmdShowSpec language showMode checkMode shouldPrintTrace source ss
| Language bundle <- language
, fragment <- bundleFragment bundle
, modules <- bundleModules bundle
= cmdParseCheckExp fragment modules mode shouldPrintTrace True source ss
>>= goResult fragment
where
mode = case checkMode of
True -> Synth
False -> Recon
goResult fragment (Just x, Just ct)
= let annot = annotOfExp x
t = annotType annot
eff = annotEffect annot
clo = annotClosure annot
features = profileFeatures $ fragmentProfile fragment
in case showMode of
ShowSpecAll
-> do outDocLn $ ppr x
outDocLn $ text ":*:" <+> ppr t
when (featuresTrackedEffects features)
$ outDocLn $ text ":!:" <+> ppr eff
when (featuresTrackedClosures features)
$ outDocLn $ text ":$:" <+> ppr clo
when shouldPrintTrace
$ do outDocLn $ checkTraceDoc ct
outDoc (text "\n")
ShowSpecData
-> outDocLn $ ppr x <+> text "::" <+> ppr t
ShowSpecEffect
-> outDocLn $ ppr x <+> text ":!:" <+> ppr eff
ShowSpecClosure
-> outDocLn $ ppr x <+> text ":$:" <+> ppr clo
goResult _ _
= return ()
cmdExpRecon :: Language -> Source -> String -> IO ()
cmdExpRecon language source ss
| Language bundle <- language
, fragment <- bundleFragment bundle
, modules <- bundleModules bundle
= cmdParseCheckExp fragment modules Recon False True source ss
>>= goResult
where
goResult (Nothing, _ct)
= return ()
goResult (Just x, _ct)
= outDocLn $ ppr x
cmdShowWType :: Language -> Source -> String -> IO ()
cmdShowWType language source str
| Language bundle <- language
, fragment <- bundleFragment bundle
= let srcName = nameOfSource source
srcLine = lineStartOfSource source
toks = fragmentLexExp fragment srcName srcLine str
eTK = loadWitnessFromTokens fragment srcName toks
in case eTK of
Left err -> outDocLn $ ppr err
Right (t, k) -> outDocLn $ ppr t <+> text "::" <+> ppr k