{-# LANGUAGE GADTs            #-}
{-# LANGUAGE TypeApplications #-}
module PlutusCore.Arity where

import Data.Proxy
import PlutusCore
import PlutusCore.Builtin
import Prettyprinter

-- | Is the next argument a term or a type?
data Param =
    TermParam | TypeParam
    deriving stock (Int -> Param -> ShowS
[Param] -> ShowS
Param -> String
(Int -> Param -> ShowS)
-> (Param -> String) -> ([Param] -> ShowS) -> Show Param
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Param -> ShowS
showsPrec :: Int -> Param -> ShowS
$cshow :: Param -> String
show :: Param -> String
$cshowList :: [Param] -> ShowS
showList :: [Param] -> ShowS
Show, Param -> Param -> Bool
(Param -> Param -> Bool) -> (Param -> Param -> Bool) -> Eq Param
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Param -> Param -> Bool
== :: Param -> Param -> Bool
$c/= :: Param -> Param -> Bool
/= :: Param -> Param -> Bool
Eq)

instance Pretty Param where
  pretty :: forall ann. Param -> Doc ann
pretty = Param -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

{-|
The (syntactic) arity of a term. That is, a record of the arguments that the
term expects before it may do some work. Since we have both type and lambda
abstractions, this is not a simple argument count, but rather a list of values
indicating whether the next argument should be a term or a type.

Note that this is the syntactic arity, i.e. it just corresponds to the number of
syntactic lambda and type abstractions on the outside of the term. It is thus
an under-approximation of how many arguments the term may need.
e.g. consider the term @let id = \x -> x in id@: the variable @id@ has syntactic
arity @[]@, but does in fact need an argument before it does any work.
-}
type Arity = [Param]

-- | Get the 'Arity' from a 'TypeScheme'.
typeSchemeArity :: TypeScheme val args res -> Arity
typeSchemeArity :: forall val (args :: [*]) res. TypeScheme val args res -> [Param]
typeSchemeArity TypeSchemeResult{}    = []
typeSchemeArity (TypeSchemeArrow TypeScheme val args1 res
sch) = Param
TermParam Param -> [Param] -> [Param]
forall a. a -> [a] -> [a]
: TypeScheme val args1 res -> [Param]
forall val (args :: [*]) res. TypeScheme val args res -> [Param]
typeSchemeArity TypeScheme val args1 res
sch
typeSchemeArity (TypeSchemeAll Proxy '(text, uniq, kind)
_ TypeScheme val args res
sch) = Param
TypeParam Param -> [Param] -> [Param]
forall a. a -> [a] -> [a]
: TypeScheme val args res -> [Param]
forall val (args :: [*]) res. TypeScheme val args res -> [Param]
typeSchemeArity TypeScheme val args res
sch

-- | Get the arity of a builtin function from the 'PLC.BuiltinSemanticsVariant'.
builtinArity
    :: forall uni fun
    . ToBuiltinMeaning uni fun
    => Proxy uni
    -> BuiltinSemanticsVariant fun
    -> fun
    -> Arity
builtinArity :: forall (uni :: * -> *) fun.
ToBuiltinMeaning uni fun =>
Proxy uni -> BuiltinSemanticsVariant fun -> fun -> [Param]
builtinArity Proxy uni
_ BuiltinSemanticsVariant fun
semvar fun
fun =
  case forall (uni :: * -> *) fun val.
(ToBuiltinMeaning uni fun, HasMeaningIn uni val) =>
BuiltinSemanticsVariant fun
-> fun -> BuiltinMeaning val (CostingPart uni fun)
toBuiltinMeaning @uni @fun @(Term TyName Name uni fun ()) BuiltinSemanticsVariant fun
semvar fun
fun of
    BuiltinMeaning TypeScheme (Term TyName Name uni fun ()) args res
sch FoldArgs args res
_ CostingPart uni fun -> BuiltinRuntime (Term TyName Name uni fun ())
_ -> TypeScheme (Term TyName Name uni fun ()) args res -> [Param]
forall val (args :: [*]) res. TypeScheme val args res -> [Param]
typeSchemeArity TypeScheme (Term TyName Name uni fun ()) args res
sch