    {-# LANGUAGE Trustworthy #-}

    -- | Utility / auxiliary functions.
    module Copilot.Theorem.Misc.Utils
     ( isSublistOf, nub', nubBy', nubEq
     , openTempFile
     ) where

    import Data.Function (on)
    import Data.List (groupBy, sortBy, group, sort)

    import Control.Applicative ((<$>))
    import Control.Monad

    import qualified Data.Set as Set

    import System.IO hiding (openTempFile)
    import System.Random
    import System.Directory

    -- | True if the given list is a subset of the second list, when both are
    -- considered as sets.
    isSublistOf :: Ord a => [a] -> [a] -> Bool
    isSublistOf :: forall a. Ord a => [a] -> [a] -> Bool
    isSublistOf = Set a -> Set a -> Bool
    forall a. Ord a => Set a -> Set a -> Bool
    Set.isSubsetOf (Set a -> Set a -> Bool) -> ([a] -> Set a) -> [a] -> [a] -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` [a] -> Set a
    forall a. Ord a => [a] -> Set a
    Set.fromList

    -- | True if both lists contain the same elements, when both are considered as
    -- sets.
    nubEq :: Ord a => [a] -> [a] -> Bool
    nubEq :: forall a. Ord a => [a] -> [a] -> Bool
    nubEq = Set a -> Set a -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Set a -> Set a -> Bool) -> ([a] -> Set a) -> [a] -> [a] -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` [a] -> Set a
    forall a. Ord a => [a] -> Set a
    Set.fromList

    -- | Remove duplicates from a list.
    --
    -- This is an efficient version of 'Data.List.nub' that works for lists with a
    -- stronger constraint on the type (i.e., 'Ord', as opposed of
    -- 'Data.List.nub''s 'Eq' constraint).
    nub' :: Ord a => [a] -> [a]
    nub' :: forall a. Ord a => [a] -> [a]
    nub' = ([a] -> a) -> [[a]] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map [a] -> a
    forall a. HasCallStack => [a] -> a
    head ([[a]] -> [a]) -> ([a] -> [[a]]) -> [a] -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [[a]]
    forall a. Eq a => [a] -> [[a]]
    group ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [a] -> [a]
    forall a. Ord a => [a] -> [a]
    sort

    -- | Variant of 'nub'' parameterized by the comparison function.
    nubBy' :: (a -> a -> Ordering) -> [a] -> [a]
    nubBy' :: forall a. (a -> a -> Ordering) -> [a] -> [a]
    nubBy' a -> a -> Ordering
    f = ([a] -> a) -> [[a]] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map [a] -> a
    forall a. HasCallStack => [a] -> a
    head ([[a]] -> [a]) -> ([a] -> [[a]]) -> [a] -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a -> Bool) -> [a] -> [[a]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (\a
    x a
    y -> a -> a -> Ordering
    f a
    x a
    y Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ) ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a -> Ordering) -> [a] -> [a]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy a -> a -> Ordering
    f

    -- | Create a temporary file and open it for writing.
    openTempFile :: String  -- ^ Directory where the file should be created.
                 -> String  -- ^ Base name for the file (prefix).
                 -> String  -- ^ File extension.
                 -> IO (String, Handle)
    openTempFile :: String -> String -> String -> IO (String, Handle)
    openTempFile String
    loc String
    baseName String
    extension = do

      path   <- IO String
    freshPath
      handle <- openFile path WriteMode
      return (path, handle)

      where

        freshPath :: IO FilePath
        freshPath :: IO String
    freshPath = do
          path   <- String -> String
    pathFromSuff (String -> String) -> IO String -> IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO String
    randSuff
          exists <- doesFileExist path
          if exists then freshPath else return path

        randSuff :: IO String
        randSuff :: IO String
    randSuff = Int -> IO Char -> IO String
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    4 (IO Char -> IO String) -> IO Char -> IO String
    forall a b. (a -> b) -> a -> b
    $ (Char, Char) -> IO Char
    forall a (m :: * -> *). (Random a, MonadIO m) => (a, a) -> m a
    randomRIO (Char
    '0', Char
    '9')

        pathFromSuff :: String -> FilePath
        pathFromSuff :: String -> String
    pathFromSuff String
    suf = String
    loc String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "/" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    baseName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    suf String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    extension