text:
module Language.LSP.Message.Workspace

import Data.SortedMap
import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
public export
record TextEdit where
  constructor MkTextEdit
  range   : Range
  newText : String
%runElab deriveJSON defaultOpts `{TextEdit}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
public export
record ChangeAnnotation where
  constructor MkChangeAnnotation
  label             : String
  needsConfirmation : Maybe Bool
  description       : Maybe String
%runElab deriveJSON defaultOpts `{ChangeAnnotation}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
public export
ChangeAnnotationIdentifier : Type
ChangeAnnotationIdentifier = String

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textEdit
public export
record AnnotatedTextEdit where
  constructor MkAnnotatedTextEdit
  range        : Range
  newText      : String
  annotationId : ChangeAnnotationIdentifier
%runElab deriveJSON defaultOpts `{AnnotatedTextEdit}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentEdit
public export
record TextDocumentEdit where
  constructor MkTextDocumentEdit
  textDocument : OptionalVersionedTextDocumentIdentifier
  edits        : List (OneOf [TextEdit, AnnotatedTextEdit])
%runElab deriveJSON defaultOpts `{TextDocumentEdit}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record InsertReplaceEdit where
  constructor MkInsertReplaceEdit
  newText : String
  insert  : Range
  replace : Range
%runElab deriveJSON defaultOpts `{InsertReplaceEdit}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record CreateFileOptions where
  constructor MkCreateFileOptions
  overwrite      : Maybe Bool
  ignoreIfExists : Maybe Bool
%runElab deriveJSON defaultOpts `{CreateFileOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record RenameFileOptions where
  constructor MkRenameFileOptions
  overwrite      : Maybe Bool
  ignoreIfExists : Maybe Bool
%runElab deriveJSON defaultOpts `{RenameFileOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record DeleteFileOptions where
  constructor MkDeleteFileOptions
  recursive         : Maybe Bool
  ignoreIfNotExists : Maybe Bool
%runElab deriveJSON defaultOpts `{DeleteFileOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record CreateFile where
  constructor MkCreateFile
  uri          : DocumentURI
  options      : Maybe CreateFileOptions
  annotationId : ChangeAnnotationIdentifier
%runElab deriveJSON (record {staticFields = [("kind", JString "create")]} defaultOpts) `{CreateFile}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record RenameFile where
  constructor MkRenameFile
  oldUri       : DocumentURI
  newUri       : DocumentURI
  options      : Maybe RenameFileOptions
  annotationId : ChangeAnnotationIdentifier
%runElab deriveJSON (record {staticFields = [("kind", JString "rename")]} defaultOpts) `{RenameFile}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#resourceChanges
public export
record DeleteFile where
  constructor MkDeleteFile
  uri          : DocumentURI
  options      : Maybe DeleteFileOptions
  annotationId : ChangeAnnotationIdentifier
%runElab deriveJSON (record {staticFields = [("kind", JString "delete")]} defaultOpts) `{DeleteFile}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEdit
public export
record WorkspaceEdit where
  constructor MkWorkspaceEdit
  changes           : Maybe (SortedMap DocumentURI (List TextEdit))
  documentChanges   : Maybe (List (OneOf [TextDocumentEdit, CreateFile, RenameFile, DeleteFile]))
  changeAnnotations : Maybe (SortedMap String ChangeAnnotation)
%runElab deriveJSON defaultOpts `{WorkspaceEdit}

namespace ResourceOperationKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
  public export
  data ResourceOperationKind = Create | Rename | Delete

export
ToJSON ResourceOperationKind where
  toJSON Create = JString "create"
  toJSON Rename = JString "rename"
  toJSON Delete = JString "delete"

export
FromJSON ResourceOperationKind where
  fromJSON (JString "create") = pure Create
  fromJSON (JString "rename") = pure Rename
  fromJSON (JString "delete") = pure Delete
  fromJSON _ = neutral

namespace FailureHandlingKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
  public export
  data FailureHandlingKind = Abort | Transactional | Undo | TextOnlyTransactional

export
ToJSON FailureHandlingKind where
  toJSON Abort                 = JString "abort"
  toJSON Transactional         = JString "transactional"
  toJSON Undo                  = JString "undo"
  toJSON TextOnlyTransactional = JString "textOnlyTransactional"

export
FromJSON FailureHandlingKind where
  fromJSON (JString "abort")                 = pure Abort
  fromJSON (JString "transactional")         = pure Transactional
  fromJSON (JString "undo")                  = pure Undo
  fromJSON (JString "textOnlyTransactional") = pure TextOnlyTransactional
  fromJSON _ = neutral

namespace WorkspaceEditClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
  public export
  record ChangeAnnotationSupport where
    constructor MkChangeAnnotationSupport
    groupsOnLabel : Maybe Bool
  %runElab deriveJSON defaultOpts `{ChangeAnnotationSupport}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspaceEditClientCapabilities
public export
record WorkspaceEditClientCapabilities where
  constructor MkWorkspaceEditClientCapabilities
  documentChanges         : Maybe Bool
  resourceOperations      : Maybe (List ResourceOperationKind)
  failureHandling         : Maybe FailureHandlingKind
  normalizesLineEndings   : Maybe Bool
  changeAnnotationSupport : Maybe ChangeAnnotationSupport
%runElab deriveJSON defaultOpts `{WorkspaceEditClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders
public export
record WorkspaceFoldersServerCapabilities where
  constructor MkWorkspaceFoldersServerCapabilities
  supported           : Maybe Bool
  changeNotifications : Maybe (OneOf [String, Bool])
%runElab deriveJSON defaultOpts `{WorkspaceFoldersServerCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_workspaceFolders
public export
record WorkspaceFolder where
  constructor MkWorkspaceFolder
  uri  : DocumentURI
  name : String
%runElab deriveJSON defaultOpts `{WorkspaceFolder}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders
public export
interface WorkspaceFoldersChangeEvent where
  added   : List WorkspaceFolder;
  removed : List WorkspaceFolder;
%runElab deriveJSON defaultOpts `{WorkspaceFoldersChangeEvent}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWorkspaceFolders
public export
record DidChangeWorkspaceFoldersParams where
  constructor MkDidChangeWorkspaceFoldersParams
  event : WorkspaceFoldersChangeEvent
%runElab deriveJSON defaultOpts `{DidChangeWorkspaceFoldersParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration
public export
record DidChangeConfigurationClientCapabilities where
  constructor MkDidChangeConfigurationClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{DidChangeConfigurationClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeConfiguration
public export
record DidChangeConfigurationParams where
  constructor MkDidChangeConfigurationParams
  settings : JSON
%runElab deriveJSON defaultOpts `{DidChangeConfigurationParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration
public export
record ConfigurationItem where
  constructor MkConfigurationItem
  scopeUri : Maybe DocumentURI;
  section  : Maybe String
%runElab deriveJSON defaultOpts `{ConfigurationItem}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_configuration
public export
record ConfigurationParams where
  constructor MkConfigurationParams
  items : List ConfigurationItem
%runElab deriveJSON defaultOpts `{ConfigurationParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
public export
record DidChangeWatchedFilesClientCapabilities where
  constructor MkDidChangeWatchedFilesClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesClientCapabilities}

namespace WatchKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
  public export
  data WatchKind = Create | Change | Delete

watchKindToBits8 : WatchKind -> Bits8
watchKindToBits8 Create = 1
watchKindToBits8 Change = 2
watchKindToBits8 Delete = 4

export
ToJSON (List WatchKind) where
  toJSON = toJSON . foldr (prim__or_Bits8 . watchKindToBits8) 0

export
FromJSON (List WatchKind) where
  fromJSON (JNumber x) = pure $ filter ((/=) 0 . prim__and_Bits8 (cast $ cast {to = Integer} x) . watchKindToBits8) [Create, Change, Delete]
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
public export
record FileSystemWatcher where
  constructor MkFileSystemWatcher
  globPattern : String
  kind        : Maybe (List WatchKind)
%runElab deriveJSON defaultOpts `{FileSystemWatcher}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
public export
record DidChangeWatchedFilesRegistrationOptions where
  constructor MkDidChangeWatchedFilesRegistrationOptions
  watchers : List FileSystemWatcher
%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesRegistrationOptions}

namespace FileChangeType
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
  public export
  data FileChangeType = Created | Changed | Deleted

export
ToJSON FileChangeType where
  toJSON Created = JNumber 1
  toJSON Changed = JNumber 2
  toJSON Deleted = JNumber 3

export
FromJSON FileChangeType where
  fromJSON (JNumber 1) = pure Created
  fromJSON (JNumber 2) = pure Changed
  fromJSON (JNumber 3) = pure Deleted
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
public export
record FileEvent where
  constructor MkFileEvent
  uri : DocumentURI
  type : FileChangeType
%runElab deriveJSON defaultOpts `{FileEvent}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didChangeWatchedFiles
public export
record DidChangeWatchedFilesParams where
  constructor MkDidChangeWatchedFilesParams
  changes : List FileEvent
%runElab deriveJSON defaultOpts `{DidChangeWatchedFilesParams}

namespace WorkspaceSymbolClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
  public export
  record SymbolKindClientCapabilities where
    constructor MkSymbolKindClientCapabilities
    valueSet : Maybe (List SymbolKind)
  %runElab deriveJSON defaultOpts `{SymbolKindClientCapabilities}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
  public export
  record TagSupportClientCapabilities where
    constructor MkTagSupportClientCapabilities
    valueSet : List SymbolTag
  %runElab deriveJSON defaultOpts `{TagSupportClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
public export
record WorkspaceSymbolClientCapabilities where
  constructor MkWorkspaceSymbolClientCapabilities
  dynamicRegistration : Maybe Bool
  symbolKind          : Maybe SymbolKindClientCapabilities
  tagSupport          : TagSupportClientCapabilities
%runElab deriveJSON defaultOpts `{WorkspaceSymbolClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
public export
record WorkspaceSymbolOptions where
  constructor MkWorkspaceSymbolOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{WorkspaceSymbolOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
public export
record WorkspaceSymbolRegistrationOptions where
  constructor MkWorkspaceSymbolRegistrationOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{WorkspaceSymbolRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_symbol
public export
record WorkspaceSymbolParams where
  constructor MkWorkspaceSymbolParams
  partialResultToken : Maybe ProgressToken
  query              : String
%runElab deriveJSON defaultOpts `{WorkspaceSymbolParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit
public export
record ApplyWorkspaceEditParams where
  constructor MkApplyWorkspaceEditParams
  label : Maybe String
  edit  : WorkspaceEdit
%runElab deriveJSON defaultOpts `{ApplyWorkspaceEditParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_applyEdit
public export
record ApplyWorkspaceEditResponse where
  constructor MkApplyWorkspaceEditResponse
  applied       : Bool
  failureReason : Maybe String
  failedChange  : Maybe Integer
%runElab deriveJSON defaultOpts `{ApplyWorkspaceEditResponse}

namespace FileOperationPatternKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
  public export
  data FileOperationPatternKind = FileKind | FolderKind

export
ToJSON FileOperationPatternKind where
  toJSON FileKind   = JString "file"
  toJSON FolderKind = JString "folder"

export
FromJSON FileOperationPatternKind where
  fromJSON (JString "file")   = pure FileKind
  fromJSON (JString "folder") = pure FolderKind
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record FileOperationPatternOptions where
  constructor MkFileOperationPatternOptions
  ignoreCase : Maybe Bool
%runElab deriveJSON defaultOpts `{FileOperationPatternOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record FileOperationPattern where
  constructor MkFileOperationPattern
  glob    : String
  matches : Maybe FileOperationPatternKind
  options : FileOperationPatternOptions
%runElab deriveJSON defaultOpts `{FileOperationPattern}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record FileOperationFilter where
  constructor MkFileOperationFilter
  scheme  : Maybe String
  pattern : FileOperationPattern
%runElab deriveJSON defaultOpts `{FileOperationFilter}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record FileOperationRegistrationOptions where
  constructor MkFileOperationRegistrationOptions
  filters : List FileOperationFilter
%runElab deriveJSON defaultOpts `{FileOperationRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record FileCreate where
  constructor MkFileCreate
  uri : URI
%runElab deriveJSON defaultOpts `{FileCreate}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willCreateFiles
public export
record CreateFilesParams where
  constructor MkCreateFilesParams
  files : List FileCreate
%runElab deriveJSON defaultOpts `{CreateFilesParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles
public export
record FileRename where
  constructor MkFileRename
  oldUri : URI
  newUri : URI
%runElab deriveJSON defaultOpts `{FileRename}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_willRenameFiles
public export
record RenameFilesParams where
  constructor MkRenameFilesParams
  files : List FileRename
%runElab deriveJSON defaultOpts `{RenameFilesParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles
public export
record FileDelete where
  constructor MkFileDelete
  uri : URI
%runElab deriveJSON defaultOpts `{FileDelete}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_didRenameFiles
public export
record DeleteFilesParams where
  constructor MkDeleteFilesParams
  files : List FileDelete
%runElab deriveJSON defaultOpts `{DeleteFilesParams}


text:
module Main

import System
import DepA
import DepB

main : IO ()
main = putStrLn "Hello world"

ext: idr

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
fib : Integer -> Integer
fib 0 = 0
fib 1 = 1
fib n = fib (n - 1) + fib (n - 2)

main : IO ()
main = do
  value <- getLine
  printLn (fib (cast value))


text:
module Flexidisc.RecordList

import Flexidisc.Record
import Flexidisc.Record.Transformation

%default total
%access export

public export
data RecordListM : (m : Type -> Type) -> (label : Type) -> List (Header label) -> Type where
  Nil  : RecordListM m label []
  (::) : RecordM m label header -> RecordListM m label headers ->
         RecordListM m label (header :: headers)

%name RecordListM xss, yss, zss

public export
RecordList : (label : Type) -> List (Header label) -> Type
RecordList = RecordListM id

public export
recordList : RecordListM m label xss -> RecordListM m label xss
recordList = id

namespace ContentConstraint

  public export
  data All : (Header label -> Type) ->
             (List (Header label)) -> Type where
    Nil : All cst []
    (::) : cst xs -> All cst xss -> All cst (xs::xss)

  public export
  data One : (Header label -> Type) -> Header label ->
             (List (Header label)) -> Type where
    Here  : cst xs -> One cst xs (xs :: xss)
    There : One cst ys xss -> One cst ys (xs::xss)

toList : RecordListM m label xss -> {auto prf : All (Sub subset) xss} ->
         List (RecordM m label subset)
toList [] = []
toList (x :: xs) {prf = _ :: prf} = project x :: toList xs

get : (xss : RecordListM m label headers) -> One cst header headers ->
      RecordM m label header
get (xs :: _)  (Here prf) = xs
get (_ :: xss) (There later) = get xss later

firstWith : DecEq k => TransformationM Maybe k mapper -> RecordList k xss ->
            {auto prf : All (HereOrNot (toSource mapper)) xss} ->
            Maybe (header ** Record k header)
firstWith f [] = Nothing
firstWith f (xs :: xss) {prf = p::_} = checkOne <|> firstWith f xss
  where
    checkOne = do
      toSub p
      res <- patchRecord f xs
      pure (_ ** res)

foldAll : (Ord k, DecEq k) => RecordFunc req opt a -> RecordList k xss ->
          {auto optNub : IsNub opt} ->
          {auto prf : All (Decomp req opt) xss} -> List a
foldAll f [] = []
foldAll f (xs :: xss) {prf = p :: prf} = foldRecord f xs :: foldAll f xss

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Main

test : List Nat -> List Nat
test xs = map (\x => x + 3) xs

test_main : List Nat
test_main = test [4, 3, 8]

main : JS_IO ()
main = putStrLn' (show test_main)


text:
-- --------------------------------------------------------------- [ Types.idr ]
-- Module  : Text.Kindle.Clippings.Types
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Text.Kindle.Clippings.Types

import        Data.Vect
import public Data.Date

%access  public export
%default total

-- ---------------------------------------------------------------- [ Document ]

||| A title is a string.
Title : Type
Title = String

||| An author is a string.
Author : Type
Author = String

||| A document consists of a title and and maybe an author.
record Document where
    ||| Make a document.
    constructor Doc
    ||| The title of the document.
    title : Title
    ||| The possible missing author of the document.
    author : Maybe Author

implementation Show Document where
    show (Doc title Nothing)       = title
    show (Doc title (Just author)) = title ++ " (" ++ author ++ ")"

implementation Eq Document where
    (Doc titleA authorA) == (Doc titleB authorB) =
        titleA == titleB &&
        authorA == authorB

-- ---------------------------------------------------------------- [ Interval ]

||| An interval is either a single integer or a range of integers.
data Interval : Type where
    ||| A single place, i.e. `Page' or `Location'.
    Singleton : Integer -> Interval
    ||| A range.
    ||| @ from The start of the range.
    ||| @ to   The end of the range.
    Proper : (from, to : Integer) -> Interval

||| A page is an interval.
Page : Type
Page = Interval

||| A location is an interval.
Location : Type
Location = Interval

implementation Show Interval where
    show (Singleton x)    = show x
    show (Proper from to) = show from ++ "-" ++ show to

-- ---------------------------------------------------------------- [ Position ]

||| A position consists of a page, location or both.
data Position : Type where
     ||| A page with no location.
     ||| @ page A page.
     PP : (page : Page) -> Position
     ||| A location with no page.
     ||| @ loc A location.
     Loc : (loc  : Location) -> Position
     ||| A page and location
     ||| @ page A page.
     ||| @ loc  A location.
     PPLoc : (page : Page)     -> (loc : Location) -> Position

||| Given a page, location or both, return a position. If both inputs are
||| `Nothing`, return `Nothing`.
||| @ page Maybe a page.
||| @ loc  Maybe a location.
mkPosition : (page : Maybe Page) -> (loc : Maybe Location) -> Maybe Position
mkPosition  Nothing     Nothing   = Nothing
mkPosition  Nothing    (Just loc) = Just $ Loc loc
mkPosition (Just page)  Nothing   = Just $ PP page
mkPosition (Just page) (Just loc) = Just $ PPLoc page loc

implementation Show Position where
    show (PP page)        = "page " ++ show page
    show (Loc loc)        = "Location " ++ show loc
    show (PPLoc page loc) = unwords [ show page, "|", show loc ]

-- ----------------------------------------------------------------- [ Content ]

||| Content is either a bookmark, some highlight text, or a note.
data Content : Type where
   ||| A bookmark.
   Bookmark  : Content
   ||| Some highlighted text.
   ||| @ selection The highlight text.
   Highlight : (selection : String) -> Content
   ||| A note.
   ||| @ body The body of a note.
   Note : (body : String) -> Content

||| If a given string can be parsed as a `Content` data constructor, return just
||| a function that takes a string and returns the appropriate `Content`. If the
||| string can't be parsed, return `Nothing`. N.B. The resulting `Bookmark`
||| function ignores it's input. This makes it easier to use when parsing
||| clippings.
||| @ type A string representing a `Content` data constructor.
mkContent : (type : String) -> Maybe (String -> Content)
mkContent "Bookmark"  = Just (const Bookmark)
mkContent "Highlight" = Just Highlight
mkContent "Note"      = Just Note
mkContent _           = Nothing

contentType : Content -> String
contentType Bookmark      = "Bookmark"
contentType (Highlight _) = "Highlight"
contentType (Note _)      = "Note"

implementation Show Content where
  show Bookmark              = "Bookmark"
  show (Highlight selection) = selection
  show (Note body)           = body

-- ---------------------------------------------------------------- [ Clipping ]

||| A Kindle clipping consists of a document, position, date and content.
record Clipping where
    ||| Make a clipping.
    constructor Clip
    ||| A document.
    document : Document
    ||| A position.
    position : Position
    ||| A date.
    date     : Date
    ||| Some content.
    content  : Content

implementation Show Clipping where
    show (Clip document position date content) =
        unlines [ show document
                , unwords [ "Your", contentType content, "on", show position
                          , "| Added on", show date ]
                , ""
                , show content
                , "==========" ]

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
module Euler_circuit

import Data.Fin
import Data.Vect as V

  -- data EulerG : Graph n -> Type where
  --   EulerEmpty : (g: Graph Z)   -> EulerG g
  --   EulerAddLoop   : (a: Fin k) -> (g: Graph1 k ** EulerG g) -> EulerG (AddEdge a a g)
  --

data Graph1 : (n : Nat) -> Type where
  WithoutEdge : Graph1 k
  AddEdge     : (a: Fin k) -> (b: Fin k) -> Graph1 k -> Graph1 k

data Graph2 : (n : Nat) -> Vect n (List (Fin n)) -> Vect n (List (Fin n)) -> Type where
  Graph2Empty     : {k: Nat} -> Graph2 k (replicate k Nil) (replicate k Nil)
  Graph2AddEdge   : (a : Fin k) -> (b : Fin k) -> (g: Graph2 k ies oes)
                  -> Graph2 k (updateAt b (a::) $ ies)
                              (updateAt a (b::) $ oes)

data EqLen : List a -> List a -> Type where
  EqLenZ : EqLen Nil Nil
  EqLenS : EqLen xs ys -> a -> b -> EqLen (a::xs) (b::ys)

data ZipPVect : (P : a -> b -> Type) -> Vect n a -> Vect n b -> Type where
  ZipPVectZ : {P: a -> b -> Type} -> ZipPVect P Nil Nil
  ZipPVectS : {P: a -> b -> Type} -> ZipPVect P xs ys -> (x: a) -> (y: b) -> P x y -> ZipPVect P (x::xs) (y::ys)

data Path : (head: Type) -> head -> Type where
  PathO : {a: Type} -> (x: a) -> (y: a) -> Path a y
  PathS : {a: Type} -> Path a x -> (y: a) -> Path a y

data ContainEdges : Path (Fin n) h -> (g: Graph2 n ies oes) -> Type where
  ContainEdgesO : (a: Fin n) -> (b: Fin n) -> ContainEdges (PathO a b) (Graph2AddEdge a b Graph2Empty)
  ContainEdgesS : (es: Path (Fin n) h) -> (g: Graph2 n ies oes) -> ContainEdges es g
               -> (a: Fin n) -> (b: Fin n) -> h = a -> ContainEdges (PathS es b) (Graph2AddEdge a b g)

data IsoGraph2 : (g1: Graph2 n1 ies1 oes1) -> (g2: Graph2 n2 ies2 oes2) -> Type where
  IsoGraph2eq : g1 = g2 -> IsoGraph2 g1 g2

delete_empty_node : (g: Graph2 (S k) (Nil::ies) (Nil::oes)) -> ZipPVect EqLen ies oes
                 -> (g': Graph2 k ies' oes' ** ZipPVect EqLen ies' oes')
delete_empty_node = ?q1

add_empty_node : (path: Path (Fin n) h) -> (g: Graph2 n ies oes) -> (contEd: ContainEdges path g') -> (isoG: IsoGraph2 g g')
              -> (path: Path (Fin n) h ** (ContainEdges path g'', IsoGraph2 g g''))
add_empty_node = ?q2

theorem : {n: Nat} -> (g: Graph2 n ies oes) -> ZipPVect EqLen ies oes
       -> Maybe (path: Path (Fin n) h ** (ContainEdges path g', IsoGraph2 g' g))
theorem Graph2Empty _ = Nothing
theorem g (ZipPVectS zipPVect [] [] (EqLenZ)) =
  let (g' ** zipPVect') = delete_empty_node g zipPVect
      (path' ** (contEd, isoG)) = case theorem g' zipPVect' of -- TODO: can't match `P path'` and `(A, B)`
         (Just x) => x
         Nothing  => absurd
  in Just $ ?add_empty_node path' g' contEd isoG

-- TODO: prove round trip add/delete empty node
{-
 g  ~  g'+1
 !      !
g-1  ~  g'
-}

max_stars_repo_name: GoPavel/idris-proof

max_issues_repo_name: GoPavel/idris-proof

max_forks_repo_name: GoPavel/idris-proof


text:
module DerivingEq

import Language.Reflection

%language ElabReflection

public export
countArgs : (ty : TTImp) -> Nat
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy
countArgs _ = 0

-- %logging 5
public export
genEq : {t : _} -> Name -> Elab (t -> t -> Bool)
genEq typeName = do
  let pos : FC = MkFC (Virtual Interactive) (0,0) (0,0)
  [(n, _)] <- getType typeName
      | _ => fail "Ambiguous name"
  constrs <- getCons n
  let and : TTImp -> TTImp -> TTImp
      and x y = `(~(x) && ~(y))
      compareEq : String -> String -> TTImp
      compareEq x y = `(~(IVar pos $ UN (Basic x)) == ~(IVar pos $ UN (Basic y)))
      makeClause : Name -> Elab Clause
      makeClause constr = do
        [(_, ty)] <- getType constr
            | _ => fail "ambiguous name for constr"
        let nArgs = countArgs ty
        let xs = map (\i => "x_" ++ show i) $ take nArgs [1..]
        let ys = map (\i => "y_" ++ show i) $ take nArgs [1..]
        let px = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) xs
        let py = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) ys
        pure $ PatClause pos `(MkPair ~(px) ~(py))
             $ foldl and `(True) $ zipWith compareEq xs ys
      finalClause : Clause
      finalClause = PatClause pos `(_) `(False)
  clauses <- traverse makeClause constrs
  let allClauses = clauses ++ [finalClause]
      caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses
      result = `(\x, y => ~(caseExpr))
  check result
%logging 0

-- This tree works

data TreeOne a = BranchOne (TreeOne a) a (TreeOne a)
               | Leaf

Eq a => Eq (TreeOne a) where
  (==) = %runElab genEq `{ TreeOne }


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

module Itea.Html
import Itea.Html.Attributes
import Itea.Html.Events

import Control.Monad.Reader
import Control.Monad.Identity

%default total
%access public export

-- Types -----------------------------------------------------------------------

||| HTML element type representing the structure of the DOM tree
data HTML : Type -> Type where
  ||| Tag element
  ||| @tagname node tag
  ||| @events list of events assigned to the tag
  ||| @attributes tag attributes such as class, href, rel
  ||| @html child nodes in the DOM tree
  HtmlElem : (tagname    : String)
          -> (events     : List (Event a))
          -> (attributes : List Attribute)
          -> (html       : List (HTML a))
          -> HTML a
  ||| Text element
  ||| @text raw text
  HtmlText : (text : String) -> HTML a

||| HTML monad for implictly passing the event queue around
Html : Type -> Type
Html a = Reader (EventQueue a) (HTML a)

-- Element ---------------------------------------------------------------------

||| Create a static element with given attributes
staticElement : String -> List Attribute -> List (Html a) -> Html a
staticElement name attr html =
  let html = map (runIdentity . flip runReaderT !ask) html in
  pure $ HtmlElem name [] attr html

||| Create an interactive element with given listeners
|||
||| @name name of element
||| @handlers list of handlers taking the event queue as input
||| @attr element attributes
||| @ok implicit proos ensuring given handler list is non empty
interactiveElement : (name     : String)
                  -> (handlers : List (EventQueue a -> Event a))
                  -> (attr     : List Attribute)
                  -> { auto ok : NonEmpty handlers }
                  -> Html a
interactiveElement name events attr =
  pure $ HtmlElem name (map (flip apply !ask) events) attr []

-- Tags ------------------------------------------------------------------------

||| Construct a text element
text : String -> Html a
text = pure . HtmlText

div : List Attribute -> List (Html a) -> Html a
div = staticElement "div"

body : List Attribute -> List (Html a) -> Html a
body = staticElement "body"

nav : List Attribute -> List (Html a) -> Html a
nav = staticElement "nav"

article : List Attribute -> List (Html a) -> Html a
article = staticElement "article"

aside : List Attribute -> List (Html a) -> Html a
aside = staticElement "aside"

h1 : List Attribute -> List (Html a) -> Html a
h1 = staticElement "h1"

h2 : List Attribute -> List (Html a) -> Html a
h2 = staticElement "h2"

h3 : List Attribute -> List (Html a) -> Html a
h3 = staticElement "h3"

h4 : List Attribute -> List (Html a) -> Html a
h4 = staticElement "h4"

h5 : List Attribute -> List (Html a) -> Html a
h5 = staticElement "h5"

h6 : List Attribute -> List (Html a) -> Html a
h6 = staticElement "h6"

br : Html a
br = staticElement "br" [] []

tr : List Attribute -> List (Html a) -> Html a
tr = staticElement "tr"

table : List Attribute -> List (Html a) -> Html a
table = staticElement "table"

td : List Attribute -> List (Html a) -> Html a
td = staticElement "td"

tbody : List Attribute -> List (Html a) -> Html a
tbody = staticElement "tbody"

thead : List Attribute -> List (Html a) -> Html a
thead = staticElement "thead"

tfoot : List Attribute -> List (Html a) -> Html a
tfoot = staticElement "tfoot"

th : List Attribute -> List (Html a) -> Html a
th = staticElement "th"

||| Image object
record Image where
  constructor MkImage
  ||| Relative link
  rel    : String
  ||| Width of image
  width  : Dimension
  ||| Height of image
  height : Dimension

img : List Attribute -> Html a
img = flip (staticElement "img") []

namespace Simple

  ||| Simple interface working with images directly
  img : List Attribute -> Image -> Html a
  img attr (MkImage rel' width' height') =
    img $ [ width width'
          , height height'
          , rel rel'
          ] ++ attr

p : List Attribute -> List (Html a) -> Html a
p = staticElement "p"

code : List Attribute -> List (Html a) -> Html a
code = staticElement "code"

strong : List Attribute -> List (Html a) -> Html a
strong = staticElement "strong"

{-
header
footer
address
main
hr
pre
blockquote
ol
ul
li
dl
dd
figure
figcaption
a
em
small
s
cite
q
abbr
time
var
samp
kbd
sup
i
u
matk
ruby
rt
rp
bdi
bdo
span
ins
del
iframe
embed
object
param
video
audio
source
track
canvas
math
caption
colgroup
col
form
fieldset
legend
label
select
datalist
optgroup
option
textarea
keygen
output
progress
meter
details
summary
menuitem
menu
-}

||| Interactive button
|||
||| @xs list of listeners along with their return messages
||| @attr button attributes
||| @ok proof of the input list having at least one element
button : (xs   : List (EventQueue a -> Event a))
      -> (attr : List Attribute)
      -> { auto ok : NonEmpty xs }
      -> Html a
button = interactiveElement "button"

||| Interactive input
|||
||| @xs list of listeners along with their return messages
||| @attr input attributes
||| @ok proof of the input list having at least one element
input : (xs   : List (EventQueue a -> Event a))
     -> (attr : List Attribute)
     -> { auto ok : NonEmpty xs }
     -> Html a
input = interactiveElement "input"

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module congruences

||| Congruence
public export
congruence : (ty1, ty2 : Type) -> (a : ty1) -> (b : ty1) -> (f : ty1 -> ty2) -> (a = b) -> ((f a) = (f b))
congruence ty1 ty2 a a f Refl = Refl


text:
zipWithS : (f : a -> b -> c) -> Stream a -> Stream b -> Stream c
zipWithS f (x :: xs) (y :: ys) = f x y :: zipWithS f xs ys

partial
fib : Stream Nat
fib = 0 :: zipWithS (+) fib (1 :: fib)

partial main : IO ()
main = printLn (take 15 fib)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Client.Action.BuildDeps

import Client.Action.CacheDeps
import Data.List
import Data.SortedMap as Map
import Data.SortedSet as Set
import Data.String
import Fmt
import Inigo.Async.Base
import Inigo.Async.Package
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Paths
import Inigo.PkgTree
import SemVar

buildIPkg : String -> Promise ()
buildIPkg path =
  do
    log (fmt "Compiling %s" (path </> inigoIPkgPath))
    debugLog "[\{path}]$ idris2 --build \{inigoIPkgPath}"
    0 <- system "idris2" ["--build", inigoIPkgPath] (Just path) False True
        | errno => reject "idris2 build error: \{show errno}"
    log (fmt "Compiled %s" (path </> inigoIPkgPath))

export
buildDeps : Bool -> Promise ()
buildDeps dev = do
    pkgs <- readDepCache
    pkg <- currPackage
    let ctxt = fromList pkgs
    log $ "Generating build order" ++ if dev then " with dev dependencies" else ""
    debugLog "Packages to build: \{show $ Set.toList $ keySet ctxt}"
    debugLog "Package context: \{show $ Map.toList $ getDeps {name=String} dev <$> ctxt}"
    build <- liftEither $ getBuildOrder dev ctxt (keySet ctxt)
    traverse_ buildIPkg build

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Extra.Buffer

import Data.Buffer

%foreign "node:lambda:(buf)=>buf.toString('base64')"
enc64__prim : Buffer -> PrimIO String

%foreign "node:lambda:(str)=>Buffer.from(str, 'base64')"
dec64__prim : String -> PrimIO Buffer

%foreign "node:lambda:(str)=>Buffer.from(str, 'utf-8')"
fromString__prim : String -> PrimIO Buffer

%foreign "node:lambda:(buf,char)=>buf.indexOf(char)"
indexOf__prim : Buffer -> Char -> PrimIO Int

export
enc64 : HasIO io => Buffer -> io String
enc64 =
  primIO . enc64__prim

export
dec64 : HasIO io => String -> io Buffer
dec64 =
  primIO . dec64__prim

export
fromString : HasIO io => String -> io Buffer
fromString =
  primIO . fromString__prim

export
indexOf : HasIO io => Char -> Buffer -> io (Maybe Int)
indexOf char buf =
  do
    res <- primIO (indexOf__prim buf char)
    if res < 0
      then pure $ Nothing
      else pure $ Just res

export
readAll : HasIO io => Buffer -> io String
readAll buf =
  do
    len <- rawSize buf
    x <- getString buf 0 len
    pure x

export
readLine : HasIO io => Buffer -> io (String, Maybe Buffer)
readLine buf =
  do
    Just index <- indexOf '\n' buf
      | Nothing =>  do
                        contents <- readAll buf
                        pure $ (contents, Nothing)
    Just (line, rest) <- splitBuffer buf (index + 1)
      | Nothing => pure $ ( "", Just buf ) -- Shrug
    contents <- readAll line
    pure $ (contents, Just rest)


text:
> module InfiniteHorizonSequentialDecisionProblems.Lala

> import Data.Vect
> import Syntax.PreorderReasoning

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Vect.Operations
> import Vect.Properties
> import Pair.Properties

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

* ---------
* Sequences
* ---------

> Seq : Type -> Type
> Seq A = Nat -> A

> head : {A : Type} -> Seq A -> A
> head f = f Z

> tail : {A : Type} -> Seq A -> Seq A
> tail f = f . S

> cons : {A : Type} -> A -> Seq A -> Seq A
> cons a f    Z  = a
> cons a f (S n) = f n

> headLemma : {A : Type} -> (a : A) -> (f : Seq A) -> head (cons a f) = a
> headLemma a f = Refl

> tailLemma : {A : Type} -> (a : A) -> (f : Seq A) -> tail (cons a f) = f
> tailLemma a d = Refl

> consLemma : {A : Type} -> (f : Seq A) -> (n : Nat) -> cons (head f) (tail f) n = f n
> consLemma f    Z  = Refl
> consLemma f (S n) = Refl

* ---------
* Fix point
* ---------

> FixPoint : {X : Type} -> X -> (X -> X) -> Type
> FixPoint x f = x = f x

* ----------------------------
* Sequential decision problems
* ----------------------------

> State  :  Type
> Ctrl   :  (x : State) -> Type
> next   :  (x : State) -> (y : Ctrl x) -> State
> Val    :  Type
> reward :  (x : State) -> (y : Ctrl x) -> State -> Val
> (<+>)  :  Val -> Val -> Val
> LTE    :  Val -> Val -> Type

* --------------------------------------
* Policies and infinite policy sequences
* --------------------------------------

> Policy  :  Type
> Policy  =  (x : State) -> Ctrl x

> PolicySeq  :  Type
> -- PolicySeq  =  Nat -> Policy
> PolicySeq  =  Seq Policy

* ---------------------------------------
* The value of infinite policiy sequences
* ---------------------------------------

The value of making infinite many decision steps with a policy sequence
by starting from a given state is given by a "value" function

> val : PolicySeq -> State -> Val

that fulfils the specification

> valSpec  :  Type
> valSpec  =  (ps : PolicySeq) -> (x : State) ->
>             val ps x = reward x (head ps x) (next x (head ps x))
>             <+>
>             val (tail ps) (next x (head ps x))

A naive attempt at implementing |val| directly "from its specification"

< val ps x = reward x (head ps x) (next x (head ps x)) <+> val (tail ps) (next x (head ps x))

yiels a possibly non total function. In contrast to SDPs with a finite
number of decision steps, we cannot rely on an induction principle for
decision problems over an infinite number of steps. Obviously, there are
cases in which |val| can be implemented. For instance, if all states
have the same successor. An important case is when |State| is finite. We
discuss this case below.

* ------------------------------
* Optimality of policy sequences
* ------------------------------

> Opt     :  PolicySeq -> Type
> Opt ps  =  (ps' : PolicySeq) -> (x : State) -> val ps' x `LTE` val ps x

* ------------------------
* Optimal policy sequences
* ------------------------

Let |LTE| be a preorder

> reflexiveLTE     :  (a : Val) -> a `LTE` a
> transitiveLTE    :  {a, b, c : Val} -> a `LTE` b -> b `LTE` c -> a `LTE` c

and let |<+>| be monotonous w.r.t. |LTE|

> monotonePlusLTE  :  {a, b, c, d : Val} -> a `LTE` b -> c `LTE` d -> (a <+> c) `LTE` (b <+> d)

We can compute the value of making a first decision step with a given
control and then infinitely many further steps with a given policy
sequence in terms of the (yet to be implemented) |val| function:

> cval         :  (ps : PolicySeq) -> (x : State) -> Ctrl x -> Val
> cval ps x y  =  reward x y (next x y) <+> val ps (next x y)

Assume that, for an arbitrary policy sequence |ps| and for an arbitrary
state |x|, we can pick up a control that maximises |cval ps x|:

> cvalmax         :  (ps : PolicySeq) -> (x : State) -> Val
> cvalargmax      :  (ps : PolicySeq) -> (x : State) -> Ctrl x

> cvalargmaxSpec  :  (ps : PolicySeq) -> (x : State) -> cvalmax ps x = cval ps x (cvalargmax ps x)
> cvalmaxSpec     :  (ps : PolicySeq) -> (x : State) -> (y : Ctrl x) -> cval ps x y `LTE` cvalmax ps x

This is certainly the case if |Ctrl x| is non empty and finite for any
|x| but there are more interesting cases in which we can compute "best"
controls. In these cases, we can compute policies that are optimal
extensions of arbitrary policy sequences:

> OptExt : Policy -> PolicySeq -> Type
> OptExt p ps = (p' : Policy) -> (x : State) -> val (cons p' ps) x `LTE` val (cons p ps) x

> optExt : (ps : PolicySeq) -> Policy
> optExt = cvalargmax

> optExtLemma : (ps : PolicySeq) -> (optExt ps) `OptExt` ps
> optExtLemma ps p' x = s5 where
>   p  : Policy
>   p  = optExt ps
>   s1 : cval ps x (p' x) `LTE` cvalmax ps x
>   s1 = cvalmaxSpec ps x (p' x)
>   s2 : reward x (p' x) (next x (p' x)) <+> val ps (next x (p' x))  `LTE` cvalmax ps x
>   s2 = s1
>   s3 : reward x (p' x) (next x (p' x)) <+> val ps (next x (p' x))  `LTE` cval ps x (p x)
>   s3 = replace {P = \ X => reward x (p' x) (next x (p' x)) <+> val ps (next x (p' x))  `LTE` X} (cvalargmaxSpec ps x) s2
>   s4 : reward x (p' x) (next x (p' x)) <+> val ps (next x (p' x))  `LTE` reward x (p x) (next x (p x)) <+> val ps (next x (p x))
>   s5 : val (cons p' ps) x `LTE` val (cons p ps) x
>   s5 = ?s5prf -- via valSpec, headLemma, tailLemma

This is interesting because of

> Bellman  :  (ps  :  PolicySeq)  ->   Opt ps ->
>             (p   :  Policy)     ->   p `OptExt` ps ->
>             Opt (cons p ps)
> Bellman ps ops p oep = opps where
>   opps : Opt (cons p ps)
>   opps ps' x = s7 where
>     p'   : Policy
>     p'   = head ps'
>     ps'' : PolicySeq
>     ps'' = tail ps'
>     s4   : val (cons p' ps'') x `LTE` val (cons p' ps) x
>     s4   = ?s4prf
>     s5   : val (cons p' ps) x `LTE` val (cons p ps) x
>     s5   = ?s5prf
>     s6   : val (cons p' ps'') x `LTE` val (cons p ps) x
>     s6   = transitiveLTE s4 s5
>     s7   : val ps' x `LTE` val (cons p ps) x
>     s7   = ?s7prf -- via valSpec, consLemma, ...

I am not sure that this is going to help us but it looks remarkably
similar to the finite horizon case. Perhaps a first step towards
something like

> piter : (Policy, PolicySeq) -> (Policy, PolicySeq)
> piter (p, ps) = (optExt ps, cons (optExt ps) ps)

> piterLemma : (p : Policy) -> (ps : PolicySeq) ->
>              (p, ps) `FixPoint` piter ->
>              (n : Nat) -> ps n = p
> piterLemma p ps fp  Z    = ( ps Z )
>                          ={ Refl }=
>                            ( head ps )
>                          ={ cong (pairEqElimSnd fp) }=
>                            ( head (cons (optExt ps) ps) )
>                          ={ headLemma (optExt ps) ps }=
>                            ( optExt ps )
>                          ={ sym (pairEqElimFst fp) }=
>                            ( p )
>                          QED
> piterLemma p ps fp (S m) = ( ps (S m) )
>                          ={ sym (consLemma ps (S m)) }=
>                            ( cons (head ps) (tail ps) (S m) )
>                          ={ Refl }=
>                            ( (tail ps) m )
>                          ={ replace {P = \ X => (tail ps) m = (tail X) m} (pairEqElimSnd fp) Refl }=
>                            ( (tail (cons (optExt ps) ps)) m )
>                          ={ replace {P = \ X => (tail (cons (optExt ps) ps)) m = (tail (cons X ps)) m} (sym (pairEqElimFst fp)) Refl }=
>                            ( (tail (cons p ps)) m )
>                          ={ replace {P = \ X => (tail (cons p ps)) m = X m} (tailLemma p ps) Refl }=
>                            ( ps m )
>                          ={ piterLemma p ps fp m }=
>                            ( p )
>                          QED

> Conj : (p : Policy) -> (ps : PolicySeq) ->
>        (p, ps) `FixPoint` piter ->
>        Opt (cons p ps)
> Conj p ps fp = opps where
>   opps : Opt (cons p ps)
>   opps = s9 where
>     s0 : (p, ps) = (optExt ps, cons (optExt ps) ps)
>     s0 = fp
>     s1 : p = optExt ps
>     s1 = pairEqElimFst s0
>     s2 : ps = cons (optExt ps) ps
>     s2 = pairEqElimSnd s0
>     s3 : ps = cons p ps
>     s3 = replace {P = \ X => ps = cons X ps} (sym s1) s2
>     s4 : (optExt ps) `OptExt` ps
>     s4 = optExtLemma ps
>     s5 : p `OptExt` ps
>     s5 = replace {P = \ X => X `OptExt` ps} (sym s1) s4
>     s9 : Opt (cons p ps)
>     s9 = Bellman ps ops p oep where
>       ops : Opt ps
>       ops = assert_total (replace {P = \ X => Opt X} (sym s3) s9)
>       oep : p `OptExt` ps
>       oep = s5

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Loc

public export
record Loc where
  constructor MkLoc
  column, line : Int

public export
record Range where
  constructor MkRange
  start, end : Loc

public export
Show Loc where
  show (MkLoc {column, line}) = "(" ++ (show column) ++ ", " ++ (show line) ++ ")"

public export
Show Range where
  show (MkRange {start, end}) = "(" ++ (show start) ++ ", " ++ (show end) ++ ")"

public export
mixRange : Range -> Range -> Range
mixRange (MkRange start _) (MkRange _ end) = (MkRange start end)

public export
emptyRange : Range
emptyRange = MkRange (MkLoc 0 0) (MkLoc 0 0)

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains error types.
module Error

||| An `Error` indicates a runtime error.
public export
interface Error exc where
  ||| Show the error in a human readable format.
  format : exc -> String

||| Indicates a value is invalid.
public export
data ValueError = MkValueError String

export
Error ValueError where
  format (MkValueError msg) = msg

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Data.Maybe.NothingMax

import Control.Function
import Data.Maybe
import Data.Prim.Ord

%default total

||| A total order for `Maybe a` where `a` has a total order
||| and `Nothing` is the maximal value.
|||
||| This is useful, for instance, when implementing provably
||| sorted (assoc-) lists, indexed by a `Maybe key`, where
||| the empty list has a `Nothing` index:
|||
||| ```idris example
||| data AssocList : (ix : Maybe Bits8) -> (a : Type) -> Type where
|||   Nil  : AssocList Nothing a
|||   (::) :  (p : (Bits8, a))
|||        -> (ps : AssocList ix a)
|||        -> (0 prf : LT (<) (Just $ fst p) ix)
|||        => AssocList (Just $ fst p) a
||| ```
public export
data LT : (lt : a -> a -> Type) -> (m1,m2 : Maybe a) -> Type where
  LTNothing : LT lt (Just v) Nothing
  LTJust    :  {0 lt : a -> a -> Type}
            -> {0 v, w : a}
            -> lt v w -> LT lt (Just v) (Just w)

public export
Uninhabited (LT lt Nothing m) where
  uninhabited LTNothing impossible
  uninhabited (LTJust _) impossible

public export
Total a lt => Uninhabited (LT lt (Just k) (Just k)) where
  uninhabited LTNothing impossible
  uninhabited (LTJust refl) = void (irrefl refl)

public export
fromLT : LT lt (Just a) (Just b) -> lt a b
fromLT (LTJust x) = x

||| Implementation and alias for `trichotomy`.
export
comp : Total a lt => (m1,m2 : Maybe a) -> Trichotomy (LT lt) m1 m2
comp (Just x) (Just y) = case trichotomy {lt} x y of
  LT p c1 c2 => LT (LTJust p) (\r => c1 (injective r)) (\x => c2 (fromLT x))
  EQ c1 p c2 => EQ (\x => c1 (fromLT x)) (cong Just p) (\x => c2 (fromLT x))
  GT c1 c2 p => GT (\x => c1 (fromLT x)) (\r => c2 (injective r)) (LTJust p)
comp (Just x) Nothing  = LT LTNothing absurd absurd
comp Nothing  (Just y) = GT absurd absurd LTNothing
comp Nothing  Nothing  = EQ absurd Refl absurd

||| If `lt` is a total order of `a`, then `LT lt` is a
||| total order of `Maybe a`.
export %inline
Total a lt => Total (Maybe a) (LT lt) where
  trichotomy = comp

  transLT (LTJust x) LTNothing  = LTNothing
  transLT (LTJust x) (LTJust y) = LTJust $ trans x y
  transLT LTNothing  y          = absurd y


text:
||| Hashconsing App
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Control.App.Hashcons

import Control.App
import Data.So

import Data.Hash
import Data.Hashtable as H

%default total

-- ---------------------------------------------------------------------------

data FreshCounter : Type where
data Cache : Type -> Type where
export data HC t = MkHC (t, Int)

export %inline unintern : HC t -> t
unintern (MkHC (x, _)) = x

Eq (HC t) where MkHC (_, l) == MkHC (_, r) = l == r
Ord t => Ord (HC t) where
  compare (MkHC (l, _)) (MkHC (r, _)) = compare l r
  (MkHC (l, _)) < (MkHC (r, _)) = l > r
  (MkHC (l, _)) > (MkHC (r, _)) = l < r
  (MkHC (l, _)) <= (MkHC (r, _)) = l >= r
  (MkHC (l, _)) >= (MkHC (r, _)) = l <= r

public export
interface Hashcons t es where
  intern : t -> App {l} es (HC t)

public export partial
(Eq t, Hashable t,
 State (Cache t) (Int, IOHashtable t Int) es, PrimIO es)
 => Hashcons t es where
  intern k = do
    (fresh, cache) <- get (Cache t)
    x <- primIO $ H.lookup' k cache
    case x of
         Just x' => pure $ MkHC x'
         Nothing => do
           x' <- primIO $ H.insert' k (fresh + 1) cache
           _ <- put (Cache t) (fresh + 1, cache)
           pure $ MkHC x'

export partial
withHashcons : (Hashcons t es, PrimIO es)
               => (cachesize:Int) -> {auto _:So (cachesize > 0)}
               -> App {l} es a -> App {l} es a
withHashcons cachesize prog = do
  cache <- primIO $ H.newHashtable {k=t} {v=Int} cachesize
  new {tag=Cache t} (0, cache) prog


text:
||| The mandatory fibonacci
module Main
import Cairo

fib : (i: Felt) -> Felt
fib n = if n == 0 || n == 1
          then n
          else fib (n - 1) + fib (n - 2)

%noinline
main : Cairo ()
main = output (fib 5)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Meriv.Core.Main.idr

||| Required for JVM backend to generate Java class files.
main : IO ()
main = pure ()

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype


text:
import Data.Vect

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

transposeHelper : (x : Vect n elem) ->
                 (xsTrans : Vect n (Vect len elem)) ->
                 Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
                         transposeHelper x xsTrans


text:
> module Nat.Predicates

> import Sigma.Sigma

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

Divisor (following an idea from Tim Richter):

> {-
> data Divisor : (m : Nat) -> (n : Nat) -> Type where
>   mkDivisor : (m : Nat) -> (n : Nat) -> Exists (\ q => m * q = n) -> Divisor m n
> -}

> Divisor : (m : Nat) -> (n : Nat) -> Type
> Divisor m n = Exists (\ q => m * q = n)

Greatest common divisor (following an idea from Tim Richter):

> data GCD : (d : Nat) -> (m : Nat) -> (n : Nat) -> Type where
>   MkGCD : d `Divisor` m ->
>           d `Divisor` n ->
>           ((d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d) ->
>           GCD d m n

> gcd : Sigma Nat (\ d => GCD d m n) -> Nat
> gcd (MkSigma d _) = d

> gcdDivisorFst : GCD d m n -> d `Divisor` m
> gcdDivisorFst {d} (MkGCD dDm dDn dG) = dDm

> gcdDivisorSnd : GCD d m n -> d `Divisor` n
> gcdDivisorSnd {d} (MkGCD dDm dDn dG) = dDn

> gcdDivisorGreatest : GCD d m n -> ((d' : Nat) -> d' `Divisor` m -> d' `Divisor` n -> d' `Divisor` d)
> gcdDivisorGreatest {d} (MkGCD dDm dDn dG) = dG

Coprime (following an idea from Tim Richter):

> data Coprime : (m : Nat) -> (n : Nat) -> Type where
>   MkCoprime : GCD d m n -> d = S Z -> Coprime m n


text:
||| Rules for stacking
||| Section 5
module Bautzen.Game.Stacking

import Bautzen.GameUnit
import Bautzen.Terrain

-- section 5.1

stackingPoints : Nation -> UnitSize -> UnitType -> Nat
stackingPoints   n         s           SupplyColumn = 1
stackingPoints   n         Regiment    t            = 2
stackingPoints   n         Brigade     t            = 3
stackingPoints   n         Division    HQ           = 3
stackingPoints   Russian   Corps       HQ           = 3
stackingPoints   Russian   Army        HQ           = 3
stackingPoints   n         Corps       Armored      = 3  -- 1KP
stackingPoints   _         _           _            = 1  -- WTF?

-- section 5.2

stackingLimit : Terrain -> Nat
stackingLimit Clear               = 6
stackingLimit Wood                = 4
stackingLimit Rough               = 4
stackingLimit RoughWood           = 4
stackingLimit (Hill base)         = stackingLimit base
stackingLimit (Village base)      = stackingLimit base
stackingLimit Town                = 6
stackingLimit (SupplySource base) = stackingLimit base

-- section 5.4, 5.5, 5.6

data Stacking : Type where
  Stacked : (n : Nat) -> Stacking
  Overstacked : (n : Nat) -> Stacking
  CannotStack : Stacking

||| What's the stacking status of `units` on `terrain`?
||| This can be used to test incrementally the stacking of adding one unit to
||| to an existing stack too.
||| @units a lits of units to check stacking of.
||| @terrain the terrain of the `Hex` the units are stacked on.
stacking : (units : List GameUnit) -> (terrain: Terrain) -> Stacking
stacking units terrain =
  if moreThan2DifferentFormations || unitsFromDifferentNations
  then CannotStack
  else let sp = sum $ map sps units
       in if sp <= stackingLimit terrain
          then Stacked sp
          else Overstacked sp
  where
    unitsFromDifferentNations : Bool
    unitsFromDifferentNations = (length . nub . map nation $ units) > 1

    moreThan2DifferentFormations : Bool
    moreThan2DifferentFormations = (length . catMaybes . nub . map parent $ units) > 2

    sps : GameUnit -> Nat
    sps (MkGameUnit nation unitType name parent size move currentMP hit combat) = stackingPoints nation size unitType

namespace StackingTest

  stacking_of_a_single_unit : stacking [ GameUnit.p13_5dp ] Clear = Stacked 2
  stacking_of_a_single_unit = Refl

  stacking_of_more_units_from_same_parent : stacking [ GameUnit.p13_5dp, GameUnit.p15_5dp, GameUnit.p17_5dp ] Clear = Stacked 6
  stacking_of_more_units_from_same_parent = Refl

  overstack_from_units_from_same_parent : stacking [ GameUnit.p13_5dp, GameUnit.p15_5dp, GameUnit.p5dp ] Clear = Overstacked 7
  overstack_from_units_from_same_parent = Refl

  cannot_stack_more_than_1_unit_from_different_parent : stacking [ GameUnit.p13_5dp, GameUnit.p33_7dp, GameUnit.p32_8dp ] Clear = CannotStack
  cannot_stack_more_than_1_unit_from_different_parent = Refl

  can_stack_independent_units : stacking [ GameUnit.p13_5dp, GameUnit.p33_7dp, GameUnit.p6l ] Clear = Overstacked 7
  can_stack_independent_units = Refl

  cannot_stack_units_from_different_nations : stacking [ GameUnit.p13_5dp, GameUnit.r857_294 ] Clear = CannotStack
  cannot_stack_units_from_different_nations = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Main

import lib.Library

main : IO ()
main = putStrLn salute


text:
module EqNat

%default total

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num

sameS : (eq : EqNat k j) -> EqNat (S k) (S j)
sameS (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same Z)
checkEqNat Z _  = Nothing
checkEqNat _ Z = Nothing
checkEqNat (S k) (S l) = case checkEqNat k l of
                              Nothing => Nothing
                              Just eq => Just (sameS eq)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Js.BrowserNetwork
{-
import Js.BrowserForeigns
import public Js.ServiceTypes

export
httpGet : String -> ASync String
httpGet url = MkASync $ httpGet_raw url

export
httpPost : String -> String -> ASync String
httpPost url body = MkASync $ httpPost_raw url body

export
callRPC : ServiceGroup ts -> (name:String) -> Elem (name, RPCServiceTy a b) ts -> a -> ASync b
callRPC group name p val =
  let (RPCService _ e1 e2) = getService name group p
  in do
    res <- httpPost name (encode e1 val)
    case decode e2 res of
      Right x => pure x
      Left err => debugError err
-}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs