module Lorentz.Errors.Numeric.Contract
( ErrorTagMap
, ErrorTagExclusions
, gatherErrorTags
, addNewErrorTags
, buildErrorTagMap
, excludeErrorTags
, applyErrorTagMap
, applyErrorTagMapWithExclusions
, useNumericErrors
, errorFromValNumeric
, errorToValNumeric
) where
import Data.Bimap (Bimap)
import qualified Data.Bimap as Bimap
import Data.Default (def)
import qualified Data.HashSet as HS
import Data.Singletons (withSingI)
import Fmt (pretty)
import Lorentz.Base
import Lorentz.Errors
import Morley.Michelson.Analyzer
import Morley.Michelson.FailPattern
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed
type ErrorTagMap = Bimap Natural MText
type ErrorTagExclusions = HashSet MText
gatherErrorTags :: inp :-> out -> HashSet MText
gatherErrorTags :: (inp :-> out) -> HashSet MText
gatherErrorTags = HashMap MText () -> HashSet MText
forall a. HashMap a () -> HashSet a
HS.fromMap (HashMap MText () -> HashSet MText)
-> ((inp :-> out) -> HashMap MText ())
-> (inp :-> out)
-> HashSet MText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap MText Word -> HashMap MText ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (HashMap MText Word -> HashMap MText ())
-> ((inp :-> out) -> HashMap MText Word)
-> (inp :-> out)
-> HashMap MText ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnalyzerRes -> HashMap MText Word
arErrorTags (AnalyzerRes -> HashMap MText Word)
-> ((inp :-> out) -> AnalyzerRes)
-> (inp :-> out)
-> HashMap MText Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr (ToTs inp) (ToTs out) -> AnalyzerRes
forall (inp :: [T]) (out :: [T]). Instr inp out -> AnalyzerRes
analyze (Instr (ToTs inp) (ToTs out) -> AnalyzerRes)
-> ((inp :-> out) -> Instr (ToTs inp) (ToTs out))
-> (inp :-> out)
-> AnalyzerRes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (inp :-> out) -> Instr (ToTs inp) (ToTs out)
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> Instr (ToTs inp) (ToTs out)
iAnyCode
addNewErrorTags :: ErrorTagMap -> HashSet MText -> ErrorTagMap
addNewErrorTags :: ErrorTagMap -> HashSet MText -> ErrorTagMap
addNewErrorTags ErrorTagMap
existingMap HashSet MText
newTags =
(ErrorTagMap -> Element [(Natural, MText)] -> ErrorTagMap)
-> ErrorTagMap -> [(Natural, MText)] -> ErrorTagMap
forall t b. Container t => (b -> Element t -> b) -> b -> t -> b
foldl' (((Natural, MText) -> ErrorTagMap -> ErrorTagMap)
-> ErrorTagMap -> (Natural, MText) -> ErrorTagMap
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Natural, MText) -> ErrorTagMap -> ErrorTagMap)
-> ErrorTagMap -> (Natural, MText) -> ErrorTagMap)
-> ((Natural, MText) -> ErrorTagMap -> ErrorTagMap)
-> ErrorTagMap
-> (Natural, MText)
-> ErrorTagMap
forall a b. (a -> b) -> a -> b
$ (Natural -> MText -> ErrorTagMap -> ErrorTagMap)
-> (Natural, MText) -> ErrorTagMap -> ErrorTagMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Natural -> MText -> ErrorTagMap -> ErrorTagMap
forall a b. (Ord a, Ord b) => a -> b -> Bimap a b -> Bimap a b
Bimap.tryInsert) ErrorTagMap
existingMap [(Natural, MText)]
newItems
where
firstUnusedNumeric :: Natural
firstUnusedNumeric
| ErrorTagMap -> Bool
forall a b. Bimap a b -> Bool
Bimap.null ErrorTagMap
existingMap = Natural
0
| Bool
otherwise = (Natural, MText) -> Natural
forall a b. (a, b) -> a
fst (ErrorTagMap -> (Natural, MText)
forall a b. Bimap a b -> (a, b)
Bimap.findMax ErrorTagMap
existingMap) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1
newItems :: [(Natural, MText)]
newItems :: [(Natural, MText)]
newItems = [Natural] -> [MText] -> [(Natural, MText)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Natural
firstUnusedNumeric .. ] (HashSet MText -> [Element (HashSet MText)]
forall t. Container t => t -> [Element t]
toList HashSet MText
newTags)
buildErrorTagMap :: HashSet MText -> ErrorTagMap
buildErrorTagMap :: HashSet MText -> ErrorTagMap
buildErrorTagMap = ErrorTagMap -> HashSet MText -> ErrorTagMap
addNewErrorTags ErrorTagMap
forall a b. Bimap a b
Bimap.empty
excludeErrorTags
:: HasCallStack
=> ErrorTagExclusions -> ErrorTagMap -> ErrorTagMap
excludeErrorTags :: HashSet MText -> ErrorTagMap -> ErrorTagMap
excludeErrorTags HashSet MText
toExclude ErrorTagMap
errMap =
(ErrorTagMap -> Element (HashSet MText) -> ErrorTagMap)
-> ErrorTagMap -> HashSet MText -> ErrorTagMap
forall t b. Container t => (b -> Element t -> b) -> b -> t -> b
foldl' ((MText -> ErrorTagMap -> ErrorTagMap)
-> ErrorTagMap -> MText -> ErrorTagMap
forall a b c. (a -> b -> c) -> b -> a -> c
flip MText -> ErrorTagMap -> ErrorTagMap
forall a a. (Ord a, Ord a, Show a) => a -> Bimap a a -> Bimap a a
deleteExistingR) ErrorTagMap
errMap HashSet MText
toExclude
where
deleteExistingR :: a -> Bimap a a -> Bimap a a
deleteExistingR a
k Bimap a a
m = case a -> Bimap a a -> Maybe a
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR a
k Bimap a a
m of
Just a
_ -> a -> Bimap a a -> Bimap a a
forall a b. (Ord a, Ord b) => b -> Bimap a b -> Bimap a b
Bimap.deleteR a
k Bimap a a
m
Maybe a
Nothing ->
Text -> Bimap a a
forall a. HasCallStack => Text -> a
error (Text -> Bimap a a) -> Text -> Bimap a a
forall a b. (a -> b) -> a -> b
$ Text
"Tag " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall b a. (Show a, IsString b) => a -> b
show a
k Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" does not appear in the contract"
applyErrorTagMap :: HasCallStack => ErrorTagMap -> inp :-> out -> inp :-> out
applyErrorTagMap :: ErrorTagMap -> (inp :-> out) -> inp :-> out
applyErrorTagMap ErrorTagMap
errorTagMap = ErrorTagMap -> HashSet MText -> (inp :-> out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
ErrorTagMap -> HashSet MText -> (inp :-> out) -> inp :-> out
applyErrorTagMapWithExclusions ErrorTagMap
errorTagMap HashSet MText
forall a. Monoid a => a
mempty
applyErrorTagMapWithExclusions
:: HasCallStack
=> ErrorTagMap -> ErrorTagExclusions -> inp :-> out -> inp :-> out
applyErrorTagMapWithExclusions :: ErrorTagMap -> HashSet MText -> (inp :-> out) -> inp :-> out
applyErrorTagMapWithExclusions ErrorTagMap
errorTagMap HashSet MText
exclusions =
(forall (o' :: [T]). Instr (ToTs inp) o' -> Instr (ToTs inp) o')
-> (inp :-> out) -> inp :-> out
forall (i1 :: [*]) (i2 :: [*]) (o :: [*]).
(forall (o' :: [T]). Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o) -> i2 :-> o
iMapAnyCode (ErrorTagMap
-> HashSet MText -> Instr (ToTs inp) o' -> Instr (ToTs inp) o'
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
ErrorTagMap -> HashSet MText -> Instr inp out -> Instr inp out
applyErrorTagMapWithExcT ErrorTagMap
errorTagMap HashSet MText
exclusions)
useNumericErrors ::
HasCallStack => inp :-> out -> (inp :-> out, ErrorTagMap)
useNumericErrors :: (inp :-> out) -> (inp :-> out, ErrorTagMap)
useNumericErrors inp :-> out
instr = (ErrorTagMap -> (inp :-> out) -> inp :-> out
forall (inp :: [*]) (out :: [*]).
HasCallStack =>
ErrorTagMap -> (inp :-> out) -> inp :-> out
applyErrorTagMap ErrorTagMap
errorTagMap inp :-> out
instr, ErrorTagMap
errorTagMap)
where
errorTagMap :: ErrorTagMap
errorTagMap = HashSet MText -> ErrorTagMap
buildErrorTagMap (HashSet MText -> ErrorTagMap) -> HashSet MText -> ErrorTagMap
forall a b. (a -> b) -> a -> b
$ (inp :-> out) -> HashSet MText
forall (inp :: [*]) (out :: [*]). (inp :-> out) -> HashSet MText
gatherErrorTags inp :-> out
instr
applyErrorTagMapWithExcT ::
HasCallStack
=> ErrorTagMap
-> ErrorTagExclusions
-> Instr inp out
-> Instr inp out
applyErrorTagMapWithExcT :: ErrorTagMap -> HashSet MText -> Instr inp out -> Instr inp out
applyErrorTagMapWithExcT ErrorTagMap
errorTagMap HashSet MText
exclusions Instr inp out
instr =
DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> Instr i o)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> Instr i o)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings ()
dfsSettings forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> Instr inp out
forall (i :: [T]) (o :: [T]). Instr i o -> Instr i o
step Instr inp out
instr
where
dfsSettings :: DfsSettings ()
dfsSettings :: DfsSettings ()
dfsSettings = DfsSettings ()
forall a. Default a => a
def
{ dsGoToValues :: Bool
dsGoToValues = Bool
True
}
tagToNatValue :: HasCallStack => MText -> SomeConstrainedValue ConstantScope
tagToNatValue :: MText -> SomeConstrainedValue ConstantScope
tagToNatValue MText
tag =
case (MText -> HashSet MText -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member MText
tag HashSet MText
exclusions, MText -> ErrorTagMap -> Maybe Natural
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR MText
tag ErrorTagMap
errorTagMap) of
(Bool
True, Maybe Natural
_) -> Value 'TString -> SomeConstrainedValue ConstantScope
forall (t :: T) (c :: T -> Constraint).
c t =>
Value t -> SomeConstrainedValue c
SomeConstrainedValue (MText -> Value 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
tag)
(Bool
False, Maybe Natural
Nothing) -> Text -> SomeConstrainedValue ConstantScope
forall a. HasCallStack => Text -> a
error (Text -> SomeConstrainedValue ConstantScope)
-> Text -> SomeConstrainedValue ConstantScope
forall a b. (a -> b) -> a -> b
$ Text
"Can't find a tag: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> MText -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty MText
tag
(Bool
False, Just Natural
n) -> Value 'TNat -> SomeConstrainedValue ConstantScope
forall (t :: T) (c :: T -> Constraint).
c t =>
Value t -> SomeConstrainedValue c
SomeConstrainedValue (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
n)
step :: HasCallStack => Instr inp out -> Instr inp out
step :: Instr inp out -> Instr inp out
step = (MText -> SomeConstrainedValue ConstantScope)
-> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
(MText -> SomeConstrainedValue ConstantScope)
-> Instr inp out -> Instr inp out
modifyTypicalFailWith HasCallStack => MText -> SomeConstrainedValue ConstantScope
MText -> SomeConstrainedValue ConstantScope
tagToNatValue
errorFromValNumeric ::
(SingI t, IsError e) => ErrorTagMap -> Value t -> Either Text e
errorFromValNumeric :: ErrorTagMap -> Value t -> Either Text e
errorFromValNumeric ErrorTagMap
errorTagMap Value t
v =
case Value t
v of
VNat Natural
tag
| Just MText
textualTag <- Natural -> ErrorTagMap -> Maybe MText
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup Natural
tag ErrorTagMap
errorTagMap ->
Value 'TString -> Either Text e
forall e (t :: T). (IsError e, SingI t) => Value t -> Either Text e
errorFromVal (Value 'TString -> Either Text e)
-> Value 'TString -> Either Text e
forall a b. (a -> b) -> a -> b
$ MText -> Value 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
textualTag
(VPair (VNat Natural
tag, Value' Instr r
something) :: Value pair)
| Just MText
textualTag <- Natural -> ErrorTagMap -> Maybe MText
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup Natural
tag ErrorTagMap
errorTagMap ->
case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @pair of
STPair l r -> Sing 'TNat -> (SingI 'TNat => Either Text e) -> Either Text e
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
Sing 'TNat
l ((SingI 'TNat => Either Text e) -> Either Text e)
-> (SingI 'TNat => Either Text e) -> Either Text e
forall a b. (a -> b) -> a -> b
$ Sing r -> (SingI r => Either Text e) -> Either Text e
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
Sing n2
r ((SingI r => Either Text e) -> Either Text e)
-> (SingI r => Either Text e) -> Either Text e
forall a b. (a -> b) -> a -> b
$
Value ('TPair 'TString r) -> Either Text e
forall e (t :: T). (IsError e, SingI t) => Value t -> Either Text e
errorFromVal (Value ('TPair 'TString r) -> Either Text e)
-> Value ('TPair 'TString r) -> Either Text e
forall a b. (a -> b) -> a -> b
$ (Value 'TString, Value' Instr r) -> Value ('TPair 'TString r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (MText -> Value 'TString
forall (instr :: [T] -> [T] -> *). MText -> Value' instr 'TString
VString MText
textualTag, Value' Instr r
something)
Value t
_ -> Value t -> Either Text e
forall e (t :: T). (IsError e, SingI t) => Value t -> Either Text e
errorFromVal Value t
v
errorToValNumeric ::
IsError e => ErrorTagMap -> e -> (forall t. ConstantScope t => Value t -> r) -> r
errorToValNumeric :: ErrorTagMap
-> e -> (forall (t :: T). ConstantScope t => Value t -> r) -> r
errorToValNumeric ErrorTagMap
errorTagMap e
e forall (t :: T). ConstantScope t => Value t -> r
cont =
e -> (forall (t :: T). ConstantScope t => Value t -> r) -> r
forall e r.
IsError e =>
e -> (forall (t :: T). ErrorScope t => Value t -> r) -> r
errorToVal e
e ((forall (t :: T). ConstantScope t => Value t -> r) -> r)
-> (forall (t :: T). ConstantScope t => Value t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \case
VString MText
textualTag
| Just Natural
tag <- MText -> ErrorTagMap -> Maybe Natural
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR MText
textualTag ErrorTagMap
errorTagMap -> Value 'TNat -> r
forall (t :: T). ConstantScope t => Value t -> r
cont (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
tag)
(VPair (VString MText
textualTag, Value' Instr r
something) :: Value pair)
| Just Natural
tag <- MText -> ErrorTagMap -> Maybe Natural
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
b -> Bimap a b -> m a
Bimap.lookupR MText
textualTag ErrorTagMap
errorTagMap ->
case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @pair of
STPair l r ->
Sing 'TString -> (SingI 'TString => r) -> r
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
Sing 'TString
l ((SingI 'TString => r) -> r) -> (SingI 'TString => r) -> r
forall a b. (a -> b) -> a -> b
$ Sing r -> (SingI r => r) -> r
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing r
Sing n2
r ((SingI r => r) -> r) -> (SingI r => r) -> r
forall a b. (a -> b) -> a -> b
$ Value ('TPair 'TNat r) -> r
forall (t :: T). ConstantScope t => Value t -> r
cont ((Value 'TNat, Value' Instr r) -> Value ('TPair 'TNat r)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Natural -> Value 'TNat
forall (instr :: [T] -> [T] -> *). Natural -> Value' instr 'TNat
VNat Natural
tag, Value' Instr r
something))
Value t
v -> Value t -> r
forall (t :: T). ConstantScope t => Value t -> r
cont Value t
v