text:
module Primitives.BigInt

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

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

    generateCode = generateMissingCodeError "add_integer"

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

    generateCode = generateMissingCodeError "sub_integer"

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

    generateCode = generateMissingCodeError "mul_integer"

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

    generateCode = generateMissingCodeError "div_integer"

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

    generateCode = generateMissingCodeError "mod_integer"

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

    generateCode = generateMissingCodeError "neg_integer"

export
[shl_integer] PrimFn where
    eval [_, ConstValue(BI 0)] = Just $ ArgValue 0
    eval [ConstValue (BI a), ConstValue (BI b)] = Just $ NewValue $ ConstValue $ BI (prim__shl_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shl_integer"

export
[shr_integer] PrimFn where
    eval [_, ConstValue(BI 0)] = Just $ ArgValue 0
    eval [ConstValue (BI a), ConstValue (BI b)] = Just $ NewValue $ ConstValue $ BI (prim__shr_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "shr_integer"

export
[and_integer] PrimFn where
    eval [ConstValue (BI a), ConstValue (BI b)] = Just $ NewValue $ ConstValue $ BI (prim__and_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "and_integer"

export
[or_integer] PrimFn where
    eval [ConstValue (BI a), ConstValue (BI b)] = Just $ NewValue $ ConstValue $ BI (prim__or_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "or_integer"

export
[xor_integer] PrimFn where
    eval [ConstValue (BI a), ConstValue (BI b)] = Just $ NewValue $ ConstValue $ BI (prim__xor_Integer (cast a) (cast b))
    eval _ = Nothing

    generateCode = generateMissingCodeError "xor_integer"

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

    generateCode = generateMissingCodeError "lt_integer"

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

    generateCode = generateMissingCodeError "lte_integer"

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

    generateCode = generateMissingCodeError "eq_integer"

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

    generateCode = generateMissingCodeError "gte_integer"

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

    generateCode = generateMissingCodeError "gt_integer"

export
[cast_to_integer] PrimFn where
    eval [ConstValue c] = map (\r => NewValue $ ConstValue $ BI r) (constToInteger c)
    eval _ = Nothing

    generateCode _ _ _ = generateMissingCodeError "cast_to_integer"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_int"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_int8"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_int16"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_int32"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_int64"

export
[cast_integer_to_felt] PrimFn where
    eval [ConstValue c] = map (\r => NewValue $ ConstValue $ F $ cast r) (constToInteger c)
    eval _ = Nothing

    generateCode r [_] _ = Instructions [ERROR r "cast_integer_to_felt is currently not supported"]
    generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode cast_integer_to_felt"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_uint8"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_uint16"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_uint32"

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

    generateCode _ _ _ = generateMissingCodeError "cast_integer_to_uint64"

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module NewGraph

import Data.AVL.Tree
import Data.AVL.Set
import Data.AVL.Dict

interface Graph (g : Type -> Type -> Type) where
  empty : g a b

record VertexData vTy eTy where
  constructor MkVertexData
  preds : Dict vTy eTy
  succs : Dict vTy eTy

record GraphData vTy eTy where
  constructor MkGraphData
  dict : Dict vTy (VertexData vTy eTy)

implementation Graph GraphData where
  empty : Graph a b
  empty = MkGraphData empty

ext: idr

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
IntOrChar : Bool -> Type
IntOrChar True = Int
IntOrChar False = Char

foo : Nat -> (x : Bool) -> IntOrChar x -> String
foo num x i
    = case x of
           True => show num
           False => show i


text:
module Ex4

import Data.Vect

data Tree : (elem : Type) -> Type where
  Empty : Ord elem => Tree elem
  Node : Ord elem => (left : Tree elem) -> (val : elem) -> (right : Tree elem) -> Tree elem

insert : elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node l v r) = case compare x v of
                               LT => Node (insert x l) v r
                               EQ => orig
                               GT => Node l v (insert x r)

listToTree : Ord elem => List elem -> Tree elem
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

treeToList : Tree elem -> List elem
treeToList Empty = []
treeToList (Node l v r) = treeToList l ++ [v] ++ treeToList r

data Expr : Type where
  Val : Int -> Expr
  Add : Expr -> Expr -> Expr
  Sub : Expr -> Expr -> Expr
  Mul : Expr -> Expr -> Expr

evaluate : Expr -> Int
evaluate (Val n) = n
evaluate (Add e1 e2) = evaluate e1 + evaluate e2
evaluate (Sub e1 e2) = evaluate e1 - evaluate e2
evaluate (Mul e1 e2) = evaluate e1 * evaluate e2

e1 : Expr
e1 = Mul (Val 10) (Add (Val 6) (Val 3))

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe (Just x) (Just y) = case compare x y of
                                  GT => Just x
                                  _ => Just y
maxMaybe _ _ = Nothing

data Shape : Type where
  Triangle : Double -> Double -> Shape
  Rectangle : Double -> Double -> Shape
  Circle : Double -> Shape

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length breadth) = length * breadth
area (Circle radius) = pi * radius * radius

data Picture : Type where
  Primitive : Shape -> Picture
  Combine : Picture -> Picture -> Picture
  Rotate : Double -> Picture -> Picture
  Translate : Double -> Double -> Picture -> Picture

pictureArea : Picture -> Double
pictureArea (Primitive s) = area s
pictureArea (Combine p1 p2) = pictureArea p1 + pictureArea p2
pictureArea (Rotate _ p) = pictureArea p
pictureArea (Translate _ _ p) = pictureArea p

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive s) = case s of
                                     Triangle _ _ => Just (area s)
                                     _ => Nothing
biggestTriangle (Combine p1 p2) = case biggestTriangle p1 of
                                       Just a1 => case biggestTriangle p2 of
                                                       Just a2 => Just (max a1 a2)
                                                       Nothing => Just a1
                                       Nothing => case biggestTriangle p2 of
                                                       Just a2 => Just a2
                                                       Nothing => Nothing
biggestTriangle (Rotate _ p) = biggestTriangle p
biggestTriangle (Translate _ _ p) = biggestTriangle p

-- dependent types

data PowerSource = Petrol | Pedal | Electricity

data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Unicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : (watts : Nat) -> Vehicle Electricity

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels Unicycle = 2
wheels (Motorcycle _) = 2
wheels (Car _) = 4
wheels (Bus _) = 4
wheels (Tram _) = 16

refuel : Vehicle Petrol -> Vehicle Petrol
refuel Bicycle impossible
refuel Unicycle impossible
refuel (Tram _) impossible
refuel (Motorcycle _) = Motorcycle 50
refuel (Car _) = Car 100
refuel (Bus _) = Bus 200

vectTake : (m : Fin (S n)) -> Vect n elem -> Vect (finToNat m) elem
vectTake FZ _ = []
vectTake (FS m) (x :: xs) = x :: vectTake m xs

sumEntries : Num a => { n : _ } -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries pos xs ys = case integerToFin pos n of
                            Nothing => Nothing
                            Just idx => Just (index idx xs + index idx ys)

-- see Ex4_1.idr

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Control.Monad.State.Interface

import Control.Monad.Maybe
import Control.Monad.Error.Either
import Control.Monad.Reader.Reader
import Control.Monad.State.State
import Control.Monad.RWS.CPS
import Control.Monad.Trans
import Control.Monad.Writer.CPS

%default total

||| A computation which runs in a context and produces an output
public export
interface Monad m => MonadState stateType m | m where
    ||| Get the context
    get : m stateType
    ||| Write a new context/output
    put : stateType -> m ()

    ||| Embed a simple state action into the monad.
    state : (stateType -> (stateType,a)) -> m a
    state f = do s <- get
                 let (s2,a) = f s
                 put s2
                 pure a

||| Apply a function to modify the context of this computation
public export
modify : MonadState stateType m => (stateType -> stateType) -> m ()
modify f
    = do s <- get
         put (f s)

||| Evaluate a function in the context held by this computation
public export
gets : MonadState stateType m => (stateType -> a) -> m a
gets f
    = do s <- get
         pure (f s)

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
Monad m => MonadState stateType (StateT stateType m) where
    get     = ST (\x => pure (x, x))
    put x   = ST (\y => pure (x, ()))
    state f = ST $ pure . f

public export %inline
MonadState s m => MonadState s (EitherT e m) where
  get = lift get
  put = lift . put
  state = lift . state

public export %inline
MonadState s m => MonadState s (MaybeT m) where
  get = lift get
  put = lift . put
  state = lift . state

public export %inline
Monad m => MonadState s (RWST r w s m) where
  get     = MkRWST $ \_,s,w => pure (s,s,w)
  put s   = MkRWST $ \_,_,w => pure ((),s,w)
  state f = MkRWST $ \_,s,w => let (s',a) = f s in pure (a,s',w)

public export %inline
MonadState s m => MonadState s (ReaderT r m) where
  get = lift get
  put = lift . put
  state = lift . state

public export %inline
MonadState s m => MonadState s (WriterT r m) where
  get = lift get
  put = lift . put
  state = lift . state


text:
data Test : Type where
  MkTest : Test

export
tpat1 : Type -> Int
tpat1 Int = 0
tpat1 String = 1
tpat1 (Maybe Test) = 2
tpat1 (Maybe String) = 3
tpat1 other = 4

export
tpat2 : (Type -> Type) -> Int
tpat2 _ = 1

main : IO ()
main = do
  printLn $ tpat1 (Maybe Test)

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen