{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

-- Needed for Pretty instance
{-# LANGUAGE UndecidableInstances #-}
module Lang.Crucible.Simulator.SymSequence
( SymSequence(..)
, nilSymSequence
, consSymSequence
, fromListSymSequence
, appendSymSequence
, muxSymSequence
, isNilSymSequence
, lengthSymSequence
, headSymSequence
, tailSymSequence
, unconsSymSequence
, traverseSymSequence
, concreteizeSymSequence
, concretizeSymSequence
, prettySymSequence

  -- * Low-level evaluation primitives
, newSeqCache
, evalWithCache
, evalWithFreshCache
) where

import           Control.Monad.State
import           Data.Functor.Const
import           Data.Kind (Type)
import           Data.IORef
import           Data.Maybe (isJust)
import           Data.Map (Map)
import qualified Data.Map as Map
import           Data.Parameterized.Nonce
import qualified Data.Parameterized.Map as MapF
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Prettyprinter (Doc)
import qualified Prettyprinter as PP

import           Lang.Crucible.Types
import           What4.Interface
import           What4.Partial

------------------------------------------------------------------------
-- SymSequence

-- | A symbolic sequence of values supporting efficent merge operations.
--   Semantically, these are essentially cons-lists, and designed to
--   support access from the front only.  Nodes carry nonce values
--   that allow DAG-based traversal, which efficently supports the common
--   case where merged nodes share a common sublist.
data SymSequence sym a where
  SymSequenceNil :: SymSequence sym a

  SymSequenceCons ::
    !(Nonce GlobalNonceGenerator a) ->
    a ->
    !(SymSequence sym a) ->
    SymSequence sym a

  SymSequenceAppend ::
    !(Nonce GlobalNonceGenerator a) ->
    !(SymSequence sym a) ->
    !(SymSequence sym a) ->
    SymSequence sym a

  SymSequenceMerge ::
    !(Nonce GlobalNonceGenerator a) ->
    !(Pred sym) ->
    !(SymSequence sym a) ->
    !(SymSequence sym a) ->
    SymSequence sym a

instance Eq (SymSequence sym a) where
  SymSequence sym a
SymSequenceNil == :: SymSequence sym a -> SymSequence sym a -> Bool
== SymSequence sym a
SymSequenceNil = Bool
True
  (SymSequenceCons Nonce GlobalNonceGenerator a
n1 a
_ SymSequence sym a
_) == (SymSequenceCons Nonce GlobalNonceGenerator a
n2 a
_ SymSequence sym a
_) =
    Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator a -> Maybe (a :~: a)
forall a b.
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Nonce GlobalNonceGenerator a
n1 Nonce GlobalNonceGenerator a
n2)
  (SymSequenceMerge Nonce GlobalNonceGenerator a
n1 Pred sym
_ SymSequence sym a
_ SymSequence sym a
_) == (SymSequenceMerge Nonce GlobalNonceGenerator a
n2 Pred sym
_ SymSequence sym a
_ SymSequence sym a
_) =
    Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator a -> Maybe (a :~: a)
forall a b.
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Nonce GlobalNonceGenerator a
n1 Nonce GlobalNonceGenerator a
n2)
  (SymSequenceAppend Nonce GlobalNonceGenerator a
n1 SymSequence sym a
_ SymSequence sym a
_) == (SymSequenceAppend Nonce GlobalNonceGenerator a
n2 SymSequence sym a
_ SymSequence sym a
_) =
    Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator a -> Maybe (a :~: a)
forall a b.
Nonce GlobalNonceGenerator a
-> Nonce GlobalNonceGenerator b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Nonce GlobalNonceGenerator a
n1 Nonce GlobalNonceGenerator a
n2)
  SymSequence sym a
_ == SymSequence sym a
_ = Bool
False

-- | Compute an if/then/else on symbolic sequences.
--   This will simply produce an internal merge node
--   except in the special case where the then and
--   else branches are sytactically identical.
muxSymSequence ::
  sym ->
  Pred sym ->
  SymSequence sym a ->
  SymSequence sym a ->
  IO (SymSequence sym a)
muxSymSequence :: forall sym a.
sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
muxSymSequence sym
_sym Pred sym
p SymSequence sym a
x SymSequence sym a
y
  | SymSequence sym a
x SymSequence sym a -> SymSequence sym a -> Bool
forall a. Eq a => a -> a -> Bool
== SymSequence sym a
y = SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym a
x
  | Bool
otherwise =
      do Nonce GlobalNonceGenerator a
n <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator a)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
         SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Nonce GlobalNonceGenerator a
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> SymSequence sym a
forall a sym.
Nonce GlobalNonceGenerator a
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> SymSequence sym a
SymSequenceMerge Nonce GlobalNonceGenerator a
n Pred sym
p SymSequence sym a
x SymSequence sym a
y)

newtype SeqCache (f :: Type -> Type)
  = SeqCache (IORef (MapF.MapF (Nonce GlobalNonceGenerator) f))

newSeqCache :: IO (SeqCache f)
newSeqCache :: forall (f :: Type -> Type). IO (SeqCache f)
newSeqCache = IORef (MapF (Nonce GlobalNonceGenerator) f) -> SeqCache f
forall (f :: Type -> Type).
IORef (MapF (Nonce GlobalNonceGenerator) f) -> SeqCache f
SeqCache (IORef (MapF (Nonce GlobalNonceGenerator) f) -> SeqCache f)
-> IO (IORef (MapF (Nonce GlobalNonceGenerator) f))
-> IO (SeqCache f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MapF (Nonce GlobalNonceGenerator) f
-> IO (IORef (MapF (Nonce GlobalNonceGenerator) f))
forall a. a -> IO (IORef a)
newIORef MapF (Nonce GlobalNonceGenerator) f
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

-- | Compute the nonce of a sequence, if it has one
symSequenceNonce :: SymSequence sym a -> Maybe (Nonce GlobalNonceGenerator a)
symSequenceNonce :: forall sym a.
SymSequence sym a -> Maybe (Nonce GlobalNonceGenerator a)
symSequenceNonce SymSequence sym a
SymSequenceNil = Maybe (Nonce GlobalNonceGenerator a)
forall a. Maybe a
Nothing
symSequenceNonce (SymSequenceCons Nonce GlobalNonceGenerator a
n a
_ SymSequence sym a
_ ) = Nonce GlobalNonceGenerator a
-> Maybe (Nonce GlobalNonceGenerator a)
forall a. a -> Maybe a
Just Nonce GlobalNonceGenerator a
n
symSequenceNonce (SymSequenceAppend Nonce GlobalNonceGenerator a
n SymSequence sym a
_ SymSequence sym a
_) = Nonce GlobalNonceGenerator a
-> Maybe (Nonce GlobalNonceGenerator a)
forall a. a -> Maybe a
Just Nonce GlobalNonceGenerator a
n
symSequenceNonce (SymSequenceMerge Nonce GlobalNonceGenerator a
n Pred sym
_ SymSequence sym a
_ SymSequence sym a
_) = Nonce GlobalNonceGenerator a
-> Maybe (Nonce GlobalNonceGenerator a)
forall a. a -> Maybe a
Just Nonce GlobalNonceGenerator a
n

{-# SPECIALIZE
  evalWithFreshCache ::
  ((SymSequence sym a -> IO (f a)) -> SymSequence sym a -> IO (f a)) ->
  (SymSequence sym a -> IO (f a))
 #-}

evalWithFreshCache :: MonadIO m =>
  ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) ->
  (SymSequence sym a -> m (f a))
evalWithFreshCache :: forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
fn SymSequence sym a
s =
  do SeqCache f
c <- IO (SeqCache f) -> m (SeqCache f)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO IO (SeqCache f)
forall (f :: Type -> Type). IO (SeqCache f)
newSeqCache
     SeqCache f
-> ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a
-> m (f a)
forall (m :: Type -> Type) (f :: Type -> Type) sym a.
MonadIO m =>
SeqCache f
-> ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a
-> m (f a)
evalWithCache SeqCache f
c (SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
fn SymSequence sym a
s

{-# SPECIALIZE
  evalWithCache ::
  SeqCache f ->
  ((SymSequence sym a -> IO (f a)) -> SymSequence sym a -> IO (f a)) ->
  (SymSequence sym a -> IO (f a))
 #-}

evalWithCache :: MonadIO m =>
  SeqCache f ->
  ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)) ->
  (SymSequence sym a -> m (f a))
evalWithCache :: forall (m :: Type -> Type) (f :: Type -> Type) sym a.
MonadIO m =>
SeqCache f
-> ((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a
-> m (f a)
evalWithCache (SeqCache IORef (MapF (Nonce GlobalNonceGenerator) f)
ref) (SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
fn = SymSequence sym a -> m (f a)
loop
  where
    loop :: SymSequence sym a -> m (f a)
loop SymSequence sym a
s
      | Just Nonce GlobalNonceGenerator a
n <- SymSequence sym a -> Maybe (Nonce GlobalNonceGenerator a)
forall sym a.
SymSequence sym a -> Maybe (Nonce GlobalNonceGenerator a)
symSequenceNonce SymSequence sym a
s =
          (Nonce GlobalNonceGenerator a
-> MapF (Nonce GlobalNonceGenerator) f -> Maybe (f a)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup Nonce GlobalNonceGenerator a
n (MapF (Nonce GlobalNonceGenerator) f -> Maybe (f a))
-> m (MapF (Nonce GlobalNonceGenerator) f) -> m (Maybe (f a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (MapF (Nonce GlobalNonceGenerator) f)
-> m (MapF (Nonce GlobalNonceGenerator) f)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IORef (MapF (Nonce GlobalNonceGenerator) f)
-> IO (MapF (Nonce GlobalNonceGenerator) f)
forall a. IORef a -> IO a
readIORef IORef (MapF (Nonce GlobalNonceGenerator) f)
ref)) m (Maybe (f a)) -> (Maybe (f a) -> m (f a)) -> m (f a)
forall a b. m a -> (a -> m b) -> m b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Just f a
v -> f a -> m (f a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure f a
v
            Maybe (f a)
Nothing ->
              do f a
v <- (SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
fn SymSequence sym a -> m (f a)
loop SymSequence sym a
s
                 IO () -> m ()
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IORef (MapF (Nonce GlobalNonceGenerator) f)
-> (MapF (Nonce GlobalNonceGenerator) f
    -> MapF (Nonce GlobalNonceGenerator) f)
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (MapF (Nonce GlobalNonceGenerator) f)
ref (Nonce GlobalNonceGenerator a
-> f a
-> MapF (Nonce GlobalNonceGenerator) f
-> MapF (Nonce GlobalNonceGenerator) f
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert Nonce GlobalNonceGenerator a
n f a
v))
                 f a -> m (f a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure f a
v

      | Bool
otherwise = (SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a)
fn SymSequence sym a -> m (f a)
loop SymSequence sym a
s

-- | Generate an empty sequence value
nilSymSequence :: sym -> IO (SymSequence sym a)
nilSymSequence :: forall sym a. sym -> IO (SymSequence sym a)
nilSymSequence sym
_sym = SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym a
forall sym a. SymSequence sym a
SymSequenceNil

-- | Cons a new value onto the front of a sequence
consSymSequence ::
  sym ->
  a ->
  SymSequence sym a ->
  IO (SymSequence sym a)
consSymSequence :: forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
consSymSequence sym
_sym a
x SymSequence sym a
xs =
  do Nonce GlobalNonceGenerator a
n <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator a)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
     SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Nonce GlobalNonceGenerator a
-> a -> SymSequence sym a -> SymSequence sym a
forall a sym.
Nonce GlobalNonceGenerator a
-> a -> SymSequence sym a -> SymSequence sym a
SymSequenceCons Nonce GlobalNonceGenerator a
n a
x SymSequence sym a
xs)

fromListSymSequence :: sym -> [a] -> IO (SymSequence sym a)
fromListSymSequence :: forall sym a. sym -> [a] -> IO (SymSequence sym a)
fromListSymSequence sym
sym =
  \case
    [] -> sym -> IO (SymSequence sym a)
forall sym a. sym -> IO (SymSequence sym a)
nilSymSequence sym
sym
    (a
x:[a]
xs) -> sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
consSymSequence sym
sym a
x (SymSequence sym a -> IO (SymSequence sym a))
-> IO (SymSequence sym a) -> IO (SymSequence sym a)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> [a] -> IO (SymSequence sym a)
forall sym a. sym -> [a] -> IO (SymSequence sym a)
fromListSymSequence sym
sym [a]
xs

-- | Append two sequences
appendSymSequence ::
  sym ->
  SymSequence sym a {- ^ front sequence -} ->
  SymSequence sym a {- ^ back sequence -} ->
  IO (SymSequence sym a)

-- special cases, nil is the unit for append
appendSymSequence :: forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
_ SymSequence sym a
xs SymSequence sym a
SymSequenceNil = SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym a
xs
appendSymSequence sym
_ SymSequence sym a
SymSequenceNil SymSequence sym a
ys = SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SymSequence sym a
ys
-- special case, append of a singleton is cons
appendSymSequence sym
sym (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
SymSequenceNil) SymSequence sym a
xs =
  sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
consSymSequence sym
sym a
v SymSequence sym a
xs
appendSymSequence sym
_sym SymSequence sym a
xs SymSequence sym a
ys =
  do Nonce GlobalNonceGenerator a
n <- NonceGenerator IO GlobalNonceGenerator
-> IO (Nonce GlobalNonceGenerator a)
forall (m :: Type -> Type) s k (tp :: k).
NonceGenerator m s -> m (Nonce s tp)
freshNonce NonceGenerator IO GlobalNonceGenerator
globalNonceGenerator
     SymSequence sym a -> IO (SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Nonce GlobalNonceGenerator a
-> SymSequence sym a -> SymSequence sym a -> SymSequence sym a
forall a sym.
Nonce GlobalNonceGenerator a
-> SymSequence sym a -> SymSequence sym a -> SymSequence sym a
SymSequenceAppend Nonce GlobalNonceGenerator a
n SymSequence sym a
xs SymSequence sym a
ys)


-- | Test if a sequence is nil (is empty)
isNilSymSequence :: forall sym a.
  IsExprBuilder sym =>
  sym ->
  SymSequence sym a ->
  IO (Pred sym)
isNilSymSequence :: forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (Pred sym)
isNilSymSequence sym
sym = \SymSequence sym a
s -> Const (Pred sym) a -> Pred sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (Pred sym) a -> Pred sym)
-> IO (Const (Pred sym) a) -> IO (Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> IO (Const (Pred sym) a))
 -> SymSequence sym a -> IO (Const (Pred sym) a))
-> SymSequence sym a -> IO (Const (Pred sym) a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> IO (Const (Pred sym) a))
-> SymSequence sym a -> IO (Const (Pred sym) a)
forall tp.
(SymSequence sym tp -> IO (Const (Pred sym) tp))
-> SymSequence sym tp -> IO (Const (Pred sym) tp)
f SymSequence sym a
s
  where
   f :: (SymSequence sym tp -> IO (Const (Pred sym) tp)) -> (SymSequence sym tp -> IO (Const (Pred sym) tp))
   f :: forall tp.
(SymSequence sym tp -> IO (Const (Pred sym) tp))
-> SymSequence sym tp -> IO (Const (Pred sym) tp)
f SymSequence sym tp -> IO (Const (Pred sym) tp)
_loop SymSequenceNil{}  = Const (Pred sym) tp -> IO (Const (Pred sym) tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Const (Pred sym) tp
forall {k} a (b :: k). a -> Const a b
Const (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym))
   f SymSequence sym tp -> IO (Const (Pred sym) tp)
_loop SymSequenceCons{} = Const (Pred sym) tp -> IO (Const (Pred sym) tp)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Pred sym -> Const (Pred sym) tp
forall {k} a (b :: k). a -> Const a b
Const (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym))
   f SymSequence sym tp -> IO (Const (Pred sym) tp)
loop (SymSequenceAppend Nonce GlobalNonceGenerator tp
_ SymSequence sym tp
xs SymSequence sym tp
ys) =
     do Pred sym
px <- Const (Pred sym) tp -> Pred sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (Pred sym) tp -> Pred sym)
-> IO (Const (Pred sym) tp) -> IO (Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym tp -> IO (Const (Pred sym) tp)
loop SymSequence sym tp
xs
        Pred sym -> Const (Pred sym) tp
forall {k} a (b :: k). a -> Const a b
Const (Pred sym -> Const (Pred sym) tp)
-> IO (Pred sym) -> IO (Const (Pred sym) tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> IO (Pred sym) -> IO (Pred sym) -> IO (Pred sym)
forall sym (m :: Type -> Type).
(IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) =>
sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
itePredM sym
sym Pred sym
px (Const (Pred sym) tp -> Pred sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (Pred sym) tp -> Pred sym)
-> IO (Const (Pred sym) tp) -> IO (Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym tp -> IO (Const (Pred sym) tp)
loop SymSequence sym tp
ys) (Pred sym -> IO (Pred sym)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
falsePred sym
sym))
   f SymSequence sym tp -> IO (Const (Pred sym) tp)
loop (SymSequenceMerge Nonce GlobalNonceGenerator tp
_ Pred sym
p SymSequence sym tp
xs SymSequence sym tp
ys) =
     Pred sym -> Const (Pred sym) tp
forall {k} a (b :: k). a -> Const a b
Const (Pred sym -> Const (Pred sym) tp)
-> IO (Pred sym) -> IO (Const (Pred sym) tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> IO (Pred sym) -> IO (Pred sym) -> IO (Pred sym)
forall sym (m :: Type -> Type).
(IsExpr (SymExpr sym), IsExprBuilder sym, MonadIO m) =>
sym -> Pred sym -> m (Pred sym) -> m (Pred sym) -> m (Pred sym)
itePredM sym
sym Pred sym
p (Const (Pred sym) tp -> Pred sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (Pred sym) tp -> Pred sym)
-> IO (Const (Pred sym) tp) -> IO (Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym tp -> IO (Const (Pred sym) tp)
loop SymSequence sym tp
xs) (Const (Pred sym) tp -> Pred sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (Pred sym) tp -> Pred sym)
-> IO (Const (Pred sym) tp) -> IO (Pred sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym tp -> IO (Const (Pred sym) tp)
loop SymSequence sym tp
ys)


-- | Compute the length of a sequence
lengthSymSequence :: forall sym a.
  IsExprBuilder sym =>
  sym ->
  SymSequence sym a ->
  IO (SymNat sym)
lengthSymSequence :: forall sym a.
IsExprBuilder sym =>
sym -> SymSequence sym a -> IO (SymNat sym)
lengthSymSequence sym
sym = \SymSequence sym a
s -> Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> IO (Const (SymNat sym) a))
 -> SymSequence sym a -> IO (Const (SymNat sym) a))
-> SymSequence sym a -> IO (Const (SymNat sym) a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> IO (Const (SymNat sym) a))
-> SymSequence sym a -> IO (Const (SymNat sym) a)
f SymSequence sym a
s
  where
   f :: (SymSequence sym a -> IO (Const (SymNat sym) a)) -> (SymSequence sym a -> IO (Const (SymNat sym) a))
   f :: (SymSequence sym a -> IO (Const (SymNat sym) a))
-> SymSequence sym a -> IO (Const (SymNat sym) a)
f SymSequence sym a -> IO (Const (SymNat sym) a)
_loop SymSequence sym a
SymSequenceNil = SymNat sym -> Const (SymNat sym) a
forall {k} a (b :: k). a -> Const a b
Const (SymNat sym -> Const (SymNat sym) a)
-> IO (SymNat sym) -> IO (Const (SymNat sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
0
   f SymSequence sym a -> IO (Const (SymNat sym) a)
loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
_ SymSequence sym a
tl) =
     do SymNat sym
x <- Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Const (SymNat sym) a)
loop SymSequence sym a
tl
        SymNat sym
one <- sym -> Natural -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Natural -> IO (SymNat sym)
natLit sym
sym Natural
1
        SymNat sym -> Const (SymNat sym) a
forall {k} a (b :: k). a -> Const a b
Const (SymNat sym -> Const (SymNat sym) a)
-> IO (SymNat sym) -> IO (Const (SymNat sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym SymNat sym
one SymNat sym
x
   f SymSequence sym a -> IO (Const (SymNat sym) a)
loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
     do SymNat sym
x <- Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Const (SymNat sym) a)
loop SymSequence sym a
xs
        SymNat sym
y <- Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Const (SymNat sym) a)
loop SymSequence sym a
ys
        SymNat sym -> Const (SymNat sym) a
forall {k} a (b :: k). a -> Const a b
Const (SymNat sym -> Const (SymNat sym) a)
-> IO (SymNat sym) -> IO (Const (SymNat sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym Pred sym
p SymNat sym
x SymNat sym
y
   f SymSequence sym a -> IO (Const (SymNat sym) a)
loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) =
     do SymNat sym
x <- Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Const (SymNat sym) a)
loop SymSequence sym a
xs
        SymNat sym
y <- Const (SymNat sym) a -> SymNat sym
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymNat sym) a -> SymNat sym)
-> IO (Const (SymNat sym) a) -> IO (SymNat sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Const (SymNat sym) a)
loop SymSequence sym a
ys
        SymNat sym -> Const (SymNat sym) a
forall {k} a (b :: k). a -> Const a b
Const (SymNat sym -> Const (SymNat sym) a)
-> IO (SymNat sym) -> IO (Const (SymNat sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natAdd sym
sym SymNat sym
x SymNat sym
y


newtype SeqHead sym a = SeqHead { forall sym a. SeqHead sym a -> PartExpr (Pred sym) a
getSeqHead :: PartExpr (Pred sym) a }

-- | Compute the head of a sequence, if it has one
headSymSequence :: forall sym a.
  IsExprBuilder sym =>
  sym ->
  (Pred sym -> a -> a -> IO a) {- ^ mux function on values -} ->
  SymSequence sym a ->
  IO (PartExpr (Pred sym) a)
headSymSequence :: forall sym a.
IsExprBuilder sym =>
sym
-> (Pred sym -> a -> a -> IO a)
-> SymSequence sym a
-> IO (PartExpr (Pred sym) a)
headSymSequence sym
sym Pred sym -> a -> a -> IO a
mux = \SymSequence sym a
s -> SeqHead sym a -> PartExpr (Pred sym) a
forall sym a. SeqHead sym a -> PartExpr (Pred sym) a
getSeqHead (SeqHead sym a -> PartExpr (Pred sym) a)
-> IO (SeqHead sym a) -> IO (PartExpr (Pred sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> IO (SeqHead sym a))
 -> SymSequence sym a -> IO (SeqHead sym a))
-> SymSequence sym a -> IO (SeqHead sym a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> IO (SeqHead sym a))
-> SymSequence sym a -> IO (SeqHead sym a)
f SymSequence sym a
s
  where
   f' :: Pred sym -> a -> a -> PartialT sym IO a
   f' :: Pred sym -> a -> a -> PartialT sym IO a
f' Pred sym
c a
x a
y = (sym -> Pred sym -> IO (PartExpr (Pred sym) a))
-> PartialT sym IO a
forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT (\sym
_ Pred sym
p -> Pred sym -> a -> PartExpr (Pred sym) a
forall p v. p -> v -> PartExpr p v
PE Pred sym
p (a -> PartExpr (Pred sym) a) -> IO a -> IO (PartExpr (Pred sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Pred sym -> a -> a -> IO a
mux Pred sym
c a
x a
y)

   f :: (SymSequence sym a -> IO (SeqHead sym a)) -> (SymSequence sym a -> IO (SeqHead sym a))
   f :: (SymSequence sym a -> IO (SeqHead sym a))
-> SymSequence sym a -> IO (SeqHead sym a)
f SymSequence sym a -> IO (SeqHead sym a)
_loop SymSequence sym a
SymSequenceNil = SeqHead sym a -> IO (SeqHead sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead PartExpr (Pred sym) a
forall p v. PartExpr p v
Unassigned)
   f SymSequence sym a -> IO (SeqHead sym a)
_loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
_) = SeqHead sym a -> IO (SeqHead sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead (sym -> a -> PartExpr (Pred sym) a
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym a
v))
   f SymSequence sym a -> IO (SeqHead sym a)
loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
     do PartExpr (Pred sym) a
mhx <- SeqHead sym a -> PartExpr (Pred sym) a
forall sym a. SeqHead sym a -> PartExpr (Pred sym) a
getSeqHead (SeqHead sym a -> PartExpr (Pred sym) a)
-> IO (SeqHead sym a) -> IO (PartExpr (Pred sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqHead sym a)
loop SymSequence sym a
xs
        PartExpr (Pred sym) a
mhy <- SeqHead sym a -> PartExpr (Pred sym) a
forall sym a. SeqHead sym a -> PartExpr (Pred sym) a
getSeqHead (SeqHead sym a -> PartExpr (Pred sym) a)
-> IO (SeqHead sym a) -> IO (PartExpr (Pred sym) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqHead sym a)
loop SymSequence sym a
ys
        PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead (PartExpr (Pred sym) a -> SeqHead sym a)
-> IO (PartExpr (Pred sym) a) -> IO (SeqHead sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (Pred sym -> a -> a -> PartialT sym IO a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> IO (PartExpr (Pred sym) a)
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
mergePartial sym
sym Pred sym -> a -> a -> PartialT sym IO a
f' Pred sym
p PartExpr (Pred sym) a
mhx PartExpr (Pred sym) a
mhy

   f SymSequence sym a -> IO (SeqHead sym a)
loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) =
     SymSequence sym a -> IO (SeqHead sym a)
loop SymSequence sym a
xs IO (SeqHead sym a)
-> (SeqHead sym a -> IO (SeqHead sym a)) -> IO (SeqHead sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       SeqHead PartExpr (Pred sym) a
Unassigned -> SymSequence sym a -> IO (SeqHead sym a)
loop SymSequence sym a
ys
       SeqHead (PE Pred sym
px a
hx)
         | Just Bool
True <- Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
px -> SeqHead sym a -> IO (SeqHead sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead (Pred sym -> a -> PartExpr (Pred sym) a
forall p v. p -> v -> PartExpr p v
PE Pred sym
px a
hx))
         | Bool
otherwise ->
             SymSequence sym a -> IO (SeqHead sym a)
loop SymSequence sym a
ys IO (SeqHead sym a)
-> (SeqHead sym a -> IO (SeqHead sym a)) -> IO (SeqHead sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               SeqHead PartExpr (Pred sym) a
Unassigned -> SeqHead sym a -> IO (SeqHead sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead (Pred sym -> a -> PartExpr (Pred sym) a
forall p v. p -> v -> PartExpr p v
PE Pred sym
px a
hx))
               SeqHead (PE Pred sym
py a
hy) ->
                 do Pred sym
p <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
px Pred sym
py
                    PartExpr (Pred sym) a -> SeqHead sym a
forall sym a. PartExpr (Pred sym) a -> SeqHead sym a
SeqHead (PartExpr (Pred sym) a -> SeqHead sym a)
-> IO (PartExpr (Pred sym) a) -> IO (SeqHead sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> PartialT sym IO a -> IO (PartExpr (Pred sym) a)
forall sym (m :: Type -> Type) a.
sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
runPartialT sym
sym Pred sym
p (Pred sym -> a -> a -> PartialT sym IO a
f' Pred sym
px a
hx a
hy)

newtype SeqUncons sym a =
  SeqUncons
  { forall sym a.
SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
getSeqUncons :: PartExpr (Pred sym) (a, SymSequence sym a)
  }

-- | Compute both the head and the tail of a sequence, if it is nonempty
unconsSymSequence :: forall sym a.
  IsExprBuilder sym =>
  sym ->
  (Pred sym -> a -> a -> IO a) {- ^ mux function on values -} ->
  SymSequence sym a ->
  IO (PartExpr (Pred sym) (a, SymSequence sym a))
unconsSymSequence :: forall sym a.
IsExprBuilder sym =>
sym
-> (Pred sym -> a -> a -> IO a)
-> SymSequence sym a
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
unconsSymSequence sym
sym Pred sym -> a -> a -> IO a
mux = \SymSequence sym a
s -> SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
forall sym a.
SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
getSeqUncons (SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (SeqUncons sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> IO (SeqUncons sym a))
 -> SymSequence sym a -> IO (SeqUncons sym a))
-> SymSequence sym a -> IO (SeqUncons sym a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> IO (SeqUncons sym a))
-> SymSequence sym a -> IO (SeqUncons sym a)
f SymSequence sym a
s
  where
   f' :: Pred sym ->
         (a, SymSequence sym a) ->
         (a, SymSequence sym a) ->
         PartialT sym IO (a, SymSequence sym a)
   f' :: Pred sym
-> (a, SymSequence sym a)
-> (a, SymSequence sym a)
-> PartialT sym IO (a, SymSequence sym a)
f' Pred sym
c (a, SymSequence sym a)
x (a, SymSequence sym a)
y = (sym
 -> Pred sym -> IO (PartExpr (Pred sym) (a, SymSequence sym a)))
-> PartialT sym IO (a, SymSequence sym a)
forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT ((sym
  -> Pred sym -> IO (PartExpr (Pred sym) (a, SymSequence sym a)))
 -> PartialT sym IO (a, SymSequence sym a))
-> (sym
    -> Pred sym -> IO (PartExpr (Pred sym) (a, SymSequence sym a)))
-> PartialT sym IO (a, SymSequence sym a)
forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
p -> Pred sym
-> (a, SymSequence sym a)
-> PartExpr (Pred sym) (a, SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
p ((a, SymSequence sym a)
 -> PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (a, SymSequence sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
                    do a
h  <- Pred sym -> a -> a -> IO a
mux Pred sym
c ((a, SymSequence sym a) -> a
forall a b. (a, b) -> a
fst (a, SymSequence sym a)
x) ((a, SymSequence sym a) -> a
forall a b. (a, b) -> a
fst (a, SymSequence sym a)
y)
                       SymSequence sym a
tl <- sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
forall sym a.
sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
muxSymSequence sym
sym Pred sym
c ((a, SymSequence sym a) -> SymSequence sym a
forall a b. (a, b) -> b
snd (a, SymSequence sym a)
x) ((a, SymSequence sym a) -> SymSequence sym a
forall a b. (a, b) -> b
snd (a, SymSequence sym a)
y)
                       (a, SymSequence sym a) -> IO (a, SymSequence sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (a
h, SymSequence sym a
tl)

   f :: (SymSequence sym a -> IO (SeqUncons sym a)) -> (SymSequence sym a -> IO (SeqUncons sym a))
   f :: (SymSequence sym a -> IO (SeqUncons sym a))
-> SymSequence sym a -> IO (SeqUncons sym a)
f SymSequence sym a -> IO (SeqUncons sym a)
_loop SymSequence sym a
SymSequenceNil = SeqUncons sym a -> IO (SeqUncons sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons PartExpr (Pred sym) (a, SymSequence sym a)
forall p v. PartExpr p v
Unassigned)
   f SymSequence sym a -> IO (SeqUncons sym a)
_loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
tl) = SeqUncons sym a -> IO (SeqUncons sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons (sym
-> (a, SymSequence sym a)
-> PartExpr (Pred sym) (a, SymSequence sym a)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym (a
v, SymSequence sym a
tl)))
   f SymSequence sym a -> IO (SeqUncons sym a)
loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
     do PartExpr (Pred sym) (a, SymSequence sym a)
ux <- SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
forall sym a.
SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
getSeqUncons (SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (SeqUncons sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqUncons sym a)
loop SymSequence sym a
xs
        PartExpr (Pred sym) (a, SymSequence sym a)
uy <- SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
forall sym a.
SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a)
getSeqUncons (SeqUncons sym a -> PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (SeqUncons sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqUncons sym a)
loop SymSequence sym a
ys
        PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (SeqUncons sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (Pred sym
    -> (a, SymSequence sym a)
    -> (a, SymSequence sym a)
    -> PartialT sym IO (a, SymSequence sym a))
-> Pred sym
-> PartExpr (Pred sym) (a, SymSequence sym a)
-> PartExpr (Pred sym) (a, SymSequence sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
mergePartial sym
sym Pred sym
-> (a, SymSequence sym a)
-> (a, SymSequence sym a)
-> PartialT sym IO (a, SymSequence sym a)
f' Pred sym
p PartExpr (Pred sym) (a, SymSequence sym a)
ux PartExpr (Pred sym) (a, SymSequence sym a)
uy

   f SymSequence sym a -> IO (SeqUncons sym a)
loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) =
     SymSequence sym a -> IO (SeqUncons sym a)
loop SymSequence sym a
xs IO (SeqUncons sym a)
-> (SeqUncons sym a -> IO (SeqUncons sym a))
-> IO (SeqUncons sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       SeqUncons PartExpr (Pred sym) (a, SymSequence sym a)
Unassigned -> SymSequence sym a -> IO (SeqUncons sym a)
loop SymSequence sym a
ys
       SeqUncons (PE Pred sym
px (a, SymSequence sym a)
ux)
         | Just Bool
True <- Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
px ->
             do SymSequence sym a
t <- sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym ((a, SymSequence sym a) -> SymSequence sym a
forall a b. (a, b) -> b
snd (a, SymSequence sym a)
ux) SymSequence sym a
ys
                SeqUncons sym a -> IO (SeqUncons sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons (Pred sym
-> (a, SymSequence sym a)
-> PartExpr (Pred sym) (a, SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
px ((a, SymSequence sym a) -> a
forall a b. (a, b) -> a
fst (a, SymSequence sym a)
ux, SymSequence sym a
t)))

         | Bool
otherwise ->
             SymSequence sym a -> IO (SeqUncons sym a)
loop SymSequence sym a
ys IO (SeqUncons sym a)
-> (SeqUncons sym a -> IO (SeqUncons sym a))
-> IO (SeqUncons sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               SeqUncons PartExpr (Pred sym) (a, SymSequence sym a)
Unassigned -> SeqUncons sym a -> IO (SeqUncons sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons (Pred sym
-> (a, SymSequence sym a)
-> PartExpr (Pred sym) (a, SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
px (a, SymSequence sym a)
ux))
               SeqUncons (PE Pred sym
py (a, SymSequence sym a)
uy) ->
                 do Pred sym
p <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
px Pred sym
py
                    SymSequence sym a
t <- sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym ((a, SymSequence sym a) -> SymSequence sym a
forall a b. (a, b) -> b
snd (a, SymSequence sym a)
ux) SymSequence sym a
ys
                    let ux' :: (a, SymSequence sym a)
ux' = ((a, SymSequence sym a) -> a
forall a b. (a, b) -> a
fst (a, SymSequence sym a)
ux, SymSequence sym a
t)
                    PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
forall sym a.
PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a
SeqUncons (PartExpr (Pred sym) (a, SymSequence sym a) -> SeqUncons sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
-> IO (SeqUncons sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> PartialT sym IO (a, SymSequence sym a)
-> IO (PartExpr (Pred sym) (a, SymSequence sym a))
forall sym (m :: Type -> Type) a.
sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
runPartialT sym
sym Pred sym
p (Pred sym
-> (a, SymSequence sym a)
-> (a, SymSequence sym a)
-> PartialT sym IO (a, SymSequence sym a)
f' Pred sym
px (a, SymSequence sym a)
ux' (a, SymSequence sym a)
uy)

newtype SeqTail sym tp =
  SeqTail
  { forall sym tp.
SeqTail sym tp -> PartExpr (Pred sym) (SymSequence sym tp)
getSeqTail :: PartExpr (Pred sym) (SymSequence sym tp) }

-- | Compute the tail of a sequence, if it has one
tailSymSequence :: forall sym a.
  IsExprBuilder sym =>
  sym ->
  SymSequence sym a ->
  IO (PartExpr (Pred sym) (SymSequence sym a))
tailSymSequence :: forall sym a.
IsExprBuilder sym =>
sym
-> SymSequence sym a
-> IO (PartExpr (Pred sym) (SymSequence sym a))
tailSymSequence sym
sym = \SymSequence sym a
s -> SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall sym tp.
SeqTail sym tp -> PartExpr (Pred sym) (SymSequence sym tp)
getSeqTail (SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a))
-> IO (SeqTail sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> IO (SeqTail sym a))
 -> SymSequence sym a -> IO (SeqTail sym a))
-> SymSequence sym a -> IO (SeqTail sym a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> IO (SeqTail sym a))
-> SymSequence sym a -> IO (SeqTail sym a)
f SymSequence sym a
s
  where
   f' :: Pred sym ->
         SymSequence sym a ->
         SymSequence sym a ->
         PartialT sym IO (SymSequence sym a)
   f' :: Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> PartialT sym IO (SymSequence sym a)
f' Pred sym
c SymSequence sym a
x SymSequence sym a
y = (sym -> Pred sym -> IO (PartExpr (Pred sym) (SymSequence sym a)))
-> PartialT sym IO (SymSequence sym a)
forall sym (m :: Type -> Type) a.
(sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym m a
PartialT ((sym -> Pred sym -> IO (PartExpr (Pred sym) (SymSequence sym a)))
 -> PartialT sym IO (SymSequence sym a))
-> (sym
    -> Pred sym -> IO (PartExpr (Pred sym) (SymSequence sym a)))
-> PartialT sym IO (SymSequence sym a)
forall a b. (a -> b) -> a -> b
$ \sym
_ Pred sym
p -> Pred sym
-> SymSequence sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
p (SymSequence sym a -> PartExpr (Pred sym) (SymSequence sym a))
-> IO (SymSequence sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
forall sym a.
sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
muxSymSequence sym
sym Pred sym
c SymSequence sym a
x SymSequence sym a
y

   f :: (SymSequence sym a -> IO (SeqTail sym a)) -> (SymSequence sym a -> IO (SeqTail sym a))
   f :: (SymSequence sym a -> IO (SeqTail sym a))
-> SymSequence sym a -> IO (SeqTail sym a)
f SymSequence sym a -> IO (SeqTail sym a)
_loop SymSequence sym a
SymSequenceNil = SeqTail sym a -> IO (SeqTail sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail PartExpr (Pred sym) (SymSequence sym a)
forall p v. PartExpr p v
Unassigned)
   f SymSequence sym a -> IO (SeqTail sym a)
_loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
_v SymSequence sym a
tl) = SeqTail sym a -> IO (SeqTail sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail (sym -> SymSequence sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall sym v.
IsExprBuilder sym =>
sym -> v -> PartExpr (Pred sym) v
justPartExpr sym
sym SymSequence sym a
tl))
   f SymSequence sym a -> IO (SeqTail sym a)
loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
     do PartExpr (Pred sym) (SymSequence sym a)
tx <- SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall sym tp.
SeqTail sym tp -> PartExpr (Pred sym) (SymSequence sym tp)
getSeqTail (SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a))
-> IO (SeqTail sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqTail sym a)
loop SymSequence sym a
xs
        PartExpr (Pred sym) (SymSequence sym a)
ty <- SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall sym tp.
SeqTail sym tp -> PartExpr (Pred sym) (SymSequence sym tp)
getSeqTail (SeqTail sym a -> PartExpr (Pred sym) (SymSequence sym a))
-> IO (SeqTail sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (SeqTail sym a)
loop SymSequence sym a
ys
        PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
-> IO (SeqTail sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (Pred sym
    -> SymSequence sym a
    -> SymSequence sym a
    -> PartialT sym IO (SymSequence sym a))
-> Pred sym
-> PartExpr (Pred sym) (SymSequence sym a)
-> PartExpr (Pred sym) (SymSequence sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
mergePartial sym
sym Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> PartialT sym IO (SymSequence sym a)
f' Pred sym
p PartExpr (Pred sym) (SymSequence sym a)
tx PartExpr (Pred sym) (SymSequence sym a)
ty
   f SymSequence sym a -> IO (SeqTail sym a)
loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) =
     SymSequence sym a -> IO (SeqTail sym a)
loop SymSequence sym a
xs IO (SeqTail sym a)
-> (SeqTail sym a -> IO (SeqTail sym a)) -> IO (SeqTail sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
       SeqTail PartExpr (Pred sym) (SymSequence sym a)
Unassigned -> SymSequence sym a -> IO (SeqTail sym a)
loop SymSequence sym a
ys
       SeqTail (PE Pred sym
px SymSequence sym a
tx)
         | Just Bool
True <- Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
px ->
             do SymSequence sym a
t <- sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym SymSequence sym a
tx SymSequence sym a
ys
                SeqTail sym a -> IO (SeqTail sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail (Pred sym
-> SymSequence sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
px SymSequence sym a
t))

         | Bool
otherwise ->
             SymSequence sym a -> IO (SeqTail sym a)
loop SymSequence sym a
ys IO (SeqTail sym a)
-> (SeqTail sym a -> IO (SeqTail sym a)) -> IO (SeqTail sym a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
               SeqTail PartExpr (Pred sym) (SymSequence sym a)
Unassigned -> SeqTail sym a -> IO (SeqTail sym a)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail (Pred sym
-> SymSequence sym a -> PartExpr (Pred sym) (SymSequence sym a)
forall p v. p -> v -> PartExpr p v
PE Pred sym
px SymSequence sym a
tx))
               SeqTail (PE Pred sym
py SymSequence sym a
ty) ->
                 do Pred sym
p <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
px Pred sym
py
                    SymSequence sym a
t <- sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym SymSequence sym a
tx SymSequence sym a
ys
                    PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a
forall sym tp.
PartExpr (Pred sym) (SymSequence sym tp) -> SeqTail sym tp
SeqTail (PartExpr (Pred sym) (SymSequence sym a) -> SeqTail sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
-> IO (SeqTail sym a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> PartialT sym IO (SymSequence sym a)
-> IO (PartExpr (Pred sym) (SymSequence sym a))
forall sym (m :: Type -> Type) a.
sym -> Pred sym -> PartialT sym m a -> m (PartExpr (Pred sym) a)
runPartialT sym
sym Pred sym
p (Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> PartialT sym IO (SymSequence sym a)
f' Pred sym
px SymSequence sym a
t SymSequence sym a
ty)


{-# SPECIALIZE
  traverseSymSequence ::
  sym ->
  (a -> IO b) ->
  SymSequence sym a ->
  IO (SymSequence sym b)
 #-}

-- | Visit every element in the given symbolic sequence,
--   applying the given action, and constructing a new
--   sequence. The traversal is memoized, so any given
--   subsequence will be visited at most once.
traverseSymSequence :: forall m sym a b.
  MonadIO m =>
  sym ->
  (a -> m b) ->
  SymSequence sym a ->
  m (SymSequence sym b)
traverseSymSequence :: forall (m :: Type -> Type) sym a b.
MonadIO m =>
sym -> (a -> m b) -> SymSequence sym a -> m (SymSequence sym b)
traverseSymSequence sym
sym a -> m b
f = \SymSequence sym a
s -> Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SymSequence sym a -> m (Const (SymSequence sym b) a))
 -> SymSequence sym a -> m (Const (SymSequence sym b) a))
-> SymSequence sym a -> m (Const (SymSequence sym b) a)
forall (m :: Type -> Type) sym a (f :: Type -> Type).
MonadIO m =>
((SymSequence sym a -> m (f a)) -> SymSequence sym a -> m (f a))
-> SymSequence sym a -> m (f a)
evalWithFreshCache (SymSequence sym a -> m (Const (SymSequence sym b) a))
-> SymSequence sym a -> m (Const (SymSequence sym b) a)
fn SymSequence sym a
s
  where
   fn :: (SymSequence sym a -> m (Const (SymSequence sym b) a)) ->
         (SymSequence sym a -> m (Const (SymSequence sym b) a))
   fn :: (SymSequence sym a -> m (Const (SymSequence sym b) a))
-> SymSequence sym a -> m (Const (SymSequence sym b) a)
fn SymSequence sym a -> m (Const (SymSequence sym b) a)
_loop SymSequence sym a
SymSequenceNil = Const (SymSequence sym b) a -> m (Const (SymSequence sym b) a)
forall a. a -> m a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymSequence sym b -> Const (SymSequence sym b) a
forall {k} a (b :: k). a -> Const a b
Const SymSequence sym b
forall sym a. SymSequence sym a
SymSequenceNil)
   fn SymSequence sym a -> m (Const (SymSequence sym b) a)
loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
tl) =
     do b
v'  <- a -> m b
f a
v
        SymSequence sym b
tl' <- Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> m (Const (SymSequence sym b) a)
loop SymSequence sym a
tl
        IO (Const (SymSequence sym b) a) -> m (Const (SymSequence sym b) a)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (SymSequence sym b -> Const (SymSequence sym b) a
forall {k} a (b :: k). a -> Const a b
Const (SymSequence sym b -> Const (SymSequence sym b) a)
-> IO (SymSequence sym b) -> IO (Const (SymSequence sym b) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> b -> SymSequence sym b -> IO (SymSequence sym b)
forall sym a.
sym -> a -> SymSequence sym a -> IO (SymSequence sym a)
consSymSequence sym
sym b
v' SymSequence sym b
tl')
   fn SymSequence sym a -> m (Const (SymSequence sym b) a)
loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) =
     do SymSequence sym b
xs' <- Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> m (Const (SymSequence sym b) a)
loop SymSequence sym a
xs
        SymSequence sym b
ys' <- Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> m (Const (SymSequence sym b) a)
loop SymSequence sym a
ys
        IO (Const (SymSequence sym b) a) -> m (Const (SymSequence sym b) a)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (SymSequence sym b -> Const (SymSequence sym b) a
forall {k} a (b :: k). a -> Const a b
Const (SymSequence sym b -> Const (SymSequence sym b) a)
-> IO (SymSequence sym b) -> IO (Const (SymSequence sym b) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymSequence sym b -> SymSequence sym b -> IO (SymSequence sym b)
forall sym a.
sym
-> SymSequence sym a -> SymSequence sym a -> IO (SymSequence sym a)
appendSymSequence sym
sym SymSequence sym b
xs' SymSequence sym b
ys')
   fn SymSequence sym a -> m (Const (SymSequence sym b) a)
loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
     do SymSequence sym b
xs' <- Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> m (Const (SymSequence sym b) a)
loop SymSequence sym a
xs
        SymSequence sym b
ys' <- Const (SymSequence sym b) a -> SymSequence sym b
forall {k} a (b :: k). Const a b -> a
getConst (Const (SymSequence sym b) a -> SymSequence sym b)
-> m (Const (SymSequence sym b) a) -> m (SymSequence sym b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> m (Const (SymSequence sym b) a)
loop SymSequence sym a
ys
        IO (Const (SymSequence sym b) a) -> m (Const (SymSequence sym b) a)
forall a. IO a -> m a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (SymSequence sym b -> Const (SymSequence sym b) a
forall {k} a (b :: k). a -> Const a b
Const (SymSequence sym b -> Const (SymSequence sym b) a)
-> IO (SymSequence sym b) -> IO (Const (SymSequence sym b) a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> Pred sym
-> SymSequence sym b
-> SymSequence sym b
-> IO (SymSequence sym b)
forall sym a.
sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
muxSymSequence sym
sym Pred sym
p SymSequence sym b
xs' SymSequence sym b
ys')


-- | Using the given evaluation function for booleans, and an evaluation
--   function for values, compute a concrete sequence corresponding
--   to the given symbolic sequence.
concreteizeSymSequence ::
  (Pred sym -> IO Bool) {- ^ evaluation for booleans -} ->
  (a -> IO b) {- ^ evaluation for values -} ->
  SymSequence sym a -> IO [b]
concreteizeSymSequence :: forall sym a b.
(Pred sym -> IO Bool) -> (a -> IO b) -> SymSequence sym a -> IO [b]
concreteizeSymSequence Pred sym -> IO Bool
conc a -> IO b
eval = SymSequence sym a -> IO [b]
loop
  where
    loop :: SymSequence sym a -> IO [b]
loop SymSequence sym a
SymSequenceNil = [b] -> IO [b]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
    loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
tl) = (:) (b -> [b] -> [b]) -> IO b -> IO ([b] -> [b])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO b
eval a
v IO ([b] -> [b]) -> IO [b] -> IO [b]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> SymSequence sym a -> IO [b]
loop SymSequence sym a
tl
    loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) = [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
(++) ([b] -> [b] -> [b]) -> IO [b] -> IO ([b] -> [b])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO [b]
loop SymSequence sym a
xs IO ([b] -> [b]) -> IO [b] -> IO [b]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> SymSequence sym a -> IO [b]
loop SymSequence sym a
ys
    loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
      do Bool
b <- Pred sym -> IO Bool
conc Pred sym
p
         if Bool
b then SymSequence sym a -> IO [b]
loop SymSequence sym a
xs else SymSequence sym a -> IO [b]
loop SymSequence sym a
ys
{-# DEPRECATED concreteizeSymSequence "Use concretizeSymSequence instead" #-} 

-- | Using the given evaluation function for booleans, and an evaluation
--   function for values, compute a concrete sequence corresponding
--   to the given symbolic sequence.
concretizeSymSequence ::
  (Pred sym -> IO Bool) {- ^ evaluation for booleans -} ->
  (a -> IO b) {- ^ evaluation for values -} ->
  SymSequence sym a ->
  IO (Seq b)
concretizeSymSequence :: forall sym a b.
(Pred sym -> IO Bool)
-> (a -> IO b) -> SymSequence sym a -> IO (Seq b)
concretizeSymSequence Pred sym -> IO Bool
conc a -> IO b
eval = SymSequence sym a -> IO (Seq b)
loop
  where
    loop :: SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
SymSequenceNil = Seq b -> IO (Seq b)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Seq b
forall a. Seq a
Seq.empty
    loop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
tl) = b -> Seq b -> Seq b
forall a. a -> Seq a -> Seq a
(Seq.<|) (b -> Seq b -> Seq b) -> IO b -> IO (Seq b -> Seq b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO b
eval a
v IO (Seq b -> Seq b) -> IO (Seq b) -> IO (Seq b)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
tl
    loop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) = Seq b -> Seq b -> Seq b
forall a. Seq a -> Seq a -> Seq a
(Seq.><) (Seq b -> Seq b -> Seq b) -> IO (Seq b) -> IO (Seq b -> Seq b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
xs IO (Seq b -> Seq b) -> IO (Seq b) -> IO (Seq b)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
ys
    loop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
      do Bool
b <- Pred sym -> IO Bool
conc Pred sym
p
         if Bool
b then SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
xs else SymSequence sym a -> IO (Seq b)
loop SymSequence sym a
ys

instance (IsExpr (SymExpr sym), PP.Pretty a) => PP.Pretty (SymSequence sym a) where
  pretty :: forall ann. SymSequence sym a -> Doc ann
pretty = (a -> Doc ann) -> SymSequence sym a -> Doc ann
forall sym a ann.
IsExpr (SymExpr sym) =>
(a -> Doc ann) -> SymSequence sym a -> Doc ann
prettySymSequence a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty

-- | Given a pretty printer for elements,
--   print a symbolic sequence.
prettySymSequence :: IsExpr (SymExpr sym) =>
  (a -> Doc ann) ->
  SymSequence sym a ->
  Doc ann
prettySymSequence :: forall sym a ann.
IsExpr (SymExpr sym) =>
(a -> Doc ann) -> SymSequence sym a -> Doc ann
prettySymSequence a -> Doc ann
ppa SymSequence sym a
s = if Map (Nonce GlobalNonceGenerator a) (Doc ann) -> Bool
forall k a. Map k a -> Bool
Map.null Map (Nonce GlobalNonceGenerator a) (Doc ann)
bs then Doc ann
x else Doc ann
letlayout
  where
    occMap :: Map (Nonce GlobalNonceGenerator a) Integer
occMap = SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) Integer
-> Map (Nonce GlobalNonceGenerator a) Integer
forall sym a.
SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) Integer
-> Map (Nonce GlobalNonceGenerator a) Integer
computeOccMap SymSequence sym a
s Map (Nonce GlobalNonceGenerator a) Integer
forall a. Monoid a => a
mempty
    (Doc ann
x,Map (Nonce GlobalNonceGenerator a) (Doc ann)
bs) = State (Map (Nonce GlobalNonceGenerator a) (Doc ann)) (Doc ann)
-> Map (Nonce GlobalNonceGenerator a) (Doc ann)
-> (Doc ann, Map (Nonce GlobalNonceGenerator a) (Doc ann))
forall s a. State s a -> s -> (a, s)
runState ((a -> Doc ann)
-> Map (Nonce GlobalNonceGenerator a) Integer
-> SymSequence sym a
-> State (Map (Nonce GlobalNonceGenerator a) (Doc ann)) (Doc ann)
forall sym a ann.
IsExpr (SymExpr sym) =>
(a -> Doc ann)
-> Map (Nonce GlobalNonceGenerator a) Integer
-> SymSequence sym a
-> State (Map (Nonce GlobalNonceGenerator a) (Doc ann)) (Doc ann)
prettyAux a -> Doc ann
ppa Map (Nonce GlobalNonceGenerator a) Integer
occMap SymSequence sym a
s) Map (Nonce GlobalNonceGenerator a) (Doc ann)
forall a. Monoid a => a
mempty
    letlayout :: Doc ann
letlayout = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [Doc ann
"let" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
PP.align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat [ Nonce GlobalNonceGenerator a -> Doc ann -> Doc ann
forall {a} {ann}.
Nonce GlobalNonceGenerator a -> Doc ann -> Doc ann
letbind Nonce GlobalNonceGenerator a
n Doc ann
d | (Nonce GlobalNonceGenerator a
n,Doc ann
d) <- Map (Nonce GlobalNonceGenerator a) (Doc ann)
-> [(Nonce GlobalNonceGenerator a, Doc ann)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Nonce GlobalNonceGenerator a) (Doc ann)
bs ]))
      ,Doc ann
" in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
x
      ]
    letbind :: Nonce GlobalNonceGenerator a -> Doc ann -> Doc ann
letbind Nonce GlobalNonceGenerator a
n Doc ann
d = Nonce GlobalNonceGenerator a -> Doc ann
forall a ann. Nonce GlobalNonceGenerator a -> Doc ann
ppSeqNonce Nonce GlobalNonceGenerator a
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
PP.align Doc ann
d

computeOccMap ::
  SymSequence sym a ->
  Map (Nonce GlobalNonceGenerator a) Integer ->
  Map (Nonce GlobalNonceGenerator a) Integer
computeOccMap :: forall sym a.
SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) Integer
-> Map (Nonce GlobalNonceGenerator a) Integer
computeOccMap = SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) Integer
-> Map (Nonce GlobalNonceGenerator a) Integer
forall {a} {sym} {a}.
Num a =>
SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop
  where
    visit :: k -> (Map k a -> Map k a) -> Map k a -> Map k a
visit k
n Map k a -> Map k a
k Map k a
m
      | Just a
i <- k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
n Map k a
m = k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
n (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) Map k a
m
      | Bool
otherwise = Map k a -> Map k a
k (k -> a -> Map k a -> Map k a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
n a
1 Map k a
m)

    loop :: SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
SymSequenceNil = Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall a. a -> a
id
    loop (SymSequenceCons Nonce GlobalNonceGenerator a
n a
_ SymSequence sym a
tl) = Nonce GlobalNonceGenerator a
-> (Map (Nonce GlobalNonceGenerator a) a
    -> Map (Nonce GlobalNonceGenerator a) a)
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall {k} {a}.
(Ord k, Num a) =>
k -> (Map k a -> Map k a) -> Map k a -> Map k a
visit Nonce GlobalNonceGenerator a
n (SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
tl)
    loop (SymSequenceAppend Nonce GlobalNonceGenerator a
n SymSequence sym a
xs SymSequence sym a
ys) = Nonce GlobalNonceGenerator a
-> (Map (Nonce GlobalNonceGenerator a) a
    -> Map (Nonce GlobalNonceGenerator a) a)
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall {k} {a}.
(Ord k, Num a) =>
k -> (Map k a -> Map k a) -> Map k a -> Map k a
visit Nonce GlobalNonceGenerator a
n (SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
xs (Map (Nonce GlobalNonceGenerator a) a
 -> Map (Nonce GlobalNonceGenerator a) a)
-> (Map (Nonce GlobalNonceGenerator a) a
    -> Map (Nonce GlobalNonceGenerator a) a)
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
ys)
    loop (SymSequenceMerge Nonce GlobalNonceGenerator a
n Pred sym
_ SymSequence sym a
xs SymSequence sym a
ys) = Nonce GlobalNonceGenerator a
-> (Map (Nonce GlobalNonceGenerator a) a
    -> Map (Nonce GlobalNonceGenerator a) a)
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall {k} {a}.
(Ord k, Num a) =>
k -> (Map k a -> Map k a) -> Map k a -> Map k a
visit Nonce GlobalNonceGenerator a
n (SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
xs (Map (Nonce GlobalNonceGenerator a) a
 -> Map (Nonce GlobalNonceGenerator a) a)
-> (Map (Nonce GlobalNonceGenerator a) a
    -> Map (Nonce GlobalNonceGenerator a) a)
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymSequence sym a
-> Map (Nonce GlobalNonceGenerator a) a
-> Map (Nonce GlobalNonceGenerator a) a
loop SymSequence sym a
ys)

ppSeqNonce :: Nonce GlobalNonceGenerator a -> Doc ann
ppSeqNonce :: forall a ann. Nonce GlobalNonceGenerator a -> Doc ann
ppSeqNonce Nonce GlobalNonceGenerator a
n = Doc ann
"s" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall a ann. Show a => a -> Doc ann
PP.viaShow (Nonce GlobalNonceGenerator a -> Word64
forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce GlobalNonceGenerator a
n)

prettyAux ::
  IsExpr (SymExpr sym) =>
  (a -> Doc ann) ->
  Map (Nonce GlobalNonceGenerator a) Integer ->
  SymSequence sym a ->
  State (Map (Nonce GlobalNonceGenerator a) (Doc ann)) (Doc ann)
prettyAux :: forall sym a ann.
IsExpr (SymExpr sym) =>
(a -> Doc ann)
-> Map (Nonce GlobalNonceGenerator a) Integer
-> SymSequence sym a
-> State (Map (Nonce GlobalNonceGenerator a) (Doc ann)) (Doc ann)
prettyAux a -> Doc ann
ppa Map (Nonce GlobalNonceGenerator a) Integer
occMap = SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
goTop
  where
    goTop :: SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
goTop SymSequence sym a
SymSequenceNil = Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.list [])
    goTop (SymSequenceCons Nonce GlobalNonceGenerator a
_ a
v SymSequence sym a
tl) = [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [] [a
v] [SymSequence sym a
tl]
    goTop (SymSequenceAppend Nonce GlobalNonceGenerator a
_ SymSequence sym a
xs SymSequence sym a
ys) = [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [] [] [SymSequence sym a
xs,SymSequence sym a
ys]
    goTop (SymSequenceMerge Nonce GlobalNonceGenerator a
_ Pred sym
p SymSequence sym a
xs SymSequence sym a
ys) =
      do Doc ann
xd <- [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [] [] [SymSequence sym a
xs]
         Doc ann
yd <- [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [] [] [SymSequence sym a
ys]
         Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann
 -> StateT
      (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann))
-> Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a b. (a -> b) -> a -> b
$ {- PP.group $ -} Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
PP.hang Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep
           [ Doc ann
"if" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Pred sym -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr Pred sym
p
           , Doc ann
"then" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
xd
           , Doc ann
"else" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Doc ann
yd
           ]

    visit :: Nonce GlobalNonceGenerator a
-> SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
visit Nonce GlobalNonceGenerator a
n SymSequence sym a
s =
      do Map (Nonce GlobalNonceGenerator a) (Doc ann)
dm <- StateT
  (Map (Nonce GlobalNonceGenerator a) (Doc ann))
  Identity
  (Map (Nonce GlobalNonceGenerator a) (Doc ann))
forall s (m :: Type -> Type). MonadState s m => m s
get
         case Nonce GlobalNonceGenerator a
-> Map (Nonce GlobalNonceGenerator a) (Doc ann) -> Maybe (Doc ann)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nonce GlobalNonceGenerator a
n Map (Nonce GlobalNonceGenerator a) (Doc ann)
dm of
           Just Doc ann
_ -> ()
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity ()
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
           Maybe (Doc ann)
Nothing ->
             do Doc ann
d <- SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
goTop SymSequence sym a
s
                (Map (Nonce GlobalNonceGenerator a) (Doc ann)
 -> Map (Nonce GlobalNonceGenerator a) (Doc ann))
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity ()
forall s (m :: Type -> Type). MonadState s m => (s -> s) -> m ()
modify (Nonce GlobalNonceGenerator a
-> Doc ann
-> Map (Nonce GlobalNonceGenerator a) (Doc ann)
-> Map (Nonce GlobalNonceGenerator a) (Doc ann)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Nonce GlobalNonceGenerator a
n Doc ann
d)
         Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Nonce GlobalNonceGenerator a -> Doc ann
forall a ann. Nonce GlobalNonceGenerator a -> Doc ann
ppSeqNonce Nonce GlobalNonceGenerator a
n)

    finalize :: [Doc ann] -> Doc ann
finalize []  = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.list []
    finalize [Doc ann
x] = Doc ann
x
    finalize [Doc ann]
xs  = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.sep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
PP.punctuate (Doc ann
forall ann. Doc ann
PP.space Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"<>") ([Doc ann] -> [Doc ann]
forall a. [a] -> [a]
reverse [Doc ann]
xs))

    elemSeq :: [a] -> Doc ann
elemSeq [a]
rs = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.list ((a -> Doc ann) -> [a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc ann
ppa ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
rs))

    addSeg :: [Doc ann] -> [a] -> Doc ann -> [Doc ann]
addSeg [Doc ann]
segs [] Doc ann
seg = (Doc ann
seg Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
segs)
    addSeg [Doc ann]
segs [a]
rs Doc ann
seg = (Doc ann
seg Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [a] -> Doc ann
elemSeq [a]
rs Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
segs)

    -- @pp@ accumulates both "segments" of sequences (segs)
    -- and individual values (rs) to be output.  Both are
    -- in reversed order.  Segments represent sequences
    -- and must be combined with the append operator,
    -- and rs represent individual elements that must be combined
    -- with cons (or, in actuality, list syntax with brackets and commas).

    -- @pp@ works over a list of SymSequence values, which represent a worklist
    -- of segments to process.  Morally, the invariant of @pp@ is that the
    -- arguments always represent the same sequence, which is computed as
    -- @concat (reverse segs) ++ reverse rs ++ concat ss@

    pp :: [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [Doc ann]
segs [] [] = Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
finalize [Doc ann]
segs)
    pp [Doc ann]
segs [a]
rs [] = Doc ann
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
forall a.
a
-> StateT (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
finalize ( [a] -> Doc ann
elemSeq [a]
rs Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann]
segs ))

    pp [Doc ann]
segs [a]
rs (SymSequence sym a
SymSequenceNil:[SymSequence sym a]
ss) = [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [Doc ann]
segs [a]
rs [SymSequence sym a]
ss

    pp [Doc ann]
segs [a]
rs (s :: SymSequence sym a
s@(SymSequenceCons Nonce GlobalNonceGenerator a
n a
v SymSequence sym a
tl) : [SymSequence sym a]
ss)
      | Just Integer
i <- Nonce GlobalNonceGenerator a
-> Map (Nonce GlobalNonceGenerator a) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nonce GlobalNonceGenerator a
n Map (Nonce GlobalNonceGenerator a) Integer
occMap, Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1
      = do Doc ann
x <- Nonce GlobalNonceGenerator a
-> SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
visit Nonce GlobalNonceGenerator a
n SymSequence sym a
s
           [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp ([Doc ann] -> [a] -> Doc ann -> [Doc ann]
addSeg [Doc ann]
segs [a]
rs Doc ann
x) [] [SymSequence sym a]
ss

      | Bool
otherwise
      = [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [Doc ann]
segs (a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs) (SymSequence sym a
tl SymSequence sym a -> [SymSequence sym a] -> [SymSequence sym a]
forall a. a -> [a] -> [a]
: [SymSequence sym a]
ss)

    pp [Doc ann]
segs [a]
rs (s :: SymSequence sym a
s@(SymSequenceAppend Nonce GlobalNonceGenerator a
n SymSequence sym a
xs SymSequence sym a
ys) : [SymSequence sym a]
ss)
      | Just Integer
i <- Nonce GlobalNonceGenerator a
-> Map (Nonce GlobalNonceGenerator a) Integer -> Maybe Integer
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nonce GlobalNonceGenerator a
n Map (Nonce GlobalNonceGenerator a) Integer
occMap, Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1
      = do Doc ann
x <- Nonce GlobalNonceGenerator a
-> SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
visit Nonce GlobalNonceGenerator a
n SymSequence sym a
s
           [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp ([Doc ann] -> [a] -> Doc ann -> [Doc ann]
addSeg [Doc ann]
segs [a]
rs Doc ann
x) [] [SymSequence sym a]
ss

      | Bool
otherwise
      = [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp [Doc ann]
segs [a]
rs (SymSequence sym a
xsSymSequence sym a -> [SymSequence sym a] -> [SymSequence sym a]
forall a. a -> [a] -> [a]
:SymSequence sym a
ysSymSequence sym a -> [SymSequence sym a] -> [SymSequence sym a]
forall a. a -> [a] -> [a]
:[SymSequence sym a]
ss)

    pp [Doc ann]
segs [a]
rs (s :: SymSequence sym a
s@(SymSequenceMerge Nonce GlobalNonceGenerator a
n Pred sym
_ SymSequence sym a
_ SymSequence sym a
_) : [SymSequence sym a]
ss)
      = do Doc ann
x <- Nonce GlobalNonceGenerator a
-> SymSequence sym a
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
visit Nonce GlobalNonceGenerator a
n SymSequence sym a
s
           [Doc ann]
-> [a]
-> [SymSequence sym a]
-> StateT
     (Map (Nonce GlobalNonceGenerator a) (Doc ann)) Identity (Doc ann)
pp ([Doc ann] -> [a] -> Doc ann -> [Doc ann]
addSeg [Doc ann]
segs [a]
rs Doc ann
x) [] [SymSequence sym a]
ss