{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE FlexibleContexts #-}
module Codec.Candid.Coerce
  ( coerceSeqDesc
  , SeqCoercion
  , coerce
  , Coercion
  )
  where

import Prettyprinter
import qualified Data.Vector as V
import qualified Data.ByteString.Lazy as BS
import qualified Data.Map as M
import Data.Bifunctor
import Data.List
import Data.Tuple
import Control.Monad.State.Lazy
import Control.Monad.Except

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

type SeqCoercion = [Value] -> Either String [Value]
type Coercion = Value -> Either String Value

coerceSeqDesc :: SeqDesc -> SeqDesc -> Either String SeqCoercion
coerceSeqDesc :: SeqDesc -> SeqDesc -> Either String SeqCoercion
coerceSeqDesc SeqDesc
sd1 SeqDesc
sd2 =
    forall r.
SeqDesc
-> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable SeqDesc
sd1 forall a b. (a -> b) -> a -> b
$ \[Type (Ref k Type)]
ts1 ->
    forall r.
SeqDesc
-> (forall k. (Pretty k, Ord k) => [Type (Ref k Type)] -> r) -> r
unrollTypeTable SeqDesc
sd2 forall a b. (a -> b) -> a -> b
$ \[Type (Ref k Type)]
ts2 ->
    forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)]
-> [Type (Ref k2 Type)] -> Either String SeqCoercion
coerceSeq [Type (Ref k Type)]
ts1 [Type (Ref k Type)]
ts2

coerceSeq ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    [Type (Ref k1 Type)] ->
    [Type (Ref k2 Type)] ->
    Either String SeqCoercion
coerceSeq :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)]
-> [Type (Ref k2 Type)] -> Either String SeqCoercion
coerceSeq [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2 = forall k1 k2 a. (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2

-- | This function implements the `C[<t> <: <t>]` coercion function from the
-- spec. It returns `Left` if no subtyping relation holds, or `Right c` if it
-- holds, together with a coercion function.
--
-- The coercion function itself is not total because the intput value isn’t
-- typed, so we have to cater for errors there. It should not fail if the
-- passed value really is inherently of the input type.
--
-- In a dependently typed language we’d maybe have something like
-- `coerce :: foreach t1 -> foreach t2 -> Either String (t1 -> t2)`
-- instead, and thus return a total function
coerce ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    Either String Coercion
coerce :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> Either String Coercion
coerce Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = forall k1 k2 a. (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

type Memo k1 k2 =
    (M.Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion,
     M.Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion)
type M k1 k2 = ExceptT String (State (Memo k1 k2))

runM :: (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM :: forall k1 k2 a. (Ord k1, Ord k2) => M k1 k2 a -> Either String a
runM M k1 k2 a
act = forall s a. State s a -> s -> a
evalState (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT M k1 k2 a
act) (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty)

flipM :: M k1 k2 a -> M k2 k1 a
flipM :: forall k1 k2 a. M k1 k2 a -> M k2 k1 a
flipM (ExceptT (StateT Memo k1 k2 -> Identity (Either String a, Memo k1 k2)
f)) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
f')
  where
    f' :: (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
 Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion)
-> Identity
     (Either String a,
      (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion,
       Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion))
f' (Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion
m1,Map (Type (Ref k1 Type), Type (Ref k2 Type)) Coercion
m2) = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a b. (a, b) -> (b, a)
swap 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)) Coercion
m2,Map (Type (Ref k2 Type), Type (Ref k1 Type)) Coercion
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) ->
    M k1 k2 Coercion

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


-- Memoization uses lazyiness: When we see a pair for the first time,
-- we optimistically put the resulting coercion into the map.
-- Either the following recursive call will fail (but then this optimistic
-- value was never used), or it will succeed, but then the guess was correct.
memo :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = do
  forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Type (Ref k1 Type)
t1,Type (Ref k2 Type)
t2) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Coercion
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
c
    Maybe Coercion
Nothing -> mdo
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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) Coercion
c))
        Coercion
c <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
        forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
c

-- Look through refs
go :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
go (RefT (Ref k1
_ Type (Ref k1 Type)
t1)) Type (Ref k2 Type)
t2 = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
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)) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat8T Type (Ref k2 Type)
Nat8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat16T Type (Ref k2 Type)
Nat16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat32T Type (Ref k2 Type)
Nat32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Nat64T Type (Ref k2 Type)
Nat64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
IntT Type (Ref k2 Type)
IntT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int8T Type (Ref k2 Type)
Int8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int16T Type (Ref k2 Type)
Int16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int32T Type (Ref k2 Type)
Int32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Int64T Type (Ref k2 Type)
Int64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Float32T Type (Ref k2 Type)
Float32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
Float64T Type (Ref k2 Type)
Float64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
BoolT Type (Ref k2 Type)
BoolT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
TextT Type (Ref k2 Type)
TextT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
NullT Type (Ref k2 Type)
NullT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go Type (Ref k1 Type)
PrincipalT Type (Ref k2 Type)
PrincipalT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- Nat <: Int
go Type (Ref k1 Type)
NatT Type (Ref k2 Type)
IntT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
    NatV Natural
n -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Integer -> Value
IntV (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n)
    Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing nat <: int"

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

-- empty <: t
go Type (Ref k1 Type)
EmptyT Type (Ref k2 Type)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \Value
v ->
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing empty"

-- vec t1 <: vec t2
go (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = do
    Coercion
c <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
        VecV Vector Value
vs -> Vector Value -> Value
VecV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Coercion
c Vector Value
vs
        Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vector"

-- Option: The normal rule
go (OptT Type (Ref k1 Type)
t1) (OptT Type (Ref k2 Type)
t2) = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right Coercion
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
        OptV Maybe Value
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)
        OptV (Just Value
v) -> Maybe Value -> Value
OptV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
        Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing option"
    Left String
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)))

-- Option: The constituent rule
go Type (Ref k1 Type)
t (OptT Type (Ref k2 Type)
t2) | Bool -> Bool
not (forall a. Type (Ref a Type) -> Bool
isOptLike Type (Ref k2 Type)
t2) = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t Type (Ref k2 Type)
t2)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right Coercion
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \Value
v -> Maybe Value -> Value
OptV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
    Left String
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)))
-- Option: The fallback rule
go Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)))

-- Records
go (RecT Fields (Ref k1 Type)
fs1) (RecT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = 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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    [(FieldName, Value)]
new_fields <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
            [ case forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t of
                OptT Type (Ref k2 Type)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (FieldName
fn, Maybe Value -> Value
OptV forall a. Maybe a
Nothing)
                Type (Ref k2 Type)
ReservedT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (FieldName
fn, Value
ReservedV)
                Type (Ref k2 Type)
t -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing record field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t
            | (FieldName
fn, Type (Ref k2 Type)
t) <- forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ Map FieldName (Type (Ref k2 Type))
m2 forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map FieldName (Type (Ref k1 Type))
m1
            ]
    [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
            [ do Coercion
c <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
                 forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \Map FieldName Value
vm -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Value
vm of
                    Maybe Value
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Record value lacks field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
                    Just Value
v -> (FieldName
fn, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
            | (FieldName
fn, (Type (Ref k1 Type)
t1, Type (Ref k2 Type)
t2)) <- forall k a. Map k a -> [(k, a)]
M.toList forall a b. (a -> b) -> a -> b
$ 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
            ]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
        TupV [Value]
ts -> do
            let vm :: Map FieldName Value
vm = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Word32 -> FieldName
hashedField Word32
n | Word32
n <- [Word32
0..]] [Value]
ts
            [(FieldName, Value)]
coerced_fields <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. (a -> b) -> a -> b
$ Map FieldName Value
vm) [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Value
RecV forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)]
coerced_fields forall a. Semigroup a => a -> a -> a
<> [(FieldName, Value)]
new_fields
        RecV [(FieldName, Value)]
fvs -> do
            let vm :: Map FieldName Value
vm = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(FieldName, Value)]
fvs
            [(FieldName, Value)]
coerced_fields <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. (a -> b) -> a -> b
$ Map FieldName Value
vm) [Map FieldName Value -> Either String (FieldName, Value)]
field_coercions
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Value
RecV forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)]
coerced_fields forall a. Semigroup a => a -> a -> a
<> [(FieldName, Value)]
new_fields
        Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing record"

-- Variants
go (VariantT Fields (Ref k1 Type)
fs1) (VariantT Fields (Ref k2 Type)
fs2) = do
    let m1 :: Map FieldName (Type (Ref k1 Type))
m1 = 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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList Fields (Ref k2 Type)
fs2
    Map FieldName Coercion
cm <- forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey (\FieldName
fn Type (Ref k1 Type)
t1 ->
        case 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 -> forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
            Maybe (Type (Ref k2 Type))
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Missing variant field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"of type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
        ) Map FieldName (Type (Ref k1 Type))
m1
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
        VariantV FieldName
fn Value
v | Just Coercion
c <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Coercion
cm -> FieldName -> Value -> Value
VariantV FieldName
fn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion
c Value
v
                      | Bool
otherwise -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected variant field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn
        Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing variant"

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

-- BlobT
go Type (Ref k1 Type)
BlobT Type (Ref k2 Type)
BlobT = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a. Applicative f => a -> f a
pure
go (VecT Type (Ref k1 Type)
t) Type (Ref k2 Type)
BlobT | forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k1 Type)
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
    VecV Vector Value
vs ->  ByteString -> Value
BlobV forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Vector a -> [a]
V.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {f :: * -> *}. MonadError String f => Value -> f Word8
goNat8 Vector Value
vs
    Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vec nat8 to blob"
   where
    goNat8 :: Value -> f Word8
goNat8 (Nat8V Word8
n) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Word8
n
    goNat8 Value
v = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing vec nat8 to blob"
go Type (Ref k1 Type)
BlobT (VecT Type (Ref k2 Type)
t) | forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k2 Type)
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
    BlobV ByteString
b -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Vector Value -> Value
VecV forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Vector a
V.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Word8 -> Value
Nat8V forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
fromIntegral) forall a b. (a -> b) -> a -> b
$ ByteString -> [Word8]
BS.unpack ByteString
b
    Value
v -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Unexpected value" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Value
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing blob to vec nat8"

go Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"is not a subtype of" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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) ->
    M k1 k2 ()
goMethodType :: forall k2 k1.
(Pretty k2, Pretty k1, Ord k2, Ord k1) =>
MethodType (Ref k1 Type) -> MethodType (Ref k2 Type) -> M k1 k2 ()
goMethodType (MethodType [Type (Ref k1 Type)]
ta1 [Type (Ref k1 Type)]
tr1 Bool
q1 Bool
o1) (MethodType [Type (Ref k2 Type)]
ta2 [Type (Ref k2 Type)]
tr2 Bool
q2 Bool
o2) = do
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
q1 forall a. Eq a => a -> a -> Bool
== Bool
q2) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in query annotation"
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
o1 forall a. Eq a => a -> a -> Bool
== Bool
o2) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"Methods differ in oneway annotation"
    forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall k1 k2 a. M k1 k2 a -> M k2 k1 a
flipM forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k2 Type)]
ta2 [Type (Ref k1 Type)]
ta1
    forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
tr1 [Type (Ref k2 Type)]
tr2

goSeq :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
_ []  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. a -> b -> a
const (forall (m :: * -> *) a. Monad m => a -> m a
return []))
goSeq [Type (Ref k1 Type)]
ts1 (RefT (Ref k2
_ Type (Ref k2 Type)
t) : [Type (Ref k2 Type)]
ts) = forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 (Type (Ref k2 Type)
tforall a. a -> [a] -> [a]
:[Type (Ref k2 Type)]
ts)
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
NullT  : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Value
NullV forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (OptT Type (Ref k2 Type)
_ : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Maybe Value -> Value
OptV forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
ReservedT : [Type (Ref k2 Type)]
ts) = do
    SeqCoercion
cs2 <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \[Value]
_vs -> (Value
ReservedV forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SeqCoercion
cs2 []
goSeq [] [Type (Ref k2 Type)]
ts =
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Argument type list too short, expecting types" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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) = do
    Coercion
c1 <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Type (Ref k1 Type) -> Type (Ref k2 Type) -> M k1 k2 Coercion
memo Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
    SeqCoercion
cs2 <- forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Type (Ref k1 Type)] -> [Type (Ref k2 Type)] -> M k1 k2 SeqCoercion
goSeq [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts2
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \case
        [] -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ Doc Any
"Expecting value of type:" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k1 Type)
t1
        (Value
v:[Value]
vs) -> do
            Value
v' <- Coercion
c1 Value
v
            [Value]
vs' <- SeqCoercion
cs2 [Value]
vs
            forall (m :: * -> *) a. Monad m => a -> m a
return (Value
v'forall a. a -> [a] -> [a]
:[Value]
vs')

unRef :: Type (Ref a Type) -> Type (Ref a Type)
unRef :: forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef (RefT (Ref a
_ Type (Ref a Type)
t)) = 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 :: forall a. Type (Ref a Type) -> Bool
isNat8 (RefT (Ref a
_ Type (Ref a Type)
t)) = 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

-- | `null <: t`?
isOptLike :: Type (Ref a Type) -> Bool
isOptLike :: forall a. Type (Ref a Type) -> Bool
isOptLike (RefT (Ref a
_ Type (Ref a Type)
t)) = forall a. Type (Ref a Type) -> Bool
isOptLike Type (Ref a Type)
t
isOptLike Type (Ref a Type)
NullT = Bool
True
isOptLike (OptT Type (Ref a Type)
_) = Bool
True
isOptLike Type (Ref a Type)
ReservedT = Bool
True
isOptLike Type (Ref a Type)
_ = Bool
False