{- |
module: $Header$
description: Utility functions
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.Util
where

-------------------------------------------------------------------------------
-- Creating unsafe versions of functions
-------------------------------------------------------------------------------

mkUnsafe :: String -> Maybe a -> a
mkUnsafe :: String -> Maybe a -> a
mkUnsafe String
_ (Just a
x) = a
x
mkUnsafe String
s Maybe a
Nothing = String -> a
forall a. HasCallStack => String -> a
error (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" failed")

mkUnsafe1 :: String -> (a -> Maybe b) -> a -> b
mkUnsafe1 :: String -> (a -> Maybe b) -> a -> b
mkUnsafe1 String
s a -> Maybe b
f = String -> Maybe b -> b
forall a. String -> Maybe a -> a
mkUnsafe String
s (Maybe b -> b) -> (a -> Maybe b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f

mkUnsafe2 :: String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 :: String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
s a -> b -> Maybe c
f = String -> (b -> Maybe c) -> b -> c
forall a b. String -> (a -> Maybe b) -> a -> b
mkUnsafe1 String
s ((b -> Maybe c) -> b -> c) -> (a -> b -> Maybe c) -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> Maybe c
f