1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 |
------------------------------------------------------------------------------ --- A collection of common non-deterministic and/or combinatorial operations. --- Many operations are intended to operate on sets. --- The representation of these sets is not hidden; rather --- sets are represented as lists. --- Ideally these lists contains no duplicate elements and --- the order of their elements cannot be observed. --- In practice, these conditions are not enforced. --- --- @author Sergio Antoy (with extensions by Michael Hanus) --- @version June 2021 ------------------------------------------------------------------------------ {-# OPTIONS_FRONTEND -Wno-overlapping -Wno-missing-signatures #-} module Combinatorial ( permute, subset, allSubsets, splitSet, sizedSubset, partition ) where import Data.List ( sum ) import Control.Search.SetFunctions import Test.Prop ------------------------------------------------------------------------------ -- Public Operations ------------------------------------------------------------------------------ --- Compute any permutation of a list. --- --- @param xs - The list. --- @return A permutation of the argument. permute :: [a] -> [a] permute [] = [] permute (x:xs) = ndinsert (permute xs) where ndinsert ys = x : ys ndinsert (y:ys) = y : ndinsert ys -- Properties: permute1234 = permute [1,2,3,4] ~> [1,3,4,2] -- The length of a permutation is identical to the length of the argument: permLength xs = length (permute xs) <~> length xs -- lengths are equal -- The permutation contains the same elements as the argument: permElems xs = anyOf (permute xs) <~> anyOf xs ------------------------------------------------------------------------------ --- Compute any sublist of a list. --- The sublist contains some of the elements of the list in the same order. --- --- @param xs - The list. --- @return A sublist of the argument. subset :: [a] -> [a] subset [] = [] subset (x:xs) = x:subset xs subset (_:xs) = subset xs -- Properties: subset1234 = subset [1,2,3,4] ~> [1,3] subset123 = subset [1,2,3] <~> ([1,2,3]?[1,2]?[1,3]?[1]?[2,3]?[2]?[3]?[]) subsetElems xs = anyOf (subset xs) <~ anyOf xs ------------------------------------------------------------------------------ --- Compute all the sublists of a list. --- --- @param xs - The list. --- @return All the sublists of the argument. allSubsets :: Ord a => [a] -> [[a]] allSubsets xs = sortValues (set1 subset xs) -- Properties: allSubsets123 = allSubsets [1,2,3] -=- [[],[1],[1,2],[1,2,3],[1,3],[2],[2,3],[3]] ------------------------------------------------------------------------------ --- Split a list into any two sublists. --- --- @param xs - The list. --- @return A pair consisting of two complementary sublists of the argument. splitSet :: [a] -> ([a],[a]) splitSet [] = ([],[]) splitSet (x:xs) = let (u,v) = splitSet xs in (x:u,v) ? (u,x:v) -- Properties: splitSet1234 = splitSet [1,2,3,4] ~> ([1,3,4],[2]) -- The sum of the length of the two sublists is the length of the argument list: splitSetLengths zs = (\ (xs,ys) -> length xs + length ys) (splitSet zs) <~> length zs -- The two sublists and the argument list have the same elements: splitSetElems zs = (\ (xs,ys) -> anyOf xs ? anyOf ys) (splitSet zs) <~> anyOf zs ------------------------------------------------------------------------------ --- Compute any sublist of fixed length of a list. --- Similar to 'subset', but the length of the result is fixed. --- --- @param c - The length of the output sublist. --- @param xs - The input list. --- @return A sublist of `xs` of length `c`. sizedSubset :: Int -> [a] -> [a] sizedSubset c l = if c == 0 then [] else aux l where aux (x:xs) = x:sizedSubset (c-1) xs ? sizedSubset c xs -- Precondition: sizedSubset'pre :: Int -> [a] -> Bool sizedSubset'pre c _ = c>=0 -- Properties: sizedSubsetLength c xs = (c>=0 && length xs >= c) ==> length (sizedSubset c xs) <~> c -- No result if the given output length is larger than the length of the input: sizedSubsetLengthTooSmall c xs = (c>=0 && length xs < c) ==> failing (sizedSubset c xs) ------------------------------------------------------------------------------ --- Compute any partition of a list. --- The output is a list of non-empty lists such that their concatenation --- is a permutation of the input list. --- No guarantee is made on the order of the arguments in the output. --- --- @param xs - The input list. --- @return A partition of `xs` represented as a list of lists. partition :: [a] -> [[a]] partition [] = [] partition (x:xs) = insert x (partition xs) where insert e [] = [[e]] insert e (y:ys) = ((e:y):ys) ? (y:insert e ys) -- Properties: partition1234 = partition [1,2,3,4] ~> [[4],[2,3],[1]] partition123 = partition [1,2,3] <~> ([[1,2,3]] ? [[2,3],[1]] ? [[1,3],[2]] ? [[3],[1,2]] ? [[3],[2],[1]]) -- The sum of the length of the sublists is the length of the argument list: partitionLengths xs = sum (map length (partition xs)) <~> length xs -- The sublists of the partition and the argument list have the same elements: partitionElems xs = anyOf (map anyOf (partition xs)) <~> anyOf xs -- end module Combinatorial |