{-# LANGUAGE CPP, PatternSynonyms, ViewPatterns,
MagicHash, UnboxedTuples, BangPatterns,
RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving,
OverloadedStrings, RoleAnnotations #-}
{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
#ifdef USE_LLVM
{-# OPTIONS_GHC -fllvm #-}
#endif
module Twee.Term.Core where
import Data.Primitive(sizeOf)
#ifdef BOUNDS_CHECKS
import Data.Primitive.ByteArray.Checked
#else
import Data.Primitive.ByteArray
#endif
import Control.Monad.ST.Strict
import Data.Bits
import Data.Int
import GHC.Types(Int(..))
import GHC.Prim
import GHC.ST hiding (liftST)
import Data.Ord
import Twee.Profile
data Symbol =
Symbol {
Symbol -> Bool
isFun :: Bool,
Symbol -> Int
index :: Int,
Symbol -> Int
size :: Int }
instance Show Symbol where
show :: Symbol -> String
show Symbol{Bool
Int
size :: Int
index :: Int
isFun :: Bool
size :: Symbol -> Int
index :: Symbol -> Int
isFun :: Symbol -> Bool
..}
| Bool
isFun = String
"f" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
index forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
| Bool
otherwise = forall a. Show a => a -> String
show (Int -> Var
V Int
index)
{-# INLINE toSymbol #-}
toSymbol :: Int64 -> Symbol
toSymbol :: Int64 -> Symbol
toSymbol Int64
n =
Bool -> Int -> Int -> Symbol
Symbol (forall a. Bits a => a -> Int -> Bool
testBit Int64
n Int
31)
(forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
n forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
32))
(forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
n forall a. Bits a => a -> a -> a
.&. Int64
0x7fffffff))
{-# INLINE fromSymbol #-}
fromSymbol :: Symbol -> Int64
fromSymbol :: Symbol -> Int64
fromSymbol Symbol{Bool
Int
size :: Int
index :: Int
isFun :: Bool
size :: Symbol -> Int
index :: Symbol -> Int
isFun :: Symbol -> Bool
..} =
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
size forall a. Num a => a -> a -> a
+
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
index forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
32 forall a. Num a => a -> a -> a
+
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Enum a => a -> Int
fromEnum Bool
isFun) forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
31
{-# INLINE symbolSize #-}
symbolSize :: Int
symbolSize :: Int
symbolSize = forall a. Prim a => a -> Int
sizeOf (Symbol -> Int64
fromSymbol forall a. HasCallStack => a
undefined)
data TermList f =
TermList {
forall f. TermList f -> Int
low :: {-# UNPACK #-} !Int,
forall f. TermList f -> Int
high :: {-# UNPACK #-} !Int,
forall f. TermList f -> ByteArray
array :: {-# UNPACK #-} !ByteArray }
type role TermList nominal
at :: Int -> TermList f -> Term f
at :: forall f. Int -> TermList f -> Term f
at Int
n TermList f
t
| Int
n forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| forall f. TermList f -> Int
low TermList f
t forall a. Num a => a -> a -> a
+ Int
n forall a. Ord a => a -> a -> Bool
>= forall f. TermList f -> Int
high TermList f
t = forall a. HasCallStack => String -> a
error String
"term index out of bounds"
| Bool
otherwise = forall f. Int -> TermList f -> Term f
unsafeAt Int
n TermList f
t
unsafeAt :: Int -> TermList f -> Term f
unsafeAt :: forall f. Int -> TermList f -> Term f
unsafeAt Int
n (TermList Int
lo Int
hi ByteArray
arr) =
case forall f. Int -> Int -> ByteArray -> TermList f
TermList (Int
loforall a. Num a => a -> a -> a
+Int
n) Int
hi ByteArray
arr of
UnsafeCons Term f
t TermList f
_ -> Term f
t
{-# INLINE lenList #-}
lenList :: TermList f -> Int
lenList :: forall f. TermList f -> Int
lenList (TermList Int
low Int
high ByteArray
_) = Int
high forall a. Num a => a -> a -> a
- Int
low
data Term f =
Term {
forall f. Term f -> Int64
root :: {-# UNPACK #-} !Int64,
forall f. Term f -> TermList f
termlist :: {-# UNPACK #-} !(TermList f) }
type role Term nominal
instance Eq (Term f) where
Term f
x == :: Term f -> Term f -> Bool
== Term f
y = forall f. Term f -> TermList f
termlist Term f
x forall a. Eq a => a -> a -> Bool
== forall f. Term f -> TermList f
termlist Term f
y
instance Ord (Term f) where
compare :: Term f -> Term f -> Ordering
compare = forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall f. Term f -> TermList f
termlist
pattern Empty :: TermList f
pattern $mEmpty :: forall {r} {f}. TermList f -> ((# #) -> r) -> ((# #) -> r) -> r
Empty <- (patHead -> Nothing)
pattern Cons :: Term f -> TermList f -> TermList f
pattern $mCons :: forall {r} {f}.
TermList f -> (Term f -> TermList f -> r) -> ((# #) -> r) -> r
Cons t ts <- (patHead -> Just (t, _, ts))
{-# COMPLETE Empty, Cons #-}
{-# COMPLETE Empty, ConsSym #-}
pattern UnsafeCons :: Term f -> TermList f -> TermList f
pattern $mUnsafeCons :: forall {r} {f}.
TermList f -> (Term f -> TermList f -> r) -> ((# #) -> r) -> r
UnsafeCons t ts <- (unsafePatHead -> (t, _, ts))
pattern ConsSym :: Term f -> TermList f -> TermList f -> TermList f
pattern $mConsSym :: forall {r} {f}.
TermList f
-> (Term f -> TermList f -> TermList f -> r) -> ((# #) -> r) -> r
ConsSym{forall f. TermList f -> Term f
hd, forall f. TermList f -> TermList f
tl, forall f. TermList f -> TermList f
rest} <- (patHead -> Just (hd, rest, tl))
pattern UnsafeConsSym :: Term f -> TermList f -> TermList f -> TermList f
pattern $mUnsafeConsSym :: forall {r} {f}.
TermList f
-> (Term f -> TermList f -> TermList f -> r) -> ((# #) -> r) -> r
UnsafeConsSym{forall f. TermList f -> Term f
uhd, forall f. TermList f -> TermList f
utl, forall f. TermList f -> TermList f
urest} <- (unsafePatHead -> (uhd, urest, utl))
{-# INLINE unsafePatHead #-}
unsafePatHead :: TermList f -> (Term f, TermList f, TermList f)
unsafePatHead :: forall f. TermList f -> (Term f, TermList f, TermList f)
unsafePatHead TermList{Int
ByteArray
array :: ByteArray
high :: Int
low :: Int
array :: forall f. TermList f -> ByteArray
high :: forall f. TermList f -> Int
low :: forall f. TermList f -> Int
..} =
(forall f. Int64 -> TermList f -> Term f
Term Int64
x (forall f. Int -> Int -> ByteArray -> TermList f
TermList Int
low (Int
lowforall a. Num a => a -> a -> a
+Int
size) ByteArray
array),
forall f. Int -> Int -> ByteArray -> TermList f
TermList (Int
lowforall a. Num a => a -> a -> a
+Int
1) Int
high ByteArray
array,
forall f. Int -> Int -> ByteArray -> TermList f
TermList (Int
lowforall a. Num a => a -> a -> a
+Int
size) Int
high ByteArray
array)
where
!x :: Int64
x = forall a. Prim a => ByteArray -> Int -> a
indexByteArray ByteArray
array Int
low
Symbol{Bool
Int
index :: Int
isFun :: Bool
size :: Int
size :: Symbol -> Int
index :: Symbol -> Int
isFun :: Symbol -> Bool
..} = Int64 -> Symbol
toSymbol Int64
x
{-# INLINE patHead #-}
patHead :: TermList f -> Maybe (Term f, TermList f, TermList f)
patHead :: forall f. TermList f -> Maybe (Term f, TermList f, TermList f)
patHead t :: TermList f
t@TermList{Int
ByteArray
array :: ByteArray
high :: Int
low :: Int
array :: forall f. TermList f -> ByteArray
high :: forall f. TermList f -> Int
low :: forall f. TermList f -> Int
..}
| Int
low forall a. Eq a => a -> a -> Bool
== Int
high = forall a. Maybe a
Nothing
| Bool
otherwise = forall a. a -> Maybe a
Just (forall f. TermList f -> (Term f, TermList f, TermList f)
unsafePatHead TermList f
t)
newtype Fun f =
F {
forall f. Fun f -> Int
fun_id :: Int }
deriving (Fun f -> Fun f -> Bool
forall f. Fun f -> Fun f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Fun f -> Fun f -> Bool
$c/= :: forall f. Fun f -> Fun f -> Bool
== :: Fun f -> Fun f -> Bool
$c== :: forall f. Fun f -> Fun f -> Bool
Eq, Fun f -> Fun f -> Bool
Fun f -> Fun f -> Ordering
Fun f -> Fun f -> Fun f
forall f. Eq (Fun f)
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
forall f. Fun f -> Fun f -> Bool
forall f. Fun f -> Fun f -> Ordering
forall f. Fun f -> Fun f -> Fun f
min :: Fun f -> Fun f -> Fun f
$cmin :: forall f. Fun f -> Fun f -> Fun f
max :: Fun f -> Fun f -> Fun f
$cmax :: forall f. Fun f -> Fun f -> Fun f
>= :: Fun f -> Fun f -> Bool
$c>= :: forall f. Fun f -> Fun f -> Bool
> :: Fun f -> Fun f -> Bool
$c> :: forall f. Fun f -> Fun f -> Bool
<= :: Fun f -> Fun f -> Bool
$c<= :: forall f. Fun f -> Fun f -> Bool
< :: Fun f -> Fun f -> Bool
$c< :: forall f. Fun f -> Fun f -> Bool
compare :: Fun f -> Fun f -> Ordering
$ccompare :: forall f. Fun f -> Fun f -> Ordering
Ord)
type role Fun nominal
newtype Var =
V {
Var -> Int
var_id :: Int } deriving (Var -> Var -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
Ord, Int -> Var
Var -> Int
Var -> [Var]
Var -> Var
Var -> Var -> [Var]
Var -> Var -> Var -> [Var]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Var -> Var -> Var -> [Var]
$cenumFromThenTo :: Var -> Var -> Var -> [Var]
enumFromTo :: Var -> Var -> [Var]
$cenumFromTo :: Var -> Var -> [Var]
enumFromThen :: Var -> Var -> [Var]
$cenumFromThen :: Var -> Var -> [Var]
enumFrom :: Var -> [Var]
$cenumFrom :: Var -> [Var]
fromEnum :: Var -> Int
$cfromEnum :: Var -> Int
toEnum :: Int -> Var
$ctoEnum :: Int -> Var
pred :: Var -> Var
$cpred :: Var -> Var
succ :: Var -> Var
$csucc :: Var -> Var
Enum)
instance Show Var where
show :: Var -> String
show Var
x = String
"x" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Var -> Int
var_id Var
x)
pattern Var :: Var -> Term f
pattern $mVar :: forall {r} {f}. Term f -> (Var -> r) -> ((# #) -> r) -> r
Var x <- (patTerm -> Left x)
pattern App :: Fun f -> TermList f -> Term f
pattern $mApp :: forall {r} {f}.
Term f -> (Fun f -> TermList f -> r) -> ((# #) -> r) -> r
App f ts <- (patTerm -> Right (f, ts))
{-# COMPLETE Var, App #-}
{-# INLINE patTerm #-}
patTerm :: Term f -> Either Var (Fun f, TermList f)
patTerm :: forall f. Term f -> Either Var (Fun f, TermList f)
patTerm Term{Int64
TermList f
termlist :: TermList f
root :: Int64
termlist :: forall f. Term f -> TermList f
root :: forall f. Term f -> Int64
..}
| Bool
isFun = forall a b. b -> Either a b
Right (forall f. Int -> Fun f
F Int
index, TermList f
ts)
| Bool
otherwise = forall a b. a -> Either a b
Left (Int -> Var
V Int
index)
where
Symbol{Bool
Int
size :: Int
index :: Int
isFun :: Bool
size :: Symbol -> Int
index :: Symbol -> Int
isFun :: Symbol -> Bool
..} = Int64 -> Symbol
toSymbol Int64
root
!UnsafeConsSym{urest :: forall f. TermList f -> TermList f
urest = TermList f
ts} = TermList f
termlist
{-# INLINE singleton #-}
singleton :: Term f -> TermList f
singleton :: forall f. Term f -> TermList f
singleton Term{Int64
TermList f
termlist :: TermList f
root :: Int64
termlist :: forall f. Term f -> TermList f
root :: forall f. Term f -> Int64
..} = TermList f
termlist
instance Eq (TermList f) where
TermList f
t == :: TermList f -> TermList f -> Bool
== TermList f
u =
forall f. TermList f -> Int
lenList TermList f
t forall a. Eq a => a -> a -> Bool
== forall f. TermList f -> Int
lenList TermList f
u Bool -> Bool -> Bool
&&
forall f. TermList f -> TermList f -> Ordering
compareSameLength TermList f
t TermList f
u forall a. Eq a => a -> a -> Bool
== Ordering
EQ
instance Ord (TermList f) where
{-# INLINE compare #-}
compare :: TermList f -> TermList f -> Ordering
compare TermList f
t TermList f
u =
forall a. Ord a => a -> a -> Ordering
compare (forall f. TermList f -> Int
lenList TermList f
t) (forall f. TermList f -> Int
lenList TermList f
u) forall a. Monoid a => a -> a -> a
`mappend`
forall f. TermList f -> TermList f -> Ordering
compareSameLength TermList f
t TermList f
u
{-# INLINE compareSameLength #-}
compareSameLength :: TermList f -> TermList f -> Ordering
compareSameLength :: forall f. TermList f -> TermList f -> Ordering
compareSameLength TermList f
t TermList f
u =
ByteArray -> Int -> ByteArray -> Int -> Int -> Ordering
compareByteArrays (forall f. TermList f -> ByteArray
array TermList f
t) (forall f. TermList f -> Int
low TermList f
t forall a. Num a => a -> a -> a
* Int
k)
(forall f. TermList f -> ByteArray
array TermList f
u) (forall f. TermList f -> Int
low TermList f
u forall a. Num a => a -> a -> a
* Int
k) ((forall f. TermList f -> Int
high TermList f
t forall a. Num a => a -> a -> a
- forall f. TermList f -> Int
low TermList f
t) forall a. Num a => a -> a -> a
* Int
k)
where
k :: Int
k = Int
symbolSize
newtype Builder f =
Builder {
forall f. Builder f -> forall s. Builder1 s f
unBuilder ::
forall s. Builder1 s f }
type role Builder nominal
type Builder1 s f = State# s -> MutableByteArray# s -> Int# -> (# State# s, MutableByteArray# s, Int# #)
instance Semigroup (Builder f) where
{-# INLINE (<>) #-}
Builder forall s. Builder1 s f
m1 <> :: Builder f -> Builder f -> Builder f
<> Builder forall s. Builder1 s f
m2 = forall f. (forall s. Builder1 s f) -> Builder f
Builder (forall s. Builder1 s f
m1 forall s f. Builder1 s f -> Builder1 s f -> Builder1 s f
`then_` forall s. Builder1 s f
m2)
instance Monoid (Builder f) where
{-# INLINE mempty #-}
mempty :: Builder f
mempty = forall f. (forall s. Builder1 s f) -> Builder f
Builder forall s f. Builder1 s f
built
{-# INLINE mappend #-}
mappend :: Builder f -> Builder f -> Builder f
mappend = forall a. Semigroup a => a -> a -> a
(<>)
{-# INLINE buildTermList #-}
buildTermList :: Builder f -> TermList f
buildTermList :: forall f. Builder f -> TermList f
buildTermList (Builder forall s. Builder1 s f
m) = forall symbol a. symbol -> a -> a
stamp String
"build term" forall a b. (a -> b) -> a -> b
$ forall a. (forall s. ST s a) -> a
runST forall a b. (a -> b) -> a -> b
$ do
MutableByteArray MutableByteArray# s
marr# <-
forall (m :: * -> *).
PrimMonad m =>
Int -> m (MutableByteArray (PrimState m))
newByteArray (Int
16 forall a. Num a => a -> a -> a
* Int
symbolSize)
(MutableByteArray s
marr, Int
n) <-
forall s a. STRep s a -> ST s a
ST forall a b. (a -> b) -> a -> b
$ \State# s
s ->
case forall s. Builder1 s f
m State# s
s MutableByteArray# s
marr# Int#
0# of
(# State# s
s, MutableByteArray# s
marr#, Int#
n# #) ->
(# State# s
s, (forall s. MutableByteArray# s -> MutableByteArray s
MutableByteArray MutableByteArray# s
marr#, Int# -> Int
I# Int#
n#) #)
forall (m :: * -> *).
PrimMonad m =>
MutableByteArray (PrimState m) -> Int -> m ()
shrinkMutableByteArray MutableByteArray s
marr (Int
n forall a. Num a => a -> a -> a
* Int
symbolSize)
!ByteArray
arr <- forall (m :: * -> *).
PrimMonad m =>
MutableByteArray (PrimState m) -> m ByteArray
unsafeFreezeByteArray MutableByteArray s
marr
forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. Int -> Int -> ByteArray -> TermList f
TermList Int
0 Int
n ByteArray
arr)
{-# INLINE built #-}
built :: Builder1 s f
built :: forall s f. Builder1 s f
built State# s
s MutableByteArray# s
arr# Int#
n# = (# State# s
s, MutableByteArray# s
arr#, Int#
n# #)
{-# INLINE then_ #-}
then_ :: Builder1 s f -> Builder1 s f -> Builder1 s f
Builder1 s f
m1 then_ :: forall s f. Builder1 s f -> Builder1 s f -> Builder1 s f
`then_` Builder1 s f
m2 = \State# s
s MutableByteArray# s
arr# Int#
n# ->
case Builder1 s f
m1 State# s
s MutableByteArray# s
arr# Int#
n# of
(# State# s
s, MutableByteArray# s
arr#, Int#
n# #) ->
Builder1 s f
m2 State# s
s MutableByteArray# s
arr# Int#
n#
{-# INLINE emitSymbolBuilder #-}
emitSymbolBuilder :: Symbol -> Builder f -> Builder f
emitSymbolBuilder :: forall f. Symbol -> Builder f -> Builder f
emitSymbolBuilder Symbol
x (Builder forall s. Builder1 s f
inner) =
forall f. (forall s. Builder1 s f) -> Builder f
Builder forall a b. (a -> b) -> a -> b
$ \State# s
s MutableByteArray# s
arr# Int#
n# ->
let n :: Int
n = Int# -> Int
I# Int#
n# in
case forall s.
State# s
-> MutableByteArray# s
-> Int#
-> (# State# s, MutableByteArray# s #)
reserve State# s
s MutableByteArray# s
arr# (Int -> Int#
unInt (Int
n forall a. Num a => a -> a -> a
+ Int
1)) of
(# State# s
s, MutableByteArray# s
arr# #) ->
case forall s. Builder1 s f
inner State# s
s MutableByteArray# s
arr# (Int -> Int#
unInt (Int
n forall a. Num a => a -> a -> a
+ Int
1)) of
(# State# s
s, MutableByteArray# s
arr#, Int#
m# #) ->
let arr :: MutableByteArray s
arr = forall s. MutableByteArray# s -> MutableByteArray s
MutableByteArray MutableByteArray# s
arr#
m :: Int
m = Int# -> Int
I# Int#
m# in
case forall s a. ST s a -> State# s -> (# State# s, a #)
unST (forall a (m :: * -> *).
(Prim a, PrimMonad m) =>
MutableByteArray (PrimState m) -> Int -> a -> m ()
writeByteArray MutableByteArray s
arr Int
n (Symbol -> Int64
fromSymbol Symbol
x { size :: Int
size = Int
m forall a. Num a => a -> a -> a
- Int
n })) State# s
s of
(# State# s
s, () #) ->
(# State# s
s, MutableByteArray# s
arr#, Int#
m# #)
{-# INLINE emitApp #-}
emitApp :: Fun f -> Builder f -> Builder f
emitApp :: forall f. Fun f -> Builder f -> Builder f
emitApp (F Int
n) Builder f
inner = forall f. Symbol -> Builder f -> Builder f
emitSymbolBuilder (Bool -> Int -> Int -> Symbol
Symbol Bool
True Int
n Int
0) Builder f
inner
{-# INLINE emitVar #-}
emitVar :: Var -> Builder f
emitVar :: forall f. Var -> Builder f
emitVar Var
x = forall f. Symbol -> Builder f -> Builder f
emitSymbolBuilder (Bool -> Int -> Int -> Symbol
Symbol Bool
False (Var -> Int
var_id Var
x) Int
1) forall a. Monoid a => a
mempty
{-# INLINE emitTermList #-}
emitTermList :: TermList f -> Builder f
emitTermList :: forall f. TermList f -> Builder f
emitTermList (TermList Int
lo Int
hi ByteArray
array) =
forall f. (forall s. Builder1 s f) -> Builder f
Builder forall a b. (a -> b) -> a -> b
$ \State# s
s MutableByteArray# s
arr# Int#
n# ->
let n :: Int
n = Int# -> Int
I# Int#
n# in
case forall s.
State# s
-> MutableByteArray# s
-> Int#
-> (# State# s, MutableByteArray# s #)
reserve State# s
s MutableByteArray# s
arr# (Int -> Int#
unInt (Int
n forall a. Num a => a -> a -> a
+ Int
hi forall a. Num a => a -> a -> a
- Int
lo)) of
(# State# s
s, MutableByteArray# s
arr# #) ->
let k :: Int
k = Int
symbolSize
arr :: MutableByteArray s
arr = forall s. MutableByteArray# s -> MutableByteArray s
MutableByteArray MutableByteArray# s
arr# in
case forall s a. ST s a -> State# s -> (# State# s, a #)
unST (forall (m :: * -> *).
PrimMonad m =>
MutableByteArray (PrimState m)
-> Int -> ByteArray -> Int -> Int -> m ()
copyByteArray MutableByteArray s
arr (Int
nforall a. Num a => a -> a -> a
*Int
k) ByteArray
array (Int
loforall a. Num a => a -> a -> a
*Int
k) ((Int
hi forall a. Num a => a -> a -> a
- Int
lo)forall a. Num a => a -> a -> a
*Int
k)) State# s
s of
(# State# s
s, () #) ->
(# State# s
s, MutableByteArray# s
arr#, Int -> Int#
unInt (Int
n forall a. Num a => a -> a -> a
+ Int
hi forall a. Num a => a -> a -> a
- Int
lo) #)
{-# NOINLINE reserve #-}
reserve :: State# s -> MutableByteArray# s -> Int# -> (# State# s, MutableByteArray# s #)
reserve :: forall s.
State# s
-> MutableByteArray# s
-> Int#
-> (# State# s, MutableByteArray# s #)
reserve State# s
s MutableByteArray# s
arr# Int#
n# =
case forall {m :: * -> *}.
PrimMonad m =>
MutableByteArray (PrimState m)
-> Int -> m (MutableByteArray (PrimState m))
reserve' (forall s. MutableByteArray# s -> MutableByteArray s
MutableByteArray MutableByteArray# s
arr#) (Int# -> Int
I# Int#
n#) of
ST STRep s (MutableByteArray s)
m ->
case STRep s (MutableByteArray s)
m State# s
s of
(# State# s
s, MutableByteArray MutableByteArray# s
arr# #) ->
(# State# s
s, MutableByteArray# s
arr# #)
where
{-# INLINE reserve' #-}
reserve' :: MutableByteArray (PrimState m)
-> Int -> m (MutableByteArray (PrimState m))
reserve' MutableByteArray (PrimState m)
arr Int
n = do
let !m :: Int
m = Int
nforall a. Num a => a -> a -> a
*Int
symbolSize
Int
size <- forall (m :: * -> *).
PrimMonad m =>
MutableByteArray (PrimState m) -> m Int
getSizeofMutableByteArray MutableByteArray (PrimState m)
arr
if Int
size forall a. Ord a => a -> a -> Bool
>= Int
m then forall (m :: * -> *) a. Monad m => a -> m a
return MutableByteArray (PrimState m)
arr else forall {m :: * -> *}.
PrimMonad m =>
MutableByteArray (PrimState m)
-> Int -> Int -> m (MutableByteArray (PrimState m))
expand MutableByteArray (PrimState m)
arr (Int
sizeforall a. Num a => a -> a -> a
*Int
2) Int
m
expand :: MutableByteArray (PrimState m)
-> Int -> Int -> m (MutableByteArray (PrimState m))
expand MutableByteArray (PrimState m)
arr Int
size Int
m
| Int
size forall a. Ord a => a -> a -> Bool
>= Int
m = forall {m :: * -> *}.
PrimMonad m =>
MutableByteArray (PrimState m)
-> Int -> m (MutableByteArray (PrimState m))
resizeMutableByteArray MutableByteArray (PrimState m)
arr Int
size
| Bool
otherwise = MutableByteArray (PrimState m)
-> Int -> Int -> m (MutableByteArray (PrimState m))
expand MutableByteArray (PrimState m)
arr (Int
sizeforall a. Num a => a -> a -> a
*Int
2) Int
m
unST :: ST s a -> State# s -> (# State# s, a #)
unST :: forall s a. ST s a -> State# s -> (# State# s, a #)
unST (ST STRep s a
m) = STRep s a
m
unInt :: Int -> Int#
unInt :: Int -> Int#
unInt (I# Int#
n) = Int#
n
{-# INLINE isSubtermOfList #-}
isSubtermOfList :: Term f -> TermList f -> Bool
isSubtermOfList :: forall f. Term f -> TermList f -> Bool
isSubtermOfList Term f
t TermList f
u =
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ forall f. Term f -> TermList f
singleton Term f
t forall a. Eq a => a -> a -> Bool
== TermList f
u{low :: Int
low = forall f. TermList f -> Int
low TermList f
u forall a. Num a => a -> a -> a
+ Int
i, high :: Int
high = forall f. TermList f -> Int
low TermList f
u forall a. Num a => a -> a -> a
+ Int
i forall a. Num a => a -> a -> a
+ Int
n}
| Int
i <- [Int
0..forall f. TermList f -> Int
lenList TermList f
u forall a. Num a => a -> a -> a
- Int
n]]
where
n :: Int
n = forall f. TermList f -> Int
lenList (forall f. Term f -> TermList f
singleton Term f
t)
{-# INLINE occursList #-}
occursList :: Var -> TermList f -> Bool
occursList :: forall f. Var -> TermList f -> Bool
occursList (V Int
x) TermList f
t = forall f. Int64 -> TermList f -> Bool
symbolOccursList (Symbol -> Int64
fromSymbol (Bool -> Int -> Int -> Symbol
Symbol Bool
False Int
x Int
1)) TermList f
t
symbolOccursList :: Int64 -> TermList f -> Bool
symbolOccursList :: forall f. Int64 -> TermList f -> Bool
symbolOccursList !Int64
_ TermList f
Empty = Bool
False
symbolOccursList Int64
n ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts} = forall f. Term f -> Int64
root Term f
t forall a. Eq a => a -> a -> Bool
== Int64
n Bool -> Bool -> Bool
|| forall f. Int64 -> TermList f -> Bool
symbolOccursList Int64
n TermList f
ts