Bits.hs

-- GeNeRaTeD fOr: ../../CBS/Funcons/Values/Primitive values/bits.aterm
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Core.Values.PrimitiveValues.Bits where

import Funcons.EDSL

entities = []

types = typeEnvFromList
    []

funcons = libFromList
    [("bytes",NullaryFuncon stepBytes),("unsigned-bits-maximum",StrictFuncon stepUnsigned_bits_maximum),("signed-bits-maximum",StrictFuncon stepSigned_bits_maximum),("signed-bits-minimum",StrictFuncon stepSigned_bits_minimum),("is-in-signed-bits",StrictFuncon stepIs_in_signed_bits),("is-in-unsigned-bits",StrictFuncon stepIs_in_unsigned_bits)]

bytes_ = FName "bytes"
stepBytes = evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            rewriteTo (FApp "bits" (FTuple [FValue (Nat 8)]))

unsigned_bits_maximum_ fargs = FApp "unsigned-bits-maximum" (FTuple fargs)
stepUnsigned_bits_maximum fargs =
    evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "values")] env
            rewriteTermTo (TApp "integer-subtract" (TTuple [TApp "integer-power" (TTuple [TFuncon (FValue (Nat 2)),TVar "N"]),TFuncon (FValue (Nat 1))])) env

signed_bits_maximum_ fargs = FApp "signed-bits-maximum" (FTuple fargs)
stepSigned_bits_maximum fargs =
    evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "values")] env
            rewriteTermTo (TApp "integer-subtract" (TTuple [TApp "integer-power" (TTuple [TFuncon (FValue (Nat 2)),TApp "integer-subtract" (TTuple [TVar "N",TFuncon (FValue (Nat 1))])]),TFuncon (FValue (Nat 1))])) env

signed_bits_minimum_ fargs = FApp "signed-bits-minimum" (FTuple fargs)
stepSigned_bits_minimum fargs =
    evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "values")] env
            rewriteTermTo (TApp "integer-negate" (TTuple [TApp "integer-power" (TTuple [TFuncon (FValue (Nat 2)),TApp "integer-subtract" (TTuple [TVar "N",TFuncon (FValue (Nat 1))])])])) env

is_in_signed_bits_ fargs = FApp "is-in-signed-bits" (FTuple fargs)
stepIs_in_signed_bits fargs =
    evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "values"),VPAnnotated (VPMetaVar "I") (TName "values")] env
            rewriteTermTo (TApp "and" (TTuple [TApp "is-less-or-equal" (TTuple [TVar "I",TApp "signed-bits-maximum" (TTuple [TVar "N"])]),TApp "is-greater-or-equal" (TTuple [TVar "I",TApp "signed-bits-minimum" (TTuple [TVar "N"])])])) env

is_in_unsigned_bits_ fargs = FApp "is-in-unsigned-bits" (FTuple fargs)
stepIs_in_unsigned_bits fargs =
    evalRules [rewrite1] []
    where rewrite1 = do
            let env = emptyEnv
            env <- vsMatch fargs [VPAnnotated (VPMetaVar "N") (TName "values"),VPAnnotated (VPMetaVar "I") (TName "values")] env
            rewriteTermTo (TApp "and" (TTuple [TApp "is-less-or-equal" (TTuple [TVar "I",TApp "unsigned-bits-maximum" (TTuple [TVar "N"])]),TApp "is-greater-or-equal" (TTuple [TVar "I",TFuncon (FValue (Nat 0))])])) env