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

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

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

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

coerceSeq ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    [Value] ->
    [Type (Ref k1 Type)] ->
    [Type (Ref k2 Type)] ->
    Either String [Value]
coerceSeq :: [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> Either String [Value]
coerceSeq [Value]
vs [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2 = SubTypeM k1 k2 [Value] -> Either String [Value]
forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM (SubTypeM k1 k2 [Value] -> Either String [Value])
-> SubTypeM k1 k2 [Value] -> Either String [Value]
forall a b. (a -> b) -> a -> b
$ [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [Type (Ref k1 Type)]
t1 [Type (Ref k2 Type)]
t2

-- | This function implements the @V : T ~> V' : T'@ relation from the Candid spec.
--
-- Because values in this library are untyped, we have to pass what we know about
-- their type down, so that we can do the subtype check upon a reference.
-- The given type must match the value closely (as it is the case when decoding
-- from the wire) and this function may behave oddly if @v@ and @t1@ are not related.
--
-- Morally, this function looks only at @v@ and @t2@. It only needs @t1@ for
-- refences, and hence needs to take @t2@ apart for the recursive calls.
-- Practically, it's sometimes more concise to look at t2 instead of v.
coerce ::
    (Pretty k1, Pretty k2, Ord k1, Ord k2) =>
    Value ->
    Type (Ref k1 Type) ->
    Type (Ref k2 Type) ->
    Either String Value
coerce :: Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> Either String Value
coerce Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = SubTypeM k1 k2 Value -> Either String Value
forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM (SubTypeM k1 k2 Value -> Either String Value)
-> SubTypeM k1 k2 Value -> Either String Value
forall a b. (a -> b) -> a -> b
$ Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2

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

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

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

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

-- Nat <: Int
go (NatV Natural
n) Type (Ref k1 Type)
NatT Type (Ref k2 Type)
IntT = Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> SubTypeM k1 k2 Value) -> Value -> SubTypeM k1 k2 Value
forall a b. (a -> b) -> a -> b
$ Integer -> Value
IntV (Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n)

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

-- empty <: t (actually just a special case of `v :/ t`)
go Value
v Type (Ref k1 Type)
EmptyT Type (Ref k2 Type)
_ = String -> SubTypeM k1 k2 Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 Value) -> String -> SubTypeM k1 k2 Value
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
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing empty"

-- vec t1 <: vec t2
go (RepeatV Int
n Value
v) (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = Int -> Value -> Value
RepeatV Int
n (Value -> Value) -> SubTypeM k1 k2 Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
go (VecV Vector Value
vs) (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = Vector Value -> Value
VecV (Vector Value -> Value)
-> ExceptT String (State (Memo k1 k2)) (Vector Value)
-> SubTypeM k1 k2 Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> SubTypeM k1 k2 Value)
-> Vector Value
-> ExceptT String (State (Memo k1 k2)) (Vector Value)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Value
v -> Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2) Vector Value
vs

-- Option: The normal rule
go (OptV Maybe Value
Nothing)  (OptT Type (Ref k1 Type)
_) (OptT Type (Ref k2 Type)
_) = Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
NullV
go (OptV (Just Value
v)) (OptT Type (Ref k1 Type)
t1) (OptT Type (Ref k2 Type)
t2) =
    State (Memo k1 k2) (Either String Value)
-> ExceptT String (State (Memo k1 k2)) (Either String Value)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SubTypeM k1 k2 Value -> State (Memo k1 k2) (Either String Value)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2)) ExceptT String (State (Memo k1 k2)) (Either String Value)
-> (Either String Value -> SubTypeM k1 k2 Value)
-> SubTypeM k1 k2 Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Value
v' -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v'))
        Left String
_   -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)

-- Option: The constituent rule
go Value
v Type (Ref k1 Type)
t1 (OptT Type (Ref k2 Type)
t2) | Bool -> Bool
not (Type (Ref k2 Type) -> Bool
forall a. Type (Ref a Type) -> Bool
isOptLike Type (Ref k2 Type)
t2) =
    State (Memo k1 k2) (Either String Value)
-> ExceptT String (State (Memo k1 k2)) (Either String Value)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SubTypeM k1 k2 Value -> State (Memo k1 k2) (Either String Value)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2)) ExceptT String (State (Memo k1 k2)) (Either String Value)
-> (Either String Value -> SubTypeM k1 k2 Value)
-> SubTypeM k1 k2 Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Value
v' -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
v'))
        Left String
_   -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)

-- Option: The fallback rule
go Value
_ Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)

-- Records
go Value
rv (RecT Fields (Ref k1 Type)
fs1) (RecT Fields (Ref k2 Type)
fs2) = do
    Map FieldName Value
vm <- case Value
rv of
        TupV [Value]
ts -> Map FieldName Value
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map FieldName Value
 -> ExceptT String (State (Memo k1 k2)) (Map FieldName Value))
-> Map FieldName Value
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Map FieldName Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(FieldName, Value)] -> Map FieldName Value)
-> [(FieldName, Value)] -> Map FieldName Value
forall a b. (a -> b) -> a -> b
$ [FieldName] -> [Value] -> [(FieldName, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Word32 -> FieldName
hashedField Word32
n | Word32
n <- [Word32
0..]] [Value]
ts
        RecV [(FieldName, Value)]
fvs -> Map FieldName Value
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Map FieldName Value
 -> ExceptT String (State (Memo k1 k2)) (Map FieldName Value))
-> Map FieldName Value
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
forall a b. (a -> b) -> a -> b
$ [(FieldName, Value)] -> Map FieldName Value
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(FieldName, Value)]
fvs
        Value
v -> String -> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String
 -> ExceptT String (State (Memo k1 k2)) (Map FieldName Value))
-> String
-> ExceptT String (State (Memo k1 k2)) (Map FieldName Value)
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
"Unexpected value" Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
"while coercing record"

    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
    ([(FieldName, Value)] -> Value)
-> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
-> SubTypeM k1 k2 Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(FieldName, Value)] -> Value
RecV (ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
 -> SubTypeM k1 k2 Value)
-> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
-> SubTypeM k1 k2 Value
forall a b. (a -> b) -> a -> b
$ Fields (Ref k2 Type)
-> ((FieldName, Type (Ref k2 Type))
    -> ExceptT String (State (Memo k1 k2)) (FieldName, Value))
-> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Fields (Ref k2 Type)
fs2 (((FieldName, Type (Ref k2 Type))
  -> ExceptT String (State (Memo k1 k2)) (FieldName, Value))
 -> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)])
-> ((FieldName, Type (Ref k2 Type))
    -> ExceptT String (State (Memo k1 k2)) (FieldName, Value))
-> ExceptT String (State (Memo k1 k2)) [(FieldName, Value)]
forall a b. (a -> b) -> a -> b
$ \(FieldName
fn, Type (Ref k2 Type)
t2) -> (FieldName
fn,) (Value -> (FieldName, Value))
-> SubTypeM k1 k2 Value
-> ExceptT String (State (Memo k1 k2)) (FieldName, Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      case (FieldName -> Map FieldName Value -> Maybe Value
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Value
vm, FieldName
-> Map FieldName (Type (Ref k1 Type)) -> Maybe (Type (Ref k1 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName (Type (Ref k1 Type))
m1) of
        (Just Value
v, Just Type (Ref k1 Type)
t1) -> Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
        (Maybe Value, Maybe (Type (Ref k1 Type)))
_ -> case Type (Ref k2 Type) -> Type (Ref k2 Type)
forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t2 of
            Type (Ref k2 Type)
NullT     -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
NullV
            OptT Type (Ref k2 Type)
_    -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing)
            Type (Ref k2 Type)
ReservedT -> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
ReservedV
            Type (Ref k2 Type)
t -> String -> SubTypeM k1 k2 Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 Value) -> String -> SubTypeM k1 k2 Value
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

-- Variants
go (VariantV FieldName
fn Value
v) (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
    case (FieldName
-> Map FieldName (Type (Ref k1 Type)) -> Maybe (Type (Ref k1 Type))
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName (Type (Ref k1 Type))
m1, 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 k1 Type)
t1, Just Type (Ref k2 Type)
t2) -> FieldName -> Value -> Value
VariantV FieldName
fn (Value -> Value) -> SubTypeM k1 k2 Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
      (Maybe (Type (Ref k1 Type))
Nothing, Maybe (Type (Ref k2 Type))
_) -> String -> SubTypeM k1 k2 Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 Value) -> String -> SubTypeM k1 k2 Value
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
"Wrongly typed variant missing 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
      (Maybe (Type (Ref k1 Type))
_, Maybe (Type (Ref k2 Type))
Nothing) -> String -> SubTypeM k1 k2 Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 Value) -> String -> SubTypeM k1 k2 Value
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
"Unexpected 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

-- Reference types
go Value
v t1 :: Type (Ref k1 Type)
t1@(FuncT MethodType (Ref k1 Type)
_) t2 :: Type (Ref k2 Type)
t2@(FuncT MethodType (Ref k2 Type)
_) = 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 SubTypeM k1 k2 () -> SubTypeM k1 k2 Value -> SubTypeM k1 k2 Value
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v t1 :: Type (Ref k1 Type)
t1@(ServiceT [(Text, MethodType (Ref k1 Type))]
_) t2 :: Type (Ref k2 Type)
t2@(ServiceT [(Text, MethodType (Ref k2 Type))]
_) = 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 SubTypeM k1 k2 () -> SubTypeM k1 k2 Value -> SubTypeM k1 k2 Value
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Value -> SubTypeM k1 k2 Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v

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

go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2 = String -> SubTypeM k1 k2 Value
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 Value) -> String -> SubTypeM k1 k2 Value
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
"Cannot coerce " Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Value -> Doc Any
forall a ann. Pretty a => a -> Doc ann
pretty Value
v Doc Any -> Doc Any -> Doc Any
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc Any
":" 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
"to 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)
t2

goSeq :: [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
_ [Type (Ref k1 Type)]
_ []  = [Value] -> SubTypeM k1 k2 [Value]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
goSeq [Value]
vs [Type (Ref k1 Type)]
ts1 (RefT (Ref k2
_ Type (Ref k2 Type)
t) : [Type (Ref k2 Type)]
ts) = [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [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)
goSeq vs :: [Value]
vs@[] ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
NullT     : [Type (Ref k2 Type)]
ts) = (Value
NullV Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:)        ([Value] -> [Value])
-> SubTypeM k1 k2 [Value] -> SubTypeM k1 k2 [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq vs :: [Value]
vs@[] ts1 :: [Type (Ref k1 Type)]
ts1@[] (OptT Type (Ref k2 Type)
_    : [Type (Ref k2 Type)]
ts) = (Maybe Value -> Value
OptV Maybe Value
forall a. Maybe a
Nothing Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:) ([Value] -> [Value])
-> SubTypeM k1 k2 [Value] -> SubTypeM k1 k2 [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq vs :: [Value]
vs@[] ts1 :: [Type (Ref k1 Type)]
ts1@[] (Type (Ref k2 Type)
ReservedT : [Type (Ref k2 Type)]
ts) = (Value
ReservedV Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
:)    ([Value] -> [Value])
-> SubTypeM k1 k2 [Value] -> SubTypeM k1 k2 [Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts
goSeq [] [] [Type (Ref k2 Type)]
ts = String -> SubTypeM k1 k2 [Value]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 [Value])
-> String -> SubTypeM k1 k2 [Value]
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 (Value
v:[Value]
vs) (Type (Ref k1 Type)
t1:[Type (Ref k1 Type)]
ts1) (Type (Ref k2 Type)
t2:[Type (Ref k2 Type)]
ts2) = do
    Value
v' <- Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
Value
-> Type (Ref k1 Type) -> Type (Ref k2 Type) -> SubTypeM k1 k2 Value
go Value
v Type (Ref k1 Type)
t1 Type (Ref k2 Type)
t2
    [Value]
vs' <- [Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
[Value]
-> [Type (Ref k1 Type)]
-> [Type (Ref k2 Type)]
-> SubTypeM k1 k2 [Value]
goSeq [Value]
vs [Type (Ref k1 Type)]
ts1 [Type (Ref k2 Type)]
ts2
    [Value] -> SubTypeM k1 k2 [Value]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Value] -> SubTypeM k1 k2 [Value])
-> [Value] -> SubTypeM k1 k2 [Value]
forall a b. (a -> b) -> a -> b
$ Value
v' Value -> [Value] -> [Value]
forall a. a -> [a] -> [a]
: [Value]
vs'
goSeq [Value]
_ [Type (Ref k1 Type)]
_ [Type (Ref k2 Type)]
_ = String -> SubTypeM k1 k2 [Value]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> SubTypeM k1 k2 [Value])
-> String -> SubTypeM k1 k2 [Value]
forall a b. (a -> b) -> a -> b
$ String
"Illtyped input to goSeq"

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

-- | `null <: t`?
isOptLike :: Type (Ref a Type) -> Bool
isOptLike :: Type (Ref a Type) -> Bool
isOptLike (RefT (Ref a
_ Type (Ref a Type)
t)) = Type (Ref a Type) -> Bool
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