mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-10-26 17:33:47 +03:00
Added test framework (copied from Blodwen)
This commit is contained in:
Edwin Brady
parent
ef36ea1752
commit
77bf4c7c44
48
Makefile
Normal file
48
Makefile
Normal file
@ -0,0 +1,48 @@
|
||||
PREFIX = ${HOME}/.yaffle
|
||||
export YAFFLE_PATH = ${CURDIR}/prelude/build:${CURDIR}/base/build
|
||||
export YAFFLE_DATA = ${CURDIR}/support
|
||||
|
||||
.PHONY: ttimp yaffle prelude test base clean lib_clean
|
||||
|
||||
all: yaffle test
|
||||
|
||||
yaffle: src/YafflePaths.idr
|
||||
idris --build yaffle.ipkg
|
||||
|
||||
src/YafflePaths.idr:
|
||||
echo 'module YafflePaths; export yprefix : String; yprefix = "${PREFIX}"' > src/YafflePaths.idr
|
||||
|
||||
#prelude:
|
||||
# make -C prelude YAFFLE=../yaffle
|
||||
|
||||
#base: prelude
|
||||
# make -C base YAFFLE=../yaffle
|
||||
|
||||
#libs : prelude base
|
||||
|
||||
clean: lib_clean
|
||||
make -C src clean
|
||||
make -C tests clean
|
||||
rm -f runtests
|
||||
rm -f yaffle
|
||||
|
||||
lib_clean:
|
||||
# make -C prelude clean
|
||||
# make -C base clean
|
||||
|
||||
test:
|
||||
idris --build tests.ipkg
|
||||
make -C tests
|
||||
|
||||
#install:
|
||||
# mkdir -p ${PREFIX}/bin
|
||||
# mkdir -p ${PREFIX}/blodwen/support/chez
|
||||
# mkdir -p ${PREFIX}/blodwen/support/chicken
|
||||
# mkdir -p ${PREFIX}/blodwen/support/racket
|
||||
# make -C prelude install BLODWEN=../blodwen
|
||||
# make -C base install BLODWEN=../blodwen
|
||||
#
|
||||
# install blodwen ${PREFIX}/bin
|
||||
# install support/chez/* ${PREFIX}/blodwen/support/chez
|
||||
# install support/chicken/* ${PREFIX}/blodwen/support/chicken
|
||||
# install support/racket/* ${PREFIX}/blodwen/support/racket
|
||||
3
src/Makefile
Normal file
3
src/Makefile
Normal file
@ -0,0 +1,3 @@
|
||||
clean:
|
||||
rm -f YafflePaths.idr
|
||||
find . -name '*.ibc' | xargs rm -f
|
||||
@ -20,13 +20,24 @@ import Yaffle.REPL
|
||||
|
||||
import System
|
||||
|
||||
coreMain : String -> Core ()
|
||||
coreMain fname
|
||||
usage : String
|
||||
usage = "Usage: yaffle <input file> [--timing]"
|
||||
|
||||
processArgs : List String -> Core Bool
|
||||
processArgs [] = pure False
|
||||
processArgs ["--timing"] = pure True
|
||||
processArgs _
|
||||
= coreLift $ do putStrLn usage
|
||||
exitWith (ExitFailure 1)
|
||||
|
||||
coreMain : String -> List String -> Core ()
|
||||
coreMain fname args
|
||||
= do defs <- initDefs
|
||||
c <- newRef Ctxt defs
|
||||
u <- newRef UST initUState
|
||||
d <- getDirs
|
||||
setLogTimings True
|
||||
t <- processArgs args
|
||||
setLogTimings t
|
||||
case span (/= '.') fname of
|
||||
(_, ".ttc") => do coreLift $ putStrLn "Processing as TTC"
|
||||
readFromTTC {extra = ()} emptyFC True fname [] []
|
||||
@ -41,9 +52,9 @@ coreMain fname
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do [_, fname] <- getArgs
|
||||
| _ => do putStrLn "Usage: yaffle [input file]"
|
||||
= do (_ :: fname :: rest) <- getArgs
|
||||
| _ => do putStrLn usage
|
||||
exitWith (ExitFailure 1)
|
||||
coreRun defaultOpts (coreMain fname)
|
||||
coreRun defaultOpts (coreMain fname rest)
|
||||
(\err : Error => putStrLn ("Uncaught error: " ++ show err))
|
||||
(\res => pure ())
|
||||
|
||||
11
tests.ipkg
Normal file
11
tests.ipkg
Normal file
@ -0,0 +1,11 @@
|
||||
package runtests
|
||||
|
||||
pkgs = contrib
|
||||
|
||||
sourcedir = tests
|
||||
executable = runtests
|
||||
|
||||
opts = "--warnreach --partial-eval"
|
||||
|
||||
main = Main
|
||||
|
||||
48
tests/Main.idr
Normal file
48
tests/Main.idr
Normal file
@ -0,0 +1,48 @@
|
||||
module Main
|
||||
|
||||
import System
|
||||
|
||||
%default covering
|
||||
|
||||
ttimpTests : List String
|
||||
ttimpTests
|
||||
= ["test001", "test002", "test003",
|
||||
"perf001", "perf002", "perf003"]
|
||||
|
||||
chdir : String -> IO Bool
|
||||
chdir dir
|
||||
= do ok <- foreign FFI_C "chdir" (String -> IO Int) dir
|
||||
pure (ok == 0)
|
||||
|
||||
fail : String -> IO ()
|
||||
fail err
|
||||
= do putStrLn err
|
||||
exitWith (ExitFailure 1)
|
||||
|
||||
runTest : String -> String -> String -> IO Bool
|
||||
runTest dir prog test
|
||||
= do chdir (dir ++ "/" ++ test)
|
||||
putStr $ dir ++ "/" ++ test ++ ": "
|
||||
system $ "sh ./run " ++ prog ++ " > output"
|
||||
Right out <- readFile "output"
|
||||
| Left err => do print err
|
||||
pure False
|
||||
Right exp <- readFile "expected"
|
||||
| Left err => do print err
|
||||
pure False
|
||||
if (out == exp)
|
||||
then putStrLn "success"
|
||||
else putStrLn "FAILURE"
|
||||
chdir "../.."
|
||||
pure (out == exp)
|
||||
|
||||
main : IO ()
|
||||
main
|
||||
= do [_, ttimp] <- getArgs
|
||||
| _ => do putStrLn "Usage: runtests [ttimp path]"
|
||||
ttimps <- traverse (runTest "ttimp" ttimp) ttimpTests
|
||||
-- blods <- traverse (runTest "blodwen" blodwen) blodwenTests
|
||||
if (any not ttimps)
|
||||
then exitWith (ExitFailure 1)
|
||||
else exitWith ExitSuccess
|
||||
|
||||
8
tests/Makefile
Normal file
8
tests/Makefile
Normal file
@ -0,0 +1,8 @@
|
||||
YAFFLE = ../../../yaffle
|
||||
|
||||
test:
|
||||
../runtests $(YAFFLE)
|
||||
|
||||
clean:
|
||||
find . -name '*.ibc' | xargs rm -f
|
||||
find . -name 'output' | xargs rm -f
|
||||
37
tests/ttimp/perf001/bigsuc.yaff
Normal file
37
tests/ttimp/perf001/bigsuc.yaff
Normal file
@ -0,0 +1,37 @@
|
||||
-- The main purpose of this test is to ensure it runs instantly!
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z $y = y
|
||||
plus (S $k) $y = S (plus k y)
|
||||
|
||||
mult : Nat -> Nat -> Nat
|
||||
mult Z $y = Z
|
||||
mult (S $k) $y = plus y (mult k y)
|
||||
|
||||
five : Nat
|
||||
five = S (S (S (S (S Z))))
|
||||
|
||||
ten : Nat
|
||||
ten = plus five five
|
||||
|
||||
thousand : Nat
|
||||
thousand = mult ten (mult ten ten)
|
||||
|
||||
tenthousand : Nat
|
||||
tenthousand = mult ten thousand
|
||||
|
||||
fiftythousand : Nat
|
||||
fiftythousand = mult five tenthousand
|
||||
|
||||
hundredthousand : Nat
|
||||
hundredthousand = mult ten tenthousand
|
||||
|
||||
data IsSuc : Nat -> Type where
|
||||
Yes : IsSuc (S $k)
|
||||
|
||||
nonZero : IsSuc hundredthousand
|
||||
nonZero = Yes
|
||||
3
tests/ttimp/perf001/expected
Normal file
3
tests/ttimp/perf001/expected
Normal file
@ -0,0 +1,3 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Bye for now!
|
||||
3
tests/ttimp/perf001/run
Executable file
3
tests/ttimp/perf001/run
Executable file
@ -0,0 +1,3 @@
|
||||
echo ':q' | $1 bigsuc.yaff
|
||||
|
||||
rm -rf build
|
||||
87
tests/ttimp/perf002/BigVect.yaff
Normal file
87
tests/ttimp/perf002/BigVect.yaff
Normal file
@ -0,0 +1,87 @@
|
||||
data Bool : Type where
|
||||
False : Bool
|
||||
True : Bool
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
data Vect : Nat -> Type -> Type where
|
||||
Nil : Vect Z $a
|
||||
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
||||
|
||||
stuff : Vect ? Bool
|
||||
stuff = Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
|
||||
4
tests/ttimp/perf002/expected
Normal file
4
tests/ttimp/perf002/expected
Normal file
@ -0,0 +1,4 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Vect (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Main.Bool)
|
||||
Yaffle> Bye for now!
|
||||
2
tests/ttimp/perf002/input
Normal file
2
tests/ttimp/perf002/input
Normal file
@ -0,0 +1,2 @@
|
||||
:t stuff
|
||||
:q
|
||||
4
tests/ttimp/perf002/output
Normal file
4
tests/ttimp/perf002/output
Normal file
@ -0,0 +1,4 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> ((Main.Vect (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) Main.Bool)
|
||||
Yaffle> Bye for now!
|
||||
3
tests/ttimp/perf002/run
Executable file
3
tests/ttimp/perf002/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 BigVect.yaff < input
|
||||
|
||||
rm -rf build
|
||||
26
tests/ttimp/perf003/Id.yaff
Normal file
26
tests/ttimp/perf003/Id.yaff
Normal file
@ -0,0 +1,26 @@
|
||||
IdType : Type
|
||||
IdType = {0 a : Type} -> a -> a
|
||||
|
||||
id : IdType
|
||||
id = \ x : _ => x
|
||||
|
||||
idid : {0 a : Type} -> a -> a
|
||||
idid = id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
|
||||
idInt : Integer
|
||||
idInt = idid 94
|
||||
5
tests/ttimp/perf003/expected
Normal file
5
tests/ttimp/perf003/expected
Normal file
@ -0,0 +1,5 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> Integer
|
||||
Yaffle> 94
|
||||
Yaffle> Bye for now!
|
||||
3
tests/ttimp/perf003/input
Normal file
3
tests/ttimp/perf003/input
Normal file
@ -0,0 +1,3 @@
|
||||
:t idInt
|
||||
idInt
|
||||
:q
|
||||
3
tests/ttimp/perf003/run
Executable file
3
tests/ttimp/perf003/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 Id.yaff < input
|
||||
|
||||
rm -rf build
|
||||
79
tests/ttimp/test001/Interp.yaff
Normal file
79
tests/ttimp/test001/Interp.yaff
Normal file
@ -0,0 +1,79 @@
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z $y = y
|
||||
plus (S $k) $y = S (plus k y)
|
||||
|
||||
data Vect : Nat -> Type -> Type where
|
||||
Nil : Vect Z $a
|
||||
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
||||
|
||||
append : Vect $n $a -> Vect $m $a -> Vect (plus $n $m) $a
|
||||
append Nil $ys = ys
|
||||
append (Cons $x $xs) $ys = Cons x (append xs ys)
|
||||
|
||||
data Fin : Nat -> Type where
|
||||
FZ : Fin (S $k)
|
||||
FS : Fin $k -> Fin (S $k)
|
||||
|
||||
lookup : Fin $k -> Vect $k $ty -> $ty
|
||||
lookup FZ (Cons $t $ts) = t;
|
||||
lookup (FS $i) (Cons $t $ts) = lookup i ts;
|
||||
|
||||
-- As a larger example, we'll implement the well-typed interpreter.
|
||||
-- So we'll need to represent the types of our expression language:
|
||||
|
||||
data Ty : Type where
|
||||
Base : Type -> Ty
|
||||
Arrow : Ty -> Ty -> Ty
|
||||
|
||||
-- Ty can be translated to a host language type
|
||||
|
||||
interpTy : Ty -> Type
|
||||
interpTy (Base $t) = t
|
||||
interpTy (Arrow $s $t) = (argTy : interpTy s) -> interpTy t
|
||||
|
||||
data HasType : Fin $k -> Ty -> Vect $k Ty -> Type where
|
||||
Stop : HasType FZ $t (Cons $t $gam)
|
||||
Pop : HasType $i $t $gam -> HasType (FS $i) $t (Cons $u $gam)
|
||||
|
||||
-- Expressions in our language, indexed by their contexts and types:
|
||||
|
||||
data Lang : Vect $k Ty -> Ty -> Type where
|
||||
Var : HasType $i $t $gam -> Lang $gam $t
|
||||
Val : (x : interpTy $a) -> Lang $gam $a
|
||||
Lam : (scope : Lang (Cons $s $gam) $t) -> Lang $gam (Arrow $s $t)
|
||||
App : Lang $gam (Arrow $s $t) -> Lang $gam $s -> Lang $gam $t;
|
||||
Op : (interpTy $a -> interpTy $b -> interpTy $c) ->
|
||||
Lang $gam $a -> Lang $gam $b -> Lang $gam $c
|
||||
|
||||
data Env : Vect $n Ty -> Type where
|
||||
ENil : Env Nil
|
||||
ECons : (x : interpTy $a) -> Env $xs -> Env (Cons $a $xs)
|
||||
|
||||
-- Find a value in an environment
|
||||
lookupEnv : HasType $i $t $gam -> Env $gam -> interpTy $t
|
||||
lookupEnv Stop (ECons $x $xs) = x
|
||||
lookupEnv (Pop $var) (ECons $x $env) = lookupEnv var env
|
||||
|
||||
interp : Env $gam -> Lang $gam $t -> interpTy $t
|
||||
interp $env (Var $i) = lookupEnv i env
|
||||
interp $env (Val $x) = x
|
||||
interp $env (App $f $a) = interp env f (interp env a)
|
||||
interp $env (Lam {s = $s} $scope)
|
||||
= \var => interp (ECons var env) scope
|
||||
interp $env (Op $fn $x $y) = fn (interp env x) (interp env y)
|
||||
|
||||
testAdd : Lang $gam (Arrow (Base Nat) (Arrow (Base Nat) (Base Nat)))
|
||||
testAdd = Lam (Lam (Op plus (Var Stop) (Var (Pop Stop))))
|
||||
|
||||
testAdd2 : Lang $gam (Base Nat)
|
||||
testAdd2 = App (App testAdd (Val (S (S Z)))) (Val (S (S (S Z))))
|
||||
|
||||
test1 : Nat
|
||||
test1 = interp ENil testAdd (S (S Z)) (S (S Z))
|
||||
|
||||
test2 : Nat
|
||||
test2 = interp ENil testAdd2
|
||||
5
tests/ttimp/test001/expected
Normal file
5
tests/ttimp/test001/expected
Normal file
@ -0,0 +1,5 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> (Main.S (Main.S (Main.S (Main.S Main.Z))))
|
||||
Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z)))))
|
||||
Yaffle> Bye for now!
|
||||
3
tests/ttimp/test001/input
Normal file
3
tests/ttimp/test001/input
Normal file
@ -0,0 +1,3 @@
|
||||
test1
|
||||
test2
|
||||
:q
|
||||
3
tests/ttimp/test001/run
Executable file
3
tests/ttimp/test001/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 Interp.yaff < input
|
||||
|
||||
rm -rf build
|
||||
15
tests/ttimp/test002/Adder.yaff
Normal file
15
tests/ttimp/test002/Adder.yaff
Normal file
@ -0,0 +1,15 @@
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
AdderTy : Nat -> Type
|
||||
AdderTy Z = Nat
|
||||
AdderTy (S $k) = Nat -> AdderTy k
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z $y = y
|
||||
plus (S $k) $y = S (plus k y)
|
||||
|
||||
adder : (i : Nat) -> (acc : Nat) -> AdderTy i
|
||||
adder Z $acc = acc
|
||||
adder (S $k) $acc = \x => adder k (plus x acc)
|
||||
7
tests/ttimp/test002/expected
Normal file
7
tests/ttimp/test002/expected
Normal file
@ -0,0 +1,7 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> (%pi RigW Explicit Nothing Main.Nat (Main.AdderTy Main.Z))
|
||||
Yaffle> (%pi RigW Explicit Nothing Main.Nat (Main.AdderTy (Main.S Main.Z)))
|
||||
Yaffle> (Main.S (Main.S (Main.S Main.Z)))
|
||||
Yaffle> (Main.S (Main.S (Main.S (Main.S (Main.S (Main.S Main.Z))))))
|
||||
Yaffle> Bye for now!
|
||||
5
tests/ttimp/test002/input
Normal file
5
tests/ttimp/test002/input
Normal file
@ -0,0 +1,5 @@
|
||||
:t adder Z
|
||||
:t adder (S Z)
|
||||
adder (S Z) (S (S Z)) (S Z)
|
||||
adder (S (S Z)) (S (S Z)) (S Z) (S (S (S Z)))
|
||||
:q
|
||||
3
tests/ttimp/test002/run
Executable file
3
tests/ttimp/test002/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 Adder.yaff < input
|
||||
|
||||
rm -rf build
|
||||
47
tests/ttimp/test003/Auto.yaff
Normal file
47
tests/ttimp/test003/Auto.yaff
Normal file
@ -0,0 +1,47 @@
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
data List : Type -> Type where
|
||||
Nil : List $a
|
||||
Cons : $a -> List $a -> List $a
|
||||
|
||||
data Elem : $a -> List $a -> Type where
|
||||
Here : Elem $x (Cons $x $xs)
|
||||
There : Elem $x $xs -> Elem $x (Cons $y $xs)
|
||||
|
||||
data Pair : Type -> Type -> Type where
|
||||
MkPair : $a -> $b -> Pair $a $b
|
||||
|
||||
fst : Pair $a $b -> $a
|
||||
fst (MkPair $x _) = x
|
||||
|
||||
snd : Pair $a $b -> $b
|
||||
snd (MkPair _ $y) = y
|
||||
|
||||
%pair Pair fst snd
|
||||
|
||||
isThere : Elem Z (Cons (S Z) (Cons Z Nil))
|
||||
isThere = %search
|
||||
|
||||
isThere2 : Elem (S Z) (Cons (S Z) (Cons Z Nil))
|
||||
isThere2 = %search
|
||||
|
||||
isThere3 : Elem (S (S Z)) (Cons (S Z) (Cons Z Nil))
|
||||
-- isThere3 = %search
|
||||
|
||||
fn : $a -> $b -> $a
|
||||
fn = %search
|
||||
|
||||
app : ($a -> $b) -> $a -> $b
|
||||
app = %search
|
||||
|
||||
test : $a -> Pair (Integer -> $a) Integer
|
||||
test $y = MkPair (\x => y) 42
|
||||
|
||||
foo : Pair (Integer -> $a) (Pair $c $b) -> Integer -> Pair $b $a
|
||||
foo = %search
|
||||
|
||||
bar : Pair (Int -> $a) (Pair $c $b) -> Int -> Pair $b Char
|
||||
|
||||
|
||||
6
tests/ttimp/test003/expected
Normal file
6
tests/ttimp/test003/expected
Normal file
@ -0,0 +1,6 @@
|
||||
Processing as TTImp
|
||||
Written TTC
|
||||
Yaffle> (((((Main.There [Just {a:17} = Main.Nat]) [Just y = (Main.S Main.Z)]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = Main.Z]) (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (Main.Nil [Just a = Main.Nat])]) [Just x = Main.Z]))
|
||||
Yaffle> (((Main.Here [Just {a:10} = Main.Nat]) [Just xs = (((Main.Cons [Just a = Main.Nat]) Main.Z) (Main.Nil [Just a = Main.Nat]))]) [Just x = (Main.S Main.Z)])
|
||||
Yaffle> ((((Main.MkPair [Just b = Integer]) [Just a = String]) "b") 94)
|
||||
Yaffle> Bye for now!
|
||||
4
tests/ttimp/test003/input
Normal file
4
tests/ttimp/test003/input
Normal file
@ -0,0 +1,4 @@
|
||||
isThere
|
||||
isThere2
|
||||
foo (MkPair (\x => x) (MkPair 'a' "b")) 94
|
||||
:q
|
||||
3
tests/ttimp/test003/run
Executable file
3
tests/ttimp/test003/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 Auto.yaff < input
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user