-- The scope-extension evidence on 'sinkBound' (a coercion) is its soundness
-- contract, not an argument it can consume, so GHC calls it redundant (and
-- suggests "simplifying" foil's quantified-constraint Ext instance into the
-- signature, which would be absurd). Both warnings stay off.
{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-redundant-constraints
                -fno-warn-simplifiable-class-constraints #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Surface syntax to the free-foil core.
--
-- A transcription of @toTerm@ from "Language.Rzk.Foil.Names", with the variable
-- handling replaced. The environment is still a function from a surface
-- identifier to a term, as before; what changes is what happens at a binder:
--
--   * a binder is a fresh 'Foil.NameBinder' rather than the de Bruijn @Z@;
--   * the environment is carried into the binder's scope with 'Foil.sink', which
--     is a coercion, where the old representation shifted every entry with
--     @S \<$\>@ and so rebuilt every term it held.
--
-- A pattern binder still binds exactly /one/ variable, as before: the components
-- of @\\ (t , s) -> …@ are projections of it, and 'Binder' records the names so
-- they can be shown back to the user.
module Language.Rzk.Foil.Convert where

import           Control.Monad.Foil       (Distinct, NameMap, Scope)
import qualified Control.Monad.Foil       as Foil
import           Control.Monad.Foil.Internal (NameMap (..))
import           Control.Monad.Free.Foil  (AST (..), ScopedAST (..))
import           Data.Data                (Data, cast, gmapQ)
import           Data.Functor             (void)
import qualified Data.IntMap              as IntMap
import           Data.Map                 (Map)
import qualified Data.Map                 as Map
import qualified Data.Set                 as Set
import           Debug.Trace              (trace)   -- FIXME: use proper mechanisms for warnings
import           Unsafe.Coerce            (unsafeCoerce)

import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names (Binder (..), Display,
                                           RzkPosition (RzkPosition),
                                           TModality (..), VarIdent, holeName,
                                           toBinder, varIdent)
import qualified Language.Rzk.Foil.Names as Free
import qualified Language.Rzk.Syntax      as Rzk

-- | The environment: what a surface identifier stands for in the current scope.
-- A pattern binder maps its leaves to projections of the single variable it
-- binds, which is why this is a map to /terms/ and not to names.
type Env n = VarIdent -> Term n

-- | Translate a closed surface term.
toTermClosed :: Rzk.Term -> Term Foil.VoidS
toTermClosed :: Term -> Term 'VoidS
toTermClosed = Scope 'VoidS -> Env 'VoidS -> Term -> Term 'VoidS
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope 'VoidS
Foil.emptyScope Env 'VoidS
forall {a} {a}. Show a => a -> a
unbound
  where
    unbound :: a -> a
unbound a
x = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"undefined variable: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
x)

-- | Enter a pattern binder with an explicit continuation for the body: bind one
-- fresh name, map the pattern's leaves to projections of it, and carry the rest
-- of the environment in with 'Foil.sink'. 'toScopedPattern' is the plain-body
-- special case; a match branch chains further arms through the continuation.
toScopedPatternWith
  :: Distinct n
  => Scope n -> Rzk.Pattern -> Env n
  -> (forall l. Distinct l => Scope l -> Env l -> Term l)
  -> ScopedTerm n
toScopedPatternWith :: forall (n :: S).
Distinct n =>
Scope n
-> Pattern
-> Env n
-> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l)
-> ScopedTerm n
toScopedPatternWith Scope n
scope Pattern
pat Env n
env forall (l :: S). Distinct l => Scope l -> Env l -> Term l
k =
  Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
-> ScopedTerm n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
 -> ScopedTerm n)
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
-> ScopedTerm n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
        bound :: [(VarIdent, Term l)]
bound = Pattern -> Term l -> [(VarIdent, Term l)]
forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
bindings Pattern
pat (Name l -> Term l
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder))
        env' :: VarIdent -> Term l
env' VarIdent
x = case VarIdent -> [(VarIdent, Term l)] -> Maybe (Term l)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup VarIdent
x [(VarIdent, Term l)]
bound of
          Just Term l
t  -> Term l
t
          Maybe (Term l)
Nothing -> AST NameBinder (AnnSig SrcPos TermSig) n -> Term l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (Env n
env VarIdent
x)   -- O(1): the old representation shifted every node
     in NameBinder n l -> Term l -> ScopedTerm n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder (Scope l -> (VarIdent -> Term l) -> Term l
forall (l :: S). Distinct l => Scope l -> Env l -> Term l
k Scope l
scope' VarIdent -> Term l
env')

-- | Enter a pattern binder over a surface body.
toScopedPattern
  :: Distinct n
  => Scope n -> Rzk.Pattern -> Env n -> Rzk.Term -> ScopedTerm n
toScopedPattern :: forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
body =
  Scope n
-> Pattern
-> Env n
-> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l)
-> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n
-> Pattern
-> Env n
-> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l)
-> ScopedTerm n
toScopedPatternWith Scope n
scope Pattern
pat Env n
env (\Scope l
scope' Env l
env' -> Scope l -> Env l -> Term -> Term l
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope l
scope' Env l
env' Term
body)

-- | Enter an anonymous binder (a non-dependent function type binds nothing).
toScopedAnon
  :: Distinct n
  => Scope n -> Env n -> Rzk.Term -> ScopedTerm n
toScopedAnon :: forall (n :: S).
Distinct n =>
Scope n -> Env n -> Term -> ScopedTerm n
toScopedAnon Scope n
scope Env n
env Term
body =
  Scope n
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
-> ScopedTerm n
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
 -> ScopedTerm n)
-> (forall (l :: S). DExt n l => NameBinder n l -> ScopedTerm n)
-> ScopedTerm n
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
    let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
     in NameBinder n l
-> AST NameBinder (AnnSig SrcPos TermSig) l -> ScopedTerm n
forall (binder :: S -> S -> *) (n :: S) (l :: S)
       (sig :: * -> * -> *).
binder n l -> AST binder sig l -> ScopedAST binder sig n
ScopedAST NameBinder n l
binder (Scope l
-> Env l -> Term -> AST NameBinder (AnnSig SrcPos TermSig) l
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope l
scope' (AST NameBinder (AnnSig SrcPos TermSig) n
-> AST NameBinder (AnnSig SrcPos TermSig) l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
Foil.sink (AST NameBinder (AnnSig SrcPos TermSig) n
 -> AST NameBinder (AnnSig SrcPos TermSig) l)
-> Env n -> Env l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env n
env) Term
body)

-- | What each leaf of a pattern stands for: a projection chain over the single
-- variable the pattern binds.
bindings :: Rzk.Pattern -> Term n -> [(VarIdent, Term n)]
bindings :: forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
bindings (Rzk.PatternUnit BNFC'Position
_loc) Term n
_ = []
bindings (Rzk.PatternVar BNFC'Position
_loc (Rzk.VarIdent BNFC'Position
_ VarIdentToken
"_")) Term n
_ = []
bindings (Rzk.PatternVar BNFC'Position
_loc VarIdent' BNFC'Position
x) Term n
t = [(VarIdent' BNFC'Position -> VarIdent
varIdent VarIdent' BNFC'Position
x, Term n
t)]
bindings (Rzk.PatternPair BNFC'Position
_loc Pattern
l Pattern
r) Term n
t = Pattern -> Term n -> [(VarIdent, Term n)]
forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
bindings Pattern
l (Term n -> Term n
forall {n :: S}. Term n -> Term n
First Term n
t) [(VarIdent, Term n)]
-> [(VarIdent, Term n)] -> [(VarIdent, Term n)]
forall a. Semigroup a => a -> a -> a
<> Pattern -> Term n -> [(VarIdent, Term n)]
forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
bindings Pattern
r (Term n -> Term n
forall {n :: S}. Term n -> Term n
Second Term n
t)
bindings (Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps) Term n
t =
  Pattern -> Term n -> [(VarIdent, Term n)]
forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
bindings (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
Free.desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1) Term n
t

toTerm :: forall n. Distinct n => Scope n -> Env n -> Rzk.Term -> Term n
toTerm :: forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope n
scope Env n
env = Term -> Term n
go
  where
    ppBNFC'Position :: Maybe (a, a) -> [Char]
ppBNFC'Position Maybe (a, a)
Nothing = [Char]
""
    ppBNFC'Position (Just (a
line_, a
col)) = [Char]
" at line " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
line_ [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" column " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
col

    -- A notation that is fine, but that a simpler one says as well.
    lint :: a -> a -> a -> a
lint a
orig a
suggestion = [Char] -> a -> a
forall a. [Char] -> a -> a
trace ([Char] -> a -> a) -> [Char] -> a -> a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
      [ [Char]
"[HINT]:" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> BNFC'Position -> [Char]
forall {a} {a}. (Show a, Show a) => Maybe (a, a) -> [Char]
ppBNFC'Position (a -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
Rzk.hasPosition a
orig) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" consider replacing"
      , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree a
orig
      , [Char]
"with the following"
      , [Char]
"  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree a
suggestion
      ]

    -- Every node is tagged with where it was written, so that a diagnostic
    -- points at the sub-term it is about rather than at the declaration around
    -- it.
    --
    -- A node with no position of its own is left with whatever the conversion
    -- of its body found. Desugaring builds surface nodes and hands them back to
    -- 'go', and not all of them carry a position: the λ that @addParams@ wraps
    -- a definition's body in is spelled nowhere, and overwriting the body's
    -- position with its absence would put every such error back on the
    -- declaration line.
    --
    -- The file is not recorded here: a term is converted while checking a known
    -- module, and the diagnostic takes the path from the context around it.
    go :: Rzk.Term -> Term n
    go :: Term -> Term n
go Term
term = case Term -> BNFC'Position
forall a. HasPosition a => a -> BNFC'Position
Rzk.hasPosition Term
term of
      BNFC'Position
Nothing  -> Term -> Term n
go' Term
term
      Just (Int, Int)
pos -> RzkPosition -> Term n -> Term n
forall (n :: S). RzkPosition -> Term n -> Term n
atSrcPos (Maybe [Char] -> BNFC'Position -> RzkPosition
RzkPosition Maybe [Char]
forall a. Maybe a
Nothing ((Int, Int) -> BNFC'Position
forall a. a -> Maybe a
Just (Int, Int)
pos)) (Term -> Term n
go' Term
term)

    go' :: Rzk.Term -> Term n
    go' :: Term -> Term n
go' = \case
      -- ASCII aliases are desugared exactly as before.
      Rzk.ASCII_CubeUnitStar BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeUnitStar BNFC'Position
loc)
      Rzk.ASCII_Cube2_0 BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_0 BNFC'Position
loc)
      Rzk.ASCII_Cube2_1 BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Cube2_1 BNFC'Position
loc)
      Rzk.ASCII_TopeTop BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeTop BNFC'Position
loc)
      Rzk.ASCII_TopeBottom BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.TopeBottom BNFC'Position
loc)
      Rzk.ASCII_TopeEQ BNFC'Position
loc Term
l Term
r -> Term -> Term n
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeEQ BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeLEQ BNFC'Position
loc Term
l Term
r -> Term -> Term n
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeLEQ BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeAnd BNFC'Position
loc Term
l Term
r -> Term -> Term n
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeAnd BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TopeOr BNFC'Position
loc Term
l Term
r -> Term -> Term n
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.TopeOr BNFC'Position
loc Term
l Term
r)
      Rzk.ASCII_TypeFun BNFC'Position
loc ParamDecl' BNFC'Position
param Term
ret -> Term -> Term n
go (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc ParamDecl' BNFC'Position
param Term
ret)
      Rzk.ASCII_TypeSigma BNFC'Position
loc Pattern
pat Term
ty Term
ret -> Term -> Term n
go (BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
loc Pattern
pat Term
ty Term
ret)
      Rzk.ASCII_TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
p [SigmaParam' BNFC'Position]
ps Term
tN -> Term -> Term n
go (BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
p [SigmaParam' BNFC'Position]
ps Term
tN)
      Rzk.ASCII_Lambda BNFC'Position
loc [Param' BNFC'Position]
pat Term
ret -> Term -> Term n
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
pat Term
ret)
      Rzk.ASCII_First BNFC'Position
loc Term
term -> Term -> Term n
go (BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.First BNFC'Position
loc Term
term)
      Rzk.ASCII_Second BNFC'Position
loc Term
term -> Term -> Term n
go (BNFC'Position -> Term -> Term
forall a. a -> Term' a -> Term' a
Rzk.Second BNFC'Position
loc Term
term)
      Rzk.ASCII_CubeI BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI BNFC'Position
loc)
      Rzk.ASCII_CubeI_0 BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_0 BNFC'Position
loc)
      Rzk.ASCII_CubeI_1 BNFC'Position
loc -> Term -> Term n
go (BNFC'Position -> Term
forall a. a -> Term' a
Rzk.CubeI_1 BNFC'Position
loc)

      Rzk.Var BNFC'Position
_loc VarIdent' BNFC'Position
x -> Env n
env (VarIdent' BNFC'Position -> VarIdent
varIdent VarIdent' BNFC'Position
x)
      Rzk.Universe BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
Universe
      Rzk.UniverseCube BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
UniverseCube
      Rzk.UniverseTope BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
UniverseTope
      Rzk.CubeUnit BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
CubeUnit
      Rzk.CubeUnitStar BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
CubeUnitStar
      Rzk.Cube2 BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
Cube2
      Rzk.Cube2_0 BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
Cube2_0
      Rzk.Cube2_1 BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
Cube2_1
      Rzk.CubeI BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
CubeI
      Rzk.CubeI_0 BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
CubeI_0
      Rzk.CubeI_1 BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
CubeI_1
      Rzk.CubeProduct BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
CubeProduct (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.TopeTop BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
TopeTop
      Rzk.TopeBottom BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
TopeBottom
      Rzk.TopeEQ BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
TopeEQ (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.TopeLEQ BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
TopeLEQ (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.TopeAnd BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
TopeAnd (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.TopeOr BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
TopeOr (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.TopeInv BNFC'Position
_loc Term
t -> Term n -> Term n
forall {n :: S}. Term n -> Term n
TopeInv (Term -> Term n
go Term
t)
      Rzk.TopeUninv BNFC'Position
_loc Term
t -> Term n -> Term n
forall {n :: S}. Term n -> Term n
TopeUninv (Term -> Term n
go Term
t)
      Rzk.CubeFlip BNFC'Position
_loc Term
t -> Term n -> Term n
forall {n :: S}. Term n -> Term n
CubeFlip (Term -> Term n
go Term
t)
      Rzk.CubeUnflip BNFC'Position
_loc Term
t -> Term n -> Term n
forall {n :: S}. Term n -> Term n
CubeUnflip (Term -> Term n
go Term
t)
      Rzk.CubeSup BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
CubeSup (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.CubeInf BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
CubeInf (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.RecBottom BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
RecBottom
      Rzk.RecOr BNFC'Position
_loc [Restriction' BNFC'Position]
rs -> [(Term n, Term n)] -> Term n
forall {n :: S}. [(Term n, Term n)] -> Term n
RecOr ((Restriction' BNFC'Position -> (Term n, Term n))
-> [Restriction' BNFC'Position] -> [(Term n, Term n)]
forall a b. (a -> b) -> [a] -> [b]
map Restriction' BNFC'Position -> (Term n, Term n)
restriction [Restriction' BNFC'Position]
rs)
      Rzk.TypeId BNFC'Position
_loc Term
x Term
tA Term
y -> Term n -> Maybe (Term n) -> Term n -> Term n
forall {n :: S}. Term n -> Maybe (Term n) -> Term n -> Term n
TypeId (Term -> Term n
go Term
x) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
tA)) (Term -> Term n
go Term
y)
      Rzk.TypeIdSimple BNFC'Position
_loc Term
x Term
y -> Term n -> Maybe (Term n) -> Term n -> Term n
forall {n :: S}. Term n -> Maybe (Term n) -> Term n -> Term n
TypeId (Term -> Term n
go Term
x) Maybe (Term n)
forall a. Maybe a
Nothing (Term -> Term n
go Term
y)
      Rzk.TypeUnit BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
TypeUnit
      Rzk.Unit BNFC'Position
_loc -> Term n
forall {n :: S}. Term n
Unit
      Rzk.App BNFC'Position
_loc Term
f Term
x -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
App (Term -> Term n
go Term
f) (Term -> Term n
go Term
x)
      Rzk.Pair BNFC'Position
_loc Term
l Term
r -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
Pair (Term -> Term n
go Term
l) (Term -> Term n
go Term
r)
      Rzk.Tuple BNFC'Position
loc Term
p1 Term
p2 (Term
p : [Term]
ps) -> Term -> Term n
go (BNFC'Position -> Term -> Term -> [Term] -> Term
forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
Rzk.Tuple BNFC'Position
loc (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
loc Term
p1 Term
p2) Term
p [Term]
ps)
      Rzk.Tuple BNFC'Position
loc Term
p1 Term
p2 [] -> Term -> Term n
go (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
loc Term
p1 Term
p2)
      Rzk.First BNFC'Position
_loc Term
term -> Term n -> Term n
forall {n :: S}. Term n -> Term n
First (Term -> Term n
go Term
term)
      Rzk.Second BNFC'Position
_loc Term
term -> Term n -> Term n
forall {n :: S}. Term n -> Term n
Second (Term -> Term n
go Term
term)
      Rzk.Refl BNFC'Position
_loc -> Maybe (Term n, Maybe (Term n)) -> Term n
forall {n :: S}. Maybe (Term n, Maybe (Term n)) -> Term n
Refl Maybe (Term n, Maybe (Term n))
forall a. Maybe a
Nothing
      Rzk.ReflTerm BNFC'Position
_loc Term
term -> Maybe (Term n, Maybe (Term n)) -> Term n
forall {n :: S}. Maybe (Term n, Maybe (Term n)) -> Term n
Refl ((Term n, Maybe (Term n)) -> Maybe (Term n, Maybe (Term n))
forall a. a -> Maybe a
Just (Term -> Term n
go Term
term, Maybe (Term n)
forall a. Maybe a
Nothing))
      Rzk.ReflTermType BNFC'Position
_loc Term
x Term
tA -> Maybe (Term n, Maybe (Term n)) -> Term n
forall {n :: S}. Maybe (Term n, Maybe (Term n)) -> Term n
Refl ((Term n, Maybe (Term n)) -> Maybe (Term n, Maybe (Term n))
forall a. a -> Maybe a
Just (Term -> Term n
go Term
x, Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
tA)))
      Rzk.IdJ BNFC'Position
_loc Term
a Term
b Term
c Term
d Term
e Term
f -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
forall {n :: S}.
Term n -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
IdJ (Term -> Term n
go Term
a) (Term -> Term n
go Term
b) (Term -> Term n
go Term
c) (Term -> Term n
go Term
d) (Term -> Term n
go Term
e) (Term -> Term n
go Term
f)
      Rzk.Match BNFC'Position
_loc Term
scrut [MatchBranch' BNFC'Position]
branches ->
        Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
forall {n :: S}.
Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
Match (Term -> Term n
go Term
scrut) Maybe (Term n)
forall a. Maybe a
Nothing ((MatchBranch' BNFC'Position -> (VarIdent, Term n))
-> [MatchBranch' BNFC'Position] -> [(VarIdent, Term n)]
forall a b. (a -> b) -> [a] -> [b]
map MatchBranch' BNFC'Position -> (VarIdent, Term n)
matchBranch [MatchBranch' BNFC'Position]
branches)
      Rzk.MatchInto BNFC'Position
_loc Term
scrut Term
motive [MatchBranch' BNFC'Position]
branches ->
        Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
forall {n :: S}.
Term n -> Maybe (Term n) -> [(VarIdent, Term n)] -> Term n
Match (Term -> Term n
go Term
scrut) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
motive)) ((MatchBranch' BNFC'Position -> (VarIdent, Term n))
-> [MatchBranch' BNFC'Position] -> [(VarIdent, Term n)]
forall a b. (a -> b) -> [a] -> [b]
map MatchBranch' BNFC'Position -> (VarIdent, Term n)
matchBranch [MatchBranch' BNFC'Position]
branches)
      Rzk.TypeAsc BNFC'Position
_loc Term
x Term
t -> Term n -> Term n -> Term n
forall {n :: S}. Term n -> Term n -> Term n
TypeAsc (Term -> Term n
go Term
x) (Term -> Term n
go Term
t)

      -- A binder may name several variables sharing a type, e.g. @(x y : A)@,
      -- which parses as an application spine; desugar into nested one-variable
      -- binders, as before.
      Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermType BNFC'Position
loc' Term
patTerm Term
arg) Term
ret
        | Term
_ : Term
_ : [Term]
_ <- [Term]
vars ->
            Term -> Term n
go ((Term -> Term -> Term) -> Term -> [Term] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term
v -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
loc' Term
v Term
arg)) Term
ret [Term]
vars)
        where vars :: [Term]
vars = Term -> [Term]
Free.flattenBinderApp Term
patTerm
      Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermModalType BNFC'Position
loc' Term
patTerm ModalColon' BNFC'Position
mc Term
ty) Term
ret
        | Term
_ : Term
_ : [Term]
_ <- [Term]
vars ->
            Term -> Term n
go ((Term -> Term -> Term) -> Term -> [Term] -> Term
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Term
v -> BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
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
loc' Term
v ModalColon' BNFC'Position
mc Term
ty)) Term
ret [Term]
vars)
        where vars :: [Term]
vars = Term -> [Term]
Free.flattenBinderApp Term
patTerm

      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamTermModalType BNFC'Position
_loc' Term
patTerm ModalColon' BNFC'Position
mc Term
ty) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
Free.unsafeTermToPattern Term
patTerm
            md :: TModality
md = ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc
         in Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
md (Term -> Term n
go Term
ty) Maybe (ScopedTerm n)
forall a. Maybe a
Nothing (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamTermModalShape BNFC'Position
_loc' Term
patTerm ModalColon' BNFC'Position
mc Term
cube Term
tope) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
Free.unsafeTermToPattern Term
patTerm
            md :: TModality
md = ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc
         in Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
md (Term -> Term n
go Term
cube)
              (ScopedTerm n -> Maybe (ScopedTerm n)
forall a. a -> Maybe a
Just (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tope))
              (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamTermType BNFC'Position
_ Term
patTerm Term
arg) Term
ret ->
        let pat :: Pattern
pat = Term -> Pattern
Free.unsafeTermToPattern Term
patTerm
         in Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (Term -> Term n
go Term
arg) Maybe (ScopedTerm n)
forall a. Maybe a
Nothing (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
ret)
      t :: Term
t@(Rzk.TypeFun BNFC'Position
loc (Rzk.ParamTermShape BNFC'Position
loc' Term
patTerm Term
cube Term
tope) Term
ret) ->
        let lint' :: a -> a
lint' = case Term
tope of
              -- a shape whose tope is a predicate applied to exactly the binder
              -- is the type of that predicate, and says so more directly
              Rzk.App BNFC'Position
_loc Term
fun Term
arg | Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
arg Term' () -> Term' () -> Bool
forall a. Eq a => a -> a -> Bool
== Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
patTerm ->
                Term -> Term -> a -> a
forall {a} {a} {a}.
(HasPosition a, Print a, Print a) =>
a -> a -> a -> a
lint Term
t (BNFC'Position -> ParamDecl' BNFC'Position -> Term -> Term
forall a. a -> ParamDecl' a -> Term' a -> Term' a
Rzk.TypeFun BNFC'Position
loc (BNFC'Position -> Term -> Term -> ParamDecl' BNFC'Position
forall a. a -> Term' a -> Term' a -> ParamDecl' a
Rzk.ParamTermType BNFC'Position
loc' Term
patTerm Term
fun) Term
ret)
              Term
_ -> a -> a
forall a. a -> a
id
            pat :: Pattern
pat = Term -> Pattern
Free.unsafeTermToPattern Term
patTerm
         in Term n -> Term n
forall a. a -> a
lint' (Term n -> Term n) -> Term n -> Term n
forall a b. (a -> b) -> a -> b
$ Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (Term -> Term n
go Term
cube)
              (ScopedTerm n -> Maybe (ScopedTerm n)
forall a. a -> Maybe a
Just (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tope))
              (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
ret)
      Rzk.TypeFun BNFC'Position
_loc (Rzk.ParamType BNFC'Position
_ Term
arg) Term
ret ->
        Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> Term n
-> Maybe (ScopedTerm n)
-> ScopedTerm n
-> Term n
TypeFun (Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing) TModality
Id (Term -> Term n
go Term
arg) Maybe (ScopedTerm n)
forall a. Maybe a
Nothing (Scope n -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Env n -> Term -> ScopedTerm n
toScopedAnon Scope n
scope Env n
env Term
ret)

      Rzk.TypeSigma BNFC'Position
_loc Pattern
pat Term
tA Term
tB ->
        Binder -> TModality -> Term n -> ScopedTerm n -> Term n
forall {n :: S}.
Binder -> TModality -> Term n -> ScopedTerm n -> Term n
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) TModality
Id (Term -> Term n
go Term
tA) (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tB)
      Rzk.TypeSigmaModal BNFC'Position
_loc Pattern
pat ModalColon' BNFC'Position
mc Term
ty Term
body ->
        Binder -> TModality -> Term n -> ScopedTerm n -> Term n
forall {n :: S}.
Binder -> TModality -> Term n -> ScopedTerm n -> Term n
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) (ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc) (Term -> Term n
go Term
ty)
          (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
body)
      Rzk.TypeSigmaTuple BNFC'Position
loc (Rzk.SigmaParamModal BNFC'Position
_loc' Pattern
pat ModalColon' BNFC'Position
mc Term
ty) [SigmaParam' BNFC'Position]
rest Term
body ->
        let tailSigma :: Term
tailSigma = case [SigmaParam' BNFC'Position]
rest of
              []       -> Term
body
              [SigmaParam' BNFC'Position
sp]     -> BNFC'Position -> SigmaParam' BNFC'Position -> Term -> Term
Free.sigmaParamToTypeSigma BNFC'Position
loc SigmaParam' BNFC'Position
sp Term
body
              (SigmaParam' BNFC'Position
sp:[SigmaParam' BNFC'Position]
sps) -> BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
sp [SigmaParam' BNFC'Position]
sps Term
body
         in Binder -> TModality -> Term n -> ScopedTerm n -> Term n
forall {n :: S}.
Binder -> TModality -> Term n -> ScopedTerm n -> Term n
TypeSigma (Pattern -> Binder
toBinder Pattern
pat) (ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc) (Term -> Term n
go Term
ty)
              (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tailSigma)
      Rzk.TypeSigmaTuple BNFC'Position
loc (Rzk.SigmaParam BNFC'Position
_ Pattern
patA Term
tA) (mp :: SigmaParam' BNFC'Position
mp@Rzk.SigmaParamModal{} : [SigmaParam' BNFC'Position]
rest) Term
body ->
        Term -> Term n
go (BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
loc Pattern
patA Term
tA (case [SigmaParam' BNFC'Position]
rest of
              [] -> BNFC'Position -> SigmaParam' BNFC'Position -> Term -> Term
Free.sigmaParamToTypeSigma BNFC'Position
loc SigmaParam' BNFC'Position
mp Term
body
              [SigmaParam' BNFC'Position]
_  -> BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
loc SigmaParam' BNFC'Position
mp [SigmaParam' BNFC'Position]
rest Term
body))
      Rzk.TypeSigmaTuple BNFC'Position
loc (Rzk.SigmaParam BNFC'Position
_ Pattern
patA Term
tA) (Rzk.SigmaParam BNFC'Position
_ Pattern
patB Term
tB : [SigmaParam' BNFC'Position]
ps) Term
tN ->
        Term -> Term n
go (BNFC'Position
-> SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position]
-> Term
-> Term
forall a.
a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a
Rzk.TypeSigmaTuple BNFC'Position
loc (BNFC'Position -> Pattern -> Term -> SigmaParam' BNFC'Position
forall a. a -> Pattern' a -> Term' a -> SigmaParam' a
Rzk.SigmaParam BNFC'Position
loc Pattern
patX Term
tX) [SigmaParam' BNFC'Position]
ps Term
tN)
        where
          patX :: Pattern
patX = BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
loc Pattern
patA Pattern
patB
          tX :: Term
tX = BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
loc Pattern
patA Term
tA Term
tB
      Rzk.TypeSigmaTuple BNFC'Position
loc (Rzk.SigmaParam BNFC'Position
_ Pattern
pat Term
tA) [] Term
tB -> Term -> Term n
go (BNFC'Position -> Pattern -> Term -> Term -> Term
forall a. a -> Pattern' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigma BNFC'Position
loc Pattern
pat Term
tA Term
tB)

      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternModalType BNFC'Position
_ [] ModalColon' BNFC'Position
_mc Term
_ty : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term n
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
params Term
body)
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternModalType BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) ModalColon' BNFC'Position
mc Term
ty : [Param' BNFC'Position]
params) Term
body ->
        Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda (Pattern -> Binder
toBinder Pattern
pat) (LambdaParam (ScopedTerm n) (Term n)
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
forall a. a -> Maybe a
Just (TModality
-> Term n
-> Maybe (ScopedTerm n)
-> LambdaParam (ScopedTerm n) (Term n)
forall scope term.
TModality -> term -> Maybe scope -> LambdaParam scope term
LambdaParam (ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc) (Term -> Term n
go Term
ty) Maybe (ScopedTerm n)
forall a. Maybe a
Nothing))
          (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env
            (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc (if [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats then [Param' BNFC'Position]
params else 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
loc' [Pattern]
pats ModalColon' BNFC'Position
mc Term
ty Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternModalShape BNFC'Position
_ [] ModalColon' BNFC'Position
_mc Term
_cube Term
_tope : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term n
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
params Term
body)
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternModalShape BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) ModalColon' BNFC'Position
mc Term
cube Term
tope : [Param' BNFC'Position]
params) Term
body ->
        Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda (Pattern -> Binder
toBinder Pattern
pat)
          (LambdaParam (ScopedTerm n) (Term n)
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
forall a. a -> Maybe a
Just (TModality
-> Term n
-> Maybe (ScopedTerm n)
-> LambdaParam (ScopedTerm n) (Term n)
forall scope term.
TModality -> term -> Maybe scope -> LambdaParam scope term
LambdaParam (ModalColon' BNFC'Position -> TModality
Free.modalColonToTModality ModalColon' BNFC'Position
mc) (Term -> Term n
go Term
cube)
                   (ScopedTerm n -> Maybe (ScopedTerm n)
forall a. a -> Maybe a
Just (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tope))))
          (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env
            (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc (if [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats then [Param' BNFC'Position]
params else 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
loc' [Pattern]
pats ModalColon' BNFC'Position
mc Term
cube Term
tope Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))
      Rzk.Lambda BNFC'Position
_loc [] Term
body -> Term -> Term n
go Term
body
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPattern BNFC'Position
_ Pattern
pat : [Param' BNFC'Position]
params) Term
body ->
        Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda (Pattern -> Binder
toBinder Pattern
pat) Maybe (LambdaParam (ScopedTerm n) (Term n))
forall a. Maybe a
Nothing
          (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
params Term
body))
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternType BNFC'Position
_ [] Term
_ty : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term n
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
params Term
body)
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternType BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) Term
ty : [Param' BNFC'Position]
params) Term
body ->
        Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda (Pattern -> Binder
toBinder Pattern
pat) (LambdaParam (ScopedTerm n) (Term n)
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
forall a. a -> Maybe a
Just (TModality
-> Term n
-> Maybe (ScopedTerm n)
-> LambdaParam (ScopedTerm n) (Term n)
forall scope term.
TModality -> term -> Maybe scope -> LambdaParam scope term
LambdaParam TModality
Id (Term -> Term n
go Term
ty) Maybe (ScopedTerm n)
forall a. Maybe a
Nothing))
          (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env
            (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc (BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
loc' [Pattern]
pats Term
ty Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))
      Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternShape BNFC'Position
_ [] Term
_cube Term
_tope : [Param' BNFC'Position]
params) Term
body ->
        Term -> Term n
go (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc [Param' BNFC'Position]
params Term
body)
      t :: Term
t@(Rzk.Lambda BNFC'Position
loc (Rzk.ParamPatternShape BNFC'Position
loc' (Pattern
pat:[Pattern]
pats) Term
cube Term
tope : [Param' BNFC'Position]
params) Term
body) ->
        let lint' :: a -> a
lint' = case Term
tope of
              Rzk.App BNFC'Position
_loc Term
fun Term
arg
                | [Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern]
pats Bool -> Bool -> Bool
&& Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term
arg Term' () -> Term' () -> Bool
forall a. Eq a => a -> a -> Bool
== Term -> Term' ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Pattern -> Term
Free.patternToTerm Pattern
pat) ->
                    Term -> Term -> a -> a
forall {a} {a} {a}.
(HasPosition a, Print a, Print a) =>
a -> a -> a -> a
lint Term
t (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc (BNFC'Position -> [Pattern] -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Param' a
Rzk.ParamPatternType BNFC'Position
loc' [Pattern
pat] Term
fun Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body)
              Term
_ -> a -> a
forall a. a -> a
id
         in Term n -> Term n
forall a. a -> a
lint' (Term n -> Term n) -> Term n -> Term n
forall a b. (a -> b) -> a -> b
$ Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
-> ScopedTerm n
-> Term n
Lambda (Pattern -> Binder
toBinder Pattern
pat)
              (LambdaParam (ScopedTerm n) (Term n)
-> Maybe (LambdaParam (ScopedTerm n) (Term n))
forall a. a -> Maybe a
Just (TModality
-> Term n
-> Maybe (ScopedTerm n)
-> LambdaParam (ScopedTerm n) (Term n)
forall scope term.
TModality -> term -> Maybe scope -> LambdaParam scope term
LambdaParam TModality
Id (Term -> Term n
go Term
cube) (ScopedTerm n -> Maybe (ScopedTerm n)
forall a. a -> Maybe a
Just (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
tope))))
              (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env
                (BNFC'Position -> [Param' BNFC'Position] -> Term -> Term
forall a. a -> [Param' a] -> Term' a -> Term' a
Rzk.Lambda BNFC'Position
loc (BNFC'Position -> [Pattern] -> Term -> Term -> Param' BNFC'Position
forall a. a -> [Pattern' a] -> Term' a -> Term' a -> Param' a
Rzk.ParamPatternShape BNFC'Position
loc' [Pattern]
pats Term
cube Term
tope Param' BNFC'Position
-> [Param' BNFC'Position] -> [Param' BNFC'Position]
forall a. a -> [a] -> [a]
: [Param' BNFC'Position]
params) Term
body))

      Rzk.Let BNFC'Position
_loc (Rzk.BindPattern BNFC'Position
_ Pattern
pat) Term
val Term
expr ->
        Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
forall {n :: S}.
Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
Let (Pattern -> Binder
toBinder Pattern
pat) Maybe (Term n)
forall a. Maybe a
Nothing (Term -> Term n
go Term
val) (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
expr)
      Rzk.Let BNFC'Position
_loc (Rzk.BindPatternType BNFC'Position
_ Pattern
pat Term
ty) Term
val Term
expr ->
        Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
forall {n :: S}.
Binder -> Maybe (Term n) -> Term n -> ScopedTerm n -> Term n
Let (Pattern -> Binder
toBinder Pattern
pat) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
ty)) (Term -> Term n
go Term
val) (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
expr)

      Rzk.TypeRestricted BNFC'Position
_loc Term
ty [Restriction' BNFC'Position]
rs -> Term n -> [(Term n, Term n)] -> Term n
forall {n :: S}. Term n -> [(Term n, Term n)] -> Term n
TypeRestricted (Term -> Term n
go Term
ty) ((Restriction' BNFC'Position -> (Term n, Term n))
-> [Restriction' BNFC'Position] -> [(Term n, Term n)]
forall a b. (a -> b) -> [a] -> [b]
map Restriction' BNFC'Position -> (Term n, Term n)
restriction [Restriction' BNFC'Position]
rs)
      Rzk.Hole BNFC'Position
_loc (Rzk.HoleIdent BNFC'Position
_ (Rzk.HoleIdentToken Text
tok)) -> Maybe VarIdent -> Term n
forall {n :: S}. Maybe VarIdent -> Term n
Hole (Text -> Maybe VarIdent
holeName Text
tok)
      Rzk.ModApp BNFC'Position
_loc Modality' BNFC'Position
md Term
body -> TModality -> Term n -> Term n
forall {n :: S}. TModality -> Term n -> Term n
ModApp (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
md) (Term -> Term n
go Term
body)
      Rzk.ModType BNFC'Position
_loc Modality' BNFC'Position
md Term
ty -> TModality -> Term n -> Term n
forall {n :: S}. TModality -> Term n -> Term n
TypeModal (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
md) (Term -> Term n
go Term
ty)
      Rzk.ModExtract{} -> [Char] -> Term n
forall a. HasCallStack => [Char] -> a
error [Char]
"$extract$ is an internal term and cannot appear in source"
      Rzk.LetModBind BNFC'Position
_loc Modality' BNFC'Position
md Bind' BNFC'Position
bind Term
val Term
body ->
        let m :: TModality
m = Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
md
         in Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind TModality
Id TModality
m (TModality -> Term n -> Term n
forall {n :: S}. TModality -> Term n -> Term n
ModApp TModality
m (Term -> Term n
go Term
val)) Maybe (Term n)
forall a. Maybe a
Nothing Term
body
      Rzk.LetModBindInto BNFC'Position
_loc Modality' BNFC'Position
md Bind' BNFC'Position
bind Term
val Term
motive Term
body ->
        let m :: TModality
m = Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
md
         in Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind TModality
Id TModality
m (TModality -> Term n -> Term n
forall {n :: S}. TModality -> Term n -> Term n
ModApp TModality
m (Term -> Term n
go Term
val)) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
motive)) Term
body
      Rzk.LetMod BNFC'Position
_loc Modality' BNFC'Position
inn Bind' BNFC'Position
bind Term
val Term
body ->
        Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind TModality
Id (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
inn) (Term -> Term n
go Term
val) Maybe (Term n)
forall a. Maybe a
Nothing Term
body
      Rzk.LetModInto BNFC'Position
_loc Modality' BNFC'Position
inn Bind' BNFC'Position
bind Term
val Term
motive Term
body ->
        Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind TModality
Id (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
inn) (Term -> Term n
go Term
val) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
motive)) Term
body
      Rzk.LetModFramed BNFC'Position
_loc Modality' BNFC'Position
ext Modality' BNFC'Position
inn Bind' BNFC'Position
bind Term
val Term
body ->
        Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
ext) (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
inn) (Term -> Term n
go Term
val) Maybe (Term n)
forall a. Maybe a
Nothing Term
body
      Rzk.LetModFramedInto BNFC'Position
_loc Modality' BNFC'Position
ext Modality' BNFC'Position
inn Bind' BNFC'Position
bind Term
val Term
motive Term
body ->
        Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
ext) (Modality' BNFC'Position -> TModality
Free.toModality Modality' BNFC'Position
inn) (Term -> Term n
go Term
val) (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
motive)) Term
body
    letMod :: Bind' BNFC'Position
-> TModality
-> TModality
-> Term n
-> Maybe (Term n)
-> Term
-> Term n
letMod Bind' BNFC'Position
bind TModality
app TModality
inn Term n
value Maybe (Term n)
mmotive Term
body =
      case Bind' BNFC'Position
bind of
        Rzk.BindPattern BNFC'Position
_ Pattern
pat ->
          Binder
-> TModality
-> TModality
-> Maybe (Term n)
-> Maybe (Term n)
-> Term n
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> TModality
-> Maybe (Term n)
-> Maybe (Term n)
-> Term n
-> ScopedTerm n
-> Term n
LetMod (Pattern -> Binder
toBinder Pattern
pat) TModality
app TModality
inn Maybe (Term n)
forall a. Maybe a
Nothing Maybe (Term n)
mmotive Term n
value (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
body)
        Rzk.BindPatternType BNFC'Position
_ Pattern
pat Term
ty ->
          Binder
-> TModality
-> TModality
-> Maybe (Term n)
-> Maybe (Term n)
-> Term n
-> ScopedTerm n
-> Term n
forall {n :: S}.
Binder
-> TModality
-> TModality
-> Maybe (Term n)
-> Maybe (Term n)
-> Term n
-> ScopedTerm n
-> Term n
LetMod (Pattern -> Binder
toBinder Pattern
pat) TModality
app TModality
inn (Term n -> Maybe (Term n)
forall a. a -> Maybe a
Just (Term -> Term n
go Term
ty)) Maybe (Term n)
mmotive Term n
value (Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
forall (n :: S).
Distinct n =>
Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
toScopedPattern Scope n
scope Pattern
pat Env n
env Term
body)

    restriction :: Restriction' BNFC'Position -> (Term n, Term n)
restriction = \case
      Rzk.Restriction BNFC'Position
_loc Term
tope Term
term       -> (Term -> Term n
go Term
tope, Term -> Term n
go Term
term)
      Rzk.ASCII_Restriction BNFC'Position
_loc Term
tope Term
term -> (Term -> Term n
go Term
tope, Term -> Term n
go Term
term)

    -- One branch of a match: each pattern becomes one 'MatchArm' binder, and
    -- the last arm's scope holds the branch body.
    matchBranch :: MatchBranch' BNFC'Position -> (VarIdent, Term n)
matchBranch (Rzk.MatchBranch BNFC'Position
_loc VarIdent' BNFC'Position
con [Pattern]
pats Term
body) =
      (VarIdent' BNFC'Position -> VarIdent
varIdent VarIdent' BNFC'Position
con, Scope n -> Env n -> [Pattern] -> Term n
forall (m :: S).
Distinct m =>
Scope m -> Env m -> [Pattern] -> Term m
arms Scope n
scope Env n
env [Pattern]
pats)
      where
        arms :: forall m. Distinct m => Scope m -> Env m -> [Rzk.Pattern] -> Term m
        arms :: forall (m :: S).
Distinct m =>
Scope m -> Env m -> [Pattern] -> Term m
arms Scope m
sc Env m
en []       = Scope m -> Env m -> Term -> Term m
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope m
sc Env m
en Term
body
        arms Scope m
sc Env m
en (Pattern
p : [Pattern]
ps) =
          Binder -> ScopedTerm m -> Term m
forall {n :: S}. Binder -> ScopedTerm n -> Term n
MatchArm (Pattern -> Binder
toBinder Pattern
p)
            (Scope m
-> Pattern
-> Env m
-> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l)
-> ScopedTerm m
forall (n :: S).
Distinct n =>
Scope n
-> Pattern
-> Env n
-> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l)
-> ScopedTerm n
toScopedPatternWith Scope m
sc Pattern
p Env m
en (\Scope l
sc' Env l
en' -> Scope l -> Env l -> [Pattern] -> Term l
forall (m :: S).
Distinct m =>
Scope m -> Env m -> [Pattern] -> Term m
arms Scope l
sc' Env l
en' [Pattern]
ps))

-- * Open terms

-- | Elaborate a surface term whose free identifiers are not known in advance.
--
-- Each identifier occurring anywhere in the term gets a name in a fresh scope, so
-- an /open/ term (the annotation of a binder, say, taken out of its context) can be
-- put into the core, transformed, and printed back with the names it came in with.
-- The reference index needs this: it splits the annotation of a pair binder through
-- the core, and has no typing context to hand.
withOpenTerm
  :: forall r. Rzk.Term
  -> (forall n. Distinct n
        => Foil.Scope n -> NameMap n Display -> Term n -> r)
  -> r
withOpenTerm :: forall r.
Term
-> (forall (n :: S).
    Distinct n =>
    Scope n -> NameMap n Display -> Term n -> r)
-> r
withOpenTerm Term
term forall (n :: S).
Distinct n =>
Scope n -> NameMap n Display -> Term n -> r
k = Scope 'VoidS
-> [(VarIdent, Name 'VoidS)]
-> Map VarIdent Display
-> [VarIdent]
-> r
forall (n :: S).
Distinct n =>
Scope n
-> [(VarIdent, Name n)] -> Map VarIdent Display -> [VarIdent] -> r
go Scope 'VoidS
Foil.emptyScope [] Map VarIdent Display
forall k a. Map k a
Map.empty [VarIdent]
idents
  where
    idents :: [VarIdent]
idents = [VarIdent] -> [VarIdent]
forall a. Ord a => [a] -> [a]
nubOrd ((VarIdent' BNFC'Position -> VarIdent)
-> [VarIdent' BNFC'Position] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map VarIdent' BNFC'Position -> VarIdent
varIdent (Term -> [VarIdent' BNFC'Position]
forall a. Data a => a -> [VarIdent' BNFC'Position]
collectVarIdents Term
term))

    go :: forall n. Distinct n
       => Foil.Scope n -> [(VarIdent, Foil.Name n)] -> Map VarIdent Display
       -> [VarIdent] -> r
    go :: forall (n :: S).
Distinct n =>
Scope n
-> [(VarIdent, Name n)] -> Map VarIdent Display -> [VarIdent] -> r
go Scope n
scope [(VarIdent, Name n)]
bound Map VarIdent Display
names [] =
      Scope n -> NameMap n Display -> Term n -> r
forall (n :: S).
Distinct n =>
Scope n -> NameMap n Display -> Term n -> r
k Scope n
scope ([(VarIdent, Name n)] -> Map VarIdent Display -> NameMap n Display
forall {k} {l :: S} {a} {n :: S}.
Ord k =>
[(k, Name l)] -> Map k a -> NameMap n a
namesOf [(VarIdent, Name n)]
bound Map VarIdent Display
names) (Scope n -> Env n -> Term -> Term n
forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
toTerm Scope n
scope ([(VarIdent, Name n)] -> Env n
forall {a} {n :: S} {binder :: S -> S -> *} {sig :: * -> * -> *}.
(Eq a, Show a) =>
[(a, Name n)] -> a -> AST binder sig n
envOf [(VarIdent, Name n)]
bound) Term
term)
    go Scope n
scope [(VarIdent, Name n)]
bound Map VarIdent Display
names (VarIdent
x : [VarIdent]
xs) =
      Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
Foil.withFresh Scope n
scope ((forall (l :: S). DExt n l => NameBinder n l -> r) -> r)
-> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NameBinder n l
binder ->
        let scope' :: Scope l
scope' = NameBinder n l -> Scope n -> Scope l
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
Foil.extendScope NameBinder n l
binder Scope n
scope
            bound' :: [(VarIdent, Name l)]
bound' = (VarIdent
x, NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
Foil.nameOf NameBinder n l
binder) (VarIdent, Name l) -> [(VarIdent, Name l)] -> [(VarIdent, Name l)]
forall a. a -> [a] -> [a]
: [(VarIdent, Name n)] -> [(VarIdent, Name l)]
forall (n :: S) (l :: S).
DExt n l =>
[(VarIdent, Name n)] -> [(VarIdent, Name l)]
sinkBound [(VarIdent, Name n)]
bound
         in Scope l
-> [(VarIdent, Name l)] -> Map VarIdent Display -> [VarIdent] -> r
forall (n :: S).
Distinct n =>
Scope n
-> [(VarIdent, Name n)] -> Map VarIdent Display -> [VarIdent] -> r
go Scope l
scope' [(VarIdent, Name l)]
bound' (VarIdent -> Display -> Map VarIdent Display -> Map VarIdent Display
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarIdent
x (VarIdent
x, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x)) Map VarIdent Display
names) [VarIdent]
xs

    envOf :: [(a, Name n)] -> a -> AST binder sig n
envOf [(a, Name n)]
bound a
x = case a -> [(a, Name n)] -> Maybe (Name n)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
x [(a, Name n)]
bound of
      Just Name n
v  -> Name n -> AST binder sig n
forall (n :: S) (binder :: S -> S -> *) (sig :: * -> * -> *).
Name n -> AST binder sig n
Var Name n
v
      -- unreachable: every identifier occurring in the term was given a name above
      Maybe (Name n)
Nothing -> [Char] -> AST binder sig n
forall a. HasCallStack => [Char] -> a
error ([Char]
"withOpenTerm: uncollected identifier " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> a -> [Char]
forall a. Show a => a -> [Char]
show a
x)

    namesOf :: [(k, Name l)] -> Map k a -> NameMap n a
namesOf [(k, Name l)]
bound Map k a
names = IntMap a -> NameMap n a
forall (n :: S) a. IntMap a -> NameMap n a
NameMap (IntMap a -> NameMap n a) -> IntMap a -> NameMap n a
forall a b. (a -> b) -> a -> b
$ [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
      [ (Name l -> Int
forall (l :: S). Name l -> Int
Foil.nameId Name l
v, a
display)
      | (k
x, Name l
v) <- [(k, Name l)]
bound
      , Just a
display <- [k -> Map k a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
x Map k a
names]
      ]

-- | Sink an association list of binders by coercion, with no per-entry
-- rebuild ('withOpenTerm' calls this at every binder it opens).
-- 'Foil.sink1' cannot see through the pair (its element must be the
-- sunk type itself), but the sinkability argument is the same: only the
-- names mention the scope, and a name sinks by coercion.
sinkBound :: Foil.DExt n l => [(VarIdent, Foil.Name n)] -> [(VarIdent, Foil.Name l)]
sinkBound :: forall (n :: S) (l :: S).
DExt n l =>
[(VarIdent, Name n)] -> [(VarIdent, Name l)]
sinkBound = [(VarIdent, Name n)] -> [(VarIdent, Name l)]
forall a b. a -> b
unsafeCoerce

-- | Every identifier occurring in a piece of surface syntax, bound or free.
collectVarIdents :: Data a => a -> [Rzk.VarIdent]
collectVarIdents :: forall a. Data a => a -> [VarIdent' BNFC'Position]
collectVarIdents a
x =
  [VarIdent' BNFC'Position]
-> (VarIdent' BNFC'Position -> [VarIdent' BNFC'Position])
-> Maybe (VarIdent' BNFC'Position)
-> [VarIdent' BNFC'Position]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (VarIdent' BNFC'Position
-> [VarIdent' BNFC'Position] -> [VarIdent' BNFC'Position]
forall a. a -> [a] -> [a]
:[]) (a -> Maybe (VarIdent' BNFC'Position)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
x) [VarIdent' BNFC'Position]
-> [VarIdent' BNFC'Position] -> [VarIdent' BNFC'Position]
forall a. [a] -> [a] -> [a]
++ [[VarIdent' BNFC'Position]] -> [VarIdent' BNFC'Position]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((forall a. Data a => a -> [VarIdent' BNFC'Position])
-> a -> [[VarIdent' BNFC'Position]]
forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
forall u. (forall d. Data d => d -> u) -> a -> [u]
gmapQ d -> [VarIdent' BNFC'Position]
forall a. Data a => a -> [VarIdent' BNFC'Position]
collectVarIdents a
x)

nubOrd :: Ord a => [a] -> [a]
nubOrd :: forall a. Ord a => [a] -> [a]
nubOrd = Set a -> [a]
forall a. Set a -> [a]
Set.toList (Set a -> [a]) -> ([a] -> Set a) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList