{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE UndecidableInstances  #-}
-- | This module defines a variation of
-- free scoped (relative) monads relying on the foil for
-- the scope-safe efficient handling of the binders.
--
-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).
module Control.Monad.Free.Foil where

import           Control.DeepSeq
import qualified Control.Monad.Foil.Internal as Foil
import qualified Control.Monad.Foil.Relative as Foil
import           Data.Bifoldable
import           Data.Bitraversable
import           Data.Bifunctor
import Data.ZipMatchK
import qualified Generics.Kind as Kind
import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:))
import           Data.Coerce                 (coerce)
import           Data.Map                    (Map)
import qualified Data.Map                    as Map
import           Data.Maybe                  (mapMaybe)
import           Data.Monoid                 (All (..))
import           GHC.Generics                (Generic)
import           Unsafe.Coerce               (unsafeCoerce)

-- | Scoped term under a (single) name binder.
data ScopedAST binder sig n where
  ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n

instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where
  rnf :: ScopedAST binder sig n -> ()
rnf (ScopedAST binder n l
binder AST binder sig l
body) = binder n l -> ()
forall a. NFData a => a -> ()
rnf binder n l
binder () -> () -> ()
forall a b. a -> b -> b
`seq` AST binder sig l -> ()
forall a. NFData a => a -> ()
rnf AST binder sig l
body

-- | A term, generated by a signature 'Bifunctor' @sig@,
-- with (free) variables in scope @n@.
data AST binder sig n where
  -- | A (free) variable in scope @n@.
  Var :: Foil.Name n -> AST binder sig n
  -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.
  Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n

deriving instance Generic (AST binder sig n)
deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
  => NFData (AST binder sig n)

instance GenericK (ScopedAST binder sig) where
  type RepK (ScopedAST binder sig) =
    Exists Foil.S
      (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0))
  toK :: forall (x :: LoT (S -> *)).
RepK (ScopedAST binder sig) x -> ScopedAST binder sig :@@: x
toK (Kind.Exists (Kind.Field Interpret (('Kon binder ':@: Var1) ':@: Var0) (t ':&&: x)
binder Kind.:*: Kind.Field Interpret
  ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (t ':&&: x)
ast)) = binder (HeadLoT x) t
-> AST binder sig t -> ScopedAST binder sig (HeadLoT x)
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder (HeadLoT x) t
Interpret (('Kon binder ':@: Var1) ':@: Var0) (t ':&&: x)
binder Interpret
  ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (t ':&&: x)
AST binder sig t
ast
  fromK :: forall (x :: LoT (S -> *)).
(ScopedAST binder sig :@@: x) -> RepK (ScopedAST binder sig) x
fromK (ScopedAST binder (HeadLoT x) l
binder AST binder sig l
ast) = (:*:)
  (Field (('Kon binder ':@: Var1) ':@: Var0))
  (Field ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0))
  (l ':&&: x)
-> Exists
     S
     (Field (('Kon binder ':@: Var1) ':@: Var0)
      :*: Field ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0))
     x
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f (t ':&&: x) -> Exists k f x
Kind.Exists (Interpret (('Kon binder ':@: Var1) ':@: Var0) (l ':&&: x)
-> Field (('Kon binder ':@: Var1) ':@: Var0) (l ':&&: x)
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Kind.Field binder (HeadLoT x) l
Interpret (('Kon binder ':@: Var1) ':@: Var0) (l ':&&: x)
binder Field (('Kon binder ':@: Var1) ':@: Var0) (l ':&&: x)
-> Field
     ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (l ':&&: x)
-> (:*:)
     (Field (('Kon binder ':@: Var1) ':@: Var0))
     (Field ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0))
     (l ':&&: x)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
Kind.:*: Interpret
  ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (l ':&&: x)
-> Field
     ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (l ':&&: x)
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Kind.Field Interpret
  ((('Kon AST ':@: 'Kon binder) ':@: 'Kon sig) ':@: Var0) (l ':&&: x)
AST binder sig l
ast)

instance GenericK (AST binder sig) where
  type RepK (AST binder sig) =
    Field (Foil.Name :$: Var0)
    :+: Field (sig
                :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0)
                :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0))

instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig)
instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig)

instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig)
instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig)

instance Foil.InjectName (AST binder sig) where
  injectName :: forall (n :: S). Name n -> AST binder sig n
injectName = Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var

-- * Substitution

-- | Substitution for free (scoped monads).
substitute
  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.Scope o
  -> Foil.Substitution (AST binder sig) i o
  -> AST binder sig i
  -> AST binder sig o
substitute :: forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o
scope Substitution (AST binder sig) i o
subst = \case
  Var Name i
name -> Substitution (AST binder sig) i o -> Name i -> AST binder sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST binder sig) i o
subst Name i
name
  Node sig (ScopedAST binder sig i) (AST binder sig i)
node -> sig (ScopedAST binder sig o) (AST binder sig o) -> AST binder sig o
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig i -> ScopedAST binder sig o)
-> (AST binder sig i -> AST binder sig o)
-> sig (ScopedAST binder sig i) (AST binder sig i)
-> sig (ScopedAST binder sig o) (AST binder sig o)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig i -> ScopedAST binder sig o
f (Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o
scope Substitution (AST binder sig) i o
subst) sig (ScopedAST binder sig i) (AST binder sig i)
node)
  where
    f :: ScopedAST binder sig i -> ScopedAST binder sig o
f (ScopedAST binder i l
binder AST binder sig l
body) =
      Scope o
-> binder i l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution (AST binder sig) i o
     -> Substitution (AST binder sig) l o')
    -> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withRefreshedPattern Scope o
scope binder i l
binder ((forall (o' :: S).
  DExt o o' =>
  (Substitution (AST binder sig) i o
   -> Substitution (AST binder sig) l o')
  -> binder o o' -> ScopedAST binder sig o)
 -> ScopedAST binder sig o)
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution (AST binder sig) i o
     -> Substitution (AST binder sig) l o')
    -> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst binder o o'
binder' ->
        let subst' :: Substitution (AST binder sig) l o'
subst' = Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) i o
-> Substitution (AST binder sig) i o
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) i o
subst)
            scope' :: Scope o'
scope' = binder o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder o o'
binder' Scope o
scope
            body' :: AST binder sig o'
body' = Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o'
scope' Substitution (AST binder sig) l o'
subst' AST binder sig l
body
        in binder o o' -> AST binder sig o' -> ScopedAST binder sig o
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder o o'
binder' AST binder sig o'
body'

-- | Substitution for free (scoped monads).
--
-- This is a version of 'substitute' that forces refreshing of all name binders,
-- resulting in a term with normalized binders:
--
-- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst
--
-- In general, 'substitute' is more efficient since it does not always refresh binders.
substituteRefreshed
  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.Scope o
  -> Foil.Substitution (AST binder sig) i o
  -> AST binder sig i
  -> AST binder sig o
substituteRefreshed :: forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o
scope Substitution (AST binder sig) i o
subst = \case
  Var Name i
name -> Substitution (AST binder sig) i o -> Name i -> AST binder sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST binder sig) i o
subst Name i
name
  Node sig (ScopedAST binder sig i) (AST binder sig i)
node -> sig (ScopedAST binder sig o) (AST binder sig o) -> AST binder sig o
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig i -> ScopedAST binder sig o)
-> (AST binder sig i -> AST binder sig o)
-> sig (ScopedAST binder sig i) (AST binder sig i)
-> sig (ScopedAST binder sig o) (AST binder sig o)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig i -> ScopedAST binder sig o
f (Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o
scope Substitution (AST binder sig) i o
subst) sig (ScopedAST binder sig i) (AST binder sig i)
node)
  where
    f :: ScopedAST binder sig i -> ScopedAST binder sig o
f (ScopedAST binder i l
binder AST binder sig l
body) =
      Scope o
-> binder i l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution (AST binder sig) i o
     -> Substitution (AST binder sig) l o')
    -> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withFreshPattern Scope o
scope binder i l
binder ((forall (o' :: S).
  DExt o o' =>
  (Substitution (AST binder sig) i o
   -> Substitution (AST binder sig) l o')
  -> binder o o' -> ScopedAST binder sig o)
 -> ScopedAST binder sig o)
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution (AST binder sig) i o
     -> Substitution (AST binder sig) l o')
    -> binder o o' -> ScopedAST binder sig o)
-> ScopedAST binder sig o
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst binder o o'
binder' ->
        let subst' :: Substitution (AST binder sig) l o'
subst' = Substitution (AST binder sig) i o
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) i o
-> Substitution (AST binder sig) i o
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) i o
subst)
            scope' :: Scope o'
scope' = binder o o' -> Scope o -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder o o'
binder' Scope o
scope
            body' :: AST binder sig o'
body' = Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o'
scope' Substitution (AST binder sig) l o'
subst' AST binder sig l
body
        in binder o o' -> AST binder sig o' -> ScopedAST binder sig o
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder o o'
binder' AST binder sig o'
body'

-- | @'AST' sig@ is a monad relative to 'Foil.Name'.
instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.RelMonad Foil.Name (AST binder sig) where
  rreturn :: forall (a :: S). Name a -> AST binder sig a
rreturn = Name a -> AST binder sig a
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var
  rbind :: forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
rbind Scope b
scope AST binder sig a
term Name a -> AST binder sig b
subst =
    case AST binder sig a
term of
      Var Name a
name  -> Name a -> AST binder sig b
subst Name a
name
      Node sig (ScopedAST binder sig a) (AST binder sig a)
node -> sig (ScopedAST binder sig b) (AST binder sig b) -> AST binder sig b
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig a -> ScopedAST binder sig b)
-> (AST binder sig a -> AST binder sig b)
-> sig (ScopedAST binder sig a) (AST binder sig a)
-> sig (ScopedAST binder sig b) (AST binder sig b)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ScopedAST binder sig a -> ScopedAST binder sig b
g' AST binder sig a -> AST binder sig b
g sig (ScopedAST binder sig a) (AST binder sig a)
node)
    where
      g :: AST binder sig a -> AST binder sig b
g AST binder sig a
x = Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
Foil.rbind Scope b
scope AST binder sig a
x Name a -> AST binder sig b
subst
      g' :: ScopedAST binder sig a -> ScopedAST binder sig b
g' (ScopedAST binder a l
binder AST binder sig l
body) =
        Scope b
-> binder a l
-> (forall (o' :: S).
    DExt b o' =>
    ((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
    -> binder b o' -> ScopedAST binder sig b)
-> ScopedAST binder sig b
forall (pattern :: S -> S -> *) (o :: S) (e :: S -> *) (n :: S)
       (l :: S) r.
(CoSinkable pattern, Distinct o, InjectName e, Sinkable e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r)
-> r
Foil.withRefreshedPattern' Scope b
scope binder a l
binder ((forall (o' :: S).
  DExt b o' =>
  ((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
  -> binder b o' -> ScopedAST binder sig b)
 -> ScopedAST binder sig b)
-> (forall (o' :: S).
    DExt b o' =>
    ((Name a -> AST binder sig b) -> Name l -> AST binder sig o')
    -> binder b o' -> ScopedAST binder sig b)
-> ScopedAST binder sig b
forall a b. (a -> b) -> a -> b
$ \(Name a -> AST binder sig b) -> Name l -> AST binder sig o'
extendSubst binder b o'
binder' ->
          let scope' :: Scope o'
scope' = binder b o' -> Scope b -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder b o'
binder' Scope b
scope
              subst' :: Name l -> AST binder sig o'
subst' = (Name a -> AST binder sig b) -> Name l -> AST binder sig o'
extendSubst Name a -> AST binder sig b
subst
           in binder b o' -> AST binder sig o' -> ScopedAST binder sig b
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder b o'
binder' (Scope o'
-> AST binder sig l
-> (Name l -> AST binder sig o')
-> AST binder sig o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b
-> AST binder sig a
-> (Name a -> AST binder sig b)
-> AST binder sig b
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> m a -> (f a -> m b) -> m b
Foil.rbind Scope o'
scope' AST binder sig l
body Name l -> AST binder sig o'
subst')

-- | Substitution for a single generalized pattern.
substitutePattern
  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.Scope o                           -- ^ Resulting scope.
  -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.
  -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.
  -> [AST binder sig o]                     -- ^ A list of terms intended to serve as
  -> AST binder sig i
  -> AST binder sig o
substitutePattern :: forall (sig :: * -> * -> *) (o :: S) (binder' :: S -> S -> *)
       (binder :: S -> S -> *) (n :: S) (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder', CoSinkable binder,
 SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) n o
-> binder' n i
-> [AST binder sig o]
-> AST binder sig i
-> AST binder sig o
substitutePattern Scope o
scope Substitution (AST binder sig) n o
env binder' n i
binders [AST binder sig o]
args AST binder sig i
body =
  Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substitute Scope o
scope Substitution (AST binder sig) i o
env' AST binder sig i
body
  where
    env' :: Substitution (AST binder sig) i o
env' = Substitution (AST binder sig) n o
-> binder' n i
-> [AST binder sig o]
-> Substitution (AST binder sig) i o
forall (binder :: S -> S -> *) (e :: S -> *) (i :: S) (o :: S)
       (i' :: S).
CoSinkable binder =>
Substitution e i o -> binder i i' -> [e o] -> Substitution e i' o
Foil.addSubstPattern Substitution (AST binder sig) n o
env binder' n i
binders [AST binder sig o]
args

-- * \(\alpha\)-equivalence

-- | Refresh (force) all binders in a term, minimizing the used indices.
refreshAST
  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.Scope n
  -> AST binder sig n
  -> AST binder sig n
refreshAST :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope = \case
  t :: AST binder sig n
t@Var{} -> AST binder sig n
t
  Node sig (ScopedAST binder sig n) (AST binder sig n)
t -> sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node ((ScopedAST binder sig n -> ScopedAST binder sig n)
-> (AST binder sig n -> AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
refreshScopedAST Scope n
scope) (Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope) sig (ScopedAST binder sig n) (AST binder sig n)
t)

-- | Similar to `refreshAST`, but for scoped terms.
refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder)
  => Foil.Scope n
  -> ScopedAST binder sig n
  -> ScopedAST binder sig n
refreshScopedAST :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
refreshScopedAST Scope n
scope (ScopedAST binder n l
binder AST binder sig l
body) =
  Scope n
-> binder n l
-> (forall {o' :: S}.
    DExt n o' =>
    (Substitution (AST binder sig) n n
     -> Substitution (AST binder sig) l o')
    -> binder n o' -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
Foil.withFreshPattern Scope n
scope binder n l
binder ((forall {o' :: S}.
  DExt n o' =>
  (Substitution (AST binder sig) n n
   -> Substitution (AST binder sig) l o')
  -> binder n o' -> ScopedAST binder sig n)
 -> ScopedAST binder sig n)
-> (forall {o' :: S}.
    DExt n o' =>
    (Substitution (AST binder sig) n n
     -> Substitution (AST binder sig) l o')
    -> binder n o' -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall a b. (a -> b) -> a -> b
$ \Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o'
extendSubst binder n o'
binder' ->
    let scope' :: Scope o'
scope' = binder n o' -> Scope n -> Scope o'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n o'
binder' Scope n
scope
        subst :: Substitution (AST binder sig) l o'
subst = Substitution (AST binder sig) n n
-> Substitution (AST binder sig) l o'
extendSubst (Substitution (AST binder sig) n n
-> Substitution (AST binder sig) n n
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST binder sig) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst)
    in binder n o' -> AST binder sig o' -> ScopedAST binder sig n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder n o'
binder' (Scope o'
-> Substitution (AST binder sig) l o'
-> AST binder sig l
-> AST binder sig o'
forall (sig :: * -> * -> *) (o :: S) (binder :: S -> S -> *)
       (i :: S).
(Bifunctor sig, Distinct o, CoSinkable binder, SinkableK binder) =>
Scope o
-> Substitution (AST binder sig) i o
-> AST binder sig i
-> AST binder sig o
substituteRefreshed Scope o'
scope' Substitution (AST binder sig) l o'
subst AST binder sig l
body)

-- | \(\alpha\)-equivalence check for two terms in one scope
-- via normalization of bound identifiers (via 'refreshAST').
--
-- Compared to 'alphaEquiv', this function may perform some unnecessary
-- changes of bound variables when the binders are the same on both sides.
alphaEquivRefreshed
  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Foil.Scope n
  -> AST binder sig n
  -> AST binder sig n
  -> Bool
alphaEquivRefreshed :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquivRefreshed Scope n
scope AST binder sig n
t1 AST binder sig n
t2 = Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope AST binder sig n
t1 AST binder sig n -> AST binder sig n -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
`unsafeEqAST` Scope n -> AST binder sig n -> AST binder sig n
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bifunctor sig, Distinct n, CoSinkable binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n
refreshAST Scope n
scope AST binder sig n
t2

-- | \(\alpha\)-equivalence check for two terms in one scope
-- via unification of bound variables (via 'unifyNameBinders').
--
-- Compared to 'alphaEquivRefreshed', this function might skip unnecessary
-- changes of bound variables when both binders in two matching scoped terms coincide.
alphaEquiv
  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Foil.Scope n
  -> AST binder sig n
  -> AST binder sig n
  -> Bool
alphaEquiv :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
_scope (Var Name n
x) (Var Name n
y) = Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name n -> Name n
forall a b. Coercible a b => a -> b
coerce Name n
y
alphaEquiv Scope n
scope (Node sig (ScopedAST binder sig n) (AST binder sig n)
l) (Node sig (ScopedAST binder sig n) (AST binder sig n)
r) =
  case sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> Maybe
     (sig
        (ScopedAST binder sig n, ScopedAST binder sig n)
        (AST binder sig n, AST binder sig n))
forall (f :: * -> * -> *) a b a' b'.
(Bitraversable f, ZipMatchK f) =>
f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
zipMatch2 sig (ScopedAST binder sig n) (AST binder sig n)
l sig (ScopedAST binder sig n) (AST binder sig n)
r of
    Maybe
  (sig
     (ScopedAST binder sig n, ScopedAST binder sig n)
     (AST binder sig n, AST binder sig n))
Nothing -> Bool
False
    Just sig
  (ScopedAST binder sig n, ScopedAST binder sig n)
  (AST binder sig n, AST binder sig n)
tt -> All -> Bool
getAll (((ScopedAST binder sig n, ScopedAST binder sig n) -> All)
-> ((AST binder sig n, AST binder sig n) -> All)
-> sig
     (ScopedAST binder sig n, ScopedAST binder sig n)
     (AST binder sig n, AST binder sig n)
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (Bool -> All
All (Bool -> All)
-> ((ScopedAST binder sig n, ScopedAST binder sig n) -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST binder sig n -> ScopedAST binder sig n -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
alphaEquivScoped Scope n
scope)) (Bool -> All
All (Bool -> All)
-> ((AST binder sig n, AST binder sig n) -> Bool)
-> (AST binder sig n, AST binder sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST binder sig n -> AST binder sig n -> Bool)
-> (AST binder sig n, AST binder sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> AST binder sig n -> AST binder sig n -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope n
scope)) sig
  (ScopedAST binder sig n, ScopedAST binder sig n)
  (AST binder sig n, AST binder sig n)
tt)
alphaEquiv Scope n
_ AST binder sig n
_ AST binder sig n
_ = Bool
False

-- | Same as 'alphaEquiv' but for scoped terms.
alphaEquivScoped
  :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Foil.Scope n
  -> ScopedAST binder sig n
  -> ScopedAST binder sig n
  -> Bool
alphaEquivScoped :: forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
alphaEquivScoped Scope n
scope
  (ScopedAST binder n l
binder1 AST binder sig l
body1)
  (ScopedAST binder n l
binder2 AST binder sig l
body2) =
    case binder n l -> binder n l -> UnifyNameBinders binder n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
binder n l -> binder n r -> UnifyNameBinders binder n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
Foil.unifyPatterns binder n l
binder1 binder n l
binder2 of
      -- if binders are the same, then we can safely compare bodies
      Foil.SameNameBinders{} ->  -- after seeing this we know that body scopes are the same
        case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1 of
          DistinctEvidence l
Foil.Distinct ->
            let scope1 :: Scope l
scope1 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder1 Scope n
scope
            in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope1 AST binder sig l
body1 AST binder sig l
AST binder sig l
body2
      -- if we can safely rename first binder into second
      Foil.RenameLeftNameBinder NameBinders n l
_ NameBinder n l -> NameBinder n l
rename1to2 ->
        case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder2 of
          DistinctEvidence l
Foil.Distinct ->
            let scope2 :: Scope l
scope2 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder2 Scope n
scope
            in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope2 (Scope l
-> (Name l -> Name l) -> AST binder sig l -> AST binder sig l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope l
scope2 ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n l
rename1to2) AST binder sig l
body1) AST binder sig l
body2
      -- if we can safely rename second binder into first
      Foil.RenameRightNameBinder NameBinders n l
_ NameBinder n l -> NameBinder n l
rename2to1 ->
        case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1 of
          DistinctEvidence l
Foil.Distinct ->
            let scope1 :: Scope l
scope1 = binder n l -> Scope n -> Scope l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n l
binder1 Scope n
scope
            in Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope l
scope1 AST binder sig l
body1 (Scope l
-> (Name l -> Name l) -> AST binder sig l -> AST binder sig l
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope l
scope1 ((NameBinder n l -> NameBinder n l) -> Name l -> Name l
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n l
rename2to1) AST binder sig l
body2)
      -- if we need to rename both patterns
      Foil.RenameBothBinders NameBinders n lr
binder' NameBinder n l -> NameBinder n lr
rename1 NameBinder n l -> NameBinder n lr
rename2 ->
        case NameBinders n lr -> DistinctEvidence lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct NameBinders n lr
binder' of
          DistinctEvidence lr
Foil.Distinct ->
            let scope' :: Scope lr
scope' = NameBinders n lr -> Scope n -> Scope lr
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern NameBinders n lr
binder' Scope n
scope
            in Scope lr -> AST binder sig lr -> AST binder sig lr -> Bool
forall (sig :: * -> * -> *) (n :: S) (binder :: S -> S -> *).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv Scope lr
scope'
                (Scope lr
-> (Name l -> Name lr) -> AST binder sig l -> AST binder sig lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n lr
rename1) AST binder sig l
body1)
                (Scope lr
-> (Name l -> Name lr) -> AST binder sig l -> AST binder sig lr
forall (f :: S -> *) (m :: S -> *) (b :: S) (a :: S).
(RelMonad f m, Distinct b) =>
Scope b -> (f a -> f b) -> m a -> m b
Foil.liftRM Scope lr
scope' ((NameBinder n l -> NameBinder n lr) -> Name l -> Name lr
forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
Foil.fromNameBinderRenaming NameBinder n l -> NameBinder n lr
rename2) AST binder sig l
body2)
      -- if we cannot unify patterns then scopes are not alpha-equivalent
      UnifyNameBinders binder n l l
Foil.NotUnifiable -> Bool
False

-- ** Unsafe equality checks

-- | /Unsafe/ equality check for two terms.
-- This check ignores the possibility that two terms might have different
-- scope extensions under binders (which might happen due to substitution
-- under a binder in absence of name conflicts).
unsafeEqAST
  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
  => AST binder sig n
  -> AST binder sig l
  -> Bool
unsafeEqAST :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
unsafeEqAST (Var Name n
x) (Var Name l
y) = Name n
x Name n -> Name n -> Bool
forall a. Eq a => a -> a -> Bool
== Name l -> Name n
forall a b. Coercible a b => a -> b
coerce Name l
y
unsafeEqAST (Node sig (ScopedAST binder sig n) (AST binder sig n)
t1) (Node sig (ScopedAST binder sig l) (AST binder sig l)
t2) =
  case sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig l) (AST binder sig l)
-> Maybe
     (sig
        (ScopedAST binder sig n, ScopedAST binder sig l)
        (AST binder sig n, AST binder sig l))
forall (f :: * -> * -> *) a b a' b'.
(Bitraversable f, ZipMatchK f) =>
f a b -> f a' b' -> Maybe (f (a, a') (b, b'))
zipMatch2 sig (ScopedAST binder sig n) (AST binder sig n)
t1 sig (ScopedAST binder sig l) (AST binder sig l)
t2 of
    Maybe
  (sig
     (ScopedAST binder sig n, ScopedAST binder sig l)
     (AST binder sig n, AST binder sig l))
Nothing -> Bool
False
    Just sig
  (ScopedAST binder sig n, ScopedAST binder sig l)
  (AST binder sig n, AST binder sig l)
tt -> All -> Bool
getAll (((ScopedAST binder sig n, ScopedAST binder sig l) -> All)
-> ((AST binder sig n, AST binder sig l) -> All)
-> sig
     (ScopedAST binder sig n, ScopedAST binder sig l)
     (AST binder sig n, AST binder sig l)
-> All
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap (Bool -> All
All (Bool -> All)
-> ((ScopedAST binder sig n, ScopedAST binder sig l) -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST binder sig n -> ScopedAST binder sig l -> Bool)
-> (ScopedAST binder sig n, ScopedAST binder sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
unsafeEqScopedAST) (Bool -> All
All (Bool -> All)
-> ((AST binder sig n, AST binder sig l) -> Bool)
-> (AST binder sig n, AST binder sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST binder sig n -> AST binder sig l -> Bool)
-> (AST binder sig n, AST binder sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry AST binder sig n -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
unsafeEqAST) sig
  (ScopedAST binder sig n, ScopedAST binder sig l)
  (AST binder sig n, AST binder sig l)
tt)
unsafeEqAST AST binder sig n
_ AST binder sig l
_ = Bool
False

-- | A version of 'unsafeEqAST' for scoped terms.
unsafeEqScopedAST
  :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)
  => ScopedAST binder sig n
  -> ScopedAST binder sig l
  -> Bool
unsafeEqScopedAST :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
unsafeEqScopedAST (ScopedAST binder n l
binder1 AST binder sig l
body1) (ScopedAST binder l l
binder2 AST binder sig l
body2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ binder n l -> binder l l -> Bool
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (n' :: S)
       (l' :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n' l' -> Bool
Foil.unsafeEqPattern binder n l
binder1 binder l l
binder2
  , case (binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder1, binder l l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder l l
binder2) of
      (DistinctEvidence l
Foil.Distinct, DistinctEvidence l
Foil.Distinct) -> AST binder sig l
body1 AST binder sig l -> AST binder sig l -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (l :: S).
(Bitraversable sig, ZipMatchK sig, UnifiablePattern binder,
 Distinct n, Distinct l) =>
AST binder sig n -> AST binder sig l -> Bool
`unsafeEqAST` AST binder sig l
body2
  ]

-- * Converting to and from free foil

-- ** Convert to free foil

-- | Convert a raw term into a scope-safe term.
convertToAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -- ^ Unpeel one syntax node (or a variable) from a raw term.
  -> (forall x z. Foil.Distinct x
      => Foil.Scope x
      -> Map rawIdent (Foil.Name x)
      -> rawPattern
      -> (forall y. Foil.DExt x y
          => binder x y
          -> Map rawIdent (Foil.Name y)
          -> z)
      -> z)
  -- ^ Convert raw pattern into a scope-safe pattern.
  -> (rawScopedTerm -> rawTerm)
  -- ^ Extract a term from a scoped term (or crash).
  -> Foil.Scope n
  -- ^ Resulting scope of the constructed term.
  -> Map rawIdent (Foil.Name n)
  -- ^ Known names of free variables in scope @n@.
  -> rawTerm
  -- ^ Raw term.
  -> AST binder sig n
convertToAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent
       (binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names rawTerm
t =
  case rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawTerm
t of
    Left rawIdent
x ->
      case rawIdent -> Map rawIdent (Name n) -> Maybe (Name n)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup rawIdent
x Map rawIdent (Name n)
names of
        Maybe (Name n)
Nothing   -> [Char] -> AST binder sig n
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined variable"
        Just Name n
name -> Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
name
    Right sig (rawPattern, rawScopedTerm) rawTerm
node -> sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S).
sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
Node (sig (ScopedAST binder sig n) (AST binder sig n)
 -> AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> AST binder sig n
forall a b. (a -> b) -> a -> b
$
      ((rawPattern, rawScopedTerm) -> ScopedAST binder sig n)
-> (rawTerm -> AST binder sig n)
-> sig (rawPattern, rawScopedTerm) rawTerm
-> sig (ScopedAST binder sig n) (AST binder sig n)
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
        ((rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent
       (binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
        ((rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent
       (binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
        sig (rawPattern, rawScopedTerm) rawTerm
node

-- | Same as 'convertToAST' but for scoped terms.
convertToScopedAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -- ^ Unpeel one syntax node (or a variable) from a raw term.
  -> (forall x z. Foil.Distinct x
      => Foil.Scope x
      -> Map rawIdent (Foil.Name x)
      -> rawPattern
      -> (forall y. Foil.DExt x y
          => binder x y
          -> Map rawIdent (Foil.Name y)
          -> z)
      -> z)
  -- ^ Convert raw pattern into a scope-safe pattern.
  -> (rawScopedTerm -> rawTerm)
  -- ^ Extract a term from a scoped term (or crash).
  -> Foil.Scope n
  -- ^ Resulting scope of the constructed term.
  -> Map rawIdent (Foil.Name n)
  -- ^ Known names of free variables in scope @n@.
  -> (rawPattern, rawScopedTerm)
  -- ^ A pair of a pattern and a corresponding scoped term.
  -> ScopedAST binder sig n
convertToScopedAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent
       (binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names (rawPattern
pat, rawScopedTerm
scopedTerm) =
  Scope n
-> Map rawIdent (Name n)
-> rawPattern
-> (forall {y :: S}.
    DExt n y =>
    binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern Scope n
scope Map rawIdent (Name n)
names rawPattern
pat ((forall {y :: S}.
  DExt n y =>
  binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
 -> ScopedAST binder sig n)
-> (forall {y :: S}.
    DExt n y =>
    binder n y -> Map rawIdent (Name y) -> ScopedAST binder sig n)
-> ScopedAST binder sig n
forall a b. (a -> b) -> a -> b
$ \binder n y
binder' Map rawIdent (Name y)
names' ->
    let scope' :: Scope y
scope' = binder n y -> Scope n -> Scope y
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder n y
binder' Scope n
scope
     in binder n y -> AST binder sig y -> ScopedAST binder sig n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder n y
binder' ((rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope y
-> Map rawIdent (Name y)
-> rawTerm
-> AST binder sig y
forall (n :: S) (sig :: * -> * -> *) rawIdent
       (binder :: S -> S -> *) rawTerm rawPattern rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (forall (x :: S) z.
    Distinct x =>
    Scope x
    -> Map rawIdent (Name x)
    -> rawPattern
    -> (forall (y :: S).
        DExt x y =>
        binder x y -> Map rawIdent (Name y) -> z)
    -> z)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST binder sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
forall (x :: S) z.
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> z)
-> z
fromRawPattern rawScopedTerm -> rawTerm
getScopedTerm Scope y
scope' Map rawIdent (Name y)
names' (rawScopedTerm -> rawTerm
getScopedTerm rawScopedTerm
scopedTerm))

-- ** Convert from free foil

-- | Convert a scope-safe term back into a raw term.
convertFromAST
  :: Bifunctor sig
  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
  -- ^ Peel back one layer of syntax.
  -> (rawIdent -> rawTerm)
  -- ^ Convert identifier into a raw variable term.
  -> (forall x y. binder x y -> rawPattern)
  -- ^ Convert scope-safe pattern into a raw pattern.
  -> (rawTerm -> rawScopedTerm)
  -- ^ Wrap raw term into a scoped term.
  -> (Int -> rawIdent)
  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.
  -> AST binder sig n
  -- ^ Scope-safe term.
  -> rawTerm
convertFromAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f = \case
  Var Name n
x -> rawIdent -> rawTerm
fromVar (Int -> rawIdent
f (Name n -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name n
x))
  Node sig (ScopedAST binder sig n) (AST binder sig n)
node -> sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
forall a b. (a -> b) -> a -> b
$
    (ScopedAST binder sig n -> (rawPattern, rawScopedTerm))
-> (AST binder sig n -> rawTerm)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (rawPattern, rawScopedTerm) rawTerm
forall a b c d. (a -> b) -> (c -> d) -> sig a c -> sig b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap
      ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar binder x y -> rawPattern
forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
      ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar binder x y -> rawPattern
forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
      sig (ScopedAST binder sig n) (AST binder sig n)
node

-- | Same as 'convertFromAST' but for scoped terms.
convertFromScopedAST
  :: Bifunctor sig
  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
  -- ^ Peel back one layer of syntax.
  -> (rawIdent -> rawTerm)
  -- ^ Convert identifier into a raw variable term.
  -> (forall x y. binder x y -> rawPattern)
  -- ^ Convert scope-safe pattern into a raw pattern.
  -> (rawTerm -> rawScopedTerm)
  -- ^ Wrap raw term into a scoped term.
  -> (Int -> rawIdent)
  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.
  -> ScopedAST binder sig n
  -- ^ Scope-safe scoped term.
  -> (rawPattern, rawScopedTerm)
convertFromScopedAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST binder sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f = \case
  ScopedAST binder n l
binder AST binder sig l
body ->
    ( binder n l -> rawPattern
forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern binder n l
binder
    , rawTerm -> rawScopedTerm
makeScoped ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig l
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (binder :: S -> S -> *) (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar binder x y -> rawPattern
forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f AST binder sig l
body))

-- ** Unsinking AST

-- | Unsink an AST from a larger scope to a smaller scope.
unsinkAST :: (Foil.Distinct l, Foil.CoSinkable binder, Bifoldable sig) => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n)
unsinkAST :: forall (l :: S) (binder :: S -> S -> *) (sig :: * -> * -> *)
       (n :: S).
(Distinct l, CoSinkable binder, Bifoldable sig) =>
Scope n -> AST binder sig l -> Maybe (AST binder sig n)
unsinkAST Scope n
scope AST binder sig l
term
  | (Name l -> Bool) -> [Name l] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name l -> Scope n -> Bool
forall (l :: S) (n :: S). Name l -> Scope n -> Bool
`Foil.member` Scope n
scope) (AST binder sig l -> [Name l]
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> [Name n]
freeVarsOf AST binder sig l
term) = AST binder sig n -> Maybe (AST binder sig n)
forall a. a -> Maybe a
Just (AST binder sig l -> AST binder sig n
forall a b. a -> b
unsafeCoerce AST binder sig l
term)
  | Bool
otherwise = Maybe (AST binder sig n)
forall a. Maybe a
Nothing

-- | Get the free variables of an AST.
freeVarsOf :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => AST binder sig n -> [Foil.Name n]
freeVarsOf :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> [Name n]
freeVarsOf = \case
  Var Name n
name -> [Name n
name]
  Node sig (ScopedAST binder sig n) (AST binder sig n)
node -> (ScopedAST binder sig n -> [Name n])
-> (AST binder sig n -> [Name n])
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> [Name n]
forall m a b. Monoid m => (a -> m) -> (b -> m) -> sig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ScopedAST binder sig n -> [Name n]
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
ScopedAST binder sig n -> [Name n]
freeVarsOfScopedAST AST binder sig n -> [Name n]
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> [Name n]
freeVarsOf sig (ScopedAST binder sig n) (AST binder sig n)
node

-- | Get the free variables of a scoped AST.
freeVarsOfScopedAST :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) => ScopedAST binder sig n -> [Foil.Name n]
freeVarsOfScopedAST :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
ScopedAST binder sig n -> [Name n]
freeVarsOfScopedAST (ScopedAST binder n l
binder AST binder sig l
body) =
  case binder n l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder n l
binder of
    DistinctEvidence l
Foil.Distinct -> (Name l -> Maybe (Name n)) -> [Name l] -> [Name n]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (binder n l -> Name l -> Maybe (Name n)
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Name l -> Maybe (Name n)
Foil.unsinkNamePattern binder n l
binder) (AST binder sig l -> [Name l]
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> [Name n]
freeVarsOf AST binder sig l
body)