c6c3901 · Idris-dev · git.iko.soy

tutorial/Makefile+1−1

compare with master

unifiedsplit

@@ -3,7 +3,7 @@ PAPER = idris-tutorial

3all: ${PAPER}.pdf

4

5TEXFILES = ${PAPER}.tex intro.tex starting.tex miscellany.tex typesfuns.tex \

6− classes.tex modules.tex

6+ classes.tex modules.tex interp.tex

7

8DIAGS =

9

tutorial/examples/interp.idrnew file+68

@@ -0,0 +1,68 @@

1+module main;

2+

3+data Ty = TyInt | TyBool| TyFun Ty Ty;

4+

5+interpTy : Ty -> Set;

6+interpTy TyInt = Int;

7+interpTy TyBool = Bool;

8+interpTy (TyFun s t) = interpTy s -> interpTy t;

9+

10+using (G : Vect Ty n) {

11+

12+ data Env : Vect Ty n -> Set where

13+ Nil : Env Nil

14+ | (::) : interpTy a -> Env G -> Env (a :: G);

15+

16+ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17+ stop : HasType fO (t :: G) t

18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t;

19+

20+ lookup : HasType i G t -> Env G -> interpTy t;

21+ lookup stop (x :: xs) = x;

22+ lookup (pop k) (x :: xs) = lookup k xs;

23+

24+ data Expr : Vect Ty n -> Ty -> Set where

25+ Var : HasType i G t -> Expr G t

26+ | Val : (x : Int) -> Expr G TyInt

27+ | Lam : Expr (a :: G) t -> Expr G (TyFun a t)

28+ | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29+ | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30+ Expr G c

31+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;

32+

33+ interp : Env G -> {static} Expr G t -> interpTy t;

34+ interp env (Var i) = lookup i env;

35+ interp env (Val x) = x;

36+ interp env (Lam sc) = \x => interp (x :: env) sc;

37+ interp env (App f s) = (interp env f) (interp env s);

38+ interp env (Op op x y) = op (interp env x) (interp env y);

39+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);

40+

41+ eId : Expr G (TyFun TyInt TyInt);

42+ eId = Lam (Var stop);

43+

44+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

45+ eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));

46+

47+ eDouble : Expr G (TyFun TyInt TyInt);

48+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop));

49+

50+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

51+ app = \f, a => App f a;

52+

53+ fact : Expr G (TyFun TyInt TyInt);

54+ fact = Lam (If (Op (==) (Var stop) (Val 0))

55+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)));

56+

57+}

58+

59+testFac : Int;

60+testFac = interp [] fact 4;

61+

62+main : IO ();

63+main = do { putStr "Enter a number: ";

64+ x <- getLine;

65+ print (interp [] fact (prim__strToInt x));

66+ };

67+

68+

tutorial/idris-tutorial.tex+3−2

@@ -24,17 +24,18 @@

24\input{typesfuns}

25\input{classes}

26\input{modules}

27+\input{interp}

27

28

28%Planned sections

29%Planned sections

29

30

30−\section{Example: The Well-Typed Interpreter}

31\section{Views}

32\section{Theorem Proving}

33\section{Provisional Definitions}

34\section{Syntax Extensions}

35%\section{Example: A verified binary adder}

36

37−\input{miscellany}

37+%\input{miscellany}

38+\section{Further Reading}

38

39

39\bibliographystyle{abbrv}

40\bibliographystyle{abbrv}

40\bibliography{literature.bib}

41\bibliography{literature.bib}

tutorial/intro.tex+1−1

@@ -59,5 +59,5 @@ verifying systems software.

59

60This tutorial includes some example code. The files are available in the \Idris{} distribution,

61so that you can try them out easily,

62−under \texttt{idris-tutorial/examples}. However, it is strongly recommended that you

62+under \texttt{tutorial/examples}. However, it is strongly recommended that you

63type them in yourself, rather than simply loading and reading them.

tutorial/miscellany.tex−1

@@ -3,7 +3,6 @@

3Small things which don't quite fit elsewhere:

4

5\begin{itemize}

6−\item Namespaces (other than modules)

7\item Literate programming

6\item Literate programming

8\item Totality checking

7\item Totality checking

9\item Foreign functions

8\item Foreign functions