text:
||| Infaces of mutable container
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.Interfaces

%default total

-- --------------------------------------------------------------------------
{-
namespace Stack
  public export
  interface MutableStack m (a:Type -> Type) where
    null  : a t -> m Bool
    length : a t -> m Nat
    push  : t -> a t -> m ()
    pop   : a t -> m (Maybe t)

namespace Queue
  public export
  interface MutableQueue m (a:Type -> Type) where
    null   : a t -> m Bool
    length : a t -> m Nat
    push   : t -> a t -> m Bool
    pull   : a t -> m (Maybe t)

namespace Map
  public export
  interface MutableMap m (a: Type -> Type) k | a where
    null   : a v -> m Bool
    length : a v -> m Nat
    contains : k -> a v -> m Bool
    insert : k -> v -> a v -> m Bool
    lookup : k -> a v -> m (Maybe v)
    delete : k -> a v -> m Bool

namespace Set
  public export
  interface MutableSet m (a:Type) k | a where
    null : a -> m Bool
    length : a -> m Bool
    contains : k -> a -> m Bool
    insert : k -> a -> m Bool
    delete : k -> a -> m Bool

-}

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Test.TestGregorian

import Data.Fin

import Test.TestUtil
import Data.Time.Calendar.Gregorian
import Data.Time.Calendar.Days

export
test_toGregorian: IO ()
test_toGregorian = do
  let result = toGregorian (MkModifiedJulianDay 59053)
  assertEq "test_toGregorian" result (MkGregorian 2020 7 23) ""

export
test_fromGregorian: IO ()
test_fromGregorian = do
  let result = fromGregorian (MkGregorian 2020 7 23)
  assertEq "test_fromGregorian" result (MkModifiedJulianDay 59053) ""

export
test_gregorianMonthLength: IO ()
test_gregorianMonthLength = do
  let result = gregorianMonthLength 2020 (FS 0)
  assertEq "test_gregorianMonthLength" result 29 (show result)

export
test_gregorianMonthLengthNonLeap: IO ()
test_gregorianMonthLengthNonLeap = do
  let result = gregorianMonthLength 2021 (FS 0)
  assertEq "test_gregorianMonthLengthNonLeap" result 28 (show result)

export
test_rolloverMonths: IO ()
test_rolloverMonths = do
  let result = rolloverMonths (2020, 11)
  assertEq "test_rolloverMonths" (2020, 11) result (show result)
  let result = rolloverMonths (2020, 13)
  assertEq "test_rolloverMonthsToNextYear" (2021, 1) result (show result)

export
test_addGregorianMonths: IO ()
test_addGregorianMonths = do
  let result = addGregorianMonths 5 (fromGregorian (MkGregorian 2020 2 15))
  assertEq "test_addGregorianMonths" result (MkGregorian 2020 7 15) (show result)

ext: idr

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Language.LSP.Message.Method

import public Data.DPair
import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

public export
data MethodFrom = Client | Server

public export
data MethodType = Notification | Request

public export
data Method : MethodFrom -> MethodType -> Type where
  Initialize                          : Method Client Request
  Initialized                         : Method Client Notification
  Shutdown                            : Method Client Request
  Exit                                : Method Client Notification
  SetTrace                            : Method Client Notification
  WindowWorkDoneProgressCancel        : Method Client Notification
  WorkspaceDidChangeWorkspaceFolders  : Method Client Notification
  WorkspaceDidChangeConfiguration     : Method Client Notification
  WorkspaceDidChangeWatchedFiles      : Method Client Notification
  WorkspaceSymbol                     : Method Client Request
  WorkspaceExecuteCommand             : Method Client Request
  WorkspaceWillCreateFiles            : Method Client Request
  TextDocumentDidOpen                 : Method Client Notification
  TextDocumentDidChange               : Method Client Notification
  TextDocumentWillSave                : Method Client Notification
  TextDocumentWillSaveWaitUntil       : Method Client Request
  TextDocumentDidSave                 : Method Client Notification
  TextDocumentDidClose                : Method Client Notification
  TextDocumentCompletion              : Method Client Request
  CompletionItemResolve               : Method Client Request
  TextDocumentHover                   : Method Client Request
  TextDocumentSignatureHelp           : Method Client Request
  TextDocumentDeclaration             : Method Client Request
  TextDocumentDefinition              : Method Client Request
  TextDocumentTypeDefinition          : Method Client Request
  TextDocumentImplementation          : Method Client Request
  TextDocumentReferences              : Method Client Request
  TextDocumentDocumentHighlight       : Method Client Request
  TextDocumentDocumentSymbol          : Method Client Request
  TextDocumentCodeAction              : Method Client Request
  CodeActionResolve                   : Method Client Request
  TextDocumentCodeLens                : Method Client Request
  CodeLensResolve                     : Method Client Request
  TextDocumentDocumentLink            : Method Client Request
  DocumentLinkResolve                 : Method Client Request
  TextDocumentDocumentColor           : Method Client Request
  TextDocumentFormatting              : Method Client Request
  TextDocumentRangeFormatting         : Method Client Request
  TextDocumentOnTypeFormatting        : Method Client Request
  TextDocumentRename                  : Method Client Request
  TextDocumentPrepareRename           : Method Client Request
  TextDocumentFoldingRange            : Method Client Request
  TextDocumentSelectionRange          : Method Client Request
  TextDocumentPrepareCallHierarchy    : Method Client Request
  CallHierarchyIncomingCalls          : Method Client Request
  CallHierarchyOutgoingCalls          : Method Client Request
  TextDocumentSemanticTokensFull      : Method Client Request
  TextDocumentSemanticTokensFullDelta : Method Client Request
  TextDocumentSemanticTokensRange     : Method Client Request
  WorkspaceSemanticTokensRefresh      : Method Client Request
  TextDocumentLinkedEditingRange      : Method Client Request
  TextDocumentMoniker                 : Method Client Request

  LogTrace                            : Method Server Notification
  WindowShowMessage                   : Method Server Notification
  WindowShowMessageRequest            : Method Server Request
  WindowShowDocument                  : Method Server Request
  WindowLogMessage                    : Method Server Notification
  WindowWorkDoneProgressCreate        : Method Server Request
  TelemetryEvent                      : Method Server Notification
  ClientRegisterCapability            : Method Server Request
  ClientUnregisterCapability          : Method Server Request
  WorkspaceWorkspaceFolders           : Method Server Request
  WorkspaceConfiguration              : Method Server Request
  WorkspaceApplyEdit                  : Method Server Request
  TextDocumentPublishDiagnostics      : Method Server Notification
  WorkspaceCodeLensRefresh            : Method Server Request

  CancelRequest                       : Method from   Notification
  Progress                            : Method from   Notification

export
methodType : Method type from -> MethodType
methodType Initialize = Request
methodType Initialized = Notification
methodType Shutdown = Request
methodType Exit = Notification
methodType SetTrace = Notification
methodType WindowWorkDoneProgressCancel = Notification
methodType WorkspaceDidChangeWorkspaceFolders = Notification
methodType WorkspaceDidChangeConfiguration = Notification
methodType WorkspaceDidChangeWatchedFiles = Notification
methodType WorkspaceSymbol = Request
methodType WorkspaceExecuteCommand = Request
methodType WorkspaceWillCreateFiles = Request
methodType TextDocumentDidOpen = Notification
methodType TextDocumentDidChange = Notification
methodType TextDocumentWillSave = Notification
methodType TextDocumentWillSaveWaitUntil = Request
methodType TextDocumentDidSave = Notification
methodType TextDocumentDidClose = Notification
methodType CompletionItemResolve = Request
methodType TextDocumentHover = Request
methodType TextDocumentSignatureHelp = Request
methodType TextDocumentDeclaration = Request
methodType TextDocumentDefinition = Request
methodType TextDocumentTypeDefinition = Request
methodType TextDocumentImplementation = Request
methodType TextDocumentReferences = Request
methodType TextDocumentDocumentHighlight = Request
methodType TextDocumentDocumentSymbol = Request
methodType TextDocumentCodeAction = Request
methodType CodeActionResolve = Request
methodType TextDocumentCodeLens = Request
methodType CodeLensResolve = Request
methodType TextDocumentDocumentLink = Request
methodType DocumentLinkResolve = Request
methodType TextDocumentDocumentColor = Request
methodType TextDocumentFormatting = Request
methodType TextDocumentRangeFormatting = Request
methodType TextDocumentOnTypeFormatting = Request
methodType TextDocumentRename = Request
methodType TextDocumentPrepareRename = Request
methodType TextDocumentFoldingRange = Request
methodType TextDocumentSelectionRange = Request
methodType TextDocumentPrepareCallHierarchy = Request
methodType CallHierarchyIncomingCalls = Request
methodType CallHierarchyOutgoingCalls = Request
methodType TextDocumentSemanticTokensFull = Request
methodType TextDocumentSemanticTokensFullDelta = Request
methodType TextDocumentSemanticTokensRange = Request
methodType WorkspaceSemanticTokensRefresh = Request
methodType TextDocumentLinkedEditingRange = Request
methodType TextDocumentMoniker = Request
methodType LogTrace = Notification
methodType WindowShowMessage = Notification
methodType WindowShowMessageRequest = Request
methodType WindowShowDocument = Request
methodType WindowLogMessage = Notification
methodType WindowWorkDoneProgressCreate = Request
methodType TelemetryEvent = Notification
methodType ClientRegisterCapability = Request
methodType ClientUnregisterCapability = Request
methodType WorkspaceWorkspaceFolders = Request
methodType WorkspaceConfiguration = Request
methodType WorkspaceApplyEdit = Request
methodType TextDocumentPublishDiagnostics = Notification
methodType TextDocumentCompletion = Request
methodType WorkspaceCodeLensRefresh = Request
methodType CancelRequest = Notification
methodType Progress = Notification

export
ToJSON (Method type from) where
  toJSON Initialize                          = JString "initialize"
  toJSON Initialized                         = JString "initialized"
  toJSON Shutdown                            = JString "shutdown"
  toJSON Exit                                = JString "exit"
  toJSON SetTrace                            = JString "$/setTrace"
  toJSON WindowWorkDoneProgressCancel        = JString "window/workDoneProgress/cancel"
  toJSON WorkspaceDidChangeWorkspaceFolders  = JString "workspace/didChangeWorkspaceFolders"
  toJSON WorkspaceDidChangeConfiguration     = JString "workspace/didChangeConfiguration"
  toJSON WorkspaceDidChangeWatchedFiles      = JString "workspace/didChangeWatchedFiles"
  toJSON WorkspaceSymbol                     = JString "workspace/symbol"
  toJSON WorkspaceExecuteCommand             = JString "workspace/executeCommand"
  toJSON WorkspaceWillCreateFiles            = JString "workspace/willCreateFiles"
  toJSON TextDocumentDidOpen                 = JString "textDocument/didOpen"
  toJSON TextDocumentDidChange               = JString "textDocument/didChange"
  toJSON TextDocumentWillSave                = JString "textDocument/willSave"
  toJSON TextDocumentWillSaveWaitUntil       = JString "textDocument/willSaveWaitUntil"
  toJSON TextDocumentDidSave                 = JString "textDocument/didSave"
  toJSON TextDocumentDidClose                = JString "textDocument/didClose"
  toJSON CompletionItemResolve               = JString "completionItem/resolve"
  toJSON TextDocumentHover                   = JString "textDocument/hover"
  toJSON TextDocumentSignatureHelp           = JString "textDocument/signatureHelp"
  toJSON TextDocumentDeclaration             = JString "textDocument/declaration"
  toJSON TextDocumentDefinition              = JString "textDocument/definition"
  toJSON TextDocumentTypeDefinition          = JString "textDocument/typeDefinition"
  toJSON TextDocumentImplementation          = JString "textDocument/implementation"
  toJSON TextDocumentReferences              = JString "textDocument/references"
  toJSON TextDocumentDocumentHighlight       = JString "textDocument/documentHighlight"
  toJSON TextDocumentDocumentSymbol          = JString "textDocument/documentSymbol"
  toJSON TextDocumentCodeAction              = JString "textDocument/codeAction"
  toJSON CodeActionResolve                   = JString "codeAction/resolve"
  toJSON TextDocumentCodeLens                = JString "textDocument/codeLens"
  toJSON CodeLensResolve                     = JString "codeLens/resolve"
  toJSON TextDocumentDocumentLink            = JString "textDocument/documentLink"
  toJSON DocumentLinkResolve                 = JString "documentLink/resolve"
  toJSON TextDocumentDocumentColor           = JString "textDocument/documentColor"
  toJSON TextDocumentFormatting              = JString "textDocument/formatting"
  toJSON TextDocumentRangeFormatting         = JString "textDocument/rangeFormatting"
  toJSON TextDocumentOnTypeFormatting        = JString "textDocument/onTypeFormatting"
  toJSON TextDocumentRename                  = JString "textDocument/rename"
  toJSON TextDocumentPrepareRename           = JString "textDocument/prepareRename"
  toJSON TextDocumentFoldingRange            = JString "textDocument/foldingRange"
  toJSON TextDocumentSelectionRange          = JString "textDocument/selectionRange"
  toJSON TextDocumentPrepareCallHierarchy    = JString "textDocument/prepareCallHierarchy"
  toJSON CallHierarchyIncomingCalls          = JString "callHierarchy/incomingCalls"
  toJSON CallHierarchyOutgoingCalls          = JString "callHierarchy/outgoingCalls"
  toJSON TextDocumentSemanticTokensFull      = JString "textDocument/semanticTokens/full"
  toJSON TextDocumentSemanticTokensFullDelta = JString "textDocument/semanticTokens/full/delta"
  toJSON TextDocumentSemanticTokensRange     = JString "textDocument/semanticTokens/range"
  toJSON WorkspaceSemanticTokensRefresh      = JString "workspace/semanticTokens/refresh"
  toJSON TextDocumentLinkedEditingRange      = JString "textDocument/linkedEditingRange"
  toJSON TextDocumentMoniker                 = JString "textDocument/moniker"
  toJSON LogTrace                            = JString "$/logTrace"
  toJSON WindowShowMessage                   = JString "window/showMessage"
  toJSON WindowShowMessageRequest            = JString "window/showMessageRequest"
  toJSON WindowShowDocument                  = JString "window/showDocument"
  toJSON WindowLogMessage                    = JString "window/logMessage"
  toJSON WindowWorkDoneProgressCreate        = JString "window/workDoneProgress/create"
  toJSON TelemetryEvent                      = JString "telemetry/event"
  toJSON ClientRegisterCapability            = JString "client/registerCapability"
  toJSON ClientUnregisterCapability          = JString "client/unregisterCapability"
  toJSON WorkspaceWorkspaceFolders           = JString "workspace/workspaceFolders"
  toJSON WorkspaceConfiguration              = JString "workspace/configuration"
  toJSON WorkspaceApplyEdit                  = JString "workspace/applyEdit"
  toJSON TextDocumentPublishDiagnostics      = JString "textDocument/publishDiagnostics"
  toJSON TextDocumentCompletion              = JString "textDocument/completion"
  toJSON WorkspaceCodeLensRefresh            = JString "workspace/codeLens/refresh"
  toJSON CancelRequest                       = JString "$/cancelRequest"
  toJSON Progress                            = JString "$/progress"

export
FromJSON (Method Client Notification) where
  fromJSON (JString "initialized")                         = pure Initialized
  fromJSON (JString "exit")                                = pure Exit
  fromJSON (JString "$/setTrace")                          = pure SetTrace
  fromJSON (JString "window/workDoneProgress/cancel")      = pure WindowWorkDoneProgressCancel
  fromJSON (JString "workspace/didChangeWorkspaceFolders") = pure WorkspaceDidChangeWorkspaceFolders
  fromJSON (JString "workspace/didChangeConfiguration")    = pure WorkspaceDidChangeConfiguration
  fromJSON (JString "workspace/didChangeWatchedFiles")     = pure WorkspaceDidChangeWatchedFiles
  fromJSON (JString "textDocument/didOpen")                = pure TextDocumentDidOpen
  fromJSON (JString "textDocument/didChange")              = pure TextDocumentDidChange
  fromJSON (JString "textDocument/willSave")               = pure TextDocumentWillSave
  fromJSON (JString "textDocument/didSave")                = pure TextDocumentDidSave
  fromJSON (JString "textDocument/didClose")               = pure TextDocumentDidClose
  fromJSON (JString "$/cancelRequest")                     = pure CancelRequest
  fromJSON (JString "$/progress")                          = pure Progress
  fromJSON _ = neutral

export
FromJSON (Method Client Request) where
  fromJSON (JString "initialize")                             = pure Initialize
  fromJSON (JString "shutdown")                               = pure Shutdown
  fromJSON (JString "workspace/symbol")                       = pure WorkspaceSymbol
  fromJSON (JString "workspace/executeCommand")               = pure WorkspaceExecuteCommand
  fromJSON (JString "workspace/willCreateFiles")              = pure WorkspaceWillCreateFiles
  fromJSON (JString "textDocument/willSaveWaitUntil")         = pure TextDocumentWillSaveWaitUntil
  fromJSON (JString "textDocument/completion")                = pure TextDocumentCompletion
  fromJSON (JString "completionItem/resolve")                 = pure CompletionItemResolve
  fromJSON (JString "textDocument/hover")                     = pure TextDocumentHover
  fromJSON (JString "textDocument/signatureHelp")             = pure TextDocumentSignatureHelp
  fromJSON (JString "textDocument/declaration")               = pure TextDocumentDeclaration
  fromJSON (JString "textDocument/definition")                = pure TextDocumentDefinition
  fromJSON (JString "textDocument/typeDefinition")            = pure TextDocumentTypeDefinition
  fromJSON (JString "textDocument/implementation")            = pure TextDocumentImplementation
  fromJSON (JString "textDocument/references")                = pure TextDocumentReferences
  fromJSON (JString "textDocument/documentHighlight")         = pure TextDocumentDocumentHighlight
  fromJSON (JString "textDocument/documentSymbol")            = pure TextDocumentDocumentSymbol
  fromJSON (JString "textDocument/codeAction")                = pure TextDocumentCodeAction
  fromJSON (JString "codeAction/resolve")                     = pure CodeActionResolve
  fromJSON (JString "textDocument/codeLens")                  = pure TextDocumentCodeLens
  fromJSON (JString "codeLens/resolve")                       = pure CodeLensResolve
  fromJSON (JString "textDocument/documentLink")              = pure TextDocumentDocumentLink
  fromJSON (JString "documentLink/resolve")                   = pure DocumentLinkResolve
  fromJSON (JString "textDocument/documentColor")             = pure TextDocumentDocumentColor
  fromJSON (JString "textDocument/formatting")                = pure TextDocumentFormatting
  fromJSON (JString "textDocument/rangeFormatting")           = pure TextDocumentRangeFormatting
  fromJSON (JString "textDocument/onTypeFormatting")          = pure TextDocumentOnTypeFormatting
  fromJSON (JString "textDocument/rename")                    = pure TextDocumentRename
  fromJSON (JString "textDocument/prepareRename")             = pure TextDocumentPrepareRename
  fromJSON (JString "textDocument/foldingRange")              = pure TextDocumentFoldingRange
  fromJSON (JString "textDocument/selectionRange")            = pure TextDocumentSelectionRange
  fromJSON (JString "textDocument/prepareCallHierarchy")      = pure TextDocumentPrepareCallHierarchy
  fromJSON (JString "callHierarchy/incomingCalls")            = pure CallHierarchyIncomingCalls
  fromJSON (JString "callHierarchy/outgoingCalls")            = pure CallHierarchyOutgoingCalls
  fromJSON (JString "textDocument/semanticTokens/full")       = pure TextDocumentSemanticTokensFull
  fromJSON (JString "textDocument/semanticTokens/full/delta") = pure TextDocumentSemanticTokensFullDelta
  fromJSON (JString "textDocument/semanticTokens/range")      = pure TextDocumentSemanticTokensRange
  fromJSON (JString "workspace/semanticTokens/refresh")       = pure WorkspaceSemanticTokensRefresh
  fromJSON (JString "textDocument/linkedEditingRange")        = pure TextDocumentLinkedEditingRange
  fromJSON (JString "textDocument/moniker")                   = pure TextDocumentMoniker
  fromJSON _ = neutral

export
FromJSON (Method Server Notification) where
  fromJSON (JString "$/logTrace")                      = pure LogTrace
  fromJSON (JString "window/showMessage")              = pure WindowShowMessage
  fromJSON (JString "window/logMessage")               = pure WindowLogMessage
  fromJSON (JString "telemetry/event")                 = pure TelemetryEvent
  fromJSON (JString "textDocument/publishDiagnostics") = pure TextDocumentPublishDiagnostics
  fromJSON (JString "$/cancelRequest")                 = pure CancelRequest
  fromJSON (JString "$/progress")                      = pure Progress
  fromJSON _ = neutral

export
FromJSON (Method Server Request) where
  fromJSON (JString "window/showMessageRequest")      = pure WindowShowMessageRequest
  fromJSON (JString "window/showDocument")            = pure WindowShowDocument
  fromJSON (JString "window/workDoneProgress/create") = pure WindowWorkDoneProgressCreate
  fromJSON (JString "client/registerCapability")      = pure ClientRegisterCapability
  fromJSON (JString "client/unregisterCapability")    = pure ClientUnregisterCapability
  fromJSON (JString "workspace/workspaceFolders")     = pure WorkspaceWorkspaceFolders
  fromJSON (JString "workspace/configuration")        = pure WorkspaceConfiguration
  fromJSON (JString "workspace/applyEdit")            = pure WorkspaceApplyEdit
  fromJSON (JString "workspace/codeLens/refresh")     = pure WorkspaceCodeLensRefresh
  fromJSON _ = neutral

export
FromJSON (from ** Method from Notification) where
  fromJSON arg =
    (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** meth))
      <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** meth))

export
FromJSON (from ** Method from Request) where
  fromJSON arg =
    (fromJSON arg >>= \meth : Method Client Request => pure (_ ** meth))
      <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** meth))

export
FromJSON (from ** type ** Method from type) where
  fromJSON arg =
    (fromJSON arg >>= \meth : Method Client Notification => pure (_ ** _ ** meth))
      <|> (fromJSON arg >>= \meth : Method Client Request => pure (_ ** _ ** meth))
      <|> (fromJSON arg >>= \meth : Method Server Notification => pure (_ ** _ ** meth))
      <|> (fromJSON arg >>= \meth : Method Server Request => pure (_ ** _ ** meth))


text:
module Sixel.Allocator

import System.FFI

import Sixel.Library
import Sixel.Symbols

%default total

public export
MAlloc : Type
MAlloc = (size : Int) -> PrimIO AnyPtr

public export
CAlloc : Type
CAlloc = (elems : Int) -> (size : Int) -> PrimIO AnyPtr

public export
ReAlloc : Type
ReAlloc = (ptr : AnyPtr) -> (size : Int) -> PrimIO AnyPtr

public export
Free : Type
Free = (ptr : AnyPtr) -> PrimIO ()

public export
PrimAllocator : Type
PrimAllocator = AnyPtr

%foreign (sixelutils "sixel_utils_allocator_null")
sixel_utils_allocator_null : PrimAllocator

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

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

%foreign (c "malloc")
c_malloc : (size : Int) -> PrimIO AnyPtr

%foreign (c "calloc")
c_calloc : (elems : Int) -> (size : Int) -> PrimIO AnyPtr

%foreign (c "realloc")
c_realloc : (ptr : AnyPtr) -> (elems : Int) -> PrimIO AnyPtr

%foreign (c "free")
c_free : (ptr : AnyPtr) -> PrimIO ()

%foreign (sixel "sixel_allocator_new")
sixel_allocator_new : Ptr AnyPtr -> MAlloc -> CAlloc -> ReAlloc -> Free -> PrimIO Int

%foreign (sixel "sixel_allocator_unref")
sixel_allocator_destroy : AnyPtr -> PrimIO ()

%foreign (sixel "sixel_allocator_ref")
sixel_allocator_ref : PrimAllocator -> ()

%foreign (sixel "sixel_allocator_unref")
sixel_allocator_unref : PrimAllocator -> ()

%foreign (sixel "sixel_allocator_free")
sixel_allocator_free : PrimAllocator -> (ptr : AnyPtr) -> PrimIO ()

%foreign (sixel "sixel_allocator_malloc")
sixel_allocator_malloc : PrimAllocator -> (size : Int) -> PrimIO AnyPtr

%foreign (sixel "sixel_allocator_calloc")
sixel_allocator_calloc : PrimAllocator -> (elems : Int) -> (size : Int) -> PrimIO AnyPtr

%foreign (sixel "sixel_allocator_realloc")
sixel_allocator_realloc : PrimAllocator -> (ptr : AnyPtr) -> (size : Int) -> PrimIO AnyPtr

export
data Allocator : (0 n : Nat) -> Type where
  NullAllocator  : Allocator n -- for the sake of serving as a default
  PointAllocator : PrimAllocator -> Allocator Z
  RootAllocator  : Allocator n -> Allocator (S n)

public export
ConcreteAllocator : Allocator n -> Type
ConcreteAllocator NullAllocator         = Void
ConcreteAllocator (PointAllocator _)    = ()
ConcreteAllocator (RootAllocator alloc) = ConcreteAllocator alloc

public export
getNullAllocator : (n : Nat) -> Allocator n
getNullAllocator _ = NullAllocator

export
MkAllocator :
  {default c_malloc malloc : MAlloc} ->    -- NULL => malloc
  {default c_calloc calloc : CAlloc} ->    -- NULL => calloc
  {default c_realloc realloc : ReAlloc} -> -- NULL => realloc
  {default c_free free : Free} ->          -- NULL => free
  IO (Either Status (Allocator Z))
MkAllocator {malloc} {calloc} {realloc} {free} = do
  ppalloc <- fromPrim sixel_utils_allocator_ptr_new
  status  <- MkStatus <$> fromPrim (sixel_allocator_new ppalloc malloc calloc realloc free)
  pure $ if succeeded status
            then Right (PointAllocator $ sixel_utils_allocator_ptr_deref ppalloc)
            else Left status

export
ref : (alloc : Allocator n) -> {auto 0 ok : ConcreteAllocator alloc} -> IO (Allocator (S n))
ref (RootAllocator alloc)         = RootAllocator <$> ref alloc
ref alloc@(PointAllocator palloc) = let _ = sixel_allocator_ref palloc in pure $ RootAllocator alloc

export
unref : (alloc : Allocator (S n)) -> {auto 0 ok : ConcreteAllocator alloc} -> IO (Allocator n)
unref (RootAllocator alloc@(RootAllocator _))       = RootAllocator <$> unref alloc
unref (RootAllocator alloc@(PointAllocator palloc)) = let _ = sixel_allocator_unref palloc in pure alloc

export
destroy : (alloc : Allocator Z) -> {auto 0 ok : ConcreteAllocator alloc} -> IO ()
destroy (PointAllocator palloc) = fromPrim $ sixel_allocator_destroy palloc

export
toPrim : Allocator n -> PrimAllocator
toPrim NullAllocator           = sixel_utils_allocator_null
toPrim (PointAllocator palloc) = palloc
toPrim (RootAllocator alloc)   = toPrim alloc

export %inline
malloc : ConcreteAllocator alloc => (alloc : Allocator n) -> (size : Int) -> IO AnyPtr
malloc alloc size = fromPrim $ sixel_allocator_malloc (toPrim alloc) size

export %inline
calloc : ConcreteAllocator alloc => (alloc : Allocator n) -> (elems : Int) -> (size : Int) -> IO AnyPtr
calloc alloc elems size = fromPrim $ sixel_allocator_calloc (toPrim alloc) elems size

export %inline
realloc : ConcreteAllocator alloc => (alloc : Allocator n) -> (ptr : AnyPtr) -> (size : Int) -> IO AnyPtr
realloc alloc ptr size = fromPrim $ sixel_allocator_realloc (toPrim alloc) ptr size

export %inline
free : ConcreteAllocator alloc => (alloc : Allocator n) -> (ptr : AnyPtr) -> IO ()
free alloc ptr = fromPrim $ sixel_allocator_free (toPrim alloc) ptr

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module SkepticLang.JSONUtils

import Language.JSON

%access public export

||| Gets the value of an attribute of a JSON object.
|||
||| @json the JSON object
||| @key  the name of the attribute
getObjAttr : (json : JSON) -> (key : String) -> Maybe JSON
getObjAttr (JObject xs) key = getObjAttr' xs key where
  getObjAttr' : (json : List (String, JSON)) -> (key : String) -> Maybe JSON
  getObjAttr' ((a, b) :: xs) key = if a == key then Just b else getObjAttr' xs key
  getObjAttr' [] _ = Nothing
getObjAttr _ _  = Nothing

max_stars_repo_name: sr-lab/skeptic-lang

max_issues_repo_name: sr-lab/skeptic-lang

max_forks_repo_name: sr-lab/skeptic-lang


text:
module Effect.Random

import Effects

data Random : Effect where
     getRandom : { Integer } Random Integer
     setSeed   : Integer -> { Integer } Random ()

using (m : Type -> Type)
  instance Handler Random m where
     handle seed getRandom k
              = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in
                    k seed' seed'
     handle seed (setSeed n) k = k () n

RND : EFFECT
RND = MkEff Integer Random

rndInt : Integer -> Integer -> { [RND] } Eff m Integer
rndInt lower upper = do v <- getRandom
                        return (v `prim__sremBigInt` (upper - lower) + lower)

srand : Integer -> { [RND] } Eff m ()
srand n = setSeed n

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 2, Stack part

import Data.Vect

-- check that all functions are total
%default total

data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd () height (S height)
  Pop : StackCmd Integer (S height) height
  Top : StackCmd Integer (S height) (S height)
  Pure : ty -> StackCmd ty s s
  (>>=) : StackCmd a s1 s2 ->
          (a -> StackCmd b s2 s3) ->
          StackCmd b s1 s3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight ->
           (ty, Vect outHeight Integer)
runStack stk (Push x) = ((), x :: stk)
runStack (x :: xs) Pop = (x, xs)
runStack (x :: xs) Top = (x, x :: xs)
runStack stk (Pure x) = (x, stk)
runStack stk (x >>= f)
  = let (res, stk') = runStack stk x in
      runStack stk' (f res)

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

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push $ val1 + val2

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Stuff

foo : Int -> Maybe Int
foo 0 = Nothing
foo x = Just (prim__mul_Int x 2)

testLet : Int -> Int
testLet x = let y = prim__mul_Int x 2
                Just ans = foo y
                     | Nothing => 99
                z = prim__mul_Int ans 2
              in z


text:
module Libra

import public Libra.Parser
import public Libra.Data
import public Libra.Constants

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module Main

import System

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

guess : (target : Nat) -> IO ()
guess target = do putStrLn "Input guess: "
                  Just guessResult <- readNumber
                  | Nothing => do putStrLn "Invalid input"
                                  guess target
                  (case compare guessResult target of
                        LT => do putStrLn "Guess is too low"
                                 guess target
                        EQ => do putStrLn "Guess is correct!"
                        GT => do putStrLn "Guess is to high"
                                 guess target)

altGuess : (target : Nat) -> (guesses : Nat) -> IO ()
altGuess target guesses = do putStrLn ((show guesses) ++ " guesses thus far")
                             putStrLn "Input guess: "
                             Just guessResult <- readNumber
                             | Nothing => do putStrLn "Invalid input"
                                             altGuess target guesses
                             (case compare guessResult target of
                                   LT => do putStrLn "Guess is too low"
                                            altGuess target (guesses + 1)
                                   EQ => do putStrLn "Guess is correct!"
                                   GT => do putStrLn "Guess is too high"
                                            altGuess target (guesses + 1))

main : IO ()
main = do t <- time
          guess (cast (mod t 100))

replWithAlt : (state : a) -> (prompt : String) ->
           (onInput: a -> String -> Maybe(String, a)) -> IO ()
replWithAlt state prompt onInput = do putStrLn prompt
                                      input <- getLine
                                      (case onInput state input of
                                            Nothing => pure ()
                                            (Just (output, resultState)) => do putStrLn output
                                                                               replWithAlt resultState prompt onInput)

replAlt : (prompt : String) -> (onInput : String -> String) -> IO ()
replAlt prompt onInput = replWithAlt () prompt (\st, str => Just (onInput str, ()))


text:
||| A Shape
data Shape = ||| A triangle
             Triangle Double Double
           | ||| A rectangle
             Rectangle Double Double
           | ||| A circle
             Circle Double

%name Shape shape, shape1, shape2

total area : Shape -> Double
area (Triangle x y) = 0.5 * x * y
area (Rectangle x y) = x * y
area (Circle x) = pi * x * x

data Picture = ||| A primitive shape
               Primitive Shape
             | ||| A combination of pictures
               Combine Picture Picture
             | ||| A rotated picture
               Rotate Double Picture
             | ||| A translated picture
               Translate Double Double Picture

%name Picture pic, pic1, pic2

--- %name directives are _awesome_
pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
                      (Combine (Translate 35 5 circle)
                               (Rotate 5 (Translate 15 25 triangle)))

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Gspider.File.SystemLoading

import Core

%access private

||| Unescapes a system character string if necessary.
|||
||| @s the system character string to unescape
unescapeSystemChar : (s : String) -> Maybe Char
unescapeSystemChar "SPACE" = Just ' '
unescapeSystemChar s = head' (unpack s)

||| Loads a system from a file.
|||
||| @path the path to the file to load
export
loadSystem : (path : String) -> IO (Maybe System)
loadSystem path =
  do
    txt <- readFile path
    case txt of
      Left _ => pure Nothing -- File read failure.
      Right txt' =>
        let rawChars = split (== ' ') txt'
            chars = map unescapeSystemChar rawChars in
            pure (Just (catMaybes chars))

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


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

||| Common enumerated types used.
module GRL.Common

import public Decidable.Equality

%default total
%access public export

data Importance = HIGH | MEDIUM | LOW | NO

-- data SValue = DENIED | WEAKDEN | WEAKSATIS | SATISFIED | CONFLICT | UNKNOWN | NONE | UNDECIDED
namespace Qualiative
  data SValue : Type where
    ||| The intentional element or indicator is sufficiently dissatisfied.
    DENIED : SValue
    ||| The intentional element is partially dissatisfied.
    WEAKDEN : SValue
    ||| The intentional element or indicator is partially satisfied.
    WEAKSATIS : SValue
    ||| The intentional element is sufficiently satisfied.
    SATISFIED : SValue
    ||| There are arguments strongly in favour and strongly against
    ||| the satisfaction of the intentional element.
    CONFLICT : SValue
    ||| The satisfaction level of the intentional element is unknown.
    UNDECIDED : SValue
    ||| The intentional element or indicator is neither satisfied nor dissatisfied.
    NONE : SValue

export
invertEval : SValue -> SValue
invertEval DENIED = SATISFIED
invertEval WEAKDEN = WEAKSATIS
invertEval WEAKSATIS = WEAKDEN
invertEval SATISFIED = DENIED
invertEval x         = x

--  data CValue = MAKES | HELPS | SOMEPOS | UNKNOWN | SOMENEG | BREAK | HURTS

namespace Contributions
  data CValue : Type where
    ||| The contribution is positive and sufficient.
    MAKES : CValue
    ||| The contribution is positive but not sufficient.
    HELPS : CValue
    ||| The contribution is positive, but the extent of the contribution is unknown.
    SOMEPOS : CValue
    ||| There is some contribution, but the extent and the degree (positive or negative) of the contribution is unknown.
    UNKNOWN : CValue
    ||| The contribution is negative, but the extent of the contribution is unknown.
    SOMENEG : CValue
    ||| The contribution of the contributing element is negative and sufficient.
    BREAK : CValue
    ||| The contribution is negative but not sufficient.
    HURTS : CValue

export
invertContrib : CValue -> CValue
invertContrib MAKES = HURTS
invertContrib HELPS = BREAK
invertContrib SOMEPOS = SOMENEG
invertContrib UNKNOWN = UNKNOWN
invertContrib SOMENEG = SOMEPOS
invertContrib BREAK = HELPS
invertContrib HURTS = MAKES

-- ------------------------------------------------------------------- [ Types ]

-- data GElemTy = GOALty | SOFTty | TASKty | RESty
-- data GIntentTy  = IMPACTty | AFFECTSty
-- data GStructTy  = ANDty | XORty | IORty | NOTty

data GTy = ELEM | INTENT | STRUCT

data GElemTy : Type where
    ||| A (hard) Goal is a condition or state of affairs in the
    ||| world that the stakeholders would like to achieve.
    |||
    ||| How the goal is to be achieved is not specified, allowing
    ||| alternatives to be considered. A goal can be either a business
    ||| goal or a system goal. A business goal expresses goals regarding
    ||| the business or state of the business affairs the individual or
    ||| organization wishes to achieve. A system goal expresses goals
    ||| the target system should achieve and generally describes the
    ||| functional requirements of the target information system.
    |||
    GOALty : GElemTy

    ||| Softgoals are often used to describe qualities and
    ||| non-functional aspects such as security, robustness,
    ||| performance, usability, etc.
    |||
    ||| A Softgoal is a condition or state of affairs in the world that
    ||| the actor would like to achieve, but unlike in the concept of
    ||| (hard) goal, there are no clear-cut criteria for whether the
    ||| condition is achieved, and it is up to subjective judgement and
    ||| interpretation of the modeller to judge whether a particular
    ||| state of affairs in fact achieves sufficiently the stated
    ||| softgoal.
    |||
    SOFTty : GElemTy

    ||| a Task specifies a particular way of doing something.
    |||
    ||| When a task is part of the decomposition of a (higher-level)
    ||| task, this restricts the higher-level task to that particular
    ||| course of action. Tasks can also be seen as the solutions in the
    ||| target system, which will address (or operationalize) goals and
    ||| softgoals. These solutions provide operations, processes, data
    ||| representations, structuring, constraints and agents in the
    ||| target system to meet the needs stated in the goals and
    ||| softgoals.
    |||
    TASKty : GElemTy

    ||| A Resource is a physical or informational entity, for which the
    ||| main concern is whether it is available.
    |||
    RESty : GElemTy

data GIntentTy : Type where
  ||| A Contribution defines the level of impact that the
  ||| satisfaction of a source intentional element or indicator has on
  ||| the satisfaction of a destination intentional element.
  IMPACTSty : GIntentTy
  |||  A correlation link emphasizes side-effects between intentional
  ||| elements in different categories or actor definitions.
  AFFECTSty : GIntentTy

data GStructTy : Type where
  ||| The AND Decomposition link enables the hierarchical
  ||| decomposition of a target intentional element by a source
  ||| element. A target intentional element can be decomposed into
  ||| many source intentional elements using as many decomposition
  ||| links. All of the source intentional elements are necessary for
  ||| the target intentional element to be satisfied.
  |||
  ANDty : GStructTy
  ||| The XOR Decomposition link enables the description of
  ||| alternative means of satisfying a target intentional element:
  ||| Mutually exclusive. The satisfaction of one and only one of the
  ||| sub-intentional elements is necessary to achieve the target.
  |||
  XORty : GStructTy
  ||| The IOR Decomposition link enables the description of
  ||| alternative means of satisfying a target intentional element:
  ||| Not mutually exclusive. The satisfaction of one of the
  ||| sub-intentional elements is sufficient to achieve the target,
  ||| but many sub-intentional elements can be satisfied.
  |||
  IORty : GStructTy

-- -------------------------------------------------------------------- [ Show ]

implementation Show GElemTy where
  show GOALty = "Goal"
  show SOFTty = "Soft"
  show TASKty = "Task"
  show RESty  = "Res"

implementation Show GIntentTy where
  show IMPACTSty = "CONTRIBUTION"
  show AFFECTSty = "CORRELATION"

implementation Show GStructTy where
  show ANDty  = "ANDTy"
  show XORty  = "XORTy"
  show IORty  = "IORTy"

implementation Show GTy where
  show ELEM   = "ELEM"
  show INTENT = "INTENT"
  show STRUCT = "STRUCT"

-- ---------------------------------------------------------------------- [ Eq ]

implementation Eq GElemTy where
  (==) GOALty GOALty = True
  (==) SOFTty SOFTty = True
  (==) TASKty TASKty = True
  (==) RESty  RESty  = True
  (==) _        _    = False

implementation Eq GIntentTy where
  (==) IMPACTSty IMPACTSty = True
  (==) AFFECTSty AFFECTSty = True
  (==) _         _         = False

implementation Eq GStructTy where
  (==) ANDty ANDty = True
  (==) XORty XORty = True
  (==) IORty IORty = True
  (==) _     _     = False

implementation Eq GTy where
  (==) ELEM   ELEM   = True
  (==) INTENT INTENT = True
  (==) STRUCT STRUCT = True
  (==) _      _      = False

-- --------------------------------------------------------------- [ Orderable ]
implementation Ord GTy where
  compare ELEM   ELEM   = EQ
  compare INTENT INTENT = EQ
  compare STRUCT STRUCT = EQ
  compare ELEM   _      = LT
  compare _      ELEM   = GT
  compare INTENT _      = LT
  compare _      INTENT = GT
  compare STRUCT _      = LT
  compare _      STRUCT = GT

-- -------------------------------------------------------------------- [ Show ]

implementation Show SValue where
  show SATISFIED = "SATISFIED"
  show WEAKSATIS = "WEAKSATIS"
  show WEAKDEN   = "WEAKDEN"
  show DENIED    = "DENIED"
  show CONFLICT  = "CONFLICT"
  show UNDECIDED = "UNDECIDED"
  show NONE      = "NONE"

implementation Eq SValue where
  (==) SATISFIED SATISFIED = True
  (==) WEAKSATIS WEAKSATIS = True
  (==) WEAKDEN   WEAKDEN   = True
  (==) DENIED    DENIED    = True
  (==) CONFLICT  CONFLICT  = True
  (==) UNDECIDED UNDECIDED = True
  (==) NONE      NONE      = True
  (==) _         _         = False

implementation Show CValue where
  show MAKES   = "MAKES"
  show HELPS   = "HELPS"
  show SOMEPOS = "SOMEPOS"
  show UNKNOWN = "UNKNOWN"
  show SOMENEG = "SOMENEG"
  show HURTS   = "HURTS"
  show BREAK   = "BREAKS"

implementation Eq CValue where
  (==) MAKES   MAKES   = True
  (==) HELPS   HELPS   = True
  (==) SOMEPOS SOMEPOS = True
  (==) UNKNOWN UNKNOWN = True
  (==) SOMENEG SOMENEG = True
  (==) HURTS   HURTS   = True
  (==) BREAK   BREAK   = True
  (==) _       _       = False

implementation Cast CValue String where
  cast MAKES   = "MAKES"
  cast HELPS   = "HELPS"
  cast SOMEPOS = "SOMEPOS"
  cast UNKNOWN = "UNKNOWN"
  cast SOMENEG = "SOMENEG"
  cast HURTS   = "HURTS"
  cast BREAK   = "BREAKS"

implementation Cast SValue String where
  cast SATISFIED = "SATISFIED"
  cast WEAKSATIS = "WEAKSATIS"
  cast WEAKDEN   = "WEAKDEN"
  cast DENIED    = "DENIED"
  cast CONFLICT  = "CONFLICT"
  cast UNDECIDED = "UNDECIDED"
  cast NONE      = "NONE"

implementation Cast String CValue where
  cast "MAKES"   = MAKES
  cast "HELPS"   = HELPS
  cast "SOMEPOS" = SOMEPOS
  cast "UNKNOWN" = UNKNOWN
  cast "SOMENEG" = SOMENEG
  cast "HURTS"   = HURTS
  cast "BREAKS"  = BREAK
  cast _         = UNKNOWN

implementation Cast String SValue where
  cast "SATISFIED"   = SATISFIED
  cast "WEAKSATIS"   = WEAKSATIS
  cast "WEAKDEN"     = WEAKDEN
  cast "DENIED"      = DENIED
  cast "CONFLICT"    = CONFLICT
  cast "UNDECIDED"   = UNDECIDED
  cast "NONE"        = NONE
  cast _             = NONE

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Conway.Parse

import Conway
import Control.Comonad.Store.Representable
import Data.Functor.Representable
import Data.List
import Data.String
import Data.Vect
import Data.Vect.Extra

%default total

parseLine : {n : Nat} -> String -> Maybe (List (Fin n))
parseLine str = findIndices (== '#') <$> toVect n (unpack str)

export
parseGrid : String -> Maybe (DPair (Nat, Nat) (\(n, m) => Grid n m Bool))
parseGrid text = do
  (S n ** rows) <- pure $ asVect (lines text) | _ => Nothing
  S m <- pure $ length (head rows) | _ => Nothing
  coords' <- traverse (parseLine {n = S m}) rows
  let coords = foldMap id $ mapWithIndex (\i, c => (i,) <$> c) coords'
  pure $ ((S n, S m) ** store @{Compose} (`elem` coords) (0, FZ))

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life