text:
||| Primitive operations for fixed size, signed integers.
module Primitives.Int

import Primitives.Common
import Core.Context
import CairoCode.CairoCode
import Data.SortedSet
import Data.SortedMap
import CommonDef
import CodeGen.CodeGenHelper

---------------------------------------------------------------------------------------------------
-- UINT ADD
---------------------------------------------------------------------------------------------------
add_intX_name : Nat -> Name
add_intX_name nBits = makeBuiltinName "add_int\{show nBits}"

add_intX_code : Name -> Nat -> String
add_intX_code name nBits = """
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res
        local overflow
        %{
            raw_res = (ids.a + ids.b) % PRIME
            if (raw_res >= \{show halfShift}) & (raw_res < \{show shift}):
                (ids.overflow, ids.res) = (1, (raw_res - \{show shift}) % PRIME)
            elif (raw_res < PRIME - \{show halfShift}) & (PRIME - \{show shift} <= raw_res):
                (ids.overflow, ids.res) = (-1 % PRIME, (raw_res + \{show shift}) % PRIME)
            else:
                (ids.overflow, ids.res) = (0, raw_res)
        %}

        assert overflow * overflow * overflow = overflow  # overflow is -1, 0 or 1
        assert res = a + b - overflow * \{show shift}

        #inlined int_check
        assert [range_check_ptr] = res + \{show halfShift}			#Ensure: -HALF_SHIFT <= res
        assert [range_check_ptr+1] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT
        let range_check_ptr = range_check_ptr + 2

        return (res, range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

add_intX : Nat -> (Name, Lazy CairoDef)
add_intX nBits = (name, def)
  where name : Name
        name = add_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (add_intX_code name nBits)) 2 1

-- Implements
export
[add_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ ArgValue 0
    eval [ConstValue (I 0), _] = Just $ ArgValue 1
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (a+b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [add_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (add_intX_name 64) args]

export
[add_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 0), _] = Just $ ArgValue 1
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (a+b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [add_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (add_intX_name 8) args]

export
[add_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 0), _] = Just $ ArgValue 1
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (a+b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [add_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (add_intX_name 16) args]

export
[add_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 0), _] = Just $ ArgValue 1
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (a+b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [add_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (add_intX_name 32) args]

export
[add_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 0), _] = Just $ ArgValue 1
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (a+b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [add_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (add_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT SUB
---------------------------------------------------------------------------------------------------
sub_intX_name : Nat -> Name
sub_intX_name nBits = makeBuiltinName "sub_int\{show nBits}"

sub_intX_code : Name -> Nat -> String
sub_intX_code name nBits = """
    # Subtraction.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local overflow : felt
        %{
            a_sub_b = (ids.a - ids.b) % PRIME
            if (a_sub_b >= \{show halfShift}) & (a_sub_b < \{show shift}):
                (ids.overflow, ids.res) = (1, (a_sub_b - \{show shift}) % PRIME)
            elif (a_sub_b < PRIME - \{show halfShift}) & (PRIME - \{show shift} <= a_sub_b):
                (ids.overflow, ids.res) = (-1 % PRIME, (a_sub_b + \{show shift}) % PRIME)
            else:
                (ids.overflow, ids.res) = (0, a_sub_b)
        %}

        assert overflow * overflow * overflow = overflow  # overflow is -1, 0 or 1
        assert res = a - b - overflow * \{show shift}

        #inlined int_check
        assert [range_check_ptr] = res + \{show halfShift}			#Ensure: -HALF_SHIFT <= res
        assert [range_check_ptr+1] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT
        let range_check_ptr = range_check_ptr + 2

        return (res,range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

sub_intX : Nat -> (Name, Lazy CairoDef)
sub_intX nBits = (name, def)
  where name : Name
        name = sub_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (sub_intX_code name nBits)) 2 1

export
[sub_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ ArgValue 0
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (a-b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [sub_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (sub_intX_name 64) args]

export
[sub_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (a-b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [sub_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (sub_intX_name 8) args]

export
[sub_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (a-b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [sub_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (sub_intX_name 16) args]

export
[sub_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (a-b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [sub_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (sub_intX_name 32) args]

export
[sub_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (a-b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [sub_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (sub_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT MUL
---------------------------------------------------------------------------------------------------
mul_intX_name : Nat -> Name
mul_intX_name nBits = makeBuiltinName "mul_int\{show nBits}"

mul_intX_code : Name -> Nat -> String
mul_intX_code name nBits = """
    # Multiplies two int.
    # Returns the result as int.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res
        local offset
        %{
            from starkware.cairo.common.math_utils import as_int
            rawMult = ((as_int(ids.a, PRIME) * as_int(ids.b, PRIME)) + \{show halfShift})
            (rawOffset, resRaw) = divmod(rawMult, \{show shift})
            ids.offset = rawOffset % PRIME
            ids.res = (resRaw - \{show halfShift}) % PRIME
        %}

        # Check offset can not trigger overflow / underflow
        #  Note: Max valid offset absolute = HALF_SHIFT*HALF_SHIFT/SHIFT = (SHIFT*SHIFT)/4*SHIFT = SHIFT/4
        #  For simplicity we weaken to -HALF_SHIFT <= offset <= HALF_SHIFT then no overflow (for 64bit): -2**128 <= +/-(2**63 * 2**63) +/- (2**63 * 2**64) <= +2**128 & overflow is at ~+/-PRIME/2 (with PRIME ~= 2**192)
        assert [range_check_ptr] = offset + \{show halfShift}		#Ensure: -HALF_SHIFT <= offset
        assert [range_check_ptr+1] = \{show halfShift} - offset	    #Ensure: offset <= HALF_SHIFT

        assert res = a * b - offset * \{show shift}

        # inlined int_check(res)
        assert [range_check_ptr+2] = res + \{show halfShift}		#Ensure: -HALF_SHIFT <= res
        assert [range_check_ptr+3] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT
        let range_check_ptr = range_check_ptr + 4

        return (res, range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

mul_intX : Nat -> (Name, Lazy CairoDef)
mul_intX nBits = (name, def)
  where name : Name
        name = mul_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (mul_intX_code name nBits)) 2 1

export
[mul_int] PrimFn where
    eval [_, ConstValue (I 1)] = Just $ ArgValue 0
    eval [ConstValue (I 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (I 0)] = Just $ NewValue $ ConstValue $ I 0
    eval [ConstValue (I 0), _] = Just $ NewValue $ ConstValue $ I 0
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (a*b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mul_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (mul_intX_name 64) args]

export
[mul_int8] PrimFn where
    eval [_, ConstValue (I8 1)] = Just $ ArgValue 0
    eval [ConstValue (I8 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (I8 0)] = Just $ NewValue $ ConstValue $ I8 0
    eval [ConstValue (I8 0), _] = Just $ NewValue $ ConstValue $ I8 0
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (a*b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mul_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (mul_intX_name 8) args]

export
[mul_int16] PrimFn where
    eval [_, ConstValue (I16 1)] = Just $ ArgValue 0
    eval [ConstValue (I16 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (I16 0)] = Just $ NewValue $ ConstValue $ I16 0
    eval [ConstValue (I16 0), _] = Just $ NewValue $ ConstValue $ I16 0
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (a*b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mul_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (mul_intX_name 16) args]

export
[mul_int32] PrimFn where
    eval [_, ConstValue (I32 1)] = Just $ ArgValue 0
    eval [ConstValue (I32 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (I32 0)] = Just $ NewValue $ ConstValue $ I32 0
    eval [ConstValue (I32 0), _] = Just $ NewValue $ ConstValue $ I32 0
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (a*b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mul_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (mul_intX_name 32) args]

export
[mul_int64] PrimFn where
    eval [_, ConstValue (I64 1)] = Just $ ArgValue 0
    eval [ConstValue (I64 1), _] = Just $ ArgValue 1
    eval [_, ConstValue (I64 0)] = Just $ NewValue $ ConstValue $ I64 0
    eval [ConstValue (I64 0), _] = Just $ NewValue $ ConstValue $ I64 0
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (a*b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mul_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (mul_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT DIV
---------------------------------------------------------------------------------------------------
div_intX_name : Nat -> Name
div_intX_name nBits = makeBuiltinName "div_int\{show nBits}"

div_intX_code : Name -> Nat -> String
div_intX_code name nBits = """
    # Division between int.
    # Returns the quotient.
    # Conforms to Idris specifications: division by 0 yields error.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (quotient : felt, range_check_ptr):
        alloc_locals
        local res
        local rem
        local sign
        local signB
        %{
            from starkware.cairo.common.math_utils import as_int
            signB = 1 if as_int(ids.b, PRIME) >= 0 else -1
            sign = signB if as_int(ids.a, PRIME) >= 0 else -signB
            ids.signB = signB % PRIME
            ids.sign = sign % PRIME
            #Note fails if b = 0, which is ok as this is expected (Hint can not find a solution)
            # Question: is it ok to fail in hint or is a check with assert 0 =  1 needed
            (res, rem) = divmod(abs(as_int(ids.a,PRIME)), abs(as_int(ids.b,PRIME)))
            ids.res = res*sign % PRIME
            ids.rem = rem*sign % PRIME
        %}

        #check that the reverse is correct (this proofs correctnes if rem is valid)
        assert res * b + signB*rem = a

        #check the sign helpers are -1 or 1
        assert sign*sign = 1
        assert signB*signB = 1

        # check that rem & res have same sign & that the sign is correct
        assert [range_check_ptr] = sign*rem 				#rem is zero or has same sign as sign
        assert [range_check_ptr+1] = sign*res 				#res is zero or has same sign as sign

        #check that rem is between b and 0 (exclusive b, inclusive 0)
        # Note: if hint lies about signB then signB*b is negative and because sign*rem is proofen to be positive the rangecheck fails
        # Note: will fail if b = 0 which is the expected behaviour
        assert [range_check_ptr+2] = signB*b - sign*rem -1	# abs(rem) < abs(b)
        let range_check_ptr = range_check_ptr + 3

        # inlined int_check(res) -- implied as res must be between a and 0 to pass the checks & a is valid (input)
        # assert [range_check_ptr+3] = res + \{show halfShift}		#Ensure: -HALF_SHIFT <= res
        # assert [range_check_ptr+4] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT

        return (res, range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

div_intX : Nat -> (Name, Lazy CairoDef)
div_intX nBits = (name, def)
  where name : Name
        name = div_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (div_intX_code name nBits)) 2 1

export
[div_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (I 1)] = Just $ ArgValue 0
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (a `div` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [div_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (div_intX_name 64) args]

export
[div_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (I8 1)] = Just $ ArgValue 0
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (a `div` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [div_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (div_intX_name 8) args]

export
[div_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (I16 1)] = Just $ ArgValue 0
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (a `div` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [div_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (div_intX_name 16) args]

export
[div_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (I32 1)] = Just $ ArgValue 0
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (a `div` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [div_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (div_intX_name 32) args]

export
[div_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ Failure "Division by zero is not defined"
    eval [_, ConstValue (I64 1)] = Just $ ArgValue 0
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (a `div` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [div_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (div_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT MOD
---------------------------------------------------------------------------------------------------
mod_intX_name : Nat -> Name
mod_intX_name nBits = makeBuiltinName "mod_int\{show nBits}"

mod_intX_code : Name -> Nat -> String
mod_intX_code name nBits = """
    # Division between int.
    # Returns the remainder.
    # Conforms to Idris specifications: division by 0 yields error.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (remainder : felt, range_check_ptr):
        alloc_locals
        local res
        local rem
        local sign
        local signB
        %{
            from starkware.cairo.common.math_utils import as_int
            signB = 1 if as_int(ids.b, PRIME) >= 0 else -1
            sign = signB if as_int(ids.a, PRIME) >= 0 else -signB
            ids.signB = signB % PRIME
            ids.sign = sign % PRIME
            #Note fails if b = 0, which is ok as this is expected (Hint can not find a solution)
            # Question: is it ok to fail in hint or is a check with assert 0 =  1 needed
            (res, rem) = divmod(abs(as_int(ids.a,PRIME)), abs(as_int(ids.b,PRIME)))
            ids.res = res*sign % PRIME
            ids.rem = rem*sign % PRIME
        %}

        #check that the reverse is correct (this proofs correctnes if rem is valid)
        assert res * b + signB*rem = a

        #check the sign helpers are -1 or 1
        assert sign*sign = 1
        assert signB*signB = 1

        # check that rem & res have same sign & that the sign is correct
        assert [range_check_ptr] = sign*rem 				#rem is zero or has same sign as sign
        assert [range_check_ptr+1] = sign*res 				#res is zero or has same sign as sign

        #check that rem is between b and 0 (exclusive b, inclusive 0)
        # Note: if hint lies about signB then signB*b is negative and because sign*rem is proofen to be positive the rangecheck fails
        # Note: will fail if b = 0 which is the expected behaviour
        assert [range_check_ptr+2] = signB*b - sign*rem -1	# abs(rem) < abs(b)
        let range_check_ptr = range_check_ptr + 3

        # inlined int_check(res) -- implied as res must be between a and 0 to pass the checks & a is valid (input)
        # assert [range_check_ptr+3] = res + \{show halfShift}		#Ensure: -HALF_SHIFT <= res
        # assert [range_check_ptr+4] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT

        return (rem, range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

mod_intX : Nat -> (Name, Lazy CairoDef)
mod_intX nBits = (name, def)
  where name : Name
        name = mod_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (mod_intX_code name nBits)) 2 1

export
[mod_int] PrimFn where
    eval [_, ConstValue (I 1)] = Just $ NewValue $ ConstValue $ I 0
    eval [_, ConstValue (I 0)] = Just $ Failure "Division by zero is not defined"
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (a `mod` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mod_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (mod_intX_name 64) args]

export
[mod_int8] PrimFn where
    eval [_, ConstValue (I8 1)] = Just $ NewValue $ ConstValue $ I8 0
    eval [_, ConstValue (I8 0)] = Just $ Failure "Division by zero is not defined"
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (a `mod` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mod_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (mod_intX_name 8) args]

export
[mod_int16] PrimFn where
    eval [_, ConstValue (I16 1)] = Just $ NewValue $ ConstValue $ I16 0
    eval [_, ConstValue (I16 0)] = Just $ Failure "Division by zero is not defined"
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (a `mod` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mod_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (mod_intX_name 16) args]

export
[mod_int32] PrimFn where
    eval [_, ConstValue (I32 1)] = Just $ NewValue $ ConstValue $ I32 0
    eval [_, ConstValue (I32 0)] = Just $ Failure "Division by zero is not defined"
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (a `mod` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mod_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (mod_intX_name 32) args]

export
[mod_int64] PrimFn where
    eval [_, ConstValue (I64 1)] = Just $ NewValue $ ConstValue $ I64 0
    eval [_, ConstValue (I64 0)] = Just $ Failure "Division by zero is not defined"
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (a `mod` b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [mod_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (mod_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT NEG:
---------------------------------------------------------------------------------------------------
neg_intX_name : Nat -> Name
neg_intX_name nBits = makeBuiltinName "neg_int\{show nBits}"

neg_intX_code : Name -> Nat -> String
neg_intX_code name nBits = """
    # Note that int_neg(-HALF_SHIFT) = -HALF_SHIFT
    func \{cairoName name}(a : felt) -> (res):
        if a == -\{show halfShift}:
            return (a)
        else:
            return (-a)
        end
    end
"""
  where halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

neg_intX : Nat -> (Name, Lazy CairoDef)
neg_intX nBits = (name, def)
  where name : Name
        name = neg_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [] empty (neg_intX_code name nBits)) 1 1

export
[neg_int] PrimFn where
    eval [ConstValue (I a)] = Just $ NewValue $ ConstValue $ I (-a)
    eval _ = Nothing

    dependencies = fromList [neg_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (neg_intX_name 64) args]

export
[neg_int8] PrimFn where
    eval [ConstValue (I8 a)] = Just $ NewValue $ ConstValue $ I8 (-a)
    eval _ = Nothing

    dependencies = fromList [neg_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (neg_intX_name 8) args]

export
[neg_int16] PrimFn where
    eval [ConstValue (I16 a)] = Just $ NewValue $ ConstValue $ I16 (-a)
    eval _ = Nothing

    dependencies = fromList [neg_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (neg_intX_name 16) args]

export
[neg_int32] PrimFn where
    eval [ConstValue (I32 a)] = Just $ NewValue $ ConstValue $ I32 (-a)
    eval _ = Nothing

    dependencies = fromList [neg_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (neg_intX_name 16) args]

export
[neg_int64] PrimFn where
    eval [ConstValue (I64 a)] = Just $ NewValue $ ConstValue $ I64 (-a)
    eval _ = Nothing

    dependencies = fromList [neg_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (neg_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT SHL:
---------------------------------------------------------------------------------------------------
shl_intX_name : Nat -> Name
shl_intX_name nBits = makeBuiltinName "shl_int\{show nBits}"

shl_intX_code : Name -> Nat -> String
shl_intX_code name nBits = """
    ## Computes the logical left shift of an int.
    func \{cairoName name}(range_check_ptr, a, b) -> (res, range_check_ptr):
        # If b >= BIT_LENGTH - 1 , the result will be zero modulo 2**(BIT_LENGTH - 1).
        tempvar res
        %{ids.res = 1 if ids.b < \{show (nBits `minus` 1)} else 0 %}
        # b < 2**128 & a < 2**128 is given by semantics
        # b >= BIT_LENGTH - 1
        if res == 0:
            assert [range_check_ptr] = b - \{show (nBits `minus` 1)}
            let range_check_ptr = range_check_ptr + 1
            return (0, range_check_ptr)
        # b < BIT_LENGTH - 1
        else:
            assert [range_check_ptr] = \{show ((nBits `minus` 1) `minus` 1)} - b
            let range_check_ptr = range_check_ptr + 1
            let (c) = pow{range_check_ptr=range_check_ptr}(2, b)
            \{cairoName (mul_intX_name nBits)}(range_check_ptr, a, c)
            ret
        end
    end
"""

shl_intX : Nat -> (Name, Lazy CairoDef)
shl_intX nBits = (name, def)
  where name : Name
        name = shl_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (shl_intX_code name nBits)) 2 1

shl_intX_imports : SortedSet Import
shl_intX_imports = singleton (MkImport "starkware.cairo.common.pow" "pow")

export
[shl_int] PrimFn where
    apStable = False

    eval [_, ConstValue(I 0)] = Just $ ArgValue 0
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (prim__shl_Int a b)
    eval _ = Nothing

    imports = shl_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_intX 64, mul_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_intX_name 64) args]

export
[shl_int8] PrimFn where
    apStable = False

    eval [_, ConstValue(I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (prim__shl_Int8 (cast a) (cast b))
    eval _ = Nothing

    imports = shl_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_intX 8, mul_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_intX_name 8) args]

export
[shl_int16] PrimFn where
    apStable = False

    eval [_, ConstValue(I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (prim__shl_Int16 (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shl_int16"

export
[shl_int32] PrimFn where
    apStable = False

    eval [_, ConstValue(I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (prim__shl_Int32 (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shl_int32"

export
[shl_int64] PrimFn where
    apStable = False

    eval [_, ConstValue(I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (prim__shl_Int64 (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shl_int64"

---------------------------------------------------------------------------------------------------
-- INT SHR:
---------------------------------------------------------------------------------------------------
shr_intX_name : Nat -> Name
shr_intX_name nBits = makeBuiltinName "shr_int\{show nBits}"

shr_intX_code : Name -> Nat -> String
shr_intX_code name nBits = """
    # Computes the logical right shift of an int.
    func \{cairoName name}(range_check_ptr, a : felt,  b : felt) -> (res : felt, range_check_ptr):
        #inlined int_pow2
        # If a >= BIT_LENGTH - 1, the result will be zero modulo 2**(BIT_LENGTH-1).
        tempvar res
        %{ids.res = 1 if ids.b < \{show (nBits `minus` 1)} else 0 %}
        # b < 2**128 & a < 2**128 is given by semantics
        # BIT_LENGTH <= b
        if res == 0:
            assert [range_check_ptr] = b - \{show (nBits `minus` 1)}
            let range_check_ptr = range_check_ptr + 1
            return (0, range_check_ptr)
        #b < BIT_LENGTH
        else:
            assert [range_check_ptr] = \{show ((nBits `minus` 1) `minus` 1)} - b
            let range_check_ptr = range_check_ptr + 1
            let (c) = pow{range_check_ptr=range_check_ptr}(2, b)
            \{cairoName (div_intX_name nBits)}(range_check_ptr, a, c)
            ret
        end
    end
"""

shr_intX : Nat -> (Name, Lazy CairoDef)
shr_intX nBits = (name, def)
  where name : Name
        name = shr_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (shr_intX_code name nBits)) 2 1

shr_intX_imports : SortedSet Import
shr_intX_imports = singleton (MkImport "starkware.cairo.common.pow" "pow")

export
[shr_int] PrimFn where
    apStable = False

    eval [_, ConstValue(I 0)] = Just $ ArgValue 0
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (prim__shr_Int a b)
    eval _ = Nothing

    imports = shr_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_intX 64, div_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_intX_name 64) args]

export
[shr_int8] PrimFn where
    apStable = False

    eval [_, ConstValue(I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (prim__shr_Int8 (cast a) (cast b))
    eval _ = Nothing

    imports = shr_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_intX 8, div_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_intX_name 8) args]

export
[shr_int16] PrimFn where
    apStable = False

    eval [_, ConstValue(I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (prim__shr_Int16 (cast a) (cast b))
    eval _ = Nothing

    imports = shr_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_intX 16, div_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_intX_name 16) args]

export
[shr_int32] PrimFn where
    apStable = False

    eval [_, ConstValue(I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (prim__shr_Int32 (cast a) (cast b))
    eval _ = Nothing

    imports = shr_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_intX 32, div_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_intX_name 32) args]

export
[shr_int64] PrimFn where
    apStable = False

    eval [_, ConstValue(I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (prim__shr_Int64 (cast a) (cast b))
    eval _ = Nothing

    imports = shr_intX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_intX 64, div_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT AND:
---------------------------------------------------------------------------------------------------
and_intX_name : Nat -> Name
and_intX_name nBits = makeBuiltinName "and_int\{show nBits}"

and_intX_code : Name -> Nat -> String
and_intX_code name nBits = """
    func \{cairoName name}(range_check_ptr, bitwise_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr, bitwise_ptr):
        alloc_locals
        local signA
        local signB
        %{
            from starkware.cairo.common.math_utils import as_int
            ids.signA = 1 if as_int(ids.a, PRIME) >= 0 else (-1 % PRIME)
            ids.signB = 1 if as_int(ids.b, PRIME) >= 0 else (-1 % PRIME)
        %}

        assert signA*signA = 1
        assert signB*signB = 1

        assert [range_check_ptr] = signA*a
        assert [range_check_ptr+1] = signB*b

        let a_offset = a - (signA - 1)*\{show halfShift} 	#from: ((signA - 1)/2)*SHIFT | ((signA - 1)/2) = -(signA == -1)
        let b_offset = b - (signB - 1)*\{show halfShift} 	#from: ((signB - 1)/2)*SHIFT | ((signB - 1)/2) = -(signB == -1)

        # inlined bitwise_and
        assert [bitwise_ptr] = a_offset
        assert [bitwise_ptr+1] = b_offset
        local res_value = [bitwise_ptr+2]
        let bitwise_ptr = bitwise_ptr + BitwiseBuiltin.SIZE

        # If the result is HALF_SHIFT or greater, this indicates a twos complement negative value
        # See int_le for explanation: note res_value < 2**127 (because max 64bits)
        local must_shift
        %{ids.must_shift = 1 if \{show halfShift} <= ids.res_value else 0 %}
        if must_shift == 0:
            assert [range_check_ptr+2] = \{show (halfShift - 1)} - res_value
            let range_check_ptr = range_check_ptr + 3
            return (res_value, range_check_ptr, bitwise_ptr )
        else:
            assert [range_check_ptr+2] = res_value - \{show halfShift}
            let range_check_ptr = range_check_ptr + 3
            return (res_value - \{show shift}, range_check_ptr, bitwise_ptr)
        end
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

and_intX : Nat -> (Name, Lazy CairoDef)
and_intX nBits = (name, def)
  where name : Name
        name = and_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin, bitwise_builtin] empty (and_intX_code name nBits)) 2 1

export
[and_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ NewValue $ ConstValue $ I 0
    eval [ConstValue (I 0), _] = Just $ NewValue $ ConstValue $ I 0
    eval [_, ConstValue (I (-1))] = Just $ ArgValue 0
    eval [ConstValue (I (-1)), _] = Just $ ArgValue 1
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (prim__and_Int a b)
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [and_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (and_intX_name 64) args]

export
[and_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ NewValue $ ConstValue $ I8 0
    eval [ConstValue (I8 0), _] = Just $ NewValue $ ConstValue $ I8 0
    eval [_, ConstValue (I8 (-1))] = Just $ ArgValue 0
    eval [ConstValue (I8 (-1)), _] = Just $ ArgValue 1
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (prim__and_Int8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [and_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (and_intX_name 8) args]

export
[and_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ NewValue $ ConstValue $ I16 0
    eval [ConstValue (I16 0), _] = Just $ NewValue $ ConstValue $ I16 0
    eval [_, ConstValue (I16 (-1))] = Just $ ArgValue 0
    eval [ConstValue (I16 (-1)), _] = Just $ ArgValue 1
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (prim__and_Int16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [and_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (and_intX_name 16) args]

export
[and_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ NewValue $ ConstValue $ I32 0
    eval [ConstValue (I32 0), _] = Just $ NewValue $ ConstValue $ I32 0
    eval [_, ConstValue (I32 (-1))] = Just $ ArgValue 0
    eval [ConstValue (I32 (-1)), _] = Just $ ArgValue 1
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (prim__and_Int32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [and_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (and_intX_name 32) args]

export
[and_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ NewValue $ ConstValue $ I64 0
    eval [ConstValue (I64 0), _] = Just $ NewValue $ ConstValue $ I64 0
    eval [_, ConstValue (I64 (-1))] = Just $ ArgValue 0
    eval [ConstValue (I64 (-1)), _] = Just $ ArgValue 1
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (prim__and_Int64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [and_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (and_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT OR:
---------------------------------------------------------------------------------------------------
or_intX_name : Nat -> Name
or_intX_name nBits = makeBuiltinName "or_int\{show nBits}"

or_intX_code : Name -> Nat -> String
or_intX_code name nBits = """
    func \{cairoName name}(range_check_ptr, bitwise_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr, bitwise_ptr):
        alloc_locals
        local signA
        local signB
        %{
            from starkware.cairo.common.math_utils import as_int
            ids.signA = 1 if as_int(ids.a, PRIME) >= 0 else (-1 % PRIME)
            ids.signB = 1 if as_int(ids.b, PRIME) >= 0 else (-1 % PRIME)
        %}

        assert signA*signA = 1
        assert signB*signB = 1

        assert [range_check_ptr] = signA*a
        assert [range_check_ptr+1] = signB*b

        let a_offset = a - (signA - 1)*\{show halfShift} 	#from: ((signA - 1)/2)*SHIFT | ((signA - 1)/2) = -(signA == -1)
        let b_offset = b - (signB - 1)*\{show halfShift} 	#from: ((signB - 1)/2)*SHIFT | ((signB - 1)/2) = -(signB == -1)

        # inlined bitwise_or
        assert [bitwise_ptr] = a_offset
        assert [bitwise_ptr+1] = b_offset
        local res_value = [bitwise_ptr+4]
        let bitwise_ptr = bitwise_ptr + BitwiseBuiltin.SIZE

        # If the result is HALF_SHIFT or greater, this indicates a twos complement negative value
        # See int_le for explanation: note res_value < 2**127 (because max 64bits)
        local must_shift
        %{ids.must_shift = 1 if \{show halfShift} <= ids.res_value else 0 %}
        if must_shift == 0:
            assert [range_check_ptr+2] = \{show (halfShift - 1)} - res_value # DK: check - is left associative
            let range_check_ptr = range_check_ptr + 3
            return (res_value, range_check_ptr, bitwise_ptr )
        else:
            assert [range_check_ptr+2] = res_value - \{show halfShift}		#-0 is for ap stability improves worse case in code gen
            let range_check_ptr = range_check_ptr + 3
            return (res_value - \{show shift}, range_check_ptr, bitwise_ptr)
        end
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

or_intX : Nat -> (Name, Lazy CairoDef)
or_intX nBits = (name, def)
  where name : Name
        name = or_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin, bitwise_builtin] empty (or_intX_code name nBits)) 2 1

export
[or_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ ArgValue 0
    eval [ConstValue (I 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (I  (-1))] = Just $ NewValue $ ConstValue $ I (-1)
    eval [ConstValue (I  (-1)), _] = Just $ NewValue $ ConstValue $ I (-1)
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (prim__or_Int a b)
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [or_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (or_intX_name 64) args]

export
[or_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (I8 (-1))] = Just $ NewValue $ ConstValue $ I8 (-1)
    eval [ConstValue (I8 (-1)), _] = Just $ NewValue $ ConstValue $ I8 (-1)
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (prim__or_Int8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [or_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (or_intX_name 8) args]

export
[or_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (I16 (-1))] = Just $ NewValue $ ConstValue $ I16 (-1)
    eval [ConstValue (I16 (-1)), _] = Just $ NewValue $ ConstValue $ I16 (-1)
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (prim__or_Int16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [or_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (or_intX_name 16) args]

export
[or_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (I32 (-1))] = Just $ NewValue $ ConstValue $ I32 (-1)
    eval [ConstValue (I32 (-1)), _] = Just $ NewValue $ ConstValue $ I32 (-1)
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (prim__or_Int32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [or_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (or_intX_name 32) args]

export
[or_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (I64 (-1))] = Just $ NewValue $ ConstValue $ I64 (-1)
    eval [ConstValue (I64 (-1)), _] = Just $ NewValue $ ConstValue $ I64 (-1)
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (prim__or_Int64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [or_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (or_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT XOR:
---------------------------------------------------------------------------------------------------
xor_intX_name : Nat -> Name
xor_intX_name nBits = makeBuiltinName "xor_int\{show nBits}"

xor_intX_code : Name -> Nat -> String
xor_intX_code name nBits = """
    func \{cairoName name}(range_check_ptr, bitwise_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr, bitwise_ptr):
        alloc_locals
        let a_offset = a + \{show halfShift}  # guarantee positive number, since minimum input value is DEFAULT_PRIME - SHIFT.  e.g. 0 maps to 128, 127 maps to 255, and -1 maps to 127.  This gets applied to _both_ inputs, so intuitively, XOR doesn't notice or care.
        let b_offset = b + \{show halfShift}

        # inlined bitwise_xor
        assert [bitwise_ptr] = a_offset
        assert [bitwise_ptr+1] = b_offset
        local res_value = [bitwise_ptr+3]
        let bitwise_ptr = bitwise_ptr + BitwiseBuiltin.SIZE

        # If the result is HALF_SHIFT of greater, this indicates a twos complement negative value
        # See int_le for explanation: note res_value < 2**127 (because max 64bits)
        local must_shift
        %{ids.must_shift = 1 if \{show halfShift} <= ids.res_value else 0 %}
        if must_shift == 0:
            assert [range_check_ptr] = \{show (halfShift-1)} - res_value
            let range_check_ptr = range_check_ptr + 1
            return (res_value, range_check_ptr, bitwise_ptr)
        else:
            assert [range_check_ptr] = res_value - \{show halfShift}
            let range_check_ptr = range_check_ptr + 1
            return (res_value - \{show shift}, range_check_ptr, bitwise_ptr)
        end
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

xor_intX : Nat -> (Name, Lazy CairoDef)
xor_intX nBits = (name, def)
  where name : Name
        name = xor_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin, bitwise_builtin] empty (xor_intX_code name nBits)) 2 1

export
[xor_int] PrimFn where
    eval [_, ConstValue (I 0)] = Just $ ArgValue 0
    eval [ConstValue (I 0), _] = Just $ ArgValue 1
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ I (prim__xor_Int a b)
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [xor_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (xor_intX_name 64) args]

export
[xor_int8] PrimFn where
    eval [_, ConstValue (I8 0)] = Just $ ArgValue 0
    eval [ConstValue (I8 0), _] = Just $ ArgValue 1
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ I8 (prim__xor_Int8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [xor_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (xor_intX_name 8) args]

export
[xor_int16] PrimFn where
    eval [_, ConstValue (I16 0)] = Just $ ArgValue 0
    eval [ConstValue (I16 0), _] = Just $ ArgValue 1
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ I16 (prim__xor_Int16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [xor_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (xor_intX_name 16) args]

export
[xor_int32] PrimFn where
    eval [_, ConstValue (I32 0)] = Just $ ArgValue 0
    eval [ConstValue (I32 0), _] = Just $ ArgValue 1
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ I32 (prim__xor_Int32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [xor_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (xor_intX_name 32) args]

export
[xor_int64] PrimFn where
    eval [_, ConstValue (I64 0)] = Just $ ArgValue 0
    eval [ConstValue (I64 0), _] = Just $ ArgValue 1
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ I64 (prim__xor_Int64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = fromList [range_check_builtin, bitwise_builtin]
    dependencies = fromList [xor_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (xor_intX_name 64) args]

---------------------------------------------------------------------------------------------------
-- INT LT
---------------------------------------------------------------------------------------------------
lt_intX_name : Name
lt_intX_name = makeBuiltinName "lt_int"

lt_intX_code : Name -> String
lt_intX_code name = """
    # Returns 1 if the first integer is less than the second, otherwise returns 0.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res, range_check_ptr):
        tempvar res
        %{
            from starkware.cairo.common.math_utils import as_int
            ids.res = 1 if as_int(ids.a,PRIME) < as_int(ids.b,PRIME) else 0
        %}
        # -2**127 <= b < 2**127 & -2**127 <= a < 2**127 is given by semantics (actuall even tighter as max 64bits)
        # implies: a - b < 2**128 & b - a < 2**128 (meaning in range check upper bound)
        # b <= a
        if res == 0:
            assert [range_check_ptr] = a - b - 0 #+0 is for ap stability improves worse case in code gen
            let range_check_ptr = range_check_ptr + 1
            return (0, range_check_ptr)
        # a < b
        else:
            assert [range_check_ptr] = b - a - 1
            let range_check_ptr = range_check_ptr + 1
            return (1, range_check_ptr)
        end
    end
"""

lt_intX : (Name, Lazy CairoDef)
lt_intX = (lt_intX_name, def)
  where def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (lt_intX_code lt_intX_name)) 2 1

generateLtCallCode : CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
generateLtCallCode res args implicits = Instructions [CALL [res] implicits lt_intX_name args]

export
[lt_int] PrimFn where
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateLtCallCode

export
[lt_int8] PrimFn where
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateLtCallCode

export
[lt_int16] PrimFn where
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateLtCallCode

export
[lt_int32] PrimFn where
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateLtCallCode

export
[lt_int64] PrimFn where
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ toInt (a<b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateLtCallCode

---------------------------------------------------------------------------------------------------
-- INT LTE
---------------------------------------------------------------------------------------------------
lte_intX_name : Name
lte_intX_name = makeBuiltinName "lte_int"

lte_intX_code : Name -> String
lte_intX_code name = """
    # Returns 1 if the first integer is less than the second, otherwise returns 0.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res, range_check_ptr):
        tempvar res
        %{
            from starkware.cairo.common.math_utils import as_int
            ids.res = 1 if as_int(ids.a,PRIME) < as_int(ids.b,PRIME) else 0
        %}
        # -2**127 <= b < 2**127 & -2**127 <= a < 2**127 is given by semantics (actuall even tighter as max 64bits)
        # implies: a - b < 2**128 & b - a < 2**128 (meaning in range check upper bound)
        # b <= a
        if res == 0:
            assert [range_check_ptr] = a - b - 0 #+0 is for ap stability improves worse case in code gen
            let range_check_ptr = range_check_ptr + 1
            return (0, range_check_ptr)
        # a < b
        else:
            assert [range_check_ptr] = b - a - 1
            let range_check_ptr = range_check_ptr + 1
            return (1, range_check_ptr)
        end
    end
"""

lte_intX : (Name, Lazy CairoDef)
lte_intX = (lte_intX_name, def)
  where def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (lte_intX_code lte_intX_name)) 2 1

generateLteCallCode : CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
generateLteCallCode res args implicits = Instructions [CALL [res] implicits lte_intX_name args]

export
[lte_int] PrimFn where
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateLtCallCode

export
[lte_int8] PrimFn where
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateLtCallCode

export
[lte_int16] PrimFn where
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateLtCallCode

export
[lte_int32] PrimFn where
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateLtCallCode

export
[lte_int64] PrimFn where
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ toInt (a<=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateLtCallCode

---------------------------------------------------------------------------------------------------
-- INT EQ
---------------------------------------------------------------------------------------------------
export
[eq_int] PrimFn where
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_int" r a i

export
[eq_int8] PrimFn where
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_int8" r a i

export
[eq_int16] PrimFn where
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_int16" r a i

export
[eq_int32] PrimFn where
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_int32" r a i

export
[eq_int64] PrimFn where
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

    generateCode r a i = Raw $ compileEqOp "eq_int64" r a i

---------------------------------------------------------------------------------------------------
-- INT GTE
-- Implementation uses flipped arguments to lte
---------------------------------------------------------------------------------------------------

generateGteCallCode : CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
generateGteCallCode res [a,b] implicits = Instructions [CALL [res] implicits lte_intX_name [b,a]] -- Flipped arguments
generateGteCallCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode gte_intX"

export
[gte_int] PrimFn where
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateGteCallCode

export
[gte_int8] PrimFn where
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateGteCallCode

export
[gte_int16] PrimFn where
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateGteCallCode

export
[gte_int32] PrimFn where
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateGteCallCode

export
[gte_int64] PrimFn where
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ toInt (a>=b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_intX]
    generateCode = generateGteCallCode

---------------------------------------------------------------------------------------------------
-- INT GT
-- Implementation uses flipped arguments to lte
---------------------------------------------------------------------------------------------------

generateGtCallCode : CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
generateGtCallCode res [a,b] implicits = Instructions [CALL [res] implicits lt_intX_name [b,a]] -- Flipped arguments
generateGtCallCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode gt_intX"

export
[gt_int] PrimFn where
    eval [ConstValue (I a), ConstValue (I b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateGtCallCode

export
[gt_int8] PrimFn where
    eval [ConstValue (I8 a), ConstValue (I8 b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateGtCallCode

export
[gt_int16] PrimFn where
    eval [ConstValue (I16 a), ConstValue (I16 b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateGtCallCode

export
[gt_int32] PrimFn where
    eval [ConstValue (I32 a), ConstValue (I32 b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateGtCallCode

export
[gt_int64] PrimFn where
    eval [ConstValue (I64 a), ConstValue (I64 b)] = Just $ NewValue $ ConstValue $ toInt (a>b)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [lt_intX]
    generateCode = generateGtCallCode

---------------------------------------------------------------------------------------------------
-- INT CASTS
---------------------------------------------------------------------------------------------------
cast_intX_name : Nat -> Name
cast_intX_name nBits = makeBuiltinName "cast_int\{show nBits}"

cast_intX_code : Name -> Nat -> String
cast_intX_code name nBits = """
    # Casts to int\{show nBits}
    # Returns the result as int\{show nBits}.
    func \{cairoName name}(range_check_ptr, a : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res
        local offset
        %{
            from starkware.cairo.common.math_utils import as_int
            rawRes = (as_int(ids.a, PRIME) + \{show halfShift})
            (rawOffset, resRaw) = divmod(rawRes, \{show shift})
            ids.offset = rawOffset % PRIME
            ids.res = (rawRes - \{show halfShift}) % PRIME
        %}

        # Check offset can not trigger overflow / underflow
        #  Note: Max valid offset absolute = HALF_SHIFT*HALF_SHIFT/SHIFT = (SHIFT*SHIFT)/4*SHIFT = SHIFT/4
        #  For simplicity we weaken to -HALF_SHIFT <= offset <= HALF_SHIFT then no overflow (for 64bit): -2**128 <= +/-(2**63 * 2**63) +/- (2**63 * 2**64) <= +2**128 & overflow is at ~+/-PRIME/2 (with PRIME ~= 2**192)
        assert [range_check_ptr] = offset + \{show halfShift}		#Ensure: -HALF_SHIFT <= offset
        assert [range_check_ptr+1] = \{show halfShift} - offset	    #Ensure: offset <= HALF_SHIFT

        assert res = a - offset * \{show shift}

        # inlined int_check(res)
        assert [range_check_ptr+2] = res + \{show halfShift}		#Ensure: -HALF_SHIFT <= res
        assert [range_check_ptr+3] = \{show (halfShift - 1)} - res	#Ensure: res < HALF_SHIFT
        let range_check_ptr = range_check_ptr + 4

        return (res, range_check_ptr)
    end

"""
  where shift : Integer
        shift = pow2 nBits
        halfShift : Integer
        halfShift = pow2 (nBits `minus` 1)

cast_intX : Nat -> (Name, Lazy CairoDef)
cast_intX nBits = (name, def)
  where name : Name
        name = cast_intX_name nBits
        def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (cast_intX_code name nBits)) 1 1

export
[cast_to_int] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ I $ cast i) (constToInteger c)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_intX_name 64) args]

export
[cast_to_int8] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ I8 $ cast i) (constToInteger c)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_intX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_intX_name 8) args]

export
[cast_to_int16] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ I16 $ cast i) (constToInteger c)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_intX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_intX_name 16) args]

export
[cast_to_int32] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ I32 $ cast i) (constToInteger c)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_intX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_intX_name 32) args]

export
[cast_to_int64] PrimFn where
    eval [ConstValue c] = map (\i => NewValue $ ConstValue $ I64 $ cast i) (constToInteger c)
    eval _ = Nothing

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_intX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_intX_name 64) args]

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
/** ============================================================================
 *   \file  soc_AM33XX.h
 *
 *   \brief This file contains the peripheral information for AM33XX SoC
 *
 *  ============================================================================

/*
* Copyright (C) 2010 Texas Instruments Incorporated - http://www.ti.com/

/*
*  Redistribution and use in source and binary forms, with or without
*  modification, are permitted provided that the following conditions
*  are met:
*
*    Redistributions of source code must retain the above copyright
*    notice, this list of conditions and the following disclaimer.
*
*    Redistributions in binary form must reproduce the above copyright
*    notice, this list of conditions and the following disclaimer in the
*    documentation and/or other materials provided with the
*    distribution.
*
*    Neither the name of Texas Instruments Incorporated nor the names of
*    its contributors may be used to endorse or promote products derived
*    from this software without specific prior written permission.
*
*  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
*  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
*  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
*  A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
*  OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
*  DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
*  THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
*  (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
*  OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*

SocAm33xxH_ : Int
SocAm33xxH_ =

extern "C" {

/** Cache Line size in ARM Cortex-A8.
socCachelineSizeMax : Int
socCachelineSizeMax =
    (64)

-- Base address of AINTC memory mapped registers
socAintcRegs : Int
socAintcRegs =
    (0x48200000)

-- Base addresses of UART memory mapped registers
socUart0Regs : Int
socUart0Regs =
    (0x44e09000)
socUart1Regs : Int
socUart1Regs =
    (0x48022000)
socUart2Regs : Int
socUart2Regs =
    (0x48024000)
socUart3Regs : Int
socUart3Regs =
    (0x481a6000)
socUart4Regs : Int
socUart4Regs =
    (0x481a8000)
socUart5Regs : Int
socUart5Regs =
    (0x481aa000)

-- Base addresses of USB memory mapped registers
socUsb0Base : Int
socUsb0Base =
    (0x47401400)
socUsb1Base : Int
socUsb1Base =
    (0x47401c00)
-- Base addresses of SPI memory mapped registers
socSpi0Regs : Int
socSpi0Regs =
    (0x48030000)
socSpi1Regs : Int
socSpi1Regs =
    (0x481a0000)

-- Base addresses of GPIO memory mapped registers
socGpio0Regs : Int
socGpio0Regs =
    (0x44e07000)
socGpio1Regs : Int
socGpio1Regs =
    (0x4804c000)
socGpio2Regs : Int
socGpio2Regs =
    (0x481ac000)
socGpio3Regs : Int
socGpio3Regs =
    (0x481ae000)

-- Base addresses of DMTIMER memory mapped registers
socDmtimer0Regs : Int
socDmtimer0Regs =
    (0x44e05000)
socDmtimer1Regs : Int
socDmtimer1Regs =
    (0x44e31000)
socDmtimer2Regs : Int
socDmtimer2Regs =
    (0x48040000)
socDmtimer3Regs : Int
socDmtimer3Regs =
    (0x48042000)
socDmtimer4Regs : Int
socDmtimer4Regs =
    (0x48044000)
socDmtimer5Regs : Int
socDmtimer5Regs =
    (0x48046000)
socDmtimer6Regs : Int
socDmtimer6Regs =
    (0x48048000)
socDmtimer7Regs : Int
socDmtimer7Regs =
    (0x4804a000)

-- Base address of MMC memory mapped registers
socMmchs0Regs : Int
socMmchs0Regs =
    (0x48060000)
socMmchs1Regs : Int
socMmchs1Regs =
    (0x481d8000)
socMmchs2Regs : Int
socMmchs2Regs =
    (0x47810000)

-- Base address of GPMC memory mapped registers
socGpmc0Regs : Int
socGpmc0Regs =
    (0x50000000)

-- Base address of GPMC memory mapped registers
socElm0Regs : Int
socElm0Regs =
    (0x48080000)

-- Base address of I2C memory mapped registers
socI2c0Regs : Int
socI2c0Regs =
    (0x44e0b000)
socI2c1Regs : Int
socI2c1Regs =
    (0x4802a000)
socI2c2Regs : Int
socI2c2Regs =
    (0x4819c000)

-- Base address of WDT memory mapped registers
socWdt0Regs : Int
socWdt0Regs =
    (0x44e33000)
socWdt1Regs : Int
socWdt1Regs =
    (0x44e35000)

-- Base address of WDT memory mapped registers
socCpswSsRegs : Int
socCpswSsRegs =
    (0x4a100000)
socCpswMdioRegs : Int
socCpswMdioRegs =
    (0x4a101000)
socCpswWrRegs : Int
socCpswWrRegs =
    (0x4a101200)
socCpswCpdmaRegs : Int
socCpswCpdmaRegs =
    (0x4a100800)
socCpswAleRegs : Int
socCpswAleRegs =
    (0x4a100d00)
socCpswStatRegs : Int
socCpswStatRegs =
    (0x4a100900)
socCpswPort0Regs : Int
socCpswPort0Regs =
    (0x4a100100)
socCpswPort1Regs : Int
socCpswPort1Regs =
    (0x4a100200)
socCpswSliver1Regs : Int
socCpswSliver1Regs =
    (0x4a100d80)
socCpswPort2Regs : Int
socCpswPort2Regs =
    (0x4a100300)
socCpswSliver2Regs : Int
socCpswSliver2Regs =
    (0x4a100dc0)
socCpswCppiRamRegs : Int
socCpswCppiRamRegs =
    (0x4a102000)

-- Base address of McASP memory mapped registers
socMcasp0CtrlRegs : Int
socMcasp0CtrlRegs =
    (0x48038000)
socMcasp0FifoRegs : Int
socMcasp0FifoRegs =
    (socMcasp0CtrlRegs + 0x1000)
socMcasp0DataRegs : Int
socMcasp0DataRegs =
    (0x46000000)
socMcasp1CtrlRegs : Int
socMcasp1CtrlRegs =
    (0x4803c000)
socMcasp1FifoRegs : Int
socMcasp1FifoRegs =
    (socMcasp1CtrlRegs + 0x1000)
socMcasp1DataRegs : Int
socMcasp1DataRegs =
    (0x46400000)

-- Base address of EMIF memory mapped registers
socEmif0Regs : Int
socEmif0Regs =
    (0x4c000000)

-- Base addresses of RTC memory mapped registers
socRtc0Regs : Int
socRtc0Regs =
    (0x44e3e000)

-- Base addresses of PRCM memory mapped registers
socPrcmRegs : Int
socPrcmRegs =
    (0x44e00000)
socCmPerRegs : Int
socCmPerRegs =
    (socPrcmRegs + 0)
socCmWkupRegs : Int
socCmWkupRegs =
    (socPrcmRegs + 0x400)
socCmDpllRegs : Int
socCmDpllRegs =
    (socPrcmRegs + 0x500)
socCmMpuRegs : Int
socCmMpuRegs =
    (socPrcmRegs + 0x600)
socCmDeviceRegs : Int
socCmDeviceRegs =
    (socPrcmRegs + 0x700)
socCmRtcRegs : Int
socCmRtcRegs =
    (socPrcmRegs + 0x800)
socCmGfxRegs : Int
socCmGfxRegs =
    (socPrcmRegs + 0x900)
socCmCefuseRegs : Int
socCmCefuseRegs =
    (socPrcmRegs + 0xa00)
socOcpSocketRamRegs : Int
socOcpSocketRamRegs =
    (socPrcmRegs + 0xb00)
socPrmPerRegs : Int
socPrmPerRegs =
    (socPrcmRegs + 0xc00)
socPrmWkupRegs : Int
socPrmWkupRegs =
    (socPrcmRegs + 0xd00)
socPrmMpuRegs : Int
socPrmMpuRegs =
    (socPrcmRegs + 0xe00)
socPrmDeviceRegs : Int
socPrmDeviceRegs =
    (socPrcmRegs + 0xf00)
socPrmRtcRegs : Int
socPrmRtcRegs =
    (socPrcmRegs + 0x1000)
socPrmGfxRegs : Int
socPrmGfxRegs =
    (socPrcmRegs + 0x1100)
socPrmCefuseRegs : Int
socPrmCefuseRegs =
    (socPrcmRegs + 0x1200)

-- Base address of control module memory mapped registers
socControlRegs : Int
socControlRegs =
    (0x44e10000)

-- Base address of Channel controller  memory mapped registers
socEdma30cc0Regs : Int
socEdma30cc0Regs =
    (0x49000000)

-- Base address of DCAN module memory mapped registers
socDcan0Regs : Int
socDcan0Regs =
    (0x481cc000)
socDcan1Regs : Int
socDcan1Regs =
    (0x481d0000)

/******************************************************************************\
*  Parameterizable Configuration:- These are fed directly from the RTL
*  parameters for the given SOC
\*****************************************************************************
tpccMux(n) : Int
tpccMux(n) =
    0xf90 + ((n) * 4)

socLcdc0Regs : Int
socLcdc0Regs =
    0x4830e000

socAdcTsc0Regs : Int
socAdcTsc0Regs =
    0x44e0d000

-- Base addresses of PWMSS memory mapped registers.

socPwmss0Regs : Int
socPwmss0Regs =
    (0x48300000)
socPwmss1Regs : Int
socPwmss1Regs =
    (0x48302000)
socPwmss2Regs : Int
socPwmss2Regs =
    (0x48304000)

socEcapRegs : Int
socEcapRegs =
    (0x00000100)
socEqepRegs : Int
socEqepRegs =
    (0x00000180)
socEpwmRegs : Int
socEpwmRegs =
    (0x00000200)

socEcap0Regs : Int
socEcap0Regs =
    (socPwmss0Regs + socEcapRegs)
socEcap1Regs : Int
socEcap1Regs =
    (socPwmss1Regs + socEcapRegs)
socEcap2Regs : Int
socEcap2Regs =
    (socPwmss2Regs + socEcapRegs)

socEqep0Regs : Int
socEqep0Regs =
    (socPwmss0Regs + socEqepRegs)
socEqep1Regs : Int
socEqep1Regs =
    (socPwmss1Regs + socEqepRegs)
socEqep2Regs : Int
socEqep2Regs =
    (socPwmss2Regs + socEqepRegs)

socEpwm0Regs : Int
socEpwm0Regs =
    (socPwmss0Regs + socEpwmRegs)
socEpwm1Regs : Int
socEpwm1Regs =
    (socPwmss1Regs + socEpwmRegs)
socEpwm2Regs : Int
socEpwm2Regs =
    (socPwmss2Regs + socEpwmRegs)

socEpwmModuleFreq : Int
socEpwmModuleFreq =
    100

ext: idr

max_stars_repo_name: mokshasoft/bare-metal-idris-core

max_issues_repo_name: mokshasoft/bare-metal-idris-core

max_forks_repo_name: mokshasoft/bare-metal-idris-core


text:
module Main

import Data.Strings

%default total

-- the definitions are in calc.scm, run the program as:
-- $ idris2 -o Chez --directive extranRuntime=calc.scm ChezGenerator.idr

%foreign "scheme:my-add"
myAdd : Int -> Int -> Int

%foreign "scheme:my-sub"
mySub : Int -> Int -> Int

%foreign "scheme:my-mul"
myMul : Int -> Int -> Int

%foreign "scheme:my-div"
myDiv : Int -> Int -> Int

readNum : HasIO io => io (Maybe Int)
readNum = do input <- getLine
             case all isDigit (unpack input) of
                  False => pure Nothing
                  True => pure $ Just (cast input)

main : HasIO io => io ()
main = do Just x <- readNum
            | Nothing => do putStrLn "First number is invalid"
          Just y <- readNum
            | Nothing => do putStrLn "Second number is invalid"
          putStrLn $ "Sum = " ++ show (myAdd x y) ++ ", diff = " ++ show (mySub x y) ++
                            ", prod = " ++ show (myMul x y) ++ ", quot = " ++ show (myDiv x y)

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Text.Markup.Edda.Model

import public Text.Markup.Edda.Model.Common
import public Text.Markup.Edda.Model.Raw
import public Text.Markup.Edda.Model.Processed

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Category

import TypesAndFunctions

%default total

{- Often needed to do category theory in Idris. -}
public export
functionalExtensionality : {a, b : Type} -> FunctionalExtensionality a b
functionalExtensionality = believe_me

public export
record Category where
  constructor MkCategory
  Object : Type
  Morphism : Object -> Object -> Type
  Identity : (a : Object) -> Morphism a a
  After : {a, b, c : Object} -> Morphism b c -> Morphism a b -> Morphism a c
  LeftIdentity : {a, b : Object} -> (m : Morphism a b) ->
    After (Identity b) m = m
  RightIdentity : {a, b : Object} -> (m : Morphism a b) ->
    After m (Identity a) = m
  Associativity : {a, b, c, d : Object} ->
    (h : Morphism c d) -> (g : Morphism b c) -> (f : Morphism a b) ->
    After (After h g) f = After h {a} {b=c} {c=d} (After {a} {b} {c} g f)

public export
catId : {cat : Category} -> (a : Object cat) -> Morphism cat a a
catId {cat} a = Identity cat a

infix 25 .*
public export
(.*) : {cat : Category} -> {a, b, c : Object cat} ->
  Morphism cat b c -> Morphism cat a b -> Morphism cat a c
g .* f = After cat g f

public export
postCompose : {cat : Category} -> {a, b, c : Object cat} ->
  Morphism cat b c -> Morphism cat a b -> Morphism cat a c
postCompose f = (.*) f

public export
preCompose : {cat : Category} -> {a, b, c : Object cat} ->
  Morphism cat a b -> Morphism cat b c -> Morphism cat a c
preCompose f = \h => h .* f

public export
TypeCategory : Category
TypeCategory = MkCategory
  Type
  (\a, b => a -> b)
  (\_ => id)
  (\g, f => g . f)
  (\m => functionalExtensionality (\_ => Refl))
  (\m => functionalExtensionality (\_ => Refl))
  (\h, g, f => Refl)

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
module Toolkit.Data.Vect.Extra

import public Decidable.Equality
import        Data.Vect

%default total

namespace Equality
   public export
   vecEq : Eq type => Vect n type -> Vect m type -> Bool
   vecEq [] [] = True
   vecEq [] (x :: xs) = False
   vecEq (x :: xs) [] = False
   vecEq (x :: xs) (y :: ys) = x == y && vecEq xs ys

namespace Decidable
  namespace SameLength
    public export
    decEq : DecEq type
          => (n = m)
          -> (xs : Vect n type)
          -> (ys : Vect m type)
          -> Dec (xs = ys)
    decEq Refl xs ys with (decEq xs ys)
      decEq Refl ys ys | (Yes Refl) = Yes Refl
      decEq Refl xs ys | (No contra) = No contra

  namespace DiffLength

    public export
    vectorsDiffLength : DecEq type
                      => (contra : (n = m) -> Void)
                      -> {xs : Vect n type}
                      -> {ys : Vect m type}
                      -> (xs = ys) -> Void
    vectorsDiffLength contra Refl = contra Refl

    public export
    decEq : DecEq type
         => {n,m : Nat}
         -> (xs : Vect n type)
         -> (ys : Vect m type)
         -> Dec (xs = ys)
    decEq xs ys {n} {m} with (decEq n m)
      decEq xs ys {n = m} {m = m} | (Yes Refl) = decEq Refl xs ys
      decEq xs ys {n = n} {m = m} | (No contra) = No (vectorsDiffLength contra)

namespace Shape

  public export
  data Shape : (xs : Vect n a)
            -> (ys : Vect m a)
            -> Type
    where
      Empty : Shape Nil Nil
      LH    : Shape (x::xs) Nil
      RH    : Shape Nil      (y::ys)
      Both  : Shape (x::xs) (y::ys)

  export
  shape : (xs : Vect n a)
       -> (ys : Vect m a)
       -> Shape xs ys
  shape [] [] = Empty
  shape [] (y :: ys) = RH
  shape (x :: xs) [] = LH
  shape (x :: xs) (y :: ys) = Both

namespace ReplaceAt

  public export
  data ReplaceAt : (idx       : Fin n)
                -> (xs        : Vect n a)
                -> (this,that : a)
                -> (ys        : Vect n a)
                             -> Type
    where
      H : ReplaceAt FZ (x::xs)
                        x
                        y
                       (y::xs)

      T : ReplaceAt     idx       xs  x y      ys
       -> ReplaceAt (FS idx) (x'::xs) x y (x'::ys)

  notSame : (x = this -> Void) -> DPair (Vect (S len) a) (ReplaceAt FZ (x :: xs) this that) -> Void
  notSame _ (MkDPair _ (T y)) impossible

  notLater : (DPair (Vect len a) (ReplaceAt x xs this that) -> Void) -> DPair (Vect (S len) a) (ReplaceAt (FS x) (y :: xs) this that) -> Void
  notLater f (MkDPair (y :: ys) (T z)) = f (MkDPair ys z)

  export
  replaceAt : DecEq a
           => (idx : Fin n)
           -> (xs  : Vect n a)
           -> (this, that : a)
           -> Dec (DPair (Vect n a) (ReplaceAt idx xs this that))
  replaceAt FZ (x :: xs) this that with (decEq x this)
    replaceAt FZ (x :: xs) x    that | (Yes Refl) = Yes (MkDPair (that :: xs) H)
    replaceAt FZ (x :: xs) this that | (No contra)
      = No (notSame contra)
  replaceAt (FS x) (y :: xs) this that with (replaceAt x xs this that)
    replaceAt (FS x) (y :: xs) this that | (Yes (MkDPair fst snd))
      = Yes (MkDPair (y :: fst) (T snd))
    replaceAt (FS x) (y :: xs) this that | (No contra)
      = No (notLater contra)

namespace Quantifier
  namespace AtIndex

    public export
    data AtIndex : (type : Type)
                -> (p    : (a : type) -> Type)
                -> (idx  : Fin n)
                -> (xs   : Vect n type)
                        -> Type
      where
        Here : (prf : p x)
                   -> AtIndex type p FZ (x::xs)

        There : (later : AtIndex type p     next            xs)
                      -> AtIndex type p (FS next) (not_x :: xs)

    export
    Uninhabited (AtIndex type p idx Nil) where
      uninhabited (Here prf) impossible
      uninhabited (There later) impossible

    notLater : (AtIndex type p     y        xs  -> Void)
             -> AtIndex type p (FS y) (x :: xs) -> Void
    notLater f (There later) = f later

    notHere : (p x -> Void)
            -> AtIndex type p FZ (x :: xs) -> Void
    notHere f (Here prf) = f prf

    export
    atIndex : {type : Type}
           -> {p    : type -> Type}
           -> (dec  : (this : type) -> Dec (p this))
           -> (idx  : Fin n)
           -> (xs   : Vect n type)
                   -> Dec (AtIndex type p idx xs)
    atIndex dec idx []
      = No absurd

    atIndex dec FZ (x :: xs) with (dec x)
      atIndex dec FZ (x :: xs) | (Yes prf)
        = Yes (Here prf)
      atIndex dec FZ (x :: xs) | (No contra)
        = No (notHere contra)

    atIndex dec (FS y) (x :: xs) with (atIndex dec y xs)
      atIndex dec (FS y) (x :: xs) | (Yes prf)
        = Yes (There prf)
      atIndex dec (FS y) (x :: xs) | (No contra)
        = No (notLater contra)

    namespace Diff
      public export
      data AtIndexI : (type : Type)
                   -> (p    : (a : type) -> Type)
                   -> (m,n  : Nat)
                   -> (idx  : Fin m)
                   -> (xs   : Vect n type)
                           -> Type
        where
          At : AtIndex  type p idx xs
            -> AtIndexI type p n n idx xs

      Uninhabited (AtIndexI type p m Z idx Nil) where
        uninhabited (At (Here prf)) impossible
        uninhabited (At (There later)) impossible

      notAtIndex : (AtIndex type p idx xs -> Void)
                -> AtIndexI type p m m idx xs -> Void
      notAtIndex f (At x) = f x

      indexDiffers : (m = n -> Void) -> AtIndexI type p m n idx xs -> Void
      indexDiffers f (At x) = f Refl

      export
      atIndexI : {type : Type}
              -> {p    : type -> Type}
              -> {m,n  : Nat}
              -> (dec  : (this : type) -> Dec (p this))
              -> (idx  : Fin m)
              -> (xs   : Vect n type)
                      -> Dec (AtIndexI type p m n idx xs)
      atIndexI {m} {n} dec idx xs with (decEq m n)
        atIndexI {m = m} {n = m} dec idx xs | (Yes Refl) with (atIndex dec idx xs)
          atIndexI {m = m} {n = m} dec idx xs | (Yes Refl) | (Yes prf)
            = Yes (At prf)

          atIndexI {m = m} {n = m} dec idx xs | (Yes Refl) | (No contra)
            = No (notAtIndex contra)
        atIndexI {m = m} {n = n} dec idx xs | (No contra)
          = No (indexDiffers contra)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Teleportation

import Data.Nat
import Data.List
import Data.Vect
import Unitary
import Control.Linear.LIO
import QStateT
import Injection
import LinearTypes
import QuantumOp
import Examples

%default total

||| Example : Teleportation protocol

||| The unitary circuit that we have to apply to the initial state.
export
telep1 : Unitary 3
telep1 = H 0 (CNOT 0 1 (apply toBellBasis IdGate [1,2]))

||| The unitary correction that has to be applied after performing the measurement in the Bell basis.
||| The two Bool arguments indicate the measurement results.
export
unitary_correction : Bool -> Bool -> Unitary 1
unitary_correction b1 b2 = (if b2 then XGate else IdGate) . (if b1 then ZGate else IdGate)

||| The Quantum Teleportation Protocol as a state transformer.
export
teleportation : QuantumOp t =>
                (1 _ : Qubit) -> QStateT (t 1) (t 1) (LFstPair Qubit (Vect 2 Bool))
teleportation q0 = do
  [q1, q2] <- newQubits 2
  [q0,q1,q2] <- applyUnitary [q0,q1,q2] telep1
  [b1, b2] <- measure [q0,q1]
  [q] <- applyUnitary [q2] (unitary_correction b1 b2)
  pure (q # [b1, b2])

||| Run the teleportation protocol where the qubit to be teleported is in state |+>.
export
runTeleportation : QuantumOp t => IO (Vect 3 Bool)
runTeleportation =
      run (do
        q <- newQubit {t = t}
        q <- applyH q
        (q # [b1, b2]) <- teleportation q
        [b3] <- measure [q]
        pure [b1,b2,b3]
      )

||| Print some useful information on the screen obtained by executing runTeleportation.
export
drawTeleportation : QuantumOp t => IO ()
drawTeleportation = do
  [b1, b2, b3] <- runTeleportation {t = t}
  putStrLn "Teleportation Protocol\n\n"
  putStrLn "First circuit:"
  draw telep1
  putStrLn "Measurement results on first two qubits:"
  putStrLn (show (b1, b2))
  putStrLn "\nUnitary corrections:"
  draw (unitary_correction b1 b2)
  putStrLn "Result of measurement on the last qubit:"
  putStrLn (show b3)

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
data InfIO : Type where
  Do : IO a
      -> (a -> Inf InfIO)
      -> InfIO

{-loopPrint : String -> InfIO
loopPrint msg = Do (putStrLn msg)
                   (\_ => loopPrint msg)-}

{-run : InfIO -> IO ()
run (Do action cont) = do res <- action
                          run (cont res)-}

{-data Fuel = Dry | More Fuel-}
data Fuel = Dry | More (Lazy Fuel)

forever : Fuel
forever = More forever

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

run : Fuel -> InfIO -> IO ()
run Dry y = putStrLn "Out of fuel"
run (More fuel) (Do c f) = do res <- c
                              run fuel (f res)

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do
loopPrint : String -> InfIO
loopPrint msg = do putStrLn msg
                   loopPrint msg


text:
data DoorState = DoorOpen | DoorClosed

data DoorCmd : Type ->
               DoorState -> DoorState ->
               Type where
  Open :     DoorCmd () DoorClosed DoorOpen
  Close :    DoorCmd () DoorOpen   DoorClosed
  RingBell : DoorCmd () DoorClosed DoorClosed

  Pure : ty -> DoorCmd ty state state
  (>>=) : DoorCmd a state1 state2 ->
          (a -> DoorCmd b state2 state3) ->
          DoorCmd b state1 state3

doorProg : DoorCmd () DoorClosed DoorClosed
doorProg = do RingBell
              Open
              Close


text:
module Depling.Reduce

import Depling
import Depling.Decr
import Depling.Incr
import Data.Fin
import Data.Vect
import Debug.Trace

total
reduce_ℙ : Vect a (DAST n) -> DAST (a + n) -> DAST n
reduce_ℙ [] ast = ast
reduce_ℙ (h :: t) ast = reduce_ℙ t $ decr 0 (incr' h) ast

total
reduce_to : DAST n -> DAST n -> DAST n
reduce_to p (𝔹 t) = p
reduce_to _ r = r

total
export
reduce : DAST n -> DAST n
reduce p@((λ at b) =!= a) = reduce_to p $ decr 0 a b
reduce p@((λT at rt) =!= a) = reduce_to p $ decr 0 a rt
reduce p@(f@(𝔽 at rt b) =!= a) = reduce_to p $ decr 0 f $ decr 0 (incr 0 a) b
reduce p@(ℙ {a=ap} (ℂ {a=ac} cnc as) cnp t f) =
	if ac == ap && cnc == believe_me cnp
	then reduce_to p $ reduce_ℙ (reverse as) $ believe_me t
	else reduce_to p f
reduce (ʌ v) = ʌ v
reduce (λ at b) = λ (reduce at) (reduce b)
reduce (λT at rt) = λT (reduce at) (reduce rt)
reduce (f =!= a) = reduce f =!= reduce a
reduce 𝕋 = 𝕋
reduce (𝔽 at rt b) = 𝔽 (reduce at) (reduce rt) (reduce b)
reduce (𝕌 n t) = 𝕌 n (reduce t)
reduce (ℂ cn as) = assert_total $ ℂ cn $ map reduce as
reduce (ℙ v cn t f) = ℙ (reduce v) cn (reduce t) (reduce f)
reduce (𝔹 t) = 𝔹 $ reduce t

total
export
fullReduce : DAST n -> DAST n
fullReduce a = assert_total $ tick (reduce a) [a]
	where
		tick : DAST n -> List (DAST n) -> DAST n
		tick r o = if elem r o then r else tick (reduce r) (r :: o)

export
fullReduce' : DAST n -> DAST n
fullReduce' a = tick (reduce a) a
	where
		tick : DAST n -> DAST n -> DAST n
		tick r o = if r == o then r else tick (reduce r) r

-- lazy reduce: reduces to weak head normal form
total
export
lreduce : DAST n -> DAST n
lreduce p@((λ at b) =!= a) = reduce_to p $ decr 0 a b
lreduce p@((λT at rt) =!= a) = reduce_to p $ decr 0 a rt
lreduce p@(f@(𝔽 at rt b) =!= a) = reduce_to p $ decr 0 f $ decr 0 (incr 0 a) b
lreduce p@(ℙ {a=ap} (ℂ {a=ac} cnc as) cnp t f) =
	 if ac == ap && cnc == believe_me cnp
	 then reduce_to p $ reduce_ℙ (reverse as) $ believe_me t
	 else reduce_to p f
lreduce (f =!= a) = lreduce f =!= a
lreduce (ℙ v cn t f) = ℙ (lreduce v) cn t f
lreduce a = a

total
export
lfreduce : DAST n -> DAST n
lfreduce a = assert_total $ tick (lreduce a) a
	where
		tick : DAST n -> DAST n -> DAST n
		tick r o = if r == o then r else tick (lreduce r) r

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
-- Prototype of RealizedAttributes as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e
-- except that the data structure is not dependently typed.

module NonDTRealizedAttributes

public export
CostT : Type
CostT = Double

public export
record Costs where
  constructor MkCosts
  financial, temporal, computational : CostT

public export
QualityT : Type
QualityT = Double

public export
record NonDTRealizedAttributes where
  constructor MkNonDTRealizedAttributes
  costs : Costs
  quality : QualityT

-- Add costs
public export
add_costs : Costs -> Costs -> Costs
add_costs x y = MkCosts (x.financial + y.financial)
                        (x.temporal + y.temporal)
                        (x.computational + y.computational)

-- Add costs, minimum quality
public export
add_costs_min_quality : NonDTRealizedAttributes ->
                        NonDTRealizedAttributes ->
                        NonDTRealizedAttributes
add_costs_min_quality f_attrs g_attrs = fg_attrs where
  fg_attrs : NonDTRealizedAttributes
  fg_attrs = MkNonDTRealizedAttributes (add_costs f_attrs.costs g_attrs.costs)
                                       (min f_attrs.quality g_attrs.quality)

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
module Data.Primitives.Views

-- We need all the believe_mes and asserts throughout this file because we're
-- working with primitive here! We also have separate implementations per
-- primitive, rather than using interfaces, because we're only going to trust
-- the primitive implementations.

namespace IntegerV
  ||| View for expressing a number as a multiplication + a remainder
  public export
  data Divides : Integer -> (d : Integer) -> Type where
       DivByZero : Divides x 0
       DivBy : (div, rem : _) ->
               (prf : rem >= 0 && rem < d = True) ->
               Divides ((d * div) + rem) d

  ||| Covering function for the `Divides` view
  public export
  divides : (val : Integer) -> (d : Integer) -> Divides val d
  divides val 0 = DivByZero
  divides val d
         = assert_total $
             let dividend = if d < 0 then -(val `div` abs d)
                                     else val `div` d
                 remainder = abs (val - dividend * d) in
                 believe_me (DivBy {d} dividend remainder
                            (believe_me (Refl {x = True})))

  ||| View for recursion over Integers
  public export
  data IntegerRec : Integer -> Type where
       IntegerZ : IntegerRec 0
       IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
       IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)

  ||| Covering function for `IntegerRec`
  public export
  integerRec : (x : Integer) -> IntegerRec x
  integerRec 0 = IntegerZ
  integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
                      else believe_me (IntegerPred {n = -x}
                                (assert_total (believe_me (integerRec (x + 1)))))

namespace IntV
  ||| View for expressing a number as a multiplication + a remainder
  public export
  data Divides : Int -> (d : Int) -> Type where
       DivByZero : IntV.Divides x 0
       DivBy : (div, rem : _) ->
               (prf : rem >= 0 && rem < d = True) ->
               IntV.Divides ((d * div) + rem) d

  -- I have assumed, but not actually verified, that this will still
  -- give a right result (i.e. still adding up) when the Ints overflow.
  -- TODO: Someone please check this and fix if necessary...

  ||| Covering function for the `Divides` view
  public export
  divides : (val : Int) -> (d : Int) -> Divides val d
  divides val 0 = DivByZero
  divides val d
         = assert_total $
             let dividend = if d < 0 then -(val `div` abs d)
                                     else val `div` d
                 remainder = abs (val - dividend * d) in
                 believe_me (DivBy {d} dividend remainder
                            (believe_me (Refl {x = True})))

  ||| View for recursion over Ints
  public export
  data IntRec : Int -> Type where
       IntZ : IntRec 0
       IntSucc : IntRec (n - 1) -> IntRec n
       IntPred : IntRec ((-n) + 1) -> IntRec (-n)

  ||| Covering function for `IntRec`
  public export
  intRec : (x : Int) -> IntRec x
  intRec 0 = IntZ
  intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
                      else believe_me (IntPred {n = -x}
                                (assert_total (believe_me (intRec (x + 1)))))


text:
||| Data type `Validated` was introduced in chapter
||| *Functor and Friends*. It provides an error type
||| with the ability of error accumulation.
module Data.Validated

%default total

public export
data Validated : (e,a : Type) -> Type where
  Invalid : (err : e) -> Validated e a
  Valid   : (val : a) -> Validated e a

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export
validated : (e -> b) -> (a -> b) -> Validated e a -> b
validated f _ (Invalid ve) = f ve
validated _ g (Valid va)   = g va

public export
fromEither : Either e a -> Validated e a
fromEither = either Invalid Valid

public export
toEither : Validated e a -> Either e a
toEither = validated Left Right

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

public export
Eq e => Eq a => Eq (Validated e a) where
  Invalid x == Invalid y = x == y
  Valid x   == Valid y   = x == y
  _         == _         = False

public export
Ord e => Ord a => Ord (Validated e a) where
  compare (Invalid x) (Invalid y) = compare x y
  compare (Invalid _) (Valid _)   = LT
  compare (Valid _)   (Invalid _) = GT
  compare (Valid x)   (Valid y)   = compare x y

public export
Show e => Show a => Show (Validated e a) where
  showPrec p (Invalid e) = showCon p "Invalid" (showArg e)
  showPrec p (Valid a)   = showCon p "Valid" (showArg a)

public export
Functor (Validated e) where
  map _ (Invalid err) = Invalid err
  map f (Valid val)   = Valid $ f val

public export
Semigroup e => Applicative (Validated e) where
  pure = Valid
  Valid   f  <*> Valid v    = Valid $ f v
  Valid   _  <*> Invalid ve = Invalid ve
  Invalid e1 <*> Invalid e2 = Invalid $ e1 <+> e2
  Invalid ve <*> Valid _    = Invalid ve

public export
Foldable (Validated e) where
  foldr acc st (Invalid _) = st
  foldr acc st (Valid v)   = acc v st

  foldl acc st (Invalid _) = st
  foldl acc st (Valid v)   = acc st v

  foldlM acc st (Invalid _) = pure st
  foldlM acc st (Valid v)   = acc st v

  foldMap f (Invalid _) = neutral
  foldMap f (Valid v)   = f v

  toList (Invalid _) = []
  toList (Valid v)   = [v]

  null (Invalid _) = True
  null (Valid v)   = False

public export
Traversable (Validated e) where
  traverse f (Invalid ve) = pure $ Invalid ve
  traverse f (Valid va)   = Valid <$> f va

public export
Bifunctor Validated where
  bimap f g (Invalid ve) = Invalid $ f ve
  bimap f g (Valid va)   = Valid $ g va

  mapFst f (Invalid ve) = Invalid $ f ve
  mapFst f (Valid va)   = Valid va

  mapSnd f (Invalid ve) = Invalid ve
  mapSnd f (Valid va)   = Valid $ f va

public export
Bifoldable Validated where
  bifoldr f g st (Invalid ve) = f ve st
  bifoldr f g st (Valid va)   = g va st

  bifoldl f g st (Invalid ve) = f st ve
  bifoldl f g st (Valid va)   = g st va

  binull _ = False

public export
Bitraversable Validated where
  bitraverse f g (Invalid ve) = Invalid <$> f ve
  bitraverse f g (Valid va)   = Valid <$> g va

public export
Monoid e => Alternative (Validated e) where
  empty = Invalid neutral

  Valid va  <|> _         = Valid va
  Invalid x <|> Invalid y = Invalid $ x <+> y
  Invalid _ <|> Valid va  = Valid va