{-# 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,
    visit,
    visitPure,
  )
where

import Data.Bifoldable
import Data.Bifunctor
import Data.Foldable (toList)
import Data.Functor.Identity (Identity (..))
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Maybe (fromMaybe)
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
renames0 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 implementation.
--
-- subvs0 counts the number of variables being renamed to a particular
-- variable
--
-- rnv0 is the variable renaming map.
renames0 ::
  (Var v, Ord v, Bifunctor f, Bifoldable f) =>
  Map v Int ->
  Map v v ->
  Term f v ->
  Term f v
renames0 :: forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v Int -> Map v v -> Term f v -> Term f v
renames0 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
renames0 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
renames0 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)

-- Simultaneous variable renaming.
renames ::
  (Var v, Ord v, Bifunctor f, Bifoldable f) =>
  Map v v ->
  Term f v ->
  Term f v
renames :: forall v (f :: * -> * -> *).
(Var v, Ord v, Bifunctor f, Bifoldable f) =>
Map v v -> Term f v -> Term f v
renames Map v v
rnv Term f v
tm = 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
renames0 Map v Int
subvs Map v v
rnv Term f v
tm
  where
    subvs :: Map v Int
subvs = (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 -> (v, Int)) -> [v] -> [(v, Int)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Int
1) ([v] -> Map v Int) -> [v] -> Map v Int
forall a b. (a -> b) -> a -> b
$ Map v v -> [v]
forall k a. Map k a -> [a]
Map.elems Map v v
rnv

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
renames0 (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

visit ::
  (Applicative g, Bifoldable f, Traversable (f v), Var v) =>
  (Term f v -> Maybe (g (Term f v))) ->
  Term f v ->
  g (Term f v)
visit :: forall (g :: * -> *) (f :: * -> * -> *) v.
(Applicative g, Bifoldable f, Traversable (f v), Var v) =>
(Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
visit Term f v -> Maybe (g (Term f v))
h Term f v
t = (g (Term f v) -> Maybe (g (Term f v)) -> g (Term f v))
-> Maybe (g (Term f v)) -> g (Term f v) -> g (Term f v)
forall a b c. (a -> b -> c) -> b -> a -> c
flip g (Term f v) -> Maybe (g (Term f v)) -> g (Term f v)
forall a. a -> Maybe a -> a
fromMaybe (Term f v -> Maybe (g (Term f v))
h Term f v
t) (g (Term f v) -> g (Term f v)) -> g (Term f v) -> g (Term f v)
forall a b. (a -> b) -> a -> b
$ case Term f v -> ABT f v
forall (f :: * -> * -> *) v. Term f v -> ABT f v
out Term f v
t of
  Abs v
x Term f v
e -> v -> Term f v -> Term f v
forall v (f :: * -> * -> *). Var v => v -> Term f v -> Term f v
TAbs v
x (Term f v -> Term f v) -> g (Term f v) -> g (Term f v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
forall (g :: * -> *) (f :: * -> * -> *) v.
(Applicative g, Bifoldable f, Traversable (f v), Var v) =>
(Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
visit Term f v -> Maybe (g (Term f v))
h Term f v
e
  Tm f v (Term f v)
body -> 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) -> g (f v (Term f v)) -> g (Term f v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term f v -> g (Term f v)) -> f v (Term f v) -> g (f v (Term f v))
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) -> f v a -> f (f v b)
traverse ((Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
forall (g :: * -> *) (f :: * -> * -> *) v.
(Applicative g, Bifoldable f, Traversable (f v), Var v) =>
(Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
visit Term f v -> Maybe (g (Term f v))
h) f v (Term f v)
body

visitPure ::
  (Bifoldable f, Traversable (f v), Var v) =>
  (Term f v -> Maybe (Term f v)) ->
  Term f v ->
  Term f v
visitPure :: forall (f :: * -> * -> *) v.
(Bifoldable f, Traversable (f v), Var v) =>
(Term f v -> Maybe (Term f v)) -> Term f v -> Term f v
visitPure Term f v -> Maybe (Term f v)
h = Identity (Term f v) -> Term f v
forall a. Identity a -> a
runIdentity (Identity (Term f v) -> Term f v)
-> (Term f v -> Identity (Term f v)) -> Term f v -> Term f v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term f v -> Maybe (Identity (Term f v)))
-> Term f v -> Identity (Term f v)
forall (g :: * -> *) (f :: * -> * -> *) v.
(Applicative g, Bifoldable f, Traversable (f v), Var v) =>
(Term f v -> Maybe (g (Term f v))) -> Term f v -> g (Term f v)
visit ((Term f v -> Identity (Term f v))
-> Maybe (Term f v) -> Maybe (Identity (Term f v))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term f v -> Identity (Term f v)
forall a. a -> Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Term f v) -> Maybe (Identity (Term f v)))
-> (Term f v -> Maybe (Term f v))
-> Term f v
-> Maybe (Identity (Term f v))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f v -> Maybe (Term f v)
h)