## StaticEvaluation Module

Module StaticEvaluation implements static evaluation of constant expressions of scalar types. To this end, all scalar types are assumed to be reduced to boolean lists, and depending on the operator, these boolean lists may simply be bitvectors, radix-2 numbers or 2-complement numbers. It is always assumed that radix-2 numbers have no redundant leading zeros, and that 2-complement numbers do not have redundant signs. In addition to the static evaluation functions, the module also provides translations of constants of Quartz expressions given as strings to boolean lists as given by functions NatConstStr2BL for nat-constants, BinBitConst2BL for binary bv-constants, OctBitConst2BL for octal bv-constants, and HexBitConst2BL for hexadecimal bv-constants. Functions NatDecStr2BL, BL2NatDecStr, Nat2BL, BL2Nat convert between natural numbers and their radix-2 representations (as boolean lists) and analogously IntDecStr2BL, BL2IntDecStr, Int2BL, BL2Int convert between integers and their 2-complement representations (as boolean lists) Finally, the module provides some additional arithmetic operators like Div, Mod, FloorLog2, and CeilLog2.

### Functions and values

 Function or value Description  BL2Int bl  Full Usage: BL2Int bl Parameters: bl : bool list Returns: int BL2Int converts boolean lists that are viewed as 2-complement representations of an integer to an F# integer i. Caution: The function may fail if bl cannot be represented with 32-bits. bl : bool list Returns: int  BL2IntDecStr bl  Full Usage: BL2IntDecStr bl Parameters: bl : bool list Returns: String BL2IntDecStr is an abbreviation for BL2IntDecStrSign "+" "-". bl : bool list Returns: String  BL2IntDecStrSign plus minus bl  Full Usage: BL2IntDecStrSign plus minus bl Parameters: plus : String minus : String bl : bool list Returns: String "BL2IntDecStrSign plus minus bl" expects a boolean list bl that is interpreted as 2-complement representation of an integer number X. The function then determines the radix-10 representation of X in terms of a string consisting of decimal digits 0,...,0. In addition, two strings "plus" and "minus" must be given that are used to prefix the generated string in case the number is non-negative or negative, respectively. plus : String minus : String bl : bool list Returns: String  BL2Nat bl  Full Usage: BL2Nat bl Parameters: bl : bool list Returns: int BL2Nat converts boolean lists that are viewed as radix-2 representations to a non-negative integer i. Caution: The function may fail if bl cannot be represented as a 32-bit integer. bl : bool list Returns: int  BL2NatDecStr bl  Full Usage: BL2NatDecStr bl Parameters: bl : bool list Returns: String Given a boolean list bl that is understood as binary representation of a natural number, BL2NatDecStr(bl) computes a string s that consists of decimal digits 0,...,9 that is the radix-10 representation of the the considered natural number. bl : bool list Returns: String  BinBitConst2BL bvs  Full Usage: BinBitConst2BL bvs Parameters: bvs : string Returns: bool list BinBitConst2BL s expects a string like "0b1011" that represents a binary bitvector constant in Quartz. The prefix "0b" is then removed and the remaining string is converted to a boolean list by mapping 0 and 1 to false and true, respectively. bvs : string Returns: bool list  CeilLog2 n  Full Usage: CeilLog2 n Parameters: n : int Returns: int CeilLog2(n) is the least integer greater than or equal to log2(n). i.e., CeilLog2 n = int (ceil ((log (double n)) / (log 2.0))) n : int Returns: int  Div (x, y)  Full Usage: Div (x, y) Parameters: x : int y : int Returns: int Div implements the mathematical definition of integer division, i.e. Div(x,y) is that number q where an integer r exists such that (1) x=q*y+r, (2) abs(r) x : int y : int Returns: int  FloorLog2 n  Full Usage: FloorLog2 n Parameters: n : int Returns: int FloorLog2(n) is the greatest integer less than or equal to log2(n). i.e., FloorLog2 n = int (floor ((log (double n)) / (log 2.0))) n : int Returns: int  HexBitConst2BL bvs  Full Usage: HexBitConst2BL bvs Parameters: bvs : string Returns: bool list HexBitConst2BL s expects a string like "0x7342" that represents an hexadecimal bitvector constant in Quartz. The prefix "0x" is then removed and the remaining string is converted to a boolean list by mapping the hexadecimal digits to their corresponding radix-2 representations. bvs : string Returns: bool list  Int2BL i  Full Usage: Int2BL i Parameters: i : int Returns: bool list Int2BL converts any non-negative integer i to its 2-complement representation given as a boolean list. i : int Returns: bool list  IntDecStr2BL s  Full Usage: IntDecStr2BL s Parameters: s : string Returns: bool list IntDecStr2BL(s) expects a string s that must start with '+' or '-' and consists of decimal digits 0,...,9 otherwise. The string is is viewed as explicit sign radix-10 representation of an integer that is converted to its binary 2-complement representation. s : string Returns: bool list  Mod (x, y)  Full Usage: Mod (x, y) Parameters: x : int y : int Returns: int Mod implements the positive remainder of integer division, i.e. Mod(x,y) is that number r where an integer q exists such that (1) x=q*y+r, (2) abs(r) x : int y : int Returns: int  Nat2BL i  Full Usage: Nat2BL i Parameters: i : int Returns: bool list Nat2BL converts a non-negative integer i to its radix-2 representation given as a boolean list. i : int Returns: bool list  NatConstStr2BL s  Full Usage: NatConstStr2BL s Parameters: s : string Returns: bool list NatConstStr2BL s expects a string like "123u" that represents an unsigned integer in Quartz. The suffix "u" is then removed and the remaining string is converted by NatDecStr2BL to a radix-2 representation. s : string Returns: bool list  NatDecStr2BL s  Full Usage: NatDecStr2BL s Parameters: s : string Returns: bool list NatDecStr2BL(s) converts any string s that consists of decimal digits 0,...,9 that is viewed as radix-10 representation of a natural number to a boolean list such that is the radix-2 representation of the decimal number s. s : string Returns: bool list  OctBitConst2BL bvs  Full Usage: OctBitConst2BL bvs Parameters: bvs : string Returns: bool list OctBitConst2BL s expects a string like "0o7342" that represents an octal bitvector constant in Quartz. The prefix "0o" is then removed and the remaining string is converted to a boolean list by mapping the octal digits to their corresponding radix-2 representations. bvs : string Returns: bool list  PrnBtvBL bl  Full Usage: PrnBtvBL bl Parameters: bl : bool list Returns: PrnDrv -> unit bl : bool list Returns: PrnDrv -> unit  PrnIntBL bl  Full Usage: PrnIntBL bl Parameters: bl : bool list Returns: PrnDrv -> unit bl : bool list Returns: PrnDrv -> unit  PrnNatBL bl  Full Usage: PrnNatBL bl Parameters: bl : bool list Returns: PrnDrv -> unit bl : bool list Returns: PrnDrv -> unit  StaticBoolBitOfBtv (bl, n)  Full Usage: StaticBoolBitOfBtv (bl, n) Parameters: bl : bool list n : int Returns: bool extract the n-th bit of bitvector bl=[bL;...;b0] and fails if out of range bl : bool list n : int Returns: bool  StaticBoolCase (cL, b)  Full Usage: StaticBoolCase (cL, b) Parameters: cL : (bool * bool) list b : bool Returns: bool evaluate StaticBoolCase([(c1,b1);...,(cn,bn)],b), i.e. if one of the ci is true, then return the leftmost bi whose ci is true, otherwise return b cL : (bool * bool) list b : bool Returns: bool  StaticBoolConj (b1, b2)  Full Usage: StaticBoolConj (b1, b2) Parameters: b1 : bool b2 : bool Returns: bool perform boolean conjunction: StaticBoolConj(b1,b2) = b1 && b2 b1 : bool b2 : bool Returns: bool  StaticBoolDisj (b1, b2)  Full Usage: StaticBoolDisj (b1, b2) Parameters: b1 : bool b2 : bool Returns: bool perform boolean disjunction: StaticBoolDisj(b1,b2) = b1 || b2 b1 : bool b2 : bool Returns: bool  StaticBoolEqu (b1, b2)  Full Usage: StaticBoolEqu (b1, b2) Parameters: b1 : bool b2 : bool Returns: bool perform boolean equivalence: StaticBoolEqu(b1,b2) = (b1=b2) b1 : bool b2 : bool Returns: bool  StaticBoolImpl (b1, b2)  Full Usage: StaticBoolImpl (b1, b2) Parameters: b1 : bool b2 : bool Returns: bool perform boolean implication: StaticBoolImpl(b1,b2) = (not b1) || b2 b1 : bool b2 : bool Returns: bool  StaticBoolIte (b1, b2, b3)  Full Usage: StaticBoolIte (b1, b2, b3) Parameters: b1 : bool b2 : bool b3 : bool Returns: bool evaluate BoolIte: StaticBoolIte(b1,b2,b3) = if b1 then b2 else b3 b1 : bool b2 : bool b3 : bool Returns: bool  StaticBoolNeg b  Full Usage: StaticBoolNeg b Parameters: b : bool Returns: bool perform boolean negation: StaticBoolNeg b = not b b : bool Returns: bool  StaticBoolNext b  Full Usage: StaticBoolNext b Parameters: b : bool Returns: bool perform boolean next: StaticBoolNext b = b b : bool Returns: bool  StaticBtvAppend (bl1, bl2)  Full Usage: StaticBtvAppend (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list perform bitvector concatenation: StaticBtvAppend(bl1,bl2) = bl1@bl2 bl1 : bool list bl2 : bool list Returns: bool list  StaticBtvCase (caseList, bl)  Full Usage: StaticBtvCase (caseList, bl) Parameters: caseList : (bool * bool list) list bl : bool list Returns: bool list evaluate StaticBtvCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl caseList : (bool * bool list) list bl : bool list Returns: bool list  StaticBtvConj (arg1, arg2)  Full Usage: StaticBtvConj (arg1, arg2) Parameters: arg0 : bool list arg1 : bool list Returns: bool list perform bitwise boolean conjunction, argument lists must have same length arg0 : bool list arg1 : bool list Returns: bool list  StaticBtvDisj (arg1, arg2)  Full Usage: StaticBtvDisj (arg1, arg2) Parameters: arg0 : bool list arg1 : bool list Returns: bool list perform bitwise boolean disjunction, argument lists must have same length arg0 : bool list arg1 : bool list Returns: bool list  StaticBtvEqu (bl1, bl2)  Full Usage: StaticBtvEqu (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool perform bitvector equality: StaticBtvEqu(bl1,bl2) = (bl1=bl2) bl1 : bool list bl2 : bool list Returns: bool  StaticBtvEqv (arg1, arg2)  Full Usage: StaticBtvEqv (arg1, arg2) Parameters: arg0 : bool list arg1 : bool list Returns: bool list perform bitwise boolean equivalence, argument lists must have same length arg0 : bool list arg1 : bool list Returns: bool list  StaticBtvImpl (arg1, arg2)  Full Usage: StaticBtvImpl (arg1, arg2) Parameters: arg0 : bool list arg1 : bool list Returns: bool list perform bitwise boolean implication, argument lists must have same length arg0 : bool list arg1 : bool list Returns: bool list  StaticBtvIte (b, bl1, bl2)  Full Usage: StaticBtvIte (b, bl1, bl2) Parameters: b : bool bl1 : bool list bl2 : bool list Returns: bool list StaticBtvIte(b,bl1,bl2) = if b then bl1 else bl2 b : bool bl1 : bool list bl2 : bool list Returns: bool list  StaticBtvNeg bl  Full Usage: StaticBtvNeg bl Parameters: bl : bool list Returns: bool list perform bitwise boolean negation bl : bool list Returns: bool list  StaticBtvNext bl  Full Usage: StaticBtvNext bl Parameters: bl : bool list Returns: bool list perform bitvector next: StaticBtvNext bl = bl bl : bool list Returns: bool list  StaticBtvOfInt (bl, n)  Full Usage: StaticBtvOfInt (bl, n) Parameters: bl : bool list n : int Returns: bool list convert int constant to bitvector constant of given length (note that int constants are already stored as 2-complement bitvectors) bl : bool list n : int Returns: bool list  StaticBtvOfNat (bl, n)  Full Usage: StaticBtvOfNat (bl, n) Parameters: bl : bool list n : int Returns: bool list convert nat constant to bitvector constant of given length (note that nat constants are already stored as radix-2 bitvectors) bl : bool list n : int Returns: bool list  StaticBtvReplicate (b, n)  Full Usage: StaticBtvReplicate (b, n) Parameters: b : bool n : int Returns: bool list replicate a boolean constant to a bitvector: StaticBtvReplicate(b,n) = [b;...;b], where the generated bitvector has length n b : bool n : int Returns: bool list  StaticBtvReverse B  Full Usage: StaticBtvReverse B Parameters: B : bool list Returns: bool list perform bitvector reversal: StaticBtvReverse([bL;...;b0]) = [b0;...;bL] B : bool list Returns: bool list  StaticBtvSegment (B, n2, n1)  Full Usage: StaticBtvSegment (B, n2, n1) Parameters: B : bool list n2 : int n1 : int Returns: bool list extract a segment of a bitvector: StaticBtvSegment([bL;...;b0],n2,n1) = [bn2;...;bn1] where L>=n2>=n1>=0 must hold B : bool list n2 : int n1 : int Returns: bool list  StaticBtvSignAdjust (n, bv)  Full Usage: StaticBtvSignAdjust (n, bv) Parameters: n : int bv : bool list Returns: bool list sign-adjust length of bitector bv to n, i.e. first remove all redundant sign bits (i.e. bits that are equal to their right neighbor) to obtain a bitvector bv', then either replicate the leftmost bit to extend bv' to length n or remove further leading bits to reduce the size to n (which modifies int-constants) n : int bv : bool list Returns: bool list  StaticBtvSignReduct bl  Full Usage: StaticBtvSignReduct bl Parameters: bl : bool list Returns: bool list perform sign-bit reduction, ie. remove all leading sign bits ie leftmost elements equal to their right neighbor bl : bool list Returns: bool list  StaticBtvZeroAdjust (n, bv)  Full Usage: StaticBtvZeroAdjust (n, bv) Parameters: n : int bv : bool list Returns: bool list zero-adjust length of bitector bv to n, i.e. first remove all leading zero bits to obtain a bitvector bv', then either add zero bits to extend bv' to length n or remove further leading bits to reduce the size to n (which modifies nat-constants) n : int bv : bool list Returns: bool list  StaticBtvZeroReduct bl  Full Usage: StaticBtvZeroReduct bl Parameters: bl : bool list Returns: bool list perform zero-bit reduction, ie. remove all leading zero bits (of course [false] is maintained as it is) bl : bool list Returns: bool list  StaticIntAbs bl  Full Usage: StaticIntAbs bl Parameters: bl : bool list Returns: bool list compute the absolute value of a 2-complement number which is given as radix-2 number representation, since used as NatExpr bl : bool list Returns: bool list  StaticIntAdd (bl1, bl2)  Full Usage: StaticIntAdd (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list addition of the 2-complement numbers bl1 and bl2 bl1 : bool list bl2 : bool list Returns: bool list  StaticIntCase (caseList, bl)  Full Usage: StaticIntCase (caseList, bl) Parameters: caseList : (bool * bool list) list bl : bool list Returns: bool list evaluate StaticIntCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl caseList : (bool * bool list) list bl : bool list Returns: bool list  StaticIntDiv (bl1, bl2)  Full Usage: StaticIntDiv (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list quotient of division of the 2-complement numbers bl1 and bl2 has meaningless value when bl2 is [false] bl1 : bool list bl2 : bool list Returns: bool list  StaticIntEqu (bl1, bl2)  Full Usage: StaticIntEqu (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticIntEqu(bl1,bl2) checks whether bl1 and bl2 represent the same the 2-complement number bl1 : bool list bl2 : bool list Returns: bool  StaticIntIte (b, bl1, bl2)  Full Usage: StaticIntIte (b, bl1, bl2) Parameters: b : bool bl1 : bool list bl2 : bool list Returns: bool list StaticIntIte(b,bl1,bl2) = if b then bl1 else bl2 b : bool bl1 : bool list bl2 : bool list Returns: bool list  StaticIntLeq (bl1, bl2)  Full Usage: StaticIntLeq (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticIntLeq(bl1,bl2) checks whether bl1 is less than or equal to bl2 when these are evaluated as 2-complement numbers bl1 : bool list bl2 : bool list Returns: bool  StaticIntLes (bl1, bl2)  Full Usage: StaticIntLes (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticIntLes(bl1,bl2) checks whether bl1 is less than bl2 when these are evaluated as 2-complement numbers bl1 : bool list bl2 : bool list Returns: bool  StaticIntMod (bl1, bl2)  Full Usage: StaticIntMod (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list remainder of division of the 2-complement numbers bl1 and bl2 has meaningless value when bl2 is [false] bl1 : bool list bl2 : bool list Returns: bool list  StaticIntMul (A, B)  Full Usage: StaticIntMul (A, B) Parameters: A : bool list B : bool list Returns: bool list multiplication of the 2-complement numbers bl1 and bl2 A : bool list B : bool list Returns: bool list  StaticIntNext bl  Full Usage: StaticIntNext bl Parameters: bl : bool list Returns: bool list perform IntExpr next: StaticIntNext bl = bl bl : bool list Returns: bool list  StaticIntOfBtv bl  Full Usage: StaticIntOfBtv bl Parameters: bl : bool list Returns: bool list convert IntExpr constant to bitvector (note that IntExpr constants are already stored in 2-complement representation bl : bool list Returns: bool list  StaticIntSat (blBound, bl)  Full Usage: StaticIntSat (blBound, bl) Parameters: blBound : bool list bl : bool list Returns: bool list bind 2-complement number, i.e. return bl if -blBound<=bl=blBound, and otherwise return -blBound (note that blBound is a radix-2 number while bl is a 2-complement number and that the result is of course also a 2-complement number) blBound : bool list bl : bool list Returns: bool list  StaticIntSub (bl1, bl2)  Full Usage: StaticIntSub (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list subtraction of the 2-complement numbers bl1 and bl2 bl1 : bool list bl2 : bool list Returns: bool list  StaticNatAdd (bl1, bl2)  Full Usage: StaticNatAdd (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list addition of the radix-2 numbers bl1 and bl2 bl1 : bool list bl2 : bool list Returns: bool list  StaticNatCase (caseList, bl)  Full Usage: StaticNatCase (caseList, bl) Parameters: caseList : (bool * bool list) list bl : bool list Returns: bool list evaluate StaticNatCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl caseList : (bool * bool list) list bl : bool list Returns: bool list  StaticNatDiv (bl1, bl2)  Full Usage: StaticNatDiv (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list quotient of division of the radix-2 numbers bl1 and bl2 has meaningless value when bl2 is [false] bl1 : bool list bl2 : bool list Returns: bool list  StaticNatEqu (bl1, bl2)  Full Usage: StaticNatEqu (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticNatEqu(bl1,bl2) checks whether bl1 and bl2 represent the same the radix-2 number bl1 : bool list bl2 : bool list Returns: bool  StaticNatExp (A, B)  Full Usage: StaticNatExp (A, B) Parameters: A : bool list B : bool list Returns: bool list exponentiation of the radix-2 numbers bl1 and bl2 A : bool list B : bool list Returns: bool list  StaticNatIte (b, bl1, bl2)  Full Usage: StaticNatIte (b, bl1, bl2) Parameters: b : bool bl1 : bool list bl2 : bool list Returns: bool list StaticNatIte(b,bl1,bl2) = if b then bl1 else bl2 b : bool bl1 : bool list bl2 : bool list Returns: bool list  StaticNatLeq (bl1, bl2)  Full Usage: StaticNatLeq (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticNatLeq(bl1,bl2) checks whether bl1 is less than or equal to bl2 when these are evaluated as radix-2 numbers bl1 : bool list bl2 : bool list Returns: bool  StaticNatLes (bl1, bl2)  Full Usage: StaticNatLes (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool StaticNatLes(bl1,bl2) checks whether bl1 is less than bl2 when these are evaluated as radix-2 numbers bl1 : bool list bl2 : bool list Returns: bool  StaticNatLog2 bl  Full Usage: StaticNatLog2 bl Parameters: bl : bool list Returns: bool list log2 of a radix-2 number: it's the number of bits minus one after zero-reduction; this number is returned as radix-2 number; note that log2(0) is not defined bl : bool list Returns: bool list  StaticNatMod (bl1, bl2)  Full Usage: StaticNatMod (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list remainder of division of the radix-2 numbers bl1 and bl2 has meaningless value when bl2 is [false] bl1 : bool list bl2 : bool list Returns: bool list  StaticNatMul (A, B)  Full Usage: StaticNatMul (A, B) Parameters: A : bool list B : bool list Returns: bool list multiplication of the radix-2 numbers bl1 and bl2 A : bool list B : bool list Returns: bool list  StaticNatNext bl  Full Usage: StaticNatNext bl Parameters: bl : bool list Returns: bool list perform NatExpr next: StaticNatNext bl = bl bl : bool list Returns: bool list  StaticNatOfBtv bl  Full Usage: StaticNatOfBtv bl Parameters: bl : bool list Returns: bool list convert NatExpr constant to bitvector (note that NatExpr constants are already stored in radix-2 representations bl : bool list Returns: bool list  StaticNatSat (blBound, bl)  Full Usage: StaticNatSat (blBound, bl) Parameters: blBound : bool list bl : bool list Returns: bool list bind radix-2 number, i.e. return bl if bl blBound : bool list bl : bool list Returns: bool list  StaticNatSub (bl1, bl2)  Full Usage: StaticNatSub (bl1, bl2) Parameters: bl1 : bool list bl2 : bool list Returns: bool list subtraction of the radix-2 numbers bl1 and bl2; has meaningless values when the radix-2 value of bl1 is less than bl2 bl1 : bool list bl2 : bool list Returns: bool list  StaticRealAdd (r1, r2)  Full Usage: StaticRealAdd (r1, r2) Parameters: r1 : double r2 : double Returns: double r1 : double r2 : double Returns: double  StaticRealCos r  Full Usage: StaticRealCos r Parameters: r : float Returns: float r : float Returns: float  StaticRealDiv (r1, r2)  Full Usage: StaticRealDiv (r1, r2) Parameters: r1 : double r2 : double Returns: double r1 : double r2 : double Returns: double  StaticRealEqu (r1, r2)  Full Usage: StaticRealEqu (r1, r2) Parameters: r1 : double r2 : double Returns: bool r1 : double r2 : double Returns: bool  StaticRealExp (r1, r2)  Full Usage: StaticRealExp (r1, r2) Parameters: r1 : float r2 : float Returns: float r1 : float r2 : float Returns: float  StaticRealLeq (r1, r2)  Full Usage: StaticRealLeq (r1, r2) Parameters: r1 : double r2 : double Returns: bool r1 : double r2 : double Returns: bool  StaticRealLes (r1, r2)  Full Usage: StaticRealLes (r1, r2) Parameters: r1 : double r2 : double Returns: bool r1 : double r2 : double Returns: bool  StaticRealLog2 r  Full Usage: StaticRealLog2 r Parameters: r : float Returns: float r : float Returns: float  StaticRealMul (r1, r2)  Full Usage: StaticRealMul (r1, r2) Parameters: r1 : double r2 : double Returns: double r1 : double r2 : double Returns: double  StaticRealOfInt bl  Full Usage: StaticRealOfInt bl Parameters: bl : bool list Returns: float bl : bool list Returns: float  StaticRealOfNat bl  Full Usage: StaticRealOfNat bl Parameters: bl : bool list Returns: float bl : bool list Returns: float  StaticRealSin r  Full Usage: StaticRealSin r Parameters: r : float Returns: float r : float Returns: float  StaticRealSub (r1, r2)  Full Usage: StaticRealSub (r1, r2) Parameters: r1 : double r2 : double Returns: double r1 : double r2 : double Returns: double  prnBtvBL bl  Full Usage: prnBtvBL bl Parameters: bl : bool list Returns: int -> Printer bl : bool list Returns: int -> Printer  prnIntBL bl  Full Usage: prnIntBL bl Parameters: bl : bool list Returns: int -> Printer bl : bool list Returns: int -> Printer  prnNatBL bl  Full Usage: prnNatBL bl Parameters: bl : bool list Returns: int -> Printer bl : bool list Returns: int -> Printer