diff --git a/kore/kore.cabal b/kore/kore.cabal index 86f148467f..bfc29945a3 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -174,7 +174,10 @@ library Kore.Internal.Condition Kore.Internal.Conditional Kore.Internal.Inj + Kore.Internal.InternalBool Kore.Internal.InternalBytes + Kore.Internal.InternalInt + Kore.Internal.InternalString Kore.Internal.MultiAnd Kore.Internal.MultiOr Kore.Internal.OrCondition @@ -287,7 +290,10 @@ library Kore.Step.Simplification.Inhabitant Kore.Step.Simplification.Inj Kore.Step.Simplification.InjSimplifier + Kore.Step.Simplification.InternalBool Kore.Step.Simplification.InternalBytes + Kore.Step.Simplification.InternalInt + Kore.Step.Simplification.InternalString Kore.Step.Simplification.Mu Kore.Step.Simplification.Next Kore.Step.Simplification.NoConfusion diff --git a/kore/src/Kore/Attribute/Pattern/ConstructorLike.hs b/kore/src/Kore/Attribute/Pattern/ConstructorLike.hs index 2de7133984..44eb545186 100644 --- a/kore/src/Kore/Attribute/Pattern/ConstructorLike.hs +++ b/kore/src/Kore/Attribute/Pattern/ConstructorLike.hs @@ -186,9 +186,6 @@ instance HasConstructorLike key => Synthetic ConstructorLike (Builtin key) where synthetic = \case - BuiltinInt _ -> ConstructorLike . Just $ ConstructorLikeHead - BuiltinBool _ -> ConstructorLike . Just $ ConstructorLikeHead - BuiltinString _ -> ConstructorLike . Just $ ConstructorLikeHead (BuiltinMap InternalAc {builtinAcChild = NormalizedMap builtinMapChild} ) -> normalizedAcConstructorLike builtinMapChild diff --git a/kore/src/Kore/Attribute/Pattern/Defined.hs b/kore/src/Kore/Attribute/Pattern/Defined.hs index 5f18f87cc4..ddc6b063ca 100644 --- a/kore/src/Kore/Attribute/Pattern/Defined.hs +++ b/kore/src/Kore/Attribute/Pattern/Defined.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Attribute.Pattern.Defined ( Defined (..) + , alwaysDefined ) where import Prelude.Kore @@ -25,9 +26,6 @@ import Kore.Internal.Inj ( Inj ) import qualified Kore.Internal.Inj as Inj -import Kore.Internal.InternalBytes - ( InternalBytes - ) import qualified Kore.Internal.Symbol as Internal import Kore.Syntax @@ -41,6 +39,9 @@ newtype Defined = Defined { isDefined :: Bool } deriving anyclass (Debug, Diff) deriving (Semigroup, Monoid) via All +alwaysDefined :: a -> Defined +alwaysDefined = const (Defined True) + instance Synthetic Defined (And sort) where synthetic = const (Defined False) {-# INLINE synthetic #-} @@ -166,31 +167,26 @@ normalizedAcDefined ac@(NormalizedAc _ _ _) = where sameAsChildren = fold ac - -- | A 'Top' pattern is always 'Defined'. instance Synthetic Defined (Top sort) where - synthetic = const (Defined True) + synthetic = alwaysDefined {-# INLINE synthetic #-} -- | A 'StringLiteral' pattern is always 'Defined'. instance Synthetic Defined (Const StringLiteral) where - synthetic = const (Defined True) - {-# INLINE synthetic #-} - --- | A 'Bytes' pattern is always 'Defined'. -instance Synthetic Defined (Const InternalBytes) where - synthetic = const (Defined True) + synthetic = alwaysDefined {-# INLINE synthetic #-} -- | An 'Inhabitant' pattern is always 'Defined'. instance Synthetic Defined Inhabitant where - synthetic = const (Defined True) + synthetic = alwaysDefined {-# INLINE synthetic #-} -- | An element variable pattern is always 'Defined'. -- A set variable is not. instance Synthetic Defined (Const (SomeVariable variable)) where - synthetic (Const unifiedVariable)= Defined (isElementVariable unifiedVariable) + synthetic (Const unifiedVariable) = + Defined (isElementVariable unifiedVariable) {-# INLINE synthetic #-} instance Synthetic Defined Inj where diff --git a/kore/src/Kore/Attribute/Pattern/Function.hs b/kore/src/Kore/Attribute/Pattern/Function.hs index a237a2f513..ce0ec398c6 100644 --- a/kore/src/Kore/Attribute/Pattern/Function.hs +++ b/kore/src/Kore/Attribute/Pattern/Function.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Attribute.Pattern.Function ( Function (..) + , alwaysFunction ) where import Prelude.Kore @@ -24,9 +25,6 @@ import Kore.Internal.Inj ( Inj ) import qualified Kore.Internal.Inj as Inj -import Kore.Internal.InternalBytes - ( InternalBytes - ) import qualified Kore.Internal.Symbol as Internal import Kore.Syntax @@ -40,6 +38,10 @@ newtype Function = Function { isFunction :: Bool } deriving anyclass (Debug, Diff) deriving (Semigroup, Monoid) via All +alwaysFunction :: a -> Function +alwaysFunction = const (Function True) +{-# INLINE alwaysFunction #-} + instance Synthetic Function (And sort) where -- TODO (thomas.tuegel): -- synthetic = getAny . Foldable.foldMap (Any . isFunction) @@ -139,11 +141,6 @@ instance Synthetic Function (Const StringLiteral) where synthetic = const (Function True) {-# INLINE synthetic #-} --- | A 'Bytes' pattern is always 'Function'. -instance Synthetic Function (Const InternalBytes) where - synthetic = const (Function True) - {-# INLINE synthetic #-} - -- | An 'Inhabitant' pattern is never 'Function'. instance Synthetic Function Inhabitant where synthetic = const (Function False) diff --git a/kore/src/Kore/Attribute/Pattern/Functional.hs b/kore/src/Kore/Attribute/Pattern/Functional.hs index 3192648ed6..a0bd704894 100644 --- a/kore/src/Kore/Attribute/Pattern/Functional.hs +++ b/kore/src/Kore/Attribute/Pattern/Functional.hs @@ -6,6 +6,7 @@ License : NCSA module Kore.Attribute.Pattern.Functional ( Functional (..) + , alwaysFunctional ) where import Prelude.Kore @@ -25,9 +26,6 @@ import Kore.Internal.Inj ( Inj ) import qualified Kore.Internal.Inj as Inj -import Kore.Internal.InternalBytes - ( InternalBytes - ) import qualified Kore.Internal.Symbol as Internal import Kore.Syntax @@ -36,18 +34,13 @@ import Kore.Syntax newtype Functional = Functional { isFunctional :: Bool } deriving (Eq, GHC.Generic, Ord, Show) deriving (Semigroup, Monoid) via All + deriving anyclass (Hashable, NFData) + deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) + deriving anyclass (Debug, Diff) -instance SOP.Generic Functional - -instance SOP.HasDatatypeInfo Functional - -instance Debug Functional - -instance Diff Functional - -instance NFData Functional - -instance Hashable Functional +alwaysFunctional :: a -> Functional +alwaysFunctional = const (Functional True) +{-# INLINE alwaysFunctional #-} instance Synthetic Functional (And sort) where synthetic = const (Functional False) @@ -185,11 +178,6 @@ instance Synthetic Functional (Const StringLiteral) where synthetic = const (Functional True) {-# INLINE synthetic #-} --- | A 'Bytes' pattern is always 'Functional'. -instance Synthetic Functional (Const InternalBytes) where - synthetic = const (Functional True) - {-# INLINE synthetic #-} - -- | An 'Inhabitant' pattern is never 'Functional'. instance Synthetic Functional Inhabitant where synthetic = const (Functional False) diff --git a/kore/src/Kore/Attribute/Pattern/Simplified.hs b/kore/src/Kore/Attribute/Pattern/Simplified.hs index f9708b44e0..6eb19e2706 100644 --- a/kore/src/Kore/Attribute/Pattern/Simplified.hs +++ b/kore/src/Kore/Attribute/Pattern/Simplified.hs @@ -13,6 +13,7 @@ module Kore.Attribute.Pattern.Simplified , isFullySimplified , simplifiedTo , fullySimplified + , alwaysSimplified , simplifiedConditionally , simplifiableConditionally , unparseTag @@ -367,9 +368,6 @@ instance Synthetic Simplified (Rewrites sort) where {-# INLINE synthetic #-} instance Synthetic Simplified (Builtin key) where - synthetic (BuiltinInt _) = fullySimplified - synthetic (BuiltinBool _) = fullySimplified - synthetic (BuiltinString _) = fullySimplified synthetic b@(BuiltinMap _) = notSimplified b synthetic b@(BuiltinList _) = notSimplified b synthetic b@(BuiltinSet _) = notSimplified b diff --git a/kore/src/Kore/Builtin/Bool.hs b/kore/src/Kore/Builtin/Bool.hs index 7fbef55d46..7d214c1aca 100644 --- a/kore/src/Kore/Builtin/Bool.hs +++ b/kore/src/Kore/Builtin/Bool.hs @@ -13,7 +13,7 @@ module Kore.Builtin.Bool , asPattern , extractBoolDomainValue , parse - , unifyBoolValues + , unifyBool , unifyBoolAnd , unifyBoolOr , unifyBoolNot @@ -36,6 +36,7 @@ import Control.Error ( MaybeT ) import qualified Control.Monad as Monad +import Data.Functor.Const import qualified Data.HashMap.Strict as HashMap import Data.Map.Strict ( Map @@ -44,7 +45,6 @@ import qualified Data.Map.Strict as Map import Data.Text ( Text ) -import qualified Data.Text as Text import qualified Text.Megaparsec as Parsec import qualified Text.Megaparsec.Char as Parsec @@ -53,8 +53,8 @@ import Kore.Attribute.Hook ) import Kore.Builtin.Bool.Bool import qualified Kore.Builtin.Builtin as Builtin -import qualified Kore.Domain.Builtin as Domain import qualified Kore.Error +import Kore.Internal.InternalBool import Kore.Internal.Pattern ( Pattern ) @@ -122,11 +122,11 @@ patternVerifierHook = patternVerifierWorker domainValue = case externalChild of StringLiteral_ lit -> do - builtinBoolValue <- Builtin.parseString parse lit - (return . BuiltinF . Domain.BuiltinBool) - Domain.InternalBool - { builtinBoolSort = domainValueSort - , builtinBoolValue + internalBoolValue <- Builtin.parseString parse lit + (return . InternalBoolF . Const) + InternalBool + { internalBoolSort = domainValueSort + , internalBoolValue } _ -> Kore.Error.koreFail "Expected literal string" where @@ -136,15 +136,9 @@ patternVerifierHook = -- | get the value from a (possibly encoded) domain value extractBoolDomainValue :: Text -- ^ error message Context - -> Builtin child - -> Bool -extractBoolDomainValue ctx = - \case - Domain.BuiltinBool Domain.InternalBool { builtinBoolValue } -> - builtinBoolValue - _ -> - Builtin.verifierBug - $ Text.unpack ctx ++ ": Bool builtin should be internal" + -> TermLike variable + -> Maybe Bool +extractBoolDomainValue _ = matchBool {- | Parse an integer string literal. -} @@ -171,20 +165,22 @@ builtinFunctions = ] where unaryOperator = - Builtin.unaryOperator extractBoolDomainValue asPattern + Builtin.unaryOperator' extractBoolDomainValue asPattern binaryOperator = - Builtin.binaryOperator extractBoolDomainValue asPattern + Builtin.binaryOperator' extractBoolDomainValue asPattern xor a b = (a && not b) || (not a && b) implies a b = not a || b -unifyBoolValues +{- | Unification of @BOOL.Bool@ values. + -} +unifyBool :: forall variable unifier . InternalVariable variable => MonadUnify unifier => TermLike variable -> TermLike variable -> MaybeT unifier (Pattern variable) -unifyBoolValues a b = +unifyBool a b = worker a b <|> worker b a where worker termLike1 termLike2 @@ -285,8 +281,8 @@ unifyBoolNot unifyChildren a b = {- | Match a @BOOL.Bool@ builtin value. -} matchBool :: TermLike variable -> Maybe Bool -matchBool (BuiltinBool_ Domain.InternalBool { builtinBoolValue }) = - Just builtinBoolValue +matchBool (InternalBool_ InternalBool { internalBoolValue }) = + Just internalBoolValue matchBool _ = Nothing {- | The @BOOL.and@ hooked symbol applied to @term@-type arguments. diff --git a/kore/src/Kore/Builtin/Bool/Bool.hs b/kore/src/Kore/Builtin/Bool/Bool.hs index 6876d039d2..c3cb9b666e 100644 --- a/kore/src/Kore/Builtin/Bool/Bool.hs +++ b/kore/src/Kore/Builtin/Bool/Bool.hs @@ -30,7 +30,7 @@ import Data.Text ( Text ) -import qualified Kore.Domain.Builtin as Domain +import Kore.Internal.InternalBool import Kore.Internal.Pattern ( Pattern ) @@ -38,13 +38,12 @@ import qualified Kore.Internal.Pattern as Pattern ( fromTermLike ) import Kore.Internal.TermLike - ( Concrete - , DomainValue (DomainValue) + ( DomainValue (DomainValue) , InternalVariable , Sort , TermLike - , mkBuiltin , mkDomainValue + , mkInternalBool , mkStringLiteral ) import qualified Kore.Internal.TermLike as TermLike @@ -71,18 +70,14 @@ asInternal -> Bool -- ^ builtin value to render -> TermLike variable asInternal builtinBoolSort builtinBoolValue = - TermLike.markSimplified . mkBuiltin + TermLike.markSimplified . mkInternalBool $ asBuiltin builtinBoolSort builtinBoolValue asBuiltin :: Sort -- ^ resulting sort -> Bool -- ^ builtin value to render - -> Domain.Builtin (TermLike Concrete) (TermLike variable) -asBuiltin builtinBoolSort builtinBoolValue = - Domain.BuiltinBool Domain.InternalBool - { builtinBoolSort - , builtinBoolValue - } + -> InternalBool +asBuiltin = InternalBool {- | Render a 'Bool' as a domain value pattern of the given sort. @@ -94,16 +89,16 @@ asBuiltin builtinBoolSort builtinBoolValue = -} asTermLike :: InternalVariable variable - => Domain.InternalBool -- ^ builtin value to render + => InternalBool -- ^ builtin value to render -> TermLike variable asTermLike builtin = mkDomainValue DomainValue - { domainValueSort = builtinBoolSort + { domainValueSort = internalBoolSort , domainValueChild = mkStringLiteral literal } where - Domain.InternalBool { builtinBoolSort } = builtin - Domain.InternalBool { builtinBoolValue = bool } = builtin + InternalBool { internalBoolSort } = builtin + InternalBool { internalBoolValue = bool } = builtin literal | bool = "true" | otherwise = "false" diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs index 7688b9b27a..938ab7e4a7 100644 --- a/kore/src/Kore/Builtin/Builtin.hs +++ b/kore/src/Kore/Builtin/Builtin.hs @@ -19,8 +19,11 @@ module Kore.Builtin.Builtin -- * Implementing builtin functions , notImplemented , unaryOperator + , unaryOperator' , binaryOperator + , binaryOperator' , ternaryOperator + , ternaryOperator' , functionEvaluator , applicationEvaluator , verifierBug @@ -175,6 +178,7 @@ unaryOperator extractVal asPattern ctx op = where get :: Builtin (TermLike variable) -> a get = extractVal ctx + unaryOperator0 :: Function unaryOperator0 resultSort children = case Cofree.tailF . Recursive.project <$> children of @@ -185,6 +189,84 @@ unaryOperator extractVal asPattern ctx op = [_] -> empty _ -> wrongArity (Text.unpack ctx) +{- | Construct a builtin unary operator. + + The operand type may differ from the result type. + + The function is skipped if its arguments are not domain values. + It is an error if the wrong number of arguments is given; this must be checked + during verification. + + -} +unaryOperator' + :: forall a b + . (forall variable. Text -> TermLike variable -> Maybe a) + -- ^ Parse operand + -> (forall variable + . InternalVariable variable => Sort -> b -> Pattern variable + ) + -- ^ Render result as pattern with given sort + -> Text + -- ^ Builtin function name (for error messages) + -> (a -> b) + -- ^ Operation on builtin types + -> BuiltinAndAxiomSimplifier +unaryOperator' extractVal asPattern ctx op = + functionEvaluator unaryOperator0 + where + get :: TermLike variable -> Maybe a + get = extractVal ctx + + unaryOperator0 :: Function + unaryOperator0 resultSort children = + case children of + [termLike] + | Just a <- get termLike -> do + -- Apply the operator to a domain value + let r = op a + return (asPattern resultSort r) + | otherwise -> empty + _ -> wrongArity (Text.unpack ctx) + +{- | Construct a builtin binary operator. + + Both operands have the same builtin type, which may be different from the + result type. + + The function is skipped if its arguments are not domain values. + It is an error if the wrong number of arguments is given; this must be checked + during verification. + + -} +binaryOperator' + :: forall a b + . (forall variable. Text -> TermLike variable -> Maybe a) + -- ^ Extract domain value + -> (forall variable + . InternalVariable variable => Sort -> b -> Pattern variable + ) + -- ^ Render result as pattern with given sort + -> Text + -- ^ Builtin function name (for error messages) + -> (a -> a -> b) + -- ^ Operation on builtin types + -> BuiltinAndAxiomSimplifier +binaryOperator' extractVal asPattern ctx op = + functionEvaluator binaryOperator0 + where + get :: TermLike variable -> Maybe a + get = extractVal ctx + + binaryOperator0 :: Function + binaryOperator0 resultSort children = + case children of + [get -> Just a, get -> Just b] -> do + -- Apply the operator to two domain values + let r = op a b + return (asPattern resultSort r) + [_, _] -> empty + _ -> wrongArity (Text.unpack ctx) + {- | Construct a builtin binary operator. Both operands have the same builtin type, which may be different from the @@ -223,6 +305,45 @@ binaryOperator extractVal asPattern ctx op = [_, _] -> empty _ -> wrongArity (Text.unpack ctx) +{- | Construct a builtin ternary operator. + + All three operands have the same builtin type, which may be different from the + result type. + + The function is skipped if its arguments are not domain values. + It is an error if the wrong number of arguments is given; this must be checked + during verification. + + -} +ternaryOperator' + :: forall a b + . (forall variable. Text -> TermLike variable -> Maybe a) + -- ^ Extract domain value + -> (forall variable + . InternalVariable variable => Sort -> b -> Pattern variable + ) + -- ^ Render result as pattern with given sort + -> Text + -- ^ Builtin function name (for error messages) + -> (a -> a -> a -> b) + -- ^ Operation on builtin types + -> BuiltinAndAxiomSimplifier +ternaryOperator' extractVal asPattern ctx op = + functionEvaluator ternaryOperator0 + where + get :: TermLike variable -> Maybe a + get = extractVal ctx + + ternaryOperator0 :: Function + ternaryOperator0 resultSort children = + case children of + [get -> Just a, get -> Just b, get -> Just c] -> do + -- Apply the operator to three domain values + let r = op a b c + return (asPattern resultSort r) + [_, _, _] -> empty + _ -> wrongArity (Text.unpack ctx) + {- | Construct a builtin ternary operator. All three operands have the same builtin type, which may be different from the diff --git a/kore/src/Kore/Builtin/External.hs b/kore/src/Kore/Builtin/External.hs index c832e1ab34..f275bd4777 100644 --- a/kore/src/Kore/Builtin/External.hs +++ b/kore/src/Kore/Builtin/External.hs @@ -68,18 +68,16 @@ externalize = Domain.BuiltinSet builtin -> (toPatternF . Recursive.project) (Set.asTermLike builtin) - Domain.BuiltinInt builtin -> - (toPatternF . Recursive.project) - (Int.asTermLike builtin) - Domain.BuiltinBool builtin -> - (toPatternF . Recursive.project) - (Bool.asTermLike builtin) - Domain.BuiltinString builtin -> - (toPatternF . Recursive.project) - (String.asTermLike builtin) + InternalBoolF (Const internalBool) -> + (toPatternF . Recursive.project) (Bool.asTermLike internalBool) + InternalIntF (Const internalInt) -> + (toPatternF . Recursive.project) (Int.asTermLike internalInt) InternalBytesF (Const internalBytes) -> (toPatternF . Recursive.project) (InternalBytes.asTermLike internalBytes) + InternalStringF (Const internalString) -> + (toPatternF . Recursive.project) + (String.asTermLike internalString) InjF inj -> (toPatternF . Recursive.project . synthesize . ApplySymbolF) (Inj.toApplication inj) @@ -144,4 +142,7 @@ externalize = $ getDefined definedF InjF _ -> error "Unexpected sort injection" BuiltinF _ -> error "Unexpected internal builtin" + InternalBoolF _ -> error "Unexpected internal builtin" InternalBytesF _ -> error "Unexpected internal builtin" + InternalIntF _ -> error "Unexpected internal builtin" + InternalStringF _ -> error "Unexpected internal builtin" diff --git a/kore/src/Kore/Builtin/Int.hs b/kore/src/Kore/Builtin/Int.hs index 7103c994b0..01a78ea939 100644 --- a/kore/src/Kore/Builtin/Int.hs +++ b/kore/src/Kore/Builtin/Int.hs @@ -30,6 +30,7 @@ module Kore.Builtin.Int , asPartialPattern , parse , unifyIntEq + , unifyInt -- * keys , randKey , srandKey @@ -65,8 +66,7 @@ module Kore.Builtin.Int , emod , pow , powmod - , log2 - ) where + , log2 ) where import Prelude.Kore @@ -81,6 +81,7 @@ import Data.Bits , (.&.) , (.|.) ) +import Data.Functor.Const import qualified Data.HashMap.Strict as HashMap import Data.Map.Strict ( Map @@ -89,7 +90,6 @@ import qualified Data.Map.Strict as Map import Data.Text ( Text ) -import qualified Data.Text as Text import GHC.Integer ( smallInteger ) @@ -109,9 +109,9 @@ import qualified Kore.Builtin.Bool as Bool import qualified Kore.Builtin.Builtin as Builtin import Kore.Builtin.EqTerm import Kore.Builtin.Int.Int -import qualified Kore.Domain.Builtin as Domain import qualified Kore.Error import qualified Kore.Internal.Condition as Condition +import Kore.Internal.InternalInt import Kore.Internal.Pattern ( Pattern ) @@ -214,29 +214,26 @@ patternVerifierHook = patternVerifierWorker external = case externalChild of StringLiteral_ lit -> do - builtinIntValue <- Builtin.parseString parse lit - (return . BuiltinF . Domain.BuiltinInt) - Domain.InternalInt - { builtinIntSort = domainValueSort - , builtinIntValue + internalIntValue <- Builtin.parseString parse lit + (return . InternalIntF . Const) + InternalInt + { internalIntSort + , internalIntValue } _ -> Kore.Error.koreFail "Expected literal string" where - DomainValue { domainValueSort } = external + DomainValue { domainValueSort = internalIntSort } = external DomainValue { domainValueChild = externalChild } = external -- | get the value from a (possibly encoded) domain value extractIntDomainValue :: Text -- ^ error message Context - -> Builtin child - -> Integer -extractIntDomainValue ctx = + -> TermLike variable + -> Maybe Integer +extractIntDomainValue _ = \case - Domain.BuiltinInt Domain.InternalInt { builtinIntValue } -> - builtinIntValue - _ -> - Builtin.verifierBug - $ Text.unpack ctx ++ ": Int builtin should be internal" + InternalInt_ InternalInt { internalIntValue } -> Just internalIntValue + _ -> Nothing {- | Parse a string literal as an integer. -} @@ -257,16 +254,9 @@ expectBuiltinInt => Text -- ^ Context for error message -> TermLike variable -- ^ Operand pattern -> MaybeT m Integer -expectBuiltinInt ctx = +expectBuiltinInt _ = \case - Builtin_ domain -> - case domain of - Domain.BuiltinInt Domain.InternalInt { builtinIntValue } -> - return builtinIntValue - _ -> - Builtin.verifierBug - $ Text.unpack ctx - ++ ": Domain value is not a string or internal value" + InternalInt_ InternalInt { internalIntValue } -> return internalIntValue _ -> empty {- | Implement builtin function evaluation. @@ -318,22 +308,22 @@ builtinFunctions = ] where unaryOperator name op = - ( name, Builtin.unaryOperator extractIntDomainValue + ( name, Builtin.unaryOperator' extractIntDomainValue asPattern name op ) binaryOperator name op = - ( name, Builtin.binaryOperator extractIntDomainValue + ( name, Builtin.binaryOperator' extractIntDomainValue asPattern name op ) comparator name op = - ( name, Builtin.binaryOperator extractIntDomainValue + ( name, Builtin.binaryOperator' extractIntDomainValue Bool.asPattern name op ) partialUnaryOperator name op = - ( name, Builtin.unaryOperator extractIntDomainValue + ( name, Builtin.unaryOperator' extractIntDomainValue asPartialPattern name op ) partialBinaryOperator name op = - ( name, Builtin.binaryOperator extractIntDomainValue + ( name, Builtin.binaryOperator' extractIntDomainValue asPartialPattern name op ) partialTernaryOperator name op = - ( name, Builtin.ternaryOperator extractIntDomainValue + ( name, Builtin.ternaryOperator' extractIntDomainValue asPartialPattern name op ) tdiv, tmod, ediv, emod, pow @@ -412,6 +402,26 @@ matchIntEqual = Monad.guard (hook2 == eqKey) & isJust +{- | Unification of Int values. + -} +unifyInt + :: forall unifier variable + . InternalVariable variable + => MonadUnify unifier + => HasCallStack + => TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +unifyInt term1@(InternalInt_ int1) term2@(InternalInt_ int2) = + assert (on (==) internalIntSort int1 int2) $ lift worker + where + worker :: unifier (Pattern variable) + worker + | on (==) internalIntValue int1 int2 = + return $ Pattern.fromTermLike term1 + | otherwise = explainAndReturnBottom "distinct integers" term1 term2 +unifyInt _ _ = empty + {- | Unification of the @INT.eq@ symbol. This function is suitable only for equality simplification. diff --git a/kore/src/Kore/Builtin/Int/Int.hs b/kore/src/Kore/Builtin/Int/Int.hs index d3d22edb31..3c8032f42d 100644 --- a/kore/src/Kore/Builtin/Int/Int.hs +++ b/kore/src/Kore/Builtin/Int/Int.hs @@ -51,7 +51,7 @@ import Data.Text ) import qualified Data.Text as Text -import qualified Kore.Domain.Builtin as Domain +import Kore.Internal.InternalInt import Kore.Internal.Pattern as Pattern import Kore.Internal.TermLike as TermLike @@ -74,18 +74,15 @@ asInternal -> Integer -- ^ builtin value to render -> TermLike variable asInternal builtinIntSort builtinIntValue = - TermLike.fromConcrete . TermLike.markSimplified . mkBuiltin + TermLike.fromConcrete . TermLike.markSimplified . mkInternalInt $ asBuiltin builtinIntSort builtinIntValue asBuiltin :: Sort -- ^ resulting sort -> Integer -- ^ builtin value to render - -> Domain.Builtin (TermLike Concrete) (TermLike variable) -asBuiltin builtinIntSort builtinIntValue = - Domain.BuiltinInt Domain.InternalInt - { builtinIntSort - , builtinIntValue - } + -> InternalInt +asBuiltin internalIntSort internalIntValue = + InternalInt { internalIntSort, internalIntValue } {- | Render an 'Integer' as a domain value pattern of the given sort. @@ -97,16 +94,15 @@ asBuiltin builtinIntSort builtinIntValue = -} asTermLike :: InternalVariable variable - => Domain.InternalInt -- ^ builtin value to render + => InternalInt -- ^ builtin value to render -> TermLike variable asTermLike builtin = mkDomainValue DomainValue - { domainValueSort = builtinIntSort - , domainValueChild = mkStringLiteral . Text.pack $ show int + { domainValueSort = internalIntSort + , domainValueChild = mkStringLiteral . Text.pack $ show internalIntValue } where - Domain.InternalInt { builtinIntSort } = builtin - Domain.InternalInt { builtinIntValue = int } = builtin + InternalInt { internalIntSort, internalIntValue } = builtin asPattern :: InternalVariable variable diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs index 975f526d0f..c8a30039da 100644 --- a/kore/src/Kore/Builtin/KEqual.hs +++ b/kore/src/Kore/Builtin/KEqual.hs @@ -32,7 +32,6 @@ import Control.Error , hoistMaybe ) import qualified Control.Monad as Monad -import qualified Data.Functor.Foldable as Recursive import qualified Data.HashMap.Strict as HashMap import Data.Map.Strict ( Map @@ -182,14 +181,8 @@ evalKIte (_ :< app) = evalIte expr t1 t2 _ -> Builtin.wrongArity iteKey where - evaluate - :: TermLike variable - -> Maybe Bool - evaluate (Recursive.project -> _ :< pat) = - case pat of - BuiltinF dv -> - Just (Bool.extractBoolDomainValue iteKey dv) - _ -> Nothing + evaluate :: TermLike variable -> Maybe Bool + evaluate = Bool.matchBool evalIte expr t1 t2 = case evaluate expr of diff --git a/kore/src/Kore/Builtin/String.hs b/kore/src/Kore/Builtin/String.hs index c71998c773..46c454d403 100644 --- a/kore/src/Kore/Builtin/String.hs +++ b/kore/src/Kore/Builtin/String.hs @@ -26,6 +26,7 @@ module Kore.Builtin.String , asTermLike , asPartialPattern , parse + , unifyString , unifyStringEq -- * keys , ltKey @@ -52,6 +53,7 @@ import Data.Char ( chr , ord ) +import Data.Functor.Const import qualified Data.HashMap.Strict as HashMap import Data.List ( findIndex @@ -78,8 +80,8 @@ import qualified Kore.Builtin.Builtin as Builtin import Kore.Builtin.EqTerm import qualified Kore.Builtin.Int as Int import Kore.Builtin.String.String -import qualified Kore.Domain.Builtin as Domain import qualified Kore.Error +import Kore.Internal.InternalString import Kore.Internal.Pattern ( Pattern ) @@ -189,8 +191,8 @@ patternVerifierHook = patternVerifierWorker domainValue = case externalChild of StringLiteral_ internalStringValue -> - (return . BuiltinF . Domain.BuiltinString) - Domain.InternalString + (return . InternalStringF . Const) + InternalString { internalStringSort , internalStringValue } @@ -201,18 +203,16 @@ patternVerifierHook = -- | get the value from a (possibly encoded) domain value extractStringDomainValue - :: Text -- ^ error message Context - -> Builtin (TermLike variable) - -> Text -extractStringDomainValue ctx = + :: Text -- ^ error message context + -> TermLike variable + -> Maybe Text +extractStringDomainValue _ = \case - Domain.BuiltinString internal -> - internalStringValue + InternalString_ internal -> + Just internalStringValue where - Domain.InternalString { internalStringValue } = internal - _ -> - Builtin.verifierBug - $ Text.unpack ctx ++ ": Domain value is not a string" + InternalString { internalStringValue } = internal + _ -> Nothing {- | Parse a string literal. -} @@ -231,17 +231,12 @@ expectBuiltinString => String -- ^ Context for error message -> TermLike variable -- ^ Operand pattern -> MaybeT m Text -expectBuiltinString ctx = +expectBuiltinString _ = \case - Builtin_ domain -> - case domain of - Domain.BuiltinString internal -> - return internalStringValue - where - Domain.InternalString { internalStringValue } = internal - _ -> - Builtin.verifierBug - $ ctx ++ ": Domain value is not a string" + InternalString_ internal -> + return internalStringValue + where + InternalString { internalStringValue } = internal _ -> empty @@ -398,10 +393,10 @@ builtinFunctions = ] where comparator name op = - ( name, Builtin.binaryOperator extractStringDomainValue + ( name, Builtin.binaryOperator' extractStringDomainValue Bool.asPattern name op ) binaryOperator name op = - ( name, Builtin.binaryOperator extractStringDomainValue + ( name, Builtin.binaryOperator' extractStringDomainValue asPattern name op ) {- | Match the @STRING.eq@ hooked symbol. @@ -414,6 +409,26 @@ matchStringEqual = Monad.guard (hook2 == eqKey) & isJust +{- | Unification of String values. + -} +unifyString + :: forall unifier variable + . InternalVariable variable + => MonadUnify unifier + => HasCallStack + => TermLike variable + -> TermLike variable + -> MaybeT unifier (Pattern variable) +unifyString term1@(InternalString_ int1) term2@(InternalString_ int2) = + assert (on (==) internalStringSort int1 int2) $ lift worker + where + worker :: unifier (Pattern variable) + worker + | on (==) internalStringValue int1 int2 = + return $ Pattern.fromTermLike term1 + | otherwise = explainAndReturnBottom "distinct strings" term1 term2 +unifyString _ _ = empty + {- | Unification of the @STRING.eq@ symbol This function is suitable only for equality simplification. diff --git a/kore/src/Kore/Builtin/String/String.hs b/kore/src/Kore/Builtin/String/String.hs index bb2cc1f049..08f3b798e3 100644 --- a/kore/src/Kore/Builtin/String/String.hs +++ b/kore/src/Kore/Builtin/String/String.hs @@ -36,7 +36,7 @@ import Data.Text ( Text ) -import qualified Kore.Domain.Builtin as Domain +import Kore.Internal.InternalString import Kore.Internal.Pattern ( Pattern ) @@ -62,18 +62,14 @@ asInternal -> Text -- ^ builtin value to render -> TermLike variable asInternal internalStringSort internalStringValue = - TermLike.fromConcrete . mkBuiltin + TermLike.fromConcrete . mkInternalString $ asBuiltin internalStringSort internalStringValue asBuiltin :: Sort -- ^ resulting sort -> Text -- ^ builtin value to render - -> Domain.Builtin (TermLike Concrete) (TermLike variable) -asBuiltin internalStringSort internalStringValue = - Domain.BuiltinString Domain.InternalString - { internalStringSort - , internalStringValue - } + -> InternalString +asBuiltin = InternalString {- | Render an 'String' as a domain value pattern of the given sort. @@ -85,7 +81,7 @@ asBuiltin internalStringSort internalStringValue = -} asTermLike :: InternalVariable variable - => Domain.InternalString -- ^ builtin value to render + => InternalString -- ^ builtin value to render -> TermLike variable asTermLike internal = mkDomainValue DomainValue @@ -93,8 +89,8 @@ asTermLike internal = , domainValueChild = mkStringLiteral internalStringValue } where - Domain.InternalString { internalStringSort } = internal - Domain.InternalString { internalStringValue } = internal + InternalString { internalStringSort } = internal + InternalString { internalStringValue } = internal asPattern :: InternalVariable variable diff --git a/kore/src/Kore/Domain/Builtin.hs b/kore/src/Kore/Domain/Builtin.hs index 9539989e0f..ec3498d3ef 100644 --- a/kore/src/Kore/Domain/Builtin.hs +++ b/kore/src/Kore/Domain/Builtin.hs @@ -40,10 +40,6 @@ module Kore.Domain.Builtin , SetElement , SetValue , NormalizedSet (..) - -- - , InternalInt (..) - , InternalBool (..) - , InternalString (..) ) where import Prelude.Kore @@ -66,9 +62,6 @@ import qualified Data.Map.Strict as Map import Data.Sequence ( Seq ) -import Data.Text - ( Text - ) import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC @@ -637,101 +630,12 @@ instance AcWrapper NormalizedSet where -} type InternalSet key child = InternalAc key NormalizedSet child --- * Builtin Int - -{- | Internal representation of the builtin @INT.Int@ domain. - -} -data InternalInt = - InternalInt - { builtinIntSort :: !Sort - , builtinIntValue :: !Integer - } - deriving (Eq, Ord, Show) - deriving (GHC.Generic) - deriving anyclass (Hashable, NFData) - deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) - deriving anyclass (Debug, Diff) - -instance Unparse InternalInt where - unparse InternalInt { builtinIntSort, builtinIntValue } = - "\\dv" - <> parameters [builtinIntSort] - <> Pretty.parens (Pretty.dquotes $ Pretty.pretty builtinIntValue) - - unparse2 InternalInt { builtinIntSort, builtinIntValue } = - "\\dv2" - <> parameters2 [builtinIntSort] - <> arguments' [Pretty.dquotes $ Pretty.pretty builtinIntValue] - --- * Builtin Bool - -{- | Internal representation of the builtin @BOOL.Bool@ domain. - -} -data InternalBool = - InternalBool - { builtinBoolSort :: !Sort - , builtinBoolValue :: !Bool - } - deriving (Eq, Ord, Show) - deriving (GHC.Generic) - deriving anyclass (Hashable, NFData) - deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) - deriving anyclass (Debug, Diff) - -instance Unparse InternalBool where - unparse InternalBool { builtinBoolSort, builtinBoolValue } = - "\\dv" - <> parameters [builtinBoolSort] - <> Pretty.parens (Pretty.dquotes value) - where - value - | builtinBoolValue = "true" - | otherwise = "false" - - unparse2 InternalBool { builtinBoolSort, builtinBoolValue } = - "\\dv2" - <> parameters2 [builtinBoolSort] - <> arguments' [Pretty.dquotes value] - where - value - | builtinBoolValue = "true" - | otherwise = "false" - --- * Builtin String - -{- | Internal representation of the builtin @STRING.String@ domain. - -} -data InternalString = - InternalString - { internalStringSort :: !Sort - , internalStringValue :: !Text - } - deriving (Eq, Ord, Show) - deriving (GHC.Generic) - deriving anyclass (Hashable, NFData) - deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) - deriving anyclass (Debug, Diff) - -instance Unparse InternalString where - unparse InternalString { internalStringSort, internalStringValue } = - "\\dv" - <> parameters [internalStringSort] - <> Pretty.parens (unparse $ StringLiteral internalStringValue) - - unparse2 InternalString { internalStringSort, internalStringValue } = - "\\dv2" - <> parameters2 [internalStringSort] - <> arguments2 [StringLiteral internalStringValue] - -- * Builtin domain representations data Builtin key child = BuiltinMap !(InternalMap key child) | BuiltinList !(InternalList child) | BuiltinSet !(InternalSet key child) - | BuiltinInt !InternalInt - | BuiltinBool !InternalBool - | BuiltinString !InternalString deriving (Eq, Ord, Show) deriving (Foldable, Functor, Traversable) deriving (GHC.Generic) @@ -748,10 +652,6 @@ instance (Unparse key, Unparse child) => Unparse (Builtin key child) where builtinSort :: Builtin key child -> Sort builtinSort builtin = case builtin of - BuiltinInt InternalInt { builtinIntSort } -> builtinIntSort - BuiltinBool InternalBool { builtinBoolSort } -> builtinBoolSort - BuiltinString InternalString { internalStringSort } -> - internalStringSort BuiltinMap InternalAc { builtinAcSort } -> builtinAcSort BuiltinList InternalList { builtinListSort } -> builtinListSort BuiltinSet InternalAc { builtinAcSort } -> builtinAcSort diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index b27770d6f4..5f206e95d4 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -63,7 +63,6 @@ import Kore.Attribute.Symbol ( StepperAttributes ) import qualified Kore.Builtin as Builtin -import qualified Kore.Domain.Builtin as Domain import Kore.Equation ( Equation ) @@ -81,6 +80,7 @@ import Kore.IndexedModule.Resolvers ( resolveInternalSymbol ) import qualified Kore.Internal.Condition as Condition +import Kore.Internal.InternalInt import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern @@ -312,7 +312,7 @@ getExitCode indexedModule configs = return exitCode where extractExit = \case - Builtin_ (Domain.BuiltinInt (Domain.InternalInt _ exit)) + InternalInt_ InternalInt { internalIntValue = exit } | exit == 0 -> ExitSuccess | otherwise -> ExitFailure (fromInteger exit) _ -> ExitFailure 111 diff --git a/kore/src/Kore/Internal/InternalBool.hs b/kore/src/Kore/Internal/InternalBool.hs new file mode 100644 index 0000000000..e85a87d444 --- /dev/null +++ b/kore/src/Kore/Internal/InternalBool.hs @@ -0,0 +1,88 @@ +{- | +Copyright : (c) Runtime Verification, 2019 +License : NCSA + -} +module Kore.Internal.InternalBool + ( InternalBool (..) + ) where + +import Prelude.Kore + +import Control.DeepSeq + ( NFData + ) +import Data.Functor.Const +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC + +import Kore.Attribute.Pattern.ConstructorLike +import Kore.Attribute.Pattern.Defined +import Kore.Attribute.Pattern.FreeVariables +import Kore.Attribute.Pattern.Function +import Kore.Attribute.Pattern.Functional +import Kore.Attribute.Pattern.Simplified +import Kore.Attribute.Synthetic +import Kore.Debug +import Kore.Sort +import Kore.Unparser +import qualified Pretty + +{- | Internal representation of the builtin @BOOL.Bool@ domain. + -} +data InternalBool = + InternalBool + { internalBoolSort :: !Sort + , internalBoolValue :: !Bool + } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + deriving anyclass (Hashable, NFData) + deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) + deriving anyclass (Debug, Diff) + +instance Unparse InternalBool where + unparse InternalBool { internalBoolSort, internalBoolValue } = + "\\dv" + <> parameters [internalBoolSort] + <> Pretty.parens (Pretty.dquotes value) + where + value + | internalBoolValue = "true" + | otherwise = "false" + + unparse2 InternalBool { internalBoolSort, internalBoolValue } = + "\\dv2" + <> parameters2 [internalBoolSort] + <> arguments' [Pretty.dquotes value] + where + value + | internalBoolValue = "true" + | otherwise = "false" + +instance Synthetic Sort (Const InternalBool) where + synthetic (Const InternalBool { internalBoolSort }) = internalBoolSort + {-# INLINE synthetic #-} + +instance Synthetic (FreeVariables variable) (Const InternalBool) where + synthetic _ = emptyFreeVariables + {-# INLINE synthetic #-} + +instance Synthetic ConstructorLike (Const InternalBool) where + synthetic _ = ConstructorLike . Just $ ConstructorLikeHead + {-# INLINE synthetic #-} + +instance Synthetic Defined (Const InternalBool) where + synthetic = alwaysDefined + {-# INLINE synthetic #-} + +instance Synthetic Function (Const InternalBool) where + synthetic = alwaysFunction + {-# INLINE synthetic #-} + +instance Synthetic Functional (Const InternalBool) where + synthetic = alwaysFunctional + {-# INLINE synthetic #-} + +instance Synthetic Simplified (Const InternalBool) where + synthetic = alwaysSimplified + {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Internal/InternalBytes.hs b/kore/src/Kore/Internal/InternalBytes.hs index 0e4ed8579d..837ccb199c 100644 --- a/kore/src/Kore/Internal/InternalBytes.hs +++ b/kore/src/Kore/Internal/InternalBytes.hs @@ -18,7 +18,10 @@ import Data.ByteString import qualified Generics.SOP as SOP import qualified GHC.Generics as GHC +import Kore.Attribute.Pattern.Defined import Kore.Attribute.Pattern.FreeVariables +import Kore.Attribute.Pattern.Function +import Kore.Attribute.Pattern.Functional import Kore.Attribute.Synthetic import qualified Kore.Builtin.Encoding as Encoding import Kore.Debug @@ -58,3 +61,15 @@ instance Synthetic Sort (Const InternalBytes) where instance Synthetic (FreeVariables variable) (Const InternalBytes) where synthetic = const emptyFreeVariables {-# INLINE synthetic #-} + +instance Synthetic Defined (Const InternalBytes) where + synthetic = alwaysDefined + {-# INLINE synthetic #-} + +instance Synthetic Function (Const InternalBytes) where + synthetic = alwaysFunction + {-# INLINE synthetic #-} + +instance Synthetic Functional (Const InternalBytes) where + synthetic = alwaysFunctional + {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Internal/InternalInt.hs b/kore/src/Kore/Internal/InternalInt.hs new file mode 100644 index 0000000000..900b313340 --- /dev/null +++ b/kore/src/Kore/Internal/InternalInt.hs @@ -0,0 +1,75 @@ +{- | +Copyright : (c) Runtime Verification, 2020 +License : NCSA +-} +module Kore.Internal.InternalInt + ( InternalInt (..) + ) where + +import Prelude.Kore + +import Control.DeepSeq + ( NFData + ) +import Data.Functor.Const +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC + +import Kore.Attribute.Pattern.ConstructorLike +import Kore.Attribute.Pattern.Defined +import Kore.Attribute.Pattern.FreeVariables +import Kore.Attribute.Pattern.Function +import Kore.Attribute.Pattern.Functional +import Kore.Attribute.Pattern.Simplified +import Kore.Attribute.Synthetic +import Kore.Debug +import Kore.Sort +import Kore.Unparser +import qualified Pretty + +{- | Internal representation of the builtin @INT.Int@ domain. + -} +data InternalInt = + InternalInt { internalIntSort :: !Sort, internalIntValue :: !Integer } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + deriving anyclass (Hashable, NFData) + deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) + deriving anyclass (Debug, Diff) + +instance Unparse InternalInt where + unparse InternalInt { internalIntSort, internalIntValue } = + "\\dv" + <> parameters [internalIntSort] + <> Pretty.parens (Pretty.dquotes $ Pretty.pretty internalIntValue) + + unparse2 InternalInt { internalIntSort, internalIntValue } = + "\\dv2" + <> parameters2 [internalIntSort] + <> arguments' [Pretty.dquotes $ Pretty.pretty internalIntValue] + +instance Synthetic Sort (Const InternalInt) where + synthetic (Const InternalInt { internalIntSort }) = internalIntSort + +instance Synthetic (FreeVariables variable) (Const InternalInt) where + synthetic _ = emptyFreeVariables + +instance Synthetic ConstructorLike (Const InternalInt) where + synthetic = const (ConstructorLike . Just $ ConstructorLikeHead) + {-# INLINE synthetic #-} + +instance Synthetic Defined (Const InternalInt) where + synthetic = alwaysDefined + {-# INLINE synthetic #-} + +instance Synthetic Function (Const InternalInt) where + synthetic = alwaysFunction + {-# INLINE synthetic #-} + +instance Synthetic Functional (Const InternalInt) where + synthetic = alwaysFunctional + {-# INLINE synthetic #-} + +instance Synthetic Simplified (Const InternalInt) where + synthetic = alwaysSimplified + {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Internal/InternalString.hs b/kore/src/Kore/Internal/InternalString.hs new file mode 100644 index 0000000000..d02c03258a --- /dev/null +++ b/kore/src/Kore/Internal/InternalString.hs @@ -0,0 +1,85 @@ +{- | +Copyright : (c) Runtime Verification, 2019 +License : NCSA + -} +module Kore.Internal.InternalString + ( InternalString (..) + ) where + +import Prelude.Kore + +import Control.DeepSeq + ( NFData + ) +import Data.Functor.Const +import Data.Text + ( Text + ) +import qualified Generics.SOP as SOP +import qualified GHC.Generics as GHC + +import Kore.Attribute.Pattern.ConstructorLike +import Kore.Attribute.Pattern.Defined +import Kore.Attribute.Pattern.FreeVariables +import Kore.Attribute.Pattern.Function +import Kore.Attribute.Pattern.Functional +import Kore.Attribute.Pattern.Simplified +import Kore.Attribute.Synthetic +import Kore.Debug +import Kore.Sort +import Kore.Syntax.StringLiteral +import Kore.Unparser +import qualified Pretty + + +{- | Internal representation of the builtin @STRING.String@ domain. + -} +data InternalString = + InternalString + { internalStringSort :: !Sort + , internalStringValue :: !Text + } + deriving (Eq, Ord, Show) + deriving (GHC.Generic) + deriving anyclass (Hashable, NFData) + deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) + deriving anyclass (Debug, Diff) + +instance Unparse InternalString where + unparse InternalString { internalStringSort, internalStringValue } = + "\\dv" + <> parameters [internalStringSort] + <> Pretty.parens (unparse $ StringLiteral internalStringValue) + + unparse2 InternalString { internalStringSort, internalStringValue } = + "\\dv2" + <> parameters2 [internalStringSort] + <> arguments2 [StringLiteral internalStringValue] + +instance Synthetic Sort (Const InternalString) where + synthetic (Const InternalString { internalStringSort }) = internalStringSort + {-# INLINE synthetic #-} + +instance Synthetic (FreeVariables variable) (Const InternalString) where + synthetic _ = emptyFreeVariables + {-# INLINE synthetic #-} + +instance Synthetic ConstructorLike (Const InternalString) where + synthetic _ = ConstructorLike . Just $ ConstructorLikeHead + {-# INLINE synthetic #-} + +instance Synthetic Defined (Const InternalString) where + synthetic = alwaysDefined + {-# INLINE synthetic #-} + +instance Synthetic Function (Const InternalString) where + synthetic = alwaysFunction + {-# INLINE synthetic #-} + +instance Synthetic Functional (Const InternalString) where + synthetic = alwaysFunctional + {-# INLINE synthetic #-} + +instance Synthetic Simplified (Const InternalString) where + synthetic = alwaysSimplified + {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 845585b6cf..a08cb02624 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -58,6 +58,9 @@ module Kore.Internal.TermLike , mkInternalBytes , mkInternalBytes' , mkBuiltin + , mkInternalBool + , mkInternalInt + , mkInternalString , mkBuiltinList , mkBuiltinMap , mkBuiltinSet @@ -118,12 +121,12 @@ module Kore.Internal.TermLike , pattern Bottom_ , pattern InternalBytes_ , pattern Builtin_ - , pattern BuiltinBool_ - , pattern BuiltinInt_ + , pattern InternalBool_ + , pattern InternalInt_ , pattern BuiltinList_ , pattern BuiltinMap_ , pattern BuiltinSet_ - , pattern BuiltinString_ + , pattern InternalString_ , pattern Ceil_ , pattern DV_ , pattern Equals_ @@ -238,7 +241,10 @@ import qualified Kore.Domain.Builtin as Domain import Kore.Error import Kore.Internal.Alias import Kore.Internal.Inj +import Kore.Internal.InternalBool import Kore.Internal.InternalBytes +import Kore.Internal.InternalInt +import Kore.Internal.InternalString import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( Representation ) @@ -349,12 +355,12 @@ hasConstructorLikeTop :: TermLike variable -> Bool hasConstructorLikeTop = \case App_ symbol _ -> isConstructor symbol DV_ _ _ -> True - BuiltinBool_ _ -> True - BuiltinInt_ _ -> True + InternalBool_ _ -> True + InternalInt_ _ -> True BuiltinList_ _ -> True BuiltinMap_ _ -> True BuiltinSet_ _ -> True - BuiltinString_ _ -> True + InternalString_ _ -> True StringLiteral_ _ -> True _ -> False @@ -708,10 +714,13 @@ forceSortPredicate ApplySymbolF _ -> illSorted forcedSort original ApplyAliasF _ -> illSorted forcedSort original BuiltinF _ -> illSorted forcedSort original + InternalBoolF _ -> illSorted forcedSort original + InternalBytesF _ -> illSorted forcedSort original + InternalIntF _ -> illSorted forcedSort original + InternalStringF _ -> illSorted forcedSort original DomainValueF _ -> illSorted forcedSort original StringLiteralF _ -> illSorted forcedSort original VariableF _ -> illSorted forcedSort original - InternalBytesF _ -> illSorted forcedSort original InhabitantF _ -> illSorted forcedSort original EndiannessF _ -> illSorted forcedSort original SignednessF _ -> illSorted forcedSort original @@ -1052,6 +1061,33 @@ mkBuiltin -> TermLike variable mkBuiltin = updateCallStack . synthesize . BuiltinF +{- | Construct an internal bool pattern. + -} +mkInternalBool + :: HasCallStack + => InternalVariable variable + => InternalBool + -> TermLike variable +mkInternalBool = updateCallStack . synthesize . InternalBoolF . Const + +{- | Construct an internal integer pattern. + -} +mkInternalInt + :: HasCallStack + => InternalVariable variable + => InternalInt + -> TermLike variable +mkInternalInt = updateCallStack . synthesize . InternalIntF . Const + +{- | Construct an internal string pattern. + -} +mkInternalString + :: HasCallStack + => InternalVariable variable + => InternalString + -> TermLike variable +mkInternalString = updateCallStack . synthesize . InternalStringF . Const + {- | Construct a builtin list pattern. -} mkBuiltinList @@ -1492,9 +1528,6 @@ mkDefined = worker \ a \\bottom pattern as defined." CeilF _ -> term DomainValueF _ -> term - BuiltinF (Domain.BuiltinBool _) -> term - BuiltinF (Domain.BuiltinInt _) -> term - BuiltinF (Domain.BuiltinString _) -> term BuiltinF (Domain.BuiltinList _) -> -- mkDefinedAtTop is not needed because the list is always -- defined if its elements are all defined. @@ -1530,7 +1563,10 @@ mkDefined = worker SignednessF _ -> term InjF _ -> mkDefined1 term InhabitantF _ -> mkDefined1 term + InternalBoolF _ -> term InternalBytesF _ -> term + InternalIntF _ -> term + InternalStringF _ -> term mkDefinedInternalAc internalAc = Lens.over (field @"builtinAcChild") mkDefinedNormalized internalAc @@ -1720,12 +1756,12 @@ pattern Builtin_ :: Domain.Builtin (TermLike Concrete) (TermLike variable) -> TermLike variable -pattern BuiltinBool_ - :: Domain.InternalBool +pattern InternalBool_ + :: InternalBool -> TermLike variable -pattern BuiltinInt_ - :: Domain.InternalInt +pattern InternalInt_ + :: InternalInt -> TermLike variable pattern BuiltinList_ @@ -1740,9 +1776,7 @@ pattern BuiltinSet_ :: Domain.InternalSet (TermLike Concrete) (TermLike variable) -> TermLike variable -pattern BuiltinString_ - :: Domain.InternalString - -> TermLike variable +pattern InternalString_ :: InternalString -> TermLike variable pattern Equals_ :: Sort @@ -1874,9 +1908,14 @@ pattern DV_ domainValueSort domainValueChild <- pattern Builtin_ builtin <- (Recursive.project -> _ :< BuiltinF builtin) -pattern BuiltinBool_ internalBool <- Builtin_ (Domain.BuiltinBool internalBool) +pattern InternalBool_ internalBool <- + (Recursive.project -> _ :< InternalBoolF (Const internalBool)) -pattern BuiltinInt_ internalInt <- Builtin_ (Domain.BuiltinInt internalInt) +pattern InternalInt_ internalInt <- + (Recursive.project -> _ :< InternalIntF (Const internalInt)) + +pattern InternalString_ internalString <- + (Recursive.project -> _ :< InternalStringF (Const internalString)) pattern BuiltinList_ internalList <- Builtin_ (Domain.BuiltinList internalList) @@ -1884,9 +1923,6 @@ pattern BuiltinMap_ internalMap <- Builtin_ (Domain.BuiltinMap internalMap) pattern BuiltinSet_ internalSet <- Builtin_ (Domain.BuiltinSet internalSet) -pattern BuiltinString_ internalString - <- Builtin_ (Domain.BuiltinString internalString) - pattern Equals_ equalsOperandSort equalsResultSort equalsFirst equalsSecond <- (Recursive.project -> _ :< EqualsF Equals diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs index 4af6fa4e47..2714ae3107 100644 --- a/kore/src/Kore/Internal/TermLike/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike/TermLike.hs @@ -78,7 +78,10 @@ import Kore.Debug import qualified Kore.Domain.Builtin as Domain import Kore.Internal.Alias import Kore.Internal.Inj +import Kore.Internal.InternalBool import Kore.Internal.InternalBytes +import Kore.Internal.InternalInt +import Kore.Internal.InternalString import Kore.Internal.Symbol hiding ( isConstructorLike ) @@ -175,36 +178,39 @@ instance {-# OVERLAPS #-} Synthetic Pattern.Defined Defined where -} data TermLikeF variable child - = AndF !(And Sort child) - | ApplySymbolF !(Application Symbol child) - | ApplyAliasF !(Application (Alias (TermLike VariableName)) child) - | BottomF !(Bottom Sort child) - | CeilF !(Ceil Sort child) - | DomainValueF !(DomainValue Sort child) - | EqualsF !(Equals Sort child) - | ExistsF !(Exists Sort variable child) - | FloorF !(Floor Sort child) - | ForallF !(Forall Sort variable child) - | IffF !(Iff Sort child) - | ImpliesF !(Implies Sort child) - | InF !(In Sort child) - | MuF !(Mu variable child) - | NextF !(Next Sort child) - | NotF !(Not Sort child) - | NuF !(Nu variable child) - | OrF !(Or Sort child) - | RewritesF !(Rewrites Sort child) - | TopF !(Top Sort child) - | InhabitantF !(Inhabitant child) - | BuiltinF !(Builtin child) - | EvaluatedF !(Evaluated child) - | StringLiteralF !(Const StringLiteral child) - | InternalBytesF !(Const InternalBytes child) - | VariableF !(Const (SomeVariable variable) child) - | EndiannessF !(Const Endianness child) - | SignednessF !(Const Signedness child) - | InjF !(Inj child) - | DefinedF !(Defined child) + = AndF !(And Sort child) + | ApplySymbolF !(Application Symbol child) + | ApplyAliasF !(Application (Alias (TermLike VariableName)) child) + | BottomF !(Bottom Sort child) + | CeilF !(Ceil Sort child) + | DomainValueF !(DomainValue Sort child) + | EqualsF !(Equals Sort child) + | ExistsF !(Exists Sort variable child) + | FloorF !(Floor Sort child) + | ForallF !(Forall Sort variable child) + | IffF !(Iff Sort child) + | ImpliesF !(Implies Sort child) + | InF !(In Sort child) + | MuF !(Mu variable child) + | NextF !(Next Sort child) + | NotF !(Not Sort child) + | NuF !(Nu variable child) + | OrF !(Or Sort child) + | RewritesF !(Rewrites Sort child) + | TopF !(Top Sort child) + | InhabitantF !(Inhabitant child) + | BuiltinF !(Builtin child) + | EvaluatedF !(Evaluated child) + | StringLiteralF !(Const StringLiteral child) + | InternalBoolF !(Const InternalBool child) + | InternalBytesF !(Const InternalBytes child) + | InternalIntF !(Const InternalInt child) + | InternalStringF !(Const InternalString child) + | VariableF !(Const (SomeVariable variable) child) + | EndiannessF !(Const Endianness child) + | SignednessF !(Const Signedness child) + | InjF !(Inj child) + | DefinedF !(Defined child) deriving (Eq, Ord, Show) deriving (Foldable, Functor, Traversable) deriving (GHC.Generic) @@ -247,7 +253,10 @@ instance BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -281,7 +290,10 @@ instance Synthetic Sort (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -315,7 +327,10 @@ instance Synthetic Pattern.Functional (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -349,7 +364,10 @@ instance Synthetic Pattern.Function (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -383,7 +401,10 @@ instance Synthetic Pattern.Defined (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -417,7 +438,10 @@ instance Synthetic Pattern.Simplified (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -451,7 +475,10 @@ instance Synthetic Pattern.ConstructorLike (TermLikeF variable) where BuiltinF builtin -> synthetic builtin EvaluatedF evaluated -> synthetic evaluated StringLiteralF stringLiteral -> synthetic stringLiteral + InternalBoolF internalBool -> synthetic internalBool InternalBytesF internalBytes -> synthetic internalBytes + InternalIntF internalInt -> synthetic internalInt + InternalStringF internalString -> synthetic internalString VariableF variable -> synthetic variable EndiannessF endianness -> synthetic endianness SignednessF signedness -> synthetic signedness @@ -689,9 +716,15 @@ instance InjF Inj { injChild } -> locationFromAst injChild SignednessF (Const signedness) -> locationFromAst signedness EndiannessF (Const endianness) -> locationFromAst endianness + BuiltinF builtin -> locationFromAst (Domain.builtinSort builtin) + InternalBoolF (Const InternalBool { internalBoolSort }) -> + locationFromAst internalBoolSort InternalBytesF (Const InternalBytes { bytesSort }) -> locationFromAst bytesSort - BuiltinF builtin -> locationFromAst (Domain.builtinSort builtin) + InternalIntF (Const InternalInt { internalIntSort }) -> + locationFromAst internalIntSort + InternalStringF (Const InternalString { internalStringSort }) -> + locationFromAst internalStringSort DefinedF Defined { getDefined } -> locationFromAst getDefined @@ -736,7 +769,10 @@ traverseVariablesF adj = OrF orP -> pure (OrF orP) RewritesF rewP -> pure (RewritesF rewP) StringLiteralF strP -> pure (StringLiteralF strP) + InternalBoolF boolP -> pure (InternalBoolF boolP) InternalBytesF bytesP -> pure (InternalBytesF bytesP) + InternalIntF intP -> pure (InternalIntF intP) + InternalStringF boolP -> pure (InternalStringF boolP) TopF topP -> pure (TopF topP) InhabitantF s -> pure (InhabitantF s) EvaluatedF childP -> pure (EvaluatedF childP) diff --git a/kore/src/Kore/Step/Axiom/Matcher.hs b/kore/src/Kore/Step/Axiom/Matcher.hs index e39d639214..c4fc7ecf4d 100644 --- a/kore/src/Kore/Step/Axiom/Matcher.hs +++ b/kore/src/Kore/Step/Axiom/Matcher.hs @@ -118,13 +118,15 @@ instance Ord TermLikeClass where findClass :: Constraint variable -> TermLikeClass findClass (Constraint (Pair left _)) = findClassWorker left where + -- TODO (thomas.tuegel): Don't use pattern synonyms here! findClassWorker (Var_ _) = Variables findClassWorker (ElemVar_ _) = Variables findClassWorker (SetVar_ _) = Variables findClassWorker (StringLiteral_ _) = ConcreteBuiltins - findClassWorker (BuiltinInt_ _) = ConcreteBuiltins - findClassWorker (BuiltinBool_ _) = ConcreteBuiltins - findClassWorker (BuiltinString_ _) = ConcreteBuiltins + findClassWorker (InternalBytes_ _ _) = ConcreteBuiltins + findClassWorker (InternalInt_ _) = ConcreteBuiltins + findClassWorker (InternalBool_ _) = ConcreteBuiltins + findClassWorker (InternalString_ _) = ConcreteBuiltins findClassWorker (App_ symbol _) = if Symbol.isConstructor symbol then ConstructorAtTop @@ -226,11 +228,11 @@ matchEqualHeads -- Terminal patterns matchEqualHeads (Pair (StringLiteral_ string1) (StringLiteral_ string2)) = Monad.guard (string1 == string2) -matchEqualHeads (Pair (BuiltinInt_ int1) (BuiltinInt_ int2)) = +matchEqualHeads (Pair (InternalInt_ int1) (InternalInt_ int2)) = Monad.guard (int1 == int2) -matchEqualHeads (Pair (BuiltinBool_ bool1) (BuiltinBool_ bool2)) = +matchEqualHeads (Pair (InternalBool_ bool1) (InternalBool_ bool2)) = Monad.guard (bool1 == bool2) -matchEqualHeads (Pair (BuiltinString_ string1) (BuiltinString_ string2)) = +matchEqualHeads (Pair (InternalString_ string1) (InternalString_ string2)) = Monad.guard (string1 == string2) matchEqualHeads (Pair (Bottom_ _) (Bottom_ _)) = return () diff --git a/kore/src/Kore/Step/SMT/Translate.hs b/kore/src/Kore/Step/SMT/Translate.hs index 432fef223c..bf3d62be3f 100644 --- a/kore/src/Kore/Step/SMT/Translate.hs +++ b/kore/src/Kore/Step/SMT/Translate.hs @@ -50,6 +50,7 @@ import Control.Monad.State.Strict ) import qualified Control.Monad.State.Strict as State import Data.Default +import Data.Functor.Const import qualified Data.Functor.Foldable as Recursive import Data.Generics.Product.Fields import Data.Map.Strict @@ -69,6 +70,8 @@ import qualified Kore.Attribute.Symbol as Attribute import qualified Kore.Builtin.Bool as Builtin.Bool import qualified Kore.Builtin.Int as Builtin.Int import Kore.IndexedModule.MetadataTools +import Kore.Internal.InternalBool +import Kore.Internal.InternalInt import Kore.Internal.Predicate import Kore.Internal.TermLike import Kore.Log.WarnSymbolSMTRepresentation @@ -171,7 +174,10 @@ translatePredicateWith translateTerm predicate = RewritesF _ -> empty VariableF _ -> empty StringLiteralF _ -> empty + InternalBoolF _ -> empty InternalBytesF _ -> empty + InternalIntF _ -> empty + InternalStringF _ -> empty InhabitantF _ -> empty EndiannessF _ -> empty SignednessF _ -> empty @@ -294,9 +300,8 @@ translatePattern translateTerm sort pat = translateInt pat' = case Cofree.tailF (Recursive.project pat') of VariableF _ -> translateUninterpreted translateTerm SMT.tInt pat' - BuiltinF dv -> - return $ SMT.int $ Builtin.Int.extractIntDomainValue - "while translating dv to SMT.int" dv + InternalIntF (Const InternalInt { internalIntValue }) -> + return $ SMT.int internalIntValue ApplySymbolF app -> translateApplication (Just SMT.tInt) pat' app DefinedF (Defined child) -> @@ -309,9 +314,8 @@ translatePattern translateTerm sort pat = translateBool pat' = case Cofree.tailF (Recursive.project pat') of VariableF _ -> translateUninterpreted translateTerm SMT.tBool pat' - BuiltinF dv -> - return $ SMT.bool $ Builtin.Bool.extractBoolDomainValue - "while translating dv to SMT.bool" dv + InternalBoolF (Const InternalBool { internalBoolValue }) -> + return $ SMT.bool internalBoolValue NotF Not { notChild } -> -- \not is equivalent to BOOL.not for functional patterns. -- The following is safe because non-functional patterns diff --git a/kore/src/Kore/Step/Simplification/AndTerms.hs b/kore/src/Kore/Step/Simplification/AndTerms.hs index b8c15d6a42..20c91a5b68 100644 --- a/kore/src/Kore/Step/Simplification/AndTerms.hs +++ b/kore/src/Kore/Step/Simplification/AndTerms.hs @@ -40,7 +40,6 @@ import qualified Kore.Builtin.Map as Builtin.Map import qualified Kore.Builtin.Set as Builtin.Set import qualified Kore.Builtin.Signedness as Builtin.Signedness import qualified Kore.Builtin.String as Builtin.String -import qualified Kore.Domain.Builtin as Domain import Kore.Internal.Condition as Condition import qualified Kore.Internal.OrCondition as OrCondition import qualified Kore.Internal.OrPattern as OrPattern @@ -219,6 +218,11 @@ andEqualsFunctions andEqualsFunctions notSimplifier = [ (AndT, \_ _ s -> expandAlias (maybeTermAnd notSimplifier s)) , (AndT, \_ _ _ -> boolAnd) + , (BothT, \_ _ _ -> Builtin.Int.unifyInt) + , (BothT, \_ _ _ -> Builtin.Bool.unifyBool) + , (BothT, \_ _ _ -> Builtin.String.unifyString) + , (BothT, \_ _ _ -> unifyDomainValue) + , (BothT, \_ _ _ -> unifyStringLiteral) , (BothT, \_ _ _ -> equalAndEquals) , (BothT, \_ _ _ -> bytesDifferent) , (EqualsT, \p _ _ -> bottomTermEquals p) @@ -230,7 +234,6 @@ andEqualsFunctions notSimplifier = , (BothT, \_ _ _ -> constructorSortInjectionAndEquals) , (BothT, \_ _ _ -> constructorAndEqualsAssumesDifferentHeads) , (BothT, \_ _ s -> overloadedConstructorSortInjectionAndEquals s) - , (BothT, \_ _ _ -> Builtin.Bool.unifyBoolValues) , (BothT, \_ _ s -> Builtin.Bool.unifyBoolAnd s) , (BothT, \_ _ s -> Builtin.Bool.unifyBoolOr s) , (BothT, \_ _ s -> Builtin.Bool.unifyBoolNot s) @@ -245,8 +248,6 @@ andEqualsFunctions notSimplifier = , (BothT, \_ _ s -> unifyDefinedModifier (Builtin.Set.unifyEquals s)) , (BothT, \_ t s -> Builtin.List.unifyEquals t s) , (BothT, \_ _ _ -> domainValueAndConstructorErrors) - , (BothT, \_ _ _ -> domainValueAndEqualsAssumesDifferent) - , (BothT, \_ _ _ -> stringLiteralAndEqualsAssumesDifferent) , (BothT, \_ _ s -> unifyDefined s) , (AndT, \_ _ _ t1 t2 -> Error.hoistMaybe $ functionAnd t1 t2) ] @@ -630,44 +631,34 @@ See also: 'equalAndEquals' -} -- TODO (thomas.tuegel): This unification case assumes that \dv is injective, -- but it is not. -domainValueAndEqualsAssumesDifferent - :: HasCallStack +unifyDomainValue + :: forall variable unifier + . HasCallStack => InternalVariable variable => MonadUnify unifier => TermLike variable -> TermLike variable - -> MaybeT unifier a -domainValueAndEqualsAssumesDifferent - first@(DV_ _ _) - second@(DV_ _ _) - = lift $ cannotUnifyDomainValues first second -domainValueAndEqualsAssumesDifferent - first@(Builtin_ (Domain.BuiltinInt _)) - second@(Builtin_ (Domain.BuiltinInt _)) - = lift $ cannotUnifyDomainValues first second -domainValueAndEqualsAssumesDifferent - first@(Builtin_ (Domain.BuiltinString _)) - second@(Builtin_ (Domain.BuiltinString _)) - = lift $ cannotUnifyDomainValues first second -domainValueAndEqualsAssumesDifferent _ _ = empty + -> MaybeT unifier (Pattern variable) +unifyDomainValue term1@(DV_ sort1 value1) term2@(DV_ sort2 value2) = + assert (sort1 == sort2) $ lift worker + where + worker :: unifier (Pattern variable) + worker + | value1 == value2 = + return $ Pattern.fromTermLike term1 + | otherwise = cannotUnifyDomainValues term1 term2 +unifyDomainValue _ _ = empty cannotUnifyDistinctDomainValues :: Pretty.Doc () -cannotUnifyDistinctDomainValues = "Cannot unify distinct domain values." +cannotUnifyDistinctDomainValues = "distinct domain values" cannotUnifyDomainValues - :: HasCallStack - => InternalVariable variable + :: InternalVariable variable => MonadUnify unifier => TermLike variable -> TermLike variable -> unifier a -cannotUnifyDomainValues first second = - assert (first /= second) $ do - explainBottom - cannotUnifyDistinctDomainValues - first - second - empty +cannotUnifyDomainValues = explainAndReturnBottom cannotUnifyDistinctDomainValues {-| Unify two literal strings. @@ -677,18 +668,21 @@ The two patterns are assumed to be inequal; therefore this case always returns See also: 'equalAndEquals' -} -stringLiteralAndEqualsAssumesDifferent - :: HasCallStack - => InternalVariable variable +unifyStringLiteral + :: forall variable unifier + . InternalVariable variable => MonadUnify unifier => TermLike variable -> TermLike variable - -> MaybeT unifier a -stringLiteralAndEqualsAssumesDifferent - first@(StringLiteral_ _) - second@(StringLiteral_ _) - = lift $ cannotUnifyDomainValues first second -stringLiteralAndEqualsAssumesDifferent _ _ = empty + -> MaybeT unifier (Pattern variable) +unifyStringLiteral term1@(StringLiteral_ _) term2@(StringLiteral_ _) = lift worker + where + worker :: unifier (Pattern variable) + worker + | term1 == term2 = + return $ Pattern.fromTermLike term1 + | otherwise = explainAndReturnBottom "distinct string literals" term1 term2 +unifyStringLiteral _ _ = empty {- | Unify any two function patterns. diff --git a/kore/src/Kore/Step/Simplification/Builtin.hs b/kore/src/Kore/Step/Simplification/Builtin.hs index 9e6f65d472..e81d005141 100644 --- a/kore/src/Kore/Step/Simplification/Builtin.hs +++ b/kore/src/Kore/Step/Simplification/Builtin.hs @@ -60,12 +60,6 @@ simplifyBuiltin = fmap mkBuiltin <$> simplifyInternalList list' Domain.BuiltinSet set' -> fmap mkBuiltin <$> simplifyInternalSet set' - Domain.BuiltinInt int -> - (return . pure . mkBuiltin) (Domain.BuiltinInt int) - Domain.BuiltinBool bool -> - (return . pure . mkBuiltin) (Domain.BuiltinBool bool) - Domain.BuiltinString string -> - (return . pure . mkBuiltin) (Domain.BuiltinString string) simplifyInternal :: (InternalVariable variable, Traversable t) diff --git a/kore/src/Kore/Step/Simplification/Ceil.hs b/kore/src/Kore/Step/Simplification/Ceil.hs index e68f8c4182..5103802072 100644 --- a/kore/src/Kore/Step/Simplification/Ceil.hs +++ b/kore/src/Kore/Step/Simplification/Ceil.hs @@ -343,9 +343,6 @@ makeEvaluateBuiltin sideCondition (Domain.BuiltinList l) = do ceils = children And.simplifyEvaluatedMultiPredicate sideCondition (MultiAnd.make ceils) makeEvaluateBuiltin _ (Domain.BuiltinMap _) = empty -makeEvaluateBuiltin _ (Domain.BuiltinBool _) = return OrCondition.top -makeEvaluateBuiltin _ (Domain.BuiltinInt _) = return OrCondition.top -makeEvaluateBuiltin _ (Domain.BuiltinString _) = return OrCondition.top {-| This handles the case when we can't simplify a term's ceil. @@ -399,9 +396,6 @@ makeSimplifiedCeil BuiltinF (Domain.BuiltinMap _) -> True BuiltinF (Domain.BuiltinList _) -> True BuiltinF (Domain.BuiltinSet _) -> True - BuiltinF (Domain.BuiltinInt _) -> unexpectedError - BuiltinF (Domain.BuiltinBool _) -> unexpectedError - BuiltinF (Domain.BuiltinString _) -> unexpectedError DomainValueF _ -> True FloorF _ -> False ForallF _ -> False @@ -413,7 +407,10 @@ makeSimplifiedCeil RewritesF _ -> False TopF _ -> unexpectedError StringLiteralF _ -> unexpectedError + InternalBoolF _ -> unexpectedError InternalBytesF _ -> unexpectedError + InternalIntF _ -> unexpectedError + InternalStringF _ -> unexpectedError VariableF _ -> False unsimplified = diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs index 5a4f55f82a..c094b589ca 100644 --- a/kore/src/Kore/Step/Simplification/Condition.hs +++ b/kore/src/Kore/Step/Simplification/Condition.hs @@ -68,6 +68,10 @@ import Kore.Internal.TermLike , pattern Exists_ , pattern Forall_ , pattern Inj_ + , pattern InternalBool_ + , pattern InternalBytes_ + , pattern InternalInt_ + , pattern InternalString_ , pattern Mu_ , pattern Not_ , pattern Nu_ @@ -336,10 +340,15 @@ retractLocalFunction = where go term1@(App_ symbol1 _) term2 | isFunction symbol1 = + -- TODO (thomas.tuegel): Add tests. case term2 of App_ symbol2 _ | isConstructor symbol2 -> Just (Pair term1 term2) Inj_ _ -> Just (Pair term1 term2) Builtin_ _ -> Just (Pair term1 term2) + InternalInt_ _ -> Just (Pair term1 term2) + InternalBytes_ _ _ -> Just (Pair term1 term2) + InternalString_ _ -> Just (Pair term1 term2) + InternalBool_ _ -> Just (Pair term1 term2) _ -> Nothing go _ _ = Nothing diff --git a/kore/src/Kore/Step/Simplification/InternalBool.hs b/kore/src/Kore/Step/Simplification/InternalBool.hs new file mode 100644 index 0000000000..78821529dc --- /dev/null +++ b/kore/src/Kore/Step/Simplification/InternalBool.hs @@ -0,0 +1,22 @@ +{-| +Copyright : (c) Runtime Verification, 2018 +License : NCSA +-} +module Kore.Step.Simplification.InternalBool + ( simplify + ) where + +import Prelude.Kore + +import Kore.Internal.InternalBool +import Kore.Internal.OrPattern + ( OrPattern + ) +import qualified Kore.Internal.OrPattern as OrPattern +import Kore.Internal.TermLike + +simplify + :: InternalVariable variable + => InternalBool + -> OrPattern variable +simplify = OrPattern.fromPattern . pure . mkInternalBool diff --git a/kore/src/Kore/Step/Simplification/InternalInt.hs b/kore/src/Kore/Step/Simplification/InternalInt.hs new file mode 100644 index 0000000000..f8dbed1814 --- /dev/null +++ b/kore/src/Kore/Step/Simplification/InternalInt.hs @@ -0,0 +1,22 @@ +{-| +Copyright : (c) Runtime Verification, 2018 +License : NCSA +-} +module Kore.Step.Simplification.InternalInt + ( simplify + ) where + +import Prelude.Kore + +import Kore.Internal.InternalInt +import Kore.Internal.OrPattern + ( OrPattern + ) +import qualified Kore.Internal.OrPattern as OrPattern +import Kore.Internal.TermLike + +simplify + :: InternalVariable variable + => InternalInt + -> OrPattern variable +simplify = OrPattern.fromPattern . pure . mkInternalInt diff --git a/kore/src/Kore/Step/Simplification/InternalString.hs b/kore/src/Kore/Step/Simplification/InternalString.hs new file mode 100644 index 0000000000..66ac291198 --- /dev/null +++ b/kore/src/Kore/Step/Simplification/InternalString.hs @@ -0,0 +1,22 @@ +{-| +Copyright : (c) Runtime Verification, 2018 +License : NCSA +-} +module Kore.Step.Simplification.InternalString + ( simplify + ) where + +import Prelude.Kore + +import Kore.Internal.InternalString +import Kore.Internal.OrPattern + ( OrPattern + ) +import qualified Kore.Internal.OrPattern as OrPattern +import Kore.Internal.TermLike + +simplify + :: InternalVariable variable + => InternalString + -> OrPattern variable +simplify = OrPattern.fromPattern . pure . mkInternalString diff --git a/kore/src/Kore/Step/Simplification/Overloading.hs b/kore/src/Kore/Step/Simplification/Overloading.hs index d640621982..6b6f0bb2d5 100644 --- a/kore/src/Kore/Step/Simplification/Overloading.hs +++ b/kore/src/Kore/Step/Simplification/Overloading.hs @@ -431,12 +431,12 @@ maybeMkInj maybeInj injChild = maybe injChild (flip mkInj injChild) maybeInj notUnifiableError :: Monad unifier => TermLike variable -> OverloadingResult unifier a notUnifiableError (DV_ _ _) = throwBottom "injected domain value" -notUnifiableError (BuiltinBool_ _) = throwBottom "injected builtin bool" -notUnifiableError (BuiltinInt_ _) = throwBottom "injected builtin int" +notUnifiableError (InternalBool_ _) = throwBottom "injected builtin bool" +notUnifiableError (InternalInt_ _) = throwBottom "injected builtin int" notUnifiableError (BuiltinList_ _) = throwBottom "injected builtin list" notUnifiableError (BuiltinMap_ _) = throwBottom "injected builtin map" notUnifiableError (BuiltinSet_ _) = throwBottom "injected builtin set" -notUnifiableError (BuiltinString_ _) = throwBottom "injected builtin string" +notUnifiableError (InternalString_ _) = throwBottom "injected builtin string" notUnifiableError _ = notApplicable notUnifiableOverloads :: Monad unifier => OverloadingResult unifier a diff --git a/kore/src/Kore/Step/Simplification/TermLike.hs b/kore/src/Kore/Step/Simplification/TermLike.hs index 16f9c62ef7..3531ae2048 100644 --- a/kore/src/Kore/Step/Simplification/TermLike.hs +++ b/kore/src/Kore/Step/Simplification/TermLike.hs @@ -107,9 +107,18 @@ import qualified Kore.Step.Simplification.Inhabitant as Inhabitant import qualified Kore.Step.Simplification.Inj as Inj ( simplify ) +import qualified Kore.Step.Simplification.InternalBool as InternalBool + ( simplify + ) import qualified Kore.Step.Simplification.InternalBytes as InternalBytes ( simplify ) +import qualified Kore.Step.Simplification.InternalInt as InternalInt + ( simplify + ) +import qualified Kore.Step.Simplification.InternalString as InternalString + ( simplify + ) import qualified Kore.Step.Simplification.Mu as Mu ( simplify ) @@ -430,8 +439,14 @@ simplify sideCondition = \termLike -> -- StringLiteralF stringLiteralF -> return $ StringLiteral.simplify (getConst stringLiteralF) + InternalBoolF internalBoolF -> + return $ InternalBool.simplify (getConst internalBoolF) InternalBytesF internalBytesF -> return $ InternalBytes.simplify (getConst internalBytesF) + InternalIntF internalIntF -> + return $ InternalInt.simplify (getConst internalIntF) + InternalStringF internalStringF -> + return $ InternalString.simplify (getConst internalStringF) VariableF variableF -> return $ Variable.simplify (getConst variableF) DefinedF definedF -> diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs index 11d92e7b7c..03adc233f6 100644 --- a/kore/test/Test/ConsistentKore.hs +++ b/kore/test/Test/ConsistentKore.hs @@ -60,9 +60,6 @@ import Kore.Builtin.Map.Map as BuiltinMap import Kore.Builtin.Set.Set as BuiltinSet ( isSymbolElement ) -import qualified Kore.Builtin.String.String as BuiltinString - ( asBuiltin - ) import qualified Kore.Domain.Builtin as Domain import Kore.IndexedModule.MetadataTools ( SmtMetadataTools @@ -74,6 +71,7 @@ import qualified Kore.Internal.Alias as Alias.DoNotUse import Kore.Internal.ApplicationSorts ( ApplicationSorts (ApplicationSorts) ) +import Kore.Internal.InternalString import qualified Kore.Internal.Symbol as Internal ( Symbol (Symbol) ) @@ -96,6 +94,9 @@ import Kore.Internal.TermLike , mkIff , mkImplies , mkIn + , mkInternalBool + , mkInternalInt + , mkInternalString , mkMu , mkNot , mkNu @@ -147,7 +148,7 @@ data BuiltinGenerator = BuiltinGenerator , attributes :: !AttributeRequirements , generator :: (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) } data CollectionSorts = CollectionSorts @@ -322,7 +323,10 @@ _checkTermImplemented term@(Recursive.project -> _ :< termF) = checkTermF (TopF _) = term checkTermF (VariableF _) = term checkTermF (StringLiteralF _) = term + checkTermF (InternalBoolF _) = term checkTermF (InternalBytesF _) = term + checkTermF (InternalIntF _) = term + checkTermF (InternalStringF _) = term checkTermF (EvaluatedF _) = term checkTermF (InhabitantF _) = term -- Not implemented. checkTermF (EndiannessF _) = term -- Not implemented. @@ -610,12 +614,9 @@ _checkAllBuiltinImplemented -> Domain.Builtin (TermLike Concrete) (TermLike variable) _checkAllBuiltinImplemented builtin = case builtin of - Domain.BuiltinBool _ -> builtin - Domain.BuiltinInt _ -> builtin Domain.BuiltinList _ -> builtin Domain.BuiltinMap _ -> builtin Domain.BuiltinSet _ -> builtin - Domain.BuiltinString _ -> builtin allBuiltinGenerators :: Gen (Map.Map SortRequirements TermGenerator) allBuiltinGenerators = do @@ -647,8 +648,7 @@ allBuiltinGenerators = do when (generatedSort /= resultSort) (error "Sort mismatch.") - builtin <- generator childGenerator - return (mkBuiltin <$> builtin) + generator childGenerator } maybeStringBuiltinGenerator :: Setup -> Maybe BuiltinGenerator @@ -669,9 +669,9 @@ maybeStringBuiltinGenerator Setup { maybeStringBuiltinSort } = stringGenerator :: Sort -> (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) stringGenerator stringSort _childGenerator = - Just . BuiltinString.asBuiltin stringSort <$> stringGen + Just . mkInternalString . InternalString stringSort <$> stringGen maybeBoolBuiltinGenerator :: Setup -> Maybe BuiltinGenerator maybeBoolBuiltinGenerator Setup { maybeBoolSort } = @@ -691,9 +691,9 @@ maybeBoolBuiltinGenerator Setup { maybeBoolSort } = boolGenerator :: Sort -> (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) boolGenerator boolSort _childGenerator = - Just . BuiltinBool.asBuiltin boolSort <$> Gen.bool + Just . mkInternalBool . BuiltinBool.asBuiltin boolSort <$> Gen.bool maybeIntBuiltinGenerator :: Setup -> Maybe BuiltinGenerator maybeIntBuiltinGenerator Setup { maybeIntSort } = @@ -713,10 +713,10 @@ maybeIntBuiltinGenerator Setup { maybeIntSort } = intGenerator :: Sort -> (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) intGenerator intSort _childGenerator = do value <- Gen.integral (Range.constant 0 2000) - return (Just (BuiltinInt.asBuiltin intSort value)) + (pure . Just . mkInternalInt) (BuiltinInt.asBuiltin intSort value) maybeListBuiltinGenerator :: Setup -> Maybe BuiltinGenerator maybeListBuiltinGenerator Setup { maybeListSorts } = @@ -739,14 +739,14 @@ maybeListBuiltinGenerator Setup { maybeListSorts } = :: Sort -> Sort -> (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) listGenerator listSort listElementSort childGenerator = do (Setup {metadataTools}, _) <- Reader.ask elements <- Gen.seq (Range.constant 0 5) (childGenerator listElementSort) return - ( BuiltinList.asBuiltin metadataTools listSort + ( mkBuiltin . BuiltinList.asBuiltin metadataTools listSort <$> sequenceA elements ) @@ -826,7 +826,7 @@ acGenerator -> Gen (Maybe (Domain.Value normalized (TermLike VariableName))) ) -> (Sort -> Gen (Maybe (TermLike VariableName))) - -> Gen (Maybe (Domain.Builtin (TermLike Concrete) (TermLike VariableName))) + -> Gen (Maybe (TermLike VariableName)) acGenerator mapSort keySort valueGenerator childGenerator = do let concreteKeyGenerator :: Gen (Maybe (TermLike Concrete)) concreteKeyGenerator = @@ -861,7 +861,7 @@ acGenerator mapSort keySort valueGenerator childGenerator = do let variablePairs :: [Domain.Element normalized (TermLike VariableName)] variablePairs = catMaybes maybeVariablePairs (Setup {metadataTools}, _) <- Reader.ask - return $ Just $ + return $ Just . mkBuiltin $ AssociativeCommutative.asInternalBuiltin metadataTools mapSort diff --git a/kore/test/Test/Expect.hs b/kore/test/Test/Expect.hs index 05039b57d9..f04e55d5de 100644 --- a/kore/test/Test/Expect.hs +++ b/kore/test/Test/Expect.hs @@ -17,7 +17,7 @@ import Control.Error ) import Debug -import Kore.Domain.Builtin +import Kore.Internal.InternalBool import Kore.Internal.TermLike import Kore.TopBottom @@ -50,7 +50,7 @@ assertTop a | otherwise = (assertFailure . show) (debug a) expectBool :: HasCallStack => TermLike VariableName -> IO Bool -expectBool (BuiltinBool_ internalBool) = return (builtinBoolValue internalBool) +expectBool (InternalBool_ internalBool) = return (internalBoolValue internalBool) expectBool term = (assertFailure . show) (debug term) expectJustT :: MonadIO io => HasCallStack => MaybeT io a -> io a diff --git a/kore/test/Test/Kore.hs b/kore/test/Test/Kore.hs index f30fc03de3..c1667c4093 100644 --- a/kore/test/Test/Kore.hs +++ b/kore/test/Test/Kore.hs @@ -24,7 +24,9 @@ module Test.Kore , setTargetVariableGen , unifiedTargetVariableGen , unifiedVariableGen - , genBuiltin + , genInternalInt + , genInternalBool + , genInternalString , couple , symbolOrAliasGen , addVariable @@ -55,11 +57,13 @@ import Data.Text ) import qualified Data.Text as Text -import qualified Kore.Domain.Builtin as Domain import Kore.Internal.ApplicationSorts ( ApplicationSorts (ApplicationSorts) ) import qualified Kore.Internal.ApplicationSorts as ApplicationSorts.DoNotUse +import Kore.Internal.InternalBool +import Kore.Internal.InternalInt +import Kore.Internal.InternalString import Kore.Internal.Predicate ( Predicate ) @@ -398,26 +402,19 @@ genDomainValue :: (Sort -> Gen child) -> Sort -> Gen (DomainValue Sort child) genDomainValue childGen domainValueSort = DomainValue domainValueSort <$> childGen stringMetaSort -genBuiltin :: Sort -> Gen (TermLike.Builtin (TermLike variable)) -genBuiltin domainValueSort = Gen.choice - [ Domain.BuiltinInt <$> genInternalInt domainValueSort - , Domain.BuiltinBool <$> genInternalBool domainValueSort - , Domain.BuiltinString <$> genInternalString domainValueSort - ] - -genInternalInt :: Sort -> Gen Domain.InternalInt +genInternalInt :: Sort -> Gen InternalInt genInternalInt builtinIntSort = - Domain.InternalInt builtinIntSort <$> genInteger + InternalInt builtinIntSort <$> genInteger where genInteger = Gen.integral (Range.linear (-1024) 1024) -genInternalBool :: Sort -> Gen Domain.InternalBool +genInternalBool :: Sort -> Gen InternalBool genInternalBool builtinBoolSort = - Domain.InternalBool builtinBoolSort <$> Gen.bool + InternalBool builtinBoolSort <$> Gen.bool -genInternalString :: Sort -> Gen Domain.InternalString +genInternalString :: Sort -> Gen InternalString genInternalString internalStringSort = - Domain.InternalString internalStringSort + InternalString internalStringSort <$> Gen.text (Range.linear 0 1024) (Reader.lift Gen.unicode) existsGen :: (Sort -> Gen child) -> Sort -> Gen (Exists Sort VariableName child) diff --git a/kore/test/Test/Kore/Builtin/Bool.hs b/kore/test/Test/Kore/Builtin/Bool.hs index 1a652698f5..3506dc1f47 100644 --- a/kore/test/Test/Kore/Builtin/Bool.hs +++ b/kore/test/Test/Kore/Builtin/Bool.hs @@ -12,6 +12,7 @@ module Test.Kore.Builtin.Bool , test_unifyBoolValues , test_unifyBoolAnd , test_unifyBoolOr + , test_contradiction -- , asPattern , asInternal @@ -31,10 +32,17 @@ import qualified Data.Text as Text import qualified Kore.Builtin.Bool as Bool import qualified Kore.Internal.Condition as Condition import Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate + ( makeAndPredicate + , makeEqualsPredicate + ) +import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike import Kore.Step.Simplification.Data ( SimplifierT , runSimplifier + , runSimplifierBranch + , simplifyCondition ) import qualified Kore.Step.Simplification.Not as Not import Kore.Unification.UnifierT @@ -149,7 +157,7 @@ test_unifyBoolValues = assertEqual "" expected actual unify term1 term2 = - run (Bool.unifyBoolValues term1 term2) + run (Bool.unifyBool term1 term2) test_unifyBoolAnd :: [TestTree] test_unifyBoolAnd = @@ -250,3 +258,28 @@ _False = asInternal False x, y :: SomeVariable VariableName x = inject (mkElementVariable "x" boolSort) y = inject (mkElementVariable "y" boolSort) + +test_contradiction :: TestTree +test_contradiction = + testCase "x andBool y = true ∧ x andBool y = false" $ do + let clause0 = + makeEqualsPredicate boolSort + _True + (andThenBool (mkVar x) (mkVar y)) + clause1 = + makeEqualsPredicate boolSort + _False + (andThenBool (mkVar x) (mkVar y)) + condition = + makeAndPredicate clause0 clause1 + & Condition.fromPredicate + actual <- simplifyCondition' condition + assertEqual "expected bottom" [] actual + where + simplifyCondition' + :: Condition VariableName + -> IO [Condition VariableName] + simplifyCondition' condition = + simplifyCondition SideCondition.top condition + & runSimplifierBranch testEnv + & runNoSMT diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs index 256766a49b..a47297ee4a 100644 --- a/kore/test/Test/Kore/Builtin/Definition.hs +++ b/kore/test/Test/Kore/Builtin/Definition.hs @@ -38,6 +38,8 @@ import qualified Kore.Builtin.Signedness as Signedness import Kore.Domain.Builtin import qualified Kore.Domain.Builtin as Domain import Kore.Internal.ApplicationSorts +import Kore.Internal.InternalBool +import Kore.Internal.InternalInt import Kore.Internal.Symbol ( constructor , function @@ -123,7 +125,7 @@ impliesBoolSymbol = notBool :: TermLike VariableName -> TermLike VariableName notBool x = mkApplySymbol notBoolSymbol [x] -andBool, impliesBool, eqBool, orBool +andBool, impliesBool, eqBool, orBool, andThenBool :: TermLike VariableName -> TermLike VariableName -> TermLike VariableName @@ -131,6 +133,7 @@ andBool x y = mkApplySymbol andBoolSymbol [x, y] impliesBool x y = mkApplySymbol impliesBoolSymbol [x, y] eqBool x y = mkApplySymbol eqBoolSymbol [x, y] orBool x y = mkApplySymbol orBoolSymbol [x, y] +andThenBool x y = mkApplySymbol andThenBoolSymbol [x, y] -- ** Int @@ -751,11 +754,12 @@ string2TokenStringSymbol = builtinSymbol "string2tokenString" userTokenSort [stringSort] & hook "STRING.string2token" -eqString +eqString, concatString :: TermLike VariableName -> TermLike VariableName -> TermLike VariableName eqString i j = mkApplySymbol eqStringSymbol [i, j] +concatString x y = mkApplySymbol concatStringSymbol [x, y] -- * Bytes @@ -1003,10 +1007,10 @@ boolSortDecl = [ hasDomainValuesAttribute, hookAttribute "BOOL.Bool" ] builtinBool :: Bool -> InternalBool -builtinBool builtinBoolValue = +builtinBool internalBoolValue = InternalBool - { builtinBoolSort = boolSort - , builtinBoolValue + { internalBoolSort = boolSort + , internalBoolValue } -- ** Int @@ -1026,10 +1030,10 @@ intSortDecl = [ hasDomainValuesAttribute, hookAttribute "INT.Int" ] builtinInt :: Integer -> InternalInt -builtinInt builtinIntValue = +builtinInt internalIntValue = InternalInt - { builtinIntSort = intSort - , builtinIntValue + { internalIntSort = intSort + , internalIntValue } -- ** KEQUAL diff --git a/kore/test/Test/Kore/Builtin/Int.hs b/kore/test/Test/Kore/Builtin/Int.hs index 8e441cdc33..dc868a5964 100644 --- a/kore/test/Test/Kore/Builtin/Int.hs +++ b/kore/test/Test/Kore/Builtin/Int.hs @@ -21,6 +21,7 @@ module Test.Kore.Builtin.Int , test_symbolic_eq_not_conclusive , test_unifyIntEq , hprop_unparse + , test_contradiction -- , asInternal , asPattern @@ -67,8 +68,8 @@ import Kore.Builtin.Int , tmod ) import qualified Kore.Builtin.Int as Int -import qualified Kore.Domain.Builtin as Domain import qualified Kore.Internal.Condition as Condition +import Kore.Internal.InternalInt import Kore.Internal.Pattern import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate @@ -382,9 +383,8 @@ test_euclidian_division_theorem = extractValue :: Pattern VariableName -> Integer extractValue (Pattern.toTermLike -> term) = case term of - Builtin_ - (Domain.BuiltinInt Domain.InternalInt { builtinIntValue }) -> - builtinIntValue + InternalInt_ InternalInt { internalIntValue } -> + internalIntValue _ -> error "Expecting builtin int." testDivEvaluatedArguments @@ -639,3 +639,32 @@ test_unifyIntEq = simplifyCondition SideCondition.top condition & runSimplifierBranch testEnv & runNoSMT + +test_contradiction :: TestTree +test_contradiction = + testCase "x + y = 0 ∧ x + y = 1" $ do + let clause0 = + makeEqualsPredicate intSort + (asInternal 0) + (addInt x y) + clause1 = + makeEqualsPredicate intSort + (asInternal 1) + (addInt x y) + condition = + makeAndPredicate clause0 clause1 + & Condition.fromPredicate + actual <- simplifyCondition' condition + assertEqual "expected bottom" [] actual + where + x, y :: TermLike VariableName + x = mkElemVar $ ofSort "x" intSort + y = mkElemVar $ ofSort "y" intSort + + simplifyCondition' + :: Condition VariableName + -> IO [Condition VariableName] + simplifyCondition' condition = + simplifyCondition SideCondition.top condition + & runSimplifierBranch testEnv + & runNoSMT diff --git a/kore/test/Test/Kore/Builtin/String.hs b/kore/test/Test/Kore/Builtin/String.hs index 429c02bd52..9177899dbb 100644 --- a/kore/test/Test/Kore/Builtin/String.hs +++ b/kore/test/Test/Kore/Builtin/String.hs @@ -13,6 +13,7 @@ module Test.Kore.Builtin.String , test_token2String , test_string2Token , test_unifyStringEq + , test_contradiction -- , asPattern , asInternal @@ -450,10 +451,6 @@ test_unifyStringEq = assertEqual "" [expect { term = () }] actual ] where - x, y :: ElementVariable VariableName - x = "x" `ofSort` stringSort - y = "y" `ofSort` stringSort - unifyStringEq :: TermLike VariableName -> TermLike VariableName @@ -476,3 +473,32 @@ test_unifyStringEq = simplifyCondition SideCondition.top condition & runSimplifierBranch testEnv & runNoSMT + +x, y :: ElementVariable VariableName +x = "x" `ofSort` stringSort +y = "y" `ofSort` stringSort + +test_contradiction :: TestTree +test_contradiction = + testCase "concatString(x, y) = \"zero\" ∧ concatString(x, y) = \"one\"" $ do + let clause0 = + makeEqualsPredicate boolSort + (asInternal "zero") + (concatString (mkElemVar x) (mkElemVar y)) + clause1 = + makeEqualsPredicate boolSort + (asInternal "one") + (concatString (mkElemVar x) (mkElemVar y)) + condition = + makeAndPredicate clause0 clause1 + & Condition.fromPredicate + actual <- simplifyCondition' condition + assertEqual "expected bottom" [] actual + where + simplifyCondition' + :: Condition VariableName + -> IO [Condition VariableName] + simplifyCondition' condition = + simplifyCondition SideCondition.top condition + & runSimplifierBranch testEnv + & runNoSMT diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 13a3e3a623..ecc3f8197c 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -42,11 +42,8 @@ import Kore.Attribute.Pattern.FreeVariables import Kore.Attribute.Synthetic ( resynthesize ) -import Kore.Domain.Builtin - ( Builtin (..) - , InternalInt (..) - ) import Kore.Internal.ApplicationSorts +import Kore.Internal.InternalInt import Kore.Internal.SideCondition ( SideCondition ) @@ -89,7 +86,9 @@ termLikeChildGen patternSort = | otherwise -> Gen.choice [ mkElemVar <$> elementVariableGen patternSort - , mkBuiltin <$> genBuiltin patternSort + , mkInternalBool <$> genInternalBool patternSort + , mkInternalInt <$> genInternalInt patternSort + , mkInternalString <$> genInternalString patternSort ] | otherwise = (Gen.small . Gen.frequency) @@ -329,16 +328,13 @@ test_hasConstructorLikeTop = True $ isConstructorLikeTop (mkDomainValue dv) let - b :: Kore.Domain.Builtin.Builtin key child - b = BuiltinInt - (InternalInt - { builtinIntSort = Mock.intSort - , builtinIntValue = 1 - } - ) + b = InternalInt + { internalIntSort = Mock.intSort + , internalIntValue = 1 + } assertEqual "BuiltinF is constructor-like-top" True - (isConstructorLikeTop $ mkBuiltin b) + (isConstructorLikeTop $ mkInternalInt b) assertEqual "StringLiteralF is constructor-like-top" True (isConstructorLikeTop $ mkStringLiteral "") diff --git a/kore/test/Test/Kore/Repl/Interpreter.hs b/kore/test/Test/Kore/Repl/Interpreter.hs index 89da5fbc42..5fbc848c48 100644 --- a/kore/test/Test/Kore/Repl/Interpreter.hs +++ b/kore/test/Test/Kore/Repl/Interpreter.hs @@ -72,9 +72,6 @@ import Kore.Step.RulePattern ( mkRewritingRule , rulePattern ) -import Kore.Step.Simplification.AndTerms - ( cannotUnifyDistinctDomainValues - ) import qualified Kore.Step.Simplification.Data as Kore import Kore.Syntax.Module ( ModuleName (..) @@ -341,8 +338,7 @@ unificationFailure = command = Try . ByIndex . Left $ AxiomIndex 0 in do Result { output, continue, state } <- run command axioms [claim] claim - expectedOutput <- - formatUnificationError cannotUnifyDistinctDomainValues one zero + expectedOutput <- formatUnificationError "distinct integers" one zero output `equalsOutput` expectedOutput continue `equals` Continue state `hasCurrentNode` ReplNode 0 @@ -358,8 +354,7 @@ unificationFailureWithName = command = Try . ByName . RuleName $ "impossible" in do Result { output, continue, state } <- run command axioms [claim] claim - expectedOutput <- - formatUnificationError cannotUnifyDistinctDomainValues one zero + expectedOutput <- formatUnificationError "distinct integers" one zero output `equalsOutput` expectedOutput continue `equals` Continue state `hasCurrentNode` ReplNode 0 @@ -407,8 +402,7 @@ forceFailure = command = TryF . ByIndex . Left $ AxiomIndex 0 in do Result { output, continue, state } <- run command axioms [claim] claim - expectedOutput <- - formatUnificationError cannotUnifyDistinctDomainValues one zero + expectedOutput <- formatUnificationError "distinct integers" one zero output `equalsOutput` expectedOutput continue `equals` Continue state `hasCurrentNode` ReplNode 0 @@ -424,8 +418,7 @@ forceFailureWithName = command = TryF . ByName . RuleName $ "impossible" in do Result { output, continue, state } <- run command axioms [claim] claim - expectedOutput <- - formatUnificationError cannotUnifyDistinctDomainValues one zero + expectedOutput <- formatUnificationError "distinct integers" one zero output `equalsOutput` expectedOutput continue `equals` Continue state `hasCurrentNode` ReplNode 0 diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index beb975c5e7..8bb89216a6 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/kore/test/Test/Kore/Step/MockSymbols.hs @@ -173,6 +173,10 @@ fSetId :: Id fSetId = testId "fSet" fIntId :: Id fIntId = testId "fInt" +fBoolId :: Id +fBoolId = testId "fBool" +fStringId :: Id +fStringId = testId "fString" fTestIntId :: Id fTestIntId = testId "fTestInt" fTestFunctionalIntId :: Id @@ -377,6 +381,12 @@ fSetSymbol = symbol fSetId [setSort] setSort & function fIntSymbol :: Symbol fIntSymbol = symbol fIntId [intSort] intSort & function +fBoolSymbol :: Symbol +fBoolSymbol = symbol fBoolId [boolSort] boolSort & function + +fStringSymbol :: Symbol +fStringSymbol = symbol fStringId [stringSort] stringSort & function + fTestIntSymbol :: Symbol fTestIntSymbol = symbol fTestIntId [testSort] intSort & function @@ -873,6 +883,20 @@ fInt -> TermLike variable fInt arg = Internal.mkApplySymbol fIntSymbol [arg] +fBool + :: InternalVariable variable + => HasCallStack + => TermLike variable + -> TermLike variable +fBool arg = Internal.mkApplySymbol fBoolSymbol [arg] + +fString + :: InternalVariable variable + => HasCallStack + => TermLike variable + -> TermLike variable +fString arg = Internal.mkApplySymbol fStringSymbol [arg] + plain00 :: InternalVariable variable => TermLike variable plain00 = Internal.mkApplySymbol plain00Symbol [] @@ -1507,6 +1531,9 @@ sortAttributesMapping = , ( boolSort , Default.def { Attribute.hook = Hook (Just "BOOL.Bool") } ) + , ( stringSort + , Default.def { Attribute.hook = Hook (Just "STRING.String") } + ) -- Also add attributes for the implicitly defined sorts. , ( stringMetaSort diff --git a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs index 605fda6a08..5cf92b5b31 100644 --- a/kore/test/Test/Kore/Step/Simplification/AndTerms.hs +++ b/kore/test/Test/Kore/Step/Simplification/AndTerms.hs @@ -1128,6 +1128,51 @@ test_andTermsSimplification = assertEqual "" expect actual ] ] + + , testGroup "internal Int values" + [ testCase "distinct values" $ do + let expect = [] + input1 = Mock.builtinInt 1 + input2 = Mock.builtinInt 2 + actual <- unify input1 input2 + assertEqual "Expected \\bottom" expect actual + , testCase "identical values" $ do + let expect = [Pattern.fromTermLike input1] + input1 = Mock.builtinInt 1 + input2 = Mock.builtinInt 1 + actual <- unify input1 input2 + assertEqual "" expect actual + ] + + , testGroup "internal Bool values" + [ testCase "distinct values" $ do + let expect = [] + input1 = Mock.builtinBool True + input2 = Mock.builtinBool False + actual <- unify input1 input2 + assertEqual "Expected \\bottom" expect actual + , testCase "identical values" $ do + let expect = [Pattern.fromTermLike input1] + input1 = Mock.builtinBool True + input2 = Mock.builtinBool True + actual <- unify input1 input2 + assertEqual "" expect actual + ] + + , testGroup "internal String values" + [ testCase "distinct values" $ do + let expect = [] + input1 = Mock.builtinString "a" + input2 = Mock.builtinString "b" + actual <- unify input1 input2 + assertEqual "Expected \\bottom" expect actual + , testCase "identical values" $ do + let expect = [Pattern.fromTermLike input1] + input1 = Mock.builtinString "a" + input2 = Mock.builtinString "a" + actual <- unify input1 input2 + assertEqual "" expect actual + ] ] mkVariable :: Text -> Variable VariableName diff --git a/kore/test/Test/Kore/Step/Simplification/Condition.hs b/kore/test/Test/Kore/Step/Simplification/Condition.hs index e179d5d2b6..f1b01e6913 100644 --- a/kore/test/Test/Kore/Step/Simplification/Condition.hs +++ b/kore/test/Test/Kore/Step/Simplification/Condition.hs @@ -1,5 +1,6 @@ module Test.Kore.Step.Simplification.Condition - ( test_predicateSimplification + ( test_simplify_local_functions + , test_predicateSimplification ) where import Prelude.Kore @@ -12,6 +13,7 @@ import Kore.Internal.Condition ( Condition , Conditional (..) ) +import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.Condition as Conditional import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.OrCondition @@ -20,6 +22,7 @@ import Kore.Internal.OrCondition import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Predicate ( makeAndPredicate + , makeCeilPredicate_ , makeEqualsPredicate_ , makeTruePredicate_ ) @@ -40,11 +43,73 @@ import qualified Kore.Step.Axiom.Identifier as AxiomIdentifier import qualified Kore.Step.Simplification.Condition as Condition import Kore.Step.Simplification.Simplify import qualified Kore.Step.Simplification.SubstitutionSimplifier as SubstitutionSimplifier +import Kore.TopBottom import qualified Test.Kore.Step.MockSymbols as Mock import qualified Test.Kore.Step.Simplification as Test import Test.Tasty.HUnit.Ext +test_simplify_local_functions :: [TestTree] +test_simplify_local_functions = + [ -- Constructor at top + test "contradiction: f(x) = a ∧ f(x) = b" f (Right a) (Right b) + , test "contradiction: a = f(x) ∧ f(x) = b" f (Left a) (Right b) + , test "contradiction: a = f(x) ∧ b = f(x)" f (Left a) (Left b) + , test "contradiction: f(x) = a ∧ b = f(x)" f (Right a) (Left b) + -- Sort injection at top + , test "contradiction: f(x) = injA ∧ f(x) = injB" f (Right injA) (Right injB) + , test "contradiction: injA = f(x) ∧ f(x) = injB" f (Left injA) (Right injB) + , test "contradiction: injA = f(x) ∧ injB = f(x)" f (Left injA) (Left injB) + , test "contradiction: f(x) = injA ∧ injB = f(x)" f (Right injA) (Left injB) + -- Int at top + , test "contradiction: f(x) = 2 ∧ f(x) = 3" fInt (Right int2) (Right int3) + , test "contradiction: 2 = f(x) ∧ f(x) = 3" fInt (Left int2) (Right int3) + , test "contradiction: 2 = f(x) ∧ 3 = f(x)" fInt (Left int2) (Left int3) + , test "contradiction: f(x) = 2 ∧ 3 = f(x)" fInt (Right int2) (Left int3) + -- Bool at top + , test "contradiction: f(x) = true ∧ f(x) = false" fBool (Right boolTrue) (Right boolFalse) + , test "contradiction: true = f(x) ∧ f(x) = false" fBool (Left boolTrue) (Right boolFalse) + , test "contradiction: true = f(x) ∧ false = f(x)" fBool (Left boolTrue) (Left boolFalse) + , test "contradiction: f(x) = true ∧ false = f(x)" fBool (Right boolTrue) (Left boolFalse) + -- String at top + , test "contradiction: f(x) = \"one\" ∧ f(x) = \"two\"" fString (Right strOne) (Right strTwo) + , test "contradiction: \"one\" = f(x) ∧ f(x) = \"two\"" fString (Left strOne) (Right strTwo) + , test "contradiction: \"one\" = f(x) ∧ \"two\" = f(x)" fString (Left strOne) (Left strTwo) + , test "contradiction: f(x) = \"one\" ∧ \"two\" = f(x)" fString (Right strOne) (Left strTwo) + ] + where + f = Mock.f (mkElemVar Mock.x) + fInt = Mock.fInt (mkElemVar Mock.xInt) + fBool = Mock.fBool (mkElemVar Mock.xBool) + fString = Mock.fString (mkElemVar Mock.xString) + defined = makeCeilPredicate_ f & Condition.fromPredicate + + a = Mock.a + b = Mock.b + + injA = Mock.sortInjection10 Mock.a + injB = Mock.sortInjection10 Mock.b + + int2 = Mock.builtinInt 2 + int3 = Mock.builtinInt 3 + + boolTrue = Mock.builtinBool True + boolFalse = Mock.builtinBool False + + strOne = Mock.builtinString "one" + strTwo = Mock.builtinString "two" + + mkLocalDefn func (Left t) = makeEqualsPredicate_ t func + mkLocalDefn func (Right t) = makeEqualsPredicate_ func t + + test name func eitherC1 eitherC2 = + testCase name $ do + let equals1 = mkLocalDefn func eitherC1 & Condition.fromPredicate + equals2 = mkLocalDefn func eitherC2 & Condition.fromPredicate + condition = defined <> equals1 <> defined <> equals2 + actual <- simplify condition + assertBool "Expected \\bottom" $ isBottom actual + test_predicateSimplification :: [TestTree] test_predicateSimplification = [ testCase "Identity for top and bottom" $ do @@ -270,6 +335,9 @@ test_predicateSimplification = assertEqual "" (MultiOr.singleton expect) actual ] +simplify :: Condition VariableName -> IO (OrCondition VariableName) +simplify condition = runSimplifier mempty condition + runSimplifier :: BuiltinAndAxiomSimplifierMap -> Condition VariableName diff --git a/kore/test/Test/Kore/Step/Simplification/Equals.hs b/kore/test/Test/Kore/Step/Simplification/Equals.hs index 56cf9caa8d..b8fc3665a5 100644 --- a/kore/test/Test/Kore/Step/Simplification/Equals.hs +++ b/kore/test/Test/Kore/Step/Simplification/Equals.hs @@ -513,20 +513,6 @@ test_equalsSimplification_TermLike = } ) ) - , testCase "domain-value != domain-value because of sorts" - (assertTermEquals - Condition.bottomCondition - (mkDomainValue DomainValue - { domainValueSort = testSort - , domainValueChild = mkStringLiteral "a" - } - ) - (mkDomainValue DomainValue - { domainValueSort = testSort2 - , domainValueChild = mkStringLiteral "a" - } - ) - ) , testCase "\"a\" == \"a\"" (assertTermEqualsGeneric Condition.topCondition @@ -1115,13 +1101,6 @@ plain1OfA = Mock.plain10 Mock.a testSort :: Sort testSort = Mock.testSort -testSort2 :: Sort -testSort2 = - SortActualSort SortActual - { sortActualName = Id "testSort2" AstLocationTest - , sortActualSorts = [] - } - evaluateOr :: Equals Sort (OrPattern VariableName) -> IO (OrPattern VariableName) diff --git a/kore/test/Test/Kore/Step/Simplification/Pattern.hs b/kore/test/Test/Kore/Step/Simplification/Pattern.hs index 839c244c61..a621833154 100644 --- a/kore/test/Test/Kore/Step/Simplification/Pattern.hs +++ b/kore/test/Test/Kore/Step/Simplification/Pattern.hs @@ -8,7 +8,6 @@ import Prelude.Kore import Test.Tasty -import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.OrPattern ( OrPattern @@ -36,9 +35,6 @@ import qualified Kore.Internal.SideCondition as SideCondition import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike import qualified Kore.Step.Simplification.Pattern as Pattern -import Kore.TopBottom - ( isBottom - ) import qualified Test.Kore.Step.MockSymbols as Mock import Test.Kore.Step.Simplification @@ -52,46 +48,6 @@ test_Pattern_simplify = $ "\\or(a, a)" , bottomLike `becomes` OrPattern.bottom $ "\\and(a, \\bottom)" - , testGroup "Local function evaluation" $ - let f = Mock.f (mkElemVar Mock.x) - fInt = Mock.fInt (mkElemVar Mock.xInt) - defined = makeCeilPredicate_ f & Condition.fromPredicate - a = Mock.a - b = Mock.b - injA = Mock.sortInjection10 Mock.a - injB = Mock.sortInjection10 Mock.b - int2 = Mock.builtinInt 2 - int3 = Mock.builtinInt 3 - mkLocalDefn func (Left t) = makeEqualsPredicate_ t func - mkLocalDefn func (Right t) = makeEqualsPredicate_ func t - test name func eitherC1 eitherC2 = - testCase name $ do - let equals1 = mkLocalDefn func eitherC1 & Condition.fromPredicate - equals2 = mkLocalDefn func eitherC2 & Condition.fromPredicate - patt = - Pattern.fromCondition_ - ( defined <> equals1 - <> defined <> equals2 - ) - actual <- simplify patt - assertBool "Expected \\bottom" $ isBottom actual - in - [ -- Constructor at top - test "contradiction: f(x) = a ∧ f(x) = b" f (Right a) (Right b) - , test "contradiction: a = f(x) ∧ f(x) = b" f (Left a) (Right b) - , test "contradiction: a = f(x) ∧ b = f(x)" f (Left a) (Left b) - , test "contradiction: f(x) = a ∧ b = f(x)" f (Right a) (Left b) - -- Sort injection at top - , test "contradiction: f(x) = injA ∧ f(x) = injB" f (Right injA) (Right injB) - , test "contradiction: injA = f(x) ∧ f(x) = injB" f (Left injA) (Right injB) - , test "contradiction: injA = f(x) ∧ injB = f(x)" f (Left injA) (Left injB) - , test "contradiction: f(x) = injA ∧ injB = f(x)" f (Right injA) (Left injB) - -- Builtin at top - , test "contradiction: f(x) = 2 ∧ f(x) = 3" fInt (Right int2) (Right int3) - , test "contradiction: 2 = f(x) ∧ f(x) = 3" fInt (Left int2) (Right int3) - , test "contradiction: 2 = f(x) ∧ 3 = f(x)" fInt (Left int2) (Left int3) - , test "contradiction: f(x) = 2 ∧ 3 = f(x)" fInt (Right int2) (Left int3) - ] , testCase "Replaces and terms under independent quantifiers" $ do let expect = Pattern.fromTermAndPredicate diff --git a/nix/kore.nix.d/kore.nix b/nix/kore.nix.d/kore.nix index b0ecbd0fd7..5a76f2c5af 100644 --- a/nix/kore.nix.d/kore.nix +++ b/nix/kore.nix.d/kore.nix @@ -235,7 +235,10 @@ "Kore/Internal/Condition" "Kore/Internal/Conditional" "Kore/Internal/Inj" + "Kore/Internal/InternalBool" "Kore/Internal/InternalBytes" + "Kore/Internal/InternalInt" + "Kore/Internal/InternalString" "Kore/Internal/MultiAnd" "Kore/Internal/MultiOr" "Kore/Internal/OrCondition" @@ -348,7 +351,10 @@ "Kore/Step/Simplification/Inhabitant" "Kore/Step/Simplification/Inj" "Kore/Step/Simplification/InjSimplifier" + "Kore/Step/Simplification/InternalBool" "Kore/Step/Simplification/InternalBytes" + "Kore/Step/Simplification/InternalInt" + "Kore/Step/Simplification/InternalString" "Kore/Step/Simplification/Mu" "Kore/Step/Simplification/Next" "Kore/Step/Simplification/NoConfusion" diff --git a/test/imp/2.merge.out.golden b/test/imp/2.merge.out.golden index 13ac7676e2..db8f4879dc 100644 --- a/test/imp/2.merge.out.golden +++ b/test/imp/2.merge.out.golden @@ -7,7 +7,7 @@ \and{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("false"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( /* Fl Fn D Sfc */ diff --git a/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden b/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden index fa7382b4b3..ccdb9cafae 100644 --- a/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden +++ b/test/imp/sum-save-proofs-spec.k.save-proofs.kore.golden @@ -8,11 +8,11 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d \and{SortGeneratedTopCell{}}( /* Spa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Spa */ Lbl'Unds-GT-Eqls'Int'Unds'{}( /* Fl Fn D Sfa */ VarN:SortInt{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Spa */ @@ -40,7 +40,6 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortAExp{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -95,7 +94,6 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortAExp{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("-1") ) ) @@ -166,8 +164,7 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d ), /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Spa */ @@ -189,7 +186,6 @@ module haskell-backend-saved-claims-43943e50-f723-47cd-99fd-07104d664c6d /* Fl Fn D Sfa */ VarN:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa */ VarN:SortInt{} diff --git a/test/issue-2095/test-issue-2095.sh.out.golden b/test/issue-2095/test-issue-2095.sh.out.golden index 69e5afdeab..5ba8046889 100644 --- a/test/issue-2095/test-issue-2095.sh.out.golden +++ b/test/issue-2095/test-issue-2095.sh.out.golden @@ -22,7 +22,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -84,7 +83,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -93,7 +91,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -102,7 +99,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -111,7 +107,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -126,7 +121,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -135,7 +129,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -156,7 +149,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -312,7 +304,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -788,7 +779,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -1052,7 +1042,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -1189,7 +1178,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -1204,7 +1192,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -1229,7 +1216,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -1381,7 +1367,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -1396,7 +1381,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -1529,13 +1513,11 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ), /* Fl Fn D Sfa Cl */ @@ -1547,7 +1529,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -1588,7 +1569,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -1719,7 +1699,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -1728,7 +1707,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -1737,7 +1715,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -1746,7 +1723,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -1761,7 +1737,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -1770,7 +1745,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -1791,7 +1765,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -1947,7 +1920,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -2086,7 +2058,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -2648,7 +2619,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -2912,7 +2882,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -3049,7 +3018,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -3064,7 +3032,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -3089,7 +3056,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -3241,7 +3207,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -3256,7 +3221,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -3389,13 +3353,11 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ @@ -3407,7 +3369,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -3449,7 +3410,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -3562,7 +3522,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -3571,7 +3530,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -3580,7 +3538,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -3589,7 +3546,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -3604,7 +3560,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -3613,7 +3568,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -3634,7 +3588,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -3790,7 +3743,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -3975,7 +3927,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ), @@ -4414,7 +4365,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -4678,7 +4628,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -4815,7 +4764,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -4830,7 +4778,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -4855,7 +4802,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -5007,7 +4953,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -5022,7 +4967,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -5155,13 +5099,11 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ @@ -5173,7 +5115,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -5215,7 +5156,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -5304,7 +5244,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -5313,7 +5252,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -5322,7 +5260,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -5331,7 +5268,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -5345,7 +5281,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -5354,7 +5289,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -5375,7 +5309,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -5530,7 +5463,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -6011,7 +5943,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -6275,7 +6206,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -6412,7 +6342,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -6427,7 +6356,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -6452,7 +6380,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -6604,7 +6531,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -6619,7 +6545,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -6750,13 +6675,11 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ @@ -6767,7 +6690,7 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ) ) @@ -6835,7 +6758,6 @@ /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( @@ -6851,7 +6773,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -7021,7 +6942,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -7030,7 +6950,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -7039,7 +6958,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -7048,7 +6966,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -7062,7 +6979,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -7071,7 +6987,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -7092,7 +7007,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ), @@ -7247,7 +7161,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -7350,7 +7263,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -7365,7 +7277,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -7390,7 +7301,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -7542,7 +7452,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -7557,7 +7466,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -7686,7 +7594,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -8211,7 +8118,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -8475,7 +8381,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -8612,7 +8517,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -8627,7 +8531,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -8652,7 +8555,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -8804,7 +8706,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -8819,7 +8720,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -9045,7 +8945,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -9061,12 +8960,11 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ @@ -9076,7 +8974,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ), /* Fl Fn D Sfa Cl */ dotk{}() @@ -9085,8 +8982,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) @@ -9153,7 +9049,7 @@ /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false"), + \dv{SortBool{}}("false"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( /* Fl Fn D Sfa */ @@ -9168,7 +9064,6 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( @@ -9319,7 +9214,7 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -9327,7 +9222,7 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -9335,7 +9230,7 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -9343,7 +9238,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -9357,7 +9251,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -9366,7 +9259,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -9387,7 +9279,7 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -9541,7 +9433,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -9769,7 +9660,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -9784,7 +9674,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -9908,7 +9797,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -10016,7 +9904,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ), @@ -10425,7 +10312,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -10689,7 +10575,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -10826,7 +10711,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -10841,7 +10725,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -10866,7 +10749,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -11018,7 +10900,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -11033,7 +10914,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -11259,7 +11139,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -11274,13 +11153,12 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'trace'-GT-'{}( @@ -11289,7 +11167,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ), /* Fl Fn D Sfa Cl */ @@ -11297,7 +11174,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ), /* Fl Fn D Sfa Cl */ dotk{}() @@ -11307,8 +11183,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) @@ -11373,7 +11248,7 @@ /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false"), + \dv{SortBool{}}("false"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( /* Fl Fn D Sfa */ @@ -11388,7 +11263,7 @@ /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( /* Fl Fn D Sfc */ @@ -11512,24 +11387,21 @@ Lbl'-LT-'mybalance'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'myamount'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mynow'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -11537,7 +11409,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -11551,7 +11422,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -11560,7 +11430,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -11580,8 +11449,7 @@ Lbl'-LT-'nonce'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -11735,7 +11603,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -11883,7 +11750,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -12283,7 +12149,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -12547,7 +12412,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -12684,7 +12548,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -12699,7 +12562,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -12724,7 +12586,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -12876,7 +12737,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -12891,7 +12751,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -13021,13 +12880,12 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'trace'-GT-'{}( @@ -13036,7 +12894,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ), /* Fl Fn D Sfa Cl */ dotk{}() @@ -13045,8 +12902,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) @@ -13110,8 +12966,7 @@ \and{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( /* Fl Fn D Sfc */ @@ -13128,7 +12983,7 @@ /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( /* Fl Fn D Sfa */ @@ -13188,7 +13043,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -13220,7 +13074,7 @@ ) ), /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ) ) ) @@ -13275,24 +13129,21 @@ Lbl'-LT-'mybalance'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'myamount'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mynow'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -13300,7 +13151,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -13314,7 +13164,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -13323,7 +13172,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -13343,8 +13191,7 @@ Lbl'-LT-'nonce'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -13498,7 +13345,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -13664,7 +13510,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -14147,7 +13992,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -14411,7 +14255,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -14548,7 +14391,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -14563,7 +14405,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -14588,7 +14429,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -14740,7 +14580,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -14755,7 +14594,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -14981,7 +14819,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -14996,13 +14833,11 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'trace'-GT-'{}( @@ -15011,7 +14846,7 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") + \dv{SortString{}}("==") ), /* Fl Fn D Sfa Cl */ dotk{}() ) @@ -15019,8 +14854,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) @@ -15084,8 +14918,7 @@ \and{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( /* Fl Fn D Sfc */ @@ -15100,8 +14933,7 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( /* Fl Fn D Sfa */ Var'QuesUnds'4:SortInt{}, @@ -15126,7 +14958,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -15157,8 +14988,7 @@ ) ) ), - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Sfc */ \equals{SortOptionData{}, SortGeneratedTopCell{}}( @@ -15242,24 +15072,21 @@ Lbl'-LT-'mybalance'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'myamount'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mynow'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -15267,7 +15094,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") ) ), @@ -15280,7 +15106,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -15289,7 +15114,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -15309,8 +15133,7 @@ Lbl'-LT-'nonce'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -15463,7 +15286,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -15609,7 +15431,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -16009,7 +15830,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -16273,7 +16093,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -16410,7 +16229,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -16425,7 +16243,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -16450,7 +16267,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -16602,7 +16418,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -16617,7 +16432,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -16745,13 +16559,11 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'trace'-GT-'{}( @@ -16759,8 +16571,7 @@ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") + /* Fl Fn D Sfa Cl */ \dv{SortString{}}("==") ), /* Fl Fn D Sfa Cl */ dotk{}() ) @@ -16768,7 +16579,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) @@ -16830,8 +16641,7 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false"), /* Fl Fn D Sfa */ Lbl'UndsEqlsEqls'Int'Unds'{}( /* Fl Fn D Sfa */ Var'QuesUnds'4:SortInt{}, @@ -16843,8 +16653,7 @@ \and{SortGeneratedTopCell{}}( /* Sfc */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfc */ Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}( /* Fl Fn D Sfc */ @@ -16969,24 +16778,21 @@ Lbl'-LT-'mybalance'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'myamount'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Mutez'LParUndsRParUnds'MICHELSON-COMMON'Unds'Mutez'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mynow'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -16994,7 +16800,7 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidMyAddr") + \dv{SortString{}}("InvalidMyAddr") ) ), /* Fl Fn D Sfa Cl */ @@ -17006,7 +16812,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSourceAddr") ) ), @@ -17015,7 +16820,6 @@ /* Fl Fn D Sfa Cl */ Lbl'Hash'Address'LParUndsRParUnds'MICHELSON-COMMON'Unds'Address'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("InvalidSenderAddr") ) ), @@ -17035,8 +16839,7 @@ Lbl'-LT-'nonce'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ @@ -17189,7 +16992,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -17354,7 +17156,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -17836,7 +17637,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("==") ) ), @@ -18100,7 +17900,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") ) ), @@ -18237,7 +18036,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true") ) ) @@ -18252,7 +18050,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") ) ), @@ -18277,7 +18074,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -18429,7 +18225,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortBool{}, SortData{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ) ) @@ -18444,7 +18239,6 @@ /* Fl Fn D Sfa Cl */ LblTRACE'LParUndsRParUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'String{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ) ), @@ -18668,7 +18462,6 @@ /* Fl Fn D Sfa */ VarI2:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") ) ) @@ -18683,12 +18476,11 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'returncode'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'assumeFailed'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'trace'-GT-'{}( @@ -18696,22 +18488,20 @@ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("=/=") + /* Fl Fn D Sfa Cl */ \dv{SortString{}}("=/=") ), /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("IN MAP") + \dv{SortString{}}("IN MAP") ), /* Fl Fn D Sfa Cl */ kseq{}( /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortString{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortString{}}("COMPARE") ), /* Fl Fn D Sfa Cl */ dotk{}() @@ -18722,7 +18512,7 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ) diff --git a/test/issue-2221/test-issue-2221.sh.out.golden b/test/issue-2221/test-issue-2221.sh.out.golden index c9131e0f48..5b137b62b9 100644 --- a/test/issue-2221/test-issue-2221.sh.out.golden +++ b/test/issue-2221/test-issue-2221.sh.out.golden @@ -9,9 +9,7 @@ /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{} ), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'size'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1") - ) + Lbl'-LT-'size'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1")) ), /* Created: Kore.Internal.Predicate.makeAndPredicate */ /* Spa */ diff --git a/test/issue-2244/test-issue-2244.sh.out.golden b/test/issue-2244/test-issue-2244.sh.out.golden index a9ed3ffe1c..a05817bc23 100644 --- a/test/issue-2244/test-issue-2244.sh.out.golden +++ b/test/issue-2244/test-issue-2244.sh.out.golden @@ -101,13 +101,13 @@ /* Fl Fn D Sfa */ VarL:SortInternalList{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + \dv{SortInt{}}("0") ), /* Fl Fn D Sfa */ Lbl'UndsPlus'Int'Unds'{}( /* Fl Fn D Sfa */ VarI:SortInt{}, /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + \dv{SortInt{}}("1") ) ) ) @@ -167,12 +167,12 @@ /* Fl Fn D Sfa */ Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( /* Fl Fn D Sfa */ VarL:SortInternalList{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa */ Lbl'UndsPlus'Int'Unds'{}( /* Fl Fn D Sfa */ VarI:SortInt{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ), /* Fl Fn D Sfa */ @@ -180,7 +180,7 @@ /* Fl Fn D Sfa */ Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}( /* Fl Fn D Sfa */ VarL:SortInternalList{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ), /* Fl Fn D Sfa */ VarI:SortInt{} ) diff --git a/test/priority/1.merge.out.golden b/test/priority/1.merge.out.golden index 2820905074..d98f6a7408 100644 --- a/test/priority/1.merge.out.golden +++ b/test/priority/1.merge.out.golden @@ -10,11 +10,11 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-GT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("8") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("8") ) ), /* Created: Kore.Internal.MultiAnd.makeAndPredicate */ @@ -22,26 +22,22 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-LT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("10") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("10") ) ), /* Sfa */ \not{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-LT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("6") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") ) ) ) diff --git a/test/priority/2.merge.out.golden b/test/priority/2.merge.out.golden index 7e2f71a5bc..bd9cb6f59b 100644 --- a/test/priority/2.merge.out.golden +++ b/test/priority/2.merge.out.golden @@ -10,11 +10,11 @@ \and{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-LT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("10") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("10") ) ), /* Created: Kore.Internal.MultiAnd.makeAndPredicate */ @@ -24,13 +24,11 @@ \not{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-GT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("8") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("8") ) ) ), @@ -38,13 +36,11 @@ \not{SortGeneratedTopCell{}}( /* Sfa */ \equals{SortBool{}, SortGeneratedTopCell{}}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("true"), + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"), /* Fl Fn D Sfa */ Lbl'Unds-LT-'Int'Unds'{}( /* Fl Fn D Sfa */ VarX0:SortInt{}, - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("6") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("6") ) ) ) diff --git a/test/regression-evm-semantics-39dd1e5/test-add0.sh.out.golden b/test/regression-evm-semantics-39dd1e5/test-add0.sh.out.golden index 76fa75f1f0..a749d9582d 100644 --- a/test/regression-evm-semantics-39dd1e5/test-add0.sh.out.golden +++ b/test/regression-evm-semantics-39dd1e5/test-add0.sh.out.golden @@ -4,9 +4,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'kevm'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'exit-code'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ), + Lbl'-LT-'exit-code'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mode'-GT-'{}( /* Fl Fn D Sfa Cl */ @@ -65,7 +63,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callValue'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'wordStack'-GT-'{}( @@ -78,28 +76,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'pc'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'memoryUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callGas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'static'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callDepth'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa */ @@ -114,12 +111,12 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'refund'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasPrice'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'origin'-GT-'{}( @@ -134,27 +131,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'block'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'previousHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommersHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'coinbase'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'stateRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'transactionsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'receiptsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'logsBloom'-GT-'{}( @@ -162,23 +159,23 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'difficulty'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'number'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasLimit'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'timestamp'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'extraData'-GT-'{}( @@ -186,11 +183,11 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mixHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'blockNonce'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommerBlockHeaders'-GT-'{}( @@ -230,7 +227,5 @@ Lbl'-LT-'generatedTop'-GT-'{}( ) ), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ) + Lbl'-LT-'generatedCounter'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")) ) \ No newline at end of file diff --git a/test/regression-evm-semantics-39dd1e5/test-branching-invalid.sh.out.golden b/test/regression-evm-semantics-39dd1e5/test-branching-invalid.sh.out.golden index 3e987ee493..318fe706eb 100644 --- a/test/regression-evm-semantics-39dd1e5/test-branching-invalid.sh.out.golden +++ b/test/regression-evm-semantics-39dd1e5/test-branching-invalid.sh.out.golden @@ -112,7 +112,6 @@ /* Fl Fn D Sfa Cli */ /* Inj: */ inj{SortInt{}, SortKItem{}}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("12") ) ) @@ -135,7 +134,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'callValue'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ @@ -152,37 +150,31 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'pc'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("11") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gas'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("9972") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'memoryUsed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callGas'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'static'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callDepth'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -209,7 +201,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'refund'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -222,7 +213,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasPrice'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -256,33 +246,27 @@ Lbl'-LT-'block'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'previousHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommersHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'coinbase'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'stateRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'transactionsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'receiptsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'logsBloom'-GT-'{}( @@ -291,28 +275,23 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'difficulty'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'number'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasLimit'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'timestamp'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'extraData'-GT-'{}( @@ -321,13 +300,11 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mixHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'blockNonce'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommerBlockHeaders'-GT-'{}( @@ -359,8 +336,7 @@ /* Fl Fn D Sfa */ Var'Unds'11:SortExitCodeCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'exit-code'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), @@ -385,7 +361,7 @@ /* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ), diff --git a/test/regression-evm-semantics-39dd1e5/test-pop1.sh.out.golden b/test/regression-evm-semantics-39dd1e5/test-pop1.sh.out.golden index 76fa75f1f0..a749d9582d 100644 --- a/test/regression-evm-semantics-39dd1e5/test-pop1.sh.out.golden +++ b/test/regression-evm-semantics-39dd1e5/test-pop1.sh.out.golden @@ -4,9 +4,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'kevm'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'exit-code'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ), + Lbl'-LT-'exit-code'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mode'-GT-'{}( /* Fl Fn D Sfa Cl */ @@ -65,7 +63,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callValue'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'wordStack'-GT-'{}( @@ -78,28 +76,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'pc'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'memoryUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callGas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'static'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callDepth'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa */ @@ -114,12 +111,12 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'refund'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasPrice'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'origin'-GT-'{}( @@ -134,27 +131,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'block'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'previousHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommersHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'coinbase'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'stateRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'transactionsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'receiptsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'logsBloom'-GT-'{}( @@ -162,23 +159,23 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'difficulty'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'number'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasLimit'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'timestamp'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'extraData'-GT-'{}( @@ -186,11 +183,11 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mixHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'blockNonce'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommerBlockHeaders'-GT-'{}( @@ -230,7 +227,5 @@ Lbl'-LT-'generatedTop'-GT-'{}( ) ), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ) + Lbl'-LT-'generatedCounter'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")) ) \ No newline at end of file diff --git a/test/regression-evm-semantics-39dd1e5/test-straight-line.sh.out.golden b/test/regression-evm-semantics-39dd1e5/test-straight-line.sh.out.golden index c74fda2764..4236d2e6f1 100644 --- a/test/regression-evm-semantics-39dd1e5/test-straight-line.sh.out.golden +++ b/test/regression-evm-semantics-39dd1e5/test-straight-line.sh.out.golden @@ -128,7 +128,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'callValue'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ @@ -136,7 +135,6 @@ /* Fl Fn D Sfa Cl */ Lbl'UndsColnUndsUnds'EVM-TYPES'Unds'WordStack'Unds'Int'Unds'WordStack{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("7"), /* Fl Fn D Sfa Cl */ Lbl'Stop'WordStack'Unds'EVM-TYPES'Unds'WordStack{}() @@ -151,37 +149,31 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'pc'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("67") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gas'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("9991") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'memoryUsed'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callGas'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'static'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callDepth'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -208,7 +200,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'refund'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -221,7 +212,6 @@ /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasPrice'-GT-'{}( /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") ) ) @@ -255,33 +245,27 @@ Lbl'-LT-'block'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'previousHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommersHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'coinbase'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'stateRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'transactionsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'receiptsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'logsBloom'-GT-'{}( @@ -290,28 +274,23 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'difficulty'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'number'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasLimit'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'timestamp'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'extraData'-GT-'{}( @@ -320,13 +299,11 @@ ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mixHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'blockNonce'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommerBlockHeaders'-GT-'{}( @@ -358,8 +335,7 @@ /* Fl Fn D Sfa */ Var'Unds'11:SortExitCodeCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'exit-code'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortInt{}}("1") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("1") ) ) ), @@ -384,7 +360,7 @@ /* Fl Fn D Sfa */ VarDotVar0:SortGeneratedCounterCell{}, /* Fl Fn D Sfa Cl */ Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ) ), diff --git a/test/regression-evm-semantics-39dd1e5/test-sumTo10.sh.out.golden b/test/regression-evm-semantics-39dd1e5/test-sumTo10.sh.out.golden index 76fa75f1f0..a749d9582d 100644 --- a/test/regression-evm-semantics-39dd1e5/test-sumTo10.sh.out.golden +++ b/test/regression-evm-semantics-39dd1e5/test-sumTo10.sh.out.golden @@ -4,9 +4,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'kevm'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'exit-code'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ), + Lbl'-LT-'exit-code'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mode'-GT-'{}( /* Fl Fn D Sfa Cl */ @@ -65,7 +63,7 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callValue'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'wordStack'-GT-'{}( @@ -78,28 +76,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'pc'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'memoryUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callGas'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'static'-GT-'{}( - /* Fl Fn D Sfa Cl */ - /* builtin: */ \dv{SortBool{}}("false") + /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'callDepth'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa */ @@ -114,12 +111,12 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'refund'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ) ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasPrice'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'origin'-GT-'{}( @@ -134,27 +131,27 @@ Lbl'-LT-'generatedTop'-GT-'{}( Lbl'-LT-'block'-GT-'{}( /* Fl Fn D Sfa Cl */ Lbl'-LT-'previousHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommersHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'coinbase'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'stateRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'transactionsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'receiptsRoot'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'logsBloom'-GT-'{}( @@ -162,23 +159,23 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'difficulty'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'number'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasLimit'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'gasUsed'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'timestamp'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'extraData'-GT-'{}( @@ -186,11 +183,11 @@ Lbl'-LT-'generatedTop'-GT-'{}( ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'mixHash'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'blockNonce'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") + /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0") ), /* Fl Fn D Sfa Cl */ Lbl'-LT-'ommerBlockHeaders'-GT-'{}( @@ -230,7 +227,5 @@ Lbl'-LT-'generatedTop'-GT-'{}( ) ), /* Fl Fn D Sfa Cl */ - Lbl'-LT-'generatedCounter'-GT-'{}( - /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0") - ) + Lbl'-LT-'generatedCounter'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")) ) \ No newline at end of file