-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, containing type classes for operating with Michelson values
-- in the context of polymorphic stack type operations.

module Michelson.Typed.Polymorphic
  ( EDivOp (..)
  , MemOp (..)
  , MapOp (..)
  , IterOp (..)
  , SizeOp (..)
  , GetOp (..)
  , UpdOp (..)
  , SliceOp (..)
  , ConcatOp (..)
  , divMich
  , modMich
  ) where

import qualified Data.ByteString as B
import qualified Data.Map as M
import qualified Data.Set as S

import Michelson.Text
import Michelson.Typed.Annotation
import Michelson.Typed.Sing (KnownT)
import Michelson.Typed.T (T(..))
import Michelson.Typed.Value (Value'(..))
import Michelson.Untyped.Annotation (noAnn)

import Tezos.Core (divModMutez, divModMutezInt)

class MemOp (c :: T) where
  type MemOpKey c :: T
  evalMem :: Value' instr (MemOpKey c) -> Value' instr c -> Bool
instance MemOp ('TSet e) where
  type MemOpKey ('TSet e) = e
  evalMem :: Value' instr (MemOpKey ('TSet e)) -> Value' instr ('TSet e) -> Bool
evalMem e :: Value' instr (MemOpKey ('TSet e))
e (VSet s :: Set (Value' instr t)
s) = Value' instr t
Value' instr (MemOpKey ('TSet e))
e Value' instr t -> Set (Value' instr t) -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set (Value' instr t)
s
instance MemOp ('TMap k v) where
  type MemOpKey ('TMap k v) = k
  evalMem :: Value' instr (MemOpKey ('TMap k v))
-> Value' instr ('TMap k v) -> Bool
evalMem k :: Value' instr (MemOpKey ('TMap k v))
k (VMap m :: Map (Value' instr k) (Value' instr v)
m) = Value' instr k
Value' instr (MemOpKey ('TMap k v))
k Value' instr k -> Map (Value' instr k) (Value' instr v) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map (Value' instr k) (Value' instr v)
m
instance MemOp ('TBigMap k v) where
  type MemOpKey ('TBigMap k v) = k
  evalMem :: Value' instr (MemOpKey ('TBigMap k v))
-> Value' instr ('TBigMap k v) -> Bool
evalMem k :: Value' instr (MemOpKey ('TBigMap k v))
k (VBigMap m :: Map (Value' instr k) (Value' instr v)
m) = Value' instr k
Value' instr (MemOpKey ('TBigMap k v))
k Value' instr k -> Map (Value' instr k) (Value' instr v) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` Map (Value' instr k) (Value' instr v)
m

class MapOp (c :: T) where
  type MapOpInp c :: T
  type MapOpRes c :: T -> T
  mapOpToList :: Value' instr c -> [Value' instr (MapOpInp c)]
  mapOpFromList
    :: (KnownT b)
    => Value' instr c -> [Value' instr b] -> Value' instr (MapOpRes c b)
instance MapOp ('TMap k v) where
  type MapOpInp ('TMap k v) = 'TPair k v
  type MapOpRes ('TMap k v) = 'TMap k
  mapOpToList :: Value' instr ('TMap k v) -> [Value' instr (MapOpInp ('TMap k v))]
mapOpToList (VMap m :: Map (Value' instr k) (Value' instr v)
m) = ((Value' instr k, Value' instr v) -> Value' instr ('TPair k v))
-> [(Value' instr k, Value' instr v)]
-> [Value' instr ('TPair k v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(k :: Value' instr k
k, v :: Value' instr v
v) -> (Value' instr k, Value' instr v) -> Value' instr ('TPair k v)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value' instr k
k, Value' instr v
v)) ([(Value' instr k, Value' instr v)]
 -> [Value' instr (MapOpInp ('TMap k v))])
-> [(Value' instr k, Value' instr v)]
-> [Value' instr (MapOpInp ('TMap k v))]
forall a b. (a -> b) -> a -> b
$ Map (Value' instr k) (Value' instr v)
-> [(Value' instr k, Value' instr v)]
forall k a. Map k a -> [(k, a)]
M.toAscList Map (Value' instr k) (Value' instr v)
m
  mapOpFromList :: Value' instr ('TMap k v)
-> [Value' instr b] -> Value' instr (MapOpRes ('TMap k v) b)
mapOpFromList (VMap m :: Map (Value' instr k) (Value' instr v)
m) l :: [Value' instr b]
l =
    Map (Value' instr k) (Value' instr b)
-> Value' instr (MapOpRes ('TMap k v) b)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' instr k) (Value' instr b)
 -> Value' instr (MapOpRes ('TMap k v) b))
-> Map (Value' instr k) (Value' instr b)
-> Value' instr (MapOpRes ('TMap k v) b)
forall a b. (a -> b) -> a -> b
$ [(Value' instr k, Value' instr b)]
-> Map (Value' instr k) (Value' instr b)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Value' instr k, Value' instr b)]
 -> Map (Value' instr k) (Value' instr b))
-> [(Value' instr k, Value' instr b)]
-> Map (Value' instr k) (Value' instr b)
forall a b. (a -> b) -> a -> b
$ [Value' instr k]
-> [Value' instr b] -> [(Value' instr k, Value' instr b)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Value' instr k, Value' instr v) -> Value' instr k)
-> [(Value' instr k, Value' instr v)] -> [Value' instr k]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (Value' instr k, Value' instr v) -> Value' instr k
forall a b. (a, b) -> a
fst ([(Value' instr k, Value' instr v)] -> [Value' instr k])
-> [(Value' instr k, Value' instr v)] -> [Value' instr k]
forall a b. (a -> b) -> a -> b
$ Map (Value' instr k) (Value' instr v)
-> [(Value' instr k, Value' instr v)]
forall k a. Map k a -> [(k, a)]
M.toAscList Map (Value' instr k) (Value' instr v)
m) [Value' instr b]
l
instance MapOp ('TList e) where
  type MapOpInp ('TList e) = e
  type MapOpRes ('TList e) = 'TList
  mapOpToList :: Value' instr ('TList e) -> [Value' instr (MapOpInp ('TList e))]
mapOpToList (VList l :: [Value' instr t]
l) = [Value' instr t]
[Value' instr (MapOpInp ('TList e))]
l
  mapOpFromList :: Value' instr ('TList e)
-> [Value' instr b] -> Value' instr (MapOpRes ('TList e) b)
mapOpFromList (VList _) l' :: [Value' instr b]
l' = [Value' instr b] -> Value' instr ('TList b)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' instr b]
l'
-- If you find it difficult to implement 'MapOp' for your datatype
-- because of order of type arguments in it, consider wrapping it
-- into a newtype.

class IterOp (c :: T) where
  type IterOpEl c :: T
  iterOpDetachOne ::
    Value' instr c -> (Maybe (Value' instr (IterOpEl c)), Value' instr c)
instance IterOp ('TMap k v) where
  type IterOpEl ('TMap k v) = 'TPair k v
  iterOpDetachOne :: Value' instr ('TMap k v)
-> (Maybe (Value' instr (IterOpEl ('TMap k v))),
    Value' instr ('TMap k v))
iterOpDetachOne (VMap m :: Map (Value' instr k) (Value' instr v)
m) =
    ((Value' instr k, Value' instr v) -> Value' instr ('TPair k v)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair ((Value' instr k, Value' instr v) -> Value' instr ('TPair k v))
-> Maybe (Value' instr k, Value' instr v)
-> Maybe (Value' instr ('TPair k v))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (Value' instr k) (Value' instr v)
-> Maybe (Value' instr k, Value' instr v)
forall k a. Map k a -> Maybe (k, a)
M.lookupMin Map (Value' instr k) (Value' instr v)
m, Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v))
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TMap k v)
forall a b. (a -> b) -> a -> b
$ Map (Value' instr k) (Value' instr v)
-> Map (Value' instr k) (Value' instr v)
forall k a. Map k a -> Map k a
M.deleteMin Map (Value' instr k) (Value' instr v)
m)
instance IterOp ('TList e) where
  type IterOpEl ('TList e) = e
  iterOpDetachOne :: Value' instr ('TList e)
-> (Maybe (Value' instr (IterOpEl ('TList e))),
    Value' instr ('TList e))
iterOpDetachOne (VList l :: [Value' instr t]
l) =
    case [Value' instr t]
l of
      x :: Value' instr t
x : xs :: [Value' instr t]
xs -> (Value' instr t -> Maybe (Value' instr t)
forall a. a -> Maybe a
Just Value' instr t
x, [Value' instr t] -> Value' instr ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' instr t]
xs)
      [] -> (Maybe (Value' instr (IterOpEl ('TList e)))
forall a. Maybe a
Nothing, [Value' instr e] -> Value' instr ('TList e)
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
[Value' instr t] -> Value' instr ('TList t)
VList [])
instance IterOp ('TSet e) where
  type IterOpEl ('TSet e) = e
  iterOpDetachOne :: Value' instr ('TSet e)
-> (Maybe (Value' instr (IterOpEl ('TSet e))),
    Value' instr ('TSet e))
iterOpDetachOne (VSet s :: Set (Value' instr t)
s) = (Set (Value' instr t) -> Maybe (Value' instr t)
forall a. Set a -> Maybe a
S.lookupMin Set (Value' instr t)
s, Set (Value' instr t) -> Value' instr ('TSet e)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet (Set (Value' instr t) -> Value' instr ('TSet e))
-> Set (Value' instr t) -> Value' instr ('TSet e)
forall a b. (a -> b) -> a -> b
$ Set (Value' instr t) -> Set (Value' instr t)
forall a. Set a -> Set a
S.deleteMin Set (Value' instr t)
s)

class SizeOp (c :: T) where
  evalSize :: Value' instr c -> Int
instance SizeOp 'TString where
  evalSize :: Value' instr 'TString -> Int
evalSize (VString s :: MText
s) = MText -> Int
forall t. Container t => t -> Int
length MText
s
instance SizeOp ('TBytes) where
  evalSize :: Value' instr 'TBytes -> Int
evalSize (VBytes b :: ByteString
b) = ByteString -> Int
forall t. Container t => t -> Int
length ByteString
b
instance SizeOp ('TSet a) where
  evalSize :: Value' instr ('TSet a) -> Int
evalSize (VSet s :: Set (Value' instr t)
s) = Set (Value' instr t) -> Int
forall a. Set a -> Int
S.size Set (Value' instr t)
s
instance SizeOp ('TList a) where
  evalSize :: Value' instr ('TList a) -> Int
evalSize (VList l :: [Value' instr t]
l) = [Value' instr t] -> Int
forall t. Container t => t -> Int
length [Value' instr t]
l
instance SizeOp ('TMap k v) where
  evalSize :: Value' instr ('TMap k v) -> Int
evalSize (VMap m :: Map (Value' instr k) (Value' instr v)
m) = Map (Value' instr k) (Value' instr v) -> Int
forall k a. Map k a -> Int
M.size Map (Value' instr k) (Value' instr v)
m

class UpdOp (c :: T) where
  type UpdOpKey c :: T
  type UpdOpParams c :: T
  evalUpd
    :: Value' instr (UpdOpKey c)
    -> Value' instr (UpdOpParams c) -> Value' instr c -> Value' instr c
instance UpdOp ('TMap k v) where
  type UpdOpKey ('TMap k v) = k
  type UpdOpParams ('TMap k v) = 'TOption v
  evalUpd :: Value' instr (UpdOpKey ('TMap k v))
-> Value' instr (UpdOpParams ('TMap k v))
-> Value' instr ('TMap k v)
-> Value' instr ('TMap k v)
evalUpd k :: Value' instr (UpdOpKey ('TMap k v))
k (VOption o :: Maybe (Value' instr t)
o) (VMap m :: Map (Value' instr k) (Value' instr v)
m) =
    case Maybe (Value' instr t)
o of
      Just newV :: Value' instr t
newV -> Map (Value' instr k) (Value' instr t) -> Value' instr ('TMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' instr k) (Value' instr t) -> Value' instr ('TMap k v))
-> Map (Value' instr k) (Value' instr t)
-> Value' instr ('TMap k v)
forall a b. (a -> b) -> a -> b
$ Value' instr k
-> Value' instr t
-> Map (Value' instr k) (Value' instr t)
-> Map (Value' instr k) (Value' instr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Value' instr k
Value' instr (UpdOpKey ('TMap k v))
k Value' instr t
newV Map (Value' instr k) (Value' instr t)
Map (Value' instr k) (Value' instr v)
m
      Nothing -> Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v)
VMap (Map (Value' instr k) (Value' instr v) -> Value' instr ('TMap k v))
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TMap k v)
forall a b. (a -> b) -> a -> b
$ Value' instr k
-> Map (Value' instr k) (Value' instr v)
-> Map (Value' instr k) (Value' instr v)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete Value' instr k
Value' instr (UpdOpKey ('TMap k v))
k Map (Value' instr k) (Value' instr v)
m
instance UpdOp ('TBigMap k v) where
  type UpdOpKey ('TBigMap k v) = k
  type UpdOpParams ('TBigMap k v) = 'TOption v
  evalUpd :: Value' instr (UpdOpKey ('TBigMap k v))
-> Value' instr (UpdOpParams ('TBigMap k v))
-> Value' instr ('TBigMap k v)
-> Value' instr ('TBigMap k v)
evalUpd k :: Value' instr (UpdOpKey ('TBigMap k v))
k (VOption o :: Maybe (Value' instr t)
o) (VBigMap m :: Map (Value' instr k) (Value' instr v)
m) =
    case Maybe (Value' instr t)
o of
      Just newV :: Value' instr t
newV -> Map (Value' instr k) (Value' instr t)
-> Value' instr ('TBigMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap (Map (Value' instr k) (Value' instr t)
 -> Value' instr ('TBigMap k v))
-> Map (Value' instr k) (Value' instr t)
-> Value' instr ('TBigMap k v)
forall a b. (a -> b) -> a -> b
$ Value' instr k
-> Value' instr t
-> Map (Value' instr k) (Value' instr t)
-> Map (Value' instr k) (Value' instr t)
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Value' instr k
Value' instr (UpdOpKey ('TBigMap k v))
k Value' instr t
newV Map (Value' instr k) (Value' instr t)
Map (Value' instr k) (Value' instr v)
m
      Nothing -> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
forall (k :: T) (v :: T) (instr :: [T] -> [T] -> *).
(KnownT k, KnownT v, Comparable k) =>
Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
VBigMap (Map (Value' instr k) (Value' instr v)
 -> Value' instr ('TBigMap k v))
-> Map (Value' instr k) (Value' instr v)
-> Value' instr ('TBigMap k v)
forall a b. (a -> b) -> a -> b
$ Value' instr k
-> Map (Value' instr k) (Value' instr v)
-> Map (Value' instr k) (Value' instr v)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete Value' instr k
Value' instr (UpdOpKey ('TBigMap k v))
k Map (Value' instr k) (Value' instr v)
m
instance UpdOp ('TSet a) where
  type UpdOpKey ('TSet a) = a
  type UpdOpParams ('TSet a) = 'TBool
  evalUpd :: Value' instr (UpdOpKey ('TSet a))
-> Value' instr (UpdOpParams ('TSet a))
-> Value' instr ('TSet a)
-> Value' instr ('TSet a)
evalUpd k :: Value' instr (UpdOpKey ('TSet a))
k (VBool b :: Bool
b) (VSet s :: Set (Value' instr t)
s) =
    case Bool
b of
      True -> Set (Value' instr t) -> Value' instr ('TSet a)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet (Set (Value' instr t) -> Value' instr ('TSet a))
-> Set (Value' instr t) -> Value' instr ('TSet a)
forall a b. (a -> b) -> a -> b
$ Value' instr t -> Set (Value' instr t) -> Set (Value' instr t)
forall a. Ord a => a -> Set a -> Set a
S.insert Value' instr t
Value' instr (UpdOpKey ('TSet a))
k Set (Value' instr t)
s
      False -> Set (Value' instr t) -> Value' instr ('TSet a)
forall (t :: T) (instr :: [T] -> [T] -> *).
(KnownT t, Comparable t) =>
Set (Value' instr t) -> Value' instr ('TSet t)
VSet (Set (Value' instr t) -> Value' instr ('TSet a))
-> Set (Value' instr t) -> Value' instr ('TSet a)
forall a b. (a -> b) -> a -> b
$ Value' instr t -> Set (Value' instr t) -> Set (Value' instr t)
forall a. Ord a => a -> Set a -> Set a
S.delete Value' instr t
Value' instr (UpdOpKey ('TSet a))
k Set (Value' instr t)
s

class GetOp (c :: T) where
  type GetOpKey c :: T
  type GetOpVal c :: T
  evalGet :: Value' instr (GetOpKey c) -> Value' instr c -> Maybe (Value' instr (GetOpVal c))
instance GetOp ('TBigMap k v) where
  type GetOpKey ('TBigMap k v) = k
  type GetOpVal ('TBigMap k v) = v
  evalGet :: Value' instr (GetOpKey ('TBigMap k v))
-> Value' instr ('TBigMap k v)
-> Maybe (Value' instr (GetOpVal ('TBigMap k v)))
evalGet k :: Value' instr (GetOpKey ('TBigMap k v))
k (VBigMap m :: Map (Value' instr k) (Value' instr v)
m) = Value' instr k
Value' instr (GetOpKey ('TBigMap k v))
k Value' instr k
-> Map (Value' instr k) (Value' instr v) -> Maybe (Value' instr v)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Value' instr k) (Value' instr v)
m
instance GetOp ('TMap k v) where
  type GetOpKey ('TMap k v) = k
  type GetOpVal ('TMap k v) = v
  evalGet :: Value' instr (GetOpKey ('TMap k v))
-> Value' instr ('TMap k v)
-> Maybe (Value' instr (GetOpVal ('TMap k v)))
evalGet k :: Value' instr (GetOpKey ('TMap k v))
k (VMap m :: Map (Value' instr k) (Value' instr v)
m) = Value' instr k
Value' instr (GetOpKey ('TMap k v))
k Value' instr k
-> Map (Value' instr k) (Value' instr v) -> Maybe (Value' instr v)
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map (Value' instr k) (Value' instr v)
m

class ConcatOp (c :: T) where
  evalConcat :: Value' instr c -> Value' instr c -> Value' instr c
  evalConcat' :: [Value' instr c] -> Value' instr c
instance ConcatOp ('TString) where
  evalConcat :: Value' instr 'TString
-> Value' instr 'TString -> Value' instr 'TString
evalConcat (VString s1 :: MText
s1) (VString s2 :: MText
s2) = (MText -> Value' instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString) (MText
s1 MText -> MText -> MText
forall a. Semigroup a => a -> a -> a
<> MText
s2)
  evalConcat' :: [Value' instr 'TString] -> Value' instr 'TString
evalConcat' l :: [Value' instr 'TString]
l =
    (forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString) (MText -> Value' instr 'TString) -> MText -> Value' instr 'TString
forall a b. (a -> b) -> a -> b
$ [MText] -> MText
forall a. Monoid a => [a] -> a
mconcat ([MText] -> MText) -> [MText] -> MText
forall a b. (a -> b) -> a -> b
$ (Value' instr 'TString -> MText)
-> [Value' instr 'TString] -> [MText]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (\(VString s :: MText
s) -> MText
s) [Value' instr 'TString]
l
instance ConcatOp ('TBytes) where
  evalConcat :: Value' instr 'TBytes
-> Value' instr 'TBytes -> Value' instr 'TBytes
evalConcat (VBytes b1 :: ByteString
b1) (VBytes b2 :: ByteString
b2) = ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString
b1 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> ByteString
b2)
  evalConcat' :: [Value' instr 'TBytes] -> Value' instr 'TBytes
evalConcat' l :: [Value' instr 'TBytes]
l =
    (forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes) (ByteString -> Value' instr 'TBytes)
-> ByteString -> Value' instr 'TBytes
forall a b. (a -> b) -> a -> b
$ (Element [Value' instr 'TBytes] -> ByteString -> ByteString)
-> ByteString -> [Value' instr 'TBytes] -> ByteString
forall t b. Container t => (Element t -> b -> b) -> b -> t -> b
foldr (ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
(<>) (ByteString -> ByteString -> ByteString)
-> (Value' instr 'TBytes -> ByteString)
-> Value' instr 'TBytes
-> ByteString
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(VBytes b :: ByteString
b) -> ByteString
b)) ByteString
forall a. Monoid a => a
mempty [Value' instr 'TBytes]
l

class SliceOp (c :: T) where
  evalSlice :: Natural -> Natural -> Value' instr c -> Maybe (Value' instr c)
instance SliceOp 'TString where
  evalSlice :: Natural
-> Natural
-> Value' instr 'TString
-> Maybe (Value' instr 'TString)
evalSlice o :: Natural
o l :: Natural
l (VString s :: MText
s) =
    MText -> Value' instr 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString (MText -> Value' instr 'TString)
-> Maybe MText -> Maybe (Value' instr 'TString)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> MText -> MText)
-> (Int -> MText -> MText)
-> Natural
-> Natural
-> MText
-> Maybe MText
forall str.
Container str =>
(Int -> str -> str)
-> (Int -> str -> str) -> Natural -> Natural -> str -> Maybe str
sliceImpl Int -> MText -> MText
dropMText Int -> MText -> MText
takeMText Natural
o Natural
l MText
s
instance SliceOp 'TBytes where
  evalSlice :: Natural
-> Natural -> Value' instr 'TBytes -> Maybe (Value' instr 'TBytes)
evalSlice o :: Natural
o l :: Natural
l (VBytes b :: ByteString
b) =
    ByteString -> Value' instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' instr 'TBytes)
-> Maybe ByteString -> Maybe (Value' instr 'TBytes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> ByteString -> ByteString)
-> (Int -> ByteString -> ByteString)
-> Natural
-> Natural
-> ByteString
-> Maybe ByteString
forall str.
Container str =>
(Int -> str -> str)
-> (Int -> str -> str) -> Natural -> Natural -> str -> Maybe str
sliceImpl Int -> ByteString -> ByteString
B.drop Int -> ByteString -> ByteString
B.take Natural
o Natural
l ByteString
b

sliceImpl ::
  Container str
  => (Int -> str -> str)
  -> (Int -> str -> str)
  -> Natural
  -> Natural
  -> str
  -> Maybe str
sliceImpl :: (Int -> str -> str)
-> (Int -> str -> str) -> Natural -> Natural -> str -> Maybe str
sliceImpl dropF :: Int -> str -> str
dropF takeF :: Int -> str -> str
takeF offset :: Natural
offset l :: Natural
l s :: str
s
  | Natural
offset Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (str -> Int
forall t. Container t => t -> Int
length str
s) Bool -> Bool -> Bool
|| Natural
offset Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
l Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (str -> Int
forall t. Container t => t -> Int
length str
s) =
    Maybe str
forall a. Maybe a
Nothing
  | Bool
otherwise
  -- Drop offset and then take requested number of items.
   = str -> Maybe str
forall a. a -> Maybe a
Just (str -> Maybe str) -> (str -> str) -> str -> Maybe str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> str -> str
takeF (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
l) (str -> str) -> (str -> str) -> str -> str
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> str -> str
dropF (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
offset) (str -> Maybe str) -> str -> Maybe str
forall a b. (a -> b) -> a -> b
$ str
s

class EDivOp (n :: T) (m :: T) where
  type EDivOpRes n m :: T
  type EModOpRes n m :: T

  -- | Converge the notes of given operands.
  convergeEDiv
    :: Notes n
    -> Notes m
    -> Either AnnConvergeError
        (Notes ('TOption ('TPair (EDivOpRes n m)
                                  (EModOpRes n m))))

  evalEDivOp
    :: Value' instr n
    -> Value' instr m
    -> Value' instr ('TOption ('TPair (EDivOpRes n m)
                                     (EModOpRes n m)))

instance EDivOp 'TInt 'TInt where
  type EDivOpRes 'TInt 'TInt = 'TInt
  type EModOpRes 'TInt 'TInt = 'TNat
  convergeEDiv :: Notes 'TInt
-> Notes 'TInt
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt))))
convergeEDiv n1 :: Notes 'TInt
n1 n2 :: Notes 'TInt
n2 =
    (\a :: Notes 'TInt
a -> TypeAnn
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TInt 'TNat)
 -> Notes ('TOption ('TPair 'TInt 'TNat)))
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TInt
-> Notes 'TNat
-> Notes ('TPair 'TInt 'TNat)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn Notes 'TInt
a (Notes 'TNat -> Notes ('TPair 'TInt 'TNat))
-> Notes 'TNat -> Notes ('TPair 'TInt 'TNat)
forall a b. (a -> b) -> a -> b
$ TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall k (a :: k). Annotation a
noAnn)
      (Notes 'TInt -> Notes ('TOption ('TPair 'TInt 'TNat)))
-> Either AnnConvergeError (Notes 'TInt)
-> Either AnnConvergeError (Notes ('TOption ('TPair 'TInt 'TNat)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notes 'TInt -> Notes 'TInt -> Either AnnConvergeError (Notes 'TInt)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TInt
n1 Notes 'TInt
n2
  evalEDivOp :: Value' instr 'TInt
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
evalEDivOp (VInt i :: Integer
i) (VInt j :: Integer
j) =
    if Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. Maybe a
Nothing
      else Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TInt) (EModOpRes 'TInt 'TInt)))
forall a b. (a -> b) -> a -> b
$ Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. a -> Maybe a
Just (Value' instr ('TPair 'TInt 'TNat)
 -> Maybe (Value' instr ('TPair 'TInt 'TNat)))
-> Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$
        (Value' instr 'TInt, Value' instr 'TNat)
-> Value' instr ('TPair 'TInt 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
divMich Integer
i Integer
j), Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' instr 'TNat) -> Natural -> Value' instr 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
modMich Integer
i Integer
j)
instance EDivOp 'TInt 'TNat where
  type EDivOpRes 'TInt 'TNat = 'TInt
  type EModOpRes 'TInt 'TNat = 'TNat
  convergeEDiv :: Notes 'TInt
-> Notes 'TNat
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))))
convergeEDiv n1 :: Notes 'TInt
n1 _ = Notes ('TOption ('TPair 'TInt 'TNat))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))))
forall a b. b -> Either a b
Right (Notes ('TOption ('TPair 'TInt 'TNat))
 -> Either
      AnnConvergeError
      (Notes
         ('TOption
            ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))))
-> Notes ('TOption ('TPair 'TInt 'TNat))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TInt 'TNat)
 -> Notes ('TOption ('TPair 'TInt 'TNat)))
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TInt
-> Notes 'TNat
-> Notes ('TPair 'TInt 'TNat)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn Notes 'TInt
n1
    (Notes 'TNat -> Notes ('TPair 'TInt 'TNat))
-> Notes 'TNat -> Notes ('TPair 'TInt 'TNat)
forall a b. (a -> b) -> a -> b
$ TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall k (a :: k). Annotation a
noAnn
  evalEDivOp :: Value' instr 'TInt
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
evalEDivOp (VInt i :: Integer
i) (VNat j :: Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. Maybe a
Nothing
      else Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TInt 'TNat) (EModOpRes 'TInt 'TNat)))
forall a b. (a -> b) -> a -> b
$ Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. a -> Maybe a
Just (Value' instr ('TPair 'TInt 'TNat)
 -> Maybe (Value' instr ('TPair 'TInt 'TNat)))
-> Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$
        (Value' instr 'TInt, Value' instr 'TNat)
-> Value' instr ('TPair 'TInt 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
divMich Integer
i (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j)), Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' instr 'TNat) -> Natural -> Value' instr 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
modMich Integer
i (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
j))
instance EDivOp 'TNat 'TInt where
  type EDivOpRes 'TNat 'TInt = 'TInt
  type EModOpRes 'TNat 'TInt = 'TNat
  convergeEDiv :: Notes 'TNat
-> Notes 'TInt
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))))
convergeEDiv n1 :: Notes 'TNat
n1 _ = Notes ('TOption ('TPair 'TInt 'TNat))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))))
forall a b. b -> Either a b
Right (Notes ('TOption ('TPair 'TInt 'TNat))
 -> Either
      AnnConvergeError
      (Notes
         ('TOption
            ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))))
-> Notes ('TOption ('TPair 'TInt 'TNat))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TInt 'TNat)
 -> Notes ('TOption ('TPair 'TInt 'TNat)))
-> Notes ('TPair 'TInt 'TNat)
-> Notes ('TOption ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TInt
-> Notes 'TNat
-> Notes ('TPair 'TInt 'TNat)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn
    (TypeAnn -> Notes 'TInt
NTInt TypeAnn
forall k (a :: k). Annotation a
noAnn) Notes 'TNat
n1
  evalEDivOp :: Value' instr 'TNat
-> Value' instr 'TInt
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
evalEDivOp (VNat i :: Natural
i) (VInt j :: Integer
j) =
    if Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. Maybe a
Nothing
      else Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TInt 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))))
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt)))
forall a b. (a -> b) -> a -> b
$ Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a. a -> Maybe a
Just (Value' instr ('TPair 'TInt 'TNat)
 -> Maybe (Value' instr ('TPair 'TInt 'TNat)))
-> Value' instr ('TPair 'TInt 'TNat)
-> Maybe (Value' instr ('TPair 'TInt 'TNat))
forall a b. (a -> b) -> a -> b
$
        (Value' instr 'TInt, Value' instr 'TNat)
-> Value' instr ('TPair 'TInt 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Integer -> Value' instr 'TInt
forall (instr :: [T] -> [T] -> *). Integer -> Value' instr 'TInt
VInt (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
divMich (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) Integer
j), Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' instr 'TNat) -> Natural -> Value' instr 'TNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer -> Natural) -> Integer -> Natural
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
modMich (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
i) Integer
j)
instance EDivOp 'TNat 'TNat where
  type EDivOpRes 'TNat 'TNat = 'TNat
  type EModOpRes 'TNat 'TNat = 'TNat
  convergeEDiv :: Notes 'TNat
-> Notes 'TNat
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat))))
convergeEDiv n1 :: Notes 'TNat
n1 n2 :: Notes 'TNat
n2 = (\a :: Notes 'TNat
a -> TypeAnn
-> Notes ('TPair 'TNat 'TNat)
-> Notes ('TOption ('TPair 'TNat 'TNat))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TNat 'TNat)
 -> Notes ('TOption ('TPair 'TNat 'TNat)))
-> Notes ('TPair 'TNat 'TNat)
-> Notes ('TOption ('TPair 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TNat
-> Notes 'TNat
-> Notes ('TPair 'TNat 'TNat)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn Notes 'TNat
a Notes 'TNat
a)
    (Notes 'TNat -> Notes ('TOption ('TPair 'TNat 'TNat)))
-> Either AnnConvergeError (Notes 'TNat)
-> Either AnnConvergeError (Notes ('TOption ('TPair 'TNat 'TNat)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notes 'TNat -> Notes 'TNat -> Either AnnConvergeError (Notes 'TNat)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TNat
n1 Notes 'TNat
n2
  evalEDivOp :: Value' instr 'TNat
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
evalEDivOp (VNat i :: Natural
i) (VNat j :: Natural
j) =
    if Natural
j Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then Maybe (Value' instr ('TPair 'TNat 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TNat 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat))))
-> Maybe (Value' instr ('TPair 'TNat 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
forall a b. (a -> b) -> a -> b
$ Maybe (Value' instr ('TPair 'TNat 'TNat))
forall a. Maybe a
Nothing
      else Maybe (Value' instr ('TPair 'TNat 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TNat 'TNat))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat))))
-> Maybe (Value' instr ('TPair 'TNat 'TNat))
-> Value'
     instr
     ('TOption ('TPair (EDivOpRes 'TNat 'TNat) (EModOpRes 'TNat 'TNat)))
forall a b. (a -> b) -> a -> b
$ Value' instr ('TPair 'TNat 'TNat)
-> Maybe (Value' instr ('TPair 'TNat 'TNat))
forall a. a -> Maybe a
Just (Value' instr ('TPair 'TNat 'TNat)
 -> Maybe (Value' instr ('TPair 'TNat 'TNat)))
-> Value' instr ('TPair 'TNat 'TNat)
-> Maybe (Value' instr ('TPair 'TNat 'TNat))
forall a b. (a -> b) -> a -> b
$
        (Value' instr 'TNat, Value' instr 'TNat)
-> Value' instr ('TPair 'TNat 'TNat)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
divMich Natural
i Natural
j), Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Natural -> Value' instr 'TNat) -> Natural -> Value' instr 'TNat
forall a b. (a -> b) -> a -> b
$ (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
modMich Natural
i Natural
j))
instance EDivOp 'TMutez 'TMutez where
  type EDivOpRes 'TMutez 'TMutez = 'TNat
  type EModOpRes 'TMutez 'TMutez = 'TMutez
  convergeEDiv :: Notes 'TMutez
-> Notes 'TMutez
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez))))
convergeEDiv n1 :: Notes 'TMutez
n1 n2 :: Notes 'TMutez
n2 = (\a :: Notes 'TMutez
a -> TypeAnn
-> Notes ('TPair 'TNat 'TMutez)
-> Notes ('TOption ('TPair 'TNat 'TMutez))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TNat 'TMutez)
 -> Notes ('TOption ('TPair 'TNat 'TMutez)))
-> Notes ('TPair 'TNat 'TMutez)
-> Notes ('TOption ('TPair 'TNat 'TMutez))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TNat
-> Notes 'TMutez
-> Notes ('TPair 'TNat 'TMutez)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn (TypeAnn -> Notes 'TNat
NTNat TypeAnn
forall k (a :: k). Annotation a
noAnn) Notes 'TMutez
a)
    (Notes 'TMutez -> Notes ('TOption ('TPair 'TNat 'TMutez)))
-> Either AnnConvergeError (Notes 'TMutez)
-> Either
     AnnConvergeError (Notes ('TOption ('TPair 'TNat 'TMutez)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Notes 'TMutez
-> Notes 'TMutez -> Either AnnConvergeError (Notes 'TMutez)
forall (t :: T).
Notes t -> Notes t -> Either AnnConvergeError (Notes t)
converge Notes 'TMutez
n1 Notes 'TMutez
n2
  evalEDivOp :: Value' instr 'TMutez
-> Value' instr 'TMutez
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez)))
evalEDivOp (VMutez i :: Mutez
i) (VMutez j :: Mutez
j) =
    Maybe (Value' instr ('TPair 'TNat 'TMutez))
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TNat 'TMutez))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez))))
-> Maybe (Value' instr ('TPair 'TNat 'TMutez))
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TMutez) (EModOpRes 'TMutez 'TMutez)))
forall a b. (a -> b) -> a -> b
$
    Mutez
i Mutez -> Mutez -> Maybe (Word64, Mutez)
`divModMutez` Mutez
j Maybe (Word64, Mutez)
-> ((Word64, Mutez) -> Value' instr ('TPair 'TNat 'TMutez))
-> Maybe (Value' instr ('TPair 'TNat 'TMutez))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      (quotient :: Word64
quotient, remainder :: Mutez
remainder) ->
        (Value' instr 'TNat, Value' instr 'TMutez)
-> Value' instr ('TPair 'TNat 'TMutez)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Natural -> Value' instr 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat (Word64 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
quotient), Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
remainder)

instance EDivOp 'TMutez 'TNat where
  type EDivOpRes 'TMutez 'TNat = 'TMutez
  type EModOpRes 'TMutez 'TNat = 'TMutez
  convergeEDiv :: Notes 'TMutez
-> Notes 'TNat
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))))
convergeEDiv n1 :: Notes 'TMutez
n1 _ = Notes ('TOption ('TPair 'TMutez 'TMutez))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))))
forall a b. b -> Either a b
Right (Notes ('TOption ('TPair 'TMutez 'TMutez))
 -> Either
      AnnConvergeError
      (Notes
         ('TOption
            ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))))
-> Notes ('TOption ('TPair 'TMutez 'TMutez))
-> Either
     AnnConvergeError
     (Notes
        ('TOption
           ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> Notes ('TPair 'TMutez 'TMutez)
-> Notes ('TOption ('TPair 'TMutez 'TMutez))
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
forall k (a :: k). Annotation a
noAnn (Notes ('TPair 'TMutez 'TMutez)
 -> Notes ('TOption ('TPair 'TMutez 'TMutez)))
-> Notes ('TPair 'TMutez 'TMutez)
-> Notes ('TOption ('TPair 'TMutez 'TMutez))
forall a b. (a -> b) -> a -> b
$ TypeAnn
-> FieldAnn
-> FieldAnn
-> Notes 'TMutez
-> Notes 'TMutez
-> Notes ('TPair 'TMutez 'TMutez)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TPair p q)
NTPair TypeAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn FieldAnn
forall k (a :: k). Annotation a
noAnn Notes 'TMutez
n1 Notes 'TMutez
n1
  evalEDivOp :: Value' instr 'TMutez
-> Value' instr 'TNat
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))
evalEDivOp (VMutez i :: Mutez
i) (VNat j :: Natural
j) =
    Maybe (Value' instr ('TPair 'TMutez 'TMutez))
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))
forall (t :: T) (instr :: [T] -> [T] -> *).
KnownT t =>
Maybe (Value' instr t) -> Value' instr ('TOption t)
VOption (Maybe (Value' instr ('TPair 'TMutez 'TMutez))
 -> Value'
      instr
      ('TOption
         ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))))
-> Maybe (Value' instr ('TPair 'TMutez 'TMutez))
-> Value'
     instr
     ('TOption
        ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat)))
forall a b. (a -> b) -> a -> b
$
    Mutez
i Mutez -> Natural -> Maybe (Mutez, Mutez)
forall a. Integral a => Mutez -> a -> Maybe (Mutez, Mutez)
`divModMutezInt` Natural
j Maybe (Mutez, Mutez)
-> ((Mutez, Mutez) -> Value' instr ('TPair 'TMutez 'TMutez))
-> Maybe (Value' instr ('TPair 'TMutez 'TMutez))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
      (quotient :: Mutez
quotient, remainder :: Mutez
remainder) ->
        (Value' instr 'TMutez, Value' instr 'TMutez)
-> Value' instr ('TPair 'TMutez 'TMutez)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
quotient, Mutez -> Value' instr 'TMutez
forall (instr :: [T] -> [T] -> *). Mutez -> Value' instr 'TMutez
VMutez Mutez
remainder)

-- | Computing 'div' function in Michelson style.
-- When divisor is negative, Haskell gives x as integer part,
-- while Michelson gives x+1.
divMich :: Integral a => a -> a -> a
divMich :: a -> a -> a
divMich divisible :: a
divisible divisor :: a
divisor = a
divisible a -> a -> a
forall a. Integral a => a -> a -> a
`div` a
divisor a -> a -> a
forall a. Num a => a -> a -> a
+ a
extra
  where
    extra :: a
extra =
      if a
divisor a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> 0 Bool -> Bool -> Bool
||
         a
divisible a -> a -> a
forall a. Integral a => a -> a -> a
`mod` a
divisor a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then 0
      else 1

-- | Computing 'mod' function in Michelson style.
-- When divisor is negative, Haskell gives a negative modulo,
-- while there is a positive modulo in Michelson.
modMich :: Integral a => a -> a -> a
modMich :: a -> a -> a
modMich divisible :: a
divisible divisor :: a
divisor = a
divisible a -> a -> a
forall a. Num a => a -> a -> a
- a
divisor a -> a -> a
forall a. Num a => a -> a -> a
* a
intPart
  where intPart :: a
intPart = a -> a -> a
forall a. Integral a => a -> a -> a
divMich a
divisible a
divisor