{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}

-- | Types and type checking
module Language.Bitcoin.Miniscript.Types (
    BaseType (..),
    ModField (..),
    MiniscriptType (..),
    boolType,
    numberType,
    bytesType,
    keyDescriptorType,
    typeCheckMiniscript,
    MiniscriptTypeError (..),
) where

import Control.Monad (unless)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Except (Except, runExcept, throwE)
import Control.Monad.Trans.Reader (ReaderT, local, runReaderT)
import Data.Bool (bool)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Text (Text)

import Language.Bitcoin.Miniscript.Syntax (
    Miniscript (..),
    Value (..),
 )
import Language.Bitcoin.Utils (requiredContextValue)

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}

data BaseType
    = -- | Base expression
      TypeB
    | -- | Verify expression
      TypeV
    | -- | Key expression
      TypeK
    | -- | Wrapped expression
      TypeW
    | -- | Number expression
      TypeNumber
    | -- | Bytes expression
      TypeBytes
    | -- | Key descriptor type
      TypeKeyDesc
    deriving (BaseType -> BaseType -> Bool
(BaseType -> BaseType -> Bool)
-> (BaseType -> BaseType -> Bool) -> Eq BaseType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BaseType -> BaseType -> Bool
$c/= :: BaseType -> BaseType -> Bool
== :: BaseType -> BaseType -> Bool
$c== :: BaseType -> BaseType -> Bool
Eq, Int -> BaseType -> ShowS
[BaseType] -> ShowS
BaseType -> String
(Int -> BaseType -> ShowS)
-> (BaseType -> String) -> ([BaseType] -> ShowS) -> Show BaseType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BaseType] -> ShowS
$cshowList :: [BaseType] -> ShowS
show :: BaseType -> String
$cshow :: BaseType -> String
showsPrec :: Int -> BaseType -> ShowS
$cshowsPrec :: Int -> BaseType -> ShowS
Show)

notW :: BaseType -> Bool
notW :: BaseType -> Bool
notW = (BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
/= BaseType
TypeW)

-- | Type modifications that imply additional properties of the expression
data ModField = ModField
    { -- | Consumes exactly 0 stack elements
      ModField -> Bool
modZ :: Bool
    , -- | One-arg: this expression always consumes exactly 1 stack element.
      ModField -> Bool
modO :: Bool
    , -- | Nonzero: this expression always consumes at least 1 stack element, no
      -- satisfaction for this expression requires the top input stack element to
      -- be zero.
      ModField -> Bool
modN :: Bool
    , -- | Dissatisfiable: a dissatisfaction for this expression can
      -- unconditionally be constructed.
      ModField -> Bool
modD :: Bool
    , -- | Unit: when satisfied put exactly 1 on the stack
      ModField -> Bool
modU :: Bool
    }
    deriving (ModField -> ModField -> Bool
(ModField -> ModField -> Bool)
-> (ModField -> ModField -> Bool) -> Eq ModField
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModField -> ModField -> Bool
$c/= :: ModField -> ModField -> Bool
== :: ModField -> ModField -> Bool
$c== :: ModField -> ModField -> Bool
Eq, Int -> ModField -> ShowS
[ModField] -> ShowS
ModField -> String
(Int -> ModField -> ShowS)
-> (ModField -> String) -> ([ModField] -> ShowS) -> Show ModField
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModField] -> ShowS
$cshowList :: [ModField] -> ShowS
show :: ModField -> String
$cshow :: ModField -> String
showsPrec :: Int -> ModField -> ShowS
$cshowsPrec :: Int -> ModField -> ShowS
Show)

data MiniscriptType = MiniscriptType
    { MiniscriptType -> BaseType
baseType :: BaseType
    , MiniscriptType -> ModField
modifiers :: ModField
    }
    deriving (MiniscriptType -> MiniscriptType -> Bool
(MiniscriptType -> MiniscriptType -> Bool)
-> (MiniscriptType -> MiniscriptType -> Bool) -> Eq MiniscriptType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MiniscriptType -> MiniscriptType -> Bool
$c/= :: MiniscriptType -> MiniscriptType -> Bool
== :: MiniscriptType -> MiniscriptType -> Bool
$c== :: MiniscriptType -> MiniscriptType -> Bool
Eq, Int -> MiniscriptType -> ShowS
[MiniscriptType] -> ShowS
MiniscriptType -> String
(Int -> MiniscriptType -> ShowS)
-> (MiniscriptType -> String)
-> ([MiniscriptType] -> ShowS)
-> Show MiniscriptType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MiniscriptType] -> ShowS
$cshowList :: [MiniscriptType] -> ShowS
show :: MiniscriptType -> String
$cshow :: MiniscriptType -> String
showsPrec :: Int -> MiniscriptType -> ShowS
$cshowsPrec :: Int -> MiniscriptType -> ShowS
Show)

emptyModField :: ModField
emptyModField :: ModField
emptyModField = Bool -> Bool -> Bool -> Bool -> Bool -> ModField
ModField Bool
False Bool
False Bool
False Bool
False Bool
False

boolType :: Bool -> MiniscriptType
boolType :: Bool -> MiniscriptType
boolType = BaseType -> ModField -> MiniscriptType
MiniscriptType BaseType
TypeB (ModField -> MiniscriptType)
-> (Bool -> ModField) -> Bool -> MiniscriptType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModField -> ModField -> Bool -> ModField
forall a. a -> a -> Bool -> a
bool ModField
falseMods ModField
trueMods
  where
    trueMods :: ModField
trueMods = ModField
emptyModField{modZ :: Bool
modZ = Bool
True, modU :: Bool
modU = Bool
True}
    falseMods :: ModField
falseMods = ModField
emptyModField{modZ :: Bool
modZ = Bool
True, modU :: Bool
modU = Bool
True, modD :: Bool
modD = Bool
True}

numberType :: MiniscriptType
numberType :: MiniscriptType
numberType = BaseType -> ModField -> MiniscriptType
MiniscriptType BaseType
TypeNumber ModField
emptyModField

bytesType :: MiniscriptType
bytesType :: MiniscriptType
bytesType = BaseType -> ModField -> MiniscriptType
MiniscriptType BaseType
TypeBytes ModField
emptyModField

keyDescriptorType :: MiniscriptType
keyDescriptorType :: MiniscriptType
keyDescriptorType = BaseType -> ModField -> MiniscriptType
MiniscriptType BaseType
TypeKeyDesc ModField
emptyModField

data MiniscriptTypeError
    = MiniscriptTypeError Miniscript
    | UntypedVariable Text
    | -- | fields: @name expectedBaseType typeAnnotation@
      WrongVariableType Text BaseType MiniscriptType
    deriving (MiniscriptTypeError -> MiniscriptTypeError -> Bool
(MiniscriptTypeError -> MiniscriptTypeError -> Bool)
-> (MiniscriptTypeError -> MiniscriptTypeError -> Bool)
-> Eq MiniscriptTypeError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MiniscriptTypeError -> MiniscriptTypeError -> Bool
$c/= :: MiniscriptTypeError -> MiniscriptTypeError -> Bool
== :: MiniscriptTypeError -> MiniscriptTypeError -> Bool
$c== :: MiniscriptTypeError -> MiniscriptTypeError -> Bool
Eq, Int -> MiniscriptTypeError -> ShowS
[MiniscriptTypeError] -> ShowS
MiniscriptTypeError -> String
(Int -> MiniscriptTypeError -> ShowS)
-> (MiniscriptTypeError -> String)
-> ([MiniscriptTypeError] -> ShowS)
-> Show MiniscriptTypeError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MiniscriptTypeError] -> ShowS
$cshowList :: [MiniscriptTypeError] -> ShowS
show :: MiniscriptTypeError -> String
$cshow :: MiniscriptTypeError -> String
showsPrec :: Int -> MiniscriptTypeError -> ShowS
$cshowsPrec :: Int -> MiniscriptTypeError -> ShowS
Show)

type TypeCheckM a = ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a

requiredVarType :: Text -> TypeCheckM MiniscriptType
requiredVarType :: Text -> TypeCheckM MiniscriptType
requiredVarType Text
name = (Map Text MiniscriptType -> Map Text MiniscriptType)
-> MiniscriptTypeError -> Text -> TypeCheckM MiniscriptType
forall r c e.
(r -> Map Text c) -> e -> Text -> ReaderT r (Except e) c
requiredContextValue Map Text MiniscriptType -> Map Text MiniscriptType
forall a. a -> a
id (Text -> MiniscriptTypeError
UntypedVariable Text
name) Text
name

-- | Check that a miniscript expression is well-typed.
typeCheckMiniscript ::
    -- | type hints for free variables in the miniscript expression
    Map Text MiniscriptType ->
    Miniscript ->
    Either MiniscriptTypeError MiniscriptType
typeCheckMiniscript :: Map Text MiniscriptType
-> Miniscript -> Either MiniscriptTypeError MiniscriptType
typeCheckMiniscript Map Text MiniscriptType
context = Except MiniscriptTypeError MiniscriptType
-> Either MiniscriptTypeError MiniscriptType
forall e a. Except e a -> Either e a
runExcept (Except MiniscriptTypeError MiniscriptType
 -> Either MiniscriptTypeError MiniscriptType)
-> (Miniscript -> Except MiniscriptTypeError MiniscriptType)
-> Miniscript
-> Either MiniscriptTypeError MiniscriptType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeCheckM MiniscriptType
-> Map Text MiniscriptType
-> Except MiniscriptTypeError MiniscriptType
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` Map Text MiniscriptType
context) (TypeCheckM MiniscriptType
 -> Except MiniscriptTypeError MiniscriptType)
-> (Miniscript -> TypeCheckM MiniscriptType)
-> Miniscript
-> Except MiniscriptTypeError MiniscriptType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext

typeCheckInContext :: Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext :: Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext = \case
    Var Text
name -> Text -> TypeCheckM MiniscriptType
requiredVarType Text
name
    Let Text
name Miniscript
expr Miniscript
body -> do
        MiniscriptType
ty <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
expr
        (Map Text MiniscriptType -> Map Text MiniscriptType)
-> TypeCheckM MiniscriptType -> TypeCheckM MiniscriptType
forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local (Text
-> MiniscriptType
-> Map Text MiniscriptType
-> Map Text MiniscriptType
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name MiniscriptType
ty) (TypeCheckM MiniscriptType -> TypeCheckM MiniscriptType)
-> TypeCheckM MiniscriptType -> TypeCheckM MiniscriptType
forall a b. (a -> b) -> a -> b
$ Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
body
    Boolean Bool
b -> MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return (MiniscriptType -> TypeCheckM MiniscriptType)
-> MiniscriptType -> TypeCheckM MiniscriptType
forall a b. (a -> b) -> a -> b
$ Bool -> MiniscriptType
boolType Bool
b
    Number{} -> MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
numberType
    Bytes{} -> MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
bytesType
    KeyDesc{} -> MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
keyDescriptorType
    Key Value KeyDescriptor
x -> BaseType -> MiniscriptType
ondu BaseType
TypeK MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value KeyDescriptor
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeKeyDesc Value KeyDescriptor
x
    KeyH Value KeyDescriptor
x -> BaseType -> MiniscriptType
ndu BaseType
TypeK MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value KeyDescriptor
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeKeyDesc Value KeyDescriptor
x
    Older Value Int
x -> BaseType
-> Value Int
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
x ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType BaseType
TypeB ModField
emptyModField{modZ :: Bool
modZ = Bool
True}
    After Value Int
x -> BaseType
-> Value Int
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
x ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType BaseType
TypeB ModField
emptyModField{modZ :: Bool
modZ = Bool
True}
    Sha256 Value ByteString
x -> BaseType -> MiniscriptType
ondu BaseType
TypeB MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value ByteString
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeBytes Value ByteString
x
    Ripemd160 Value ByteString
x -> BaseType -> MiniscriptType
ondu BaseType
TypeB MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value ByteString
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeBytes Value ByteString
x
    Hash256 Value ByteString
x -> BaseType -> MiniscriptType
ondu BaseType
TypeB MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value ByteString
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeBytes Value ByteString
x
    Hash160 Value ByteString
x -> BaseType -> MiniscriptType
ondu BaseType
TypeB MiniscriptType
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> TypeCheckM MiniscriptType
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BaseType
-> Value ByteString
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeBytes Value ByteString
x
    e :: Miniscript
e@(AndOr Miniscript
x Miniscript
y Miniscript
z) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
ty <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
y
        MiniscriptType
tz <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
z

        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            my :: ModField
my = MiniscriptType -> ModField
modifiers MiniscriptType
ty
            mz :: ModField
mz = MiniscriptType -> ModField
modifiers MiniscriptType
tz

            bty :: BaseType
bty = MiniscriptType -> BaseType
baseType MiniscriptType
ty

        if (MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB) Bool -> Bool -> Bool
&& (MiniscriptType -> BaseType
baseType MiniscriptType
tz BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
bty) Bool -> Bool -> Bool
&& BaseType -> Bool
notW BaseType
bty Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
bty
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modO :: Bool
modO = (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
my Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
mz) Bool -> Bool -> Bool
|| (ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz)
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
my Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
mz
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mz
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AndV Miniscript
x Miniscript
y) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
ty <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
y
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            my :: ModField
my = MiniscriptType -> ModField
modifiers MiniscriptType
ty
            bty :: BaseType
bty = MiniscriptType -> BaseType
baseType MiniscriptType
ty
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeV Bool -> Bool -> Bool
&& BaseType -> Bool
notW BaseType
bty
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
bty
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my
                        , modO :: Bool
modO = (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
my) Bool -> Bool -> Bool
|| (ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my)
                        , modN :: Bool
modN = ModField -> Bool
modN ModField
mx Bool -> Bool -> Bool
|| (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modN ModField
my)
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
my
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AndB Miniscript
x Miniscript
y) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
ty <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
y
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            my :: ModField
my = MiniscriptType -> ModField
modifiers MiniscriptType
ty
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
ty BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeW
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my
                        , modO :: Bool
modO = (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
my) Bool -> Bool -> Bool
|| (ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
my)
                        , modN :: Bool
modN = ModField -> Bool
modN ModField
mx Bool -> Bool -> Bool
|| (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modN ModField
my)
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
my
                        , modU :: Bool
modU = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(OrB Miniscript
x Miniscript
z) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
tz <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
z
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            mz :: ModField
mz = MiniscriptType -> ModField
modifiers MiniscriptType
tz
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeW Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
mz
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modO :: Bool
modO =
                            (ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
mz)
                                Bool -> Bool -> Bool
|| (ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz)
                        , modD :: Bool
modD = Bool
True
                        , modU :: Bool
modU = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(OrC Miniscript
x Miniscript
z) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
tz <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
z
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            mz :: ModField
mz = MiniscriptType -> ModField
modifiers MiniscriptType
tz
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeV Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeV
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modO :: Bool
modO = ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(OrD Miniscript
x Miniscript
z) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
tz <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
z
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            mz :: ModField
mz = MiniscriptType -> ModField
modifiers MiniscriptType
tz
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modO :: Bool
modO = ModField -> Bool
modO ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mz
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
mz
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(OrI Miniscript
x Miniscript
z) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        MiniscriptType
tz <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
z
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            mz :: ModField
mz = MiniscriptType -> ModField
modifiers MiniscriptType
tz
            btx :: BaseType
btx = MiniscriptType -> BaseType
baseType MiniscriptType
tx
        if (MiniscriptType -> BaseType
baseType MiniscriptType
tz BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
btx) Bool -> Bool -> Bool
&& BaseType -> Bool
notW BaseType
btx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
btx
                    ModField
emptyModField
                        { modO :: Bool
modO = ModField -> Bool
modZ ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mz
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mx Bool -> Bool -> Bool
|| ModField -> Bool
modD ModField
mz
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
mx Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
mz
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(Thresh Value Int
k Miniscript
x [Miniscript]
ys) -> do
        BaseType
-> Value Int
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
k
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        [MiniscriptType]
tys <- (Miniscript -> TypeCheckM MiniscriptType)
-> [Miniscript]
-> ReaderT
     (Map Text MiniscriptType)
     (Except MiniscriptTypeError)
     [MiniscriptType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext [Miniscript]
ys
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
            mys :: [ModField]
mys = MiniscriptType -> ModField
modifiers (MiniscriptType -> ModField) -> [MiniscriptType] -> [ModField]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MiniscriptType]
tys
            allMods :: [ModField]
allMods = ModField
mx ModField -> [ModField] -> [ModField]
forall a. a -> [a] -> [a]
: [ModField]
mys
            zCount :: Int
zCount = (ModField -> Bool) -> [ModField] -> Int
forall (t :: * -> *) c a.
(Foldable t, Num c, Functor t) =>
(a -> Bool) -> t a -> c
count ModField -> Bool
modZ [ModField]
allMods
            oCount :: Int
oCount = (ModField -> Bool) -> [ModField] -> Int
forall (t :: * -> *) c a.
(Foldable t, Num c, Functor t) =>
(a -> Bool) -> t a -> c
count ModField -> Bool
modO [ModField]
allMods :: Int
            count :: (a -> Bool) -> t a -> c
count a -> Bool
f = t c -> c
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (t c -> c) -> (t a -> t c) -> t a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c) -> t a -> t c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (c -> c -> Bool -> c
forall a. a -> a -> Bool -> a
bool c
0 c
1 (Bool -> c) -> (a -> Bool) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Bool
f)
            isDU :: ModField -> Bool
isDU ModField
m = ModField -> Bool
modD ModField
m Bool -> Bool -> Bool
&& ModField -> Bool
modU ModField
m

        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& (BaseType -> Bool) -> [BaseType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeW) (MiniscriptType -> BaseType
baseType (MiniscriptType -> BaseType) -> [MiniscriptType] -> [BaseType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MiniscriptType]
tys) Bool -> Bool -> Bool
&& (ModField -> Bool) -> [ModField] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ModField -> Bool
isDU [ModField]
allMods
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = (ModField -> Bool) -> [ModField] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ModField -> Bool
modZ [ModField]
allMods
                        , modO :: Bool
modO = Int
zCount Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Miniscript] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Miniscript]
ys Bool -> Bool -> Bool
&& Int
oCount Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
                        , modD :: Bool
modD = Bool
True
                        , modU :: Bool
modU = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    Multi Value Int
k [Value KeyDescriptor]
ks -> do
        BaseType
-> Value Int
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
k
        (Value KeyDescriptor
 -> ReaderT
      (Map Text MiniscriptType) (Except MiniscriptTypeError) ())
-> [Value KeyDescriptor]
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (BaseType
-> Value KeyDescriptor
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeKeyDesc) [Value KeyDescriptor]
ks
        MiniscriptType -> TypeCheckM MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return (MiniscriptType -> TypeCheckM MiniscriptType)
-> MiniscriptType -> TypeCheckM MiniscriptType
forall a b. (a -> b) -> a -> b
$ BaseType -> MiniscriptType
ndu BaseType
TypeB
    e :: Miniscript
e@(AnnA Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeW
                    ModField
emptyModField
                        { modD :: Bool
modD = ModField -> Bool
modD ModField
mx
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
mx
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnS Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeW
                    ModField
emptyModField
                        { modD :: Bool
modD = ModField -> Bool
modD ModField
mx
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
mx
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnC Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeK
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modO :: Bool
modO = ModField -> Bool
modO ModField
mx
                        , modN :: Bool
modN = ModField -> Bool
modN ModField
mx
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mx
                        , modU :: Bool
modU = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnD Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeV Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modO :: Bool
modO = ModField -> Bool
modZ ModField
mx
                        , modN :: Bool
modN = Bool
True
                        , modU :: Bool
modU = Bool
True
                        , modD :: Bool
modD = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnV Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeV
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx
                        , modO :: Bool
modO = ModField -> Bool
modO ModField
mx
                        , modN :: Bool
modN = ModField -> Bool
modN ModField
mx
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnJ Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& ModField -> Bool
modN ModField
mx
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modO :: Bool
modO = ModField -> Bool
modO ModField
mx
                        , modN :: Bool
modN = Bool
True
                        , modD :: Bool
modD = Bool
True
                        , modU :: Bool
modU = ModField -> Bool
modU ModField
mx
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    e :: Miniscript
e@(AnnN Miniscript
x) -> do
        MiniscriptType
tx <- Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
x
        let mx :: ModField
mx = MiniscriptType -> ModField
modifiers MiniscriptType
tx
        if MiniscriptType -> BaseType
baseType MiniscriptType
tx BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                BaseType -> ModField -> TypeCheckM MiniscriptType
forall (m :: * -> *).
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = ModField -> Bool
modZ ModField
mx
                        , modO :: Bool
modO = ModField -> Bool
modO ModField
mx
                        , modN :: Bool
modN = ModField -> Bool
modN ModField
mx
                        , modD :: Bool
modD = ModField -> Bool
modD ModField
mx
                        , modU :: Bool
modU = Bool
True
                        }
            else Miniscript -> TypeCheckM MiniscriptType
forall a.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
  where
    ondu :: BaseType -> MiniscriptType
ondu = (BaseType -> ModField -> MiniscriptType)
-> ModField -> BaseType -> MiniscriptType
forall a b c. (a -> b -> c) -> b -> a -> c
flip BaseType -> ModField -> MiniscriptType
MiniscriptType ModField
emptyModField{modO :: Bool
modO = Bool
True, modN :: Bool
modN = Bool
True, modD :: Bool
modD = Bool
True, modU :: Bool
modU = Bool
True}
    ndu :: BaseType -> MiniscriptType
ndu = (BaseType -> ModField -> MiniscriptType)
-> ModField -> BaseType -> MiniscriptType
forall a b c. (a -> b -> c) -> b -> a -> c
flip BaseType -> ModField -> MiniscriptType
MiniscriptType ModField
emptyModField{modN :: Bool
modN = Bool
True, modD :: Bool
modD = Bool
True, modU :: Bool
modU = Bool
True}

    exprType :: BaseType -> ModField -> m MiniscriptType
exprType BaseType
t = MiniscriptType -> m MiniscriptType
forall (m :: * -> *) a. Monad m => a -> m a
return (MiniscriptType -> m MiniscriptType)
-> (ModField -> MiniscriptType) -> ModField -> m MiniscriptType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BaseType -> ModField -> MiniscriptType
MiniscriptType BaseType
t
    typeError :: Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError = ExceptT MiniscriptTypeError Identity a
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT MiniscriptTypeError Identity a
 -> ReaderT
      (Map Text MiniscriptType) (Except MiniscriptTypeError) a)
-> (Miniscript -> ExceptT MiniscriptTypeError Identity a)
-> Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MiniscriptTypeError -> ExceptT MiniscriptTypeError Identity a
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (MiniscriptTypeError -> ExceptT MiniscriptTypeError Identity a)
-> (Miniscript -> MiniscriptTypeError)
-> Miniscript
-> ExceptT MiniscriptTypeError Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Miniscript -> MiniscriptTypeError
MiniscriptTypeError

    literal :: BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
bt (Variable Text
n) = do
        MiniscriptType
t' <- Text -> TypeCheckM MiniscriptType
requiredVarType Text
n
        Bool
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MiniscriptType -> BaseType
baseType MiniscriptType
t' BaseType -> BaseType -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType
bt) (ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
 -> ReaderT
      (Map Text MiniscriptType) (Except MiniscriptTypeError) ())
-> (MiniscriptTypeError
    -> ReaderT
         (Map Text MiniscriptType) (Except MiniscriptTypeError) ())
-> MiniscriptTypeError
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT MiniscriptTypeError Identity ()
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT MiniscriptTypeError Identity ()
 -> ReaderT
      (Map Text MiniscriptType) (Except MiniscriptTypeError) ())
-> (MiniscriptTypeError -> ExceptT MiniscriptTypeError Identity ())
-> MiniscriptTypeError
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MiniscriptTypeError -> ExceptT MiniscriptTypeError Identity ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE (MiniscriptTypeError
 -> ReaderT
      (Map Text MiniscriptType) (Except MiniscriptTypeError) ())
-> MiniscriptTypeError
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall a b. (a -> b) -> a -> b
$ Text -> BaseType -> MiniscriptType -> MiniscriptTypeError
WrongVariableType Text
n BaseType
bt MiniscriptType
t'
    literal BaseType
_ Value a
_ = ()
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()