module DDC.Core.Load
( C.AnTEC (..)
, Error (..)
, loadModuleFromFile
, loadModuleFromString
, loadModuleFromTokens
, loadExp
, loadType
, loadWitness)
where
import DDC.Core.Transform.SpreadX
import DDC.Core.Fragment.Profile
import DDC.Core.Lexer.Tokens
import DDC.Core.Exp
import DDC.Core.Annot.AnT (AnT)
import DDC.Type.Transform.SpreadT
import DDC.Core.Module
import DDC.Base.Pretty
import DDC.Data.Token
import qualified DDC.Core.Fragment as I
import qualified DDC.Core.Parser as C
import qualified DDC.Core.Check as C
import qualified DDC.Type.Check as T
import qualified DDC.Type.Env as Env
import qualified DDC.Base.Parser as BP
import Data.Map.Strict (Map)
import System.Directory
data Error n
= ErrorRead !String
| ErrorParser !BP.ParseError
| ErrorCheckType !(T.Error n)
| ErrorCheckExp !(C.Error BP.SourcePos n)
| ErrorCompliance !(I.Error (C.AnTEC BP.SourcePos n) n)
deriving Show
instance (Eq n, Show n, Pretty n) => Pretty (Error n) where
ppr err
= case err of
ErrorRead str
-> vcat [ text "While reading."
, indent 2 $ text str ]
ErrorParser err'
-> vcat [ text "While parsing."
, indent 2 $ ppr err' ]
ErrorCheckType err'
-> vcat [ text "When checking type."
, indent 2 $ ppr err' ]
ErrorCheckExp err'
-> vcat [ text "When checking expression."
, indent 2 $ ppr err' ]
ErrorCompliance err'
-> vcat [ text "During fragment compliance check."
, indent 2 $ ppr err' ]
loadModuleFromFile
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> (String -> [Token (Tok n)])
-> FilePath
-> IO (Either (Error n)
(Module (C.AnTEC BP.SourcePos n) n))
loadModuleFromFile profile lexSource filePath
= do
exists <- doesFileExist filePath
if not exists
then return $ Left $ ErrorRead "Cannot read file."
else do
src <- readFile filePath
let toks = lexSource src
return $ loadModuleFromTokens profile filePath toks
loadModuleFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> (String -> [Token (Tok n)])
-> FilePath
-> String
-> Either (Error n)
(Module (C.AnTEC BP.SourcePos n) n)
loadModuleFromString profile lexSource filePath src
= loadModuleFromTokens profile filePath (lexSource src)
loadModuleFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> FilePath
-> [Token (Tok n)]
-> Either (Error n)
(Module (C.AnTEC BP.SourcePos n) n)
loadModuleFromTokens profile sourceName toks'
= goParse toks'
where
config = C.configOfProfile profile
kenv = profilePrimKinds profile
tenv = profilePrimTypes profile
goParse toks
= case BP.runTokenParser describeTok sourceName
(C.pModule (C.contextOfProfile profile))
toks of
Left err -> Left (ErrorParser err)
Right mm -> goCheckType (spreadX kenv tenv mm)
goCheckType mm
= case C.checkModule config mm of
Left err -> Left (ErrorCheckExp err)
Right mm' -> goCheckCompliance mm'
goCheckCompliance mm
= case I.complies profile mm of
Just err -> Left (ErrorCompliance err)
Nothing -> Right mm
loadExp
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> Map ModuleName (Module (C.AnTEC () n) n)
-> FilePath
-> [Token (Tok n)]
-> Either (Error n)
(Exp (C.AnTEC BP.SourcePos n) n)
loadExp profile modules sourceName toks'
= goParse toks'
where
config = C.configOfProfile profile
kenv = modulesExportKinds modules $ profilePrimKinds profile
tenv = modulesExportTypes modules $ profilePrimTypes profile
goParse toks
= case BP.runTokenParser describeTok sourceName
(C.pExp (C.contextOfProfile profile))
toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadX kenv tenv t)
goCheckType x
= case C.checkExp config kenv tenv x of
Left err -> Left (ErrorCheckExp err)
Right (x', _, _, _) -> goCheckCompliance x'
goCheckCompliance x
= case I.compliesWithEnvs profile kenv tenv x of
Just err -> Left (ErrorCompliance err)
Nothing -> Right x
loadType
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> FilePath
-> [Token (Tok n)]
-> Either (Error n)
(Type n, Kind n)
loadType profile sourceName toks'
= goParse toks'
where
goParse toks
= case BP.runTokenParser describeTok sourceName
(C.pType (C.contextOfProfile profile))
toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadT (profilePrimKinds profile) t)
goCheckType t
= case T.checkType (T.configOfProfile profile) Env.empty t of
Left err -> Left (ErrorCheckType err)
Right k -> Right (t, k)
loadWitness
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n
-> FilePath
-> [Token (Tok n)]
-> Either (Error n)
(Witness (AnT BP.SourcePos n) n, Type n)
loadWitness profile sourceName toks'
= goParse toks'
where
config = C.configOfProfile profile
kenv = profilePrimKinds profile
tenv = profilePrimTypes profile
goParse toks
= case BP.runTokenParser describeTok sourceName
(C.pWitness (C.contextOfProfile profile))
toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadX kenv tenv t)
goCheckType w
= case C.checkWitness config kenv tenv w of
Left err -> Left (ErrorCheckExp err)
Right (w', t) -> Right (w', t)