text:
module Compiler.Jvm.Variable

import Core.Core
import Core.FC

import Compiler.Jvm.Asm
import Compiler.Jvm.InferredType

import Data.Maybe
import Data.List

getLocTy : Map Int InferredType -> Int -> IO InferredType
getLocTy typesByIndex varIndex = do
    optTy <- Map.get typesByIndex varIndex
    pure $ fromMaybe IUnknown optTy

getVarIndex : Map Int InferredType -> Int -> IO Int
getVarIndex types index = go 0 0 where
  go : Int -> Int -> IO Int
  go pos currVarIndex =
    if currVarIndex == index then
        pure pos
    else do
        currVarTy <- getLocTy types currVarIndex
        let isTwoWordTy = currVarTy == IDouble || currVarTy == ILong
        let nextPos = if isTwoWordTy then pos + 2 else succ pos
        go nextPos (succ currVarIndex)

opWithWordSize : Map Int InferredType -> (Int -> Asm ()) -> Int -> Asm ()
opWithWordSize types op var = do
    newPos <- LiftIo $ getVarIndex types var
    op newPos

boxDouble : Asm ()
boxDouble = InvokeMethod InvokeStatic "java/lang/Double" "valueOf" "(D)Ljava/lang/Double;" False

boxFloat : Asm ()
boxFloat = InvokeMethod InvokeStatic "java/lang/Float" "valueOf" "(F)Ljava/lang/Float;" False

boxBool : Asm ()
boxBool = InvokeMethod InvokeStatic "java/lang/Boolean" "valueOf" "(Z)Ljava/lang/Boolean;" False

boxByte : Asm ()
boxByte = InvokeMethod InvokeStatic "java/lang/Byte" "valueOf" "(B)Ljava/lang/Byte;" False

boxChar : Asm ()
boxChar = InvokeMethod InvokeStatic "java/lang/Character" "valueOf" "(C)Ljava/lang/Character;" False

boxInt : Asm ()
boxInt = InvokeMethod InvokeStatic "java/lang/Integer" "valueOf" "(I)Ljava/lang/Integer;" False

boxShort : Asm ()
boxShort = InvokeMethod InvokeStatic "java/lang/Short" "valueOf" "(S)Ljava/lang/Short;" False

boxLong : Asm ()
boxLong = InvokeMethod InvokeStatic "java/lang/Long" "valueOf" "(J)Ljava/lang/Long;" False

thunkInt : Asm ()
thunkInt = let descriptor = "(I)" ++ getJvmTypeDescriptor (getThunkType IInt)
    in InvokeMethod InvokeStatic runtimeClass "createThunk" descriptor False

thunkLong : Asm ()
thunkLong = let descriptor = "(J)" ++ getJvmTypeDescriptor (getThunkType ILong)
    in InvokeMethod InvokeStatic runtimeClass "createThunk" descriptor False

thunkDouble : Asm ()
thunkDouble = let descriptor = "(D)" ++ getJvmTypeDescriptor (getThunkType IDouble)
    in InvokeMethod InvokeStatic runtimeClass "createThunk" descriptor False

thunkObject : Asm ()
thunkObject = let descriptor = "(Ljava/lang/Object;)" ++ getJvmTypeDescriptor (getThunkType inferredObjectType)
    in InvokeMethod InvokeStatic runtimeClass "createThunk" descriptor False

unboxToIntThunk : Asm ()
unboxToIntThunk =
    let descriptor = "(" ++ getJvmTypeDescriptor (getThunkType inferredObjectType) ++ ")" ++
            getJvmTypeDescriptor (getThunkType IInt)
    in InvokeMethod InvokeStatic runtimeClass "unboxToIntThunk" descriptor False

unboxToLongThunk : Asm ()
unboxToLongThunk =
    let descriptor = "(" ++ getJvmTypeDescriptor (getThunkType inferredObjectType) ++ ")" ++
            getJvmTypeDescriptor (getThunkType ILong)
    in InvokeMethod InvokeStatic runtimeClass "unboxToLongThunk" descriptor False

unboxToDoubleThunk : Asm ()
unboxToDoubleThunk =
    let descriptor = "(" ++ getJvmTypeDescriptor (getThunkType inferredObjectType) ++ ")" ++
            getJvmTypeDescriptor (getThunkType IDouble)
    in InvokeMethod InvokeStatic runtimeClass "unboxToDoubleThunk" descriptor False

unwrapIntThunk : Asm ()
unwrapIntThunk = InvokeMethod InvokeStatic runtimeClass "unwrapIntThunk" "(Ljava/lang/Object;)I" False

unwrapIntThunkToChar : Asm ()
unwrapIntThunkToChar = InvokeMethod InvokeStatic runtimeClass "unwrapIntThunkToChar" "(Ljava/lang/Object;)C" False

unwrapLongThunk : Asm ()
unwrapLongThunk = InvokeMethod InvokeStatic runtimeClass "unwrapLongThunk" "(Ljava/lang/Object;)J" False

unwrapDoubleThunk : Asm ()
unwrapDoubleThunk = InvokeMethod InvokeStatic runtimeClass "unwrapDoubleThunk" "(Ljava/lang/Object;)D" False

export
unwrapObjectThunk : Asm ()
unwrapObjectThunk = InvokeMethod InvokeStatic runtimeClass "unwrap" "(Ljava/lang/Object;)Ljava/lang/Object;" False

unboxBool : Asm ()
unboxBool = InvokeMethod InvokeVirtual "java/lang/Boolean" "booleanValue" "()Z" False

unboxByte : Asm ()
unboxByte = InvokeMethod InvokeVirtual "java/lang/Byte" "byteValue" "()B" False

unboxInt : Asm ()
unboxInt = InvokeMethod InvokeVirtual "java/lang/Integer" "intValue" "()I" False

unboxChar : Asm ()
unboxChar = InvokeMethod InvokeVirtual "java/lang/Character" "charValue" "()C" False

unboxShort : Asm ()
unboxShort = InvokeMethod InvokeVirtual "java/lang/Short" "shortValue" "()S" False

unboxLong : Asm ()
unboxLong = InvokeMethod InvokeVirtual "java/lang/Long" "longValue" "()J" False

unboxDouble : Asm ()
unboxDouble = InvokeMethod InvokeVirtual "java/lang/Double" "doubleValue" "()D" False

unboxFloat : Asm ()
unboxFloat = InvokeMethod InvokeVirtual "java/lang/Float" "floatValue" "()F" False

%inline
export
conversionClass : String
conversionClass = "io/github/mmhelloworld/idrisjvm/runtime/Conversion"

boolObjToBool : Asm ()
boolObjToBool = InvokeMethod InvokeStatic conversionClass "toBoolean1" "(Ljava/lang/Object;)Z" False

boolToInt : Asm ()
boolToInt = InvokeMethod InvokeStatic conversionClass "boolToInt1" "(Z)I" False

objToInt : Asm ()
objToInt = InvokeMethod InvokeStatic conversionClass "toInt1" "(Ljava/lang/Object;)I" False

objToChar : Asm ()
objToChar = InvokeMethod InvokeStatic conversionClass "toChar" "(Ljava/lang/Object;)C" False

objToBoolean : Asm ()
objToBoolean = InvokeMethod InvokeStatic conversionClass "toBoolean1" "(Ljava/lang/Object;)Z" False

objToByte : Asm ()
objToByte = InvokeMethod InvokeStatic conversionClass "toByte" "(Ljava/lang/Object;)B" False

charObjToChar : Asm ()
charObjToChar = do Checkcast "java/lang/Character"; unboxChar

objToShort : Asm ()
objToShort = InvokeMethod InvokeStatic conversionClass "toShort" "(Ljava/lang/Object;)S" False

longObjToLong : Asm ()
longObjToLong = do Checkcast "java/lang/Long"; unboxLong

objToFloat : Asm ()
objToFloat = InvokeMethod InvokeStatic conversionClass "toFloat" "(Ljava/lang/Object;)F" False

objToDouble : Asm ()
objToDouble = InvokeMethod InvokeStatic conversionClass "toDouble" "(Ljava/lang/Object;)D" False

export
checkcast : String -> Asm ()
checkcast "java/lang/Object" = pure ()
checkcast cname              = Checkcast cname

export
asmCast : (sourceType: InferredType) -> (targetType: InferredType) -> Asm ()

asmCast ty1@(IRef class1) ty2@(IRef class2) =
  cond [
      (class1 == class2, Pure ()),
      (isThunkType ty1 && class2 == thunkClass, Pure ()),
      (class2 == thunkClass, thunkObject),
      (class1 == thunkClass && class2 == intThunkClass, unboxToIntThunk),
      (class1 == thunkClass && class2 == longThunkClass, unboxToLongThunk),
      (class1 == thunkClass && class2 == doubleThunkClass, unboxToDoubleThunk),
      (isThunkType ty1, do unwrapObjectThunk; checkcast class2)
    ]
    (checkcast class2)

asmCast IUnknown ty@(IRef clazz) = if isThunkType ty
    then thunkObject
    else checkcast clazz

asmCast IBool IBool     = Pure ()
asmCast IByte IByte     = Pure ()
asmCast IChar IChar     = Pure ()
asmCast IShort IShort   = Pure ()
asmCast IInt IBool      = Pure ()
asmCast IInt IInt       = Pure ()
asmCast ILong ILong     = Pure ()
asmCast IFloat IFloat   = Pure ()
asmCast IDouble IDouble = Pure ()

asmCast IBool IInt = boolToInt
asmCast IInt IChar = I2c
asmCast IInt IByte = I2b
asmCast IInt IShort = I2s
asmCast IFloat IDouble = F2d
asmCast IDouble IFloat = D2f

asmCast ty IBool = objToBoolean

asmCast ty IByte = unwrapIntThunk

asmCast ty IChar = objToChar

asmCast ty IShort = unwrapIntThunk

asmCast ty IInt = unwrapIntThunk

asmCast ty ILong = unwrapLongThunk

asmCast ty IFloat = unwrapDoubleThunk

asmCast ty IDouble = unwrapDoubleThunk

asmCast IBool ty = if isThunkType ty then thunkInt else boxBool

asmCast IByte ty = if isThunkType ty then thunkInt else boxByte

asmCast IChar ty = if isThunkType ty then thunkInt else boxChar

asmCast IShort ty = if isThunkType ty then thunkInt else boxShort

asmCast IInt ty =
    if isThunkType ty then thunkInt
    else if ty == inferredBigIntegerType then do
        I2l
        InvokeMethod InvokeStatic "java/math/BigInteger" "valueOf" "(J)Ljava/math/BigInteger;" False
    else boxInt

asmCast ILong ty = if isThunkType ty then thunkLong else boxLong

asmCast IFloat ty = boxFloat

asmCast IDouble ty = if isThunkType ty then thunkDouble else boxDouble

asmCast (IRef _) arr@(IArray _) = Checkcast $ getJvmTypeDescriptor arr

asmCast IVoid IVoid = Pure ()
asmCast IVoid (IRef _) = Aconstnull
asmCast IVoid IUnknown = Aconstnull
asmCast ty IUnknown = when (isThunkType ty) unwrapObjectThunk

asmCast ty1 ty2 = Throw emptyFC $ "Cannot convert from " ++ show ty1 ++ " to " ++ show ty2

loadAndBox : (Int -> Asm ()) -> Asm () -> Map Int InferredType -> Int -> Asm ()
loadAndBox loadOp boxOp sourceLocTys var = let op = \index => do loadOp index; boxOp
                                           in opWithWordSize sourceLocTys op var

loadAndBoxBool : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxBool ty = loadAndBox Iload (if ty == intThunkType then thunkInt else boxBool)

loadAndBoxByte : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxByte ty = loadAndBox Iload (if ty == intThunkType then thunkInt else boxByte)

loadAndBoxChar : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxChar ty = loadAndBox Iload (if ty == intThunkType then thunkInt else boxChar)

loadAndBoxShort : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxShort ty = loadAndBox Iload (if ty == intThunkType then thunkInt else boxShort)

loadAndBoxInt : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxInt ty = loadAndBox Iload (if ty == intThunkType then thunkInt else boxInt)

loadAndBoxLong : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxLong ty = loadAndBox Lload (if ty == longThunkType then thunkLong else boxLong)

loadAndBoxFloat : Map Int InferredType -> Int -> Asm ()
loadAndBoxFloat = loadAndBox Fload boxFloat

loadAndBoxDouble : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndBoxDouble ty = loadAndBox Dload (if ty == doubleThunkType then thunkDouble else boxDouble)

loadAndUnboxBool : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxBool ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == intThunkType then unwrapIntThunk else boolObjToBool
    in opWithWordSize sourceLocTys loadInstr var

loadAndUnboxByte : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxByte ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == intThunkType then unwrapIntThunk else objToByte
    in opWithWordSize sourceLocTys loadInstr var

loadAndUnboxChar : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxChar ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == intThunkType then unwrapIntThunkToChar else objToChar
    in opWithWordSize sourceLocTys loadInstr var

loadAndUnboxShort : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxShort ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == intThunkType then unwrapIntThunk else objToShort
    in opWithWordSize sourceLocTys loadInstr var

loadAndUnboxInt : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxInt ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == intThunkType then unwrapIntThunk else objToInt
    in opWithWordSize sourceLocTys loadInstr var

loadAndUnboxDouble : InferredType -> Map Int InferredType -> Int -> Asm ()
loadAndUnboxDouble ty sourceLocTys var =
    let loadInstr = \index => do Aload index; if ty == doubleThunkType then unwrapDoubleThunk else objToDouble
    in opWithWordSize sourceLocTys loadInstr var

export
loadVar : Map Int InferredType -> (srcTy: InferredType) -> (targetTy: InferredType) -> Int -> Asm ()
loadVar sourceLocTys IBool IBool var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IByte IByte var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IChar IChar var  = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IShort IShort var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IBool IInt  var = opWithWordSize sourceLocTys (\var => do Iload var; boolToInt) var
loadVar sourceLocTys IByte IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IChar IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IShort IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IInt IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IInt IChar  var = opWithWordSize sourceLocTys (\var => do Iload var; I2c) var
loadVar sourceLocTys IInt IByte  var = opWithWordSize sourceLocTys (\var => do Iload var; I2b) var
loadVar sourceLocTys IInt IShort  var = opWithWordSize sourceLocTys (\var => do Iload var; I2s) var
loadVar sourceLocTys ILong ILong  var = opWithWordSize sourceLocTys Lload var
loadVar sourceLocTys IFloat IFloat var = opWithWordSize sourceLocTys Fload var
loadVar sourceLocTys IFloat IDouble var = opWithWordSize sourceLocTys (\var => do Fload var; F2d) var
loadVar sourceLocTys IDouble IDouble var = opWithWordSize sourceLocTys Dload var
loadVar sourceLocTys IDouble IFloat var = opWithWordSize sourceLocTys (\var => do Dload var; D2f)  var

loadVar sourceLocTys IBool ty var = loadAndBoxBool ty sourceLocTys var
loadVar sourceLocTys IByte ty var = loadAndBoxByte ty sourceLocTys var
loadVar sourceLocTys IChar ty var = loadAndBoxChar ty sourceLocTys var
loadVar sourceLocTys IShort ty var  = loadAndBoxShort ty sourceLocTys var
loadVar sourceLocTys IInt ty var  = loadAndBoxInt ty sourceLocTys var

loadVar sourceLocTys ILong ty var = loadAndBoxLong ty sourceLocTys var

loadVar sourceLocTys IFloat _ var = loadAndBoxFloat sourceLocTys var

loadVar sourceLocTys IDouble ty var = loadAndBoxDouble ty sourceLocTys var

loadVar sourceLocTys ty IBool var = loadAndUnboxBool ty sourceLocTys var

loadVar sourceLocTys ty IByte var = loadAndUnboxByte ty sourceLocTys var

loadVar sourceLocTys ty IChar var = loadAndUnboxChar ty sourceLocTys var

loadVar sourceLocTys ty IShort var = loadAndUnboxShort ty sourceLocTys var

loadVar sourceLocTys ty IInt var = loadAndUnboxInt ty sourceLocTys var

loadVar sourceLocTys ty ILong var =
    let loadInstr = \index => do Aload index; longObjToLong
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys ty IFloat var =
    let loadInstr = \index => do Aload index; objToFloat
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys ty IDouble var = loadAndUnboxDouble ty sourceLocTys var

loadVar sourceLocTys IUnknown arr@(IArray _) var =
    let loadInstr = \index => do Aload index; checkcast $ getJvmTypeDescriptor arr
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown ty2@(IRef _) var =
    let loadInstr = \index => do Aload index; asmCast IUnknown ty2
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys (IRef _) IUnknown var = opWithWordSize sourceLocTys Aload var
loadVar sourceLocTys IUnknown IUnknown var = opWithWordSize sourceLocTys Aload var

loadVar sourceLocTys ty1@(IRef _) ty2@(IRef _) var =
    let loadInstr = \index => do Aload index; asmCast ty1 ty2
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys ty1 ty2 var = Throw emptyFC ("Cannot load variable " ++ show var ++ " of type " ++ show ty1 ++
    " to type " ++ show ty2)

storeVarWithWordSize : (Int -> Asm ()) -> Int -> Asm ()
storeVarWithWordSize storeOp var = opWithWordSize !getVariableTypes storeOp var

boxStore : Asm () -> Int -> Asm ()
boxStore boxOp var = storeVarWithWordSize (\index => do boxOp; Astore index) var

export
storeVar : (srcTy: InferredType) -> (targetTy: InferredType) -> Int -> Asm ()
storeVar IBool IBool     var = do types <- getVariableTypes; opWithWordSize types Istore var
storeVar IByte IByte     var = do types <- getVariableTypes; opWithWordSize types Istore var
storeVar IChar IChar     var = do types <- getVariableTypes; opWithWordSize types Istore var
storeVar IShort IShort   var = do types <- getVariableTypes; opWithWordSize types Istore var
storeVar IInt IInt       var = do types <- getVariableTypes; opWithWordSize types Istore var
storeVar ILong ILong     var = do types <- getVariableTypes; opWithWordSize types Lstore var
storeVar IFloat IFloat   var = do types <- getVariableTypes; opWithWordSize types Fstore var
storeVar IDouble IDouble var = do types <- getVariableTypes; opWithWordSize types Dstore var

storeVar IBool ty var = boxStore (if ty == intThunkType then thunkInt else boxBool) var
storeVar IByte ty var = boxStore (if ty == intThunkType then thunkInt else boxByte) var
storeVar IChar ty var = boxStore (if ty == intThunkType then thunkInt else boxChar) var
storeVar IShort ty var = boxStore (if ty == intThunkType then thunkInt else boxShort) var
storeVar IInt ty var = boxStore (if ty == intThunkType then thunkInt else boxInt) var
storeVar ILong ty var = boxStore boxLong var
storeVar IFloat ty var = boxStore boxFloat var
storeVar IDouble ty var = boxStore (if ty == intThunkType then thunkDouble else boxDouble) var

storeVar ty IBool var = storeVarWithWordSize (\index => do asmCast ty IBool; Istore index) var

storeVar ty IByte var = storeVarWithWordSize (\index => do asmCast ty IByte; Istore index) var

storeVar ty IChar var = storeVarWithWordSize (\index => do asmCast ty IChar; Istore index) var

storeVar ty IShort var = storeVarWithWordSize (\index => do asmCast ty IShort; Istore index) var

storeVar ty IInt var = storeVarWithWordSize (\index => do asmCast ty IInt; Istore index) var

storeVar ty ILong var = storeVarWithWordSize (\index => do asmCast ty ILong; Lstore index) var

storeVar ty IFloat var = storeVarWithWordSize (\index => do asmCast ty IFloat; Fstore index) var

storeVar ty IDouble var = storeVarWithWordSize (\index => do asmCast ty IDouble; Dstore index) var

storeVar ty arr@(IArray elemTy) var =
    storeVarWithWordSize (\index => do checkcast $ getJvmTypeDescriptor arr; Astore index) var

storeVar ty targetTy@(IRef _) var = do
    types <- getVariableTypes
    asmCast ty targetTy
    opWithWordSize types Astore var

storeVar _ _ var = opWithWordSize !getVariableTypes Astore var


text:
module Quantities.FreeAbelianGroup

import Quantities.Power

%default total
%access public export

mergeWithBy : (k -> k -> Ordering) -> (v -> v -> v) ->
              List (k, v) -> List (k, v) -> List (k, v)
mergeWithBy _ _ [] ys = ys
mergeWithBy _ _ xs [] = xs
mergeWithBy order combine ((k1, v1) :: xs) ((k2, v2) :: ys) = let o = order k1 k2 in
  if o == LT then (k1, v1) :: mergeWithBy order combine xs ((k2, v2) :: ys)
  else if o == GT then (k2, v2) :: mergeWithBy order combine ((k1, v1) :: xs) ys
  else (k1, combine v1 v2) :: mergeWithBy order combine xs ys

mergeWith : Ord k => (v -> v -> v) ->
            List (k, v) -> List (k, v) -> List (k, v)
mergeWith = mergeWithBy compare

filterValues : (v -> Bool) -> List (k, v) -> List (k, v)
filterValues p = filter (p . snd)

mapValue : (v -> w) -> List (k, v) -> List (k, w)
mapValue f = map (\(k, v) => (k, f v))

data FreeAbGrp : Type -> Type where
  MkFreeAbGrp : {a : Type} -> (List (a, Integer)) -> FreeAbGrp a

mkFreeAbGrp : Ord a => List (a, Integer) -> FreeAbGrp a
mkFreeAbGrp = MkFreeAbGrp . filterValues (\x => x /= 0)
                          . foldr (\x => mergeWith (+) [x]) []

unit : FreeAbGrp a
unit = MkFreeAbGrp []

implicit
inject : a -> FreeAbGrp a
inject x = MkFreeAbGrp [(x, 1)]

freeAbGrpPower : FreeAbGrp a -> Integer -> FreeAbGrp a
freeAbGrpPower _ 0 = unit
freeAbGrpPower (MkFreeAbGrp xs) i = MkFreeAbGrp $ mapValue (i*) xs

freeAbGrpInverse : FreeAbGrp a -> FreeAbGrp a
freeAbGrpInverse x = freeAbGrpPower x (-1)

infixl 6 <<+>>
(<<+>>) : Ord a => FreeAbGrp a -> FreeAbGrp a -> FreeAbGrp a
(MkFreeAbGrp xs) <<+>> (MkFreeAbGrp ys) = MkFreeAbGrp $ filterValues (\x => x /= 0) $ mergeWithBy compare (+) xs ys

implementation Eq a => Eq (FreeAbGrp a) where
  (MkFreeAbGrp xs) == (MkFreeAbGrp ys) = xs == ys

implementation Ord a => Ord (FreeAbGrp a) where
  compare (MkFreeAbGrp xs) (MkFreeAbGrp ys) = compare xs ys

implementation [freeabgrppower] Power (FreeAbGrp a) where
  (^) = freeAbGrpPower

implementation Ord a => Semigroup (FreeAbGrp a) where
  (<+>) = (<<+>>)

implementation Ord a => Monoid (FreeAbGrp a) where
  neutral = unit

implementation Ord a => Group (FreeAbGrp a) where
  inverse = freeAbGrpInverse

implementation Ord a => AbelianGroup (FreeAbGrp a) where

-- Lift a function A -> G to a group homomorphism between the freely generated
-- abelian group of A to the group G.
lift : (Group g, Power g) => (a -> g) -> FreeAbGrp a -> g
lift f (MkFreeAbGrp xs) = concatMap (\(x, i) => ((f x) ^ i)) xs

inject_lift_lem : (Group g, Power g) => (f : a -> g) -> (x : a) -> lift f (inject x) = f x
inject_lift_lem f x = really_believe_me (Refl {x=(lift f (inject x))})

lift_power_lem : (Group g, Power g, Ord a) => (f : a -> g) -> (x : FreeAbGrp a) ->
                 (i : Integer) -> lift f (x ^ i) = lift f x ^ i
lift_power_lem f x i = really_believe_me (Refl {x=(lift f (x ^ i))})

lift_mult_lem : (Ord a, Group g, Power g) => (f : a -> g) -> (x : FreeAbGrp a) ->
                (y : FreeAbGrp a) -> lift f (x <+> y) = lift f x <+> lift f y
lift_mult_lem f x y = really_believe_me (Refl {x=(lift f (x <+> y))})

freeabgrppower_correct : (Ord a) => (x : FreeAbGrp a) -> (i : Integer) -> freeAbGrpPower x i = (^) x i
freeabgrppower_correct x i = really_believe_me (Refl {x=(freeAbGrpPower x i)})

ext: idr

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module Control.App

import Data.List
import Data.IORef

public export
data Effect : Type where
     St : Type -> Effect
     Exc : Type -> Effect
     Sys : Effect

public export
data HasEff : Effect -> List Effect -> Type where
     Here : HasEff e (e :: es)
     There : HasEff e es -> HasEff e (e' :: es)

public export
0 Has : List (a -> Type) -> a -> Type
Has [] es = ()
Has [e] es = e es
Has (e :: es') es = (e es, Has es' es)

export
data Env : List Effect -> Type where
     None : Env []
     Ref : IORef t -> Env es -> Env (St t :: es)
     SkipE : Env es -> Env (Exc t :: es)
     SkipP : Env es -> Env (Sys :: es)

getState : Env es -> (p : HasEff (St t) es) -> IORef t
getState (Ref r env) Here = r
getState (Ref r env) (There p) = getState env p
getState (SkipE env) (There p) = getState env p
getState (SkipP env) (There p) = getState env p

public export
data Path : Type where
     [noHints]
     MayThrow : Path
     NoThrow : Path

%hint public export
dpath : Path
dpath = MayThrow

data OneOf : List Type -> Path -> Type where
     First : e -> OneOf (e :: es) MayThrow
     Later : OneOf es MayThrow -> OneOf (e :: es) MayThrow

updateP : OneOf es p -> OneOf es p'
updateP {p=MayThrow} {p'=MayThrow} x = x

Uninhabited (OneOf [] p) where
  uninhabited (First x) impossible
  uninhabited (Later x) impossible

Uninhabited (OneOf es NoThrow) where
  uninhabited (First x) impossible
  uninhabited (Later x) impossible

public export
0 excTy : List Effect -> List Type
excTy [] = []
excTy (St t :: es) = excTy es
excTy (Exc e :: es) = e :: excTy es
excTy (Sys :: es) = excTy es

0 execTy : Path -> List Effect -> Type -> Type
execTy p es ty = Either (OneOf (excTy es) p) ty

export
data App : (l : Path) => (es : List Effect) -> Type -> Type where
     MkApp : (1 prog : Env e -> IO (execTy l e t)) -> App {l} e t

pureApp : a -> App {l} e a
pureApp x = MkApp (\env => pure (Right x))

public export
data SafeBind : Path -> (l' : Path) -> Type where
     [search l']
     SafeSame : SafeBind l l
     SafeToThrow : SafeBind NoThrow MayThrow

bindApp : SafeBind l l' =>
          App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
bindApp (MkApp prog) k
    = MkApp $ \env =>
              do Right res <- prog env
                       | Left err => pure (Left (updateP err))
                 let MkApp ka = k res
                 ka env

absurdWith : (1 x : a) -> OneOf e NoThrow -> any
absurdWith x (First p) impossible

export
bindL : App {l=NoThrow} e a -> (1 k : a -> App {l} e b) -> App {l} e b
bindL (MkApp prog) k
    = MkApp $ \env =>
              io_bind (prog env) $ \r =>
                   case r of
                        Left err => absurdWith k err
                        Right res =>
                              let MkApp ka = k res in ka env

export
lift : App e t -> App (eff :: e) t
lift (MkApp p)
    = MkApp (\env =>
          case env of
               Ref r env' => p env'
               SkipP env' => p env'
               SkipE env' =>
                  do res <- p env'
                     case res of
                          Left err => pure (Left (Later err))
                          Right ok => pure (Right ok))

export
Functor (App {l} es) where
  map f ap = bindApp ap $ \ap' => pureApp (f ap')

export
Applicative (App {l} es) where
  pure = pureApp
  (<*>) f a = bindApp f $ \f' =>
              bindApp a $ \a' => pure (f' a')

export
Monad (App es) where
  (>>=) = bindApp -- won't get used, but handy to have the instance

export
(>>=) : SafeBind l l' =>
        App {l} e a -> (k : a -> App {l=l'} e b) -> App {l=l'} e b
(>>=) = bindApp

export
new : a -> App {l} (St a :: es) t -> App {l} es t
new val (MkApp prog)
    = MkApp $ \env =>
          do ref <- newIORef val
             prog (Ref ref env)

public export
interface State t es where
  get : App {l} es t
  put : t -> App {l} es ()

export
HasEff (St t) es => State t es where
  get
      = MkApp $ \env =>
            do let ref = getState env %search
               val <- readIORef ref
               pure (Right val)
  put val
      = MkApp $ \env =>
            do let ref = getState env %search
               writeIORef ref val
               pure (Right ())

public export
interface Exception e es where
  throw : e -> App es a
  catch : App es a -> (err : e -> App es a) -> App es a

findException : Env es -> HasEff (Exc e) es -> e -> OneOf (excTy es) MayThrow
findException (SkipE env) Here err = First err
findException (Ref r env) (There p) err = findException env p err
findException (SkipE env) (There p) err = Later $ findException env p err
findException (SkipP env) (There p) err = findException env p err

findError : Env es -> HasEff (Exc e) es -> OneOf (excTy es) MayThrow -> Maybe e
findError (SkipE env) Here (First err) = Just err
findError (SkipE env) Here (Later p) = Nothing -- wrong exception
findError (SkipE env) (There p) (First err) = Nothing -- wrong exception
findError (SkipE env) (There p) (Later q) = findError env p q
findError (Ref r env) (There p) err = findError env p err
findError (SkipP env) (There p) err = findError env p err

export
HasEff (Exc e) es => Exception e es where
  throw err
      = MkApp $ \env =>
           pure (Left (findException env %search err))
  catch (MkApp prog) handler
      = MkApp $ \env =>
           do res <- prog env
              case res of
                   Left err =>
                        case findError env %search err of
                             Nothing => pure (Left err)
                             Just err' =>
                                  let MkApp e' = handler err' in
                                      e' env
                   Right ok => pure (Right ok)

export
handle : App (Exc err :: e) a ->
         (onok : a -> App e b) ->
         (onerr : err -> App e b) -> App e b
handle (MkApp prog) onok onerr
    = MkApp $ \env =>
          do res <- prog (SkipE env)
             case res of
                  Left (First err) =>
                        let MkApp err' = onerr err in
                            err' env
                  Left (Later p) =>
                        -- different exception, so rethrow
                        pure (Left p)
                  Right ok =>
                        let MkApp ok' = onok ok in
                            ok' env

public export
interface PrimIO es where
  primIO : IO a -> App {l} es a
  -- Copies the environment, to make sure states are local to threads
  fork : App es () -> App {l} es ()

copyEnv : Env es -> IO (Env es)
copyEnv None = pure None
copyEnv (Ref t env)
    = do val <- readIORef t
         t' <- newIORef val
         env' <- copyEnv env
         pure (Ref t' env')
copyEnv (SkipE env)
    = do env' <- copyEnv env
         pure (SkipE env')
copyEnv (SkipP env)
    = do env' <- copyEnv env
         pure (SkipP env')

export
HasEff Sys es => PrimIO es where
  primIO io
      = MkApp $ \env =>
            do res <- io
               pure (Right res)
  fork (MkApp p)
      = MkApp $ \env =>
            do fork (do env' <- copyEnv env
                        p env'
                        pure ())
               pure (Right ())

public export
Init : List Effect
Init = [Sys]

export
run : App Init a -> IO a
run (MkApp prog)
    = do Right res <- prog (SkipP None)
               | Left err => absurd err
         pure res

infix 5 @@

public export
data Res : (a : Type) -> (a -> Type) -> Type where
     (@@) : (val : a) -> (1 r : t val) -> Res a t


text:
[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1

test : Monoid a => a -> a
test x = x <+> x <+> neutral

[CmpLess] Ord Int where
  compare x y = if (x == y) then EQ else
                   if (boolOp prim__sltInt x y) then GT else LT

foo : Int -> Int -> Bool
foo x y = x < y

using implementation CmpLess
  foo' : Int -> Int -> Bool
  foo' x y = x < y

using implementation PlusNatMonoid
  main : IO ()
  main = do printLn (test (the Nat 6))
            printLn (test @{MultNatMonoid} 6)

            printLn (foo 3 4)
            printLn (foo' 3 4)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Extra.C.Float

import Extra.C.FFI
import Extra.C.Types

-- DO NOT public export, otherwise it will be evaluated to canonical form
export
CFloat : Type
CFloat = Bits32

%foreign libextra "double_to_cfloat"
export
prim__double_to_cfloat : CDouble -> PrimIO CFloat

%foreign libextra "cfloat_to_double"
export
prim__cfloat_to_double : CFloat -> PrimIO CDouble

%foreign libextra "cfloat_add"
export
prim__cfloat_add : CFloat -> CFloat -> PrimIO CFloat

%foreign libextra "cfloat_sub"
export
prim__cfloat_sub : CFloat -> CFloat -> PrimIO CFloat

%foreign libextra "cfloat_neg"
export
prim__cfloat_neg : CFloat -> PrimIO CFloat

%foreign libextra "cfloat_mul"
export
prim__cfloat_mul : CFloat -> CFloat -> PrimIO CFloat

%foreign libextra "cfloat_div"
export
prim__cfloat_div : CFloat -> CFloat -> PrimIO CFloat

%foreign libextra "cfloat_recip"
export
prim__cfloat_recip : CFloat -> PrimIO CFloat

%foreign libextra "cfloat_abs"
export
prim__cfloat_abs : CFloat -> PrimIO CFloat

%foreign libextra "peek_float_t"
prim__peek_float_t : Ptr CFloat -> PrimIO CFloat

%foreign libextra "poke_float_t"
prim__poke_float_t : Ptr CFloat -> CFloat -> PrimIO ()

export
peekFloat : Ptr CFloat -> PrimIO CFloat
peekFloat ptr = prim__peek_float_t ptr

export
pokeFloat : Ptr CFloat -> CFloat -> PrimIO ()
pokeFloat ptr x = prim__poke_float_t ptr x

export
fromDouble : CDouble -> CFloat
fromDouble d = unsafePerformIO $ primIO $ prim__double_to_cfloat d

export
toDouble : CFloat -> CDouble
toDouble d = unsafePerformIO $ primIO $ prim__cfloat_to_double d

export
Show CFloat where
  show x = (show $ toDouble x) <+> "f"

export
[FloatNum] Num CFloat where
  a + b = unsafePerformIO $ primIO $ prim__cfloat_add a b
  a * b = unsafePerformIO $ primIO $ prim__cfloat_mul a b
  fromInteger = fromDouble . fromInteger

export
Neg CFloat using FloatNum where
  negate a = unsafePerformIO $ primIO $ prim__cfloat_neg a
  a - b = unsafePerformIO $ primIO $ prim__cfloat_sub a b

export
Fractional CFloat using FloatNum where
  a / b = unsafePerformIO $ primIO $ prim__cfloat_div a b
  recip a = unsafePerformIO $ primIO $ prim__cfloat_recip a

export
Abs CFloat using FloatNum where
  abs a = unsafePerformIO $ primIO $ prim__cfloat_abs a


text:
module Extra.C.Storable

import Extra.C.FFI
import Extra.C.Types
import Extra.C.Float
import Extra.C.Ptr
import Data.List

export
interface Storable a where
  sizeOfType : SizeT
  peek : HasIO io => Ptr a -> io a
  poke : HasIO io => Ptr a -> a -> io ()

%foreign libextra "peek_uint8_t"
prim__peek_uint8_t : Ptr CUInt8 -> PrimIO CUInt8

%foreign libextra "poke_uint8_t"
prim__poke_uint8_t : Ptr CUInt8 -> CUInt8 -> PrimIO ()

%foreign libextra "peek_uint16_t"
prim__peek_uint16_t : Ptr CUInt16 -> PrimIO CUInt16

%foreign libextra "poke_uint16_t"
prim__poke_uint16_t : Ptr CUInt16 -> CUInt16 -> PrimIO ()

%foreign libextra "peek_uint32_t"
prim__peek_uint32_t : Ptr CUInt32 -> PrimIO CUInt32

%foreign libextra "poke_uint32_t"
prim__poke_uint32_t : Ptr CUInt32 -> CUInt32 -> PrimIO ()

%foreign libextra "peek_uint64_t"
prim__peek_uint64_t : Ptr CUInt64 -> PrimIO CUInt64

%foreign libextra "poke_uint64_t"
prim__poke_uint64_t : Ptr CUInt64 -> CUInt64 -> PrimIO ()

%foreign libextra "peek_int32_t"
prim__peek_int32_t : Ptr CInt32 -> PrimIO CInt32

%foreign libextra "poke_int32_t"
prim__poke_int32_t : Ptr CInt32 -> CInt32 -> PrimIO ()

%foreign libextra "peek_double_t"
prim__peek_double_t : Ptr CDouble -> PrimIO CDouble

%foreign libextra "poke_double_t"
prim__poke_double_t : Ptr CDouble -> CDouble -> PrimIO ()

export
Storable CInt32 where
  sizeOfType = 4
  peek ptr = primIO $ prim__peek_int32_t ptr
  poke ptr x = primIO $ prim__poke_int32_t ptr x

export
Storable CUInt8 where
  sizeOfType = 1
  peek ptr = primIO $ prim__peek_uint8_t ptr
  poke ptr x = primIO $ prim__poke_uint8_t ptr x

export
Storable CUInt16 where
  sizeOfType = 2
  peek ptr = primIO $ prim__peek_uint16_t ptr
  poke ptr x = primIO $ prim__poke_uint16_t ptr x

export
Storable CUInt32 where
  sizeOfType = 4
  peek ptr = primIO $ prim__peek_uint32_t ptr
  poke ptr x = primIO $ prim__poke_uint32_t ptr x

export
Storable CUInt64 where
  sizeOfType = 8
  peek ptr = primIO $ prim__peek_uint64_t ptr
  poke ptr x = primIO $ prim__poke_uint64_t ptr x

export
Storable CFloat where
  sizeOfType = 4
  peek ptr = primIO $ peekFloat ptr
  poke ptr x = primIO $ pokeFloat ptr x

export
Storable CDouble where
  sizeOfType = 8
  peek ptr = primIO $ prim__peek_double_t ptr
  poke ptr x = primIO $ prim__poke_double_t ptr x

export
withThe : (HasIO io, Storable a) => (Ptr a -> io b) -> io b
withThe f = do
  ptr <- primIO $ prim__malloc (sizeOfType {a=a})
  ret <- f (castPtr ptr)
  primIO $ prim__free ptr
  pure ret

export
pokeArray : (HasIO io, Storable a) => Ptr a -> List a -> io ()
pokeArray ptr Nil = pure ()
pokeArray ptr (x :: xs) = do
  poke ptr x
  pokeArray (plusPtr ptr (cast $ sizeOfType {a=a})) xs

export
withArray : (HasIO io, Storable a) => List a -> (Ptr a -> io b) -> io b
withArray list f = do
  let len = cast $ natToInteger $ length list
  ptr <- primIO $ prim__malloc (sizeOfType {a=a} * len)
  pokeArray (castPtr ptr) list
  ret <- f (castPtr ptr)
  primIO $ prim__free ptr
  pure ret

export
withCString : HasIO io => String -> (CString -> io a) -> io a
withCString str = withArray (map (cast . ord) (unpack str `snoc` '\0'))

export
peekArray : (HasIO io, Storable a) => SizeT -> Ptr a -> io (List a)
peekArray 0      ptr = pure []
peekArray length ptr = do
  x <- peek ptr
  let ptr' = plusPtr ptr (cast (sizeOfType {a=a}))
  let length' = cast $ cast {to = Integer} length - 1
  xs <- peekArray length' ptr'
  pure $ x :: xs

export
peekArray0 : (HasIO io, Storable a, Eq a) => a -> Ptr a -> io (List a)
peekArray0 end ptr = do
  x <- peek ptr
  case x == end of
    True => pure []
    False => do
      let ptr' = plusPtr ptr (cast (sizeOfType {a=a}))
      xs <- peekArray0 end ptr'
      pure $ x :: xs

export
peekCString : (HasIO io) => CString -> io String
peekCString ptr = do
  arr <- peekArray0 0 ptr
  pure $ pack $ map (chr . cast) arr


text:
{- 1 -}

data TakeN : List a -> Type where
     Fewer : TakeN xs
     Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) with (takeN k xs)
  takeN (S k) (x :: xs) | Fewer = Fewer
  takeN (S k) (x :: (n_xs ++ rest)) | Exact _ = Exact (x :: n_xs)

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

{- 2 -}

halves : List a -> (List a, List a)
halves input with (takeN (length input `div` 2) input)
  halves input | Fewer = (input, [])
  halves (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Graph.DictStub

import Data.SortedMap as M

%access export

-- A stub of Haskell's `IntMap` API but with arbitrary keys.
-- The implementation may be highly inefficient.

DictStub : Type -> Type -> Type
DictStub k v = SortedMap k v

empty : Ord k => DictStub k v
empty = M.empty

||| Insert k new key/value pair in the map.
||| If the key is already present in the map, the associated value
||| is replaced with the supplied value
insert : k -> v -> DictStub k v -> DictStub k v
insert = M.insert

||| Insert with a combining function. `insertWith f key value mp` will
||| insert the pair `(key, value)` into `mp` if `key` does not exist in the
||| map. If the key does exist, the function will insert f new_value
||| old_value
insertWith : (v -> v -> v) -> k -> v -> DictStub k v -> DictStub k v
insertWith f key value mp
  = case M.lookup key mp of
         Nothing => M.insert key value mp
         (Just old_value) => M.insert key (f value old_value) mp

||| Number of elements in the map
size : DictStub k v -> Nat
size = length . M.toList

||| Convert the map to a list of key/pairs. Subject to list fusion
toList : DictStub k v -> List (k, v)
toList = M.toList

||| Lookup the value at a key in the map
lookup : k -> DictStub k v -> Maybe v
lookup = M.lookup

||| Delete a key and its value from the map. When the key is not a member
||| of the map, the original map is returned.
delete : k -> DictStub k v -> DictStub k v
delete = M.delete

selectViewWithk : Ord k => Ordering -> DictStub k v -> Maybe ((k, v), DictStub k v)
selectViewWithk ordering mp
  = case M.toList mp of
         [] => Nothing
         (x :: xs) => let selected = foldr select x xs in
                          Just (selected, M.delete (fst selected) mp)
  where
    select : Ord k => (k, v) -> (k, v) -> (k, v)
    select elem@(key, value) acc@(skey, svalue)
     = if (compare skey key) == ordering then acc else elem

||| Retrieves the maximal (key, value) pair of the map, and the map
||| stripped of that element, or `Nothing` if passed an empty map.
maxViewWithk : Ord k => DictStub k v -> Maybe ((k, v), DictStub k v)
maxViewWithk = selectViewWithk GT

||| Retrives the minimal (key, value) pair of the map, and the map
||| stripped of that element, or `Nothing` if passed and empty map
minViewWithk : Ord k => DictStub k v -> Maybe ((k, v), DictStub k v)
minViewWithk = selectViewWithk LT

||| Return all keys of the map in ascending order. Subject to list fusion.
keys : DictStub k v -> List k
keys = map fst . M.toList

||| Map a function over all values in the map.
mapWithKey : Ord k => (k -> v1 -> v2) -> DictStub k v1 -> DictStub k v2
mapWithKey f = M.fromList . map (\(key, value) => (key, f key value)) . M.toList

||| Map a function over all values in the map.
map : Ord k => (v1 -> v2) -> DictStub k v1 -> DictStub k v2
map f = mapWithKey (\key, value => f value)

||| Build a map from a list of key/value pairs.
fromList : Ord k => List (k, v) -> DictStub k v
fromList = M.fromList

||| Build a map from a list of key/value pairs with a combining function.
fromListWith : Ord k => (v -> v -> v) -> List (k, v) -> DictStub k v
fromListWith f = foldr proc Data.SortedMap.empty where
  proc : (k, v) -> DictStub k v -> DictStub k v
  proc (key, value) = insertWith f key value

||| Adjust a value at a specific key. If the key is not a member of the map,
||| the original map is returned.
adjust : (v -> v) -> k -> DictStub k v -> DictStub k v
adjust f key mp
  = case M.lookup key mp of
         Nothing => mp
         (Just value) => M.insert key (f value) mp

||| Is the map empty?
null : DictStub a b -> Bool
null mp = case M.toList mp of
               [] => True
               _ => False

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
-- --------------------------------------------------------- [ Description.idr ]
-- Module    : Description.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Data types for modelling abstract descriptions of interfaces.
module Cordial.Model.Specification

import        Data.Vect
import        Data.DList
import public Cordial.Model.Common

%default total
%access public export

||| Individual port in an interface.
|||
record PortTy annot (labelTy : Type) where
  constructor PortDesc
  info : annot
  kind  : PortShape
  label : Name nKind labelTy
  wkind : WireTy
  flow  : Flow
  width : PortWidthDesc kind

  sens  : Sensitivity

  required : OptionalTy
  origin   : Origin

  valueOrigin  : ValueOrigin width
  doc          : DocString

data OptionalPortType : (endpoint : Endpoint) -> (type : PortTy annot labelTy) -> Type where
  IsOptionalPortType : (prf : OptionalKind endpoint optTy OPT)
                    -> OptionalPortType endpoint (PortDesc i k l ty f w s optTy o vo doc)

data SystemPortType : (type : PortTy annot labelTy) -> Type where
   IsSystemPortType : (name : String) -> SystemPortType (PortDesc i k l ty f w s optTy (SYSTEM name) vo doc)

data IPPortType : (type : PortTy annot labelTy) -> Type where
   IsIPPortType : IPPortType (PortDesc i k l ty f w s optTy IP vo doc)

portIsSystem : IPPortType (PortDesc i k l wk f w s r (SYSTEM x) v d)
            -> Void
portIsSystem IsIPPortType impossible

portIsIP : SystemPortType (PortDesc i k l wk f w s r IP v d)
        -> Void
portIsIP (IsSystemPortType _) impossible

isPortTypeSystem : (type : PortTy annot labelTy)
                -> Dec (SystemPortType type)
isPortTypeSystem (PortDesc info kind label wkind flow width sens required (SYSTEM x) valueOrigin doc) = Yes (IsSystemPortType x)
isPortTypeSystem (PortDesc info kind label wkind flow width sens required IP valueOrigin doc) = No portIsIP

isPortTypeIP : (type : PortTy annot labelTy)
           -> Dec (IPPortType type)
isPortTypeIP (PortDesc info kind label wkind flow width sens required (SYSTEM x) valueOrigin doc) = No portIsSystem
isPortTypeIP (PortDesc info kind label wkind flow width sens required IP valueOrigin doc) = Yes IsIPPortType

||| Collection of Ports
PortGroupTy : (annot : Type) -> (labelTy : Type) -> Type
PortGroupTy annot labelTy = List (PortTy annot labelTy)

record Channel (annot : Type) (labelTy : Type) where
  constructor MkChan
  name : String
  info : annot
  ports : PortGroupTy annot labelTy

flatten : List (Channel annot labelTy) -> PortGroupTy annot labelTy
flatten Nil     = Nil
flatten (c::cs) = ports c ++ flatten cs

||| An interface is a list of ports with a given number of producers
||| and consumers, and a communication style.
|||
record InterfaceTy (annot : Type) (labelTy : Type) where
   constructor MkInterfaceTy
   name         : VLNV
   info         : annot
   cstyle       : CommStyle
   maxProducers : Whole
   maxConsumers : Whole
   portGroupTy  : PortGroupTy annot labelTy
   channels     : List (Channel annot labelTy)
   doc          : DocString

fullPortGroupTy : InterfaceTy annot labelTy -> PortGroupTy annot labelTy
fullPortGroupTy iface = (portGroupTy iface) ++ (flatten $ channels iface)

||| Collection of interfaces
data InterfaceTys : (annot : Type) -> (labelTys : List Type)-> Type where
  Nil  : InterfaceTys  annot Nil
  (::) : InterfaceTy   annot labelTy
      -> InterfaceTys  annot hs
      -> InterfaceTys  annot (labelTy::hs)

data IsBroadcast : InterfaceTy annot labelTy -> Type where
  YesIsBroadcast : IsBroadcast (MkInterfaceTy n i Broadcast p c ps cs doc)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
{-
True
0
False
False
4
42
42
True
False
[33, 42, 42, 42, 42]
[42, 42, 33, 42, 42]
[42, 42, 42, 42, 33]
[33, 42, 42, 42]
[42, 42, 33, 42]
[42, 42, 42, 33]
False
True
-}

import Data.Vector

main : IO ()
main = do
  let e = the (Vector Int) empty
  printLn (null e)
  printLn (length e)
  printLn (elem 42 e)
  let a = replicate 4 (the Int 42)
  printLn (null a)
  printLn (length a)
  printLn (a !! 0)
  printLn (a !! 3)
  printLn (elem 42 a)
  printLn (elem 33 a)
  printLn (unsafeInsertAt 0 33 a)
  printLn (unsafeInsertAt 2 33 a)
  printLn (unsafeInsertAt (length a) 33 a)
  printLn (unsafeReplaceAt 0 33 a)
  printLn (unsafeReplaceAt 2 33 a)
  printLn (maybe a (\index => unsafeReplaceAt index 33 a) (lastIndex a))
  printLn (elem 33 a)
  printLn (elem 33 (singleton 33))

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
-- --------------------------------------------------------------- [ State.idr ]
-- Module      : Chapter.State
-- Description : Definitions from Chapter 12 of Edwin Brady's book,
--               "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Chapter.State

-- NOTE: See 12.1.3
import public Control.Monad.State

-- NOTE: See 12.3.6
import Data.Primitives.Views

-- ----------------------------------------- [ 12.1 Working with Mutable State ]

||| Attach labels from `lbls` to elements of `vals`.
||| @ lbls A stream of labels.
||| @ vals A list of values.
export
labelWith : (lbls : Stream labelType) -> (vals : List a) -> List (labelType, a)
labelWith lbls [] = []
labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals

-- ---------------------------------- [ 12.1.1 Running Example: Tree Traversal ]

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

public export
testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

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

-- -------------------------- [ 12.1.2 Representing Mutable State using a Pair ]

export
treeLabelWith : Stream labelType -> Tree a ->
                (Stream labelType, Tree (labelType, a))
treeLabelWith lbls Empty = (lbls, Empty)
treeLabelWith lbls (Node left val right)
  = let (this :: lblsLeft, leftLabelled) = treeLabelWith lbls left
        (lblsRight, rightLabelled) = treeLabelWith lblsLeft right in
        (lblsRight, Node leftLabelled (this, val) rightLabelled)

export
treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = snd (treeLabelWith [1..] tree)

-- ----------------- [ 12.1.3 State, a Type for Describing Stateful Operations ]

export
increase : Nat -> State Nat ()
increase inc = do current <- get
                  put (current + inc)

-- NOTE:
-- runState : StateT stateType Identity a -> stateType -> (a, stateType)
-- evalState : State stateType a -> stateType -> a
-- execState : State stateType a -> stateType -> stateType
-- get : MonadState stateType m => m stateType
-- put : MonadState stateType m => stateType -> m ()

-- ---------------------------------------- [ 12.1.4 Tree Traversal with State ]

namespace Stateful
  export
  treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
  treeLabelWith Empty = pure Empty
  treeLabelWith (Node left val right)
    = do leftLabelled <- treeLabelWith left
         -- Get the current stream of labels.
         (this :: rest) <- get
         -- Set the new stream of labels to be
         -- the tail of the current stream, rest.
         put rest
         rightLabelled <- treeLabelWith right
         pure (Node leftLabelled (this, val) rightLabelled)

  export
  treeLabel : Tree a -> Tree (Integer, a)
  treeLabel tree = evalState (treeLabelWith tree) [1..]

-- ----------------------------------------------------------- [ Listing 12.13 ]

export
addIfPositive : Integer -> State Integer Bool
addIfPositive val = do let positive = val > 0
                       when positive $ update (+ val)
                       pure positive
  where
    update = (get >>=) . (put .)

export
addPositives : List Integer -> State Integer Nat
addPositives vals = do added <- traverse addIfPositive vals
                       pure (length (filter id added))

-- ---------------------------------------------------- [ 12.3.2 Complex State ]

public export
record Score where
       constructor MkScore
       correct, attempted : Nat

public export
record GameState where
       constructor MkGameState
       score : Score
       difficulty : Int

public export
implementation Show GameState where
  show st = show (record { score->correct } st) ++ " / " ++
            show (record { score->attempted } st) ++ "\n" ++
            "Difficulty: " ++ show (difficulty st)

export
initState : GameState
initState = MkGameState (MkScore 0 0) 12

-- ------------------------------------- [ 12.3.1 The Arithmetic Quiz Revisted ]

public export
data Command : Type -> Type where
     PutStr : String -> Command ()
     GetLine : Command String

     GetRandom : Command Int

     GetGameState : Command GameState

     PutGameState : GameState -> Command ()

     Pure : ty -> Command ty
     Bind : Command a -> (a -> Command b) -> Command b

public export
data ConsoleIO : Type -> Type where
     Quit : a -> ConsoleIO a
     Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace CommandDo

  public export
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

namespace ConsoleDo

  public export
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) =  Do

public export
data Fuel = Dry | More (Lazy Fuel)

public export
partial
forever : Fuel
forever = More forever

-- ----------------------------------------------- [ 12.3.6 Executing the Quiz ]

export
runCommand : Stream Int ->
             GameState ->
             Command a ->
             IO (a, Stream Int, GameState)
runCommand rnds state (PutStr x) = do putStr x
                                      pure ((), rnds, state)
runCommand rnds state GetLine    = do str <- getLine
                                      pure (str, rnds, state)

runCommand (val :: rnds) state GetRandom =
  pure (getRandom val (difficulty state), rnds, state)
  where
    getRandom : Int -> Int -> Int
    getRandom val max with (divides val max)
      getRandom val 0             | DivByZero = 1
      getRandom ((_ * _) + rem) _ | DivBy prf = abs rem + 1

runCommand rnds state GetGameState            = pure (state, rnds, state)
runCommand rnds state (PutGameState newState) = pure ((), rnds, newState)

runCommand rnds state (Pure val) = pure (val, rnds, state)
runCommand rnds state (Bind c f) =
  do (res, newRnds, newState) <- runCommand rnds state c
     runCommand newRnds newState (f res)

export
run : Fuel -> Stream Int -> GameState -> ConsoleIO a ->
      IO (Maybe a, Stream Int, GameState)
run fuel rnds state (Quit val) = do pure (Just val, rnds, state)
run (More fuel) rnds state (Do cmd f) =
  do (res, newRnds, newState) <- runCommand rnds state cmd
     run fuel newRnds newState (f res)
run Dry rnds state _ = pure (Nothing, rnds, state)

-- ------------------------------------- [ 12.3.3 Updating Record Field Values ]

export
setDifficulty : Int -> GameState -> GameState
setDifficulty newDiff = record { difficulty = newDiff}

export
addWrong : GameState -> GameState
addWrong = record { score->attempted $= (+1) }

export
addCorrect : GameState -> GameState
addCorrect = record { score->correct   $= (+1)
                    , score->attempted $= (+1)
                    }

-- -------------------------------------------- [ 12.3.5 Implementing the Quiz ]

-- Copied from 11.3.3
public export
data Input = Answer Int
           | QuitCmd

mutual
  export
  correct : ConsoleIO GameState
  correct = do PutStr "Correct!\n"
               st <- GetGameState
               PutGameState (addCorrect st)
               quiz
  export
  wrong : Int -> ConsoleIO GameState
  wrong ans = do PutStr $ "Wrong, the answer is " ++ show ans ++ "\n"
                 st <- GetGameState
                 PutGameState (addWrong st)
                 quiz
  export
  readInput : (prompt : String) -> Command Input
  readInput prompt = do PutStr prompt
                        answer <- GetLine
                        if toLower answer == "quit"
                           then Pure QuitCmd
                           else Pure (Answer (cast answer))
  export
  quiz : ConsoleIO GameState
  quiz = do x <- GetRandom
            y <- GetRandom
            st <- GetGameState
            PutStr $ show st ++ "\n"
            let solution = x * y
            QuitCmd <- readInput $ show x ++ " * " ++ show y ++ "? "
              | Answer answer => if solution == answer
                                    then correct
                                    else wrong solution
            Quit st

-- ----------------------------------------------------------- [ Listing 12.32 ]

export
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Sixel.Encoder

import Data.Buffer
import System.FFI

import Sixel.Library
import Sixel.Symbols
import Sixel.Allocator

public export
PrimEncoder : Type
PrimEncoder = GCAnyPtr

export
data Encoder : (0 n : Nat) -> Type where
  PointEncoder : PrimEncoder -> Encoder Z
  RootEncoder  : Encoder n -> Encoder (S n)

%foreign (sixelutils "sixel_utils_int_ptr_new")
sixel_utils_int_ptr_new : Int -> PrimIO (Ptr Int)

%foreign (sixelutils "sixel_utils_encoder_ptr_new")
sixel_utils_encoder_ptr_new : PrimIO (Ptr AnyPtr)

%foreign (sixelutils "sixel_utils_encoder_ptr_deref")
sixel_utils_encoder_ptr_deref : Ptr AnyPtr -> AnyPtr

%foreign (sixel "sixel_encoder_new")
sixel_encoder_new : Ptr AnyPtr -> PrimAllocator -> PrimIO Int

%foreign (sixel "sixel_encoder_ref")
sixel_encoder_ref : PrimEncoder -> ()

%foreign (sixel "sixel_encoder_unref")
sixel_encoder_unref : PrimEncoder -> ()

%foreign (sixel "sixel_encoder_unref")
sixel_encoder_destroy : AnyPtr -> PrimIO ()

%foreign (sixel "sixel_encoder_set_cancel_flag")
sixel_encoder_set_cancel_flag : PrimEncoder -> Ptr Int -> ()

%foreign (sixel "sixel_encoder_setopt")
sixel_encoder_setopt : PrimEncoder -> (optflag : Int) -> (setting : String) -> PrimIO Int

%foreign (sixel "sixel_encoder_encode")
sixel_encoder_encode : PrimEncoder -> (filename : String) -> PrimIO Int

%foreign (sixel "sixel_encoder_encode_bytes")
sixel_encoder_encode_bytes :
  PrimEncoder -> (bytes : Buffer) -> (w : Int) -> (h : Int) ->
    (pixelformat : Int) -> (palette : Buffer) -> (ncolors : Int) ->
    PrimIO Int

export
MkEncoder : {auto n : Nat} -> {default (getNullAllocator n) alloc : Allocator n} -> IO (Either Status (Encoder Z))
MkEncoder {alloc} = do
  ppencoder <- fromPrim sixel_utils_encoder_ptr_new
  status    <- MkStatus <$> fromPrim (sixel_encoder_new ppencoder (toPrim alloc))
  pencoder  <- onCollectAny (sixel_utils_encoder_ptr_deref ppencoder) (\pe => fromPrim $ sixel_encoder_destroy pe)
  pure $ if succeeded status then Right (PointEncoder pencoder) else Left status

export
ref : Encoder n -> IO (Encoder (S n))
ref (RootEncoder encoder)           = RootEncoder <$> ref encoder
ref encoder@(PointEncoder pencoder) = let _ = sixel_encoder_ref pencoder in pure $ RootEncoder encoder

export
unref : Encoder (S n) -> IO (Encoder n)
unref (RootEncoder encoder@(RootEncoder _))         = RootEncoder <$> unref encoder
unref (RootEncoder encoder@(PointEncoder pencoder)) = let _ = sixel_encoder_unref pencoder in pure encoder

export
refs : Encoder n -> Nat
refs (RootEncoder encoder) = S (refs encoder)
refs (PointEncoder _)      = Z

export
toPrim : Encoder n -> PrimEncoder
toPrim (RootEncoder encoder)   = toPrim encoder
toPrim (PointEncoder pencoder) = pencoder

export
setCancelFlag : Encoder n -> (setting : Bool) -> IO ()
setCancelFlag encoder setting = do
  cancelFlag <- fromPrim $ sixel_utils_int_ptr_new $ ifThenElse setting 1 0
  pure $ sixel_encoder_set_cancel_flag (toPrim encoder) cancelFlag

export
setOpt : Encoder n -> (optflag : OptFlag) -> (setting : String) -> IO (Either Status ())
setOpt encoder optflag setting = do
  status <- MkStatus <$> fromPrim (sixel_encoder_setopt (toPrim encoder) (binding optflag) setting)
  pure $ if succeeded status then Right () else Left status

export
encode : Encoder n -> (filename : String) -> IO (Either Status ())
encode encoder filename = do
  status <- MkStatus <$> fromPrim (sixel_encoder_encode (toPrim encoder) filename)
  pure $ if succeeded status then Right () else Left status

export
encodeBytes :
  Encoder n -> (bytes : Buffer) -> (w : Int) -> (h : Int) ->
    (pixelformat : PixelFormat) -> (palette : Buffer) -> (ncolors : Int) ->
    IO (Either Status ())
encodeBytes encoder bytes w h pixelformat palette ncolors = do
  status <- MkStatus <$> fromPrim (sixel_encoder_encode_bytes
    (toPrim encoder) bytes w h (binding pixelformat) palette ncolors)
  pure $ if succeeded status then Right () else Left status

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text: module Dailyprover

max_stars_repo_name: farrellm/dailyprover

max_issues_repo_name: farrellm/dailyprover

max_forks_repo_name: farrellm/dailyprover


text:
module Text.WebIDL.Types.Member

import Generics.Derive
import Text.WebIDL.Types.Argument
import Text.WebIDL.Types.Attribute
import Text.WebIDL.Types.Identifier
import Text.WebIDL.Types.StringLit
import Text.WebIDL.Types.Type

%language ElabReflection

||| Const ::
|||     const ConstType identifier = ConstValue ;
|||
||| ConstValue ::
|||     BooleanLiteral
|||     FloatLiteral
|||     integer
public export
record Const where
  constructor MkConst
  type  : ConstType
  name  : Identifier
  value : ConstValue

%runElab derive "Const" [Generic,Meta,Eq,Show,HasAttributes]

--------------------------------------------------------------------------------
--          Operation
--------------------------------------------------------------------------------

||| OperationName ::
|||     OperationNameKeyword
|||     identifier
|||
||| OperationNameKeyword ::
|||     includes
public export
record OperationName where
  constructor MkOpName
  value : String

%runElab derive "OperationName" [Generic,Meta,Eq,Show,HasAttributes]

||| Special ::
|||     getter
|||     setter
|||     deleter
public export
data Special = Getter | Setter | Deleter

%runElab derive "Special" [Generic,Meta,Eq,Show,HasAttributes]

||| RegularOperation ::
|||     Type OperationRest
|||
||| OperationRest ::
|||     OptionalOperationName ( ArgumentList ) ;
|||
||| OptionalOperationName ::
|||     OperationName
|||     ε
|||
||| SpecialOperation ::
|||     Special RegularOperation
|||
||| Operation ::
|||     RegularOperation
|||     SpecialOperation
public export
record Op a where
  constructor MkOp
  special : a
  type    : IdlType
  name    : Maybe OperationName
  args    : ArgumentList

%runElab derive "Op" [Generic,Meta,Eq,Show,HasAttributes]

public export
0 RegularOperation : Type
RegularOperation = Op ()

public export
0 SpecialOperation : Type
SpecialOperation = Op Special

public export
0 Operation : Type
Operation = Op (Maybe Special)

public export
regToOp : RegularOperation -> Operation
regToOp = record { special = Nothing }

public export
specToOp : SpecialOperation -> Operation
specToOp = record { special $= Just }

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

||| CallbackInterfaceMember ::
|||     Const
|||     RegularOperation
public export
0 CallbackInterfaceMember : Type
CallbackInterfaceMember = NS I [Const,RegularOperation]

||| CallbackInterfaceMembers ::
|||     ExtendedAttributeList CallbackInterfaceMember CallbackInterfaceMembers
|||     ε
public export
0 CallbackInterfaceMembers : Type
CallbackInterfaceMembers = List (Attributed CallbackInterfaceMember)

--------------------------------------------------------------------------------
--          Dictionary
--------------------------------------------------------------------------------

||| Inheritance ::
|||     : identifier
|||     ε
public export
0 Inheritance : Type
Inheritance = Maybe Identifier

||| DictionaryMemberRest ::
|||     required TypeWithExtendedAttributes identifier ;
|||     Type identifier Default ;
public export
data DictionaryMemberRest : Type where
  Required :  (attrs : ExtAttributeList)
           -> (type : IdlType)
           -> (name : Identifier)
           -> DictionaryMemberRest

  Optional :  (type  : IdlType)
           -> (name  : Identifier)
           -> (deflt : Default)
           -> DictionaryMemberRest

%runElab derive "DictionaryMemberRest" [Generic,Meta,Eq,Show,HasAttributes]

||| DictionaryMember ::
|||     ExtendedAttributeList DictionaryMemberRest
public export
0 DictionaryMember : Type
DictionaryMember = Attributed DictionaryMemberRest

||| DictionaryMembers ::
|||     DictionaryMember DictionaryMembers
|||     ε
public export
0 DictionaryMembers : Type
DictionaryMembers = List DictionaryMember

--------------------------------------------------------------------------------
--          Attributes
--------------------------------------------------------------------------------

public export
record Readonly a where
  constructor MkRO
  value : a

%runElab derive "Readonly" [Generic,Meta,Eq,Show,HasAttributes]

public export
record Inherit a where
  constructor MkI
  value : a

%runElab derive "Inherit" [Generic,Meta,Eq,Show,HasAttributes]

||| AttributeName ::
|||     AttributeNameKeyword
|||     identifier
|||
||| AttributeNameKeyword ::
|||     async
|||     required
public export
record AttributeName where
  constructor MkAttributeName
  value : String

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

||| AttributeRest ::
|||     attribute TypeWithExtendedAttributes AttributeName ;
public export
record Attribute where
  constructor MkAttribute
  attrs : ExtAttributeList
  type  : IdlType
  name  : AttributeName

%runElab derive "Attribute" [Generic,Meta,Eq,Show,HasAttributes]

||| ReadWriteMaplike ::
|||     MaplikeRest
|||
||| MaplikeRest ::
|||     maplike < TypeWithExtendedAttributes , TypeWithExtendedAttributes > ;
public export
record Maplike where
  constructor MkMaplike
  fstTpe : Attributed IdlType
  sndTpe : Attributed IdlType

%runElab derive "Maplike" [Generic,Meta,Eq,Show,HasAttributes]

export
HasAttributes Maplike where
  attributes v = fst (v.fstTpe) ++ fst (v.sndTpe)

||| ReadWriteSetlike ::
|||     SetlikeRest
|||
||| SetlikeRest ::
|||     setlike < TypeWithExtendedAttributes > ;
public export
record Setlike where
  constructor MkSetlike
  type : Attributed IdlType

%runElab derive "Setlike" [Generic,Meta,Eq,Show,HasAttributes]

||| StringifierRest ::
|||     OptionalReadOnly AttributeRest
|||     RegularOperation
|||     ;
|||
||| Stringifier ::
|||     stringifier StringifierRest
public export
0 Stringifier : Type
Stringifier = NS I [Attribute, Readonly Attribute, RegularOperation,()]

||| StaticMember ::
|||     static StaticMemberRest
|||
||| StaticMemberRest ::
|||     OptionalReadOnly AttributeRest
|||     RegularOperation
public export
0 StaticMember : Type
StaticMember = NS I [Attribute, Readonly Attribute, RegularOperation]

--------------------------------------------------------------------------------
--          Namespace
--------------------------------------------------------------------------------

||| NamespaceMember ::
|||     RegularOperation
|||     readonly AttributeRest
public export
0 NamespaceMember : Type
NamespaceMember = NS I [RegularOperation, Readonly Attribute]

||| NamespaceMembers ::
|||     ExtendedAttributeList NamespaceMember NamespaceMembers
|||     ε
public export
0 NamespaceMembers : Type
NamespaceMembers = List (Attributed NamespaceMember)

--------------------------------------------------------------------------------
--          Interface
--------------------------------------------------------------------------------

||| Constructor ::
|||     constructor ( ArgumentList ) ;
public export
record Constructor where
  constructor MkConstructor
  args : ArgumentList

%runElab derive "Constructor" [Generic,Meta,Eq,Show,HasAttributes]

||| PartialInterfaceMember ::
|||     Const
|||     Operation
|||     Stringifier
|||     StaticMember
|||     Iterable
|||     AsyncIterable
|||     ReadOnlyMember
|||     ReadWriteAttribute
|||     ReadWriteMaplike
|||     ReadWriteSetlike
|||     InheritAttribute
|||
||| Iterable ::
|||     iterable < TypeWithExtendedAttributes OptionalType > ;
public export
data PartialInterfaceMember =
    IConst   Const
  | IOp      Operation
  | IStr     Stringifier
  | IStatic  StaticMember
  | IAttr    Attribute
  | IMap     Maplike
  | ISet     Setlike
  | IAttrRO  (Readonly Attribute)
  | IMapRO   (Readonly Maplike)
  | ISetRO   (Readonly Setlike)
  | IAttrInh (Inherit Attribute)
  | IIterable (Attributed IdlType) OptionalType
  | IAsync   (Attributed IdlType) OptionalType ArgumentList

%runElab derive "PartialInterfaceMember" [Generic,Meta,Eq,Show,HasAttributes]

||| MixinMember ::
|||     Const
|||     RegularOperation
|||     Stringifier
|||     OptionalReadOnly AttributeRest
public export
data MixinMember =
    MConst   Const
  | MOp      RegularOperation
  | MStr     Stringifier
  | MAttr    Attribute
  | MAttrRO  (Readonly Attribute)

%runElab derive "MixinMember" [Generic,Meta,Eq,Show,HasAttributes]

||| PartialInterfaceMembers ::
|||     ExtendedAttributeList PartialInterfaceMember PartialInterfaceMembers
|||     ε
public export
0 PartialInterfaceMembers : Type
PartialInterfaceMembers = List (Attributed PartialInterfaceMember)

||| InterfaceMember ::
|||     PartialInterfaceMember
|||     Constructor
public export
0 InterfaceMember : Type
InterfaceMember = NS I [Constructor,PartialInterfaceMember]

||| InterfaceMembers ::
|||     ExtendedAttributeList InterfaceMember InterfaceMembers
|||     ε
public export
0 InterfaceMembers : Type
InterfaceMembers = List (Attributed InterfaceMember)

||| MixinMembers ::
|||     ExtendedAttributeList MixinMember MixinMembers
|||     ε
public export
0 MixinMembers : Type
MixinMembers = List (Attributed MixinMember)

--------------------------------------------------------------------------------
--          Extractors
--------------------------------------------------------------------------------

namespace CallbackInterfaceMember
  export
  const : Attributed CallbackInterfaceMember -> Maybe Const
  const (_,Z x) = Just x
  const _       = Nothing

namespace Dictionary
  export
  optional : DictionaryMember -> Maybe Attribute
  optional (_, Required _ _ _) = Nothing
  optional (_, Optional t n _) =
    Just $ MkAttribute Nil t (MkAttributeName n.value)

  export
  required : DictionaryMember -> Maybe Attribute
  required (_, Required _ t n) =
    Just $ MkAttribute Nil t (MkAttributeName n.value)
  required (_, Optional _ _ _) = Nothing

namespace InterfaceMember
  export
  part :  (PartialInterfaceMember -> Maybe a)
       -> Attributed InterfaceMember
       -> Maybe a
  part f (_,(S $ Z $ p)) = f p
  part _ _               = Nothing

namespace MixinMember
  export
  const : Attributed MixinMember -> Maybe Const
  const (_,MConst x) = Just x
  const _            = Nothing

  export
  attrRO : Attributed MixinMember -> Maybe (Readonly Attribute)
  attrRO (_, (MAttrRO x)) = Just x
  attrRO _                = Nothing

  export
  attr : Attributed MixinMember -> Maybe Attribute
  attr (_, (MAttr x)) = Just x
  attr _              = Nothing

namespace NamespaceMember

  export
  attrRO : NamespaceMember -> Maybe (Readonly Attribute)
  attrRO (S $ Z x) = Just x
  attrRO (Z _)     = Nothing

namespace PartialInterfaceMember
  export
  const : PartialInterfaceMember -> Maybe Const
  const (IConst x) = Just x
  const _          = Nothing

  export
  attrRO : PartialInterfaceMember -> Maybe (Readonly Attribute)
  attrRO (IAttrRO x) = Just x
  attrRO _           = Nothing

  export
  attr : PartialInterfaceMember -> Maybe Attribute
  attr (IAttr x) = Just x
  attr _         = Nothing


text:
-- --------------------------------------------------------------- [ Day04.idr ]
-- Module      : Data.Advent.Day04
-- Description : My solution to the Day 4 puzzle of the 2016 Advent of Code.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : http://adventofcode.com/2016/day/4
-- --------------------------------------------------------------------- [ EOH ]
||| Day 4: Security Through Obscurity
module Data.Advent.Day04

import public Data.SortedMap

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings
import public Lightyear.StringFile

%access export

-- NOTE: This is not awesome, but the maps here will be small...
private
inc : k -> SortedMap k Nat -> SortedMap k Nat
inc k m =
    case lookup k m of
         Nothing => insert k 1 m
         Just v  => insert k (S v) $ delete k m

-- ----------------------------------------------------------------- [ Parsers ]

encryptedName : Parser (List Char)
encryptedName = concat <$> some (some letter <* token "-")

sectorId : Parser Integer
sectorId = integer

checksum : Parser String
checksum = quoted' '[' ']'

room : Parser (List Char, Integer, String)
room = liftA2 MkPair encryptedName $ liftA2 MkPair sectorId checksum

-- ------------------------------------------------------------------- [ Logic ]

implementation [day04] Ord (Char, Nat) where
    compare (a,x) (b,y) = let o = compare y x in
                              if EQ /= o
                                 then o
                                 else compare a b

computeChecksum : List Char -> String
computeChecksum = pack . map Basics.fst .
                  take 5 . sort @{day04} . toList .
                  foldr inc empty

isReal : (List Char, Integer, String) -> Bool
isReal (cs, _, cksum) = cksum == computeChecksum cs

main' : Show a => Parser (List (List Char, Integer, String)) ->
        (List (List Char, Integer, String) -> a) -> IO ()
main' p f =
    either putStrLn (printLn . f)
           !(run $ parseFile (const show) (const id) p "input/day04.txt")

-- ---------------------------------------------------------------- [ Part One ]

namespace PartOne

    main : IO ()
    main = main' (some room) $ foldr go 0
      where
        go r@(_,sid,_) sum = if isReal r then sum + sid else sum

-- ---------------------------------------------------------------- [ Part Two ]

namespace PartTwo

    roomToMessage : (List Char, Integer, String) -> String
    roomToMessage (cs, sid, _) =
        let az = cycle ['a' .. 'z']
            n = toNat sid `mod` 26 in
            pack $ map (\c => index n (drop (toNat c `minus` 97) az)) cs

    main : IO ()
    main = main' (filter isReal <$> some room) $ \rs =>
           fromMaybe (-404) $ (\(_,sid,_) => sid) <$>
           find (("northpoleobjectstorage" ==) . roomToMessage) rs

-- -------------------------------------------------------------------- [ Main ]

namespace Main

    main : IO ()
    main = putStr "Part One: " *> PartOne.main *>
           putStr "Part Two: " *> PartTwo.main

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

max_stars_repo_name: yurrriq/advent-of-code


text:
module Flexidisc.TaggedValue

%default total

infixl 8 :=

public export
data TaggedValue : (key : k) -> (v : Type) -> Type where
  (:=) : (key : k) -> v -> TaggedValue key v

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Examples

import Data.Vect
import ProcessLib
import Proto
import HoriComp
import VertComp
import Primitives
import SumWire
import Dualise
import SumWire
import CupCap
import Util

%flag C "-O3"

gt5: Hom [Down Int] [Down Int, Down Int]
gt5 = mkPure "gt5: " (\n => if n > 5 then Left n else Right n) -*- splitEither

inc: Hom [Down Int] [Down Int]
inc = mkPure "inc: " (\i => i + 1)

downIntWire: Hom [Down Int] [Down Int]
downIntWire = mkPure "down int: " id

upIntWire: Hom [Up Int] [Up Int]
upIntWire = dualise downIntWire

myProc: Hom [Down Int] []
myProc =     downIntWire + cap
         -*- (splice -*- inc -*- gt5) + upIntWire
         -*- downPrinter + cup

test: Client ()
test = do Just proc <- Spawn myProc | _ => Action (putStrLn "failed to spawn the process")
          val_resp <- Request proc (Val (TopInWire Here) 1)
          Action $ putStrLn $ "result: " ++ show val_resp
          Util.dot_sleeper 20

namespace Main
  main: IO ()
  main = runProc test

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Main

import Data.Time.Calendar
import Data.Time.Clock
import Data.Time.Clock.System

%default total

partial main : IO ()
main = do
  do
    t <- getSystemLocalTime
    putStrLn $ "getSystemLocalTime : " ++ show t

  do
    t <- getSystemTime
    putStrLn $ "systemEpochDay : " ++ show systemEpochDay
    putStrLn $ "getSystemTIme : " ++ show t
    putStrLn $ "  systemToUTCTime : " ++ show (systemToUTCTime t)
    putStrLn $ "    <-> utcToSystemTime : " ++ show (utcToSystemTime (systemToUTCTime t))
    putStrLn $ "  truncateSystemTimeLeapSecond : " ++ show (truncateSystemTimeLeapSecond t)
    putStrLn $ show $ dayOfWeek $ fromGregorian 2021 8 21
    putStrLn $ show $ (modifiedJulianDay $ fromGregorian 2021 8 21) `mod` 7


text:
module Cycle2

import Cycle1


text:
-- https://stackoverflow.com/questions/28257620/choosing-a-typeclass-on-construction-of-a-data-type
-- Using Idris 0.9.18.1

module ClassDataSE

----- Common definitions

class Foo a where
	fooval : a

class Bar a where
	barval : a

%case data Operator = Up | Down

total
classChoice : (x : Operator) -> (Type -> Type)
classChoice Up = Foo
classChoice Down = Bar

data Doo : Type where
	Da : Doo

instance [foodoo] Foo Doo where
	fooval = Da

instance Bar Doo where
	barval = Da

----- Solution by wrapping function of class's datatype in constrained function
-- Commenting out the definition of mkChoosy and reproving, there's clearly a problem.
-- I imagine this could hinder arguments about the value of choosier, which doesn't depend on its arguments in as much as each argument is considered two different things.

data Choosy : (op : Operator) -> (a : Type) -> { P : classChoice op a } -> Type where
	Chosen : Choosy op a

choosier : classChoice op a => (op : Operator) -> (a : Type) -> Type
-- For some reason ?instanceChoice doesn't think the argument `op` and `a` are the signature `op` and `a`, so the constraint argument `classChoice op a` is not assumed.
-- choosier op a = Choosy op a {P=?instanceChoice}
choosier = ?mkChoosy

mkChoosy = proof
	intros
	exact (Choosy op a {P=constrarg})

{-
Can't resolve type class classChoice op a

> guess = choosier Up Doo
-}

guess : Type
guess = ?guess'

-- With direct interface
guess' = proof
  exact (Choosy Up Doo {P=foodoo})

{-
-- With wrapper function instead

guess' = proof
  exact (choosier Up Doo)
  exact Up
  exact Doo
  compute
  exact foodoo
-}

guessanon : Type
guessanon = ?guessanon'

{-
(exact a) not needed after compute when (a) is an anonymous instance:

"When checking right hand side of ClassDataSE.guessanon':
INTERNAL ERROR: Nothing to fill in.
This is probably a bug, or a missing error message.
Please consider reporting at https://github.com/idris-lang/Idris-dev/issues"

> guessanon' = proof
> 	exact (choosier Down Doo)
> 	exact Down
> 	exact Doo
> 	compute
> 	exact %instance
-}

guessanon' = proof
	exact (choosier Down Doo)
	exact Down
	exact Doo
	compute

----- Usage of class's datatype as-is

data Choosy2 : (op : Operator) -> (a : Type) -> {inst : classChoice op a} -> Type where
	Chosen2 : Choosy2 op a

knownTypeBar : Type
knownTypeBar = Choosy2 Down Doo {inst=?knownInstBar_pr}

{-
Alternative - (exact %instance) doesn't work in the REPL, only instance with a name declared.

> knownInstBar : Bar Doo
> knownInstBar = %instance

> knownInstBar_pr = proof
> 	compute
> 	exact knownInstBar
-}

knownInstBar_pr = proof
	compute
	exact %instance

knownTypeFoo : Type
knownTypeFoo = Choosy2 Up Doo {inst=?knownInstFoo_pr}

knownInstFoo_pr = proof
	compute
	exact foodoo

----- Simplify circumstances of not being able to resolve the typeclass

foosyn : Type -> Type
foosyn = Foo

-- if seewhatsinside has two arguments of type `a`, there's the issue.
-- It doesn't, the goal is (Foo a -> a -> b)
checkmeforclues : foosyn a => a -> b
checkmeforclues = ?seewhatsinside

-- No problem, the goal is (Foo a -> a -> Foo a)
checkmeforclues2 : foosyn a => a -> foosyn a
checkmeforclues2 = ?seewhatsinside2

{-
> foosyn2 : Type -> Type
> foosyn2 t = case t of
> 		Nat => Foo t
> 		_ => Bar t

You try and prove lookwhatsinside

> checkmeforcluestoo : foosyn2 a => a -> b
> checkmeforcluestoo = ?lookwhatsinside

and if you apply (compute) you get (case block in foosyn2 a a = Foo a), which looks like a bug.

This won't do the same, for instance:

> bake : Bool -> Bool
> bake t = case t of
> 		False => t
> 		_ => t

> bakeisid : bake t = t
> bakeisid = ?bake_lem
-}

----- More options explored

{-
Successful isolation step in contrast of Choosy3 w/ checkmeforclues:

When checking type of ClassDataSE.Chosen3:
Can't resolve type class foosyn a

> data Choosy3 : foosyn a => (a : Type) -> Type where
> 	Chosen3 : Choosy3 a
-}

{-
-- This doesn't help
> data Choosy4 : (p : foosyn a) => (a : Type) -> Type where
> 	Chosen4 : {a : Type} -> { p' : foosyn a } -> Choosy4 a
-}

-- This also works.
data Choosy5 : (a : Type) -> (p : foosyn a) -> Type where
	Chosen5 : (p' : foosyn a) -> Choosy5 a p'

{-
When checking type of ClassDataSE.Special6:
Choosy6 a constrarg Doo does not have a function type (Type)

data Choosy6 : foosyn a => (a : Type) -> Type where
	Special6 : Choosy6 Doo @{foodoo}
-}

----- A functioning option where a constraint argument appears in the type of (Choosy7).

{-
This works, but passes the same errors from before down the line to declaring the values.

The (<==) is 'match' application, documented in part here:
http://docs.idris-lang.org/en/latest/reference/misc.html
-}
data Choosy7 : (p : foosyn a) => (a : Type) -> Type where
	Chosen7 : Type <== Choosy7

{-
I suspect this is at the heart of the problem.

> Chosen7

(input):Can't infer argument a to Chosen7,
        Can't infer argument p to Chosen7,
        Can't infer argument a2 to Chosen7

> Chosen7 {a=Doo}

(input):1:9:a is not an implicit argument of ClassDataSE.Chosen7

> Choosy7 Doo

Can't resolve type class foosyn a

> inspector: Choosy7 Doo

When checking type of ClassDataSE.inspector:
Can't resolve type class foosyn a

That is to say, there is a hole of type (foosyn a) arising from a declaration, rather than a definition, and that hole must be filled for the type to check.

I count the following as a successful proof of (Choosy7 Doo).
Though reported as type (chews), running printdef on (chews) will show (Choosy7 Doo), so it should be recognized as a (Choosy7 Doo) when its type is computed.
-}

inspector: ?chews
inspector = Chosen7

chews = proof
  exact (Choosy7 Doo)
  exact Doo
  compute
  exact foodoo

-- For good measure, an anonymous instance version of a (Choosy7 a) proof
data Dar = Dei

instance Foo Dar where fooval = Dei

inspectorAnon : ?chomps
inspectorAnon = Chosen7

chomps = proof
  exact (Choosy7 Dar)
  exact Dar
  compute
-- Only in REPL, where anonymous instance isn't acknowledged: exact %instance

{-
An alternative proof to chomps:

> chomps = proof
>   exact (Choosy7 Dar)
>   exact Doo
>   compute
>   exact foodoo

It's kind of hard to see whether it makes a difference whether you perform the proof correctly or as just shown.
-}

{-
This (seeker) declared below has a bad value, since the parameters to (Choosy7) are undetermined.

In the alternative proof to (chomps), the goal satisfied by (exact (Choosy7 Dar)) and the mismatching goals that emerge after satisfying it are the same as the assumptions available when defining (seeker) in the REPL, which in turn show the same splitting of one argument into two - the (a : Type) that (seeker) depends on and the (a2 : Type) that (Choosy7 a2) depends on - seen in (mkChoice).

We do not need to make such a proof, and have defined it by the exact constructor. However, the behavior of the proof engine here is very interesting, because it appears an instance of (foosyn a) is accepted as an instance of (foosyn a2).
-}

seeker : Type <== Choosy7
seeker = Chosen7

{-
-- Try defining interactively as if by below to see the assumptions or behavior of the proof engine.

seeker = ?seeker_sat
seeker_sat = proof
  intros
  exact Chosen7
-}

----- One last option

{-
When checking type of ClassDataSE.Chosen8:
Can't resolve type class foosyn a

> data Choosy8 : foosyn a => (a : Type) -> Type where
> 	Chosen8 : foosyn a => Choosy8 a

Still allows bad value by method of (seeker) for Choosy7, but does constrain the circumstances for it.

> data Choosy8 : foosyn a => (a : Type) -> Type where
> 	Chosen8 : foosyn a => Type <== Choosy8
-}

max_stars_repo_name: runKleisli/idris-classdata

max_issues_repo_name: runKleisli/idris-classdata

max_forks_repo_name: runKleisli/idris-classdata


text:
module Test.Accumulate

import Accumulate

%access export

assertEq : Eq a => String -> (given : a) -> (expected : a) -> IO ()
assertEq label g e = putStrLn $ if g == e then label ++ ": Test Passed" else label ++ ": Test Failed"

testEmptyListDoesNothing : IO ()
testEmptyListDoesNothing = assertEq "empty list does nothing" (accumulate (\x => x) []) (the (List Int) [])

testIdentityFunctionDoesNothing : IO ()
testIdentityFunctionDoesNothing = assertEq "identity function does nothing" (accumulate (\x => x) [1,2,3]) [1,2,3]

testSquareFunctionDoublesInput : IO ()
testSquareFunctionDoublesInput = assertEq "square function doubles input" (accumulate (\x => x * x) [1,2,3]) [1,4,9]

testCubeFunctionTriplesInput : IO ()
testCubeFunctionTriplesInput = assertEq "cube function triples input" (accumulate (\x => x * x * x) [1,2,3]) [1,8,27]

testIncrementFunctionAddsOneToAllInput : IO ()
testIncrementFunctionAddsOneToAllInput = assertEq "increment function adds 1 to input" (accumulate (\x => x + 1) [1,2,3]) [2,3,4]

testDecrementFunctionAddsOneToAllInput : IO ()
testDecrementFunctionAddsOneToAllInput = assertEq "decrement function subtracts 1 from input" (accumulate (\x => x - 1) [1,2,3]) (the (List Int) [0,1,2])

runTests : IO ()
runTests = do
  testEmptyListDoesNothing
  testIdentityFunctionDoesNothing
  testSquareFunctionDoublesInput
  testCubeFunctionTriplesInput
  testIncrementFunctionAddsOneToAllInput
  testDecrementFunctionAddsOneToAllInput


text:
import Data.Fin
import Data.Maybe

data NNat = NZ | NS NNat

zsym : (x : NNat) -> x = NZ -> NZ = x
zsym NZ Refl = Refl
zsym (NS _) Refl impossible

zsym' : (x : NNat) -> x = NZ -> NZ = x
zsym' NZ Refl = Refl

foo : Nat -> String
foo 0 = "zero"
foo 1 = "one"
foo x = "something else"

bar : Fin (S (S (S Z))) -> String
bar 0 = "a"
bar 1 = "b"
bar 2 = "c"


text:
module Data.Universe

%default total

public export
record Universe where
  constructor BigBang
  Ty        : Type
  typeOf    : Ty -> Type
  defaultOf : (t : Ty) -> typeOf t
  decEq     : (t : Ty) -> (s : Ty) -> Dec (t = s)

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Main

import Data.Fixed
import Data.Integral.Gcd
import Data.Complex
import Text.Format.Decimal

chk : (Show a, Show b) => String -> List (a, b) -> (b -> a) -> (b -> a -> a -> Bool) -> IO ()
chk dsc xs f g = do
  putStr (dsc ++ ": ")
  for_ xs $
    \xs@(e, x) => do
      let ans = f x
      if g x e ans
         then putStr "✓"
         else putStrLn ("\n  ✗ test=" ++ show xs ++ " ans=" ++ show ans)
  putStrLn ""

partial main : IO ()
main = testGcd >> testLcm >> testTextFormat >> testComplex
  where
    testGcd : IO ()
    testGcd = chk "Gcd golden"
          [ (13, (0, 13)), (523, (523, 0)), (13, (13, 13)), (1, (37, 600))
          , (20, (20, 100)), (18913, (624129, 2061517)) ]
          (uncurry gcd) (const (==))

    testLcm : IO ()
    testLcm = chk "Lcm golden"
          [ (0, 0, 22), (0, 42, 0), (60, 12, 20) ]
          (uncurry lcm) (const (==))

    testTextFormat : IO ()
    testTextFormat = do
      do
        let fmt00 = record { width = Just 4, prec = Just 0, pad = Nothing,
                           spc = ' ', point = '.',
                           minus = Just (Left "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Int + Width)"
            [ ("   0", 0), ("   1", 1), ("  10", 10), (" -10", -10)
            , ("-999", -999), (" 999", 999), ("1234", 1234), ("-1234", -1234)
            , ("99999", 99999) ]
            (format fmt00) (const (==))
      do
        let fmt00 = record { width = Nothing, prec = Just 0, pad = Nothing,
                      spc = ' ', point = '.',
                      minus = Just (Left "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Int + no width)"
            [ ("0", 0), ("1", 1), ("10", 10), ("-10", -10), ("-999", -999)
            , ("999", 999), ("1234", 1234), ("-1234", -1234), ("99999", 99999) ]
            (format fmt00) (const (==))
      do
        let fmt00 = record { width = Just 4, prec = Just 0, pad = Nothing,
                      spc = ' ', point = '.',
                      minus = Just (Left "-"), plus = Just (Left "+") } defaultDecimalFormat
        chk "Text format (Int + Width and PlusSign"
            [ ("  +0", 0), ("  +1", 1), ("+123", 123), ("+1234", 1234) ]
            (format fmt00) (const (==))

      do
        let fmt00 = record { width = Just 4, prec = Just 0, pad = Nothing,
                      spc = ' ', point = '.',
                      minus = Just (Right "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Int + TailingSign)"
            [ ("   0", 0), ("   1-", -1), (" 123-", -123), ("1234-", -1234) ]
            (format fmt00) (const (==))

      do
        let fmt00 = record { width = Just 4, prec = Just 0, pad = Just '0',
                      spc = ' ', point = '.',
                      minus = Just (Left "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Int + Padding)"
            [ ("0000", 0), ("-0001", -1), ("-0123", -123), ("-1234", -1234) ]
            (format fmt00) (const (==))

      do
        let fmt00 = record { width = Nothing, prec = Just 0, pad = Just '0',
                      spc = ' ', point = '.',
                      minus = Just (Left "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Int + no width + padding)"
            [ ("0", 0), ("-1", -1), ("-123", -123), ("-1234", -1234) ]
            (format fmt00) (const (==))

      do
        let fmt00 = record { width = Just 4, prec = Nothing, pad = Nothing,
                      spc = ' ', point = '.',
                      minus = Just (Left "-"), plus = Nothing } defaultDecimalFormat
        chk "Text format (Fixed + Width)"
            [("   0.000000000000", the (Fixed 12) 0),
             ("   1.000000000000", 1), (" -10.000000000000", -10) ]
            (format fmt00) (const (==))

    testComplex : IO ()
    testComplex = do
      chk "Complex Eq"
          [ (True, (MkComplex 0 1, MkComplex 0 1))
          , (False, (MkComplex 1 1, MkComplex 0 1)) ]
        (uncurry (==)) (const (==))


text:
import Data.Vect

allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

insert : Ord elem =>
  (x : elem) -> (xsSorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = if x < y
  then x :: y :: xs
  else y :: insert x xs

insSort : Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                        insert x xsSorted


text:
module FreerCont

-- Based on https://github.com/lambdageek/freer-church

data FreerCont : (f : Type -> Type) -> Type -> Type where
  Cont : ({r : Type} -> (a -> r) -> ({x : Type} -> f x -> (x -> r) -> r) -> r) -> FreerCont f a

pure : a -> FreerCont f a
pure x = Cont (\k, _ => k x)

(>>=) : FreerCont f a -> (a -> FreerCont f b) -> FreerCont f b
(>>=) (Cont g) f = Cont (\k, imp => g (\x => let (Cont g') = f x in g' k imp) imp)

-- State effect
data State : (s : Type) -> Type -> Type where
  Get : State s s
  Put : s -> State s ()

get : FreerCont (State s) s
get = Cont (\k, imp => imp Get k)

put : s -> FreerCont (State s) ()
put s = Cont (\k, imp => imp (Put s) k)

imp : State s x -> (x -> s -> (s, a)) -> s -> (s, a)
imp Get k st = k st st
imp (Put x) k st = k () x

runState : FreerCont (State s) a -> s -> (s, a)
runState (Cont f) = f k imp
  where
    k : a -> s -> (s, a)
    k x st = (st, x)

example : FreerCont (State Int) Int
example = do s <- get
             put (s + 1)
             s <- get
             pure (s + 1)

test : (Int, Int)
test = runState example 0

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Libraries.Data.List.Quantifiers.Extra

import Data.List
import Data.List.Quantifiers
import Decidable.Equality

%default total

export
lookup : {xs : List a} -> DecEq a => (v : a) -> All p xs -> Maybe (p v)
lookup v [] = Nothing
lookup v (px :: pxs)
  = case decEq (head xs) v of
      No _ => lookup v pxs
      Yes Refl => Just px

export
(++) : All p xs -> All p ys -> All p (xs ++ ys)
[] ++ pys = pys
(px :: pxs) ++ pys = px :: (pxs ++ pys)

export
tabulate : ((x : a) -> p x) -> (xs : List a) -> All p xs
tabulate f [] = []
tabulate f (x :: xs) = f x :: tabulate f xs


text:
module Data.IxRel

%access public export
%default total

||| Indexed binary relations
data IxRel : (a -> b -> c) -> c -> a -> b -> Type where
  MkIxRel : IxRel p (p a b) a b

||| A binary boolean predicate
Predicate : (a -> b -> Bool) -> a -> b -> Type
Predicate p x y = IxRel p True x y

||| Given parameters, constructs the index and relation
relate : (p : a -> b -> c) -> (x : a) -> (y : b) -> (q ** IxRel p q x y)
relate p x y = (p x y ** MkIxRel)

||| Helper for decide
private
unique : IxRel p w x y -> IxRel p q x y -> w = q
unique MkIxRel MkIxRel = Refl

||| Given parameters and an index, decides if a relation exists for that index
decide : DecEq c => (p : a -> b -> c) -> (w : c) -> (x : a) -> (y : b) -> Dec (IxRel p w x y)
decide p w x y with (relate p x y)
  | (q ** pf) =
    case decEq w q of
      Yes pfe => Yes (rewrite pfe in pf)
      No contra => No (\r => contra (unique r pf))

||| Decide specialized to predicates
decidePredicate : (p : a -> b -> Bool) -> (x : a) -> (y : b) -> Dec (Predicate p x y)
decidePredicate p x y = decide p True x y

max_stars_repo_name: ejconlon/idris-array

max_issues_repo_name: ejconlon/ixarray

max_forks_repo_name: ejconlon/ixarray


text:
module Simple

%default total

public export
data LSys : a -> Type where
  MkLSys : List a -> (a -> List a) -> LSys a

iterate : Nat -> LSys a -> List a
iterate Z (MkLSys axiom _) = axiom
iterate n (MkLSys axiom rules) = go n axiom
  where
    go : Nat -> List a -> List a
    go Z word = word
    go (S n) word = let nextWord = word >>= rules
                     in go n nextWord

----------------
-- An example --
----------------

data Algae = A | B

Show Algae where
  show A = "A"
  show B = "B"

algaeRules : Algae -> List Algae
algaeRules A = [A, B]
algaeRules B = pure A

algaeExample : LSys Algae
algaeExample = MkLSys [A] algaeRules

main : IO ()
main = print $ Simple.iterate 10 algaeExample

max_stars_repo_name: PeterHajdu/ilsys

max_issues_repo_name: PeterHajdu/ilsys

max_forks_repo_name: PeterHajdu/ilsys


text:
module ZZUtils
import ZZ
import NatUtils
%access public export
%default total

data IsNonNegative : ZZ->Type where
 NonNegative :(IsNonNegative (Pos k))

|||Proof that negative integers are not non negative
negsAreNotNonNegs:(IsNonNegative (NegS k))->Void
negsAreNotNonNegs NonNegative impossible
|||A function that checks whether an integer is non negative and returns a
|||proof or a contradiction
decideIsNonNeg:(a: ZZ) -> Dec (IsNonNegative   a)
decideIsNonNeg (Pos k) = Yes NonNegative
decideIsNonNeg (NegS k) = No (negsAreNotNonNegs)
|||Proof that natural numbers are non negative
naturalsNonNegative: (x:Nat)->IsNonNegative (Pos x)
naturalsNonNegative x = NonNegative

|||The less than type for ZZ
LTZ :ZZ->ZZ->Type
LTZ a b = LTEZ (1+a) b

|||Theorem that if a and b are natural numbers and a<b
|||then, (Pos a) <(Pos b)
ltNatToZZ:{a:Nat}->{b:Nat}->(LT a b)->(LTZ (Pos a) (Pos b))
ltNatToZZ (LTESucc x) = PositiveLTE (LTESucc x)

data NotBothZeroZ :ZZ->ZZ->Type where
  LeftPositive :NotBothZeroZ (Pos (S k)) m
  LeftNegative :NotBothZeroZ (NegS k) m
  RightPositive :NotBothZeroZ m (Pos (S k))
  RightNegative :NotBothZeroZ m (NegS k)