{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveFoldable        #-}
{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# 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.IntMap.Strict          (IntMap)
import qualified Data.IntMap.Strict          as IntMap
import           Data.Map                    (Map)
import qualified Data.Map                    as Map
import           GHC.Generics                (Generic)
import           Unsafe.Coerce               (unsafeCoerce)

-- | Scoped term under a (single) name binder.
--
-- @since 0.0.1
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@.
--
-- @since 0.0.1
data AST binder sig n where
  -- | A (free) variable in scope @n@.
  Var :: {-# UNPACK #-} !(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).
--
-- @since 0.0.1
{-# INLINABLE substitute #-}
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 AST binder sig i
term
  -- An empty substitution maps every name to itself ('addRename' deletes
  -- identity renames), so the result is the very term, and the coercion is
  -- the one 'Foil.sink' performs. Substitutions go empty often: opening a
  -- scoped term with its own binder's name is an identity rename, and under
  -- a deterministic allocation policy a refreshed binder usually keeps its
  -- name, deleting its entry. Binders that shadow the ambient scope are
  -- left as they stand, as on the no-clash path below. A caller that wants
  -- them refreshed asks 'substituteRefreshed'.
  | Substitution (AST binder sig) i o -> Bool
forall (e :: S -> *) (i :: S) (o :: S). Substitution e i o -> Bool
Foil.nullSubst Substitution (AST binder sig) i o
subst = AST binder sig i -> AST binder sig o
forall a b. a -> b
unsafeCoerce AST binder sig i
term
  | Bool
otherwise = AST binder sig i -> AST binder sig o
go AST binder sig i
term
  where
    -- The substitution is known non-empty here, and it can only change
    -- under a binder, so the walk between binders is unchecked and each
    -- binder entry re-enters 'substitute', testing emptiness exactly once.
    go :: AST binder sig i -> AST binder sig o
go = \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 AST binder sig i -> AST binder sig o
go sig (ScopedAST binder sig i) (AST binder sig i)
node)
    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' -> Scope 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' -> Scope 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' -> Scope 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' -> Scope 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' Scope o'
scope' ->
        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)
            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.
--
-- @since 0.0.3
{-# INLINABLE substituteRefreshed #-}
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' -> Scope 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' -> Scope 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' -> Scope 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' -> Scope 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' Scope o'
scope' ->
        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)
            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' -> Scope 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' -> Scope 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' -> Scope 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' -> Scope 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' Scope o'
scope' ->
          let 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.
--
-- @since 0.2.0
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.
--
-- @since 0.0.3
{-# INLINABLE refreshAST #-}
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.
--
-- @since 0.0.3
{-# INLINABLE refreshScopedAST #-}
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' -> Scope 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' -> Scope 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' -> Scope 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' -> Scope 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' Scope o'
scope' ->
    let 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 renames every binder on both sides
-- unconditionally, so it does strictly more work. It remains as an
-- independent implementation of the same test.
--
-- @since 0.0.3
{-# INLINABLE alphaEquivRefreshed #-}
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

-- | A term is a scope-indexed value that can be compared up to α, which is what
-- a pattern carrying terms as payloads needs of them.
instance (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.SinkableK binder)
    => Foil.AlphaEquiv (AST binder sig) where
  alphaEquivIn :: forall (n :: S).
Distinct n =>
Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquivIn = 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

-- | \(\alpha\)-equivalence check for two terms in one scope
-- via unification of bound variables (via 'unifyNameBinders').
--
-- When two matching binders coincide, comparison continues with no work at
-- all. When they differ, the prescribed renaming is /threaded down the
-- recursion/ (see 'alphaEquivEnv') and consulted at variables only, so
-- nothing is ever copied. Applying the renaming eagerly instead would
-- materialise a renamed copy of the remaining body at every mismatched
-- binder, which is quadratic on a chain of them.
--
-- @since 0.0.3
{-# INLINABLE alphaEquiv #-}
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 (ScopedAST binder sig n -> ScopedAST binder sig n -> Maybe ())
-> (AST binder sig n -> AST binder sig n -> Maybe ())
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> Maybe (sig () ())
forall (f :: * -> * -> *) a a' a'' b b' b''.
(Bitraversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'')
-> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2 ((ScopedAST binder sig n -> Bool)
-> ScopedAST binder sig n -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((ScopedAST binder sig n -> Bool)
 -> ScopedAST binder sig n -> Maybe ())
-> (ScopedAST binder sig n -> ScopedAST binder sig n -> Bool)
-> ScopedAST binder sig n
-> ScopedAST binder sig n
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: 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) ((AST binder sig n -> Bool) -> AST binder sig n -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((AST binder sig n -> Bool) -> AST binder sig n -> Maybe ())
-> (AST binder sig n -> AST binder sig n -> Bool)
-> AST binder sig n
-> AST binder sig n
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) (AST binder sig n)
l sig (ScopedAST binder sig n) (AST binder sig n)
r of
    Maybe (sig () ())
Nothing -> Bool
False
    Just sig () ()
_  -> Bool
True
  where
    unit :: (t -> Bool) -> t -> Maybe ()
unit t -> Bool
f t
x = if t -> Bool
f t
x then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
alphaEquiv Scope n
_ AST binder sig n
_ AST binder sig n
_ = Bool
False

-- | Same as 'alphaEquiv' but for scoped terms.
--
-- While the binders of the two sides coincide, this runs with no renaming
-- state at all. The first pair that differs switches to 'alphaEquivEnv',
-- which threads the renamings down and switches back when they empty out.
--
-- @since 0.0.3
{-# INLINABLE alphaEquivScoped #-}
alphaEquivScoped
  :: forall sig binder n. (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 :: * -> * -> *) (binder :: S -> S -> *) (n :: 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 Scope n
-> binder n l -> binder n l -> UnifyNameBinders binder n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Scope 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) =>
Scope n
-> pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
Foil.unifyPatternsIn Scope n
scope binder n l
binder1 binder n l
binder2 of
      -- the binders coincide: compare the bodies as they stand
      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
      -- the left binder is renamed towards the right one
      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
                pairs :: [(Id, Id)]
pairs = [ (Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
x, (NameBinder n l -> NameBinder n l) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n l
rename1to2 Name l
x)
                        | Name l
x <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder1 ]
            in [(Id, Id)]
-> Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (m :: S) (l1 :: S) (l2 :: S).
Distinct m =>
[(Id, Id)]
-> Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool
enterEnv [(Id, Id)]
pairs Scope l
scope2 AST binder sig l
body1 AST binder sig l
body2
      -- the right binder is renamed towards the left one
      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
                pairs :: [(Id, Id)]
pairs = [ ((NameBinder n l -> NameBinder n l) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n l
rename2to1 Name l
y, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
y)
                        | Name l
y <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder2 ]
            in [(Id, Id)]
-> Scope l -> AST binder sig l -> AST binder sig l -> Bool
forall (m :: S) (l1 :: S) (l2 :: S).
Distinct m =>
[(Id, Id)]
-> Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool
enterEnv [(Id, Id)]
pairs Scope l
scope1 AST binder sig l
body1 AST binder sig l
body2
      -- both are renamed towards a unified pattern: pair the two sides'
      -- names through the unified name each maps to
      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
                leftU :: IntMap Id
leftU = [(Id, Id)] -> IntMap Id
forall a. [(Id, a)] -> IntMap a
IntMap.fromList
                  [ ((NameBinder n l -> NameBinder n lr) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n lr
rename1 Name l
x, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
x)
                  | Name l
x <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder1 ]
                rightU :: IntMap Id
rightU = [(Id, Id)] -> IntMap Id
forall a. [(Id, a)] -> IntMap a
IntMap.fromList
                  [ ((NameBinder n l -> NameBinder n lr) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n lr
rename2 Name l
y, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
y)
                  | Name l
y <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder2 ]
                pairs :: [(Id, Id)]
pairs = IntMap (Id, Id) -> [(Id, Id)]
forall a. IntMap a -> [a]
IntMap.elems ((Id -> Id -> (Id, Id)) -> IntMap Id -> IntMap Id -> IntMap (Id, Id)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith (,) IntMap Id
leftU IntMap Id
rightU)
            in [(Id, Id)]
-> Scope lr -> AST binder sig l -> AST binder sig l -> Bool
forall (m :: S) (l1 :: S) (l2 :: S).
Distinct m =>
[(Id, Id)]
-> Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool
enterEnv [(Id, Id)]
pairs Scope lr
scope' AST binder sig l
body1 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
  where
    enterEnv
      :: forall m l1 l2. Foil.Distinct m
      => [(Int, Int)] -> Foil.Scope m
      -> AST binder sig l1 -> AST binder sig l2 -> Bool
    enterEnv :: forall (m :: S) (l1 :: S) (l2 :: S).
Distinct m =>
[(Id, Id)]
-> Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool
enterEnv [(Id, Id)]
pairs Scope m
scope' = Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
0 IntMap Id
forall a. IntMap a
IntMap.empty IntMap Id
forall a. IntMap a
IntMap.empty [(Id, Id)]
pairs Scope m
scope'

-- | The raw name a verdict's renaming assigns to a pattern's name.
--
-- @since 0.4.0
renamedId :: (Foil.NameBinder n a -> Foil.NameBinder n b) -> Foil.Name a -> Int
renamedId :: forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n a -> NameBinder n b
rename = Name b -> Id
forall (l :: S). Name l -> Id
Foil.nameId (Name b -> Id) -> (Name a -> Name b) -> Name a -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameBinder n b -> Name b
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf (NameBinder n b -> Name b)
-> (Name a -> NameBinder n b) -> Name a -> Name b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameBinder n a -> NameBinder n b
rename (NameBinder n a -> NameBinder n b)
-> (Name a -> NameBinder n a) -> Name a -> NameBinder n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> NameBinder n a
forall (n :: S) (l :: S). Name l -> NameBinder n l
Foil.UnsafeNameBinder

-- | Bind the paired names of a binder pair. A pair whose names coincide
-- shadows both sides identically and is deleted from the environments. A pair
-- whose names differ binds both to one fresh level. Continues with
-- 'alphaEquivEnv' on the bodies.
--
-- @since 0.4.0
bindPairs
  :: forall sig binder m l1 l2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct m, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Int -> IntMap Int -> IntMap Int -> [(Int, Int)]
  -> Foil.Scope m
  -> AST binder sig l1 -> AST binder sig l2 -> Bool
bindPairs :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
lvl IntMap Id
envL IntMap Id
envR [(Id, Id)]
pairs Scope m
scope AST binder sig l1
body1 AST binder sig l2
body2 = case [(Id, Id)]
pairs of
  [] -> Id
-> IntMap Id
-> IntMap Id
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> AST binder sig n1
-> AST binder sig n2
-> Bool
alphaEquivEnv Id
lvl IntMap Id
envL IntMap Id
envR Scope m
scope AST binder sig l1
body1 AST binder sig l2
body2
  ((Id
x, Id
y) : [(Id, Id)]
rest)
    | Id
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
y    -> Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
lvl (Id -> IntMap Id -> IntMap Id
forall a. Id -> IntMap a -> IntMap a
IntMap.delete Id
x IntMap Id
envL) (Id -> IntMap Id -> IntMap Id
forall a. Id -> IntMap a -> IntMap a
IntMap.delete Id
y IntMap Id
envR) [(Id, Id)]
rest Scope m
scope AST binder sig l1
body1 AST binder sig l2
body2
    | Bool
otherwise -> Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs (Id
lvl Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
1) (Id -> Id -> IntMap Id -> IntMap Id
forall a. Id -> a -> IntMap a -> IntMap a
IntMap.insert Id
x Id
lvl IntMap Id
envL) (Id -> Id -> IntMap Id -> IntMap Id
forall a. Id -> a -> IntMap a -> IntMap a
IntMap.insert Id
y Id
lvl IntMap Id
envR) [(Id, Id)]
rest Scope m
scope AST binder sig l1
body1 AST binder sig l2
body2

-- | The renaming-threading worker behind 'alphaEquiv': compare two terms
-- under partial renamings of their names into shared /levels/.
--
-- Each environment maps a raw name to the level of the binder pair that bound
-- it on the comparison path, and a name outside its environment stands for
-- itself. A variable occurrence then compares as a level against a level, or
-- as a raw name against a raw name, and the two can never be conflated. This
-- is what makes threading sound where applying a raw renaming at the variables
-- would not be, since a renamed name could collide with one that passes
-- through unchanged and happens to share the target spelling. Levels are also
-- why no capture check is needed: a level is never a name, so there is nothing
-- for a binder to capture.
--
-- A binder pair whose names coincide /deletes/ those names from both
-- environments, the pair shadowing both sides identically. When the
-- environments empty out the comparison drops back to the stateless
-- 'alphaEquiv', so only the region of the terms below a mismatched binder,
-- and above the point where the mismatch is shadowed away, pays for the
-- threading at all.
--
-- The indices of the two terms are deliberately independent, in the style
-- of 'unsafeEqAST': the terms are never renamed into a common scope, so
-- no common index exists to give them.
--
-- @since 0.4.0
{-# INLINABLE alphaEquivEnv #-}
alphaEquivEnv
  :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Int          -- ^ Next fresh level.
  -> IntMap Int   -- ^ Left renaming: raw name to the level that bound it.
  -> IntMap Int   -- ^ Right renaming.
  -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Foil.unifyPatternsIn').
  -> AST binder sig n1
  -> AST binder sig n2
  -> Bool
alphaEquivEnv :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> AST binder sig n1
-> AST binder sig n2
-> Bool
alphaEquivEnv Id
lvl IntMap Id
envL IntMap Id
envR Scope n
scope AST binder sig n1
t1 AST binder sig n2
t2
  | IntMap Id -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Id
envL Bool -> Bool -> Bool
&& IntMap Id -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap Id
envR =
      -- The renamings have emptied out (or never held anything): the
      -- terms coincide raw-for-raw from here on, so compare them where
      -- they stand. The coercion brings both indices to the scope's,
      -- which is the unified path the comparison speaks of.
      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 (AST binder sig n1 -> AST binder sig n
forall a b. a -> b
unsafeCoerce AST binder sig n1
t1 :: AST binder sig n) (AST binder sig n2 -> AST binder sig n
forall a b. a -> b
unsafeCoerce AST binder sig n2
t2 :: AST binder sig n)
  | Bool
otherwise = case (AST binder sig n1
t1, AST binder sig n2
t2) of
      (Var Name n1
x, Var Name n2
y) ->
        case (Id -> IntMap Id -> Maybe Id
forall a. Id -> IntMap a -> Maybe a
IntMap.lookup (Name n1 -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name n1
x) IntMap Id
envL, Id -> IntMap Id -> Maybe Id
forall a. Id -> IntMap a -> Maybe a
IntMap.lookup (Name n2 -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name n2
y) IntMap Id
envR) of
          (Just Id
k1, Just Id
k2) -> Id
k1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
k2
          (Maybe Id
Nothing, Maybe Id
Nothing) -> Name n1 -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name n1
x Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Name n2 -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name n2
y
          (Maybe Id, Maybe Id)
_                  -> Bool
False
      (Node sig (ScopedAST binder sig n1) (AST binder sig n1)
l, Node sig (ScopedAST binder sig n2) (AST binder sig n2)
r) ->
        case (ScopedAST binder sig n1 -> ScopedAST binder sig n2 -> Maybe ())
-> (AST binder sig n1 -> AST binder sig n2 -> Maybe ())
-> sig (ScopedAST binder sig n1) (AST binder sig n1)
-> sig (ScopedAST binder sig n2) (AST binder sig n2)
-> Maybe (sig () ())
forall (f :: * -> * -> *) a a' a'' b b' b''.
(Bitraversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'')
-> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2
               ((ScopedAST binder sig n2 -> Bool)
-> ScopedAST binder sig n2 -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((ScopedAST binder sig n2 -> Bool)
 -> ScopedAST binder sig n2 -> Maybe ())
-> (ScopedAST binder sig n1 -> ScopedAST binder sig n2 -> Bool)
-> ScopedAST binder sig n1
-> ScopedAST binder sig n2
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> ScopedAST binder sig n1
-> ScopedAST binder sig n2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> ScopedAST binder sig n1
-> ScopedAST binder sig n2
-> Bool
alphaEquivScopedEnv Id
lvl IntMap Id
envL IntMap Id
envR Scope n
scope)
               ((AST binder sig n2 -> Bool) -> AST binder sig n2 -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((AST binder sig n2 -> Bool) -> AST binder sig n2 -> Maybe ())
-> (AST binder sig n1 -> AST binder sig n2 -> Bool)
-> AST binder sig n1
-> AST binder sig n2
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> AST binder sig n1
-> AST binder sig n2
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> AST binder sig n1
-> AST binder sig n2
-> Bool
alphaEquivEnv Id
lvl IntMap Id
envL IntMap Id
envR Scope n
scope) sig (ScopedAST binder sig n1) (AST binder sig n1)
l sig (ScopedAST binder sig n2) (AST binder sig n2)
r of
          Maybe (sig () ())
Nothing -> Bool
False
          Just sig () ()
_  -> Bool
True
      (AST binder sig n1, AST binder sig n2)
_ -> Bool
False
  where
    unit :: (t -> Bool) -> t -> Maybe ()
unit t -> Bool
f t
x = if t -> Bool
f t
x then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing

-- | The scoped half of 'alphaEquivEnv': get the verdict from
-- 'Foil.unifyPatternsIn', extend the environments as it prescribes, and
-- recurse into the bodies as they stand.
--
-- @since 0.4.0
{-# INLINABLE alphaEquivScopedEnv #-}
alphaEquivScopedEnv
  :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder)
  => Int
  -> IntMap Int
  -> IntMap Int
  -> Foil.Scope n
  -> ScopedAST binder sig n1
  -> ScopedAST binder sig n2
  -> Bool
alphaEquivScopedEnv :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> ScopedAST binder sig n1
-> ScopedAST binder sig n2
-> Bool
alphaEquivScopedEnv Id
lvl IntMap Id
envL IntMap Id
envR Scope n
scope ScopedAST binder sig n1
scoped1 ScopedAST binder sig n2
scoped2 =
  -- The scoped terms are compared where they stand; the coercion only
  -- brings their indices to the scope's, which is the unified path the
  -- environments and the verdicts speak of.
  case (ScopedAST binder sig n1 -> ScopedAST binder sig n
forall a b. a -> b
unsafeCoerce ScopedAST binder sig n1
scoped1 :: ScopedAST binder sig n, ScopedAST binder sig n2 -> ScopedAST binder sig n
forall a b. a -> b
unsafeCoerce ScopedAST binder sig n2
scoped2 :: ScopedAST binder sig n) of
    (ScopedAST binder n l
binder1 AST binder sig l
body1, ScopedAST binder n l
binder2 AST binder sig l
body2) ->
      case Scope n
-> binder n l -> binder n l -> UnifyNameBinders binder n l l
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
Scope 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) =>
Scope n
-> pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
Foil.unifyPatternsIn Scope n
scope binder n l
binder1 binder n l
binder2 of
        -- the binders coincide: the pair shadows both sides identically
        Foil.SameNameBinders{} ->
          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 scope' :: Scope l
scope' = 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
                  names :: [Id]
names = (Name l -> Id) -> [Name l] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId (binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder1)
                  envL' :: IntMap Id
envL' = [Id] -> IntMap Id -> IntMap Id
forall {a}. [Id] -> IntMap a -> IntMap a
deleteAll [Id]
names IntMap Id
envL
                  envR' :: IntMap Id
envR' = [Id] -> IntMap Id -> IntMap Id
forall {a}. [Id] -> IntMap a -> IntMap a
deleteAll [Id]
names IntMap Id
envR
               in Id
-> IntMap Id
-> IntMap Id
-> Scope l
-> AST binder sig l
-> AST binder sig l
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (n :: S)
       (n1 :: S) (n2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct n,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> Scope n
-> AST binder sig n1
-> AST binder sig n2
-> Bool
alphaEquivEnv Id
lvl IntMap Id
envL' IntMap Id
envR' Scope l
scope' AST binder sig l
body1 AST binder sig l
body2
        -- the left binder is renamed towards the right one
        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 scope' :: Scope l
scope' = 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
                  pairs :: [(Id, Id)]
pairs = [ (Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
x, (NameBinder n l -> NameBinder n l) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n l
rename1to2 Name l
x)
                          | Name l
x <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder1 ]
               in Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope l
-> AST binder sig l
-> AST binder sig l
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
lvl IntMap Id
envL IntMap Id
envR [(Id, Id)]
pairs Scope l
scope' AST binder sig l
body1 AST binder sig l
body2
        -- the right binder is renamed towards the left one
        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 scope' :: Scope l
scope' = 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
                  pairs :: [(Id, Id)]
pairs = [ ((NameBinder n l -> NameBinder n l) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n l
rename2to1 Name l
y, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
y)
                          | Name l
y <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder2 ]
               in Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope l
-> AST binder sig l
-> AST binder sig l
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
lvl IntMap Id
envL IntMap Id
envR [(Id, Id)]
pairs Scope l
scope' AST binder sig l
body1 AST binder sig l
body2
        -- both are renamed towards a unified pattern: pair the two sides'
        -- names through the unified name each maps to
        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
                  leftU :: IntMap Id
leftU = [(Id, Id)] -> IntMap Id
forall a. [(Id, a)] -> IntMap a
IntMap.fromList
                    [ ((NameBinder n l -> NameBinder n lr) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n lr
rename1 Name l
x, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
x)
                    | Name l
x <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder1 ]
                  rightU :: IntMap Id
rightU = [(Id, Id)] -> IntMap Id
forall a. [(Id, a)] -> IntMap a
IntMap.fromList
                    [ ((NameBinder n l -> NameBinder n lr) -> Name l -> Id
forall (n :: S) (a :: S) (b :: S).
(NameBinder n a -> NameBinder n b) -> Name a -> Id
renamedId NameBinder n l -> NameBinder n lr
rename2 Name l
y, Name l -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name l
y)
                    | Name l
y <- binder n l -> [Name l]
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
Foil.namesOfPattern binder n l
binder2 ]
                  pairs :: [(Id, Id)]
pairs = IntMap (Id, Id) -> [(Id, Id)]
forall a. IntMap a -> [a]
IntMap.elems ((Id -> Id -> (Id, Id)) -> IntMap Id -> IntMap Id -> IntMap (Id, Id)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith (,) IntMap Id
leftU IntMap Id
rightU)
               in Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope lr
-> AST binder sig l
-> AST binder sig l
-> Bool
forall (sig :: * -> * -> *) (binder :: S -> S -> *) (m :: S)
       (l1 :: S) (l2 :: S).
(Bitraversable sig, ZipMatchK sig, Distinct m,
 UnifiablePattern binder, SinkableK binder) =>
Id
-> IntMap Id
-> IntMap Id
-> [(Id, Id)]
-> Scope m
-> AST binder sig l1
-> AST binder sig l2
-> Bool
bindPairs Id
lvl IntMap Id
envL IntMap Id
envR [(Id, Id)]
pairs Scope lr
scope' AST binder sig l
body1 AST binder sig l
body2
        UnifyNameBinders binder n l l
Foil.NotUnifiable -> Bool
False
  where
    deleteAll :: [Id] -> IntMap a -> IntMap a
deleteAll [Id]
names IntMap a
env = case [Id]
names of
      []       -> IntMap a
env
      (Id
i : [Id]
is) -> [Id] -> IntMap a -> IntMap a
deleteAll [Id]
is (Id -> IntMap a -> IntMap a
forall a. Id -> IntMap a -> IntMap a
IntMap.delete Id
i IntMap a
env)

-- ** 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).
--
-- @since 0.0.3
{-# INLINABLE unsafeEqAST #-}
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 (ScopedAST binder sig n -> ScopedAST binder sig l -> Maybe ())
-> (AST binder sig n -> AST binder sig l -> Maybe ())
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> sig (ScopedAST binder sig l) (AST binder sig l)
-> Maybe (sig () ())
forall (f :: * -> * -> *) a a' a'' b b' b''.
(Bitraversable f, ZipMatchK f) =>
(a -> a' -> Maybe a'')
-> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'')
zipMatchWith2 ((ScopedAST binder sig l -> Bool)
-> ScopedAST binder sig l -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((ScopedAST binder sig l -> Bool)
 -> ScopedAST binder sig l -> Maybe ())
-> (ScopedAST binder sig n -> ScopedAST binder sig l -> Bool)
-> ScopedAST binder sig n
-> ScopedAST binder sig l
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) ((AST binder sig l -> Bool) -> AST binder sig l -> Maybe ()
forall {t}. (t -> Bool) -> t -> Maybe ()
unit ((AST binder sig l -> Bool) -> AST binder sig l -> Maybe ())
-> (AST binder sig n -> AST binder sig l -> Bool)
-> AST binder sig n
-> AST binder sig l
-> Maybe ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) (AST binder sig n)
t1 sig (ScopedAST binder sig l) (AST binder sig l)
t2 of
    Maybe (sig () ())
Nothing -> Bool
False
    Just sig () ()
_  -> Bool
True
  where
    unit :: (t -> Bool) -> t -> Maybe ()
unit t -> Bool
f t
x = if t -> Bool
f t
x then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
unsafeEqAST AST binder sig n
_ AST binder sig l
_ = Bool
False

-- | A version of 'unsafeEqAST' for scoped terms.
--
-- @since 0.0.3
{-# INLINABLE unsafeEqScopedAST #-}
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

-- | An identifier a raw term mentions that the names given for conversion do
-- not account for.
--
-- Note what this does and does not carry. It cannot carry a position: the
-- conversion functions are generic in the raw term and only ever see it through
-- @toSig@, so a source location, if the syntax has one, is not theirs to read.
-- What they do know, and a caller checking names beforehand does not, is which
-- names were in scope /at the occurrence/, the binders passed on the way down
-- included. That is what a \"did you mean\" needs.
--
-- @since 0.4.0
data UnresolvedName rawIdent = UnresolvedName
  { forall rawIdent. UnresolvedName rawIdent -> rawIdent
unresolvedIdent   :: rawIdent
    -- ^ The identifier that did not resolve.
  , forall rawIdent. UnresolvedName rawIdent -> [rawIdent]
unresolvedInScope :: [rawIdent]
    -- ^ What was in scope where it occurred.
  } deriving (UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
(UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool)
-> (UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool)
-> Eq (UnresolvedName rawIdent)
forall rawIdent.
Eq rawIdent =>
UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall rawIdent.
Eq rawIdent =>
UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
== :: UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
$c/= :: forall rawIdent.
Eq rawIdent =>
UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
/= :: UnresolvedName rawIdent -> UnresolvedName rawIdent -> Bool
Eq, Id -> UnresolvedName rawIdent -> ShowS
[UnresolvedName rawIdent] -> ShowS
UnresolvedName rawIdent -> String
(Id -> UnresolvedName rawIdent -> ShowS)
-> (UnresolvedName rawIdent -> String)
-> ([UnresolvedName rawIdent] -> ShowS)
-> Show (UnresolvedName rawIdent)
forall rawIdent.
Show rawIdent =>
Id -> UnresolvedName rawIdent -> ShowS
forall rawIdent.
Show rawIdent =>
[UnresolvedName rawIdent] -> ShowS
forall rawIdent. Show rawIdent => UnresolvedName rawIdent -> String
forall a.
(Id -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall rawIdent.
Show rawIdent =>
Id -> UnresolvedName rawIdent -> ShowS
showsPrec :: Id -> UnresolvedName rawIdent -> ShowS
$cshow :: forall rawIdent. Show rawIdent => UnresolvedName rawIdent -> String
show :: UnresolvedName rawIdent -> String
$cshowList :: forall rawIdent.
Show rawIdent =>
[UnresolvedName rawIdent] -> ShowS
showList :: [UnresolvedName rawIdent] -> ShowS
Show, (forall a b. (a -> b) -> UnresolvedName a -> UnresolvedName b)
-> (forall a b. a -> UnresolvedName b -> UnresolvedName a)
-> Functor UnresolvedName
forall a b. a -> UnresolvedName b -> UnresolvedName a
forall a b. (a -> b) -> UnresolvedName a -> UnresolvedName b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> UnresolvedName a -> UnresolvedName b
fmap :: forall a b. (a -> b) -> UnresolvedName a -> UnresolvedName b
$c<$ :: forall a b. a -> UnresolvedName b -> UnresolvedName a
<$ :: forall a b. a -> UnresolvedName b -> UnresolvedName a
Functor, (forall m. Monoid m => UnresolvedName m -> m)
-> (forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m)
-> (forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m)
-> (forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b)
-> (forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b)
-> (forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b)
-> (forall a. (a -> a -> a) -> UnresolvedName a -> a)
-> (forall a. (a -> a -> a) -> UnresolvedName a -> a)
-> (forall rawIdent. UnresolvedName rawIdent -> [rawIdent])
-> (forall a. UnresolvedName a -> Bool)
-> (forall a. UnresolvedName a -> Id)
-> (forall a. Eq a => a -> UnresolvedName a -> Bool)
-> (forall a. Ord a => UnresolvedName a -> a)
-> (forall a. Ord a => UnresolvedName a -> a)
-> (forall a. Num a => UnresolvedName a -> a)
-> (forall a. Num a => UnresolvedName a -> a)
-> Foldable UnresolvedName
forall a. Eq a => a -> UnresolvedName a -> Bool
forall a. Num a => UnresolvedName a -> a
forall a. Ord a => UnresolvedName a -> a
forall m. Monoid m => UnresolvedName m -> m
forall a. UnresolvedName a -> Bool
forall a. UnresolvedName a -> Id
forall rawIdent. UnresolvedName rawIdent -> [rawIdent]
forall a. (a -> a -> a) -> UnresolvedName a -> a
forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m
forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b
forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Id)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => UnresolvedName m -> m
fold :: forall m. Monoid m => UnresolvedName m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> UnresolvedName a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b
foldr :: forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> UnresolvedName a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b
foldl :: forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> UnresolvedName a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> UnresolvedName a -> a
foldr1 :: forall a. (a -> a -> a) -> UnresolvedName a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> UnresolvedName a -> a
foldl1 :: forall a. (a -> a -> a) -> UnresolvedName a -> a
$ctoList :: forall rawIdent. UnresolvedName rawIdent -> [rawIdent]
toList :: forall rawIdent. UnresolvedName rawIdent -> [rawIdent]
$cnull :: forall a. UnresolvedName a -> Bool
null :: forall a. UnresolvedName a -> Bool
$clength :: forall a. UnresolvedName a -> Id
length :: forall a. UnresolvedName a -> Id
$celem :: forall a. Eq a => a -> UnresolvedName a -> Bool
elem :: forall a. Eq a => a -> UnresolvedName a -> Bool
$cmaximum :: forall a. Ord a => UnresolvedName a -> a
maximum :: forall a. Ord a => UnresolvedName a -> a
$cminimum :: forall a. Ord a => UnresolvedName a -> a
minimum :: forall a. Ord a => UnresolvedName a -> a
$csum :: forall a. Num a => UnresolvedName a -> a
sum :: forall a. Num a => UnresolvedName a -> a
$cproduct :: forall a. Num a => UnresolvedName a -> a
product :: forall a. Num a => UnresolvedName a -> a
Foldable, Functor UnresolvedName
Foldable UnresolvedName
(Functor UnresolvedName, Foldable UnresolvedName) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> UnresolvedName a -> f (UnresolvedName b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    UnresolvedName (f a) -> f (UnresolvedName a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> UnresolvedName a -> m (UnresolvedName b))
-> (forall (m :: * -> *) a.
    Monad m =>
    UnresolvedName (m a) -> m (UnresolvedName a))
-> Traversable UnresolvedName
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
UnresolvedName (m a) -> m (UnresolvedName a)
forall (f :: * -> *) a.
Applicative f =>
UnresolvedName (f a) -> f (UnresolvedName a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnresolvedName a -> m (UnresolvedName b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnresolvedName a -> f (UnresolvedName b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnresolvedName a -> f (UnresolvedName b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> UnresolvedName a -> f (UnresolvedName b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnresolvedName (f a) -> f (UnresolvedName a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
UnresolvedName (f a) -> f (UnresolvedName a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnresolvedName a -> m (UnresolvedName b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> UnresolvedName a -> m (UnresolvedName b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
UnresolvedName (m a) -> m (UnresolvedName a)
sequence :: forall (m :: * -> *) a.
Monad m =>
UnresolvedName (m a) -> m (UnresolvedName a)
Traversable)

-- | The identifiers a raw term mentions that a set of names cannot resolve, in
-- the order they occur.
--
-- This is 'unsafeConvertToAST' with the conversion left out, so it descends
-- under binders in the same way and accounts for what they bind.
--
-- @since 0.4.0
unresolvedNames
  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.
     (Foil.Distinct n, Bifoldable 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.
  -> [UnresolvedName rawIdent]
unresolvedNames :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) rawIdent
       rawTerm rawPattern rawScopedTerm (n :: S).
(Distinct n, Bifoldable 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
-> [UnresolvedName rawIdent]
unresolvedNames 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
-> Map rawIdent (Name n) -> rawTerm -> [UnresolvedName rawIdent]
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x) -> rawTerm -> [UnresolvedName rawIdent]
go
  where
    go :: forall x. Foil.Distinct x
       => Foil.Scope x -> Map rawIdent (Foil.Name x) -> rawTerm -> [UnresolvedName rawIdent]
    go :: forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x) -> rawTerm -> [UnresolvedName rawIdent]
go Scope x
scope Map rawIdent (Name x)
names rawTerm
t = case rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawTerm
t of
      Left rawIdent
x
        | rawIdent -> Map rawIdent (Name x) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member rawIdent
x Map rawIdent (Name x)
names -> []
        | Bool
otherwise          -> [rawIdent -> [rawIdent] -> UnresolvedName rawIdent
forall rawIdent. rawIdent -> [rawIdent] -> UnresolvedName rawIdent
UnresolvedName rawIdent
x (Map rawIdent (Name x) -> [rawIdent]
forall k a. Map k a -> [k]
Map.keys Map rawIdent (Name x)
names)]
      Right sig (rawPattern, rawScopedTerm) rawTerm
node -> ((rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent])
-> (rawTerm -> [UnresolvedName rawIdent])
-> sig (rawPattern, rawScopedTerm) rawTerm
-> [UnresolvedName rawIdent]
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 (Scope x
-> Map rawIdent (Name x)
-> (rawPattern, rawScopedTerm)
-> [UnresolvedName rawIdent]
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> (rawPattern, rawScopedTerm)
-> [UnresolvedName rawIdent]
goScoped Scope x
scope Map rawIdent (Name x)
names) (Scope x
-> Map rawIdent (Name x) -> rawTerm -> [UnresolvedName rawIdent]
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x) -> rawTerm -> [UnresolvedName rawIdent]
go Scope x
scope Map rawIdent (Name x)
names) sig (rawPattern, rawScopedTerm) rawTerm
node

    goScoped :: forall x. Foil.Distinct x
             => Foil.Scope x -> Map rawIdent (Foil.Name x)
             -> (rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent]
    goScoped :: forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> (rawPattern, rawScopedTerm)
-> [UnresolvedName rawIdent]
goScoped Scope x
scope Map rawIdent (Name x)
names (rawPattern
pat, rawScopedTerm
scopedTerm) =
      Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> [UnresolvedName rawIdent])
-> [UnresolvedName rawIdent]
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 x
scope Map rawIdent (Name x)
names rawPattern
pat ((forall (y :: S).
  DExt x y =>
  binder x y -> Map rawIdent (Name y) -> [UnresolvedName rawIdent])
 -> [UnresolvedName rawIdent])
-> (forall (y :: S).
    DExt x y =>
    binder x y -> Map rawIdent (Name y) -> [UnresolvedName rawIdent])
-> [UnresolvedName rawIdent]
forall a b. (a -> b) -> a -> b
$ \binder x y
binder' Map rawIdent (Name y)
names' ->
        Scope y
-> Map rawIdent (Name y) -> rawTerm -> [UnresolvedName rawIdent]
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x) -> rawTerm -> [UnresolvedName rawIdent]
go (binder x y -> Scope x -> Scope y
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder x y
binder' Scope x
scope) Map rawIdent (Name y)
names' (rawScopedTerm -> rawTerm
getScopedTerm rawScopedTerm
scopedTerm)

-- | Convert a raw term into a scope-safe term, reporting the first identifier
-- that does not resolve.
--
-- One pass, short-circuiting at the first failure, so a term that resolves
-- costs no more than 'unsafeConvertToAST' does. The report is complete for
-- that one identifier, since 'unresolvedInScope' is built where the conversion
-- fails and is never computed on the way through.
--
-- A caller wanting /every/ unresolved identifier rather than the first pays a
-- second pass for it, with 'unresolvedNames'. The successful path stays fast
-- that way, and a failure can afford to be walked again for a better message.
--
-- @since 0.4.0
tryConvertToAST
  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.
     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,
      Foil.CoSinkable binder, Foil.SinkableK 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.
  -> Either (UnresolvedName rawIdent) (AST binder sig n)
tryConvertToAST :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) rawIdent
       rawTerm rawPattern rawScopedTerm (n :: S).
(Distinct n, Bitraversable sig, Ord rawIdent, CoSinkable binder,
 SinkableK 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
-> Either (UnresolvedName rawIdent) (AST binder sig n)
tryConvertToAST 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
 -> 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)
-> Map rawIdent (AST binder sig n)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig n)
forall (sig :: * -> * -> *) (binder :: S -> S -> *) rawIdent
       rawTerm rawPattern rawScopedTerm (n :: S).
(Distinct n, Bitraversable sig, Ord rawIdent, CoSinkable binder,
 SinkableK 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)
-> Map rawIdent (AST binder sig n)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig n)
tryConvertToASTWith 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 Map rawIdent (AST binder sig n)
forall k a. Map k a
Map.empty

-- | Convert a raw term into a scope-safe term, resolving some identifiers to
-- whole terms rather than to variables.
--
-- The extra table is what a language with /constants/ needs: an identifier that
-- denotes a top-level declaration, a primitive, or an abbreviation stands for
-- something that is not a variable, and resolving it during conversion is the
-- only place where the binders are known. Doing it in a pass of one's own means
-- writing a binder-aware traversal of the raw syntax by hand.
--
-- Variables win: the table of names is consulted first, so a binder shadows an
-- entry here, and an entry here shadows nothing. The table is sunk when going
-- under a binder, exactly as the names are, so its entries may mention anything
-- in scope where conversion started and need not be closed.
--
-- @since 0.4.0
tryConvertToASTWith
  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.
     (Foil.Distinct n, Bitraversable sig, Ord rawIdent,
      Foil.CoSinkable binder, Foil.SinkableK 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@.
  -> Map rawIdent (AST binder sig n)
  -- ^ Identifiers that denote a term rather than a variable.
  -> rawTerm
  -- ^ Raw term.
  -> Either (UnresolvedName rawIdent) (AST binder sig n)
tryConvertToASTWith :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) rawIdent
       rawTerm rawPattern rawScopedTerm (n :: S).
(Distinct n, Bitraversable sig, Ord rawIdent, CoSinkable binder,
 SinkableK 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)
-> Map rawIdent (AST binder sig n)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig n)
tryConvertToASTWith 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
-> Map rawIdent (Name n)
-> Map rawIdent (AST binder sig n)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig n)
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig x)
go
  where
    go :: forall x. Foil.Distinct x
       => Foil.Scope x -> Map rawIdent (Foil.Name x)
       -> Map rawIdent (AST binder sig x) -> rawTerm
       -> Either (UnresolvedName rawIdent) (AST binder sig x)
    go :: forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig x)
go Scope x
scope Map rawIdent (Name x)
names Map rawIdent (AST binder sig x)
terms rawTerm
t = case rawTerm
-> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)
toSig rawTerm
t of
      Left rawIdent
x -> case rawIdent -> Map rawIdent (Name x) -> Maybe (Name x)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup rawIdent
x Map rawIdent (Name x)
names of
        Just Name x
name -> AST binder sig x
-> Either (UnresolvedName rawIdent) (AST binder sig x)
forall a b. b -> Either a b
Right (Name x -> AST binder sig x
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name x
name)
        Maybe (Name x)
Nothing   -> case rawIdent
-> Map rawIdent (AST binder sig x) -> Maybe (AST binder sig x)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup rawIdent
x Map rawIdent (AST binder sig x)
terms of
          Just AST binder sig x
term -> AST binder sig x
-> Either (UnresolvedName rawIdent) (AST binder sig x)
forall a b. b -> Either a b
Right AST binder sig x
term
          Maybe (AST binder sig x)
Nothing   -> UnresolvedName rawIdent
-> Either (UnresolvedName rawIdent) (AST binder sig x)
forall a b. a -> Either a b
Left (rawIdent -> [rawIdent] -> UnresolvedName rawIdent
forall rawIdent. rawIdent -> [rawIdent] -> UnresolvedName rawIdent
UnresolvedName rawIdent
x (Map rawIdent (Name x) -> [rawIdent]
forall k a. Map k a -> [k]
Map.keys Map rawIdent (Name x)
names [rawIdent] -> [rawIdent] -> [rawIdent]
forall a. Semigroup a => a -> a -> a
<> Map rawIdent (AST binder sig x) -> [rawIdent]
forall k a. Map k a -> [k]
Map.keys Map rawIdent (AST binder sig x)
terms))
      Right sig (rawPattern, rawScopedTerm) rawTerm
node ->
        sig (ScopedAST binder sig x) (AST binder sig x) -> AST binder sig x
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 x) (AST binder sig x)
 -> AST binder sig x)
-> Either
     (UnresolvedName rawIdent)
     (sig (ScopedAST binder sig x) (AST binder sig x))
-> Either (UnresolvedName rawIdent) (AST binder sig x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((rawPattern, rawScopedTerm)
 -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x))
-> (rawTerm -> Either (UnresolvedName rawIdent) (AST binder sig x))
-> sig (rawPattern, rawScopedTerm) rawTerm
-> Either
     (UnresolvedName rawIdent)
     (sig (ScopedAST binder sig x) (AST binder sig x))
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c) -> (b -> f d) -> sig a b -> f (sig c d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> (rawPattern, rawScopedTerm)
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> (rawPattern, rawScopedTerm)
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
goScoped Scope x
scope Map rawIdent (Name x)
names Map rawIdent (AST binder sig x)
terms) (Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig x)
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig x)
go Scope x
scope Map rawIdent (Name x)
names Map rawIdent (AST binder sig x)
terms) sig (rawPattern, rawScopedTerm) rawTerm
node

    goScoped :: forall x. Foil.Distinct x
             => Foil.Scope x -> Map rawIdent (Foil.Name x)
             -> Map rawIdent (AST binder sig x)
             -> (rawPattern, rawScopedTerm)
             -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
    goScoped :: forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> (rawPattern, rawScopedTerm)
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
goScoped Scope x
scope Map rawIdent (Name x)
names Map rawIdent (AST binder sig x)
terms (rawPattern
pat, rawScopedTerm
scopedTerm) =
      Scope x
-> Map rawIdent (Name x)
-> rawPattern
-> (forall (y :: S).
    DExt x y =>
    binder x y
    -> Map rawIdent (Name y)
    -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x))
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
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 x
scope Map rawIdent (Name x)
names rawPattern
pat ((forall (y :: S).
  DExt x y =>
  binder x y
  -> Map rawIdent (Name y)
  -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x))
 -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x))
-> (forall (y :: S).
    DExt x y =>
    binder x y
    -> Map rawIdent (Name y)
    -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x))
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
forall a b. (a -> b) -> a -> b
$ \binder x y
binder' Map rawIdent (Name y)
names' ->
        binder x y -> AST binder sig y -> ScopedAST binder sig x
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST binder x y
binder'
          (AST binder sig y -> ScopedAST binder sig x)
-> Either (UnresolvedName rawIdent) (AST binder sig y)
-> Either (UnresolvedName rawIdent) (ScopedAST binder sig x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope y
-> Map rawIdent (Name y)
-> Map rawIdent (AST binder sig y)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig y)
forall (x :: S).
Distinct x =>
Scope x
-> Map rawIdent (Name x)
-> Map rawIdent (AST binder sig x)
-> rawTerm
-> Either (UnresolvedName rawIdent) (AST binder sig x)
go (binder x y -> Scope x -> Scope y
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
Foil.extendScopePattern binder x y
binder' Scope x
scope) Map rawIdent (Name y)
names'
                 (Map rawIdent (AST binder sig x) -> Map rawIdent (AST binder sig y)
forall (f :: * -> *) (e :: S -> *) (n :: S) (l :: S).
(Functor f, Sinkable e, DExt n l) =>
f (e n) -> f (e l)
Foil.sink1 Map rawIdent (AST binder sig x)
terms) (rawScopedTerm -> rawTerm
getScopedTerm rawScopedTerm
scopedTerm)

-- | Convert a raw term into a scope-safe term, calling 'error' on an
-- identifier that does not resolve.
--
-- Prefer 'tryConvertToAST', which reports such identifiers. This is for callers
-- that have already established that every name resolves.
--
-- @since 0.4.0
unsafeConvertToAST
  :: (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
unsafeConvertToAST :: 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
unsafeConvertToAST 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   -> String -> AST binder sig n
forall a. HasCallStack => String -> a
error String
"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
unsafeConvertToScopedAST 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
unsafeConvertToAST 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 'unsafeConvertToAST' but for scoped terms.
--
-- @since 0.4.0
unsafeConvertToScopedAST
  :: (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
unsafeConvertToScopedAST :: 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
unsafeConvertToScopedAST 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
unsafeConvertToAST 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 a raw term into a scope-safe term.
--
-- @since 0.0.3
convertToAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -> (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)
  -> (rawScopedTerm -> rawTerm)
  -> Foil.Scope n
  -> Map rawIdent (Foil.Name n)
  -> rawTerm
  -> 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))
-> (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
unsafeConvertToAST
{-# DEPRECATED convertToAST "Renamed to unsafeConvertToAST, since it calls error on an unresolved identifier. Use tryConvertToAST to report them instead." #-}

-- | Same as 'convertToAST' but for scoped terms.
--
-- @since 0.0.3
convertToScopedAST
  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
  -> (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)
  -> (rawScopedTerm -> rawTerm)
  -> Foil.Scope n
  -> Map rawIdent (Foil.Name n)
  -> (rawPattern, rawScopedTerm)
  -> 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))
-> (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
unsafeConvertToScopedAST
{-# DEPRECATED convertToScopedAST "Renamed to unsafeConvertToScopedAST, since it calls error on an unresolved identifier." #-}

-- ** Convert from free foil

-- | Convert a scope-safe term back into a raw term.
--
-- @since 0.0.3
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)
-> (Id -> 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 Id -> rawIdent
f = \case
  Var Name n
x -> rawIdent -> rawTerm
fromVar (Id -> rawIdent
f (Name n -> Id
forall (l :: S). Name l -> Id
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)
-> (Id -> 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)
-> (Id -> 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 Id -> rawIdent
f)
      ((sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Id -> 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)
-> (Id -> 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 Id -> rawIdent
f)
      sig (ScopedAST binder sig n) (AST binder sig n)
node

-- | Same as 'convertFromAST' but for scoped terms.
--
-- @since 0.0.3
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)
-> (Id -> 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 Id -> 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)
-> (Id -> 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)
-> (Id -> 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 Id -> rawIdent
f AST binder sig l
body))

-- | Convert a scope-safe term back into a raw term, naming the variables that
-- occur /free in the whole term/ separately from the bound ones.
--
-- 'convertFromAST' applies one naming function to every variable it meets,
-- bound or free, and gives it only a raw name. That is often not enough, since
-- raw names are not unique across scope indices: a binder inside a term may
-- share one with a name of the ambient scope, so naming by raw name alone can
-- print a bound variable as whatever the ambient scope calls that name.
--
-- Keeping the typed name is what distinguishes them, and 'Foil.unsinkNamePattern'
-- is the operation for it: composing one per binder on the way down builds a
-- @'Foil.Name' x -> 'Maybe' ('Foil.Name' n)@ that answers exactly the question.
--
-- @since 0.4.0
convertFromASTWith
  :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n.
     (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)
  => (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.
  -> (Foil.Name n -> rawIdent)
  -- ^ Name a variable that is free in the whole term.
  -> (Int -> rawIdent)
  -- ^ Name a bound variable, from its underlying integer identifier.
  -> AST binder sig n
  -- ^ Scope-safe term.
  -> rawTerm
convertFromASTWith :: forall (sig :: * -> * -> *) (binder :: S -> S -> *) rawIdent
       rawTerm rawPattern rawScopedTerm (n :: S).
(Bifunctor sig, Distinct n, CoSinkable binder) =>
(sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)
-> (rawIdent -> rawTerm)
-> (forall (x :: S) (y :: S). binder x y -> rawPattern)
-> (rawTerm -> rawScopedTerm)
-> (Name n -> rawIdent)
-> (Id -> rawIdent)
-> AST binder sig n
-> rawTerm
convertFromASTWith sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig rawIdent -> rawTerm
fromVar forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern rawTerm -> rawScopedTerm
makeScoped Name n -> rawIdent
freeName Id -> rawIdent
boundName =
    (Name n -> Maybe (Name n)) -> AST binder sig n -> rawTerm
forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n)) -> AST binder sig x -> rawTerm
go Name n -> Maybe (Name n)
forall a. a -> Maybe a
Just
  where
    go :: forall x. Foil.Distinct x
       => (Foil.Name x -> Maybe (Foil.Name n)) -> AST binder sig x -> rawTerm
    go :: forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n)) -> AST binder sig x -> rawTerm
go Name x -> Maybe (Name n)
unsink = \case
      Var Name x
x -> rawIdent -> rawTerm
fromVar (rawIdent -> rawTerm) -> rawIdent -> rawTerm
forall a b. (a -> b) -> a -> b
$ case Name x -> Maybe (Name n)
unsink Name x
x of
        Just Name n
name -> Name n -> rawIdent
freeName Name n
name
        Maybe (Name n)
Nothing   -> Id -> rawIdent
boundName (Name x -> Id
forall (l :: S). Name l -> Id
Foil.nameId Name x
x)
      Node sig (ScopedAST binder sig x) (AST binder sig x)
node -> sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm
fromSig ((ScopedAST binder sig x -> (rawPattern, rawScopedTerm))
-> (AST binder sig x -> rawTerm)
-> sig (ScopedAST binder sig x) (AST binder sig x)
-> 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 ((Name x -> Maybe (Name n))
-> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)
forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n))
-> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)
goScoped Name x -> Maybe (Name n)
unsink) ((Name x -> Maybe (Name n)) -> AST binder sig x -> rawTerm
forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n)) -> AST binder sig x -> rawTerm
go Name x -> Maybe (Name n)
unsink) sig (ScopedAST binder sig x) (AST binder sig x)
node)

    goScoped :: forall x. Foil.Distinct x
             => (Foil.Name x -> Maybe (Foil.Name n))
             -> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)
    goScoped :: forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n))
-> ScopedAST binder sig x -> (rawPattern, rawScopedTerm)
goScoped Name x -> Maybe (Name n)
unsink (ScopedAST binder x l
binder AST binder sig l
body) =
      case binder x l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
Foil.assertDistinct binder x l
binder of
        DistinctEvidence l
Foil.Distinct ->
          ( binder x l -> rawPattern
forall (x :: S) (y :: S). binder x y -> rawPattern
makePattern binder x l
binder
          , rawTerm -> rawScopedTerm
makeScoped
              ((Name l -> Maybe (Name n)) -> AST binder sig l -> rawTerm
forall (x :: S).
Distinct x =>
(Name x -> Maybe (Name n)) -> AST binder sig x -> rawTerm
go (\Name l
name -> binder x l -> Name l -> Maybe (Name x)
forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Name l -> Maybe (Name n)
Foil.unsinkNamePattern binder x l
binder Name l
name Maybe (Name x) -> (Name x -> Maybe (Name n)) -> Maybe (Name n)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name x -> Maybe (Name n)
unsink) AST binder sig l
body) )

-- ** Unsinking AST

-- | The support of a term: exactly the names that occur free in it.
--
-- This is the annotation that co-de-Bruijn syntax carries intrinsically and
-- that the foil, having global names and therefore free weakening, does not.
-- Computing it is \(O(size)\); a client that restricts often should cache it.
--
-- @since 0.4.0
supportOf
  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)
  => AST binder sig n -> Foil.NameSet n
supportOf :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf = \case
  Var Name n
name  -> Name n -> NameSet n
forall (n :: S). Name n -> NameSet n
Foil.nameSetSingleton Name n
name
  Node sig (ScopedAST binder sig n) (AST binder sig n)
node -> (ScopedAST binder sig n -> NameSet n)
-> (AST binder sig n -> NameSet n)
-> sig (ScopedAST binder sig n) (AST binder sig n)
-> NameSet 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 -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
ScopedAST binder sig n -> NameSet n
supportOfScopedAST AST binder sig n -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf sig (ScopedAST binder sig n) (AST binder sig n)
node

-- | The support of a scoped term, in the scope /outside/ its binder.
--
-- @since 0.4.0
supportOfScopedAST
  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)
  => ScopedAST binder sig n -> Foil.NameSet n
supportOfScopedAST :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
ScopedAST binder sig n -> NameSet n
supportOfScopedAST (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 -> binder n l -> NameSet l -> NameSet n
forall (binder :: S -> S -> *) (n :: S) (l :: S).
CoSinkable binder =>
binder n l -> NameSet l -> NameSet n
Foil.unsinkNameSet binder n l
binder (AST binder sig l -> NameSet l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf AST binder sig l
body)

-- | Cut a term down to the scope of exactly the names it uses.
--
-- This is the a-priori form of restriction, and the cheap one: the term
-- inhabits the smaller scope /by construction/, so nothing is tested and
-- nothing can fail. @'Foil.Ext' m n@ comes back with it, so the term can be
-- 'Foil.sink'ed to where it came from for free.
--
-- Verifying a declared dependency, such as a @uses@ clause or a module's
-- parameters, is this plus a comparison: compute the scope a term really
-- inhabits, and check the declared one against it.
--
-- @since 0.4.0
withRelevantScope
  :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig)
  => AST binder sig n
  -> (forall m. (Foil.Ext m n, Foil.Distinct m)
      => Foil.Scope m -> AST binder sig m -> r)
  -> r
withRelevantScope :: forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *) r.
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n
-> (forall (m :: S).
    (Ext m n, Distinct m) =>
    Scope m -> AST binder sig m -> r)
-> r
withRelevantScope AST binder sig n
term forall (m :: S).
(Ext m n, Distinct m) =>
Scope m -> AST binder sig m -> r
cont =
  NameSet n
-> (forall (m :: S). (Ext m n, Distinct m) => Scope m -> r) -> r
forall (n :: S) r.
Distinct n =>
NameSet n
-> (forall (m :: S). (Ext m n, Distinct m) => Scope m -> r) -> r
Foil.withRestrictedScope (AST binder sig n -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf AST binder sig n
term) ((forall (m :: S). (Ext m n, Distinct m) => Scope m -> r) -> r)
-> (forall (m :: S). (Ext m n, Distinct m) => Scope m -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Scope m
scope ->
    Scope m -> AST binder sig m -> r
forall (m :: S).
(Ext m n, Distinct m) =>
Scope m -> AST binder sig m -> r
cont Scope m
scope (AST binder sig n -> AST binder sig m
forall a b. a -> b
unsafeCoerce AST binder sig n
term)

-- | Unsink an AST from a larger scope to a smaller scope.
--
-- This is the a-posteriori form, and the one that has to be paid for: the
-- term's support is computed and compared against the scope. When it succeeds
-- the term itself is untouched, since restriction of a term that does inhabit
-- the smaller scope is a coercion.
--
-- @since 0.3.0
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
  | NameSet l -> Scope n -> Bool
forall (l :: S) (n :: S). NameSet l -> Scope n -> Bool
Foil.nameSetSubsetOfScope (AST binder sig l -> NameSet l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf AST binder sig l
term) Scope n
scope = 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.
--
-- These come from 'supportOf', so they are distinct and in ascending order of
-- their identifiers.
--
-- @since 0.3.0
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 = NameSet n -> [Name n]
forall (n :: S). NameSet n -> [Name n]
Foil.nameSetToList (NameSet n -> [Name n])
-> (AST binder sig n -> NameSet n) -> AST binder sig n -> [Name n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AST binder sig n -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
AST binder sig n -> NameSet n
supportOf

-- | Get the free variables of a scoped AST, in the scope outside its binder.
--
-- @since 0.3.0
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 = NameSet n -> [Name n]
forall (n :: S). NameSet n -> [Name n]
Foil.nameSetToList (NameSet n -> [Name n])
-> (ScopedAST binder sig n -> NameSet n)
-> ScopedAST binder sig n
-> [Name n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopedAST binder sig n -> NameSet n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
(Distinct n, CoSinkable binder, Bifoldable sig) =>
ScopedAST binder sig n -> NameSet n
supportOfScopedAST