text:
module Examples.AuthorityLattice

import public DepSec.Lattice

%access public export
%default total

data Principal : Type where
  Top : Principal
  Alice : Principal
  Bob : Principal
  Chuck : Principal
  Bot : Principal

implementation JoinSemilattice Principal where
  join Top b = Top
  join Alice Top =Top
  join Alice Alice = Alice
  join Alice Bob = Top
  join Alice Chuck = Top
  join Alice Bot = Alice
  join Bob Top = Top
  join Bob Alice = Top
  join Bob Bob = Bob
  join Bob Chuck = Top
  join Bob Bot = Bob
  join Chuck Top = Top
  join Chuck Alice = Top
  join Chuck Bob = Top
  join Chuck Chuck = Chuck
  join Chuck Bot = Chuck
  join Bot b = b

  associative Top b c = Refl
  associative Alice Top c = Refl
  associative Alice Alice Top = Refl
  associative Alice Alice Alice = Refl
  associative Alice Alice Bob = Refl
  associative Alice Alice Chuck = Refl
  associative Alice Alice Bot = Refl
  associative Alice Bob Top = Refl
  associative Alice Bob Alice = Refl
  associative Alice Bob Bob = Refl
  associative Alice Bob Chuck = Refl
  associative Alice Bob Bot = Refl
  associative Alice Chuck Top = Refl
  associative Alice Chuck Alice = Refl
  associative Alice Chuck Bob = Refl
  associative Alice Chuck Chuck = Refl
  associative Alice Chuck Bot = Refl
  associative Alice Bot c = Refl
  associative Bob Top c = Refl
  associative Bob Alice Top = Refl
  associative Bob Alice Alice = Refl
  associative Bob Alice Bob = Refl
  associative Bob Alice Chuck = Refl
  associative Bob Alice Bot = Refl
  associative Bob Bob Top = Refl
  associative Bob Bob Alice = Refl
  associative Bob Bob Bob = Refl
  associative Bob Bob Chuck = Refl
  associative Bob Bob Bot = Refl
  associative Bob Chuck Top = Refl
  associative Bob Chuck Alice = Refl
  associative Bob Chuck Bob = Refl
  associative Bob Chuck Chuck = Refl
  associative Bob Chuck Bot = Refl
  associative Bob Bot c = Refl
  associative Chuck Top c = Refl
  associative Chuck Alice Top = Refl
  associative Chuck Alice Alice = Refl
  associative Chuck Alice Bob = Refl
  associative Chuck Alice Chuck = Refl
  associative Chuck Alice Bot = Refl
  associative Chuck Bob Top = Refl
  associative Chuck Bob Alice = Refl
  associative Chuck Bob Bob = Refl
  associative Chuck Bob Chuck = Refl
  associative Chuck Bob Bot = Refl
  associative Chuck Chuck Top = Refl
  associative Chuck Chuck Alice = Refl
  associative Chuck Chuck Bob = Refl
  associative Chuck Chuck Chuck = Refl
  associative Chuck Chuck Bot = Refl
  associative Chuck Bot c = Refl
  associative Bot b c = Refl

  commutative Top Top = Refl
  commutative Top Alice = Refl
  commutative Top Bob = Refl
  commutative Top Chuck = Refl
  commutative Top Bot = Refl
  commutative Alice Top = Refl
  commutative Alice Alice = Refl
  commutative Alice Bob = Refl
  commutative Alice Chuck = Refl
  commutative Alice Bot = Refl
  commutative Bob Top = Refl
  commutative Bob Alice = Refl
  commutative Bob Bob = Refl
  commutative Bob Chuck = Refl
  commutative Bob Bot = Refl
  commutative Chuck Top = Refl
  commutative Chuck Alice = Refl
  commutative Chuck Bob = Refl
  commutative Chuck Chuck = Refl
  commutative Chuck Bot = Refl
  commutative Bot Top = Refl
  commutative Bot Alice = Refl
  commutative Bot Bob = Refl
  commutative Bot Chuck = Refl
  commutative Bot Bot = Refl

  idempotent Top = Refl
  idempotent Alice = Refl
  idempotent Bob = Refl
  idempotent Chuck = Refl
  idempotent Bot = Refl

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Main

import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) -> (items : Vect size String) -> DataStore

data Command = Add String
             | Search String
             | Get Integer
             | Size
             | Quit

size : DataStore -> Nat
size (MkData size' items) = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) y = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [y]
    addToData (x :: xs) = x :: addToData xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp = let val = cast inp in
          if val < 0
             then Nothing
             else let newVal = tot + val in
                      Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = if all isDigit (unpack val) then Just (Get (cast val)) else Nothing
parseCommand "search" str = Just (Search str)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ args = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (ind : Integer) -> (ds : DataStore) -> Maybe (String, DataStore)
getEntry ind ds = let storeItems = items ds in
                      (case (integerToFin ind (size ds)) of
                            Nothing => Just ("Out of bounds \n", ds)
                            (Just x) => Just (index x storeItems ++ "\n", ds))

searchForEntry : (str : String) -> (ds : DataStore) -> Maybe (String, DataStore)
searchForEntry "" ds = Just ("", ds)
searchForEntry str ds = let storeItems = items ds
                            filteredPair = Data.Vect.filter (isInfixOf str) storeItems
                            filteredItems = snd filteredPair
                            resultString = foldl (\acc, x => acc ++ getIndex x storeItems ++ ": " ++ x ++ "\n") "" filteredItems in
                            Just (resultString, ds)
                        where getIndex : String -> Vect m String -> String
                              getIndex x storeItems = fromMaybe "0" $ (map show (map finToNat $ elemIndex x storeItems))

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput ds inp = case parse inp of
                           Nothing => Just ("Invalid command inputed\n", ds)
                           (Just x) => (case x of
                                             (Add item) => Just ("ID " ++ show (size ds) ++ "\n", addToStore ds item)
                                             (Get ind) => getEntry ind ds
                                             (Search str) => searchForEntry str ds
                                             Size => Just ("Size Of Datastore: " ++ show (size ds) ++ "\n", ds)
                                             Quit => Nothing)

main : IO ()
main = replWith (MkData _ []) "Command: " processInput

ext: idr


text:
module Elabs
import Language.Reflection.Elab

%language ElabReflection
-- https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr

addTypeDecl : Elab ()
addTypeDecl = do
  let tname : TTName = `{{GenData}}
  declareDatatype $ Declare tname []  RType
  defineDatatype $ DefineDatatype tname []

%runElab addTypeDecl

genTypeTest : GenData -> ()
genTypeTest x = ()

-- https://github.com/idris-lang/Idris-dev/blob/a02bfec13cbb6a49d553d33b61ca44ff2d83c9a7/test/meta002/DataDef.idr
addTypeDecl2 : Elab ()
addTypeDecl2 = do
  declareDatatype $ Declare `{{N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
  defineDatatype $ DefineDatatype `{{N}} [
           Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] (RApp (Var `{{N}}) (Var `{{x}})),
           Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] (RApp (Var `{{N}}) (RApp (Var `{S}) (Var `{{x}})))]

%runElab addTypeDecl2
--N : Nat -> Type
one : N 1
one = MkN

two : N 2
two = MkN' 1

--  generate lambdas
idNat : Nat -> Nat
idNat = %runElab (do intro `{{x}}
                     fill (Var `{{x}})
                     solve)

addFunDecls : Elab ()
addFunDecls = do
  declareType $ Declare `{{fun1}} [] `(() -> ())
  defineFunction $ DefineFun `{{fun1}} [MkFunClause `(()) `(())]

%runElab addFunDecls

fun2 : ()->()
fun2 = fun1

addImplsShow : Elab ()
addImplsShow = do
--  let instn = NS (SN $ ImplementationN `{Show} [show `{{a}}]) !currentNamespace
  addImplementation `{Show} `{{x}} -- x is placeholder,  not working yet!

-- An Elab script to insert plus Z (S Z)
isrt : Elab ()
isrt = do
  [x, y] <- apply `(plus) [False, False]
  solve
  focus x; fill `(Z); solve
  focus y; fill `(S Z); solve

max_stars_repo_name: idris-industry/paradise

max_issues_repo_name: idris-industry/paradise

max_forks_repo_name: idris-industry/paradise


text:
module Data.SnocList.Elem

import Data.SnocList
import Decidable.Equality

||| A proof that some element is found in a list.
public export
data Elem : a -> SnocList a -> Type where
  ||| A proof that the element is at the head of the list
  Here : Elem x (sx :< x)
  ||| A proof that the element is in the tail of the list
  There : Elem x sx -> Elem x (sx :< y)

export
Uninhabited (Here = There e) where
  uninhabited Refl impossible

export
Uninhabited (There e = Here) where
  uninhabited Refl impossible

export
Uninhabited (Elem {a} x [<]) where
  uninhabited Here impossible
  uninhabited (There p) impossible

export
thereInjective : {0 e1, e2 : Elem x sx} -> There e1 = There e2 -> e1 = e2
thereInjective Refl = Refl

export
DecEq (x `Elem` sx) where
  decEq Here Here = Yes Refl
  decEq Here (There _) = No absurd
  decEq (There _) Here = No absurd
  decEq (There y) (There z) with (decEq y z)
    decEq (There y) (There y) | Yes Refl = Yes Refl
    decEq (There y) (There z) | No neq = No $ neq . thereInjective

||| Remove the element at the given position.
public export
dropElem : (sx : SnocList a) -> (p : Elem x sx) -> SnocList a
dropElem (sy :< _) Here = sy
dropElem (sy :< y) (There p) = (dropElem sy p) :< y

||| Erase the indices, returning the numeric position of the element
public export
elemToNat : Elem x sx -> Nat
elemToNat Here = Z
elemToNat (There p) = S (elemToNat p)

||| Find the element with a proof at a given position (in reverse), if it is valid
public export
indexElem : Nat -> (sx : SnocList a) -> Maybe (x ** Elem x sx)
indexElem _ [<] = Nothing
indexElem Z (_ :< y) = Just (y ** Here)
indexElem (S k) (sy :< _) = (\(y ** p) => (y ** There p)) `map` (indexElem k sy)

||| Lift the membership proof to a mapped list
export
elemMap : (0 f : a -> b) -> Elem x sx -> Elem (f x) (map f sx)
elemMap f Here = Here
elemMap f (There el) = There $ elemMap f el

||| An item not in the head and not in the tail is not in the list at all.
export
neitherHereNorThere : Not (x = y) -> Not (Elem x sx) -> Not (Elem x (sx :< y))
neitherHereNorThere xny _ Here = xny Refl
neitherHereNorThere _ xnxs (There xxs) = xnxs xxs


text:
module Libra.Data

import Data.Vect

import Libra.Constants

%access public export -- data constructors :)
%default total

{-
  Proofs
-}

||| Proof builder ensuring all characters in a list are Alphanumeric
|||
||| @cs A list of possibly alphanumeric characters
allAlphanumeric : (cs : List Char) -> Type
allAlphanumeric [] = Elem True [True]
allAlphanumeric (c :: cs) = case c `isElem` Alphanumeric of
                                Yes prf => allAlphanumeric cs
                                No contra => Elem c Alphanumeric

{-
  Types
-}

||| The empty atom
data Empty : Type where
  MkEmpty : Empty

||| The letter atom-part
data Letter : Char -> Type where
  MkLetter : (c : Char) -> { auto prf : Elem c Alphabet } -> Letter c

||| The number atom-part
data Number : Char -> Type where
  MkNumber : (n : Char) -> { auto prf : Elem n Digits } -> Number n

||| It's the smallest entity with resolvable meaning in Libra.
|||
||| Always starts with a letter and may contain an arbitrary number of
||| alphanumeric characters afterwards.
data Symbol : Type where
  MkSymbol : ( s : String ) ->
             { auto nonEmpty : NonEmpty (unpack s) } ->
             { auto headPrf : Elem (head (unpack s)) Alphabet } ->
             { auto tailPrf : allAlphanumeric (tail (unpack s)) } ->
             -- Considered using Data.Vect.Quantifiers.All but it was fairly
             -- slower.
             -- https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect/Quantifiers.idr#L70
             -- { auto tailPrf : All ?isAlphanumeric (fromList (tail (unpack s))) } ->
             Symbol

data SExpr : Type where
  -- temporary, figure out how to make parseSymbol _guarantee_ a call to
  -- MkName (MkSymbol name) -- with a non-empty name
  MkName  : String -> SExpr
  MkSExpr : List SExpr -> SExpr

partial toString : SExpr -> String
toString (MkName x) = x
toString (MkSExpr []) = "()"
toString (MkSExpr xs) = let
    body = (foldr (++) "" (intersperse " " (map toString xs)))
  in
    "(" ++ body ++ ")"

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module Compiler.LLVM.Rapid.Integer

import Data.Bits
import Data.Vect

import Compiler.LLVM.IR
import Compiler.LLVM.Instruction
import Compiler.LLVM.Rapid.Object
import Control.Codegen

GMP_LIMB_SIZE : Integer
GMP_LIMB_SIZE = 8

GMP_LIMB_BITS : Integer
GMP_LIMB_BITS = 8 * GMP_LIMB_SIZE

GMP_LIMB_BOUND : Integer
GMP_LIMB_BOUND = (1 `prim__shl_Integer` (GMP_LIMB_BITS))

-- To estimate required count of limbs (upper bound):
-- x = the number (result)
--   length of string == number of digits <= log10(x) + 1
--   required limbs: log10(x) / log10(2^LIMB_BITS)
--     LIMB_BITS=32 -> required limbs <= number of digits / 9
--     LIMB_BITS=64 -> required limbs <= number of digits / 19
GMP_ESTIMATE_DIGITS_PER_LIMB : Integer
GMP_ESTIMATE_DIGITS_PER_LIMB = 19

TARGET_SIZE_T : IRType
TARGET_SIZE_T = I64

MP_LIMB_T : IRType
MP_LIMB_T = I64

twosComplement : Num a => Bits a => a -> a
twosComplement x = 1 + (complement x)

export
cgMkConstInteger : Integer -> Codegen (IRValue IRObjPtr)
cgMkConstInteger val =
    do
      let absVal = abs val
      let (len ** limbs) = getLimbs absVal
      let len32 = cast {to=Bits32} $ cast {to=Int} len
      let lenForHeader = if (val >= 0) then len32 else (twosComplement len32)
      let newHeader = constHeader OBJECT_TYPE_ID_BIGINT lenForHeader
      let typeSignature = "{i64, [" ++ show len ++ " x %LimbT]}"
      cName <- addConstant $ "private unnamed_addr addrspace(1) constant " ++ typeSignature ++ " {" ++ toIR newHeader ++ ", [" ++ show len ++ " x %LimbT] [" ++ (getLimbsIR limbs) ++ "]}, align 8"
      pure $ SSA IRObjPtr $ "bitcast (" ++ typeSignature ++ " addrspace(1)* " ++ cName ++ " to %ObjPtr)"
  where
      getLimbs : Integer -> (n:Nat ** Vect n Integer)
      getLimbs 0 = (0 ** [])
      getLimbs x = let (n ** v) = (getLimbs (x `div` GMP_LIMB_BOUND))
                       limb = (x `mod` GMP_LIMB_BOUND) in
                       ((S n) ** (limb::v))
      getLimbsIR : Vect n Integer -> String
      getLimbsIR [] = ""
      getLimbsIR (limb::[]) = "%LimbT " ++ show limb
      getLimbsIR (limb::rest) = "%LimbT " ++ show limb ++ ", " ++ (getLimbsIR rest)

export
integer0 : Codegen (IRValue IRObjPtr)
integer0 = do
  newObj <- dynamicAllocate (Const I64 0)
  putObjectHeader newObj (constHeader OBJECT_TYPE_ID_BIGINT 0)
  pure newObj

export
cgMkIntegerSigned : IRValue I64 -> Codegen (IRValue IRObjPtr)
cgMkIntegerSigned val = do
  isNegative <- icmp "slt" val (Const I64 0)
  isZero <- icmp "eq" val (Const I64 0)
  newSize1 <- mkSelect isNegative (Const I32 (-1)) (Const I32 1)
  newSize <- mkSelect isZero (Const I32 0) newSize1
  newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT newSize
  newSizeAbs <- mkAbs newSize
  allocSize <- mkMul !(mkZext newSizeAbs) (Const I64 GMP_LIMB_SIZE)
  newObj <- dynamicAllocate allocSize
  ignore $ mkIf (pure isZero) (pure (Const I1 0)) (do
       absVal <- mkAbs64 val
       putObjectSlot newObj (Const I64 0) absVal
       pure $ Const I1 0)
  putObjectHeader newObj newHeader
  pure newObj

export
cgMkIntegerUnsigned : IRValue I64 -> Codegen (IRValue IRObjPtr)
cgMkIntegerUnsigned ival = do
  isZero <- icmp "eq" (Const I64 0) ival
  newObj <- mkIf (pure isZero) integer0 (do
      newInteger <- dynamicAllocate (Const I64 GMP_LIMB_SIZE)
      putObjectHeader newInteger !(mkHeader OBJECT_TYPE_ID_BIGINT (Const I32 1))
      putObjectSlot newInteger (Const I64 0) ival
      pure newInteger
    )
  pure newObj

export
unboxIntegerUnsigned : IRValue IRObjPtr -> Codegen (IRValue I64)
unboxIntegerUnsigned integerObj = do
  isZero <- icmp "eq" (Const I32 0) !(getObjectSize integerObj)
  -- get first limb (LSB)
  mkIf (pure isZero) (pure $ Const I64 0) (getObjectSlot {t=I64} integerObj 0)

export
unboxIntegerSigned : IRValue IRObjPtr -> Codegen (IRValue I64)
unboxIntegerSigned integerObj = do
  size <- getObjectSize integerObj
  isZero <- icmp "eq" (Const I32 0) size
  let isNegative = icmp "sgt" (Const I32 0) size
  -- get first limb (LSB)
  firstLimb <- getObjectSlot {t=I64} integerObj 0
  -- TODO: this is probably wrong for 64bit
  mkIf (pure isZero) (pure $ Const I64 0) (mkIf isNegative (mkSub (Const I64 0) firstLimb) (pure firstLimb))

||| compare two BigInts `a` and `b`, return -1 if a<b, +1 if a>b, 0 otherwise
export
compareInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue I64)
compareInteger obj1 obj2 = do
  size1 <- getObjectSize obj1
  size2 <- getObjectSize obj2
  cmpResult <- mkIf (icmp "slt" size1 size2) (pure (Const I64 (-1))) (
    mkIf (icmp "sgt" size1 size2) (pure (Const I64 1)) (do
         limbs1 <- getObjectPayloadAddr {t=I64} obj1
         limbs2 <- getObjectPayloadAddr {t=I64} obj2
         absSize <- mkZext {to=I64} !(mkAbs size1)
         mpnResult <- call {t=I32} "ccc" "@__gmpn_cmp" [toIR limbs1, toIR limbs2, toIR absSize]
         sizeIsNegative <- icmp "slt" size1 (Const I32 0)
         mkSext !(mkSelect sizeIsNegative !(mkSub (Const I32 0) mpnResult) mpnResult)
         )
         )

  pure cmpResult

normaliseIntegerSize : IRValue IRObjPtr -> IRValue I32 -> IRValue I1 -> Codegen ()
normaliseIntegerSize integerObj maxSizeSigned invert = do
  maxSizeAbs <- mkAbs maxSizeSigned
  absRealNewSize <- mkTrunc {to=I32} !(call {t=I64} "ccc" "@rapid_bigint_real_size" [
    toIR !(getObjectPayloadAddr {t=I64} integerObj),
    toIR !(mkZext {to=I64} maxSizeAbs)
    ])
  isNegative <- icmp "slt" maxSizeSigned (Const I32 0)
  invertResult <- mkXOr isNegative invert
  signedNewSize <- mkSelect invertResult !(mkSub (Const I32 0) absRealNewSize) absRealNewSize
  newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize
  putObjectHeader integerObj newHeader

export
addInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
addInteger i1 i2 = do
      s1 <- getObjectSize i1
      s2 <- getObjectSize i2
      i1Negative <- icmp "slt" s1 (Const I32 0)
      s1a <- mkAbs s1
      s2a <- mkAbs s2
      i1longer <- icmp "ugt" s1a s2a
      -- "big" and "small" refer just to the respective limb counts
      -- it doesn't matter which number is actually bigger
      big <- mkSelect i1longer i1 i2
      small <- mkSelect i1longer i2 i1
      size1 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s1a s2a)
      size2 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s2a s1a)
      newLength <- mkAdd size1 (Const I64 1)
      newSize <- mkMul (Const I64 GMP_LIMB_SIZE) newLength
      newObj <- dynamicAllocate newSize
      carry <- call {t=I64} "ccc" "@__gmpn_add" [
        toIR !(getObjectPayloadAddr {t=I64} newObj),
        toIR !(getObjectPayloadAddr {t=I64} big),
        toIR size1,
        toIR !(getObjectPayloadAddr {t=I64} small),
        toIR size2
        ]
      putObjectSlot newObj size1 carry
      absRealNewSize <- mkAdd size1 carry
      signedNewSize <- mkSelect i1Negative !(mkSub (Const I64 0) absRealNewSize) absRealNewSize
      signedNewSize32 <- mkTrunc {to=I32} signedNewSize
      newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
      putObjectHeader newObj newHeader
      pure newObj

export
subInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
subInteger i1 i2 = do
      -- Subtract the smaller (by abs. value) from the larger (by abs. value)
      -- and use the sign of the larger (by abs. value) number as sign for the
      -- returned result.
      s1 <- getObjectSize i1
      s2 <- getObjectSize i2
      i1Negative <- icmp "slt" s1 (Const I32 0)
      s1a <- mkAbs s1
      s2a <- mkAbs s2
      i1longer <- icmp "ugt" s1a s2a
      i2longer <- icmp "ugt" s2a s1a
      i1bigger <- mkIf (pure i1longer) (pure $ Const I1 1) (mkIf (pure i2longer) (pure $ Const I1 0) (icmp "sgt" !(call "ccc" "@__gmpn_cmp" [
                                toIR !(getObjectPayloadAddr {t=I64} i1),
                                toIR !(getObjectPayloadAddr {t=I64} i2),
                                toIR !(mkZext {to=I64} s1a)
                                ]) (Const I32 0))
        )
      big <- mkSelect i1bigger i1 i2
      small <- mkSelect i1bigger i2 i1
      swapped <- mkSelect i1bigger (Const I1 0) (Const I1 1)
      bigSize <- getObjectSize big
      bigSizeAbs <- mkAbs bigSize
      smallSizeAbs <- mkAbs !(getObjectSize small)
      newSize <- mkMul (Const I64 GMP_LIMB_SIZE) !(mkZext {to=I64} bigSizeAbs)
      newObj <- dynamicAllocate newSize
      absDiff <- call {t=I64} "ccc" "@__gmpn_sub" [
        toIR !(getObjectPayloadAddr {t=I64} newObj),
        toIR !(getObjectPayloadAddr {t=I64} big),
        toIR !(mkZext {to=I64} bigSizeAbs),
        toIR !(getObjectPayloadAddr {t=I64} small),
        toIR !(mkZext {to=I64} smallSizeAbs)
        ]
      absRealNewSize <- call {t=I64} "ccc" "@rapid_bigint_real_size" [
        toIR !(getObjectPayloadAddr {t=I64} newObj),
        toIR !(mkZext {to=I64} bigSizeAbs)
        ]
      resultIsNegative <- mkXOr swapped i1Negative
      signedNewSize <- mkSelect resultIsNegative !(mkSub (Const I64 0) absRealNewSize) absRealNewSize
      signedNewSize32 <- mkTrunc {to=I32} signedNewSize
      newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
      putObjectHeader newObj newHeader
      pure newObj

export
andInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
andInteger i1 i2 = do
  -- TODO: what to do with negative numbers?
  s1 <- getObjectSize i1
  s2 <- getObjectSize i2
  zero1 <- icmp "eq" s1 (Const I32 0)
  zero2 <- icmp "eq" s2 (Const I32 0)
  resultIsZero <- mkOr zero1 zero2

  mkIf (pure resultIsZero) (mkSelect zero1 i1 i2) (do
    s1a <- mkAbs s1
    s2a <- mkAbs s2
    i1longer <- icmp "ugt" s1a s2a
    -- "long" and "short" refer just to the respective limb counts
    -- it doesn't matter which number is actually bigger
    long <- mkSelect i1longer i1 i2
    short <- mkSelect i1longer i2 i1
    size1 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s1a s2a)
    size2 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s2a s1a)
    -- result can not be longer than shortest number
    let newLength = size2
    newSize <- mkMul (Const I64 GMP_LIMB_SIZE) newLength
    newObj <- dynamicAllocate newSize
    putObjectHeader newObj !(mkHeader OBJECT_TYPE_ID_BIGINT !(mkTrunc newLength))

    newLimbs <- getObjectPayloadAddr {t=I64} newObj
    shortLimbs <- getObjectPayloadAddr {t=I64} short
    longLimbs <- getObjectPayloadAddr {t=I64} long
    voidCall "ccc" "@__gmpn_and_n" [toIR newLimbs, toIR shortLimbs, toIR longLimbs, toIR newLength]

    normaliseIntegerSize newObj !(mkTrunc newLength) (Const I1 0)

    pure newObj
    )

export
orInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
orInteger i1 i2 = do
  -- TODO: what to do with negative numbers?
  s1 <- getObjectSize i1
  s2 <- getObjectSize i2
  zero1 <- icmp "eq" s1 (Const I32 0)
  zero2 <- icmp "eq" s2 (Const I32 0)
  resultIsZero <- mkAnd zero1 zero2

  mkIf (pure resultIsZero) (pure i1) (do
    s1a <- mkAbs s1
    s2a <- mkAbs s2
    i1longer <- icmp "ugt" s1a s2a
    -- "big" and "small" refer just to the respective limb counts
    -- it doesn't matter which number is actually bigger
    big <- mkSelect i1longer i1 i2
    small <- mkSelect i1longer i2 i1
    size1 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s1a s2a)
    size2 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s2a s1a)
    mkIf (icmp "eq" (Const I64 0) size2) (pure big) (do
      let newLength = size1
      newSize <- mkMul (Const I64 GMP_LIMB_SIZE) newLength
      newObj <- dynamicAllocate newSize
      putObjectHeader newObj !(mkHeader OBJECT_TYPE_ID_BIGINT !(mkTrunc newLength))

      newPayload <- getObjectPayloadAddr {t=I8} newObj
      bigPayload <- getObjectPayloadAddr {t=I8} big
      appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR newPayload ++ ", " ++ toIR bigPayload ++ ", " ++ toIR newSize++ ", i1 false)"

      newLimbs <- getObjectPayloadAddr {t=I64} newObj
      smallLimbs <- getObjectPayloadAddr {t=I64} small
      voidCall "ccc" "@__gmpn_ior_n" [toIR newLimbs, toIR newLimbs, toIR smallLimbs, toIR size2]
      pure newObj
      )
    )

export
xorInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
xorInteger i1 i2 = do
  -- TODO: what to do with negative numbers?
  s1 <- getObjectSize i1
  s2 <- getObjectSize i2
  zero1 <- icmp "eq" s1 (Const I32 0)
  zero2 <- icmp "eq" s2 (Const I32 0)
  resultIsUnchanged <- mkOr zero1 zero2

  mkIf (pure resultIsUnchanged) (mkSelect zero1 i2 i1) (do
    s1a <- mkAbs s1
    s2a <- mkAbs s2
    i1longer <- icmp "ugt" s1a s2a
    -- "long" and "short" refer just to the respective limb counts
    -- it doesn't matter which number is actually bigger
    long <- mkSelect i1longer i1 i2
    short <- mkSelect i1longer i2 i1
    size1 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s1a s2a)
    size2 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s2a s1a)
    -- result can not be longer than longest number
    let newLength = size1
    newSize <- mkMul (Const I64 GMP_LIMB_SIZE) newLength
    newObj <- dynamicAllocate newSize
    putObjectHeader newObj !(mkHeader OBJECT_TYPE_ID_BIGINT !(mkTrunc newLength))

    newPayload <- getObjectPayloadAddr {t=I8} newObj
    longPayload <- getObjectPayloadAddr {t=I8} long
    appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR newPayload ++ ", " ++ toIR longPayload ++ ", " ++ toIR newSize ++ ", i1 false)"

    newLimbs <- getObjectPayloadAddr {t=I64} newObj
    shortLimbs <- getObjectPayloadAddr {t=I64} short
    voidCall "ccc" "@__gmpn_xor_n" [toIR newLimbs, toIR newLimbs, toIR shortLimbs, toIR size2]

    normaliseIntegerSize newObj !(mkTrunc newLength) (Const I1 0)

    pure newObj
    )

export
mulInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
mulInteger i1 i2 = do
      s1 <- getObjectSize i1
      s2 <- getObjectSize i2
      zero1 <- icmp "eq" s1 (Const I32 0)
      zero2 <- icmp "eq" s2 (Const I32 0)
      resultIsZero <- mkOr zero1 zero2
      mkIf (pure resultIsZero) {- then -} integer0 {- else -} (do
        sx <- mkXOr s1 s2
        signsMatch <- icmp "sge" sx (Const I32 0)
        s1a <- mkAbs s1
        s2a <- mkAbs s2
        i1longer <- icmp "ugt" s1a s2a
        -- "big" and "small" refer just to the respective limb counts
        -- it doesn't matter which number is actually bigger
        big <- mkSelect i1longer i1 i2
        small <- mkSelect i1longer i2 i1
        size1 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s1a s2a)
        size2 <- mkZext {to=I64} !(mkSelect {t=I32} i1longer s2a s1a)
        newLength <- mkAdd size1 size2
        newSize <- mkMul (Const I64 GMP_LIMB_SIZE) newLength
        newObj <- dynamicAllocate newSize
        ignore $ call {t=I64} "ccc" "@__gmpn_mul" [
          toIR !(getObjectPayloadAddr {t=I64} newObj),
          toIR !(getObjectPayloadAddr {t=I64} big),
          toIR size1,
          toIR !(getObjectPayloadAddr {t=I64} small),
          toIR size2
          ]
        absRealNewSize <- call {t=I64} "ccc" "@rapid_bigint_real_size" [
          toIR !(getObjectPayloadAddr {t=I64} newObj),
          toIR newLength
          ]
        signedNewSize <- mkSelect signsMatch absRealNewSize !(mkSub (Const I64 0) absRealNewSize)
        signedNewSize32 <- mkTrunc {to=I32} signedNewSize
        newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
        putObjectHeader newObj newHeader
        pure newObj)

||| divide i1 by i2, return (quotient, remainder)
divInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr, IRValue IRObjPtr)
divInteger i1 i2 = do
  s1 <- getObjectSize i1
  s2 <- getObjectSize i2
  s1a <- mkZext !(mkAbs s1)
  s2a <- mkZext !(mkAbs s2)
  zero1 <- icmp "eq" s1 (Const I32 0)
  zero2 <- icmp "eq" s2 (Const I32 0)
  ignore $ mkIf (pure zero2) (do
                mkRuntimeCrash "division by 0"
                pure (Const I1 0)
                ) (pure (Const I1 0))

  retZeroLbl <- genLabel "ret0"
  checkDividendLbl <- genLabel "div_chk"
  dividendLargerLbl <- genLabel "div_lg"
  divLbl <- genLabel "div"
  endLbl <- genLabel "div_end"

  branch zero1 retZeroLbl checkDividendLbl

  beginLabel retZeroLbl
  zeroInteger <- integer0
  jump endLbl

  beginLabel checkDividendLbl
  dividendLarger <- icmp "ugt" s2a s1a
  branch dividendLarger dividendLargerLbl divLbl

  beginLabel dividendLargerLbl
  zeroQuotient <- integer0
  jump endLbl

  beginLabel divLbl
  -- i1, i2 /= 0
  sx <- mkXOr s1 s2
  signsMatch <- icmp "sge" sx (Const I32 0)

  -- remainder can not be bigger than divisor
  let maxLimbsRemainder = s2a
  remainder <- dynamicAllocate !(mkMul (Const I64 GMP_LIMB_SIZE) maxLimbsRemainder)
  -- object must have a valid header, because the next allocation might trigger a GC
  tempHeader <- mkHeader OBJECT_TYPE_ID_BIGINT !(mkTrunc maxLimbsRemainder)
  putObjectHeader remainder tempHeader

  maxLimbsQuotient <- mkMax (Const I64 1) !(mkAdd (Const I64 1) !(mkSub s1a s2a))
  quotient <- dynamicAllocate !(mkMul (Const I64 GMP_LIMB_SIZE) maxLimbsQuotient)

  voidCall "ccc" "@__gmpn_tdiv_qr" [
    toIR !(getObjectPayloadAddr {t=I64} quotient),
    toIR !(getObjectPayloadAddr {t=I64} remainder),
    toIR (Const I64 0),
    toIR !(getObjectPayloadAddr {t=I64} i1),
    toIR s1a,
    toIR !(getObjectPayloadAddr {t=I64} i2),
    toIR s2a
    ]
  qRealNewSize <- call {t=I64} "ccc" "@rapid_bigint_real_size" [
    toIR !(getObjectPayloadAddr {t=I64} quotient),
    toIR maxLimbsQuotient
    ]
  signedNewSize <- mkSelect signsMatch qRealNewSize !(mkSub (Const I64 0) qRealNewSize)
  signedNewSize32 <- mkTrunc {to=I32} signedNewSize
  newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
  putObjectHeader quotient newHeader

  i1negative <- icmp "slt" s1 (Const I32 0)
  rRealNewSize <- call {t=I64} "ccc" "@rapid_bigint_real_size" [
    toIR !(getObjectPayloadAddr {t=I64} remainder),
    toIR maxLimbsRemainder
    ]
  signedNewSize <- mkSelect i1negative !(mkSub (Const I64 0) rRealNewSize) rRealNewSize
  signedNewSize32 <- mkTrunc {to=I32} signedNewSize
  newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
  putObjectHeader remainder newHeader

  jump endLbl

  beginLabel endLbl
  quotient  <- phi [(zeroInteger, retZeroLbl), (zeroQuotient, dividendLargerLbl), (quotient,  divLbl)]
  remainder <- phi [(zeroInteger, retZeroLbl), (i1,           dividendLargerLbl), (remainder, divLbl)]
  pure (quotient, remainder)

export
divIntegerQuotient : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
divIntegerQuotient a b = fst <$> divInteger a b

export
divIntegerRemainder : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
divIntegerRemainder a b = snd <$> divInteger a b

export
shiftLeftInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
shiftLeftInteger integerObj bitCountObj = do
  bitCount <- mkTrunc {to=I32} !(unboxIntegerUnsigned bitCountObj)

  size <- getObjectSize integerObj
  unchanged <- mkOr !(icmp "eq" size (Const I32 0)) !(icmp "eq" bitCount (Const I32 0))
  mkIf (pure unchanged) (do
    pure integerObj
    ) (do
    sizeAbs <- mkAbs size
    fullLimbs <- mkUDiv bitCount (Const I32 GMP_LIMB_BITS)
    maxLimbsCount <- mkAdd !(mkAdd fullLimbs sizeAbs) (Const I32 1)

    newObj <- dynamicAllocate !(mkZext !(mkMul maxLimbsCount (Const I32 GMP_LIMB_SIZE)))
    lowerLimbsAddr <- getObjectPayloadAddr {t=I8} newObj
    appendCode $ "  call void @llvm.memset.p1i8.i64(" ++ toIR lowerLimbsAddr ++ ", i8 0, " ++ toIR !(mkMul !(mkZext fullLimbs) (Const I64 8)) ++ ", i1 false)"

    restBits <- mkURem bitCount (Const I32 GMP_LIMB_BITS)
    mkIf_ (icmp "ne" (Const I32 0) restBits) (do
      srcLimbs <- getObjectPayloadAddr {t=I64} integerObj
      higherLimbsAddr <- getObjectSlotAddrVar {t=I64} newObj !(mkZext {to=I64} fullLimbs)
      msbLimb <- call {t=I64} "ccc" "@__gmpn_lshift" [
        toIR higherLimbsAddr,
        toIR srcLimbs,
        toIR !(mkZext {to=I64} sizeAbs),
        toIR restBits
        ]
      msbLimbAddr <- getObjectSlotAddrVar {t=I64} newObj !(mkZext !(mkSub maxLimbsCount (Const I32 1)))
      store msbLimb msbLimbAddr
      ) (do
      srcLimbs <- getObjectPayloadAddr {t=I8} integerObj
      higherLimbsAddr <- getObjectSlotAddrVar {t=I8} newObj !(mkZext {to=I64} fullLimbs)
      voidCall "ccc" "@llvm.memcpy.p1i8.p1i8.i64" [
        toIR higherLimbsAddr,
        toIR srcLimbs,
        toIR !(mkMul !(mkZext size) (Const I64 GMP_LIMB_SIZE)),
        "i1 false"
        ]
      )

    isNegative <- icmp "slt" size (Const I32 0)
    normaliseIntegerSize newObj maxLimbsCount isNegative
    pure newObj
    )

export
shiftRightInteger : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
shiftRightInteger integerObj bitCountObj = do
  bitCount <- mkTrunc {to=I32} !(unboxIntegerUnsigned bitCountObj)

  size <- getObjectSize integerObj
  unchanged <- mkOr !(icmp "eq" size (Const I32 0)) !(icmp "eq" bitCount (Const I32 0))
  mkIf (pure unchanged) (pure integerObj) (do
    sizeAbs <- mkAbs size
    fullLimbs <- mkUDiv bitCount (Const I32 GMP_LIMB_BITS)
    maxLimbsCount <- mkSub sizeAbs fullLimbs

    mkIf (icmp "sle" maxLimbsCount (Const I32 0)) integer0 (do
      newObj <- dynamicAllocate !(mkZext !(mkMul maxLimbsCount (Const I32 GMP_LIMB_SIZE)))

      restBits <- mkURem bitCount (Const I32 GMP_LIMB_BITS)
      mkIf_ (icmp "ne" (Const I32 0) restBits) (do
        srcHigherLimbs <- getObjectSlotAddrVar {t=I64} integerObj !(mkZext {to=I64} fullLimbs)
        dstLimbsAddr <- getObjectPayloadAddr {t=I64} newObj
        ignore $ call {t=I64} "ccc" "@__gmpn_rshift" [
          toIR dstLimbsAddr,
          toIR srcHigherLimbs,
          toIR !(mkZext {to=I64} maxLimbsCount),
          toIR restBits
          ]
        ) (do
        srcHigherLimbs <- getObjectSlotAddrVar {t=I8} integerObj !(mkZext {to=I64} fullLimbs)
        dstLimbsAddr <- getObjectPayloadAddr {t=I8} newObj
        voidCall "ccc" "@llvm.memcpy.p1i8.p1i8.i64" [
          toIR dstLimbsAddr,
          toIR srcHigherLimbs,
          toIR !(mkMul !(mkZext maxLimbsCount) (Const I64 GMP_LIMB_SIZE)),
          "i1 false"
          ]
        )

      isNegative <- icmp "slt" size (Const I32 0)
      normaliseIntegerSize newObj maxLimbsCount isNegative
      pure newObj
      )

    )

IEEE_DOUBLE_MASK_EXP  : Bits64
IEEE_DOUBLE_MASK_EXP  = 0x7ff0000000000000
IEEE_DOUBLE_MASK_FRAC : Bits64
IEEE_DOUBLE_MASK_FRAC = 0x000fffffffffffff
IEEE_DOUBLE_MASK_SIGN : Bits64
IEEE_DOUBLE_MASK_SIGN = 0x8000000000000000
IEEE_DOUBLE_INF_POS   : Bits64
IEEE_DOUBLE_INF_POS   = 0x7ff0000000000000
IEEE_DOUBLE_INF_NEG   : Bits64
IEEE_DOUBLE_INF_NEG   = 0xfff0000000000000

export
castDoubleToInteger : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
castDoubleToInteger floatObj = do
  floatBitsAsI64 <- getObjectSlot {t=I64} floatObj 0
  exponent <- mkShiftR !(mkAnd (Const I64 $ cast IEEE_DOUBLE_MASK_EXP) floatBitsAsI64) (Const I64 52)
  -- NaN and infinity will be returned as "0"
  isInfOrNaN <- icmp "eq" exponent (Const I64 0x7ff)
  -- absolute values < 1.0 will be returned as "0"
  isSmallerThanOne <- icmp "ult" exponent (Const I64 1023)
  returnZero <- mkOr isInfOrNaN isSmallerThanOne

  mkIf (pure returnZero) {- then -} integer0 {- else -} (do
    fraction <- mkAnd (Const I64 $ cast IEEE_DOUBLE_MASK_FRAC) floatBitsAsI64
    -- highest bit is sign bit in both, Double and I64, so we can just use that one
    isNegative <- icmp "slt" floatBitsAsI64 (Const I64 0)
    initial <- mkOr fraction (Const I64 0x10000000000000)
    toShift <- mkSub exponent (Const I64 1075)
    shiftLeft <- icmp "sgt" toShift (Const I64 0)
    mkIf (pure shiftLeft) (do
      let maxLimbCount = Const I64 17
      payloadSize <- mkMul maxLimbCount (Const I64 GMP_LIMB_SIZE)
      -- requiredBits <- (exponent - 1022)
      -- requiredLimbs <- (requiredBits+63) / 64
      -- newObj <- allocObject (requiredLimbs * 8)
      newObj <- dynamicAllocate payloadSize
      payloadAddr <- getObjectPayloadAddr {t=I8} newObj
      appendCode $ "  call void @llvm.memset.p1i8.i64(" ++ toIR payloadAddr ++ ", i8 0, " ++ toIR payloadSize ++ ", i1 false)"
      putObjectSlot newObj (Const I64 0) initial
      absRealNewSize <- call {t=I64} "ccc" "@rapid_bigint_lshift_inplace" [
        toIR !(getObjectPayloadAddr {t=I64} newObj),
        toIR maxLimbCount,
        toIR !(mkTrunc {to=I32} toShift)
      ]
      signedNewSize <- mkSelect isNegative !(mkSub (Const I64 0) absRealNewSize) absRealNewSize
      size32 <- mkTrunc {to=I32} signedNewSize
      newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT size32
      putObjectHeader newObj newHeader
      pure newObj
      ) (do
        newObj <- dynamicAllocate (Const I64 8)
        toShiftRight <- mkSub (Const I64 0) toShift
        shifted <- mkShiftR initial toShiftRight
        putObjectSlot newObj (Const I64 0) shifted
        signedNewSize32 <- mkSelect isNegative (Const I32 (-1)) (Const I32 1)
        newHeader <- mkHeader OBJECT_TYPE_ID_BIGINT signedNewSize32
        putObjectHeader newObj newHeader
        pure newObj
      )
    )

export
castIntegerToDouble : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
castIntegerToDouble intObj = do
  size <- getObjectSize intObj
  isZero <- icmp "eq" (Const I32 0) size

  mkIf (pure isZero) (cgMkConstDouble 0.0) (do
    sizeAbs <- mkAbs size
    highestLimbIndex <- mkZext {to=I64} !(mkSub sizeAbs (Const I32 1))
    msbLimbAddr <- getObjectSlotAddrVar {t=I64} intObj highestLimbIndex
    msbLimb <- load msbLimbAddr
    countLeadingZeros <- SSA I64 <$> assignSSA ("  call ccc i64 @llvm.ctlz.i64(" ++ toIR msbLimb ++ ", i1 1)")
    exponentOffset <- mkAdd (Const I64 (1023 + 63)) !(mkMul highestLimbIndex (Const I64 64))
    exponent <- mkSub exponentOffset countLeadingZeros

    isInfinity <- icmp "ugt" exponent (Const I64 2046)
    doubleAsBits <- mkIf (pure isInfinity) (do
        pure (Const I64 $ cast IEEE_DOUBLE_INF_POS)
      ) (do
        fracShiftLeft <- icmp "uge" countLeadingZeros (Const I64 12)
        shiftedFraction <- mkIf (pure fracShiftLeft) (do
            mkShiftL msbLimb !(mkSub countLeadingZeros (Const I64 11))
          ) (do
            mkShiftR msbLimb !(mkSub (Const I64 11) countLeadingZeros)
          )
        fraction <- mkIf (icmp "eq" sizeAbs (Const I32 1)) (do
            pure shiftedFraction
          ) (do
            mkIf (pure fracShiftLeft) (do
                secondMsbLimbAddr <- getObjectSlotAddrVar {t=I64} intObj !(mkSub highestLimbIndex (Const I64 1))
                secondMsbLimb <- load secondMsbLimbAddr
                fractionLowerPart <- mkShiftR secondMsbLimb !(mkSub (Const I64 (64 + 11)) countLeadingZeros)
                mkOr shiftedFraction fractionLowerPart
              ) (do
                pure shiftedFraction
              )
          )
        shiftedExponent <- mkShiftL exponent (Const I64 52)
        maskedFraction <- mkAnd (Const I64 $ cast IEEE_DOUBLE_MASK_FRAC) fraction
        mkOr shiftedExponent maskedFraction
      )
    isNegative <- icmp "slt" size (Const I32 0)
    sign <- mkSelect isNegative (Const I64 $ cast IEEE_DOUBLE_MASK_SIGN) (Const I64 0)
    signedDoubleAsBits <- mkOr sign doubleAsBits
    cgMkDoubleFromBits signedDoubleAsBits
    )

export
castStringToInteger : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
castStringToInteger strObj = do
  strLength <- getObjectSize strObj
  maxLimbsCount <- mkUDiv strLength (Const I32 GMP_ESTIMATE_DIGITS_PER_LIMB)
  -- GMP requires 1 limb scratch space
  maxLimbsCountPlus1 <- mkAdd maxLimbsCount (Const I32 1)

  newObj <- dynamicAllocate !(mkZext !(mkMul maxLimbsCountPlus1 (Const I32 GMP_LIMB_SIZE)))
  putObjectHeader newObj !(mkHeader OBJECT_TYPE_ID_BIGINT maxLimbsCountPlus1)
  ignore $ call {t=I32} "ccc" "@rapid_bigint_set_str" [
    toIR newObj,
    toIR strObj
    ]
  pure newObj

export
castIntegerToString : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
castIntegerToString i1 = do
  s1 <- getObjectSize i1
  u1 <- mkZext {to=I64} !(mkAbs s1)

  isZero <- icmp "eq" s1 (Const I32 0)

  mkIf (pure isZero) (mkStr "0") (do
      maxDigits <- call {t=TARGET_SIZE_T} "ccc" "@__gmpn_sizeinbase" [toIR !(getObjectPayloadAddr {t=MP_LIMB_T} i1), toIR u1, "i32 10"]
      isNegative <- icmp "slt" s1 (Const I32 0)

      -- we need to add one extra byte of "scratch space" for mpn_get_str
      -- if the number is negative we need one character more for the leading minus
      needsSign <- mkSelect isNegative (Const I64 2) (Const I64 1)
      maxDigitsWithSign <- mkAdd maxDigits needsSign

      newStr <- dynamicAllocate maxDigitsWithSign
      newHeader <- mkHeader OBJECT_TYPE_ID_STR !(mkTrunc maxDigitsWithSign)
      putObjectHeader newStr newHeader

      actualDigits <- call {t=I64} "ccc" "@rapid_bigint_get_str" [toIR newStr, toIR i1, "i32 10"]
      actualLengthHeader <- mkHeader OBJECT_TYPE_ID_STR !(mkTrunc actualDigits)
      putObjectHeader newStr actualLengthHeader

      pure newStr
    )


text:
%default partial

data Foo : Int -> Type where
     FZero : Foo 0
     FPlus : (x : Int) -> (y : Int) -> Foo (x + y)

tfoo : (x : Int) -> Foo x -> Int
tfoo 0 FZero = ?bar
tfoo (x + y) (FPlus x y) = ?baz

foo : (x : Int) -> Foo x

wfoo : (x : Int) -> Int
wfoo x with (foo x)
  wfoo 0 | FZero = ?wfoo_rhs_1
  wfoo (y + z) | (FPlus y z) = ?wfoo_rhs_2

wbar : (x : Int) -> Int
wbar x with (foo x)
  wbar 0 | FZero = ?wbar_rhs_1
  wbar (1 + z) | (FPlus 1 z) = ?wbar_rhs_2

wbar1 : (x : Int) -> Int
wbar1 x with (foo x)
  wbar1 0 | FZero = ?wbar1_rhs_1
  wbar1 (1 + z) | (FPlus 1 z) = ?wbar1_rhs_2
  wbar1 (y + z) | (FPlus y z) = ?wbar1_rhs_3


text:
module Data.SortedMap.Extra

import Data.SortedMap
import Data.List

export
filter : Ord k => (k -> v -> Bool) -> SortedMap k v -> SortedMap k v
filter pred = fromList . filter (uncurry pred) . toList

export
size : Foldable t => t a -> Nat
size = foldr (\_ => (+ 1)) 0


text:
import Data.Vect

addMatrix : Num numType =>
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType) ->
            Vect rows (Vect cols numType)

multMatrix : Num numType =>
            Vect n (Vect m numType) -> Vect m (Vect p numType) ->
            Vect n (Vect p numType)

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ [] -- "No such variable n"

transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) -> Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                         zipWith ((el, v) -> el :: v) x xsTrans


text:
module CodeGen.RegAlloc

import CommonDef
import Core.Name.Namespace
import Core.Context
import Compiler.Common
import Compiler.ANF
import Data.List
import Data.String
import Data.Vect
import Data.SortedSet
import Data.SortedMap
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Primitives.Externals
import Primitives.Primitives

%hide Prelude.toList

data Elem : Type where
   Branch : Int -> Elem
   Case : Int -> Elem

Eq Elem where
 (==) (Branch a) (Branch b) = a == b
 (==) (Case a) (Case b) = a == b
 (==) _ _ = False
 (/=) (Branch a) (Branch b) = a /= b
 (/=) (Case a) (Case b) = a /= b
 (/=) _ _ = True

data UseDef : Type where
   Use : List Elem -> Int -> UseDef
   Def : List Elem -> Int -> Maybe CairoConst -> UseDef

%prefix_record_projections off
record RegInfo where
    constructor MkRegInfo
    positions: List UseDef
    reg: CairoReg              --Is the original Register
    alloc: CairoReg            --Is the newly allocated Register

emptyRegInfo : CairoReg -> RegInfo
emptyRegInfo r = MkRegInfo [] r r

addUseDef: UseDef -> RegInfo -> RegInfo
addUseDef ud rg = { positions $= (ud::) } rg

mutual
    %prefix_record_projections off
    record RegTreeBlock where
        constructor MkRegTreeBlock
        depth : Int
        regs: List RegInfo
        cases: SortedMap Int RegTreeCase

    %prefix_record_projections off
    record RegTreeCase where
        constructor MkRegTreeCase
        depth : Int
        regs: List RegInfo
        blocks: SortedMap Int RegTreeBlock

commonPrefix : List Elem -> List Elem -> List Elem
commonPrefix _ Nil = Nil
commonPrefix Nil _ = Nil
commonPrefix (h1::tail1) (h2::tail2) = if h1 == h2 then h1::(commonPrefix tail1 tail2) else Nil

insertReg : RegTreeBlock -> RegInfo -> RegTreeBlock
insertReg root regInfo = insertIntoBlock (root.depth) pathRes (Just root)
 where
   computePrefix: Maybe (List Elem) -> UseDef -> Maybe (List Elem)
   computePrefix Nothing (Def path _ _) = Just path
   computePrefix Nothing (Use path _) = Just path
   computePrefix (Just pathAcc) (Def path _ _) = Just (commonPrefix path pathAcc)
   computePrefix (Just pathAcc) (Use path _) = Just (commonPrefix path pathAcc)
   pathRes: List Elem
   pathRes = fromMaybe [] (foldl computePrefix Nothing (regInfo.positions))
   mutual
       insertIntoBlock: Int -> List Elem -> Maybe RegTreeBlock -> RegTreeBlock
       insertIntoBlock _ Nil (Just block) = MkRegTreeBlock (block.depth) (regInfo::(block.regs)) (block.cases)
       insertIntoBlock depth Nil Nothing = MkRegTreeBlock depth [regInfo] empty
       insertIntoBlock depth ((Case i)::rest) (Just block) = MkRegTreeBlock (block.depth) (block.regs) (insert i (insertIntoCase depth rest (lookup i (block.cases))) (block.cases))
       insertIntoBlock depth ((Case i)::rest) Nothing = MkRegTreeBlock depth [] (singleton i (insertIntoCase depth rest Nothing))
       insertIntoBlock depth _ _ = MkRegTreeBlock depth [] empty -- should not happen

       insertIntoCase : Int -> List Elem -> Maybe RegTreeCase -> RegTreeCase
       insertIntoCase _ Nil (Just cases) = MkRegTreeCase (cases.depth) (regInfo::(cases.regs)) (cases.blocks)
       insertIntoCase depth Nil Nothing = MkRegTreeCase depth [regInfo] empty
       insertIntoCase depth ((Branch i)::rest) (Just cases) = MkRegTreeCase (cases.depth) (cases.regs) (insert i (insertIntoBlock (depth+1) rest (lookup i (cases.blocks))) (cases.blocks))
       insertIntoCase depth ((Branch i)::rest) Nothing = MkRegTreeCase depth [] (singleton i (insertIntoBlock (depth+1) rest Nothing))
       insertIntoCase depth _ _ = MkRegTreeCase depth [] empty -- should not happen

buildTree : SortedMap CairoReg RegInfo -> RegTreeBlock
buildTree regInfoMap = foldl insertReg (MkRegTreeBlock 0 [] empty) (values regInfoMap)

RegUseState : Type
RegUseState = (Int,Int,Int) -- currentApRegion, nextApRegion, nextCaseIndex

addRegDef : UseDef -> SortedMap CairoReg RegInfo -> CairoReg -> SortedMap CairoReg RegInfo
addRegDef ud apMap reg = insert reg (includeUseDef (lookup reg apMap)) apMap
    where
     includeUseDef : Maybe RegInfo -> RegInfo
     includeUseDef Nothing = MkRegInfo [ud] reg reg
     includeUseDef (Just oldInfo) = addUseDef ud oldInfo

addResRegDef : List Elem -> Int -> Maybe CairoConst -> CairoReg -> SortedMap CairoReg RegInfo -> SortedMap CairoReg RegInfo
addResRegDef path apRegion const reg apMap = addRegDef (Def path apRegion const) apMap reg

addResRegDefs : List Elem -> Int -> List CairoReg -> SortedMap CairoReg RegInfo -> SortedMap CairoReg RegInfo
addResRegDefs path apRegion regs apMap = foldl addRegDefAcc apMap regs
 where
  addRegDefAcc : SortedMap CairoReg RegInfo -> CairoReg -> SortedMap CairoReg RegInfo
  addRegDefAcc acc reg = addResRegDef path apRegion Nothing reg acc

addRegUse : List Elem -> Int -> CairoReg -> SortedMap CairoReg RegInfo -> SortedMap CairoReg RegInfo
addRegUse path apRegion reg apMap = insert reg (includeUseDef (lookup reg apMap)) apMap
    where
     ud : UseDef
     ud = Use path apRegion
     includeUseDef : Maybe RegInfo -> RegInfo
     includeUseDef Nothing = MkRegInfo [ud] reg reg
     includeUseDef (Just oldInfo) = addUseDef ud oldInfo

addRegUses : List Elem -> Int -> List CairoReg -> SortedMap CairoReg RegInfo -> SortedMap CairoReg RegInfo
addRegUses path apRegion regs apMap = foldl addRegUseAcc apMap regs
 where
  addRegUseAcc : SortedMap CairoReg RegInfo -> CairoReg -> SortedMap CairoReg RegInfo
  addRegUseAcc acc reg = addRegUse path apRegion reg acc

collectCairoInstRegUseBefore : List Elem -> Int -> SortedMap CairoReg RegInfo -> CairoInst -> SortedMap CairoReg RegInfo
collectCairoInstRegUseBefore path apRegion apMap (ASSIGN _ from) = addRegUse (reverse path) apRegion from apMap
collectCairoInstRegUseBefore path apRegion apMap (MKCON _ _ args) = addRegUses (reverse path) apRegion args apMap
collectCairoInstRegUseBefore path apRegion apMap (MKCLOSURE _ _ _ args) = addRegUses (reverse path) apRegion args apMap
collectCairoInstRegUseBefore path apRegion apMap (APPLY _ impls clo arg) = addRegUses (reverse path) apRegion (clo::arg::(map fst (values impls))) apMap
collectCairoInstRegUseBefore path apRegion apMap (MKCONSTANT _ _ ) =  apMap
collectCairoInstRegUseBefore path apRegion apMap (CALL _ impls _ args) = addRegUses (reverse path) apRegion (args ++ (map fst (values impls))) apMap
collectCairoInstRegUseBefore path apRegion apMap (OP _ impls _ args) = addRegUses (reverse path) apRegion (args ++ (map fst (values impls))) apMap
collectCairoInstRegUseBefore path apRegion apMap (EXTPRIM _ impls _ args) = addRegUses (reverse path) apRegion (args ++ (map fst (values impls))) apMap
collectCairoInstRegUseBefore path apRegion apMap (CASE from _ _) = addRegUse (reverse path) apRegion from apMap
collectCairoInstRegUseBefore path apRegion apMap (CONSTCASE from _ _) = addRegUse (reverse path) apRegion from apMap
collectCairoInstRegUseBefore path apRegion apMap (RETURN froms impls) = addRegUses (reverse path) apRegion (froms ++ (values impls)) apMap
collectCairoInstRegUseBefore path apRegion apMap (PROJECT _ from _) = addRegUse (reverse path) apRegion from apMap
collectCairoInstRegUseBefore path apRegion apMap (NULL _) = apMap
collectCairoInstRegUseBefore path apRegion apMap (ERROR _ _) = apMap

collectCairoInstRegUseAfter : List Elem -> Int -> SortedMap CairoReg RegInfo -> CairoInst -> SortedMap CairoReg RegInfo
collectCairoInstRegUseAfter path apRegion apMap (ASSIGN to _) = addResRegDef (reverse path) apRegion Nothing to apMap
collectCairoInstRegUseAfter path apRegion apMap (MKCON to _ _) = addResRegDef (reverse path) apRegion Nothing to apMap
collectCairoInstRegUseAfter path apRegion apMap (MKCLOSURE to _ _ _) = addResRegDef (reverse path) apRegion Nothing to apMap
collectCairoInstRegUseAfter path apRegion apMap (APPLY to impls _ _) = addResRegDefs (reverse path) apRegion (to::(map snd (values impls))) apMap
collectCairoInstRegUseAfter path apRegion apMap (MKCONSTANT to c ) = addResRegDef (reverse path) apRegion (Just c) to apMap
collectCairoInstRegUseAfter path apRegion apMap (CALL tos impls _ _) = addResRegDefs (reverse path) apRegion (tos ++ (map snd (values impls))) apMap
collectCairoInstRegUseAfter path apRegion apMap (OP to impls _ _) = addResRegDefs (reverse path) apRegion (to::(map snd (values impls))) apMap
collectCairoInstRegUseAfter path apRegion apMap (EXTPRIM tos impls _ _) = addResRegDefs (reverse path) apRegion (tos ++ (map snd (values impls))) apMap
collectCairoInstRegUseAfter path apRegion apMap (CASE _ _ _) = apMap
collectCairoInstRegUseAfter path apRegion apMap (CONSTCASE _ _ _) = apMap
collectCairoInstRegUseAfter path apRegion apMap (RETURN _ _) = apMap
collectCairoInstRegUseAfter path apRegion apMap (PROJECT to _ _) = addResRegDef (reverse path) apRegion Nothing to apMap
collectCairoInstRegUseAfter path apRegion apMap (NULL to) = addResRegDef (reverse path) apRegion Nothing to apMap
collectCairoInstRegUseAfter path apRegion apMap (ERROR to _) = addResRegDef (reverse path) apRegion Nothing to apMap

isCairoInstApModStatic : SortedSet Name -> CairoInst -> Bool
isCairoInstApModStatic _ (APPLY _ _ _ _) = False -- An apply can result in an arbitrary ap mod, so this is undef
isCairoInstApModStatic safeCalls (CALL _ _ n _) = contains n safeCalls
isCairoInstApModStatic _ (EXTPRIM _ _ name _) = externalApStable name
isCairoInstApModStatic _ (OP _ _ fn _) = primFnApStable fn
isCairoInstApModStatic _ (CASE _ _ _) = False
isCairoInstApModStatic _ (CONSTCASE _ _ _) = False
isCairoInstApModStatic _ (ERROR _ _ ) = False
isCairoInstApModStatic _ _ = True

mutual
    collectCairoInstRegUseCase : SortedSet Name -> List Elem -> (SortedMap CairoReg RegInfo, RegUseState) -> CairoInst -> List (List CairoInst) -> (SortedMap CairoReg RegInfo, RegUseState)
    collectCairoInstRegUseCase safeCalls path (apMap, (curApRegion, nextApRegion, nextCase)) inst cases = (after, (afterApRegion, afterApRegion+1, nextCase+1))
             where
               before : SortedMap CairoReg RegInfo
               before = collectCairoInstRegUseBefore path curApRegion apMap inst

               branchExtractHelper : Int -> (SortedMap CairoReg RegInfo, RegUseState) -> (SortedMap CairoReg RegInfo, (Int,Int))
               branchExtractHelper nextBr (apMap,(_, next, _)) = (apMap, (next,nextBr))

               newPath : List Elem
               newPath = (Case nextCase)::path

               applyBranch : (SortedMap CairoReg RegInfo, (Int,Int)) -> List CairoInst -> (SortedMap CairoReg RegInfo, (Int,Int))
               applyBranch (state, (nextApRegion, br)) insts = branchExtractHelper (br+1) (collectCairoInstRegUses safeCalls (Branch br::newPath) (state, (curApRegion, nextApRegion, 0)) insts)

               inside : (SortedMap CairoReg RegInfo, (Int,Int))
               inside = foldl applyBranch (before,(nextApRegion,0)) cases

               afterApRegion : Int
               afterApRegion = fst (snd inside)

               after : SortedMap CairoReg RegInfo
               after = collectCairoInstRegUseAfter path afterApRegion (fst inside) inst

    collectCairoInstRegUse : SortedSet Name -> List Elem -> (SortedMap CairoReg RegInfo, RegUseState) -> CairoInst -> (SortedMap CairoReg RegInfo, RegUseState)
    collectCairoInstRegUse safeCalls path state (CASE from alts Nothing) = collectCairoInstRegUseCase safeCalls path state (CASE from alts Nothing) (map snd alts)
    collectCairoInstRegUse safeCalls path state (CASE from alts (Just def)) =  collectCairoInstRegUseCase safeCalls path state (CASE from alts (Just def)) (def::(map snd alts))
    collectCairoInstRegUse safeCalls path state (CONSTCASE from alts Nothing) =  collectCairoInstRegUseCase safeCalls path state (CONSTCASE from alts Nothing) (map snd alts)
    collectCairoInstRegUse safeCalls path state (CONSTCASE from alts (Just def)) =  collectCairoInstRegUseCase safeCalls path state (CONSTCASE from alts (Just def)) (def::(map snd alts))
    collectCairoInstRegUse safeCalls path (apMap, (curApRegion, nextApRegion, nextCase)) inst = process (isCairoInstApModStatic safeCalls inst)
     where
       before : SortedMap CairoReg RegInfo
       before = collectCairoInstRegUseBefore path curApRegion apMap inst

       applyAfter : Int -> SortedMap CairoReg RegInfo -> SortedMap CairoReg RegInfo
       applyAfter region curApMap = collectCairoInstRegUseAfter path region curApMap inst

       process : Bool -> (SortedMap CairoReg RegInfo, RegUseState)
       process False = (applyAfter nextApRegion before, (nextApRegion, nextApRegion+1, nextCase))
       process True = (applyAfter curApRegion before, (curApRegion, nextApRegion, nextCase))

    collectCairoInstRegUses: SortedSet Name -> List Elem -> (SortedMap CairoReg RegInfo, RegUseState) -> List CairoInst -> (SortedMap CairoReg RegInfo, RegUseState)
    collectCairoInstRegUses safeCalls path state insts = foldl (collectCairoInstRegUse safeCalls path) state insts

collectRegUse : SortedSet Name -> List CairoReg -> List CairoInst -> (SortedMap CairoReg RegInfo, Bool)
collectRegUse safeCalls args insts = (fst collectionRes, hasSingleApRegion)
    where
     mapEntry : CairoReg -> (CairoReg, RegInfo)
     mapEntry reg = (reg, MkRegInfo [Def [] 0 Nothing] reg reg)

     initial : List CairoReg -> SortedMap CairoReg RegInfo
     initial args = fromList (map mapEntry args)

     initialApRegion: Int
     initialApRegion = 0

     collectionRes : (SortedMap CairoReg RegInfo, RegUseState)
     collectionRes = collectCairoInstRegUses safeCalls [] (initial args,(initialApRegion,initialApRegion+1,0)) insts

     hasSingleApRegion : Bool
     hasSingleApRegion = (fst (snd collectionRes)) == initialApRegion

SelectionState : Type
SelectionState = (SortedMap CairoReg CairoReg,(Int, Int))

assignRegs : SelectionState -> Int -> List RegInfo -> SelectionState
assignRegs state depth regs = foldl assignReg state regs
    where
     decideTempType : Maybe CairoConst -> Bool -> Int -> CairoReg
     decideTempType (Just v) _ _ = Const v
     decideTempType Nothing False index = Temp index depth
     decideTempType Nothing True index = Let index depth

     extractUsePath : UseDef -> List (List Elem)
     extractUsePath (Use p _) = [p]
     extractUsePath (Def _ _ _) = []

     isCase : Maybe Elem -> Bool
     isCase Nothing = False               -- share the root, so in same branch
     isCase (Just (Branch _)) = False     -- share a branch
     isCase (Just (Case _)) = True        -- share a case but not a branch

     checkPrefixCase : List Elem -> List (List Elem) -> Bool
     checkPrefixCase _ Nil = True
     checkPrefixCase p1 (p2::tail) = isCase (last' (commonPrefix p1 p2))

     distinctBranch : List (List Elem) -> Bool
     distinctBranch Nil = True
     distinctBranch (p::tail) = (checkPrefixCase p tail) && (distinctBranch tail)

     isSingleUse : List UseDef -> Bool
     isSingleUse uds = distinctBranch (uds >>= extractUsePath)

     extractConstant : UseDef -> List CairoConst
     extractConstant (Use _ _) = Nil
     extractConstant (Def _ _ Nothing) = Nil
     extractConstant (Def _ _ (Just s)) = [s]

     uniqueElem : List CairoConst -> Maybe CairoConst
     uniqueElem [v] = Just v
     uniqueElem _ = Nothing

     extractSingleConstant : List UseDef -> Maybe CairoConst
     extractSingleConstant uds = uniqueElem (toList (SortedSet.fromList (uds >>= extractConstant)))

     doRegAlloc : Maybe Int -> SelectionState -> RegInfo -> SelectionState
     doRegAlloc (Just regio) (mapping, (nextLocal, nextTemp)) (MkRegInfo ud r _) = (insert r (decideTempType (extractSingleConstant ud) (isSingleUse ud) nextTemp) mapping, (nextLocal,nextTemp+1))  -- is temp/let/const assignable
     doRegAlloc Nothing (mapping, (nextLocal, nextTemp)) (MkRegInfo ud r _) = (insert r (Local nextLocal depth) mapping, (nextLocal+1,nextTemp))                                                 -- must be local assigned

     mergeApRegions : Int -> Maybe Int -> Maybe Int
     mergeApRegions _ Nothing = Nothing
     mergeApRegions newRegion (Just oldRegion) = if newRegion == oldRegion then Just oldRegion else Nothing

     detectApRegion : List UseDef -> Maybe Int
     detectApRegion Nil = Nothing                                                           -- should never happen
     detectApRegion ((Use _ apRegion)::Nil) = Just apRegion
     detectApRegion ((Def _ apRegion _)::Nil) = Just apRegion
     detectApRegion ((Use _ apRegion)::tail) = mergeApRegions apRegion (detectApRegion tail)
     detectApRegion ((Def _ apRegion _)::tail) = mergeApRegions apRegion (detectApRegion tail)

     assignReg : SelectionState -> RegInfo -> SelectionState
     assignReg state assig@(MkRegInfo locs r (Unassigned _ _ _)) = doRegAlloc (detectApRegion locs) state assig
     assignReg (mapping, counters) (MkRegInfo _ r res) = (insert r res mapping, counters) --Already ia allocated skip

mutual
    assignBlockRegs : SelectionState -> RegTreeBlock -> SelectionState
    assignBlockRegs state block = assignNestedRegs
        where
         assignBlockLocatedRegs : SelectionState
         assignBlockLocatedRegs = assignRegs state (block.depth) (block.regs)

         assignNestedRegs : SelectionState
         assignNestedRegs = foldl assignCaseRegs assignBlockLocatedRegs (values block.cases)

    assignCaseRegs : SelectionState -> RegTreeCase -> SelectionState
    assignCaseRegs state cases = mergeResults (assignNestedBranchesRegs assignCaseLocatedRegs)
        where
         assignCaseLocatedRegs : SelectionState
         assignCaseLocatedRegs = assignRegs state (cases.depth) (cases.regs)

         assignNestedBranchesRegs : SelectionState -> List SelectionState
         assignNestedBranchesRegs (_, counters) = map (assignBlockRegs (empty, counters)) (values cases.blocks)

         mergeStates : SelectionState -> SelectionState -> SelectionState
         mergeStates (mapping1, (nextLocal1, nextTemp1)) (mapping2, (nextLocal2, nextTemp2)) = (mergeLeft mapping1 mapping2, (max nextLocal1 nextLocal2, max nextTemp1 nextTemp2))

         mergeResults : List SelectionState -> SelectionState
         mergeResults branchResults = foldl mergeStates (fst assignCaseLocatedRegs, (0,0)) branchResults

public export
allocateCairoDefRegisters : SortedSet Name -> (Name, CairoDef) -> (CairoDef, SortedSet Name)
allocateCairoDefRegisters safeCalls def@(n, FunDef args implicits rets body) = (updatedDef, updatedSafeCalls)
    where collectedRegs : (SortedMap CairoReg RegInfo, Bool)
          collectedRegs = collectRegUse safeCalls args body
          builtTree : RegTreeBlock
          builtTree = buildTree (fst collectedRegs)
          assignedRegs : SelectionState
          assignedRegs = assignBlockRegs (empty,(0,0)) builtTree
          updatedDef : CairoDef
          updatedDef = snd $ substituteDefRegisters (\reg => lookup reg (fst assignedRegs)) def
          updatedSafeCalls : SortedSet Name
          updatedSafeCalls = if (snd collectedRegs) then (insert n safeCalls) else safeCalls
allocateCairoDefRegisters safeCalls def@(n, ForeignDef info _ _) = if isApStable info
    then (snd def, insert n safeCalls)
    else (snd def, safeCalls)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 12

module Tree

-- check that all functions are total
%default total

public export
data Tree a = Empty
            | Node (Tree a) a (Tree a)

-- from Haskell's Data.Tree
private
shift : String -> String -> List String -> List String
shift str1 str2 strings
  = zipWith (++) (take (length strings) $ str1 :: repeat str2) strings

-- from Haskell's Data.Tree
partial private
draw : Show a => Tree a -> List String
draw Empty = ["*"]
draw (Node left x right) = (show x) :: helper [left, right]
where
  partial
  helper : List (Tree a) -> List String
  helper [] = []
  helper (t :: []) = "|" :: shift "`- " "   " (draw t)
  helper (t :: ts) = "|" :: shift "+- " "|  " (draw t) ++ helper ts

-- from Haskell's Data.Tree
partial private
drawTree : Show a => Tree a -> String
drawTree = unlines . draw

partial export
Show a => Show (Tree a) where
  show x = drawTree x

export
flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module TyTTP.URL.Path

import Data.List
import Data.String
import public Data.Either
import TyTTP
import TyTTP.URL

%default total

data Elem : Type where
  Literal : List Char -> Elem
  Param : List Char -> Elem
  Rest : Elem

Eq Elem where
  (==) (Literal s1) (Literal s2) = s1 == s2
  (==) (Param s1) (Param s2) = s1 == s2
  (==) Rest Rest = True
  (==) _ _ = False

data ParseState
  = InLiteral (List Char)
  | InParam (List Char)
  | InRest

public export
data ParseError
  = EmptyPattern
  | ParamShouldFollowALiteral String (List Elem)
  | RestShouldFollowALiteral String (List Elem)
  | ParamAlreadyDefined String (List Elem)
  | ParamEmpty String (List Elem)
  | UnclosedParam String (List Elem)
  | InvalidStartCharInParam Char (List Elem)
  | InvalidCharInParam Char (List Elem)
  | RestShouldBeLast String (List Elem)

export
data ParsedPattern : (0 s : String) -> Type where
  MkParsedPattern : List Elem -> ParsedPattern s

public export
parse : (s : String) -> Either ParseError (ParsedPattern s)
parse "" = Left EmptyPattern
parse s = map (MkParsedPattern . reverse) $ go (InLiteral []) [] $ unpack s
  where
    isAllowedInParam : Char -> Bool
    isAllowedInParam c = isAlpha c || c == '-' || c == '_'

    go : ParseState -> List Elem -> List Char -> Either ParseError $ List Elem
    go (InLiteral []) p r@('{' :: xs) = Left $ ParamShouldFollowALiteral (pack r) $ reverse p
    go (InLiteral s) p ('{' :: xs) = go (InParam []) (Literal (reverse s) :: p) xs
    go (InLiteral []) p r@('*' :: xs) = Left $ RestShouldFollowALiteral (pack r) $ reverse p
    go (InLiteral s) p ('*' :: xs) = go InRest (Literal (reverse s) :: p) xs
    go (InLiteral s) p ['/'] = Right $ Literal (reverse s) :: p
    go (InLiteral []) p [] = Right p
    go (InLiteral s) p [] = Right $ Literal (reverse s) :: p
    go (InLiteral s) p (x :: xs) = go (InLiteral $ x :: s) p xs
    go (InParam s) p r@('}' :: xs) =
      let name = reverse s
          param = Param name
      in do
        False <- pure $ elem param p
          | True => Left $ ParamAlreadyDefined (pack name) $ reverse p
        False <- pure $ null name
          | True => Left $ ParamEmpty (pack $ '{' :: r) $ reverse p
        go (InLiteral []) (param :: p) xs
    go (InParam s) p [] = Left $ UnclosedParam (pack $ reverse s) $ reverse p
    go (InParam []) p (x :: xs) =
      if isAlpha x
      then go (InParam [x]) p xs
      else Left $ InvalidStartCharInParam x $ reverse p
    go (InParam s) p (x :: xs) =
      if isAllowedInParam x
      then go (InParam (x :: s)) p xs
      else Left $ InvalidCharInParam x $ reverse p
    go InRest p [] = Right $ Rest :: p
    go InRest p r@(x :: _) = Left $ RestShouldBeLast (pack r) $ reverse p

public export
record Path where
  constructor MkPath
  raw : String
  params : List (String, String)
  rest : String

matcher : (s : String) -> ParsedPattern str -> Maybe Path
matcher s (MkParsedPattern ls) = go ls (unpack s) $ MkPath s [] ""
  where

    consumeLiteral : List Char -> List Char -> Maybe $ List Char
    consumeLiteral [] xs = Just xs
    consumeLiteral (_::_) [] = Nothing
    consumeLiteral (l::ls) (x::xs) =
      case l == x of
        True => consumeLiteral ls xs
        False => Nothing

    go : List Elem -> List Char -> Path -> Maybe Path
    go [] [] p = Just p
    go [] xs _ = Nothing
    go (Literal l :: ps) xs p = do
      remaining <- consumeLiteral l xs
      go ps (assert_smaller xs remaining) p
    go (Param param :: Literal l@(f::fs) :: ps) xs p =
        let (value, remaining) = List.break (==f) xs
        in if null value
        then Nothing
        else go (Literal l :: ps) (assert_smaller xs remaining) $ { params $= ((pack param, pack value)::) } p
    go (Param param :: Nil) xs p =
      if null xs
      then Nothing
      else Just $ { params $= ((pack param, pack xs)::) } p
    go (Rest :: Nil) xs p = Just $ { rest := pack xs } p
    go _ _ _ = Nothing

export
pattern : Monad m
  => Alternative m
  => (str : String)
  -> {auto 0 ok : IsRight (Path.parse str)}
  -> (
    Step me (URL auth Path s) h1 st h2 a b
    -> m $ Step me' (URL auth Path s) h1' st' h2' a' b'
  )
  -> Step me (URL auth String s) h1 st h2 a b
  -> m $ Step me' (URL auth String s) h1' st' h2' a' b'
pattern str {ok} handler step with (Path.parse str)
  _ | Right parsedPattern =
    case matcher step.request.url.path parsedPattern of
      Just p => do
        result <- handler $ { request.url := { path := p } step.request.url } step
        pure $ { request.url := { path := step.request.url.path } result.request.url } result
      Nothing => empty

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Pipes

import public Pipes.Core
import public Pipes.Prelude

--

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
module Test.Int32

import Data.Prim.Int32
import Data.SOP
import Hedgehog
import Test.RingLaws

allInt32 : Gen Int32
allInt32 = int32 (linear (-0x80000000) 0xffffffff)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allInt32
  (b8 <= MaxInt32) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allInt32
  (b8 >= MinInt32) === True

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allInt32, allInt32]
  toOrdering (comp m n) === compare m n

export
props : Group
props = MkGroup "Int32" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  ] ++ ringProps allInt32


text:
module Data.JSON.FromString

import Data.JSON.Value
import Data.Scientific

import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core

private
strNull : String
strNull = "null"

private
strTrue : String
strTrue = "true"

private
strFalse : String
strFalse = "false"

private
data Bracket = Open
             | Close

private
Eq Bracket where
  Open == Open = True
  Close == Close = True
  _ == _ = False

private
data JSONTokenKind = TNull
                   | TBool
                   | TNumber
                   | TString
                   | TSquareBracket Bracket
                   | TCurlyBracket Bracket
                   | TComma
                   | TColon
                   | TWhitespace

private
Eq JSONTokenKind where
  TNull == TNull = True
  TBool == TBool = True
  TNumber == TNumber = True
  TString == TString = True
  TSquareBracket x == TSquareBracket y = x == y
  TCurlyBracket x == TCurlyBracket y = x == y
  TComma == TComma = True
  TColon == TColon = True
  TWhitespace == TWhitespace = True
  _ == _ = False

private
TokenKind JSONTokenKind where
  TokType TNull = ()
  TokType TBool = Bool
  TokType TNumber = Scientific 10
  TokType TString = String
  TokType (TSquareBracket _) = ()
  TokType (TCurlyBracket _) = ()
  TokType TComma = ()
  TokType TColon = ()
  TokType TWhitespace = ()
  tokValue TNull _ = ()
  tokValue TBool x = x == strTrue
  tokValue TNumber x = ?parseScientific x
  tokValue TString x = ?parseString x
  tokValue (TSquareBracket _) _ = ()
  tokValue (TCurlyBracket _) _ = ()
  tokValue TComma _ = ()
  tokValue TColon _ = ()
  tokValue TWhitespace _ = ()

private
jsonTokenMap : TokenMap (Token JSONTokenKind)
jsonTokenMap = toTokenMap $
  [ (spaces, TWhitespace)
  , (is ',', TComma)
  , (is ':', TColon)
  , (is '[', TSquareBracket Open)
  , (is ']', TSquareBracket Close)
  , (is '{', TCurlyBracket Open)
  , (is '}', TCurlyBracket Close)
  , (exact strNull, TNull)
  , (exact strTrue <|> exact strFalse, TBool)
  , (?number, TNumber)
  , (?string, TString)
  ]

public export
fromString : String -> JSONValue -- TODO


text:
module Main

import Effects
import Effect.StdIO

import IdrisNet.Packet
import IdrisNet.PacketLang
import Network.Socket
import IdrisNet.TCP.TCPClient

import PacketStruct

printRecvPacket : (mkTy simpleResponse) -> { [STDIO] } Eff IO ()
printRecvPacket (s1 ## s2) = do
  putStr "Received packet: \n"
  putStr $ "S1: " ++ s1 ++ "\n"
  putStr $ "S2: " ++ s2 ++ "\n"

recvResponse : { [STDIO, TCPCLIENT (ClientConnected)] ==>
                 [STDIO, TCPCLIENT ()] } Eff IO ()
recvResponse = do
  OperationSuccess m_packet <- tcpReadPacket simpleResponse 1024
    | RecoverableError err => do putStr ("Error: " ++ (show err) ++ "\n")
                                 tcpClose
    | FatalError err => do putStr ("Error: " ++ (show err) ++ "\n")
                           tcpFinalise
    | ConnectionClosed => return ()
  case m_packet of
    Just (pckt, len) => do printRecvPacket pckt
                           tcpClose
    Nothing => do putStr "Error decoding packet"
                  tcpClose

sendAndRecv : { [STDIO, TCPCLIENT (ClientConnected)] ==>
                [STDIO, TCPCLIENT ()] } Eff IO ()
sendAndRecv = do
  OperationSuccess _ <- tcpWritePacket simpleStruct simpleStructInstance
    | RecoverableError err => do
         putStr ("Error: " ++ (show err) ++ "\n")
         tcpClose
    | FatalError err => do
         putStr ("Fatal error sending packet: " ++ (show err) ++ "\n")
         tcpFinalise
    | ConnectionClosed => return ()
  recvResponse

clientTask : SocketAddress -> Port -> { [STDIO, TCPCLIENT ()] } Eff IO ()
clientTask sa p = do
  OperationSuccess _ <- tcpConnect sa p
    | RecoverableError _ => clientTask sa p
    | FatalError err =>
         putStr ("Fatal error connecting: " ++ (show err) ++ "\n")
    | ConnectionClosed => return ()
  sendAndRecv

main : IO ()
main = run (clientTask (IPv4Addr 127 0 0 1) 1234)


text:
module Base64

-- Example of streaming from/to files.

import Streaming
import Streaming.Bytes as B
import Streaming.Char as C
import Streaming.Encoding.UTF8
import Streaming.Encoding.Base64
import Util -- withFile

import Control.Monad.Trans
import Control.Monad.Identity
import Control.Monad.Either

import System.File
import Data.Strings

import Data.List as L -- reverse

import Control.Monad.Managed

-------------------------------------------------
-- Streaming Base64 Encoding/Decoding Example

{- Here we read in some test ascii data and see if it encodes and decodes into
   the same data. A further test is done by reading in from urandom to see if
   entirely arbitrary data roundtrips properly.

   This is written in a 'forward' style to follow along with the steps the
   stream takes. One could as easily use . and $ and write this in regular
   'reverse' style Idris/Haskell composition.
-}
-------------------------------------------------

text : String
text = "Man is distinguished, not only by his reason, but by this singular passion from other animals, which is a lust of the mind, that by a perseverance of delight in the continued and indefatigable generation of knowledge, exceeds the short vehemence of any carnal pleasure."

text_enc : String
text_enc = "TWFuIGlzIGRpc3Rpbmd1aXNoZWQsIG5vdCBvbmx5IGJ5IGhpcyByZWFzb24sIGJ1dCBieSB0aGlzIHNpbmd1bGFyIHBhc3Npb24gZnJvbSBvdGhlciBhbmltYWxzLCB3aGljaCBpcyBhIGx1c3Qgb2YgdGhlIG1pbmQsIHRoYXQgYnkgYSBwZXJzZXZlcmFuY2Ugb2YgZGVsaWdodCBpbiB0aGUgY29udGludWVkIGFuZCBpbmRlZmF0aWdhYmxlIGdlbmVyYXRpb24gb2Yga25vd2xlZGdlLCBleGNlZWRzIHRoZSBzaG9ydCB2ZWhlbWVuY2Ugb2YgYW55IGNhcm5hbCBwbGVhc3VyZS4="

-- rfc reference strings
test_str1_ref : String
test_str1_ref = ""
test_str2_ref : String
test_str2_ref = "f"
test_str3_ref : String
test_str3_ref = "fo"
test_str4_ref : String
test_str4_ref = "foo"
test_str5_ref : String
test_str5_ref = "foob"
test_str6_ref : String
test_str6_ref = "fooba"
test_str7_ref : String
test_str7_ref = "foobar"
-- rfc reference encoded-strings
test_str1_enc : String
test_str1_enc = ""
test_str2_enc : String
test_str2_enc = "Zg=="
test_str3_enc : String
test_str3_enc = "Zm8="
test_str4_enc : String
test_str4_enc = "Zm9v"
test_str5_enc : String
test_str5_enc = "Zm9vYg=="
test_str6_enc : String
test_str6_enc = "Zm9vYmE="
test_str7_enc : String
test_str7_enc = "Zm9vYmFy"

fromString' : Monad m => String -> Stream (Of Char) m ()
fromString' str = each''' (unpack str)

toString' : Monad m => Stream (Of Char) m r -> m String
toString' = S.foldr_ strCons ""

-- Making it easy to change for testing
alphabet : Alphabet
alphabet = standardAlphabet

-- The Strings used here are expected to be comprised of ascii data for this test
roundtrip : String -> String
roundtrip s = fromString' s
           &$ maps (cast . ord)
           |> encodeBase64 alphabet
           |> decodeBase64 alphabet
           |> maps (chr . cast)
           |> runIdentity . toString'

roundtrip' : String -> String
roundtrip' s = fromString' s &$
               maps (cast . ord) |>
               encodeBase64 alphabet |>
               decodeBase64 alphabet |>
               maps (chr . cast) |>
               runIdentity . toString'

-- encode and check against our specific rfc reference strings
enc : String -> String -> Bool
enc s1 s2 = fromString' s1
         &$ maps (cast . ord) -- turn to Bits8
         |> encodeBase64 alphabet
         |> maps (chr . cast) -- back to Char
         |> toString'
         |> (== s2) . runIdentity

-- using Managed for fun, it's not really that useful for just one 'withFoo'
randoStr : Stream (Of Bits8) Managed (Either FileError ())
randoStr = effect $ do
  Right rand <- use . managed $ withFile "/dev/urandom" Read
    | Left err => pure . pure $ Left err
  pure $ bits8FromFile {io=Managed} rand *> pure (Right ())

rando : Monad m => Stream (Of Bits8) m r -> m Bool
rando str = str
     &$ take 3000
     |> copy
     |> encodeBase64 alphabet
     |> decodeBase64 alphabet
     |> S.toList -- encoded/decoded data
     |> S.toList -- original data
     |> map (\(enc :> orig) => zipWith (==) enc (fstOf orig)) -- compare them
     |> map (and . map delay) -- check they're all True
     -- This is surely slow since we're acting on the results of a ran Stream,
     -- ideally we'd want to stream the comparison and not convert to list.

export
main : IO ()
main = do
    putStrLn $ "text encodes: " ++ show (enc text text_enc)
    putStrLn $ "text roundtrips: " ++ show (roundtrip text == text)

    putStrLn $ "st1 encodes: " ++ show (enc test_str1_ref test_str1_enc)
    putStrLn $ "st2 encodes: " ++ show (enc test_str2_ref test_str2_enc)
    putStrLn $ "st3 encodes: " ++ show (enc test_str3_ref test_str3_enc)
    putStrLn $ "st4 encodes: " ++ show (enc test_str4_ref test_str4_enc)
    putStrLn $ "st5 encodes: " ++ show (enc test_str5_ref test_str5_enc)
    putStrLn $ "st6 encodes: " ++ show (enc test_str6_ref test_str6_enc)
    putStrLn $ "st7 encodes: " ++ show (enc test_str7_ref test_str7_enc)

    putStrLn $ "st1 roundtrips: " ++ show (roundtrip test_str1_ref == test_str1_ref)
    putStrLn $ "st2 roundtrips: " ++ show (roundtrip test_str2_ref == test_str2_ref)
    putStrLn $ "st3 roundtrips: " ++ show (roundtrip test_str3_ref == test_str3_ref)
    putStrLn $ "st4 roundtrips: " ++ show (roundtrip test_str4_ref == test_str4_ref)
    putStrLn $ "st5 roundtrips: " ++ show (roundtrip test_str5_ref == test_str5_ref)
    putStrLn $ "st6 roundtrips: " ++ show (roundtrip test_str6_ref == test_str6_ref)
    putStrLn $ "st7 roundtrips: " ++ show (roundtrip test_str7_ref == test_str7_ref)

    -- slowslowslow, but the encoder works and the memory use is consistent
    -- It'd be nice to track down which part is slow with this.
    runManaged $ do
      r <- rando randoStr
      putStrLn $ "/dev/urandom data roundtripped: " ++ show r
    pure ()


text:
module IR.Reader

import Effects

data Reader : Effect where
  Ask : { a } Reader a

instance Handler Reader m where
  handle st Ask k = k st st

READER : Type -> EFFECT
READER t = MkEff t Reader

ask : { [READER x] } Eff x
ask = call Ask

max_stars_repo_name: puffnfresh/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
||| Provides semantic versioning `Version` type and utilities.
||| See [semver](https://semver.org/) for proper definition of semantic versioning
module Libraries.Data.Version

import Data.List
import Data.String

import Libraries.Text.Parser
import Libraries.Text.Lexer

%default total

||| Semantic versioning with optional tag
public export
record Version where
  constructor MkVersion
  ||| Semantic version
  ||| Should follow the (major, minor, patch) convention
  semVer : (Nat, Nat, Nat)
  ||| Optional tag
  ||| Usually contains git sha1 of this software's build in between releases
  versionTag : Maybe String

||| String representation of a Version with optional display of `tag`
export
showVersion : Bool -> Version -> String
showVersion tag (MkVersion (maj,min,patch) versionTag) =
  concat (intersperse "." (map show [ maj, min, patch])) ++
         if tag then showTag else ""
  where
    showTag : String
    showTag = case versionTag of
                Nothing => ""
                Just tag => "-" ++ tag

export
Show Version where
  show = showVersion True

export
Eq Version where
  (==) (MkVersion ver tag) (MkVersion ver' tag') = ver == ver' && tag == tag'

export
Ord Version where
  compare (MkVersion ver tag) (MkVersion ver' tag')  =
    case compare ver ver' of
      EQ => compare tag tag'
      other => other

--------------------------------------------------------------------------------
-- Parser
--------------------------------------------------------------------------------

data VersionTokenKind = VersionText | VersionNum | VersionDot | VersionDash

Eq VersionTokenKind where
  (==) VersionText VersionText = True
  (==) VersionNum VersionNum = True
  (==) VersionDot VersionDot = True
  (==) VersionDash VersionDash = True
  (==) _ _ = False

VersionToken : Type
VersionToken = Token VersionTokenKind

TokenKind VersionTokenKind where
  TokType VersionText = String
  TokType VersionDot = ()
  TokType VersionDash = ()
  TokType VersionNum = Nat

  tokValue VersionText x = x
  tokValue VersionDot _ = ()
  tokValue VersionDash _ = ()
  tokValue VersionNum n = stringToNatOrZ n

versionTokenMap : TokenMap VersionToken
versionTokenMap = toTokenMap $
  [ (is '.', VersionDot)
  , (is '-', VersionDash)
  , (digits, VersionNum)
  , (some alphaNum, VersionText)
  ]

lexVersion : String -> List (WithBounds VersionToken)
lexVersion str =
  let
    (tokens, _, _, _) = lex versionTokenMap str
  in
    tokens

versionParser : Grammar () VersionToken True Version
versionParser = do
  maj <- match VersionNum
  match VersionDot
  min <- match VersionNum
  match VersionDot
  patch <- match VersionNum
  optTag <- optional $ match VersionDash *> match VersionText
  pure $ MkVersion (maj, min, patch) optTag

||| Parse given string into a proper `Version` record
|||
||| Expected format must be:
||| ```
||| <major>.<minor>.<patch>(-<tag>)?
||| ```
||| where <major>, <minor> and <patch> are natural integers and tag is an optional
||| alpha-numeric string.
export
parseVersion : String -> Maybe Version
parseVersion str =
  case parse versionParser (lexVersion str) of
    Right (_, version, []) => Just version
    _ => Nothing


text:
module Data.Bool.Extra

%default total

public export
andSameNeutral : (x : Bool) -> x && x = x
andSameNeutral False = Refl
andSameNeutral True = Refl

public export
andFalseFalse : (x : Bool) -> x && False = False
andFalseFalse False = Refl
andFalseFalse True = Refl

public export
andTrueNeutral : (x : Bool) -> x && True = x
andTrueNeutral False = Refl
andTrueNeutral True = Refl

public export
orSameNeutral : (x : Bool) -> x || x = x
orSameNeutral False = Refl
orSameNeutral True = Refl

public export
orFalseNeutral : (x : Bool) -> x || False = x
orFalseNeutral False = Refl
orFalseNeutral True = Refl

public export
orTrueTrue : (x : Bool) -> x || True = True
orTrueTrue False = Refl
orTrueTrue True = Refl

public export
orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
orSameAndRightNeutral False _ = Refl
orSameAndRightNeutral True _ = Refl

export
anyTrue : List Bool -> Bool
anyTrue [] = False
anyTrue (x :: xs) = x || anyTrue xs

export
allTrue : List Bool -> Bool
allTrue [] = True
allTrue (x :: xs) = x && allTrue xs


text:
module IdrisNet.UDP.UDPCommon
import Network.Socket

data UDPRes : (res : Type) -> Type where
  UDPSuccess : res -> UDPRes res
  UDPRecoverableError : SocketError -> UDPRes res
  UDPFailure : SocketError -> UDPRes res


text:
data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
                          Empty => NonEmpty [] x
                          NonEmpty xs y => NonEmpty (x :: xs) y

describe_list_end : List Int -> String

describe_list_end input with (listLast input)
  describe_list_end [] | Empty = ?describe_list_end_rhs_1
  describe_list_end (xs ++ [x]) | (NonEmpty xs x) = ?describe_list_end_rhs_2

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Examples.AOC2

import Data.String
import Data.Nat

import Stream
import System
import System.File

record Pos where
  constructor MkPos
  aim        : Int32
  depth      : Int32
  horizontal : Int32

initialPos : Pos
initialPos = MkPos 0 0 0

adjustPos : Pos -> String -> Pos
adjustPos (MkPos a d h) s = case words $ trim s of
  ["forward",v] => MkPos a d (h + cast v)
  ["down",v]    => MkPos a (d + cast v) h
  ["up",v]      => MkPos a (d - cast v) h
  _             => MkPos a d h

adjustPos2 : Pos -> String -> Pos
adjustPos2 (MkPos a d h) s = case words $ trim s of
  ["forward",v] => MkPos a (d + a * cast v) (h + cast v)
  ["down",v]    => MkPos (a + cast v) d h
  ["up",v]      => MkPos (a - cast v) d h
  _             => MkPos a d h

export
part1 : IO ()
part1 = ignore $ withLines "resources/aoc2a" $ \ls => do
  MkPos a d h <- run $ fold_ adjustPos initialPos id ls
  putStrLn "Day2, Result A: \{show $ d * h} (Depth: \{show d}, Pos: \{show h})"

export
part2 : IO ()
part2 = ignore $ withLines "resources/aoc2a" $ \ls => do
  MkPos a d h <- run $ fold_ adjustPos2 initialPos id ls
  putStrLn "Day2, Result B: \{show $ d * h} (Depth: \{show d}, Pos: \{show h})"


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

import Effects
import Effect.State

import Data.AVL.Dict
import Data.DList
import GRL.Lang.GLang

import XML.DOM

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API

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

%access private
%default partial

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

mkDescNode : Maybe String -> Document ELEMENT
mkDescNode Nothing  = mkNode "description"
mkDescNode (Just d) = "description" <+=> d

mkNDNode : String -> String -> Maybe String -> Document ELEMENT
mkNDNode n t d = (mkNode n)
            <++> (mkDescNode d)
            <++> ("name" <+=> t)

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

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

convertReq : REQUIREMENT impl d -> Eff (Document ELEMENT) XEffs
convertReq p = do
       let ty = SifExpr.getRTy p
       let t  = SifExpr.getTitle p
       let d  = SifExpr.getDesc p
       let e  = mkNDNode (cast ty) t d
       (idGen,_) <- get
       let idVal = cast {to=Int} (S idGen)
       let e' = setAttribute "id" (cast idVal) e
       update (\(idGen,ids) => ((S idGen), insert t (S idGen) ids))
       pure $ e'

convertProblem : PROBLEM impl d -> Eff (Document ELEMENT) XEffs
convertProblem p = do
       let t  = SifExpr.getTitle p
       let d  = SifExpr.getDesc p
       let rs = SifExpr.getReqs p
       let e  = mkNode "problem"

       -- <mess>
       rsC <- mapE (\r => convertReq r) rs
       let rNodes = foldl (\n,r => n <++> r) (mkSimpleElement "requirements") rsC
       -- </mess>
       pure $ e
         <++> rNodes
         <++> (mkDescNode d)
         <++> ("name" <+=> t)

convertAffect : AFFECT impl d -> Eff (Document ELEMENT) XEffs
convertAffect p = do
       let d    = SifExpr.getDesc p
       let cval = Model.SifExpr.getCValue p
       let r    = SifExpr.getReq p

       (_,ids) <- get

       let id = lookup (SifExpr.getTitle r) ids
       let e  = case d of
           Nothing => mkNode "affect"
           Just d' => "affect" <+=> d'
       let idval = cast {to=Int} $ fromMaybe 0 id

       pure $ (setAttribute "cvalue" (cast cval)
              (setAttribute "linksTo" (cast idval) e))

convertTrait : TRAIT impl d -> Eff (Document ELEMENT) XEffs
convertTrait p = do
       let ty = SifExpr.getTTy p
       let t  = SifExpr.getTitle p
       let d  = SifExpr.getDesc p
       let s  = SifExpr.getSValue p
       let as = SifExpr.getAffects p

       let e  = mkNode (toLower $ show ty)
       let e' = setAttribute "svalue" (cast s) e

       -- <mess>
       asC <- mapE (\a => convertAffect a) as
       let rNodes = foldl (\n,r => n <++> r) (mkSimpleElement "affects") asC
       -- </mess>
       pure $ e'
         <++> (rNodes)
         <++> (mkDescNode d)
         <++> ("name" <+=> t)

convertProperty : PROPERTY impl d -> Eff (Document ELEMENT) XEffs
convertProperty p = do
       let t  = SifExpr.getTitle p
       let d  = SifExpr.getDesc p
       let ts = SifExpr.getTraits p
       let e  = mkNode "property"

       -- <mess>
       tsC <- mapE (\t => convertTrait t) ts
       let rNodes = foldl (\n,r => n <++> r) (mkSimpleElement "traits") tsC
       -- </mess>

       pure $ e
         <++> rNodes
         <++> (mkDescNode d)
         <++> ("name" <+=> t)

convertSolution : SOLUTION impl d -> Eff (Document ELEMENT) XEffs
convertSolution p = do
       let t  = SifExpr.getTitle p
       let d  = SifExpr.getDesc p
       let ps = SifExpr.getProperties p
       let e  = mkNode "solution"

       -- <mess>
       psC <- mapE (\p => convertProperty p) ps
       let rNodes = foldl (\n,r => n <++> r) (mkSimpleElement "properties") psC
       -- </mess>

       pure $ e
         <++> rNodes
         <++> (mkDescNode d)
         <++> ("name" <+=> t)

convertDomain : SifDomain -> Eff (Document ELEMENT) XEffs
convertDomain (MkDomain t d) = pure $ (mkNDNode "context" t d)

convertPattern : PATTERN impl d -> Eff (Document ELEMENT) XEffs
convertPattern pat = do
       let t = SifExpr.getTitle pat
       let d = SifExpr.getDesc pat

       dNode <- convertDomain   $ SifExpr.getDomain pat
       pNode <- convertProblem  $ SifExpr.getProblem pat
       sNode <- convertSolution $ SifExpr.getSolution pat

       pure $ mkNode "sif"
          <++> sNode
          <++> pNode
          <++> dNode
          <++> (mkDescNode d)
          <++> ("name" <+=> t)

namespace Sif
  export
  toXML : PATTERN impl d -> Document DOCUMENT
  toXML p = mkDocument root
    where
      partial
      root : Document ELEMENT
      root = runPureInit [(Z,Dict.empty)] (convertPattern p)

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Main

import Data.Strings

%default total

libsmall : String -> String
libsmall fn = "C:" ++ fn ++ ",libsmall"

%foreign (libsmall "add")
prim_add : Int -> Int -> PrimIO Int

add : HasIO io => Int -> Int -> io Int
add x y = primIO $ prim_add x y

%foreign (libsmall "sub")
prim_sub : Int -> Int -> PrimIO Int

sub : HasIO io => Int -> Int -> io Int
sub x y = primIO $ prim_sub x y

%foreign (libsmall "mul")
prim_mul : Int -> Int -> PrimIO Int

mul : HasIO io => Int -> Int -> io Int
mul x y = primIO $ prim_mul x y

%foreign (libsmall "divide")
prim_div : Int -> Int -> PrimIO Int

div : HasIO io => Int -> Int -> io Int
div x y = primIO $ prim_div x y

%foreign (libsmall "add_with_message")
prim_addWithMessage : String -> Int -> Int -> PrimIO ()

addWithMessage : HasIO io => String -> Int -> Int -> io ()
addWithMessage m x y = primIO $ prim_addWithMessage m x y

%foreign (libsmall "sub_with_message")
prim_subWithMessage : String -> Int -> Int -> PrimIO ()

subWithMessage : HasIO io => String -> Int -> Int -> io ()
subWithMessage m x y = primIO $ prim_subWithMessage m x y

%foreign (libsmall "mul_with_message")
prim_mulWithMessage : String -> Int -> Int -> PrimIO ()

mulWithMessage : HasIO io => String -> Int -> Int -> io ()
mulWithMessage m x y = primIO $ prim_mulWithMessage m x y

%foreign (libsmall "div_with_message")
prim_divWithMessage : String -> Int -> Int -> PrimIO ()

divWithMessage : HasIO io => String -> Int -> Int -> io ()
divWithMessage m x y = primIO $ prim_divWithMessage m x y

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

main : IO ()
main = do Just x <- readInt
            | Nothing => putStrLn "first number is invalid"
          Just y <- readInt
            | Nothing => putStrLn "second number is invalid"
          sum <- add x y
          printLn sum
          addWithMessage "sum" x y
          subWithMessage "sub" x y
          mulWithMessage "mul" x y
          divWithMessage "div" x y

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

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

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


text:
module Text.WebIDL.Types.StringLit

import Generics.Derive

%default total

%language ElabReflection

||| A quoted string literal
public export
record StringLit where
  constructor MkStrLit
  value : String

%runElab derive "StringLit" [Generic,Meta,Eq,Ord,Show]


text:
module Data.Floating

||| Haskell's `Floating` with all inverse hyperbolic trigo functions absent
public export
interface Fractional a => Floating a where
  pi : a
  exp, ln, sqrt : a -> a
  pow : a -> a -> a
  log : (base : a) -> a -> a
  sin, cos, tan, asin, acos, atan, sinh, cosh, tanh : a -> a

export
Floating Double where
  pi = Prelude.pi
  exp = Prelude.exp
  ln = Prelude.log
  log base x = ln x / ln base
  sqrt = Prelude.sqrt
  pow = Prelude.pow
  sin = Prelude.sin
  cos = Prelude.cos
  tan = Prelude.tan
  asin = Prelude.asin
  acos = Prelude.acos
  atan = Prelude.atan
  sinh = Prelude.sinh
  cosh = Prelude.cosh
  tanh = Prelude.tanh


text:
||| This module presents a realisation of ARMs APB protocol using our
||| abstract interface definition language.
module Example.Specification.APB

import Text.Markup.Edda
import Text.Markup.Edda.Org

import Cordial.EDSL.Specification

%access public export
%default total

||| Concrete labels for port descriptions.
data APBRTy = CLOCK | RESET | ADDR | PROT | SELECT
            | ENABLE | WRITE | WDATA | STROBE | READY
            | RDATA | ERROR

||| Equality type is required to differentiate labels.
Eq APBRTy where
  (==) CLOCK  CLOCK  = True
  (==) RESET  RESET  = True
  (==) ADDR   ADDR   = True
  (==) PROT   PROT   = True
  (==) SELECT SELECT = True
  (==) ENABLE ENABLE = True
  (==) WRITE  WRITE  = True
  (==) WDATA  WDATA  = True
  (==) STROBE STROBE = True
  (==) READY  READY  = True
  (==) RDATA  RDATA  = True
  (==) ERROR  ERROR  = True
  (==) _      _      = False

namespace Initiator
  ||| This function represents the abstract interface description for
  ||| APBs initiating interface.
  |||
  ||| This interface connect is designed to be connected to a single
  ||| interconnect component, which in turn connects to many target
  ||| components.
  |||
  ||| @dWidth The width of the data bus must be one of [32,16,8].
  ||| @noTargets The number of targets we connect to.
  APB_Initiator_Gen : (dWidth,aWidth,noTargets : Nat)
                   -> (prfD  : ValidArraySpec dWidth [32,16,8])
                   -> (prfA  : ValidArraySpec aWidth [32,16,8])
                   -> (prfT  : IsSucc noTargets)
                   -> IDL APBRTy
  APB_Initiator_Gen dWidth aWidth noTargets prfD prfA prfT = do
    setVendor "ARM"
    setLibrary "examples"
    setName ("APB_Initiator_" <+> show noTargets <+> "_Targets")
    setVersion "0.1"
    setCommunicationStyle Unicast

    c   <- label CLOCK
    r   <- label RESET
    a   <- label ADDR
    p   <- label PROT
    sel <- label SELECT
    e   <- label ENABLE
    w   <- label WRITE
    wd  <- label WDATA
    str <- label STROBE
    rdy <- label READY
    rd  <- label RDATA
    err <- label ERROR

    let dWidth' = fromNat dWidth prfD
    let aWidth' = fromNat aWidth prfA

    clock c Nothing Nothing Nothing
      # system "SYS"
      # fromTargetAlways
    reset r
      # system "SYS"
      # fromTargetAlways
      # setSensitivity Low

    address a aWidth'
    info p (fromNat 2)
    replicate noTargets (control sel)
    control e
    control w
    bus wd dWidth'

    let nrStr = assert_total (div dWidth 8)
    -- nat division is not total.

    replicate nrStr (control str)

    control rdy    # fromTarget
    bus rd dWidth' # fromTarget
    control err    # fromTarget
    stop

  ||| Transform the specification into a model.
  APB_Initiator : (dWidth, aWidth, nrTargets : Nat)
               -> {auto prfD  : ValidArraySpec dWidth [32,16,8]}
               -> {auto prfA  : ValidArraySpec aWidth [32,16,8]}
               -> {auto prfT : IsSucc nrTargets}
               -> InterfaceTy () APBRTy
  APB_Initiator d a t {prfD} {prfA} {prfT} =
    buildSpec (APB_Initiator_Gen d a t prfD prfA prfT)

namespace Target
  ||| This function represents the abstract interface description for
  ||| APBs targeted interface.
  |||
  ||| This interface connect is designed to be connected from a single
  ||| interconnect component, which in turn will connect to a single
  ||| target component.
  |||
  ||| @dWidth The width of the data bus must be one of [32,16,8].
  ||| @aWidth The width of the address bus must be one of [32,16,8].
  APB_Target_Gen : (dWidth,aWidth : Nat)
                -> (prfD  : ValidArraySpec dWidth [32,16,8])
                -> (prfA  : ValidArraySpec aWidth [32,16,8])
                -> IDL APBRTy
  APB_Target_Gen dWidth aWidth prfD prfA = do
    setVendor "ARM"
    setLibrary "examples"
    setName ("APB_Target")
    setVersion "0.1"
    setCommunicationStyle Unicast

    c   <- label CLOCK
    r   <- label RESET
    a   <- label ADDR
    p   <- label PROT
    sel <- label SELECT
    e   <- label ENABLE
    w   <- label WRITE
    wd  <- label WDATA
    str <- label STROBE
    rdy <- label READY
    rd  <- label RDATA
    err <- label ERROR

    let dWidth' = fromNat dWidth prfD
    let aWidth' = fromNat aWidth prfA

    clock c Nothing Nothing Nothing
      # system "SYS"
      # fromTargetAlways
    reset r
      # system "SYS"
      # fromTargetAlways
      # setSensitivity Low

    address a aWidth'
    info p (fromNat 2)

    control sel

    control e
    control w
    bus wd dWidth'

    let nrStr = assert_total (div dWidth 8)
    -- nat division is not total.

    replicate nrStr (control str)

    control rdy    # fromTarget
    bus rd dWidth' # fromTarget
    control err    # fromTarget
    stop

  ||| Transform the specification into a model.
  APB_Target : (dWidth, aWidth : Nat)
            -> {auto prfD  : ValidArraySpec dWidth [32,16,8]}
            -> {auto prfA  : ValidArraySpec aWidth [32,16,8]}
            -> InterfaceTy () APBRTy
  APB_Target d a {prfD} {prfA} =
    buildSpec (APB_Target_Gen d a prfD prfA)

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial