text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.1

import System.Concurrency.Channels

-- check that all functions are total
%default total

data Message = Add Nat Nat

namespace section_15_1_2

  partial
  adder : IO ()
  adder = do Just sender_chan <- listen 1
             | Nothing => section_15_1_2.adder
             Just msg <- unsafeRecv Message sender_chan
             | Nothing => section_15_1_2.adder
             case msg of
               Add x y => do ok <- unsafeSend sender_chan (x + y)
                             section_15_1_2.adder

  partial
  main : IO ()
  main = do Just adder_id <- spawn section_15_1_2.adder
            | Nothing => putStrLn "Spawn failed"
            Just chan <- connect adder_id
            | Nothing => putStrLn "Connection failed"
            ok <- unsafeSend chan (Add 2 3)
            Just answer <- unsafeRecv Nat chan
            | Nothing => putStrLn "Send failed"
            printLn answer

namespace section_15_1_3_pb1

  partial
  adder : IO ()
  adder = do Just sender_chan <- listen 1
             | Nothing => section_15_1_3_pb1.adder
             Just msg <- unsafeRecv Message sender_chan
             | Nothing => section_15_1_3_pb1.adder
             case msg of
               Add x y => do ok <- unsafeSend sender_chan (x + y)
                             section_15_1_3_pb1.adder

  partial
  main : IO ()
  main = do Just adder_id <- spawn section_15_1_3_pb1.adder
            | Nothing => putStrLn "Spawn failed"
            Just chan <- connect adder_id
            | Nothing => putStrLn "Connection failed"
            ok <- unsafeSend chan (Add 2 3)
            Just answer <- unsafeRecv String chan
            | Nothing => putStrLn "Send failed"
            printLn answer

namespace section_15_1_3_pb2

  partial
  adder : IO ()
  adder = do Just sender_chan <- listen 1
             | Nothing => section_15_1_3_pb2.adder
             Just msg <- unsafeRecv Message sender_chan
             | Nothing => section_15_1_3_pb2.adder
             case msg of
               Add x y => do ok <- unsafeSend sender_chan (x + y)
                             section_15_1_3_pb2.adder

  partial
  main : IO ()
  main = do Just adder_id <- spawn section_15_1_3_pb2.adder
            | Nothing => putStrLn "Spawn failed"
            Just chan <- connect adder_id
            | Nothing => putStrLn "Connection failed"
            ok <- unsafeSend chan (Add 2 3)
            Just answer <- unsafeRecv Nat chan
            | Nothing => putStrLn "Send failed"
            printLn answer
            ok <- unsafeSend chan (Add 3 4)
            Just answer <- unsafeRecv Nat chan
            | Nothing => putStrLn "Send failed"
            printLn answer

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Decidable.Equality

data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

exactLength : {m : _} ->
              (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case decEq m len of
                                 Yes Refl => Just input
                                 No contra => Nothing

ext: idr


text:
module CodeGen

%default total
%access public export

||| Stands for "Static Method Inline"
record SMI where
  constructor StatMethInli
  name : String
  args : List String
  retT : String
  impl : String

genSMI : SMI -> String
genSMI x =
  let argz = concat $ intersperse ", " $ args x
  in concat ["  static member inline ", name x, " (", argz, ") : ", retT x, " = ", impl x]

data AutoOpen = AutoOpen'

record NSAndModule where
  constructor NSNModule
  maybeModule : Maybe (String, Maybe AutoOpen)
  ns : String

nsOnly : String -> NSAndModule
nsOnly ns = NSNModule Nothing ns

record FSFile where
  constructor FSF
  nsm : NSAndModule
  type : (String, List (List SMI))

maybeGenAutoOpen : Maybe AutoOpen -> List String -> List String
maybeGenAutoOpen Nothing = id
maybeGenAutoOpen (Just AutoOpen') = (::) "[<AutoOpen>]"

genNSAndModule : NSAndModule -> List String
genNSAndModule nsam =
  case maybeModule nsam of
    Nothing => [ "namespace " ++ ns nsam, ""]
    Just (modName, maybeAutoOpen) => maybeGenAutoOpen maybeAutoOpen
      [ "module " ++ ns nsam ++ "." ++ modName
      , ""
      ]

genClass : String -> List String
genClass x = ["type " ++ x ++ " () ="]

genHeader : FSFile -> List String
genHeader fsfile = genNSAndModule (nsm fsfile) ++ genClass (fst $ type fsfile)

genClassBody : List (List (SMI)) -> List String
genClassBody xs = xs >>= ((::) "" . map genSMI)

genFSFile : FSFile -> List String
genFSFile x = genHeader x ++ genClassBody (snd $ type x)

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

export
program : CanSpawn m => CanSleep m => PrintString m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"
  spawn $ do
    for 5 $ do
      printTime offset "spawned, before 1000"
      sleepFor 1.seconds
      printTime offset "spawned, before 2000"
      sleepFor 2.seconds
    printTime offset "spawned, end"
  for 10 $ do
    printTime offset "                      trunk, before 350"
    sleepFor 350.millis
    printTime offset "                      trunk, before 750"
    sleepFor 750.millis
  printTime offset "                      trunk, end"


text:
module Books

import public Books.Comic as Books

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| Primitive operations for fixed size, unsigned integers.
module Primitives.UInt

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

---------------------------------------------------------------------------------------------------
-- UINT ADD
---------------------------------------------------------------------------------------------------
add_uintX_name : Nat -> Name
add_uintX_name nBits = makeBuiltinName "add_uint\{show nBits}"

add_uintX_code : Name -> Nat -> String
add_uintX_code name nBits = """
    # Adds two uints
    # Returns the result as a uint
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local carry : felt
        %{ (ids.carry, ids.res) = divmod(ids.a + ids.b, \{show shift}) %}

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

        # inlined uint_check(res)
        assert [range_check_ptr] = res
        assert [range_check_ptr+1] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+2

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT SUB
---------------------------------------------------------------------------------------------------
sub_uintX_name : Nat -> Name
sub_uintX_name nBits = makeBuiltinName "sub_uint\{show nBits}"

sub_uintX_code : Name -> Nat -> String
sub_uintX_code name nBits = """
    # Subtracts two integers.
    # Returns the result as a uint.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local borrow : felt
        %{
            (carry, ids.res) = divmod(ids.a - ids.b, \{show shift})
            ids.borrow = -carry  # if b > a then carry is -1
        %}

        assert borrow * borrow = borrow  # borrow is 0 or 1
        assert res = a - b + borrow * \{show shift}
        # inlined uint_check(res)
        assert [range_check_ptr] = res
        assert [range_check_ptr+1] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+2

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT MUL
---------------------------------------------------------------------------------------------------
mul_uintX_name : Nat -> Name
mul_uintX_name nBits = makeBuiltinName "mul_uint\{show nBits}"

mul_uintX_code : Name -> Nat -> String
mul_uintX_code name nBits = """
    # Multiplies two uint.
    # Returns the result
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local offset : felt
        %{ (ids.offset, ids.res) = divmod(ids.a * ids.b, \{show shift}) %}

        # Check offset can not trigger overflow / underflow
        #  to trigger overflow offset*SHIFT must be negative
        #  to trigger underflow offset*SHIFT must be > PRIME - (SHIFT-1)**2
        #    Note: 2**128 (rangecheck) < PRIME - (SHIFT-1)**2 (e.g: 64 => approx 2**128 < 2**192? - 2**128)
        #    Note: Max needed offset*SHIFT = (SHIFT-1)*(SHIFT-1)- SHIFT = (SHIFT-2)*(SHIFT-1) < SHIFT**2
        #	 Note: for SHIFT = 2 ** 64 => offset*SHIFT < 2**128 ((2**64)**2)
        tempvar realOffset = offset * \{show shift}
        assert [range_check_ptr] = realOffset # is positive & smaller 2**128 (this is exactly range_check semantic)
        assert res = a * b - realOffset

        # inlined uint_check(res)
        assert [range_check_ptr+1] = res
        assert [range_check_ptr+2] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+3

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT DIV
---------------------------------------------------------------------------------------------------
div_uintX_name : Nat -> Name
div_uintX_name nBits = makeBuiltinName "div_uint\{show nBits}"

div_uintX_code : Name -> Nat -> String
div_uintX_code name nBits = """
    # Division between uint.
    # 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 : felt
        local rem : felt
        #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
        %{ (ids.res, ids.rem) = divmod(ids.a, ids.b) %}

        # Check res * b + rem can not trigger overflow / underflow
        #  Note: 0 < b < 2**64 -- given by semantics
        #  Note: 0 <= res < 2**64 -- checked by uint_check
        #  Implies: 0 <= res * b < 2**128
        #  Note: 0 < rem < 2**64 -- (must be checked -- as hint can lie)
        #  If we weaken to: 0 < rem < 2**128 (rangecheck)
        #  then still: 0 < res * b + rem < 2**129 < PRIME / 2 (positive numbers)

        assert [range_check_ptr] = rem 				# is positive & smaller 2**128 (this is exactly range_check semantic)
        # Note: will fail if b = 0 which is the expected behaviour
        assert [range_check_ptr+1] = b - rem - 1	# rem < b
        assert res * b + rem = a

        # inlined uint_check(res) -- implied as res must be between 0 and a to pass the checks & a is valid (input)
        # assert [range_check_ptr+2] = res
        # assert [range_check_ptr+3] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+2

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT MOD
---------------------------------------------------------------------------------------------------
mod_uintX_name : Nat -> Name
mod_uintX_name nBits = makeBuiltinName "mod_uint\{show nBits}"

mod_uintX_code : Name -> Nat -> String
mod_uintX_code name nBits = """
    # Division between uint.
    # 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 : felt
        local rem : felt
        #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
        %{ (ids.res, ids.rem) = divmod(ids.a, ids.b) %}

        # Check res * b + rem can not trigger overflow / underflow
        #  Note: 0 < b < 2**64 -- given by semantics
        #  Note: 0 <= res < 2**64 -- checked by uint_check
        #  Implies: 0 <= res * b < 2**128
        #  Note: 0 < rem < 2**64 -- (must be checked -- as hint can lie)
        #  If we weaken to: 0 < rem < 2**128 (rangecheck)
        #  then still: 0 < res * b + rem < 2**129 < PRIME / 2 (positive numbers)

        assert [range_check_ptr] = rem 				# is positive & smaller 2**128 (this is exactly range_check semantic)
        # Note: will fail if b = 0 which is the expected behaviour
        assert [range_check_ptr+1] = b - rem - 1	# rem < b
        assert res * b + rem = a

        # inlined uint_check(res) -- implied as res must be between 0 and a to pass the checks & a is valid (input)
        # assert [range_check_ptr+2] = res
        # assert [range_check_ptr+3] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+2

        return (rem, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT NEG:
---------------------------------------------------------------------------------------------------
neg_uintX_name : Nat -> Name
neg_uintX_name nBits = makeBuiltinName "neg_uint\{show nBits}"

neg_uintX_code : Name -> Nat -> String
neg_uintX_code name nBits = """
    # Returns -x the negation of x, in the sense that it is that number such that x + -x = 0, if addition wraps around such that 255+1=0.
    # Note that -128 is 128, since 128+128=0.
    func \{cairoName name}(range_check_ptr, b : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local borrow : felt
        %{
            (carry, ids.res) = divmod(0 - ids.b, \{show shift})
            ids.borrow = -carry  # if b > 0 then carry is -1
        %}

        assert borrow * borrow = borrow  # borrow is 0 or 1
        assert res = - b + borrow * \{show shift}
        # inlined uint_check(res)
        assert [range_check_ptr] = res
        assert [range_check_ptr+1] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+2

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT SHL
---------------------------------------------------------------------------------------------------
shl_uintX_name : Nat -> Name
shl_uintX_name nBits = makeBuiltinName "shl_uint\{show nBits}"

-- Todo: Analyze complexity of pow and see if a bitpattern based mult is more efficient
shl_uintX_code : Name -> Nat -> String
shl_uintX_code name nBits = """
    # Computes the logical left shift of a uint.
    #  Note: We should consider not supporting these
    #  Reason: Programmers expect them to be quick and often try to optimize by replacing some *,/ with <<, >>
    #          But in cairo these are horrendibly slow
    #		   Inconviniently these are the only one requiring imports and they are the only one that are not ap stable
    func \{cairoName name}(range_check_ptr, a : felt,  b : felt) -> (res : felt, range_check_ptr):

        #inlined uint_pow2
        # If b >= BIT_LENGTH, the result will be zero modulo 2**BIT_LENGTH.
        tempvar res
        %{ids.res = 1 if ids.b < \{show nBits} 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}
            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)} - b
            let range_check_ptr = range_check_ptr + 1
            let (c) = pow{range_check_ptr=range_check_ptr}(2, b)
            \{cairoName (mul_uintX_name nBits)}(range_check_ptr, a, c)
            ret
        end
    end
"""

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

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

export
[shl_uint8] PrimFn where
    apStable = False

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

    imports = shl_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_uintX 8, mul_uintX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_uintX_name 8) args]

export
[shl_uint16] PrimFn where
    apStable = False

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

    imports = shl_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_uintX 16, mul_uintX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_uintX_name 16) args]

export
[shl_uint32] PrimFn where
    apStable = False

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

    imports = shl_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_uintX 32, mul_uintX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_uintX_name 32) args]

export
[shl_uint64] PrimFn where
    apStable = False

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

    imports = shl_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shl_uintX 64, mul_uintX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (shl_uintX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT SHR
---------------------------------------------------------------------------------------------------
shr_uintX_name : Nat -> Name
shr_uintX_name nBits = makeBuiltinName "shr_uint\{show nBits}"

-- Todo: Analyze complexity of pow and see if a bitpattern based div is more efficient
shr_uintX_code : Name -> Nat -> String
shr_uintX_code name nBits = """
    # Computes the logical right shift of a uint.
    #  Reason: Programmers expect them to be quick and often try to optimize by replacing some *,/ with <<, >>
    #          But in cairo these are horrendibly slow
    #		   Inconviniently these are the only one requiring imports and they are the only one that are not ap stable
    func \{cairoName name}(range_check_ptr, a : felt,  b : felt) -> (res : felt, range_check_ptr):
        #inlined uint_pow2
        # If b >= BIT_LENGTH, the result will be zero modulo 2**BIT_LENGTH.
        tempvar res
        %{ids.res = 1 if ids.b < \{show nBits} 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}
            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)} - b
            let range_check_ptr = range_check_ptr + 1
            let (c) = pow{range_check_ptr=range_check_ptr}(2, b)
            \{cairoName (div_uintX_name nBits)}(range_check_ptr, a, c)
            ret
        end
    end
"""

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

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

export
[shr_uint8] PrimFn where
    apStable = False

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

    imports = shr_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_uintX 8, div_uintX 8]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_uintX_name 8) args]

export
[shr_uint16] PrimFn where
    apStable = False

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

    imports = shr_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_uintX 16, div_uintX 16]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_uintX_name 16) args]

export
[shr_uint32] PrimFn where
    apStable = False

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

    imports = shr_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_uintX 32, div_uintX 32]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_uintX_name 32) args]

export
[shr_uint64] PrimFn where
    apStable = False

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

    imports = shr_uintX_imports
    implicits = singleton range_check_builtin
    dependencies = fromList [shr_uintX 64, div_uintX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (shr_uintX_name 64) args]

---------------------------------------------------------------------------------------------------
-- UINT AND
{-
func bitwise_and{bitwise_ptr : BitwiseBuiltin*}(x : felt, y : felt) -> (x_and_y : felt):
    bitwise_ptr.x = x
    bitwise_ptr.y = y
    let x_and_y = bitwise_ptr.x_and_y
    let x_xor_y = bitwise_ptr.x_xor_y
    let x_or_y = bitwise_ptr.x_or_y
    let bitwise_ptr = bitwise_ptr + BitwiseBuiltin.SIZE
    return (x_and_y=x_and_y)
end

struct BitwiseBuiltin:
    member x : felt
    member y : felt
    member x_and_y : felt
    member x_xor_y : felt
    member x_or_y : felt
end
-}
---------------------------------------------------------------------------------------------------

and_uintX_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
and_uintX_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+2]

"""

and_uintX : Nat -> CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
and_uintX _ res [a,b] implicits =
  case lookup bitwise_builtin implicits of
        Just (bw_in, bw_out) => Raw $ and_uintX_code res bw_in bw_out a b
        Nothing => assert_total $ idris_crash "bitwise_ptr not found"
and_uintX nBits _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode and_uint\{show nBits}"

export
[and_uint8] PrimFn where
    eval [_, ConstValue (B8 0)] = Just $ NewValue $ ConstValue $ B8 0
    eval [ConstValue (B8 0), _] = Just $ NewValue $ ConstValue $ B8 0
    eval [_, ConstValue (B8 255)] = Just $ ArgValue 0
    eval [ConstValue (B8 255), _] = Just $ ArgValue 1
    eval [ConstValue (B8 a), ConstValue (B8 b)] = Just $ NewValue $ ConstValue $ B8 (prim__and_Bits8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = and_uintX 8

export
[and_uint16] PrimFn where
    eval [_, ConstValue (B16 0)] = Just $ NewValue $ ConstValue $ B16 0
    eval [ConstValue (B16 0), _] = Just $ NewValue $ ConstValue $ B16 0
    eval [_, ConstValue (B16 65535)] = Just $ ArgValue 0
    eval [ConstValue (B16 65535), _] = Just $ ArgValue 1
    eval [ConstValue (B16 a), ConstValue (B16 b)] = Just $ NewValue $ ConstValue $ B16 (prim__and_Bits16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = and_uintX 16

export
[and_uint32] PrimFn where
    eval [_, ConstValue (B32 0)] = Just $ NewValue $ ConstValue $ B32 0
    eval [ConstValue (B32 0), _] = Just $ NewValue $ ConstValue $ B32 0
    eval [_, ConstValue (B32 4294967295)] = Just $ ArgValue 0
    eval [ConstValue (B32 4294967295), _] = Just $ ArgValue 1
    eval [ConstValue (B32 a), ConstValue (B32 b)] = Just $ NewValue $ ConstValue $ B32 (prim__and_Bits32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = and_uintX 32

export
[and_uint64] PrimFn where
    eval [_, ConstValue (B64 0)] = Just $ NewValue $ ConstValue $ B64 0
    eval [ConstValue (B64 0), _] = Just $ NewValue $ ConstValue $ B64 0
    eval [_, ConstValue (B64 18446744073709551615)] = Just $ ArgValue 0
    eval [ConstValue (B64 18446744073709551615), _] = Just $ ArgValue 1
    eval [ConstValue (B64 a), ConstValue (B64 b)] = Just $ NewValue $ ConstValue $ B64 (prim__and_Bits64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = and_uintX 64

---------------------------------------------------------------------------------------------------
-- UINT OR
---------------------------------------------------------------------------------------------------
or_uintX_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
or_uintX_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+4]

"""

or_uintX : Nat -> CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
or_uintX _ res [a,b] implicits =
  case lookup bitwise_builtin implicits of
        Just (bw_in, bw_out) => Raw $ or_uintX_code res bw_in bw_out a b
        Nothing => assert_total $ idris_crash "bitwise_ptr not found"
or_uintX nBits _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode or_uint\{show nBits}"

export
[or_uint8] PrimFn where
    eval [_, ConstValue (B8 0)] = Just $ ArgValue 0
    eval [ConstValue (B8 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (B8 255)] = Just $ NewValue $ ConstValue $ B8 255
    eval [ConstValue (B8 255), _] = Just $ NewValue $ ConstValue $ B8 255
    eval [ConstValue (B8 a), ConstValue (B8 b)] = Just $ NewValue $ ConstValue $ B8 (prim__or_Bits8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = or_uintX 8

export
[or_uint16] PrimFn where
    eval [_, ConstValue (B16 0)] = Just $ ArgValue 0
    eval [ConstValue (B16 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (B16 65535)] = Just $ NewValue $ ConstValue $ B16 65535
    eval [ConstValue (B16 65535), _] = Just $ NewValue $ ConstValue $ B16 65535
    eval [ConstValue (B16 a), ConstValue (B16 b)] = Just $ NewValue $ ConstValue $ B16 (prim__or_Bits16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = or_uintX 16

export
[or_uint32] PrimFn where
    eval [_, ConstValue (B32 0)] = Just $ ArgValue 0
    eval [ConstValue (B32 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (B32 4294967295)] = Just $ NewValue $ ConstValue $ B32 4294967295
    eval [ConstValue (B32 4294967295), _] = Just $ NewValue $ ConstValue $ B32 4294967295
    eval [ConstValue (B32 a), ConstValue (B32 b)] = Just $ NewValue $ ConstValue $ B32 (prim__or_Bits32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = or_uintX 32

export
[or_uint64] PrimFn where
    eval [_, ConstValue (B64 0)] = Just $ ArgValue 0
    eval [ConstValue (B64 0), _] = Just $ ArgValue 1
    eval [_, ConstValue (B64 18446744073709551615)] = Just $ NewValue $ ConstValue $ B64 18446744073709551615
    eval [ConstValue (B64 18446744073709551615), _] = Just $ NewValue $ ConstValue $ B64 18446744073709551615
    eval [ConstValue (B64 a), ConstValue (B64 b)] = Just $ NewValue $ ConstValue $ B64 (prim__or_Bits64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = or_uintX 64

---------------------------------------------------------------------------------------------------
-- UINT XOR
---------------------------------------------------------------------------------------------------
xor_uintX_code : CairoReg -> CairoReg -> CairoReg -> CairoReg -> CairoReg -> String
xor_uintX_code r bitwise_ptr_in bitwise_ptr_out x y = """
    assert [\{compileReg bitwise_ptr_in}] = \{compileReg x}
    assert [\{compileReg bitwise_ptr_in}+1] = \{compileReg y}
    \{ compileRegDecl bitwise_ptr_out} = \{compileReg bitwise_ptr_in} + BitwiseBuiltin.SIZE
    \{ compileRegDecl r } = [\{compileReg bitwise_ptr_in}+3]

"""

xor_uintX : Nat -> CairoReg -> List CairoReg -> LinearImplicitArgs -> PrimFnCode
xor_uintX _ res [a,b] implicits =
  case lookup bitwise_builtin implicits of
        Just (bw_in, bw_out) => Raw $ xor_uintX_code res bw_in bw_out a b
        Nothing => assert_total $ idris_crash "bitwise_ptr not found"
xor_uintX nBits _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode xor_uint\{show nBits}"

export
[xor_uint8] PrimFn where
    eval [_, ConstValue (B8 0)] = Just $ ArgValue 0
    eval [ConstValue (B8 0), _] = Just $ ArgValue 1
    eval [ConstValue (B8 a), ConstValue (B8 b)] = Just $ NewValue $ ConstValue $ B8 (prim__xor_Bits8 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = xor_uintX 8

export
[xor_uint16] PrimFn where
    eval [_, ConstValue (B16 0)] = Just $ ArgValue 0
    eval [ConstValue (B16 0), _] = Just $ ArgValue 1
    eval [ConstValue (B16 a), ConstValue (B16 b)] = Just $ NewValue $ ConstValue $ B16 (prim__xor_Bits16 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = xor_uintX 16

export
[xor_uint32] PrimFn where
    eval [_, ConstValue (B32 0)] = Just $ ArgValue 0
    eval [ConstValue (B32 0), _] = Just $ ArgValue 1
    eval [ConstValue (B32 a), ConstValue (B32 b)] = Just $ NewValue $ ConstValue $ B32 (prim__xor_Bits32 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = xor_uintX 32

export
[xor_uint64] PrimFn where
    eval [_, ConstValue (B64 0)] = Just $ ArgValue 0
    eval [ConstValue (B64 0), _] = Just $ ArgValue 1
    eval [ConstValue (B64 a), ConstValue (B64 b)] = Just $ NewValue $ ConstValue $ B64 (prim__xor_Bits64 (cast a) (cast b))
    eval _ = Nothing

    imports = singleton $ bitwiseBuiltinImport
    implicits = singleton bitwise_builtin
    generateCode = xor_uintX 64

---------------------------------------------------------------------------------------------------
-- UINT LT
---------------------------------------------------------------------------------------------------
lt_uintX_name : Name
lt_uintX_name = makeBuiltinName "lt_uint"

lt_uintX_code : Name -> String
lt_uintX_code name = """
    # Returns 1 if the first unsigned integer is less than the second unsigned integer, otherwise returns 0.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res, range_check_ptr):
        tempvar res
        %{ids.res = 1 if ids.a < ids.b else 0 %}
        # b < 2**128 & a < 2**128 is given by semantics
        # 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_uintX : (Name, Lazy CairoDef)
lt_uintX = (lt_uintX_name, def)
  where def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (lt_uintX_code lt_uintX_name)) 2 1

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT LTE
---------------------------------------------------------------------------------------------------
lte_uintX_name : Name
lte_uintX_name = makeBuiltinName "lte_uint"

lte_uintX_code : Name -> String
lte_uintX_code name = """
    # Returns 1 if the first unsigned integer is less than or equal to the second unsigned integer, otherwise returns 0.
    func \{cairoName name}(range_check_ptr, a : felt, b : felt) -> (res, range_check_ptr):
        tempvar res
        %{ids.res = 1 if ids.a <= ids.b else 0 %}
        # b < 2**128 & a < 2**128 is given by semantics
        # b < a
        if res == 0:
            assert [range_check_ptr] = a - b - 1
            let range_check_ptr = range_check_ptr + 1
            return (0, range_check_ptr)
        #a <= b
        else:
            assert [range_check_ptr] = b - a - 0	#+0 is for ap stability improves worse case in code gen
            let range_check_ptr = range_check_ptr + 1
            return (1, range_check_ptr)
        end
    end
"""

lte_uintX : (Name, Lazy CairoDef)
lte_uintX = (lte_uintX_name, def)
  where def : CairoDef
        def = ForeignDef (MkForeignInfo True Nothing [range_check_builtin] empty (lte_uintX_code lte_uintX_name)) 2 1

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

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

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_uintX]
    generateCode = generateLteCallCode

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

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_uintX]
    generateCode = generateLteCallCode

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

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_uintX]
    generateCode = generateLteCallCode

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

    implicits = singleton range_check_builtin
    dependencies = fromList [lte_uintX]
    generateCode = generateLteCallCode

---------------------------------------------------------------------------------------------------
-- UINT EQ
---------------------------------------------------------------------------------------------------
export
[eq_uint8] PrimFn where
    eval [ConstValue (B8 a), ConstValue (B8 b)] = Just $ NewValue $ ConstValue $ toInt (a==b)
    eval _ = Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT GT
-- Implementation uses flipped arguments to lt
---------------------------------------------------------------------------------------------------

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

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

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

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

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

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

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

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

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

---------------------------------------------------------------------------------------------------
-- UINT CAST
---------------------------------------------------------------------------------------------------
cast_uintX_name : Nat -> Name
cast_uintX_name nBits = makeBuiltinName "cast_uint\{show nBits}"

cast_uintX_code : Name -> Nat -> String
cast_uintX_code name nBits = """
    # Casts to uint\{show nBits}
    # Returns the result as uint\{show nBits}.
    func \{cairoName name}(range_check_ptr, a : felt) -> (res : felt, range_check_ptr):
        alloc_locals
        local res : felt
        local offset : felt
        %{ (ids.offset, ids.res) = divmod(ids.a, \{show shift}) %}

        # Check offset can not trigger overflow / underflow
        #  to trigger overflow offset*SHIFT must be negative
        #  to trigger underflow offset*SHIFT must be > PRIME - (SHIFT-1)**2
        #    Note: 2**128 (rangecheck) < PRIME - (SHIFT-1)**2 (e.g: 64 => approx 2**128 < 2**192? - 2**128)
        #    Note: Max needed offset*SHIFT = (SHIFT-1)*(SHIFT-1)- SHIFT = (SHIFT-2)*(SHIFT-1) < SHIFT**2
        #	 Note: for SHIFT = 2 ** 64 => offset*SHIFT < 2**128 ((2**64)**2)
        tempvar realOffset = offset * \{show shift}
        assert [range_check_ptr] = realOffset # is positive & smaller 2**128 (this is exactly range_check semantic)
        assert res = a - realOffset

        # inlined uint_check(res)
        assert [range_check_ptr+1] = res
        assert [range_check_ptr+2] = \{show (shift - 1)} - res
        let range_check_ptr = range_check_ptr+3

        return (res, range_check_ptr)
    end
"""
  where shift : Integer
        shift = pow2 nBits

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

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

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

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

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

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

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

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

    implicits = singleton range_check_builtin
    dependencies = fromList [cast_uintX 64]
    generateCode res args implicits = Instructions [CALL [res] implicits (cast_uintX_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:
module Test.SemVar.LexerTest

import IdrTest.Test
import IdrTest.Expectation

import SemVar.Lexer

lexerSpecs : List (String, Maybe (List SemVarToken))
lexerSpecs =
  [
    (
      "1.2.3-prerelease+commit",
      Just $
      [ Tok Number "1"
      , Tok Dot "."
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      , Tok Hyphen "-"
      , Tok Text "prerelease"
      , Tok Plus "+"
      , Tok Text "commit"
      ]
    ),
    (
      "~1.2.3",
      Just $
      [ Tok Tilde "~"
      , Tok Number "1"
      , Tok Dot "."
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      ]
    ),
    (
      "^1.22.3",
      Just $
      [ Tok Caret "^"
      , Tok Number "1"
      , Tok Dot "."
      , Tok Number "22"
      , Tok Dot "."
      , Tok Number "3"
      ]
    ),
    (
      "1.*",
      Just $
      [ Tok Number "1"
      , Tok Dot "."
      , Tok Asterisk "*"
      ]
    ),
    (
      ">=1",
      Just $
      [ Tok CmpGTE ">="
      , Tok Number "1"
      ]
    ),
    (
      "1.2.3 - 2.3",
      Just $
      [ Tok Number "1"
      , Tok Dot "."
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      , Tok Whitespace " "
      , Tok Hyphen ""
      , Tok Whitespace " "
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      ]
    ),
    (
      "1.2.3 || 2.3",
      Just $
      [ Tok Number "1"
      , Tok Dot "."
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      , Tok Whitespace " "
      , Tok Pipe "||"
      , Tok Whitespace " "
      , Tok Number "2"
      , Tok Dot "."
      , Tok Number "3"
      ]
    )
  ]

export
suite : Test
suite =
  let
    lexerTests =
      map (\(text, result) =>
        test text (\_ => assertEq (lexSemVar text) result)
      ) lexerSpecs
  in
    describe "Lexer Tests"
      [ describe "Lexer Specs" lexerTests
      ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Solutions.Predicates

import Data.Vect
import Decidable.Equality

%default total

--------------------------------------------------------------------------------
--          Preconditions
--------------------------------------------------------------------------------

data NonEmpty : (as : List a) -> Type where
  IsNonEmpty : NonEmpty (h :: t)

-- 1

tail : (as : List a) -> (0 _ : NonEmpty as) => List a
tail (_ :: xs) = xs
tail [] impossible

-- 2

concat1 : Semigroup a => (as : List a) -> (0 _ : NonEmpty as) => a
concat1 (h :: t) = foldl (<+>) h t

foldMap1 : Semigroup m => (a -> m) -> (as : List a) -> (0 _ : NonEmpty as) => m
foldMap1 f (h :: t) = foldl (\x,y => x <+> f y) (f h) t

-- 3

maximum : Ord a => (as : List a) -> (0 _ : NonEmpty as) => a
maximum (x :: xs) = foldl max x xs

minimum : Ord a => (as : List a) -> (0 _ : NonEmpty as) => a
minimum (x :: xs) = foldl min x xs

-- 4

data Positive : Nat -> Type where
  IsPositive : Positive (S n)

saveDiv : (m,n : Nat) -> (0 _ : Positive n) => Nat
saveDiv m (S k) = go 0 m k
  where go : (res, rem, sub : Nat) -> Nat
        go res 0       _     = res
        go res (S rem) 0     = go (res + 1) rem k
        go res (S rem) (S x) = go res rem x

-- 5

data IJust : Maybe a -> Type where
  ItIsJust : IJust (Just v)

Uninhabited (IJust Nothing) where
  uninhabited ItIsJust impossible

isJust : (m : Maybe a) -> Dec (IJust m)
isJust Nothing  = No uninhabited
isJust (Just x) = Yes ItIsJust

fromJust : (m : Maybe a) -> (0 _ : IJust m) => a
fromJust (Just x) = x
fromJust Nothing  impossible

-- 6

data IsLeft : Either e a -> Type where
  ItIsLeft : IsLeft (Left v)

Uninhabited (IsLeft $ Right w) where
  uninhabited ItIsLeft impossible

isLeft : (v : Either e a) -> Dec (IsLeft v)
isLeft (Right _) = No uninhabited
isLeft (Left x)  = Yes ItIsLeft

data IsRight : Either e a -> Type where
  ItIsRight : IsRight (Right v)

Uninhabited (IsRight $ Left w) where
  uninhabited ItIsRight impossible

isRight : (v : Either e a) -> Dec (IsRight v)
isRight (Left _)  = No uninhabited
isRight (Right x) = Yes ItIsRight

fromLeft : (v : Either e a) -> (0 _ : IsLeft v) => e
fromLeft (Left x) = x
fromLeft (Right x) impossible

fromRight : (v : Either e a) -> (0 _ : IsRight v) => a
fromRight (Right x) = x
fromRight (Left x) impossible

--------------------------------------------------------------------------------
--          Contracts between Values
--------------------------------------------------------------------------------

data ColType = I64 | Str | Boolean | Float

IdrisType : ColType -> Type
IdrisType I64     = Int64
IdrisType Str     = String
IdrisType Boolean = Bool
IdrisType Float   = Double

record Column where
  constructor MkColumn
  name : String
  type : ColType

infixr 8 :>

(:>) : String -> ColType -> Column
(:>) = MkColumn

Schema : Type
Schema = List Column

data Row : Schema -> Type where
  Nil  : Row []
  (::) :  {0 name : String}
       -> {0 type : ColType}
       -> (v : IdrisType type)
       -> Row ss
       -> Row (name :> type :: ss)

data InSchema :  (name    : String)
              -> (schema  : Schema)
              -> (colType : ColType)
              -> Type where
  [search name schema]
  IsHere  : InSchema n (n :> t :: ss) t
  IsThere : InSchema n ss t -> InSchema n (fld :: ss) t

getAt :  {0 ss   : Schema}
      -> (name : String)
      -> Row ss
      -> (prf : InSchema name ss c)
      => IdrisType c
getAt name (v :: vs) {prf = IsHere}    = v
getAt name (_ :: vs) {prf = IsThere p} = getAt name vs

-- 1

Uninhabited (InSchema n [] c) where
  uninhabited IsHere impossible
  uninhabited (IsThere _) impossible

inSchema : (ss : Schema) -> (n : String) -> Dec (c ** InSchema n ss c)
inSchema []                    _ = No $ \(_ ** prf) => uninhabited prf
inSchema (MkColumn cn t :: xs) n = case decEq cn n of
  Yes Refl   => Yes (t ** IsHere)
  No  contra => case inSchema xs n of
    Yes (t ** prf) => Yes (t ** IsThere prf)
    No  contra2    => No $ \case (_ ** IsHere)    => contra Refl
                                 (t ** IsThere p) => contra2 (t ** p)

-- 2

updateAt : (name : String)
         -> Row ss
         -> (prf : InSchema name ss c)
         => (f : IdrisType c -> IdrisType c)
         -> Row ss
updateAt name (v :: vs) {prf = IsHere}    f = f v :: vs
updateAt name (v :: vs) {prf = IsThere p} f = v :: updateAt name vs f

-- 3

public export
data Elems : (xs,ys : List a) -> Type where
  ENil   : Elems [] ys
  EHere  : Elems xs ys -> Elems (x :: xs) (x :: ys)
  EThere : Elems xs ys -> Elems xs (y :: ys)

extract :  (0 s1 : Schema)
        -> (row : Row s2)
        -> (prf : Elems s1 s2)
        => Row s1
extract []       _         {prf = ENil}     = []
extract (_ :: t) (v :: vs) {prf = EHere x}  = v :: extract t vs
extract s1       (v :: vs) {prf = EThere x} = extract s1 vs

-- 4

namespace AllInSchema
  public export
  data AllInSchema :  (names : List String)
                   -> (schema : Schema)
                   -> (result : Schema)
                   -> Type where
    [search names schema]
    Nil  :  AllInSchema [] s []
    (::) :  InSchema n s c
         -> AllInSchema ns s res
         -> AllInSchema (n :: ns) s (n :> c :: res)

getAll :  {0 ss  : Schema}
       -> (names : List String)
       -> Row ss
       -> (prf : AllInSchema names ss res)
       => Row res
getAll []        _   {prf = []}     = []
getAll (n :: ns) row {prf = _ :: _} = getAt n row :: getAll ns row

--------------------------------------------------------------------------------
--          Use Case: Flexible Error Handling
--------------------------------------------------------------------------------

data Has :  (v : a) -> (vs  : Vect n a) -> Type where
  Z : Has v (v :: vs)
  S : Has v vs -> Has v (w :: vs)

Uninhabited (Has v []) where
  uninhabited Z impossible
  uninhabited (S _) impossible

data Union : Vect n Type -> Type where
  U : {0 ts : _} -> (ix : Has t ts) -> (val : t) -> Union ts

Uninhabited (Union []) where
  uninhabited (U ix _) = absurd ix

0 Err : Vect n Type -> Type -> Type
Err ts t = Either (Union ts) t

-- 1

project : (0 t : Type) -> (prf : Has t ts) => Union ts -> Maybe t
project t {prf = Z}   (U Z val)     = Just val
project t {prf = S p} (U (S x) val) = project t (U x val)
project t {prf = Z}   (U (S x) val) = Nothing
project t {prf = S p} (U Z val)     = Nothing

project1 : Union [t] -> t
project1 (U Z val) = val
project1 (U (S x) val) impossible

safe : Err [] a -> a
safe (Right x) = x
safe (Left x)  = absurd x

-- 2

weakenHas : Has t ts -> Has t (ts ++ ss)
weakenHas Z     = Z
weakenHas (S x) = S (weakenHas x)

weaken : Union ts -> Union (ts ++ ss)
weaken (U ix val) = U (weakenHas ix) val

extendHas : {m : _} -> {0 pre : Vect m a} -> Has t ts -> Has t (pre ++ ts)
extendHas {m = Z}   {pre = []}     x = x
extendHas {m = S p} {pre = _ :: _} x = S (extendHas x)

extend : {m : _} -> {0 pre : Vect m _} -> Union ts -> Union (pre ++ ts)
extend (U ix val) = U (extendHas ix) val

-- 3

0 Errs : Vect m Type -> Vect n Type -> Type
Errs []        _  = ()
Errs (x :: xs) ts = (Has x ts, Errs xs ts)

inject : Has t ts => (v : t) -> Union ts
inject v = U %search v

embed : (prf : Errs ts ss) => Union ts -> Union ss
embed (U Z val)     = inject val
embed (U (S x) val) = embed (U x val)

-- 4

data Rem : (v : a) -> (vs : Vect (S n) a) -> (rem : Vect n a) -> Type where
  [search v vs]
  RZ : Rem v (v :: rem) rem
  RS : Rem v vs rem -> Rem v (w :: vs) (w :: rem)

split : (prf : Rem t ts rem) => Union ts -> Either t (Union rem)
split {prf = RZ}   (U Z     val) = Left val
split {prf = RZ}   (U (S x) val) = Right (U x val)
split {prf = RS p} (U Z     val) = Right (U Z val)
split {prf = RS p} (U (S x) val) = case split {prf = p} (U x val) of
  Left vt        => Left vt
  Right (U ix y) => Right $ U (S ix) y

handle :  Applicative f
       => Rem t ts rem
       => (h : t -> f (Err rem a))
       -> Err ts a
       -> f (Err rem a)
handle h (Left x)  = case split x of
  Left v    => h v
  Right err => pure $ Left err
handle _ (Right x) = pure $ Right x

--------------------------------------------------------------------------------
--          Tests
--------------------------------------------------------------------------------

EmployeeSchema : Schema
EmployeeSchema = [ "firstName"  :> Str
                 , "lastName"   :> Str
                 , "email"      :> Str
                 , "age"        :> I64
                 , "salary"     :> Float
                 , "management" :> Boolean
                 ]

0 Employee : Type
Employee = Row EmployeeSchema

hock : Employee
hock = [ "Stefan", "Höck", "hock@foo.com", 46, 5443.2, False ]

shoeck : String
shoeck = getAt "firstName" hock ++ " " ++ getAt "lastName" hock

shoeck2 : String
shoeck2 = case getAll ["firstName", "lastName", "age"] hock of
  [fn,ln,a] => "\{fn} \{ln}: \{show a} years old."

embedTest :  Err [Nat,Bits8] a
          -> Err [String, Bits8, Int32, Nat] a
embedTest = mapFst embed


text:
import Control.Linear.LIO

foo : LinearIO io => L io ()
foo = do putStrLn "Hello"
         putStrLn "World"

data DoorState = CLOSED | OPEN

data OpenResult = Jammed | OK

data Door : DoorState -> Type where

newDoor : LinearIO io => (1 _ : (1 _ : Door CLOSED) -> L io ()) -> L io ()

openDoor : LinearIO io =>
           (1 _ : Door CLOSED) ->
           L io {use=1} (Res OpenResult (\case
                                           Jammed => Door CLOSED
                                           OK => Door OPEN))

closeDoor : LinearIO io => (1 _ : Door OPEN) -> L io {use=1} (Door CLOSED)
deleteDoor : LinearIO io => (1 _ : Door CLOSED) -> L io ()

doorProg : LinearIO io => L io ()
doorProg
    = newDoor $ \d =>
         do ok # d <- openDoor d
            case ok of
                 Jammed => deleteDoor d
                 OK => do d <- closeDoor d
                          putStrLn "Yay"
                          deleteDoor d


text:
labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith lbl [] = []
labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals

label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)


text:
module MultipleClientsServer

import System.Concurrency.Channels
import public Network.Socket

recMessages : (sock : Socket) -> (ip : SocketAddress) -> IO ()
recMessages sock ip = do Right (str, res) <- recv sock 1024  | Left err => putStrLn (show err)
                         putStrLn $ (show ip) ++ " send: " ++ str
                         putStrLn $ "Sending back: " ++ str
                         Right ok <- send sock $ str | Left err => putStrLn (show err)
                         recMessages sock ip

listenForClients : (sock : Socket) -> IO ()
listenForClients sock = do putStrLn $ "Listening for clients...."
                           Right (newSock, newIp) <- accept sock | Left err => putStrLn (show err)
                           putStrLn $ "Socket accepted connection from: " ++ (show newIp)
                           spawn (recMessages newSock newIp)
                           listenForClients sock

serverbound : (sock : Socket) -> (ok : Int) -> (ip : SocketAddress) -> (port : Port) -> IO ()
serverbound sock ok ip port = do putStrLn $ "Socket is bound to: " ++ (show ip) ++ ":" ++ (show port)
                                 listeningCode <- listen sock
                                 listenForClients sock

servererr : (sock : Socket) -> (ok : Int) -> IO ()
servererr sock ok = putStrLn $ "Server failed" ++ (show ok)

startServer : IO ()
startServer = do Right sock <- socket AF_INET Stream 0 | Left err => putStr (show err)
                 putStrLn "Socket created"
                 ip <- pure (IPv4Addr 192 168 87 189)
                 port <- pure (the (Port) 9420)
                 ok <- bind sock (Just ip) port
                 if ok == 0 then (serverbound sock ok ip port)
                            else (servererr sock ok)

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module Chapter2

||| Calculate the average length of words in a string
||| @str a string containing words separated by whitespace
export
average : (str : String) -> Double
average str = let num_words = word_count str
                  total_length = sum (word_lengths (words str)) in
                  cast total_length / cast num_words
where
  word_count : String -> Nat
  word_count str = length (words str)

  word_lengths : List String -> List Nat
  word_lengths strs = map length strs

showAverage : String -> String
showAverage str = "The average word length is: " ++
                   show (average str) ++ "\n"

palindrome : Nat -> String -> Bool
palindrome nat str = if ((length str) > nat) then (toLower str) == (reverse (toLower str)) else False

counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

top_ten : Ord a => List a -> List a
top_ten lst = take 10 $ reverse $ sort lst

over_length : Nat -> List String -> Nat
over_length nat lst = length $ filter (\s => (length s) > nat) lst

main : IO ()
main = repl "Enter a string: " showAverage

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module AssRecRule

import Data.Fin
import Data.Vect

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (y :: ys) = step y ys (recList a x base step ys)

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.

Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f x = recList a (List b) [] step x where
  step = \y : a => \ys : List a => \result : List b => (f y) :: result

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3

Note: Define using `recList` and without pattern matching on lists.
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op y = recList a a init step y where
  step = \y : a => \ys : List a => \result : a => op y result

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin _ _ _ Z FZ impossible
inducFin _ _ _ Z FS impossible
inducFin xs base step (S k) FZ = base k
inducFin xs base step (S k) (FS j) = step k j (inducFin xs base step k j)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`
-}
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j v = inducFin xs base step q j v where
  xs : (n : Nat) -> Fin n -> Type
  xs q j = Vect q a -> a
  base : (m : Nat) -> xs (S m) FZ
  base m = f where
    f (x :: xs) = x
  step : (p : Nat) -> (k : Fin p) -> (prev : xs p k) -> (xs (S p) (FS k))
  step p k prev (y :: ys) = prev ys


text:
-- ----------------------------------------------------------------- [ XML.idr ]
-- Module    : XML.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Freyja.Convert.XML

import Effects
import Effect.State

import Data.AVL.Dict
import Data.DList
import Data.DList.Eff

import Edda
import Edda.Writer.Org

import GRL.Lang.GLang

import XML.DOM

import Freyja

-- -------------------------------------------------------------- [ Directives ]

%access private
%default partial

-- ------------------------------------------------------------------- [ Utils ]

addNameDesc : EddaString
           -> EddaBody
           -> XMLElem
           -> XMLElem
addNameDesc n d e = e
    <++> ("description" <+=> concatMap block d)
    <++> ("name" <+=> inlines n)

convertMany : String
           -> String
           -> (a -> String)
           -> List a
           -> XMLElem
convertMany p c f ns = foldl doFold (mkNode p) ns
  where
    doFold : XMLElem -> a -> XMLElem
    doFold p t = p <++> (mkNode c <=> (f t))

convertEList : String -> String -> List EddaString -> XMLElem
convertEList o i Nil = mkNode o <++> (mkNode i <=> "Fill me in")
convertEList o i cs  = convertMany o i inlines cs

-- ---------------------------------------------------------------- [ Metadata ]

convertMData : Metadata -> XMLElem
convertMData mdata = setAttribute "id" (ident mdata) $
        mkNode "metadata"
  <++> (convertEList "auditors" "auditor" (auditors mdata))
  <++> (convertEList "tags"     "tag"     (tags mdata))
  <++> (convertEList "authors"  "author"  (authors mdata))
  <++> (convertEList "auditors" "auditor" (auditors mdata))
  <++> ("evaluated" <+=> (evaluated mdata))
  <++> ("modified"  <+=> (modified mdata))
  <++> ("created"  <+=> (created mdata))

-- ----------------------------------------------------------------- [ Studies ]

convertStudies : List Study -> Document ELEMENT
convertStudies = foldl (mkStudy) (mkNode "studies")
  where
    mkStudy : XMLElem -> Study -> XMLElem
    mkStudy p (MkStudy n b a) =
      p <++> (mkNode "study"
             <++> ("after"  <+=> concatMap block a)
             <++> ("before" <+=> concatMap block b)
             <++> ("name"   <+=> inlines n))

-- ------------------------------------------------------------------ [ Models ]

convertModel : Model ty -> XMLElem
convertModel (MkModel n ty d m) =
         setAttribute "modelTy" "unknown" $
         mkNode (tname ty)
    <++> (mkNode "model" <++> CData m)
    <++> ("description" <+=> concatMap block d)
    <++> ("name" <+=> inlines n)

  where
    tname : MTy -> String
    tname STRUCT = "structure"
    tname DYN    = "dynamic"

convertModels : DList MTy Model ms -> XMLElem
convertModels = DList.foldl (doConvert) (mkNode "models")
  where
    doConvert : XMLElem -> Model ty -> XMLElem
    doConvert p m = p <++> (convertModel m)

-- ----------------------------------------------------------------- [ Context ]

convertContext : Context -> XMLElem
convertContext (MkContext n d) = addNameDesc n d (mkNode "context")

-- --------------------------------------------------------------- [ Relations ]

convertRelations : DList.DList LTy Relation rs -> XMLElem
convertRelations = DList.foldl doConvert (mkNode "relations")
  where
    doConvert : XMLElem -> Relation ty -> XMLElem
    doConvert doc (MkRelation ty i Nothing) = doc <++>
        (setAttribute "patternID" i (mkNode (cast ty)))
    doConvert doc (MkRelation ty i (Just d)) = doc <++>
        (setAttribute "patternID" i (mkNode (cast ty)))
          <=> (concatMap block d)

-- --------------------------------------------------------------------- [ XML ]

XEffs : List EFFECT
XEffs = [STATE (Nat, Dict String Nat)]

convertReq : Requirement ty -> Eff (XMLElem) XEffs
convertReq (MkReq ty n d) = do
    let r = mkNode (cast ty)
    (idGen,_) <- get
    let idVal = cast {to=Int} (S idGen)
    let e = setAttribute "id" (cast idVal) r
    update (\(idGen,ids) => ((S idGen), insert (inlines n) (S idGen) ids))
    pure $ addNameDesc n d e

convertProblem : Problem -> Eff (XMLElem) XEffs
convertProblem (MkProblem n d rs) = do
       let e = mkNode "problem"
       rsC <-  mapDListE (\r => convertReq r) rs
       let rNodes = Foldable.foldr
                       (\r,n => n <++> r)
                       (mkNode "requirements")
                       rsC
       pure $ addNameDesc n d (e <++> rNodes)

convertAffect : Affect -> Eff (XMLElem) XEffs
convertAffect (MkAffect c r d) = do
       (_,ids) <- get
       let id = Dict.lookup (inlines $ name r) ids
       let e = case d of
           Nothing => mkNode "affect"
           Just xs => "affect" <+=> concatMap block xs
       let idval = cast {to=Int} $ fromMaybe 0 id
       pure $ (setAttribute "cvalue" (cast c)
              (setAttribute "id" (cast idval) e))

convertTrait : Trait ty -> Eff (XMLElem) XEffs
convertTrait (MkTrait ty n d s as) = do
       let e  = mkNode (toLower $ show ty)
       let e' = setAttribute "svalue" (cast s) e
       -- <mess>
       asC <- mapE (\a => convertAffect a) as
       let rNodes = foldr (\r,n => n <++> r) (mkNode "affects") asC
       -- </mess>
       pure $ addNameDesc n d $ (e' <++> (rNodes))

convertProperty : Property -> Eff (XMLElem) XEffs
convertProperty (MkProperty n d ts) = do
       let e = mkNode "property"
       -- <mess>
       tsC <- mapDListE (\t => convertTrait t) ts
       let rNodes = foldr (\r,n => n <++> r) (mkNode "traits") tsC
       -- </mess>
       pure $ addNameDesc n d (e <++> rNodes)

convertSolution : Solution -> Eff (XMLElem) XEffs
convertSolution (MkSolution n d ms ps) = do
       let e = mkNode "solution"
       -- <mess>
       psC <- mapE (\p => convertProperty p) ps
       let rNodes = foldr (\r,n => n <++> r) (mkNode "properties") psC
       -- </mess>
       let mNodes = convertModels ms

       pure $ addNameDesc n d $ (e <++> rNodes <++> mNodes)

convertPattern : PatternDoc -> Eff (XMLElem) XEffs
convertPattern p = do
    pnode <- convertProblem (problem p)
    snode <- convertSolution (solution p)
    pure $ mkNode "pattern"
       <++> (convertRelations (relations p))
       <++> (convertStudies (studies p))
       <++> ("evidence" <+=> concatMap block (evidence p))
       <++> snode
       <++> pnode
       <++> (convertContext (context p))
       <++> (convertMData (mdata p))
       <++> ("description" <+=> concatMap block (summary p))
       <++> ("name" <+=> inlines (name p))

namespace Freyja
  export
  toXML : PatternDoc -> XMLDoc
  toXML p =  mkDocument root
    where
      partial
      root : XMLElem
      root = runPureInit [(Z,Dict.empty)] (convertPattern p)

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module Prelude.Enum

import Data.List
import Data.Nat

export
Cast Int Nat where
  cast i = fromInteger (cast i)

export
Cast Integer Nat where
  cast = fromInteger

export
natRange : Nat -> List Nat
natRange n = List.reverse (go n)
  where go : Nat -> List Nat
        go Z = []
        go (S n) = n :: go n

-- predefine Nat versions of Enum, so we can use them in the default impls
export
countFrom : Num n => n -> n -> Stream n
countFrom start diff = start :: countFrom (start + diff) diff

export total
natEnumFromThen : Nat -> Nat -> Stream Nat
natEnumFromThen n next = countFrom n (minus next n)

export total
natEnumFromTo : Nat -> Nat -> List Nat
natEnumFromTo n m = if n <= m
                    then go n m
                    else List.reverse $ go m n
  where go : Nat -> Nat -> List Nat
        go n m = map (plus n) (natRange (minus (S m) n))

export total
natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat
natEnumFromThenTo' _ Z       _ = []
natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))

export total
natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
natEnumFromThenTo n next m = if n == m then [n]
                             else if n < m then natEnumFromThenTo' n (minus next n) m
                             else case minus n next of
                                  Z => []
                                  S step => List.reverse . map (+ (modNatNZ (minus n m) (S step) SIsNotZ)) $ natEnumFromThenTo' m (minus n next) n
    where modNatNZ : Nat -> (m : Nat) -> Not (m = 0) -> Nat
          modNatNZ n m nz = minus n $ mult m $ divNatNZ n m nz

public export
interface Enum a where
  total pred : a -> a
  total succ : a -> a
  succ e = fromNat (S (toNat e))
  total toNat : a -> Nat
  total fromNat : Nat -> a
  total enumFrom : a -> Stream a
  enumFrom n = n :: enumFrom (succ n)
  total enumFromThen : a -> a -> Stream a
  enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
  total enumFromTo : a -> a -> List a
  enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
  total enumFromThenTo : a -> a -> a -> List a
  enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))

public export
Enum Nat where
  pred n = Nat.pred n
  succ n = S n
  toNat x = id x
  fromNat x = id x
  enumFromThen x y = natEnumFromThen x y
  enumFromThenTo x y z = natEnumFromThenTo x y z
  enumFromTo x y = natEnumFromTo x y

public export
Enum Integer where
  pred n = n - 1
  succ n = n + 1
  toNat n = cast n
  fromNat n = cast n
  enumFromThen n inc = countFrom n (inc - n)
  enumFromTo n m = if n <= m
                   then go n m
                   else List.reverse $ go m n
    where go' : Integer -> List Nat -> List Integer
          go' _ [] = []
          go' n (x :: xs) = n + cast x :: go' n xs
          go : Integer -> Integer -> List Integer
          go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
  enumFromThenTo n next m = if n == m then [n]
                            else if next - n == 0 || (next - n < 0) /= (m - n < 0) then []
                            else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
    where go : List Nat -> List Integer
          go [] = []
          go (x :: xs) = n + (cast x * (next - n)) :: go xs

public export
Enum Int where
  pred n = n - 1
  succ n = n + 1
  toNat n = cast n
  fromNat n = cast n
  enumFromTo n m = if n <= m
                   then go n m
                   else List.reverse $ go m n
    where go' : List Int -> Nat -> Int -> List Int
          go' acc Z     m = m :: acc
          go' acc (S k) m = go' (m :: acc) k (m - 1)
          go : Int -> Int -> List Int
          go n m = go' [] (cast {to = Nat} (m - n)) m
  enumFromThen n inc = countFrom n (inc - n)

  enumFromThenTo n next m = if n == m then [n]
                            else if next - n == 0 || (next - n < 0) /= (m - n < 0) then []
                            else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
    where go : List Nat -> List Int
          go [] = []
          go (x :: xs) = n + (cast x * (next - n)) :: go xs

public export
Enum Char where
  toNat c   = toNat (fromInteger $ cast c)
  fromNat n = cast (cast n {to=Int})

  pred c = fromNat (pred (toNat c))

-- syntax "[" [start] ".." [end] "]"
--      = enumFromTo start end
-- syntax "[" [start] "," [next] ".." [end] "]"
--      = enumFromThenTo start next end

-- syntax "[" [start] ".." "]"
--      = enumFrom start
-- syntax "[" [start] "," [next] ".." "]"
--      = enumFromThen start next

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Value

import public Data.SortedMap
import Data.List
import Data.String

public export
Key : Type
Key = String

mutual
    public export
    data Value
        = VString String
        | VInteger Integer
        | VFloat Double
        | VBoolean Bool
        | VArray (List Value)
        | VTable Table

    public export
    Table : Type
    Table = SortedMap Key Value

export
lookupNested : (key : List String) -> (table : Table) -> Maybe Value
lookupNested [] table = Nothing
lookupNested [x] table = lookup x table
lookupNested (x :: xs) table = do
    VTable t <- lookup x table
        | _ => Nothing
    lookupNested xs t

public export
Eq Value where
    (VString x) == (VString y) = x == y
    (VInteger x) == (VInteger y) = x == y
    (VFloat x) == (VFloat y) = x == y
    (VBoolean x) == (VBoolean y) = x == y
    (VArray xs) == (VArray ys) = assert_total $ xs == ys
    (VTable x) == (VTable y) = assert_total $ SortedMap.toList x == SortedMap.toList y
    _ == _ = False

    a /= b = not $ (assert_total (==)) a b

public export
Show Value where
    show (VString x) = show x
    show (VInteger x) = show x
    show (VFloat x) = show x
    show (VBoolean True) = "true"
    show (VBoolean False) = "false"
    show (VArray xs) = "["
        ++ fastConcat (intersperse ", " $ map (assert_total show) xs)
        ++ "]"
    show (VTable x) =
        let kvs = the (List (Key, Value)) $ toList x in
        "{"
        ++ fastConcat (intersperse ", " . flip map kvs $ \(k, v) =>
                            show k ++ " = " ++ assert_total show v
                        )
        ++ "}"

export
[Raw] Show Value where
    show (VString x) = "string \{show x}"
    show (VInteger x) = "integer \{show x}"
    show (VFloat x) = "float \{show x}"
    show (VBoolean x) = if x then "bool true" else "bool false"
    show (VArray xs) = "list [\{concat $ intersperse ", " $ map (assert_total show) xs}]"
    show (VTable x) =
        let kvs = SortedMap.toList x in
            "{\{fastConcat (intersperse ", " . flip map kvs $ \(k, v) =>
                            show k ++ " = " ++ assert_total show v
                        )}}"

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
-- Prototype of NonDTRealizedFunction as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e

module NonDTRealizedFunction

import public NonDTRealizedAttributes

public export
record NonDTRealizedFunction a where
  constructor MkNonDTRealizedFunction
  function : a
  attributes : NonDTRealizedAttributes

-- Perform the composition between 2 realized functions.  The
-- resulting realized function is formed as follows:
--
-- 1. Composed lifted functions
-- 2. Costs are added
-- 3. Minimum quality is retained
--
-- For now only the IO types of the functions are dependent types, not
-- the attribtes.
public export
compose : (NonDTRealizedFunction (b -> c)) ->
          (NonDTRealizedFunction (a -> b)) ->
          (NonDTRealizedFunction (a -> c))
compose rlz_f rlz_g = MkNonDTRealizedFunction rlz_fg fg_attrs where
  rlz_fg : a -> c
  rlz_fg = rlz_f.function . rlz_g.function
  fg_attrs : NonDTRealizedAttributes
  fg_attrs = add_costs_min_quality rlz_f.attributes rlz_g.attributes

-- Perform function application over realized functions.  Maybe we'd
-- want to used some funded data, as defined in FndType.
public export
apply : NonDTRealizedFunction (a -> b) -> a -> b
apply rlz_f = rlz_f.function

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
||| Utilities for dealing with %nomangle functions
module Compiler.NoMangle

import Core.Core
import Core.Context
import Libraries.Data.NameMap
import Libraries.Data.NameMap.Traversable

export
record NoMangleMap where
    constructor MkNMMap
    map : NameMap (Maybe String)

findNoMangle : List DefFlag -> Maybe NoMangleDirective
findNoMangle [] = Nothing
findNoMangle (NoMangle x :: _) = Just x
findNoMangle (_ :: xs) = findNoMangle xs

||| Get a map of all %nomangle names
||| Errors for all invalid names, so the backend can skip checking
||| or adding escape characters.
||| @ backend what backend is this being used in?
||| @ valid a validator to check a name is valid
|||         for the given backend
export
initNoMangle :
    {auto d : Ref Ctxt Defs} ->
    (backend : String) ->
    (valid : String -> Bool) ->
    Core (Ref NoMangleMap NoMangleMap)
initNoMangle backend valid = do
    defs <- get Ctxt
    let ctxt = defs.gamma
    map <- traverseNameMap
        (\nm, res => do
            Just gdef <- lookupCtxtExact (Resolved res) ctxt
                | Nothing => pure Nothing
            let Just ns = findNoMangle gdef.flags
                | Nothing => pure Nothing
            name <- case ns of
                CommonName name => pure name
                BackendNames ns =>
                    maybe
                        (throw (InternalError "missing %nomangle name for \{show nm} on \{backend} backend"))
                        pure
                        (lookupBackend ns)
            let True = valid name
                | False => throw (InternalError "\{show name} is not a valid name on the \{backend} backend")
            pure $ Just name
        ) ctxt.resolvedAs
    newRef NoMangleMap $ MkNMMap map
  where
    lookupBackend : List (String, String) -> Maybe String
    lookupBackend [] = Nothing
    lookupBackend ((b, n) :: ns) = if b == backend then Just n else lookupBackend ns

export
isNoMangle : NoMangleMap -> Name -> Maybe String
isNoMangle nm n = join $ lookup n nm.map

export
lookupNoMangle :
    {auto nm : Ref NoMangleMap NoMangleMap} ->
    Name ->
    Core (Maybe String)
lookupNoMangle n = pure $ isNoMangle !(get NoMangleMap) n

export
getAllNoMangle : {auto c : Ref Ctxt Defs} -> Core (List Name)
getAllNoMangle = do
    defs <- get Ctxt
    foldlNames (addNames defs) (pure []) defs.gamma.resolvedAs
  where
    addNames : Defs -> Core (List Name) -> Name -> Int -> Core (List Name)
    addNames defs acc _ res = do
        Just gdef <- lookupCtxtExact (Resolved res) defs.gamma
            | Nothing => acc
        let Just name = findNoMangle gdef.flags
            | Nothing => acc
        ns <- acc
        pure $ (Resolved res) :: ns