@@ -4,7 +4,7 @@ Static Arguments and Partial Evaluation
44
55As of version 0.9.15, Idris has support for *partial evaluation* of
66statically known arguments. This involves creating specialised versions
7−of functions with arguments annotated as ``[static]``.
7+of functions with arguments annotated as ``%static``.
88
99(This is an implementation of the partial evaluator described in `this
1010ICFP 2010
@@ -66,18 +66,18 @@ Automatic specialisation of ``pow``
6666~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6767
6868The trick is to mark the statically known arguments with the
69−``[static]`` flag:
69+``%static`` flag:
7070
7171::
7272
73− my_pow : Nat -> [static] Nat -> Nat
73+ my_pow : Nat -> %static Nat -> Nat
7474 my_pow k Z = 1
7575 my_pow k (S j) = mult k (my_pow k j)
7676
7777When an argument is annotated in this way, Idris will try to create a
7878specialised version whenever it accounts a call with a concrete value
7979(i.e. a constant, constructor form, or globally defined function) in a
80−``[static]`` position. If ``my_pow`` is defined this way, and ``powFn``
80+``%static`` position. If ``my_pow`` is defined this way, and ``powFn``
8181defined as above, we can see the effect by typing ``:printdef powFn`` at
8282the REPL:
8383
@@ -108,7 +108,7 @@ Specialising Type Classes
108108-------------------------
109109
110110Type class dictionaries are very often statically known, so Idris
111−automatically marks any type class constraint as ``[static]`` and builds
111+automatically marks any type class constraint as ``%static`` and builds
112112specialised versions of top level functions where the class is
113113instantiated. For example, given:
114114
@@ -177,7 +177,7 @@ writing ``map`` as follows:
177177
178178::
179179
180− my_map : [static] (a -> b) -> List a -> List b
180+ my_map : %static (a -> b) -> List a -> List b
181181 my_map f [] = []
182182 my_map f (x :: xs) = f x :: my_map f xs
183183
@@ -246,11 +246,11 @@ Then, a function which calculates the factorial of its input:
246246 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
247247
248248The interpreter's type is written as follows, marking the expression to
249−be evaluated as ``[static]``:
249+be evaluated as ``%static``:
250250
251251::
252252
253− interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
253+ interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
254254
255255This means that if we write an Idris program to calculate a factorial by
256256calling ``interp`` on ``eFac``, the resulting definition will be