mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 03:05:00 +03:00
Update interpreter section of crash course
This commit is contained in:
Edwin Brady
parent
a70c0a6ef6
commit
0be0c27d1a
@ -1,12 +1,12 @@
|
||||
$ idris interp.idr
|
||||
____ __ _
|
||||
/ _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.3.2
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
$ idris2 interp.idr
|
||||
____ __ _ ___
|
||||
/ _/___/ /____(_)____ |__ \
|
||||
/ // __ / ___/ / ___/ __/ / Version 0.1.0
|
||||
_/ // /_/ / / / (__ ) / __/ https://www.idris-lang.org
|
||||
/___/\__,_/_/ /_/____/ /____/
|
||||
|
||||
Type checking ./interp.idr
|
||||
*interp> :exec
|
||||
Welcome to Idris 2. Enjoy yourself!
|
||||
Main> :exec main
|
||||
Enter a number: 6
|
||||
720
|
||||
*interp>
|
||||
|
||||
|
||||
@ -4,8 +4,6 @@
|
||||
Example: The Well-Typed Interpreter
|
||||
***********************************
|
||||
|
||||
[NOT UPDATED FOR IDRIS 2 YET]
|
||||
|
||||
In this section, we’ll use the features we’ve seen so far to write a
|
||||
larger example, an interpreter for a simple functional programming
|
||||
language, with variables, function application, binary operators and
|
||||
@ -38,17 +36,15 @@ We're going to define a representation of our language in such a way
|
||||
that only well-typed programs can be represented. We'll index the
|
||||
representations of expressions by their type, **and** the types of
|
||||
local variables (the context). The context can be represented using
|
||||
the ``Vect`` data type, and as it will be used regularly it will be
|
||||
represented as an implicit argument. To do so we define everything in
|
||||
a ``using`` block (keep in mind that everything after this point needs
|
||||
to be indented so as to be inside the ``using`` block):
|
||||
the ``Vect`` data type, so we'll need to import ``Data.Vect`` at the top of our
|
||||
source file:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
using (G:Vect n Ty)
|
||||
import Data.Vect
|
||||
|
||||
Expressions are indexed by the types of the local variables, and the type of
|
||||
the expression itself:
|
||||
Expressions are indexed by the types of the local
|
||||
variables, and the type of the expression itself:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -59,28 +55,23 @@ The full representation of expressions is:
|
||||
.. code-block:: idris
|
||||
|
||||
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
|
||||
Stop : HasType FZ (t :: G) t
|
||||
Pop : HasType k G t -> HasType (FS k) (u :: G) t
|
||||
Stop : HasType FZ (t :: ctxt) t
|
||||
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
|
||||
|
||||
data Expr : Vect n Ty -> Ty -> Type where
|
||||
Var : HasType i G t -> Expr G t
|
||||
Val : (x : Integer) -> Expr G TyInt
|
||||
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
|
||||
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
|
||||
Var : HasType i ctxt t -> Expr ctxt t
|
||||
Val : (x : Integer) -> Expr ctxt TyInt
|
||||
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
|
||||
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
|
||||
Op : (interpTy a -> interpTy b -> interpTy c) ->
|
||||
Expr G a -> Expr G b -> Expr G c
|
||||
If : Expr G TyBool ->
|
||||
Lazy (Expr G a) ->
|
||||
Lazy (Expr G a) -> Expr G a
|
||||
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
|
||||
If : Expr ctxt TyBool ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Lazy (Expr ctxt a) -> Expr ctxt a
|
||||
|
||||
The code above makes use of the ``Vect`` and ``Fin`` types from the
|
||||
Idris standard library. We import them because they are not provided
|
||||
in the prelude:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
import Data.Vect
|
||||
import Data.Fin
|
||||
base libraries. ``Fin`` is available as part of ``Data.Vect``. Throughout,
|
||||
``ctxt`` refers to the local variable context.
|
||||
|
||||
Since expressions are indexed by their type, we can read the typing
|
||||
rules of the language from the definitions of the constructors. Let us
|
||||
@ -88,14 +79,14 @@ look at each constructor in turn.
|
||||
|
||||
We use a nameless representation for variables — they are *de Bruijn
|
||||
indexed*. Variables are represented by a proof of their membership in
|
||||
the context, ``HasType i G T``, which is a proof that variable ``i``
|
||||
in context ``G`` has type ``T``. This is defined as follows:
|
||||
the context, ``HasType i ctxt T``, which is a proof that variable ``i``
|
||||
in context ``ctxt`` has type ``T``. This is defined as follows:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
|
||||
Stop : HasType FZ (t :: G) t
|
||||
Pop : HasType k G t -> HasType (FS k) (u :: G) t
|
||||
Stop : HasType FZ (t :: ctxt) t
|
||||
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
|
||||
|
||||
We can treat *Stop* as a proof that the most recently defined variable
|
||||
is well-typed, and *Pop n* as a proof that, if the ``n``\ th most
|
||||
@ -106,7 +97,7 @@ the ``Var`` constructor:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Var : HasType i G t -> Expr G t
|
||||
Var : HasType i ctxt t -> Expr ctxt t
|
||||
|
||||
So, in an expression ``\x. \y. x y``, the variable ``x`` would have a
|
||||
de Bruijn index of 1, represented as ``Pop Stop``, and ``y 0``,
|
||||
@ -117,7 +108,7 @@ A value carries a concrete representation of an integer:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Val : (x : Integer) -> Expr G TyInt
|
||||
Val : (x : Integer) -> Expr ctxt TyInt
|
||||
|
||||
A lambda creates a function. In the scope of a function of type ``a ->
|
||||
t``, there is a new local variable of type ``a``, which is expressed
|
||||
@ -125,14 +116,14 @@ by the context index:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
Lam : Expr (a :: G) t -> Expr G (TyFun a t)
|
||||
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
|
||||
|
||||
Function application produces a value of type ``t`` given a function
|
||||
from ``a`` to ``t`` and a value of type ``a``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
App : Expr G (TyFun a t) -> Expr G a -> Expr G t
|
||||
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
|
||||
|
||||
We allow arbitrary binary operators, where the type of the operator
|
||||
informs what the types of the arguments must be:
|
||||
@ -140,7 +131,7 @@ informs what the types of the arguments must be:
|
||||
.. code-block:: idris
|
||||
|
||||
Op : (interpTy a -> interpTy b -> interpTy c) ->
|
||||
Expr G a -> Expr G b -> Expr G c
|
||||
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
|
||||
|
||||
Finally, ``If`` expressions make a choice given a boolean. Each branch
|
||||
must have the same type, and we will evaluate the branches lazily so
|
||||
@ -148,10 +139,10 @@ that only the branch which is taken need be evaluated:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
If : Expr G TyBool ->
|
||||
Lazy (Expr G a) ->
|
||||
Lazy (Expr G a) ->
|
||||
Expr G a
|
||||
If : Expr ctxt TyBool ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Expr ctxt a
|
||||
|
||||
Writing the Interpreter
|
||||
=======================
|
||||
@ -169,9 +160,9 @@ environment:
|
||||
|
||||
data Env : Vect n Ty -> Type where
|
||||
Nil : Env Nil
|
||||
(::) : interpTy a -> Env G -> Env (a :: G)
|
||||
(::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
|
||||
|
||||
lookup : HasType i G t -> Env G -> interpTy t
|
||||
lookup : HasType i ctxt t -> Env ctxt -> interpTy t
|
||||
lookup Stop (x :: xs) = x
|
||||
lookup (Pop k) (x :: xs) = lookup k xs
|
||||
|
||||
@ -181,7 +172,7 @@ specific environment:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
interp : Env G -> Expr G t -> interpTy t
|
||||
interp : Env ctxt -> Expr ctxt t -> interpTy t
|
||||
|
||||
The complete interpreter is defined as follows, for reference. For
|
||||
each constructor, we translate it into the corresponding Idris value:
|
||||
@ -246,7 +237,7 @@ We can make some simple test functions. Firstly, adding two inputs
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
|
||||
add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
|
||||
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
|
||||
|
||||
More interestingly, a factorial function ``fact``
|
||||
@ -255,7 +246,7 @@ can be written as:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fact : Expr G (TyFun TyInt TyInt)
|
||||
fact : Expr ctxt (TyFun TyInt TyInt)
|
||||
fact = Lam (If (Op (==) (Var Stop) (Val 0))
|
||||
(Val 1)
|
||||
(Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
|
||||
@ -279,7 +270,6 @@ one type to another if possible. Here, it converts a string to an
|
||||
integer, giving 0 if the input is invalid. An example run of this
|
||||
program at the Idris interactive environment is:
|
||||
|
||||
|
||||
.. _factrun:
|
||||
.. literalinclude:: ../listing/idris-prompt-interp.txt
|
||||
|
||||
|
||||
@ -4,8 +4,6 @@
|
||||
Packages
|
||||
********
|
||||
|
||||
[NOT UPDATED FOR IDRIS 2 YET]
|
||||
|
||||
Idris includes a simple build system for building packages and executables
|
||||
from a named package description file. These files can be used with the
|
||||
Idris compiler to manage the development process.
|
||||
@ -50,12 +48,12 @@ available to help with, for example, building packages, installing
|
||||
packages, and cleaning packages. For instance, given the ``maths``
|
||||
package from earlier we can use Idris as follows:
|
||||
|
||||
+ ``idris --build maths.ipkg`` will build all modules in the package
|
||||
+ ``idris2 --build maths.ipkg`` will build all modules in the package
|
||||
|
||||
+ ``idris --install maths.ipkg`` will install the package, making it
|
||||
+ ``idris2 --install maths.ipkg`` will install the package, making it
|
||||
accessible by other Idris libraries and programs.
|
||||
|
||||
+ ``idris --clean maths.ipkg`` will delete all intermediate code and
|
||||
+ ``idris2 --clean maths.ipkg`` will delete all intermediate code and
|
||||
executable files generated when building.
|
||||
|
||||
Once the maths package has been installed, the command line option
|
||||
@ -64,99 +62,7 @@ For example:
|
||||
|
||||
::
|
||||
|
||||
idris -p maths Main.idr
|
||||
|
||||
|
||||
Testing Idris Packages
|
||||
======================
|
||||
|
||||
The integrated build system includes a simple testing framework.
|
||||
This framework collects functions listed in the ``ipkg`` file under ``tests``.
|
||||
All test functions must return ``IO ()``.
|
||||
|
||||
When you enter ``idris --testpkg yourmodule.ipkg``,
|
||||
the build system creates a temporary file in a fresh environment on your machine
|
||||
by listing the ``tests`` functions under a single ``main`` function.
|
||||
It compiles this temporary file to an executable and then executes it.
|
||||
|
||||
The tests themselves are responsible for reporting their success or failure.
|
||||
Test functions commonly use ``putStrLn`` to report test results.
|
||||
The test framework does not impose any standards for reporting and consequently
|
||||
does not aggregate test results.
|
||||
|
||||
For example, lets take the following list of functions that are defined in a
|
||||
module called ``NumOps`` for a sample package ``maths``:
|
||||
|
||||
.. name: Math/NumOps.idr
|
||||
.. code-block:: idris
|
||||
|
||||
module Maths.NumOps
|
||||
|
||||
%access export -- to make functions under test visible
|
||||
|
||||
double : Num a => a -> a
|
||||
double a = a + a
|
||||
|
||||
triple : Num a => a -> a
|
||||
triple a = a + double a
|
||||
|
||||
|
||||
A simple test module, with a qualified name of ``Test.NumOps`` can be declared as:
|
||||
|
||||
.. name: Math/TestOps.idr
|
||||
.. code-block:: idris
|
||||
|
||||
module Test.NumOps
|
||||
|
||||
import Maths.NumOps
|
||||
|
||||
%access export -- to make the test functions visible
|
||||
|
||||
assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
|
||||
assertEq g e = if g == e
|
||||
then putStrLn "Test Passed"
|
||||
else putStrLn "Test Failed"
|
||||
|
||||
assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
|
||||
assertNotEq g e = if not (g == e)
|
||||
then putStrLn "Test Passed"
|
||||
else putStrLn "Test Failed"
|
||||
|
||||
testDouble : IO ()
|
||||
testDouble = assertEq (double 2) 4
|
||||
|
||||
testTriple : IO ()
|
||||
testTriple = assertNotEq (triple 2) 5
|
||||
|
||||
|
||||
The functions ``assertEq`` and ``assertNotEq`` are used to run expected passing,
|
||||
and failing, equality tests. The actual tests are ``testDouble`` and ``testTriple``,
|
||||
and are declared in the ``maths.ipkg`` file as follows:
|
||||
|
||||
::
|
||||
|
||||
package maths
|
||||
|
||||
modules = Maths.NumOps
|
||||
, Test.NumOps
|
||||
|
||||
tests = Test.NumOps.testDouble
|
||||
, Test.NumOps.testTriple
|
||||
|
||||
|
||||
The testing framework can then be invoked using ``idris --testpkg maths.ipkg``:
|
||||
|
||||
::
|
||||
|
||||
> idris --testpkg maths.ipkg
|
||||
Type checking ./Maths/NumOps.idr
|
||||
Type checking ./Test/NumOps.idr
|
||||
Type checking /var/folders/63/np5g0d5j54x1s0z12rf41wxm0000gp/T/idristests144128232716531729.idr
|
||||
Test Passed
|
||||
Test Passed
|
||||
|
||||
Note how both tests have reported success by printing ``Test Passed``
|
||||
as we arranged for with the ``assertEq`` and ``assertNoEq`` functions.
|
||||
idris2 -p maths Main.idr
|
||||
|
||||
Package Dependencies Using Atom
|
||||
===============================
|
||||
@ -179,9 +85,3 @@ a simple recipe for this trivial case:
|
||||
pkgs = pruviloj, lightyear
|
||||
|
||||
- In Atom, use the File menu to Open Folder myProject.
|
||||
|
||||
More information
|
||||
================
|
||||
|
||||
More details, including a complete listing of available fields, can be
|
||||
found in the reference manual in :ref:`ref-sect-packages`.
|
||||
|
||||
57
samples/Interp.idr
Normal file
57
samples/Interp.idr
Normal file
@ -0,0 +1,57 @@
|
||||
import Data.Vect
|
||||
|
||||
data Ty = TyInt | TyBool | TyFun Ty Ty
|
||||
|
||||
interpTy : Ty -> Type
|
||||
interpTy TyInt = Integer
|
||||
interpTy TyBool = Bool
|
||||
interpTy (TyFun a t) = interpTy a -> interpTy t
|
||||
|
||||
data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
|
||||
Stop : HasType FZ (t :: ctxt) t
|
||||
Pop : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t
|
||||
|
||||
data Expr : Vect n Ty -> Ty -> Type where
|
||||
Var : HasType i ctxt t -> Expr ctxt t
|
||||
Val : (x : Integer) -> Expr ctxt TyInt
|
||||
Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
|
||||
App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
|
||||
Op : (interpTy a -> interpTy b -> interpTy c) ->
|
||||
Expr ctxt a -> Expr ctxt b -> Expr ctxt c
|
||||
If : Expr ctxt TyBool ->
|
||||
Lazy (Expr ctxt a) ->
|
||||
Lazy (Expr ctxt a) -> Expr ctxt a
|
||||
|
||||
data Env : Vect n Ty -> Type where
|
||||
Nil : Env Nil
|
||||
(::) : interpTy a -> Env ctxt -> Env (a :: ctxt)
|
||||
|
||||
lookup : HasType i ctxt t -> Env ctxt -> interpTy t
|
||||
lookup Stop (x :: xs) = x
|
||||
lookup (Pop k) (x :: xs) = lookup k xs
|
||||
|
||||
interp : Env ctxt -> Expr ctxt t -> interpTy t
|
||||
interp env (Var i) = lookup i env
|
||||
interp env (Val x) = x
|
||||
interp env (Lam sc) = \x => interp (x :: env) sc
|
||||
interp env (App f s) = interp env f (interp env s)
|
||||
interp env (Op op x y) = op (interp env x) (interp env y)
|
||||
interp env (If x t e) = if interp env x then interp env t
|
||||
else interp env e
|
||||
|
||||
add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
|
||||
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
|
||||
|
||||
fact : Expr ctxt (TyFun TyInt TyInt)
|
||||
fact = Lam (If (Op (==) (Var Stop) (Val 0))
|
||||
(Val 1)
|
||||
(Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
|
||||
(Var Stop)))
|
||||
|
||||
main : IO ()
|
||||
main = do putStr "Enter a number: "
|
||||
x <- getLine
|
||||
printLn (interp [] fact (cast x))
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user