{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
module PlutusIR.Analysis.VarInfo where

import Control.Lens hiding (Strict)
import Data.List.Extra ((!?))
import Data.Traversable
import PlutusCore qualified as PLC
import PlutusCore.Arity
import PlutusCore.Core (funTyArgs)
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Name.UniqueMap qualified as UMap
import PlutusIR.Core

-- | Information about variables and type variables in the program.
data VarsInfo tyname name uni a = VarsInfo
  { forall tyname name (uni :: * -> *) a.
VarsInfo tyname name uni a
-> UniqueMap TermUnique (VarInfo tyname name uni a)
termVarInfoMap :: PLC.UniqueMap PLC.TermUnique (VarInfo tyname name uni a)
  , forall tyname name (uni :: * -> *) a.
VarsInfo tyname name uni a
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
typeVarInfoMap :: PLC.UniqueMap PLC.TypeUnique (TyVarInfo tyname name uni a)
  }

instance Semigroup (VarsInfo tyname name uni a) where
  (VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
t UniqueMap TypeUnique (TyVarInfo tyname name uni a)
ty) <> :: VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
<> (VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
t' UniqueMap TypeUnique (TyVarInfo tyname name uni a)
ty') = UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo (UniqueMap TermUnique (VarInfo tyname name uni a)
t UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Semigroup a => a -> a -> a
<> UniqueMap TermUnique (VarInfo tyname name uni a)
t') (UniqueMap TypeUnique (TyVarInfo tyname name uni a)
ty UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Semigroup a => a -> a -> a
<> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
ty')

instance Monoid (VarsInfo tyname name uni a) where
  mempty :: VarsInfo tyname name uni a
mempty = UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty

-- | Lookup the 'VarInfo' for a 'name'.
lookupVarInfo ::
  (PLC.HasUnique name PLC.TermUnique)
  => name
  -> VarsInfo tyname name uni a
  -> Maybe (VarInfo tyname name uni a)
lookupVarInfo :: forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo name
name (VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
vim UniqueMap TypeUnique (TyVarInfo tyname name uni a)
_) = name
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> Maybe (VarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
UMap.lookupName name
name UniqueMap TermUnique (VarInfo tyname name uni a)
vim

-- | Lookup the 'TyVarInfo' for a 'tyname'.
lookupTyVarInfo ::
  (PLC.HasUnique tyname PLC.TypeUnique)
  => tyname
  -> VarsInfo tyname name uni a
  -> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo :: forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo tyname
name (VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
_ UniqueMap TypeUnique (TyVarInfo tyname name uni a)
vim) = tyname
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> Maybe (TyVarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
UMap.lookupName tyname
name UniqueMap TypeUnique (TyVarInfo tyname name uni a)
vim

-- | Information about a type variable in the program.
data TyVarInfo tyname name uni a =
  -- | A normal type variable, which could be anything.
  NormalTyVar
  -- | A type variable corresponding to a datatype.
  -- Tells us the number of type variables and the constructors.
  | DatatypeTyVar (Datatype tyname name uni a)

data VarInfo tyname name uni a =
  -- | A normal term variable, which could be anything.
  -- Tells us if it is strictly evaluated, its type, and possibly its arity.
  NormalVar Strictness (Type tyname uni a) (Maybe Arity)
  -- | A term variable corresponding to a datatype constructor.
  -- Tells us the index of the constructor and the name of the datatype that owns it.
  | DatatypeConstructor Int tyname
  -- | A term variable corresponding to a datatype matcher.
  -- Tells us the name of the datatype that owns it.
  | DatatypeMatcher tyname

varInfoStrictness :: VarInfo tyname name uni a -> Strictness
varInfoStrictness :: forall tyname name (uni :: * -> *) a.
VarInfo tyname name uni a -> Strictness
varInfoStrictness = \case
  NormalVar Strictness
s Type tyname uni a
_ Maybe Arity
_       -> Strictness
s
  DatatypeConstructor{} -> Strictness
Strict
  DatatypeMatcher{}     -> Strictness
Strict

varInfoArity ::
  (PLC.HasUnique tyname PLC.TypeUnique)
  => VarInfo tyname name uni a
  -> VarsInfo tyname name uni a
  -> Maybe Arity
varInfoArity :: forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
VarInfo tyname name uni a
-> VarsInfo tyname name uni a -> Maybe Arity
varInfoArity VarInfo tyname name uni a
vinfo VarsInfo tyname name uni a
vinfos = case VarInfo tyname name uni a
vinfo of
  NormalVar Strictness
_ Type tyname uni a
_ Maybe Arity
a            -> Maybe Arity
a
  DatatypeConstructor Int
i tyname
dtName -> case tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo tyname
dtName VarsInfo tyname name uni a
vinfos of
    Just (DatatypeTyVar Datatype tyname name uni a
dt) -> Int -> Datatype tyname name uni a -> Maybe Arity
forall tyname uni (fun :: * -> *) a.
Int -> Datatype tyname uni fun a -> Maybe Arity
datatypeConstructorArity Int
i Datatype tyname name uni a
dt
    Maybe (TyVarInfo tyname name uni a)
_                       -> Maybe Arity
forall a. Maybe a
Nothing
  DatatypeMatcher tyname
dtName     -> case tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo tyname
dtName VarsInfo tyname name uni a
vinfos of
    Just (DatatypeTyVar Datatype tyname name uni a
dt) -> Arity -> Maybe Arity
forall a. a -> Maybe a
Just (Arity -> Maybe Arity) -> Arity -> Maybe Arity
forall a b. (a -> b) -> a -> b
$ Datatype tyname name uni a -> Arity
forall tyname uni (fun :: * -> *) a.
Datatype tyname uni fun a -> Arity
datatypeMatcherArity Datatype tyname name uni a
dt
    Maybe (TyVarInfo tyname name uni a)
_                       -> Maybe Arity
forall a. Maybe a
Nothing

termVarInfo ::
  (PLC.HasUnique name PLC.TermUnique
  , PLC.HasUnique tyname PLC.TypeUnique)
  => Term tyname name uni fun a
  -> VarsInfo tyname name uni a
termVarInfo :: forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo = \case
  Let a
_ Recursivity
_ NonEmpty (Binding tyname name uni fun a)
bs Term tyname name uni fun a
t   -> (Binding tyname name uni fun a -> VarsInfo tyname name uni a)
-> NonEmpty (Binding tyname name uni fun a)
-> VarsInfo tyname name uni a
forall m a. Monoid m => (a -> m) -> NonEmpty a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Binding tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Binding tyname name uni fun a -> VarsInfo tyname name uni a
bindingVarInfo NonEmpty (Binding tyname name uni fun a)
bs VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  LamAbs a
_ name
n Type tyname uni a
ty Term tyname name uni fun a
t ->
    UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo (name
-> VarInfo tyname name uni a
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
n (Strictness
-> Type tyname uni a -> Maybe Arity -> VarInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
Strictness
-> Type tyname uni a -> Maybe Arity -> VarInfo tyname name uni a
NormalVar Strictness
Strict Type tyname uni a
ty Maybe Arity
forall a. Maybe a
Nothing) UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty) UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty
    VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  TyAbs a
_ tyname
n Kind a
_ Term tyname name uni fun a
t   ->
    UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty (tyname
-> TyVarInfo tyname name uni a
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName tyname
n TyVarInfo tyname name uni a
forall tyname name (uni :: * -> *) a. TyVarInfo tyname name uni a
NormalTyVar UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty)
    VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  -- No binders
  t :: Term tyname name uni fun a
t@(Apply{})    -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(TyInst{})   -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(IWrap{})    -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Unwrap{})   -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Constr{})   -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Case{})     -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Var{})      -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Constant{}) -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Error{})    -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  t :: Term tyname name uni fun a
t@(Builtin{})  -> Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
-> (Term tyname name uni fun a -> VarsInfo tyname name uni a)
-> Term tyname name uni fun a
-> VarsInfo tyname name uni a
forall r s a. Getting r s a -> (a -> r) -> s -> r
foldMapOf Getting
  (VarsInfo tyname name uni a)
  (Term tyname name uni fun a)
  (Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubterms Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t

datatypeMatcherArity :: Datatype tyname uni fun a -> Arity
datatypeMatcherArity :: forall tyname uni (fun :: * -> *) a.
Datatype tyname uni fun a -> Arity
datatypeMatcherArity (Datatype a
_ TyVarDecl tyname a
_ [TyVarDecl tyname a]
tyvars uni
_ [VarDecl tyname uni fun a]
constrs)=
  -- One parameter for all the datatype type variables
  (TyVarDecl tyname a -> Param) -> [TyVarDecl tyname a] -> Arity
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Param -> TyVarDecl tyname a -> Param
forall a b. a -> b -> a
const Param
TypeParam) [TyVarDecl tyname a]
tyvars
  -- The scrutineee, and then a type paramter for the result type
  Arity -> Arity -> Arity
forall a. [a] -> [a] -> [a]
++ [Param
TermParam, Param
TypeParam]
  -- One parameter with the case for each constructor
  Arity -> Arity -> Arity
forall a. [a] -> [a] -> [a]
++ (VarDecl tyname uni fun a -> Param)
-> [VarDecl tyname uni fun a] -> Arity
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Param -> VarDecl tyname uni fun a -> Param
forall a b. a -> b -> a
const Param
TermParam) [VarDecl tyname uni fun a]
constrs

datatypeConstructorArity :: Int -> Datatype tyname uni fun a -> Maybe Arity
datatypeConstructorArity :: forall tyname uni (fun :: * -> *) a.
Int -> Datatype tyname uni fun a -> Maybe Arity
datatypeConstructorArity Int
i (Datatype a
_ TyVarDecl tyname a
_ [TyVarDecl tyname a]
tyvars uni
_ [VarDecl tyname uni fun a]
constrs) =
  case [VarDecl tyname uni fun a]
constrs [VarDecl tyname uni fun a]
-> Int -> Maybe (VarDecl tyname uni fun a)
forall a. [a] -> Int -> Maybe a
!? Int
i of
    Just (VarDecl a
_ uni
_ Type tyname fun a
constrTy) -> Arity -> Maybe Arity
forall a. a -> Maybe a
Just (Arity -> Maybe Arity) -> Arity -> Maybe Arity
forall a b. (a -> b) -> a -> b
$
      -- One type parameter for all of the datatype type parameters
      (TyVarDecl tyname a -> Param) -> [TyVarDecl tyname a] -> Arity
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Param -> TyVarDecl tyname a -> Param
forall a b. a -> b -> a
const Param
TypeParam) [TyVarDecl tyname a]
tyvars
      -- One term parameter for all the constructor function type arguments
      Arity -> Arity -> Arity
forall a. [a] -> [a] -> [a]
++ (Type tyname fun a -> Param) -> [Type tyname fun a] -> Arity
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Param -> Type tyname fun a -> Param
forall a b. a -> b -> a
const Param
TermParam) (Type tyname fun a -> [Type tyname fun a]
forall tyname (uni :: * -> *) a.
Type tyname uni a -> [Type tyname uni a]
funTyArgs Type tyname fun a
constrTy)
    Maybe (VarDecl tyname uni fun a)
_ -> Maybe Arity
forall a. Maybe a
Nothing

bindingVarInfo ::
  (PLC.HasUnique name PLC.TermUnique
  , PLC.HasUnique tyname PLC.TypeUnique)
  => Binding tyname name uni fun a
  -> VarsInfo tyname name uni a
bindingVarInfo :: forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Binding tyname name uni fun a -> VarsInfo tyname name uni a
bindingVarInfo = \case
  -- TODO: arity for term bindings
  TermBind a
_ Strictness
s (VarDecl a
_ name
n Type tyname uni a
ty) Term tyname name uni fun a
t ->
    UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo (name
-> VarInfo tyname name uni a
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
n (Strictness
-> Type tyname uni a -> Maybe Arity -> VarInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
Strictness
-> Type tyname uni a -> Maybe Arity -> VarInfo tyname name uni a
NormalVar Strictness
s Type tyname uni a
ty Maybe Arity
forall a. Maybe a
Nothing) UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty) UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty
    VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> Term tyname name uni fun a -> VarsInfo tyname name uni a
forall name tyname (uni :: * -> *) fun a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
Term tyname name uni fun a -> VarsInfo tyname name uni a
termVarInfo Term tyname name uni fun a
t
  TypeBind a
_ (TyVarDecl a
_ tyname
n Kind a
_) Type tyname uni a
_ ->
    UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty (tyname
-> TyVarInfo tyname name uni a
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName tyname
n TyVarInfo tyname name uni a
forall tyname name (uni :: * -> *) a. TyVarInfo tyname name uni a
NormalTyVar UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty)
  DatatypeBind a
_ d :: Datatype tyname name uni a
d@(Datatype a
_ (TyVarDecl a
_ tyname
tyname Kind a
_) [TyVarDecl tyname a]
_ name
matcher [VarDecl tyname name uni a]
constrs) ->
    let
      dtInfo :: VarsInfo tyname name uni a
dtInfo =
        let info :: TyVarInfo tyname name uni a
info = Datatype tyname name uni a -> TyVarInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
Datatype tyname name uni a -> TyVarInfo tyname name uni a
DatatypeTyVar Datatype tyname name uni a
d
        in UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty (tyname
-> TyVarInfo tyname name uni a
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName tyname
tyname TyVarInfo tyname name uni a
info UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty)
      matcherInfo :: VarsInfo tyname name uni a
matcherInfo =
        let info :: VarInfo tyname name uni a
info = tyname -> VarInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
tyname -> VarInfo tyname name uni a
DatatypeMatcher tyname
tyname
        in UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo (name
-> VarInfo tyname name uni a
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
matcher VarInfo tyname name uni a
forall {name} {uni :: * -> *} {a}. VarInfo tyname name uni a
info UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty) UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty
      constrInfo :: Int -> VarDecl tyname name uni ann -> VarsInfo tyname name uni a
constrInfo Int
i (VarDecl ann
_ name
n Type tyname uni ann
_) =
        let info :: VarInfo tyname name uni a
info = Int -> tyname -> VarInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
Int -> tyname -> VarInfo tyname name uni a
DatatypeConstructor Int
i tyname
tyname
        in UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
forall tyname name (uni :: * -> *) a.
UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TypeUnique (TyVarInfo tyname name uni a)
-> VarsInfo tyname name uni a
VarsInfo (name
-> VarInfo tyname name uni a
-> UniqueMap TermUnique (VarInfo tyname name uni a)
-> UniqueMap TermUnique (VarInfo tyname name uni a)
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
UMap.insertByName name
n VarInfo tyname name uni a
forall {name} {uni :: * -> *} {a}. VarInfo tyname name uni a
info UniqueMap TermUnique (VarInfo tyname name uni a)
forall a. Monoid a => a
mempty) UniqueMap TypeUnique (TyVarInfo tyname name uni a)
forall a. Monoid a => a
mempty
    in VarsInfo tyname name uni a
dtInfo VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> VarsInfo tyname name uni a
forall {name} {uni :: * -> *} {a}. VarsInfo tyname name uni a
matcherInfo VarsInfo tyname name uni a
-> VarsInfo tyname name uni a -> VarsInfo tyname name uni a
forall a. Semigroup a => a -> a -> a
<> (Int -> VarDecl tyname name uni a -> VarsInfo tyname name uni a)
-> [VarDecl tyname name uni a] -> VarsInfo tyname name uni a
forall m a. Monoid m => (Int -> a -> m) -> [a] -> m
forall i (f :: * -> *) m a.
(FoldableWithIndex i f, Monoid m) =>
(i -> a -> m) -> f a -> m
ifoldMap Int -> VarDecl tyname name uni a -> VarsInfo tyname name uni a
forall {name} {tyname} {uni :: * -> *} {ann} {name} {uni :: * -> *}
       {a}.
HasUnique name TermUnique =>
Int -> VarDecl tyname name uni ann -> VarsInfo tyname name uni a
constrInfo [VarDecl tyname name uni a]
constrs

-- | Get the arities of the constructors for the given datatype name.
getConstructorArities
  :: (PLC.HasUnique name PLC.TermUnique, PLC.HasUnique tyname PLC.TypeUnique)
  => tyname
  -> VarsInfo tyname name uni a
  -> Maybe [Arity]
getConstructorArities :: forall name tyname (uni :: * -> *) a.
(HasUnique name TermUnique, HasUnique tyname TypeUnique) =>
tyname -> VarsInfo tyname name uni a -> Maybe [Arity]
getConstructorArities tyname
tn VarsInfo tyname name uni a
vinfo |
  Just (DatatypeTyVar (Datatype a
_ TyVarDecl tyname a
_ [TyVarDecl tyname a]
_ name
_ [VarDecl tyname name uni a]
constrs)) <- tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
tyname
-> VarsInfo tyname name uni a
-> Maybe (TyVarInfo tyname name uni a)
lookupTyVarInfo tyname
tn VarsInfo tyname name uni a
vinfo
  , Just [Arity]
constrArities <- [VarDecl tyname name uni a]
-> (VarDecl tyname name uni a -> Maybe Arity) -> Maybe [Arity]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [VarDecl tyname name uni a]
constrs ((VarDecl tyname name uni a -> Maybe Arity) -> Maybe [Arity])
-> (VarDecl tyname name uni a -> Maybe Arity) -> Maybe [Arity]
forall a b. (a -> b) -> a -> b
$ \VarDecl tyname name uni a
c -> do
      VarInfo tyname name uni a
cInfo <- name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
forall name tyname (uni :: * -> *) a.
HasUnique name TermUnique =>
name
-> VarsInfo tyname name uni a -> Maybe (VarInfo tyname name uni a)
lookupVarInfo (VarDecl tyname name uni a -> name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName VarDecl tyname name uni a
c) VarsInfo tyname name uni a
vinfo
      VarInfo tyname name uni a
-> VarsInfo tyname name uni a -> Maybe Arity
forall tyname name (uni :: * -> *) a.
HasUnique tyname TypeUnique =>
VarInfo tyname name uni a
-> VarsInfo tyname name uni a -> Maybe Arity
varInfoArity VarInfo tyname name uni a
cInfo VarsInfo tyname name uni a
vinfo
  = [Arity] -> Maybe [Arity]
forall a. a -> Maybe a
Just [Arity]
constrArities
  | Bool
otherwise = Maybe [Arity]
forall a. Maybe a
Nothing