--- /dev/null
+/Clean System Files/
+StdStack
--- /dev/null
+definition module StdSortList\r
+\r
+import StdClass\r
+\r
+:: SortList a\r
+\r
+newSortList :: SortList a // lege gesorteerde lijst\r
+memberSort :: a (SortList a) -> Bool | Eq, Ord a // is element van\r
+insertSort :: a (SortList a) -> SortList a | Ord a // voeg element toe\r
+removeFirst :: a (SortList a) -> SortList a | Eq, Ord a // verwijder eerste voorkomen\r
+removeAll :: a (SortList a) -> SortList a | Eq, Ord a // verwijder alle voorkomens\r
+elements :: (SortList a) -> [a] // geef alle elementen\r
+count :: (SortList a) -> Int // aantal elementen\r
+\r
+minimum :: (SortList a) -> a // huidige minimum waarde\r
+maximum :: (SortList a) -> a // huidige maximum waarde\r
+\r
+mergeSortList :: (SortList a) (SortList a) -> SortList a | Eq, Ord a // meng gesorteerde lijsten\r
--- /dev/null
+implementation module StdSortList\r
+\r
+import StdEnv\r
+\r
+:: SortList a :== [a]\r
+\r
+newSortList :: (SortList a)\r
+newSortList = []\r
+\r
+memberSort :: a (SortList a) -> Bool | Eq, Ord a // is element van\r
+memberSort _ [] = False\r
+memberSort m l\r
+ | hd l == m = True\r
+ | hd l > m = False\r
+ | otherwise = memberSort m (tl l)\r
+\r
+insertSort :: a (SortList a) -> SortList a | Ord a // voeg element toe\r
+insertSort m l = insertSort` newSortList m l \r
+where \r
+ insertSort` :: (SortList a) a (SortList a) -> (SortList a) | Ord a\r
+ insertSort` l1 m l2\r
+ | count l2 == 0 = l1 ++ [m]\r
+ | minimum l2 >= m = l1 ++ [m] ++ l2\r
+ | otherwise = insertSort` (l1 ++ [hd l2]) m (tl l2)\r
+\r
+removeFirst :: a (SortList a) -> SortList a | Eq, Ord a // verwijder eerste voorkomen\r
+removeFirst m l = removeFirst` newSortList m l\r
+where\r
+ removeFirst` :: (SortList a) a (SortList a) -> (SortList a) | Eq, Ord a\r
+ removeFirst` l1 m l2\r
+ | count l2 == 0 = l1\r
+ | minimum l2 > m = l1 ++ l2\r
+ | minimum l2 == m = l1 ++ tl l2\r
+ | otherwise = removeFirst` (l1 ++ [hd l2]) m (tl l2)\r
+\r
+removeAll :: a (SortList a) -> SortList a | Eq, Ord a // verwijder alle voorkomens\r
+removeAll m l = removeAll` newSortList m l\r
+where\r
+ removeAll` :: (SortList a) a (SortList a) -> (SortList a) | Eq, Ord a\r
+ removeAll` l1 m l2\r
+ | count l2 == 0 = l1\r
+ | minimum l2 > m = l1 ++ l2\r
+ | minimum l2 == m = removeAll` l1 m (tl l2)\r
+ | otherwise = removeAll` (l1 ++ [hd l2]) m (tl l2)\r
+\r
+elements :: (SortList a) -> [a] // geef alle elementen\r
+elements l = l\r
+\r
+count :: (SortList a) -> Int // aantal elementen\r
+count l = length l\r
+\r
+minimum :: (SortList a) -> a // huidige minimum waarde\r
+minimum l = hd l\r
+\r
+maximum :: (SortList a) -> a // huidige maximum waarde\r
+maximum l = last l\r
+\r
+mergeSortList :: (SortList a) (SortList a) -> SortList a | Eq, Ord a // meng gesorteerde lijsten\r
+mergeSortList l1 [] = l1\r
+mergeSortList l1 l2 = mergeSortList (insertSort (hd l2) l1) (tl l2)\r
--- /dev/null
+module StdSortListTest\r
+\r
+/* Test module StdSortList\r
+ Voor werken met Gast: \r
+ (*) gebruik Environment 'Gast'\r
+ (*) zet Project Options op 'Basic Values Only' en '16M' Maximum Heap Size.\r
+*/\r
+\r
+import gast\r
+import GenLexOrd\r
+import StdSortList\r
+\r
+Start = testn 10000 \r
+ (\n` n2` m -> let n = lst2slst (cast [A,B,C] n` )\r
+ n2 = lst2slst (cast [A,B,C] n2`) \r
+ in \r
+ leeg_is_leeg /\\r
+ count_matches_elems n /\\r
+ is_sorted_elems n /\\r
+ member_is_member n m /\\r
+ member_na_insert n m /\\r
+ member_na_remove n m /\\r
+ insert_remove_invariant n m /\\r
+ minimum_property n /\\r
+ maximum_property n /\\r
+ merge_additive n n2 /\\r
+ merge_member n n2 m /\\r
+ True\r
+ )\r
+\r
+:: Enum = A | B | C \r
+\r
+derive bimap []\r
+derive ggen Enum\r
+derive genShow Enum\r
+derive gEq Enum\r
+derive gLexOrd Enum\r
+instance == Enum where (==) x y = gEq{|*|} x y\r
+instance < Enum where (<) x y = gEq{|*|} (gLexOrd{|*|} x y) LT\r
+\r
+// clean should have something like this!\r
+cast :: a a -> a\r
+cast _ x = x\r
+\r
+leeg_is_leeg :: Property\r
+leeg_is_leeg \r
+ = name "leeg_is_leeg"\r
+ (count newSortList == 0)\r
+\r
+count_matches_elems :: (SortList a) -> Property | Eq, Ord a\r
+count_matches_elems n \r
+ = name "count_matches_elems" \r
+ (length (elements n) == count n)\r
+\r
+is_sorted_elems :: (SortList a) -> Property | Eq, Ord a\r
+is_sorted_elems n\r
+ = name "is_sorted_elems"\r
+ (isSorted (elements n))\r
+ where isSorted lst = and [ x<=y \\ x<-lst & y<-tl lst ]\r
+\r
+member_is_member :: (SortList a) a -> Property | Eq, Ord a\r
+member_is_member lst e\r
+ = name "member_is_member"\r
+ ((isMember e (elements lst)) <==> (memberSort e lst))\r
+\r
+member_na_insert :: (SortList a) a -> Property | Eq, Ord a\r
+member_na_insert lst e\r
+ = name "member_na_insert"\r
+ (memberSort e (insertSort e lst))\r
+\r
+member_na_remove :: (SortList a) a -> Property | Eq, Ord a\r
+member_na_remove lst e\r
+ = name "member_na_remove"\r
+ (not (memberSort e (removeAll e lst)))\r
+\r
+insert_remove_invariant :: (SortList a) a -> Property | Eq, Ord a\r
+insert_remove_invariant lst e\r
+ = name "insert_remove_invariant"\r
+ (memberSort e lst <==> memberSort e lst`)\r
+ where lst` = removeFirst e (insertSort e lst)\r
+\r
+minimum_property :: (SortList a) -> Property | Eq,Ord a\r
+minimum_property n\r
+ = name "minimum_property"\r
+ (count n > 0 ==> (memberSort min n /\ all ((<=) min) (elements n)))\r
+ where min = minimum n\r
+\r
+maximum_property :: (SortList a) -> Property | Eq,Ord a\r
+maximum_property n\r
+ = name "maximum_property"\r
+ (count n > 0 ==> (memberSort max n /\ all ((>=) max) (elements n)))\r
+ where max = maximum n\r
+\r
+merge_member :: (SortList a) (SortList a) a -> Property | Eq,Ord a\r
+merge_member n m e\r
+ = name "merge_member"\r
+ (memberSort e nm <==> (memberSort e n \/ memberSort e m))\r
+ where nm = mergeSortList n m\r
+\r
+merge_additive :: (SortList a) (SortList a) -> Property | Eq,Ord a\r
+merge_additive n m \r
+ = name "merge_additive"\r
+ (count n + count m == count nm)\r
+ where nm = mergeSortList n m\r
+\r
+lst2slst :: [a] -> SortList a | Eq,Ord a\r
+lst2slst xs = seq (map insertSort xs) newSortList\r
--- /dev/null
+definition module StdStack\r
+\r
+:: Stack a\r
+\r
+newStack :: Stack a // lege stack\r
+push :: a (Stack a) -> Stack a // plaats nieuw element bovenop de stack\r
+pushes :: [a] (Stack a) -> Stack a // plaats elementen achtereenvolgens bovenop stack\r
+pop :: (Stack a) -> Stack a // haal top element van stack\r
+popn :: Int (Stack a) -> Stack a // haal bovenste $n$ top elementen van stack\r
+top :: (Stack a) -> a // geef top element van stack\r
+topn :: Int (Stack a) -> [a] // geef bovenste $n$ top elementen van stack\r
+elements :: (Stack a) -> [a] // geef alle elementen van stack\r
+count :: (Stack a) -> Int // tel aantal elementen in stack\r
--- /dev/null
+implementation module StdStack\r
+\r
+import StdEnv\r
+import StdList\r
+\r
+:: Stack a :== [a]\r
+\r
+newStack :: (Stack a)\r
+newStack = []\r
+\r
+push :: a (Stack a) -> (Stack a)\r
+push a s = [a] ++ s\r
+\r
+pop :: (Stack a) -> (Stack a)\r
+pop [a:s] = s\r
+pop [] = []\r
+\r
+popn :: Int (Stack a) -> (Stack a)\r
+popn 0 s = s\r
+popn n s = popn (n-1) (pop s)\r
+\r
+pushes :: [a] (Stack a) -> (Stack a)\r
+pushes [] s = s\r
+pushes a s = pushes (tl a) (push (hd a) s)\r
+\r
+top :: (Stack a) -> a\r
+top [] = abort "`top s` with s = []"\r
+top s = hd s\r
+\r
+topn :: Int (Stack a) -> [a]\r
+topn n s\r
+ | n > length s = abort "`topn n s` with n > length s"\r
+ | otherwise = take n s\r
+\r
+count :: (Stack a) -> Int\r
+count s = length s\r
+\r
+elements :: (Stack a) -> [a]\r
+elements s = s\r
+\r
+Start = ( "s0 = newStack = ", s0,'\n'\r
+ , "s1 = push 1 s0 = ", s1,'\n'\r
+ , "s2 = pushes [2..5] s1 = ",s2,'\n'\r
+ , "s3 = pop s2 = ", s3,'\n'\r
+ , "s4 = popn 3 s3 = ", s4,'\n'\r
+ , "s5 = top s4 = ", s5,'\n'\r
+ , "s6 = topn 3 s2 = ", s6,'\n'\r
+ , "s7 = elements s2 = ", s7,'\n'\r
+// , "s8 = push 10 s1 = ", s8,'\n'\r
+// , "s9 = popn 10 s8 = ", s9,'\n'\r
+// , "sa = topn 5 s4 = ", sa,'\n'\r
+// , "sb = top s0 = ", sb,'\n'\r
+ )\r
+where\r
+ s0 = newStack\r
+ s1 = push 1 s0\r
+ s2 = pushes [2..5] s1\r
+ s3 = pop s2\r
+ s4 = popn 3 s3\r
+ s5 = top s4\r
+ s6 = topn 3 s2\r
+ s7 = elements s2\r
+// s8 = push 10 s1\r
+// s9 = popn 10 s8\r
+// sa = topn 5 s4\r
+// sb = top s0\r
--- /dev/null
+module StdStackTest\r
+\r
+/* Test module StdStack\r
+ Voor werken met Gast: \r
+ (*) gebruik Environment 'Gast'\r
+ (*) zet Project Options op 'Basic Values Only' en '2M' Maximum Heap Size\r
+*/\r
+\r
+import gast\r
+import StdStack\r
+\r
+Start\r
+ = testn 1000\r
+ (\x n ->\r
+ newStack_is_empty /\\r
+ stack_is_reverse n /\\r
+ pop_empty_is_ok /\\r
+ top_na_push n x /\\r
+ pop_na_push x /\\r
+ count_counts n x /\\r
+ pop_maakt_stack_korter n /\\r
+ True\r
+ )\r
+\r
+newStack_is_empty :: Property\r
+newStack_is_empty = name "newStack_is_empty" (isEmpty (elements empty))\r
+\r
+stack_is_reverse :: Int -> Property\r
+stack_is_reverse n = name "stack_is_reverse"\r
+ (elements (pushes [1..n`] newStack) == reverse [1..n`])\r
+where n` = min (abs n) 100\r
+\r
+pop_empty_is_ok :: Property\r
+pop_empty_is_ok = name "pop_empty_is_ok" (count (pop empty) == 0)\r
+\r
+top_na_push :: Int Int -> Property\r
+top_na_push x n = name "top_na_push"\r
+ (top (push x (pushes [1..n`] newStack)) == x)\r
+where n` = min (abs n) 100\r
+\r
+pop_na_push :: Int -> Property\r
+pop_na_push a = name "pop_na_push"\r
+ (top (pop (pop (pushes [a,b,c] newStack))) == a)\r
+where b = a + a + one\r
+ c = b + a + one\r
+\r
+count_counts :: Int Int -> Property\r
+count_counts n x = name "count_counts"\r
+ (length (elements stack) == count stack)\r
+where stack = pushes [1..n`] newStack\r
+ n` = min (abs n) 100\r
+\r
+pop_maakt_stack_korter :: Int -> Property\r
+pop_maakt_stack_korter n = name "pop_maakt_stack_korter"\r
+ (count stack == 0 || count (pop stack) == count stack - 1)\r
+where stack = pushes [1..n`] newStack\r
+ n` = min (abs n) 100\r
+\r
+empty :: Stack Int\r
+empty = newStack\r
repositories / fp1415.git / commitdiff