{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
{-# LANGUAGE DeriveFoldable     #-}
{-# LANGUAGE DeriveFunctor      #-}
{-# LANGUAGE DeriveTraversable  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE RecordWildCards    #-}

-- | Surface names, binders and modalities.
--
-- These are what the checker shows the user, and they are independent of how a
-- term represents its variables: a 'VarIdent' is a surface identifier (with the
-- position of its defining occurrence), and a 'Binder' records the /names/ a binder
-- introduces — including a pair pattern, which still binds exactly one variable
-- whose components are projections of it.
module Language.Rzk.Foil.Names where

import           Data.Char           (chr, ord)
import           Data.Coerce         (coerce)
import           Data.List           (intercalate)
import           Data.Maybe          (fromMaybe)
import           Data.String         (IsString (..))
import           Data.Set            (Set)
import qualified Data.Set            as Set
import qualified Data.Text           as T

import qualified Language.Rzk.Syntax as Rzk

-- | An identifier that is not in scope becomes a hole under a /marked/ name.
--
-- A free-foil term refers to a variable by name, and an unresolved identifier has
-- none — so the term cannot represent it. Elaboration marks it instead, and the
-- checker reports it when it reaches it, which is what keeps the error where the
-- identifier was used (inside the binders and topes it was written under) rather
-- than at the top of the declaration.
--
-- The marker cannot be mistaken for a hole the user wrote: the grammar forbids @#@
-- in an identifier.
markUnresolved :: VarIdent -> VarIdent
markUnresolved :: VarIdent -> VarIdent
markUnresolved VarIdent
x = String -> VarIdent
forall a. IsString a => String -> a
fromString (Char
'#' Char -> String -> String
forall a. a -> [a] -> [a]
: VarIdent -> String
forall a. Show a => a -> String
show VarIdent
x)

unmarkUnresolved :: VarIdent -> Maybe VarIdent
unmarkUnresolved :: VarIdent -> Maybe VarIdent
unmarkUnresolved VarIdent
x = case VarIdent -> String
forall a. Show a => a -> String
show VarIdent
x of
  Char
'#' : String
name -> VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (String -> VarIdent
forall a. IsString a => String -> a
fromString String
name)
  String
_          -> Maybe VarIdent
forall a. Maybe a
Nothing

-- | What a bound name is shown as: the display name standing for the variable
-- itself, and the (freshened) binder, which gives the pattern to print and the
-- component names to fold projections back to.
type Display = (VarIdent, Binder)

-- | The annotation on every node of a typed term: its type, plus its memoised weak
-- head and normal forms.
data TypeInfo term = TypeInfo
  { forall term. TypeInfo term -> term
infoType :: term
  , forall term. TypeInfo term -> Maybe term
infoWHNF :: Maybe term
  , forall term. TypeInfo term -> Maybe term
infoNF   :: Maybe term
  } deriving ((forall a b. (a -> b) -> TypeInfo a -> TypeInfo b)
-> (forall a b. a -> TypeInfo b -> TypeInfo a) -> Functor TypeInfo
forall a b. a -> TypeInfo b -> TypeInfo a
forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
fmap :: forall a b. (a -> b) -> TypeInfo a -> TypeInfo b
$c<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
<$ :: forall a b. a -> TypeInfo b -> TypeInfo a
Functor, (forall m. Monoid m => TypeInfo m -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeInfo a -> m)
-> (forall m a. Monoid m => (a -> m) -> TypeInfo a -> m)
-> (forall a b. (a -> b -> b) -> b -> TypeInfo a -> b)
-> (forall a b. (a -> b -> b) -> b -> TypeInfo a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeInfo a -> b)
-> (forall b a. (b -> a -> b) -> b -> TypeInfo a -> b)
-> (forall a. (a -> a -> a) -> TypeInfo a -> a)
-> (forall a. (a -> a -> a) -> TypeInfo a -> a)
-> (forall a. TypeInfo a -> [a])
-> (forall a. TypeInfo a -> Bool)
-> (forall a. TypeInfo a -> Int)
-> (forall a. Eq a => a -> TypeInfo a -> Bool)
-> (forall a. Ord a => TypeInfo a -> a)
-> (forall a. Ord a => TypeInfo a -> a)
-> (forall a. Num a => TypeInfo a -> a)
-> (forall a. Num a => TypeInfo a -> a)
-> Foldable TypeInfo
forall a. Eq a => a -> TypeInfo a -> Bool
forall a. Num a => TypeInfo a -> a
forall a. Ord a => TypeInfo a -> a
forall m. Monoid m => TypeInfo m -> m
forall a. TypeInfo a -> Bool
forall a. TypeInfo a -> Int
forall a. TypeInfo a -> [a]
forall a. (a -> a -> a) -> TypeInfo a -> a
forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => TypeInfo m -> m
fold :: forall m. Monoid m => TypeInfo m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TypeInfo a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TypeInfo a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TypeInfo a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldr1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
foldl1 :: forall a. (a -> a -> a) -> TypeInfo a -> a
$ctoList :: forall a. TypeInfo a -> [a]
toList :: forall a. TypeInfo a -> [a]
$cnull :: forall a. TypeInfo a -> Bool
null :: forall a. TypeInfo a -> Bool
$clength :: forall a. TypeInfo a -> Int
length :: forall a. TypeInfo a -> Int
$celem :: forall a. Eq a => a -> TypeInfo a -> Bool
elem :: forall a. Eq a => a -> TypeInfo a -> Bool
$cmaximum :: forall a. Ord a => TypeInfo a -> a
maximum :: forall a. Ord a => TypeInfo a -> a
$cminimum :: forall a. Ord a => TypeInfo a -> a
minimum :: forall a. Ord a => TypeInfo a -> a
$csum :: forall a. Num a => TypeInfo a -> a
sum :: forall a. Num a => TypeInfo a -> a
$cproduct :: forall a. Num a => TypeInfo a -> a
product :: forall a. Num a => TypeInfo a -> a
Foldable, Functor TypeInfo
Foldable TypeInfo
(Functor TypeInfo, Foldable TypeInfo) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TypeInfo a -> f (TypeInfo b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TypeInfo (f a) -> f (TypeInfo a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TypeInfo a -> m (TypeInfo b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TypeInfo (m a) -> m (TypeInfo a))
-> Traversable TypeInfo
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TypeInfo a -> f (TypeInfo b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TypeInfo (f a) -> f (TypeInfo a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TypeInfo a -> m (TypeInfo b)
$csequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
sequence :: forall (m :: * -> *) a. Monad m => TypeInfo (m a) -> m (TypeInfo a)
Traversable)

data RzkPosition = RzkPosition
  { RzkPosition -> Maybe String
rzkFilePath :: Maybe FilePath
  , RzkPosition -> BNFC'Position
rzkLineCol  :: Rzk.BNFC'Position
  }

ppRzkPosition :: RzkPosition -> String
ppRzkPosition :: RzkPosition -> String
ppRzkPosition RzkPosition{Maybe String
BNFC'Position
rzkFilePath :: RzkPosition -> Maybe String
rzkLineCol :: RzkPosition -> BNFC'Position
rzkFilePath :: Maybe String
rzkLineCol :: BNFC'Position
..} = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
":" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ [String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"<stdin>" Maybe String
rzkFilePath]
  , ((Int, Int) -> [String]) -> BNFC'Position -> [String]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Int
row, Int
col) -> (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int
row, Int
col]) BNFC'Position
rzkLineCol]

newtype VarIdent = VarIdent { VarIdent -> VarIdent' RzkPosition
getVarIdent :: Rzk.VarIdent' RzkPosition }

instance Show VarIdent where
  show :: VarIdent -> String
show = VarIdent' RzkPosition -> String
forall a. Print a => a -> String
Rzk.printTree (VarIdent' RzkPosition -> String)
-> (VarIdent -> VarIdent' RzkPosition) -> VarIdent -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarIdent -> VarIdent' RzkPosition
getVarIdent

-- | Identifiers are equal when they are spelled the same, whatever their source
-- positions.
--
-- Written out rather than @(==) \`on\` (void . getVarIdent)@, which allocated a
-- position-free copy of the whole syntax node and compared that: identifier
-- equality is on the hot path (every name lookup, every refreshing of a display
-- name, every match of two terms that mention a hole), and profiling put it at 6%
-- of the checker's time.
instance Eq VarIdent where
  VarIdent (Rzk.VarIdent RzkPosition
_ VarIdentToken
x) == :: VarIdent -> VarIdent -> Bool
== VarIdent (Rzk.VarIdent RzkPosition
_ VarIdentToken
y) = VarIdentToken
x VarIdentToken -> VarIdentToken -> Bool
forall a. Eq a => a -> a -> Bool
== VarIdentToken
y

-- | Identifiers are ordered by name, ignoring the source position, so that the
-- order agrees with 'Eq'. Only used to key identifiers in a set or a map.
instance Ord VarIdent where
  compare :: VarIdent -> VarIdent -> Ordering
compare (VarIdent (Rzk.VarIdent RzkPosition
_ VarIdentToken
x)) (VarIdent (Rzk.VarIdent RzkPosition
_ VarIdentToken
y)) = VarIdentToken -> VarIdentToken -> Ordering
forall a. Ord a => a -> a -> Ordering
compare VarIdentToken
x VarIdentToken
y

instance IsString VarIdent where
  fromString :: String -> VarIdent
fromString String
s = VarIdent' RzkPosition -> VarIdent
VarIdent (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent (Maybe String -> BNFC'Position -> RzkPosition
RzkPosition Maybe String
forall a. Maybe a
Nothing BNFC'Position
forall a. Maybe a
Nothing) (String -> VarIdentToken
forall a. IsString a => String -> a
fromString String
s))

ppVarIdentWithLocation :: VarIdent -> String
ppVarIdentWithLocation :: VarIdent -> String
ppVarIdentWithLocation (VarIdent var :: VarIdent' RzkPosition
var@(Rzk.VarIdent RzkPosition
pos VarIdentToken
_ident)) =
  VarIdent' RzkPosition -> String
forall a. Print a => a -> String
Rzk.printTree VarIdent' RzkPosition
var String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> RzkPosition -> String
ppRzkPosition RzkPosition
pos String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")"

varIdent :: Rzk.VarIdent -> VarIdent
varIdent :: VarIdent -> VarIdent
varIdent = Maybe String -> VarIdent -> VarIdent
varIdentAt Maybe String
forall a. Maybe a
Nothing

varIdentAt :: Maybe FilePath -> Rzk.VarIdent -> VarIdent
varIdentAt :: Maybe String -> VarIdent -> VarIdent
varIdentAt Maybe String
path (Rzk.VarIdent BNFC'Position
pos VarIdentToken
ident) = VarIdent' RzkPosition -> VarIdent
VarIdent (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent (Maybe String -> BNFC'Position -> RzkPosition
RzkPosition Maybe String
path BNFC'Position
pos) VarIdentToken
ident)

fromVarIdent :: VarIdent -> Rzk.VarIdent
fromVarIdent :: VarIdent -> VarIdent
fromVarIdent (VarIdent (Rzk.VarIdent (RzkPosition Maybe String
_file BNFC'Position
pos) VarIdentToken
ident)) = BNFC'Position -> VarIdentToken -> VarIdent
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent BNFC'Position
pos VarIdentToken
ident

-- | The display name of a hole from its surface token text. The token includes
-- the leading @?@; an anonymous hole (bare @?@) has no name.
holeName :: T.Text -> Maybe VarIdent
holeName :: Text -> Maybe VarIdent
holeName Text
tok =
  case Int -> Text -> Text
T.drop Int
1 Text
tok of
    Text
name | Text -> Bool
T.null Text
name -> Maybe VarIdent
forall a. Maybe a
Nothing
         | Bool
otherwise   -> VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (String -> VarIdent
forall a. IsString a => String -> a
fromString (Text -> String
T.unpack Text
name))

-- | The surface token text (including the leading @?@) for a hole name.
holeIdentToken :: Maybe VarIdent -> T.Text
holeIdentToken :: Maybe VarIdent -> Text
holeIdentToken Maybe VarIdent
Nothing  = Text
"?"
holeIdentToken (Just VarIdent
x) = Text
"?" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (VarIdent -> String
forall a. Show a => a -> String
show VarIdent
x)

-- | The name(s) a binder introduces. A binder may name a single (possibly
-- anonymous) variable, or destructure a pair\/tuple via a pattern. The pattern
-- structure is kept around purely so that goals, holes and error messages can
-- show the user's original names (e.g. @t@ and @s@ for @\\ (t , s) -> …@)
-- instead of projections of a fresh variable (e.g. @π₁ x₄@ and @π₂ x₄@).
--
-- Operationally a pair pattern still binds a /single/ variable; the components
-- are projections of it (see 'toScopePattern'). 'Binder' only records the names
-- so they can be restored when rendering.
data Binder
  = BinderVar (Maybe VarIdent)   -- ^ a single variable (@Nothing@ for @_@)
  | BinderPair Binder Binder     -- ^ a pair pattern @(l , r)@
  | BinderUnit                   -- ^ the unit pattern @unit@
  deriving (Binder -> Binder -> Bool
(Binder -> Binder -> Bool)
-> (Binder -> Binder -> Bool) -> Eq Binder
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Binder -> Binder -> Bool
== :: Binder -> Binder -> Bool
$c/= :: Binder -> Binder -> Bool
/= :: Binder -> Binder -> Bool
Eq)

-- | The single name of a binder, if it binds exactly one named variable.
-- A pair\/unit pattern has no single name, so this is 'Nothing' for them.
-- Used wherever the old @Maybe VarIdent@ binder name is still sufficient.
binderName :: Binder -> Maybe VarIdent
binderName :: Binder -> Maybe VarIdent
binderName (BinderVar Maybe VarIdent
mname) = Maybe VarIdent
mname
binderName Binder
_                 = Maybe VarIdent
forall a. Maybe a
Nothing

data TModality = Sharp | Flat | Op | Id deriving (TModality -> TModality -> Bool
(TModality -> TModality -> Bool)
-> (TModality -> TModality -> Bool) -> Eq TModality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TModality -> TModality -> Bool
== :: TModality -> TModality -> Bool
$c/= :: TModality -> TModality -> Bool
/= :: TModality -> TModality -> Bool
Eq, Int -> TModality -> String -> String
[TModality] -> String -> String
TModality -> String
(Int -> TModality -> String -> String)
-> (TModality -> String)
-> ([TModality] -> String -> String)
-> Show TModality
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> TModality -> String -> String
showsPrec :: Int -> TModality -> String -> String
$cshow :: TModality -> String
show :: TModality -> String
$cshowList :: [TModality] -> String -> String
showList :: [TModality] -> String -> String
Show)

toModality :: Rzk.Modality -> TModality
toModality :: Modality -> TModality
toModality Rzk.Sharp{}       = TModality
Sharp
toModality Rzk.ASCII_Sharp{} = TModality
Sharp
toModality Rzk.Flat{}        = TModality
Flat
toModality Rzk.ASCII_Flat{}  = TModality
Flat
toModality Rzk.Op{}          = TModality
Op
toModality Rzk.ASCII_Op{}    = TModality
Op
toModality Rzk.Id{}          = TModality
Id

fromMod :: TModality -> Rzk.Modality
fromMod :: TModality -> Modality
fromMod TModality
Sharp = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Flat  = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Op    = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
forall a. Maybe a
Nothing
fromMod TModality
Id    = BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Id BNFC'Position
forall a. Maybe a
Nothing


-- | A tuple pattern is sugar for nested pairs.
desugarTuple :: Rzk.BNFC'Position -> [Rzk.Pattern] -> Rzk.Pattern -> Rzk.Pattern -> Rzk.Pattern
desugarTuple :: BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
desugarTuple BNFC'Position
loc [Pattern]
ps Pattern
p2 Pattern
p1 =
  case [Pattern]
ps of
    []          -> BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
loc Pattern
p1 Pattern
p2
    Pattern
pLast : [Pattern]
ps' -> BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
loc (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
desugarTuple BNFC'Position
loc [Pattern]
ps' Pattern
p2 Pattern
p1) Pattern
pLast


toBinder :: Rzk.Pattern -> Binder
toBinder :: Pattern -> Binder
toBinder (Rzk.PatternVar BNFC'Position
_loc (Rzk.VarIdent BNFC'Position
_ VarIdentToken
"_")) = Maybe VarIdent -> Binder
BinderVar Maybe VarIdent
forall a. Maybe a
Nothing
toBinder (Rzk.PatternVar BNFC'Position
_loc VarIdent
x)                    = Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just (VarIdent -> VarIdent
varIdent VarIdent
x))
toBinder (Rzk.PatternUnit BNFC'Position
_loc)                     = Binder
BinderUnit
toBinder (Rzk.PatternPair BNFC'Position
_loc Pattern
l Pattern
r)                 = Binder -> Binder -> Binder
BinderPair (Pattern -> Binder
toBinder Pattern
l) (Pattern -> Binder
toBinder Pattern
r)
toBinder (Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps)            = Pattern -> Binder
toBinder (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1)

patternToTerm :: Rzk.Pattern -> Rzk.Term
patternToTerm :: Pattern -> Term
patternToTerm = Pattern -> Term
ptt
  where
    ptt :: Pattern -> Term
ptt = \case
      Rzk.PatternVar BNFC'Position
loc VarIdent
x    -> BNFC'Position -> VarIdent -> Term
forall a. a -> VarIdent' a -> Term' a
Rzk.Var BNFC'Position
loc VarIdent
x
      Rzk.PatternPair BNFC'Position
loc Pattern
l Pattern
r -> BNFC'Position -> Term -> Term -> Term
forall a. a -> Term' a -> Term' a -> Term' a
Rzk.Pair BNFC'Position
loc (Pattern -> Term
ptt Pattern
l) (Pattern -> Term
ptt Pattern
r)
      Rzk.PatternUnit BNFC'Position
loc     -> BNFC'Position -> Term
forall a. a -> Term' a
Rzk.Unit BNFC'Position
loc
      Rzk.PatternTuple BNFC'Position
loc Pattern
p1 Pattern
p2 [Pattern]
ps -> Pattern -> Term
patternToTerm (BNFC'Position -> [Pattern] -> Pattern -> Pattern -> Pattern
desugarTuple BNFC'Position
loc ([Pattern] -> [Pattern]
forall a. [a] -> [a]
reverse [Pattern]
ps) Pattern
p2 Pattern
p1)


modalColonModality :: Rzk.ModalColon -> Rzk.Modality
modalColonModality :: ModalColon -> Modality
modalColonModality = \case
  Rzk.ModalColonFlat BNFC'Position
loc        -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
loc
  Rzk.ModalColonSharp BNFC'Position
loc       -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
loc
  Rzk.ModalColonOp BNFC'Position
loc          -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
loc
  Rzk.ModalColonId BNFC'Position
loc          -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Id BNFC'Position
loc
  Rzk.ASCII_ModalColonFlat BNFC'Position
loc  -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Flat BNFC'Position
loc
  Rzk.ASCII_ModalColonSharp BNFC'Position
loc -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Sharp BNFC'Position
loc
  Rzk.ASCII_ModalColonOp BNFC'Position
loc    -> BNFC'Position -> Modality
forall a. a -> Modality' a
Rzk.Op BNFC'Position
loc

modalColonToTModality :: Rzk.ModalColon -> TModality
modalColonToTModality :: ModalColon -> TModality
modalColonToTModality = Modality -> TModality
toModality (Modality -> TModality)
-> (ModalColon -> Modality) -> ModalColon -> TModality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModalColon -> Modality
modalColonModality

fromTModalityToModalColon :: TModality -> Rzk.ModalColon
fromTModalityToModalColon :: TModality -> ModalColon
fromTModalityToModalColon = \case
  TModality
Sharp -> BNFC'Position -> ModalColon
forall a. a -> ModalColon' a
Rzk.ModalColonSharp BNFC'Position
forall a. Maybe a
Nothing
  TModality
Flat  -> BNFC'Position -> ModalColon
forall a. a -> ModalColon' a
Rzk.ModalColonFlat BNFC'Position
forall a. Maybe a
Nothing
  TModality
Op    -> BNFC'Position -> ModalColon
forall a. a -> ModalColon' a
Rzk.ModalColonOp BNFC'Position
forall a. Maybe a
Nothing
  TModality
Id    -> BNFC'Position -> ModalColon
forall a. a -> ModalColon' a
Rzk.ModalColonId BNFC'Position
forall a. Maybe a
Nothing

-- | Split a binder term into the individual variables it names. A multi-variable
-- binder like @(x y : A)@ is parsed as the application spine @x y@; this returns
-- @[x, y]@ so each can become its own nested binder. A single binder term (a
-- variable, a pair pattern, …) is returned unchanged as a singleton.
flattenBinderApp :: Rzk.Term -> [Rzk.Term]
flattenBinderApp :: Term -> [Term]
flattenBinderApp = \case
  Rzk.App BNFC'Position
_loc Term
f Term
x -> Term -> [Term]
flattenBinderApp Term
f [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
x]
  Term
t                -> [Term
t]

unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern
unsafeTermToPattern :: Term -> Pattern
unsafeTermToPattern = Term -> Pattern
forall {a}. Term' a -> Pattern' a
ttp
  where
    ttp :: Term' a -> Pattern' a
ttp = \case
      Rzk.Unit a
loc                        -> a -> Pattern' a
forall a. a -> Pattern' a
Rzk.PatternUnit a
loc
      Rzk.Var a
loc VarIdent' a
x                       -> a -> VarIdent' a -> Pattern' a
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar a
loc VarIdent' a
x
      Rzk.Pair a
loc Term' a
l Term' a
r                    -> a -> Pattern' a -> Pattern' a -> Pattern' a
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair a
loc (Term' a -> Pattern' a
ttp Term' a
l) (Term' a -> Pattern' a
ttp Term' a
r)
      Rzk.Tuple a
loc Term' a
t1 Term' a
t2 [Term' a]
ts              -> a -> Pattern' a -> Pattern' a -> [Pattern' a] -> Pattern' a
forall a.
a -> Pattern' a -> Pattern' a -> [Pattern' a] -> Pattern' a
Rzk.PatternTuple a
loc (Term' a -> Pattern' a
ttp Term' a
t1) (Term' a -> Pattern' a
ttp Term' a
t2) ((Term' a -> Pattern' a) -> [Term' a] -> [Pattern' a]
forall a b. (a -> b) -> [a] -> [b]
map Term' a -> Pattern' a
ttp [Term' a]
ts)
      Term' a
term -> String -> Pattern' a
forall a. HasCallStack => String -> a
error (String
"ERROR: expected a pattern but got\n  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term' a -> String
forall a. Print a => a -> String
Rzk.printTree Term' a
term)

sigmaParamToTypeSigma :: Rzk.BNFC'Position -> Rzk.SigmaParam -> Rzk.Term -> Rzk.Term
sigmaParamToTypeSigma :: BNFC'Position -> SigmaParam -> Term -> Term
sigmaParamToTypeSigma BNFC'Position
loc SigmaParam
sp Term
body = case SigmaParam
sp of
  Rzk.SigmaParam      BNFC'Position
_ Pattern
pat Term
ty      -> 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
body
  Rzk.SigmaParamModal BNFC'Position
_ Pattern
pat ModalColon
mc Term
ty  -> BNFC'Position -> Pattern -> ModalColon -> Term -> Term -> Term
forall a.
a -> Pattern' a -> ModalColon' a -> Term' a -> Term' a -> Term' a
Rzk.TypeSigmaModal BNFC'Position
loc Pattern
pat ModalColon
mc Term
ty Term
body

-- | A projection step: first (@π₁@) or second (@π₂@) component.
data Proj = PFst | PSnd
  deriving (Proj -> Proj -> Bool
(Proj -> Proj -> Bool) -> (Proj -> Proj -> Bool) -> Eq Proj
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Proj -> Proj -> Bool
== :: Proj -> Proj -> Bool
$c/= :: Proj -> Proj -> Bool
/= :: Proj -> Proj -> Bool
Eq)

-- | Render a 'Binder' as a surface pattern (used to display the binder itself,
-- e.g. @(t , s)@). Anonymous variables become @_@.
binderToPattern :: Binder -> Rzk.Pattern
binderToPattern :: Binder -> Pattern
binderToPattern (BinderVar Maybe VarIdent
Nothing)  = BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> VarIdent
fromVarIdent VarIdent
"_")
binderToPattern (BinderVar (Just VarIdent
x)) = BNFC'Position -> VarIdent -> Pattern
forall a. a -> VarIdent' a -> Pattern' a
Rzk.PatternVar BNFC'Position
forall a. Maybe a
Nothing (VarIdent -> VarIdent
fromVarIdent VarIdent
x)
binderToPattern (BinderPair Binder
l Binder
r)     = BNFC'Position -> Pattern -> Pattern -> Pattern
forall a. a -> Pattern' a -> Pattern' a -> Pattern' a
Rzk.PatternPair BNFC'Position
forall a. Maybe a
Nothing (Binder -> Pattern
binderToPattern Binder
l) (Binder -> Pattern
binderToPattern Binder
r)
binderToPattern Binder
BinderUnit           = BNFC'Position -> Pattern
forall a. a -> Pattern' a
Rzk.PatternUnit BNFC'Position
forall a. Maybe a
Nothing



-- | A 'VarIdent' that prints as the binder's surface pattern, e.g. @(t , s)@.
-- Used to display a pattern binder in a hole's local context as the pattern
-- itself rather than as the underlying single variable.
binderDisplayName :: Binder -> VarIdent
binderDisplayName :: Binder -> VarIdent
binderDisplayName = String -> VarIdent
forall a. IsString a => String -> a
fromString (String -> VarIdent) -> (Binder -> String) -> Binder -> VarIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> String
forall a. Print a => a -> String
Rzk.printTree (Pattern -> String) -> (Binder -> Pattern) -> Binder -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> Pattern
binderToPattern

-- | The named leaves of a binder, each paired with the projection path that
-- reaches it from the bound variable. For example @(t , (a , b))@ yields
-- @[([PFst], t), ([PSnd, PFst], a), ([PSnd, PSnd], b)]@.
binderPaths :: Binder -> [([Proj], VarIdent)]
binderPaths :: Binder -> [([Proj], VarIdent)]
binderPaths (BinderVar (Just VarIdent
x)) = [([], VarIdent
x)]
binderPaths (BinderVar Maybe VarIdent
Nothing)  = []
binderPaths Binder
BinderUnit           = []
binderPaths (BinderPair Binder
l Binder
r)     =
  [ (Proj
PFst Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
p, VarIdent
n) | ([Proj]
p, VarIdent
n) <- Binder -> [([Proj], VarIdent)]
binderPaths Binder
l ] [([Proj], VarIdent)]
-> [([Proj], VarIdent)] -> [([Proj], VarIdent)]
forall a. [a] -> [a] -> [a]
++
  [ (Proj
PSnd Proj -> [Proj] -> [Proj]
forall a. a -> [a] -> [a]
: [Proj]
p, VarIdent
n) | ([Proj]
p, VarIdent
n) <- Binder -> [([Proj], VarIdent)]
binderPaths Binder
r ]

-- | The names appearing in a binder.
binderLeaves :: Binder -> [VarIdent]
binderLeaves :: Binder -> [VarIdent]
binderLeaves = (([Proj], VarIdent) -> VarIdent)
-> [([Proj], VarIdent)] -> [VarIdent]
forall a b. (a -> b) -> [a] -> [b]
map ([Proj], VarIdent) -> VarIdent
forall a b. (a, b) -> b
snd ([([Proj], VarIdent)] -> [VarIdent])
-> (Binder -> [([Proj], VarIdent)]) -> Binder -> [VarIdent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> [([Proj], VarIdent)]
binderPaths

-- | Does this binder destructure a pair\/tuple (as opposed to naming a single
-- variable or @_@)?
binderIsCompound :: Binder -> Bool
binderIsCompound :: Binder -> Bool
binderIsCompound BinderVar{} = Bool
False
binderIsCompound Binder
_           = Bool
True

-- | Refresh the named leaves of a binder so they avoid the given names (and one
-- another). Anonymous leaves and the unit pattern are left unchanged.
freshenBinderLeaves :: [VarIdent] -> Binder -> Binder
freshenBinderLeaves :: [VarIdent] -> Binder -> Binder
freshenBinderLeaves [VarIdent]
used = ([VarIdent], Binder) -> Binder
forall a b. (a, b) -> b
snd (([VarIdent], Binder) -> Binder)
-> (Binder -> ([VarIdent], Binder)) -> Binder -> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
used
  where
    go :: [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u (BinderVar (Just VarIdent
x)) = let x' :: VarIdent
x' = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
u VarIdent
x in (VarIdent
x' VarIdent -> [VarIdent] -> [VarIdent]
forall a. a -> [a] -> [a]
: [VarIdent]
u, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x'))
    go [VarIdent]
u b :: Binder
b@(BinderVar Maybe VarIdent
Nothing) = ([VarIdent]
u, Binder
b)
    go [VarIdent]
u Binder
BinderUnit            = ([VarIdent]
u, Binder
BinderUnit)
    go [VarIdent]
u (BinderPair Binder
l Binder
r)      =
      let ([VarIdent]
u1, Binder
l') = [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u Binder
l
          ([VarIdent]
u2, Binder
r') = [VarIdent] -> Binder -> ([VarIdent], Binder)
go [VarIdent]
u1 Binder
r
      in ([VarIdent]
u2, Binder -> Binder -> Binder
BinderPair Binder
l' Binder
r')

-- | Decompose a chain of projections applied to a variable into the projection
-- path /from the variable outwards/, matching 'binderPaths'. The outermost
-- projection is applied last, so it goes at the /end/ of the path: e.g.
-- @π₂ (π₁ x)@ (select @π₁@ first, then @π₂@) becomes @Just ([PFst, PSnd], x)@.

defaultVarIdents :: [VarIdent]
defaultVarIdents :: [VarIdent]
defaultVarIdents =
  [ String -> VarIdent
forall a. IsString a => String -> a
fromString String
name
  | Int
n <- [Int
1 :: Int ..]
  , let name :: String
name = String
"x" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitToSub (Int -> String
forall a. Show a => a -> String
show Int
n) ]
  where
    digitToSub :: Char -> Char
digitToSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'₀')

-- $setup
-- >>> :set -XOverloadedStrings
-- >>> import qualified Data.Text as T
-- >>> import qualified Data.Set as Set

-- | Given a list of used variable names in the current context,
-- generate a unique fresh name based on a given one.
--
-- >>> print $ refreshVar ["x", "y", "x₁", "z"] "x"
-- x₂
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar :: [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
vars VarIdent
x
  | VarIdent
x VarIdent -> [VarIdent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VarIdent]
vars = [VarIdent] -> VarIdent -> VarIdent
refreshVar [VarIdent]
vars (VarIdent -> VarIdent
incVarIdentIndex VarIdent
x)
  | Bool
otherwise     = VarIdent
x

-- | Refresh a name against a /set/ of taken ones.
--
-- The list version above is O(taken) per call, and naming a whole context calls it
-- once per entry, which made reading the naming off a context with every top-level
-- definition of a project in it quadratic.
--
-- >>> print $ refreshVarIn (Set.fromList ["x", "y", "x₁", "z"]) "x"
-- x₂
refreshVarIn :: Set VarIdent -> VarIdent -> VarIdent
refreshVarIn :: Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
taken VarIdent
x
  | VarIdent
x VarIdent -> Set VarIdent -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set VarIdent
taken = Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
taken (VarIdent -> VarIdent
incVarIdentIndex VarIdent
x)
  | Bool
otherwise            = VarIdent
x

-- | 'freshenBinderLeaves' against a /set/ of taken names, for the same
-- reason 'refreshVarIn' exists beside 'refreshVar'.
freshenBinderLeavesIn :: Set VarIdent -> Binder -> Binder
freshenBinderLeavesIn :: Set VarIdent -> Binder -> Binder
freshenBinderLeavesIn Set VarIdent
used = (Set VarIdent, Binder) -> Binder
forall a b. (a, b) -> b
snd ((Set VarIdent, Binder) -> Binder)
-> (Binder -> (Set VarIdent, Binder)) -> Binder -> Binder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set VarIdent -> Binder -> (Set VarIdent, Binder)
go Set VarIdent
used
  where
    go :: Set VarIdent -> Binder -> (Set VarIdent, Binder)
go Set VarIdent
u (BinderVar (Just VarIdent
x)) =
      let x' :: VarIdent
x' = Set VarIdent -> VarIdent -> VarIdent
refreshVarIn Set VarIdent
u VarIdent
x in (VarIdent -> Set VarIdent -> Set VarIdent
forall a. Ord a => a -> Set a -> Set a
Set.insert VarIdent
x' Set VarIdent
u, Maybe VarIdent -> Binder
BinderVar (VarIdent -> Maybe VarIdent
forall a. a -> Maybe a
Just VarIdent
x'))
    go Set VarIdent
u b :: Binder
b@(BinderVar Maybe VarIdent
Nothing) = (Set VarIdent
u, Binder
b)
    go Set VarIdent
u Binder
BinderUnit            = (Set VarIdent
u, Binder
BinderUnit)
    go Set VarIdent
u (BinderPair Binder
l Binder
r)      =
      let (Set VarIdent
u1, Binder
l') = Set VarIdent -> Binder -> (Set VarIdent, Binder)
go Set VarIdent
u Binder
l
          (Set VarIdent
u2, Binder
r') = Set VarIdent -> Binder -> (Set VarIdent, Binder)
go Set VarIdent
u1 Binder
r
      in (Set VarIdent
u2, Binder -> Binder -> Binder
BinderPair Binder
l' Binder
r')

incVarIdentIndex :: VarIdent -> VarIdent
incVarIdentIndex :: VarIdent -> VarIdent
incVarIdentIndex (VarIdent (Rzk.VarIdent RzkPosition
loc VarIdentToken
token)) =
  VarIdent' RzkPosition -> VarIdent
VarIdent (RzkPosition -> VarIdentToken -> VarIdent' RzkPosition
forall a. a -> VarIdentToken -> VarIdent' a
Rzk.VarIdent RzkPosition
loc ((Text -> Text) -> VarIdentToken -> VarIdentToken
forall a b. Coercible a b => a -> b
coerce Text -> Text
incIndex VarIdentToken
token))

-- | Increment the subscript number at the end of the indentifier.
--
-- >>> putStrLn $ T.unpack $ incIndex "x"
-- x₁
-- >>> putStrLn $ T.unpack $ incIndex "x₁₉"
-- x₂₀
incIndex :: T.Text -> T.Text
incIndex :: Text -> Text
incIndex Text
s = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ String
name String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
newIndex
  where
    digitsSub :: String
digitsSub = String
"₀₁₂₃₄₅₆₇₈₉" :: String
    isDigitSub :: Char -> Bool
isDigitSub = (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
digitsSub)
    digitFromSub :: Char -> Char
digitFromSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'₀') Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'0')
    digitToSub :: Char -> Char
digitToSub Char
c = Int -> Char
chr ((Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord Char
'₀')
    (String
name, String
index) = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isDigitSub (Text -> String
T.unpack Text
s)
    oldIndexN :: Int
oldIndexN = String -> Int
forall a. Read a => String -> a
read (Char
'0' Char -> String -> String
forall a. a -> [a] -> [a]
: (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitFromSub String
index) :: Int -- FIXME: read
    newIndex :: String
newIndex = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
digitToSub (Int -> String
forall a. Show a => a -> String
show (Int
oldIndexN Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))