@@ -4,15 +4,15 @@ Static Arguments and Partial Evaluation
5As of version 0.9.15, Idris has support for *partial evaluation* of
5As of version 0.9.15, Idris has support for *partial evaluation* of
6statically known arguments. This involves creating specialised versions
6statically known arguments. This involves creating specialised versions
7−of functions with arguments annotated as ``[static]``.
7+of functions with arguments annotated as ``%static``.
9(This is an implementation of the partial evaluator described in `this
9(This is an implementation of the partial evaluator described in `this
11paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
11paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
12Please refer to this for more precise definitions of what follows.)
12Please refer to this for more precise definitions of what follows.)
14−Partial evaluation is switched on by default. It can be disabled with
14+Partial evaluation is switched off by default since Idris 1.0. It can
15−the ``--no-partial-eval`` flag.
15+be enabled with the ``--partial-eval`` flag.
17Introductory Example
17Introductory Example
18--------------------
18--------------------
@@ -66,18 +66,18 @@ Automatic specialisation of ``pow``
66~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
68The trick is to mark the statically known arguments with the
68The trick is to mark the statically known arguments with the
69−``[static]`` flag:
69+``%static`` flag:
73− my_pow : Nat -> [static] Nat -> Nat
73+ my_pow : Nat -> %static Nat -> Nat
74 my_pow k Z = 1
74 my_pow k Z = 1
75 my_pow k (S j) = mult k (my_pow k j)
75 my_pow k (S j) = mult k (my_pow k j)
77When an argument is annotated in this way, Idris will try to create a
77When an argument is annotated in this way, Idris will try to create a
78specialised version whenever it accounts a call with a concrete value
78specialised version whenever it accounts a call with a concrete value
79(i.e. a constant, constructor form, or globally defined function) in a
79(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``
81defined as above, we can see the effect by typing ``:printdef powFn`` at
81defined as above, we can see the effect by typing ``:printdef powFn`` at
@@ -108,7 +108,7 @@ Specialising Type Classes
108-------------------------
108-------------------------
110Type class dictionaries are very often statically known, so Idris
110Type 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
112specialised versions of top level functions where the class is
112specialised versions of top level functions where the class is
113instantiated. For example, given:
113instantiated. For example, given:
@@ -177,7 +177,7 @@ writing ``map`` as follows:
180− my_map : [static] (a -> b) -> List a -> List b
180+ my_map : %static (a -> b) -> List a -> List b
181 my_map f [] = []
181 my_map f [] = []
182 my_map f (x :: xs) = f x :: my_map f xs
182 my_map f (x :: xs) = f x :: my_map f xs
@@ -246,11 +246,11 @@ Then, a function which calculates the factorial of its input:
246 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
246 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
248The interpreter's type is written as follows, marking the expression to
248The interpreter's type is written as follows, marking the expression to
249−be evaluated as ``[static]``:
249+be evaluated as ``%static``:
253− interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
253+ interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
255This means that if we write an Idris program to calculate a factorial by
255This means that if we write an Idris program to calculate a factorial by
256calling ``interp`` on ``eFac``, the resulting definition will be
256calling ``interp`` on ``eFac``, the resulting definition will be