{-# LANGUAGE OverloadedStrings #-}

-- | Showing a term to the user.
--
-- A term of the core names its variables by 'Foil.Name' (an @Int@), so anything
-- user-facing — an error, a trace of a judgement, a hole's goal — has to say what
-- each name is /called/. That is a 'Naming': a display name and a display binder
-- per name in scope, plus the supply of fresh names for the binders the printer
-- meets on the way down.
--
-- This replaces the old @var -> VarIdent@ threading (@name@, @nameInc@,
-- @BinderNames@, @ppTermInContext@ — four copies of the same idea), and with it
-- the unwinding loop that rebuilt those names one binder at a time.
module Rzk.TypeCheck.Display where

import           Control.Monad.Foil          (NameMap)
import qualified Control.Monad.Foil          as Foil
import           Control.Monad.Foil.Internal (NameMap (..))
import qualified Data.IntMap                 as IntMap
import           Data.List                   (nub, (\\))
import qualified Data.Set                    as Set

import           Language.Rzk.Foil.Print     (fromTerm)
import           Language.Rzk.Foil.Syntax
import           Language.Rzk.Foil.Names    (Binder (..), Display,
                                              TypeInfo (..), VarIdent,
                                              binderIsCompound, binderLeaves,
                                              binderDisplayName, binderToPattern, defaultVarIdents,
                                              freshenBinderLeaves, fromVarIdent,
                                              refreshVarIn)
import qualified Language.Rzk.Syntax         as Rzk
import           Rzk.TypeCheck.Context

-- | What every name in scope is called, and what the printer may call the
-- binders it has yet to meet.
data Naming n = Naming
  { forall (n :: S). Naming n -> NameMap n Display
namingOf     :: NameMap n Display
  , forall (n :: S). Naming n -> [VarIdent]
namingUsed   :: [VarIdent]
    -- ^ the display names taken, so a bound binder is refreshed away from them
  , forall (n :: S). Naming n -> [VarIdent]
namingSupply :: [VarIdent]
    -- ^ the names left over, for anonymous binders
  }

-- | Read the naming off a context.
--
-- A named binder keeps its name, refreshed only if an outer name has already
-- taken it. An anonymous one draws from the supply. A pattern binder has its
-- component names freshened as a group, so that the pattern shown in the context
-- and the projections folded inside a term agree on them.
--
-- Entries are named oldest binding first (see 'ctxBound'), so an outer binder
-- keeps its name and an inner one is the one refreshed away from it.
namingOfContext :: Context n -> Naming n
namingOfContext :: forall (n :: S). Context n -> Naming n
namingOfContext Context n
ctx = Naming
  { namingOf :: NameMap n Display
namingOf = IntMap Display -> NameMap n Display
forall (n :: S) a. IntMap a -> NameMap n a
NameMap ([(Key, Display)] -> IntMap Display
forall a. [(Key, a)] -> IntMap a
IntMap.fromList [(Key, Display)]
entries)
  , namingUsed :: [VarIdent]
namingUsed = [VarIdent]
used
  , namingSupply :: [VarIdent]
namingSupply = [VarIdent]
defaultVarIdents [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [VarIdent]
used
  }
  where
    ([(Key, Display)]
entries, Set VarIdent
usedSet) = Set VarIdent
-> [VarIdent]
-> [(Name n, VarInfo n)]
-> ([(Key, Display)], Set VarIdent)
forall {l :: S} {n :: S}.
Set VarIdent
-> [VarIdent]
-> [(Name l, VarInfo n)]
-> ([(Key, Display)], Set VarIdent)
go Set VarIdent
forall a. Set a
Set.empty [VarIdent]
defaultVarIdents (Context n -> [(Name n, VarInfo n)]
forall (n :: S). Context n -> [(Name n, VarInfo n)]
varsInScope Context n
ctx)
    used :: [VarIdent]
used = Set VarIdent -> [VarIdent]
forall a. Set a -> [a]
Set.toList Set VarIdent
usedSet

    -- Name the entries in binding order, each avoiding the names already taken.
    -- The taken names are a set: this runs once per entry, and a context can hold
    -- every top-level definition of a project.
    go :: Set VarIdent
-> [VarIdent]
-> [(Name l, VarInfo n)]
-> ([(Key, Display)], Set VarIdent)
go Set VarIdent
taken [VarIdent]
_supply [] = ([], Set VarIdent
taken)
    go Set VarIdent
taken [VarIdent]
supply ((Name l
v, VarInfo n
info) : [(Name l, VarInfo n)]
rest) =
      case VarInfo n -> Binder
forall (n :: S). VarInfo n -> Binder
varOrig VarInfo n
info of
        BinderVar (Just VarIdent
x) ->
          let x' :: VarIdent
x' = Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
taken VarIdent
x
           in Display
-> [VarIdent] -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
forall {t :: * -> *}.
Foldable t =>
Display
-> t VarIdent -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
name (VarIdent
x', Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x')) [VarIdent
x'] [VarIdent]
supply
        BinderVar Maybe VarIdent
Nothing ->
          case [VarIdent]
supply of
            VarIdent
x : [VarIdent]
supply' -> Display
-> [VarIdent] -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
forall {t :: * -> *}.
Foldable t =>
Display
-> t VarIdent -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
name (VarIdent
x, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x)) [VarIdent
x] [VarIdent]
supply'
            []          -> String -> ([(Key, Display)], Set VarIdent)
forall a. String -> a
panicImpossible String
"not enough fresh variables"
        Binder
binder ->
          -- A pattern binder: the variable itself needs a placeholder name only
          -- when the whole point is used, and then it prints as the pattern —
          -- so the placeholder is the pattern's own display name ("(na, nb)"),
          -- which the identifier lexer can never produce. It must not draw
          -- from the default supply: claiming x₁ here would displace a later
          -- user-written x₁ in the display (and its hole moves) while the
          -- source keeps the name. Only the leaves are freshened and claimed.
          let binder' :: Binder
binder' = [VarIdent] -> Binder -> Binder
freshenBinderLeaves (Set VarIdent -> [VarIdent]
forall a. Set a -> [a]
Set.toList Set VarIdent
taken) Binder
binder
           in Display
-> [VarIdent] -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
forall {t :: * -> *}.
Foldable t =>
Display
-> t VarIdent -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
name (Binder -> VarIdent
binderDisplayName Binder
binder', Binder
binder') (Binder -> [VarIdent]
binderLeaves Binder
binder') [VarIdent]
supply
      where
        name :: Display
-> t VarIdent -> [VarIdent] -> ([(Key, Display)], Set VarIdent)
name Display
display t VarIdent
claimed [VarIdent]
supply' =
          let ([(Key, Display)]
acc, Set VarIdent
taken') = Set VarIdent
-> [VarIdent]
-> [(Name l, VarInfo n)]
-> ([(Key, Display)], Set VarIdent)
go ((VarIdent -> Set VarIdent -> Set VarIdent)
-> Set VarIdent -> t VarIdent -> Set VarIdent
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr VarIdent -> Set VarIdent -> Set VarIdent
forall a. Ord a => a -> Set a -> Set a
Set.insert Set VarIdent
taken t VarIdent
claimed) [VarIdent]
supply' [(Name l, VarInfo n)]
rest
           in ((Name l -> Key
forall (l :: S). Name l -> Key
Foil.nameId Name l
v, Display
display) (Key, Display) -> [(Key, Display)] -> [(Key, Display)]
forall a. a -> [a] -> [a]
: [(Key, Display)]
acc, Set VarIdent
taken')

-- | A term already rendered for the user, kept as surface syntax rather than a
-- string so that a consumer may still inspect it.
--
-- Its 'Show' prints the surface syntax, which is what the old @Term'@ did, so a
-- rendered goal or candidate reads the same as it always has (@\\ (t, s) → ?@).
newtype Rendered = Rendered { Rendered -> Term
getRendered :: Rzk.Term }

instance Show Rendered where
  show :: Rendered -> String
show = Term -> String
forall a. Print a => a -> String
Rzk.printTree (Term -> String) -> (Rendered -> Term) -> Rendered -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rendered -> Term
getRendered

-- | Two rendered terms are equal when they read the same. (The surface AST
-- carries source positions, which a rendered term should not be judged by.)
instance Eq Rendered where
  Rendered
l == :: Rendered -> Rendered -> Bool
== Rendered
r = Rendered -> String
forall a. Show a => a -> String
show Rendered
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Rendered -> String
forall a. Show a => a -> String
show Rendered
r

-- | A term as surface syntax, with the context's names.
--
-- A binder /inside/ the term is freshened only against the names the term itself
-- mentions — not against everything in scope. A type shows the binder it was
-- written with (@Σ (a : A), B a@), even where the context happens to have an @a@ of
-- its own: the two are different variables, and shadowing is what binders are for.
renderTerm :: Naming n -> Term n -> Rendered
renderTerm :: forall (n :: S). Naming n -> Term n -> Rendered
renderTerm Naming n
naming Term n
t = Term -> Rendered
Rendered ([VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
forall (n :: S).
[VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
fromTerm [VarIdent]
used [VarIdent]
supply (Naming n -> NameMap n Display
forall (n :: S). Naming n -> NameMap n Display
namingOf Naming n
naming) Term n
t)
  where
    used :: [VarIdent]
used = [VarIdent] -> [VarIdent]
forall a. Eq a => [a] -> [a]
nub ([VarIdent] -> [VarIdent]) -> [VarIdent] -> [VarIdent]
forall a b. (a -> b) -> a -> b
$ [[VarIdent]] -> [VarIdent]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ VarIdent
x VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: Binder -> [VarIdent]
binderLeaves Binder
binder
      | Name n
v <- Term n -> [Name n]
forall (n :: S). Term n -> [Name n]
freeVarsOfTerm Term n
t
      , let (VarIdent
x, Binder
binder) = Naming n -> Name n -> Display
forall (n :: S). Naming n -> Name n -> Display
displayOf Naming n
naming Name n
v
      ]
    supply :: [VarIdent]
supply = [VarIdent]
defaultVarIdents [VarIdent] -> [VarIdent] -> [VarIdent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [VarIdent]
used

-- | A term shown to the user.
ppTerm :: Naming n -> Term n -> String
ppTerm :: forall (n :: S). Naming n -> Term n -> String
ppTerm Naming n
naming = Rendered -> String
forall a. Show a => a -> String
show (Rendered -> String) -> (Term n -> Rendered) -> Term n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Naming n -> Term n -> Rendered
forall (n :: S). Naming n -> Term n -> Rendered
renderTerm Naming n
naming

-- | A typed term shown as @term : type@, as the old @ppFoldT@ did. A variable is
-- shown bare: its type is in the context, not on the node.
ppTermT :: Naming n -> TermT n -> String
ppTermT :: forall (n :: S). Naming n -> TermT n -> String
ppTermT Naming n
naming TermT n
t =
  case TermT n -> Maybe (TypeInfo (TermT n))
forall (n :: S). TermT n -> Maybe (TypeInfo (TermT n))
typeInfoOf TermT n
t of
    Maybe (TypeInfo (TermT n))
Nothing   -> Naming n -> Term n -> String
forall (n :: S). Naming n -> Term n -> String
ppTerm Naming n
naming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
t)
    Just TypeInfo (TermT n)
info -> Naming n -> Term n -> String
forall (n :: S). Naming n -> Term n -> String
ppTerm Naming n
naming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped TermT n
t) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" : " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Naming n -> Term n -> String
forall (n :: S). Naming n -> Term n -> String
ppTerm Naming n
naming (TermT n -> Term n
forall (n :: S). TermT n -> Term n
untyped (TypeInfo (TermT n) -> TermT n
forall term. TypeInfo term -> term
infoType TypeInfo (TermT n)
info))

-- | What a name is called, and the (freshened) binder it was introduced by.
displayOf :: Naming n -> Foil.Name n -> Display
displayOf :: forall (n :: S). Naming n -> Name n -> Display
displayOf Naming n
naming Name n
name = Name n -> NameMap n Display -> Display
forall (n :: S) a. Name n -> NameMap n a -> a
Foil.lookupName Name n
name (Naming n -> NameMap n Display
forall (n :: S). Naming n -> NameMap n Display
namingOf Naming n
naming)

-- | A variable as the user sees it: a pattern binder shows as its pattern
-- (@(t, s)@), anything else by its display name.
ppName :: Naming n -> Foil.Name n -> String
ppName :: forall (n :: S). Naming n -> Name n -> String
ppName Naming n
naming Name n
name =
  case Name n -> NameMap n Display -> Display
forall (n :: S) a. Name n -> NameMap n a -> a
Foil.lookupName Name n
name (Naming n -> NameMap n Display
forall (n :: S). Naming n -> NameMap n Display
namingOf Naming n
naming) of
    (VarIdent
_, Binder
binder) | Binder -> Bool
binderIsCompound Binder
binder -> Pattern -> String
forall a. Print a => a -> String
Rzk.printTree (Binder -> Pattern
binderToPattern Binder
binder)
    (VarIdent
x, Binder
_)                                -> VarIdent -> String
forall a. Print a => a -> String
Rzk.printTree (VarIdent -> VarIdent
fromVarIdent VarIdent
x)

panicImpossible :: String -> a
panicImpossible :: forall a. String -> a
panicImpossible String
msg = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
  [ String
"PANIC! Impossible happened (" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
msg String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")!"
  , String
"Please, report a bug at https://github.com/rzk-lang/rzk/issues"
  ]