module Covenant.Internal.Type
  ( AbstractTy (..),
    Renamed (..),
    CompT (..),
    CompTBody (..),
    ValT (..),
    BuiltinFlatT (..),
  )
where

import Control.Monad.Reader
  ( MonadReader (local),
    Reader,
    asks,
    runReader,
  )
import Covenant.DeBruijn (DeBruijn)
import Covenant.Index
  ( Count,
    Index,
    intCount,
    intIndex,
  )
import Data.Functor.Classes (Eq1 (liftEq))
import Data.Kind (Type)
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty (NonEmptyVector)
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Word (Word64)
import GHC.Exts (fromListN)
import Optics.At ()
import Optics.Core
  ( A_Lens,
    LabelOptic (labelOptic),
    ix,
    lens,
    over,
    preview,
    review,
    set,
    view,
    (%),
  )
import Prettyprinter
  ( Doc,
    Pretty (pretty),
    hsep,
    parens,
    viaShow,
    (<+>),
  )

-- | A type abstraction, using a combination of a DeBruijn index (to indicate
-- which scope it refers to) and a positional index (to indicate which bound
-- variable in that scope it refers to).
--
-- = Important note
--
-- This is a /relative/ representation: any given 'AbstractTy' could refer to
-- different things when placed in different positions in the ASG. This stems
-- from how DeBruijn indices behave: 'Z' refers to \'our immediate enclosing
-- scope\', @'S' 'Z'@ to \'one scope outside our immediate enclosing scope\',
-- etc. This can mean different things depending on what these scope(s) are.
--
-- @since 1.0.0
data AbstractTy = BoundAt DeBruijn (Index "tyvar")
  deriving stock
    ( -- | @since 1.0.0
      AbstractTy -> AbstractTy -> Bool
(AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool) -> Eq AbstractTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbstractTy -> AbstractTy -> Bool
== :: AbstractTy -> AbstractTy -> Bool
$c/= :: AbstractTy -> AbstractTy -> Bool
/= :: AbstractTy -> AbstractTy -> Bool
Eq,
      -- | @since 1.0.0
      Eq AbstractTy
Eq AbstractTy =>
(AbstractTy -> AbstractTy -> Ordering)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> AbstractTy)
-> (AbstractTy -> AbstractTy -> AbstractTy)
-> Ord AbstractTy
AbstractTy -> AbstractTy -> Bool
AbstractTy -> AbstractTy -> Ordering
AbstractTy -> AbstractTy -> AbstractTy
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 :: AbstractTy -> AbstractTy -> Ordering
compare :: AbstractTy -> AbstractTy -> Ordering
$c< :: AbstractTy -> AbstractTy -> Bool
< :: AbstractTy -> AbstractTy -> Bool
$c<= :: AbstractTy -> AbstractTy -> Bool
<= :: AbstractTy -> AbstractTy -> Bool
$c> :: AbstractTy -> AbstractTy -> Bool
> :: AbstractTy -> AbstractTy -> Bool
$c>= :: AbstractTy -> AbstractTy -> Bool
>= :: AbstractTy -> AbstractTy -> Bool
$cmax :: AbstractTy -> AbstractTy -> AbstractTy
max :: AbstractTy -> AbstractTy -> AbstractTy
$cmin :: AbstractTy -> AbstractTy -> AbstractTy
min :: AbstractTy -> AbstractTy -> AbstractTy
Ord,
      -- | @since 1.0.0
      Int -> AbstractTy -> ShowS
[AbstractTy] -> ShowS
AbstractTy -> String
(Int -> AbstractTy -> ShowS)
-> (AbstractTy -> String)
-> ([AbstractTy] -> ShowS)
-> Show AbstractTy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbstractTy -> ShowS
showsPrec :: Int -> AbstractTy -> ShowS
$cshow :: AbstractTy -> String
show :: AbstractTy -> String
$cshowList :: [AbstractTy] -> ShowS
showList :: [AbstractTy] -> ShowS
Show
    )

-- | A type abstraction that has undergone renaming from a specific context.
--
-- @since 1.0.0
data Renamed
  = -- | Set by an enclosing scope, and thus is essentially a
    -- concrete type, we just don't know which. First field is its \'true
    -- level\', second field is the positional index in that scope.
    Rigid Int (Index "tyvar")
  | -- | Can be unified with something, but must be consistent: that is, only one
    -- unification for every instance. Field is this variable's positional index;
    -- we don't need to track the scope, as only one scope contains unifiable
    -- bindings.
    Unifiable (Index "tyvar")
  | -- | /Must/ unify with everything, except with other distinct wildcards in the
    -- same scope. First field is a unique /scope/ identifier; second is its
    -- \'true level\' simialr to @'Rigid'@; third is the positional index within
    -- its scope. We must have unique identifiers for wildcard scopes, as
    -- wildcards unify with everything /except/ other wildcards in the /same/
    -- scope, and child scopes aren't unique.
    Wildcard Word64 Int (Index "tyvar")
  deriving stock
    ( -- | @since 1.0.0
      Renamed -> Renamed -> Bool
(Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool) -> Eq Renamed
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Renamed -> Renamed -> Bool
== :: Renamed -> Renamed -> Bool
$c/= :: Renamed -> Renamed -> Bool
/= :: Renamed -> Renamed -> Bool
Eq,
      -- | @since 1.0.0
      Eq Renamed
Eq Renamed =>
(Renamed -> Renamed -> Ordering)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Renamed)
-> (Renamed -> Renamed -> Renamed)
-> Ord Renamed
Renamed -> Renamed -> Bool
Renamed -> Renamed -> Ordering
Renamed -> Renamed -> Renamed
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 :: Renamed -> Renamed -> Ordering
compare :: Renamed -> Renamed -> Ordering
$c< :: Renamed -> Renamed -> Bool
< :: Renamed -> Renamed -> Bool
$c<= :: Renamed -> Renamed -> Bool
<= :: Renamed -> Renamed -> Bool
$c> :: Renamed -> Renamed -> Bool
> :: Renamed -> Renamed -> Bool
$c>= :: Renamed -> Renamed -> Bool
>= :: Renamed -> Renamed -> Bool
$cmax :: Renamed -> Renamed -> Renamed
max :: Renamed -> Renamed -> Renamed
$cmin :: Renamed -> Renamed -> Renamed
min :: Renamed -> Renamed -> Renamed
Ord,
      -- | @since 1.0.0
      Int -> Renamed -> ShowS
[Renamed] -> ShowS
Renamed -> String
(Int -> Renamed -> ShowS)
-> (Renamed -> String) -> ([Renamed] -> ShowS) -> Show Renamed
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Renamed -> ShowS
showsPrec :: Int -> Renamed -> ShowS
$cshow :: Renamed -> String
show :: Renamed -> String
$cshowList :: [Renamed] -> ShowS
showList :: [Renamed] -> ShowS
Show
    )

-- | The \'body\' of a computation type, consisting of the types of its
-- arguments and the type of its result.
--
-- @since 1.0.0
newtype CompTBody (a :: Type) = CompTBody (NonEmptyVector (ValT a))
  deriving stock
    ( -- | @since 1.0.0
      CompTBody a -> CompTBody a -> Bool
(CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool) -> Eq (CompTBody a)
forall a. Eq a => CompTBody a -> CompTBody a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => CompTBody a -> CompTBody a -> Bool
== :: CompTBody a -> CompTBody a -> Bool
$c/= :: forall a. Eq a => CompTBody a -> CompTBody a -> Bool
/= :: CompTBody a -> CompTBody a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (CompTBody a)
Eq (CompTBody a) =>
(CompTBody a -> CompTBody a -> Ordering)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> CompTBody a)
-> (CompTBody a -> CompTBody a -> CompTBody a)
-> Ord (CompTBody a)
CompTBody a -> CompTBody a -> Bool
CompTBody a -> CompTBody a -> Ordering
CompTBody a -> CompTBody a -> CompTBody a
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
forall a. Ord a => Eq (CompTBody a)
forall a. Ord a => CompTBody a -> CompTBody a -> Bool
forall a. Ord a => CompTBody a -> CompTBody a -> Ordering
forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
$ccompare :: forall a. Ord a => CompTBody a -> CompTBody a -> Ordering
compare :: CompTBody a -> CompTBody a -> Ordering
$c< :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
< :: CompTBody a -> CompTBody a -> Bool
$c<= :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
<= :: CompTBody a -> CompTBody a -> Bool
$c> :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
> :: CompTBody a -> CompTBody a -> Bool
$c>= :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
>= :: CompTBody a -> CompTBody a -> Bool
$cmax :: forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
max :: CompTBody a -> CompTBody a -> CompTBody a
$cmin :: forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
min :: CompTBody a -> CompTBody a -> CompTBody a
Ord,
      -- | @since 1.0.0
      Int -> CompTBody a -> ShowS
[CompTBody a] -> ShowS
CompTBody a -> String
(Int -> CompTBody a -> ShowS)
-> (CompTBody a -> String)
-> ([CompTBody a] -> ShowS)
-> Show (CompTBody a)
forall a. Show a => Int -> CompTBody a -> ShowS
forall a. Show a => [CompTBody a] -> ShowS
forall a. Show a => CompTBody a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CompTBody a -> ShowS
showsPrec :: Int -> CompTBody a -> ShowS
$cshow :: forall a. Show a => CompTBody a -> String
show :: CompTBody a -> String
$cshowList :: forall a. Show a => [CompTBody a] -> ShowS
showList :: [CompTBody a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 CompTBody where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
liftEq a -> b -> Bool
f (CompTBody NonEmptyVector (ValT a)
xs) (CompTBody NonEmptyVector (ValT b)
ys) =
    (ValT a -> ValT b -> Bool)
-> NonEmptyVector (ValT a) -> NonEmptyVector (ValT b) -> Bool
forall a b.
(a -> b -> Bool) -> NonEmptyVector a -> NonEmptyVector b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) NonEmptyVector (ValT a)
xs NonEmptyVector (ValT b)
ys

-- | A computation type, with abstractions indicated by the type argument. In
-- pretty much any case imaginable, this would be either 'AbstractTy' (in the
-- ASG), or 'Renamed' (after renaming).
--
-- @since 1.0.0
data CompT (a :: Type) = CompT (Count "tyvar") (CompTBody a)
  deriving stock
    ( -- | @since 1.0.0
      CompT a -> CompT a -> Bool
(CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool) -> Eq (CompT a)
forall a. Eq a => CompT a -> CompT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => CompT a -> CompT a -> Bool
== :: CompT a -> CompT a -> Bool
$c/= :: forall a. Eq a => CompT a -> CompT a -> Bool
/= :: CompT a -> CompT a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (CompT a)
Eq (CompT a) =>
(CompT a -> CompT a -> Ordering)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> CompT a)
-> (CompT a -> CompT a -> CompT a)
-> Ord (CompT a)
CompT a -> CompT a -> Bool
CompT a -> CompT a -> Ordering
CompT a -> CompT a -> CompT a
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
forall a. Ord a => Eq (CompT a)
forall a. Ord a => CompT a -> CompT a -> Bool
forall a. Ord a => CompT a -> CompT a -> Ordering
forall a. Ord a => CompT a -> CompT a -> CompT a
$ccompare :: forall a. Ord a => CompT a -> CompT a -> Ordering
compare :: CompT a -> CompT a -> Ordering
$c< :: forall a. Ord a => CompT a -> CompT a -> Bool
< :: CompT a -> CompT a -> Bool
$c<= :: forall a. Ord a => CompT a -> CompT a -> Bool
<= :: CompT a -> CompT a -> Bool
$c> :: forall a. Ord a => CompT a -> CompT a -> Bool
> :: CompT a -> CompT a -> Bool
$c>= :: forall a. Ord a => CompT a -> CompT a -> Bool
>= :: CompT a -> CompT a -> Bool
$cmax :: forall a. Ord a => CompT a -> CompT a -> CompT a
max :: CompT a -> CompT a -> CompT a
$cmin :: forall a. Ord a => CompT a -> CompT a -> CompT a
min :: CompT a -> CompT a -> CompT a
Ord,
      -- | @since 1.0.0
      Int -> CompT a -> ShowS
[CompT a] -> ShowS
CompT a -> String
(Int -> CompT a -> ShowS)
-> (CompT a -> String) -> ([CompT a] -> ShowS) -> Show (CompT a)
forall a. Show a => Int -> CompT a -> ShowS
forall a. Show a => [CompT a] -> ShowS
forall a. Show a => CompT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CompT a -> ShowS
showsPrec :: Int -> CompT a -> ShowS
$cshow :: forall a. Show a => CompT a -> String
show :: CompT a -> String
$cshowList :: forall a. Show a => [CompT a] -> ShowS
showList :: [CompT a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 CompT where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> CompT a -> CompT b -> Bool
liftEq a -> b -> Bool
f (CompT Count "tyvar"
abses1 CompTBody a
xs) (CompT Count "tyvar"
abses2 CompTBody b
ys) =
    Count "tyvar"
abses1 Count "tyvar" -> Count "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Count "tyvar"
abses2 Bool -> Bool -> Bool
&& (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
forall a b. (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f CompTBody a
xs CompTBody b
ys

-- | @since 1.0.0
instance Pretty (CompT Renamed) where
  pretty :: forall ann. CompT Renamed -> Doc ann
pretty = PrettyM ann (Doc ann) -> Doc ann
forall ann a. PrettyM ann a -> a
runPrettyM (PrettyM ann (Doc ann) -> Doc ann)
-> (CompT Renamed -> PrettyM ann (Doc ann))
-> CompT Renamed
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT Renamed -> PrettyM ann (Doc ann)
forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext

-- | A value type, with abstractions indicated by the type argument. In pretty
-- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or
-- 'Renamed' (after renaming).
--
-- @since 1.0.0
data ValT (a :: Type)
  = -- | An abstract type.
    Abstraction a
  | -- | A suspended computation.
    ThunkT (CompT a)
  | -- | A builtin type without any nesting.
    BuiltinFlat BuiltinFlatT
  deriving stock
    ( -- | @since 1.0.0
      ValT a -> ValT a -> Bool
(ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool) -> Eq (ValT a)
forall a. Eq a => ValT a -> ValT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => ValT a -> ValT a -> Bool
== :: ValT a -> ValT a -> Bool
$c/= :: forall a. Eq a => ValT a -> ValT a -> Bool
/= :: ValT a -> ValT a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (ValT a)
Eq (ValT a) =>
(ValT a -> ValT a -> Ordering)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> ValT a)
-> (ValT a -> ValT a -> ValT a)
-> Ord (ValT a)
ValT a -> ValT a -> Bool
ValT a -> ValT a -> Ordering
ValT a -> ValT a -> ValT a
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
forall a. Ord a => Eq (ValT a)
forall a. Ord a => ValT a -> ValT a -> Bool
forall a. Ord a => ValT a -> ValT a -> Ordering
forall a. Ord a => ValT a -> ValT a -> ValT a
$ccompare :: forall a. Ord a => ValT a -> ValT a -> Ordering
compare :: ValT a -> ValT a -> Ordering
$c< :: forall a. Ord a => ValT a -> ValT a -> Bool
< :: ValT a -> ValT a -> Bool
$c<= :: forall a. Ord a => ValT a -> ValT a -> Bool
<= :: ValT a -> ValT a -> Bool
$c> :: forall a. Ord a => ValT a -> ValT a -> Bool
> :: ValT a -> ValT a -> Bool
$c>= :: forall a. Ord a => ValT a -> ValT a -> Bool
>= :: ValT a -> ValT a -> Bool
$cmax :: forall a. Ord a => ValT a -> ValT a -> ValT a
max :: ValT a -> ValT a -> ValT a
$cmin :: forall a. Ord a => ValT a -> ValT a -> ValT a
min :: ValT a -> ValT a -> ValT a
Ord,
      -- | @since 1.0.0
      Int -> ValT a -> ShowS
[ValT a] -> ShowS
ValT a -> String
(Int -> ValT a -> ShowS)
-> (ValT a -> String) -> ([ValT a] -> ShowS) -> Show (ValT a)
forall a. Show a => Int -> ValT a -> ShowS
forall a. Show a => [ValT a] -> ShowS
forall a. Show a => ValT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ValT a -> ShowS
showsPrec :: Int -> ValT a -> ShowS
$cshow :: forall a. Show a => ValT a -> String
show :: ValT a -> String
$cshowList :: forall a. Show a => [ValT a] -> ShowS
showList :: [ValT a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 ValT where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
liftEq a -> b -> Bool
f = \case
    Abstraction a
abs1 -> \case
      Abstraction b
abs2 -> a -> b -> Bool
f a
abs1 b
abs2
      ValT b
_ -> Bool
False
    ThunkT CompT a
t1 -> \case
      ThunkT CompT b
t2 -> (a -> b -> Bool) -> CompT a -> CompT b -> Bool
forall a b. (a -> b -> Bool) -> CompT a -> CompT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f CompT a
t1 CompT b
t2
      ValT b
_ -> Bool
False
    BuiltinFlat BuiltinFlatT
t1 -> \case
      BuiltinFlat BuiltinFlatT
t2 -> BuiltinFlatT
t1 BuiltinFlatT -> BuiltinFlatT -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinFlatT
t2
      ValT b
_ -> Bool
False

-- | All builtin types that are \'flat\': that is, do not have other types
-- \'nested inside them\'.
data BuiltinFlatT
  = UnitT
  | BoolT
  | IntegerT
  | StringT
  | ByteStringT
  | BLS12_381_G1_ElementT
  | BLS12_381_G2_ElementT
  | BLS12_381_MlResultT
  deriving stock
    ( -- | @since 1.0.0
      BuiltinFlatT -> BuiltinFlatT -> Bool
(BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool) -> Eq BuiltinFlatT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinFlatT -> BuiltinFlatT -> Bool
== :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c/= :: BuiltinFlatT -> BuiltinFlatT -> Bool
/= :: BuiltinFlatT -> BuiltinFlatT -> Bool
Eq,
      -- | @since 1.0.0
      Eq BuiltinFlatT
Eq BuiltinFlatT =>
(BuiltinFlatT -> BuiltinFlatT -> Ordering)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT)
-> (BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT)
-> Ord BuiltinFlatT
BuiltinFlatT -> BuiltinFlatT -> Bool
BuiltinFlatT -> BuiltinFlatT -> Ordering
BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
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 :: BuiltinFlatT -> BuiltinFlatT -> Ordering
compare :: BuiltinFlatT -> BuiltinFlatT -> Ordering
$c< :: BuiltinFlatT -> BuiltinFlatT -> Bool
< :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c<= :: BuiltinFlatT -> BuiltinFlatT -> Bool
<= :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c> :: BuiltinFlatT -> BuiltinFlatT -> Bool
> :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c>= :: BuiltinFlatT -> BuiltinFlatT -> Bool
>= :: BuiltinFlatT -> BuiltinFlatT -> Bool
$cmax :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
max :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
$cmin :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
min :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
Ord,
      -- | @since 1.0.0
      Int -> BuiltinFlatT -> ShowS
[BuiltinFlatT] -> ShowS
BuiltinFlatT -> String
(Int -> BuiltinFlatT -> ShowS)
-> (BuiltinFlatT -> String)
-> ([BuiltinFlatT] -> ShowS)
-> Show BuiltinFlatT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinFlatT -> ShowS
showsPrec :: Int -> BuiltinFlatT -> ShowS
$cshow :: BuiltinFlatT -> String
show :: BuiltinFlatT -> String
$cshowList :: [BuiltinFlatT] -> ShowS
showList :: [BuiltinFlatT] -> ShowS
Show
    )

-- Helpers

newtype ScopeBoundary = ScopeBoundary Int
  deriving (Int -> ScopeBoundary -> ShowS
[ScopeBoundary] -> ShowS
ScopeBoundary -> String
(Int -> ScopeBoundary -> ShowS)
-> (ScopeBoundary -> String)
-> ([ScopeBoundary] -> ShowS)
-> Show ScopeBoundary
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScopeBoundary -> ShowS
showsPrec :: Int -> ScopeBoundary -> ShowS
$cshow :: ScopeBoundary -> String
show :: ScopeBoundary -> String
$cshowList :: [ScopeBoundary] -> ShowS
showList :: [ScopeBoundary] -> ShowS
Show, ScopeBoundary -> ScopeBoundary -> Bool
(ScopeBoundary -> ScopeBoundary -> Bool)
-> (ScopeBoundary -> ScopeBoundary -> Bool) -> Eq ScopeBoundary
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScopeBoundary -> ScopeBoundary -> Bool
== :: ScopeBoundary -> ScopeBoundary -> Bool
$c/= :: ScopeBoundary -> ScopeBoundary -> Bool
/= :: ScopeBoundary -> ScopeBoundary -> Bool
Eq, Eq ScopeBoundary
Eq ScopeBoundary =>
(ScopeBoundary -> ScopeBoundary -> Ordering)
-> (ScopeBoundary -> ScopeBoundary -> Bool)
-> (ScopeBoundary -> ScopeBoundary -> Bool)
-> (ScopeBoundary -> ScopeBoundary -> Bool)
-> (ScopeBoundary -> ScopeBoundary -> Bool)
-> (ScopeBoundary -> ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary -> ScopeBoundary)
-> Ord ScopeBoundary
ScopeBoundary -> ScopeBoundary -> Bool
ScopeBoundary -> ScopeBoundary -> Ordering
ScopeBoundary -> ScopeBoundary -> ScopeBoundary
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 :: ScopeBoundary -> ScopeBoundary -> Ordering
compare :: ScopeBoundary -> ScopeBoundary -> Ordering
$c< :: ScopeBoundary -> ScopeBoundary -> Bool
< :: ScopeBoundary -> ScopeBoundary -> Bool
$c<= :: ScopeBoundary -> ScopeBoundary -> Bool
<= :: ScopeBoundary -> ScopeBoundary -> Bool
$c> :: ScopeBoundary -> ScopeBoundary -> Bool
> :: ScopeBoundary -> ScopeBoundary -> Bool
$c>= :: ScopeBoundary -> ScopeBoundary -> Bool
>= :: ScopeBoundary -> ScopeBoundary -> Bool
$cmax :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
max :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
$cmin :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
min :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
Ord, Integer -> ScopeBoundary
ScopeBoundary -> ScopeBoundary
ScopeBoundary -> ScopeBoundary -> ScopeBoundary
(ScopeBoundary -> ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary)
-> (ScopeBoundary -> ScopeBoundary)
-> (Integer -> ScopeBoundary)
-> Num ScopeBoundary
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
+ :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
$c- :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
- :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
$c* :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
* :: ScopeBoundary -> ScopeBoundary -> ScopeBoundary
$cnegate :: ScopeBoundary -> ScopeBoundary
negate :: ScopeBoundary -> ScopeBoundary
$cabs :: ScopeBoundary -> ScopeBoundary
abs :: ScopeBoundary -> ScopeBoundary
$csignum :: ScopeBoundary -> ScopeBoundary
signum :: ScopeBoundary -> ScopeBoundary
$cfromInteger :: Integer -> ScopeBoundary
fromInteger :: Integer -> ScopeBoundary
Num) via Int

-- Keeping the field names for clarity even if we don't use them
data PrettyContext (ann :: Type)
  = PrettyContext
  { forall ann.
PrettyContext ann -> Map ScopeBoundary (Vector (Doc ann))
_boundIdents :: Map ScopeBoundary (Vector (Doc ann)),
    forall ann. PrettyContext ann -> ScopeBoundary
_currentScope :: ScopeBoundary,
    forall ann. PrettyContext ann -> [Doc ann]
_varStream :: [Doc ann]
  }

instance
  (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) =>
  LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (PrettyContext ann) (PrettyContext ann) a b
labelOptic =
    (PrettyContext ann -> a)
-> (PrettyContext ann -> b -> PrettyContext ann)
-> Lens (PrettyContext ann) (PrettyContext ann) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
x ScopeBoundary
_ [Doc ann]
_) -> a
Map ScopeBoundary (Vector (Doc ann))
x)
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
_ ScopeBoundary
y [Doc ann]
z) b
x -> Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
forall ann.
Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
PrettyContext b
Map ScopeBoundary (Vector (Doc ann))
x ScopeBoundary
y [Doc ann]
z)

instance
  (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) =>
  LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (PrettyContext ann) (PrettyContext ann) a b
labelOptic =
    (PrettyContext ann -> a)
-> (PrettyContext ann -> b -> PrettyContext ann)
-> Lens (PrettyContext ann) (PrettyContext ann) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
_ ScopeBoundary
x [Doc ann]
_) -> a
ScopeBoundary
x)
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
x ScopeBoundary
_ [Doc ann]
z) b
y -> Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
forall ann.
Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
PrettyContext Map ScopeBoundary (Vector (Doc ann))
x b
ScopeBoundary
y [Doc ann]
z)

instance
  (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) =>
  LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (PrettyContext ann) (PrettyContext ann) a b
labelOptic =
    (PrettyContext ann -> a)
-> (PrettyContext ann -> b -> PrettyContext ann)
-> Lens (PrettyContext ann) (PrettyContext ann) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
_ ScopeBoundary
_ [Doc ann]
x) -> a
[Doc ann]
x)
      (\(PrettyContext Map ScopeBoundary (Vector (Doc ann))
x ScopeBoundary
y [Doc ann]
_) b
z -> Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
forall ann.
Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
PrettyContext Map ScopeBoundary (Vector (Doc ann))
x ScopeBoundary
y b
[Doc ann]
z)

-- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail
newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a)
  deriving
    ( (forall a b. (a -> b) -> PrettyM ann a -> PrettyM ann b)
-> (forall a b. a -> PrettyM ann b -> PrettyM ann a)
-> Functor (PrettyM ann)
forall a b. a -> PrettyM ann b -> PrettyM ann a
forall a b. (a -> b) -> PrettyM ann a -> PrettyM ann b
forall ann a b. a -> PrettyM ann b -> PrettyM ann a
forall ann a b. (a -> b) -> PrettyM ann a -> PrettyM ann b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall ann a b. (a -> b) -> PrettyM ann a -> PrettyM ann b
fmap :: forall a b. (a -> b) -> PrettyM ann a -> PrettyM ann b
$c<$ :: forall ann a b. a -> PrettyM ann b -> PrettyM ann a
<$ :: forall a b. a -> PrettyM ann b -> PrettyM ann a
Functor,
      Functor (PrettyM ann)
Functor (PrettyM ann) =>
(forall a. a -> PrettyM ann a)
-> (forall a b.
    PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b)
-> (forall a b c.
    (a -> b -> c) -> PrettyM ann a -> PrettyM ann b -> PrettyM ann c)
-> (forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b)
-> (forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann a)
-> Applicative (PrettyM ann)
forall ann. Functor (PrettyM ann)
forall a. a -> PrettyM ann a
forall ann a. a -> PrettyM ann a
forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann a
forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
forall a b. PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b
forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann a
forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
forall ann a b.
PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b
forall a b c.
(a -> b -> c) -> PrettyM ann a -> PrettyM ann b -> PrettyM ann c
forall ann a b c.
(a -> b -> c) -> PrettyM ann a -> PrettyM ann b -> PrettyM ann c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall ann a. a -> PrettyM ann a
pure :: forall a. a -> PrettyM ann a
$c<*> :: forall ann a b.
PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b
<*> :: forall a b. PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b
$cliftA2 :: forall ann a b c.
(a -> b -> c) -> PrettyM ann a -> PrettyM ann b -> PrettyM ann c
liftA2 :: forall a b c.
(a -> b -> c) -> PrettyM ann a -> PrettyM ann b -> PrettyM ann c
$c*> :: forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
*> :: forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
$c<* :: forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann a
<* :: forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann a
Applicative,
      Applicative (PrettyM ann)
Applicative (PrettyM ann) =>
(forall a b.
 PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b)
-> (forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b)
-> (forall a. a -> PrettyM ann a)
-> Monad (PrettyM ann)
forall ann. Applicative (PrettyM ann)
forall a. a -> PrettyM ann a
forall ann a. a -> PrettyM ann a
forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
forall a b. PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b
forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
forall ann a b.
PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall ann a b.
PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b
>>= :: forall a b. PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b
$c>> :: forall ann a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
>> :: forall a b. PrettyM ann a -> PrettyM ann b -> PrettyM ann b
$creturn :: forall ann a. a -> PrettyM ann a
return :: forall a. a -> PrettyM ann a
Monad,
      MonadReader (PrettyContext ann)
    )
    via (Reader (PrettyContext ann))

runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a
runPrettyM :: forall ann a. PrettyM ann a -> a
runPrettyM (PrettyM Reader (PrettyContext ann) a
ma) = Reader (PrettyContext ann) a -> PrettyContext ann -> a
forall r a. Reader r a -> r -> a
runReader Reader (PrettyContext ann) a
ma (Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
forall ann.
Map ScopeBoundary (Vector (Doc ann))
-> ScopeBoundary -> [Doc ann] -> PrettyContext ann
PrettyContext Map ScopeBoundary (Vector (Doc ann))
forall a. Monoid a => a
mempty ScopeBoundary
0 [Doc ann]
infiniteVars)
  where
    -- Lazily generated infinite list of variables. Will start with a, b, c...
    -- and cycle around to a1, b2, c3 etc.
    -- We could do something more sophisticated but this should work.
    infiniteVars :: [Doc ann]
    infiniteVars :: [Doc ann]
infiniteVars =
      let aToZ :: String
aToZ = [Char
'a' .. Char
'z']
          intStrings :: [String]
intStrings = (String
"" String -> String -> [String]
forall a b. a -> [b] -> [a]
forall (f :: Type -> Type) a b. Functor f => a -> f b -> f a
<$ String
aToZ) [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> (Integer -> String) -> [Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show @Integer) [Integer
0 ..]
       in (Char -> String -> Doc ann) -> String -> [String] -> [Doc ann]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Char
x String
xs -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Char
x Char -> ShowS
forall a. a -> [a] -> [a]
: String
xs)) String
aToZ [String]
intStrings

prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext :: forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext (CompT Count "tyvar"
count (CompTBody NonEmptyVector (ValT Renamed)
funArgs))
  | Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy NonEmptyVector (ValT Renamed)
funArgs
  | Bool
otherwise = Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall ann a.
Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
bindVars Count "tyvar"
count ((Vector (Doc ann) -> PrettyM ann (Doc ann))
 -> PrettyM ann (Doc ann))
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ \Vector (Doc ann)
newVars -> do
      Doc ann
funTy <- NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy NonEmptyVector (ValT Renamed)
funArgs
      Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Vector (Doc ann) -> Doc ann -> Doc ann
forall ann. Vector (Doc ann) -> Doc ann -> Doc ann
mkForall Vector (Doc ann)
newVars Doc ann
funTy

prettyFunTy ::
  forall (ann :: Type).
  NonEmptyVector (ValT Renamed) ->
  PrettyM ann (Doc ann)
prettyFunTy :: forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy NonEmptyVector (ValT Renamed)
args = case NonEmptyVector (ValT Renamed)
-> (ValT Renamed, Vector (ValT Renamed))
forall a. NonEmptyVector a -> (a, Vector a)
NonEmpty.uncons NonEmptyVector (ValT Renamed)
args of
  (ValT Renamed
arg, Vector (ValT Renamed)
rest) -> (PrettyM ann (Doc ann) -> ValT Renamed -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
-> Vector (ValT Renamed)
-> PrettyM ann (Doc ann)
forall a b. (a -> b -> a) -> a -> Vector b -> a
Vector.foldl' PrettyM ann (Doc ann) -> ValT Renamed -> PrettyM ann (Doc ann)
go ((Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>) (Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValT Renamed -> PrettyM ann (Doc ann)
prettyArg ValT Renamed
arg) Vector (ValT Renamed)
rest
  where
    go ::
      PrettyM ann (Doc ann) ->
      ValT Renamed ->
      PrettyM ann (Doc ann)
    go :: PrettyM ann (Doc ann) -> ValT Renamed -> PrettyM ann (Doc ann)
go PrettyM ann (Doc ann)
acc ValT Renamed
t = (\Doc ann
x Doc ann
y -> Doc ann
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
y) (Doc ann -> Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann -> Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValT Renamed -> PrettyM ann (Doc ann)
prettyArg ValT Renamed
t PrettyM ann (Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann)
forall a b. PrettyM ann (a -> b) -> PrettyM ann a -> PrettyM ann b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> PrettyM ann (Doc ann)
acc
    prettyArg :: ValT Renamed -> PrettyM ann (Doc ann)
    prettyArg :: ValT Renamed -> PrettyM ann (Doc ann)
prettyArg ValT Renamed
vt =
      let prettyVT :: PrettyM ann (Doc ann)
prettyVT = ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext ValT Renamed
vt
       in if ValT Renamed -> Bool
forall a. ValT a -> Bool
isSimpleValT ValT Renamed
vt
            then PrettyM ann (Doc ann)
prettyVT
            else Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> PrettyM ann (Doc ann)
prettyVT

bindVars ::
  forall (ann :: Type) (a :: Type).
  Count "tyvar" ->
  (Vector (Doc ann) -> PrettyM ann a) ->
  PrettyM ann a
bindVars :: forall ann a.
Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
bindVars Count "tyvar"
count' Vector (Doc ann) -> PrettyM ann a
act
  | Int
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = PrettyM ann a -> PrettyM ann a
crossBoundary (Vector (Doc ann) -> PrettyM ann a
act Vector (Doc ann)
forall a. Vector a
Vector.empty)
  | Bool
otherwise = PrettyM ann a -> PrettyM ann a
crossBoundary (PrettyM ann a -> PrettyM ann a) -> PrettyM ann a -> PrettyM ann a
forall a b. (a -> b) -> a -> b
$ do
      ScopeBoundary
here <- (PrettyContext ann -> ScopeBoundary) -> PrettyM ann ScopeBoundary
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  ScopeBoundary
  ScopeBoundary
-> PrettyContext ann -> ScopeBoundary
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  ScopeBoundary
  ScopeBoundary
#currentScope)
      Int -> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
forall ann a.
Int -> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
withFreshVarNames Int
count ((Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a)
-> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
forall a b. (a -> b) -> a -> b
$ \Vector (Doc ann)
newBoundVars ->
        (PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall a.
(PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  (Map ScopeBoundary (Vector (Doc ann)))
  (Map ScopeBoundary (Vector (Doc ann)))
-> (Map ScopeBoundary (Vector (Doc ann))
    -> Map ScopeBoundary (Vector (Doc ann)))
-> PrettyContext ann
-> PrettyContext ann
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  (Map ScopeBoundary (Vector (Doc ann)))
  (Map ScopeBoundary (Vector (Doc ann)))
#boundIdents (ScopeBoundary
-> Vector (Doc ann)
-> Map ScopeBoundary (Vector (Doc ann))
-> Map ScopeBoundary (Vector (Doc ann))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ScopeBoundary
here Vector (Doc ann)
newBoundVars)) (Vector (Doc ann) -> PrettyM ann a
act Vector (Doc ann)
newBoundVars)
  where
    -- Increment the current scope
    crossBoundary :: PrettyM ann a -> PrettyM ann a
    crossBoundary :: PrettyM ann a -> PrettyM ann a
crossBoundary = (PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall a.
(PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  ScopeBoundary
  ScopeBoundary
-> (ScopeBoundary -> ScopeBoundary)
-> PrettyContext ann
-> PrettyContext ann
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> (a -> b) -> s -> t
over Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  ScopeBoundary
  ScopeBoundary
#currentScope (ScopeBoundary -> ScopeBoundary -> ScopeBoundary
forall a. Num a => a -> a -> a
+ ScopeBoundary
1))
    count :: Int
    count :: Int
count = Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
count'

mkForall ::
  forall (ann :: Type).
  Vector (Doc ann) ->
  Doc ann ->
  Doc ann
mkForall :: forall ann. Vector (Doc ann) -> Doc ann -> Doc ann
mkForall Vector (Doc ann)
tvars Doc ann
funTyBody =
  if Vector (Doc ann) -> Bool
forall a. Vector a -> Bool
Vector.null Vector (Doc ann)
tvars
    then Doc ann
funTyBody
    else Doc ann
"forall" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList Vector (Doc ann)
tvars) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
funTyBody

-- I.e. can we omit parens and get something unambiguous? This might be overly aggressive w/ parens but that's OK
isSimpleValT :: forall (a :: Type). ValT a -> Bool
isSimpleValT :: forall a. ValT a -> Bool
isSimpleValT = \case
  ThunkT CompT a
thunk -> CompT a -> Bool
isSimpleCompT CompT a
thunk
  ValT a
_ -> Bool
True
  where
    isSimpleCompT :: CompT a -> Bool
    isSimpleCompT :: CompT a -> Bool
isSimpleCompT (CompT Count "tyvar"
count (CompTBody NonEmptyVector (ValT a)
args)) =
      Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& NonEmptyVector (ValT a) -> Int
forall a. NonEmptyVector a -> Int
NonEmpty.length NonEmptyVector (ValT a)
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1

prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext :: forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext = \case
  Abstraction Renamed
abstr -> Renamed -> PrettyM ann (Doc ann)
forall ann. Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext Renamed
abstr
  ThunkT CompT Renamed
compT -> CompT Renamed -> PrettyM ann (Doc ann)
forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext CompT Renamed
compT
  BuiltinFlat BuiltinFlatT
biFlat -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow BuiltinFlatT
biFlat

-- Generate N fresh var names and use the supplied monadic function to do something with them.
withFreshVarNames ::
  forall (ann :: Type) (a :: Type).
  Int ->
  (Vector (Doc ann) -> PrettyM ann a) ->
  PrettyM ann a
withFreshVarNames :: forall ann a.
Int -> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
withFreshVarNames Int
n Vector (Doc ann) -> PrettyM ann a
act = do
  [Doc ann]
stream <- (PrettyContext ann -> [Doc ann]) -> PrettyM ann [Doc ann]
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx (PrettyContext ann) [Doc ann]
-> PrettyContext ann -> [Doc ann]
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (PrettyContext ann) [Doc ann]
#varStream)
  let ([Doc ann]
used, [Doc ann]
rest) = Int -> [Doc ann] -> ([Doc ann], [Doc ann])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Doc ann]
stream
  (PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall a.
(PrettyContext ann -> PrettyContext ann)
-> PrettyM ann a -> PrettyM ann a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Optic' A_Lens NoIx (PrettyContext ann) [Doc ann]
-> [Doc ann] -> PrettyContext ann -> PrettyContext ann
forall k (is :: IxList) s t a b.
Is k A_Setter =>
Optic k is s t a b -> b -> s -> t
set Optic' A_Lens NoIx (PrettyContext ann) [Doc ann]
#varStream [Doc ann]
rest) (PrettyM ann a -> PrettyM ann a)
-> ([Doc ann] -> PrettyM ann a) -> [Doc ann] -> PrettyM ann a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Doc ann) -> PrettyM ann a
act (Vector (Doc ann) -> PrettyM ann a)
-> ([Doc ann] -> Vector (Doc ann)) -> [Doc ann] -> PrettyM ann a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Item (Vector (Doc ann))] -> Vector (Doc ann)
forall l. IsList l => Int -> [Item l] -> l
fromListN Int
n ([Doc ann] -> PrettyM ann a) -> [Doc ann] -> PrettyM ann a
forall a b. (a -> b) -> a -> b
$ [Doc ann]
used

prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext :: forall ann. Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext = \case
  Rigid Int
offset Index "tyvar"
index -> Int -> Index "tyvar" -> PrettyM ann (Doc ann)
forall ann. Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction Int
offset Index "tyvar"
index
  Unifiable Index "tyvar"
i -> Int -> Index "tyvar" -> PrettyM ann (Doc ann)
forall ann. Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction Int
0 Index "tyvar"
i
  Wildcard Word64
w64 Int
offset Index "tyvar"
i -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
offset Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"_" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Word64
w64 Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"#" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
i)

lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction :: forall ann. Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction Int
offset Index "tyvar"
argIndex = do
  let scopeOffset :: ScopeBoundary
scopeOffset = Int -> ScopeBoundary
ScopeBoundary Int
offset
  let argIndex' :: Int
argIndex' = Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
argIndex
  ScopeBoundary
here <- (PrettyContext ann -> ScopeBoundary) -> PrettyM ann ScopeBoundary
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' A_Lens NoIx (PrettyContext ann) ScopeBoundary
-> PrettyContext ann -> ScopeBoundary
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' A_Lens NoIx (PrettyContext ann) ScopeBoundary
#currentScope)
  (PrettyContext ann -> Maybe (Doc ann))
-> PrettyM ann (Maybe (Doc ann))
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Optic' An_AffineTraversal NoIx (PrettyContext ann) (Doc ann)
-> PrettyContext ann -> Maybe (Doc ann)
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview (Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  (Map ScopeBoundary (Vector (Doc ann)))
  (Map ScopeBoundary (Vector (Doc ann)))
#boundIdents Optic
  A_Lens
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  (Map ScopeBoundary (Vector (Doc ann)))
  (Map ScopeBoundary (Vector (Doc ann)))
-> Optic
     (IxKind (Map ScopeBoundary (Vector (Doc ann))))
     NoIx
     (Map ScopeBoundary (Vector (Doc ann)))
     (Map ScopeBoundary (Vector (Doc ann)))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
-> Optic
     An_AffineTraversal
     NoIx
     (PrettyContext ann)
     (PrettyContext ann)
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (Map ScopeBoundary (Vector (Doc ann)))
-> Optic
     (IxKind (Map ScopeBoundary (Vector (Doc ann))))
     NoIx
     (Map ScopeBoundary (Vector (Doc ann)))
     (Map ScopeBoundary (Vector (Doc ann)))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix (ScopeBoundary
here ScopeBoundary -> ScopeBoundary -> ScopeBoundary
forall a. Num a => a -> a -> a
+ ScopeBoundary
scopeOffset) Optic
  An_AffineTraversal
  NoIx
  (PrettyContext ann)
  (PrettyContext ann)
  (IxValue (Map ScopeBoundary (Vector (Doc ann))))
  (IxValue (Map ScopeBoundary (Vector (Doc ann))))
-> Optic
     (IxKind (IxValue (Map ScopeBoundary (Vector (Doc ann)))))
     NoIx
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (Doc ann)
     (Doc ann)
-> Optic' An_AffineTraversal NoIx (PrettyContext ann) (Doc ann)
forall k l m (is :: IxList) (js :: IxList) (ks :: IxList) s t u v a
       b.
(JoinKinds k l m, AppendIndices is js ks) =>
Optic k is s t u v -> Optic l js u v a b -> Optic m ks s t a b
% Index (IxValue (Map ScopeBoundary (Vector (Doc ann))))
-> Optic'
     (IxKind (IxValue (Map ScopeBoundary (Vector (Doc ann)))))
     NoIx
     (IxValue (Map ScopeBoundary (Vector (Doc ann))))
     (IxValue (IxValue (Map ScopeBoundary (Vector (Doc ann)))))
forall m. Ixed m => Index m -> Optic' (IxKind m) NoIx m (IxValue m)
ix Int
Index (IxValue (Map ScopeBoundary (Vector (Doc ann))))
argIndex')) PrettyM ann (Maybe (Doc ann))
-> (Maybe (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall a b. PrettyM ann a -> (a -> PrettyM ann b) -> PrettyM ann b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe (Doc ann)
Nothing ->
      -- TODO: actual error reporting
      String -> PrettyM ann (Doc ann)
forall a. HasCallStack => String -> a
error (String -> PrettyM ann (Doc ann))
-> String -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$
        String
"Internal error: The encountered a variable at arg index "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
argIndex'
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" with true level "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ScopeBoundary -> String
forall a. Show a => a -> String
show ScopeBoundary
scopeOffset
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" but could not locate the corresponding pretty form at scope level "
          String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ScopeBoundary -> String
forall a. Show a => a -> String
show ScopeBoundary
here
    Just Doc ann
res' -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
res'