{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Unison.ABT.Normalized
  ( ABT (..),
    Term (.., TAbs, TTm, TAbss),
    Align (..),
    alpha,
    renames,
    rename,
    transform,
  )
where

import Data.Bifoldable
import Data.Bifunctor
import Data.Foldable (toList)
-- import Data.Bitraversable

import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Unison.ABT (Var (..))

-- ABTs with support for 'normalized' structure where only variables
-- may occur at some positions. This is accomplished by passing the
-- variable type to the base functor.
data ABT f v
  = Abs v (Term f v)
  | Tm (f v (Term f v))

data Term f v = Term
  { forall (f :: * -> * -> *) v. Term f v -> Set v
freeVars :: Set v,
    forall (f :: * -> * -> *) v. Term f v -> ABT f v
out :: ABT f v
  }

instance
  (forall a b. (Show a) => (Show b) => Show (f a b), Show v) =>
  Show (ABT f v)
  where
  showsPrec :: Int -> ABT f v -> ShowS
showsPrec Int
p ABT f v
a = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ case ABT f v
a of
    Abs v
v Term f v
tm ->
      String -> ShowS
showString String
"Abs "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 v
v
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" "
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term f v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Term f v
tm
    Tm f v (Term f v)
e -> String -> ShowS
showString String
"Tm " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f v (Term f v) -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 f v (Term f v)
e

instance
  (forall a b. (Show a) => (Show b) => Show (f a b), Show v) =>
  Show (Term f v)
  where
  showsPrec :: Int -> Term f v -> ShowS
showsPrec Int
p (Term Set v
_ ABT f v
e) =
    Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Term " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ABT f v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 ABT f v
e

instance
  (forall a b. (Eq a) => (Eq b) => Eq (f a b), Bifunctor f, Bifoldable f, Var v) =>
  Eq (ABT f v)
  where
  Abs v
v1 Term f v
e1 == :: ABT f v -> ABT f v -> Bool
== Abs v
v2 Term f v
e2
    | v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 = Term f v
e1 Term f v -> Term f v -> Bool
forall a. Eq a => a -> a -> Bool
== Term f v
e2
    | Bool
otherwise = Term f v
e1 Term f v -> Term f v -> Bool
forall a. Eq a => a -> a -> Bool
== v -> v -> Term f v -> Term f v
forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
v -> v -> Term f v -> Term f v
rename v
v2 v
v1 Term f v
e2
  Tm f v (Term f v)
e1 == Tm f v (Term f v)
e2 = f v (Term f v)
e1 f v (Term f v) -> f v (Term f v) -> Bool
forall a. Eq a => a -> a -> Bool
== f v (Term f v)
e2
  ABT f v
_ == ABT f v
_ = Bool
False

instance
  (forall a b. (Eq a) => (Eq b) => Eq (f a b), Bifunctor f, Bifoldable f, Var v) =>
  Eq (Term f v)
  where
  Term Set v
_ ABT f v
abt1 == :: Term f v -> Term f v -> Bool
== Term Set v
_ ABT f v
abt2 = ABT f v
abt1 ABT f v -> ABT f v -> Bool
forall a. Eq a => a -> a -> Bool
== ABT f v
abt2

pattern TAbs :: (Var v) => v -> Term f v -> Term f v
pattern $mTAbs :: forall {r} {v} {f :: * -> * -> *}.
Var v =>
Term f v -> (v -> Term f v -> r) -> ((# #) -> r) -> r
$bTAbs :: forall v (f :: * -> * -> *). Var v => v -> Term f v -> Term f v
TAbs u bd <-
  Term _ (Abs u bd)
  where
    TAbs v
u Term f v
bd = Set v -> ABT f v -> Term f v
forall (f :: * -> * -> *) v. Set v -> ABT f v -> Term f v
Term (v -> Set v -> Set v
forall a. Ord a => a -> Set a -> Set a
Set.delete v
u (Term f v -> Set v
forall (f :: * -> * -> *) v. Term f v -> Set v
freeVars Term f v
bd)) (v -> Term f v -> ABT f v
forall (f :: * -> * -> *) v. v -> Term f v -> ABT f v
Abs v
u Term f v
bd)

pattern TTm :: (Var v, Bifoldable f) => f v (Term f v) -> Term f v
pattern $mTTm :: forall {r} {v} {f :: * -> * -> *}.
(Var v, Bifoldable f) =>
Term f v -> (f v (Term f v) -> r) -> ((# #) -> r) -> r
$bTTm :: forall v (f :: * -> * -> *).
(Var v, Bifoldable f) =>
f v (Term f v) -> Term f v
TTm bd <-
  Term _ (Tm bd)
  where
    TTm f v (Term f v)
bd = Set v -> ABT f v -> Term f v
forall (f :: * -> * -> *) v. Set v -> ABT f v -> Term f v
Term ((v -> Set v) -> (Term f v -> Set v) -> f v (Term f v) -> Set v
forall m a b. Monoid m => (a -> m) -> (b -> m) -> f a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap v -> Set v
forall a. a -> Set a
Set.singleton Term f v -> Set v
forall (f :: * -> * -> *) v. Term f v -> Set v
freeVars f v (Term f v)
bd) (f v (Term f v) -> ABT f v
forall (f :: * -> * -> *) v. f v (Term f v) -> ABT f v
Tm f v (Term f v)
bd)

{-# COMPLETE TAbs, TTm #-}

class (Bifoldable f, Bifunctor f) => Align f where
  align ::
    (Applicative g) =>
    (vl -> vr -> g vs) ->
    (el -> er -> g es) ->
    f vl el ->
    f vr er ->
    Maybe (g (f vs es))

alphaErr ::
  (Align f) => (Var v) => Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) a
alphaErr :: forall (f :: * -> * -> *) v a.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) a
alphaErr Map v v
un Term f v
tml Term f v
tmr = (Term f v, Term f v) -> Either (Term f v, Term f v) a
forall a b. a -> Either a b
Left (Term f v
tml, Map v Int -> Map v v -> Term f v -> Term f v
forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames Map v Int
count Map v v
un Term f v
tmr)
  where
    count :: Map v Int
count = (Int -> Int -> Int) -> [(v, Int)] -> Map v Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([(v, Int)] -> Map v Int)
-> ([v] -> [(v, Int)]) -> [v] -> Map v Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([v] -> [Int] -> [(v, Int)]) -> [Int] -> [v] -> [(v, Int)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [v] -> [Int] -> [(v, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1, Int
1 ..] ([v] -> Map v Int) -> [v] -> Map v Int
forall a b. (a -> b) -> a -> b
$ Map v v -> [v]
forall a. Map v a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Map v v
un

-- Checks if two terms are equal up to a given variable renaming. The
-- renaming should map variables in the right hand term to the
-- equivalent variable in the left hand term.
alpha :: (Align f) => (Var v) => Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
alpha :: forall (f :: * -> * -> *) v.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
alpha Map v v
un (TAbs v
u Term f v
tml) (TAbs v
v Term f v
tmr) =
  Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
forall (f :: * -> * -> *) v.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
alpha (v -> v -> Map v v -> Map v v
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v v
u ((v -> Bool) -> Map v v -> Map v v
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
u) Map v v
un)) Term f v
tml Term f v
tmr
alpha Map v v
un tml :: Term f v
tml@(TTm f v (Term f v)
bdl) tmr :: Term f v
tmr@(TTm f v (Term f v)
bdr)
  | Just Either (Term f v, Term f v) (f () ())
sub <- (v -> v -> Either (Term f v, Term f v) ())
-> (Term f v -> Term f v -> Either (Term f v, Term f v) ())
-> f v (Term f v)
-> f v (Term f v)
-> Maybe (Either (Term f v, Term f v) (f () ()))
forall (g :: * -> *) vl vr vs el er es.
Applicative g =>
(vl -> vr -> g vs)
-> (el -> er -> g es) -> f vl el -> f vr er -> Maybe (g (f vs es))
forall (f :: * -> * -> *) (g :: * -> *) vl vr vs el er es.
(Align f, Applicative g) =>
(vl -> vr -> g vs)
-> (el -> er -> g es) -> f vl el -> f vr er -> Maybe (g (f vs es))
align v -> v -> Either (Term f v, Term f v) ()
av (Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
forall (f :: * -> * -> *) v.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
alpha Map v v
un) f v (Term f v)
bdl f v (Term f v)
bdr = () ()
-> Either (Term f v, Term f v) (f () ())
-> Either (Term f v, Term f v) ()
forall a b.
a -> Either (Term f v, Term f v) b -> Either (Term f v, Term f v) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Either (Term f v, Term f v) (f () ())
sub
  where
    av :: v -> v -> Either (Term f v, Term f v) ()
av v
u v
v
      | Bool -> (v -> Bool) -> Maybe v -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
u) (v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v v
un) = () -> Either (Term f v, Term f v) ()
forall a. a -> Either (Term f v, Term f v) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      | Bool
otherwise = Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
forall (f :: * -> * -> *) v a.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) a
alphaErr Map v v
un Term f v
tml Term f v
tmr
alpha Map v v
un Term f v
tml Term f v
tmr = Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) ()
forall (f :: * -> * -> *) v a.
(Align f, Var v) =>
Map v v -> Term f v -> Term f v -> Either (Term f v, Term f v) a
alphaErr Map v v
un Term f v
tml Term f v
tmr

unabss :: (Var v) => Term f v -> ([v], Term f v)
unabss :: forall v (f :: * -> * -> *). Var v => Term f v -> ([v], Term f v)
unabss (TAbs v
v (Term f v -> ([v], Term f v)
forall v (f :: * -> * -> *). Var v => Term f v -> ([v], Term f v)
unabss -> ([v]
vs, Term f v
bd))) = (v
v v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs, Term f v
bd)
unabss Term f v
bd = ([], Term f v
bd)

pattern TAbss :: (Var v) => [v] -> Term f v -> Term f v
pattern $mTAbss :: forall {r} {v} {f :: * -> * -> *}.
Var v =>
Term f v -> ([v] -> Term f v -> r) -> ((# #) -> r) -> r
$bTAbss :: forall v (f :: * -> * -> *). Var v => [v] -> Term f v -> Term f v
TAbss vs bd <-
  (unabss -> (vs, bd))
  where
    TAbss [v]
vs Term f v
bd = (v -> Term f v -> Term f v) -> Term f v -> [v] -> Term f v
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr v -> Term f v -> Term f v
forall v (f :: * -> * -> *). Var v => v -> Term f v -> Term f v
TAbs Term f v
bd [v]
vs

{-# COMPLETE TAbss #-}

-- Simultaneous variable renaming.
--
-- subvs0 counts the number of variables being renamed to a particular
-- variable
--
-- rnv0 is the variable renaming map.
renames ::
  (Var v, Ord v, Bifunctor f, Bifoldable f) =>
  Map v Int ->
  Map v v ->
  Term f v ->
  Term f v
renames :: forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames Map v Int
subvs0 Map v v
rnv0 Term f v
tm = case Term f v
tm of
  TAbs v
u Term f v
body
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map v v -> Bool
forall k a. Map k a -> Bool
Map.null Map v v
rnv' -> v -> Term f v -> Term f v
forall v (f :: * -> * -> *). Var v => v -> Term f v -> Term f v
TAbs v
u' (Map v Int -> Map v v -> Term f v -> Term f v
forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames Map v Int
subvs' Map v v
rnv' Term f v
body)
    where
      rnv' :: Map v v
rnv' = (Maybe v -> Maybe v) -> v -> Map v v -> Map v v
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (Maybe v -> Maybe v -> Maybe v
forall a b. a -> b -> a
const (Maybe v -> Maybe v -> Maybe v) -> Maybe v -> Maybe v -> Maybe v
forall a b. (a -> b) -> a -> b
$ Maybe v
adjustment) v
u Map v v
rnv
      -- if u is in the set of variables we're substituting in, it
      -- needs to be renamed to avoid capturing things.
      u' :: v
u'
        | v
u v -> Map v Int -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map v Int
subvs = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn (Set v
fvs Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Map v Int -> Set v
forall k a. Map k a -> Set k
Map.keysSet Map v Int
subvs) v
u
        | Bool
otherwise = v
u

      -- if u needs to be renamed to avoid capturing subvs
      -- and u actually occurs in the body, then add it to
      -- the substitutions
      (Maybe v
adjustment, Map v Int
subvs')
        | v
u v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
u' Bool -> Bool -> Bool
&& v
u v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
fvs = (v -> Maybe v
forall a. a -> Maybe a
Just v
u', (Int -> Int -> Int) -> v -> Int -> Map v Int -> Map v Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) v
u' Int
1 Map v Int
subvs)
        | Bool
otherwise = (Maybe v
forall a. Maybe a
Nothing, Map v Int
subvs)
  TTm f v (Term f v)
body
    | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map v v -> Bool
forall k a. Map k a -> Bool
Map.null Map v v
rnv ->
        f v (Term f v) -> Term f v
forall v (f :: * -> * -> *).
(Var v, Bifoldable f) =>
f v (Term f v) -> Term f v
TTm (f v (Term f v) -> Term f v) -> f v (Term f v) -> Term f v
forall a b. (a -> b) -> a -> b
$ (v -> v)
-> (Term f v -> Term f v) -> f v (Term f v) -> f v (Term f v)
forall a b c d. (a -> b) -> (c -> d) -> f a c -> f b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (\v
u -> v -> v -> Map v v -> v
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault v
u v
u Map v v
rnv) (Map v Int -> Map v v -> Term f v -> Term f v
forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames Map v Int
subvs Map v v
rnv) f v (Term f v)
body
  Term f v
_ -> Term f v
tm
  where
    fvs :: Set v
fvs = Term f v -> Set v
forall (f :: * -> * -> *) v. Term f v -> Set v
freeVars Term f v
tm

    -- throw out irrelevant renamings
    rnv :: Map v v
rnv = Map v v -> Set v -> Map v v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map v v
rnv0 Set v
fvs

    -- decrement the variable usage counts for the renamings we threw away
    subvs :: Map v Int
subvs = (Map v Int -> v -> Map v Int) -> Map v Int -> Map v v -> Map v Int
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Map v Int -> v -> Map v Int
forall {k} {a}. (Ord k, Ord a, Num a) => Map k a -> k -> Map k a
decrement Map v Int
subvs0 (Map v v -> Map v Int) -> Map v v -> Map v Int
forall a b. (a -> b) -> a -> b
$ Map v v -> Set v -> Map v v
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys Map v v
rnv0 Set v
fvs
    decrement :: Map k a -> k -> Map k a
decrement Map k a
sv k
v = (a -> Maybe a) -> k -> Map k a -> Map k a
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update a -> Maybe a
forall {a}. (Ord a, Num a) => a -> Maybe a
drop k
v Map k a
sv
    drop :: a -> Maybe a
drop a
n
      | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
1 = Maybe a
forall a. Maybe a
Nothing
      | Bool
otherwise = a -> Maybe a
forall a. a -> Maybe a
Just (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

rename ::
  (Var v, Ord v, Bifunctor f, Bifoldable f) =>
  v ->
  v ->
  Term f v ->
  Term f v
rename :: forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
v -> v -> Term f v -> Term f v
rename v
old v
new = Map v Int -> Map v v -> Term f v -> Term f v
forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames (v -> Int -> Map v Int
forall k a. k -> a -> Map k a
Map.singleton v
new Int
1) (v -> v -> Map v v
forall k a. k -> a -> Map k a
Map.singleton v
old v
new)

transform ::
  (Var v, Bifunctor g, Bifoldable f, Bifoldable g) =>
  (forall a b. f a b -> g a b) ->
  Term f v ->
  Term g v
transform :: forall v (g :: * -> * -> *) (f :: * -> * -> *).
(Var v, Bifunctor g, Bifoldable f, Bifoldable g) =>
(forall a b. f a b -> g a b) -> Term f v -> Term g v
transform forall a b. f a b -> g a b
phi (TTm f v (Term f v)
body) = g v (Term g v) -> Term g v
forall v (f :: * -> * -> *).
(Var v, Bifoldable f) =>
f v (Term f v) -> Term f v
TTm (g v (Term g v) -> Term g v)
-> (g v (Term f v) -> g v (Term g v)) -> g v (Term f v) -> Term g v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v -> Term g v) -> g v (Term f v) -> g v (Term g v)
forall b c a. (b -> c) -> g a b -> g a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((forall a b. f a b -> g a b) -> Term f v -> Term g v
forall v (g :: * -> * -> *) (f :: * -> * -> *).
(Var v, Bifunctor g, Bifoldable f, Bifoldable g) =>
(forall a b. f a b -> g a b) -> Term f v -> Term g v
transform f a b -> g a b
forall a b. f a b -> g a b
phi) (g v (Term f v) -> Term g v) -> g v (Term f v) -> Term g v
forall a b. (a -> b) -> a -> b
$ f v (Term f v) -> g v (Term f v)
forall a b. f a b -> g a b
phi f v (Term f v)
body
transform forall a b. f a b -> g a b
phi (TAbs v
u Term f v
body) = v -> Term g v -> Term g v
forall v (f :: * -> * -> *). Var v => v -> Term f v -> Term f v
TAbs v
u (Term g v -> Term g v) -> Term g v -> Term g v
forall a b. (a -> b) -> a -> b
$ (forall a b. f a b -> g a b) -> Term f v -> Term g v
forall v (g :: * -> * -> *) (f :: * -> * -> *).
(Var v, Bifunctor g, Bifoldable f, Bifoldable g) =>
(forall a b. f a b -> g a b) -> Term f v -> Term g v
transform f a b -> g a b
forall a b. f a b -> g a b
phi Term f v
body