git.iko.soy/Idris-dev
on master help sign in
Added test directory and a single test...
commit663c464326285b3cd38456ac18001554288b6439 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 22:13 (15 years ago) parent374fc26
7 files changed+207−1
compare with master
unifiedsplit
Makefile+1−1 test/Makefile+12 test/mktest.pl+21 test/runtest.pl+91 test/test001/expected+1 test/test001/run+4 test/test001/test001.idr+77
Makefile+1−1
@@ -14,7 +14,7 @@ configure: .PHONY
1414 cabal configure
1515
1616test : .PHONY
17− echo "Yes, probably should write tests."
17+ make -C test
1818
1919linecount : .PHONY
2020 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+