{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
module Codec.Candid.Subtype
  ( isSubtypeOf
  , SubTypeM
  , runSubTypeM
  , isSubtypeOfM
  )
  where

import Prettyprinter
import qualified Data.Map as M
import Data.Bifunctor
import Data.Tuple
import Control.Monad
import Control.Monad.State.Lazy
import Control.Monad.Except
import Control.Monad.Trans.Except

import Codec.Candid.Types
import Codec.Candid.TypTable

type Memo k1 k2 =
    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))

type SubTypeM k1 k2 = ExceptT String (State (Memo k1 k2))

runSubTypeM :: (Ord k1, Ord k2) => SubTypeM k1 k2 a -> Either String a
runSubTypeM :: SubTypeM k1 k2 a -> Either String a
runSubTypeM SubTypeM k1 k2 a
act = State (Memo k1 k2) (Either String a)
-> Memo k1 k2 -> Either String a
forall s a. State s a -> s -> a
evalState (SubTypeM k1 k2 a -> State (Memo k1 k2) (Either String a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT SubTypeM k1 k2 a
act) (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
forall a. Monoid a => a
mempty, Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())
forall a. Monoid a => a
mempty)

-- | Returns 'Right' if the first argument is a subtype of the second, or
-- returns 'Left' with an explanation if not
isSubtypeOf ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    Either String ()
isSubtypeOf :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> Either String ()
isSubtypeOf Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = SubTypeM k1 k2 () -> Either String ()
forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM (SubTypeM k1 k2 () -> Either String ())
-> SubTypeM k1 k2 () -> Either String ()
forall a b. (a -> b) -> a -> b
$ Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
isSubtypeOfM Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

isSubtypeOfM ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    SubTypeM k1 k2 ()
isSubtypeOfM :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
isSubtypeOfM Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

flipM :: SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM :: SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM (ExceptT (StateT Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f)) = StateT
  (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
   Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
  Identity
  (Either String a)
-> SubTypeM k2 k1 a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (((Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
  Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
 -> Identity
      (Either String a,
       (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
        Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))))
-> StateT
     (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
      Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
     Identity
     (Either String a)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
f')
  where
    f' :: (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
f' (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())
m1,Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
m2) = (Memo k1 k2
 -> (Map
       (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
     Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
-> (Either String a, Memo k1 k2)
-> (Either String a,
    (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
     Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Memo k1 k2
-> (Map
      (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
    Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
forall a b. (a, b) -> (b, a)
swap ((Either String a, Memo k1 k2)
 -> (Either String a,
     (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
      Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))))
-> Identity (Either String a, Memo k1 k2)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()),
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
m2,Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())
m1) -- f (m2,m1) >>= \case (r, (m2',m1')) -> pure (r, (m1', m2'))

memo, go ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    SubTypeM k1 k2 ()

goSeq ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    [Type (Ref k1 Type)] ->
    [Type (Ref k2 Type)] ->
    SubTypeM k1 k2 ()

-- Memoization: When we see a pair for the first time,
-- we optimistically put 'True' into the map.
-- Either the following recursive call will fail (but then this optimistic
-- value wasn't a problem), or it will succeed, but then the guess was correct.
-- If it fails we put 'False' into it, to as a caching optimization
memo :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = do
  ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
  Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))
 -> Maybe (Either String ()))
-> ExceptT
     String
     (State
        (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
         Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())))
     (Maybe (Either String ()))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Type (Ref k1 Type), Type (Ref k2 Type))
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
-> Maybe (Either String ())
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
 -> Maybe (Either String ()))
-> ((Map
       (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
     Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))
    -> Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()))
-> (Map
      (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
    Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))
-> Maybe (Either String ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
 Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ()))
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ())
forall a b. (a, b) -> a
fst) ExceptT
  String
  (State
     (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either String ()),
      Map (Type (Ref k2 Type), Type (Ref k1 Type)) (Either String ())))
  (Maybe (Either String ()))
-> (Maybe (Either String ()) -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Either String ()
r -> Either String () -> SubTypeM k1 k2 ()
forall (m :: * -> *) e a. Monad m => Either e a -> ExceptT e m a
except Either String ()
r
    Maybe (Either String ())
Nothing -> SubTypeM k1 k2 ()
assume_ok SubTypeM k1 k2 () -> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 SubTypeM k1 k2 ()
-> (String -> SubTypeM k1 k2 ()) -> SubTypeM k1 k2 ()
forall (m :: * -> *) e a e'.
Monad m =>
ExceptT e m a -> (e -> ExceptT e' m a) -> ExceptT e' m a
`catchE` String -> SubTypeM k1 k2 ()
forall (m :: * -> *) (p :: * -> * -> *) e b c b.
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) (Either e b)) c)
   m,
 Bifunctor p, MonadError e m) =>
e -> m b
remember_failure)
  where
    remember :: a -> m ()
remember a
r         = (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c
 -> p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c)
-> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map (Type (Ref k1 Type), Type (Ref k2 Type)) a
 -> Map (Type (Ref k1 Type), Type (Ref k2 Type)) a)
-> p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c
-> p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Type (Ref k1 Type), Type (Ref k2 Type))
-> a
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) a
-> Map (Type (Ref k1 Type), Type (Ref k2 Type)) a
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) a
r))
    assume_ok :: SubTypeM k1 k2 ()
assume_ok          = Either String () -> SubTypeM k1 k2 ()
forall (p :: * -> * -> *) a c (m :: * -> *).
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c) m,
 Bifunctor p) =>
a -> m ()
remember (() -> Either String ()
forall a b. b -> Either a b
Right ())
    remember_failure :: e -> m b
remember_failure e
e = Either e b -> m ()
forall (p :: * -> * -> *) a c (m :: * -> *).
(MonadState
   (p (Map (Type (Ref k1 Type), Type (Ref k2 Type)) a) c) m,
 Bifunctor p) =>
a -> m ()
remember (e -> Either e b
forall a b. a -> Either a b
Left e
e) m () -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> e -> m b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError e
e

-- Look through refs
go :: Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
go (RefT (Ref k1
_ Type (Ref k1 Type)
t1)) Type (Ref k2 Type)
t2 = Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
go Type (Ref k1 Type)
t1 (RefT (Ref k2
_ Type (Ref k2 Type)
t2)) = Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

-- Identity coercion for primitive values
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
NatT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat8T Type (Ref k2 Type)
Nat8T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat16T Type (Ref k2 Type)
Nat16T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat32T Type (Ref k2 Type)
Nat32T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Nat64T Type (Ref k2 Type)
Nat64T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
IntT Type (Ref k2 Type)
IntT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int8T Type (Ref k2 Type)
Int8T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int16T Type (Ref k2 Type)
Int16T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int32T Type (Ref k2 Type)
Int32T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Int64T Type (Ref k2 Type)
Int64T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Float32T Type (Ref k2 Type)
Float32T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
Float64T Type (Ref k2 Type)
Float64T = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
BoolT Type (Ref k2 Type)
BoolT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
TextT Type (Ref k2 Type)
TextT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
NullT Type (Ref k2 Type)
NullT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
PrincipalT Type (Ref k2 Type)
PrincipalT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Nat <: Int
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
IntT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- t <: reserved
go Type (Ref k1 Type)
_ Type (Ref k2 Type)
ReservedT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- empty <: t
go Type (Ref k1 Type)
EmptyT Type (Ref k2 Type)
_ = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- vec t1 <: vec t2
go (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

-- Option: very simple
go Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Records
go (RecT Fields (Ref k1 Type)
fs1) (RecT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = Fields (Ref k1 Type) -> Map FieldName (Type (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k1 Type)
fs1
    let m2 :: Map FieldName (Type (Ref k2 Type))
m2 = Fields (Ref k2 Type) -> Map FieldName (Type (Ref k2 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    -- Check missing fields
    [SubTypeM k1 k2 ()] -> SubTypeM k1 k2 ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      [ case Type (Ref k2 Type) -> Type (Ref k2 Type)
forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t of
          Type (Ref k2 Type)
NullT     -> () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          OptT Type (Ref k2 Type)
_    -> () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Type (Ref k2 Type)
ReservedT -> () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          Type (Ref k2 Type)
t -> String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 ()) -> String -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing record field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t
      | (FieldName
fn, Type (Ref k2 Type)
t) <- Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type)
forall k a. Map k a -> [(k, a)]
M.toList (Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type))
-> Map FieldName (Type (Ref k2 Type)) -> Fields (Ref k2 Type)
forall a b. (a -> b) -> a -> b
$ Map FieldName (Type (Ref k2 Type))
m2 Map FieldName (Type (Ref k2 Type))
-> Map FieldName (Type (Ref k1 Type))
-> Map FieldName (Type (Ref k2 Type))
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map FieldName (Type (Ref k1 Type))
m1
      ]
    -- Check existing fields
    [SubTypeM k1 k2 ()] -> SubTypeM k1 k2 ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 | (FieldName
_fn, (Type (Ref k1 Type)
t1, Type (Ref k2 Type)
t2)) <- Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
-> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))]
forall k a. Map k a -> [(k, a)]
M.toList (Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
 -> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))])
-> Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
-> [(FieldName, (Type (Ref k1 Type), Type (Ref k2 Type)))]
forall a b. (a -> b) -> a -> b
$ (Type (Ref k1 Type)
 -> Type (Ref k2 Type) -> (Type (Ref k1 Type), Type (Ref k2 Type)))
-> Map FieldName (Type (Ref k1 Type))
-> Map FieldName (Type (Ref k2 Type))
-> Map FieldName (Type (Ref k1 Type), Type (Ref k2 Type))
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map FieldName (Type (Ref k1 Type))
m1 Map FieldName (Type (Ref k2 Type))
m2 ]

-- Variants
go (VariantT Fields (Ref k1 Type)
fs1) (VariantT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = Fields (Ref k1 Type) -> Map FieldName (Type (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k1 Type)
fs1
    let m2 :: Map FieldName (Type (Ref k2 Type))
m2 = Fields (Ref k2 Type) -> Map FieldName (Type (Ref k2 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    [SubTypeM k1 k2 ()] -> SubTypeM k1 k2 ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
      [ case FieldName
-> Map FieldName (Type (Ref k2 Type)) -> Maybe (Type (Ref k2 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName (Type (Ref k2 Type))
m2 of
            Just Type (Ref k2 Type)
t2 -> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
            Maybe (Type (Ref k2 Type))
Nothing -> String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 ()) -> String -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing variant field" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FieldName -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
      | (FieldName
fn, Type (Ref k1 Type)
t1) <- Map FieldName (Type (Ref k1 Type)) -> Fields (Ref k1 Type)
forall k a. Map k a -> [(k, a)]
M.toList Map FieldName (Type (Ref k1 Type))
m1
      ]

-- Reference types
go (FuncT MethodType (Ref k1 Type)
mt1) (FuncT MethodType (Ref k2 Type)
mt2) = MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2
go (ServiceT [(Text, MethodType (Ref k1 Type))]
meths1) (ServiceT [(Text, MethodType (Ref k2 Type))]
meths2) = do
    let m1 :: Map Text (MethodType (Ref k1 Type))
m1 = [(Text, MethodType (Ref k1 Type))]
-> Map Text (MethodType (Ref k1 Type))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Text, MethodType (Ref k1 Type))]
meths1
    [(Text, MethodType (Ref k2 Type))]
-> ((Text, MethodType (Ref k2 Type)) -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Text, MethodType (Ref k2 Type))]
meths2 (((Text, MethodType (Ref k2 Type)) -> SubTypeM k1 k2 ())
 -> SubTypeM k1 k2 ())
-> ((Text, MethodType (Ref k2 Type)) -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ \(Text
m, MethodType (Ref k2 Type)
mt2) -> case Text
-> Map Text (MethodType (Ref k1 Type))
-> Maybe (MethodType (Ref k1 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
m Map Text (MethodType (Ref k1 Type))
m1 of
        Just MethodType (Ref k1 Type)
mt1 -> MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
goMethodType MethodType (Ref k1 Type)
mt1 MethodType (Ref k2 Type)
mt2
        Maybe (MethodType (Ref k1 Type))
Nothing -> String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 ()) -> String -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing service method" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Text
m Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> MethodType (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty MethodType (Ref k2 Type)
mt2

-- BlobT
go Type (Ref k1 Type)
BlobT Type (Ref k2 Type)
BlobT = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go (VecT Type (Ref k1 Type)
t) Type (Ref k2 Type)
BlobT | Type (Ref k1 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k1 Type)
t = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
go Type (Ref k1 Type)
BlobT (VecT Type (Ref k2 Type)
t) | Type (Ref k2 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k2 Type)
t = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- Final catch-all
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 ()) -> String -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Type" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k1 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1 Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"is not a subtype of" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type (Ref k2 Type) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t2

goMethodType ::
    (Pretty k2, Pretty k1, Ord k2, Ord k1) =>
    MethodType (Ref k1 Type) ->
    MethodType (Ref k2 Type) ->
    SubTypeM k1 k2 ()
goMethodType :: MethodType (Ref k1 Type)
-> MethodType (Ref k2 Type) -> SubTypeM k1 k2 ()
goMethodType (MethodType [Type (Ref k1 Type)]
ta1 [Type (Ref k1 Type)]
tr1 Bool
q1 Bool
cq1 Bool
o1) (MethodType [Type (Ref k2 Type)]
ta2 [Type (Ref k2 Type)]
tr2 Bool
q2 Bool
cq2 Bool
o2) = do
    Bool -> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
q1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
q2) (SubTypeM k1 k2 () -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in query annotation"
    Bool -> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
o1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
o2) (SubTypeM k1 k2 () -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in oneway annotation"
    Bool -> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
cq1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
cq2) (SubTypeM k1 k2 () -> SubTypeM k1 k2 ())
-> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in oneway annotation"
    SubTypeM k2 k1 () -> SubTypeM k1 k2 ()
forall k1 k2 a. SubTypeM k1 k2 a -> SubTypeM k2 k1 a
flipM (SubTypeM k2 k1 () -> SubTypeM k1 k2 ())
-> SubTypeM k2 k1 () -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ [Type (Ref k2 Type)] -> [Type (Ref k1 Type)] -> SubTypeM k2 k1 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k2 Type)]
ta2 [Type (Ref k1 Type)]
ta1
    [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
tr1 [Type (Ref k2 Type)]
tr2

goSeq :: [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
_ []  = () -> SubTypeM k1 k2 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
goSeq [Type (Ref k1 Type)]
ts1 (RefT (Ref k2
_ Type (Ref k2 Type)
t) : [Type (Ref k2 Type)]
ts) = [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 (Type (Ref k2 Type)
tType (Ref k2 Type) -> [Type (Ref k2 Type)] -> [Type (Ref k2 Type)]
forall a. a -> [a] -> [a]
:[Type (Ref k2 Type)]
ts)
-- Missing optional arguments are ok
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
NullT : [Type (Ref k2 Type)]
ts)     = [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (OptT Type (Ref k2 Type)
_ : [Type (Ref k2 Type)]
ts)    = [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
ReservedT : [Type (Ref k2 Type)]
ts) = [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq [] [Type (Ref k2 Type)]
ts = String -> SubTypeM k1 k2 ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 ()) -> String -> SubTypeM k1 k2 ()
forall a b. (a -> b) -> a -> b
$ Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ Doc Any
"Argument type list too short, expecting types" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Type (Ref k2 Type)] -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty [Type (Ref k2 Type)]
ts
goSeq (Type (Ref k1 Type)
t1:[Type (Ref k1 Type)]
ts1) (Type (Ref k2 Type)
t2:[Type (Ref k2 Type)]
ts2) = Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 ()
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 SubTypeM k1 k2 () -> SubTypeM k1 k2 () -> SubTypeM k1 k2 ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> SubTypeM k1 k2 ()
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts2

unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Type (Ref a Type)
forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref a Type)
t
unRef Type (Ref a Type)
t = Type (Ref a Type)
t

isNat8 :: Type (Ref a Type) -> Bool
isNat8 :: Type (Ref a Type) -> Bool
isNat8 (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref a Type)
t
isNat8 Type (Ref a Type)
Nat8T = Bool
True
isNat8 Type (Ref a Type)
_ = Bool
False