编译指示（Pragmas）

Idris2 支持多种编译指示（以 % 前缀标识）。有些编译指示会改变编译器行为，直到再次用同名指示恢复；有些则只作用于紧随其后的声明。还有一小部分编译指示直接作用于一个或多个参数，而不是后续代码（如下文 %name 指示）。

备注

本页内容仍在完善中。如果你了解未被描述的编译指示，欢迎提交 Pull Request！

全局编译指示（Global pragmas）

%language

启用语言扩展。目前仅支持 [1]。

%language ElabReflection

%default

设置函数的默认完备性要求，可选值为 total、covering 或 partial。默认值为 covering，除非使用命令行参数 --total，此时默认值为 total。

%builtin

%builtin Natural 指示会将递归/一元表示的自然数转换为原生 Integer 表示。

该指示在专门页面有详细说明，详见 内建（Builtins）。

%name

为特定类型向编译器提供建议名称，用于自动生成值名。可指定任意数量的名称，若单个定义需要多个名称，则按顺序使用。

data Foo = X | Y

%name Foo foo,bar

%ambiguity_depth

设置 Idris 解析嵌套歧义名称的最大深度，超出则放弃。默认值为 3，增大该值会影响编译性能。详见 有歧义名称的解析。

%totality_depth

设置 Idris 检查完备性时递归匹配构造子的最大层数。例如，若允许深入匹配构造子，则 Just xs 小于 Just (x :: xs)。默认值为 5，增大该值会降低检查速度。

%auto_implicit_depth

设置 auto 隐式参数的搜索深度，默认值为 50。

%logging

更改日志级别。详见 日志（Logging）。

%logging 1
%logging "elab" 5

%prefix_record_projections

配置是否为记录生成不带前导点的投影函数。默认开启。详见 记录展开（Record elaboration）。

%transform

在运行时用另一个实现替换函数。这样可以在类型检查时使用合适的实现，运行时则用高效版本。例如：

plus : Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S $ plus x y

%transform "plus" plus j k = integerToNat (natToInteger j + natToInteger j)

%unbound_implicits

配置是否为未绑定的小写名称自动添加隐式绑定。默认开启。详见 未绑定隐式参数（Unbound Implicits）。

%auto_lazy

配置编译器是否在必要时自动添加 delay 和 force。默认开启。

%search_timeout

设置表达式搜索超时时间（毫秒），默认值为 1000。

%search_timeout 1000

%nf_metavar_threshold

设置统一 meta 时允许的最大卡住应用次数，默认值为 25。

%cg

可以用 %cg 指示在源码中包含代码生成指令。例如，chez 后端下可用 %cg 代替命令行参数 --directive extraRuntime=mycode.ss：

%cg chez extraRuntime=mycode.ss

%cg 指示后跟代码生成器名称和指令，以换行结束。导入模块（包括传递导入）的指令会聚合。所有源码中的指令都会存储在模块中，但链接时只使用当前代码生成器的指令。

指令的聚合方式取决于代码生成器和具体指令。例如，Chez 代码生成器的 extraRuntime 指令会去重；JavaScript 后端若同时存在 minimal 和 compact，则优先采用 minimal。

各代码生成器可用指令详见 编译为可执行文件。

声明上的编译指示（Pragmas on declarations）

%deprecate

将后续定义标记为已弃用。每当该函数被使用时，Idris 会显示弃用警告。

%deprecate
foo : String -> String
foo x = x ++ "!"

bar : String
bar = foo "hello"

Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version.

你可以用代码文档（||| docs 三竖线）建议移除弃用函数调用的方案，相关文档会与警告一同显示。

||| Please use the @altFoo@ function from now on.
%deprecate
foo : String -> String
foo x = x ++ "!"

bar : String
bar = foo "hello"

Warning: Deprecation warning: Man.foo is deprecated and will be removed in a future version.
  Please use the @altFoo@ function from now on.

%inline

指示编译器在应用时内联后续定义。通常建议让编译器和后端根据预设规则优化代码，但如需强制某函数被内联，可用此指示。

%inline
foo : String -> String
foo x = x ++ "!"

%noinline

指示编译器在应用时不要内联后续定义。通常建议让编译器和后端根据预设规则优化代码，但如需强制某函数绝不被内联，可用此指示。

%noinline
foo : String -> String
foo x = x ++ "!"

%tcinline

指示编译器在完备性检查期间内联该函数。

%hide

隐藏某个定义，使其在被导入时不可见。对于需要重定义模块中的函数或类型但仍需导入该模块时尤其有用。

module MyNat

%hide Prelude.Nat
%hide Prelude.S
%hide Prelude.Nat

data Nat = Z | S Nat

如需自定义 fixity，也可隐藏原有 fixity 声明。

module MyNat

%hide Prelude.Ops.infixl.(+)

infixr 5 +

%unhide

%unhide 指示可取消之前用 %hide 隐藏的定义。

%unsafe

将类似 believe_me 的函数标记为不安全。该函数会以不同颜色高亮，提醒用户注意其使用。

%spec

根据参数列表对函数进行特化。

%spec a
identity : List a -> List a
identity [] = []
identity (x :: xs) = x :: identity xs

%foreign

声明外部函数。其后为缩进的字符串表达式块。详见 FFI 概述。

%foreign_impl

为其他文件中已有的 %foreign 添加实现。可用于为其他后端补充实现而无需修改原文件。若同一后端有多个声明，将采用最近加载模块中的实现。

%foreign_impl Prelude.IO.prim__fork "javascript:lambda:(proc) => { throw new Error() }"

%export

将 Idris 函数导出到底层宿主语言。每个后端的名称在缩进的字符串表达式块中指定，类似 %foreign。目前仅 JavaScript 后端支持该指示。

%export "javascript:addNat"
addNat : Nat -> Nat -> Nat
addNat a b = a + b

%nomangle

该指示已弃用，请用 %export 向后端暴露函数。

%hint

将函数标记为 auto 搜索用（详见 auto-隐式和接口 和 自动隐式参数）。Hint 在实例解析时内部使用，未命名实例会自动加上 %hint。

%defaulthint

将 hint 标记为无其他 hint 匹配时尝试。

%globalhint

全局 hint 类似于 %hint，但总会尝试，而 %hint 仅在返回类型匹配时尝试。

%extern

声明函数由外部实现，但由代码生成器补全实现而非指定名称。函数名需在代码生成器中显式处理。常用于 prelude 中如 prim__newIORef 之类的函数。

%macro

将返回 Elab monad 的函数标记为宏。该函数在表达式中被调用时，会在编译期运行，并用 elaboration 结果替换调用。

%start

%start 指示尚未实现。

%allow_overloads

该指示已不再被编译器使用。

内部（Internal）

这些指示用于 prelude，但用户程序通常不会用到。

%rewrite

指定 rewrite 语句使用的 Equal 类型和重写函数。

%rewrite Equal rewrite__impl

%pair

该指示用于 prelude，告知 auto 隐式搜索如何处理 pair。

%pair Pair fst snd

%integerLit

定义用于解释整数字面量的函数。在 prelude 中设为 fromInteger，因此字面量 2 会被 elaboration 为 fromInteger 2。

%integerLit fromInteger

%stringLit

定义用于解释字符串字面量的函数。在 prelude 中设为 fromString，因此字面量 "idris" 会被 elaboration 为 fromString "idris"。

%stringLit fromString

%charLit

定义用于解释字符字面量的函数。在 prelude 中设为 fromChar，因此字面量 `x` 会被 elaboration 为 fromChar 'x'。

%charLit fromChar

%doubleLit

定义用于解释带小数点数字字面量的函数。在 prelude 中设为 fromDouble，因此字面量 `2.0` 会被 elaboration 为 fromDouble 2.0。

%charLit fromDouble

反射字面量（Reflection Literals）

%TTImpLit

允许将带引号的表达式转换为用户自定义类型。

%TTImpLit fromTTImp

public export
data NatExpr : Type where
     Plus : NatExpr -> NatExpr -> NatExpr
     Mult : NatExpr -> NatExpr -> NatExpr
     Val : Nat -> NatExpr
     Var : String -> NatExpr

public export
natExpr : TTImp -> Elab NatExpr
natExpr `(~(l) + ~(r)) = [| Plus (natExpr l) (natExpr r) |]
natExpr `(~(l) * ~(r)) = [| Mult (natExpr l) (natExpr r) |]
natExpr `(fromInteger ~(IPrimVal _ (BI n))) = pure $ Val $ fromInteger n
natExpr (IVar _ (UN (Basic nm))) = pure $ Var nm
natExpr s = failAt (getFC s) "Invalid NatExpr"

%macro
fromTTImp : TTImp -> Elab NatExpr
fromTTImp = natExpr

export
natExprMacroTest : NatExpr
natExprMacroTest = `(1 + 2 + x)

%declsLit

允许将带引号的声明转换为用户自定义类型。

%nameLit

允许将带引号的名称转换为用户自定义类型。

表达式相关（Expressions）

出现在表达式内部的编译指示。

%runElab

%runElab 可用于顶层或表达式中。它接受一个 elaborator 脚本作为参数，在 Elab monad 中运行，可访问 Idris 的类型检查机制并生成代码。

%World

IO 用 world token 的类型。详见 World。

%MkWorld

IO 用 world token。详见 World。

%syntactic

%syntactic 可出现在 with 关键字后。它以语法方式抽象值而非按值抽象，在涉及大型类型时可显著加快 elaboration，但通用性较低。如果 with 很慢可尝试此指示。