使用新后端构建 Idris 2

The way to extend Idris 2 with new backends is to use it as a library. The module Idris.Driver exports the function mainWithCodegens, that takes a list of (String, Codegen), starting idris with these codegens in addition to the built-in ones. The first codegen in the list will be set as the default codegen.

入门

要将 Idris 2 用作库，您需要自托管安装，然后安装 idris2api 库（位于 Idris2 存储库的顶层）

make install-api

接下来创建一个文件，包含以下内容

module Main

import Core.Context
import Compiler.Common
import Idris.Driver
import Idris.Syntax

compile :
  Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
  (tmpDir : String) -> (execDir : String) ->
  ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile syn defs tmp dir term file
  = do coreLift $ putStrLn "I'd rather not."
       pure Nothing

execute :
  Ref Ctxt Defs -> Ref Syn SyntaxInfo ->
  (execDir : String) -> ClosedTerm -> Core ()
execute defs syn dir term = do coreLift $ putStrLn "Maybe in an hour."

lazyCodegen : Codegen
lazyCodegen = MkCG compile execute Nothing Nothing

main : IO ()
main = mainWithCodegens [("lazy", lazyCodegen)]

构建它

$ idris2 -p idris2 -p contrib -p network Lazy.idr -o lazy-idris2

现在您有了一个带有附加后端的 idris2 。

$ ./build/exec/lazy-idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.2.0-bd9498c00
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
With codegen for: lazy
Main>

不过，它不会过分急于用新的后端实际编译任何代码

$ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
I'd rather not.
$

关于目录

代码生成器可以假设 tmpDir 和 outputDir 都存在。 tmpDir 用于临时文件，而 outputDir 是放置所需输出文件的位置。默认情况下， tmpDir 和 outputDir 指向同一个目录（ build/exec ）。可以从包描述（参见 包 部分）或通过命令行选项（在 idris2 --help 中列出）设置目录。