-- GeNeRaTeD fOr: ../../CBS-beta/Funcons-beta/Values/Composite/Bits/Bits.cbs
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.Composite.Bits.Bits where

import Funcons.EDSL

import Funcons.Operations hiding (Values,libFromList)
entities :: [a]
entities = []

types :: TypeRelation
types = [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList
    [(Name
"bit-vectors",Name -> [TPattern] -> [DataTypeAltt] -> DataTypeMembers
DataTypeMemberss Name
"bit-vectors" [MetaVar -> TPattern
TPVar MetaVar
"N"] [Name -> [FTerm] -> Maybe [TPattern] -> DataTypeAltt
DataTypeMemberConstructor Name
"bit-vector" [FTerm -> FTerm -> FTerm
TSortPower (Name -> FTerm
TName Name
"bits") (MetaVar -> FTerm
TVar MetaVar
"N")] ([TPattern] -> Maybe [TPattern]
forall a. a -> Maybe a
Just [MetaVar -> TPattern
TPVar MetaVar
"N"])])]

funcons :: FunconLibrary
funcons = [(Name, EvalFunction)] -> FunconLibrary
libFromList
    [(Name
"bits",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepBits),(Name
"bit-vector",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBit_vector),(Name
"bytes",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepBytes),(Name
"octets",NullaryFuncon -> EvalFunction
NullaryFuncon NullaryFuncon
stepBytes),(Name
"unsigned-bit-vector-maximum",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepUnsigned_bit_vector_maximum),(Name
"signed-bit-vector-maximum",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSigned_bit_vector_maximum),(Name
"signed-bit-vector-minimum",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepSigned_bit_vector_minimum),(Name
"is-in-signed-bit-vector",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_in_signed_bit_vector),(Name
"is-in-unsigned-bit-vector",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepIs_in_unsigned_bit_vector),(Name
"bit-vectors",StrictFuncon -> EvalFunction
StrictFuncon StrictFuncon
stepBit_vectors)]

bits_ :: Funcons
bits_ = Name -> Funcons
FName Name
"bits"
stepBits :: NullaryFuncon
stepBits = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> FTerm
TName Name
"booleans") Env
forall k a. Map k a
env

bit_vector_ :: [Funcons] -> Funcons
bit_vector_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"bit-vector" ([Funcons]
fargs)
stepBit_vector :: StrictFuncon
stepBit_vector [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"_X1*" SeqSortOp
StarOp] Env
forall k a. Map k a
env
            Env
env <- SideCondition -> Env -> Rewrite Env
sideCondition (FTerm -> FTerm -> SideCondition
SCIsInSort (MetaVar -> FTerm
TVar MetaVar
"_X1*") (FTerm -> SeqSortOp -> FTerm
TSortSeq (FTerm -> SeqSortOp -> FTerm
TSortSeq (Name -> FTerm
TName Name
"values") SeqSortOp
QuestionMarkOp) SeqSortOp
StarOp)) Env
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"datatype-value" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"list" [Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
98)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
105)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
45)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
118)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
101)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
99)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
116)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
111)]),Values -> Funcons
FValue (Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"unicode-character" [Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Int Integer
114)])])),MetaVar -> FTerm
TVar MetaVar
"_X1*"]) Env
env

bytes_ :: Funcons
bytes_ = Name -> Funcons
FName Name
"bytes"
octets_ :: Funcons
octets_ = Name -> Funcons
FName Name
"bytes"
stepBytes :: NullaryFuncon
stepBytes = [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"bit-vectors" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
8))]) Env
forall k a. Map k a
env

unsigned_bit_vector_maximum_ :: [Funcons] -> Funcons
unsigned_bit_vector_maximum_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"unsigned-bit-vector-maximum" ([Funcons]
fargs)
stepUnsigned_bit_vector_maximum :: StrictFuncon
stepUnsigned_bit_vector_maximum [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"natural-numbers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"integer-subtract" [Name -> [FTerm] -> FTerm
TApp Name
"integer-power" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
2)),MetaVar -> FTerm
TVar MetaVar
"N"],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))]) Env
env

signed_bit_vector_maximum_ :: [Funcons] -> Funcons
signed_bit_vector_maximum_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"signed-bit-vector-maximum" ([Funcons]
fargs)
stepSigned_bit_vector_maximum :: StrictFuncon
stepSigned_bit_vector_maximum [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"natural-numbers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"integer-subtract" [Name -> [FTerm] -> FTerm
TApp Name
"integer-power" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
2)),Name -> [FTerm] -> FTerm
TApp Name
"integer-subtract" [MetaVar -> FTerm
TVar MetaVar
"N",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))]],Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))]) Env
env

signed_bit_vector_minimum_ :: [Funcons] -> Funcons
signed_bit_vector_minimum_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"signed-bit-vector-minimum" ([Funcons]
fargs)
stepSigned_bit_vector_minimum :: StrictFuncon
stepSigned_bit_vector_minimum [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"natural-numbers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"integer-negate" [Name -> [FTerm] -> FTerm
TApp Name
"integer-power" [Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
2)),Name -> [FTerm] -> FTerm
TApp Name
"integer-subtract" [MetaVar -> FTerm
TVar MetaVar
"N",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
1))]]]) Env
env

is_in_signed_bit_vector_ :: [Funcons] -> Funcons
is_in_signed_bit_vector_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-in-signed-bit-vector" ([Funcons]
fargs)
stepIs_in_signed_bit_vector :: StrictFuncon
stepIs_in_signed_bit_vector [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M") (Name -> FTerm
TName Name
"integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"natural-numbers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"integer-is-less-or-equal" [MetaVar -> FTerm
TVar MetaVar
"M",Name -> [FTerm] -> FTerm
TApp Name
"signed-bit-vector-maximum" [MetaVar -> FTerm
TVar MetaVar
"N"]],Name -> [FTerm] -> FTerm
TApp Name
"integer-is-greater-or-equal" [MetaVar -> FTerm
TVar MetaVar
"M",Name -> [FTerm] -> FTerm
TApp Name
"signed-bit-vector-minimum" [MetaVar -> FTerm
TVar MetaVar
"N"]]]) Env
env

is_in_unsigned_bit_vector_ :: [Funcons] -> Funcons
is_in_unsigned_bit_vector_ [Funcons]
fargs = Name -> [Funcons] -> Funcons
FApp Name
"is-in-unsigned-bit-vector" ([Funcons]
fargs)
stepIs_in_unsigned_bit_vector :: StrictFuncon
stepIs_in_unsigned_bit_vector [Values]
fargs =
    [NullaryFuncon] -> [MSOS StepRes] -> NullaryFuncon
evalRules [NullaryFuncon
rewrite1] []
    where rewrite1 :: NullaryFuncon
rewrite1 = do
            let env :: Map k a
env = Map k a
forall k a. Map k a
emptyEnv
            Env
env <- [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
fargs [VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"M") (Name -> FTerm
TName Name
"integers"),VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
"N") (Name -> FTerm
TName Name
"natural-numbers")] Env
forall k a. Map k a
env
            FTerm -> Env -> NullaryFuncon
rewriteTermTo (Name -> [FTerm] -> FTerm
TApp Name
"and" [Name -> [FTerm] -> FTerm
TApp Name
"integer-is-less-or-equal" [MetaVar -> FTerm
TVar MetaVar
"M",Name -> [FTerm] -> FTerm
TApp Name
"unsigned-bit-vector-maximum" [MetaVar -> FTerm
TVar MetaVar
"N"]],Name -> [FTerm] -> FTerm
TApp Name
"integer-is-greater-or-equal" [MetaVar -> FTerm
TVar MetaVar
"M",Funcons -> FTerm
TFuncon (Values -> Funcons
FValue (Integer -> Values
forall t. Integer -> Values t
Nat Integer
0))]]) Env
env

bit_vectors_ :: [Funcons] -> Funcons
bit_vectors_ = Name -> [Funcons] -> Funcons
FApp Name
"bit-vectors"
stepBit_vectors :: StrictFuncon
stepBit_vectors [Values]
ts = Name -> StrictFuncon
rewriteType Name
"bit-vectors" [Values]
ts