{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS -Wno-orphans #-}
module Codec.Candid.TypTable where

import qualified Data.Map as M
import Control.Monad
import Control.Monad.State.Lazy
import Data.Void
import Prettyprinter
import Data.DList (singleton, DList)
import Data.Graph
import Data.Foldable

import Codec.Candid.Types

data SeqDesc where
    SeqDesc :: forall k. (Pretty k, Ord k) => M.Map k (Type k) -> [Type k] -> SeqDesc

instance Pretty SeqDesc where
    pretty :: forall ann. SeqDesc -> Doc ann
pretty (SeqDesc Map k (Type k)
m [Type k]
ts) = forall a ann. Pretty a => a -> Doc ann
pretty (forall k a. Map k a -> [(k, a)]
M.toList Map k (Type k)
m, [Type k]
ts)

data Ref k f  = Ref k (f (Ref k f))

instance Pretty k => Pretty (Ref k f) where
    pretty :: forall ann. Ref k f -> Doc ann
pretty (Ref k
k f (Ref k f)
_) = forall a ann. Pretty a => a -> Doc ann
pretty k
k
instance Eq k => Eq (Ref k f) where
    == :: Ref k f -> Ref k f -> Bool
(==) (Ref k
k1 f (Ref k f)
_) (Ref k
k2 f (Ref k f)
_) = forall a. Eq a => a -> a -> Bool
(==) k
k1 k
k2
instance Ord k => Ord (Ref k f) where
    compare :: Ref k f -> Ref k f -> Ordering
compare (Ref k
k1 f (Ref k f)
_) (Ref k
k2 f (Ref k f)
_) = forall a. Ord a => a -> a -> Ordering
compare k
k1 k
k2

unrollTypeTable :: SeqDesc -> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable :: forall r.
SeqDesc
-> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable (SeqDesc Map k (Type k)
m [Type k]
t) forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r
k = forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r
k (forall k.
Ord k =>
Map k (Type k) -> [Type k] -> [Type (Ref k Type)]
unrollTypeTable' Map k (Type k)
m [Type k]
t)

unrollTypeTable' :: forall k. Ord k => M.Map k (Type k) -> [Type k] -> [Type (Ref k Type)]
unrollTypeTable' :: forall k.
Ord k =>
Map k (Type k) -> [Type k] -> [Type (Ref k Type)]
unrollTypeTable' Map k (Type k)
m [Type k]
ts = [Type (Ref k Type)]
ts'
  where
    f :: k -> Type (Ref k Type)
    f :: k -> Type (Ref k Type)
f k
k = forall a. a -> Type a
RefT (forall k (f :: * -> *). k -> f (Ref k f) -> Ref k f
Ref k
k (Map k (Type (Ref k Type))
m' forall k a. Ord k => Map k a -> k -> a
M.! k
k))
    m' :: M.Map k (Type (Ref k Type))
    m' :: Map k (Type (Ref k Type))
m' = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= k -> Type (Ref k Type)
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map k (Type k)
m
    ts' :: [Type (Ref k Type)]
    ts' :: [Type (Ref k Type)]
ts' = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= k -> Type (Ref k Type)
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type k]
ts

buildSeqDesc :: forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> SeqDesc
buildSeqDesc :: forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> SeqDesc
buildSeqDesc [Type (Ref k Type)]
ts = forall k.
(Pretty k, Ord k) =>
Map k (Type k) -> [Type k] -> SeqDesc
SeqDesc Map k (Type k)
m [Type k]
ts'
  where
    ([Type k]
ts', Map k (Type k)
m) = forall s a. State s a -> s -> (a, s)
runState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Ref k Type -> State (Map k (Type k)) k
go) [Type (Ref k Type)]
ts) forall a. Monoid a => a
mempty

    go :: Ref k Type -> State (M.Map k (Type k)) k
    go :: Ref k Type -> State (Map k (Type k)) k
go (Ref k
k Type (Ref k Type)
t) = do
        Bool
seen <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Bool
M.member k
k)
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
seen forall a b. (a -> b) -> a -> b
$ mdo
            forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k Type k
t')
            Type k
t' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Ref k Type -> State (Map k (Type k)) k
go Type (Ref k Type)
t
            forall (m :: * -> *) a. Monad m => a -> m a
return ()
        forall (m :: * -> *) a. Monad m => a -> m a
return k
k

voidEmptyTypes :: SeqDesc -> SeqDesc
voidEmptyTypes :: SeqDesc -> SeqDesc
voidEmptyTypes (SeqDesc Map k (Type k)
m [Type k]
ts) = forall k.
(Pretty k, Ord k) =>
Map k (Type k) -> [Type k] -> SeqDesc
SeqDesc Map k (Type k)
m' [Type k]
ts
  where
    edges :: [(k, k, [k])]
edges = [ (k
k,k
k, forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall k. Type k -> DList k
underRec Type k
t)) | (k
k,Type k
t) <- forall k a. Map k a -> [(k, a)]
M.toList Map k (Type k)
m ]
    sccs :: [SCC k]
sccs = forall key node. Ord key => [(node, key, [key])] -> [SCC node]
stronglyConnComp [(k, k, [k])]
edges
    bad :: [k]
bad = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [k]
xs | CyclicSCC [k]
xs <- [SCC k]
sccs ]
    m' :: Map k (Type k)
m' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Map k (Type k)
m k
k -> forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert k
k forall a. Type a
EmptyT Map k (Type k)
m) Map k (Type k)
m [k]
bad


underRec :: Type k -> DList k
underRec :: forall k. Type k -> DList k
underRec (RefT k
x) = forall a. a -> DList a
singleton k
x
underRec (RecT Fields k
fs) = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall k. Type k -> DList k
underRec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Fields k
fs
underRec Type k
_ = forall a. Monoid a => a
mempty

-- | This takes a type description and replaces all named types with their definition.
--
-- This can produce an infinite type! Only use this in sufficiently lazy contexts, or when the
-- type is known to be not recursive.
tieKnot :: SeqDesc -> [Type Void]
tieKnot :: SeqDesc -> [Type Void]
tieKnot (SeqDesc Map k (Type k)
m ([Type k]
ts :: [Type k])) = [Type Void]
ts'
  where
    f :: k -> Type Void
    f :: k -> Type Void
f k
k = Map k (Type Void)
m' forall k a. Ord k => Map k a -> k -> a
M.! k
k
    m' :: M.Map k (Type Void)
    m' :: Map k (Type Void)
m' = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= k -> Type Void
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map k (Type k)
m
    ts' :: [Type Void]
    ts' :: [Type Void]
ts' = (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= k -> Type Void
f) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type k]
ts