{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE EmptyDataDeriving   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}

module PlutusCore.Generators.NEAT.Common where

{-
!!! THIS FILE IS GENERATED FROM Common.agda
!!! DO NOT EDIT THIS FILE. EDIT Common.agda
!!! AND THEN RUN agda2hs ON IT.
-}








import Control.Enumerable
import Data.Stream qualified as Stream
import Data.Text qualified as Text
import PlutusCore.Name.Unique (Name, TyName (..))
import PlutusCore.Quote (MonadQuote (..), freshName)

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

data S n = FZ
         | FS n
             deriving stock (S n -> S n -> Bool
(S n -> S n -> Bool) -> (S n -> S n -> Bool) -> Eq (S n)
forall n. Eq n => S n -> S n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall n. Eq n => S n -> S n -> Bool
== :: S n -> S n -> Bool
$c/= :: forall n. Eq n => S n -> S n -> Bool
/= :: S n -> S n -> Bool
Eq, Eq (S n)
Eq (S n) =>
(S n -> S n -> Ordering)
-> (S n -> S n -> Bool)
-> (S n -> S n -> Bool)
-> (S n -> S n -> Bool)
-> (S n -> S n -> Bool)
-> (S n -> S n -> S n)
-> (S n -> S n -> S n)
-> Ord (S n)
S n -> S n -> Bool
S n -> S n -> Ordering
S n -> S n -> S n
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 n. Ord n => Eq (S n)
forall n. Ord n => S n -> S n -> Bool
forall n. Ord n => S n -> S n -> Ordering
forall n. Ord n => S n -> S n -> S n
$ccompare :: forall n. Ord n => S n -> S n -> Ordering
compare :: S n -> S n -> Ordering
$c< :: forall n. Ord n => S n -> S n -> Bool
< :: S n -> S n -> Bool
$c<= :: forall n. Ord n => S n -> S n -> Bool
<= :: S n -> S n -> Bool
$c> :: forall n. Ord n => S n -> S n -> Bool
> :: S n -> S n -> Bool
$c>= :: forall n. Ord n => S n -> S n -> Bool
>= :: S n -> S n -> Bool
$cmax :: forall n. Ord n => S n -> S n -> S n
max :: S n -> S n -> S n
$cmin :: forall n. Ord n => S n -> S n -> S n
min :: S n -> S n -> S n
Ord, Int -> S n -> ShowS
[S n] -> ShowS
S n -> String
(Int -> S n -> ShowS)
-> (S n -> String) -> ([S n] -> ShowS) -> Show (S n)
forall n. Show n => Int -> S n -> ShowS
forall n. Show n => [S n] -> ShowS
forall n. Show n => S n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall n. Show n => Int -> S n -> ShowS
showsPrec :: Int -> S n -> ShowS
$cshow :: forall n. Show n => S n -> String
show :: S n -> String
$cshowList :: forall n. Show n => [S n] -> ShowS
showList :: [S n] -> ShowS
Show, (forall a b. (a -> b) -> S a -> S b)
-> (forall a b. a -> S b -> S a) -> Functor S
forall a b. a -> S b -> S a
forall a b. (a -> b) -> S a -> S b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> S a -> S b
fmap :: forall a b. (a -> b) -> S a -> S b
$c<$ :: forall a b. a -> S b -> S a
<$ :: forall a b. a -> S b -> S a
Functor)

instance Enumerable Z where
  enumerate :: forall (f :: * -> *). (Typeable f, Sized f) => Shared f Z
enumerate = [Shareable f Z] -> Shared f Z
forall a (f :: * -> *).
(Typeable a, Sized f, Typeable f) =>
[Shareable f a] -> Shared f a
datatype []

instance Enumerable n => Enumerable (S n) where
  enumerate :: forall (f :: * -> *). (Typeable f, Sized f) => Shared f (S n)
enumerate = Shareable f (S n) -> Shared f (S n)
forall a (f :: * -> *).
(Typeable a, Typeable f) =>
Shareable f a -> Shared f a
share (Shareable f (S n) -> Shared f (S n))
-> Shareable f (S n) -> Shared f (S n)
forall a b. (a -> b) -> a -> b
$ [Shareable f (S n)] -> Shareable f (S n)
forall a. [Shareable f a] -> Shareable f a
forall (f :: * -> *) a. Sized f => [f a] -> f a
aconcat
    [ S n -> Shareable f (S n)
forall (f :: * -> *) a. Sized f => a -> Shareable f a
c0 S n
forall n. S n
FZ
    , (n -> S n) -> Shareable f (S n)
forall a (f :: * -> *) x.
(Enumerable a, Sized f, Typeable f) =>
(a -> x) -> Shareable f x
c1 n -> S n
forall n. n -> S n
FS
    ]

-- |Absurd for the zero type.
fromZ :: Z -> a
fromZ :: forall a. Z -> a
fromZ Z
i = case Z
i of {}

-- * Namespaces

data NameState n = NameState { forall n. NameState n -> n -> Name
nameOf :: n -> Name, forall n. NameState n -> Stream Text
freshNameStrings :: Stream.Stream Text.Text }

newtype TyNameState n = TyNameState (NameState n)

tynameOf :: TyNameState n -> n -> TyName
tynameOf :: forall n. TyNameState n -> n -> TyName
tynameOf (TyNameState NameState{Stream Text
n -> Name
nameOf :: forall n. NameState n -> n -> Name
freshNameStrings :: forall n. NameState n -> Stream Text
nameOf :: n -> Name
freshNameStrings :: Stream Text
..}) n
i = Name -> TyName
TyName (n -> Name
nameOf n
i)

-- |Create an empty name state from a stream of text names.
emptyNameState :: Stream.Stream Text.Text -> NameState Z
emptyNameState :: Stream Text -> NameState Z
emptyNameState Stream Text
strs = NameState { nameOf :: Z -> Name
nameOf = Z -> Name
forall a. Z -> a
fromZ, freshNameStrings :: Stream Text
freshNameStrings = Stream Text
strs }

-- |Extend name state with a fresh name.
extNameState
  :: (MonadQuote m)
  => NameState n
  -> m (NameState (S n))
extNameState :: forall (m :: * -> *) n.
MonadQuote m =>
NameState n -> m (NameState (S n))
extNameState NameState{Stream Text
n -> Name
nameOf :: forall n. NameState n -> n -> Name
freshNameStrings :: forall n. NameState n -> Stream Text
nameOf :: n -> Name
freshNameStrings :: Stream Text
..} = Quote (NameState (S n)) -> m (NameState (S n))
forall a. Quote a -> m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (NameState (S n)) -> m (NameState (S n)))
-> Quote (NameState (S n)) -> m (NameState (S n))
forall a b. (a -> b) -> a -> b
$ do
  let str :: Text
str = Stream Text -> Text
forall a. Stream a -> a
Stream.head Stream Text
freshNameStrings
      freshNameStrings' :: Stream Text
freshNameStrings' = Stream Text -> Stream Text
forall a. Stream a -> Stream a
Stream.tail Stream Text
freshNameStrings
  Name
name <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
str
  let nameOf' :: S n -> Name
nameOf' S n
FZ     = Name
name
      nameOf' (FS n
i) = n -> Name
nameOf n
i
  NameState (S n) -> Quote (NameState (S n))
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return NameState { nameOf :: S n -> Name
nameOf = S n -> Name
nameOf', freshNameStrings :: Stream Text
freshNameStrings = Stream Text
freshNameStrings' }

-- |Create an empty name state from a stream of text names.
emptyTyNameState :: Stream.Stream Text.Text -> TyNameState Z
emptyTyNameState :: Stream Text -> TyNameState Z
emptyTyNameState Stream Text
strs = NameState Z -> TyNameState Z
forall n. NameState n -> TyNameState n
TyNameState (Stream Text -> NameState Z
emptyNameState Stream Text
strs)

-- |Extend type name state with a fresh type name.
extTyNameState
  :: (MonadQuote m)
  => TyNameState n
  -> m (TyNameState (S n))
extTyNameState :: forall (m :: * -> *) n.
MonadQuote m =>
TyNameState n -> m (TyNameState (S n))
extTyNameState (TyNameState NameState n
nameState) =
  NameState (S n) -> TyNameState (S n)
forall n. NameState n -> TyNameState n
TyNameState (NameState (S n) -> TyNameState (S n))
-> m (NameState (S n)) -> m (TyNameState (S n))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NameState n -> m (NameState (S n))
forall (m :: * -> *) n.
MonadQuote m =>
NameState n -> m (NameState (S n))
extNameState NameState n
nameState

-- |Create a stream of names |x0, x1, x2, ...| from a prefix |"x"|
mkTextNameStream :: Text.Text -> Stream.Stream Text.Text
mkTextNameStream :: Text -> Stream Text
mkTextNameStream Text
prefix =
  (Integer -> Text) -> Stream Integer -> Stream Text
forall a b. (a -> b) -> Stream a -> Stream b
Stream.map
    (\Integer
n -> Text
prefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (Integer -> String
forall a. Show a => a -> String
show Integer
n))
    ((Integer -> Integer) -> Integer -> Stream Integer
forall a. (a -> a) -> a -> Stream a
Stream.iterate (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Integer
0 :: Integer))