{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

module PlutusIR.Subst (
  fvTerm,
  ftvTerm,
  fvBinding,
  ftvBinding,
  ftvTy,
  vTerm,
  tvTerm,
  tvTy,
) where

import PlutusCore.Core (typeTyVars)
import PlutusCore.Core qualified as PLC
import PlutusCore.Name.Unique qualified as PLC
import PlutusCore.Name.UniqueSet qualified as USet
import PlutusCore.Subst (ftvTy, ftvTyCtx, tvTy)

import PlutusIR.Core

import Control.Lens
import Control.Lens.Unsound qualified as Unsound
import Data.Traversable (mapAccumL)
import PlutusCore.Name.Unique (HasUnique, TermUnique, TypeUnique)
import PlutusCore.Name.UniqueSet (UniqueSet)

-- | Get all the free term variables in a PIR term.
fvTerm :: (HasUnique name TermUnique) => Traversal' (Term tyname name uni fun ann) name
fvTerm :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Traversal' (Term tyname name uni fun ann) name
fvTerm = UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
forall a. Monoid a => a
mempty

fvTermCtx
  :: forall tyname name uni fun ann .
  (HasUnique name TermUnique) =>
  UniqueSet TermUnique ->
  Traversal' (Term tyname name uni fun ann) name
fvTermCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound name -> f name
f = \case
  Let ann
a r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
    let fvLinearScope :: UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
fvLinearScope UniqueSet TermUnique
boundSoFar Binding tyname name uni fun ann
b =
          (UniqueSet TermUnique
boundSoFar UniqueSet TermUnique
-> UniqueSet TermUnique -> UniqueSet TermUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
  (UniqueSet TermUnique) (Binding tyname name uni fun ann) name
-> Binding tyname name uni fun ann -> UniqueSet TermUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting
  (UniqueSet TermUnique) (Binding tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(name -> f name)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingNames Binding tyname name uni fun ann
b, UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
boundSoFar name -> f name
f Binding tyname name uni fun ann
b)
        (UniqueSet TermUnique
boundAtTheEnd, NonEmpty (f (Binding tyname name uni fun ann))
bs') = (UniqueSet TermUnique
 -> Binding tyname name uni fun ann
 -> (UniqueSet TermUnique, f (Binding tyname name uni fun ann)))
-> UniqueSet TermUnique
-> NonEmpty (Binding tyname name uni fun ann)
-> (UniqueSet TermUnique,
    NonEmpty (f (Binding tyname name uni fun ann)))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
forall {tyname} {uni :: * -> *} {fun} {ann}.
UniqueSet TermUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TermUnique, f (Binding tyname name uni fun ann))
fvLinearScope UniqueSet TermUnique
bound NonEmpty (Binding tyname name uni fun ann)
bs
     in ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
a Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (f (Binding tyname name uni fun ann))
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
NonEmpty (f a) -> f (NonEmpty a)
sequenceA NonEmpty (f (Binding tyname name uni fun ann))
bs' f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
boundAtTheEnd name -> f name
f Term tyname name uni fun ann
tIn
  Let ann
a r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
    let bound' :: UniqueSet TermUnique
bound' = UniqueSet TermUnique
bound UniqueSet TermUnique
-> UniqueSet TermUnique -> UniqueSet TermUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
  (UniqueSet TermUnique)
  (NonEmpty (Binding tyname name uni fun ann))
  name
-> NonEmpty (Binding tyname name uni fun ann)
-> UniqueSet TermUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((Binding tyname name uni fun ann
 -> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
     (UniqueSet TermUnique) (NonEmpty (Binding tyname name uni fun ann))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
  Int
  (NonEmpty (Binding tyname name uni fun ann))
  (NonEmpty (Binding tyname name uni fun ann))
  (Binding tyname name uni fun ann)
  (Binding tyname name uni fun ann)
traversed ((Binding tyname name uni fun ann
  -> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> Const
      (UniqueSet TermUnique)
      (NonEmpty (Binding tyname name uni fun ann)))
-> ((name -> Const (UniqueSet TermUnique) name)
    -> Binding tyname name uni fun ann
    -> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann))
-> Getting
     (UniqueSet TermUnique)
     (NonEmpty (Binding tyname name uni fun ann))
     name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> Const (UniqueSet TermUnique) name)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TermUnique) (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(name -> f name)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingNames) NonEmpty (Binding tyname name uni fun ann)
bs
     in ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
a Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse (UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
bound name -> f name
f) NonEmpty (Binding tyname name uni fun ann)
bs f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound' name -> f name
f Term tyname name uni fun ann
tIn
  Var ann
a name
n -> ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var ann
a (name -> Term tyname name uni fun ann)
-> f name -> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (if name -> UniqueSet TermUnique -> Bool
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> Bool
USet.memberByName name
n UniqueSet TermUnique
bound then name -> f name
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure name
n else name -> f name
f name
n)
  LamAbs ann
a name
n Type tyname uni ann
ty Term tyname name uni fun ann
t -> ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs ann
a name
n Type tyname uni ann
ty (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx (name -> UniqueSet TermUnique -> UniqueSet TermUnique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName name
n UniqueSet TermUnique
bound) name -> f name
f Term tyname name uni fun ann
t
  Term tyname name uni fun ann
t -> ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
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 ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((name -> f name)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound) name -> f name
f Term tyname name uni fun ann
t

-- | Get all the free type variables in a PIR term.
ftvTerm :: (HasUnique tyname TypeUnique) => Traversal' (Term tyname name uni fun ann) tyname
ftvTerm :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Traversal' (Term tyname name uni fun ann) tyname
ftvTerm = UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
forall a. Monoid a => a
mempty

ftvTermCtx ::
  (HasUnique tyname TypeUnique) =>
  UniqueSet TypeUnique ->
  Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound tyname -> f tyname
f = \case
  Let ann
a r :: Recursivity
r@Recursivity
NonRec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
    let ftvLinearScope :: UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
ftvLinearScope UniqueSet TypeUnique
bound' Binding tyname name uni fun ann
b =
          (UniqueSet TypeUnique
bound' UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
  (UniqueSet TypeUnique) (Binding tyname name uni fun ann) tyname
-> Binding tyname name uni fun ann -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting
  (UniqueSet TypeUnique) (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingTyNames Binding tyname name uni fun ann
b, Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound' tyname -> f tyname
f Binding tyname name uni fun ann
b)
        (UniqueSet TypeUnique
bound'', NonEmpty (f (Binding tyname name uni fun ann))
bs') = (UniqueSet TypeUnique
 -> Binding tyname name uni fun ann
 -> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann)))
-> UniqueSet TypeUnique
-> NonEmpty (Binding tyname name uni fun ann)
-> (UniqueSet TypeUnique,
    NonEmpty (f (Binding tyname name uni fun ann)))
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
forall {name} {uni :: * -> *} {fun} {ann}.
UniqueSet TypeUnique
-> Binding tyname name uni fun ann
-> (UniqueSet TypeUnique, f (Binding tyname name uni fun ann))
ftvLinearScope UniqueSet TypeUnique
bound NonEmpty (Binding tyname name uni fun ann)
bs
     in ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
a Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (f (Binding tyname name uni fun ann))
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
NonEmpty (f a) -> f (NonEmpty a)
sequenceA NonEmpty (f (Binding tyname name uni fun ann))
bs' f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound'' tyname -> f tyname
f Term tyname name uni fun ann
tIn
  Let ann
a r :: Recursivity
r@Recursivity
Rec NonEmpty (Binding tyname name uni fun ann)
bs Term tyname name uni fun ann
tIn ->
    let bound' :: UniqueSet TypeUnique
bound' = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` Getting
  (UniqueSet TypeUnique)
  (NonEmpty (Binding tyname name uni fun ann))
  tyname
-> NonEmpty (Binding tyname name uni fun ann)
-> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((Binding tyname name uni fun ann
 -> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> Const
     (UniqueSet TypeUnique) (NonEmpty (Binding tyname name uni fun ann))
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
  Int
  (NonEmpty (Binding tyname name uni fun ann))
  (NonEmpty (Binding tyname name uni fun ann))
  (Binding tyname name uni fun ann)
  (Binding tyname name uni fun ann)
traversed ((Binding tyname name uni fun ann
  -> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
 -> NonEmpty (Binding tyname name uni fun ann)
 -> Const
      (UniqueSet TypeUnique)
      (NonEmpty (Binding tyname name uni fun ann)))
-> ((tyname -> Const (UniqueSet TypeUnique) tyname)
    -> Binding tyname name uni fun ann
    -> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann))
-> Getting
     (UniqueSet TypeUnique)
     (NonEmpty (Binding tyname name uni fun ann))
     tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> Const (UniqueSet TypeUnique) tyname)
-> Binding tyname name uni fun ann
-> Const (UniqueSet TypeUnique) (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingTyNames) NonEmpty (Binding tyname name uni fun ann)
bs
     in ann
-> Recursivity
-> NonEmpty (Binding tyname name uni fun ann)
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let ann
a Recursivity
r (NonEmpty (Binding tyname name uni fun ann)
 -> Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
-> f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> NonEmpty (Binding tyname name uni fun ann)
-> f (NonEmpty (Binding tyname name uni fun ann))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> NonEmpty a -> f (NonEmpty b)
traverse (Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f) NonEmpty (Binding tyname name uni fun ann)
bs f (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound' tyname -> f tyname
f Term tyname name uni fun ann
tIn
  TyAbs ann
a tyname
tn Kind ann
k Term tyname name uni fun ann
t -> ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs ann
a tyname
tn Kind ann
k (Term tyname name uni fun ann -> Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
-> f (Term tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx (tyname -> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall name unique.
HasUnique name unique =>
name -> UniqueSet unique -> UniqueSet unique
USet.insertByName tyname
tn UniqueSet TypeUnique
bound) tyname -> f tyname
f Term tyname name uni fun ann
t
  -- sound because the subterms and subtypes are disjoint
  Term tyname name uni fun ann
t -> (((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
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 ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((tyname -> f tyname)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound) Traversal' (Term tyname name uni fun ann) tyname
-> Traversal' (Term tyname name uni fun ann) tyname
-> Traversal' (Term tyname name uni fun ann) tyname
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin` ((Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Term tyname name uni fun a -> f (Term tyname name uni fun a)
termSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((tyname -> f tyname)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
bound)) tyname -> f tyname
f Term tyname name uni fun ann
t

-- | Get all the free variables in a PIR single let-binding.
fvBinding :: (HasUnique name TermUnique) => Traversal' (Binding tyname name uni fun ann) name
fvBinding :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
Traversal' (Binding tyname name uni fun ann) name
fvBinding = UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
forall a. Monoid a => a
mempty

fvBindingCtx ::
  (HasUnique name TermUnique) =>
  UniqueSet TermUnique ->
  Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx :: forall name tyname (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Binding tyname name uni fun ann) name
fvBindingCtx UniqueSet TermUnique
bound = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> ((name -> f name)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
forall tyname name (uni :: * -> *) fun ann.
HasUnique name TermUnique =>
UniqueSet TermUnique
-> Traversal' (Term tyname name uni fun ann) name
fvTermCtx UniqueSet TermUnique
bound

-- | Get all the free type variables in a PIR single let-binding.
ftvBinding ::
  (HasUnique tyname TypeUnique) =>
  Recursivity ->
  Traversal' (Binding tyname name uni fun ann) tyname
ftvBinding :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity -> Traversal' (Binding tyname name uni fun ann) tyname
ftvBinding Recursivity
r = Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
forall a. Monoid a => a
mempty

ftvBindingCtx ::
  (HasUnique tyname TypeUnique) =>
  Recursivity ->
  UniqueSet TypeUnique ->
  Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx :: forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Binding tyname name uni fun ann) tyname
ftvBindingCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f = \case
  DatatypeBind ann
a Datatype tyname name uni ann
d -> ann
-> Datatype tyname name uni ann -> Binding tyname name uni fun ann
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind ann
a (Datatype tyname name uni ann -> Binding tyname name uni fun ann)
-> f (Datatype tyname name uni ann)
-> f (Binding tyname name uni fun ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
forall tyname name (uni :: * -> *) ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f Datatype tyname name uni ann
d
  -- sound because the subterms and subtypes are disjoint
  Binding tyname name uni fun ann
b ->
    ( ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Term tyname name uni fun a -> f (Term tyname name uni fun a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubterms ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> ((tyname -> f tyname)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
forall tyname name (uni :: * -> *) fun ann.
HasUnique tyname TypeUnique =>
UniqueSet TypeUnique
-> Traversal' (Term tyname name uni fun ann) tyname
ftvTermCtx UniqueSet TypeUnique
bound)
        (forall {f :: * -> *}.
 Applicative f =>
 (tyname -> f tyname)
 -> Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> (forall {f :: * -> *}.
    Applicative f =>
    (tyname -> f tyname)
    -> Binding tyname name uni fun ann
    -> f (Binding tyname name uni fun ann))
-> forall {f :: * -> *}.
   Applicative f =>
   (tyname -> f tyname)
   -> Binding tyname name uni fun ann
   -> f (Binding tyname name uni fun ann)
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin` ((Type tyname uni ann -> f (Type tyname uni ann))
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Binding tyname name uni fun a
-> f (Binding tyname name uni fun a)
bindingSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Binding tyname name uni fun ann
 -> f (Binding tyname name uni fun ann))
-> ((tyname -> f tyname)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Binding tyname name uni fun ann
-> f (Binding tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
bound)
    )
      tyname -> f tyname
f
      Binding tyname name uni fun ann
b

ftvDatatypeCtx ::
  (HasUnique tyname TypeUnique) =>
  Recursivity ->
  UniqueSet TypeUnique ->
  Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx :: forall tyname name (uni :: * -> *) ann.
HasUnique tyname TypeUnique =>
Recursivity
-> UniqueSet TypeUnique
-> Traversal' (Datatype tyname name uni ann) tyname
ftvDatatypeCtx Recursivity
r UniqueSet TypeUnique
bound tyname -> f tyname
f d :: Datatype tyname name uni ann
d@(Datatype ann
a TyVarDecl tyname ann
tyconstr [TyVarDecl tyname ann]
tyvars name
destr [VarDecl tyname name uni ann]
constrs) =
  let
    tyConstr :: UniqueSet TypeUnique
tyConstr = Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
-> TyVarDecl tyname ann -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName TyVarDecl tyname ann
tyconstr
    tyVars :: UniqueSet TypeUnique
tyVars = Getting (UniqueSet TypeUnique) [TyVarDecl tyname ann] tyname
-> [TyVarDecl tyname ann] -> UniqueSet TypeUnique
forall name unique s.
HasUnique name unique =>
Getting (UniqueSet unique) s name -> s -> UniqueSet unique
USet.setOfByName ((TyVarDecl tyname ann
 -> Const (UniqueSet TypeUnique) (TyVarDecl tyname ann))
-> [TyVarDecl tyname ann]
-> Const (UniqueSet TypeUnique) [TyVarDecl tyname ann]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
  Int
  [TyVarDecl tyname ann]
  [TyVarDecl tyname ann]
  (TyVarDecl tyname ann)
  (TyVarDecl tyname ann)
traversed ((TyVarDecl tyname ann
  -> Const (UniqueSet TypeUnique) (TyVarDecl tyname ann))
 -> [TyVarDecl tyname ann]
 -> Const (UniqueSet TypeUnique) [TyVarDecl tyname ann])
-> Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
-> Getting (UniqueSet TypeUnique) [TyVarDecl tyname ann] tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (UniqueSet TypeUnique) (TyVarDecl tyname ann) tyname
forall tyname1 ann tyname2 (f :: * -> *).
Functor f =>
(tyname1 -> f tyname2)
-> TyVarDecl tyname1 ann -> f (TyVarDecl tyname2 ann)
PLC.tyVarDeclName) [TyVarDecl tyname ann]
tyvars
    allBound :: UniqueSet TypeUnique
allBound = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyConstr UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyVars
    varsBound :: UniqueSet TypeUnique
varsBound = UniqueSet TypeUnique
bound UniqueSet TypeUnique
-> UniqueSet TypeUnique -> UniqueSet TypeUnique
forall unique.
UniqueSet unique -> UniqueSet unique -> UniqueSet unique
`USet.union` UniqueSet TypeUnique
tyVars
   in
    case Recursivity
r of
      -- recursive: introduced names are in scope throughout
      Recursivity
Rec -> ((Type tyname uni ann -> f (Type tyname uni ann))
-> Datatype tyname name uni ann -> f (Datatype tyname name uni ann)
forall tyname name (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Datatype tyname name uni a -> f (Datatype tyname name uni a)
datatypeSubtypes ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Datatype tyname name uni ann
 -> f (Datatype tyname name uni ann))
-> ((tyname -> f tyname)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Datatype tyname name uni ann
-> f (Datatype tyname name uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique -> Traversal' (Type tyname uni ann) tyname
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
allBound) tyname -> f tyname
f Datatype tyname name uni ann
d
      -- nonrecursive: type constructor is in scope only in the result type of the constructors
      Recursivity
NonRec ->
        let
          combinedTraversal :: (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
combinedTraversal =
            -- type arguments are in scope in the argument types
            ((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs ((Type tyname uni a -> f (Type tyname uni a))
 -> Type tyname uni a -> f (Type tyname uni a))
-> ((tyname -> f tyname)
    -> Type tyname uni a -> f (Type tyname uni a))
-> (tyname -> f tyname)
-> Type tyname uni a
-> f (Type tyname uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> forall {f :: * -> *}.
   Applicative f =>
   (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
varsBound)
              -- sound because the argument types and result type are disjoint
              (forall {f :: * -> *}.
 Applicative f =>
 (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a))
-> (forall {f :: * -> *}.
    Applicative f =>
    (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a))
-> forall {f :: * -> *}.
   Applicative f =>
   (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall s a. Traversal' s a -> Traversal' s a -> Traversal' s a
`Unsound.adjoin`
              -- type constructor and arguments are in scope in the result type
              ((Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes ((Type tyname uni a -> f (Type tyname uni a))
 -> Type tyname uni a -> f (Type tyname uni a))
-> ((tyname -> f tyname)
    -> Type tyname uni a -> f (Type tyname uni a))
-> (tyname -> f tyname)
-> Type tyname uni a
-> f (Type tyname uni a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueSet TypeUnique
-> forall {f :: * -> *}.
   Applicative f =>
   (tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
UniqueSet unique -> Traversal' (Type tyname uni ann) tyname
ftvTyCtx UniqueSet TypeUnique
allBound)
          constrs' :: f [VarDecl tyname name uni ann]
constrs' = LensLike
  f
  [VarDecl tyname name uni ann]
  [VarDecl tyname name uni ann]
  tyname
  tyname
-> LensLike
     f
     [VarDecl tyname name uni ann]
     [VarDecl tyname name uni ann]
     tyname
     tyname
forall (f :: * -> *) s t a b.
LensLike f s t a b -> LensLike f s t a b
traverseOf ((VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> [VarDecl tyname name uni ann] -> f [VarDecl tyname name uni ann]
forall (f :: * -> *) a b.
Traversable f =>
IndexedTraversal Int (f a) (f b) a b
IndexedTraversal
  Int
  [VarDecl tyname name uni ann]
  [VarDecl tyname name uni ann]
  (VarDecl tyname name uni ann)
  (VarDecl tyname name uni ann)
traversed ((VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
 -> [VarDecl tyname name uni ann]
 -> f [VarDecl tyname name uni ann])
-> ((tyname -> f tyname)
    -> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> LensLike
     f
     [VarDecl tyname name uni ann]
     [VarDecl tyname name uni ann]
     tyname
     tyname
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann -> f (Type tyname uni ann))
-> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann)
forall tyname1 name (uni1 :: * -> *) ann tyname2 (uni2 :: * -> *)
       (f :: * -> *).
Functor f =>
(Type tyname1 uni1 ann -> f (Type tyname2 uni2 ann))
-> VarDecl tyname1 name uni1 ann
-> f (VarDecl tyname2 name uni2 ann)
PLC.varDeclType ((Type tyname uni ann -> f (Type tyname uni ann))
 -> VarDecl tyname name uni ann -> f (VarDecl tyname name uni ann))
-> ((tyname -> f tyname)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> VarDecl tyname name uni ann
-> f (VarDecl tyname name uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall {uni :: * -> *} {a}.
(tyname -> f tyname) -> Type tyname uni a -> f (Type tyname uni a)
combinedTraversal) tyname -> f tyname
f [VarDecl tyname name uni ann]
constrs
         in
          ann
-> TyVarDecl tyname ann
-> [TyVarDecl tyname ann]
-> name
-> [VarDecl tyname name uni ann]
-> Datatype tyname name uni ann
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype ann
a TyVarDecl tyname ann
tyconstr [TyVarDecl tyname ann]
tyvars name
destr ([VarDecl tyname name uni ann] -> Datatype tyname name uni ann)
-> f [VarDecl tyname name uni ann]
-> f (Datatype tyname name uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f [VarDecl tyname name uni ann]
constrs'

-- | Traverse the arguments of a function type (nothing if the type is not a function type).
funArgs :: Traversal' (Type tyname uni a) (Type tyname uni a)
funArgs :: forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs Type tyname uni a -> f (Type tyname uni a)
f = \case
  TyFun a
a Type tyname uni a
dom cod :: Type tyname uni a
cod@TyFun{} -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a (Type tyname uni a -> Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a)
-> f (Type tyname uni a -> Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
dom f (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Applicative f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funArgs Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
cod
  TyFun a
a Type tyname uni a
dom Type tyname uni a
res         -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a (Type tyname uni a -> Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a)
-> f (Type tyname uni a -> Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
dom f (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname uni a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type tyname uni a -> f (Type tyname uni a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
res
  Type tyname uni a
t                       -> Type tyname uni a -> f (Type tyname uni a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type tyname uni a
t

-- | Traverse the result type of a function type (the type itself if it is not a function type).
funRes :: Lens' (Type tyname uni a) (Type tyname uni a)
funRes :: forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes Type tyname uni a -> f (Type tyname uni a)
f = \case
  TyFun a
a Type tyname uni a
dom Type tyname uni a
cod -> a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun a
a Type tyname uni a
dom (Type tyname uni a -> Type tyname uni a)
-> f (Type tyname uni a) -> f (Type tyname uni a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
forall tyname (uni :: * -> *) a (f :: * -> *).
Functor f =>
(Type tyname uni a -> f (Type tyname uni a))
-> Type tyname uni a -> f (Type tyname uni a)
funRes Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
cod
  Type tyname uni a
t               -> Type tyname uni a -> f (Type tyname uni a)
f Type tyname uni a
t

-- TODO: these could be Traversals
-- | Get all the term variables in a term.
vTerm :: Fold (Term tyname name uni fun ann) name
vTerm :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
vTerm = (Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtermsDeep ((Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((name -> f name)
    -> Term tyname name uni fun ann
    -> f (Term tyname name uni fun ann))
-> (name -> f name)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(name -> f name)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termVars

-- | Get all the type variables in a term.
tvTerm :: Fold (Term tyname name uni fun ann) tyname
tvTerm :: forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(tyname -> f tyname)
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
tvTerm = (Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
(Contravariant f, Applicative f) =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypesDeep ((Type tyname uni ann -> f (Type tyname uni ann))
 -> Term tyname name uni fun ann
 -> f (Term tyname name uni fun ann))
-> ((tyname -> f tyname)
    -> Type tyname uni ann -> f (Type tyname uni ann))
-> (tyname -> f tyname)
-> Term tyname name uni fun ann
-> f (Term tyname name uni fun ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
forall tyname (uni :: * -> *) ann (f :: * -> *).
Applicative f =>
(tyname -> f tyname)
-> Type tyname uni ann -> f (Type tyname uni ann)
typeTyVars