{-# 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
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
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 = (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
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
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
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
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
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
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 = forall r c e.
(r -> Map Text c) -> e -> Text -> ReaderT r (Except e) c
requiredContextValue 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 = forall e a. Except e a -> Either e a
runExcept forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` Map Text MiniscriptType
context) 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
        forall r (m :: * -> *) a.
(r -> r) -> ReaderT r m a -> ReaderT r m a
local (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
name MiniscriptType
ty) forall a b. (a -> b) -> a -> b
$ Miniscript -> TypeCheckM MiniscriptType
typeCheckInContext Miniscript
body
    Boolean Bool
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> MiniscriptType
boolType Bool
b
    Number{} -> forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
numberType
    Bytes{} -> forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
bytesType
    KeyDesc{} -> forall (m :: * -> *) a. Monad m => a -> m a
return MiniscriptType
keyDescriptorType
    Key Value KeyDescriptor
x -> BaseType -> MiniscriptType
ondu BaseType
TypeK forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall {a}.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeKeyDesc Value KeyDescriptor
x
    Older Value Int
x -> forall {a}.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall {m :: * -> *}.
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType BaseType
TypeB ModField
emptyModField{modZ :: Bool
modZ = Bool
True}
    After Value Int
x -> forall {a}.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB) Bool -> Bool -> Bool
&& (MiniscriptType -> BaseType
baseType MiniscriptType
tz 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
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeV Bool -> Bool -> Bool
&& BaseType -> Bool
notW BaseType
bty
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
ty forall a. Eq a => a -> a -> Bool
== BaseType
TypeW
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz 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
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz 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
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& MiniscriptType -> BaseType
baseType MiniscriptType
tz 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
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
btx) Bool -> Bool -> Bool
&& BaseType -> Bool
notW BaseType
btx
            then
                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 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
        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 <- 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MiniscriptType]
tys
            allMods :: [ModField]
allMods = ModField
mx forall a. a -> [a] -> [a]
: [ModField]
mys
            zCount :: Int
zCount = forall {t :: * -> *} {c} {a}.
(Foldable t, Num c, Functor t) =>
(a -> Bool) -> t a -> c
count ModField -> Bool
modZ [ModField]
allMods
            oCount :: Int
oCount = 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 = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> a -> Bool -> a
bool c
0 c
1 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== BaseType
TypeW) (MiniscriptType -> BaseType
baseType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MiniscriptType]
tys) Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ModField -> Bool
isDU [ModField]
allMods
            then
                forall {m :: * -> *}.
Monad m =>
BaseType -> ModField -> m MiniscriptType
exprType
                    BaseType
TypeB
                    ModField
emptyModField
                        { modZ :: Bool
modZ = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ModField -> Bool
modZ [ModField]
allMods
                        , modO :: Bool
modO = Int
zCount forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Miniscript]
ys Bool -> Bool -> Bool
&& Int
oCount forall a. Eq a => a -> a -> Bool
== Int
1
                        , modD :: Bool
modD = Bool
True
                        , modU :: Bool
modU = Bool
True
                        }
            else forall {a}.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
    Multi Value Int
k [Value KeyDescriptor]
ks -> do
        forall {a}.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeNumber Value Int
k
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {a}.
BaseType
-> Value a
-> ReaderT
     (Map Text MiniscriptType) (Except MiniscriptTypeError) ()
literal BaseType
TypeKeyDesc) [Value KeyDescriptor]
ks
        forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& ModField -> Bool
modO ModField
mx
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeK
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeV Bool -> Bool -> Bool
&& ModField -> Bool
modZ ModField
mx
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB Bool -> Bool -> Bool
&& ModField -> Bool
modN ModField
mx
            then
                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 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 forall a. Eq a => a -> a -> Bool
== BaseType
TypeB
            then
                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 forall {a}.
Miniscript
-> ReaderT (Map Text MiniscriptType) (Except MiniscriptTypeError) a
typeError Miniscript
e
  where
    ondu :: BaseType -> MiniscriptType
ondu = 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 = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE 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
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (MiniscriptType -> BaseType
baseType MiniscriptType
t' forall a. Eq a => a -> a -> Bool
== BaseType
bt) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE forall a b. (a -> b) -> a -> b
$ Text -> BaseType -> MiniscriptType -> MiniscriptTypeError
WrongVariableType Text
n BaseType
bt MiniscriptType
t'
    literal BaseType
_ Value a
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()