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