Prepare for additional codegens

The idea is to make everything accessible via the API, so
codegen implementors will be able to reuse all infrastructure by calling
the appropriate function in Idris.Driver supplying their codegen.
This commit is contained in:
Niklas Larsson 2020-06-14 14:55:06 +02:00
parent 9f325945b9
commit 5221954aca
11 changed files with 311 additions and 254 deletions

View File

@ -60,6 +60,7 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Driver,
Idris.Elab.Implementation,
Idris.Elab.Interface,
Idris.Error,
@ -68,6 +69,7 @@ modules =
Idris.IDEMode.MakeClause,
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.SyntaxHighlight,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
@ -144,6 +146,7 @@ modules =
TTImp.WithClause,
Utils.Binary,
Utils.Either,
Utils.Hex,
Utils.Octal,
Utils.Shunting,

View File

@ -60,6 +60,7 @@ modules =
Idris.CommandLine,
Idris.Desugar,
Idris.Driver,
Idris.Elab.Implementation,
Idris.Elab.Interface,
Idris.Error,
@ -68,6 +69,7 @@ modules =
Idris.IDEMode.MakeClause,
Idris.IDEMode.Parser,
Idris.IDEMode.REPL,
Idris.IDEMode.SyntaxHighlight,
Idris.IDEMode.TokenLine,
Idris.IDEMode.Holes,
Idris.ModTree,
@ -119,6 +121,7 @@ modules =
TTImp.Elab.Quote,
TTImp.Elab.Record,
TTImp.Elab.Rewrite,
TTImp.Elab.RunElab,
TTImp.Elab.Term,
TTImp.Elab.Utils,
TTImp.Impossible,
@ -143,6 +146,7 @@ modules =
TTImp.WithClause,
Utils.Binary,
Utils.Either,
Utils.Hex,
Utils.Octal,
Utils.Shunting,

View File

@ -30,7 +30,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 33
ttcVersion = 34
export
checkTTCVersion : String -> Int -> Int -> Core ()

View File

@ -1619,7 +1619,7 @@ addDirective : {auto c : Ref Ctxt Defs} ->
String -> String -> Core ()
addDirective c str
= do defs <- get Ctxt
case getCG c of
case getCG (options defs) c of
Nothing => -- warn, rather than fail, because the CG may exist
-- but be unknown to this particular instance
coreLift $ putStrLn $ "Unknown code generator " ++ c

View File

@ -41,12 +41,14 @@ public export
data CG = Chez
| Racket
| Gambit
| Other String
export
Eq CG where
Chez == Chez = True
Racket == Racket = True
Gambit == Gambit = True
Other s == Other t = s == t
_ == _ = False
export
@ -54,19 +56,9 @@ Show CG where
show Chez = "chez"
show Racket = "racket"
show Gambit = "gambit"
show (Other s) = s
export
availableCGs : List (String, CG)
availableCGs
= [("chez", Chez),
("racket", Racket),
("gambit", Gambit)]
export
getCG : String -> Maybe CG
getCG cg = lookup (toLower cg) availableCGs
-- Name options, to be saved in TTC
public export
record PairNames where
constructor MkPairNs
@ -142,6 +134,19 @@ record Options where
rewritenames : Maybe RewriteNames
primnames : PrimNames
extensions : List LangExt
additionalCGs : List (String, CG)
export
availableCGs : Options -> List (String, CG)
availableCGs o
= [("chez", Chez),
("racket", Racket),
("gambit", Gambit)] ++ additionalCGs o
export
getCG : Options -> String -> Maybe CG
getCG o cg = lookup (toLower cg) (availableCGs o)
defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build"
@ -164,7 +169,7 @@ export
defaults : Options
defaults = MkOptions defaultDirs defaultPPrint defaultSession
defaultElab Nothing Nothing
(MkPrimNs Nothing Nothing Nothing)
(MkPrimNs Nothing Nothing Nothing) []
[]
-- Reset the options which are set by source files
@ -204,3 +209,7 @@ setExtension e = record { extensions $= (e ::) }
export
isExtension : LangExt -> Options -> Bool
isExtension e opts = e `elem` extensions opts
export
addCG : (String, CG) -> Options -> Options
addCG cg = record { additionalCGs $= (cg::) }

View File

@ -733,12 +733,15 @@ TTC CG where
toBuf b Chez = tag 0
toBuf b Racket = tag 2
toBuf b Gambit = tag 3
toBuf b (Other s) = do tag 4; toBuf b s
fromBuf b
= case !getTag of
0 => pure Chez
2 => pure Racket
3 => pure Gambit
4 => do s <- fromBuf b
pure (Other s)
_ => corrupt "CG"
export

239
src/Idris/Driver.idr Normal file
View File

@ -0,0 +1,239 @@
module Idris.Driver
import Compiler.Common
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.Unify
import Idris.CommandLine
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Data.List
import Data.So
import Data.Strings
import System
import System.Directory
import System.File
import Utils.Path
import Yaffle.Main
%default covering
findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
Core ()
updateEnv
= do defs <- get Ctxt
bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
Just p => setPrefix p
Nothing => setPrefix yprefix
bpath <- coreLift $ getEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ getEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ getEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
Just e => case getCG (options defs) e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
-- version
defs <- get Ctxt
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "support")
addLibDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "lib")
Just cwd <- coreLift $ currentDir
| Nothing => throw (InternalError "Can't get current directory")
addLibDir cwd
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
the (Core ()) $ case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
showInfo : {auto c : Ref Ctxt Defs}
-> {auto o : Ref ROpts REPLOpts}
-> List CLOpt
-> Core Bool
showInfo Nil = pure False
showInfo (BlodwenPaths :: _)
= do defs <- get Ctxt
iputStrLn (toString (dirs (options defs)))
pure True
showInfo (_::rest) = showInfo rest
tryYaffle : List CLOpt -> Core Bool
tryYaffle [] = pure False
tryYaffle (Yaffle f :: _) = do yaffleMain f []
pure True
tryYaffle (c :: cs) = tryYaffle cs
tryTTM : List CLOpt -> Core Bool
tryTTM [] = pure False
tryTTM (Metadata f :: _) = do dumpTTM f
pure True
tryTTM (c :: cs) = tryTTM cs
banner : String
banner = " ____ __ _ ___ \n" ++
" / _/___/ /____(_)____ |__ \\ \n" ++
" / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++
" _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++
" /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++
"\n" ++
"Welcome to Idris 2. Enjoy yourself!"
checkVerbose : List CLOpt -> Bool
checkVerbose [] = False
checkVerbose (Verbose :: _) = True
checkVerbose (_ :: xs) = checkVerbose xs
stMain : List (String, Codegen) -> List CLOpt -> Core ()
stMain cgs opts
= do False <- tryYaffle opts
| True => pure ()
False <- tryTTM opts
| True => pure ()
defs <- initDefs
let updated = foldl (\o, (s, _) => addCG (s, Other s) o) (options defs) cgs
c <- newRef Ctxt (record { options = updated } defs)
s <- newRef Syn initSyntax
addPrimitives
setWorkingDir "."
updateEnv
let ide = ideMode opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
let fname = findInput opts
o <- newRef ROpts (REPLOpts.defaultOpts fname outmode cgs)
finish <- showInfo opts
if finish
then pure ()
else do
-- If there's a --build or --install, just do that then quit
done <- processPackageOpts opts
when (not done) $
do True <- preOptions opts
| False => pure ()
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD initMetadata
updateREPLOpts
session <- getSession
when (not $ nobanner session) $ do
iputStrLn banner
when (isCons cgs) $ iputStrLn ("With codegen for: " ++
fastAppend (map (\(s, _) => s ++ " ") cgs))
fname <- if findipkg session
then findIpkg fname
else pure fname
setMainFile fname
the (Core ()) $ case fname of
Nothing => logTime "Loading prelude" $
when (not $ noprelude session) $
readPrelude True
Just f => logTime "Loading main file" $
(loadMainFile f >>= displayErrors)
doRepl <- postOptions opts
if doRepl then
if ide || ideSocket then
if not ideSocket
then do
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
let (host, port) = ideSocketModeAddress opts
f <- coreLift $ initIDESocketFile host port
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exitWith (ExitFailure 1)
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
repl {c} {u} {m}
showTimeRecord
else
-- exit with an error code if there was an error, otherwise
-- just exit
do ropts <- get ROpts
showTimeRecord
case errorLine ropts of
Nothing => pure ()
Just _ => coreLift $ exitWith (ExitFailure 1)
-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
= do putStrLn versionMsg
pure False
quitOpts (Help :: _)
= do putStrLn usage
pure False
quitOpts (ShowPrefix :: _)
= do putStrLn yprefix
pure False
quitOpts (_ :: opts) = quitOpts opts
export
mainWithCodegens : List (String, Codegen) -> IO ()
mainWithCodegens cgs = do Right opts <- getCmdOpts
| Left err => do putStrLn err
putStrLn usage
continue <- quitOpts opts
if continue
then
coreRun (stMain cgs opts)
(\err : Error => do putStrLn ("Uncaught error: " ++ show err)
exitWith (ExitFailure 1))
(\res => pure ())
else pure ()

View File

@ -1,232 +1,6 @@
module Main
import Core.Core
import Core.InitPrimitives
import Core.Metadata
import Core.Unify
import Idris.CommandLine
import Idris.IDEMode.REPL
import Idris.ModTree
import Idris.Package
import Idris.ProcessIdr
import Idris.REPL
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths
import Data.So
import Data.Strings
import System
import System.Directory
import System.File
import Utils.Path
import Yaffle.Main
%default covering
findInput : List CLOpt -> Maybe String
findInput [] = Nothing
findInput (InputFile f :: fs) = Just f
findInput (_ :: fs) = findInput fs
-- Add extra data from the "IDRIS2_x" environment variables
updateEnv : {auto c : Ref Ctxt Defs} ->
Core ()
updateEnv
= do bprefix <- coreLift $ getEnv "IDRIS2_PREFIX"
the (Core ()) $ case bprefix of
Just p => setPrefix p
Nothing => setPrefix yprefix
bpath <- coreLift $ getEnv "IDRIS2_PATH"
the (Core ()) $ case bpath of
Just path => do traverse_ addExtraDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
bdata <- coreLift $ getEnv "IDRIS2_DATA"
the (Core ()) $ case bdata of
Just path => do traverse_ addDataDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
blibs <- coreLift $ getEnv "IDRIS2_LIBS"
the (Core ()) $ case blibs of
Just path => do traverse_ addLibDir (map trim (split (==pathSeparator) path))
Nothing => pure ()
cg <- coreLift $ getEnv "IDRIS2_CG"
the (Core ()) $ case cg of
Just e => case getCG e of
Just cg => setCG cg
Nothing => throw (InternalError ("Unknown code generator " ++ show e))
Nothing => pure ()
-- IDRIS2_PATH goes first so that it overrides this if there's
-- any conflicts. In particular, that means that setting IDRIS2_PATH
-- for the tests means they test the local version not the installed
-- version
defs <- get Ctxt
addPkgDir "prelude"
addPkgDir "base"
addDataDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "support")
addLibDir (dir_prefix (dirs (options defs)) </>
("idris2-" ++ showVersion False version) </> "lib")
Just cwd <- coreLift $ currentDir
| Nothing => throw (InternalError "Can't get current directory")
addLibDir cwd
updateREPLOpts : {auto o : Ref ROpts REPLOpts} ->
Core ()
updateREPLOpts
= do opts <- get ROpts
ed <- coreLift $ getEnv "EDITOR"
the (Core ()) $ case ed of
Just e => put ROpts (record { editor = e } opts)
Nothing => pure ()
showInfo : {auto c : Ref Ctxt Defs}
-> {auto o : Ref ROpts REPLOpts}
-> List CLOpt
-> Core Bool
showInfo Nil = pure False
showInfo (BlodwenPaths :: _)
= do defs <- get Ctxt
iputStrLn (toString (dirs (options defs)))
pure True
showInfo (_::rest) = showInfo rest
tryYaffle : List CLOpt -> Core Bool
tryYaffle [] = pure False
tryYaffle (Yaffle f :: _) = do yaffleMain f []
pure True
tryYaffle (c :: cs) = tryYaffle cs
tryTTM : List CLOpt -> Core Bool
tryTTM [] = pure False
tryTTM (Metadata f :: _) = do dumpTTM f
pure True
tryTTM (c :: cs) = tryTTM cs
banner : String
banner = " ____ __ _ ___ \n" ++
" / _/___/ /____(_)____ |__ \\ \n" ++
" / // __ / ___/ / ___/ __/ / Version " ++ showVersion True version ++ "\n" ++
" _/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org \n" ++
" /___/\\__,_/_/ /_/____/ /____/ Type :? for help \n" ++
"\n" ++
"Welcome to Idris 2. Enjoy yourself!"
checkVerbose : List CLOpt -> Bool
checkVerbose [] = False
checkVerbose (Verbose :: _) = True
checkVerbose (_ :: xs) = checkVerbose xs
stMain : List CLOpt -> Core ()
stMain opts
= do False <- tryYaffle opts
| True => pure ()
False <- tryTTM opts
| True => pure ()
defs <- initDefs
c <- newRef Ctxt defs
s <- newRef Syn initSyntax
addPrimitives
setWorkingDir "."
updateEnv
let ide = ideMode opts
let ideSocket = ideModeSocket opts
let outmode = if ide then IDEMode 0 stdin stdout else REPL False
let fname = findInput opts
o <- newRef ROpts (REPLOpts.defaultOpts fname outmode)
finish <- showInfo opts
if finish
then pure ()
else do
-- If there's a --build or --install, just do that then quit
done <- processPackageOpts opts
when (not done) $
do True <- preOptions opts
| False => pure ()
when (checkVerbose opts) $ -- override Quiet if implicitly set
setOutput (REPL False)
u <- newRef UST initUState
m <- newRef MD initMetadata
updateREPLOpts
session <- getSession
when (not $ nobanner session) $
iputStrLn banner
fname <- if findipkg session
then findIpkg fname
else pure fname
setMainFile fname
the (Core ()) $ case fname of
Nothing => logTime "Loading prelude" $
when (not $ noprelude session) $
readPrelude True
Just f => logTime "Loading main file" $
(loadMainFile f >>= displayErrors)
doRepl <- postOptions opts
if doRepl then
if ide || ideSocket then
if not ideSocket
then do
setOutput (IDEMode 0 stdin stdout)
replIDE {c} {u} {m}
else do
let (host, port) = ideSocketModeAddress opts
f <- coreLift $ initIDESocketFile host port
case f of
Left err => do
coreLift $ putStrLn err
coreLift $ exitWith (ExitFailure 1)
Right file => do
setOutput (IDEMode 0 file file)
replIDE {c} {u} {m}
else do
repl {c} {u} {m}
showTimeRecord
else
-- exit with an error code if there was an error, otherwise
-- just exit
do ropts <- get ROpts
showTimeRecord
case errorLine ropts of
Nothing => pure ()
Just _ => coreLift $ exitWith (ExitFailure 1)
-- Run any options (such as --version or --help) which imply printing a
-- message then exiting. Returns wheter the program should continue
quitOpts : List CLOpt -> IO Bool
quitOpts [] = pure True
quitOpts (Version :: _)
= do putStrLn versionMsg
pure False
quitOpts (Help :: _)
= do putStrLn usage
pure False
quitOpts (ShowPrefix :: _)
= do putStrLn yprefix
pure False
quitOpts (_ :: opts) = quitOpts opts
import Idris.Driver
main : IO ()
main = do Right opts <- getCmdOpts
| Left err =>
do putStrLn err
putStrLn usage
continue <- quitOpts opts
if continue
then
coreRun (stMain opts)
(\err : Error =>
do putStrLn ("Uncaught error: " ++ show err)
exitWith (ExitFailure 1))
(\res => pure ())
else pure ()
main = mainWithCodegens []

View File

@ -153,7 +153,8 @@ setOpt (Editor e)
= do opts <- get ROpts
put ROpts (record { editor = e } opts)
setOpt (CG e)
= case getCG e of
= do defs <- get Ctxt
case getCG (options defs) e of
Just cg => setCG cg
Nothing => iputStrLn "No such code generator available"
@ -169,13 +170,18 @@ getOptions = do
]
export
findCG : {auto c : Ref Ctxt Defs} -> Core Codegen
findCG : {auto o : Ref ROpts REPLOpts} ->
{auto c : Ref Ctxt Defs} -> Core Codegen
findCG
= do defs <- get Ctxt
case codegen (session (options defs)) of
Chez => pure codegenChez
Racket => pure codegenRacket
Gambit => pure codegenGambit
Other s => case !(getCodegen s) of
Just cg => pure cg
Nothing => do coreLift $ putStrLn ("No such code generator: " ++ s)
coreLift $ exitWith (ExitFailure 1)
anyAt : (FC -> Bool) -> FC -> a -> Bool
anyAt p loc y = p loc
@ -433,6 +439,7 @@ execExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> Core REPLResult
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)

View File

@ -1,7 +1,9 @@
module Idris.REPLOpts
import Compiler.Common
import Idris.Syntax
import Data.List
import Data.Strings
import System.File
@ -23,11 +25,15 @@ record REPLOpts where
errorLine : Maybe Int
idemode : OutputMode
currentElabSource : String
-- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
-- better to stick it now.
extraCodegens : List (String, Codegen)
export
defaultOpts : Maybe String -> OutputMode -> REPLOpts
defaultOpts fname outmode
= MkREPLOpts False NormaliseAll fname "" "vim" Nothing outmode ""
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
defaultOpts fname outmode cgs
= MkREPLOpts False NormaliseAll fname "" "vim" Nothing outmode "" cgs
export
data ROpts : Type where
@ -94,3 +100,14 @@ getCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
getCurrentElabSource
= do opts <- get ROpts
pure (currentElabSource opts)
addCodegen : {auto o : Ref ROpts REPLOpts} ->
String -> Codegen -> Core ()
addCodegen s cg = do opts <- get ROpts
put ROpts (record { extraCodegens $= ((s,cg)::) } opts)
export
getCodegen : {auto o : Ref ROpts REPLOpts} ->
String -> Core (Maybe Codegen)
getCodegen s = do opts <- get ROpts
pure $ lookup s (extraCodegens opts)

View File

@ -62,13 +62,14 @@ preOptions (NoPrelude :: opts)
= do setSession (record { noprelude = True } !getSession)
preOptions opts
preOptions (SetCG e :: opts)
= case getCG e of
= do defs <- get Ctxt
case getCG (options defs) e of
Just cg => do setCG cg
preOptions opts
Nothing =>
do coreLift $ putStrLn "No such code generator"
coreLift $ putStrLn $ "Code generators available: " ++
showSep ", " (map fst availableCGs)
showSep ", " (map fst (availableCGs (options defs)))
coreLift $ exitWith (ExitFailure 1)
preOptions (PkgPath p :: opts)
= do addPkgDir p