{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-orphans -fno-warn-unused-binds #-}

module Data.Logic.ATP.Lib
    ( Failing(Success, Failure)
    , failing
    , SetLike(slView, slMap, slUnion, slEmpty, slSingleton), slInsert, prettyFoldable

    , setAny
    , setAll
    , flatten
    -- , itlist2
    -- , itlist  -- same as foldr with last arguments flipped
    , tryfind
    , tryfindM
    , runRS
    , evalRS
    , settryfind
    -- , end_itlist -- same as foldr1
    , (|=>)
    , (|->)
    , fpf
    -- * Time and timeout
    , timeComputation
    , timeMessage
    , time
    , timeout
    , compete
    -- * Map aliases
    , defined
    , undefine
    , apply
    -- , exists
    , tryApplyD
    , allpairs
    , distrib
    , image
    , optimize
    , minimize
    , maximize
    , can
    , allsets
    , allsubsets
    , allnonemptysubsets
    , mapfilter
    , setmapfilter
    , (∅)
    , deepen, Depth(Depth)
    , testLib
    ) where

import Control.Applicative.Error (Failing(..))
import Control.Concurrent (forkIO, killThread, newEmptyMVar, putMVar, takeMVar, threadDelay)
#if MIN_VERSION_base(4,9,0)
import qualified Control.Monad.Fail as Fail
#endif
import Control.Monad.RWS (evalRWS, runRWS, RWS)
import Data.Data (Data)
import Data.Foldable as Foldable
import Data.Function (on)
import qualified Data.List as List (map)
import Data.Map.Strict as Map (delete, findMin, insert, lookup, Map, member, singleton)
import Data.Maybe
import Data.Monoid ((<>))
import Data.Sequence as Seq (Seq, viewl, ViewL(EmptyL, (:<)), (><), singleton)
import Data.Set as Set (delete, empty, fold, fromList, insert, minView, Set, singleton, union)
import qualified Data.Set as Set (map)
import Data.Time.Clock (DiffTime, diffUTCTime, getCurrentTime, NominalDiffTime)
import Data.Typeable (Typeable)
import Debug.Trace (trace)
import Prelude hiding (map)
import System.IO (hPutStrLn, stderr)
import Text.PrettyPrint.HughesPJClass (Doc, fsep, punctuate, comma, space, Pretty(pPrint), text)
import Test.HUnit (assertEqual, Test(TestCase, TestLabel, TestList))

-- | An error idiom.  Rather like the error monad, but collect all
-- errors together
type ErrorMsg = String

failing :: ([String] -> b) -> (a -> b) -> Failing a -> b
failing :: forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing [String] -> b
f a -> b
_ (Failure [String]
errs) = [String] -> b
f [String]
errs
failing [String] -> b
_ a -> b
f (Success a
a)    = a -> b
f a
a

-- Declare a Monad instance for Failing so we can chain a series of
-- Failing actions with >> or >>=.  If any action fails the subsequent
-- actions in the chain will be aborted.
instance Monad Failing where
  return :: forall a. a -> Failing a
return = a -> Failing a
forall a. a -> Failing a
Success
  Failing a
m >>= :: forall a b. Failing a -> (a -> Failing b) -> Failing b
>>= a -> Failing b
f =
      case Failing a
m of
        (Failure [String]
errs) -> ([String] -> Failing b
forall a. [String] -> Failing a
Failure [String]
errs)
        (Success a
a) -> a -> Failing b
f a
a
#if !MIN_VERSION_base(4,13,0)
  fail errMsg = Failure [errMsg]
#endif

#if MIN_VERSION_base(4,9,0)
instance Fail.MonadFail Failing where
  fail :: forall a. String -> Failing a
fail String
errMsg = [String] -> Failing a
forall a. [String] -> Failing a
Failure [String
errMsg]
#endif

deriving instance Typeable Failing
deriving instance Data a => Data (Failing a)
deriving instance Read a => Read (Failing a)
deriving instance Eq a => Eq (Failing a)
deriving instance Ord a => Ord (Failing a)

instance Pretty a => Pretty (Failing a) where
    pPrint :: Failing a -> Doc
pPrint (Failure [String]
ss) = String -> Doc
text ([String] -> String
unlines (String
"Failures:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
List.map (String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
ss))
    pPrint (Success a
a) = a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
a

-- | A simple class, slightly more powerful than Foldable, so we can
-- write functions that operate on the elements of a set or a list.
class Foldable c => SetLike c where
    slView :: forall a. c a -> Maybe (a, c a)
    slMap :: forall a b. Ord b => (a -> b) -> c a -> c b
    slUnion :: Ord a => c a -> c a -> c a
    slEmpty :: c a
    slSingleton :: a -> c a

instance SetLike Set where
    slView :: forall a. Set a -> Maybe (a, Set a)
slView = Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView
    slMap :: forall a b. Ord b => (a -> b) -> Set a -> Set b
slMap = (a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map
    slUnion :: forall a. Ord a => Set a -> Set a -> Set a
slUnion = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    slEmpty :: forall a. Set a
slEmpty = Set a
forall a. Set a
Set.empty
    slSingleton :: forall a. a -> Set a
slSingleton = a -> Set a
forall a. a -> Set a
Set.singleton

instance SetLike [] where
    slView :: forall a. [a] -> Maybe (a, [a])
slView [] = Maybe (a, [a])
forall a. Maybe a
Nothing
    slView (a
h : [a]
t) = (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
h, [a]
t)
    slMap :: forall a b. Ord b => (a -> b) -> [a] -> [b]
slMap = (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
List.map
    slUnion :: forall a. Ord a => [a] -> [a] -> [a]
slUnion = [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
(<>)
    slEmpty :: forall a. [a]
slEmpty = [a]
forall a. Monoid a => a
mempty
    slSingleton :: forall a. a -> [a]
slSingleton = (a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [])

instance SetLike Seq where
    slView :: forall a. Seq a -> Maybe (a, Seq a)
slView Seq a
s = case Seq a -> ViewL a
forall a. Seq a -> ViewL a
viewl Seq a
s of
               ViewL a
EmptyL -> Maybe (a, Seq a)
forall a. Maybe a
Nothing
               a
h :< Seq a
t -> (a, Seq a) -> Maybe (a, Seq a)
forall a. a -> Maybe a
Just (a
h, Seq a
t)
    slMap :: forall a b. Ord b => (a -> b) -> Seq a -> Seq b
slMap = (a -> b) -> Seq a -> Seq b
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
    slUnion :: forall a. Ord a => Seq a -> Seq a -> Seq a
slUnion = Seq a -> Seq a -> Seq a
forall a. Seq a -> Seq a -> Seq a
(><)
    slEmpty :: forall a. Seq a
slEmpty = Seq a
forall a. Monoid a => a
mempty
    slSingleton :: forall a. a -> Seq a
slSingleton = a -> Seq a
forall a. a -> Seq a
Seq.singleton

slInsert :: (SetLike set, Ord a) => a -> set a -> set a
slInsert :: forall (set :: * -> *) a.
(SetLike set, Ord a) =>
a -> set a -> set a
slInsert a
x set a
s = set a -> set a -> set a
forall a. Ord a => set a -> set a -> set a
forall (c :: * -> *) a. (SetLike c, Ord a) => c a -> c a -> c a
slUnion (a -> set a
forall a. a -> set a
forall (c :: * -> *) a. SetLike c => a -> c a
slSingleton a
x) set a
s

prettyFoldable :: (Foldable t, Pretty a) => t a -> Doc
prettyFoldable :: forall (t :: * -> *) a. (Foldable t, Pretty a) => t a -> Doc
prettyFoldable t a
s = [Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space) ((a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
List.map a -> Doc
forall a. Pretty a => a -> Doc
pPrint ((a -> [a] -> [a]) -> [a] -> t a -> [a]
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.foldr (:) [] t a
s)))

--instance (Pretty a, SetLike set) => Pretty (set a) where
--    pPrint = prettyFoldable

(∅) :: (Monoid (c a), SetLike c) => c a
∅ :: forall (c :: * -> *) a. (Monoid (c a), SetLike c) => c a
(∅) = c a
forall a. Monoid a => a
mempty

setAny :: Foldable t => (a -> Bool) -> t a -> Bool
setAny :: forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any

setAll :: Foldable t => (a -> Bool) -> t a -> Bool
setAll :: forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAll = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all

flatten :: Ord a => Set (Set a) -> Set a
flatten :: forall a. Ord a => Set (Set a) -> Set a
flatten Set (Set a)
ss' = (Set a -> Set a -> Set a) -> Set a -> Set (Set a) -> Set a
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set a
forall a. Set a
Set.empty Set (Set a)
ss'

{-
(* ========================================================================= *)
(* Misc library functions to set up a nice environment.                      *)
(* ========================================================================= *)

let identity x = x;;

let ( ** ) = fun f g x -> f(g x);;

(* ------------------------------------------------------------------------- *)
(* GCD and LCM on arbitrary-precision numbers.                               *)
(* ------------------------------------------------------------------------- *)

let gcd_num n1 n2 =
  abs_num(num_of_big_int
      (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)));;

let lcm_num n1 n2 = abs_num(n1 */ n2) // gcd_num n1 n2;;

(* ------------------------------------------------------------------------- *)
(* A useful idiom for "non contradictory" etc.                               *)
(* ------------------------------------------------------------------------- *)

let non p x = not(p x);;

(* ------------------------------------------------------------------------- *)
(* Kind of assertion checking.                                               *)
(* ------------------------------------------------------------------------- *)

let check p x = if p(x) then x else failwith "check";;

(* ------------------------------------------------------------------------- *)
(* Repetition of a function.                                                 *)
(* ------------------------------------------------------------------------- *)

let rec funpow n f x =
  if n < 1 then x else funpow (n-1) f (f x);;
-}
-- let can f x = try f x; true with Failure _ -> false;;
can :: (t -> Failing a) -> t -> Bool
can :: forall t a. (t -> Failing a) -> t -> Bool
can t -> Failing a
f t
x = ([String] -> Bool) -> (a -> Bool) -> Failing a -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
True) (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
False) (t -> Failing a
f t
x)

{-
let rec repeat f x = try repeat f (f x) with Failure _ -> x;;

(* ------------------------------------------------------------------------- *)
(* Handy list operations.                                                    *)
(* ------------------------------------------------------------------------- *)

let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);;

let rec (---) = fun m n -> if m >/ n then [] else m::((m +/ Int 1) --- n);;

let rec map2 f l1 l2 =
  match (l1,l2) with
    [],[] -> []
  | (h1::t1),(h2::t2) -> let h = f h1 h2 in h::(map2 f t1 t2)
  | _ -> failwith "map2: length mismatch";;

let rev =
  let rec rev_append acc l =
    match l with
      [] -> acc
    | h::t -> rev_append (h::acc) t in
  fun l -> rev_append [] l;;

let hd l =
  match l with
   h::t -> h
  | _ -> failwith "hd";;

let tl l =
  match l with
   h::t -> t
  | _ -> failwith "tl";;
-}

-- (^) = (++)

itlist :: Foldable t => (a -> b -> b) -> t a -> b -> b
itlist :: forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> t a -> b -> b
itlist a -> b -> b
f t a
xs b
z = (a -> b -> b) -> b -> t a -> b
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.foldr a -> b -> b
f b
z t a
xs

end_itlist :: Foldable t => (a -> a -> a) -> t a -> a
end_itlist :: forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
end_itlist = (a -> a -> a) -> t a -> a
forall a. (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
Foldable.foldr1

itlist2 :: (SetLike s, SetLike t) =>
           (a -> b -> Failing r -> Failing r) ->
           s a -> t b -> Failing r -> Failing r
itlist2 :: forall (s :: * -> *) (t :: * -> *) a b r.
(SetLike s, SetLike t) =>
(a -> b -> Failing r -> Failing r)
-> s a -> t b -> Failing r -> Failing r
itlist2 a -> b -> Failing r -> Failing r
f s a
s t b
t Failing r
r =
    case (s a -> Maybe (a, s a)
forall a. s a -> Maybe (a, s a)
forall (c :: * -> *) a. SetLike c => c a -> Maybe (a, c a)
slView s a
s, t b -> Maybe (b, t b)
forall a. t a -> Maybe (a, t a)
forall (c :: * -> *) a. SetLike c => c a -> Maybe (a, c a)
slView t b
t) of
      (Maybe (a, s a)
Nothing, Maybe (b, t b)
Nothing) -> Failing r
r
      (Just (a
a, s a
s'), Just (b
b, t b
t')) ->
          a -> b -> Failing r -> Failing r
f a
a b
b ((a -> b -> Failing r -> Failing r)
-> s a -> t b -> Failing r -> Failing r
forall (s :: * -> *) (t :: * -> *) a b r.
(SetLike s, SetLike t) =>
(a -> b -> Failing r -> Failing r)
-> s a -> t b -> Failing r -> Failing r
itlist2 a -> b -> Failing r -> Failing r
f s a
s' t b
t' Failing r
r)
      (Maybe (a, s a), Maybe (b, t b))
_ -> [String] -> Failing r
forall a. [String] -> Failing a
Failure [String
"itlist2"]

{-
let rec zip l1 l2 =
  match (l1,l2) with
        ([],[]) -> []
      | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
      | _ -> failwith "zip";;

let rec forall p l =
  match l with
    [] -> true
  | h::t -> p(h) & forall p t;;
-}
exists :: Foldable t => (a -> Bool) -> t a -> Bool
exists :: forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
exists = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any
{-
let partition p l =
    itlist (fun a (yes,no) -> if p a then a::yes,no else yes,a::no) l ([],[]);;

let filter p l = fst(partition p l);;

let length =
  let rec len k l =
    if l = [] then k else len (k + 1) (tl l) in
  fun l -> len 0 l;;

let rec last l =
  match l with
    [x] -> x
  | (h::t) -> last t
  | [] -> failwith "last";;

let rec butlast l =
  match l with
    [_] -> []
  | (h::t) -> h::(butlast t)
  | [] -> failwith "butlast";;

let rec find p l =
  match l with
      [] -> failwith "find"
    | (h::t) -> if p(h) then h else find p t;;

let rec el n l =
  if n = 0 then hd l else el (n - 1) (tl l);;

let map f =
  let rec mapf l =
    match l with
      [] -> []
    | (x::t) -> let y = f x in y::(mapf t) in
  mapf;;
-}

-- allpairs :: forall a b c. (Ord c) => (a -> b -> c) -> Set a -> Set b -> Set c
-- allpairs f xs ys = Set.fold (\ x zs -> Set.fold (\ y zs' -> Set.insert (f x y) zs') zs ys) Set.empty xs

allpairs :: forall a b c set. (SetLike set, Ord c) => (a -> b -> c) -> set a -> set b -> set c
allpairs :: forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs a -> b -> c
f set a
xs set b
ys = (a -> set c -> set c) -> set c -> set a -> set c
forall a b. (a -> b -> b) -> b -> set a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.foldr (\ a
x set c
zs -> (b -> set c -> set c) -> set c -> set b -> set c
forall a b. (a -> b -> b) -> b -> set a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Foldable.foldr (a -> b -> set c -> set c
g a
x) set c
zs set b
ys) set c
forall a. set a
forall (c :: * -> *) a. SetLike c => c a
slEmpty set a
xs
    where g :: a -> b -> set c -> set c
          g :: a -> b -> set c -> set c
g a
x b
y set c
zs' = c -> set c -> set c
forall (set :: * -> *) a.
(SetLike set, Ord a) =>
a -> set a -> set a
slInsert (a -> b -> c
f a
x b
y) set c
zs'

distrib :: Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib :: forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib Set (Set a)
s1 Set (Set a)
s2 = (Set a -> Set a -> Set a)
-> Set (Set a) -> Set (Set a) -> Set (Set a)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union) Set (Set a)
s1 Set (Set a)
s2

test01 :: Test
test01 :: Test
test01 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Int, Int) -> Set (Int, Int) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"allpairs" Set (Int, Int)
expected Set (Int, Int)
input
    where input :: Set (Int, Int)
input = (Int -> Int -> (Int, Int)) -> Set Int -> Set Int -> Set (Int, Int)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (,) ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
1,Int
2,Int
3]) ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int
4,Int
5,Int
6])
          expected :: Set (Int, Int)
expected = [(Int, Int)] -> Set (Int, Int)
forall a. Ord a => [a] -> Set a
Set.fromList [(Int
1,Int
4),(Int
1,Int
5),(Int
1,Int
6),(Int
2,Int
4),(Int
2,Int
5),(Int
2,Int
6),(Int
3,Int
4),(Int
3,Int
5),(Int
3,Int
6)] :: Set (Int, Int)

{-
let rec distinctpairs l =
  match l with
   x::t -> itlist (fun y a -> (x,y) :: a) t (distinctpairs t)
  | [] -> [];;

let rec chop_list n l =
  if n = 0 then [],l else
  try let m,l' = chop_list (n-1) (tl l) in (hd l)::m,l'
  with Failure _ -> failwith "chop_list";;

let replicate n a = map (fun x -> a) (1--n);;

let rec insertat i x l =
  if i = 0 then x::l else
  match l with
    [] -> failwith "insertat: list too short for position to exist"
  | h::t -> h::(insertat (i-1) x t);;

let rec forall2 p l1 l2 =
  match (l1,l2) with
    [],[] -> true
  | (h1::t1,h2::t2) -> p h1 h2 & forall2 p t1 t2
  | _ -> false;;

let index x =
  let rec ind n l =
    match l with
      [] -> failwith "index"
    | (h::t) -> if Pervasives.compare x h = 0 then n else ind (n + 1) t in
  ind 0;;

let rec unzip l =
  match l with
    [] -> [],[]
  | (x,y)::t ->
      let xs,ys = unzip t in x::xs,y::ys;;

(* ------------------------------------------------------------------------- *)
(* Whether the first of two items comes earlier in the list.                 *)
(* ------------------------------------------------------------------------- *)

let rec earlier l x y =
  match l with
    h::t -> (Pervasives.compare h y <> 0) &
            (Pervasives.compare h x = 0 or earlier t x y)
  | [] -> false;;

(* ------------------------------------------------------------------------- *)
(* Application of (presumably imperative) function over a list.              *)
(* ------------------------------------------------------------------------- *)

let rec do_list f l =
  match l with
    [] -> ()
  | h::t -> f(h); do_list f t;;

(* ------------------------------------------------------------------------- *)
(* Association lists.                                                        *)
(* ------------------------------------------------------------------------- *)

let rec assoc a l =
  match l with
    (x,y)::t -> if Pervasives.compare x a = 0 then y else assoc a t
  | [] -> failwith "find";;

let rec rev_assoc a l =
  match l with
    (x,y)::t -> if Pervasives.compare y a = 0 then x else rev_assoc a t
  | [] -> failwith "find";;

(* ------------------------------------------------------------------------- *)
(* Merging of sorted lists (maintaining repetitions).                        *)
(* ------------------------------------------------------------------------- *)

let rec merge ord l1 l2 =
  match l1 with
    [] -> l2
  | h1::t1 -> match l2 with
                [] -> l1
              | h2::t2 -> if ord h1 h2 then h1::(merge ord t1 l2)
                          else h2::(merge ord l1 t2);;

(* ------------------------------------------------------------------------- *)
(* Bottom-up mergesort.                                                      *)
(* ------------------------------------------------------------------------- *)

let sort ord =
  let rec mergepairs l1 l2 =
    match (l1,l2) with
        ([s],[]) -> s
      | (l,[]) -> mergepairs [] l
      | (l,[s1]) -> mergepairs (s1::l) []
      | (l,(s1::s2::ss)) -> mergepairs ((merge ord s1 s2)::l) ss in
  fun l -> if l = [] then [] else mergepairs [] (map (fun x -> [x]) l);;

(* ------------------------------------------------------------------------- *)
(* Common measure predicates to use with "sort".                             *)
(* ------------------------------------------------------------------------- *)

let increasing f x y = Pervasives.compare (f x) (f y) < 0;;

let decreasing f x y = Pervasives.compare (f x) (f y) > 0;;

(* ------------------------------------------------------------------------- *)
(* Eliminate repetitions of adjacent elements, with and without counting.    *)
(* ------------------------------------------------------------------------- *)

let rec uniq l =
  match l with
    x::(y::_ as t) -> let t' = uniq t in
                      if Pervasives.compare x y = 0 then t' else
                      if t'==t then l else x::t'
 | _ -> l;;

let repetitions =
  let rec repcount n l =
    match l with
      x::(y::_ as ys) -> if Pervasives.compare y x = 0 then repcount (n + 1) ys
                  else (x,n)::(repcount 1 ys)
    | [x] -> [x,n]
    | [] -> failwith "repcount" in
  fun l -> if l = [] then [] else repcount 1 l;;
-}

tryfind :: Foldable t => (a -> Failing r) -> t a -> Failing r
tryfind :: forall (t :: * -> *) a r.
Foldable t =>
(a -> Failing r) -> t a -> Failing r
tryfind a -> Failing r
p t a
s = Failing r -> (a -> Failing r) -> Maybe a -> Failing r
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing r
forall a. [String] -> Failing a
Failure [String
"tryfind"]) a -> Failing r
p ((a -> Bool) -> t a -> Maybe a
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([String] -> Bool) -> (r -> Bool) -> Failing r -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> r -> Bool
forall a b. a -> b -> a
const Bool
True) (Failing r -> Bool) -> (a -> Failing r) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Failing r
p) t a
s)

tryfindM :: Monad m => (t -> m (Failing a)) -> [t] -> m (Failing a)
tryfindM :: forall (m :: * -> *) t a.
Monad m =>
(t -> m (Failing a)) -> [t] -> m (Failing a)
tryfindM t -> m (Failing a)
_ [] = Failing a -> m (Failing a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing a -> m (Failing a)) -> Failing a -> m (Failing a)
forall a b. (a -> b) -> a -> b
$ [String] -> Failing a
forall a. [String] -> Failing a
Failure [String
"tryfindM"]
tryfindM t -> m (Failing a)
f (t
h : [t]
t) = t -> m (Failing a)
f t
h m (Failing a) -> (Failing a -> m (Failing a)) -> m (Failing a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([String] -> m (Failing a))
-> (a -> m (Failing a)) -> Failing a -> m (Failing a)
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (\[String]
_ -> (t -> m (Failing a)) -> [t] -> m (Failing a)
forall (m :: * -> *) t a.
Monad m =>
(t -> m (Failing a)) -> [t] -> m (Failing a)
tryfindM t -> m (Failing a)
f [t]
t) (Failing a -> m (Failing a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing a -> m (Failing a))
-> (a -> Failing a) -> a -> m (Failing a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Failing a
forall a. a -> Failing a
Success)

evalRS :: RWS r () s a -> r -> s -> a
evalRS :: forall r s a. RWS r () s a -> r -> s -> a
evalRS RWS r () s a
action r
r s
s = (a, ()) -> a
forall a b. (a, b) -> a
fst ((a, ()) -> a) -> (a, ()) -> a
forall a b. (a -> b) -> a -> b
$ RWS r () s a -> r -> s -> (a, ())
forall r w s a. RWS r w s a -> r -> s -> (a, w)
evalRWS RWS r () s a
action r
r s
s

runRS :: RWS r () s a -> r -> s -> (a, s)
runRS :: forall r s a. RWS r () s a -> r -> s -> (a, s)
runRS RWS r () s a
action r
r s
s = (\(a
a, s
s', ()
_w) -> (a
a, s
s')) ((a, s, ()) -> (a, s)) -> (a, s, ()) -> (a, s)
forall a b. (a -> b) -> a -> b
$ RWS r () s a -> r -> s -> (a, s, ())
forall r w s a. RWS r w s a -> r -> s -> (a, s, w)
runRWS RWS r () s a
action r
r s
s

test02 :: Test
test02 :: Test
test02 =
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$
    String -> Failing Int -> Failing Int -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual
      String
"tryfind on infinite list"
      (Int -> Failing Int
forall a. a -> Failing a
Success Int
3 :: Failing Int)
      ((Int -> Failing Int) -> [Int] -> Failing Int
forall (t :: * -> *) a r.
Foldable t =>
(a -> Failing r) -> t a -> Failing r
tryfind (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3
                      then Int -> Failing Int
forall a. a -> Failing a
Success Int
3
                      else [String] -> Failing Int
forall a. [String] -> Failing a
Failure [String
"test02"]) ([Int
1..] :: [Int]))

settryfind :: (t -> Failing a) -> Set t -> Failing a
settryfind :: forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind t -> Failing a
f Set t
l =
    case Set t -> Maybe (t, Set t)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set t
l of
      Maybe (t, Set t)
Nothing -> [String] -> Failing a
forall a. [String] -> Failing a
Failure [String
"settryfind"]
      Just (t
h, Set t
t) -> ([String] -> Failing a)
-> (a -> Failing a) -> Failing a -> Failing a
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (\ [String]
_ -> (t -> Failing a) -> Set t -> Failing a
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind t -> Failing a
f Set t
t) a -> Failing a
forall a. a -> Failing a
Success (t -> Failing a
f t
h)

mapfilter :: (a -> Failing b) -> [a] -> [b]
mapfilter :: forall a b. (a -> Failing b) -> [a] -> [b]
mapfilter a -> Failing b
f [a]
l = [Maybe b] -> [b]
forall a. [Maybe a] -> [a]
catMaybes ((a -> Maybe b) -> [a] -> [Maybe b]
forall a b. (a -> b) -> [a] -> [b]
List.map (([String] -> Maybe b) -> (b -> Maybe b) -> Failing b -> Maybe b
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Maybe b -> [String] -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing) b -> Maybe b
forall a. a -> Maybe a
Just (Failing b -> Maybe b) -> (a -> Failing b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Failing b
f) [a]
l)
    -- filter (failing (const False) (const True)) (map f l)

setmapfilter :: Ord b => (a -> Failing b) -> Set a -> Set b
setmapfilter :: forall b a. Ord b => (a -> Failing b) -> Set a -> Set b
setmapfilter a -> Failing b
f Set a
s = (a -> Set b -> Set b) -> Set b -> Set a -> Set b
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ a
a Set b
r -> ([String] -> Set b) -> (b -> Set b) -> Failing b -> Set b
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Set b -> [String] -> Set b
forall a b. a -> b -> a
const Set b
r) (b -> Set b -> Set b
forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set b
r) (a -> Failing b
f a
a)) Set b
forall a. Set a
Set.empty Set a
s

-- -------------------------------------------------------------------------
-- Find list member that maximizes or minimizes a function.
-- -------------------------------------------------------------------------

optimize :: forall s a b. (SetLike s, Foldable s) => (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
optimize :: forall (s :: * -> *) a b.
(SetLike s, Foldable s) =>
(b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
optimize b -> b -> Ordering
_ a -> b
_ s a
l | Maybe (a, s a) -> Bool
forall a. Maybe a -> Bool
isNothing (s a -> Maybe (a, s a)
forall a. s a -> Maybe (a, s a)
forall (c :: * -> *) a. SetLike c => c a -> Maybe (a, c a)
slView s a
l) = Maybe a
forall a. Maybe a
Nothing
optimize b -> b -> Ordering
ord a -> b
f s a
l = a -> Maybe a
forall a. a -> Maybe a
Just ((a -> a -> Ordering) -> s a -> a
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
Foldable.maximumBy (b -> b -> Ordering
ord (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) s a
l)

maximize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a
maximize :: forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
maximize = (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
forall (s :: * -> *) a b.
(SetLike s, Foldable s) =>
(b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
optimize b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare

minimize :: (Ord b, SetLike s, Foldable s) => (a -> b) -> s a -> Maybe a
minimize :: forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
minimize = (b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
forall (s :: * -> *) a b.
(SetLike s, Foldable s) =>
(b -> b -> Ordering) -> (a -> b) -> s a -> Maybe a
optimize ((b -> b -> Ordering) -> b -> b -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare)

-- -------------------------------------------------------------------------
-- Set operations on ordered lists.
-- -------------------------------------------------------------------------
{-
let setify =
  let rec canonical lis =
     match lis with
       x::(y::_ as rest) -> Pervasives.compare x y < 0 & canonical rest
     | _ -> true in
  fun l -> if canonical l then l
           else uniq (sort (fun x y -> Pervasives.compare x y <= 0) l);;

let union =
  let rec union l1 l2 =
    match (l1,l2) with
        ([],l2) -> l2
      | (l1,[]) -> l1
      | ((h1::t1 as l1),(h2::t2 as l2)) ->
          if h1 = h2 then h1::(union t1 t2)
          else if h1 < h2 then h1::(union t1 l2)
          else h2::(union l1 t2) in
  fun s1 s2 -> union (setify s1) (setify s2);;

let intersect =
  let rec intersect l1 l2 =
    match (l1,l2) with
        ([],l2) -> []
      | (l1,[]) -> []
      | ((h1::t1 as l1),(h2::t2 as l2)) ->
          if h1 = h2 then h1::(intersect t1 t2)
          else if h1 < h2 then intersect t1 l2
          else intersect l1 t2 in
  fun s1 s2 -> intersect (setify s1) (setify s2);;

let subtract =
  let rec subtract l1 l2 =
    match (l1,l2) with
        ([],l2) -> []
      | (l1,[]) -> l1
      | ((h1::t1 as l1),(h2::t2 as l2)) ->
          if h1 = h2 then subtract t1 t2
          else if h1 < h2 then h1::(subtract t1 l2)
          else subtract l1 t2 in
  fun s1 s2 -> subtract (setify s1) (setify s2);;

let subset,psubset =
  let rec subset l1 l2 =
    match (l1,l2) with
        ([],l2) -> true
      | (l1,[]) -> false
      | (h1::t1,h2::t2) ->
          if h1 = h2 then subset t1 t2
          else if h1 < h2 then false
          else subset l1 t2
  and psubset l1 l2 =
    match (l1,l2) with
        (l1,[]) -> false
      | ([],l2) -> true
      | (h1::t1,h2::t2) ->
          if h1 = h2 then psubset t1 t2
          else if h1 < h2 then false
          else subset l1 t2 in
  (fun s1 s2 -> subset (setify s1) (setify s2)),
  (fun s1 s2 -> psubset (setify s1) (setify s2));;

let rec set_eq s1 s2 = (setify s1 = setify s2);;

let insert x s = union [x] s;;
-}

image :: (Ord b, Ord a) => (a -> b) -> Set a -> Set b
image :: forall b a. (Ord b, Ord a) => (a -> b) -> Set a -> Set b
image a -> b
f Set a
s = (a -> b) -> Set a -> Set b
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> b
f Set a
s

{-
(* ------------------------------------------------------------------------- *)
(* Union of a family of sets.                                                *)
(* ------------------------------------------------------------------------- *)

let unions s = setify(itlist (@) s []);;

(* ------------------------------------------------------------------------- *)
(* List membership. This does *not* assume the list is a set.                *)
(* ------------------------------------------------------------------------- *)

let rec mem x lis =
  match lis with
    [] -> false
  | (h::t) -> Pervasives.compare x h = 0 or mem x t;;
-}

-- -------------------------------------------------------------------------
-- Finding all subsets or all subsets of a given size.
-- -------------------------------------------------------------------------

-- allsets :: Ord a => Int -> Set a -> Set (Set a)
allsets :: forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets :: forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets a
0 Set b
_ = Set b -> Set (Set b)
forall a. a -> Set a
Set.singleton Set b
forall a. Set a
Set.empty
allsets a
m Set b
l =
    case Set b -> Maybe (b, Set b)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set b
l of
      Maybe (b, Set b)
Nothing -> Set (Set b)
forall a. Set a
Set.empty
      Just (b
h, Set b
t) -> Set (Set b) -> Set (Set b) -> Set (Set b)
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((Set b -> Set b) -> Set (Set b) -> Set (Set b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (b -> Set b -> Set b
forall a. Ord a => a -> Set a -> Set a
Set.insert b
h) (a -> Set b -> Set (Set b)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets (a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
1) Set b
t)) (a -> Set b -> Set (Set b)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets a
m Set b
t)

allsubsets :: forall a. Ord a => Set a -> Set (Set a)
allsubsets :: forall a. Ord a => Set a -> Set (Set a)
allsubsets Set a
s =
    Set (Set a)
-> ((a, Set a) -> Set (Set a)) -> Maybe (a, Set a) -> Set (Set a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Set a -> Set (Set a)
forall a. a -> Set a
Set.singleton Set a
forall a. Set a
Set.empty)
          (\ (a
x, Set a
t) ->
               let res :: Set (Set a)
res = Set a -> Set (Set a)
forall a. Ord a => Set a -> Set (Set a)
allsubsets Set a
t in
               Set (Set a) -> Set (Set a) -> Set (Set a)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Set a)
res ((Set a -> Set a) -> Set (Set a) -> Set (Set a)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x) Set (Set a)
res))
          (Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set a
s)


allnonemptysubsets :: forall a. Ord a => Set a -> Set (Set a)
allnonemptysubsets :: forall a. Ord a => Set a -> Set (Set a)
allnonemptysubsets Set a
s = Set a -> Set (Set a) -> Set (Set a)
forall a. Ord a => a -> Set a -> Set a
Set.delete Set a
forall a. Set a
Set.empty (Set a -> Set (Set a)
forall a. Ord a => Set a -> Set (Set a)
allsubsets Set a
s)

{-
(* ------------------------------------------------------------------------- *)
(* Explosion and implosion of strings.                                       *)
(* ------------------------------------------------------------------------- *)

let explode s =
  let rec exap n l =
     if n < 0 then l else
      exap (n - 1) ((String.sub s n 1)::l) in
  exap (String.length s - 1) [];;

let implode l = itlist (^) l "";;

(* ------------------------------------------------------------------------- *)
(* Timing; useful for documentation but not logically necessary.             *)
(* ------------------------------------------------------------------------- *)

let time f x =
  let start_time = Sys.time() in
  let result = f x in
  let finish_time = Sys.time() in
  print_string
    ("CPU time (user): "^(string_of_float(finish_time -. start_time)));
  print_newline();
  result;;
-}

-- | Perform an IO operation and return the elapsed time along with the result.
timeComputation :: IO r -> IO (r, NominalDiffTime)
timeComputation :: forall r. IO r -> IO (r, NominalDiffTime)
timeComputation IO r
a = do
  UTCTime
start <- IO UTCTime
getCurrentTime
  r
r <- IO r
a
  UTCTime
end <- IO UTCTime
getCurrentTime
  (r, NominalDiffTime) -> IO (r, NominalDiffTime)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (r
r, UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
end UTCTime
start)

-- | Perform an IO operation and output a message about how long it took.
timeMessage :: (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage :: forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage r -> NominalDiffTime -> String
pp IO r
a = do
  (r
r, NominalDiffTime
e) <- IO r -> IO (r, NominalDiffTime)
forall r. IO r -> IO (r, NominalDiffTime)
timeComputation IO r
a
  Handle -> String -> Assertion
hPutStrLn Handle
stderr (r -> NominalDiffTime -> String
pp r
r NominalDiffTime
e)
  r -> IO r
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return r
r

-- | Output elapsed time
time :: IO r -> IO r
time :: forall r. IO r -> IO r
time IO r
a = (r -> NominalDiffTime -> String) -> IO r -> IO r
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\r
_ NominalDiffTime
e -> String
"Computation time: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
e) IO r
a

-- | Allow a computation to proceed for a given amount of time.
timeout :: String -> DiffTime -> IO r -> IO (Either String r)
timeout :: forall r. String -> DiffTime -> IO r -> IO (Either String r)
timeout String
message DiffTime
delay IO r
a = do
  [IO (Either String r)] -> IO (Either String r)
forall a. [IO a] -> IO a
compete [Int -> Assertion
threadDelay (Rational -> Int
forall a. Enum a => a -> Int
fromEnum (DiffTime -> Rational
forall a b. (Real a, Fractional b) => a -> b
realToFrac (DiffTime
delay DiffTime -> DiffTime -> DiffTime
forall a. Fractional a => a -> a -> a
/ DiffTime
1e6) :: Rational)) Assertion -> IO (Either String r) -> IO (Either String r)
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either String r -> IO (Either String r)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String r
forall a b. a -> Either a b
Left String
message),
           r -> Either String r
forall a b. b -> Either a b
Right (r -> Either String r) -> IO r -> IO (Either String r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO r
a]

-- | Run several IO operations in parallel, return the result of the
-- first one that completes and kill the others.
compete :: [IO a] -> IO a
compete :: forall a. [IO a] -> IO a
compete [IO a]
actions = do
  MVar a
mvar <- IO (MVar a)
forall a. IO (MVar a)
newEmptyMVar
  [ThreadId]
tids <- (IO a -> IO ThreadId) -> [IO a] -> IO [ThreadId]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\IO a
action -> Assertion -> IO ThreadId
forkIO (Assertion -> IO ThreadId) -> Assertion -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ IO a
action IO a -> (a -> Assertion) -> Assertion
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MVar a -> a -> Assertion
forall a. MVar a -> a -> Assertion
putMVar MVar a
mvar) [IO a]
actions
  a
result <- MVar a -> IO a
forall a. MVar a -> IO a
takeMVar MVar a
mvar
  (ThreadId -> Assertion) -> [ThreadId] -> Assertion
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ThreadId -> Assertion
killThread [ThreadId]
tids
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result

-- | Polymorphic finite partial functions via Patricia trees.
--
-- The point of this strange representation is that it is canonical (equal
-- functions have the same encoding) yet reasonably efficient on average.
--
-- Idea due to Diego Olivier Fernandez Pons (OCaml list, 2003/11/10).
data Func a b
    = Empty
    | Leaf Int [(a, b)]
    | Branch Int Int (Func a b) (Func a b)

-- | Undefined function.
undefinedFunction :: Func a b
undefinedFunction :: forall a b. Func a b
undefinedFunction = Func a b
forall a b. Func a b
Empty

-- -------------------------------------------------------------------------
-- In case of equality comparison worries, better use this.
-- -------------------------------------------------------------------------

isUndefined :: Func a b -> Bool
isUndefined :: forall a b. Func a b -> Bool
isUndefined Func a b
Empty = Bool
True
isUndefined Func a b
_ = Bool
False

-- -------------------------------------------------------------------------
-- Operation analogous to "map" for functions.
-- -------------------------------------------------------------------------

mapf :: (b -> c) -> Func a b -> Func a c
mapf :: forall b c a. (b -> c) -> Func a b -> Func a c
mapf b -> c
f Func a b
t =
    case Func a b
t of
      Func a b
Empty -> Func a c
forall a b. Func a b
Empty
      Leaf Int
h [(a, b)]
l -> Int -> [(a, c)] -> Func a c
forall a b. Int -> [(a, b)] -> Func a b
Leaf Int
h ((b -> c) -> [(a, b)] -> [(a, c)]
forall {t} {b} {a}. (t -> b) -> [(a, t)] -> [(a, b)]
map_list b -> c
f [(a, b)]
l)
      Branch Int
p Int
b Func a b
l Func a b
r -> Int -> Int -> Func a c -> Func a c -> Func a c
forall a b. Int -> Int -> Func a b -> Func a b -> Func a b
Branch Int
p Int
b ((b -> c) -> Func a b -> Func a c
forall b c a. (b -> c) -> Func a b -> Func a c
mapf b -> c
f Func a b
l) ((b -> c) -> Func a b -> Func a c
forall b c a. (b -> c) -> Func a b -> Func a c
mapf b -> c
f Func a b
r)
    where
      map_list :: (t -> b) -> [(a, t)] -> [(a, b)]
map_list t -> b
f' [(a, t)]
l' =
          case [(a, t)]
l' of
            [] -> []
            (a
x,t
y) : [(a, t)]
t' -> (a
x, t -> b
f' t
y) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: (t -> b) -> [(a, t)] -> [(a, b)]
map_list t -> b
f' [(a, t)]
t'

-- -------------------------------------------------------------------------
-- Operations analogous to "fold" for lists.
-- -------------------------------------------------------------------------

foldlFn :: (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn :: forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn r -> a -> b -> r
f r
a Func a b
t =
    case Func a b
t of
      Func a b
Empty -> r
a
      Leaf Int
_h [(a, b)]
l -> (r -> a -> b -> r) -> r -> [(a, b)] -> r
foldl_list r -> a -> b -> r
f r
a [(a, b)]
l
      Branch Int
_p Int
_b Func a b
l Func a b
r -> (r -> a -> b -> r) -> r -> Func a b -> r
forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn r -> a -> b -> r
f ((r -> a -> b -> r) -> r -> Func a b -> r
forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn r -> a -> b -> r
f r
a Func a b
l) Func a b
r
    where
      foldl_list :: (r -> a -> b -> r) -> r -> [(a, b)] -> r
foldl_list r -> a -> b -> r
_f r
a' [(a, b)]
l =
          case [(a, b)]
l of
            [] -> r
a'
            (a
x,b
y) : [(a, b)]
t' -> (r -> a -> b -> r) -> r -> [(a, b)] -> r
foldl_list r -> a -> b -> r
f (r -> a -> b -> r
f r
a' a
x b
y) [(a, b)]
t'

foldrFn :: (a -> b -> r -> r) -> Func a b -> r -> r
foldrFn :: forall a b r. (a -> b -> r -> r) -> Func a b -> r -> r
foldrFn a -> b -> r -> r
f Func a b
t r
a =
    case Func a b
t of
      Func a b
Empty -> r
a
      Leaf Int
_h [(a, b)]
l -> (a -> b -> r -> r) -> [(a, b)] -> r -> r
forall {t} {t} {t}. (t -> t -> t -> t) -> [(t, t)] -> t -> t
foldr_list a -> b -> r -> r
f [(a, b)]
l r
a
      Branch Int
_p Int
_b Func a b
l Func a b
r -> (a -> b -> r -> r) -> Func a b -> r -> r
forall a b r. (a -> b -> r -> r) -> Func a b -> r -> r
foldrFn a -> b -> r -> r
f Func a b
l ((a -> b -> r -> r) -> Func a b -> r -> r
forall a b r. (a -> b -> r -> r) -> Func a b -> r -> r
foldrFn a -> b -> r -> r
f Func a b
r r
a)
    where
      foldr_list :: (t -> t -> t -> t) -> [(t, t)] -> t -> t
foldr_list t -> t -> t -> t
f' [(t, t)]
l t
a' =
          case [(t, t)]
l of
            [] -> t
a'
            (t
x, t
y) : [(t, t)]
t' -> t -> t -> t -> t
f' t
x t
y ((t -> t -> t -> t) -> [(t, t)] -> t -> t
foldr_list t -> t -> t -> t
f' [(t, t)]
t' t
a')

-- -------------------------------------------------------------------------
-- Mapping to sorted-list representation of the graph, domain and range.
-- -------------------------------------------------------------------------

graph :: (Ord a, Ord b) => Func a b -> Set (a, b)
graph :: forall a b. (Ord a, Ord b) => Func a b -> Set (a, b)
graph Func a b
f = [(a, b)] -> Set (a, b)
forall a. Ord a => [a] -> Set a
Set.fromList (([(a, b)] -> a -> b -> [(a, b)])
-> [(a, b)] -> Func a b -> [(a, b)]
forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn (\ [(a, b)]
a a
x b
y -> (a
x,b
y) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
a) [] Func a b
f)

dom :: Ord a => Func a b -> Set a
dom :: forall a b. Ord a => Func a b -> Set a
dom Func a b
f = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList (([a] -> a -> b -> [a]) -> [a] -> Func a b -> [a]
forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn (\ [a]
a a
x b
_y -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
a) [] Func a b
f)

ran :: Ord b => Func a b -> Set b
ran :: forall b a. Ord b => Func a b -> Set b
ran Func a b
f = [b] -> Set b
forall a. Ord a => [a] -> Set a
Set.fromList (([b] -> a -> b -> [b]) -> [b] -> Func a b -> [b]
forall r a b. (r -> a -> b -> r) -> r -> Func a b -> r
foldlFn (\ [b]
a a
_x b
y -> b
y b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
a) [] Func a b
f)

-- -------------------------------------------------------------------------
-- Application.
-- -------------------------------------------------------------------------

applyD :: Ord k => Map k a -> k -> a -> Map k a
applyD :: forall k a. Ord k => Map k a -> k -> a -> Map k a
applyD Map k a
m k
k a
a = k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k a
a Map k a
m

apply :: Ord k => Map k a -> k -> Maybe a
apply :: forall k a. Ord k => Map k a -> k -> Maybe a
apply Map k a
m k
k = k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k a
m

tryApplyD :: Ord k => Map k a -> k -> a -> a
tryApplyD :: forall k a. Ord k => Map k a -> k -> a -> a
tryApplyD Map k a
m k
k a
d = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
d (k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k a
m)

tryApplyL :: Ord k => Map k [a] -> k -> [a]
tryApplyL :: forall k a. Ord k => Map k [a] -> k -> [a]
tryApplyL Map k [a]
m k
k = Map k [a] -> k -> [a] -> [a]
forall k a. Ord k => Map k a -> k -> a -> a
tryApplyD Map k [a]
m k
k []
{-
applyD :: (t -> Maybe b) -> (t -> b) -> t -> b
applyD f d x = maybe (d x) id (f x)

apply :: (t -> Maybe b) -> t -> b
apply f = applyD f (\ _ -> error "apply")

tryApplyD :: (t -> Maybe b) -> t -> b -> b
tryApplyD f a d = maybe d id (f a)

tryApplyL :: (t -> Maybe [a]) -> t -> [a]
tryApplyL f x = tryApplyD f x []
-}

defined :: Ord t => Map t a -> t -> Bool
defined :: forall t a. Ord t => Map t a -> t -> Bool
defined = (t -> Map t a -> Bool) -> Map t a -> t -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip t -> Map t a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member

-- | Undefinition.
undefine :: forall k a. Ord k => k -> Map k a -> Map k a
undefine :: forall k a. Ord k => k -> Map k a -> Map k a
undefine k
k Map k a
mp = k -> Map k a -> Map k a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete k
k Map k a
mp

{-
(* ------------------------------------------------------------------------- *)
(* Redefinition and combination.                                             *)
(* ------------------------------------------------------------------------- *)

let (|->),combine =
  let newbranch p1 t1 p2 t2 =
    let zp = p1 lxor p2 in
    let b = zp land (-zp) in
    let p = p1 land (b - 1) in
    if p1 land b = 0 then Branch(p,b,t1,t2)
    else Branch(p,b,t2,t1) in
  let rec define_list (x,y as xy) l =
    match l with
      (a,b as ab)::t ->
          let c = Pervasives.compare x a in
          if c = 0 then xy::t
          else if c < 0 then xy::l
          else ab::(define_list xy t)
    | [] -> [xy]
  and combine_list op z l1 l2 =
    match (l1,l2) with
      [],_ -> l2
    | _,[] -> l1
    | ((x1,y1 as xy1)::t1,(x2,y2 as xy2)::t2) ->
          let c = Pervasives.compare x1 x2 in
          if c < 0 then xy1::(combine_list op z t1 l2)
          else if c > 0 then xy2::(combine_list op z l1 t2) else
          let y = op y1 y2 and l = combine_list op z t1 t2 in
          if z(y) then l else (x1,y)::l in
  let (|->) x y =
    let k = Hashtbl.hash x in
    let rec upd t =
      match t with
        Empty -> Leaf (k,[x,y])
      | Leaf(h,l) ->
           if h = k then Leaf(h,define_list (x,y) l)
           else newbranch h t k (Leaf(k,[x,y]))
      | Branch(p,b,l,r) ->
          if k land (b - 1) <> p then newbranch p t k (Leaf(k,[x,y]))
          else if k land b = 0 then Branch(p,b,upd l,r)
          else Branch(p,b,l,upd r) in
    upd in
  let rec combine op z t1 t2 =
    match (t1,t2) with
      Empty,_ -> t2
    | _,Empty -> t1
    | Leaf(h1,l1),Leaf(h2,l2) ->
          if h1 = h2 then
            let l = combine_list op z l1 l2 in
            if l = [] then Empty else Leaf(h1,l)
          else newbranch h1 t1 h2 t2
    | (Leaf(k,lis) as lf),(Branch(p,b,l,r) as br) ->
          if k land (b - 1) = p then
            if k land b = 0 then
              (match combine op z lf l with
                 Empty -> r | l' -> Branch(p,b,l',r))
            else
              (match combine op z lf r with
                 Empty -> l | r' -> Branch(p,b,l,r'))
          else
            newbranch k lf p br
    | (Branch(p,b,l,r) as br),(Leaf(k,lis) as lf) ->
          if k land (b - 1) = p then
            if k land b = 0 then
              (match combine op z l lf with
                Empty -> r | l' -> Branch(p,b,l',r))
            else
              (match combine op z r lf with
                 Empty -> l | r' -> Branch(p,b,l,r'))
          else
            newbranch p br k lf
    | Branch(p1,b1,l1,r1),Branch(p2,b2,l2,r2) ->
          if b1 < b2 then
            if p2 land (b1 - 1) <> p1 then newbranch p1 t1 p2 t2
            else if p2 land b1 = 0 then
              (match combine op z l1 t2 with
                 Empty -> r1 | l -> Branch(p1,b1,l,r1))
            else
              (match combine op z r1 t2 with
                 Empty -> l1 | r -> Branch(p1,b1,l1,r))
          else if b2 < b1 then
            if p1 land (b2 - 1) <> p2 then newbranch p1 t1 p2 t2
            else if p1 land b2 = 0 then
              (match combine op z t1 l2 with
                 Empty -> r2 | l -> Branch(p2,b2,l,r2))
            else
              (match combine op z t1 r2 with
                 Empty -> l2 | r -> Branch(p2,b2,l2,r))
          else if p1 = p2 then
           (match (combine op z l1 l2,combine op z r1 r2) with
              (Empty,r) -> r | (l,Empty) -> l | (l,r) -> Branch(p1,b1,l,r))
          else
            newbranch p1 t1 p2 t2 in
  (|->),combine;;
-}

-- -------------------------------------------------------------------------
-- Special case of point function.
-- -------------------------------------------------------------------------

(|=>) :: Ord k => k -> a -> Map k a
k
x |=> :: forall k a. Ord k => k -> a -> Map k a
|=> a
y = k -> a -> Map k a
forall k a. k -> a -> Map k a
Map.singleton k
x a
y

-- -------------------------------------------------------------------------
-- Idiom for a mapping zipping domain and range lists.
-- -------------------------------------------------------------------------

(|->) :: Ord k => k -> a -> Map k a -> Map k a
|-> :: forall k a. Ord k => k -> a -> Map k a -> Map k a
(|->) = k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert

fpf :: Ord a => Map a b -> a -> Maybe b
fpf :: forall k a. Ord k => Map k a -> k -> Maybe a
fpf = (a -> Map a b -> Maybe b) -> Map a b -> a -> Maybe b
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup

-- -------------------------------------------------------------------------
-- Grab an arbitrary element.
-- -------------------------------------------------------------------------

choose :: Map k a -> (k, a)
choose :: forall k a. Map k a -> (k, a)
choose = Map k a -> (k, a)
forall k a. Map k a -> (k, a)
Map.findMin

{-
(* ------------------------------------------------------------------------- *)
(* Install a (trivial) printer for finite partial functions.                 *)
(* ------------------------------------------------------------------------- *)

let print_fpf (f:('a,'b)func) = print_string "<func>";;

#install_printer print_fpf;;

(* ------------------------------------------------------------------------- *)
(* Related stuff for standard functions.                                     *)
(* ------------------------------------------------------------------------- *)

let valmod a y f x = if x = a then y else f(x);;

let undef x = failwith "undefined function";;

(* ------------------------------------------------------------------------- *)
(* Union-find algorithm.                                                     *)
(* ------------------------------------------------------------------------- *)

type ('a)pnode = Nonterminal of 'a | Terminal of 'a * int;;

type ('a)partition = Partition of ('a,('a)pnode)func;;

let rec terminus (Partition f as ptn) a =
  match (apply f a) with
    Nonterminal(b) -> terminus ptn b
  | Terminal(p,q) -> (p,q);;

let tryterminus ptn a =
  try terminus ptn a with Failure _ -> (a,1);;

let canonize ptn a = fst(tryterminus ptn a);;

let equivalent eqv a b = canonize eqv a = canonize eqv b;;

let equate (a,b) (Partition f as ptn) =
  let (a',na) = tryterminus ptn a
  and (b',nb) = tryterminus ptn b in
  Partition
   (if a' = b' then f else
    if na <= nb then
       itlist identity [a' |-> Nonterminal b'; b' |-> Terminal(b',na+nb)] f
    else
       itlist identity [b' |-> Nonterminal a'; a' |-> Terminal(a',na+nb)] f);;

let unequal = Partition undefined;;

let equated (Partition f) = dom f;;

(* ------------------------------------------------------------------------- *)
(* First number starting at n for which p succeeds.                          *)
(* ------------------------------------------------------------------------- *)

let rec first n p = if p(n) then n else first (n +/ Int 1) p;;
-}

-- | Try f with higher and higher values of n until it succeeds, or
-- optional maximum depth limit is exceeded.
{-
let rec deepen f n =
  try print_string "Searching with depth limit ";
      print_int n; print_newline(); f n
  with Failure _ -> deepen f (n + 1);;
-}
deepen :: (Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen :: forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen Depth -> Failing t
_ Depth
n (Just Depth
m) | Depth
n Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
> Depth
m = [String] -> Failing (t, Depth)
forall a. [String] -> Failing a
Failure [String
"Exceeded maximum depth limit"]
deepen Depth -> Failing t
f Depth
n Maybe Depth
m =
    -- If no maximum depth limit is given print a trace of the
    -- levels tried.  The assumption is that we are running
    -- interactively.
    let n' :: Depth
n' = Depth -> (Depth -> Depth) -> Maybe Depth -> Depth
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Depth -> Depth
forall a. String -> a -> a
trace (String
"Searching with depth limit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Depth -> String
forall a. Show a => a -> String
show Depth
n) Depth
n) (\Depth
_ -> Depth
n) Maybe Depth
m in
    case Depth -> Failing t
f Depth
n' of
      Failure [String]
_ -> (Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen Depth -> Failing t
f (Depth -> Depth
forall a. Enum a => a -> a
succ Depth
n) Maybe Depth
m
      Success t
x -> (t, Depth) -> Failing (t, Depth)
forall a. a -> Failing a
Success (t
x, Depth
n)

newtype Depth = Depth Int deriving (Depth -> Depth -> Bool
(Depth -> Depth -> Bool) -> (Depth -> Depth -> Bool) -> Eq Depth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Depth -> Depth -> Bool
== :: Depth -> Depth -> Bool
$c/= :: Depth -> Depth -> Bool
/= :: Depth -> Depth -> Bool
Eq, Eq Depth
Eq Depth =>
(Depth -> Depth -> Ordering)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Bool)
-> (Depth -> Depth -> Depth)
-> (Depth -> Depth -> Depth)
-> Ord Depth
Depth -> Depth -> Bool
Depth -> Depth -> Ordering
Depth -> Depth -> Depth
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Depth -> Depth -> Ordering
compare :: Depth -> Depth -> Ordering
$c< :: Depth -> Depth -> Bool
< :: Depth -> Depth -> Bool
$c<= :: Depth -> Depth -> Bool
<= :: Depth -> Depth -> Bool
$c> :: Depth -> Depth -> Bool
> :: Depth -> Depth -> Bool
$c>= :: Depth -> Depth -> Bool
>= :: Depth -> Depth -> Bool
$cmax :: Depth -> Depth -> Depth
max :: Depth -> Depth -> Depth
$cmin :: Depth -> Depth -> Depth
min :: Depth -> Depth -> Depth
Ord, Int -> Depth -> String -> String
[Depth] -> String -> String
Depth -> String
(Int -> Depth -> String -> String)
-> (Depth -> String) -> ([Depth] -> String -> String) -> Show Depth
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Depth -> String -> String
showsPrec :: Int -> Depth -> String -> String
$cshow :: Depth -> String
show :: Depth -> String
$cshowList :: [Depth] -> String -> String
showList :: [Depth] -> String -> String
Show)

instance Enum Depth where
    toEnum :: Int -> Depth
toEnum = Int -> Depth
Depth
    fromEnum :: Depth -> Int
fromEnum (Depth Int
n) = Int
n

instance Pretty Depth where
    pPrint :: Depth -> Doc
pPrint = String -> Doc
text (String -> Doc) -> (Depth -> String) -> Depth -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Depth -> String
forall a. Show a => a -> String
show

testLib :: Test
testLib :: Test
testLib = String -> Test -> Test
TestLabel String
"Lib" ([Test] -> Test
TestList [Test
test01])