Permalink
Browse files

Added test directory and a single test...

  • Loading branch information...
1 parent 374fc26 commit 663c464326285b3cd38456ac18001554288b6439 Edwin Brady committed Nov 17, 2011
Showing with 207 additions and 1 deletion.
  1. +1 −1 Makefile
  2. +12 −0 test/Makefile
  3. +21 −0 test/mktest.pl
  4. +91 −0 test/runtest.pl
  5. +1 −0 test/test001/expected
  6. +4 −0 test/test001/run
  7. +77 −0 test/test001/test001.idr
View
@@ -14,7 +14,7 @@ configure: .PHONY
cabal configure
test : .PHONY
- echo "Yes, probably should write tests."
+ make -C test
linecount : .PHONY
wc -l src/Idris/*.hs src/Core/*.hs
View
@@ -0,0 +1,12 @@
+test:
+ perl ./runtest.pl all
+
+update:
+ perl ./runtest.pl all -u
+
+diff:
+ perl ./runtest.pl all -d
+
+distclean:
+ rm -f *~
+ rm -f */output
View
@@ -0,0 +1,21 @@
+#!/usr/bin/perl
+
+if ($#ARGV>=0) {
+ $test=shift(@ARGV);
+} else {
+ print "What's its name?\n";
+ exit;
+}
+
+mkdir($test);
+
+chdir($test);
+open(FOO,">run");
+
+print FOO "#!/bin/bash\n";
+print FOO "idris $test.idr -o $test\n";
+print FOO "./$test\n";print FOO "rm -f $test\n";
+
+close(FOO);
+
+system("chmod +x run");
View
@@ -0,0 +1,91 @@
+#!/usr/bin/perl
+
+my $exitstatus = 0;
+
+sub runtest {
+ my ($test, $update) = @_;
+
+ chdir($test);
+
+ print "Running $test...";
+ $got = `sh ./run`;
+ $exp = `cat expected`;
+
+ open(OUT,">output");
+ print OUT $got;
+ close(OUT);
+
+# $ok = system("diff output expected &> /dev/null");
+# Mangle newlines in $got and $exp
+ $got =~ s/\r\n/\n/g;
+ $exp =~ s/\r\n/\n/g;
+
+ if ($got eq $exp) {
+ print "success\n";
+ } else {
+ if ($update == 0) {
+ $exitstatus = 1;
+ print "FAILURE\n";
+ } else {
+ system("cp output expected");
+ print "UPDATED\n";
+ }
+ }
+ chdir("..");
+}
+
+if ($#ARGV>=0) {
+ $test=shift(@ARGV);
+ if ($test eq "all") {
+ opendir(DIR, ".");
+ @list = readdir(DIR);
+ foreach $file (@list) {
+ if ($file =~ /^test/) {
+ push(@tests,$file);
+ }
+ }
+ @tests = sort @tests;
+ }
+ else
+ {
+ push(@tests, $test);
+ }
+ @opts = @ARGV;
+} else {
+ print "Give a test name, or 'all' to run all.\n";
+ exit;
+}
+
+$update=0;
+$diff=0;
+$show=0;
+
+while ($opt=shift(@opts)) {
+ if ($opt eq "-u") { $update = 1; }
+ if ($opt eq "-d") { $diff = 1; }
+ if ($opt eq "-s") { $show = 1; }
+}
+
+foreach $test (@tests) {
+
+ if ($diff == 0 && $show == 0) {
+ runtest($test,$update);
+ }
+ else {
+ chdir($test);
+
+ if ($show == 1) {
+ system("cat output");
+ }
+ if ($diff == 1) {
+ print "Differences in $test:\n";
+ $ok = system("diff output expected");
+ if ($ok == 0) {
+ print "No differences found.\n";
+ }
+ }
+ chdir("..");
+ }
+
+}
+exit $exitstatus;
View
@@ -0,0 +1 @@
+24
View
@@ -0,0 +1,4 @@
+#!/bin/bash
+idris test001.idr -o test001
+./test001
+rm -f test001
View
@@ -0,0 +1,77 @@
+data Ty = TyInt | TyBool| TyFun Ty Ty;
+
+interpTy : Ty -> Set;
+interpTy TyInt = Int;
+interpTy TyBool = Bool;
+interpTy (TyFun s t) = interpTy s -> interpTy t;
+
+using (G : Vect Ty n) {
+
+ data Env : Vect Ty n -> Set where
+ Empty : Env VNil
+ | Extend : interpTy a -> Env G -> Env (a :: G);
+
+ envLookup : (i : Fin n) -> Env G -> interpTy (vlookup i G);
+ envLookup fO (Extend x xs) = x;
+ envLookup (fS i) (Extend x xs) = envLookup i xs;
+
+ data Expr : Vect Ty n -> Ty -> Set where
+ Var : (i : Fin n) -> Expr G (vlookup i G)
+ | Val : (x : Int) -> 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
+ | Op : (Int -> Int -> interpTy c) ->
+ Expr G TyInt -> Expr G TyInt -> Expr G c
+ | Op' : (interpTy a -> interpTy b -> interpTy c) ->
+ Expr G a -> Expr G b -> Expr G c
+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a
+ | Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b;
+
+ interp : Env G -> [static] Expr G t -> interpTy t;
+ interp env (Var i) = envLookup i env;
+ interp env (Val x) = x;
+ interp env (Lam sc) = \x => interp (Extend 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 (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);
+ interp env (Bind v f) = interp env (f (interp env v));
+
+ eId : Expr G (TyFun TyInt TyInt);
+ eId = Lam (Var fO);
+
+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
+ eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
+
+-- eDouble : Expr G (TyFun TyInt TyInt);
+-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));
+
+ eDouble : Expr G (TyFun TyInt TyInt);
+ eDouble = Lam (App (App eAdd (Var fO)) (Var fO));
+
+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;
+ app = \f, a => App f a;
+
+ eFac : Expr G (TyFun TyInt TyInt);
+ eFac = Lam (If (Op (==) (Var fO) (Val 0))
+ (Val 1) (Op (*) (app eFac (Op (-) (Var fO) (Val 1))) (Var fO)));
+
+ -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2
+
+ eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt));
+ eProg = Lam (Lam
+ (Bind (App eDouble (Var (fS fO)))
+ (\x => Bind (App eDouble (Var fO))
+ (\y => Bind (App eDouble (Val x))
+ (\z => App (App eAdd (Val y)) (Val z))))));
+}
+
+test : Int;
+test = interp Empty eProg 2 2;
+
+testFac : Int;
+testFac = interp Empty eFac 4;
+
+main : IO ();
+main = print testFac;
+

0 comments on commit 663c464

Please sign in to comment.