text:
module Idris.Codegen.ExtSTG.String

import Core.Context
import Core.Core
import Core.TT
import Compiler.ANF
import Core.CompileExpr
import Data.HVect
import Data.Vect
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.ADTMap

{-
This module contains the ANF implementation of the String handling primitives.

The high level Haskell codes can be found in the IdristString.hs file.

STG Samples:
https://github.com/csabahruska/manual-stg-experiment/blob/master/StgSample.hs
-}

{-
[x] Str(..)
[x] strEq
[x] strCompare
[x] strLength
[ ] strHead
[ ] strTail
[ ] strIndex
[ ] strCons
[ ] strAppend
[ ] strReverse
[ ] strSubstr

[ ] Fix the Rep types in STG definitions
-}

{-
Values are primitive values and are represented as boxed STG values.
-}

e : FC
e = EmptyFC

STRING_TYPE_NAME : String
STRING_TYPE_NAME = "Idris.String"

STRING_TYPE_LIT_DATACON : String
STRING_TYPE_LIT_DATACON = "Idris.String.Lit"

STRING_TYPE_VAL_DATACON : String
STRING_TYPE_VAL_DATACON = "Idris.String.Val"

litDataConId :  DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core (DataConId (AlgDataCon [LiftedRep]))
litDataConId = do
  dataConId <- mkDataConIdStr STRING_TYPE_LIT_DATACON
  checkDataCon "litDataConId" (AlgDataCon [LiftedRep]) dataConId

valDataConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core DataConIdSg
valDataConId = mkDataConIdStr STRING_TYPE_VAL_DATACON

valDataConId2
  : DataTypeMapRef => UniqueMapRef => Ref Counter Int
  => Core (DataConId (AlgDataCon [LiftedRep]))
valDataConId2 = do
  dataConId <- mkDataConIdStr STRING_TYPE_VAL_DATACON
  checkDataCon "valDataConId2" (AlgDataCon [LiftedRep]) dataConId

export
idrisStringTyConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TyConId
idrisStringTyConId = mkTyConIdStr STRING_TYPE_NAME

ADDR_TYPE_NAME : String
ADDR_TYPE_NAME = "Idris.String.Addr"

ADDR_DATACON_NAME : String
ADDR_DATACON_NAME = "Idris.String.Addr"

addrTyConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TyConId
addrTyConId = mkTyConIdStr ADDR_TYPE_NAME

addrDataConId
  :  DataTypeMapRef
  => UniqueMapRef
  => Ref Counter Int
  => Core (DataConId (AlgDataCon [AddrRep]))
addrDataConId = do
  dataConId <- mkDataConIdStr ADDR_DATACON_NAME
  checkDataCon "addrDataConId" (AlgDataCon [AddrRep]) dataConId

BYTEARRAY_TYPE_NAME : String
BYTEARRAY_TYPE_NAME = "Idris.String.ByteArray"

BYTEARRAY_DATACON_NAME : String
BYTEARRAY_DATACON_NAME = "Idris.String.ByteArray"

byteArrayTyConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TyConId
byteArrayTyConId = mkTyConIdStr BYTEARRAY_TYPE_NAME

byteArrayDataConId
  :  DataTypeMapRef
  => UniqueMapRef
  => Ref Counter Int
  => Core (DataConId (AlgDataCon [UnliftedRep]))
byteArrayDataConId = do
  dataConId <- mkDataConIdStr BYTEARRAY_DATACON_NAME
  checkDataCon "byteArrayDataConId" (AlgDataCon [UnliftedRep]) dataConId

MBYTEARRAY_TYPE_NAME : String
MBYTEARRAY_TYPE_NAME = "Idris.String.MutableByteArray"

MBYTEARRAY_DATACON_NAME : String
MBYTEARRAY_DATACON_NAME = "Idris.String.MutableByteArray"

mutableByteArrayTyConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TyConId
mutableByteArrayTyConId = mkTyConIdStr MBYTEARRAY_TYPE_NAME

mutableByteArrayDataConId
  :  DataTypeMapRef
  => UniqueMapRef
  => Ref Counter Int
  => Core (DataConId (AlgDataCon [UnliftedRep]))
mutableByteArrayDataConId = do
  dataConId <- mkDataConIdStr MBYTEARRAY_DATACON_NAME
  checkDataCon "mutableByteArrayDataConId" (AlgDataCon [UnliftedRep]) dataConId

UNIT_TYPE_NAME : String
UNIT_TYPE_NAME = "Idris.String.Unit"

UNIT_DATACON_NAME : String
UNIT_DATACON_NAME = "Idris.String.Unit"

export
unitTyConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TyConId
unitTyConId = mkTyConIdStr UNIT_TYPE_NAME

export
unitDataConId : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core (DataConId (AlgDataCon []))
unitDataConId = do
  dataConId <- mkDataConIdStr UNIT_DATACON_NAME
  checkDataCon "unitDataConId" (AlgDataCon []) dataConId

export
defineStringTypes
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Ref ADTs ADTMap
  => Core ()
defineStringTypes = do
  let noSpan = SsUnhelpfulSpan
  define
    (STRING_TYPE_NAME, noSpan STRING_TYPE_NAME)
    [ (STRING_TYPE_LIT_DATACON, AlgDataCon [LiftedRep], noSpan STRING_TYPE_LIT_DATACON) -- Idris.String.Addr
    , (STRING_TYPE_VAL_DATACON, AlgDataCon [LiftedRep], noSpan STRING_TYPE_VAL_DATACON) -- Idris.String.ByteArray
    ]
  define
    (ADDR_TYPE_NAME, noSpan ADDR_TYPE_NAME)
    [ (ADDR_DATACON_NAME, AlgDataCon [AddrRep], noSpan ADDR_DATACON_NAME) ]
  define
    (BYTEARRAY_TYPE_NAME, noSpan BYTEARRAY_TYPE_NAME)
    [ (BYTEARRAY_DATACON_NAME, AlgDataCon [ByteArrayRep], noSpan BYTEARRAY_DATACON_NAME) ]
  define
    (MBYTEARRAY_TYPE_NAME, noSpan MBYTEARRAY_TYPE_NAME)
    [ (MBYTEARRAY_DATACON_NAME, AlgDataCon [ByteArrayRep], noSpan MBYTEARRAY_DATACON_NAME) ]
  define
    (UNIT_TYPE_NAME, noSpan UNIT_TYPE_NAME)
    [ (UNIT_DATACON_NAME, AlgDataCon [], noSpan UNIT_DATACON_NAME) ]
  where
    define : (STG.Name, SrcSpan) -> List (STG.Name, DataConRep, SrcSpan) -> Core ()
    define t ds = do
      st <- createSTyCon t ds
      _ <- traverse (registerInternalDataConToTyCon st . UN . fst) ds
      defineDataType (MkUnitId MAIN_UNIT) (MkModuleName MAIN_MODULE) st

indexWord8OffAddr : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
indexWord8OffAddr = do
  ad1 <- addrDataConId
  ti1 <- dataConIdForConstant IntType
  ((AlgDataCon [IntRep]) ** ti1) <- dataConIdForConstant IntType
    | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show ("indexWord8OffAddr2", wrongRep)
  v1 <- mkSBinderLocalStr "Idris.String.indexWord8OffAddr1"
  v2 <- mkSBinderLocalStr "Idris.String.indexWord8OffAddr2"
  v3 <- mkSBinderLocalStr "Idris.String.indexWord8OffAddr3"
  v4 <- mkSBinderRepLocalStr (SingleValue AddrRep) "Idris.String.indexWord8OffAddr4"
  v5 <- mkSBinderLocalStr "Idris.String.indexWord8OffAddr4"
  v6 <- mkSBinderRepLocalStr (SingleValue IntRep)   "Idris.String.indexWord8OffAddr4"
  v7 <- mkSBinderRepLocalStr (SingleValue Word8Rep) "Idris.String.indexWord8OffAddr4"
  pure
    $ topLevel !(mkSBinderTopLevel "Idris.String.indexWord8OffAddr") [mkSBinderSg v1,mkSBinderSg v2]
    $ unBox v1 ad1 !addrTyConId v3 v4
    $ unBox v2 ti1 !(tyConIdForConstant IntType) v5 v6
    $ StgCase
        (PrimAlt Word8Rep)
        (StgOpApp IndexWord8OffAddr [StgVarArg $ binderId v4, StgVarArg $ binderId v6])
        v7
        [ MkAlt AltDefault () (StgConApp !(dataConIdRepForConstant Word8Rep Bits8Type) (StgVarArg (binderId v7))) ]

indexWord8Array : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
indexWord8Array = do
  ((AlgDataCon [IntRep]) ** ad1) <- dataConIdForConstant IntType
    | wrongRep => coreFail $ InternalError $ "DataConId has wrong RepType: " ++ show ("indexWord8Array1", wrongRep)
  ba1     <- byteArrayDataConId
  arr     <- mkSBinderLocalStr "Idris.String.indexWord8Array1"
  i       <- mkSBinderLocalStr "Idris.String.indexWord8Array2"
  arrPrim <- mkSBinderRepLocalStr (SingleValue ByteArrayRep) "Idris.String.indexWord8Array3"
  iPrim   <- mkSBinderRepLocalStr (SingleValue IntRep)       "Idris.String.indexWord8Array4"
  w       <- mkSBinderRepLocalStr (SingleValue Word8Rep)     "Idris.String.indexWord8Array5"
  pure
    $ topLevel !(mkSBinderTopLevel "Idris.String.indexWord8Array") [mkSBinderSg arr,mkSBinderSg i]
    $ unBox arr ba1 !byteArrayTyConId !nonused arrPrim
    $ unBox i   ad1 !(tyConIdForConstant IntType) !nonused iPrim
    $ StgCase
        (PrimAlt Word8Rep)
        (StgOpApp IndexWord8Array [StgVarArg $ binderId arrPrim, StgVarArg $ binderId iPrim])
        w
        [ MkAlt AltDefault () (StgConApp !(dataConIdRepForConstant Word8Rep Bits8Type) (StgVarArg (binderId w))) ]

sizeofByteArray : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
sizeofByteArray = do -- GHC.Exts.sizeofByteArray#
  v1 <- mkSBinderLocalStr "Idris.String.sizeofByteArray1"
  v2 <- mkSBinderLocalStr "Idris.String.sizeofByteArray2"
  v3 <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.sizeofByteArray3"
  v4 <- mkSBinderRepLocalStr (SingleValue IntRep)      "Idris.String.sizeofByteArray4"
  ba1 <- byteArrayDataConId
  pure
    $ StgTopLifted
    $ StgNonRec !(mkSBinderTopLevel "Idris.String.sizeofByteArray")
    $ StgRhsClosure ReEntrant [mkSBinderSg v1]
    $ StgCase (AlgAlt !byteArrayTyConId) (StgApp (binderId v1) [] (SingleValue LiftedRep)) v2
      [ MkAlt (AltDataCon (mkDataConIdSg ba1)) v3
      $ StgCase
          (PrimAlt IntRep)
          (StgOpApp SizeOfByteArray (StgVarArg (binderId v3)))
          v4
          [ MkAlt AltDefault () (StgConApp !(dataConIdRepForConstant IntRep IntType) (StgVarArg (binderId v4))) ]
      ]

export
STRING_FROM_ADDR : String
STRING_FROM_ADDR = "Idris.String.stringFromAddr"

export
stringFromAddrBinderId2 : UniqueMapRef => Ref Counter Int => Core (BinderId (SingleValue LiftedRep))
stringFromAddrBinderId2 = mkBinderIdStr STRING_FROM_ADDR

export
stringFromAddrBinderId : UniqueMapRef => Ref Counter Int => Core BinderIdSg
stringFromAddrBinderId = map mkBinderIdSg $ mkBinderIdStr STRING_FROM_ADDR

-- Wrap an Addr# with (Idris.String.Val (Idris.String.Addr Addr#)) because String primitives are
-- implemented in ANF and compileANF compiles primitive types to Boxed types.
stringFromAddr : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
stringFromAddr = do
  v1 <- mkSBinderRepLocalStr (SingleValue AddrRep) "Idris.String.stringFromAddr1"
  v2 <- mkSBinderLocalStr "Idris.String.stringFromAddr2"
  pure
    $ StgTopLifted
    $ StgNonRec !(mkSBinderTopLevel STRING_FROM_ADDR)
    $ StgRhsClosure ReEntrant [mkSBinderSg v1]
    $ StgCase (AlgAlt !addrTyConId) (StgConApp !addrDataConId (StgVarArg (binderId v1))) v2
      [ MkAlt AltDefault () (StgConApp !litDataConId (StgVarArg (binderId v2))) ]

export
ADDR_FROM_STRING : String
ADDR_FROM_STRING = "Idris.String.addrFromString"

export
addrFromStringBinderId : UniqueMapRef => Ref Counter Int => Core (BinderId (SingleValue LiftedRep))
addrFromStringBinderId = mkBinderIdStr ADDR_FROM_STRING

addrFromString : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
addrFromString = do
  arg <- mkSBinderLocalStr "Idris.String.addrFromString1"
  litBinder <- mkSBinderLocalStr "Idris.String.addrFromString2"
  addrBinder <- mkSBinderRepLocalStr (SingleValue AddrRep) "Idris.String.addrFromString3"
  valBinder <- mkSBinderLocalStr "Idris.String.addFromString4"
  byteArrayBinder <- mkSBinderRepLocalStr (SingleValue ByteArrayRep) "Idris.String.addrFromString5"
  pure
    $ StgTopLifted
    $ StgNonRec !(mkSBinderTopLevel ADDR_FROM_STRING)
    $ StgRhsClosure ReEntrant [mkSBinderSg arg]
    $ StgCase
        (AlgAlt !idrisStringTyConId)
        (StgApp
          (binderId (the (SBinder (SingleValue LiftedRep)) arg))
          []
          (SingleValue LiftedRep))
        !nonused
        [ -- Lit
          MkAlt (AltDataCon (mkDataConIdSg !litDataConId)) litBinder
                (StgCase
                  (AlgAlt !addrTyConId)
                  (StgApp
                    (binderId (the (SBinder (SingleValue LiftedRep)) litBinder))
                    []
                    (SingleValue LiftedRep))
                  !nonused
                  [ MkAlt (AltDataCon (mkDataConIdSg !addrDataConId)) addrBinder
                          (StgApp (binderId addrBinder) [] (SingleValue AddrRep))
                  ])
        ,
          MkAlt (AltDataCon (mkDataConIdSg !valDataConId2)) valBinder
                (StgCase
                  (AlgAlt !byteArrayTyConId)
                  (StgApp
                    (binderId (the (SBinder (SingleValue LiftedRep)) valBinder))
                    []
                    (SingleValue LiftedRep))
                  !nonused
                  [ MkAlt (AltDataCon (mkDataConIdSg !byteArrayDataConId)) byteArrayBinder
                          (StgOpApp ByteArrayContents (StgVarArg (binderId byteArrayBinder)))
                  ])
        ]

-- Creates a mutable byte array
newByteArray : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
newByteArray = do
  v1 <- mkSBinderLocalStr "Idris.String.newByteArray1"
  v2 <- mkSBinderLocalStr "Idris.String.newByteArray2"
  v3 <- mkSBinderRepLocalStr (SingleValue IntRep) "Idris.String.newByteArray3"
  v4 <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.newByteArray4"
  da1 <- dataConIdRepForConstant IntRep IntType
  pure
    $ StgTopLifted
    $ StgNonRec !(mkSBinderTopLevel "Idris.String.newByteArray")
    $ StgRhsClosure ReEntrant [mkSBinderSg v1]
    $ StgCase (AlgAlt !(tyConIdForConstant IntType)) (StgApp (binderId v1) [] (SingleValue LiftedRep)) v2
      [ MkAlt (AltDataCon (mkDataConIdSg da1)) v3
      $ StgCase
          (PrimAlt MutableByteArrayRep) -- MutableByteArray has its own tag in GHC.
          (StgOpApp NewByteArray (StgVarArg (binderId v3)))
          v4
          [ MkAlt AltDefault () (StgConApp !mutableByteArrayDataConId (StgVarArg (binderId v4))) ]
      ]

copyAddrToByteArray : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
copyAddrToByteArray = do
  addr     <- mkSBinderLocalStr "Idris.String.copyAddrToByteArray1"
  marr     <- mkSBinderLocalStr "Idris.String.copyAddrToByteArray2"
  i        <- mkSBinderLocalStr "Idris.String.copyAddrToByteArray3"
  n        <- mkSBinderLocalStr "Idris.String.copyAddrToByteArray4"
  addrPrim <- mkSBinderRepLocalStr (SingleValue AddrRep) "Idris.String.copyAddrToByteArray5"
  marrPrim <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.copyAddrToByteArray6"
  iPrim    <- mkSBinderRepLocalStr (SingleValue IntRep) "Idris.String.copyAddrToByteArray7"
  nPrim    <- mkSBinderRepLocalStr (SingleValue IntRep) "Idris.String.copyAddrToByteArray8"
  ad1 <- addrDataConId
  m1  <- mutableByteArrayDataConId
  ti1 <- dataConIdRepForConstant IntRep IntType
  pure
    $ topLevel !(mkSBinderTopLevel "Idris.String.copyAddrToByteArray")
               [ mkSBinderSg addr
               , mkSBinderSg marr
               , mkSBinderSg i
               , mkSBinderSg n
               ]
    $ unBox addr ad1 !addrTyConId !nonused addrPrim
    $ unBox marr  m1 !mutableByteArrayTyConId !nonused marrPrim
    $ unBox i    ti1 !(tyConIdForConstant IntType) !nonused iPrim
    $ unBox n    ti1 !(tyConIdForConstant IntType) !nonused nPrim
    $ StgCase
        (MultiValAlt 0) -- Unboxed tuple of arity 0
        (StgOpApp
          CopyAddrToByteArray
            [ StgVarArg $ binderId addrPrim
            , StgVarArg $ binderId marrPrim
            , StgVarArg $ binderId iPrim
            , StgVarArg $ binderId nPrim ])
        !(nonusedRep (SingleValue VoidRep))
        [ MkAlt AltDefault () (StgConApp !unitDataConId ()) ]

writeByteArray : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
writeByteArray = do
  marr     <- mkSBinderLocalStr "Idris.String.writeByteArray1"
  i        <- mkSBinderLocalStr "Idris.String.writeByteArray2"
  w        <- mkSBinderLocalStr "Idris.String.writeByteArray3"
  marrPrim <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.writeByteArray4"
  iPrim    <- mkSBinderRepLocalStr (SingleValue IntRep)      "Idris.String.writeByteArray5"
  wPrim    <- mkSBinderRepLocalStr (SingleValue Word8Rep)    "Idris.String.writeByteArray6"
  m1  <- mutableByteArrayDataConId
  ti1 <- dataConIdRepForConstant IntRep IntType
  ti2 <- dataConIdRepForConstant Word8Rep CharType
  pure
    $ topLevel !(mkSBinderTopLevel "Idris.String.writeByteArray")
               [mkSBinderSg marr, mkSBinderSg i, mkSBinderSg w]
    $ unBox marr m1 !mutableByteArrayTyConId      !nonused marrPrim
    $ unBox i   ti1 !(tyConIdForConstant IntType) !nonused iPrim
    $ unBox w   ti2 !(tyConIdForConstant CharType) !nonused wPrim
    $ StgCase
        (MultiValAlt 0)
        (StgOpApp
          WriteWord8Array
          [ StgVarArg $ binderId marrPrim
          , StgVarArg $ binderId iPrim
          , StgVarArg $ binderId wPrim
          ])
        !(nonusedRep (SingleValue VoidRep))
        [ MkAlt AltDefault () (StgConApp !unitDataConId ()) ]

unsafeFreezeByteArray : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core TopBinding
unsafeFreezeByteArray = do
  marr      <- mkSBinderLocalStr "Idris.String.unsafeFreezeByteArray1"
  marrPrim  <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.unsafeFreezeByteArray2"
  arrResult <- mkSBinderRepLocalStr (SingleValue UnliftedRep) "Idris.String.unsafeFreezeByteArray3"
  ma <- mutableByteArrayDataConId
  pure
    $ topLevel !(mkSBinderTopLevel "Idris.String.unsafeFreezeByteArray") [mkSBinderSg marr]
    $ unBox marr ma !mutableByteArrayTyConId !nonused marrPrim
    $ StgCase
        (PrimAlt ByteArrayRep)
        (StgOpApp UnsafeFreezeByteArray (StgVarArg (binderId marrPrim)))
        arrResult
        [ MkAlt AltDefault () (StgConApp !byteArrayDataConId (StgVarArg (binderId arrResult))) ]

export
stgTopBindings : DataTypeMapRef => UniqueMapRef => Ref Counter Int => Core (List TopBinding)
stgTopBindings = traverse id
  [
--  copyAddrToByteArray
--  , indexWord8Array -- TODO: Bring them back
--  , indexWord8OffAddr
--  , newByteArray
--  , sizeofByteArray
    stringFromAddr
  , addrFromString
--  , unsafeFreezeByteArray
--  , writeByteArray
  ]

copyToLitVal : (Name.Name, ANFDef)
copyToLitVal =
  ( UN "Idris.String.copyToLitVal"
  , MkAFun [0]
  $ ALet e 1 (APrimVal e (I 0))
  $ ALet e 2 (APrimVal e (I 1))
  $ ALet e 3 (APrimVal e (B8 0)) -- w
  $ ALet e 4 (AAppName e Nothing (UN "Idris.String.addrStrLength") (map ALocal [0,1])) -- s
  $ ALet e 5 (AOp      e Nothing (Add IntType) (map ALocal [4,2])) -- s + 1
  $ ALet e 6 (AAppName e Nothing (UN "Idris.String.newByteArray") [ALocal 5]) -- arr
  $ ALet e 7 (AAppName e Nothing (UN "Idris.String.copyAddrToByteArray") (map ALocal [0,6,1,4]))
  $ AAppName e Nothing (UN "Idris.String.writeByteArray") (map ALocal [6,4,3])
  )

indexWord8Str : (Name.Name, ANFDef)
indexWord8Str =
  ( UN "Idris.String.indexWord8Str"
  , MkAFun [0, 1]
  $ AConCase e (ALocal 0)
    [ MkAConAlt (UN "Idris.String.Lit") DATACON (Just 0) [2]
      $ AAppName e Nothing (UN "Idris.String.indexWord8OffAddr") [ALocal 2, ALocal 1]
    , MkAConAlt (UN "Idris.String.Val") DATACON (Just 1) [3]
      $ AAppName e Nothing (UN "Idris.String.indexWord8Array") [ALocal 3, ALocal 1]
    ] Nothing
  )

strCompareGo : (Name.Name, ANFDef)
strCompareGo =
  ( UN "Idris.String.strCompareGo"
  , MkAFun [0,1,2,3,4] -- str1, str2, length1, length2, i
  $ ALet e 5 (AOp e Nothing (EQ IntType) (ALocal <$> [2,4]))
  $ AConstCase e (ALocal 5)
    [ -- True
      MkAConstAlt (I 1) $ AOp e Nothing (Sub IntType) (ALocal <$> [2, 3])
    , -- False
      MkAConstAlt (I 0)
      $ ALet e 6 (AOp e Nothing (EQ IntType) (ALocal <$> [3, 4]))
      $ AConstCase e (ALocal 6)
        [ -- True
          MkAConstAlt (I 1) $ AOp e Nothing (Sub IntType) (ALocal <$> [2, 3])
        , -- False
          MkAConstAlt (I 0)
          $ ALet e 7 (AAppName e Nothing (UN "Idris.String.indexWord8Str") [ALocal 0, ALocal 4])
          $ ALet e 8 (AAppName e Nothing (UN "Idris.String.indexWord8Str") [ALocal 1, ALocal 4])
          $ ALet e 9 (AOp      e Nothing (EQ Bits8Type) (ALocal <$> [7,8]))
          $ AConstCase e (ALocal 9)
            [ MkAConstAlt (I 1)
              $ ALet e 10 (APrimVal e (I 1))
              $ ALet e 11 (AOp e Nothing (Add IntType) (ALocal <$> [4,10]))
              $ AAppName e Nothing (UN "Idris.String.strCompareGo") (ALocal <$> [0,1,2,3,11])
            , MkAConstAlt (I 0)
              $ ALet e 12 (AOp e Nothing (Cast Bits8Type IntType) [ALocal 7])
              $ ALet e 13 (AOp e Nothing (Cast Bits8Type IntType) [ALocal 8])
              $ AOp e Nothing (Sub IntType) (ALocal <$> [12, 13])
            ] Nothing
        ] Nothing
    ] Nothing
  )

strCompare : (Name.Name, ANFDef)
strCompare =
  ( UN "Idris.String.strCompare"
  , MkAFun [0,1] -- str1, str2
  $ ALet e 2 (AAppName e Nothing (UN "Idris.String.strLength") [ALocal 0])
  $ ALet e 3 (AAppName e Nothing (UN "Idris.String.strLength") [ALocal 1])
  $ ALet e 4 (APrimVal e (I 0))
  $ AAppName e Nothing (UN "Idris.String.strCompareGo") (ALocal <$> [0,1,2,3,4])
  )

strEq : (Name.Name, ANFDef)
strEq =
  ( UN "Idris.String.strEq"
  , MkAFun [0,1] -- str1, str2
  $ ALet e 3 (AAppName e Nothing (UN "Idris.String.strCompare") (ALocal <$> [0,1]))
  $ AConstCase e (ALocal 3)
    [ MkAConstAlt (I 0) $ APrimVal e (I 1)
    ] $ Just $ APrimVal e (I 0)
  )

addrStrLength : (Name.Name, ANFDef)
addrStrLength =
  ( UN "Idris.String.addrStrLength"
  , MkAFun [0,1]
  $ ALet e 2 (AAppName e Nothing (UN "Idris.String.indexWord8OffAddr") [ALocal 0, ALocal 1]) -- ALocal0 should represent (Addr Addr#)
  $ AConstCase e (ALocal 2)
    [ MkAConstAlt (I 0) $ AV e (ALocal 1) ]
    $ Just
    $ ALet e 3 (APrimVal e (I 1))
    $ ALet e 4 (AOp e Nothing (Add IntType) [ALocal 1, ALocal 3])
    $ AAppName e Nothing (UN "Idris.String.addrStrLength") [ALocal 0, ALocal 4]
  )

strLength : (Name.Name, ANFDef)
strLength =
  ( UN "Idris.String.strLength"
  , MkAFun [0]
  $ AConCase e (ALocal 0)
    [ MkAConAlt (UN "Idris.String.Lit") DATACON (Just 0) [1]
      $ ALet e 2 (APrimVal e (I 0))
      $ AAppName e Nothing (UN "Idris.String.addrStrLength") [ALocal 1, ALocal 2]

    , MkAConAlt (UN "Idris.String.Val") DATACON (Just 1) [3]
      $ ALet e 4 (APrimVal e (I 1))
      $ ALet e 5 (AAppName e Nothing (UN "Idris.String.sizeofByteArray") [ALocal 3])
      $ AOp e Nothing (Sub IntType) [ALocal 5, ALocal 4]

    ] Nothing
  )

export
topLevelANFDefs : List (Name.Name, ANFDef)
topLevelANFDefs = []
{- --TODO: Bring them back
  [ addrStrLength
  , copyToLitVal
  , indexWord8Str
  , strCompare
  , strCompareGo
  , strEq
  , strLength
  ]
-}

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
-- ---------------------------------------------------------- [ KnockKnock.idr ]
--
-- Implementation of the knock protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module KnockKnock

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System
import System.Protocol

import RFC.Knock

-- ---------------------------------------------------------- [ Server Process ]
covering
knockServer : (client : PID)
            -> Process (knockknock) 'Server ['Client := client] [STDIO] ()
knockServer client = do
    (kk ** _ ) <- recvFrom 'Client
    putStrLn $ "From Teller: " ++ kk

    sendTo 'Client ("Who's there?" ** Refl)

    res <- recvFrom 'Client
    putStrLn $ "From Teller: " ++ res

    sendTo 'Client ((res ++ " who?") ** Refl)

    putStrLn $ "From Teller: " ++ !(recvFrom 'Client)

-- ---------------------------------------------------------- [ Client Process ]
covering
knockClient : String -> String
            -> (server : PID) -> Process (knockknock) 'Client ['Server := server] [STDIO] ()
knockClient setup reveal svr = do
    sendTo 'Server ("Knock Knock" ** Refl)

    (res ** _) <- recvFrom 'Server
    putStrLn $ "From Mark: " ++ res

    sendTo 'Server setup

    (res' ** _) <- recvFrom 'Server
    putStrLn $ "From Mark: " ++ res'

    sendTo 'Server reveal

-- ------------------------------------------------------ [ Sample Innvocation ]

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
covering
doKnockKnock : String -> String -> IO ()
doKnockKnock setup reveal = runConc [()] (doKnock setup reveal)
  where
    doKnock : String -> String -> Process (knockknock) 'Client [] [STDIO] ()
    doKnock s r = do
       server <- spawn (knockServer) [()]
       setChan 'Server server
       knockClient s r server
       dropChan 'Server
       pure ()

processArgs : (List String) -> Maybe (String, String)
processArgs [x] = Nothing
processArgs (x::y::z) = Just (y, unwords z)

-- -------------------------------------------------------------------- [ Main ]
usage : String
usage = unwords ["Usage: ./knockknock <setup> <reveal>"]

namespace Main
  main : IO ()
  main = do
    args <- getArgs
    case processArgs args of
      Just (x,y) => doKnockKnock x y
      Nothing => putStrLn usage

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

ext: idr

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Extra.Binary

import public Data.Binary.Digit
import Data.Bits
import Data.DPair
import Data.Vect
import Data.Nat

||| `False` -> `O`, `True` -> `I`
public export
boolToDigit : Bool -> Digit
boolToDigit False = O
boolToDigit True = I

||| `O` -> `0`, `I` -> `1`
export
digitToInteger : Digit -> Integer
digitToInteger O = 0
digitToInteger I = 1

||| A type to represent endianness
public export
data Endianness : Type where
  ||| Little endian
  LE : Endianness
  ||| Big endian
  BE : Endianness

||| `LE` -> `BE`, `BE` -> `LE`
public export
flip : Endianness -> Endianness
flip LE = BE
flip BE = LE

||| Binary representation, basically `Vect` but takes account into endianness
public export
data Binary : Endianness -> Nat -> Type where
  Nil : Binary endian 0
  (::) : Digit -> Binary endian n -> Binary endian (S n)

||| Convert a `Vect` into a `Binary LE`
public export
fromVectLE : Vect n Digit -> Binary LE n
fromVectLE Nil = Nil
fromVectLE (x :: xs) = x :: fromVectLE xs

||| Convert a `Vect` into a `Binary BE`
public export
fromVectBE : Vect n Digit -> Binary BE n
fromVectBE Nil = Nil
fromVectBE (x :: xs) = x :: fromVectBE xs

||| An auxiliary function for `reverse`, useful for proving stuff
public export
reverseOnto : Binary (flip endian) a -> Binary endian m -> Binary (flip endian) (a + m)
reverseOnto acc Nil = rewrite plusZeroRightNeutral a in acc
reverseOnto {m = S n} acc (x :: xs) = rewrite sym (plusSuccRightSucc a n) in reverseOnto (x :: acc) xs

||| Reverse a `Binary`, and flips its endianness
public export
reverse : Binary endian n -> Binary (flip endian) n
reverse xs = reverseOnto Nil xs

||| Some helper function for showing `Binary BE`
private
showBEHelper : {default True first : Bool} -> Binary BE n -> String
showBEHelper {first = False} Nil = ""
showBEHelper {first = False} (O :: xs) = strCons '0' (showBEHelper {first = False} xs)
showBEHelper {first = False} (I :: xs) = strCons '1' (showBEHelper {first = False} xs)
showBEHelper {first = True} xs = "0b" <+> showBEHelper {first = False} xs

export
{endian : Endianness} -> Show (Binary endian n) where
  show Nil = ""
  show {endian = LE} xs = show $ reverse xs
  show {endian = BE} xs = showBEHelper xs

||| Converts a `Bits8` into `Binary LE 8`
export
fromBits8LE : Bits8 -> Binary LE 8
fromBits8LE m = fromVectLE $ map (boolToDigit . testBit m)
  [ (Element 0 (lteReflectsLTE 1 8 Refl))
  , (Element 1 (lteReflectsLTE 2 8 Refl))
  , (Element 2 (lteReflectsLTE 3 8 Refl))
  , (Element 3 (lteReflectsLTE 4 8 Refl))
  , (Element 4 (lteReflectsLTE 5 8 Refl))
  , (Element 5 (lteReflectsLTE 6 8 Refl))
  , (Element 6 (lteReflectsLTE 7 8 Refl))
  , (Element 7 (lteReflectsLTE 8 8 Refl))
  ]

||| Converts a `Bits16` into `Binary LE 16`
export
fromBits16LE : Bits16 -> Binary LE 16
fromBits16LE m = fromVectLE $ map (boolToDigit . testBit m)
  [ Element 0 (lteReflectsLTE 1 16 Refl)
  , Element 1 (lteReflectsLTE 2 16 Refl)
  , Element 2 (lteReflectsLTE 3 16 Refl)
  , Element 3 (lteReflectsLTE 4 16 Refl)
  , Element 4 (lteReflectsLTE 5 16 Refl)
  , Element 5 (lteReflectsLTE 6 16 Refl)
  , Element 6 (lteReflectsLTE 7 16 Refl)
  , Element 7 (lteReflectsLTE 8 16 Refl)
  , Element 8 (lteReflectsLTE 9 16 Refl)
  , Element 9 (lteReflectsLTE 10 16 Refl)
  , Element 10 (lteReflectsLTE 11 16 Refl)
  , Element 11 (lteReflectsLTE 12 16 Refl)
  , Element 12 (lteReflectsLTE 13 16 Refl)
  , Element 13 (lteReflectsLTE 14 16 Refl)
  , Element 14 (lteReflectsLTE 15 16 Refl)
  , Element 15 (lteReflectsLTE 16 16 Refl)
  ]

||| Converts a `Bits32` into `Binary LE 32`
export
fromBits32LE : Bits32 -> Binary LE 32
fromBits32LE m = fromVectLE $ map (boolToDigit . testBit m)
  [ Element 0 (lteReflectsLTE 1 32 Refl)
  , Element 1 (lteReflectsLTE 2 32 Refl)
  , Element 2 (lteReflectsLTE 3 32 Refl)
  , Element 3 (lteReflectsLTE 4 32 Refl)
  , Element 4 (lteReflectsLTE 5 32 Refl)
  , Element 5 (lteReflectsLTE 6 32 Refl)
  , Element 6 (lteReflectsLTE 7 32 Refl)
  , Element 7 (lteReflectsLTE 8 32 Refl)
  , Element 8 (lteReflectsLTE 9 32 Refl)
  , Element 9 (lteReflectsLTE 10 32 Refl)
  , Element 10 (lteReflectsLTE 11 32 Refl)
  , Element 11 (lteReflectsLTE 12 32 Refl)
  , Element 12 (lteReflectsLTE 13 32 Refl)
  , Element 13 (lteReflectsLTE 14 32 Refl)
  , Element 14 (lteReflectsLTE 15 32 Refl)
  , Element 15 (lteReflectsLTE 16 32 Refl)
  , Element 16 (lteReflectsLTE 17 32 Refl)
  , Element 17 (lteReflectsLTE 18 32 Refl)
  , Element 18 (lteReflectsLTE 19 32 Refl)
  , Element 19 (lteReflectsLTE 20 32 Refl)
  , Element 20 (lteReflectsLTE 21 32 Refl)
  , Element 21 (lteReflectsLTE 22 32 Refl)
  , Element 22 (lteReflectsLTE 23 32 Refl)
  , Element 23 (lteReflectsLTE 24 32 Refl)
  , Element 24 (lteReflectsLTE 25 32 Refl)
  , Element 25 (lteReflectsLTE 26 32 Refl)
  , Element 26 (lteReflectsLTE 27 32 Refl)
  , Element 27 (lteReflectsLTE 28 32 Refl)
  , Element 28 (lteReflectsLTE 29 32 Refl)
  , Element 29 (lteReflectsLTE 30 32 Refl)
  , Element 30 (lteReflectsLTE 31 32 Refl)
  , Element 31 (lteReflectsLTE 32 32 Refl)
  ]

||| Convert a `Binary` into its corresponding integer representation
export
toInteger : {endian : Endianness} -> Binary endian n -> Integer
toInteger Nil = 0
toInteger {endian = LE} (x :: xs) = digitToInteger x + 2 * (toInteger xs)
toInteger {endian = BE} xs = toInteger $ reverse xs

public export
append : Binary endian m -> Binary endian n -> Binary endian (m + n)
append Nil ys = ys
append (x :: xs) ys = x :: (append xs ys)


text:
||| A minimalistic testing framework with pretty priting
||| and (not yet implemented) value diffing.
module Test.Mini

import Control.ANSI.SGR
import Generics.Derive
import Text.Show.Pretty

%language ElabReflection

--------------------------------------------------------------------------------
--          Test Results
--------------------------------------------------------------------------------

namespace Success

  ||| A successful test case
  public export
  record Success i o where
    constructor MkSuccess
    input  : i
    result : o

  %runElab derive "Success" [Generic,Meta,Show,Eq,PrettyVal]

namespace Failure

  ||| A failed test case
  public export
  record Failure i o where
    constructor MkFailure
    input    : i
    result   : o
    expected : o

  %runElab derive "Failure" [Generic,Meta,Show,Eq,PrettyVal]

public export
record Result i o where
  constructor MkResult
  ok     : List (Success i o)
  failed : List (Failure i o)

%runElab derive "Result" [Generic,Meta,Show,Eq,Semigroup,Monoid]

export
Semigroup (Result i o) where (<+>) = genAppend

export
Monoid (Result i o) where neutral = genNeutral

--------------------------------------------------------------------------------
--          Running Tests
--------------------------------------------------------------------------------

public export
run :  Foldable t
    => (f : i -> Either (Failure i o) (Success i o))
    -> t i
    -> Result i o
run f = concatMap run'
  where run' : i -> Result i o
        run' inp = case f inp of
                        (Left x)  => MkResult [] [x]
                        (Right x) => MkResult [x] []

public export
runEq : (Foldable t, Eq o) => (f : i -> o) -> t (i,o) -> Result i o
runEq f = concatMap run'
  where run' : (i,o) -> Result i o
        run' (inp,exp) = let res = f inp
                          in if exp == res
                                then MkResult [MkSuccess inp exp] []
                                else MkResult [] [MkFailure inp res exp]

--------------------------------------------------------------------------------
--          ANSI Colorings and Reporting
--------------------------------------------------------------------------------

export
foreground : Color -> String -> String
foreground c s = escapeSGR [SetForeground c] ++ s ++ escapeSGR [Reset]

export
greenOk : String
greenOk =   "[" ++ foreground Green "OK" ++ "]      "

export
redFailed : String
redFailed = "[" ++ foreground Red   "Failed" ++ "]  "

export
spaces : String
spaces = "          "

export
report : PrettyVal i => PrettyVal o => Result i o -> IO Bool
report (MkResult ok [])      =
  putStrLn (greenOk ++ show (length ok) ++ " tests run") $> True

report (MkResult ok (f::fs)) =
  do putStrLn (redFailed ++ summary)
     putStrLn "First failure"
     dumpIO f
     pure False
  where summary : String
        summary = unlines [ show (length ok + length fs + 1) ++ " tests run"
                          , spaces ++ show (length fs + 1) ++ " tests failed"
                          ]

export
testAll : List (IO Bool) -> IO Bool
testAll = map and . traverse (map delay)


text:
module LightClick.Types.Direction

import Decidable.Equality

import Toolkit.Decidable.Informative

%default total

public export
data Direction = IN | OUT | INOUT

export
Show Direction where
  show IN = "IN"
  show OUT = "OUT"
  show INOUT = "INOUT"

inNotOut : (IN = OUT) -> Void
inNotOut Refl impossible

inNotInOut : (IN = INOUT) -> Void
inNotInOut Refl impossible

outNotInOut : (OUT = INOUT) -> Void
outNotInOut Refl impossible

export
DecEq Direction where
  decEq IN IN = Yes Refl
  decEq IN OUT = No inNotOut
  decEq IN INOUT = No inNotInOut

  decEq OUT IN = No (negEqSym inNotOut)
  decEq OUT OUT = Yes Refl
  decEq OUT INOUT = No outNotInOut

  decEq INOUT IN = No (negEqSym inNotInOut)
  decEq INOUT OUT = No (negEqSym outNotInOut)
  decEq INOUT INOUT = Yes Refl

namespace Valid

  public export
  data Valid : (src,dest : Direction) -> Type where
    VOI : Valid OUT   IN
    VBI : Valid INOUT IN
    VOB : Valid OUT   INOUT
    VBB : Valid INOUT INOUT

  dirIsLR : Valid IN dest -> Void
  dirIsLR VOI impossible
  dirIsLR VBI impossible
  dirIsLR VOB impossible
  dirIsLR VBB impossible

  dirAreSame : Valid OUT OUT -> Void
  dirAreSame VOI impossible
  dirAreSame VBI impossible
  dirAreSame VOB impossible
  dirAreSame VBB impossible

  dirIsLR' : Valid INOUT OUT -> Void
  dirIsLR' VOI impossible
  dirIsLR' VBI impossible
  dirIsLR' VOB impossible
  dirIsLR' VBB impossible

  public export
  data Error = InputCannotSend | DirIsSame | OutputCannotReceive

  export
  valid : (src, dest : Direction)
                    -> DecInfo Direction.Valid.Error (Valid src dest)
  valid IN dest = No InputCannotSend dirIsLR
  valid OUT dest with (dest)
    valid OUT dest | IN = Yes VOI
    valid OUT dest | OUT = No DirIsSame dirAreSame
    valid OUT dest | INOUT = Yes VOB

  valid INOUT dest with (dest)
    valid INOUT dest | IN = Yes VBI
    valid INOUT dest | OUT = No OutputCannotReceive (dirIsLR')
    valid INOUT dest | INOUT = Yes VBB

namespace Safe

  public export
  data Safe : (src,dest : Direction) -> Type where
    SOI : Safe OUT   IN
    SBI : Safe INOUT IN
    SBB : Safe INOUT INOUT

  safeDirCannotIn : Safe IN dest -> Void
  safeDirCannotIn SOI impossible
  safeDirCannotIn SBI impossible
  safeDirCannotIn SBB impossible

  safeDirNotOO : Safe OUT OUT -> Void
  safeDirNotOO SOI impossible
  safeDirNotOO SBI impossible
  safeDirNotOO SBB impossible

  safeDirNoFeedbackOO : Safe OUT INOUT -> Void
  safeDirNoFeedbackOO SOI impossible
  safeDirNoFeedbackOO SBI impossible
  safeDirNoFeedbackOO SBB impossible

  safeDirNoFeedbackBO : Safe INOUT OUT -> Void
  safeDirNoFeedbackBO SOI impossible
  safeDirNoFeedbackBO SBI impossible
  safeDirNoFeedbackBO SBB impossible

  public export
  data Error = VCError Direction.Valid.Error
             | PossibleFeedbackFromReceiver
             | PossibleFeedbackFromSender

  export
  safe : (src, dest : Direction) -> DecInfo Direction.Safe.Error (Safe src dest)
  safe IN dest = No (VCError InputCannotSend) safeDirCannotIn
  safe OUT dest with (dest)
    safe OUT dest | IN = Yes SOI
    safe OUT dest | OUT = No (VCError DirIsSame) safeDirNotOO
    safe OUT dest | INOUT = No PossibleFeedbackFromReceiver safeDirNoFeedbackOO

  safe INOUT dest with (dest)
    safe INOUT dest | IN = Yes SBI
    safe INOUT dest | OUT = No PossibleFeedbackFromSender safeDirNoFeedbackBO
    safe INOUT dest | INOUT = Yes SBB

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
-- ---------------------------------------------------------- [ KnockKnock.idr ]
--
-- Implementation of the knock protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module KnocKnockArgs

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System
import System.Protocol

import RFC.Knock

-- ---------------------------------------------------------- [ Server Process ]
covering
knockee : (client : PID)
            -> Process (knockknock) 'Server ['Client := client] [STDIO] ()
knockee client = do
    (kk ** _ ) <- recvFrom 'Client
    putStrLn $ "From Knocker: " ++ kk

    sendTo 'Client ("Who's there?" ** Refl)

    res <- recvFrom 'Client
    putStrLn $ "From Knocker: " ++ res

    sendTo 'Client ((res ++ " who?") ** Refl)

    putStrLn $ "From Knocker: " ++ !(recvFrom 'Client)

-- ---------------------------------------------------------- [ Client Process ]
covering
knocker : (server : PID)
            -> Process (knockknock) 'Client ['Server := server] [STDIO] ()
knocker server = do
    sendTo 'Server ("Knock Knock" ** Refl)

    (res ** _) <- recvFrom 'Server
    putStrLn $ "From Knockee: " ++ res

    putStr "Enter the msg: "
    setup <- getStr
    sendTo 'Server $ trim setup

    (res' ** _) <- recvFrom 'Server
    putStrLn $ "From Knockee: " ++ res'

    putStr "Enter the res: "
    reveal <- getStr
    sendTo 'Server $ trim reveal

-- ------------------------------------------------------ [ Sample Innvocation ]

doKnockKnock : IO ()
doKnockKnock = runConc [()] doKnock
  where
    doKnock : Process (knockknock) 'Client [] [STDIO] ()
    doKnock = do
       server <- spawn (knockee) [()]
       setChan 'Server server
       knocker server
       dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doKnockKnock

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


text:
> module FastSimpleProb.BasicProperties

> import Data.List

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import Double.Predicates
> import List.Operations
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Properties
> import List.Operations
> import List.Properties

> %default total
> %access public export
> %auto_implicits on

* Properties of |toList|:

> using implementation NumNonNegDouble
>   |||
>   toListLemma : {A : Type} -> (sp : SimpleProb A) -> Positive (toDouble (sumMapSnd (toList sp)))
>   toListLemma (MkSimpleProb _ prf) = prf

* Properties of weights:

> using implementation NumNonNegDouble
>   |||
>   positiveWeights : {A : Type} -> (sp : SimpleProb A) -> Positive (toDouble (sum (weights sp)))
>   positiveWeights = toListLemma

> |||
> lengthSupportWeightsLemma : {A : Type} ->
>                             (sp : SimpleProb A) ->
>                             length (support sp) = length (weights sp)
> lengthSupportWeightsLemma sp = lengthLemma (toList sp) fst snd

* Implementations:

> using implementation ShowNonNegDouble
>   ||| SimpleProb is an implementation of Show
>   implementation Show a => Show (SimpleProb a) where
>     show sp = show (toList sp)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
counts : String -> (Nat, Nat)
counts str =
  let numWords = length (words str)
      numChars = length str
  in
  (numWords, numChars)

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Main

import IdrisScript
import IdrisScript.RegExps

main : JS_IO ()
main = do
  let text = "The Cloud is where all the Cloud Computing happens!"
  regex <- newRegExp "Cloud" [Global]

  print !(replace text regex "Kitten")

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Sanity.Hello
import Effects
import Effect.StdIO
||| Defining this in another file using the STDIO effect is not that practical,
||| but it should help illustrate the project structure.
public export
sayHello : Eff () [STDIO]
sayHello = putStrLn "Hello, world!"

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module TTImp.Elab.RunElab

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.GetType
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Reflect
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Reflect
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

%default covering

export
elabScript : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             FC -> NestedNames vars ->
             Env Term vars -> NF vars -> Maybe (Glued vars) ->
             Core (NF vars)
elabScript fc nest env script@(NDCon nfc nm t ar args) exp
    = do defs <- get Ctxt
         fnm <- toFullNames nm
         case fnm of
              NS ns (UN (Basic n))
                 => if ns == reflectionNS
                      then elabCon defs n (map snd args)
                      else failWith defs $ "bad reflection namespace " ++ show ns
              _ => failWith defs $ "bad fullnames " ++ show fnm
  where
    failWith : Defs -> String -> Core a
    failWith defs desc
      = do empty <- clearDefs defs
           throw (BadRunElab fc env !(quote empty env script) desc)

    scriptRet : Reflect a => a -> Core (NF vars)
    scriptRet tm
        = do defs <- get Ctxt
             nfOpts withAll defs env !(reflect fc defs False env tm)

    elabCon : Defs -> String -> List (Closure vars) -> Core (NF vars)
    elabCon defs "Pure" [_,val]
        = do empty <- clearDefs defs
             evalClosure empty val
    elabCon defs "Bind" [_,_,act,k]
        = do act' <- elabScript fc nest env
                                !(evalClosure defs act) exp
             case !(evalClosure defs k) of
                  NBind _ x (Lam _ _ _ _) sc =>
                      elabScript fc nest env
                              !(sc defs (toClosure withAll env
                                              !(quote defs env act'))) exp
                  x => failWith defs $ "non-function RHS of a Bind: " ++ show x
    elabCon defs "Fail" [_, mbfc, msg]
        = do msg' <- evalClosure defs msg
             let customFC = case !(evalClosure defs mbfc >>= reify defs) of
                               EmptyFC => fc
                               x       => x
             throw (GenericMsg customFC ("Error during reflection: " ++
                                      !(reify defs msg')))
    elabCon defs "LogMsg" [topic, verb, str]
        = do topic' <- evalClosure defs topic
             verb' <- evalClosure defs verb
             unverifiedLogC !(reify defs topic') !(reify defs verb') $
                  do str' <- evalClosure defs str
                     reify defs str'
             scriptRet ()
    elabCon defs "LogTerm" [topic, verb, str, tm]
        = do topic' <- evalClosure defs topic
             verb' <- evalClosure defs verb
             unverifiedLogC !(reify defs topic') !(reify defs verb') $
                  do str' <- evalClosure defs str
                     tm' <- evalClosure defs tm
                     pure $ !(reify defs str') ++ ": " ++
                             show (the RawImp !(reify defs tm'))
             scriptRet ()
    elabCon defs "Check" [exp, ttimp]
        = do exp' <- evalClosure defs exp
             ttimp' <- evalClosure defs ttimp
             tidx <- resolveName (UN $ Basic "[elaborator script]")
             e <- newRef EST (initEState tidx env)
             (checktm, _) <- runDelays (const True) $
                     check top (initElabInfo InExpr) nest env !(reify defs ttimp')
                           (Just (glueBack defs env exp'))
             empty <- clearDefs defs
             nf empty env checktm
    elabCon defs "Quote" [exp, tm]
        = do tm' <- evalClosure defs tm
             defs <- get Ctxt
             empty <- clearDefs defs
             scriptRet $ map rawName !(unelabUniqueBinders env !(quote empty env tm'))
    elabCon defs "Lambda" [x, _, scope]
        = do empty <- clearDefs defs
             NBind bfc x (Lam fc' c p ty) sc <- evalClosure defs scope
                   | _ => throw (GenericMsg fc "Not a lambda")
             n <- genVarName "x"
             sc' <- sc defs (toClosure withAll env (Ref bfc Bound n))
             qsc <- quote empty env sc'
             let lamsc = refToLocal n x qsc
             qp <- quotePi p
             qty <- quote empty env ty
             let env' = Lam fc' c qp qty :: env

             runsc <- elabScript fc (weaken nest) env'
                                 !(nf defs env' lamsc) Nothing -- (map weaken exp)
             nf empty env (Bind bfc x (Lam fc' c qp qty) !(quote empty env' runsc))
       where
         quotePi : PiInfo (Closure vars) -> Core (PiInfo (Term vars))
         quotePi Explicit = pure Explicit
         quotePi Implicit = pure Implicit
         quotePi AutoImplicit = pure AutoImplicit
         quotePi (DefImplicit t) = throw (GenericMsg fc "Can't add default lambda")
    elabCon defs "Goal" []
        = do let Just gty = exp
                 | Nothing => nfOpts withAll defs env
                                     !(reflect fc defs False env (the (Maybe RawImp) Nothing))
             ty <- getTerm gty
             scriptRet (Just $ map rawName $ !(unelabUniqueBinders env ty))
    elabCon defs "LocalVars" []
        = scriptRet vars
    elabCon defs "GenSym" [str]
        = do str' <- evalClosure defs str
             n <- genVarName !(reify defs str')
             scriptRet n
    elabCon defs "InCurrentNS" [n]
        = do n' <- evalClosure defs n
             nsn <- inCurrentNS !(reify defs n')
             scriptRet nsn
    elabCon defs "GetType" [n]
        = do n' <- evalClosure defs n
             res <- lookupTyName !(reify defs n') (gamma defs)
             scriptRet !(traverse unelabType res)
      where
        unelabType : (Name, Int, ClosedTerm) -> Core (Name, RawImp)
        unelabType (n, _, ty)
            = pure (n, map rawName !(unelabUniqueBinders [] ty))
    elabCon defs "GetLocalType" [n]
        = do n' <- evalClosure defs n
             n <- reify defs n'
             case defined n env of
                  Just (MkIsDefined rigb lv) =>
                       do let binder = getBinder lv env
                          let bty = binderType binder
                          scriptRet $ map rawName !(unelabUniqueBinders env bty)
                  _ => throw (GenericMsg fc (show n ++ " is not a local variable"))
    elabCon defs "GetCons" [n]
        = do n' <- evalClosure defs n
             cn <- reify defs n'
             Just (TCon _ _ _ _ _ _ cons _) <-
                     lookupDefExact cn (gamma defs)
                 | _ => throw (GenericMsg fc (show cn ++ " is not a type"))
             scriptRet cons
    elabCon defs "Declare" [d]
        = do d' <- evalClosure defs d
             decls <- reify defs d'
             traverse_ (processDecl [] (MkNested []) []) decls
             scriptRet ()
    elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++
                                          ", or incorrect count of arguments: " ++ show (length args)
elabScript fc nest env script exp
    = do defs <- get Ctxt
         empty <- clearDefs defs
         throw (BadRunElab fc env !(quote empty env script) "script is not a data value")

export
checkRunElab : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               {auto e : Ref EST (EState vars)} ->
               RigCount -> ElabInfo ->
               NestedNames vars -> Env Term vars ->
               FC -> RawImp -> Maybe (Glued vars) ->
               Core (Term vars, Glued vars)
checkRunElab rig elabinfo nest env fc script exp
    = do expected <- mkExpected exp
         defs <- get Ctxt
         unless (isExtension ElabReflection defs) $
             throw (GenericMsg fc "%language ElabReflection not enabled")
         let n = NS reflectionNS (UN $ Basic "Elab")
         let ttn = reflectiontt "TT"
         elabtt <- appCon fc defs n [expected]
         (stm, sty) <- runDelays (const True) $
                           check rig elabinfo nest env script (Just (gnf env elabtt))
         defs <- get Ctxt -- checking might have resolved some holes
         ntm <- elabScript fc nest env
                           !(nfOpts withAll defs env stm) (Just (gnf env expected))
         defs <- get Ctxt -- might have updated as part of the script
         empty <- clearDefs defs
         pure (!(quote empty env ntm), gnf env expected)
  where
    mkExpected : Maybe (Glued vars) -> Core (Term vars)
    mkExpected (Just ty) = pure !(getTerm ty)
    mkExpected Nothing
        = do nm <- genName "scriptTy"
             metaVar fc erased env nm (TType fc)


text:
import Data.Vect
import vect

data GameState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
  MkGameState : (word : String)
                -> (missing : Vect letters Char)
                -> GameState guesses_remaining letters

data Finished : Type where
  Lost : (game : GameState 0 (S letters)) -> Finished
  Won : (game : GameState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
  Letter : (c : Char) -> ValidInput [c]

isValidNil : ValidInput [] -> Void
isValidNil (Letter _) impossible

isValidTwo : ValidInput (x :: (y :: xs)) -> Void
isValidTwo (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No isValidNil
isValidInput (x :: []) = Yes (Letter x)
isValidInput (x :: (y :: xs)) = No isValidTwo

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

readGuess : IO (x ** ValidInput x)
readGuess = do
  putStr "Guess: "
  x <- getLine
  case isValidString (toUpper x) of
    Yes prf => pure (_ ** prf)
    No contra => do
      putStrLn "Invalid Guess"
      readGuess

processGuess : (letter : Char) ->
               GameState (S guesses) (S letters) ->
               Either (GameState guesses (S letters))
                      (GameState (S guesses) letters)
processGuess letter (MkGameState word missing)
  = case isElem letter missing of
         (Yes prf) => Right (MkGameState word (removeElem letter missing))
         (No contra) => Left (MkGameState word missing)

game : GameState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st = do
  (_ ** Letter letter) <- readGuess
  case processGuess letter st of
       Left l => do
         putStrLn "Wrong!"
         case guesses of
              Z => pure (Lost l)
              S k => game l
       Right r => do
         putStrLn "Right!"
         case letters of
              Z => pure (Won r)
              S k => game r

main : IO ()
main = do
  result <- game {guesses=2} (MkGameState "Test" ['T', 'E', 'S'])
  case result of
       Lost (MkGameState word missing) =>
         putStrLn ("You lose. The word was " ++ word)
       Won (MkGameState word missing) =>
         putStrLn ("You win! The word was " ++ word)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Stack

import Data.Vect

data StackCmd : Type -> Nat -> Nat -> Type where
  Push: Integer -> StackCmd () hieght (S hieght)
  Pop: StackCmd Integer (S hieght) hieght
  Top: StackCmd Integer (S hieght) (S hieght)

  Pure: Integer -> StackCmd Integer state state
  (>>=): StackCmd a state1 state2 -> (a -> StackCmd Integer state2 state3) -> StackCmd Integer state1 state3

testAdd : StackCmd Integer 0 0
testAdd = do Push 10
             Push 20
             val1 <- Pop
             val2 <- Pop
             Pure (val1 + val2)

runStack : (stack: Vect inH Integer) -> StackCmd ty inH outH -> (ty, Vect outH Integer)
runStack stack (Push x) = ((), x::stack)
runStack (val::xs) Pop = (val, xs)
runStack (val::xs) Top = (val, val::xs)

runStack stack (Pure x) = (x, stack)
runStack stack (x >>= f) = let (res, newStack) = runStack stack x
  in runStack newStack (f res)

readVectLen: Vect n String
readVectLen = ["test", "twenty"]

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Language.LSP.Message.Location

import Data.URI
import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%hide Prelude.Range
%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#position
public export
record Position where
  constructor MkPosition
  line      : Int
  character : Int
%runElab deriveJSON defaultOpts `{Position}

export
Eq Position where
  (MkPosition line1 char1) == (MkPosition line2 char2) = line1 == line2 && char1 == char2

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#range
public export
record Range where
  constructor MkRange
  start : Position
  end   : Position
%runElab deriveJSON defaultOpts `{Range}

export
Eq Range where
  (MkRange start1 end1) == (MkRange start2 end2) = start1 == start2 && end1 == end2

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#location
public export
record Location where
  constructor MkLocation
  uri   : URI
  range : Range
%runElab deriveJSON defaultOpts `{Location}

export
Eq Location where
  (MkLocation uri1 range1) == (MkLocation uri2 range2) = uri1 == uri2 && range1 == range2

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#locationLink
public export
record LocationLink where
  constructor MkLocationLink
  originSelectionRange : Maybe Range
  targetUri            : URI
  targetRange          : Range
  targetSelectionRange : Range
%runElab deriveJSON defaultOpts `{LocationLink}


text:
import Data.Vect

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

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

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (\a, b => a + b) x y :: addMatrix xs ys

computeRow : Num a => Vect m a -> Vect k (Vect m a) -> Vect k a
computeRow xs [] = []
computeRow xs (y :: ys) = sum (zipWith (*) xs y) :: computeRow xs ys

multMatrix: Num a => Vect n (Vect m a) -> Vect m (Vect k a) -> Vect n (Vect k a)
multMatrix [] ys = []
multMatrix (x :: xs) ys = let rightTrans = transposeMat ys in
                          computeRow x rightTrans :: multMatrix xs ys


text:
module ArithExp.Types

import ArithExp.AST
import ArithExp.SmallStep

||| Types for the ArithBool language
data SimpleType = TBool | TNum

-- syntax to make writing out types more natural.
syntax "[" [x] ":" [t] "]" = TypeOf x t

||| The ArithBool typing relation. There is no need to include a `gamma`-like
||| parameter here, as we don't have any variables.
data TypeOf : ArithBool -> SimpleType -> Type where
  ZeroT   : [ Zero : TNum ]
  SuccT   : [ n : TNum ] -> [ (Succ n) : TNum ]
  PredT   : [ n : TNum ] -> [ (Pred n) : TNum ]
  TruT    : [ Tru  : TBool ]
  FalsT   : [ Fals : TBool ]
  IfT     : [ c : TBool ] -> [ tcase : a ] -> [ fcase : a ]
         -> [ (IF c tcase fcase) : a ]
  IsZeroT : [ n : TNum ] -> [ (IsZero n) : TBool ]

||| Predicate for values in the language. Needed for defining progress
data IsValue : ArithBool -> Type where
  NumsValues : NV s -> IsValue s
  TruValue   : IsValue Tru
  FalsValue  : IsValue Fals

-- Boilerplate uninhabitted instances needed below.
--
-- These were all generated automatically with the idris-specific commands in
-- my editor, so the compiler should be able to infer it in principle. These
-- first two instances are just proofs that booleans cannot be typed as numbers.
Uninhabited [Fals : TNum] where
  uninhabited ZeroT impossible
  uninhabited (SuccT _) impossible
  uninhabited (PredT _) impossible
  uninhabited TruT impossible
  uninhabited FalsT impossible
  uninhabited (IfT _ _ _) impossible
  uninhabited (IsZeroT _) impossible

Uninhabited [Tru : TNum] where
  uninhabited ZeroT impossible
  uninhabited (SuccT _) impossible
  uninhabited (PredT _) impossible
  uninhabited TruT impossible
  uninhabited FalsT impossible
  uninhabited (IfT _ _ _) impossible
  uninhabited (IsZeroT _) impossible

||| Numbers are not booleans
boolNotNum : [c : TBool] -> NV c -> Void
boolNotNum TruT NvZero impossible
boolNotNum TruT (NvSucc _) impossible
boolNotNum FalsT NvZero impossible
boolNotNum FalsT (NvSucc _) impossible
boolNotNum (IfT _ _ _) NvZero impossible
boolNotNum (IfT _ _ _) (NvSucc _) impossible
boolNotNum (IsZeroT _) NvZero impossible
boolNotNum (IsZeroT _) (NvSucc _) impossible

||| Preservation lemma for type soundness
preservation : (a =>> b) -> [a : t] -> [b : t]
preservation IfTrue (IfT x y z) = y
preservation IfFalse (IfT x y z) = z
preservation (IfStep x) (IfT y z w) = IfT (preservation x y) z w
preservation (SuccStep x) (SuccT y) = SuccT (preservation x y)
preservation (IsZeroStep x) (IsZeroT y) = IsZeroT (preservation x y)
preservation IsZeroZero (IsZeroT x) = TruT
preservation IsZeroSucc (IsZeroT x) = FalsT
preservation (PredStep x) (PredT y) = PredT (preservation x y)
preservation PredZero (PredT x) = ZeroT
preservation PredSucc (PredT (SuccT x)) = x

||| Progress lemma for type soundness.
|||
||| This was more difficult to write, mostly because there are more cases
||| to consider. Each individual case is fairly straight-forward, so some
||| elaborator reflection should be able to automate this.
progress : [a : t] -> Either (IsValue a) (b ** (a =>> b))
progress ZeroT = Left (NumsValues NvZero)
progress (SuccT x) = case progress x of
                          Left  (NumsValues nv) => Left $ NumsValues (NvSucc nv)
                          -- booleans are not numbers
                          Left  TruValue        => absurd x
                          Left  FalsValue       => absurd x
                          Right (red ** step)   => Right ((Succ red) ** (SuccStep step))
progress (PredT x) =
  case progress x of
       Left (NumsValues NvZero)           => Right (Zero ** PredZero)
       Left (NumsValues (NvSucc k {n=n})) => Right (n ** PredSucc {prf=k})
       Left  TruValue                     => absurd x
       Left  FalsValue                    => absurd x
       Right (red ** step)                => Right ((Pred red) ** (PredStep step))
progress TruT   = Left TruValue
progress FalsT  = Left FalsValue
progress (IfT {tcase=tcase} {fcase=fcase} x y z) =
  case progress x of
       Left TruValue        => Right (tcase ** IfTrue)
       Left FalsValue       => Right (fcase ** IfFalse)
       Left (NumsValues nv) => absurd (boolNotNum x nv)
       Right (red ** step)  => Right ((IF red tcase fcase) ** IfStep step)
progress (IsZeroT x) =
  case progress x of
       Left TruValue                => absurd x
       Left FalsValue               => absurd x
       Left (NumsValues NvZero)     => Right (Tru ** IsZeroZero)
       Left (NumsValues (NvSucc k)) => Right (Fals ** IsZeroSucc)
       Right (red ** step)          => Right (IsZero red ** IsZeroStep step)

max_stars_repo_name: ezrosent/TAPL-idris

max_issues_repo_name: ezrosent/TAPL-idris

max_forks_repo_name: ezrosent/TAPL-idris


text:
module Web.Internal.MediasourceTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace ReadyState

  public export
  data ReadyState = Closed | Open | Ended

  public export
  Show ReadyState where
    show Closed = "closed"
    show Open = "open"
    show Ended = "ended"

  public export
  Eq ReadyState where
    (==) = (==) `on` show

  public export
  Ord ReadyState where
    compare = compare `on` show

  public export
  read : String -> Maybe ReadyState
  read "closed" = Just Closed
  read "open" = Just Open
  read "ended" = Just Ended
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ReadyState.read s)}
             -> ReadyState
  fromString s = fromJust $ read s

  export
  ToFFI ReadyState String where
    toFFI = show

  export
  FromFFI ReadyState String where
    fromFFI = read

namespace EndOfStreamError

  public export
  data EndOfStreamError = Network | Decode

  public export
  Show EndOfStreamError where
    show Network = "network"
    show Decode = "decode"

  public export
  Eq EndOfStreamError where
    (==) = (==) `on` show

  public export
  Ord EndOfStreamError where
    compare = compare `on` show

  public export
  read : String -> Maybe EndOfStreamError
  read "network" = Just Network
  read "decode" = Just Decode
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (EndOfStreamError.read s)}
             -> EndOfStreamError
  fromString s = fromJust $ read s

  export
  ToFFI EndOfStreamError String where
    toFFI = show

  export
  FromFFI EndOfStreamError String where
    fromFFI = read

namespace AppendMode

  public export
  data AppendMode = Segments | Sequence

  public export
  Show AppendMode where
    show Segments = "segments"
    show Sequence = "sequence"

  public export
  Eq AppendMode where
    (==) = (==) `on` show

  public export
  Ord AppendMode where
    compare = compare `on` show

  public export
  read : String -> Maybe AppendMode
  read "segments" = Just Segments
  read "sequence" = Just Sequence
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (AppendMode.read s)}
             -> AppendMode
  fromString s = fromJust $ read s

  export
  ToFFI AppendMode String where
    toFFI = show

  export
  FromFFI AppendMode String where
    fromFFI = read

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

export data MediaSource : Type where [external]

export
ToFFI MediaSource MediaSource where toFFI = id

export
FromFFI MediaSource MediaSource where fromFFI = Just

export
SafeCast MediaSource where
  safeCast = unsafeCastOnPrototypeName "MediaSource"

export data SourceBuffer : Type where [external]

export
ToFFI SourceBuffer SourceBuffer where toFFI = id

export
FromFFI SourceBuffer SourceBuffer where fromFFI = Just

export
SafeCast SourceBuffer where
  safeCast = unsafeCastOnPrototypeName "SourceBuffer"

export data SourceBufferList : Type where [external]

export
ToFFI SourceBufferList SourceBufferList where toFFI = id

export
FromFFI SourceBufferList SourceBufferList where fromFFI = Just

export
SafeCast SourceBufferList where
  safeCast = unsafeCastOnPrototypeName "SourceBufferList"


text:
{------------------------------------------------------------------------------
    SimpleBmp.idr
------------------------------------------------------------------------------}

||| A small library for writing RGBA32 BMP files.

module SimpleBmp

import Debug.Error

import Data.Bits
import Data.Buffer
import Data.IOArray

import Test.Unit.Assertions

%default total

%language ElabReflection -- for Data.Error.error

-------------------------------------------------------------------------------
--  constants                                                                --
-------------------------------------------------------------------------------

bitmapFileHeaderSize : Bits8
bitmapFileHeaderSize = 14 -- bytes
dibHeaderSize        : Bits8
dibHeaderSize        = 40 -- bytes
dibHeaderSizeInt     : Int
dibHeaderSizeInt     = prim__zextB8_Int dibHeaderSize
||| Pixel array starts immediately after the header. This is equal to the
||| combined bitmap file header + dib header sizes.
pixelArrayOffset     : Bits8
pixelArrayOffset     = bitmapFileHeaderSize + dibHeaderSize
pixelArrayOffsetInt  : Int
pixelArrayOffsetInt  = prim__zextB8_Int pixelArrayOffset
pixelArrayOffsetNat  : Nat
pixelArrayOffsetNat  = (fromIntegerNat . prim__zextInt_BigInt)
  pixelArrayOffsetInt

-------------------------------------------------------------------------------
--  datatypes                                                                --
-------------------------------------------------------------------------------

||| 14 byte bitmap file header + 40 byte DIB header.
public export
record Header where
  constructor MkHeader
  fileSize    : Bits32
  pixelWidth  : Bits16
  pixelHeight : Bits16
  headerData  : IOArray Bits8  -- pixelArrayOffset == 54 bytes

||| Combined header and raw image data. Note image data is stored as BGRA
||| pixels in reverse row order.
public export
record Bmp where
  constructor MkBmp
  header    : Header
  imageData : IOArray Bits8

-------------------------------------------------------------------------------
--  functions                                                                --
-------------------------------------------------------------------------------

--
--  private
--

||| 14 byte bitmap file header + 40 byte dib header + 2 bytes padding = 54 byte
||| header (bytes 0x00-0x37). File size (0x02-0x05) and image width and height
||| (0x12-0x19) fields are uninitialized.
newHeaderRaw : IO (IOArray Bits8)
newHeaderRaw = do
  let header_size = prim__zextB8_Int pixelArrayOffset -- convert to Int
  header <- newArray header_size 0x00 -- 54 zero-initialized bytes
  --
  --  bitmap file header: 14 bytes (0x00-0x0D)
  --
  unsafeWriteArray header 0x00 $ the Bits8 0x42   -- 'B'
  unsafeWriteArray header 0x01 $ the Bits8 0x4D   -- 'M'
  -- 0x02-0x05 to be filled in with file size
  -- 0x06-0x09 reserved left as 0x00
  unsafeWriteArray header 0x0A pixelArrayOffset -- 54 (bytes)
  -- 0x0B-0x0D additional bytes for pixel array offset not needed
  --
  --  dib header: 40 bytes (0x0E-0x35)
  --
  unsafeWriteArray header 0x0E dibHeaderSize    -- 40 (bytes)
  -- 0x0F-0x11 additional bytes for dib header size not needed
  -- 0x12-0x19 to be filled in with image width and height (pixels)
  unsafeWriteArray header 0x1A $ the Bits8 1      -- 1 color plane
  -- 0x1B additional byte for color planes not needed
  unsafeWriteArray header 0x1C $ the Bits8 32     -- 32 bpp
  -- 0x1D additional byte for bpp not needed
  -- 0x1E-0x21 compression method 0 == none
  -- 0x22-0x25 size of raw image data left as dummy value 0 for uncompressed bmps
  unsafeWriteArray header 0x26 $ the Bits8 0x13   -- horizontal resolution (2835)
  unsafeWriteArray header 0x27 $ the Bits8 0x0B   -- (2nd byte)
  -- 0x28-0x29 additional bytes for horizontal resolution not needed
  unsafeWriteArray header 0x2A $ the Bits8 0x13   -- vertical resolution (2835)
  unsafeWriteArray header 0x2B $ the Bits8 0x0B   -- (2nd byte)
  -- 0x2C-0x2D additional bytes for vertical resolution not needed
  -- 0x2E-0x31 number of colors in palette left as 0
  -- 0x32-0x35 number important colors used left as 0
  pure header

||| Create an initialized header with the given bits-per-pixel and image
||| dimensions.
headerWithSize : (pixel_width : Bits16) -> (pixel_height : Bits16) -> IO Header
headerWithSize pixel_width pixel_height = do
  let width32            = prim__zextB16_B32 pixel_width
  let height32           = prim__zextB16_B32 pixel_height
  let pixel_array_size   = the Bits32 $ 4 * width32 * height32 -- 4 bytes per pixel
  let header_size        = prim__zextB8_B32 pixelArrayOffset
  let file_size          = header_size + pixel_array_size
  -- reversed because values are little-endian, so the least significant
  -- bytes come first
  let file_size_bytes    = reverse $ b32ToBytes file_size
  let pixel_width_bytes  = reverse $ b16ToBytes pixel_width
  let pixel_height_bytes = reverse $ b16ToBytes pixel_height
  header_array <- newHeaderRaw
  -- 0x02-0x05 file size (bytes)
  unsafeWriteArray header_array 0x02 $ index 0 file_size_bytes
  unsafeWriteArray header_array 0x03 $ index 1 file_size_bytes
  unsafeWriteArray header_array 0x04 $ index 2 file_size_bytes
  unsafeWriteArray header_array 0x05 $ index 3 file_size_bytes
  -- 0x12-0x19 to be filled in with image width and height (pixels)
  unsafeWriteArray header_array 0x12 $ index 0 pixel_width_bytes
  unsafeWriteArray header_array 0x13 $ index 1 pixel_width_bytes
  -- 0x14-0x15 unused width bytes
  unsafeWriteArray header_array 0x16 $ index 0 pixel_height_bytes
  unsafeWriteArray header_array 0x17 $ index 1 pixel_height_bytes
  -- 0x18-0x19 unused height bytes
  pure $ MkHeader file_size pixel_width pixel_height header_array

||| Zero-initialized raw image data (4 * width * height bytes)
newImageDataRaw : (pixel_width : Bits16) -> (pixel_height : Bits16)
  -> IO (IOArray Bits8)
newImageDataRaw pixel_width pixel_height = do
  let width32   = prim__zextB16_B32 pixel_width
  let height32  = prim__zextB16_B32 pixel_height
  let bytes     = 4 * width32 * height32
  newArray (prim__zextB32_Int bytes) 0x00

--
--  public
--

||| Byte offset of given row-major pixel coords into the raw image data.
||| Returns `Nothing` if coordinates are out of bounds.
export
pixelOffset : Bmp -> Int -> Int -> Maybe Int
pixelOffset bmp row col =
  if row < 0 || pixel_height <= row || col < 0 || pixel_width <= col
  then Nothing else Just $ 4 * (pixel_width * (pixel_height - row - 1) + col)
where
  pixel_width  : Int
  pixel_width  = (prim__zextB16_Int . pixelWidth . header) bmp
  pixel_height : Int
  pixel_height = (prim__zextB16_Int . pixelHeight . header) bmp

||| Create a new `Bmp` record with the given dimensions. This will contain an
||| initialized `header` and a zero-initialized pixel array in `imageData`.
export
newBmp : (pixel_width : Bits16) -> (pixel_height : Bits16) -> IO Bmp
newBmp pixel_width pixel_height = do
  header     <- headerWithSize  pixel_width pixel_height
  image_data <- newImageDataRaw pixel_width pixel_height
  pure $ MkBmp header image_data

||| Return the RGBA values for the pixel at the given coordinates. Returns
||| `Nothing` if coordinates are outside of the image boundaries. Note that the
||| bytes are not returned in the same order as they are stored, which is BGRA.
export
covering
getPixel : Bmp -> Int -> Int -> IO (Maybe (Bits8, Bits8, Bits8, Bits8))
getPixel bmp@(MkBmp header image_data) row col = do
  let pixel_offset = pixelOffset bmp row col
  if isNothing pixel_offset then pure Nothing
  else do
    let pixel_offset = fromMaybe (error "unreachable") pixel_offset
    pure $ Just (
      !(unsafeReadArray image_data (pixel_offset + 2)), -- R
      !(unsafeReadArray image_data (pixel_offset + 1)), -- G
      !(unsafeReadArray image_data (pixel_offset + 0)), -- B
      !(unsafeReadArray image_data (pixel_offset + 3))  -- A
    )

||| Write RGBA values into the pixel at the given coordinates. Returns
||| `Nothing` if coordinates are outside of the image boundaries. Note that the
||| byte arguments are not in the same order as they are stored, which is BGRA.
export
covering
setPixel : Bmp -> Int -> Int -> (Bits8, Bits8, Bits8, Bits8) -> IO (Maybe ())
setPixel bmp@(MkBmp header image_data) row col (r, g, b, a) = do
  let pixel_offset = pixelOffset bmp row col
  if isNothing pixel_offset then pure Nothing
  else do
    let pixel_offset = fromMaybe (error "unreachable") pixel_offset
    unsafeWriteArray image_data (pixel_offset + 2) r -- R
    unsafeWriteArray image_data (pixel_offset + 1) g -- G
    unsafeWriteArray image_data (pixel_offset + 0) b -- B
    unsafeWriteArray image_data (pixel_offset + 3) a -- A
    pure $ Just ()

||| Writes `Bmp` to file.
export
writeBmpToFile : File -> Bmp -> IO (Maybe ())
writeBmpToFile file bmp = do
  let file_size  = prim__zextB32_Int $ (fileSize . header) bmp
  let image_size = (fromIntegerNat . prim__zextInt_BigInt) $
    file_size - pixelArrayOffsetInt
  Just buffer <- newBuffer file_size | Nothing => pure Nothing
  for_ (take pixelArrayOffsetNat $ iterate (+1) 0)
    (\i => setByte buffer i !(unsafeReadArray ((headerData . header) bmp) i))
  for_ (take image_size $ iterate (+1) 0)
    (\i => setByte buffer (pixelArrayOffsetInt + i)
      !(unsafeReadArray (imageData bmp) i))
  _ <- writeBufferToFile file buffer file_size
  pure $ Just ()

-------------------------------------------------------------------------------
--  tests                                                                    --
-------------------------------------------------------------------------------

export
test : IO ()
test = do
  bmp <- newBmp 3 3
  assertEquals (pixelOffset bmp 0 0) (Just 24)
  assertEquals (pixelOffset bmp 0 1) (Just 28)
  assertEquals (pixelOffset bmp 0 2) (Just 32)
  assertEquals (pixelOffset bmp 1 0) (Just 12)
  assertEquals (pixelOffset bmp 1 1) (Just 16)
  assertEquals (pixelOffset bmp 1 2) (Just 20)
  assertEquals (pixelOffset bmp 2 0) (Just 0)
  assertEquals (pixelOffset bmp 2 1) (Just 4)
  assertEquals (pixelOffset bmp 2 2) (Just 8)
  assertNothing !(setPixel bmp (-1) (-1) (0x63, 0x62, 0x61, 0x64))
  assertJust !(setPixel bmp 0 0 (0x63, 0x62, 0x61, 0x64))
  assertJust !(setPixel bmp 0 1 (0x2E, 0x2E, 0x2E, 0x2E))
  assertJust !(setPixel bmp 0 2 (0x2E, 0x2E, 0x2E, 0x0A))
  assertJust !(setPixel bmp 1 0 (0x2E, 0x2E, 0x2E, 0x2E))
  assertJust !(setPixel bmp 1 1 (0x2E, 0x2E, 0x2E, 0x2E))
  assertJust !(setPixel bmp 1 2 (0x2E, 0x2E, 0x2E, 0x0A))
  assertJust !(setPixel bmp 2 0 (0x2E, 0x2E, 0x2E, 0x2E))
  assertJust !(setPixel bmp 2 1 (0x2E, 0x2E, 0x2E, 0x2E))
  assertJust !(setPixel bmp 2 2 (0x7A, 0x79, 0x78, 0x0A))
  assertNothing !(setPixel bmp 3 3 (0x63, 0x62, 0x61, 0x64))
  assertJust !(writeBmpToFile stderr bmp)
  pure ()

max_stars_repo_name: spearman/simple-bmp

max_issues_repo_name: spearman/simple-bmp

max_forks_repo_name: spearman/simple-bmp