{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# 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.Bifunctor
import           Data.Bifunctor.Sum
import           Data.Coerce                 (coerce)
import           Data.Map                    (Map)
import qualified Data.Map                    as Map
import           Data.Monoid                 (All (..))
import           GHC.Generics                (Generic)

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

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

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

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

instance Bifunctor sig => Foil.Sinkable (AST sig) where
  sinkabilityProof :: forall (n :: S) (l :: S).
(Name n -> Name l) -> AST sig n -> AST sig l
sinkabilityProof Name n -> Name l
rename = \case
    Var Name n
name -> Name l -> AST sig l
forall (n :: S) (sig :: * -> * -> *). Name n -> AST sig n
Var (Name n -> Name l
rename Name n
name)
    Node sig (ScopedAST sig n) (AST sig n)
node -> sig (ScopedAST sig l) (AST sig l) -> AST sig l
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node ((ScopedAST sig n -> ScopedAST sig l)
-> (AST sig n -> AST sig l)
-> sig (ScopedAST sig n) (AST sig n)
-> sig (ScopedAST sig l) (AST sig l)
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 sig n -> ScopedAST sig l
f ((Name n -> Name l) -> AST sig n -> AST sig l
forall (n :: S) (l :: S).
(Name n -> Name l) -> AST sig n -> AST sig l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
Foil.sinkabilityProof Name n -> Name l
rename) sig (ScopedAST sig n) (AST sig n)
node)
    where
      f :: ScopedAST sig n -> ScopedAST sig l
f (ScopedAST NameBinder n l
binder AST sig l
body) =
        (Name n -> Name l)
-> NameBinder n l
-> (forall (l' :: S).
    (Name l -> Name l') -> NameBinder l l' -> ScopedAST sig l)
-> ScopedAST sig l
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
Foil.extendRenaming Name n -> Name l
rename NameBinder n l
binder ((forall (l' :: S).
  (Name l -> Name l') -> NameBinder l l' -> ScopedAST sig l)
 -> ScopedAST sig l)
-> (forall (l' :: S).
    (Name l -> Name l') -> NameBinder l l' -> ScopedAST sig l)
-> ScopedAST sig l
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename' NameBinder l l'
binder' ->
          NameBinder l l' -> AST sig l' -> ScopedAST sig l
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder l l'
binder' ((Name l -> Name l') -> AST sig l -> AST sig l'
forall (n :: S) (l :: S).
(Name n -> Name l) -> AST sig n -> AST sig l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
Foil.sinkabilityProof Name l -> Name l'
rename' AST sig l
body)

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

-- * Substitution

-- | Substitution for free (scoped monads).
substitute
  :: (Bifunctor sig, Foil.Distinct o)
  => Foil.Scope o
  -> Foil.Substitution (AST sig) i o
  -> AST sig i
  -> AST sig o
substitute :: forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substitute Scope o
scope Substitution (AST sig) i o
subst = \case
  Var Name i
name -> Substitution (AST sig) i o -> Name i -> AST sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST sig) i o
subst Name i
name
  Node sig (ScopedAST sig i) (AST sig i)
node -> sig (ScopedAST sig o) (AST sig o) -> AST sig o
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node ((ScopedAST sig i -> ScopedAST sig o)
-> (AST sig i -> AST sig o)
-> sig (ScopedAST sig i) (AST sig i)
-> sig (ScopedAST sig o) (AST 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 sig i -> ScopedAST sig o
f (Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substitute Scope o
scope Substitution (AST sig) i o
subst) sig (ScopedAST sig i) (AST sig i)
node)
  where
    f :: ScopedAST sig i -> ScopedAST sig o
f (ScopedAST NameBinder i l
binder AST sig l
body) =
      Scope o
-> Name l
-> (forall (o' :: S).
    DExt o o' =>
    NameBinder o o' -> ScopedAST sig o)
-> ScopedAST sig o
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
Foil.withRefreshed Scope o
scope (NameBinder i l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder i l
binder) ((forall (o' :: S).
  DExt o o' =>
  NameBinder o o' -> ScopedAST sig o)
 -> ScopedAST sig o)
-> (forall (o' :: S).
    DExt o o' =>
    NameBinder o o' -> ScopedAST sig o)
-> ScopedAST sig o
forall a b. (a -> b) -> a -> b
$ \NameBinder o o'
binder' ->
        let subst' :: Substitution (AST sig) l o'
subst' = Substitution (AST sig) i o'
-> NameBinder i l -> Name o' -> Substitution (AST sig) l o'
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution (AST sig) i o -> Substitution (AST sig) i o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST sig) i o
subst) NameBinder i l
binder (NameBinder o o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder o o'
binder')
            scope' :: Scope o'
scope' = NameBinder o o' -> Scope o -> Scope o'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder o o'
binder' Scope o
scope
            body' :: AST sig o'
body' = Scope o' -> Substitution (AST sig) l o' -> AST sig l -> AST sig o'
forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substitute Scope o'
scope' Substitution (AST sig) l o'
subst' AST sig l
body
        in NameBinder o o' -> AST sig o' -> ScopedAST sig o
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder o o'
binder' AST 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.Scope o
  -> Foil.Substitution (AST sig) i o
  -> AST sig i
  -> AST sig o
substituteRefreshed :: forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substituteRefreshed Scope o
scope Substitution (AST sig) i o
subst = \case
  Var Name i
name -> Substitution (AST sig) i o -> Name i -> AST sig o
forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
Foil.lookupSubst Substitution (AST sig) i o
subst Name i
name
  Node sig (ScopedAST sig i) (AST sig i)
node -> sig (ScopedAST sig o) (AST sig o) -> AST sig o
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node ((ScopedAST sig i -> ScopedAST sig o)
-> (AST sig i -> AST sig o)
-> sig (ScopedAST sig i) (AST sig i)
-> sig (ScopedAST sig o) (AST 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 sig i -> ScopedAST sig o
f (Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substituteRefreshed Scope o
scope Substitution (AST sig) i o
subst) sig (ScopedAST sig i) (AST sig i)
node)
  where
    f :: ScopedAST sig i -> ScopedAST sig o
f (ScopedAST NameBinder i l
binder AST sig l
body) =
      Scope o
-> (forall (l :: S). DExt o l => NameBinder o l -> ScopedAST sig o)
-> ScopedAST sig o
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope o
scope ((forall (l :: S). DExt o l => NameBinder o l -> ScopedAST sig o)
 -> ScopedAST sig o)
-> (forall (l :: S). DExt o l => NameBinder o l -> ScopedAST sig o)
-> ScopedAST sig o
forall a b. (a -> b) -> a -> b
$ \NameBinder o l
binder' ->
        let subst' :: Substitution (AST sig) l l
subst' = Substitution (AST sig) i l
-> NameBinder i l -> Name l -> Substitution (AST sig) l l
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution (AST sig) i o -> Substitution (AST sig) i l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST sig) i o
subst) NameBinder i l
binder (NameBinder o l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder o l
binder')
            scope' :: Scope l
scope' = NameBinder o l -> Scope o -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder o l
binder' Scope o
scope
            body' :: AST sig l
body' = Scope l -> Substitution (AST sig) l l -> AST sig l -> AST sig l
forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substituteRefreshed Scope l
scope' Substitution (AST sig) l l
subst' AST sig l
body
        in NameBinder o l -> AST sig l -> ScopedAST sig o
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder o l
binder' AST sig l
body'

-- | @'AST' sig@ is a monad relative to 'Foil.Name'.
instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where
  rreturn :: forall (a :: S). Name a -> AST sig a
rreturn = Name a -> AST sig a
forall (n :: S) (sig :: * -> * -> *). Name n -> AST sig n
Var
  rbind :: forall (b :: S) (a :: S).
Distinct b =>
Scope b -> AST sig a -> (Name a -> AST sig b) -> AST sig b
rbind Scope b
scope AST sig a
term Name a -> AST sig b
subst =
    case AST sig a
term of
      Var Name a
name  -> Name a -> AST sig b
subst Name a
name
      Node sig (ScopedAST sig a) (AST sig a)
node -> sig (ScopedAST sig b) (AST sig b) -> AST sig b
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node ((ScopedAST sig a -> ScopedAST sig b)
-> (AST sig a -> AST sig b)
-> sig (ScopedAST sig a) (AST sig a)
-> sig (ScopedAST sig b) (AST 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 sig a -> ScopedAST sig b
g' AST sig a -> AST sig b
g sig (ScopedAST sig a) (AST sig a)
node)
    where
      g :: AST sig a -> AST sig b
g AST sig a
x = Scope b -> AST sig a -> (Name a -> AST sig b) -> AST sig b
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> AST sig a -> (Name a -> AST sig b) -> AST 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 sig a
x Name a -> AST sig b
subst
      g' :: ScopedAST sig a -> ScopedAST sig b
g' (ScopedAST NameBinder a l
binder AST sig l
body) =
        Scope b
-> Name l
-> (forall (o' :: S).
    DExt b o' =>
    NameBinder b o' -> ScopedAST sig b)
-> ScopedAST sig b
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
Foil.withRefreshed Scope b
scope (NameBinder a l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder a l
binder) ((forall (o' :: S).
  DExt b o' =>
  NameBinder b o' -> ScopedAST sig b)
 -> ScopedAST sig b)
-> (forall (o' :: S).
    DExt b o' =>
    NameBinder b o' -> ScopedAST sig b)
-> ScopedAST sig b
forall a b. (a -> b) -> a -> b
$ \NameBinder b o'
binder' ->
          let scope' :: Scope o'
scope' = NameBinder b o' -> Scope b -> Scope o'
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder b o'
binder' Scope b
scope
              subst' :: Name l -> AST sig o'
subst' Name l
name = case NameBinder a l -> Name l -> Maybe (Name a)
forall (n :: S) (l :: S).
NameBinder n l -> Name l -> Maybe (Name n)
Foil.unsinkName NameBinder a l
binder Name l
name of
                          Maybe (Name a)
Nothing -> Name o' -> AST sig o'
forall (a :: S). Name a -> AST sig a
forall (f :: S -> *) (m :: S -> *) (a :: S).
RelMonad f m =>
f a -> m a
Foil.rreturn (NameBinder b o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder b o'
binder')
                          Just Name a
n  -> AST sig b -> AST sig o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (Name a -> AST sig b
subst Name a
n)
           in NameBinder b o' -> AST sig o' -> ScopedAST sig b
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder b o'
binder' (Scope o' -> AST sig l -> (Name l -> AST sig o') -> AST sig o'
forall (b :: S) (a :: S).
Distinct b =>
Scope b -> AST sig a -> (Name a -> AST sig b) -> AST 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 sig l
body Name l -> AST sig o'
subst')

-- * \(\alpha\)-equivalence

-- | Refresh (force) all binders in a term, minimizing the used indices.
refreshAST
  :: (Bifunctor sig, Foil.Distinct n)
  => Foil.Scope n
  -> AST sig n
  -> AST sig n
refreshAST :: forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n
refreshAST Scope n
scope = \case
  t :: AST sig n
t@Var{} -> AST sig n
t
  Node sig (ScopedAST sig n) (AST sig n)
t -> sig (ScopedAST sig n) (AST sig n) -> AST sig n
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node ((ScopedAST sig n -> ScopedAST sig n)
-> (AST sig n -> AST sig n)
-> sig (ScopedAST sig n) (AST sig n)
-> sig (ScopedAST sig n) (AST 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 sig n -> ScopedAST sig n
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> ScopedAST sig n -> ScopedAST sig n
refreshScopedAST Scope n
scope) (Scope n -> AST sig n -> AST sig n
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n
refreshAST Scope n
scope) sig (ScopedAST sig n) (AST sig n)
t)

-- | Similar to `refreshAST`, but for scoped terms.
refreshScopedAST :: (Bifunctor sig, Foil.Distinct n)
  => Foil.Scope n
  -> ScopedAST sig n
  -> ScopedAST sig n
refreshScopedAST :: forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> ScopedAST sig n -> ScopedAST sig n
refreshScopedAST Scope n
scope (ScopedAST NameBinder n l
binder AST sig l
body) =
  Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
-> ScopedAST sig n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
 -> ScopedAST sig n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
-> ScopedAST sig n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder' ->
    let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder' Scope n
scope
        subst :: Substitution (AST sig) l l
subst = Substitution (AST sig) n l
-> NameBinder n l -> Name l -> Substitution (AST sig) l l
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
Foil.addRename (Substitution (AST sig) n n -> Substitution (AST sig) n l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink Substitution (AST sig) n n
forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
Foil.identitySubst) NameBinder n l
binder (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder')
    in NameBinder n l -> AST sig l -> ScopedAST sig n
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder n l
binder' (Scope l -> Substitution (AST sig) l l -> AST sig l -> AST sig l
forall (sig :: * -> * -> *) (o :: S) (i :: S).
(Bifunctor sig, Distinct o) =>
Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substituteRefreshed Scope l
scope' Substitution (AST sig) l l
subst AST 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
  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
  => Foil.Scope n
  -> AST sig n
  -> AST sig n
  -> Bool
alphaEquivRefreshed :: forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n -> Bool
alphaEquivRefreshed Scope n
scope AST sig n
t1 AST sig n
t2 = Scope n -> AST sig n -> AST sig n
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n
refreshAST Scope n
scope AST sig n
t1 AST sig n -> AST sig n -> Bool
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
AST sig n -> AST sig l -> Bool
`unsafeEqAST` Scope n -> AST sig n -> AST sig n
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n
refreshAST Scope n
scope AST 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
  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
  => Foil.Scope n
  -> AST sig n
  -> AST sig n
  -> Bool
alphaEquiv :: forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST 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 sig n) (AST sig n)
l) (Node sig (ScopedAST sig n) (AST sig n)
r) =
  case sig (ScopedAST sig n) (AST sig n)
-> sig (ScopedAST sig n) (AST sig n)
-> Maybe
     (sig (ScopedAST sig n, ScopedAST sig n) (AST sig n, AST sig n))
forall scope term scope' term'.
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch sig (ScopedAST sig n) (AST sig n)
l sig (ScopedAST sig n) (AST sig n)
r of
    Maybe
  (sig (ScopedAST sig n, ScopedAST sig n) (AST sig n, AST sig n))
Nothing -> Bool
False
    Just sig (ScopedAST sig n, ScopedAST sig n) (AST sig n, AST sig n)
tt -> All -> Bool
getAll (((ScopedAST sig n, ScopedAST sig n) -> All)
-> ((AST sig n, AST sig n) -> All)
-> sig (ScopedAST sig n, ScopedAST sig n) (AST sig n, AST 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 sig n, ScopedAST sig n) -> Bool)
-> (ScopedAST sig n, ScopedAST sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST sig n -> ScopedAST sig n -> Bool)
-> (ScopedAST sig n, ScopedAST sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> ScopedAST sig n -> ScopedAST sig n -> Bool
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> ScopedAST sig n -> ScopedAST sig n -> Bool
alphaEquivScoped Scope n
scope)) (Bool -> All
All (Bool -> All)
-> ((AST sig n, AST sig n) -> Bool)
-> (AST sig n, AST sig n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST sig n -> AST sig n -> Bool) -> (AST sig n, AST sig n) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Scope n -> AST sig n -> AST sig n -> Bool
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n -> Bool
alphaEquiv Scope n
scope)) sig (ScopedAST sig n, ScopedAST sig n) (AST sig n, AST sig n)
tt)
alphaEquiv Scope n
_ AST sig n
_ AST sig n
_ = Bool
False

-- | Same as 'alphaEquiv' but for scoped terms.
alphaEquivScoped
  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)
  => Foil.Scope n
  -> ScopedAST sig n
  -> ScopedAST sig n
  -> Bool
alphaEquivScoped :: forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> ScopedAST sig n -> ScopedAST sig n -> Bool
alphaEquivScoped Scope n
scope
  (ScopedAST NameBinder n l
binder1 AST sig l
body1)
  (ScopedAST NameBinder n l
binder2 AST sig l
body2) =
    case NameBinder n l -> NameBinder n l -> UnifyNameBinders n l l
forall (i :: S) (l :: S) (r :: S).
NameBinder i l -> NameBinder i r -> UnifyNameBinders i l r
Foil.unifyNameBinders NameBinder n l
binder1 NameBinder n l
binder2 of
      -- if binders are the same, then we can safely compare bodies
      UnifyNameBinders n l l
Foil.SameNameBinders ->  -- after seeing this we know that body scopes are the same
        case NameBinder n l -> DistinctEvidence l
forall (n :: S) (l :: S).
Distinct n =>
NameBinder n l -> DistinctEvidence l
Foil.assertDistinct NameBinder n l
binder1 of
          DistinctEvidence l
Foil.Distinct ->
            let scope1 :: Scope l
scope1 = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder1 Scope n
scope
            in Scope l -> AST sig l -> AST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n -> Bool
alphaEquiv Scope l
scope1 AST sig l
body1 AST sig l
AST sig l
body2
      -- if we can safely rename first binder into second
      Foil.RenameLeftNameBinder NameBinder n l -> NameBinder n l
rename1to2 ->
        case NameBinder n l -> DistinctEvidence l
forall (n :: S) (l :: S).
Distinct n =>
NameBinder n l -> DistinctEvidence l
Foil.assertDistinct NameBinder n l
binder2 of
          DistinctEvidence l
Foil.Distinct ->
            let scope2 :: Scope l
scope2 = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder2 Scope n
scope
            in Scope l -> AST sig l -> AST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n -> Bool
alphaEquiv Scope l
scope2 (Scope l -> (Name l -> Name l) -> AST sig l -> AST 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 sig l
body1) AST sig l
body2
      -- if we can safely rename second binder into first
      Foil.RenameRightNameBinder NameBinder n l -> NameBinder n l
rename2to1 ->
        case NameBinder n l -> DistinctEvidence l
forall (n :: S) (l :: S).
Distinct n =>
NameBinder n l -> DistinctEvidence l
Foil.assertDistinct NameBinder n l
binder1 of
          DistinctEvidence l
Foil.Distinct ->
            let scope1 :: Scope l
scope1 = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder1 Scope n
scope
            in Scope l -> AST sig l -> AST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S).
(Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) =>
Scope n -> AST sig n -> AST sig n -> Bool
alphaEquiv Scope l
scope1 AST sig l
body1 (Scope l -> (Name l -> Name l) -> AST sig l -> AST 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 sig l
body2)

-- ** 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
  :: (Bifoldable sig, ZipMatch sig)
  => AST sig n
  -> AST sig l
  -> Bool
unsafeEqAST :: forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
AST sig n -> AST 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 sig n) (AST sig n)
t1) (Node sig (ScopedAST sig l) (AST sig l)
t2) =
  case sig (ScopedAST sig n) (AST sig n)
-> sig (ScopedAST sig l) (AST sig l)
-> Maybe
     (sig (ScopedAST sig n, ScopedAST sig l) (AST sig n, AST sig l))
forall scope term scope' term'.
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch sig (ScopedAST sig n) (AST sig n)
t1 sig (ScopedAST sig l) (AST sig l)
t2 of
    Maybe
  (sig (ScopedAST sig n, ScopedAST sig l) (AST sig n, AST sig l))
Nothing -> Bool
False
    Just sig (ScopedAST sig n, ScopedAST sig l) (AST sig n, AST sig l)
tt -> All -> Bool
getAll (((ScopedAST sig n, ScopedAST sig l) -> All)
-> ((AST sig n, AST sig l) -> All)
-> sig (ScopedAST sig n, ScopedAST sig l) (AST sig n, AST 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 sig n, ScopedAST sig l) -> Bool)
-> (ScopedAST sig n, ScopedAST sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScopedAST sig n -> ScopedAST sig l -> Bool)
-> (ScopedAST sig n, ScopedAST sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ScopedAST sig n -> ScopedAST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
ScopedAST sig n -> ScopedAST sig l -> Bool
unsafeEqScopedAST) (Bool -> All
All (Bool -> All)
-> ((AST sig n, AST sig l) -> Bool)
-> (AST sig n, AST sig l)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AST sig n -> AST sig l -> Bool) -> (AST sig n, AST sig l) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry AST sig n -> AST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
AST sig n -> AST sig l -> Bool
unsafeEqAST) sig (ScopedAST sig n, ScopedAST sig l) (AST sig n, AST sig l)
tt)
unsafeEqAST AST sig n
_ AST sig l
_ = Bool
False

-- | A version of 'unsafeEqAST' for scoped terms.
unsafeEqScopedAST
  :: (Bifoldable sig, ZipMatch sig)
  => ScopedAST sig n
  -> ScopedAST sig l
  -> Bool
unsafeEqScopedAST :: forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
ScopedAST sig n -> ScopedAST sig l -> Bool
unsafeEqScopedAST (ScopedAST NameBinder n l
binder1 AST sig l
body1) (ScopedAST NameBinder l l
binder2 AST sig l
body2) = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
  [ NameBinder n l
binder1 NameBinder n l -> NameBinder n l -> Bool
forall a. Eq a => a -> a -> Bool
== NameBinder l l -> NameBinder n l
forall a b. Coercible a b => a -> b
coerce NameBinder l l
binder2
  , AST sig l
body1 AST sig l -> AST sig l -> Bool
forall (sig :: * -> * -> *) (n :: S) (l :: S).
(Bifoldable sig, ZipMatch sig) =>
AST sig n -> AST sig l -> Bool
`unsafeEqAST` AST sig l
body2
  ]

-- ** Syntactic matching (unification)

-- | Perform one-level matching for the two (non-variable) terms.
class ZipMatch sig where
  zipMatch
    :: sig scope term     -- ^ Left non-variable term.
    -> sig scope' term'   -- ^ Right non-variable term.
    -> Maybe (sig (scope, scope') (term, term'))

instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where
  zipMatch :: forall scope term scope' term'.
Sum f g scope term
-> Sum f g scope' term'
-> Maybe (Sum f g (scope, scope') (term, term'))
zipMatch (L2 f scope term
f) (L2 f scope' term'
f') = f (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term')
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
p a b -> Sum p q a b
L2 (f (scope, scope') (term, term')
 -> Sum f g (scope, scope') (term, term'))
-> Maybe (f (scope, scope') (term, term'))
-> Maybe (Sum f g (scope, scope') (term, term'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f scope term
-> f scope' term' -> Maybe (f (scope, scope') (term, term'))
forall scope term scope' term'.
f scope term
-> f scope' term' -> Maybe (f (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch f scope term
f f scope' term'
f'
  zipMatch (R2 g scope term
g) (R2 g scope' term'
g') = g (scope, scope') (term, term')
-> Sum f g (scope, scope') (term, term')
forall {k} {k1} (p :: k -> k1 -> *) (q :: k -> k1 -> *) (a :: k)
       (b :: k1).
q a b -> Sum p q a b
R2 (g (scope, scope') (term, term')
 -> Sum f g (scope, scope') (term, term'))
-> Maybe (g (scope, scope') (term, term'))
-> Maybe (Sum f g (scope, scope') (term, term'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g scope term
-> g scope' term' -> Maybe (g (scope, scope') (term, term'))
forall scope term scope' term'.
g scope term
-> g scope' term' -> Maybe (g (scope, scope') (term, term'))
forall (sig :: * -> * -> *) scope term scope' term'.
ZipMatch sig =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
zipMatch g scope term
g g scope' term'
g'
  zipMatch Sum f g scope term
_ Sum f g scope' term'
_            = Maybe (Sum f g (scope, scope') (term, term'))
forall a. Maybe a
Nothing

-- * Converting to and from free foil

-- ** Convert to free foil

convertToAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -> (rawPattern -> Maybe rawIdent)
  -> (rawScopedTerm -> rawTerm)
  -> Foil.Scope n
  -> Map rawIdent (Foil.Name n) -> rawTerm -> AST sig n
convertToAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent rawTerm rawPattern
       rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawPattern -> Maybe rawIdent
getPatternBinder 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 sig n
forall a. HasCallStack => [Char] -> a
error [Char]
"undefined variable"
        Just Name n
name -> Name n -> AST sig n
forall (n :: S) (sig :: * -> * -> *). Name n -> AST sig n
Var Name n
name
    Right sig (rawPattern, rawScopedTerm) rawTerm
node -> sig (ScopedAST sig n) (AST sig n) -> AST sig n
forall (sig :: * -> * -> *) (n :: S).
sig (ScopedAST sig n) (AST sig n) -> AST sig n
Node (sig (ScopedAST sig n) (AST sig n) -> AST sig n)
-> sig (ScopedAST sig n) (AST sig n) -> AST sig n
forall a b. (a -> b) -> a -> b
$
      ((rawPattern, rawScopedTerm) -> ScopedAST sig n)
-> (rawTerm -> AST sig n)
-> sig (rawPattern, rawScopedTerm) rawTerm
-> sig (ScopedAST sig n) (AST 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))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent rawTerm rawPattern
       rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawPattern -> Maybe rawIdent
getPatternBinder rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
        ((rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST sig n
forall (n :: S) (sig :: * -> * -> *) rawIdent rawTerm rawPattern
       rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawPattern -> Maybe rawIdent
getPatternBinder rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names)
        sig (rawPattern, rawScopedTerm) rawTerm
node

convertToScopedAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -> (rawPattern -> Maybe rawIdent)
  -> (rawScopedTerm -> rawTerm)
  -> Foil.Scope n
  -> Map rawIdent (Foil.Name n)
  -> (rawPattern, rawScopedTerm)
  -> ScopedAST sig n
convertToScopedAST :: forall (n :: S) (sig :: * -> * -> *) rawIdent rawTerm rawPattern
       rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST sig n
convertToScopedAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawPattern -> Maybe rawIdent
getPatternBinder rawScopedTerm -> rawTerm
getScopedTerm Scope n
scope Map rawIdent (Name n)
names (rawPattern
pat, rawScopedTerm
scopedTerm) =
  Scope n
-> (forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
-> ScopedAST sig n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
 -> ScopedAST sig n)
-> (forall {l :: S}. DExt n l => NameBinder n l -> ScopedAST sig n)
-> ScopedAST sig n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
        names' :: Map rawIdent (Name l)
names' =
          case rawPattern -> Maybe rawIdent
getPatternBinder rawPattern
pat of
            Maybe rawIdent
Nothing -> Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (Name n -> Name l)
-> Map rawIdent (Name n) -> Map rawIdent (Name l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map rawIdent (Name n)
names
            Just rawIdent
x  -> rawIdent
-> Name l -> Map rawIdent (Name l) -> Map rawIdent (Name l)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert rawIdent
x (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) (Name n -> Name l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (Name n -> Name l)
-> Map rawIdent (Name n) -> Map rawIdent (Name l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map rawIdent (Name n)
names)
     in NameBinder n l -> AST sig l -> ScopedAST sig n
forall (n :: S) (l :: S) (sig :: * -> * -> *).
NameBinder n l -> AST sig l -> ScopedAST sig n
ScopedAST NameBinder n l
binder ((rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope l
-> Map rawIdent (Name l)
-> rawTerm
-> AST sig l
forall (n :: S) (sig :: * -> * -> *) rawIdent rawTerm rawPattern
       rawScopedTerm.
(Distinct n, Bifunctor sig, Ord rawIdent) =>
(rawTerm
 -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (rawPattern -> Maybe rawIdent)
-> (rawScopedTerm -> rawTerm)
-> Scope n
-> Map rawIdent (Name n)
-> rawTerm
-> AST sig n
convertToAST rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawPattern -> Maybe rawIdent
getPatternBinder rawScopedTerm -> rawTerm
getScopedTerm Scope l
scope' Map rawIdent (Name l)
names' (rawScopedTerm -> rawTerm
getScopedTerm rawScopedTerm
scopedTerm))

-- ** Convert from free foil

convertFromAST
  :: Bifunctor sig
  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
  -> (rawIdent -> rawTerm)
  -> (rawIdent -> rawPattern)
  -> (rawTerm -> rawScopedTerm)
  -> (Int -> rawIdent) -> AST sig n -> rawTerm
convertFromAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar rawIdent -> 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 sig n) (AST 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 sig n -> (rawPattern, rawScopedTerm))
-> (AST sig n -> rawTerm)
-> sig (ScopedAST sig n) (AST 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)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST sig n
-> (rawPattern, rawScopedTerm)
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar rawIdent -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
      ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST sig n
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar rawIdent -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f)
      sig (ScopedAST sig n) (AST sig n)
node

convertFromScopedAST
  :: Bifunctor sig
  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
  -> (rawIdent -> rawTerm)
  -> (rawIdent -> rawPattern)
  -> (rawTerm -> rawScopedTerm)
  -> (Int -> rawIdent) -> ScopedAST sig n -> (rawPattern, rawScopedTerm)
convertFromScopedAST :: forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> ScopedAST sig n
-> (rawPattern, rawScopedTerm)
convertFromScopedAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar rawIdent -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f = \case
  ScopedAST NameBinder n l
binder AST sig l
body ->
    ( rawIdent -> rawPattern
makePattern (Int -> rawIdent
f (Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder)))
    , rawTerm -> rawScopedTerm
makeScoped ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST sig l
-> rawTerm
forall (sig :: * -> * -> *) rawPattern rawScopedTerm rawTerm
       rawIdent (n :: S).
Bifunctor sig =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (rawIdent -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Int -> rawIdent)
-> AST sig n
-> rawTerm
convertFromAST sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar rawIdent -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Int -> rawIdent
f AST sig l
body))