663c464 · Idris-dev · git.iko.soy

Makefile+1−1

compare with master

unifiedsplit

@@ -14,7 +14,7 @@ configure: .PHONY

14 cabal configure

15

16test : .PHONY

17− echo "Yes, probably should write tests."

17+ make -C test

18

19linecount : .PHONY

20 wc -l src/Idris/*.hs src/Core/*.hs

test/Makefilenew file+12

@@ -0,0 +1,12 @@

1+test:

2+ perl ./runtest.pl all

3+

4+update:

5+ perl ./runtest.pl all -u

6+

7+diff:

8+ perl ./runtest.pl all -d

9+

10+distclean:

11+ rm -f *~

12+ rm -f */output

test/mktest.plnew file+21

@@ -0,0 +1,21 @@

1+#!/usr/bin/perl

2+

3+if ($#ARGV>=0) {

4+ $test=shift(@ARGV);

5+} else {

6+ print "What's its name?\n";

7+ exit;

8+}

9+

10+mkdir($test);

11+

12+chdir($test);

13+open(FOO,">run");

14+

15+print FOO "#!/bin/bash\n";

16+print FOO "idris $test.idr -o $test\n";

17+print FOO "./$test\n";print FOO "rm -f $test\n";

18+

19+close(FOO);

20+

21+system("chmod +x run");

test/runtest.plnew file+91

@@ -0,0 +1,91 @@

1+#!/usr/bin/perl

2+

3+my $exitstatus = 0;

4+

5+sub runtest {

6+ my ($test, $update) = @_;

7+

8+ chdir($test);

9+

10+ print "Running $test...";

11+ $got = `sh ./run`;

12+ $exp = `cat expected`;

13+

14+ open(OUT,">output");

15+ print OUT $got;

16+ close(OUT);

17+

18+# $ok = system("diff output expected &> /dev/null");

19+# Mangle newlines in $got and $exp

20+ $got =~ s/\r\n/\n/g;

21+ $exp =~ s/\r\n/\n/g;

22+

23+ if ($got eq $exp) {

24+ print "success\n";

25+ } else {

26+ if ($update == 0) {

27+ $exitstatus = 1;

28+ print "FAILURE\n";

29+ } else {

30+ system("cp output expected");

31+ print "UPDATED\n";

32+ }

33+ }

34+ chdir("..");

35+}

36+

37+if ($#ARGV>=0) {

38+ $test=shift(@ARGV);

39+ if ($test eq "all") {

40+ opendir(DIR, ".");

41+ @list = readdir(DIR);

42+ foreach $file (@list) {

43+ if ($file =~ /^test/) {

44+ push(@tests,$file);

45+ }

46+ }

47+ @tests = sort @tests;

48+ }

49+ else

50+ {

51+ push(@tests, $test);

52+ }

53+ @opts = @ARGV;

54+} else {

55+ print "Give a test name, or 'all' to run all.\n";

56+ exit;

57+}

58+

59+$update=0;

60+$diff=0;

61+$show=0;

62+

63+while ($opt=shift(@opts)) {

64+ if ($opt eq "-u") { $update = 1; }

65+ if ($opt eq "-d") { $diff = 1; }

66+ if ($opt eq "-s") { $show = 1; }

67+}

68+

69+foreach $test (@tests) {

70+

71+ if ($diff == 0 && $show == 0) {

72+ runtest($test,$update);

73+ }

74+ else {

75+ chdir($test);

76+

77+ if ($show == 1) {

78+ system("cat output");

79+ }

80+ if ($diff == 1) {

81+ print "Differences in $test:\n";

82+ $ok = system("diff output expected");

83+ if ($ok == 0) {

84+ print "No differences found.\n";

85+ }

86+ }

87+ chdir("..");

88+ }

89+

90+}

91+exit $exitstatus;

test/test001/expectednew file+1

@@ -0,0 +1 @@

1+24

test/test001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris test001.idr -o test001

3+./test001

4+rm -f test001

test/test001/test001.idrnew file+77

@@ -0,0 +1,77 @@

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

2+

3+interpTy : Ty -> Set;

4+interpTy TyInt = Int;

5+interpTy TyBool = Bool;

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

7+

8+using (G : Vect Ty n) {

9+

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

11+ Empty : Env VNil

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

13+

14+ envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);

15+ envLookup fO (Extend x xs) = x;

16+ envLookup (fS i) (Extend x xs) = envLookup i xs;

17+

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

19+ Var : (i : Fin n) -> Expr G (vlookup i G)

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

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

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

23+ | Op : (Int -> Int -> interpTy c) ->

24+ Expr G TyInt -> Expr G TyInt -> Expr G c

25+ | Op' : (interpTy a -> interpTy b -> interpTy c) ->

26+ Expr G a -> Expr G b -> Expr G c

27+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

28+ | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;

29+

30+ interp : Env G -> [static] Expr G t -> interpTy t;

31+ interp env (Var i) = envLookup i env;

32+ interp env (Val x) = x;

33+ interp env (Lam sc) = \x => interp (Extend x env) sc;

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

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

36+ interp env (Op' op x y) = op (interp env x) (interp env y);

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

38+ interp env (Bind v f) = interp env (f (interp env v));

39+

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

41+ eId = Lam (Var fO);

42+

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

44+ eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

45+

46+-- eDouble : Expr G (TyFun TyInt TyInt);

47+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

48+

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

50+ eDouble = Lam (App (App eAdd (Var fO)) (Var fO));

51+

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

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

54+

55+ eFac : Expr G (TyFun TyInt TyInt);

56+ eFac = Lam (If (Op (==) (Var fO) (Val 0))

57+ (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));

58+

59+ -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

60+

61+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));

62+ eProg = Lam (Lam

63+ (Bind (App eDouble (Var (fS fO)))

64+ (\x => Bind (App eDouble (Var fO))

65+ (\y => Bind (App eDouble (Val x))

66+ (\z => App (App eAdd (Val y)) (Val z))))));

67+}

68+

69+test : Int;

70+test = interp Empty eProg 2 2;

71+

72+testFac : Int;

73+testFac = interp Empty eFac 4;

74+

75+main : IO ();

76+main = print testFac;

77+