{-# OPTIONS_GHC -fno-warn-orphans      #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE TemplateHaskell           #-}

module PlutusCore.Generators.NEAT.Type where

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












import Control.Enumerable
import Control.Monad (ap)
import PlutusCore
import PlutusCore.Generators.NEAT.Common

newtype Neutral a = Neutral
  { forall a. Neutral a -> a
unNeutral :: a
  }

data TypeBuiltinG = TyByteStringG
                  | TyIntegerG
                  | TyBoolG
                  | TyUnitG
                  | TyStringG
                  | TyListG TypeBuiltinG
                  | TyDataG
                      deriving stock (Int -> TypeBuiltinG -> ShowS
[TypeBuiltinG] -> ShowS
TypeBuiltinG -> String
(Int -> TypeBuiltinG -> ShowS)
-> (TypeBuiltinG -> String)
-> ([TypeBuiltinG] -> ShowS)
-> Show TypeBuiltinG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeBuiltinG -> ShowS
showsPrec :: Int -> TypeBuiltinG -> ShowS
$cshow :: TypeBuiltinG -> String
show :: TypeBuiltinG -> String
$cshowList :: [TypeBuiltinG] -> ShowS
showList :: [TypeBuiltinG] -> ShowS
Show, TypeBuiltinG -> TypeBuiltinG -> Bool
(TypeBuiltinG -> TypeBuiltinG -> Bool)
-> (TypeBuiltinG -> TypeBuiltinG -> Bool) -> Eq TypeBuiltinG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeBuiltinG -> TypeBuiltinG -> Bool
== :: TypeBuiltinG -> TypeBuiltinG -> Bool
$c/= :: TypeBuiltinG -> TypeBuiltinG -> Bool
/= :: TypeBuiltinG -> TypeBuiltinG -> Bool
Eq, Eq TypeBuiltinG
Eq TypeBuiltinG =>
(TypeBuiltinG -> TypeBuiltinG -> Ordering)
-> (TypeBuiltinG -> TypeBuiltinG -> Bool)
-> (TypeBuiltinG -> TypeBuiltinG -> Bool)
-> (TypeBuiltinG -> TypeBuiltinG -> Bool)
-> (TypeBuiltinG -> TypeBuiltinG -> Bool)
-> (TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG)
-> (TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG)
-> Ord TypeBuiltinG
TypeBuiltinG -> TypeBuiltinG -> Bool
TypeBuiltinG -> TypeBuiltinG -> Ordering
TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG
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 :: TypeBuiltinG -> TypeBuiltinG -> Ordering
compare :: TypeBuiltinG -> TypeBuiltinG -> Ordering
$c< :: TypeBuiltinG -> TypeBuiltinG -> Bool
< :: TypeBuiltinG -> TypeBuiltinG -> Bool
$c<= :: TypeBuiltinG -> TypeBuiltinG -> Bool
<= :: TypeBuiltinG -> TypeBuiltinG -> Bool
$c> :: TypeBuiltinG -> TypeBuiltinG -> Bool
> :: TypeBuiltinG -> TypeBuiltinG -> Bool
$c>= :: TypeBuiltinG -> TypeBuiltinG -> Bool
>= :: TypeBuiltinG -> TypeBuiltinG -> Bool
$cmax :: TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG
max :: TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG
$cmin :: TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG
min :: TypeBuiltinG -> TypeBuiltinG -> TypeBuiltinG
Ord)

deriveEnumerable ''TypeBuiltinG

data TypeG n = TyVarG n
             | TyFunG (TypeG n) (TypeG n)
             | TyIFixG (TypeG n) (Kind ()) (TypeG n)
             | TyForallG (Kind ()) (TypeG (S n))
             | TyBuiltinG TypeBuiltinG
             | TyLamG (TypeG (S n))
             | TyAppG (TypeG n) (TypeG n) (Kind ())
                 deriving stock (TypeG n -> TypeG n -> Bool
(TypeG n -> TypeG n -> Bool)
-> (TypeG n -> TypeG n -> Bool) -> Eq (TypeG n)
forall n. Eq n => TypeG n -> TypeG n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall n. Eq n => TypeG n -> TypeG n -> Bool
== :: TypeG n -> TypeG n -> Bool
$c/= :: forall n. Eq n => TypeG n -> TypeG n -> Bool
/= :: TypeG n -> TypeG n -> Bool
Eq, Eq (TypeG n)
Eq (TypeG n) =>
(TypeG n -> TypeG n -> Ordering)
-> (TypeG n -> TypeG n -> Bool)
-> (TypeG n -> TypeG n -> Bool)
-> (TypeG n -> TypeG n -> Bool)
-> (TypeG n -> TypeG n -> Bool)
-> (TypeG n -> TypeG n -> TypeG n)
-> (TypeG n -> TypeG n -> TypeG n)
-> Ord (TypeG n)
TypeG n -> TypeG n -> Bool
TypeG n -> TypeG n -> Ordering
TypeG n -> TypeG n -> TypeG 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 (TypeG n)
forall n. Ord n => TypeG n -> TypeG n -> Bool
forall n. Ord n => TypeG n -> TypeG n -> Ordering
forall n. Ord n => TypeG n -> TypeG n -> TypeG n
$ccompare :: forall n. Ord n => TypeG n -> TypeG n -> Ordering
compare :: TypeG n -> TypeG n -> Ordering
$c< :: forall n. Ord n => TypeG n -> TypeG n -> Bool
< :: TypeG n -> TypeG n -> Bool
$c<= :: forall n. Ord n => TypeG n -> TypeG n -> Bool
<= :: TypeG n -> TypeG n -> Bool
$c> :: forall n. Ord n => TypeG n -> TypeG n -> Bool
> :: TypeG n -> TypeG n -> Bool
$c>= :: forall n. Ord n => TypeG n -> TypeG n -> Bool
>= :: TypeG n -> TypeG n -> Bool
$cmax :: forall n. Ord n => TypeG n -> TypeG n -> TypeG n
max :: TypeG n -> TypeG n -> TypeG n
$cmin :: forall n. Ord n => TypeG n -> TypeG n -> TypeG n
min :: TypeG n -> TypeG n -> TypeG n
Ord, Int -> TypeG n -> ShowS
[TypeG n] -> ShowS
TypeG n -> String
(Int -> TypeG n -> ShowS)
-> (TypeG n -> String) -> ([TypeG n] -> ShowS) -> Show (TypeG n)
forall n. Show n => Int -> TypeG n -> ShowS
forall n. Show n => [TypeG n] -> ShowS
forall n. Show n => TypeG n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall n. Show n => Int -> TypeG n -> ShowS
showsPrec :: Int -> TypeG n -> ShowS
$cshow :: forall n. Show n => TypeG n -> String
show :: TypeG n -> String
$cshowList :: forall n. Show n => [TypeG n] -> ShowS
showList :: [TypeG n] -> ShowS
Show)

deriving stock instance Ord (Kind ())

deriveEnumerable ''Kind

deriveEnumerable ''TypeG

type ClosedTypeG = TypeG Z

instance Functor TypeG where
  fmap :: forall a b. (a -> b) -> TypeG a -> TypeG b
fmap = (a -> b) -> TypeG a -> TypeG b
forall a b. (a -> b) -> TypeG a -> TypeG b
ren

ext :: (m -> n) -> S m -> S n
ext :: forall m n. (m -> n) -> S m -> S n
ext m -> n
_ S m
FZ     = S n
forall n. S n
FZ
ext m -> n
f (FS m
x) = n -> S n
forall n. n -> S n
FS (m -> n
f m
x)

ren :: (m -> n) -> TypeG m -> TypeG n
ren :: forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f (TyVarG m
x)           = n -> TypeG n
forall n. n -> TypeG n
TyVarG (m -> n
f m
x)
ren m -> n
f (TyFunG TypeG m
ty1 TypeG m
ty2)     = TypeG n -> TypeG n -> TypeG n
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty1) ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty2)
ren m -> n
f (TyIFixG TypeG m
ty1 Kind ()
k TypeG m
ty2)  = TypeG n -> Kind () -> TypeG n -> TypeG n
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty1) Kind ()
k ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty2)
ren m -> n
f (TyForallG Kind ()
k TypeG (S m)
ty)     = Kind () -> TypeG (S n) -> TypeG n
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG Kind ()
k ((S m -> S n) -> TypeG (S m) -> TypeG (S n)
forall a b. (a -> b) -> TypeG a -> TypeG b
ren ((m -> n) -> S m -> S n
forall m n. (m -> n) -> S m -> S n
ext m -> n
f) TypeG (S m)
ty)
ren m -> n
_ (TyBuiltinG TypeBuiltinG
someUni) = TypeBuiltinG -> TypeG n
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
someUni
ren m -> n
f (TyLamG TypeG (S m)
ty)          = TypeG (S n) -> TypeG n
forall n. TypeG (S n) -> TypeG n
TyLamG ((S m -> S n) -> TypeG (S m) -> TypeG (S n)
forall a b. (a -> b) -> TypeG a -> TypeG b
ren ((m -> n) -> S m -> S n
forall m n. (m -> n) -> S m -> S n
ext m -> n
f) TypeG (S m)
ty)
ren m -> n
f (TyAppG TypeG m
ty1 TypeG m
ty2 Kind ()
k)   = TypeG n -> TypeG n -> Kind () -> TypeG n
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty1) ((m -> n) -> TypeG m -> TypeG n
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> n
f TypeG m
ty2) Kind ()
k

exts :: (n -> TypeG m) -> S n -> TypeG (S m)
exts :: forall n m. (n -> TypeG m) -> S n -> TypeG (S m)
exts n -> TypeG m
_ S n
FZ     = S m -> TypeG (S m)
forall n. n -> TypeG n
TyVarG S m
forall n. S n
FZ
exts n -> TypeG m
s (FS n
i) = (m -> S m) -> TypeG m -> TypeG (S m)
forall a b. (a -> b) -> TypeG a -> TypeG b
ren m -> S m
forall n. n -> S n
FS (n -> TypeG m
s n
i)

sub :: (n -> TypeG m) -> TypeG n -> TypeG m
sub :: forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s (TyVarG n
i)             = n -> TypeG m
s n
i
sub n -> TypeG m
s (TyFunG TypeG n
ty1 TypeG n
ty2)       = TypeG m -> TypeG m -> TypeG m
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty1) ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty2)
sub n -> TypeG m
s (TyIFixG TypeG n
ty1 Kind ()
k TypeG n
ty2)    = TypeG m -> Kind () -> TypeG m -> TypeG m
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty1) Kind ()
k ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty2)
sub n -> TypeG m
s (TyForallG Kind ()
k TypeG (S n)
ty)       = Kind () -> TypeG (S m) -> TypeG m
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG Kind ()
k ((S n -> TypeG (S m)) -> TypeG (S n) -> TypeG (S m)
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub ((n -> TypeG m) -> S n -> TypeG (S m)
forall n m. (n -> TypeG m) -> S n -> TypeG (S m)
exts n -> TypeG m
s) TypeG (S n)
ty)
sub n -> TypeG m
_ (TyBuiltinG TypeBuiltinG
tyBuiltin) = TypeBuiltinG -> TypeG m
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
tyBuiltin
sub n -> TypeG m
s (TyLamG TypeG (S n)
ty)            = TypeG (S m) -> TypeG m
forall n. TypeG (S n) -> TypeG n
TyLamG ((S n -> TypeG (S m)) -> TypeG (S n) -> TypeG (S m)
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub ((n -> TypeG m) -> S n -> TypeG (S m)
forall n m. (n -> TypeG m) -> S n -> TypeG (S m)
exts n -> TypeG m
s) TypeG (S n)
ty)
sub n -> TypeG m
s (TyAppG TypeG n
ty1 TypeG n
ty2 Kind ()
k)     = TypeG m -> TypeG m -> Kind () -> TypeG m
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty1) ((n -> TypeG m) -> TypeG n -> TypeG m
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub n -> TypeG m
s TypeG n
ty2) Kind ()
k

instance Monad TypeG where
  TypeG a
a >>= :: forall a b. TypeG a -> (a -> TypeG b) -> TypeG b
>>= a -> TypeG b
f = (a -> TypeG b) -> TypeG a -> TypeG b
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub a -> TypeG b
f TypeG a
a
--  return = pure

instance Applicative TypeG where
  <*> :: forall a b. TypeG (a -> b) -> TypeG a -> TypeG b
(<*>) = TypeG (a -> b) -> TypeG a -> TypeG b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
  pure :: forall n. n -> TypeG n
pure = a -> TypeG a
forall n. n -> TypeG n
TyVarG