{-# 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 =
    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) =>
[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 :: 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 k1 Type)]
t1 [Type (Ref k2 Type)]
t2 = forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM forall a b. (a -> b) -> a -> b
$ 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 :: forall k1 k2.
(Pretty k1, Pretty k2, Ord k1, Ord k2) =>
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 = forall k1 k2 a.
(Ord k1, Ord k2) =>
SubTypeM k1 k2 a -> Either String a
runSubTypeM forall a b. (a -> b) -> a -> b
$ 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 :: 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 (RefT (Ref k1
_ Type (Ref k1 Type)
t1)) Type (Ref k2 Type)
t2 = 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)) = 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Nat8T Type (Ref k2 Type)
Nat8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Nat16T Type (Ref k2 Type)
Nat16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Nat32T Type (Ref k2 Type)
Nat32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Nat64T Type (Ref k2 Type)
Nat64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
IntT Type (Ref k2 Type)
IntT = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Int8T Type (Ref k2 Type)
Int8T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Int16T Type (Ref k2 Type)
Int16T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Int32T Type (Ref k2 Type)
Int32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Int64T Type (Ref k2 Type)
Int64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Float32T Type (Ref k2 Type)
Float32T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
Float64T Type (Ref k2 Type)
Float64T = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
BoolT Type (Ref k2 Type)
BoolT = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
TextT Type (Ref k2 Type)
TextT = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
NullT Type (Ref k2 Type)
NullT = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
v
go Value
v Type (Ref k1 Type)
PrincipalT Type (Ref k2 Type)
PrincipalT = 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 = 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)

-- t <: reserved
go Value
_ Type (Ref k1 Type)
_ Type (Ref k2 Type)
ReservedT = 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)
_ = 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 (VecV Vector Value
vs) (VecT Type (Ref k1 Type)
t1) (VecT Type (Ref k2 Type)
t2) = 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 (\Value
v -> 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)
_) = 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) =
    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) =>
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)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Value
v' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV (forall a. a -> Maybe a
Just Value
v'))
        Left String
_   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV 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 (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) =>
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)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Value
v' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV (forall a. a -> Maybe a
Just Value
v'))
        Left String
_   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)

-- Option: The fallback rule
go Value
_ Type (Ref k1 Type)
_ (OptT Type (Ref k2 Type)
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV 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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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
        RecV [(FieldName, Value)]
fvs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(FieldName, Value)]
fvs
        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"

    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
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(FieldName, Value)] -> Value
RecV forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Fields (Ref k2 Type)
fs2 forall a b. (a -> b) -> a -> b
$ \(FieldName
fn, Type (Ref k2 Type)
t2) -> (FieldName
fn,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      case (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName Value
vm, 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) -> 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 forall a. Type (Ref a Type) -> Type (Ref a Type)
unRef Type (Ref k2 Type)
t2 of
            OptT Type (Ref k2 Type)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Value -> Value
OptV forall a. Maybe a
Nothing)
            Type (Ref k2 Type)
ReservedT -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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

-- 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 = 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
    case (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FieldName
fn Map FieldName (Type (Ref k1 Type))
m1, 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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))
_) -> 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
"Wrongly typed variant missing field " forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty FieldName
fn
      (Maybe (Type (Ref k1 Type))
_, 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
"Unexpected variant field" forall ann. Doc ann -> Doc ann -> Doc ann
<+> 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)
_) = 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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))]
_) = 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 = 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 | forall a. Type (Ref a Type) -> Bool
isNat8 Type (Ref k1 Type)
t = 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
   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 (BlobV ByteString
b) 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
$ 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

go Value
v 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
"Cannot coerce " 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
":" 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
"to type " forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Type (Ref k2 Type)
t2

goSeq :: 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]
_ [Type (Ref k1 Type)]
_ []  = 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) = 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)
tforall a. a -> [a] -> [a]
:[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 forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. a -> [a] -> [a]
:)    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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 (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' <- 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' <- 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
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Value
v' forall a. a -> [a] -> [a]
: [Value]
vs'
goSeq [Value]
_ [Type (Ref k1 Type)]
_ [Type (Ref k2 Type)]
_ = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Illtyped input to goSeq"

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