module DDC.Core.Load
( C.AnTEC (..)
, Error (..)
, Mode (..)
, CheckTrace (..)
, loadModuleFromFile
, loadModuleFromString
, loadModuleFromTokens
, loadExpFromString
, loadExpFromTokens
, loadTypeFromString
, loadTypeFromTokens
, loadWitnessFromString
, loadWitnessFromTokens)
where
import DDC.Core.Transform.SpreadX
import DDC.Core.Fragment.Profile
import DDC.Core.Lexer.Tokens
import DDC.Core.Check (Mode(..), CheckTrace)
import DDC.Core.Exp
import DDC.Core.Annot.AnT (AnT)
import DDC.Type.Transform.SpreadT
import DDC.Type.Universe
import DDC.Core.Module
import DDC.Base.Pretty
import DDC.Data.Token
import DDC.Core.Fragment (Fragment)
import qualified DDC.Core.Fragment as F
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 err
= ErrorRead !String
| ErrorParser !BP.ParseError
| ErrorCheckType !(T.Error n)
| ErrorCheckExp !(C.Error BP.SourcePos n)
| ErrorCompliance !(F.Error (C.AnTEC BP.SourcePos n) n)
| ErrorFragment !(err (C.AnTEC BP.SourcePos n))
instance ( Eq n, Show n, Pretty n
, Pretty (err (C.AnTEC BP.SourcePos n)))
=> Pretty (Error n err) 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' ]
ErrorFragment err'
-> vcat [ text "During fragment specific check."
, indent 2 $ ppr err' ]
loadModuleFromFile
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> FilePath
-> Mode n
-> IO ( Either (Error n err)
(Module (C.AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
loadModuleFromFile fragment filePath mode
= do
exists <- doesFileExist filePath
if not exists
then return ( Left $ ErrorRead $ "No such file '" ++ filePath ++ "'"
, Nothing)
else do
src <- readFile filePath
let toks = (F.fragmentLexModule fragment) filePath 1 src
return $ loadModuleFromTokens fragment filePath mode toks
loadModuleFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> FilePath
-> Int
-> Mode n
-> String
-> ( Either (Error n err)
(Module (C.AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
loadModuleFromString fragment filePath lineStart mode src
= do let toks = F.fragmentLexModule fragment filePath lineStart src
loadModuleFromTokens fragment filePath mode toks
loadModuleFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> FilePath
-> Mode n
-> [Token (Tok n)]
-> ( Either (Error n err)
(Module (C.AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
loadModuleFromTokens fragment sourceName mode toks'
= goParse toks'
where
profile = F.fragmentProfile fragment
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), Nothing)
Right mm -> goCheckType (spreadX kenv tenv mm)
goCheckType mm
= case C.checkModule config mm mode of
(Left err, ct) -> (Left (ErrorCheckExp err), Just ct)
(Right mm', ct) -> goCheckCompliance ct mm'
goCheckCompliance ct mm
= case F.complies profile mm of
Just err -> (Left (ErrorCompliance err), Just ct)
Nothing -> goCheckFragment ct mm
goCheckFragment ct mm
= case F.fragmentCheckModule fragment mm of
Just err -> (Left (ErrorFragment err), Just ct)
Nothing -> (Right mm, Just ct)
loadExpFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> Map ModuleName (Module (C.AnTEC () n) n)
-> FilePath
-> Mode n
-> String
-> ( Either (Error n err)
(Exp (C.AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
loadExpFromString fragment modules sourceName mode src
= do let toks = F.fragmentLexExp fragment sourceName 1 src
loadExpFromTokens fragment modules sourceName mode toks
loadExpFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> Map ModuleName (Module (C.AnTEC () n) n)
-> FilePath
-> Mode n
-> [Token (Tok n)]
-> ( Either (Error n err)
(Exp (C.AnTEC BP.SourcePos n) n)
, Maybe CheckTrace)
loadExpFromTokens fragment modules sourceName mode toks'
= goParse toks'
where
profile = F.fragmentProfile fragment
config = C.configOfProfile profile
kenv = modulesExportTypes modules $ profilePrimKinds profile
tenv = modulesExportValues modules $ profilePrimTypes profile
goParse toks
= case BP.runTokenParser describeTok sourceName
(C.pExp (C.contextOfProfile profile))
toks of
Left err -> (Left (ErrorParser err), Nothing)
Right t -> goCheckType (spreadX kenv tenv t)
goCheckType x
= case C.checkExp config kenv tenv x mode of
(Left err, ct) -> (Left (ErrorCheckExp err), Just ct)
(Right (x', _, _, _), ct) -> goCheckCompliance ct x'
goCheckCompliance ct x
= case F.compliesWithEnvs profile kenv tenv x of
Just err -> (Left (ErrorCompliance err), Just ct)
Nothing -> goCheckFragment ct x
goCheckFragment ct x
= case F.fragmentCheckExp fragment x of
Just err -> (Left (ErrorFragment err), Just ct)
Nothing -> (Right x, Just ct)
loadTypeFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> Universe
-> FilePath
-> String
-> Either (Error n err)
(Type n, Kind n)
loadTypeFromString fragment uni sourceName str
= do let toks = F.fragmentLexExp fragment sourceName 1 str
loadTypeFromTokens fragment uni sourceName toks
loadTypeFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> Universe
-> FilePath
-> [Token (Tok n)]
-> Either (Error n err)
(Type n, Kind n)
loadTypeFromTokens fragment uni sourceName toks'
= goParse toks'
where
profile = F.fragmentProfile fragment
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 uni t of
Left err -> Left (ErrorCheckType err)
Right (t', k) -> Right (t', k)
loadWitnessFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> FilePath
-> String
-> Either (Error n err)
(Witness (AnT BP.SourcePos n) n, Type n)
loadWitnessFromString fragment sourceName str
= do let toks = F.fragmentLexExp fragment sourceName 1 str
loadWitnessFromTokens fragment sourceName toks
loadWitnessFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Fragment n err
-> FilePath
-> [Token (Tok n)]
-> Either (Error n err)
(Witness (AnT BP.SourcePos n) n, Type n)
loadWitnessFromTokens fragment sourceName toks'
= goParse toks'
where
profile = F.fragmentProfile fragment
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)