{-# 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           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 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