X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=afp%2Fa12%2FgastyStart.dcl;fp=afp%2Fa12%2FgastyStart.dcl;h=053ac97e6a76c26b6f16f458b058979ecf6ac66d;hb=01bad43f6e31dfb1ff59371ed264e94397745df9;hp=0000000000000000000000000000000000000000;hpb=3842e90cb6c88f3073c433d30b52c3e2985df521;p=clean-tests.git

diff --git a/afp/a12/gastyStart.dcl b/afp/a12/gastyStart.dcl
new file mode 100644
index 0000000..053ac97
--- /dev/null
+++ b/afp/a12/gastyStart.dcl
@@ -0,0 +1,37 @@
+definition module gastyStart
+
+/*
+	Pieter Koopman, Radboud University, 2016 - 2018
+	pieter@cs.ru.nl
+	Advanced programming
+	A simplified MBT tool based on logical properties
+	
+	Use the iTask environment!
+	Execute with "Basic values only" option
+*/
+
+import StdEnv, StdGeneric, Data.GenEq
+
+test :: p -> [String] | prop p
+class prop a where holds :: a Prop -> [Prop]
+
+:: Prop
+
+instance prop Bool
+instance prop (a->b) | prop b & testArg a
+class testArg a | gen{|*|}, string{|*|}, gEq{|*|} a
+
+generic gen a :: [a]
+derive gen Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS, OBJECT, RECORD, FIELD
+
+generic string a :: a -> String
+derive string Int, Real, Bool, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT, RECORD of grd, FIELD of gfd
+
+:: For = E.a b: (For) infix 0 (a -> b) [a] & prop b & string{|*|} a
+instance prop For
+
+:: Select = E.p: (==>) infixl 0 Bool p & prop p
+instance prop Select
+
+:: Equ = E.a: (=.=) infix 4 a a & testArg a
+instance prop Equ