{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | The free-foil core back to surface syntax.
--
-- A transcription of @fromTermWith'@ from "Language.Rzk.Foil.Names". The
-- structure is the same, and so are the display rules:
--
--   * a binder's user-written name is kept, refreshed only against names already
--     in use; an anonymous binder draws from 'defaultVarIdents';
--   * a pattern binder is shown as the pattern, and projections of the variable
--     it binds are folded back to the component names, so a goal reads
--     @\\ (t , s) -> …@ and not @\\ x -> … π₁ x …@;
--   * an anonymous binder the codomain does not use is not shown at all, so
--     @(x₁ : A) → B@ prints as @A → B@.
--
-- What changes is the bookkeeping: a variable is a 'Foil.Name', so the display
-- names live in a 'Foil.NameMap' keyed by name, rather than being threaded
-- through de Bruijn shifts.
module Language.Rzk.Foil.Print where

import           Control.Monad.Foil       (NameMap)
import qualified Control.Monad.Foil       as Foil
import           Control.Monad.Free.Foil  (AST (..), ScopedAST (..))
import           Data.Bifoldable          (bifoldMap)

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (Binder (..), Display, Proj (..),
                                           TModality (..),
                                           VarIdent, binderIsCompound,
                                           binderLeaves, binderPaths,
                                           binderToPattern, defaultVarIdents,
                                           fromTModalityToModalColon,
                                           fromVarIdent, fromMod, holeIdentToken,
                                           patternToTerm,
                                           refreshVar)
import qualified Language.Rzk.Syntax      as Rzk

-- | Print a closed term.
fromTermClosed :: Term Foil.VoidS -> Rzk.Term
fromTermClosed :: Term 'VoidS -> Term
fromTermClosed = [VarIdent]
-> [VarIdent] -> NameMap 'VoidS Display -> Term 'VoidS -> Term
forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [] [VarIdent]
defaultVarIdents NameMap 'VoidS Display
forall a. NameMap 'VoidS a
Foil.emptyNameMap

fromTerm :: forall n. [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Rzk.Term
fromTerm :: forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [VarIdent]
used [VarIdent]
supply NameMap n Display
names = Term n -> Term
go
  where
    loc :: Maybe a
loc = Maybe a
forall a. Maybe a
Nothing

    goMod :: TModality -> Rzk.Modality
    goMod :: TModality -> Modality
goMod = TModality -> Modality
fromMod

    -- Enter a binder and print the scopes it binds over.
    --
    -- A Pi-type and a lambda each bind /two/ scopes under one binder (the shape
    -- tope and the body). In the old representation both were indexed by the
    -- same de Bruijn Z; here each 'ScopedAST' carries its own 'NameBinder'. That
    -- is operationally the same (the checker instantiates both with the same
    -- argument), but they must be /shown/ under one name, so each scope's binder
    -- is mapped to the same display name.
    withBinder1 :: Binder -> ScopedTerm n -> ((Binder, Rzk.Term) -> r) -> r
    withBinder1 :: forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
s (Binder, Term) -> r
k = Binder -> (Binder -> (ScopedTerm n -> Term) -> r) -> r
forall r. Binder -> (Binder -> (ScopedTerm n -> Term) -> r) -> r
withBinder Binder
z ((Binder -> (ScopedTerm n -> Term) -> r) -> r)
-> (Binder -> (ScopedTerm n -> Term) -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Binder
z' ScopedTerm n -> Term
printScope -> (Binder, Term) -> r
k (Binder
z', ScopedTerm n -> Term
printScope ScopedTerm n
s)

    withBinder2 :: Binder -> ScopedTerm n -> ScopedTerm n -> ((Binder, Rzk.Term, Rzk.Term) -> r) -> r
    withBinder2 :: forall r.
Binder
-> ScopedTerm n -> ScopedTerm n -> ((Binder, Term, Term) -> r) -> r
withBinder2 Binder
z ScopedTerm n
s1 ScopedTerm n
s2 (Binder, Term, Term) -> r
k =
      Binder -> (Binder -> (ScopedTerm n -> Term) -> r) -> r
forall r. Binder -> (Binder -> (ScopedTerm n -> Term) -> r) -> r
withBinder Binder
z ((Binder -> (ScopedTerm n -> Term) -> r) -> r)
-> (Binder -> (ScopedTerm n -> Term) -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Binder
z' ScopedTerm n -> Term
printScope -> (Binder, Term, Term) -> r
k (Binder
z', ScopedTerm n -> Term
printScope ScopedTerm n
s1, ScopedTerm n -> Term
printScope ScopedTerm n
s2)

    withBinder
      :: Binder
      -> (Binder -> (ScopedTerm n -> Rzk.Term) -> r)
      -> r
    withBinder :: forall r. Binder -> (Binder -> (ScopedTerm n -> Term) -> r) -> r
withBinder Binder
z Binder -> (ScopedTerm n -> Term) -> r
k = Binder -> (ScopedTerm n -> Term) -> r
k Binder
z' ScopedTerm n -> Term
printScope
      where
        (Binder
z', [VarIdent]
supply') = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
used [VarIdent]
supply Binder
z
        x :: VarIdent
x = Binder -> [VarIdent] -> VarIdent
displayNameOf Binder
z' [VarIdent]
supply'
        supply'' :: [VarIdent]
supply'' = case Binder
z' of
          BinderVar (Just VarIdent
_) -> [VarIdent]
supply'
          Binder
_                  -> Int -> [VarIdent] -> [VarIdent]
forall a. Int -> [a] -> [a]
drop Int
1 [VarIdent]
supply'
        used' :: [VarIdent]
used' = VarIdent
x VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
used [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
<> Binder -> [VarIdent]
binderLeaves Binder
z'
        printScope :: ScopedTerm n -> Term
printScope (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig SrcPos TermSig) l
body) =
          [VarIdent]
-> [VarIdent]
-> NameMap l Display
-> AST NameBinder (AnnSig SrcPos TermSig) l
-> Term
forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [VarIdent]
used' [VarIdent]
supply'' (NameBinder n l -> Display -> NameMap n Display -> NameMap l Display
forall (n :: S) (l :: S) a.
NameBinder n l -> a -> NameMap n a -> NameMap l a
Foil.addNameBinder NameBinder n l
binder (VarIdent
x, Binder
z') NameMap n Display
names) AST NameBinder (AnnSig SrcPos TermSig) l
body

    -- A projection chain over a pattern binder's variable is shown as the
    -- component's name: @π₁ x@ is @t@.
    projChain :: Term n -> Maybe ([Proj], Foil.Name n)
    projChain :: Term n -> Maybe ([Proj], Name n)
projChain (First Term n
t)  = (([Proj], Name n) -> ([Proj], Name n))
-> Maybe ([Proj], Name n) -> Maybe ([Proj], Name n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Proj]
ps, Name n
x) -> (Proj
PFst Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
ps, Name n
x)) (Term n -> Maybe ([Proj], Name n)
projChain Term n
t)
    projChain (Second Term n
t) = (([Proj], Name n) -> ([Proj], Name n))
-> Maybe ([Proj], Name n) -> Maybe ([Proj], Name n)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([Proj]
ps, Name n
x) -> (Proj
PSnd Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
ps, Name n
x)) (Term n -> Maybe ([Proj], Name n)
projChain Term n
t)
    projChain (Var Name n
x)    = ([Proj], Name n) -> Maybe ([Proj], Name n)
forall a. a -> Maybe a
Just ([], Name n
x)
    projChain Term n
_          = Maybe ([Proj], Name n)
forall a. Maybe a
Nothing

    foldedProjection :: Term n -> Maybe Rzk.Term
    foldedProjection :: Term n -> Maybe Term
foldedProjection Term n
t = do
      (ps, x) <- Term n -> Maybe ([Proj], Name n)
projChain Term n
t
      case ps of
        [] -> Maybe Term
forall a. Maybe a
Nothing
        [Proj]
_  -> do
          let (VarIdent
_, Binder
binder) = Name n -> NameMap n Display -> Display
forall (n :: S) a. Name n -> NameMap n a -> a
Foil.lookupName Name n
x NameMap n Display
names
          leaf <- [Proj] -> [([Proj], VarIdent)] -> Maybe VarIdent
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ([Proj] -> [Proj]
forall a. [a] -> [a]
reverse [Proj]
ps) (Binder -> [([Proj], VarIdent)]
binderPaths Binder
binder)
          pure (Rzk.Var loc (fromVarIdent leaf))

    go :: Term n -> Rzk.Term
    go :: Term n -> Term
go Term n
t | Just Term
t' <- Term n -> Maybe Term
foldedProjection Term n
t = Term
t'
    go (Var Name n
x) =
      case Name n -> NameMap n Display -> Display
forall (n :: S) a. Name n -> NameMap n a -> a
Foil.lookupName Name n
x NameMap n Display
names of
        -- A bare use of a pattern binder's variable (the point itself) reads as
        -- the pattern, not as the placeholder.
        (VarIdent
_, Binder
binder) | Binder -> Bool
binderIsCompound Binder
binder -> Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
binder)
        (VarIdent
name, Binder
_)                             -> BNFC'Position -> VarIdent' BNFC'Position -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
forall a. Maybe a
loc (VarIdent -> VarIdent' BNFC'Position
fromVarIdent VarIdent
name)

    go Term n
Universe = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Universe BNFC'Position
forall a. Maybe a
loc
    go Term n
UniverseCube = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.UniverseCube BNFC'Position
forall a. Maybe a
loc
    go Term n
UniverseTope = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.UniverseTope BNFC'Position
forall a. Maybe a
loc
    go Term n
CubeUnit = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnit BNFC'Position
forall a. Maybe a
loc
    go Term n
CubeUnitStar = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnitStar BNFC'Position
forall a. Maybe a
loc
    go Term n
Cube2 = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2 BNFC'Position
forall a. Maybe a
loc
    go Term n
Cube2_0 = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_0 BNFC'Position
forall a. Maybe a
loc
    go Term n
Cube2_1 = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_1 BNFC'Position
forall a. Maybe a
loc
    go Term n
CubeI = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI BNFC'Position
forall a. Maybe a
loc
    go Term n
CubeI_0 = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_0 BNFC'Position
forall a. Maybe a
loc
    go Term n
CubeI_1 = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_1 BNFC'Position
forall a. Maybe a
loc
    go (CubeProduct Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.CubeProduct BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (CubeSup Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.CubeSup BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (CubeInf Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.CubeInf BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (CubeFlip Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.CubeFlip BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go (CubeUnflip Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.CubeUnflip BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go Term n
TopeTop = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeTop BNFC'Position
forall a. Maybe a
loc
    go Term n
TopeBottom = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeBottom BNFC'Position
forall a. Maybe a
loc
    go (TopeEQ Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeEQ BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (TopeLEQ Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeLEQ BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (TopeAnd Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeAnd BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (TopeOr Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeOr BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (TopeInv Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.TopeInv BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go (TopeUninv Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.TopeUninv BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go Term n
RecBottom = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.RecBottom BNFC'Position
forall a. Maybe a
loc
    go (RecOr [(Term n, Term n)]
rs) = BNFC'Position -> [Restriction' BNFC'Position] -> Term
forall a. a -> [Restriction' a] -> Term' a
Rzk.RecOr BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
tope) (Term n -> Term
go Term n
term) | (Term n
tope, Term n
term) <- [(Term n, Term n)]
rs]
    go (Hole Maybe VarIdent
mname) = BNFC'Position -> HoleIdent' BNFC'Position -> Term
forall a. a -> HoleIdent' a -> Term' a
Rzk.Hole BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> HoleIdentToken -> HoleIdent' BNFC'Position
forall a. a -> HoleIdentToken -> HoleIdent' a
Rzk.HoleIdent BNFC'Position
forall a. Maybe a
loc (Text -> HoleIdentToken
Rzk.HoleIdentToken (Maybe VarIdent -> Text
holeIdentToken Maybe VarIdent
mname)))

    -- An anonymous binder the codomain does not use is not shown: @(x₁ : A) → B@
    -- reads better as @A → B@. A user-written name is kept even when unused.
    go (TypeFun z :: Binder
z@(BinderVar Maybe VarIdent
Nothing) TModality
Id Term n
arg Maybe (ScopedTerm n)
Nothing ScopedTerm n
ret)
      | Bool -> Bool
not (ScopedTerm n -> Bool
forall (n :: S). ScopedTerm n -> Bool
scopeUsesItsBinder ScopedTerm n
ret) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
ret (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
_z', Term
ret') ->
          BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> ParamDecl' a
Rzk.ParamType BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
arg)) Term
ret'
    go (TypeFun Binder
z TModality
md Term n
arg Maybe (ScopedTerm n)
Nothing ScopedTerm n
ret) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
ret (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
ret') ->
      let pat :: Term
pat = Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')
       in case TModality
md of
            TModality
Id -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
forall a. Maybe a
loc Term
pat (Term n -> Term
go Term n
arg)) Term
ret'
            TModality
_  -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position
-> Term
-> ModalColon' BNFC'Position
-> Term
-> ParamDecl' BNFC'Position
forall a. a -> Term' a -> ModalColon' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalType BNFC'Position
forall a. Maybe a
loc Term
pat (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term n -> Term
go Term n
arg)) Term
ret'
    go (TypeFun Binder
z TModality
md Term n
arg (Just ScopedTerm n
tope) ScopedTerm n
ret) = Binder
-> ScopedTerm n
-> ScopedTerm n
-> ((Binder, Term, Term) -> Term)
-> Term
forall r.
Binder
-> ScopedTerm n -> ScopedTerm n -> ((Binder, Term, Term) -> r) -> r
withBinder2 Binder
z ScopedTerm n
tope ScopedTerm n
ret (((Binder, Term, Term) -> Term) -> Term)
-> ((Binder, Term, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
tope', Term
ret') ->
      let pat :: Term
pat = Pattern -> Term
patternToTerm (Binder -> Pattern
binderToPattern Binder
z')
       in case TModality
md of
            TModality
Id -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Term -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermShape BNFC'Position
forall a. Maybe a
loc Term
pat (Term n -> Term
go Term n
arg) Term
tope') Term
ret'
            TModality
_  -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
forall a. Maybe a
loc (BNFC'Position
-> Term
-> ModalColon' BNFC'Position
-> Term
-> Term
-> ParamDecl' BNFC'Position
forall a.
a -> Term' a -> ModalColon' a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermModalShape BNFC'Position
forall a. Maybe a
loc Term
pat (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term n -> Term
go Term n
arg) Term
tope') Term
ret'

    go (TypeSigma Binder
z TModality
md Term n
a ScopedTerm n
b) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
b (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
b') ->
      case TModality
md of
        TModality
Id -> BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (Term n -> Term
go Term n
a) Term
b'
        TModality
_  -> BNFC'Position
-> Pattern -> ModalColon' BNFC'Position -> Term -> Term -> Term
forall a.
a -> Pattern' a -> ModalColon' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigmaModal BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term n -> Term
go Term n
a) Term
b'

    go (TypeId Term n
l (Just Term n
tA) Term n
r) = BNFC'Position -> Term -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a -> Term' a
Rzk.TypeId BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
tA) (Term n -> Term
go Term n
r)
    go (TypeId Term n
l Maybe (Term n)
Nothing Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeIdSimple BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (App Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.App BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)

    go (Lambda Binder
z Maybe (LambdaParam (ScopedTerm n) (Term n))
Nothing ScopedTerm n
body) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
body (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
body') ->
      BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [BNFC'Position -> Pattern -> Param' BNFC'Position
forall a. a -> Pattern' a -> Param' a
Rzk.ParamPattern BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z')] Term
body'
    go (Lambda Binder
z (Just (LambdaParam TModality
md Term n
ty Maybe (ScopedTerm n)
Nothing)) ScopedTerm n
body) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
body (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
body') ->
      let pat :: Pattern
pat = Binder -> Pattern
binderToPattern Binder
z'
          param :: Param' BNFC'Position
param = case TModality
md of
            TModality
Id -> BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
forall a. Maybe a
loc [Pattern
pat] (Term n -> Term
go Term n
ty)
            TModality
_  -> BNFC'Position
-> [Pattern]
-> ModalColon' BNFC'Position
-> Term
-> Param' BNFC'Position
forall a. a -> [Pattern' a] -> ModalColon' a -> Term' a -> Param' a
Rzk.ParamPatternModalType BNFC'Position
forall a. Maybe a
loc [Pattern
pat] (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term n -> Term
go Term n
ty)
       in BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [Param' BNFC'Position
param] Term
body'
    go (Lambda Binder
z (Just (LambdaParam TModality
md Term n
cube (Just ScopedTerm n
tope))) ScopedTerm n
body) =
      Binder
-> ScopedTerm n
-> ScopedTerm n
-> ((Binder, Term, Term) -> Term)
-> Term
forall r.
Binder
-> ScopedTerm n -> ScopedTerm n -> ((Binder, Term, Term) -> r) -> r
withBinder2 Binder
z ScopedTerm n
tope ScopedTerm n
body (((Binder, Term, Term) -> Term) -> Term)
-> ((Binder, Term, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
tope', Term
body') ->
        let pat :: Pattern
pat = Binder -> Pattern
binderToPattern Binder
z'
            param :: Param' BNFC'Position
param = case TModality
md of
              TModality
Id -> BNFC'Position -> [Pattern] -> Term -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape BNFC'Position
forall a. Maybe a
loc [Pattern
pat] (Term n -> Term
go Term n
cube) Term
tope'
              TModality
_  -> BNFC'Position
-> [Pattern]
-> ModalColon' BNFC'Position
-> Term
-> Term
-> Param' BNFC'Position
forall a.
a
-> [Pattern' a] -> ModalColon' a -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternModalShape BNFC'Position
forall a. Maybe a
loc [Pattern
pat] (TModality -> ModalColon' BNFC'Position
fromTModalityToModalColon TModality
md) (Term n -> Term
go Term n
cube) Term
tope'
         in BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
forall a. Maybe a
loc [Param' BNFC'Position
param] Term
body'

    go (Let Binder
z Maybe (Term n)
mty Term n
val ScopedTerm n
body) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
body (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
body') ->
      let bind :: Bind' BNFC'Position
bind = case Maybe (Term n)
mty of
            Maybe (Term n)
Nothing -> BNFC'Position -> Pattern -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Bind' a
Rzk.BindPattern BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z')
            Just Term n
ty -> BNFC'Position -> Pattern -> Term -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> Bind' a
Rzk.BindPatternType BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (Term n -> Term
go Term n
ty)
       in BNFC'Position -> Bind' BNFC'Position -> Term -> Term -> Term
forall a. a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.Let BNFC'Position
forall a. Maybe a
loc Bind' BNFC'Position
bind (Term n -> Term
go Term n
val) Term
body'

    go (Pair Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (First Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.First BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go (Second Term n
t) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.Second BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go Term n
TypeUnit = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TypeUnit BNFC'Position
forall a. Maybe a
loc
    go Term n
Unit = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Unit BNFC'Position
forall a. Maybe a
loc
    go (Refl Maybe (Term n, Maybe (Term n))
Nothing) = BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Refl BNFC'Position
forall a. Maybe a
loc
    go (Refl (Just (Term n
t, Maybe (Term n)
Nothing))) = BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.ReflTerm BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t)
    go (Refl (Just (Term n
t, Just Term n
ty))) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.ReflTermType BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
t) (Term n -> Term
go Term n
ty)
    go (IdJ Term n
a Term n
b Term n
c Term n
d Term n
e Term n
f) = BNFC'Position
-> Term -> Term -> Term -> Term -> Term -> Term -> Term
forall a.
a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.IdJ BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
a) (Term n -> Term
go Term n
b) (Term n -> Term
go Term n
c) (Term n -> Term
go Term n
d) (Term n -> Term
go Term n
e) (Term n -> Term
go Term n
f)

    go (Match Term n
scrut Maybe (Term n)
mmotive [(VarIdent, Term n)]
branches) =
      case Maybe (Term n)
mmotive of
        Maybe (Term n)
Nothing     -> BNFC'Position -> Term -> [MatchBranch' BNFC'Position] -> Term
forall a. a -> Term' a -> [MatchBranch' a] -> Term' a
Rzk.Match BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
scrut) (((VarIdent, Term n) -> MatchBranch' BNFC'Position)
-> [(VarIdent, Term n)] -> [MatchBranch' BNFC'Position]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdent, Term n) -> MatchBranch' BNFC'Position
goBranch [(VarIdent, Term n)]
branches)
        Just Term n
motive -> BNFC'Position
-> Term -> Term -> [MatchBranch' BNFC'Position] -> Term
forall a. a -> Term' a -> Term' a -> [MatchBranch' a] -> Term' a
Rzk.MatchInto BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
scrut) (Term n -> Term
go Term n
motive) (((VarIdent, Term n) -> MatchBranch' BNFC'Position)
-> [(VarIdent, Term n)] -> [MatchBranch' BNFC'Position]
forall a b. (a -> b) -> [a] -> [b]
map (VarIdent, Term n) -> MatchBranch' BNFC'Position
goBranch [(VarIdent, Term n)]
branches)
      where
        goBranch :: (VarIdent, Term n) -> MatchBranch' BNFC'Position
goBranch (VarIdent
con, Term n
chain) = BNFC'Position
-> VarIdent' BNFC'Position
-> [Pattern]
-> Term
-> MatchBranch' BNFC'Position
forall a.
a -> VarIdent' a -> [Pattern' a] -> Term' a -> MatchBranch' a
Rzk.MatchBranch BNFC'Position
forall a. Maybe a
loc (VarIdent -> VarIdent' BNFC'Position
fromVarIdent VarIdent
con) [Pattern]
pats Term
body
          where ([Pattern]
pats, Term
body) = [VarIdent]
-> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term)
forall (n :: S).
[VarIdent]
-> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term)
matchArms [VarIdent]
used [VarIdent]
supply NameMap n Display
names Term n
chain
    -- An arm never stands alone: the conversion only builds it inside a match
    -- branch, and 'matchArms' peels it before 'go' can see it.
    go MatchArm{} = [Char] -> Term
forall a. HasCallStack => [Char] -> a
error [Char]
"fromTerm: MatchArm outside of a match branch"
    go (TypeAsc Term n
l Term n
r) = BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TypeAsc BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
l) (Term n -> Term
go Term n
r)
    go (TypeRestricted Term n
ty [(Term n, Term n)]
rs) =
      BNFC'Position -> Term -> [Restriction' BNFC'Position] -> Term
forall a. a -> Term' a -> [Restriction' a] -> Term' a
Rzk.TypeRestricted BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
ty) [BNFC'Position -> Term -> Term -> Restriction' BNFC'Position
forall a. a -> Term' a -> Term' a -> Restriction' a
Rzk.Restriction BNFC'Position
forall a. Maybe a
loc (Term n -> Term
go Term n
tope) (Term n -> Term
go Term n
term) | (Term n
tope, Term n
term) <- [(Term n, Term n)]
rs]
    go (TypeModal TModality
m Term n
ty) = BNFC'Position -> Modality -> Term -> Term
forall a. a -> Modality' a -> Term' a -> Term' a
Rzk.ModType BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
m) (Term n -> Term
go Term n
ty)
    go (ModApp TModality
m Term n
t) = BNFC'Position -> Modality -> Term -> Term
forall a. a -> Modality' a -> Term' a -> Term' a
Rzk.ModApp BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
m) (Term n -> Term
go Term n
t)
    go (ModExtract TModality
app TModality
inn Term n
t) = BNFC'Position -> ModComp' BNFC'Position -> Term -> Term
forall a. a -> ModComp' a -> Term' a -> Term' a
Rzk.ModExtract BNFC'Position
forall a. Maybe a
loc (BNFC'Position -> Modality -> Modality -> ModComp' BNFC'Position
forall a. a -> Modality' a -> Modality' a -> ModComp' a
Rzk.Comp BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
app) (TModality -> Modality
goMod TModality
inn)) (Term n -> Term
go Term n
t)
    go (LetMod Binder
z TModality
app TModality
inn Maybe (Term n)
mty Maybe (Term n)
mmotive Term n
val ScopedTerm n
body) = Binder -> ScopedTerm n -> ((Binder, Term) -> Term) -> Term
forall r. Binder -> ScopedTerm n -> ((Binder, Term) -> r) -> r
withBinder1 Binder
z ScopedTerm n
body (((Binder, Term) -> Term) -> Term)
-> ((Binder, Term) -> Term) -> Term
forall a b. (a -> b) -> a -> b
$ \(Binder
z', Term
body') ->
      let bind :: Bind' BNFC'Position
bind = case Maybe (Term n)
mty of
            Maybe (Term n)
Nothing -> BNFC'Position -> Pattern -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Bind' a
Rzk.BindPattern BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z')
            Just Term n
ty -> BNFC'Position -> Pattern -> Term -> Bind' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> Bind' a
Rzk.BindPatternType BNFC'Position
forall a. Maybe a
loc (Binder -> Pattern
binderToPattern Binder
z') (Term n -> Term
go Term n
ty)
       in case (TModality
app, Maybe (Term n)
mmotive) of
            (TModality
Id, Maybe (Term n)
Nothing)     -> BNFC'Position
-> Modality -> Bind' BNFC'Position -> Term -> Term -> Term
forall a.
a -> Modality' a -> Bind' a -> Term' a -> Term' a -> Term' a
Rzk.LetMod BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
inn) Bind' BNFC'Position
bind (Term n -> Term
go Term n
val) Term
body'
            (TModality
Id, Just Term n
motive) -> BNFC'Position
-> Modality -> Bind' BNFC'Position -> Term -> Term -> Term -> Term
forall a.
a
-> Modality' a
-> Bind' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.LetModInto BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
inn) Bind' BNFC'Position
bind (Term n -> Term
go Term n
val) (Term n -> Term
go Term n
motive) Term
body'
            (TModality
_, Maybe (Term n)
Nothing)      -> BNFC'Position
-> Modality
-> Modality
-> Bind' BNFC'Position
-> Term
-> Term
-> Term
forall a.
a
-> Modality' a
-> Modality' a
-> Bind' a
-> Term' a
-> Term' a
-> Term' a
Rzk.LetModFramed BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
app) (TModality -> Modality
goMod TModality
inn) Bind' BNFC'Position
bind (Term n -> Term
go Term n
val) Term
body'
            (TModality
_, Just Term n
motive)  -> BNFC'Position
-> Modality
-> Modality
-> Bind' BNFC'Position
-> Term
-> Term
-> Term
-> Term
forall a.
a
-> Modality' a
-> Modality' a
-> Bind' a
-> Term' a
-> Term' a
-> Term' a
-> Term' a
Rzk.LetModFramedInto BNFC'Position
forall a. Maybe a
loc (TModality -> Modality
goMod TModality
app) (TModality -> Modality
goMod TModality
inn) Bind' BNFC'Position
bind (Term n -> Term
go Term n
val) (Term n -> Term
go Term n
motive) Term
body'

-- | Peel a match branch's arm chain back into its binder patterns and body.
--
-- Each 'MatchArm' contributes one pattern; the bookkeeping per binder is the
-- same as 'fromTerm' does for a λ (freshen the binder's leaves, record the
-- display name, spend a supply name for a placeholder).
matchArms :: [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> ([Rzk.Pattern], Rzk.Term)
matchArms :: forall (n :: S).
[VarIdent]
-> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term)
matchArms [VarIdent]
used [VarIdent]
supply NameMap n Display
names = \case
  MatchArm Binder
z (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig SrcPos TermSig) l
body) ->
    let (Binder
z', [VarIdent]
supply') = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
used [VarIdent]
supply Binder
z
        x :: VarIdent
x = Binder -> [VarIdent] -> VarIdent
displayNameOf Binder
z' [VarIdent]
supply'
        supply'' :: [VarIdent]
supply'' = case Binder
z' of
          BinderVar (Just VarIdent
_) -> [VarIdent]
supply'
          Binder
_                  -> Int -> [VarIdent] -> [VarIdent]
forall a. Int -> [a] -> [a]
drop Int
1 [VarIdent]
supply'
        used' :: [VarIdent]
used' = VarIdent
x VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
used [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
<> Binder -> [VarIdent]
binderLeaves Binder
z'
        ([Pattern]
pats, Term
t) = [VarIdent]
-> [VarIdent]
-> NameMap l Display
-> AST NameBinder (AnnSig SrcPos TermSig) l
-> ([Pattern], Term)
forall (n :: S).
[VarIdent]
-> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term)
matchArms [VarIdent]
used' [VarIdent]
supply'' (NameBinder n l -> Display -> NameMap n Display -> NameMap l Display
forall (n :: S) (l :: S) a.
NameBinder n l -> a -> NameMap n a -> NameMap l a
Foil.addNameBinder NameBinder n l
binder (VarIdent
x, Binder
z') NameMap n Display
names) AST NameBinder (AnnSig SrcPos TermSig) l
body
     in (Binder -> Pattern
binderToPattern Binder
z' Pattern -> [Pattern] -> [Pattern]
forall a. a -> [a] -> [a]
: [Pattern]
pats, Term
t)
  Term n
body -> ([], [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [VarIdent]
used [VarIdent]
supply NameMap n Display
names Term n
body)

-- | The name standing for the variable itself. A single-variable binder uses
-- its own name; a pattern binder needs a placeholder, which is only shown if
-- the whole point is used (in a shape tope, say), and then it is printed as
-- the pattern anyway.
displayNameOf :: Binder -> [VarIdent] -> VarIdent
displayNameOf :: Binder -> [VarIdent] -> VarIdent
displayNameOf (BinderVar (Just VarIdent
x)) [VarIdent]
_ = VarIdent
x
displayNameOf Binder
_ (VarIdent
x : [VarIdent]
_)              = VarIdent
x
displayNameOf Binder
_ []                   = [Char] -> VarIdent
forall a. HasCallStack => [Char] -> a
error [Char]
"not enough fresh variables!"

-- | Refresh a binder's named leaves against the names already in use; draw
-- fresh names for anonymous leaves from the remaining supply.
freshenBinder :: [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder :: [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
_ [VarIdent]
stream (BinderVar Maybe VarIdent
Nothing) =
  case [VarIdent]
stream of
    VarIdent
x : [VarIdent]
xs -> (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x), [VarIdent]
xs)
    [VarIdent]
_      -> [Char] -> (Binder, [VarIdent])
forall a. HasCallStack => [Char] -> a
error [Char]
"not enough fresh variables!"
freshenBinder [VarIdent]
used' [VarIdent]
stream (BinderVar (Just VarIdent
z)) =
  (Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
z'), (VarIdent -> Bool) -> [VarIdent] -> [VarIdent]
forall a. (a -> Bool) -> [a] -> [a]
filter (VarIdent -> VarIdent -> Bool
forall a. Eq a => a -> a -> Bool
/= VarIdent
z') [VarIdent]
stream)
  where z' :: VarIdent
z' = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
used' VarIdent
z
freshenBinder [VarIdent]
_ [VarIdent]
stream Binder
BinderUnit = (Binder
BinderUnit, [VarIdent]
stream)
freshenBinder [VarIdent]
used' [VarIdent]
stream (BinderPair Binder
l Binder
r) =
  let (Binder
l', [VarIdent]
s1) = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder [VarIdent]
used' [VarIdent]
stream Binder
l
      (Binder
r', [VarIdent]
s2) = [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
freshenBinder ([VarIdent]
used' [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Semigroup a => a -> a -> a
<> Binder -> [VarIdent]
binderLeaves Binder
l') [VarIdent]
s1 Binder
r
   in (Binder -> Binder -> Binder
BinderPair Binder
l' Binder
r', [VarIdent]
s2)

-- | Does a scope actually use the variable it binds?
--
-- Compares name /ids/ rather than names, which sidesteps having to unsink the
-- inner scopes' names back into this one. Ids are unique per binder, so a hit is
-- an occurrence of exactly this binder's variable.
--
-- (free-foil's own @freeVarsOf@ would do, but it is not in the 0.2.0 release --
-- it is one of the unreleased helpers on free-foil's @main@.)
scopeUsesItsBinder :: ScopedTerm n -> Bool
scopeUsesItsBinder :: forall (n :: S). ScopedTerm n -> Bool
scopeUsesItsBinder (ScopedAST NameBinder n l
binder AST NameBinder (AnnSig SrcPos TermSig) l
body) =
  Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` AST NameBinder (AnnSig SrcPos TermSig) l -> [Int]
forall (l :: S). Term l -> [Int]
nameIdsOf AST NameBinder (AnnSig SrcPos TermSig) l
body

-- | Every name id occurring in a term, bound or free.
nameIdsOf :: Term l -> [Int]
nameIdsOf :: forall (l :: S). Term l -> [Int]
nameIdsOf (Var Name l
x) = [Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
x]
nameIdsOf (Node AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) l)
  (AST NameBinder (AnnSig SrcPos TermSig) l)
sig) = (ScopedAST NameBinder (AnnSig SrcPos TermSig) l -> [Int])
-> (AST NameBinder (AnnSig SrcPos TermSig) l -> [Int])
-> AnnSig
     SrcPos
     TermSig
     (ScopedAST NameBinder (AnnSig SrcPos TermSig) l)
     (AST NameBinder (AnnSig SrcPos TermSig) l)
-> [Int]
forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> AnnSig SrcPos TermSig a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ScopedAST NameBinder (AnnSig SrcPos TermSig) l -> [Int]
forall {n :: S}.
ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> [Int]
goScoped AST NameBinder (AnnSig SrcPos TermSig) l -> [Int]
forall (l :: S). Term l -> [Int]
nameIdsOf AnnSig
  SrcPos
  TermSig
  (ScopedAST NameBinder (AnnSig SrcPos TermSig) l)
  (AST NameBinder (AnnSig SrcPos TermSig) l)
sig
  where
    goScoped :: ScopedAST NameBinder (AnnSig SrcPos TermSig) n -> [Int]
goScoped (ScopedAST NameBinder n l
_binder AST NameBinder (AnnSig SrcPos TermSig) l
body) = AST NameBinder (AnnSig SrcPos TermSig) l -> [Int]
forall (l :: S). Term l -> [Int]
nameIdsOf AST NameBinder (AnnSig SrcPos TermSig) l
body