-- editorconfig-checker-disable-file
{-| Description: PLC Syntax, typechecker,semantics property based testing.

This file contains
1. A duplicate of the Plutus Core Abstract Syntax (types and terms)
2. A kind checker and a type checker
3. Reduction semantics for types
-}

{-# OPTIONS_GHC -fno-warn-orphans      #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TemplateHaskell           #-}
{-# LANGUAGE TypeApplications          #-}


module PlutusCore.Generators.NEAT.Term
  ( TypeBuiltinG (..)
  , TermConstantG (..)
  , TypeG (..)
  , ClosedTypeG
  , convertClosedType
  , TermG (..)
  , ClosedTermG
  , convertClosedTerm
  , Check (..)
  , stepTypeG
  , normalizeTypeG
  , GenError (..)
  , Neutral (..)
  ) where

import Control.Enumerable
import Control.Monad.Except
import Data.Bifunctor.TH
import Data.ByteString (ByteString, pack)
import Data.Coolean (Cool, false, toCool, true, (&&&))
import Data.Map qualified as Map
import Data.Stream qualified as Stream
import Data.Text qualified as Text
import Data.Text.Encoding (decodeUtf8)
import PlutusCore
import PlutusCore.Data
import PlutusCore.Default
import PlutusCore.Generators.NEAT.Common
import Text.Printf

import PlutusCore.Generators.NEAT.Type

{-

NOTE: We don't just want to enumerate arbitrary types but also normal
      types that cannot reduce any further. Neutral types are a subset
      of normal forms that consist of either a variable or a stuck
      application.

      Two approaches spring to mind:

      1. We could define a separate AST for normal types and possibly
      also a separate AST for terms with normalized types. This would
      be the safest option as it would then be impossible to generate
      a non-normalized type that claimed to be normalized. This is how
      it's done in the metatheory package. The downside is that there
      there is some duplication of code and/or it's a bit cumbersome and
      slow to convert from a normalized type back to an ordinary one.

     2. We could use a simple newtype wrapper to mark a type as
     normalized/neutral. This is how it's done in the plutus-core
     package. It's a helpful cue but there's nothing stopping us
     marking any type as normalised. This saves some extra work as we
     can conveniently unwrap a normal form and reuse code such as
     substitution.

     Here we go with option 2. The enumerable instances below explain
     how to construct a normalized or neutral type using the machinery of
     Control.Enumerable from the sized-based package.
-}

instance Enumerable tyname => Enumerable (Normalized (TypeG tyname)) where
  enumerate :: forall (f :: * -> *).
(Typeable f, Sized f) =>
Shared f (Normalized (TypeG tyname))
enumerate = Shareable f (Normalized (TypeG tyname))
-> Shared f (Normalized (TypeG tyname))
forall a (f :: * -> *).
(Typeable a, Typeable f) =>
Shareable f a -> Shared f a
share (Shareable f (Normalized (TypeG tyname))
 -> Shared f (Normalized (TypeG tyname)))
-> Shareable f (Normalized (TypeG tyname))
-> Shared f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ [Shareable f (Normalized (TypeG tyname))]
-> Shareable f (Normalized (TypeG tyname))
forall a. [Shareable f a] -> Shareable f a
forall (f :: * -> *) a. Sized f => [f a] -> f a
aconcat
    [       (Neutral (TypeG tyname) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a (f :: * -> *) x.
(Enumerable a, Sized f, Typeable f) =>
(a -> x) -> Shareable f x
c1 ((Neutral (TypeG tyname) -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (Neutral (TypeG tyname) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Neutral (TypeG tyname)
ty -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (Neutral (TypeG tyname) -> TypeG tyname
forall a. Neutral a -> a
unNeutral Neutral (TypeG tyname)
ty)
    , Shareable f (Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> ((Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
    -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a (f :: * -> *) x.
(Enumerable a, Sized f, Typeable f) =>
(a -> x) -> Shareable f x
c1 ((Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Normalized (TypeG (S tyname))
ty -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (TypeG (S tyname) -> TypeG tyname
forall n. TypeG (S n) -> TypeG n
TyLamG (Normalized (TypeG (S tyname)) -> TypeG (S tyname)
forall a. Normalized a -> a
unNormalized Normalized (TypeG (S tyname))
ty))
    , Shareable f (Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> ((Normalized (TypeG tyname)
     -> Kind ()
     -> Normalized (TypeG tyname)
     -> Normalized (TypeG tyname))
    -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG tyname)
    -> Kind ()
    -> Normalized (TypeG tyname)
    -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Normalized (TypeG tyname)
 -> Kind ()
 -> Normalized (TypeG tyname)
 -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b c (f :: * -> *) x.
(Enumerable a, Enumerable b, Enumerable c, Sized f, Typeable f) =>
(a -> b -> c -> x) -> Shareable f x
c3 ((Normalized (TypeG tyname)
  -> Kind ()
  -> Normalized (TypeG tyname)
  -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG tyname)
    -> Kind ()
    -> Normalized (TypeG tyname)
    -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Normalized (TypeG tyname)
ty1 Kind ()
k Normalized (TypeG tyname)
ty2 -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (TypeG tyname -> Kind () -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (Normalized (TypeG tyname) -> TypeG tyname
forall a. Normalized a -> a
unNormalized Normalized (TypeG tyname)
ty1) Kind ()
k (Normalized (TypeG tyname) -> TypeG tyname
forall a. Normalized a -> a
unNormalized Normalized (TypeG tyname)
ty2))
    , Shareable f (Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> ((Kind ()
     -> Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
    -> Shareable f (Normalized (TypeG tyname)))
-> (Kind ()
    -> Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind ()
 -> Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b (f :: * -> *) x.
(Enumerable a, Enumerable b, Sized f, Typeable f) =>
(a -> b -> x) -> Shareable f x
c2 ((Kind ()
  -> Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (Kind ()
    -> Normalized (TypeG (S tyname)) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Kind ()
k Normalized (TypeG (S tyname))
ty      -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (Kind () -> TypeG (S tyname) -> TypeG tyname
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG Kind ()
k (Normalized (TypeG (S tyname)) -> TypeG (S tyname)
forall a. Normalized a -> a
unNormalized Normalized (TypeG (S tyname))
ty))
    , Shareable f (Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> ((TypeBuiltinG -> Normalized (TypeG tyname))
    -> Shareable f (Normalized (TypeG tyname)))
-> (TypeBuiltinG -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeBuiltinG -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a (f :: * -> *) x.
(Enumerable a, Sized f, Typeable f) =>
(a -> x) -> Shareable f x
c1 ((TypeBuiltinG -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (TypeBuiltinG -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \TypeBuiltinG
tyBuiltin -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
tyBuiltin)
    , Shareable f (Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> ((Normalized (TypeG tyname)
     -> Normalized (TypeG tyname) -> Normalized (TypeG tyname))
    -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG tyname)
    -> Normalized (TypeG tyname) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Normalized (TypeG tyname)
 -> Normalized (TypeG tyname) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b (f :: * -> *) x.
(Enumerable a, Enumerable b, Sized f, Typeable f) =>
(a -> b -> x) -> Shareable f x
c2 ((Normalized (TypeG tyname)
  -> Normalized (TypeG tyname) -> Normalized (TypeG tyname))
 -> Shareable f (Normalized (TypeG tyname)))
-> (Normalized (TypeG tyname)
    -> Normalized (TypeG tyname) -> Normalized (TypeG tyname))
-> Shareable f (Normalized (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Normalized (TypeG tyname)
ty1 Normalized (TypeG tyname)
ty2   -> TypeG tyname -> Normalized (TypeG tyname)
forall a. a -> Normalized a
Normalized (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (Normalized (TypeG tyname) -> TypeG tyname
forall a. Normalized a -> a
unNormalized Normalized (TypeG tyname)
ty1) (Normalized (TypeG tyname) -> TypeG tyname
forall a. Normalized a -> a
unNormalized Normalized (TypeG tyname)
ty2))
    ]

instance Enumerable tyname => Enumerable (Neutral (TypeG tyname)) where
  enumerate :: forall (f :: * -> *).
(Typeable f, Sized f) =>
Shared f (Neutral (TypeG tyname))
enumerate = Shareable f (Neutral (TypeG tyname))
-> Shared f (Neutral (TypeG tyname))
forall a (f :: * -> *).
(Typeable a, Typeable f) =>
Shareable f a -> Shared f a
share (Shareable f (Neutral (TypeG tyname))
 -> Shared f (Neutral (TypeG tyname)))
-> Shareable f (Neutral (TypeG tyname))
-> Shared f (Neutral (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ [Shareable f (Neutral (TypeG tyname))]
-> Shareable f (Neutral (TypeG tyname))
forall a. [Shareable f a] -> Shareable f a
forall (f :: * -> *) a. Sized f => [f a] -> f a
aconcat
    [ Shareable f (Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Neutral (TypeG tyname))
 -> Shareable f (Neutral (TypeG tyname)))
-> ((tyname -> Neutral (TypeG tyname))
    -> Shareable f (Neutral (TypeG tyname)))
-> (tyname -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a (f :: * -> *) x.
(Enumerable a, Sized f, Typeable f) =>
(a -> x) -> Shareable f x
c1 ((tyname -> Neutral (TypeG tyname))
 -> Shareable f (Neutral (TypeG tyname)))
-> (tyname -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \tyname
i         -> TypeG tyname -> Neutral (TypeG tyname)
forall a. a -> Neutral a
Neutral (tyname -> TypeG tyname
forall n. n -> TypeG n
TyVarG tyname
i)
    , Shareable f (Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a. Shareable f a -> Shareable f a
forall (f :: * -> *) a. Sized f => f a -> f a
pay (Shareable f (Neutral (TypeG tyname))
 -> Shareable f (Neutral (TypeG tyname)))
-> ((Neutral (TypeG tyname)
     -> Normalized (TypeG tyname) -> Kind () -> Neutral (TypeG tyname))
    -> Shareable f (Neutral (TypeG tyname)))
-> (Neutral (TypeG tyname)
    -> Normalized (TypeG tyname) -> Kind () -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Neutral (TypeG tyname)
 -> Normalized (TypeG tyname) -> Kind () -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a b c (f :: * -> *) x.
(Enumerable a, Enumerable b, Enumerable c, Sized f, Typeable f) =>
(a -> b -> c -> x) -> Shareable f x
c3 ((Neutral (TypeG tyname)
  -> Normalized (TypeG tyname) -> Kind () -> Neutral (TypeG tyname))
 -> Shareable f (Neutral (TypeG tyname)))
-> (Neutral (TypeG tyname)
    -> Normalized (TypeG tyname) -> Kind () -> Neutral (TypeG tyname))
-> Shareable f (Neutral (TypeG tyname))
forall a b. (a -> b) -> a -> b
$ \Neutral (TypeG tyname)
ty1 Normalized (TypeG tyname)
ty2 Kind ()
k -> TypeG tyname -> Neutral (TypeG tyname)
forall a. a -> Neutral a
Neutral (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (Neutral (TypeG tyname) -> TypeG tyname
forall a. Neutral a -> a
unNeutral Neutral (TypeG tyname)
ty1) (Normalized (TypeG tyname) -> TypeG tyname
forall a. Normalized a -> a
unNormalized Normalized (TypeG tyname)
ty2) Kind ()
k)
    ]

-- ** Enumerating terms

-- Word8 is enumerable so we get an enumerable instance via pack
instance Enumerable ByteString where
  enumerate :: forall (f :: * -> *). (Typeable f, Sized f) => Shared f ByteString
enumerate = Shareable f ByteString -> Shared f ByteString
forall a (f :: * -> *).
(Typeable a, Typeable f) =>
Shareable f a -> Shared f a
share (Shareable f ByteString -> Shared f ByteString)
-> Shareable f ByteString -> Shared f ByteString
forall a b. (a -> b) -> a -> b
$ ([Word8] -> ByteString)
-> Shareable f [Word8] -> Shareable f ByteString
forall a b. (a -> b) -> Shareable f a -> Shareable f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Word8] -> ByteString
pack Shareable f [Word8]
forall a (f :: * -> *).
(Enumerable a, Sized f, Typeable f) =>
Shareable f a
access

instance (Enumerable Text.Text) where
  enumerate :: forall (f :: * -> *). (Typeable f, Sized f) => Shared f Text
enumerate = Shareable f Text -> Shared f Text
forall a (f :: * -> *).
(Typeable a, Typeable f) =>
Shareable f a -> Shared f a
share (Shareable f Text -> Shared f Text)
-> Shareable f Text -> Shared f Text
forall a b. (a -> b) -> a -> b
$ ([Word8] -> Text) -> Shareable f [Word8] -> Shareable f Text
forall a b. (a -> b) -> Shareable f a -> Shareable f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ByteString -> Text
decodeUtf8 (ByteString -> Text) -> ([Word8] -> ByteString) -> [Word8] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
pack) Shareable f [Word8]
forall a (f :: * -> *).
(Enumerable a, Sized f, Typeable f) =>
Shareable f a
access

data TermConstantG = TmIntegerG Integer
                   | TmByteStringG ByteString
                   | TmStringG Text.Text
                   | TmBoolG Bool
                   | TmUnitG ()
                   | TmDataG Data
                   deriving stock (Int -> TermConstantG -> ShowS
[TermConstantG] -> ShowS
TermConstantG -> String
(Int -> TermConstantG -> ShowS)
-> (TermConstantG -> String)
-> ([TermConstantG] -> ShowS)
-> Show TermConstantG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TermConstantG -> ShowS
showsPrec :: Int -> TermConstantG -> ShowS
$cshow :: TermConstantG -> String
show :: TermConstantG -> String
$cshowList :: [TermConstantG] -> ShowS
showList :: [TermConstantG] -> ShowS
Show, TermConstantG -> TermConstantG -> Bool
(TermConstantG -> TermConstantG -> Bool)
-> (TermConstantG -> TermConstantG -> Bool) -> Eq TermConstantG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TermConstantG -> TermConstantG -> Bool
== :: TermConstantG -> TermConstantG -> Bool
$c/= :: TermConstantG -> TermConstantG -> Bool
/= :: TermConstantG -> TermConstantG -> Bool
Eq)

deriveEnumerable ''Data

deriveEnumerable ''TermConstantG

deriveEnumerable ''DefaultFun

data TermG tyname name
    = VarG
      name
    | LamAbsG
      (TermG tyname (S name))
    | ApplyG
      (TermG tyname name)
      (TermG tyname name)
      (TypeG tyname)
    | TyAbsG
      (TermG (S tyname) name)
    | TyInstG
      (TermG tyname name)
      (TypeG (S tyname))
      (TypeG tyname)
      (Kind ())
    | ConstantG TermConstantG
    | BuiltinG DefaultFun
    | WrapG (TermG tyname name)
    | UnWrapG (TypeG tyname) (Kind ()) (TypeG tyname) (TermG tyname name)
    | ErrorG (TypeG tyname)
    deriving stock (TermG tyname name -> TermG tyname name -> Bool
(TermG tyname name -> TermG tyname name -> Bool)
-> (TermG tyname name -> TermG tyname name -> Bool)
-> Eq (TermG tyname name)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall tyname name.
(Eq name, Eq tyname) =>
TermG tyname name -> TermG tyname name -> Bool
$c== :: forall tyname name.
(Eq name, Eq tyname) =>
TermG tyname name -> TermG tyname name -> Bool
== :: TermG tyname name -> TermG tyname name -> Bool
$c/= :: forall tyname name.
(Eq name, Eq tyname) =>
TermG tyname name -> TermG tyname name -> Bool
/= :: TermG tyname name -> TermG tyname name -> Bool
Eq, (forall a b. (a -> b) -> TermG tyname a -> TermG tyname b)
-> (forall a b. a -> TermG tyname b -> TermG tyname a)
-> Functor (TermG tyname)
forall a b. a -> TermG tyname b -> TermG tyname a
forall a b. (a -> b) -> TermG tyname a -> TermG tyname b
forall tyname a b. a -> TermG tyname b -> TermG tyname a
forall tyname a b. (a -> b) -> TermG tyname a -> TermG tyname b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall tyname a b. (a -> b) -> TermG tyname a -> TermG tyname b
fmap :: forall a b. (a -> b) -> TermG tyname a -> TermG tyname b
$c<$ :: forall tyname a b. a -> TermG tyname b -> TermG tyname a
<$ :: forall a b. a -> TermG tyname b -> TermG tyname a
Functor, Int -> TermG tyname name -> ShowS
[TermG tyname name] -> ShowS
TermG tyname name -> String
(Int -> TermG tyname name -> ShowS)
-> (TermG tyname name -> String)
-> ([TermG tyname name] -> ShowS)
-> Show (TermG tyname name)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall tyname name.
(Show name, Show tyname) =>
Int -> TermG tyname name -> ShowS
forall tyname name.
(Show name, Show tyname) =>
[TermG tyname name] -> ShowS
forall tyname name.
(Show name, Show tyname) =>
TermG tyname name -> String
$cshowsPrec :: forall tyname name.
(Show name, Show tyname) =>
Int -> TermG tyname name -> ShowS
showsPrec :: Int -> TermG tyname name -> ShowS
$cshow :: forall tyname name.
(Show name, Show tyname) =>
TermG tyname name -> String
show :: TermG tyname name -> String
$cshowList :: forall tyname name.
(Show name, Show tyname) =>
[TermG tyname name] -> ShowS
showList :: [TermG tyname name] -> ShowS
Show)

deriveBifunctor ''TermG
deriveEnumerable ''TermG

type ClosedTermG = TermG Z Z

-- * Converting types

-- |Convert generated builtin types to Plutus builtin types.
convertTypeBuiltin :: TypeBuiltinG -> SomeTypeIn DefaultUni
convertTypeBuiltin :: TypeBuiltinG -> SomeTypeIn DefaultUni
convertTypeBuiltin TypeBuiltinG
TyByteStringG = DefaultUni (Esc ByteString) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc ByteString)
DefaultUniByteString
convertTypeBuiltin TypeBuiltinG
TyIntegerG    = DefaultUni (Esc Integer) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Integer)
DefaultUniInteger
convertTypeBuiltin TypeBuiltinG
TyBoolG       = DefaultUni (Esc Bool) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Bool)
DefaultUniBool
convertTypeBuiltin TypeBuiltinG
TyUnitG       = DefaultUni (Esc ()) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc ())
DefaultUniUnit
convertTypeBuiltin (TyListG TypeBuiltinG
a)   =
  case TypeBuiltinG -> SomeTypeIn DefaultUni
convertTypeBuiltin TypeBuiltinG
a of
    SomeTypeIn DefaultUni (Esc a)
a' -> case [Int] -> Maybe (SomeTypeIn (Kinded DefaultUni))
forall (uni :: * -> *).
Closed uni =>
[Int] -> Maybe (SomeTypeIn (Kinded uni))
decodeKindedUni (DefaultUni (Esc a) -> [Int]
forall a. DefaultUni a -> [Int]
forall (uni :: * -> *) a. Closed uni => uni a -> [Int]
encodeUni DefaultUni (Esc a)
a') of
      Maybe (SomeTypeIn (Kinded DefaultUni))
Nothing -> String -> SomeTypeIn DefaultUni
forall a. HasCallStack => String -> a
error String
"encode;decode failed"
      Just (SomeTypeIn (Kinded DefaultUni (Esc a)
ka)) -> case forall (uni :: * -> *) a (x :: a).
Typeable a =>
uni (Esc x) -> Maybe (a :~: *)
checkStar @DefaultUni DefaultUni (Esc a)
ka of
        Maybe (k :~: *)
Nothing   -> String -> SomeTypeIn DefaultUni
forall a. HasCallStack => String -> a
error String
"higher kinded thing in list"
        Just k :~: *
Refl -> DefaultUni (Esc [a]) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn (DefaultUni (Esc a) -> DefaultUni (Esc [a])
forall {a} {k1} {k2} {f :: k1 -> k2} {a1 :: k1}.
(a ~ Esc (f a1), Esc f ~ Esc []) =>
DefaultUni (Esc a1) -> DefaultUni a
DefaultUniList DefaultUni (Esc a)
ka)

convertTypeBuiltin TypeBuiltinG
TyStringG     = DefaultUni (Esc Text) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Text)
DefaultUniString
convertTypeBuiltin TypeBuiltinG
TyDataG       = DefaultUni (Esc Data) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc Data)
DefaultUniData

-- |Convert well-kinded generated types to Plutus types.
--
-- NOTE: Passes an explicit `TyNameState`, instead of using a State
--       monad, as the type of the `TyNameState` changes throughout
--       the computation.  Alternatively, this could be written using
--       an indexed State monad.
--
-- NOTE: Roman points out that this is more like reader than state,
--       however it doesn't fit easily into this pattern as the
--       function `extTyNameState` is monadic (`MonadQuote`).
convertType
  :: (Show tyname, MonadQuote m, MonadError GenError m)
  => TyNameState tyname -- ^ Type name environment with fresh name stream
  -> Kind ()            -- ^ Kind of type below
  -> TypeG tyname       -- ^ Type to convert
  -> m (Type TyName DefaultUni ())
convertType :: forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns Kind ()
_ (TyVarG tyname
i) =
  Type TyName DefaultUni () -> m (Type TyName DefaultUni ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () (TyNameState tyname -> tyname -> TyName
forall n. TyNameState n -> n -> TyName
tynameOf TyNameState tyname
tns tyname
i))
convertType TyNameState tyname
tns (Type ()
_) (TyFunG TypeG tyname
ty1 TypeG tyname
ty2) =
  ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ())
-> m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty1 m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()) -> m (Type TyName DefaultUni ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty2
convertType TyNameState tyname
tns (Type ()
_) (TyIFixG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2) =
  ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ())
-> m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (Kind () -> Kind ()
toPatFuncKind Kind ()
k) TypeG tyname
ty1 m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()) -> m (Type TyName DefaultUni ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns Kind ()
k TypeG tyname
ty2
convertType TyNameState tyname
tns (Type ()
_) (TyForallG Kind ()
k TypeG (S tyname)
ty) = do
  TyNameState (S tyname)
tns' <- TyNameState tyname -> m (TyNameState (S tyname))
forall (m :: * -> *) n.
MonadQuote m =>
TyNameState n -> m (TyNameState (S n))
extTyNameState TyNameState tyname
tns
  ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () (TyNameState (S tyname) -> S tyname -> TyName
forall n. TyNameState n -> n -> TyName
tynameOf TyNameState (S tyname)
tns' S tyname
forall n. S n
FZ) Kind ()
k (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()) -> m (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState (S tyname)
-> Kind () -> TypeG (S tyname) -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState (S tyname)
tns' (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG (S tyname)
ty
convertType TyNameState tyname
_ Kind ()
_ (TyBuiltinG TypeBuiltinG
tyBuiltin) =
  Type TyName DefaultUni () -> m (Type TyName DefaultUni ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName DefaultUni () -> m (Type TyName DefaultUni ()))
-> Type TyName DefaultUni () -> m (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ () -> SomeTypeIn DefaultUni -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin () (TypeBuiltinG -> SomeTypeIn DefaultUni
convertTypeBuiltin TypeBuiltinG
tyBuiltin)
convertType TyNameState tyname
tns (KindArrow ()
_ Kind ()
k1 Kind ()
k2) (TyLamG TypeG (S tyname)
ty) = do
  TyNameState (S tyname)
tns' <- TyNameState tyname -> m (TyNameState (S tyname))
forall (m :: * -> *) n.
MonadQuote m =>
TyNameState n -> m (TyNameState (S n))
extTyNameState TyNameState tyname
tns
  ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () (TyNameState (S tyname) -> S tyname -> TyName
forall n. TyNameState n -> n -> TyName
tynameOf TyNameState (S tyname)
tns' S tyname
forall n. S n
FZ) Kind ()
k1 (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()) -> m (Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState (S tyname)
-> Kind () -> TypeG (S tyname) -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState (S tyname)
tns' Kind ()
k2 TypeG (S tyname)
ty
convertType TyNameState tyname
tns Kind ()
k2 (TyAppG TypeG tyname
ty1 TypeG tyname
ty2 Kind ()
k1) =
  ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (Type TyName DefaultUni ()
 -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ())
-> m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k1 Kind ()
k2) TypeG tyname
ty1 m (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()) -> m (Type TyName DefaultUni ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns Kind ()
k1 TypeG tyname
ty2
convertType TyNameState tyname
_ Kind ()
k TypeG tyname
ty = GenError -> m (Type TyName DefaultUni ())
forall a. GenError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (GenError -> m (Type TyName DefaultUni ()))
-> GenError -> m (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> TypeG tyname -> GenError
forall tyname. Show tyname => Kind () -> TypeG tyname -> GenError
BadTypeG Kind ()
k TypeG tyname
ty

-- |Convert generated closed types to Plutus types.
convertClosedType
  :: (MonadQuote m, MonadError GenError m)
  => Stream.Stream Text.Text
  -> Kind ()
  -> ClosedTypeG
  -> m (Type TyName DefaultUni ())
convertClosedType :: forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
convertClosedType Stream Text
tynames = TyNameState Z
-> Kind () -> ClosedTypeG -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType (Stream Text -> TyNameState Z
emptyTyNameState Stream Text
tynames)

-- ** Converting terms

-- |Convert (well-typed) generated terms to Plutus terms.
--
-- NOTE: Passes an explicit `TyNameState` and `NameState`, instead of using a
--       State monad, as the type of the `TyNameState` changes throughout the
--       computation. This could be written using an indexed State monad.
--
--       No checking is performed during conversion. The type is given
--       as it contains information needed to fully annotate a `Term`.
--       `Term`, unlike `TermG`, contains all necessary type
--       information to infer the type of the term. It is expected
--       that this function is only called on a well-typed
--       term. Violating this would point to an error in the
--       generator/checker.
convertTermConstant :: TermConstantG -> Some (ValueOf DefaultUni)
convertTermConstant :: TermConstantG -> Some (ValueOf DefaultUni)
convertTermConstant (TmByteStringG ByteString
b) = ValueOf DefaultUni ByteString -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni ByteString -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni ByteString -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc ByteString)
-> ByteString -> ValueOf DefaultUni ByteString
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc ByteString)
DefaultUniByteString ByteString
b
convertTermConstant (TmIntegerG Integer
i)    = ValueOf DefaultUni Integer -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni Integer -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni Integer -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Integer) -> Integer -> ValueOf DefaultUni Integer
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc Integer)
DefaultUniInteger Integer
i
convertTermConstant (TmStringG Text
s)     = ValueOf DefaultUni Text -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni Text -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni Text -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Text) -> Text -> ValueOf DefaultUni Text
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc Text)
DefaultUniString Text
s
convertTermConstant (TmBoolG Bool
b)       = ValueOf DefaultUni Bool -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni Bool -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni Bool -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Bool) -> Bool -> ValueOf DefaultUni Bool
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc Bool)
DefaultUniBool Bool
b
convertTermConstant (TmUnitG ()
u)       = ValueOf DefaultUni () -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni () -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni () -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc ()) -> () -> ValueOf DefaultUni ()
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc ())
DefaultUniUnit ()
u
convertTermConstant (TmDataG Data
d)       = ValueOf DefaultUni Data -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
Some (ValueOf DefaultUni Data -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni Data -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc Data) -> Data -> ValueOf DefaultUni Data
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
ValueOf DefaultUni (Esc Data)
DefaultUniData Data
d

convertTerm
  :: (Show tyname, Show name, MonadQuote m, MonadError GenError m)
  => TyNameState tyname -- ^ Type name environment with fresh name stream
  -> NameState name     -- ^ Name environment with fresh name stream
  -> TypeG tyname       -- ^ Type of term below
  -> TermG tyname name  -- ^ Term to convert
  -> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm :: forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
_tns NameState name
ns TypeG tyname
_ty (VarG name
i) =
  Term TyName Name DefaultUni DefaultFun ()
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () (NameState name -> name -> Name
forall n. NameState n -> n -> Name
nameOf NameState name
ns name
i))
convertTerm TyNameState tyname
tns NameState name
ns (TyFunG TypeG tyname
ty1 TypeG tyname
ty2) (LamAbsG TermG tyname (S name)
tm) = do
  NameState (S name)
ns' <- NameState name -> m (NameState (S name))
forall (m :: * -> *) n.
MonadQuote m =>
NameState n -> m (NameState (S n))
extNameState NameState name
ns
  Type TyName DefaultUni ()
ty1' <- TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty1
  ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () (NameState (S name) -> S name -> Name
forall n. NameState n -> n -> Name
nameOf NameState (S name)
ns' S name
forall n. S n
FZ) Type TyName DefaultUni ()
ty1' (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> NameState (S name)
-> TypeG tyname
-> TermG tyname (S name)
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState (S name)
ns' TypeG tyname
ty2 TermG tyname (S name)
tm
convertTerm TyNameState tyname
tns NameState name
ns TypeG tyname
ty2 (ApplyG TermG tyname name
tm1 TermG tyname name
tm2 TypeG tyname
ty1) =
  ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ()
      -> Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState name
ns (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG TypeG tyname
ty1 TypeG tyname
ty2) TermG tyname name
tm1 m (Term TyName Name DefaultUni DefaultFun ()
   -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState name
ns TypeG tyname
ty1 TermG tyname name
tm2
convertTerm TyNameState tyname
tns NameState name
ns (TyForallG Kind ()
k TypeG (S tyname)
ty) (TyAbsG TermG (S tyname) name
tm) = do
  TyNameState (S tyname)
tns' <- TyNameState tyname -> m (TyNameState (S tyname))
forall (m :: * -> *) n.
MonadQuote m =>
TyNameState n -> m (TyNameState (S n))
extTyNameState TyNameState tyname
tns
  ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () (TyNameState (S tyname) -> S tyname -> TyName
forall n. TyNameState n -> n -> TyName
tynameOf TyNameState (S tyname)
tns' S tyname
forall n. S n
FZ) Kind ()
k (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState (S tyname)
-> NameState name
-> TypeG (S tyname)
-> TermG (S tyname) name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState (S tyname)
tns' NameState name
ns TypeG (S tyname)
ty TermG (S tyname) name
tm
convertTerm TyNameState tyname
tns NameState name
ns TypeG tyname
_ (TyInstG TermG tyname name
tm TypeG (S tyname)
cod TypeG tyname
ty Kind ()
k) =
  ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (Term TyName Name DefaultUni DefaultFun ()
 -> Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni ()
      -> Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState name
ns (Kind () -> TypeG (S tyname) -> TypeG tyname
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG Kind ()
k TypeG (S tyname)
cod) TermG tyname name
tm m (Type TyName DefaultUni ()
   -> Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns Kind ()
k TypeG tyname
ty
convertTerm TyNameState tyname
_tns NameState name
_ns TypeG tyname
_ (ConstantG TermConstantG
c) =
  Term TyName Name DefaultUni DefaultFun ()
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term TyName Name DefaultUni DefaultFun ()
 -> m (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ ()
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant () (TermConstantG -> Some (ValueOf DefaultUni)
convertTermConstant TermConstantG
c)
convertTerm TyNameState tyname
_tns NameState name
_ns TypeG tyname
_ (BuiltinG DefaultFun
b) = Term TyName Name DefaultUni DefaultFun ()
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term TyName Name DefaultUni DefaultFun ()
 -> m (Term TyName Name DefaultUni DefaultFun ()))
-> Term TyName Name DefaultUni DefaultFun ()
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ () -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin () DefaultFun
b
convertTerm TyNameState tyname
tns NameState name
ns (TyIFixG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2) (WrapG TermG tyname name
tm) = ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap ()
    (Type TyName DefaultUni ()
 -> Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni ())
-> m (Type TyName DefaultUni ()
      -> Term TyName Name DefaultUni DefaultFun ()
      -> Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (Kind () -> Kind ()
toPatFuncKind Kind ()
k) TypeG tyname
ty1
    m (Type TyName DefaultUni ()
   -> Term TyName Name DefaultUni DefaultFun ()
   -> Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni ())
-> m (Term TyName Name DefaultUni DefaultFun ()
      -> Term TyName Name DefaultUni DefaultFun ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns Kind ()
k TypeG tyname
ty2
    m (Term TyName Name DefaultUni DefaultFun ()
   -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState name
ns (TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n
normalizeTypeG TypeG tyname
ty') TermG tyname name
tm
  where
    -- Γ ⊢ A · ƛ (μ (weaken A) (` Z)) · B
    ty' :: TypeG tyname
ty' = TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG TypeG tyname
ty1 (TypeG (S tyname) -> TypeG tyname
forall n. TypeG (S n) -> TypeG n
TyLamG (TypeG (S tyname) -> Kind () -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (TypeG tyname -> TypeG (S tyname)
forall m. TypeG m -> TypeG (S m)
weakenTy TypeG tyname
ty1) Kind ()
k (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ))) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))) TypeG tyname
ty2 Kind ()
k
convertTerm TyNameState tyname
tns NameState name
ns TypeG tyname
_ (UnWrapG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2 TermG tyname name
tm) = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm TyNameState tyname
tns NameState name
ns (TypeG tyname -> Kind () -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2) TermG tyname name
tm
convertTerm TyNameState tyname
tns NameState name
_ns TypeG tyname
_ (ErrorG TypeG tyname
ty) = ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error () (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> m (Type TyName DefaultUni ())
-> m (Term TyName Name DefaultUni DefaultFun ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
forall tyname (m :: * -> *).
(Show tyname, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> Kind () -> TypeG tyname -> m (Type TyName DefaultUni ())
convertType TyNameState tyname
tns (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty
convertTerm TyNameState tyname
_ NameState name
_ TypeG tyname
ty TermG tyname name
tm = GenError -> m (Term TyName Name DefaultUni DefaultFun ())
forall a. GenError -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (GenError -> m (Term TyName Name DefaultUni DefaultFun ()))
-> GenError -> m (Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TypeG tyname -> TermG tyname name -> GenError
forall tyname name.
(Show tyname, Show name) =>
TypeG tyname -> TermG tyname name -> GenError
BadTermG TypeG tyname
ty TermG tyname name
tm

-- |Convert generated closed terms to Plutus terms.
convertClosedTerm
  :: (MonadQuote m, MonadError GenError m)
  => Stream.Stream Text.Text
  -> Stream.Stream Text.Text
  -> ClosedTypeG
  -> ClosedTermG
  -> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm :: forall (m :: * -> *).
(MonadQuote m, MonadError GenError m) =>
Stream Text
-> Stream Text
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
convertClosedTerm Stream Text
tynames Stream Text
names = TyNameState Z
-> NameState Z
-> ClosedTypeG
-> ClosedTermG
-> m (Term TyName Name DefaultUni DefaultFun ())
forall tyname name (m :: * -> *).
(Show tyname, Show name, MonadQuote m, MonadError GenError m) =>
TyNameState tyname
-> NameState name
-> TypeG tyname
-> TermG tyname name
-> m (Term TyName Name DefaultUni DefaultFun ())
convertTerm (Stream Text -> TyNameState Z
emptyTyNameState Stream Text
tynames) (Stream Text -> NameState Z
emptyNameState Stream Text
names)


-- * Checking

class Check t a where
  check :: t -> a -> Cool


-- ** Kind checking

-- |Kind check builtin types.
--
-- NOTE: If we make |checkTypeBuiltinG| non-strict in its second argument,
--       lazy-search will only ever return one of the various builtin types.
--       Perhaps this is preferable?
--
instance Check (Kind ()) TypeBuiltinG where
  check :: Kind () -> TypeBuiltinG -> Cool
check (Type ()
_) TypeBuiltinG
TyByteStringG = Cool
true
  check (Type ()
_) TypeBuiltinG
TyIntegerG    = Cool
true
  check (Type ()
_) TypeBuiltinG
TyBoolG       = Cool
true
  check (Type ()
_) TypeBuiltinG
TyUnitG       = Cool
true
  check (Type ()
_) (TyListG TypeBuiltinG
_a)  = Cool
false -- check (Type ()) a
  check (Type ()
_) TypeBuiltinG
TyStringG     = Cool
true
  check (Type ()
_) TypeBuiltinG
TyDataG       = Cool
true
  check Kind ()
_        TypeBuiltinG
_             = Cool
false

-- |Kind check types.
checkKindG :: KCS n -> Kind () -> TypeG n -> Cool
checkKindG :: forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs Kind ()
k (TyVarG n
i)
  = Cool
varKindOk
  where
    varKindOk :: Cool
varKindOk = Bool -> Cool
forall b. Coolean b => b -> Cool
toCool (Bool -> Cool) -> Bool -> Cool
forall a b. (a -> b) -> a -> b
$ Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== KCS n -> n -> Kind ()
forall tyname. KCS tyname -> tyname -> Kind ()
kindOf KCS n
kcs n
i

checkKindG KCS n
kcs (Type ()
_) (TyFunG TypeG n
ty1 TypeG n
ty2)
  = Cool
ty1KindOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
ty2KindOk
  where
    ty1KindOk :: Cool
ty1KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG n
ty1
    ty2KindOk :: Cool
ty2KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG n
ty2

checkKindG KCS n
kcs (Type ()
_) (TyIFixG TypeG n
ty1 Kind ()
k TypeG n
ty2)
  = Cool
ty1KindOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
ty2KindOk
  where
    ty1Kind :: Kind ()
ty1Kind   = Kind () -> Kind ()
toPatFuncKind Kind ()
k
    ty1KindOk :: Cool
ty1KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs Kind ()
ty1Kind TypeG n
ty1
    ty2KindOk :: Cool
ty2KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs Kind ()
k TypeG n
ty2

checkKindG KCS n
kcs (Type ()
_) (TyForallG Kind ()
k TypeG (S n)
body)
  = Cool
tyKindOk
  where
    tyKindOk :: Cool
tyKindOk = KCS (S n) -> Kind () -> TypeG (S n) -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG (Kind () -> KCS n -> KCS (S n)
forall tyname. Kind () -> KCS tyname -> KCS (S tyname)
extKCS Kind ()
k KCS n
kcs) (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG (S n)
body

checkKindG KCS n
_ Kind ()
k (TyBuiltinG TypeBuiltinG
tyBuiltin)
  = Cool
tyBuiltinKindOk
  where
    tyBuiltinKindOk :: Cool
tyBuiltinKindOk = Kind () -> TypeBuiltinG -> Cool
forall t a. Check t a => t -> a -> Cool
check Kind ()
k TypeBuiltinG
tyBuiltin

checkKindG KCS n
kcs (KindArrow () Kind ()
k1 Kind ()
k2) (TyLamG TypeG (S n)
body)
  = Cool
bodyKindOk
  where
    bodyKindOk :: Cool
bodyKindOk = KCS (S n) -> Kind () -> TypeG (S n) -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG (Kind () -> KCS n -> KCS (S n)
forall tyname. Kind () -> KCS tyname -> KCS (S tyname)
extKCS Kind ()
k1 KCS n
kcs) Kind ()
k2 TypeG (S n)
body

checkKindG KCS n
kcs Kind ()
k' (TyAppG TypeG n
ty1 TypeG n
ty2 Kind ()
k)
  = Cool
ty1KindOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
ty2KindOk
  where
    ty1Kind :: Kind ()
ty1Kind   = () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k Kind ()
k'
    ty1KindOk :: Cool
ty1KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs Kind ()
ty1Kind TypeG n
ty1
    ty2KindOk :: Cool
ty2KindOk = KCS n -> Kind () -> TypeG n -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS n
kcs Kind ()
k TypeG n
ty2

checkKindG KCS n
_ Kind ()
_ TypeG n
_ = Cool
false


instance Check (Kind ()) ClosedTypeG where
  check :: Kind () -> ClosedTypeG -> Cool
check = KCS Z -> Kind () -> ClosedTypeG -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS Z
emptyKCS


instance Check (Kind ()) (Normalized ClosedTypeG) where
  check :: Kind () -> Normalized ClosedTypeG -> Cool
check Kind ()
k Normalized ClosedTypeG
ty = Kind () -> ClosedTypeG -> Cool
forall t a. Check t a => t -> a -> Cool
check Kind ()
k (Normalized ClosedTypeG -> ClosedTypeG
forall a. Normalized a -> a
unNormalized Normalized ClosedTypeG
ty)


-- ** Kind checking state

newtype KCS tyname = KCS{ forall tyname. KCS tyname -> tyname -> Kind ()
kindOf :: tyname -> Kind () }

emptyKCS :: KCS Z
emptyKCS :: KCS Z
emptyKCS = KCS{ kindOf :: Z -> Kind ()
kindOf = Z -> Kind ()
forall a. Z -> a
fromZ }

extKCS :: forall tyname. Kind () -> KCS tyname -> KCS (S tyname)
extKCS :: forall tyname. Kind () -> KCS tyname -> KCS (S tyname)
extKCS Kind ()
k KCS{tyname -> Kind ()
kindOf :: forall tyname. KCS tyname -> tyname -> Kind ()
kindOf :: tyname -> Kind ()
..} = KCS{ kindOf :: S tyname -> Kind ()
kindOf = S tyname -> Kind ()
kindOf' }
  where
    kindOf' :: S tyname -> Kind ()
    kindOf' :: S tyname -> Kind ()
kindOf' S tyname
FZ     = Kind ()
k
    kindOf' (FS tyname
i) = tyname -> Kind ()
kindOf tyname
i


-- ** Type checking

instance Check (TypeG n) TermConstantG where
  check :: TypeG n -> TermConstantG -> Cool
check (TyBuiltinG TypeBuiltinG
TyByteStringG) (TmByteStringG ByteString
_) = Cool
true
  check (TyBuiltinG TypeBuiltinG
TyIntegerG   ) (TmIntegerG    Integer
_) = Cool
true
  check (TyBuiltinG TypeBuiltinG
TyBoolG      ) (TmBoolG       Bool
_) = Cool
true
  check (TyBuiltinG TypeBuiltinG
TyUnitG      ) (TmUnitG       ()
_) = Cool
true
  check (TyBuiltinG TypeBuiltinG
TyStringG    ) (TmStringG     Text
_) = Cool
true
  check (TyBuiltinG TypeBuiltinG
TyDataG      ) (TmDataG     Data
_)   = Cool
true
  check TypeG n
_                          TermConstantG
_                 = Cool
false


-- | DEPRECATED: No Need to Update for a new Builtin.
-- NEAT tests are useless for builtins, see https://github.com/IntersectMBO/plutus/issues/6075
defaultFunTypes :: Ord tyname => Map.Map (TypeG tyname) [DefaultFun]
defaultFunTypes :: forall tyname. Ord tyname => Map (TypeG tyname) [DefaultFun]
defaultFunTypes = [(TypeG tyname, [DefaultFun])] -> Map (TypeG tyname) [DefaultFun]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG))
                   ,[DefaultFun
AddInteger,DefaultFun
SubtractInteger,DefaultFun
MultiplyInteger,DefaultFun
DivideInteger,DefaultFun
QuotientInteger,DefaultFun
RemainderInteger,DefaultFun
ModInteger])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyBoolG))
                   ,[DefaultFun
LessThanInteger,DefaultFun
LessThanEqualsInteger,DefaultFun
EqualsInteger])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG))
                   ,[DefaultFun
AppendByteString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG))
                   ,[DefaultFun
ConsByteString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG)))
                   ,[DefaultFun
SliceByteString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG)
                   ,[DefaultFun
LengthOfByteString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG))
                   ,[DefaultFun
IndexByteString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG)
                   ,[DefaultFun
Sha2_256,DefaultFun
Sha3_256,DefaultFun
Blake2b_224,DefaultFun
Blake2b_256,DefaultFun
Keccak_256,DefaultFun
Ripemd_160])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyBoolG)))
                   ,[DefaultFun
VerifyEd25519Signature])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyBoolG))
                   ,[DefaultFun
EqualsByteString,DefaultFun
LessThanByteString,DefaultFun
LessThanEqualsByteString])
                  ,(Kind () -> TypeG (S tyname) -> TypeG tyname
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (TypeG (S tyname) -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG (S tyname)
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyBoolG) (TypeG (S tyname) -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ) (TypeG (S tyname) -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ) (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ))))
                   ,[DefaultFun
IfThenElse])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG))
                   ,[DefaultFun
AppendString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyBoolG))
                   ,[DefaultFun
EqualsString])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG)
                   ,[DefaultFun
EncodeUtf8])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG)
                   ,[DefaultFun
DecodeUtf8])
                  ,(Kind () -> TypeG (S tyname) -> TypeG tyname
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (TypeG (S tyname) -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG (S tyname)
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyStringG) (TypeG (S tyname) -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ) (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ)))
                   ,[DefaultFun
Trace])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyDataG)
                  ,[DefaultFun
IData])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyDataG)
                  ,[DefaultFun
BData])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyDataG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyIntegerG)
                  ,[DefaultFun
UnIData])
                  ,(TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyDataG) (TypeBuiltinG -> TypeG tyname
forall n. TypeBuiltinG -> TypeG n
TyBuiltinG TypeBuiltinG
TyByteStringG)
                  ,[DefaultFun
UnBData, DefaultFun
SerialiseData])
                  ]

instance Ord tyname => Check (TypeG tyname) DefaultFun where
  check :: TypeG tyname -> DefaultFun -> Cool
check TypeG tyname
ty DefaultFun
b = case TypeG tyname
-> Map (TypeG tyname) [DefaultFun] -> Maybe [DefaultFun]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeG tyname
ty Map (TypeG tyname) [DefaultFun]
forall tyname. Ord tyname => Map (TypeG tyname) [DefaultFun]
defaultFunTypes of
    Just [DefaultFun]
bs -> Bool -> Cool
forall b. Coolean b => b -> Cool
toCool (Bool -> Cool) -> Bool -> Cool
forall a b. (a -> b) -> a -> b
$ DefaultFun -> [DefaultFun] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem DefaultFun
b [DefaultFun]
bs
    Maybe [DefaultFun]
Nothing -> Cool
false

-- it's not clear to me whether this function should insist that some
-- types are in normal form...
checkTypeG
  :: Ord tyname
  => KCS tyname
  -> TCS tyname name
  -> TypeG tyname
  -> TermG tyname name
  -> Cool
checkTypeG :: forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
_ TCS tyname name
tcs TypeG tyname
ty (VarG name
i)
  = Cool
varTypeOk
  where
    varTypeOk :: Cool
varTypeOk = Bool -> Cool
forall b. Coolean b => b -> Cool
toCool (Bool -> Cool) -> Bool -> Cool
forall a b. (a -> b) -> a -> b
$ TypeG tyname
ty TypeG tyname -> TypeG tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TCS tyname name -> name -> TypeG tyname
forall tyname name. TCS tyname name -> name -> TypeG tyname
typeOf TCS tyname name
tcs name
i

checkTypeG KCS tyname
kcs TCS tyname name
tcs (TyForallG Kind ()
k TypeG (S tyname)
ty) (TyAbsG TermG (S tyname) name
tm)
  = Cool
tmTypeOk
  where
    tmTypeOk :: Cool
tmTypeOk = KCS (S tyname)
-> TCS (S tyname) name
-> TypeG (S tyname)
-> TermG (S tyname) name
-> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG (Kind () -> KCS tyname -> KCS (S tyname)
forall tyname. Kind () -> KCS tyname -> KCS (S tyname)
extKCS Kind ()
k KCS tyname
kcs) ((tyname -> S tyname) -> TCS tyname name -> TCS (S tyname) name
forall tyname tyname' name.
(tyname -> tyname') -> TCS tyname name -> TCS tyname' name
firstTCS tyname -> S tyname
forall n. n -> S n
FS TCS tyname name
tcs) TypeG (S tyname)
ty TermG (S tyname) name
tm

checkTypeG KCS tyname
kcs TCS tyname name
tcs (TyFunG TypeG tyname
ty1 TypeG tyname
ty2) (LamAbsG TermG tyname (S name)
tm)
  = Cool
tyKindOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
tmTypeOk
  where
    tyKindOk :: Cool
tyKindOk = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty1
    tmTypeOk :: Cool
tmTypeOk = KCS tyname
-> TCS tyname (S name)
-> TypeG tyname
-> TermG tyname (S name)
-> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs (TypeG tyname -> TCS tyname name -> TCS tyname (S name)
forall tyname name.
TypeG tyname -> TCS tyname name -> TCS tyname (S name)
extTCS TypeG tyname
ty1 TCS tyname name
tcs) TypeG tyname
ty2 TermG tyname (S name)
tm

checkTypeG KCS tyname
kcs TCS tyname name
tcs TypeG tyname
ty2 (ApplyG TermG tyname name
tm1 TermG tyname name
tm2 TypeG tyname
ty1)
  = Cool
tm1TypeOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
tm2TypeOk
  where
    tm1TypeOk :: Cool
tm1TypeOk = KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs TCS tyname name
tcs (TypeG tyname -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG TypeG tyname
ty1 TypeG tyname
ty2) TermG tyname name
tm1
    tm2TypeOk :: Cool
tm2TypeOk = KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs TCS tyname name
tcs TypeG tyname
ty1 TermG tyname name
tm2

checkTypeG KCS tyname
kcs TCS tyname name
tcs TypeG tyname
vTy (TyInstG TermG tyname name
tm TypeG (S tyname)
vCod TypeG tyname
ty Kind ()
k)
  = Cool
tmTypeOk Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
tyKindOk Cool -> Bool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Bool
tyOk
  where
    tmTypeOk :: Cool
tmTypeOk = KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs TCS tyname name
tcs (Kind () -> TypeG (S tyname) -> TypeG tyname
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG Kind ()
k TypeG (S tyname)
vCod) TermG tyname name
tm
    tyKindOk :: Cool
tyKindOk = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs Kind ()
k TypeG tyname
ty
    tyOk :: Bool
tyOk = TypeG tyname
vTy TypeG tyname -> TypeG tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n
normalizeTypeG (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG (S tyname) -> TypeG tyname
forall n. TypeG (S n) -> TypeG n
TyLamG TypeG (S tyname)
vCod) TypeG tyname
ty Kind ()
k)
checkTypeG KCS tyname
_kcs TCS tyname name
_tcs TypeG tyname
tc (ConstantG TermConstantG
c) = TypeG tyname -> TermConstantG -> Cool
forall t a. Check t a => t -> a -> Cool
check TypeG tyname
tc TermConstantG
c
checkTypeG KCS tyname
kcs TCS tyname name
tcs (TyIFixG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2) (WrapG TermG tyname name
tm) = Cool
ty1Ok Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
ty2Ok Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
tmOk
  where
    ty1Ok :: Cool
ty1Ok = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs (Kind () -> Kind ()
toPatFuncKind Kind ()
k) TypeG tyname
ty1
    ty2Ok :: Cool
ty2Ok = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs Kind ()
k TypeG tyname
ty2
    tmTy :: TypeG tyname
tmTy  = TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG TypeG tyname
ty1 (TypeG (S tyname) -> TypeG tyname
forall n. TypeG (S n) -> TypeG n
TyLamG (TypeG (S tyname) -> Kind () -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (TypeG tyname -> TypeG (S tyname)
forall m. TypeG m -> TypeG (S m)
weakenTy TypeG tyname
ty1) Kind ()
k (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ))) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))) TypeG tyname
ty2 Kind ()
k
    tmOk :: Cool
tmOk  = KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs TCS tyname name
tcs (TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n
normalizeTypeG TypeG tyname
tmTy) TermG tyname name
tm
checkTypeG KCS tyname
kcs TCS tyname name
tcs TypeG tyname
vTy (UnWrapG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2 TermG tyname name
tm) = Cool
ty1Ok Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
ty2Ok Cool -> Cool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Cool
tmOk Cool -> Bool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Bool
vTyOk
  where
    ty1Ok :: Cool
ty1Ok = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs (Kind () -> Kind ()
toPatFuncKind Kind ()
k) TypeG tyname
ty1
    ty2Ok :: Cool
ty2Ok = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs Kind ()
k TypeG tyname
ty2
    tmOk :: Cool
tmOk  = KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS tyname
kcs TCS tyname name
tcs (TypeG tyname -> Kind () -> TypeG tyname -> TypeG tyname
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG TypeG tyname
ty1 Kind ()
k TypeG tyname
ty2) TermG tyname name
tm
    vTyOk :: Bool
vTyOk = TypeG tyname
vTy TypeG tyname -> TypeG tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n
normalizeTypeG (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG tyname -> TypeG tyname -> Kind () -> TypeG tyname
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG TypeG tyname
ty1 (TypeG (S tyname) -> TypeG tyname
forall n. TypeG (S n) -> TypeG n
TyLamG (TypeG (S tyname) -> Kind () -> TypeG (S tyname) -> TypeG (S tyname)
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (TypeG tyname -> TypeG (S tyname)
forall m. TypeG m -> TypeG (S m)
weakenTy TypeG tyname
ty1) Kind ()
k (S tyname -> TypeG (S tyname)
forall n. n -> TypeG n
TyVarG S tyname
forall n. S n
FZ))) (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
k (() -> Kind ()
forall ann. ann -> Kind ann
Type ()))) TypeG tyname
ty2 Kind ()
k)
checkTypeG KCS tyname
kcs TCS tyname name
_tcs TypeG tyname
vTy (ErrorG TypeG tyname
ty) = Cool
tyKindOk Cool -> Bool -> Cool
forall a b. (Coolean a, Coolean b) => a -> b -> Cool
&&& Bool
tyOk
  where
    tyKindOk :: Cool
tyKindOk = KCS tyname -> Kind () -> TypeG tyname -> Cool
forall n. KCS n -> Kind () -> TypeG n -> Cool
checkKindG KCS tyname
kcs (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) TypeG tyname
ty
    tyOk :: Bool
tyOk = TypeG tyname
vTy TypeG tyname -> TypeG tyname -> Bool
forall a. Eq a => a -> a -> Bool
== TypeG tyname -> TypeG tyname
forall n. TypeG n -> TypeG n
normalizeTypeG TypeG tyname
ty
checkTypeG KCS tyname
_kcs TCS tyname name
_tcs TypeG tyname
vTy (BuiltinG DefaultFun
b) = TypeG tyname -> DefaultFun -> Cool
forall t a. Check t a => t -> a -> Cool
check TypeG tyname
vTy DefaultFun
b
checkTypeG KCS tyname
_ TCS tyname name
_ TypeG tyname
_ TermG tyname name
_ = Cool
false

instance Check ClosedTypeG ClosedTermG where
  check :: ClosedTypeG -> ClosedTermG -> Cool
check = KCS Z -> TCS Z Z -> ClosedTypeG -> ClosedTermG -> Cool
forall tyname name.
Ord tyname =>
KCS tyname
-> TCS tyname name -> TypeG tyname -> TermG tyname name -> Cool
checkTypeG KCS Z
emptyKCS TCS Z Z
forall tyname. TCS tyname Z
emptyTCS


-- ** Type checking state

newtype TCS tyname name = TCS{ forall tyname name. TCS tyname name -> name -> TypeG tyname
typeOf :: name -> TypeG tyname }

emptyTCS :: TCS tyname Z
emptyTCS :: forall tyname. TCS tyname Z
emptyTCS = TCS{ typeOf :: Z -> TypeG tyname
typeOf = Z -> TypeG tyname
forall a. Z -> a
fromZ }

extTCS :: forall tyname name. TypeG tyname -> TCS tyname name -> TCS tyname (S name)
extTCS :: forall tyname name.
TypeG tyname -> TCS tyname name -> TCS tyname (S name)
extTCS TypeG tyname
ty TCS{name -> TypeG tyname
typeOf :: forall tyname name. TCS tyname name -> name -> TypeG tyname
typeOf :: name -> TypeG tyname
..} = TCS{ typeOf :: S name -> TypeG tyname
typeOf = S name -> TypeG tyname
typeOf' }
  where
    typeOf' :: S name -> TypeG tyname
    typeOf' :: S name -> TypeG tyname
typeOf' S name
FZ     = TypeG tyname
ty
    typeOf' (FS name
i) = name -> TypeG tyname
typeOf name
i

firstTCS :: (tyname -> tyname') -> TCS tyname name -> TCS tyname' name
firstTCS :: forall tyname tyname' name.
(tyname -> tyname') -> TCS tyname name -> TCS tyname' name
firstTCS tyname -> tyname'
f TCS tyname name
tcs = TCS{ typeOf :: name -> TypeG tyname'
typeOf = (tyname -> tyname') -> TypeG tyname -> TypeG tyname'
forall a b. (a -> b) -> TypeG a -> TypeG b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap tyname -> tyname'
f (TypeG tyname -> TypeG tyname')
-> (name -> TypeG tyname) -> name -> TypeG tyname'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCS tyname name -> name -> TypeG tyname
forall tyname name. TCS tyname name -> name -> TypeG tyname
typeOf TCS tyname name
tcs }


-- * Normalisation

weakenTy :: TypeG m -> TypeG (S m)
weakenTy :: forall m. TypeG m -> TypeG (S m)
weakenTy TypeG m
ty = (m -> TypeG (S m)) -> TypeG m -> TypeG (S m)
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub (S m -> TypeG (S m)
forall n. n -> TypeG n
TyVarG (S m -> TypeG (S m)) -> (m -> S m) -> m -> TypeG (S m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> S m
forall n. n -> S n
FS) TypeG m
ty

-- |Reduce a generated type by a single step, or fail.
stepTypeG :: TypeG n -> Maybe (TypeG n)
stepTypeG :: forall n. TypeG n -> Maybe (TypeG n)
stepTypeG (TyVarG n
_)                  = Maybe (TypeG n)
forall a. Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
stepTypeG (TyFunG TypeG n
ty1 TypeG n
ty2)            = (TypeG n -> TypeG n -> TypeG n
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeG n -> TypeG n -> TypeG n)
-> Maybe (TypeG n) -> Maybe (TypeG n -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty1 Maybe (TypeG n -> TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty2)
                                    Maybe (TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (TypeG n -> TypeG n -> TypeG n
forall n. TypeG n -> TypeG n -> TypeG n
TyFunG (TypeG n -> TypeG n -> TypeG n)
-> Maybe (TypeG n) -> Maybe (TypeG n -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty1 Maybe (TypeG n -> TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty2)
stepTypeG (TyIFixG TypeG n
ty1 Kind ()
k TypeG n
ty2)         = (TypeG n -> Kind () -> TypeG n -> TypeG n
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (TypeG n -> Kind () -> TypeG n -> TypeG n)
-> Maybe (TypeG n) -> Maybe (Kind () -> TypeG n -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty1 Maybe (Kind () -> TypeG n -> TypeG n)
-> Maybe (Kind ()) -> Maybe (TypeG n -> TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
k Maybe (TypeG n -> TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty2)
                                    Maybe (TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (TypeG n -> Kind () -> TypeG n -> TypeG n
forall n. TypeG n -> Kind () -> TypeG n -> TypeG n
TyIFixG (TypeG n -> Kind () -> TypeG n -> TypeG n)
-> Maybe (TypeG n) -> Maybe (Kind () -> TypeG n -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty1 Maybe (Kind () -> TypeG n -> TypeG n)
-> Maybe (Kind ()) -> Maybe (TypeG n -> TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
k Maybe (TypeG n -> TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty2)
stepTypeG (TyForallG Kind ()
k TypeG (S n)
ty)            = Kind () -> TypeG (S n) -> TypeG n
forall n. Kind () -> TypeG (S n) -> TypeG n
TyForallG (Kind () -> TypeG (S n) -> TypeG n)
-> Maybe (Kind ()) -> Maybe (TypeG (S n) -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
k Maybe (TypeG (S n) -> TypeG n)
-> Maybe (TypeG (S n)) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG (S n) -> Maybe (TypeG (S n))
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG (S n)
ty
stepTypeG (TyBuiltinG TypeBuiltinG
_)              = Maybe (TypeG n)
forall a. Maybe a
forall (f :: * -> *) a. Alternative f => f a
empty
stepTypeG (TyLamG TypeG (S n)
ty)                 = TypeG (S n) -> TypeG n
forall n. TypeG (S n) -> TypeG n
TyLamG (TypeG (S n) -> TypeG n) -> Maybe (TypeG (S n)) -> Maybe (TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG (S n) -> Maybe (TypeG (S n))
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG (S n)
ty
stepTypeG (TyAppG (TyLamG TypeG (S n)
ty1) TypeG n
ty2 Kind ()
_) = TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((S n -> TypeG n) -> TypeG (S n) -> TypeG n
forall n m. (n -> TypeG m) -> TypeG n -> TypeG m
sub (\case S n
FZ -> TypeG n
ty2; FS n
i -> n -> TypeG n
forall n. n -> TypeG n
TyVarG n
i) TypeG (S n)
ty1)
stepTypeG (TyAppG TypeG n
ty1 TypeG n
ty2 Kind ()
k)          = (TypeG n -> TypeG n -> Kind () -> TypeG n
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG n -> TypeG n -> Kind () -> TypeG n)
-> Maybe (TypeG n) -> Maybe (TypeG n -> Kind () -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty1 Maybe (TypeG n -> Kind () -> TypeG n)
-> Maybe (TypeG n) -> Maybe (Kind () -> TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty2 Maybe (Kind () -> TypeG n) -> Maybe (Kind ()) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
k)
                                    Maybe (TypeG n) -> Maybe (TypeG n) -> Maybe (TypeG n)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (TypeG n -> TypeG n -> Kind () -> TypeG n
forall n. TypeG n -> TypeG n -> Kind () -> TypeG n
TyAppG (TypeG n -> TypeG n -> Kind () -> TypeG n)
-> Maybe (TypeG n) -> Maybe (TypeG n -> Kind () -> TypeG n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeG n -> Maybe (TypeG n)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeG n
ty1 Maybe (TypeG n -> Kind () -> TypeG n)
-> Maybe (TypeG n) -> Maybe (Kind () -> TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty2 Maybe (Kind () -> TypeG n) -> Maybe (Kind ()) -> Maybe (TypeG n)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Kind () -> Maybe (Kind ())
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind ()
k)

-- |Normalise a generated type.
normalizeTypeG :: TypeG n -> TypeG n
normalizeTypeG :: forall n. TypeG n -> TypeG n
normalizeTypeG TypeG n
ty = TypeG n -> (TypeG n -> TypeG n) -> Maybe (TypeG n) -> TypeG n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TypeG n
ty TypeG n -> TypeG n
forall n. TypeG n -> TypeG n
normalizeTypeG (TypeG n -> Maybe (TypeG n)
forall n. TypeG n -> Maybe (TypeG n)
stepTypeG TypeG n
ty)

-- * Errors

-- NOTE: The errors we need to handle in property-based testing are
--       when the generator generates garbage (which shouldn't happen).

data GenError
  = forall tyname. Show tyname => BadTypeG (Kind ()) (TypeG tyname)
  | forall tyname name. (Show tyname, Show name) => BadTermG (TypeG tyname) (TermG tyname name)

instance Show GenError where
  show :: GenError -> String
show (BadTypeG Kind ()
k TypeG tyname
ty) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Test generation error: convert type %s at kind %s" (TypeG tyname -> String
forall a. Show a => a -> String
show TypeG tyname
ty) (Kind () -> String
forall a. Show a => a -> String
show Kind ()
k)
  show (BadTermG TypeG tyname
ty TermG tyname name
tm) =
    String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"Test generation error: convert term %s at type %s" (TermG tyname name -> String
forall a. Show a => a -> String
show TermG tyname name
tm) (TypeG tyname -> String
forall a. Show a => a -> String
show TypeG tyname
ty)