ddc-core-0.3.1.1: DDC/Core/Load.hs
-- | \"Loading\" refers to the combination of parsing and type checking.
-- This is the easiest way to turn source tokens into a type-checked
-- abstract syntax tree.
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.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.Base.Parser as BP
import Data.Map.Strict (Map)
import System.Directory
-- | Things that can go wrong when loading a core thing.
data Error n
= ErrorRead !String
| ErrorParser !BP.ParseError
| ErrorCheckType !(T.Error n)
| ErrorCheckExp !(C.Error () n)
| ErrorCompliance !(I.Error 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' ]
-- Module ---------------------------------------------------------------------
-- | Parse and type check a core module from a file.
loadModuleFromFile
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> (String -> [Token (Tok n)]) -- ^ Function to lex the source file.
-> FilePath -- ^ File containing source code.
-> IO (Either (Error n)
(Module (C.AnTEC () n) n))
loadModuleFromFile profile lexSource filePath
= do
-- Check whether the file exists.
exists <- doesFileExist filePath
if not exists
then return $ Left $ ErrorRead "Cannot read file."
else do
-- Read the source file.
src <- readFile filePath
-- Lex the source.
let toks = lexSource src
return $ loadModuleFromTokens profile filePath toks
-- | Parse and type check a core module from a string.
loadModuleFromString
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> (String -> [Token (Tok n)]) -- ^ Function to lex the source file.
-> FilePath -- ^ Path to source file for error messages.
-> String -- ^ Program text.
-> Either (Error n) (Module (C.AnTEC () n) n)
loadModuleFromString profile lexSource filePath src
= loadModuleFromTokens profile filePath (lexSource src)
-- | Parse and type check a core module.
loadModuleFromTokens
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> FilePath -- ^ Path to source file for error messages.
-> [Token (Tok n)] -- ^ Source tokens.
-> Either (Error n) (Module (C.AnTEC () n) n)
loadModuleFromTokens profile sourceName toks'
= goParse toks'
where
-- Type checker config kind and type environments.
config = C.configOfProfile profile
kenv = profilePrimKinds profile
tenv = profilePrimTypes profile
-- Parse the tokens.
goParse toks
= case BP.runTokenParser describeTok sourceName C.pModule toks of
Left err -> Left (ErrorParser err)
Right mm -> goCheckType (spreadX kenv tenv mm)
-- Check that the module is type sound.
goCheckType mm
= case C.checkModule config mm of
Left err -> Left (ErrorCheckExp err)
Right mm' -> goCheckCompliance mm'
-- Check that the module compiles with the language fragment.
goCheckCompliance mm
= case I.complies profile mm of
Just err -> Left (ErrorCompliance err)
Nothing -> Right mm
-- Exp ------------------------------------------------------------------------
-- | Parse and check an expression
-- returning it along with its spec, effect and closure
loadExp
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> Map ModuleName (Module (C.AnTEC () n) n)
-- ^ Other modules currently in scope.
-- We add their exports to the environment.
-> FilePath -- ^ Path to source file for error messages.
-> [Token (Tok n)] -- ^ Source tokens.
-> Either (Error n)
(Exp (C.AnTEC () n) n)
loadExp profile modules sourceName toks'
= goParse toks'
where
-- Type checker profile, kind and type environments.
config = C.configOfProfile profile
kenv = modulesExportKinds modules $ profilePrimKinds profile
tenv = modulesExportTypes modules $ profilePrimTypes profile
-- Parse the tokens.
goParse toks
= case BP.runTokenParser describeTok sourceName C.pExp toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadX kenv tenv t)
-- Check the kind of the type.
goCheckType x
= case C.checkExp config kenv tenv x of
Left err -> Left (ErrorCheckExp err)
Right (x', _, _, _) -> goCheckCompliance x'
-- Check that the module compiles with the language fragment.
goCheckCompliance x
= case I.compliesWithEnvs profile kenv tenv x of
Just err -> Left (ErrorCompliance err)
Nothing -> Right x
-- Type -----------------------------------------------------------------------
-- | Parse and check a type,
-- returning it along with its kind.
loadType
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> FilePath -- ^ Path to source file for error messages.
-> [Token (Tok n)] -- ^ Source tokens.
-> Either (Error n)
(Type n, Kind n)
loadType profile sourceName toks'
= goParse toks'
where defs = profilePrimDataDefs profile
kenv = profilePrimKinds profile
-- Parse the tokens.
goParse toks
= case BP.runTokenParser describeTok sourceName C.pType toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadT kenv t)
-- Check the kind of the type.
goCheckType t
= case T.checkType defs kenv t of
Left err -> Left (ErrorCheckType err)
Right k -> Right (t, k)
-- Witness --------------------------------------------------------------------
-- | Parse and check a witness,
-- returning it along with its type.
loadWitness
:: (Eq n, Ord n, Show n, Pretty n)
=> Profile n -- ^ Language fragment profile.
-> FilePath -- ^ Path to source file for error messages.
-> [Token (Tok n)] -- ^ Source tokens.
-> Either (Error n)
(Witness n, Type n)
loadWitness profile sourceName toks'
= goParse toks'
where -- Type checker config, kind and type environments.
config = C.configOfProfile profile
kenv = profilePrimKinds profile
tenv = profilePrimTypes profile
-- Parse the tokens.
goParse toks
= case BP.runTokenParser describeTok sourceName C.pWitness toks of
Left err -> Left (ErrorParser err)
Right t -> goCheckType (spreadX kenv tenv t)
-- Check the kind of the type.
goCheckType w
= case C.checkWitness config kenv tenv w of
Left err -> Left (ErrorCheckExp err)
Right k -> Right (w, k)