module U.Codebase.Type where

import Control.Monad.Writer.Strict qualified as Writer
import Data.Maybe qualified as Maybe
import Data.Set qualified as Set
import U.Codebase.Kind (Kind)
import U.Codebase.Reference (Reference, Reference')
import U.Core.ABT qualified as ABT
import Unison.Hash (Hash)
import Unison.Prelude
import Unsafe.Coerce (unsafeCoerce)

-- | For standalone types, like those in Term.Ann
type FT = F' Reference

-- | For potentially recursive types, like those in DataDeclaration
type FD = F' (Reference' Text (Maybe Hash))

data F' r a
  = Ref r
  | Arrow a a
  | Ann a Kind
  | App a a
  | Effect a a
  | Effects [a]
  | Forall a
  | IntroOuter a -- binder like ∀, used to introduce variables that are
  -- bound by outer type signatures, to support scoped type
  -- variables
  deriving ((forall m. Monoid m => F' r m -> m)
-> (forall m a. Monoid m => (a -> m) -> F' r a -> m)
-> (forall m a. Monoid m => (a -> m) -> F' r a -> m)
-> (forall a b. (a -> b -> b) -> b -> F' r a -> b)
-> (forall a b. (a -> b -> b) -> b -> F' r a -> b)
-> (forall b a. (b -> a -> b) -> b -> F' r a -> b)
-> (forall b a. (b -> a -> b) -> b -> F' r a -> b)
-> (forall a. (a -> a -> a) -> F' r a -> a)
-> (forall a. (a -> a -> a) -> F' r a -> a)
-> (forall a. F' r a -> [a])
-> (forall a. F' r a -> Bool)
-> (forall a. F' r a -> Int)
-> (forall a. Eq a => a -> F' r a -> Bool)
-> (forall a. Ord a => F' r a -> a)
-> (forall a. Ord a => F' r a -> a)
-> (forall a. Num a => F' r a -> a)
-> (forall a. Num a => F' r a -> a)
-> Foldable (F' r)
forall a. Eq a => a -> F' r a -> Bool
forall a. Num a => F' r a -> a
forall a. Ord a => F' r a -> a
forall m. Monoid m => F' r m -> m
forall a. F' r a -> Bool
forall a. F' r a -> Int
forall a. F' r a -> [a]
forall a. (a -> a -> a) -> F' r a -> a
forall r a. Eq a => a -> F' r a -> Bool
forall r a. Num a => F' r a -> a
forall r a. Ord a => F' r a -> a
forall m a. Monoid m => (a -> m) -> F' r a -> m
forall r m. Monoid m => F' r m -> m
forall r a. F' r a -> Bool
forall r a. F' r a -> Int
forall r a. F' r a -> [a]
forall b a. (b -> a -> b) -> b -> F' r a -> b
forall a b. (a -> b -> b) -> b -> F' r a -> b
forall r a. (a -> a -> a) -> F' r a -> a
forall r m a. Monoid m => (a -> m) -> F' r a -> m
forall r b a. (b -> a -> b) -> b -> F' r a -> b
forall r a b. (a -> b -> b) -> b -> F' r 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 r m. Monoid m => F' r m -> m
fold :: forall m. Monoid m => F' r m -> m
$cfoldMap :: forall r m a. Monoid m => (a -> m) -> F' r a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> F' r a -> m
$cfoldMap' :: forall r m a. Monoid m => (a -> m) -> F' r a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> F' r a -> m
$cfoldr :: forall r a b. (a -> b -> b) -> b -> F' r a -> b
foldr :: forall a b. (a -> b -> b) -> b -> F' r a -> b
$cfoldr' :: forall r a b. (a -> b -> b) -> b -> F' r a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> F' r a -> b
$cfoldl :: forall r b a. (b -> a -> b) -> b -> F' r a -> b
foldl :: forall b a. (b -> a -> b) -> b -> F' r a -> b
$cfoldl' :: forall r b a. (b -> a -> b) -> b -> F' r a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> F' r a -> b
$cfoldr1 :: forall r a. (a -> a -> a) -> F' r a -> a
foldr1 :: forall a. (a -> a -> a) -> F' r a -> a
$cfoldl1 :: forall r a. (a -> a -> a) -> F' r a -> a
foldl1 :: forall a. (a -> a -> a) -> F' r a -> a
$ctoList :: forall r a. F' r a -> [a]
toList :: forall a. F' r a -> [a]
$cnull :: forall r a. F' r a -> Bool
null :: forall a. F' r a -> Bool
$clength :: forall r a. F' r a -> Int
length :: forall a. F' r a -> Int
$celem :: forall r a. Eq a => a -> F' r a -> Bool
elem :: forall a. Eq a => a -> F' r a -> Bool
$cmaximum :: forall r a. Ord a => F' r a -> a
maximum :: forall a. Ord a => F' r a -> a
$cminimum :: forall r a. Ord a => F' r a -> a
minimum :: forall a. Ord a => F' r a -> a
$csum :: forall r a. Num a => F' r a -> a
sum :: forall a. Num a => F' r a -> a
$cproduct :: forall r a. Num a => F' r a -> a
product :: forall a. Num a => F' r a -> a
Foldable, (forall a b. (a -> b) -> F' r a -> F' r b)
-> (forall a b. a -> F' r b -> F' r a) -> Functor (F' r)
forall a b. a -> F' r b -> F' r a
forall a b. (a -> b) -> F' r a -> F' r b
forall r a b. a -> F' r b -> F' r a
forall r a b. (a -> b) -> F' r a -> F' r b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall r a b. (a -> b) -> F' r a -> F' r b
fmap :: forall a b. (a -> b) -> F' r a -> F' r b
$c<$ :: forall r a b. a -> F' r b -> F' r a
<$ :: forall a b. a -> F' r b -> F' r a
Functor, F' r a -> F' r a -> Bool
(F' r a -> F' r a -> Bool)
-> (F' r a -> F' r a -> Bool) -> Eq (F' r a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall r a. (Eq r, Eq a) => F' r a -> F' r a -> Bool
$c== :: forall r a. (Eq r, Eq a) => F' r a -> F' r a -> Bool
== :: F' r a -> F' r a -> Bool
$c/= :: forall r a. (Eq r, Eq a) => F' r a -> F' r a -> Bool
/= :: F' r a -> F' r a -> Bool
Eq, Eq (F' r a)
Eq (F' r a) =>
(F' r a -> F' r a -> Ordering)
-> (F' r a -> F' r a -> Bool)
-> (F' r a -> F' r a -> Bool)
-> (F' r a -> F' r a -> Bool)
-> (F' r a -> F' r a -> Bool)
-> (F' r a -> F' r a -> F' r a)
-> (F' r a -> F' r a -> F' r a)
-> Ord (F' r a)
F' r a -> F' r a -> Bool
F' r a -> F' r a -> Ordering
F' r a -> F' r a -> F' r 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 r a. (Ord r, Ord a) => Eq (F' r a)
forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Bool
forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Ordering
forall r a. (Ord r, Ord a) => F' r a -> F' r a -> F' r a
$ccompare :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Ordering
compare :: F' r a -> F' r a -> Ordering
$c< :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Bool
< :: F' r a -> F' r a -> Bool
$c<= :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Bool
<= :: F' r a -> F' r a -> Bool
$c> :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Bool
> :: F' r a -> F' r a -> Bool
$c>= :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> Bool
>= :: F' r a -> F' r a -> Bool
$cmax :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> F' r a
max :: F' r a -> F' r a -> F' r a
$cmin :: forall r a. (Ord r, Ord a) => F' r a -> F' r a -> F' r a
min :: F' r a -> F' r a -> F' r a
Ord, Int -> F' r a -> ShowS
[F' r a] -> ShowS
F' r a -> String
(Int -> F' r a -> ShowS)
-> (F' r a -> String) -> ([F' r a] -> ShowS) -> Show (F' r a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall r a. (Show r, Show a) => Int -> F' r a -> ShowS
forall r a. (Show r, Show a) => [F' r a] -> ShowS
forall r a. (Show r, Show a) => F' r a -> String
$cshowsPrec :: forall r a. (Show r, Show a) => Int -> F' r a -> ShowS
showsPrec :: Int -> F' r a -> ShowS
$cshow :: forall r a. (Show r, Show a) => F' r a -> String
show :: F' r a -> String
$cshowList :: forall r a. (Show r, Show a) => [F' r a] -> ShowS
showList :: [F' r a] -> ShowS
Show, Functor (F' r)
Foldable (F' r)
(Functor (F' r), Foldable (F' r)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> F' r a -> f (F' r b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    F' r (f a) -> f (F' r a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> F' r a -> m (F' r b))
-> (forall (m :: * -> *) a. Monad m => F' r (m a) -> m (F' r a))
-> Traversable (F' r)
forall r. Functor (F' r)
forall r. Foldable (F' r)
forall r (m :: * -> *) a. Monad m => F' r (m a) -> m (F' r a)
forall r (f :: * -> *) a. Applicative f => F' r (f a) -> f (F' r a)
forall r (m :: * -> *) a b.
Monad m =>
(a -> m b) -> F' r a -> m (F' r b)
forall r (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F' r a -> f (F' r b)
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 => F' r (m a) -> m (F' r a)
forall (f :: * -> *) a. Applicative f => F' r (f a) -> f (F' r a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> F' r a -> m (F' r b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F' r a -> f (F' r b)
$ctraverse :: forall r (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F' r a -> f (F' r b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F' r a -> f (F' r b)
$csequenceA :: forall r (f :: * -> *) a. Applicative f => F' r (f a) -> f (F' r a)
sequenceA :: forall (f :: * -> *) a. Applicative f => F' r (f a) -> f (F' r a)
$cmapM :: forall r (m :: * -> *) a b.
Monad m =>
(a -> m b) -> F' r a -> m (F' r b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> F' r a -> m (F' r b)
$csequence :: forall r (m :: * -> *) a. Monad m => F' r (m a) -> m (F' r a)
sequence :: forall (m :: * -> *) a. Monad m => F' r (m a) -> m (F' r a)
Traversable)

-- | Non-recursive type
type TypeT v = ABT.Term FT v ()

-- | Potentially-recursive type
type TypeD v = ABT.Term FD v ()

type TypeR r v = ABT.Term (F' r) v ()

rmap :: (Ord v) => (r -> r') -> ABT.Term (F' r) v a -> ABT.Term (F' r') v a
rmap :: forall v r r' a.
Ord v =>
(r -> r') -> Term (F' r) v a -> Term (F' r') v a
rmap r -> r'
f = Identity (Term (F' r') v a) -> Term (F' r') v a
forall a. Identity a -> a
runIdentity (Identity (Term (F' r') v a) -> Term (F' r') v a)
-> (Term (F' r) v a -> Identity (Term (F' r') v a))
-> Term (F' r) v a
-> Term (F' r') v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r -> Identity r')
-> Term (F' r) v a -> Identity (Term (F' r') v a)
forall v (f :: * -> *) r r' a.
(Ord v, Monad f) =>
(r -> f r') -> Term (F' r) v a -> f (Term (F' r') v a)
rmapM (r' -> Identity r'
forall a. a -> Identity a
Identity (r' -> Identity r') -> (r -> r') -> r -> Identity r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. r -> r'
f)

rmapM ::
  (Ord v, Monad f) =>
  (r -> f r') ->
  ABT.Term (F' r) v a ->
  f (ABT.Term (F' r') v a)
rmapM :: forall v (f :: * -> *) r r' a.
(Ord v, Monad f) =>
(r -> f r') -> Term (F' r) v a -> f (Term (F' r') v a)
rmapM r -> f r'
f = (forall a1. F' r a1 -> f (F' r' a1))
-> Term (F' r) v a -> f (Term (F' r') v a)
forall v (m :: * -> *) (g :: * -> *) (f :: * -> *) a.
(Ord v, Monad m, Traversable g) =>
(forall a1. f a1 -> m (g a1)) -> Term f v a -> m (Term g v a)
ABT.transformM \case
  Ref r
r -> r' -> F' r' a1
forall r a. r -> F' r a
Ref (r' -> F' r' a1) -> f r' -> f (F' r' a1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> r -> f r'
f r
r
  F' r a1
x -> F' r' a1 -> f (F' r' a1)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (F' r' a1 -> f (F' r' a1)) -> F' r' a1 -> f (F' r' a1)
forall a b. (a -> b) -> a -> b
$ F' r a1 -> F' r' a1
forall a b. a -> b
unsafeCoerce F' r a1
x

typeD2T :: (Ord v) => Hash -> TypeD v -> TypeT v
typeD2T :: forall v. Ord v => Hash -> TypeD v -> TypeT v
typeD2T Hash
h = (Reference' Text (Maybe Hash) -> Reference)
-> Term (F' (Reference' Text (Maybe Hash))) v ()
-> Term (F' Reference) v ()
forall v r r' a.
Ord v =>
(r -> r') -> Term (F' r) v a -> Term (F' r') v a
rmap ((Reference' Text (Maybe Hash) -> Reference)
 -> Term (F' (Reference' Text (Maybe Hash))) v ()
 -> Term (F' Reference) v ())
-> (Reference' Text (Maybe Hash) -> Reference)
-> Term (F' (Reference' Text (Maybe Hash))) v ()
-> Term (F' Reference) v ()
forall a b. (a -> b) -> a -> b
$ (Text -> Text)
-> (Maybe Hash -> Hash)
-> Reference' Text (Maybe Hash)
-> Reference
forall a b c d.
(a -> b) -> (c -> d) -> Reference' a c -> Reference' b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Text -> Text
forall a. a -> a
id ((Maybe Hash -> Hash) -> Reference' Text (Maybe Hash) -> Reference)
-> (Maybe Hash -> Hash)
-> Reference' Text (Maybe Hash)
-> Reference
forall a b. (a -> b) -> a -> b
$ Hash -> Maybe Hash -> Hash
forall a. a -> Maybe a -> a
Maybe.fromMaybe Hash
h

dependencies :: (Ord v, Ord r) => ABT.Term (F' r) v a -> Set r
dependencies :: forall v r a. (Ord v, Ord r) => Term (F' r) v a -> Set r
dependencies = Writer (Set r) (Term (F' r) v a) -> Set r
forall w a. Writer w a -> w
Writer.execWriter (Writer (Set r) (Term (F' r) v a) -> Set r)
-> (Term (F' r) v a -> Writer (Set r) (Term (F' r) v a))
-> Term (F' r) v a
-> Set r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (F' r (Term (F' r) v a)
 -> WriterT (Set r) Identity (F' r (Term (F' r) v a)))
-> Term (F' r) v a -> Writer (Set r) (Term (F' r) v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
ABT.visit' F' r (Term (F' r) v a)
-> WriterT (Set r) Identity (F' r (Term (F' r) v a))
forall r a. Ord r => F' r a -> Writer (Set r) (F' r a)
f
  where
    f :: (Ord r) => F' r a -> Writer.Writer (Set r) (F' r a)
    f :: forall r a. Ord r => F' r a -> Writer (Set r) (F' r a)
f t :: F' r a
t@(Ref r
r) = Set r -> WriterT (Set r) Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
Writer.tell (r -> Set r
forall a. a -> Set a
Set.singleton r
r) WriterT (Set r) Identity ()
-> F' r a -> WriterT (Set r) Identity (F' r a)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> F' r a
t
    f F' r a
t = F' r a -> WriterT (Set r) Identity (F' r a)
forall a. a -> WriterT (Set r) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure F' r a
t