text:
||| Definitions of messages and associated payloads and responses.
|||
||| (C) The Idris Community, 2021
module Language.LSP.Message.Message

import Data.OneOf
import Language.JSON
import Language.LSP.Message.CallHierarchy
import Language.LSP.Message.Cancel
import Language.LSP.Message.CodeAction
import Language.LSP.Message.CodeLens
import Language.LSP.Message.Command
import Language.LSP.Message.Completion
import Language.LSP.Message.Declaration
import Language.LSP.Message.Definition
import Language.LSP.Message.Derive
import Language.LSP.Message.Diagnostics
import Language.LSP.Message.DocumentColor
import Language.LSP.Message.DocumentFormatting
import Language.LSP.Message.DocumentHighlight
import Language.LSP.Message.DocumentLink
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.FoldingRange
import Language.LSP.Message.Hover
import Language.LSP.Message.Implementation
import Language.LSP.Message.Initialize
import Language.LSP.Message.LinkedEditingRange
import Language.LSP.Message.Location
import Language.LSP.Message.Method
import Language.LSP.Message.Moniker
import Language.LSP.Message.Progress
import Language.LSP.Message.References
import Language.LSP.Message.Registration
import Language.LSP.Message.Rename
import Language.LSP.Message.SelectionRange
import Language.LSP.Message.SemanticTokens
import Language.LSP.Message.SignatureHelp
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Trace
import Language.LSP.Message.Utils
import Language.LSP.Message.Window
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

||| Maps the parameters associated to each type of method.
public export
MessageParams : (method : Method from type) -> Type
MessageParams Initialize                          = InitializeParams
MessageParams Initialized                         = InitializedParams
MessageParams Shutdown                            = Maybe Null
MessageParams Exit                                = Maybe Null
MessageParams SetTrace                            = SetTraceParams
MessageParams WindowWorkDoneProgressCancel        = WorkDoneProgressCancelParams
MessageParams WorkspaceDidChangeWorkspaceFolders  = DidChangeWorkspaceFoldersParams
MessageParams WorkspaceDidChangeConfiguration     = DidChangeConfigurationParams
MessageParams WorkspaceDidChangeWatchedFiles      = DidChangeWatchedFilesParams
MessageParams WorkspaceSymbol                     = WorkspaceSymbolParams
MessageParams WorkspaceExecuteCommand             = ExecuteCommandParams
MessageParams WorkspaceWillCreateFiles            = CreateFilesParams
MessageParams TextDocumentDidOpen                 = DidOpenTextDocumentParams
MessageParams TextDocumentDidChange               = DidChangeTextDocumentParams
MessageParams TextDocumentWillSave                = WillSaveTextDocumentParams
MessageParams TextDocumentWillSaveWaitUntil       = WillSaveTextDocumentParams
MessageParams TextDocumentDidSave                 = DidSaveTextDocumentParams
MessageParams TextDocumentDidClose                = DidCloseTextDocumentParams
MessageParams CompletionItemResolve               = CompletionItem
MessageParams TextDocumentHover                   = HoverParams
MessageParams TextDocumentSignatureHelp           = SignatureHelpParams
MessageParams TextDocumentDeclaration             = DeclarationParams
MessageParams TextDocumentDefinition              = DefinitionParams
MessageParams TextDocumentTypeDefinition          = TypeDefinitionParams
MessageParams TextDocumentImplementation          = ImplementationParams
MessageParams TextDocumentReferences              = ReferenceParams
MessageParams TextDocumentDocumentHighlight       = DocumentHighlightParams
MessageParams TextDocumentDocumentSymbol          = DocumentSymbolParams
MessageParams TextDocumentCodeAction              = CodeActionParams
MessageParams CodeActionResolve                   = CodeAction
MessageParams TextDocumentCodeLens                = CodeLensParams
MessageParams CodeLensResolve                     = CodeLens
MessageParams TextDocumentDocumentLink            = DocumentLinkParams
MessageParams DocumentLinkResolve                 = DocumentLink
MessageParams TextDocumentDocumentColor           = DocumentColorParams
MessageParams TextDocumentFormatting              = DocumentFormattingParams
MessageParams TextDocumentRangeFormatting         = DocumentRangeFormattingParams
MessageParams TextDocumentOnTypeFormatting        = DocumentOnTypeFormattingParams
MessageParams TextDocumentRename                  = RenameParams
MessageParams TextDocumentPrepareRename           = PrepareRenameParams
MessageParams TextDocumentFoldingRange            = FoldingRangeParams
MessageParams TextDocumentSelectionRange          = SelectionRangeParams
MessageParams TextDocumentPrepareCallHierarchy    = CallHierarchyParams
MessageParams CallHierarchyIncomingCalls          = CallHierarchyIncomingCallsParams
MessageParams CallHierarchyOutgoingCalls          = CallHierarchyOutgoingCallsParams
MessageParams TextDocumentSemanticTokensFull      = SemanticTokensParams
MessageParams TextDocumentSemanticTokensFullDelta = SemanticTokensDeltaParams
MessageParams TextDocumentSemanticTokensRange     = SemanticTokensRangeParams
MessageParams WorkspaceSemanticTokensRefresh      = Maybe Null
MessageParams TextDocumentLinkedEditingRange      = LinkedEditingRangeParams
MessageParams TextDocumentMoniker                 = MonikerParams
MessageParams LogTrace                            = LogTraceParams
MessageParams WindowShowMessage                   = ShowMessageParams
MessageParams WindowShowMessageRequest            = ShowMessageRequestParams
MessageParams WindowShowDocument                  = ShowDocumentParams
MessageParams WindowLogMessage                    = LogMessageParams
MessageParams WindowWorkDoneProgressCreate        = WorkDoneProgressCreateParams
MessageParams TelemetryEvent                      = JSON
MessageParams ClientRegisterCapability            = RegistrationParams
MessageParams ClientUnregisterCapability          = UnregistrationParams
MessageParams WorkspaceWorkspaceFolders           = Maybe Null
MessageParams WorkspaceConfiguration              = ConfigurationParams
MessageParams WorkspaceApplyEdit                  = ApplyWorkspaceEditParams
MessageParams TextDocumentPublishDiagnostics      = PublishDiagnosticsParams
MessageParams TextDocumentCompletion              = CompletionOptions
MessageParams WorkspaceCodeLensRefresh            = Maybe Null
MessageParams CancelRequest                       = CancelParams
MessageParams Progress                            = OneOf [WorkDoneProgressBegin, WorkDoneProgressReport, WorkDoneProgressEnd]

-- Hacky, but avoids having to carry a FromJSON (MessageParams method) inside sigma types
findParamsImpl : (method : Method from type) -> FromJSON (MessageParams method)
findParamsImpl Initialize                          = %search
findParamsImpl Initialized                         = %search
findParamsImpl Shutdown                            = %search
findParamsImpl Exit                                = %search
findParamsImpl SetTrace                            = %search
findParamsImpl WindowWorkDoneProgressCancel        = %search
findParamsImpl WorkspaceDidChangeWorkspaceFolders  = %search
findParamsImpl WorkspaceDidChangeConfiguration     = %search
findParamsImpl WorkspaceDidChangeWatchedFiles      = %search
findParamsImpl WorkspaceSymbol                     = %search
findParamsImpl WorkspaceExecuteCommand             = %search
findParamsImpl WorkspaceWillCreateFiles            = %search
findParamsImpl TextDocumentDidOpen                 = %search
findParamsImpl TextDocumentDidChange               = %search
findParamsImpl TextDocumentWillSave                = %search
findParamsImpl TextDocumentWillSaveWaitUntil       = %search
findParamsImpl TextDocumentDidSave                 = %search
findParamsImpl TextDocumentDidClose                = %search
findParamsImpl CompletionItemResolve               = %search
findParamsImpl TextDocumentHover                   = %search
findParamsImpl TextDocumentSignatureHelp           = %search
findParamsImpl TextDocumentDeclaration             = %search
findParamsImpl TextDocumentDefinition              = %search
findParamsImpl TextDocumentTypeDefinition          = %search
findParamsImpl TextDocumentImplementation          = %search
findParamsImpl TextDocumentReferences              = %search
findParamsImpl TextDocumentDocumentHighlight       = %search
findParamsImpl TextDocumentDocumentSymbol          = %search
findParamsImpl TextDocumentCodeAction              = %search
findParamsImpl CodeActionResolve                   = %search
findParamsImpl TextDocumentCodeLens                = %search
findParamsImpl CodeLensResolve                     = %search
findParamsImpl TextDocumentDocumentLink            = %search
findParamsImpl DocumentLinkResolve                 = %search
findParamsImpl TextDocumentDocumentColor           = %search
findParamsImpl TextDocumentFormatting              = %search
findParamsImpl TextDocumentRangeFormatting         = %search
findParamsImpl TextDocumentOnTypeFormatting        = %search
findParamsImpl TextDocumentRename                  = %search
findParamsImpl TextDocumentPrepareRename           = %search
findParamsImpl TextDocumentFoldingRange            = %search
findParamsImpl TextDocumentSelectionRange          = %search
findParamsImpl TextDocumentPrepareCallHierarchy    = %search
findParamsImpl CallHierarchyIncomingCalls          = %search
findParamsImpl CallHierarchyOutgoingCalls          = %search
findParamsImpl TextDocumentSemanticTokensFull      = %search
findParamsImpl TextDocumentSemanticTokensFullDelta = %search
findParamsImpl TextDocumentSemanticTokensRange     = %search
findParamsImpl WorkspaceSemanticTokensRefresh      = %search
findParamsImpl TextDocumentLinkedEditingRange      = %search
findParamsImpl TextDocumentMoniker                 = %search
findParamsImpl LogTrace                            = %search
findParamsImpl WindowShowMessage                   = %search
findParamsImpl WindowShowMessageRequest            = %search
findParamsImpl WindowShowDocument                  = %search
findParamsImpl WindowLogMessage                    = %search
findParamsImpl WindowWorkDoneProgressCreate        = %search
findParamsImpl TelemetryEvent                      = %search
findParamsImpl ClientRegisterCapability            = %search
findParamsImpl ClientUnregisterCapability          = %search
findParamsImpl WorkspaceWorkspaceFolders           = %search
findParamsImpl WorkspaceConfiguration              = %search
findParamsImpl WorkspaceApplyEdit                  = %search
findParamsImpl TextDocumentPublishDiagnostics      = %search
findParamsImpl TextDocumentCompletion              = %search
findParamsImpl WorkspaceCodeLensRefresh            = %search
findParamsImpl CancelRequest                       = %search
findParamsImpl Progress                            = %search

||| Maps the response associated to each type of method.
public export
ResponseResult : (method : Method from Request) -> Type
ResponseResult Initialize                          = InitializeResult
ResponseResult Shutdown                            = Maybe Null
ResponseResult WorkspaceSymbol                     = OneOf [List SymbolInformation, Null]
ResponseResult WorkspaceExecuteCommand             = JSON
ResponseResult WorkspaceWillCreateFiles            = OneOf [WorkspaceEdit, Null]
ResponseResult TextDocumentWillSaveWaitUntil       = OneOf [List TextEdit, Null]
ResponseResult CompletionItemResolve               = CompletionItem
ResponseResult TextDocumentHover                   = OneOf [Hover, Null]
ResponseResult TextDocumentSignatureHelp           = OneOf [SignatureHelp, Null]
ResponseResult TextDocumentDeclaration             = OneOf [Location, List Location, List LocationLink, Null]
ResponseResult TextDocumentDefinition              = OneOf [Location, List Location, List LocationLink, Null]
ResponseResult TextDocumentTypeDefinition          = OneOf [Location, List Location, List LocationLink, Null]
ResponseResult TextDocumentImplementation          = OneOf [Location, List Location, List LocationLink, Null]
ResponseResult TextDocumentReferences              = OneOf [List Location, Null]
ResponseResult TextDocumentDocumentHighlight       = OneOf [List DocumentHighlight, Null]
ResponseResult TextDocumentDocumentSymbol          = OneOf [List DocumentSymbol, SymbolInformation, Null]
ResponseResult TextDocumentCodeAction              = OneOf [List (OneOf [Command, CodeAction]), Null]
ResponseResult CodeActionResolve                   = CodeAction
ResponseResult TextDocumentCodeLens                = OneOf [List CodeLens, Null]
ResponseResult CodeLensResolve                     = Maybe Null
ResponseResult TextDocumentDocumentLink            = OneOf [List DocumentLink, Null]
ResponseResult DocumentLinkResolve                 = DocumentLink
ResponseResult TextDocumentDocumentColor           = List ColorInformation
ResponseResult TextDocumentFormatting              = OneOf [List TextEdit, Null]
ResponseResult TextDocumentRangeFormatting         = OneOf [List TextEdit, Null]
ResponseResult TextDocumentOnTypeFormatting        = OneOf [List TextEdit, Null]
ResponseResult TextDocumentRename                  = OneOf [WorkspaceEdit, Null]
ResponseResult TextDocumentPrepareRename           = OneOf [Range, PrepareRenamePlaceholderResponse, PrepareRenameDefaultResponse, Null]
ResponseResult TextDocumentFoldingRange            = OneOf [List FoldingRange, Null]
ResponseResult TextDocumentSelectionRange          = OneOf [List SelectionRange, Null]
ResponseResult TextDocumentPrepareCallHierarchy    = OneOf [List CallHierarchyItem, Null]
ResponseResult CallHierarchyIncomingCalls          = OneOf [List CallHierarchyIncomingCall, Null]
ResponseResult CallHierarchyOutgoingCalls          = OneOf [List CallHierarchyOutgoingCall, Null]
ResponseResult TextDocumentSemanticTokensFull      = OneOf [SemanticTokens, Null]
ResponseResult TextDocumentSemanticTokensFullDelta = OneOf [SemanticTokens, SemanticTokensDelta, Null]
ResponseResult TextDocumentSemanticTokensRange     = OneOf [SemanticTokens, Null]
ResponseResult WorkspaceSemanticTokensRefresh      = Maybe Null
ResponseResult TextDocumentLinkedEditingRange      = OneOf [LinkedEditingRanges, Null]
ResponseResult TextDocumentMoniker                 = OneOf [List Moniker, Null]
ResponseResult WindowShowMessageRequest            = OneOf [MessageActionItem, Null]
ResponseResult WindowShowDocument                  = ShowDocumentResult
ResponseResult WindowWorkDoneProgressCreate        = Maybe Null
ResponseResult ClientRegisterCapability            = Maybe Null
ResponseResult ClientUnregisterCapability          = Maybe Null
ResponseResult WorkspaceWorkspaceFolders           = OneOf [List WorkspaceFolder, Null]
ResponseResult WorkspaceConfiguration              = List JSON
ResponseResult WorkspaceApplyEdit                  = ApplyWorkspaceEditResponse
ResponseResult TextDocumentCompletion              = OneOf [List CompletionItem, CompletionList, Null]
ResponseResult WorkspaceCodeLensRefresh            = Maybe Null

findNotificationImpl : (method : Method from Notification) -> ToJSON (MessageParams method)
findNotificationImpl Initialized = %search
findNotificationImpl Exit = %search
findNotificationImpl SetTrace = %search
findNotificationImpl WindowWorkDoneProgressCancel = %search
findNotificationImpl WorkspaceDidChangeWorkspaceFolders = %search
findNotificationImpl WorkspaceDidChangeConfiguration = %search
findNotificationImpl WorkspaceDidChangeWatchedFiles = %search
findNotificationImpl TextDocumentDidOpen = %search
findNotificationImpl TextDocumentDidChange = %search
findNotificationImpl TextDocumentWillSave = %search
findNotificationImpl TextDocumentDidSave = %search
findNotificationImpl TextDocumentDidClose = %search
findNotificationImpl LogTrace = %search
findNotificationImpl WindowShowMessage = %search
findNotificationImpl WindowLogMessage = %search
findNotificationImpl TelemetryEvent = %search
findNotificationImpl TextDocumentPublishDiagnostics = %search
findNotificationImpl CancelRequest = %search
findNotificationImpl Progress = %search

findResultImpl : (method : Method from Request) -> ToJSON (ResponseResult method)
findResultImpl Initialize = %search
findResultImpl Shutdown = %search
findResultImpl WorkspaceSymbol = %search
findResultImpl WorkspaceExecuteCommand = %search
findResultImpl WorkspaceWillCreateFiles = %search
findResultImpl TextDocumentWillSaveWaitUntil = %search
findResultImpl CompletionItemResolve = %search
findResultImpl TextDocumentHover = %search
findResultImpl TextDocumentSignatureHelp = %search
findResultImpl TextDocumentDeclaration = %search
findResultImpl TextDocumentDefinition = %search
findResultImpl TextDocumentTypeDefinition = %search
findResultImpl TextDocumentImplementation = %search
findResultImpl TextDocumentReferences = %search
findResultImpl TextDocumentDocumentHighlight = %search
findResultImpl TextDocumentDocumentSymbol = %search
findResultImpl TextDocumentCodeAction = %search
findResultImpl CodeActionResolve = %search
findResultImpl TextDocumentCodeLens = %search
findResultImpl CodeLensResolve = %search
findResultImpl TextDocumentDocumentLink = %search
findResultImpl DocumentLinkResolve = %search
findResultImpl TextDocumentDocumentColor = %search
findResultImpl TextDocumentFormatting = %search
findResultImpl TextDocumentRangeFormatting = %search
findResultImpl TextDocumentOnTypeFormatting = %search
findResultImpl TextDocumentRename = %search
findResultImpl TextDocumentPrepareRename = %search
findResultImpl TextDocumentFoldingRange = %search
findResultImpl TextDocumentSelectionRange = %search
findResultImpl TextDocumentPrepareCallHierarchy = %search
findResultImpl CallHierarchyIncomingCalls = %search
findResultImpl CallHierarchyOutgoingCalls = %search
findResultImpl TextDocumentSemanticTokensFull = %search
findResultImpl TextDocumentSemanticTokensFullDelta = %search
findResultImpl TextDocumentSemanticTokensRange = %search
findResultImpl WorkspaceSemanticTokensRefresh = %search
findResultImpl TextDocumentLinkedEditingRange = %search
findResultImpl TextDocumentMoniker = %search
findResultImpl WindowShowMessageRequest = %search
findResultImpl WindowShowDocument = %search
findResultImpl WindowWorkDoneProgressCreate = %search
findResultImpl ClientRegisterCapability = %search
findResultImpl ClientUnregisterCapability = %search
findResultImpl WorkspaceWorkspaceFolders = %search
findResultImpl WorkspaceConfiguration = %search
findResultImpl WorkspaceApplyEdit = %search
findResultImpl TextDocumentCompletion = %search
findResultImpl WorkspaceCodeLensRefresh = %search

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#notificationMessage
public export
data NotificationMessage : Method from Notification -> Type where
  MkNotificationMessage : (method : Method from Notification)
                       -> (params : MessageParams method)
                       -> NotificationMessage method

export
{method : Method from Notification} -> ToJSON (NotificationMessage method) where
  toJSON (MkNotificationMessage method params) =
    JObject ([("jsonrpc", JString "2.0"), ("method", toJSON method), ("params", toJSON @{findNotificationImpl method} params)])

export
FromJSON (from ** method : Method from Notification ** NotificationMessage method) where
  fromJSON (JObject arg) = do
    lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
    (from ** meth) <- lookup "method" arg >>= fromJSON {a = (from ** Method from Notification)}
    case meth of
      Exit => do let par = lookup "params" arg >>= (fromJSON @{findParamsImpl meth})
                 pure (from ** meth ** MkNotificationMessage meth (join par))
      _ => do par <- lookup "params" arg >>= (fromJSON @{findParamsImpl meth})
              pure (from ** meth ** MkNotificationMessage meth par)
  fromJSON _ = neutral

namespace NotificationMessage
  export
  method : {0 m : Method from Notification} -> NotificationMessage m -> Method from Notification
  method (MkNotificationMessage m _) = m

  export
  params : {0 method : Method from Notification} -> NotificationMessage method -> MessageParams method
  params (MkNotificationMessage _ p) = p

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#requestMessage
public export
data RequestMessage : Method from Request -> Type where
  MkRequestMessage : (id : OneOf [Int, String])
                  -> (method : Method from Request)
                  -> (params : MessageParams method)
                  -> RequestMessage method

export
ToJSON (MessageParams method) => ToJSON (RequestMessage method) where
  toJSON (MkRequestMessage id method params) =
    JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("method", toJSON method), ("params", toJSON params)])

export
FromJSON (from ** method : Method from Request ** RequestMessage method) where
  fromJSON (JObject arg) = do
    lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
    id <- lookup "id" arg >>= fromJSON
    (from ** method) <- lookup "method" arg >>= fromJSON {a = (from ** Method from Request)}
    case method of
      Shutdown => do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
                     pure (from ** method ** MkRequestMessage id method (join params))
      WorkspaceSemanticTokensRefresh =>
        do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
           pure (from ** method ** MkRequestMessage id method (join params))
      WorkspaceWorkspaceFolders =>
        do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
           pure (from ** method ** MkRequestMessage id method (join params))
      WorkspaceCodeLensRefresh =>
        do let params = lookup "params" arg >>= (fromJSON @{findParamsImpl method})
           pure (from ** method ** MkRequestMessage id method (join params))
      _ => do params <- lookup "params" arg >>= (fromJSON @{findParamsImpl method})
              pure (from ** method ** MkRequestMessage id method params)
  fromJSON _ = neutral

namespace RequestMessage
  export
  id : RequestMessage m -> OneOf [Int, String]
  id (MkRequestMessage i _ _) = i

  export
  method : {0 m : Method from Request} -> RequestMessage m -> Method from Request
  method (MkRequestMessage _ m _) = m

  export
  params : {0 method : Method from Request} -> RequestMessage method -> MessageParams method
  params (MkRequestMessage _ _ p) = p

||| Maps the message payload to each type of method.
public export
Message : (type : MethodType) -> (Method from type -> Type)
Message Notification = NotificationMessage
Message Request = RequestMessage

export
FromJSON (from ** type ** method : Method from type ** Message type method) where
  fromJSON arg =
    (fromJSON arg >>= \(f ** m ** msg) : (from ** method : Method from Request ** RequestMessage method) => pure (f ** _ ** m ** msg))
      <|> (fromJSON arg >>= \(f ** m ** msg) : (from ** method : Method from Notification ** NotificationMessage method) => pure (f ** _ ** m ** msg))

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage
namespace ErrorCodes
  public export
  data ErrorCodes
    = ParseError
    | InvalidRequest
    | MethodNotFound
    | InvalidParams
    | InternalError
    | ServerNotInitialized
    | UnknownErrorCode
    | ContentModified
    | RequestCancelled
    | JSONRPCReserved Int
    | LSPReserved Int
    | Custom Int

export
ToJSON ErrorCodes where
  toJSON ParseError             = JNumber (-32700)
  toJSON InvalidRequest         = JNumber (-32600)
  toJSON MethodNotFound         = JNumber (-32601)
  toJSON InvalidParams          = JNumber (-32602)
  toJSON InternalError          = JNumber (-32603)
  toJSON ServerNotInitialized   = JNumber (-32002)
  toJSON UnknownErrorCode       = JNumber (-32001)
  toJSON ContentModified        = JNumber (-32801)
  toJSON RequestCancelled       = JNumber (-32800)
  toJSON (JSONRPCReserved code) = JNumber (cast code)
  toJSON (LSPReserved code)     = JNumber (cast code)
  toJSON (Custom code)          = JNumber (cast code)

export
FromJSON ErrorCodes where
  -- TODO: Can't match on negative numbers :(, temporary fix until compiler PR.
  fromJSON (JNumber code) =
    if code == (-32700) then pure ParseError
    else if code == (-32600) then pure InvalidRequest
    else if code == (-32601) then pure MethodNotFound
    else if code == (-32602) then pure InvalidParams
    else if code == (-32603) then pure InternalError
    else if code == (-32002) then pure ServerNotInitialized
    else if code == (-32001) then pure UnknownErrorCode
    else if code == (-32801) then pure ContentModified
    else if code == (-32800) then pure RequestCancelled
    else if (-32099) <= code && code <= (-32000) then pure (JSONRPCReserved $ cast code)
    else if (-32899) <= code && code <= (-32800) then pure (LSPReserved $ cast code)
    else pure (Custom $ cast code)
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage
public export
record ResponseError where
  constructor MkResponseError
  code : ErrorCodes
  message : String
  data_ : JSON
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{{ResponseError}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#responseMessage
public export
data ResponseMessage : Method from type -> Type where
  Success : (id : OneOf [Int, String, Null]) -> (result : ResponseResult method) -> ResponseMessage method
  Failure : (id : OneOf [Int, String, Null]) -> (error : ResponseError) -> ResponseMessage method

export
{method : Method from Request} -> ToJSON (ResponseMessage method) where
  toJSON (Success id result) =
    JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("result", toJSON @{findResultImpl method} result)])
  toJSON (Failure id error) =
    JObject ([("jsonrpc", JString "2.0"), ("id", toJSON id), ("error", toJSON error)])

export
FromJSON (ResponseResult method) => FromJSON (ResponseMessage method) where
  fromJSON (JObject arg) = do
    lookup "jsonrpc" arg >>= (guard . (== JString "2.0"))
    id <- lookup "id" arg >>= fromJSON
    case lookup "result" arg of
         Just v => Success id <$> fromJSON v
         Nothing => Failure id <$> (lookup "error" arg >>= fromJSON)
  fromJSON _ = neutral

namespace ResponseMessage
  export
  id : ResponseMessage method -> OneOf [Int, String, Null]
  id (Success i _) = i
  id (Failure i _) = i

  export
  getResponseId : RequestMessage method -> OneOf [Int, String, Null]
  getResponseId = extend . RequestMessage.id


text:
module Control.Comonad.Env

import public Control.Comonad.Env.Env as Control.Comonad.Env
import public Control.Comonad.Env.Interface as Control.Comonad.Env

ext: idr


text:
module Js.Typeable

import Pruviloj.Core
import Data.Vect

%language ElabReflection

public export
data TypeRep : Type -> Type where
  TRString : TypeRep String
  TRInteger : TypeRep Integer
  TUnit : TypeRep ()
  TRCons : String -> List String -> (a: Type) -> TypeRep a
  TRCons1 : String -> List String -> (a: Type) -> (f: Type->Type) -> TypeRep a -> TypeRep (f a)
  TRCons2 : String -> List String -> (a: Type) -> (b: Type) -> (f: Type->Type->Type) ->
                TypeRep a -> TypeRep b -> TypeRep (f a b)
  TRCons_Nat : String -> List String -> (f: Nat -> Type) -> (n: Nat) -> TypeRep (f n)
  TRFun : TypeRep a -> TypeRep b -> TypeRep (a -> b)

same : TypeRep a -> TypeRep b -> Bool
same TRString TRString = True
same TRInteger TRInteger = True
same TUnit TUnit = True
same (TRCons x1 y1 _) (TRCons x2 y2 _) = x1 == x2 && y1 == y2
same (TRCons1 x1 y1 _ _ z1) (TRCons1 x2 y2 _ _ z2) = x1 == x2 && y1 == y2 && same z1 z2
same (TRCons2 x1 y1 _ _ _ z1 w1) (TRCons2 x2 y2 _ _ _ z2 w2) = x1 == x2 && y1 == y2 && same z1 z2 && same w1 w2
same (TRCons_Nat x1 y1 _ z1) (TRCons_Nat x2 y2 _ z2) = x1 == x2 && y1 == y2 && z1 == z2
same (TRFun x1 y1) (TRFun x2 y2) = same x1 x2 && same y1 y2
same _ _ = False

export
interface Typeable (a: Type) where
  getTypeRep : TypeRep a

export
tcast : (Typeable a, Typeable b) => a -> Maybe b
tcast {a} {b} x =
  if same (the (TypeRep a) getTypeRep) (the (TypeRep b) getTypeRep) then Just $ believe_me x
    else Nothing

useGetTypeRep : Elab ()
useGetTypeRep =
  do
    [_, s2] <- apply (Var `{getTypeRep}) [True, False]
    solve
    focus s2
    hypothesis

deriveTCons1 : String -> List String -> TTName -> Elab ()
deriveTCons1 name modName x=
  do
    [sub] <- apply `(TRCons1 ~(quote name) ~(quote modName) ~(Var x) ~(Var (NS (UN name) modName))) [False]
    solve
    focus sub
    useGetTypeRep

deriveTCons_Nat : String -> List String -> Elab ()
deriveTCons_Nat name modName =
  do
    [_] <- apply `(TRCons_Nat ~(quote name) ~(quote modName) ~(Var (NS (UN name) modName))) [True]
    solve

deriveTypeableAux : TTName -> TT -> Elab ()
deriveTypeableAux dname val =
  case val of
    P (TCon _ 0) (NS (UN name) modName) _ =>
      do
        fill `(TRCons ~(quote name) ~(quote modName) ~(Var (NS (UN name) modName)))
        solve
    App
      (P (TCon _ 1) (NS (UN name) modName) _)
      (P Bound x _) =>
        deriveTCons1 name modName x <|> deriveTCons_Nat name modName
    App
      (App
        (P (TCon _ 2) (NS (UN name) modName) _)
        (P Bound x _))
      (P Bound y _) =>
        do
          [sub1, sub2] <- apply
                    `(TRCons2 ~(quote name) ~(quote modName) ~(Var x) ~(Var y) ~(Var (NS (UN name) modName)))
                    [False, False]
          solve
          focus sub1
          useGetTypeRep
          focus sub2
          useGetTypeRep
    other => fail [ TermPart other
                  , TextPart "cannot make typeable"
                  ]

export
deriveTypeable : Elab ()
deriveTypeable =
  do
    (ng,tg) <- getGoal
    case tg of
      `(TypeRep ~val) =>
        deriveTypeableAux ng val
      otherGoal => fail [ TermPart otherGoal
                        , TextPart "has an unexpected form for getTypeRep?"
                        ]

export
Typeable String where
  getTypeRep = TRString

export
Typeable Integer where
  getTypeRep = TRInteger

export
(Typeable a, Typeable b) => Typeable (a->b) where
  getTypeRep = TRFun getTypeRep getTypeRep

export
Typeable Bool where
  getTypeRep = %runElab deriveTypeable

export
Typeable () where
  getTypeRep = TUnit

export
Typeable Nat where
  getTypeRep = %runElab deriveTypeable

export
Typeable a => Typeable (Maybe a) where
  getTypeRep = %runElab deriveTypeable

export
Typeable a => Typeable (List a) where
  getTypeRep = %runElab deriveTypeable

export
(Typeable a, Typeable b) => Typeable (Either a b) where
  getTypeRep = %runElab deriveTypeable

export
Typeable (Fin n) where
  getTypeRep = %runElab deriveTypeable

export
(Typeable a, Typeable b) => Typeable (a, b) where
  getTypeRep = %runElab deriveTypeable

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Main

import Erlang

-- Wrappers around `run_curriedX` that takes a curried, pure function

erlRunCurriedFun1 : (Int -> Int) -> IO Int
erlRunCurriedFun1 f = do
  let f' = MkFun1 f
  pure $ erlUnsafeCall Int "test_support" "run_curried1" [f']

erlRunCurriedFun2 : (Int -> Int -> Int) -> IO Int
erlRunCurriedFun2 f = do
  let f' = MkFun1 (\x => MkFun1 (f x))
  pure $ erlUnsafeCall Int "test_support" "run_curried2" [f']

-- Wrappers around `runX` that takes a pure function

erlRunFun0 : Int -> IO Int
erlRunFun0 x = pure $ erlUnsafeCall Int "test_support" "run0" [MkFun0 x]

erlRunFun1 : (Int -> Int) -> IO Int
erlRunFun1 x = pure $ erlUnsafeCall Int "test_support" "run1" [MkFun1 x]

erlRunFun2 : (Int -> Int -> Int) -> IO Int
erlRunFun2 x = pure $ erlUnsafeCall Int "test_support" "run2" [MkFun2 x]

-- Wrappers around `runX` that takes an IO action

erlRunIO0 : IO Int -> IO Int
erlRunIO0 x = pure $ erlUnsafeCall Int "test_support" "run0" [MkIOFun0 x]

erlRunIO1 : (Int -> IO Int) -> IO Int
erlRunIO1 x = pure $ erlUnsafeCall Int "test_support" "run1" [MkIOFun1 x]

erlRunIO2 : (Int -> Int -> IO Int) -> IO Int
erlRunIO2 x = pure $ erlUnsafeCall Int "test_support" "run2" [MkIOFun2 x]

-- Tests

curriedFunTest : IO ()
curriedFunTest = do
  putStrLn "curriedFunTest"
  res1 <- erlRunCurriedFun1 (+ 10)
  printLn res1
  res2 <- erlRunCurriedFun2 (*)
  printLn res2

funTest : IO ()
funTest = do
  putStrLn "funTest"
  res0 <- erlRunFun0 42
  printLn res0
  res1 <- erlRunFun1 (+ 42)
  printLn res1
  res2 <- erlRunFun2 (+)
  printLn res2

ioTest : IO ()
ioTest = do
  putStrLn "ioTest"
  res0 <- erlRunIO0 (do { putStrLn "Running IO action with arity 0"; pure 42 })
  printLn res0
  res1 <- erlRunIO1 (\x => do { putStrLn "Running IO action with arity 1"; pure (x + 42) })
  printLn res1
  res2 <- erlRunIO2 (\x, y => do { putStrLn "Running IO action with arity 2"; pure (x + y) })
  printLn res2

main : IO ()
main = do
  curriedFunTest
  funTest
  ioTest


text:
module Main

import Data.Vect

-- let .. in defines local variables
-- where .. allows for local function definitions

-- Nat is a natural number type, non-negative integers.
-- ++ is for appending Strings or Lists to each other.
-- words : String -> List String -- splits on a space
average : (str : String) -> Double
average str =
  let
    numWords = wordCount str
    totalLength = sum (allLengths (words str)) in
    cast totalLength / cast numWords -- this line is the result.
  where
    wordCount : String -> Nat
    wordCount str = length (words str)

    allLengths : List String -> List Nat
    allLengths strs = map length strs

showAverage : String -> String
showAverage str =
  "Average word lenth: " ++
  show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showAverage
-- repl displays a prompt, reads a String from the console and displays the
-- result of running a function on that String, forever.

-- Where an expression can be one of several types, you can declare which
-- inline with the function 'the'
-- the Int 45 yields an Int with the value 45. This is not syntax sugar, 'the'
-- is an ordinary function.
-- the : (a: Type) -> a -> a
-- Given a type, a, and a value of that type, 'the' returns the value. The
-- implementation might look like the type = id -- identity

-- Can partially apply functions
add : Num a => a -> a -> a
add x y = x + y
--
add3 : Int -> Int
add3 = add 3

nine : Int
nine = add3 6

-- <T> T identity(T t) { return t; }
identity : ty -> ty
identity x = x

-- If we want to write a function that can add a number to itself, this won't
-- work:
-- bad_double : ty -> ty
-- bad_double x = x + x
-- "ty is not a numeric type"
-- => means we're setting a restriction on a
double : Num ty => ty -> ty
double x = x + x

-- Defining a function that executes a function twice over a value
twice : (a -> a) -> a -> a
twice f x = f (f x)

quadruple : Num a => a -> a
quadruple x = double (double x)

-- lambda is \arg => result
squared_twice : Integer
squared_twice = twice (\x => x * x) 2 -- 16

-- :t \x => x * x -- Integer -> Integer

-- :t \x : Int, y : Int => x + y -- Int -> Int

-- Tuples are nested pairs
tuples_are_nested_pairs : Bool
tuples_are_nested_pairs = (1, (2, (3, (4)))) == (1, 2, 3, 4)

-- Lists use []. Appending two lists:
one_to_seven : List Integer
one_to_seven = [1, 2, 3] ++ [4, 5, 6, 7]

-- Prepending (consing) to a list is (::)
zero_to_seven : List Integer
zero_to_seven = 0 :: one_to_seven

one_to_four : List Integer
one_to_four = 1 :: 2 :: 3 :: 4 :: []

one_to_a_hundred : List Integer
one_to_a_hundred = [1..100]

-- module Xyz at the top of the file, generally matches Xyz.idr in the filename
-- import Foo looks for Foo.idr in the same directory or elsewhere that Idris
-- can find.

{- Multiline
comment -}

||| Documentation comment for foo
foo : String
-- can be viewed with :doc foo or Ctrl-Alt-D in Atom

-- Exercises
-- 1. Types of
-- ("A", "B", "C") -- (String, String, String)
-- ["A", "B", "C"] -- List String
-- (("A", "B"), "C") -- ((String, String), String)

-- Given a natural number, min, and a String, str, convert str to lowercase and
-- return true if it's the same forwards as backwards, as long as it's over the
-- length 'min'.
palindrome : Nat -> String -> Bool
palindrome min str = if (length str > min) then
    (let lstr = toLower str in reverse lstr == lstr)
  else False

-- (x, y) is a tuple of an x and a y. (Nat, Nat) is a type, two natural numbers.
-- (length (words str), length str) is a value of that type.
counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

-- Ord is an interface something like Java's Comparable.
-- <A extends Comparable<A>> List<A> topTen(List<A> list)
top_ten : Ord a => List a -> List a
top_ten list = take 10 (reverse (sort list))

over_length : Nat -> List String -> Nat
over_length len list = length (filter (\str => length str > len) list)

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
total twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

partial loop : Void
loop = loop

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.IxArray

import Data.IOArray
import Data.IxRel

%access export

private
newArrayUninitialized : Int -> IO (IOArray elem)
newArrayUninitialized len = newArray {elem=elem} len (really_believe_me prim__null)

public export
CanResize : Int -> Int -> Type
CanResize = Predicate (<=)

public export
CanIndex : Int -> Int -> Type
CanIndex = Predicate (\ix, len => ix >= 0 && ix < len)

data IxArray : Int -> Type -> Type where
  MkIxArray : (len : Int) -> (parr : IOArray a) -> IxArray len a

length : IxArray len a -> Int
length (MkIxArray len parr) = len

fromList : List a -> IO (len ** IxArray len a)
fromList xs = do
  let len = cast $ length xs
  parr <- newArrayUninitialized len
  for_ {b = ()} (zip [0 .. len - 1] xs) $ \(ix, elem) => unsafeWriteArray parr ix elem
  pure $ (len ** MkIxArray len parr)

index : (ix: Int) -> IxArray len a -> {auto canIndex: CanIndex ix len} -> IO a
index ix (MkIxArray len parr) = unsafeReadArray parr ix

setAt : (ix: Int) -> a -> IxArray len a -> {auto canIndex: CanIndex ix len} -> IO ()
setAt ix elem (MkIxArray len parr) = unsafeWriteArray parr ix elem

replicate : (len: Int) -> a -> IO (IxArray len a)
replicate len fillElem = do
  parr <- newArray len fillElem
  pure $ MkIxArray len parr

imap : (a -> a) -> IxArray len a -> IO ()
imap f (MkIxArray len parr) =
  for_ {b = ()} [0 .. len - 1] $ \ix => do
    elem <- unsafeReadArray parr ix
    let newElem = f elem
    unsafeWriteArray parr ix newElem

itraverse : (a -> IO a) -> IxArray len a -> IO ()
itraverse f (MkIxArray len parr) =
  for_ {b = ()} [0 .. len - 1] $ \ix => do
    elem <- unsafeReadArray parr ix
    newElem <- f elem
    unsafeWriteArray parr ix newElem

resize : (newLen : Int) -> a -> IxArray len a -> {auto canResize : CanResize len newLen} -> IO (IxArray newLen a)
resize newLen fillElem (MkIxArray len parr) = do
  newParr <- newArray newLen fillElem
  for_ {b = ()} [0 .. len - 1] $ \ix => do
    elem <- unsafeReadArray parr ix
    unsafeWriteArray newParr ix elem
  pure $ MkIxArray newLen newParr

clone : IxArray len a -> IO (IxArray len a)
clone (MkIxArray len parr) = do
  newParr <- newArrayUninitialized len
  for_ {b = ()} [0 .. len - 1] $ \ix => do
    elem <- unsafeReadArray parr ix
    unsafeWriteArray newParr ix elem
  pure $ MkIxArray len newParr

max_stars_repo_name: ejconlon/idris-array

max_issues_repo_name: ejconlon/ixarray

max_forks_repo_name: ejconlon/ixarray


text:
module TypedContainers.LawfulOrd

%default total

public export
interface LawfulOrd a where
  compare : a -> a -> Ordering
  0 reflexivity : (x : a) -> (compare x x = EQ)
  0 reversion1 : (x : a) -> (y : a) -> (compare x y = LT) -> (compare y x = GT)
  0 reversion2 : (x : a) -> (y : a) -> (compare x y = GT) -> (compare y x = LT)
  0 reversion3 : (x : a) -> (y : a) -> (compare x y = EQ) -> (compare y x = EQ)
  0 transitivity : (x : a) -> (y : a) -> (z : a) -> (compare x y = LT) -> (compare y z = LT) -> (compare x z = LT)
  0 equality1 : (x : a) -> (y : a) -> (z : a) -> (compare x y = EQ) -> (compare x z = compare y z)
  0 equality2 : (x : a) -> (y : a) -> (z : a) -> (compare x y = EQ) -> (compare z x = compare z y)

public export
interface LawfulOrd a => LawfullerOrd a where
  -- `compare` needs to be unambigious here because the name is
  -- seemingly resolved where the instances are defined...
  0 realEquality : (x : a) -> (y : a) -> (TypedContainers.LawfulOrd.compare x y = EQ) -> (x = y)

public export
(==) : LawfulOrd a => a -> a -> Bool
x == y = case compare x y of { EQ => True; _ => False }

public export
(<) : LawfulOrd a => a -> a -> Bool
x < y = case compare x y of { LT => True; _ => False }

public export
(>) : LawfulOrd a => a -> a -> Bool
x > y = case compare x y of { GT => True; _ => False }

public export
convLT : LawfulOrd a => (x : a) -> (y : a) -> (x < y = True) -> (compare x y = LT)
convLT x y p with (compare x y)
  convLT x y Refl | GT impossible
  convLT x y Refl | EQ impossible
  convLT x y Refl | LT = Refl

public export
convGT : LawfulOrd a => (x : a) -> (y : a) -> (x > y = True) -> (compare x y = GT)
convGT x y p with (compare x y)
  convGT x y Refl | GT = Refl
  convGT x y Refl | EQ impossible
  convGT x y Refl | LT impossible

public export
convEQ : LawfulOrd a => (x : a) -> (y : a) -> (x == y = True) -> (compare x y = EQ)
convEQ x y p with (compare x y)
  convEQ x y Refl | GT impossible
  convEQ x y Refl | EQ = Refl
  convEQ x y Refl | LT impossible

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 7

-- check that all functions are total
%default total

--
-- section 7.1
-- see Shape.idr
--

--
-- section 7.2
-- see Expr.idr
--

--
-- section 7.3
-- see Expr.idr
--

-- we define Vect by hand because Eq and Foldable already exist for Data.Vect
data Vect : (size : Nat) -> (ty : Type) -> Type where
  Nil : Vect Z ty
  (::) : (x : ty) -> (xs : Vect size ty) -> Vect (S size) ty

Eq ty => Eq (Vect n ty) where
  (==) [] [] = True
  (==) (x :: xs) (y :: ys) = (x == y) && xs == ys
  (==) _ _ = False

Foldable (Vect n) where
  foldr func init [] = init
  foldr func init (x :: xs) = func x (foldr func init xs)

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Data.Matrix.AlgebraicVerified

import Control.Algebra
import Control.Algebra.VectorSpace -- definition of module
import Classes.Verified -- definition of verified algebras other than modules
import Control.Algebra.DiamondInstances
import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20

import Data.Vect.Structural

-- Style & syntax
import Syntax.PreorderReasoning

-- Support
import Control.Algebra.DiamondInstances

%default total

{-
Definitions:
* Verified module
* Verified vector space

Ripped from comments of Classes.Verified, commenting out there coincides with definition of module being in the separate module Control.Algebra.VectorSpace from Control.Algebra.
-}

class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
  total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
  total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v
  total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
  total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

--class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}

-- As desired in Data.Matrix.Algebraic
instance [vectModule] Module a b => Module a (Vect n b) where
	(<#>) r = map (r <#>)

{-
Definitions:
* Verified module instance for Matrix n m ZZ.
* A verified module instance for Vect n ZZ will prevent you from writing one for Matrix,
	the proof of which depends on (Vect n ZZ) being a (VerifiedModule) in all but name.
-}

semigroupOpIsAssociative_Vect : (VerifiedRingWithUnity a) => (l, c, r : Vect n a) -> l <+> (c <+> r) = l <+> c <+> r
semigroupOpIsAssociative_Vect [] [] [] = Refl
semigroupOpIsAssociative_Vect (l::ls) (c::cs) (r::rs) = vecHeadtailsEq (semigroupOpIsAssociative _ _ _) (semigroupOpIsAssociative_Vect _ _ _)

monoidNeutralIsNeutralL_Vect : (VerifiedRingWithUnity a) => (l : Vect n a) -> l <+> Algebra.neutral = l
monoidNeutralIsNeutralL_Vect [] = Refl
monoidNeutralIsNeutralL_Vect (l::ls) = vecHeadtailsEq (monoidNeutralIsNeutralL _) $ monoidNeutralIsNeutralL_Vect _

monoidNeutralIsNeutralR_Vect : (VerifiedRingWithUnity a) => (r : Vect n a) -> Algebra.neutral <+> r = r
monoidNeutralIsNeutralR_Vect [] = Refl
monoidNeutralIsNeutralR_Vect (r::rs) = vecHeadtailsEq (monoidNeutralIsNeutralR _) $ monoidNeutralIsNeutralR_Vect _

groupInverseIsInverseL_Vect : (VerifiedRingWithUnity a) => (l : Vect n a) -> l <+> inverse l = Algebra.neutral
groupInverseIsInverseL_Vect [] = Refl
groupInverseIsInverseL_Vect (l::ls) = vecHeadtailsEq (groupInverseIsInverseL _) $ groupInverseIsInverseL_Vect _

groupInverseIsInverseR_Vect : (VerifiedRingWithUnity a) => (r : Vect n a) -> inverse r <+> r = Algebra.neutral
groupInverseIsInverseR_Vect [] = Refl
groupInverseIsInverseR_Vect (r::rs) = vecHeadtailsEq (groupInverseIsInverseR _) $ groupInverseIsInverseR_Vect _

abelianGroupOpIsCommutative_Vect : (VerifiedRingWithUnity a) => (l, r : Vect n a) -> l <+> r = r <+> l
abelianGroupOpIsCommutative_Vect [] [] = Refl
abelianGroupOpIsCommutative_Vect (l::ls) (r::rs) = vecHeadtailsEq (abelianGroupOpIsCommutative _ _) $ abelianGroupOpIsCommutative_Vect _ _

moduleScalarMultiplyComposition_Vect : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> ( x, y : a ) -> ( v : Vect n a )
	-> x <#> (y <#> v) = x <.> y <#> v
moduleScalarMultiplyComposition_Vect x y [] = Refl
moduleScalarMultiplyComposition_Vect {ok} x y (v::vs) =
	vecHeadtailsEq
		(rewrite ok in ringOpIsAssociative x y v)
	$ moduleScalarMultiplyComposition_Vect x y vs

{-
This doesn't exist because of a diamond inheritance problem.

moduleScalarUnityIsUnity_Vect : (VerifiedRingWithUnity a) => ( v : Vect n a ) -> (Algebra.unity {a=a}) <#> v = v
moduleScalarUnityIsUnity_Vect [] = Refl
moduleScalarUnityIsUnity_Vect (v::vs) = ?moduleScalarUnityIsUnity_Vect'

---

So we use this instead,
where the equality between (<.>)s coming from different instances is
an automatically solved assumption.
-}

moduleScalarUnityIsUnity_Vect : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> ( v : Vect n a )
	-> (Algebra.unity {a=a}) <#> v = v
moduleScalarUnityIsUnity_Vect [] = Refl
moduleScalarUnityIsUnity_Vect {ok} (v::vs) =
	vecHeadtailsEq (
		trans (cong {f=\t => t Algebra.unity v} ok)
		$ ringWithUnityIsUnityR v)
	$ moduleScalarUnityIsUnity_Vect vs

moduleScalarMultDistributiveWRTVectorAddition_Vect : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (s : a) -> (v, w : Vect n a)
	-> s <#> v <+> w = (s <#> v) <+> (s <#> w)
moduleScalarMultDistributiveWRTVectorAddition_Vect s [] [] = Refl
moduleScalarMultDistributiveWRTVectorAddition_Vect {ok} s (v::vs) (w::ws) =
	vecHeadtailsEq
		(rewrite ok in ringOpIsDistributiveL s v w)
	$ moduleScalarMultDistributiveWRTVectorAddition_Vect s vs ws

moduleScalarMultDistributiveWRTModuleAddition_Vect : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (s, t : a) -> (v : Vect n a)
	-> s <+> t <#> v = (s <#> v) <+> (t <#> v)
moduleScalarMultDistributiveWRTModuleAddition_Vect s t [] = Refl
moduleScalarMultDistributiveWRTModuleAddition_Vect {ok} s t (v::vs) =
	vecHeadtailsEq
		(rewrite ok in ringOpIsDistributiveR s t v)
	$ moduleScalarMultDistributiveWRTModuleAddition_Vect s t vs

{-
instance (VerifiedRingWithUnity a) => VerifiedSemigroup (Vect n a) where
	semigroupOpIsAssociative = ?semigroupOpIsAssociative_Vect

instance (VerifiedRingWithUnity a) => VerifiedMonoid (Vect n a) where {
	monoidNeutralIsNeutralL = ?monoidNeutralIsNeutralL_Vect
	monoidNeutralIsNeutralR = ?monoidNeutralIsNeutralR_Vect
}

instance (VerifiedRingWithUnity a) => VerifiedGroup (Vect n a) where {
	groupInverseIsInverseL = ?groupInverseIsInverseL_Vect
	groupInverseIsInverseR = ?groupInverseIsInverseR_Vect
}

instance (VerifiedRingWithUnity a) => VerifiedAbelianGroup (Vect n a) where {
	abelianGroupOpIsCommutative = ?abelianGroupOpIsCommutative_Vect
}

instance (VerifiedRingWithUnity a) => VerifiedModule a (Vect n a) where {
	moduleScalarMultiplyComposition = ?moduleScalarMultiplyComposition_Vect
	moduleScalarUnityIsUnity = ?moduleScalarUnityIsUnity_Vect
	moduleScalarMultDistributiveWRTVectorAddition = ?moduleScalarMultDistributiveWRTVectorAddition_Vect
	moduleScalarMultDistributiveWRTModuleAddition = ?moduleScalarMultDistributiveWRTModuleAddition_Vect
}
-}

semigroupOpIsAssociative_Mat : (VerifiedRingWithUnity a) => (l, c, r : Matrix n m a) -> l <+> (c <+> r) = l <+> c <+> r
semigroupOpIsAssociative_Mat [] [] [] = Refl
semigroupOpIsAssociative_Mat (l::ls) (c::cs) (r::rs) = vecHeadtailsEq (semigroupOpIsAssociative_Vect _ _ _) (semigroupOpIsAssociative_Mat _ _ _)

monoidNeutralIsNeutralL_Mat : (VerifiedRingWithUnity a) => (l : Matrix n m a) -> l <+> Algebra.neutral = l
monoidNeutralIsNeutralL_Mat [] = Refl
monoidNeutralIsNeutralL_Mat (l::ls) = vecHeadtailsEq (monoidNeutralIsNeutralL_Vect _) $ monoidNeutralIsNeutralL_Mat _

monoidNeutralIsNeutralR_Mat : (VerifiedRingWithUnity a) => (r : Matrix n m a) -> Algebra.neutral <+> r = r
monoidNeutralIsNeutralR_Mat [] = Refl
monoidNeutralIsNeutralR_Mat (r::rs) = vecHeadtailsEq (monoidNeutralIsNeutralR_Vect _) $ monoidNeutralIsNeutralR_Mat _

groupInverseIsInverseL_Mat : (VerifiedRingWithUnity a) => (l : Matrix n m a) -> l <+> inverse l = Algebra.neutral
groupInverseIsInverseL_Mat [] = Refl
groupInverseIsInverseL_Mat (l::ls) = vecHeadtailsEq (groupInverseIsInverseL_Vect _) $ groupInverseIsInverseL_Mat _

groupInverseIsInverseR_Mat : (VerifiedRingWithUnity a) => (r : Matrix n m a) -> inverse r <+> r = Algebra.neutral
groupInverseIsInverseR_Mat [] = Refl
groupInverseIsInverseR_Mat (r::rs) = vecHeadtailsEq (groupInverseIsInverseR_Vect _) $ groupInverseIsInverseR_Mat _

abelianGroupOpIsCommutative_Mat : (VerifiedRingWithUnity a) => (l, r : Matrix n m a) -> l <+> r = r <+> l
abelianGroupOpIsCommutative_Mat [] [] = Refl
abelianGroupOpIsCommutative_Mat (l::ls) (r::rs) = vecHeadtailsEq (abelianGroupOpIsCommutative_Vect _ _) $ abelianGroupOpIsCommutative_Mat _ _

moduleScalarMultiplyComposition_Mat : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> ( x, y : a ) -> ( v : Matrix n m a )
	-> x <#> (y <#> v) = x <.> y <#> v
moduleScalarMultiplyComposition_Mat x y [] = Refl
moduleScalarMultiplyComposition_Mat x y (v::vs) = vecHeadtailsEq (moduleScalarMultiplyComposition_Vect _ _ _) $ moduleScalarMultiplyComposition_Mat _ _ _

moduleScalarUnityIsUnity_Mat : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> ( v : Matrix n m a )
	-> (Algebra.unity {a=a}) <#> v = v
moduleScalarUnityIsUnity_Mat [] = Refl
moduleScalarUnityIsUnity_Mat (v::vs) = vecHeadtailsEq (moduleScalarUnityIsUnity_Vect _)
	$ moduleScalarUnityIsUnity_Mat _

moduleScalarMultDistributiveWRTVectorAddition_Mat : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (s : a) -> (v, w : Matrix n m a)
	-> s <#> v <+> w = (s <#> v) <+> (s <#> w)
moduleScalarMultDistributiveWRTVectorAddition_Mat s [] [] = Refl
moduleScalarMultDistributiveWRTVectorAddition_Mat s (v::vs) (w::ws) = vecHeadtailsEq (moduleScalarMultDistributiveWRTVectorAddition_Vect _ _ _) $ moduleScalarMultDistributiveWRTVectorAddition_Mat _ _ _

moduleScalarMultDistributiveWRTModuleAddition_Mat : (VerifiedRingWithUnity a)
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (s, t : a) -> (v : Matrix n m a)
	-> s <+> t <#> v = (s <#> v) <+> (t <#> v)
moduleScalarMultDistributiveWRTModuleAddition_Mat s t [] = Refl
moduleScalarMultDistributiveWRTModuleAddition_Mat s t (v::vs) = vecHeadtailsEq (moduleScalarMultDistributiveWRTModuleAddition_Vect _ _ _) $ moduleScalarMultDistributiveWRTModuleAddition_Mat _ _ _

instance (VerifiedRingWithUnity a) => VerifiedSemigroup (Matrix n m a) where
	semigroupOpIsAssociative = semigroupOpIsAssociative_Mat

instance (VerifiedRingWithUnity a) => VerifiedMonoid (Matrix n m a) where {
	monoidNeutralIsNeutralL = monoidNeutralIsNeutralL_Mat
	monoidNeutralIsNeutralR = monoidNeutralIsNeutralR_Mat
}

instance (VerifiedRingWithUnity a) => VerifiedGroup (Matrix n m a) where {
	groupInverseIsInverseL = groupInverseIsInverseL_Mat
	groupInverseIsInverseR = groupInverseIsInverseR_Mat
}

instance (VerifiedRingWithUnity a) => VerifiedAbelianGroup (Matrix n m a) where {
	abelianGroupOpIsCommutative = abelianGroupOpIsCommutative_Mat
}

{-
Trivial identities about (unital) rings.
-}

-- Actually theorems about quasigroups
groupOpIsCancellativeL : VerifiedGroup a => (left, right1, right2 : a) -> left<+>right1 = left<+>right2 -> right1=right2
groupOpIsCancellativeL left right1 right2 pr = trans (sym $ trans (cong {f=(<+>right1)} $ groupInverseIsInverseR left) $ monoidNeutralIsNeutralR right1) $ trans (trans (sym $ semigroupOpIsAssociative (inverse left) left right1) $ trans (cong {f=((inverse left)<+>)} pr) $ semigroupOpIsAssociative (inverse left) left right2) $ trans (cong {f=(<+>right2)} $ groupInverseIsInverseR left) $ monoidNeutralIsNeutralR right2

groupOpIsCancellativeR : VerifiedGroup a => (left1, left2, right : a) -> left1<+>right = left2<+>right -> left1=left2
groupOpIsCancellativeR left1 left2 right pr = trans (sym $ trans (cong {f=(left1<+>)} $ groupInverseIsInverseL right) $ monoidNeutralIsNeutralL left1) $ trans (trans (semigroupOpIsAssociative left1 right (inverse right)) $ trans (cong {f=(<+>(inverse right))} pr) $ sym $ semigroupOpIsAssociative left2 right (inverse right)) $ trans (cong {f=(left2<+>)} $ groupInverseIsInverseL right) $ monoidNeutralIsNeutralL left2

groupOpIsCancellativeL_Vect : VerifiedRingWithUnity a =>
	(left, right1, right2 : Vect n a)
	-> left<+>right1 = left<+>right2 -> right1=right2
groupOpIsCancellativeL_Vect left right1 right2 pr =
	trans (sym $ trans (cong {f=(<+>right1)} $ groupInverseIsInverseR_Vect left)
		$ monoidNeutralIsNeutralR_Vect right1)
	$ trans (trans (sym $ semigroupOpIsAssociative_Vect (inverse left) left right1)
		$ trans (cong {f=((inverse left)<+>)} pr)
		$ semigroupOpIsAssociative_Vect (inverse left) left right2)
	$ trans (cong {f=(<+>right2)} $ groupInverseIsInverseR_Vect left)
	$ monoidNeutralIsNeutralR_Vect right2

groupOpIsCancellativeR_Vect : VerifiedRingWithUnity a =>
	(left1, left2, right : Vect n a)
	-> (left1 <+> right = left2 <+> right) -> left1 = left2
groupOpIsCancellativeR_Vect left1 left2 right pr =
	trans (sym $ trans (cong {f=(left1<+>)} $ groupInverseIsInverseL_Vect right)
		$ monoidNeutralIsNeutralL_Vect left1)
	$ trans (trans (semigroupOpIsAssociative_Vect left1 right (inverse right))
		$ trans (cong {f=(<+>(inverse right))} pr)
		$ sym $ semigroupOpIsAssociative_Vect left2 right (inverse right))
	$ trans (cong {f=(left2<+>)} $ groupInverseIsInverseL_Vect right)
	$ monoidNeutralIsNeutralL_Vect left2

-- Not used for the below, but for elsewhere.
neutralSelfInverse : VerifiedGroup a => inverse $ the a $ Algebra.neutral = the a $ Algebra.neutral
neutralSelfInverse = groupOpIsCancellativeL _ _ _ $ trans (groupInverseIsInverseL _) $ sym $ monoidNeutralIsNeutralL _

groupElemOwnDoubleImpliesNeut : VerifiedGroup a => (x : a) -> x<+>x=x -> x = Algebra.neutral
groupElemOwnDoubleImpliesNeut x pr = groupOpIsCancellativeL x x Algebra.neutral $ trans pr $ sym $ monoidNeutralIsNeutralL x

groupSubtractionIsRDivision : VerifiedGroup t
	=> {auto ok :
		((<+>) @{vgrpSemigroupByGrp $ the (VerifiedGroup t) %instance})
		= ((<+>) @{vgrpSemigroupByVMon $ the (VerifiedGroup t) %instance})
		}
	-> (a, b : t)
	-> (a <-> b) <+> b = a
groupSubtractionIsRDivision {ok} a b = rewrite ok in
	trans (sym $ semigroupOpIsAssociative a (inverse b) b)
	$ trans (cong $ groupInverseIsInverseR b)
	$ monoidNeutralIsNeutralL a

groupSubtractionIsRDivision_Vect : VerifiedGroup t
	=> {auto ok :
		((<+>) @{vgrpSemigroupByGrp $ the (VerifiedGroup t) %instance})
		= ((<+>) @{vgrpSemigroupByVMon $ the (VerifiedGroup t) %instance})
		}
	-> (a, b : Vect n t)
	-> (a <-> b) <+> b = a
groupSubtractionIsRDivision_Vect [] [] = Refl
groupSubtractionIsRDivision_Vect (a::as) (b::bs)
	= vecHeadtailsEq (groupSubtractionIsRDivision a b)
	$ groupSubtractionIsRDivision_Vect as bs

groupDivisionAddLToSubR : VerifiedGroup t
	=> {auto ok :
		((<+>) @{vgrpSemigroupByGrp $ the (VerifiedGroup t) %instance})
		= ((<+>) @{vgrpSemigroupByVMon $ the (VerifiedGroup t) %instance})
		}
	-> (x, y, z : t)
	-> x <+> y = z
	-> x = z <-> y
groupDivisionAddLToSubR {ok} x y z pr
	= groupOpIsCancellativeR x (z <-> y) y
	$ trans pr
	$ sym $ groupSubtractionIsRDivision {ok=ok} z y

inverseIsInvolution : VerifiedGroup t
	=> (r : t)
	-> inverse $ inverse r = r
inverseIsInvolution r = groupOpIsCancellativeR (inverse $ inverse r) r (inverse r)
	$ trans (groupInverseIsInverseR _)
	$ sym $ groupInverseIsInverseL _

ringNeutralIsMultZeroL : VerifiedRing a => (x : a) -> Algebra.neutral <.> x = Algebra.neutral
ringNeutralIsMultZeroL x = groupElemOwnDoubleImpliesNeut (Algebra.neutral <.> x) $ trans (sym $ ringOpIsDistributiveR Algebra.neutral Algebra.neutral x) $ cong {f=(<.>x)} $ monoidNeutralIsNeutralL Algebra.neutral

ringNeutralIsMultZeroR : VerifiedRing a => (x : a) -> x <.> Algebra.neutral = Algebra.neutral
ringNeutralIsMultZeroR x = groupElemOwnDoubleImpliesNeut (x <.> Algebra.neutral) $ trans (sym $ ringOpIsDistributiveL x Algebra.neutral Algebra.neutral) $ cong {f=(x<.>)} $ monoidNeutralIsNeutralL Algebra.neutral

ringNegationCommutesWithLeftMult : VerifiedRing a => (left, right : a) -> left<.>(inverse right) = inverse $ left<.>right
ringNegationCommutesWithLeftMult left right = groupOpIsCancellativeR (left<.>(inverse right)) (inverse $ left<.>right) (left<.>right) $ trans (trans (sym $ ringOpIsDistributiveL left (inverse right) right) $ trans (cong {f=(left<.>)} $ groupInverseIsInverseR right) $ ringNeutralIsMultZeroR left) $ sym $ groupInverseIsInverseR $ left<.>right

ringNegationCommutesWithRightMult : VerifiedRing a => (left, right : a) -> (inverse left)<.>right = inverse $ left<.>right
ringNegationCommutesWithRightMult left right = groupOpIsCancellativeR ((inverse left)<.>right) (inverse $ left<.>right) (left<.>right) $ trans (trans (sym $ ringOpIsDistributiveR (inverse left) left right) $ trans (cong {f=(<.>right)} $ groupInverseIsInverseR left) $ ringNeutralIsMultZeroL right) $ sym $ groupInverseIsInverseR $ left<.>right

ringNegationCancelsWithMult : VerifiedRing t
	=> (x, y : t) -> inverse x <.> inverse y = x <.> y
ringNegationCancelsWithMult x y =
	trans (ringNegationCommutesWithRightMult x (inverse y))
	$ trans (cong {f=inverse} $ ringNegationCommutesWithLeftMult x y)
	$ inverseIsInvolution (x <.> y)

ringOpIsDistributiveSubR : VerifiedRing a
	=> {auto ok :
		((<+>) @{vrSemigroupByGrp $ the (VerifiedRing a) %instance})
		= ((<+>) @{vrSemigroupByVMon $ the (VerifiedRing a) %instance})
		}
	-> (l, c, r : a)
	-> (l <-> c) <.> r = l <.> r <-> c <.> r
ringOpIsDistributiveSubR {ok} l c r =
	( (l <-> c) <.> r )
		={ rewrite ok in Refl }=
	( (l <+> inverse c) <.> r )
		={ ringOpIsDistributiveR l (inverse c) r }=
	( l <.> r <+> (inverse c) <.> r )
		={ rewrite sym ok
			in cong $ ringNegationCommutesWithRightMult c r }=
	( l <.> r <-> c <.> r )
		QED
-- (but true by divisibility of addition even without associativity)

ringOpIsDistributiveSubL : VerifiedRing a
	=> {auto ok :
		((<+>) @{vrSemigroupByGrp $ the (VerifiedRing a) %instance})
		= ((<+>) @{vrSemigroupByVMon $ the (VerifiedRing a) %instance})
		}
	-> (l, c, r : a)
	-> l <.> (c <-> r) = l <.> c <-> l <.> r
ringOpIsDistributiveSubL {ok} l c r =
	trans (rewrite ok in ringOpIsDistributiveL l c (inverse r))
	$ rewrite sym ok in cong $ ringNegationCommutesWithLeftMult l r
-- (but true by divisibility of addition even without associativity)


text:
module Main

-------------------------------
-- Define arithmetic
-------------------------------

-- A natural number type --
data Peano = Cero | Prox Peano

-- Addition of our naturals
total
add : Peano -> Peano -> Peano
add x Cero = Cero
add x (Prox y) = Prox (add x y)

-- Multiplication of our naturals.
total
mult : Peano -> Peano -> Peano
mult x Cero = Cero
mult x (Prox y) = add x (mult x y)

-- Differences of naturals.
total
diff: Peano -> Peano -> Maybe Peano
diff x Cero = Just x
diff Cero (Prox y) = Nothing
diff (Prox x) (Prox y) = diff x y

--------------------------------
-- Define needed relations
--------------------------------

-- A less-than type: a < b <=> exists c, a+(c+1)=b
data LT : Peano -> Peano -> Type where
    mkLT : {a:Peano} ->
         {b:Peano} ->
         (c:Peano) ->
         (pf:(add a (Prox c)) = b) -> LT a b

--------------------------------
-- Define needed subsets
--------------------------------

-- A type PN for {n : N | 0<n}
data Pos :Type where
    mkPos: (k:Peano) -> (pf:LT Cero k) -> Pos

-- embed Pos -> Peano
total
Pos2Peano : Pos -> Peano
Pos2Peano (mkPos k pf) = Prox k

-- A type for [n]={k:N | k < n}
data Rng: Peano -> Type where
    mkRng : {n:Peano} -> (k:Peano) -> (pf: LT k n) -> Rng n

-- embed Rng -> Peano
total
Rng2Peano : Rng n -> Peano
Rng2Peano (mkRng k pf) = k

------------------------------
-- Prove division algorithm.
------------------------------

div : (m:Peano) -> (n:Pos) -> (q:Peano**(r:(Rng (Pos2Peano n))**(m=(add (mult q (Pos2Peano n)) (Rng2Peano r)))))
div m n = case (diff m n) of
            Just k =>
            Nothing => (Cero**(mkRng m n))

-- main : IO ()
-- main = return ()

max_stars_repo_name: algeboy/TypedDivision

max_issues_repo_name: algeboy/TypedDivision

max_forks_repo_name: algeboy/TypedDivision


text:
|||
module Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All

import Decidable.Equality

import Data.String
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Do
import Toolkit.Decidable.Informative

import Toolkit.Data.Nat
import Toolkit.Data.Pair
import Toolkit.Data.List.Size
import Toolkit.Data.List.Occurs.Does

import Toolkit.Data.Graph.EdgeBounded

import public Toolkit.Data.Graph.EdgeBounded.DegreeCommon
import public Toolkit.Data.Graph.EdgeBounded.HasExactDegree

%default total

public export
HasExactDegrees : Vertices type -> Edges -> Type
HasExactDegrees vs es = All (\v => HasExactDegree v es) vs

errorHead : {x : type}
         -> {p : type -> Type}
         -> (p x -> Void)
         -> All p (x :: xs) -> Void
errorHead contra (y :: z) = contra y

errorTail : (All p xs -> Void) -> All p (x :: xs) -> Void
errorTail f (y :: z) = f z

all : {type : Type}
   -> {p  : type -> Type}
   -> (f  : (x : type) -> DecInfo e (p x))
   -> (xs : List type)
         -> DecInfo e (All p xs)
all f [] = Yes []
all f (x :: xs) with (f x)
  all f (x :: xs) | (Yes prfWhy) with (all f xs)
    all f (x :: xs) | (Yes prfWhy) | (Yes y)
      = Yes (prfWhy :: y)
    all f (x :: xs) | (Yes prfWhy) | (No msgWhyNot prfWhyNot)
      = No msgWhyNot (errorTail prfWhyNot)

  all f (x :: xs) | (No msgWhyNot prfWhyNot) = No msgWhyNot (errorHead prfWhyNot)

export
hasExactDegrees : {type : Type}
               -> (vs   : Vertices type)
               -> (es   : Edges)
                       -> DecInfo (HasExactDegree.Error type)
                                  (HasExactDegrees vs es)
hasExactDegrees vs es = all (\v => hasExactDegree v es) vs

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- | Exercises on Ranges
module Koans.Ranges

rangeNums : Bool
rangeNums = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] == [1..13]

stepUp : Bool
stepUp = [3, 6, 9, 12, 15, 18] == [3,6..20]

-- stepDown : Bool
-- stepDown = False == [20,17..1]

stopMe : List Integer
stopMe = take 5 [1..]

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

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
module Cursor

import Data.Fin

%default total

public export
data Cursor : Nat -> Type where
  MkCursor : Nat -> Fin n -> Cursor n

export
right : Cursor n -> Cursor n
right (MkCursor x y) = MkCursor (S x) y

export
left : Cursor n -> Cursor n
left (MkCursor (S x) y) = MkCursor x y
left (MkCursor Z y) = MkCursor Z y

dec : Fin n -> Fin n
dec FZ = FZ
dec (FS k) = weaken k

export
up : Cursor n -> Cursor n
up (MkCursor x y) = MkCursor x (dec y)

export
down : Cursor n -> Cursor (S n)
down (MkCursor x y) = MkCursor x (shift 1 y)

export
downInBounds : Cursor n -> Cursor n
downInBounds originalCursor@(MkCursor x y) =
  case strengthen $ shift 1 y of
    Left _ => originalCursor
    Right newY => MkCursor x newY

--todo: is it possible to use something like strengthenN and shift?
export
downWithnInBounds : Nat -> Cursor n -> Cursor n
downWithnInBounds d originalCursor@(MkCursor x y) {n} =
  case natToFin ((finToNat y) + d) n of
    Nothing => originalCursor
    Just newY => MkCursor x newY

export
lineStart : Cursor n -> Cursor n
lineStart (MkCursor _ y) = MkCursor Z y

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
main : JS_IO ()
main = putStr' "ola"


text:
module System.Concurrency

import Data.IORef

%default total

-- At the moment this is pretty fundamentally tied to the Scheme RTS.
-- Given that different back ends will have entirely different threading
-- models, it might be unavoidable, but we might want to think about possible
-- primitives that back ends should support.

-- Thread mailboxes

%foreign "scheme:blodwen-set-thread-data"
prim__setThreadData : {a : Type} -> a -> PrimIO ()
%foreign "scheme:blodwen-get-thread-data"
prim__getThreadData : (a : Type) -> PrimIO a

export
setThreadData : HasIO io => {a : Type} -> a -> io ()
setThreadData val = primIO (prim__setThreadData val)

export
getThreadData : HasIO io => (a : Type) -> io a
getThreadData a = primIO (prim__getThreadData a)

-- Mutexes

export
data Mutex : Type where [external]

%foreign "scheme:blodwen-make-mutex"
prim__makeMutex : PrimIO Mutex
%foreign "scheme:blodwen-mutex-acquire"
prim__mutexAcquire : Mutex -> PrimIO ()
%foreign "scheme:blodwen-mutex-release"
prim__mutexRelease : Mutex -> PrimIO ()

||| Creates and returns a new mutex.
export
makeMutex : HasIO io => io Mutex
makeMutex = primIO prim__makeMutex

||| Acquires the mutex identified by `mutex`. The thread blocks until the mutex
||| has been acquired.
|||
||| Mutexes are recursive in Posix threads terminology, which means that the
||| calling thread can use mutex-acquire to (re)acquire a mutex it already has.
||| In this case, an equal number of mutex-release calls is necessary to release
||| the mutex.
export
mutexAcquire : HasIO io => Mutex -> io ()
mutexAcquire m = primIO (prim__mutexAcquire m)

||| Releases the mutex identified by `mutex`. Unpredictable behavior results if
||| the mutex is not owned by the calling thread.
export
mutexRelease : HasIO io => Mutex -> io ()
mutexRelease m = primIO (prim__mutexRelease m)

-- Condition variables

export
data Condition : Type where [external]

%foreign "scheme,racket:blodwen-make-cv"
         "scheme,chez:blodwen-make-condition"
prim__makeCondition : PrimIO Condition

%foreign "scheme,racket:blodwen-cv-wait"
         "scheme,chez:blodwen-condition-wait"
prim__conditionWait : Condition -> Mutex -> PrimIO ()

%foreign "scheme,chez:blodwen-condition-wait-timeout"
--         "scheme,racket:blodwen-cv-wait-timeout"
prim__conditionWaitTimeout : Condition -> Mutex -> Int -> PrimIO ()

%foreign "scheme,racket:blodwen-cv-signal"
         "scheme,chez:blodwen-condition-signal"
prim__conditionSignal : Condition -> PrimIO ()

%foreign "scheme,racket:blodwen-cv-broadcast"
         "scheme,chez:blodwen-condition-broadcast"
prim__conditionBroadcast : Condition -> PrimIO ()

||| Creates and returns a new condition variable.
export
makeCondition : HasIO io => io Condition
makeCondition = primIO prim__makeCondition

||| Waits up to the specified timeout for the condition identified by the
||| condition variable `cond`. The calling thread must have acquired the mutex
||| identified by `mutex` at the time `conditionWait` is called. The mutex is
||| released as a side effect of the call to `conditionWait`. When a thread is
||| later released from the condition variable by one of the procedures
||| described below, the mutex is reacquired and `conditionWait` returns.
export
conditionWait : HasIO io => Condition -> Mutex -> io ()
conditionWait cond mutex = primIO (prim__conditionWait cond mutex)

||| Variant of `conditionWait` with a timeout in microseconds.
||| When the timeout expires, the thread is released, `mutex` is reacquired, and
||| `conditionWaitTimeout` returns.
export
conditionWaitTimeout : HasIO io => Condition -> Mutex -> Int -> io ()
conditionWaitTimeout cond mutex timeout = primIO (prim__conditionWaitTimeout cond mutex timeout)

||| Releases one of the threads waiting for the condition identified by `cond`.
export
conditionSignal : HasIO io => Condition -> io ()
conditionSignal c = primIO (prim__conditionSignal c)

||| Releases all of the threads waiting for the condition identified by `cond`.
export
conditionBroadcast : HasIO io => Condition -> io ()
conditionBroadcast c = primIO (prim__conditionBroadcast c)

-- Semaphores

export
data Semaphore : Type where [external]

%foreign "scheme:blodwen-make-semaphore"
prim__makeSemaphore : Int -> PrimIO Semaphore
%foreign "scheme:blodwen-semaphore-post"
prim__semaphorePost : Semaphore -> PrimIO ()
%foreign "scheme:blodwen-semaphore-wait"
prim__semaphoreWait : Semaphore -> PrimIO ()

||| Creates and returns a new semaphore with the counter initially set to `init`.
export
makeSemaphore : HasIO io => Int -> io Semaphore
makeSemaphore init = primIO (prim__makeSemaphore init)

||| Increments the semaphore's internal counter.
export
semaphorePost : HasIO io => Semaphore -> io ()
semaphorePost sema = primIO (prim__semaphorePost sema)

||| Blocks until the internal counter for semaphore sema is non-zero. When the
||| counter is non-zero, it is decremented and `semaphoreWait` returns.
export
semaphoreWait : HasIO io => Semaphore -> io ()
semaphoreWait sema = primIO (prim__semaphoreWait sema)

-- Barriers

||| A barrier enables multiple threads to synchronize the beginning of some
||| computation.
export
data Barrier : Type where [external]

%foreign "scheme:blodwen-make-barrier"
prim__makeBarrier : Int -> PrimIO Barrier
%foreign "scheme:blodwen-barrier-wait"
prim__barrierWait : Barrier -> PrimIO ()

||| Creates a new barrier that can block a given number of threads.
export
makeBarrier : HasIO io => Int -> io Barrier
makeBarrier numThreads = primIO (prim__makeBarrier numThreads)

||| Blocks the current thread until all threads have rendezvoused here.
export
barrierWait : HasIO io => Barrier -> io ()
barrierWait barrier = primIO (prim__barrierWait barrier)

-- Channels

export
data Channel : Type -> Type where [external]

%foreign "scheme:blodwen-make-channel"
prim__makeChannel : PrimIO (Channel a)
%foreign "scheme:blodwen-channel-get"
prim__channelGet : Channel a -> PrimIO a
%foreign "scheme:blodwen-channel-put"
prim__channelPut : Channel a -> a -> PrimIO ()

||| Creates and returns a new channel. The channel can be used with channelGet
||| to receive a value through the channel. The channel can be used with
||| channelPut to send a value through the channel.
export
makeChannel : HasIO io => io (Channel a)
makeChannel = primIO prim__makeChannel

||| Blocks until a sender is ready to provide a value through `chan`. The result
||| is the sent value.
export
channelGet : HasIO io => Channel a -> io a
channelGet chan = primIO (prim__channelGet chan)

||| CAUTION: Different behaviour under chez and racket:
||| - Chez: Puts a value on the channel. If there already is a value, blocks
|||         until that value has been received.
||| - Racket: Blocks until a receiver is ready to accept the value `val` through
|||           `chan`.
export
channelPut : HasIO io => Channel a -> a -> io ()
channelPut chan val = primIO (prim__channelPut chan val)


text:
module WebAssembly.Validation.Modules.DataSegments

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Instructions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#data-segments)
|||
||| ```
||| C.mems[x] = limits    C ⊢ expr : [i32]    C ⊢ expr const
||| --------------------------------------------------------
||| C ⊢ {data x, offset expr, init b*} ok
||| ```
public export
data ValidData : Context -> Data -> Type where
  MkValidData  : (c : Context)
              -> (x : MemIdx)
              -> (expr : Expr)
              -> (bs : List Byte)
              -> {auto in_bounds: InBounds x (mems c)}
              -> ValidSequence c expr ([] ->> [TI32])
              -> ConstExpr c expr
              -> ValidData c (MkData x expr bs)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 4

import Data.Vect

-- check that all functions are total
%default total

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

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

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

addToStore : DataStore -> String -> DataStore
addToStore (MkData size store) newItem = MkData (S size) (addToData store)
  where
    addToData : Vect oldsize String -> Vect (S oldsize) String
    addToData [] = [newItem]
    addToData (x :: xs) = x :: addToData xs

||| Supported commands
data Command = ||| Add an item
               Add String
             | ||| Get an item by its id
               Get Integer
             | ||| Search an item
               Search String
             | ||| Get the number of items
               Size
             | |||| Quit
               Quit

parseCommand : String -> String -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "search" str = Just (Search str)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

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

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store
  = let store_items = items store in
      case integerToFin pos (size store) of
        Nothing => Just ("Out of range \n", store)
        Just id => Just ((index id store_items) ++ "\n", store)

findFromSubstring : (store : DataStore) -> (str : String) -> List (Nat, String)
findFromSubstring store str = helper (items store) str 0
  where
    helper : Vect n String -> String -> Nat -> List (Nat, String)
    helper [] _ _ = []
    helper (x :: xs) s k = case isInfixOf s x of
                                False => helper xs s (S k)
                                True => (k, x) :: helper xs s (S k)

presentResults : List (Nat, String) -> String
presentResults results = foldl (++) "" $ map helper results
  where
    helper : (Nat, String) -> String
    helper (x, res) = show x ++ ": " ++ res ++ "\n"

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
  = case parse input of
        Nothing => Just ("Invalid command\n", store)
        Just (Add item) =>
          Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
        Just (Get pos) => getEntry pos store
        Just (Search str) =>
          let foundItems = findFromSubstring store str in
            Just (presentResults foundItems, store)
        Just Size => Just (show (size store) ++ "\n", store)
        Just Quit => Nothing

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


text:
module Dummy

import Erlang.System.Directory

main : IO ()
main = do
  True <- dirExists "custom_build"
    | False => putStrLn "Could not find build directory"
  putStrLn "Found build directory"


text:
> module NonNegRational.tests.Main

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Fraction.Fraction
> import PNat.PNat
> import Nat.Positive

> %default total
> %auto_implicits off

> postulate sumOneLemma : {m, n, d : Nat} -> m + n = S d ->
>                         fromFraction (m, Element (S d) MkPositive)
>                         +
>                         fromFraction (n, Element (S d) MkPositive)
>                         =
>                         1

> n1 : Nat
> n1 = 1

> n2 : Nat
> n2 = 3

> d  : Nat
> d  = 3

> x  : NonNegRational
> x  = fromFraction (n1, Element (S d) MkPositive)

> y  : NonNegRational
> y  = fromFraction (n2, Element (S d) MkPositive)

> postulate h : n1 + n2 = S d

> p : x + y = 1
> p = NonNegRational.tests.Main.sumOneLemma {m = n1} {n = n2} {d = d} h

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module Void.Properties

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Sigma.Sigma

> %default total

> %access public export

> ||| Mapping |Void|s to |Fin|s
> toFin : Void -> Fin Z
> toFin = void
> %freeze toFin

> ||| Mapping |Fin Z|s to |Void|s
> fromFin : Fin Z -> Void
> fromFin k = absurd k
> %freeze fromFin

> ||| |toFin| is the left-inverse of |fromFin|
> toFinFromFinLemma : (k : Fin Z) -> toFin (fromFin k) = k
> toFinFromFinLemma k = absurd k
> %freeze toFinFromFinLemma

> ||| |fromFin| is the left-inverse of |toFin|
> fromFinToFinLemma : (e : Void) -> fromFin (toFin e) = e
> fromFinToFinLemma e = void e
> %freeze fromFinToFinLemma

> ||| Void is finite
> finiteVoid : Finite Void
> finiteVoid = MkSigma Z iso where
>   iso : Iso Void (Fin Z)
>   iso = MkIso toFin fromFin toFinFromFinLemma fromFinToFinLemma

> ||| Void is decidable
> decidableVoid : Dec Void
> decidableVoid = No void

> {-

> ---}


text:
module Node.FS.Stream

import Node.FS

data ReadStream : Type where [external]

%foreign "node:lambda: (fs,path)=>fs.createReadStream(path)"
ffi_createReadStream : FS -> String -> PrimIO ReadStream

export
createReadStream : HasIO io => { auto fs : FS } -> String -> io ReadStream
createReadStream path = primIO $ ffi_createReadStream fs path

%foreign "node:lambda: (ty, req, data) => { req.on('data', a => data(a)()) }"
ffi_onData : ReadStream -> (a -> PrimIO ()) -> PrimIO ()

export
(.onData) : HasIO io => ReadStream -> (a -> IO ()) -> io ()
(.onData) req cb = primIO $ ffi_onData req $ \a => toPrim $ cb a

%foreign "node:lambda: (req, end) => { req.on('end', () => end()()) }"
ffi_onEnd : ReadStream -> (() -> PrimIO ()) -> PrimIO ()

export
(.onEnd) : HasIO io => ReadStream -> (() -> IO ()) -> io ()
(.onEnd) req cb = primIO $ ffi_onEnd req $ \_ => toPrim $ cb ()

%foreign "node:lambda: (ty, req, error) => { req.on('error', e => error(e)()) }"
ffi_onError : ReadStream -> (e -> PrimIO ()) -> PrimIO ()

export
(.onError) : HasIO io => ReadStream -> (e -> IO ()) -> io ()
(.onError) req cb = primIO $ ffi_onError req $ \e => toPrim $ cb e

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module CFT.Zippers

import CFT
import Datatypes

namespace Zipper
  public export
  data ZList a = MkZipper (List a) (List a)

  moveRight : ZList a -> ZList a
  moveRight ls@(MkZipper xs []) = ls
  moveRight (MkZipper xs (x :: ys)) = MkZipper (x :: xs) ys

  moveLeft : ZList a -> ZList a
  moveLeft ls@(MkZipper [] ys) = ls
  moveLeft (MkZipper (x :: xs) ys) = MkZipper xs (x :: ys)

  cycleR : ZList a -> ZList a
  cycleR (MkZipper xs []) = MkZipper [] (reverse xs)
  cycleR (MkZipper xs (x :: ys)) = MkZipper (x :: xs) ys

namespace ZipperDesc
  public export
  TZip : {n : _} -> CFT (S n)
  TZip = TList * TList

  tMoveRight : Ty TZip (a :: t) -> Ty TZip (a :: t)
  tMoveRight (Pair x (In (Left Unit))) = Pair x (In (Left Unit))
  tMoveRight (Pair x (In (Right (Pair (Pop (Top y)) (Top z)))))  = Pair (cons y x) z

toList : Ty TList (a :: t) -> List (Ty a t)
toList (In (Left Unit)) = []
toList (In (Right (Pair (Pop (Top x)) (Top y)))) = x :: toList y

fromList : List (Ty a t) -> Ty TList (a :: t)
fromList [] = In (Left Unit)
fromList (x :: xs) = cons x (fromList xs)

pairInj : (f : Ty TList (a :: t) -> Ty TList (a :: t)) -> fromList (toList y) = y -> CFT.fromList (CFT.toList (f y)) = f y
pairInj f prf = ?pairInj_rhs

toFromList : (x : Ty (Mu (One + (VS VZ * VZ))) (a :: t)) -> fromList (toList x) = x
toFromList (In (Left Unit)) = Refl
toFromList (In (Right (Pair x (Top y)))) = let result = toFromList y in
                                             pairInj (In . Right . Pair x . Top) result

fromToList : (x : List (Ty a t)) -> CFT.toList (fromList x) = x
fromToList [] = Refl
fromToList (x :: xs) = let rec = fromToList xs in cong (x :: ) rec

ListTListIso : Iso (List (Ty a t)) (Ty TList (a :: t))
ListTListIso = MkIso
  { to = fromList
  , from = toList
  , toFrom = toFromList
  , fromTo = fromToList
  }

fromZList : ZList (Ty a t) -> Ty TZip (a :: t)
fromZList (MkZipper xs ys) = Pair (fromList xs) (fromList ys)

toZList : Ty TZip (a :: t) -> ZList (Ty a t)
toZList (Pair x y) = MkZipper (toList x) (toList y)

toFromZList : (x : Ty TZip (a :: t)) -> fromZList (toZList x) = x
toFromZList (Pair x y) = ?toFromZList_rhs_1

ZListTZipIso : Iso (ZList (Ty a t)) (Ty TZip (a :: t))
ZListTZipIso = MkIso
  { to = fromZList
  , from = toZList
  , toFrom = toFromZList
  , fromTo = ?aiod
  }

derive : {n : _} -> Fin n -> CFT n -> CFT n
derive FZ     VZ = One
derive (FS x) VZ = Zero
derive FZ     (VS y) = Zero
derive (FS x) (VS y) = Zero
derive n      (App f x) = App (derive (FS n) f) x
                        + App (derive FZ f) x * derive n x
derive n      Zero = Zero
derive n      One = Zero
derive n      (a + b) = derive n a + derive n b
derive n      (a * b) = derive n a * b + a * derive n b
derive n      (Mu f) = App TList (App (derive FZ f) (Mu f))
                     * App (derive (FS n) f) (Mu f)

DerivedList : CFT 1
DerivedList = derive FZ TList

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module TTImp.Elab.Utils

import Core.Context
import Core.Core
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.TTImp

%default covering

detagSafe : {auto c : Ref Ctxt Defs} ->
            Defs -> NF [] -> Core Bool
detagSafe defs (NTCon _ n _ _ args)
    = do Just (TCon _ _ _ _ _ _ _ (Just detags)) <- lookupDefExact n (gamma defs)
              | _ => pure False
         args' <- traverse (evalClosure defs) args
         pure $ notErased 0 detags args'
  where
    -- if any argument positions are in the detaggable set, and unerased, then
    -- detagging is safe
    notErased : Nat -> List Nat -> List (NF []) -> Bool
    notErased i [] _ = True -- Don't need an index available
    notErased i ns [] = False
    notErased i ns (NErased _ True :: rest)
        = notErased (i + 1) ns rest -- Can't detag here, look elsewhere
    notErased i ns (_ :: rest) -- Safe to detag via this argument
        = elem i ns || notErased (i + 1) ns rest
detagSafe defs _ = pure False

findErasedFrom : {auto c : Ref Ctxt Defs} ->
                 Defs -> Nat -> NF [] -> Core (List Nat, List Nat)
findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
    = do -- In the scope, use 'Erased fc True' to mean 'argument is erased'.
         -- It's handy here, because we can use it to tell if a detaggable
         -- argument position is available
         sc <- scf defs (toClosure defaultOpts [] (Erased fc (isErased c)))
         (erest, dtrest) <- findErasedFrom defs (1 + pos) sc
         let dt' = if !(detagSafe defs aty)
                      then (pos :: dtrest) else dtrest
         pure $ if isErased c
                   then (pos :: erest, dt')
                   else (erest, dt')
findErasedFrom defs pos tm = pure ([], [])

-- Find the argument positions in the given type which are guaranteed to be
-- erasable
export
findErased : {auto c : Ref Ctxt Defs} ->
             ClosedTerm -> Core (List Nat, List Nat)
findErased tm
    = do defs <- get Ctxt
         tmnf <- nf defs [] tm
         findErasedFrom defs 0 tmnf

export
updateErasable : {auto c : Ref Ctxt Defs} ->
                 Name -> Core ()
updateErasable n
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure ()
         (es, dtes) <- findErased (type gdef)
         addDef n (record { eraseArgs = es,
                            safeErase = dtes } gdef)
         pure ()
export
wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a
wrapErrorC opts err
    = if InCase `elem` opts
         then id
         else wrapError err

plicit : Binder (Term vars) -> PiInfo RawImp
plicit (Pi _ _ p _) = forgetDef p
plicit (PVar _ _ p _) = forgetDef p
plicit _ = Explicit

export
bindNotReq : {vs : _} ->
             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
             List (PiInfo RawImp, Name) ->
             Term vs -> (List (PiInfo RawImp, Name), Term pre)
bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
bindNotReq fc i (b :: env) SubRefl ns tm
   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
         (ns', refToLocal (MN "arg" i) _ btm)
bindNotReq fc i (b :: env) (KeepCons p) ns tm
   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
         (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
         (ns', refToLocal (MN "arg" i) _ btm)
bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
   = bindNotReq fc i env p ((plicit b, n) :: ns)
       (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b)) tm)

export
bindReq : {vs : _} ->
          FC -> Env Term vs -> (sub : SubVars pre vs) ->
          List (PiInfo RawImp, Name) ->
          Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)
bindReq {vs} fc env SubRefl ns tm
    = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
  where
    notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
    notLets acc [] _ = acc
    notLets acc (v :: vs) (b :: env) = if isLet b then notLets acc vs env
                                       else notLets (v :: acc) vs env
bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
    = do b' <- shrinkBinder b p
         bindReq fc env p ((plicit b, n) :: ns)
            (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b')) tm)
bindReq fc (b :: env) (DropCons p) ns tm
    = bindReq fc env p ns tm


text:
module Control.Lens.Review
import Data.Contravariant
import Control.Lens.Types
import Control.Lens.Getter
import Control.Monad.Identity
import Data.Profunctor
import Data.Tagged

%default total
%access public export

infixr 8 #

(#) : AReview t b -> b -> t
(#) p = runIdentity . untag . p . MkTagged . Id

re : AReview t b -> Getter b t
re p = to (p #)

max_stars_repo_name: andrevidela/idris-lens

max_issues_repo_name: andrevidela/idris-lens

max_forks_repo_name: andrevidela/idris-lens


text:
module Inigo.Async.Archive

import Data.Buffer
import Data.List
import Data.Maybe
import Data.String
import Extra.Buffer
import Extra.String
import Fmt
import Inigo.Archive.Archive as Archive
import Inigo.Archive.Path
import Inigo.Async.Base
import Inigo.Async.Compress.Brotli
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.Package
import System
import System.Path

-- Simple archive format for storing files compressed in Toml files

-- Overall, this file is still a bit complex and does
-- too much in promises, but it's a start

compressFileEnc64 : String -> Promise String
compressFileEnc64 path =
  do
    compressed <- compressFile path
    liftIO $ enc64 compressed

export
buildArchive : Package -> String -> Promise String
buildArchive package rootPath =
  do
    allFiles <- fs_getFilesR rootPath
    -- We're going to skip `ipkg` files
    let files = ignoreFiles allFiles
    enc <- all (map encodeFile files)
    pure (Archive.encode enc)
  where
    encodeFile : String -> Promise (List String, String)
    encodeFile file =
      do
        res <- compressFileEnc64 file
        let relPath = fromMaybe "" $ Path.dropBase rootPath file
        log (fmt "Archiving %s..." relPath)
        pure (splitPath relPath, res)

export
saveArchive : Package -> String -> String -> Promise ()
saveArchive package rootPath outFile =
  do
    contents <- buildArchive package rootPath
    fs_writeFile outFile contents
    log ("Wrote archive " ++ outFile)

decompressFile : String -> (List String, String) -> Promise ()
decompressFile outPath (filename, compressed) =
  do
    let resultFile = outPath </> (joinPath filename)
    buffer <- liftIO $ dec64 compressed
    res <- decompress buffer
    log ("Decompressing " ++ resultFile ++ "...")
    pure ()
    let resultDir = fromMaybe "" $ parent resultFile
    fs_mkdir True resultDir
    fs_writeFileBuf resultFile res

expect : String -> Maybe a -> Promise a
expect msg (Just val) = pure val
expect msg Nothing = reject msg

export
extractArchive : Buffer -> String -> Promise ()
extractArchive archive outPath =
  do
    contents <- liftIO (readAll archive)
    files <- expect "Failed to read archive" (Archive.decode contents)
    ignore $ all (map (decompressFile outPath) files)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Intro

sm : List Nat -> Nat
sm [] = 0
sm (x :: xs) = x + (sm xs)

fct : Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)

fbp : Nat -> (Nat, Nat)
fbp Z = (1, 1)
fbp (S k) = (snd (fbp k), fst (fbp k) + snd (fbp k))

fib : Nat -> Nat
fib n = fst (fbp n)

add : Nat -> Nat -> Nat
add Z j = j
add (S k) j = S (add k j)

mul : Nat -> Nat -> Nat
mul Z j = Z
mul (S k) j = add j (mul k j)

sub : (n: Nat) -> (m : Nat) -> (LTE m n) -> Nat
sub n Z LTEZero = n
sub (S right) (S left) (LTESucc x) = sub right left x


text:
module Complex

import Control.Monad.TransitionIndexed
import Control.Monad.TransitionIndexed.Do

data Substate = Sub1 | Sub2

data ComplexState = First Substate | Second | Third

data IsFirst : ComplexState -> Type where
  ItIsFirst : IsFirst (First _)

||| Result of moving from Second to Third state
data Trans2Result = OK | Error

data ComplexCmd : (ty : Type) ->
                  ComplexState ->
                  (ty -> ComplexState) ->
                  Type where
  Init       :              ComplexCmd () (First Sub1) (const (First Sub1))
  SubTrans   :              ComplexCmd () (First Sub1) (const (First Sub2))
  Trans1Easy : IsFirst s => ComplexCmd () s (const Second)
  Trans1Hard :              ComplexCmd () (First Sub2) (const Second)
  Trans2     :              ComplexCmd Trans2Result Second (\case OK => Third; Error => Second)
  Cheat      :              ComplexCmd () Second (const Third)

  Pure : (res : ty) -> ComplexCmd ty (state_fn res) state_fn
  Bind : ComplexCmd a state1 state2_fn ->
          ((res: a) -> ComplexCmd b (state2_fn res) state3_fn) ->
          ComplexCmd b state1 state3_fn

TransitionIndexedPointed ComplexState ComplexCmd where
  pure = Pure

TransitionIndexedMonad ComplexState ComplexCmd where
  bind = Bind

easyProg : ComplexCmd () (First Sub1) (const Third)
easyProg = do
  Init
  Trans1Easy
  OK <- Trans2
    | Error => Cheat
  Pure ()

hardProg : ComplexCmd () (First Sub1) (const Third)
hardProg = do
  Init
  SubTrans
  Trans1Hard
  res <- Trans2
  case res of
       OK => Pure ()
       Error => Cheat

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
-- Module      : Itea.Dom.Primitives
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Dom.Primitives
import Itea.Html
import Itea.Html.Events
import Itea.Html.Attributes
import Itea.Javascript.Types
import Itea.Utils
-- This part is full of belive_me as it's required when working with opaque
-- types. Type safety is regained by the node type preventing any other place
-- than the DOM from taking a DOM pointer. The lack of constructors here is for
-- performance as wrapping JS values in a data type won't really change much
-- since they're opaque.

%default covering
%access export

||| The opaque type representing a DOM node
Node : Type
Node = JSRef 'Node

believeIO : JS_IO Ptr -> JS_IO a
believeIO = believe_me

document : JS_IO Node
document = believeIO $ jscall "document" _

documentBody : JS_IO Node
documentBody = believeIO $ jscall "document.body" _

createTextNode : String -> JS_IO Node
createTextNode = believeIO . jscall "document.createTextNode(%0)" _

createElement : String -> JS_IO Node
createElement = believeIO . jscall "document.createElement(%0)" _

setInnerHtml : Node -> String -> JS_IO ()
setInnerHtml node = jscall "%0.setInnerHTML = %1"
                           (Ptr -> String -> JS_IO ())
                           (believe_me node)

getElementById : String -> JS_IO Node
getElementById = believeIO . jscall "document.getElementById(%0)" _

nthChild : Node -> Int -> JS_IO Node
nthChild node = believeIO . jscall "%0.childNodes[%0]"
                                   (Ptr -> Int -> JS_IO Ptr)
                                   (believe_me node)

appendChild : Node -> Node -> JS_IO Node
appendChild parent child =
  believeIO $ jscall "%0.appendChild(%1)"
                     (Ptr -> Ptr -> JS_IO Ptr)
                     (believe_me parent)
                     (believe_me child)

replaceChild : Node -> Node -> Node -> JS_IO ()
replaceChild parent old new =
  jscall "%0.replaceChild(%1,%2)"
         (Ptr -> Ptr -> Ptr -> JS_IO ())
         (believe_me parent)
         (believe_me old)
         (believe_me new)

removeChild : Node -> Node -> JS_IO Node
removeChild parent child =
  believeIO $ jscall "%0.removeChild(%1)"
                     (Ptr -> Ptr -> JS_IO Ptr)
                     (believe_me parent)
                     (believe_me child)

setAttribute : Node -> String -> String -> JS_IO ()
setAttribute node = jscall "%0.setAttribute(%1,%2)"
                           (Ptr -> String -> String -> JS_IO ())
                           (believe_me node)

removeAttribute : Node -> String -> JS_IO ()
removeAttribute node =
  jscall "%0.removeAttribute(%1)"
         (Ptr -> String -> JS_IO ())
         (believe_me node)

addEventListener : Node
                -> String
                -> JsFn (Ptr -> JS_IO ())
                -> JSRef 'EventOptions
                -> JS_IO ()
addEventListener node name fn opt =
  jscall "%0.addEventListener(%1,%2,%3)"
         (Ptr -> String -> JsFn (Ptr -> JS_IO ()) -> Ptr -> JS_IO ())
         (believe_me node) name fn (believe_me opt)

removeEventListener : Node
                   -> String
                   -> JsFn (Ptr -> JS_IO ())
                   -> JSRef 'EventOptions
                   -> JS_IO ()
removeEventListener node name fn opt =
  jscall "%0.removeEventListener(%1,%2,%3)"
         (Ptr -> String -> JsFn (Ptr -> JS_IO ()) -> Ptr -> JS_IO ())
         (believe_me node) name fn (believe_me opt)

addEventHandler : Node -> Event a -> JS_IO ()
addEventHandler node (MkEvent name handler options) =
  addEventListener node name handler options

updateAttributes : Node
                -> List (String, String)
                -> List (String, String)
                -> JS_IO ()
updateAttributes node old new =
  do traverse_ (removeAttribute node . fst) old
     traverse_ (uncurry $ setAttribute node) new

createDomNode : HTML a -> JS_IO Node
createDomNode (HtmlElem tagname events attributes html) =
  do nodes <- traverse createDomNode html
     tag   <- createElement tagname
     traverse_ (addEventHandler tag) events
     updateAttributes tag [] attributes
     traverse_ (appendChild tag) nodes
     pure tag
createDomNode (HtmlText text) =
  createTextNode text

render : Node -> Maybe (HTML a) -> Maybe (HTML a) -> JS_IO ()
render root old new = renderList (indexed $ toList old) (toList new)
  -- TODO diffing
  where

    renderList : List (Int, HTML a) -> List (HTML a) -> JS_IO ()
    renderList old new = setInnerHtml root ""
                      *> traverse createDomNode new
                      >>= traverse_ (appendChild root)

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea