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.Driver.Command.Compile
import DDC.Driver.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.Annot
import DDC.Core.Pretty
import DDC.Type.Transform.SpreadT
import DDC.Type.Universe
import DDC.Type.Equiv
import Control.Monad.Trans.Except
import Control.Monad.IO.Class
import Control.Monad
import System.FilePath
import System.Directory
import DDC.Build.Interface.Store (Store)
import qualified DDC.Base.Parser as BP
import qualified DDC.Type.Check as T
import qualified DDC.Core.Check as C
cmdCheckFromFile
:: Config
-> Store
-> FilePath
-> ExceptT String IO ()
cmdCheckFromFile config store filePath
| ".ds" <- takeExtension filePath
= cmdCheckSourceTetraFromFile config store filePath
| Just language <- languageOfExtension (takeExtension filePath)
= cmdCheckCoreFromFile config language filePath
| otherwise
= let ext = takeExtension filePath
in throwE $ "Cannot check '" ++ ext ++ "'files."
cmdCheckSourceTetraFromFile
:: Config
-> Store
-> FilePath
-> ExceptT String IO ()
cmdCheckSourceTetraFromFile config store filePath
= do
exists <- liftIO $ doesFileExist filePath
when (not exists)
$ throwE $ "No such file " ++ show filePath
cmdCompileRecursive config False store filePath
src <- liftIO $ readFile filePath
cmdCheckSourceTetraFromString config store (SourceFile filePath) src
cmdCheckSourceTetraFromString
:: Config
-> Store
-> Source
-> String
-> ExceptT String IO ()
cmdCheckSourceTetraFromString config store source str
= let
pmode = prettyModeOfConfig $ configPretty config
pipeLoad
= pipeText (nameOfSource source) (lineStartOfSource source) str
$ stageSourceTetraLoad config source store
[ PipeCoreOutput pmode SinkDiscard ]
in do
errs <- liftIO pipeLoad
case errs of
[] -> return ()
es -> throwE $ renderIndent $ vcat $ map ppr es
cmdCheckCoreFromFile
:: Config
-> Language
-> FilePath
-> ExceptT 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) -> throwE (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
-> ExceptT 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) -> throwE (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