161deaa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2854 from jfdm/sphinx-doc-fixes

161deaaEdwin Brady11 years ago

docs/tutorial/interp.rst+9−8

compare with master

unifiedsplit

@@ -32,13 +32,14 @@ calculated just like any other value:

32 interpTy TyBool = Bool

33 interpTy (TyFun A T) = interpTy A -> interpTy T

35−We’re going to define a representation of our language in such a way

35+We're going to define a representation of our language in such a way

36−that only well-typed programs can be represented. We’ll index the

36+that only well-typed programs can be represented. We'll index the

37−representations of expressions by their type and the types of local

37+representations of expressions by their type, **and** the types of

38−variables (the context), which we’ll be using regularly as an implicit

38+local variables (the context). The context can be represented using

39+the ``Vect`` data type, and as it will be used regularly it will be

39−argument, so we define everything in a ``using`` block (keep in mind

40+represented as an implicit argument. To do so we define everything in

40−that everything after this point needs to be indented so as to be

41+a ``using`` block (keep in mind that everything after this point needs

41−inside the ``using`` block):

42+to be indented so as to be inside the ``using`` block):

43.. code-block:: idris

44.. code-block:: idris

@@ -153,7 +154,7 @@ that only the branch which is taken need be evaluated:

153Writing the Interpreter

154Writing the Interpreter

154=======================

155=======================

155

156

156−When we evaluate an ``Expr``, we’ll need to know the values in scope,

157+When we evaluate an ``Expr``, we'll need to know the values in scope,

157as well as their types. ``Env`` is an environment, indexed over the

158as well as their types. ``Env`` is an environment, indexed over the

158types in scope. Since an environment is just another form of list,

159types in scope. Since an environment is just another form of list,

159albeit with a strongly specified connection to the vector of local

160albeit with a strongly specified connection to the vector of local

docs/tutorial/modules.rst+12−2

@@ -212,14 +212,24 @@ using a ``parameters`` declaration, for example:

212 addAll z = x + y + z

213

214The effect of a ``parameters`` block is to add the declared parameters

215−to every function, type and data constructor within the block. Outside

215+to every function, type and data constructor within the

216+block. Specifically, adding the parameters to the front of the

216−the block, the parameters must be given explicitly:

217+argument list. Outside the block, the parameters must be given

218+explicitly. The ``addAll`` function, when called from the REPL, will

219+thus have the following type signature.

217

220

218::

221::

219

222

220 *params> :t addAll

223 *params> :t addAll

221 addAll : Nat -> Nat -> Nat -> Nat

224 addAll : Nat -> Nat -> Nat -> Nat

222

225

226+and the following definition.

227+

228+.. code-block:: idris

229+

230+ addAll : (x : Nat) -> (y : Nat) -> (z : Nat) -> Nat

231+ addAll x y z = x + y + z

232+

223Parameters blocks can be nested, and can also include data declarations,

233Parameters blocks can be nested, and can also include data declarations,

224in which case the parameters are added explicitly to all type and data

234in which case the parameters are added explicitly to all type and data

225constructors. They may also be dependent types with implicit arguments:

235constructors. They may also be dependent types with implicit arguments:

docs/tutorial/typesfuns.rst+4−6

@@ -445,7 +445,7 @@ are not given in applications of ``index``; their values can be

445inferred from the types of the ``Fin n`` and ``Vect n a``

446arguments. Any name beginning with a lower case letter which appears

447as a parameter or index in a

448−type declaration, which is not applied to any arguments, will

448+type declaration, which is not applied to any arguments, will

449*always* be automatically

450bound as an implicit argument. Implicit arguments can still be given

451explicitly in applications, using ``{a=value}`` and ``{n=value}``, for

@@ -1057,11 +1057,9 @@ Intermediate values can be calculated using ``let`` bindings:

1057

1058.. code-block:: idris

1059

1060− data Person = MkPerson String Int

1060+ mirror : List a -> List a

1061−

1061+ mirror xs = let xs' = reverse xs in

1062− showPerson : Person -> String

1062+ xs ++ xs'

1063− showPerson p = let MkPerson name age = p in

1064− name ++ " is " ++ show age ++ " years old"

1065

1063

1066We can do simple pattern matching in ``let`` bindings too. For

1064We can do simple pattern matching in ``let`` bindings too. For

1067example, we can extract fields from a record as follows, as well as by

1065example, we can extract fields from a record as follows, as well as by