{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE OverloadedStrings #-}

module Language.Rzk.VSCode.ReferenceIndex (
  Uri (..),
  Position (..),
  Range (..),
  Location (..),
  Binding (..),
  ReferenceIndex (..),
  indexModules,
  lookupAt,
  bindingSites,
  locationPath,
  fileOccurrences,
  AssumeScope (..),
  assumeScopeAt,
) where

import           Control.Applicative      ((<|>))
import qualified Data.Map.Strict          as Map
import           Data.Maybe               (listToMaybe)
import qualified Data.Text                as T

import           Language.Rzk.Foil.Convert (withOpenTerm)
import qualified Language.Rzk.Foil.Names   as Free
import           Language.Rzk.Foil.Print   (fromTerm)
import           Language.Rzk.Foil.Syntax  (Term, instantiateUntyped,
                                            pattern CubeProduct, pattern First,
                                            pattern Pair, pattern Second,
                                            pattern TypeSigma)
import qualified Language.Rzk.Syntax      as Rzk

data Uri = Uri
  { Uri -> [Char]
uriPath :: FilePath
  }
  deriving (Uri -> Uri -> Bool
(Uri -> Uri -> Bool) -> (Uri -> Uri -> Bool) -> Eq Uri
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Uri -> Uri -> Bool
== :: Uri -> Uri -> Bool
$c/= :: Uri -> Uri -> Bool
/= :: Uri -> Uri -> Bool
Eq, Eq Uri
Eq Uri =>
(Uri -> Uri -> Ordering)
-> (Uri -> Uri -> Bool)
-> (Uri -> Uri -> Bool)
-> (Uri -> Uri -> Bool)
-> (Uri -> Uri -> Bool)
-> (Uri -> Uri -> Uri)
-> (Uri -> Uri -> Uri)
-> Ord Uri
Uri -> Uri -> Bool
Uri -> Uri -> Ordering
Uri -> Uri -> Uri
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Uri -> Uri -> Ordering
compare :: Uri -> Uri -> Ordering
$c< :: Uri -> Uri -> Bool
< :: Uri -> Uri -> Bool
$c<= :: Uri -> Uri -> Bool
<= :: Uri -> Uri -> Bool
$c> :: Uri -> Uri -> Bool
> :: Uri -> Uri -> Bool
$c>= :: Uri -> Uri -> Bool
>= :: Uri -> Uri -> Bool
$cmax :: Uri -> Uri -> Uri
max :: Uri -> Uri -> Uri
$cmin :: Uri -> Uri -> Uri
min :: Uri -> Uri -> Uri
Ord, Int -> Uri -> ShowS
[Uri] -> ShowS
Uri -> [Char]
(Int -> Uri -> ShowS)
-> (Uri -> [Char]) -> ([Uri] -> ShowS) -> Show Uri
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Uri -> ShowS
showsPrec :: Int -> Uri -> ShowS
$cshow :: Uri -> [Char]
show :: Uri -> [Char]
$cshowList :: [Uri] -> ShowS
showList :: [Uri] -> ShowS
Show)

data Position = Position
  { Position -> Int
positionLine      :: Int
  , Position -> Int
positionCharacter :: Int
  }
  deriving (Position -> Position -> Bool
(Position -> Position -> Bool)
-> (Position -> Position -> Bool) -> Eq Position
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Position -> Position -> Bool
== :: Position -> Position -> Bool
$c/= :: Position -> Position -> Bool
/= :: Position -> Position -> Bool
Eq, Eq Position
Eq Position =>
(Position -> Position -> Ordering)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Bool)
-> (Position -> Position -> Position)
-> (Position -> Position -> Position)
-> Ord Position
Position -> Position -> Bool
Position -> Position -> Ordering
Position -> Position -> Position
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Position -> Position -> Ordering
compare :: Position -> Position -> Ordering
$c< :: Position -> Position -> Bool
< :: Position -> Position -> Bool
$c<= :: Position -> Position -> Bool
<= :: Position -> Position -> Bool
$c> :: Position -> Position -> Bool
> :: Position -> Position -> Bool
$c>= :: Position -> Position -> Bool
>= :: Position -> Position -> Bool
$cmax :: Position -> Position -> Position
max :: Position -> Position -> Position
$cmin :: Position -> Position -> Position
min :: Position -> Position -> Position
Ord, Int -> Position -> ShowS
[Position] -> ShowS
Position -> [Char]
(Int -> Position -> ShowS)
-> (Position -> [Char]) -> ([Position] -> ShowS) -> Show Position
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Position -> ShowS
showsPrec :: Int -> Position -> ShowS
$cshow :: Position -> [Char]
show :: Position -> [Char]
$cshowList :: [Position] -> ShowS
showList :: [Position] -> ShowS
Show)

data Range = Range
  { Range -> Position
rangeStart :: Position
  , Range -> Position
rangeEnd   :: Position
  }
  deriving (Range -> Range -> Bool
(Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
/= :: Range -> Range -> Bool
Eq, Eq Range
Eq Range =>
(Range -> Range -> Ordering)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Bool)
-> (Range -> Range -> Range)
-> (Range -> Range -> Range)
-> Ord Range
Range -> Range -> Bool
Range -> Range -> Ordering
Range -> Range -> Range
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Range -> Range -> Ordering
compare :: Range -> Range -> Ordering
$c< :: Range -> Range -> Bool
< :: Range -> Range -> Bool
$c<= :: Range -> Range -> Bool
<= :: Range -> Range -> Bool
$c> :: Range -> Range -> Bool
> :: Range -> Range -> Bool
$c>= :: Range -> Range -> Bool
>= :: Range -> Range -> Bool
$cmax :: Range -> Range -> Range
max :: Range -> Range -> Range
$cmin :: Range -> Range -> Range
min :: Range -> Range -> Range
Ord, Int -> Range -> ShowS
[Range] -> ShowS
Range -> [Char]
(Int -> Range -> ShowS)
-> (Range -> [Char]) -> ([Range] -> ShowS) -> Show Range
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Range -> ShowS
showsPrec :: Int -> Range -> ShowS
$cshow :: Range -> [Char]
show :: Range -> [Char]
$cshowList :: [Range] -> ShowS
showList :: [Range] -> ShowS
Show)

data Location = Location
  { Location -> Uri
locationUri   :: Uri
  , Location -> Range
locationRange :: Range
  }
  deriving (Location -> Location -> Bool
(Location -> Location -> Bool)
-> (Location -> Location -> Bool) -> Eq Location
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Location -> Location -> Bool
== :: Location -> Location -> Bool
$c/= :: Location -> Location -> Bool
/= :: Location -> Location -> Bool
Eq, Eq Location
Eq Location =>
(Location -> Location -> Ordering)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Bool)
-> (Location -> Location -> Location)
-> (Location -> Location -> Location)
-> Ord Location
Location -> Location -> Bool
Location -> Location -> Ordering
Location -> Location -> Location
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Location -> Location -> Ordering
compare :: Location -> Location -> Ordering
$c< :: Location -> Location -> Bool
< :: Location -> Location -> Bool
$c<= :: Location -> Location -> Bool
<= :: Location -> Location -> Bool
$c> :: Location -> Location -> Bool
> :: Location -> Location -> Bool
$c>= :: Location -> Location -> Bool
>= :: Location -> Location -> Bool
$cmax :: Location -> Location -> Location
max :: Location -> Location -> Location
$cmin :: Location -> Location -> Location
min :: Location -> Location -> Location
Ord, Int -> Location -> ShowS
[Location] -> ShowS
Location -> [Char]
(Int -> Location -> ShowS)
-> (Location -> [Char]) -> ([Location] -> ShowS) -> Show Location
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Location -> ShowS
showsPrec :: Int -> Location -> ShowS
$cshow :: Location -> [Char]
show :: Location -> [Char]
$cshowList :: [Location] -> ShowS
showList :: [Location] -> ShowS
Show)

data Binding = Binding
  { Binding -> Text
bindingName :: T.Text
  , Binding -> Location
bindingDef  :: Location
  , Binding -> Maybe Text
bindingType :: Maybe T.Text
    -- ^ The printed surface annotation of the binder, when it has one
    -- (e.g. @A@ for @(x : A)@, @I | φ t@ for @(t : I | φ t)@). Top-level
    -- names carry 'Nothing'; their elaborated type comes from the
    -- typecheck cache instead.
  , Binding -> [Location]
bindingRefs :: [Location]
  }
  deriving (Binding -> Binding -> Bool
(Binding -> Binding -> Bool)
-> (Binding -> Binding -> Bool) -> Eq Binding
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Binding -> Binding -> Bool
== :: Binding -> Binding -> Bool
$c/= :: Binding -> Binding -> Bool
/= :: Binding -> Binding -> Bool
Eq, Int -> Binding -> ShowS
[Binding] -> ShowS
Binding -> [Char]
(Int -> Binding -> ShowS)
-> (Binding -> [Char]) -> ([Binding] -> ShowS) -> Show Binding
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Binding -> ShowS
showsPrec :: Int -> Binding -> ShowS
$cshow :: Binding -> [Char]
show :: Binding -> [Char]
$cshowList :: [Binding] -> ShowS
showList :: [Binding] -> ShowS
Show)

data ReferenceIndex = ReferenceIndex
  { ReferenceIndex -> Map ([Char], Int) [(Int, Int, Binding)]
occurrences :: Map.Map (FilePath, Int) [(Int, Int, Binding)]
    -- ^ Every occurrence (definition or reference), keyed by file and line,
    -- as column spans; identifiers never span lines. This is what makes
    -- 'lookupAt' a map lookup rather than a scan over all bindings.
  , ReferenceIndex -> Map Location AssumeScope
assumeSites :: Map.Map Location AssumeScope
    -- ^ The definition sites of @#assume@d names, with their scope.
    -- Assumptions do not survive to the typechecked declarations (the
    -- section mechanism folds them into the definitions that use them), so
    -- the semantic token overlay recognises them here, syntactically. The
    -- scope is kept because the two kinds warrant different styling: a
    -- top-level assumption is a file-wide axiom (such as function
    -- extensionality), while one inside a section is a hypothesis the
    -- section abstracts over at its @#end@.
  }
  deriving (Int -> ReferenceIndex -> ShowS
[ReferenceIndex] -> ShowS
ReferenceIndex -> [Char]
(Int -> ReferenceIndex -> ShowS)
-> (ReferenceIndex -> [Char])
-> ([ReferenceIndex] -> ShowS)
-> Show ReferenceIndex
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ReferenceIndex -> ShowS
showsPrec :: Int -> ReferenceIndex -> ShowS
$cshow :: ReferenceIndex -> [Char]
show :: ReferenceIndex -> [Char]
$cshowList :: [ReferenceIndex] -> ShowS
showList :: [ReferenceIndex] -> ShowS
Show)

-- | Where a name was @#assume@d.
data AssumeScope
  = AssumeTopLevel   -- ^ outside any section: a file-wide axiom
  | AssumeInSection  -- ^ inside a section: a hypothesis, discharged at @#end@
  deriving (AssumeScope -> AssumeScope -> Bool
(AssumeScope -> AssumeScope -> Bool)
-> (AssumeScope -> AssumeScope -> Bool) -> Eq AssumeScope
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssumeScope -> AssumeScope -> Bool
== :: AssumeScope -> AssumeScope -> Bool
$c/= :: AssumeScope -> AssumeScope -> Bool
/= :: AssumeScope -> AssumeScope -> Bool
Eq, Int -> AssumeScope -> ShowS
[AssumeScope] -> ShowS
AssumeScope -> [Char]
(Int -> AssumeScope -> ShowS)
-> (AssumeScope -> [Char])
-> ([AssumeScope] -> ShowS)
-> Show AssumeScope
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AssumeScope -> ShowS
showsPrec :: Int -> AssumeScope -> ShowS
$cshow :: AssumeScope -> [Char]
show :: AssumeScope -> [Char]
$cshowList :: [AssumeScope] -> ShowS
showList :: [AssumeScope] -> ShowS
Show)

-- | The assume-scope of a definition site, if it is one of an @#assume@d
-- name. A local that shadows an assumption resolves to its own binder,
-- not to a site recorded here.
assumeScopeAt :: ReferenceIndex -> Location -> Maybe AssumeScope
assumeScopeAt :: ReferenceIndex -> Location -> Maybe AssumeScope
assumeScopeAt ReferenceIndex
index Location
loc = Location -> Map Location AssumeScope -> Maybe AssumeScope
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Location
loc (ReferenceIndex -> Map Location AssumeScope
assumeSites ReferenceIndex
index)

-- | One resolved occurrence: name, definition site, occurrence site, and
-- (for the self-link of a binder) its printed type annotation.
data Link = Link T.Text Location Location (Maybe T.Text)

-- | Names in scope. Locals shadow globals by insertion.
type Env = Map.Map T.Text Location

varText :: Rzk.VarIdent' a -> T.Text
varText :: forall a. VarIdent' a -> Text
varText (Rzk.VarIdent a
_ (Rzk.VarIdentToken Text
t)) = Text
t

identLoc :: FilePath -> Rzk.VarIdent -> Maybe Location
identLoc :: [Char] -> VarIdent -> Maybe Location
identLoc [Char]
file (Rzk.VarIdent BNFC'Position
pos (Rzk.VarIdentToken Text
name)) = case BNFC'Position
pos of
  Just (Int
l, Int
c) ->
    let l0 :: Int
l0 = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        c0 :: Int
c0 = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
        c1 :: Int
c1 = Int
c0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Text -> Int
T.length Text
name
    in Location -> Maybe Location
forall a. a -> Maybe a
Just (Uri -> Range -> Location
Location (Uri { uriPath :: [Char]
uriPath = [Char]
file }) (Position -> Position -> Range
Range (Int -> Int -> Position
Position Int
l0 Int
c0) (Int -> Int -> Position
Position Int
l0 Int
c1)))
  BNFC'Position
Nothing -> Maybe Location
forall a. Maybe a
Nothing

locationPath :: Location -> FilePath
locationPath :: Location -> [Char]
locationPath (Location Uri
u Range
_) = Uri -> [Char]
uriPath Uri
u

bindingSites :: Binding -> [Location]
bindingSites :: Binding -> [Location]
bindingSites Binding
b = Binding -> Location
bindingDef Binding
b Location -> [Location] -> [Location]
forall a. a -> [a] -> [a]
: Binding -> [Location]
bindingRefs Binding
b

lookupAt :: ReferenceIndex -> Uri -> Position -> Maybe Binding
lookupAt :: ReferenceIndex -> Uri -> Position -> Maybe Binding
lookupAt ReferenceIndex
index (Uri [Char]
path) (Position Int
l Int
c) =
  case ([Char], Int)
-> Map ([Char], Int) [(Int, Int, Binding)]
-> Maybe [(Int, Int, Binding)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ([Char]
path, Int
l) (ReferenceIndex -> Map ([Char], Int) [(Int, Int, Binding)]
occurrences ReferenceIndex
index) of
    Maybe [(Int, Int, Binding)]
Nothing    -> Maybe Binding
forall a. Maybe a
Nothing
    Just [(Int, Int, Binding)]
spans -> [Binding] -> Maybe Binding
forall a. [a] -> Maybe a
listToMaybe [ Binding
b | (Int
s, Int
e, Binding
b) <- [(Int, Int, Binding)]
spans, Int
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
c, Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
e ]

-- | Every occurrence recorded for a file, with the binding it resolves to:
-- 0-based line and column span. Zero-width spans (the derived def entries of
-- generated eliminators) are skipped; they occupy no characters.
fileOccurrences :: ReferenceIndex -> FilePath -> [(Binding, Int, Int, Int)]
fileOccurrences :: ReferenceIndex -> [Char] -> [(Binding, Int, Int, Int)]
fileOccurrences ReferenceIndex
index [Char]
path =
  [ (Binding
b, Int
l, Int
s, Int
e)
  | (([Char]
p, Int
l), [(Int, Int, Binding)]
spans) <- Map ([Char], Int) [(Int, Int, Binding)]
-> [(([Char], Int), [(Int, Int, Binding)])]
forall k a. Map k a -> [(k, a)]
Map.toList (ReferenceIndex -> Map ([Char], Int) [(Int, Int, Binding)]
occurrences ReferenceIndex
index)
  , [Char]
p [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
path
  , (Int
s, Int
e, Binding
b) <- [(Int, Int, Binding)]
spans
  , Int
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
s
  ]

indexModules :: [(FilePath, Rzk.Module)] -> ReferenceIndex
indexModules :: [([Char], Module)] -> ReferenceIndex
indexModules [([Char], Module)]
modules = [Link] -> ReferenceIndex
group ([Link] -> ReferenceIndex) -> [Link] -> ReferenceIndex
forall a b. (a -> b) -> a -> b
$
  [[Link]] -> [Link]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char] -> Env -> Command -> [Link]
goCommand [Char]
file Env
env0 Command
c | ([Char]
file, Module
m) <- [([Char], Module)]
modules, Command
c <- Module -> [Command]
moduleCommands Module
m ]
  where
    -- On duplicate names, the first definition wins (as scope lookup would).
    env0 :: Env
env0 = (Location -> Location -> Location) -> [(Text, Location)] -> Env
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith (\Location
_new Location
old -> Location
old)
      ([[(Text, Location)]] -> [(Text, Location)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char] -> Module -> [(Text, Location)]
globalEntries [Char]
file Module
m | ([Char]
file, Module
m) <- [([Char], Module)]
modules ])
    group :: [Link] -> ReferenceIndex
group [Link]
links = ReferenceIndex
      { occurrences :: Map ([Char], Int) [(Int, Int, Binding)]
occurrences = ([(Int, Int, Binding)]
 -> [(Int, Int, Binding)] -> [(Int, Int, Binding)])
-> [(([Char], Int), [(Int, Int, Binding)])]
-> Map ([Char], Int) [(Int, Int, Binding)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [(Int, Int, Binding)]
-> [(Int, Int, Binding)] -> [(Int, Int, Binding)]
forall a. [a] -> [a] -> [a]
(++)
          [ (([Char]
path, Int
l), [(Int
s, Int
e, Binding
b)])
          | Binding
b <- [Binding]
bs
          , Location (Uri [Char]
path) (Range (Position Int
l Int
s) (Position Int
_ Int
e)) <- Binding -> [Location]
bindingSites Binding
b
          ]
      , assumeSites :: Map Location AssumeScope
assumeSites = [(Location, AssumeScope)] -> Map Location AssumeScope
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [ (Location
loc, AssumeScope
scope)
          | ([Char]
file, Module
m) <- [([Char], Module)]
modules
          , (VarIdent
v, AssumeScope
scope) <- [Command] -> [(VarIdent, AssumeScope)]
assumesWithScope (Module -> [Command]
moduleCommands Module
m)
          , Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v]
          ]
      }
      where
        -- Binders produce a self-link (definition site linked to itself) so
        -- that every binding has a key; keep it out of the reference list,
        -- which 'bindingSites' prepends the definition to.
        -- Accumulate by prepending (constant time per link) and restore the
        -- encounter order with one reverse at the end; appending would be
        -- quadratic in the number of references of a binding.
        bs :: [Binding]
bs = [ Text -> Location -> Maybe Text -> [Location] -> Binding
Binding Text
n Location
d Maybe Text
ann ([Location] -> [Location]
forall a. [a] -> [a]
reverse [Location]
rs)
             | ((Text
n, Location
d), ([Location]
rs, Maybe Text
ann)) <- Map (Text, Location) ([Location], Maybe Text)
-> [((Text, Location), ([Location], Maybe Text))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Text, Location) ([Location], Maybe Text)
 -> [((Text, Location), ([Location], Maybe Text))])
-> Map (Text, Location) ([Location], Maybe Text)
-> [((Text, Location), ([Location], Maybe Text))]
forall a b. (a -> b) -> a -> b
$ (([Location], Maybe Text)
 -> ([Location], Maybe Text) -> ([Location], Maybe Text))
-> [((Text, Location), ([Location], Maybe Text))]
-> Map (Text, Location) ([Location], Maybe Text)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith ([Location], Maybe Text)
-> ([Location], Maybe Text) -> ([Location], Maybe Text)
forall {f :: * -> *} {a} {a}.
Alternative f =>
([a], f a) -> ([a], f a) -> ([a], f a)
merge
                 [ ((Text
n, Location
d), (if Location
r Location -> Location -> Bool
forall a. Eq a => a -> a -> Bool
== Location
d then [] else [Location
r], Maybe Text
a)) | Link Text
n Location
d Location
r Maybe Text
a <- [Link]
links ]
             ]
        -- fromListWith combines as f new old: prepend the new references,
        -- prefer the earliest annotation (the binder's self-link).
        merge :: ([a], f a) -> ([a], f a) -> ([a], f a)
merge ([a]
rsNew, f a
aNew) ([a]
rsOld, f a
aOld) = ([a]
rsNew [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
rsOld, f a
aOld f a -> f a -> f a
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> f a
aNew)

moduleCommands :: Rzk.Module -> [Rzk.Command]
moduleCommands :: Module -> [Command]
moduleCommands (Rzk.Module BNFC'Position
_ LanguageDecl' BNFC'Position
_ [Command]
cmds) = [Command]
cmds

-- | The assumed names of a module with their scope, walking the flat
-- command list with a section-depth counter.
assumesWithScope :: [Rzk.Command] -> [(Rzk.VarIdent, AssumeScope)]
assumesWithScope :: [Command] -> [(VarIdent, AssumeScope)]
assumesWithScope = Int -> [Command] -> [(VarIdent, AssumeScope)]
forall {t} {a}.
(Ord t, Num t) =>
t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go (Int
0 :: Int)
  where
    go :: t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go t
_ [] = []
    go t
depth (Command' a
c : [Command' a]
cs) = case Command' a
c of
      Rzk.CommandSection a
_ SectionName' a
_     -> t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go (t
depth t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [Command' a]
cs
      Rzk.CommandSectionEnd a
_ SectionName' a
_  -> t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go (t -> t -> t
forall a. Ord a => a -> a -> a
max t
0 (t
depth t -> t -> t
forall a. Num a => a -> a -> a
- t
1)) [Command' a]
cs
      Rzk.CommandAssume a
_ [VarIdent' a]
vars Term' a
_ ->
        let scope :: AssumeScope
scope = if t
depth t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 then AssumeScope
AssumeTopLevel else AssumeScope
AssumeInSection
        in [ (VarIdent' a
v, AssumeScope
scope) | VarIdent' a
v <- [VarIdent' a]
vars ] [(VarIdent' a, AssumeScope)]
-> [(VarIdent' a, AssumeScope)] -> [(VarIdent' a, AssumeScope)]
forall a. [a] -> [a] -> [a]
++ t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go t
depth [Command' a]
cs
      Command' a
_                          -> t -> [Command' a] -> [(VarIdent' a, AssumeScope)]
go t
depth [Command' a]
cs

-- | The top-level names a module contributes, with their definition sites.
-- A @#data@ contributes its type name and constructors, plus the /derived/
-- eliminator names @ind-D@ and @rec-D@: they have no source declaration, so
-- they point at the @#data@ name with a zero-width range — resolvable (and
-- jumped to) from their uses, but never occluding the name they sit on.
globalEntries :: FilePath -> Rzk.Module -> [(T.Text, Location)]
globalEntries :: [Char] -> Module -> [(Text, Location)]
globalEntries [Char]
file = (Command -> [(Text, Location)]) -> [Command] -> [(Text, Location)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Command -> [(Text, Location)]
cmd ([Command] -> [(Text, Location)])
-> (Module -> [Command]) -> Module -> [(Text, Location)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> [Command]
moduleCommands
  where
    plain :: VarIdent -> [(Text, Location)]
plain VarIdent
v = [ (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v, Location
loc) | Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v] ]
    derived :: Text -> VarIdent -> [(Text, Location)]
derived Text
prefix VarIdent
v =
      [ (Text
prefix Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v, Location -> Location
zeroWidth Location
loc) | Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v] ]
    zeroWidth :: Location -> Location
zeroWidth (Location Uri
u (Range Position
s Position
_)) = Uri -> Range -> Location
Location Uri
u (Position -> Position -> Range
Range Position
s Position
s)
    cmd :: Command -> [(Text, Location)]
cmd = \case
      Rzk.CommandDefine BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
_ Term
_ Term
_  -> VarIdent -> [(Text, Location)]
plain VarIdent
name
      Rzk.CommandPostulate BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
_ Term
_ -> VarIdent -> [(Text, Location)]
plain VarIdent
name
      Rzk.CommandAssume BNFC'Position
_ [VarIdent]
vars Term
_        -> (VarIdent -> [(Text, Location)])
-> [VarIdent] -> [(Text, Location)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarIdent -> [(Text, Location)]
plain [VarIdent]
vars
      Rzk.CommandData BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
_ DataSort' BNFC'Position
_ DataBody' BNFC'Position
body -> [[(Text, Location)]] -> [(Text, Location)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ VarIdent -> [(Text, Location)]
plain VarIdent
name
        , Text -> VarIdent -> [(Text, Location)]
derived Text
"ind-" VarIdent
name
        , Text -> VarIdent -> [(Text, Location)]
derived Text
"rec-" VarIdent
name
        , (VarIdent -> [(Text, Location)])
-> [VarIdent] -> [(Text, Location)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VarIdent -> [(Text, Location)]
plain (DataBody' BNFC'Position -> [VarIdent]
constructorNames DataBody' BNFC'Position
body)
        ]
      Command
_                                 -> []

constructorNames :: Rzk.DataBody -> [Rzk.VarIdent]
constructorNames :: DataBody' BNFC'Position -> [VarIdent]
constructorNames = \case
  Rzk.NoDataBody BNFC'Position
_ -> []
  Rzk.SomeDataBody BNFC'Position
_ [Constructor' BNFC'Position]
cons [DataElim' BNFC'Position]
_elims ->
    [ VarIdent
cname | Rzk.Constructor BNFC'Position
_ VarIdent
cname [Param' BNFC'Position]
_ ConstructorType' BNFC'Position
_ <- [Constructor' BNFC'Position]
cons ]

use :: FilePath -> Env -> Rzk.VarIdent -> [Link]
use :: [Char] -> Env -> VarIdent -> [Link]
use [Char]
file Env
env VarIdent
v = case (Text -> Env -> Maybe Location
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v) Env
env, [Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v) of
  (Just Location
defLoc, Just Location
occLoc) -> [Text -> Location -> Location -> Maybe Text -> Link
Link (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v) Location
defLoc Location
occLoc Maybe Text
forall a. Maybe a
Nothing]
  (Maybe Location, Maybe Location)
_                          -> []

-- | A binder annotation, kept structured so that a pair pattern can be
-- matched against the shape of its type.
data BinderAnn
  = AnnType Rzk.Term            -- ^ @(x : A)@
  | AnnShape Rzk.Term Rzk.Term  -- ^ @(t : I | φ)@

typeAnn :: Rzk.Term -> Maybe BinderAnn
typeAnn :: Term -> Maybe BinderAnn
typeAnn = BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just (BinderAnn -> Maybe BinderAnn)
-> (Term -> BinderAnn) -> Term -> Maybe BinderAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> BinderAnn
AnnType

shapeAnn :: Rzk.Term -> Rzk.Term -> Maybe BinderAnn
shapeAnn :: Term -> Term -> Maybe BinderAnn
shapeAnn Term
cube Term
tope = BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just (Term -> Term -> BinderAnn
AnnShape Term
cube Term
tope)

printAnn :: BinderAnn -> T.Text
printAnn :: BinderAnn -> Text
printAnn (AnnType Term
ty) = [Char] -> Text
T.pack (Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term
ty)
printAnn (AnnShape Term
cube Term
tope) =
  [Char] -> Text
T.pack (Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term
cube [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" | " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall a. Print a => a -> [Char]
Rzk.printTree Term
tope)

-- | Decompose the annotation of a pair pattern into annotations of the two
-- components, through the scoped core: a cube product splits into its two
-- sides, and for a Σ-type the first component gets the base while the second
-- gets the family instantiated at the first component (@q : B p@, not
-- @q : B x@). Substitution in the core is capture-avoiding. For a shape
-- annotation, the tope constrains the components jointly, so the components
-- only inherit their cube.
splitPairAnn :: Rzk.Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn)
splitPairAnn :: Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn)
splitPairAnn Term
firstComp (AnnShape Term
cube Term
_tope) = Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn)
splitPairAnn Term
firstComp (Term -> BinderAnn
AnnType Term
cube)
splitPairAnn Term
firstComp (AnnType Term
ty) =
  -- The annotation is an open term (it mentions whatever is in scope where it was
  -- written), so every identifier in it gets a name, and the names are mapped back
  -- when it is printed.
  Term
-> (forall (n :: S).
    Distinct n =>
    Scope n
    -> NameMap n Display -> Term n -> Maybe (BinderAnn, BinderAnn))
-> Maybe (BinderAnn, BinderAnn)
forall r.
Term
-> (forall (n :: S).
    Distinct n =>
    Scope n -> NameMap n Display -> Term n -> r)
-> r
withOpenTerm (BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
forall a. Maybe a
Nothing Term
ty Term
firstComp) ((forall (n :: S).
  Distinct n =>
  Scope n
  -> NameMap n Display -> Term n -> Maybe (BinderAnn, BinderAnn))
 -> Maybe (BinderAnn, BinderAnn))
-> (forall (n :: S).
    Distinct n =>
    Scope n
    -> NameMap n Display -> Term n -> Maybe (BinderAnn, BinderAnn))
-> Maybe (BinderAnn, BinderAnn)
forall a b. (a -> b) -> a -> b
$ \Scope n
scope NameMap n Display
names Term n
paired ->
    case Term n
paired of
      Pair Term n
ty' Term n
first' -> case Term n
ty' of
        CubeProduct Term n
a Term n
b -> (BinderAnn, BinderAnn) -> Maybe (BinderAnn, BinderAnn)
forall a. a -> Maybe a
Just (NameMap n Display -> Term n -> BinderAnn
forall {n :: S}. NameMap n Display -> Term n -> BinderAnn
render NameMap n Display
names Term n
a, NameMap n Display -> Term n -> BinderAnn
forall {n :: S}. NameMap n Display -> Term n -> BinderAnn
render NameMap n Display
names Term n
b)
        TypeSigma Binder
_ TModality
_ Term n
a ScopedTerm n
scoped ->
          (BinderAnn, BinderAnn) -> Maybe (BinderAnn, BinderAnn)
forall a. a -> Maybe a
Just ( NameMap n Display -> Term n -> BinderAnn
forall {n :: S}. NameMap n Display -> Term n -> BinderAnn
render NameMap n Display
names Term n
a
               , NameMap n Display -> Term n -> BinderAnn
forall {n :: S}. NameMap n Display -> Term n -> BinderAnn
render NameMap n Display
names (Term n -> Term n
forall (n :: S). Term n -> Term n
reduceProjections (Scope n -> ScopedTerm n -> Term n -> Term n
forall (n :: S).
Distinct n =>
Scope n -> ScopedTerm n -> Term n -> Term n
instantiateUntyped Scope n
scope ScopedTerm n
scoped Term n
first'))
               )
        Term n
_ -> Maybe (BinderAnn, BinderAnn)
forall a. Maybe a
Nothing
      Term n
_ -> Maybe (BinderAnn, BinderAnn)
forall a. Maybe a
Nothing
  where
    render :: NameMap n Display -> Term n -> BinderAnn
render NameMap n Display
names = Term -> BinderAnn
AnnType (Term -> BinderAnn) -> (Term n -> Term) -> Term n -> BinderAnn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [] [] NameMap n Display
names

-- | Reduce projections of literal pairs (π₁ (a, b) → a). A pattern binder refers to
-- its components through projections, so substituting a pair for it leaves these
-- redexes behind.
reduceProjections :: Term n -> Term n
reduceProjections :: forall (n :: S). Term n -> Term n
reduceProjections = \case
  First Term n
t -> case Term n -> Term n
forall (n :: S). Term n -> Term n
reduceProjections Term n
t of
    Pair Term n
a Term n
_ -> Term n
a
    Term n
t'       -> Term n -> Term n
forall (n :: S). Term n -> Term n
First Term n
t'
  Second Term n
t -> case Term n -> Term n
forall (n :: S). Term n -> Term n
reduceProjections Term n
t of
    Pair Term n
_ Term n
b -> Term n
b
    Term n
t'       -> Term n -> Term n
forall (n :: S). Term n -> Term n
Second Term n
t'
  Term n
t -> Term n
t

-- | A pattern as the term it matches.
patternTerm :: Rzk.Pattern -> Rzk.Term
patternTerm :: Pattern -> Term
patternTerm = \case
  Rzk.PatternUnit BNFC'Position
loc         -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Unit BNFC'Position
loc
  Rzk.PatternVar BNFC'Position
loc VarIdent
v        -> BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
loc VarIdent
v
  Rzk.PatternPair BNFC'Position
loc Pattern
a Pattern
b     -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
loc (Pattern -> Term
patternTerm Pattern
a) (Pattern -> Term
patternTerm Pattern
b)
  Rzk.PatternTuple BNFC'Position
loc Pattern
a Pattern
b [Pattern]
cs -> BNFC'Position -> Term -> Term -> [Term] -> Term
forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
Rzk.Tuple BNFC'Position
loc (Pattern -> Term
patternTerm Pattern
a) (Pattern -> Term
patternTerm Pattern
b) ((Pattern -> Term) -> [Pattern] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Pattern -> Term
patternTerm [Pattern]
cs)

bindVars :: FilePath -> Env -> [(Rzk.VarIdent, Maybe T.Text)] -> (Env, [Link])
bindVars :: [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env [(VarIdent, Maybe Text)]
vs =
  ( Env -> Env -> Env
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ((Location -> Location -> Location) -> [(Text, Location)] -> Env
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith (\Location
_new Location
old -> Location
old) [ (Text
n, Location
loc) | (Text
n, Location
loc, Maybe Text
_) <- [(Text, Location, Maybe Text)]
binds ]) Env
env
  , [ Text -> Location -> Location -> Maybe Text -> Link
Link Text
n Location
loc Location
loc Maybe Text
ann | (Text
n, Location
loc, Maybe Text
ann) <- [(Text, Location, Maybe Text)]
binds ]
  )
  where
    binds :: [(Text, Location, Maybe Text)]
binds = [ (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v, Location
loc, Maybe Text
ann) | (VarIdent
v, Maybe Text
ann) <- [(VarIdent, Maybe Text)]
vs, Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v] ]

bindPat :: FilePath -> Env -> Maybe BinderAnn -> Rzk.Pattern -> (Env, [Link])
bindPat :: [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env Maybe BinderAnn
ann = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env ([(VarIdent, Maybe Text)] -> (Env, [Link]))
-> (Pattern -> [(VarIdent, Maybe Text)])
-> Pattern
-> (Env, [Link])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars Maybe BinderAnn
ann

-- | Distribute an annotation over a pattern: a plain variable inherits it,
-- a pair pattern splits it along the type when the type's shape allows.
-- Tuples desugar to left-nested pairs, matching both 'Free.toTerm'''s
-- treatment of tuple patterns and its translation of Σ-tuples.
annotatedPatternVars :: Maybe BinderAnn -> Rzk.Pattern -> [(Rzk.VarIdent, Maybe T.Text)]
annotatedPatternVars :: Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars Maybe BinderAnn
ann = \case
  Rzk.PatternUnit BNFC'Position
_  -> []
  Rzk.PatternVar BNFC'Position
_ VarIdent
v -> [(VarIdent
v, BinderAnn -> Text
printAnn (BinderAnn -> Text) -> Maybe BinderAnn -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BinderAnn
ann)]
  Rzk.PatternPair BNFC'Position
_ Pattern
a Pattern
b -> case Maybe BinderAnn
ann Maybe BinderAnn
-> (BinderAnn -> Maybe (BinderAnn, BinderAnn))
-> Maybe (BinderAnn, BinderAnn)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn)
splitPairAnn (Pattern -> Term
patternTerm Pattern
a) of
    Just (BinderAnn
annA, BinderAnn
annB) ->
      Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just BinderAnn
annA) Pattern
a [(VarIdent, Maybe Text)]
-> [(VarIdent, Maybe Text)] -> [(VarIdent, Maybe Text)]
forall a. [a] -> [a] -> [a]
++ Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just BinderAnn
annB) Pattern
b
    Maybe (BinderAnn, BinderAnn)
Nothing ->
      Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars Maybe BinderAnn
forall a. Maybe a
Nothing Pattern
a [(VarIdent, Maybe Text)]
-> [(VarIdent, Maybe Text)] -> [(VarIdent, Maybe Text)]
forall a. [a] -> [a] -> [a]
++ Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars Maybe BinderAnn
forall a. Maybe a
Nothing Pattern
b
  Rzk.PatternTuple BNFC'Position
loc Pattern
a Pattern
b [Pattern]
cs ->
    -- Reuse the core's own tuple desugaring (left-nested pairs), so this
    -- split cannot drift from how toTerm' scopes tuple patterns.
    Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars Maybe BinderAnn
ann (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
Free.desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
cs) Pattern
b Pattern
a)

annotatedTermPatVars :: Maybe BinderAnn -> Rzk.Term -> [(Rzk.VarIdent, Maybe T.Text)]
annotatedTermPatVars :: Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars Maybe BinderAnn
ann = \case
  Rzk.Var BNFC'Position
_ VarIdent
v -> [(VarIdent
v, BinderAnn -> Text
printAnn (BinderAnn -> Text) -> Maybe BinderAnn -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BinderAnn
ann)]
  Rzk.Pair BNFC'Position
_ Term
a Term
b -> case Maybe BinderAnn
ann Maybe BinderAnn
-> (BinderAnn -> Maybe (BinderAnn, BinderAnn))
-> Maybe (BinderAnn, BinderAnn)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn)
splitPairAnn Term
a of
    Just (BinderAnn
annA, BinderAnn
annB) ->
      Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just BinderAnn
annA) Term
a [(VarIdent, Maybe Text)]
-> [(VarIdent, Maybe Text)] -> [(VarIdent, Maybe Text)]
forall a. [a] -> [a] -> [a]
++ Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (BinderAnn -> Maybe BinderAnn
forall a. a -> Maybe a
Just BinderAnn
annB) Term
b
    Maybe (BinderAnn, BinderAnn)
Nothing ->
      Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars Maybe BinderAnn
forall a. Maybe a
Nothing Term
a [(VarIdent, Maybe Text)]
-> [(VarIdent, Maybe Text)] -> [(VarIdent, Maybe Text)]
forall a. [a] -> [a] -> [a]
++ Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars Maybe BinderAnn
forall a. Maybe a
Nothing Term
b
  Rzk.Tuple BNFC'Position
loc Term
a Term
b [Term]
cs ->
    Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars Maybe BinderAnn
ann (BNFC'Position -> Term -> Term -> [Term] -> Term
forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
tuplePairs BNFC'Position
loc Term
a Term
b [Term]
cs)
  Term
t -> [ (VarIdent
v, Maybe Text
forall a. Maybe a
Nothing) | VarIdent
v <- Term -> [VarIdent]
termPatVars Term
t ]

-- | A tuple term as left-nested pairs, following the treatment of tuples in
-- 'Free.toTerm''.
tuplePairs :: a -> Rzk.Term' a -> Rzk.Term' a -> [Rzk.Term' a] -> Rzk.Term' a
tuplePairs :: forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
tuplePairs a
loc Term' a
t1 Term' a
t2 []       = a -> Term' a -> Term' a -> Term' a
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair a
loc Term' a
t1 Term' a
t2
tuplePairs a
loc Term' a
t1 Term' a
t2 (Term' a
t : [Term' a]
ts) = a -> Term' a -> Term' a -> [Term' a] -> Term' a
forall a. a -> Term' a -> Term' a -> [Term' a] -> Term' a
tuplePairs a
loc (a -> Term' a -> Term' a -> Term' a
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair a
loc Term' a
t1 Term' a
t2) Term' a
t [Term' a]
ts

termPatVars :: Rzk.Term -> [Rzk.VarIdent]
termPatVars :: Term -> [VarIdent]
termPatVars = \case
  Rzk.Var BNFC'Position
_ VarIdent
v        -> [VarIdent
v]
  Rzk.Pair BNFC'Position
_ Term
a Term
b     -> Term -> [VarIdent]
termPatVars Term
a [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. [a] -> [a] -> [a]
++ Term -> [VarIdent]
termPatVars Term
b
  Rzk.Tuple BNFC'Position
_ Term
a Term
b [Term]
cs -> (Term -> [VarIdent]) -> [Term] -> [VarIdent]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Term -> [VarIdent]
termPatVars (Term
a Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
b Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
cs)
  Term
_                  -> []

goCommand :: FilePath -> Env -> Rzk.Command -> [Link]
goCommand :: [Char] -> Env -> Command -> [Link]
goCommand [Char]
file Env
env = \case
  Rzk.CommandDefine BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
ps Term
ty Term
body ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
env [Param' BNFC'Position]
ps
    in VarIdent -> [Link]
def VarIdent
name [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
body
  Rzk.CommandPostulate BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
ps Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
env [Param' BNFC'Position]
ps
    in VarIdent -> [Link]
def VarIdent
name [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
ty
  -- Assumptions (#assume, #variable, #variables) carry their declared type
  -- as the annotation; unlike #define, nothing is elaborated away.
  Rzk.CommandAssume BNFC'Position
_ [VarIdent]
vars Term
ty ->
    [ Text -> Location -> Location -> Maybe Text -> Link
Link (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v) Location
loc Location
loc (Text -> Maybe Text
forall a. a -> Maybe a
Just (BinderAnn -> Text
printAnn (Term -> BinderAnn
AnnType Term
ty)))
    | VarIdent
v <- [VarIdent]
vars, Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v] ]
      [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty
  -- A #data declares the type, its constructors, and (implicitly) the
  -- generated eliminators; the type name is in scope in the sort and in
  -- the constructor types (for return types, and for recursion later).
  Rzk.CommandData BNFC'Position
_ VarIdent
name DeclUsedVars' BNFC'Position
_ [Param' BNFC'Position]
ps DataSort' BNFC'Position
sort DataBody' BNFC'Position
body ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
env [Param' BNFC'Position]
ps
        envD :: Env
envD = case [Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
name of
          Just Location
loc -> Text -> Location -> Env -> Env
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
name) Location
loc Env
env'
          Maybe Location
Nothing  -> Env
env'
        goSort :: [Link]
goSort = case DataSort' BNFC'Position
sort of
          Rzk.SomeDataSort BNFC'Position
_ Term
ty -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
envD Term
ty
          Rzk.NoDataSort BNFC'Position
_      -> []
        goBody :: [Link]
goBody = case DataBody' BNFC'Position
body of
          Rzk.SomeDataBody BNFC'Position
_ [Constructor' BNFC'Position]
cons [DataElim' BNFC'Position]
elims -> [[Link]] -> [Link]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            [ (Constructor' BNFC'Position -> [Link])
-> [Constructor' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Constructor' BNFC'Position -> [Link]
goCon [Constructor' BNFC'Position]
cons
            , (DataElim' BNFC'Position -> [Link])
-> [DataElim' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
                (\case
                  Rzk.DataElim BNFC'Position
_ VarIdent
_elim Term
ty    -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
envD Term
ty
                  Rzk.DataCompute BNFC'Position
_ VarIdent
_rule Term
ty -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
envD Term
ty)
                [DataElim' BNFC'Position]
elims
            ]
          Rzk.NoDataBody BNFC'Position
_ -> []
        goCon :: Constructor' BNFC'Position -> [Link]
goCon (Rzk.Constructor BNFC'Position
_ VarIdent
cname [Param' BNFC'Position]
cps ConstructorType' BNFC'Position
cty) =
          let (Env
env'', [Link]
coccs) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
envD [Param' BNFC'Position]
cps
          in VarIdent -> [Link]
def VarIdent
cname [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
coccs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ case ConstructorType' BNFC'Position
cty of
               Rzk.SomeConstructorType BNFC'Position
_ Term
ty -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env'' Term
ty
               Rzk.NoConstructorType BNFC'Position
_      -> []
    in VarIdent -> [Link]
def VarIdent
name [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
goSort [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
goBody
  Rzk.CommandCheck BNFC'Position
_ Term
a Term
b       -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.CommandCompute BNFC'Position
_ Term
a       -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.CommandComputeWHNF BNFC'Position
_ Term
a   -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.CommandComputeNF BNFC'Position
_ Term
a     -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.CommandSetOption{}       -> []
  Rzk.CommandUnsetOption{}     -> []
  Rzk.CommandSection{}         -> []
  Rzk.CommandSectionEnd{}      -> []
  where
    def :: VarIdent -> [Link]
def VarIdent
v = [ Text -> Location -> Location -> Maybe Text -> Link
Link (VarIdent -> Text
forall a. VarIdent' a -> Text
varText VarIdent
v) Location
loc Location
loc Maybe Text
forall a. Maybe a
Nothing | Just Location
loc <- [[Char] -> VarIdent -> Maybe Location
identLoc [Char]
file VarIdent
v] ]

goTerm :: FilePath -> Env -> Rzk.Term -> [Link]
goTerm :: [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env = \case
  Rzk.Var BNFC'Position
_ VarIdent
v  -> [Char] -> Env -> VarIdent -> [Link]
use [Char]
file Env
env VarIdent
v
  Rzk.Hole BNFC'Position
_ HoleIdent' BNFC'Position
_ -> []

  Rzk.Lambda BNFC'Position
_ [Param' BNFC'Position]
ps Term
body                      -> [Char] -> Env -> [Param' BNFC'Position] -> Term -> [Link]
paramScope [Char]
file Env
env [Param' BNFC'Position]
ps Term
body
  Rzk.ASCII_Lambda BNFC'Position
_ [Param' BNFC'Position]
ps Term
body                -> [Char] -> Env -> [Param' BNFC'Position] -> Term -> [Link]
paramScope [Char]
file Env
env [Param' BNFC'Position]
ps Term
body
  Rzk.Let BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
body                   -> [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetModBind BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
body              -> [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetMod BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
body           -> [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetModFramed BNFC'Position
_ Modality' BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
body        -> [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetModBindInto BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
motive Term
body   -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
motive [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetModInto BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
motive Term
body -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
motive [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.LetModFramedInto BNFC'Position
_ Modality' BNFC'Position
_ Modality' BNFC'Position
_ Bind' BNFC'Position
bind Term
val Term
motive Term
body -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
motive [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body
  Rzk.TypeSigma BNFC'Position
_ Pattern
pat Term
ty Term
ret                -> [Char] -> Env -> Pattern -> Term -> Term -> [Link]
sigmaScope [Char]
file Env
env Pattern
pat Term
ty Term
ret
  Rzk.ASCII_TypeSigma BNFC'Position
_ Pattern
pat Term
ty Term
ret          -> [Char] -> Env -> Pattern -> Term -> Term -> [Link]
sigmaScope [Char]
file Env
env Pattern
pat Term
ty Term
ret
  Rzk.TypeSigmaModal BNFC'Position
_ Pattern
pat ModalColon' BNFC'Position
_ Term
ty Term
ret         -> [Char] -> Env -> Pattern -> Term -> Term -> [Link]
sigmaScope [Char]
file Env
env Pattern
pat Term
ty Term
ret
  Rzk.TypeSigmaTuple BNFC'Position
_ SigmaParam' BNFC'Position
sp [SigmaParam' BNFC'Position]
sps Term
ret           -> [Char] -> Env -> [SigmaParam' BNFC'Position] -> Term -> [Link]
sigmaTupleScope [Char]
file Env
env (SigmaParam' BNFC'Position
sp SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position] -> [SigmaParam' BNFC'Position]
forall a. a -> [a] -> [a]
: [SigmaParam' BNFC'Position]
sps) Term
ret
  Rzk.ASCII_TypeSigmaTuple BNFC'Position
_ SigmaParam' BNFC'Position
sp [SigmaParam' BNFC'Position]
sps Term
ret     -> [Char] -> Env -> [SigmaParam' BNFC'Position] -> Term -> [Link]
sigmaTupleScope [Char]
file Env
env (SigmaParam' BNFC'Position
sp SigmaParam' BNFC'Position
-> [SigmaParam' BNFC'Position] -> [SigmaParam' BNFC'Position]
forall a. a -> [a] -> [a]
: [SigmaParam' BNFC'Position]
sps) Term
ret
  Rzk.TypeFun BNFC'Position
_ ParamDecl' BNFC'Position
pd Term
ret                      -> [Char] -> Env -> ParamDecl' BNFC'Position -> Term -> [Link]
paramDeclScope [Char]
file Env
env ParamDecl' BNFC'Position
pd Term
ret
  Rzk.ASCII_TypeFun BNFC'Position
_ ParamDecl' BNFC'Position
pd Term
ret                -> [Char] -> Env -> ParamDecl' BNFC'Position -> Term -> [Link]
paramDeclScope [Char]
file Env
env ParamDecl' BNFC'Position
pd Term
ret

  Rzk.CubeProduct BNFC'Position
_ Term
a Term
b         -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.CubeSup BNFC'Position
_ Term
a Term
b             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.CubeInf BNFC'Position
_ Term
a Term
b             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TopeEQ BNFC'Position
_ Term
a Term
b              -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TopeLEQ BNFC'Position
_ Term
a Term
b             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TopeAnd BNFC'Position
_ Term
a Term
b             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TopeOr BNFC'Position
_ Term
a Term
b              -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.ASCII_TopeEQ BNFC'Position
_ Term
a Term
b        -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.ASCII_TopeLEQ BNFC'Position
_ Term
a Term
b       -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.ASCII_TopeAnd BNFC'Position
_ Term
a Term
b       -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.ASCII_TopeOr BNFC'Position
_ Term
a Term
b        -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TopeInv BNFC'Position
_ Term
a               -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.TopeUninv BNFC'Position
_ Term
a             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.CubeFlip BNFC'Position
_ Term
a              -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.CubeUnflip BNFC'Position
_ Term
a            -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.RecOr BNFC'Position
_ [Restriction' BNFC'Position]
rs                -> (Restriction' BNFC'Position -> [Link])
-> [Restriction' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> Restriction' BNFC'Position -> [Link]
restriction [Char]
file Env
env) [Restriction' BNFC'Position]
rs
  Rzk.TypeId BNFC'Position
_ Term
a Term
b Term
c            -> (Term -> [Link]) -> [Term] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env) [Term
a, Term
b, Term
c]
  Rzk.TypeIdSimple BNFC'Position
_ Term
a Term
b        -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.TypeRestricted BNFC'Position
_ Term
a [Restriction' BNFC'Position]
rs     -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ (Restriction' BNFC'Position -> [Link])
-> [Restriction' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> Restriction' BNFC'Position -> [Link]
restriction [Char]
file Env
env) [Restriction' BNFC'Position]
rs
  Rzk.App BNFC'Position
_ Term
a Term
b                 -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.Pair BNFC'Position
_ Term
a Term
b                -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.Tuple BNFC'Position
_ Term
a Term
b [Term]
cs            -> (Term -> [Link]) -> [Term] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env) (Term
a Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
b Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
cs)
  Rzk.ModApp BNFC'Position
_ Modality' BNFC'Position
_ Term
a              -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ModType BNFC'Position
_ Modality' BNFC'Position
_ Term
a             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ModExtract BNFC'Position
_ ModComp' BNFC'Position
_ Term
a          -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.First BNFC'Position
_ Term
a                 -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.Second BNFC'Position
_ Term
a                -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ASCII_First BNFC'Position
_ Term
a           -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ASCII_Second BNFC'Position
_ Term
a          -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ReflTerm BNFC'Position
_ Term
a              -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a
  Rzk.ReflTermType BNFC'Position
_ Term
a Term
b        -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.IdJ BNFC'Position
_ Term
a Term
b Term
c Term
d Term
e Term
f         -> (Term -> [Link]) -> [Term] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env) [Term
a, Term
b, Term
c, Term
d, Term
e, Term
f]
  Rzk.Match BNFC'Position
_ Term
scrut [MatchBranch' BNFC'Position]
bs          -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
scrut [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ (MatchBranch' BNFC'Position -> [Link])
-> [MatchBranch' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> MatchBranch' BNFC'Position -> [Link]
matchBranchScope [Char]
file Env
env) [MatchBranch' BNFC'Position]
bs
  Rzk.MatchInto BNFC'Position
_ Term
scrut Term
motive [MatchBranch' BNFC'Position]
bs ->
    [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
scrut [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
motive [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ (MatchBranch' BNFC'Position -> [Link])
-> [MatchBranch' BNFC'Position] -> [Link]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Char] -> Env -> MatchBranch' BNFC'Position -> [Link]
matchBranchScope [Char]
file Env
env) [MatchBranch' BNFC'Position]
bs
  Rzk.TypeAsc BNFC'Position
_ Term
a Term
b             -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b

  Rzk.Universe{}           -> []
  Rzk.UniverseCube{}       -> []
  Rzk.UniverseTope{}       -> []
  Rzk.CubeUnit{}           -> []
  Rzk.CubeUnitStar{}       -> []
  Rzk.Cube2{}              -> []
  Rzk.Cube2_0{}            -> []
  Rzk.Cube2_1{}            -> []
  Rzk.CubeI{}              -> []
  Rzk.CubeI_0{}            -> []
  Rzk.CubeI_1{}            -> []
  Rzk.TopeTop{}            -> []
  Rzk.TopeBottom{}         -> []
  Rzk.RecBottom{}          -> []
  Rzk.TypeUnit{}           -> []
  Rzk.Unit{}               -> []
  Rzk.Refl{}               -> []
  Rzk.ASCII_CubeUnitStar{} -> []
  Rzk.ASCII_Cube2_0{}      -> []
  Rzk.ASCII_Cube2_1{}      -> []
  Rzk.ASCII_CubeI{}        -> []
  Rzk.ASCII_CubeI_0{}      -> []
  Rzk.ASCII_CubeI_1{}      -> []
  Rzk.ASCII_TopeTop{}      -> []
  Rzk.ASCII_TopeBottom{}   -> []

paramScope :: FilePath -> Env -> [Rzk.Param] -> Rzk.Term -> [Link]
paramScope :: [Char] -> Env -> [Param' BNFC'Position] -> Term -> [Link]
paramScope [Char]
file Env
env [Param' BNFC'Position]
ps Term
body =
  let (Env
env', [Link]
occs) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
env [Param' BNFC'Position]
ps in [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
body

letScope :: FilePath -> Env -> Rzk.Bind -> Rzk.Term -> Rzk.Term -> [Link]
letScope :: [Char] -> Env -> Bind' BNFC'Position -> Term -> Term -> [Link]
letScope [Char]
file Env
env Bind' BNFC'Position
bind Term
val Term
body =
  let (Env
env', [Link]
occs) = [Char] -> Env -> Bind' BNFC'Position -> (Env, [Link])
goBind [Char]
file Env
env Bind' BNFC'Position
bind
  in [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
val [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
body

sigmaScope :: FilePath -> Env -> Rzk.Pattern -> Rzk.Term -> Rzk.Term -> [Link]
sigmaScope :: [Char] -> Env -> Pattern -> Term -> Term -> [Link]
sigmaScope [Char]
file Env
env Pattern
pat Term
ty Term
ret =
  let (Env
env', [Link]
occs) = [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env (Term -> Maybe BinderAnn
typeAnn Term
ty) Pattern
pat
  in [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
ret

sigmaTupleScope :: FilePath -> Env -> [Rzk.SigmaParam] -> Rzk.Term -> [Link]
sigmaTupleScope :: [Char] -> Env -> [SigmaParam' BNFC'Position] -> Term -> [Link]
sigmaTupleScope [Char]
file Env
env [SigmaParam' BNFC'Position]
sps Term
ret =
  let (Env
env', [Link]
occs) = [Char] -> Env -> [SigmaParam' BNFC'Position] -> (Env, [Link])
goSigmaParams [Char]
file Env
env [SigmaParam' BNFC'Position]
sps in [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
ret

paramDeclScope :: FilePath -> Env -> Rzk.ParamDecl -> Rzk.Term -> [Link]
paramDeclScope :: [Char] -> Env -> ParamDecl' BNFC'Position -> Term -> [Link]
paramDeclScope [Char]
file Env
env ParamDecl' BNFC'Position
pd Term
ret =
  let (Env
env', [Link]
occs) = [Char] -> Env -> ParamDecl' BNFC'Position -> (Env, [Link])
goParamDecl [Char]
file Env
env ParamDecl' BNFC'Position
pd in [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
ret

restriction :: FilePath -> Env -> Rzk.Restriction -> [Link]
restriction :: [Char] -> Env -> Restriction' BNFC'Position -> [Link]
restriction [Char]
file Env
env = \case
  Rzk.Restriction BNFC'Position
_ Term
a Term
b       -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b
  Rzk.ASCII_Restriction BNFC'Position
_ Term
a Term
b -> [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
a [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
b

-- | A match branch: the constructor name is a use (linked to the constructor's
-- declaration), and the binder patterns scope over the branch body.
matchBranchScope :: FilePath -> Env -> Rzk.MatchBranch -> [Link]
matchBranchScope :: [Char] -> Env -> MatchBranch' BNFC'Position -> [Link]
matchBranchScope [Char]
file Env
env (Rzk.MatchBranch BNFC'Position
_ VarIdent
con [Pattern]
pats Term
body) =
  [Char] -> Env -> VarIdent -> [Link]
use [Char]
file Env
env VarIdent
con [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ Env -> [Pattern] -> [Link]
goPats Env
env [Pattern]
pats
  where
    goPats :: Env -> [Pattern] -> [Link]
goPats Env
env' []       = [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
body
    goPats Env
env' (Pattern
p : [Pattern]
ps) =
      let (Env
env'', [Link]
occs) = [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env' Maybe BinderAnn
forall a. Maybe a
Nothing Pattern
p
       in [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ Env -> [Pattern] -> [Link]
goPats Env
env'' [Pattern]
ps

goBind :: FilePath -> Env -> Rzk.Bind -> (Env, [Link])
goBind :: [Char] -> Env -> Bind' BNFC'Position -> (Env, [Link])
goBind [Char]
file Env
env = \case
  Rzk.BindPattern BNFC'Position
_ Pattern
pat -> [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env Maybe BinderAnn
forall a. Maybe a
Nothing Pattern
pat
  Rzk.BindPatternType BNFC'Position
_ Pattern
pat Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env (Term -> Maybe BinderAnn
typeAnn Term
ty) Pattern
pat in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)

goParams :: FilePath -> Env -> [Rzk.Param] -> (Env, [Link])
goParams :: [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
_    Env
env []       = (Env
env, [])
goParams [Char]
file Env
env (Param' BNFC'Position
p : [Param' BNFC'Position]
ps) =
  let (Env
env1, [Link]
o1) = [Char] -> Env -> Param' BNFC'Position -> (Env, [Link])
goParam [Char]
file Env
env Param' BNFC'Position
p
      (Env
env2, [Link]
o2) = [Char] -> Env -> [Param' BNFC'Position] -> (Env, [Link])
goParams [Char]
file Env
env1 [Param' BNFC'Position]
ps
  in (Env
env2, [Link]
o1 [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
o2)

goParam :: FilePath -> Env -> Rzk.Param -> (Env, [Link])
goParam :: [Char] -> Env -> Param' BNFC'Position -> (Env, [Link])
goParam [Char]
file Env
env = \case
  Rzk.ParamPattern BNFC'Position
_ Pattern
pat -> [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env Maybe BinderAnn
forall a. Maybe a
Nothing Pattern
pat
  Rzk.ParamPatternType BNFC'Position
_ [Pattern]
pats Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env ((Pattern -> [(VarIdent, Maybe Text)])
-> [Pattern] -> [(VarIdent, Maybe Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (Term -> Maybe BinderAnn
typeAnn Term
ty)) [Pattern]
pats)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)
  Rzk.ParamPatternShape BNFC'Position
_ [Pattern]
pats Term
cube Term
tope ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env ((Pattern -> [(VarIdent, Maybe Text)])
-> [Pattern] -> [(VarIdent, Maybe Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (Term -> Term -> Maybe BinderAnn
shapeAnn Term
cube Term
tope)) [Pattern]
pats)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
cube [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
tope)
  Rzk.ParamPatternModalType BNFC'Position
_ [Pattern]
pats ModalColon' BNFC'Position
_ Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env ((Pattern -> [(VarIdent, Maybe Text)])
-> [Pattern] -> [(VarIdent, Maybe Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (Term -> Maybe BinderAnn
typeAnn Term
ty)) [Pattern]
pats)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)
  Rzk.ParamPatternModalShape BNFC'Position
_ [Pattern]
pats ModalColon' BNFC'Position
_ Term
cube Term
tope ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env ((Pattern -> [(VarIdent, Maybe Text)])
-> [Pattern] -> [(VarIdent, Maybe Text)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Maybe BinderAnn -> Pattern -> [(VarIdent, Maybe Text)]
annotatedPatternVars (Term -> Term -> Maybe BinderAnn
shapeAnn Term
cube Term
tope)) [Pattern]
pats)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
cube [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
tope)

goParamDecl :: FilePath -> Env -> Rzk.ParamDecl -> (Env, [Link])
goParamDecl :: [Char] -> Env -> ParamDecl' BNFC'Position -> (Env, [Link])
goParamDecl [Char]
file Env
env = \case
  Rzk.ParamType BNFC'Position
_ Term
ty -> (Env
env, [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty)
  Rzk.ParamTermType BNFC'Position
_ Term
patTerm Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env (Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (Term -> Maybe BinderAnn
typeAnn Term
ty) Term
patTerm)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)
  Rzk.ParamTermShape BNFC'Position
_ Term
patTerm Term
cube Term
tope ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env (Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (Term -> Term -> Maybe BinderAnn
shapeAnn Term
cube Term
tope) Term
patTerm)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
cube [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
tope)
  Rzk.ParamTermModalType BNFC'Position
_ Term
patTerm ModalColon' BNFC'Position
_ Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env (Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (Term -> Maybe BinderAnn
typeAnn Term
ty) Term
patTerm)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)
  Rzk.ParamTermModalShape BNFC'Position
_ Term
patTerm ModalColon' BNFC'Position
_ Term
cube Term
tope ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> [(VarIdent, Maybe Text)] -> (Env, [Link])
bindVars [Char]
file Env
env (Maybe BinderAnn -> Term -> [(VarIdent, Maybe Text)]
annotatedTermPatVars (Term -> Term -> Maybe BinderAnn
shapeAnn Term
cube Term
tope) Term
patTerm)
    in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
cube [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env' Term
tope)

goSigmaParams :: FilePath -> Env -> [Rzk.SigmaParam] -> (Env, [Link])
goSigmaParams :: [Char] -> Env -> [SigmaParam' BNFC'Position] -> (Env, [Link])
goSigmaParams [Char]
_    Env
env []       = (Env
env, [])
goSigmaParams [Char]
file Env
env (SigmaParam' BNFC'Position
p : [SigmaParam' BNFC'Position]
ps) =
  let (Env
env1, [Link]
o1) = [Char] -> Env -> SigmaParam' BNFC'Position -> (Env, [Link])
goSigmaParam [Char]
file Env
env SigmaParam' BNFC'Position
p
      (Env
env2, [Link]
o2) = [Char] -> Env -> [SigmaParam' BNFC'Position] -> (Env, [Link])
goSigmaParams [Char]
file Env
env1 [SigmaParam' BNFC'Position]
ps
  in (Env
env2, [Link]
o1 [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
o2)

goSigmaParam :: FilePath -> Env -> Rzk.SigmaParam -> (Env, [Link])
goSigmaParam :: [Char] -> Env -> SigmaParam' BNFC'Position -> (Env, [Link])
goSigmaParam [Char]
file Env
env = \case
  Rzk.SigmaParam BNFC'Position
_ Pattern
pat Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env (Term -> Maybe BinderAnn
typeAnn Term
ty) Pattern
pat in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)
  Rzk.SigmaParamModal BNFC'Position
_ Pattern
pat ModalColon' BNFC'Position
_ Term
ty ->
    let (Env
env', [Link]
occs) = [Char] -> Env -> Maybe BinderAnn -> Pattern -> (Env, [Link])
bindPat [Char]
file Env
env (Term -> Maybe BinderAnn
typeAnn Term
ty) Pattern
pat in (Env
env', [Char] -> Env -> Term -> [Link]
goTerm [Char]
file Env
env Term
ty [Link] -> [Link] -> [Link]
forall a. [a] -> [a] -> [a]
++ [Link]
occs)