text:
module Scheme_Parsers

%access public export

||| The type of outputs of a parsing
data ParseResult : Type -> Type where
  Success : {a: Type} -> (result : a) -> (rest: List Char) -> ParseResult a
  Failed : {a: Type} -> (rest: List Char) -> ParseResult a

||| The type of parsers
Parser: Type -> Type
Parser a = (List Char) -> ParseResult a

||| Convenience method to apply a parser to a input
parseChars : {a: Type} -> Parser a -> List Char -> ParseResult a
parseChars p xs = p xs

||| Convenience method to parse strings instead of lists of characters
parse : {a: Type} -> Parser a -> String -> ParseResult a
parse p s = parseChars p (unpack s)

||| Method to decide if something is true about the character. Will be used mostly
||| to decide if it is equal to some specific character.
charPred : (Char -> Bool) -> Parser Char
charPred p l = (case l of
    [] => Failed  ([])
    (x :: xs) =>
        if (p x) then (Success x xs) else Failed (x :: xs))

||| Given a character gives the function to check if another character is equal to it
charLit : Char -> Parser Char
charLit c = charPred (\x => x == c)

||| Given a function (A -> B) and a parser of type A gives a Parser of type B.
map : {a: Type} -> {b: Type} -> Parser a -> (a -> b) -> Parser b
map p f cs = (case (p cs) of
    (Success  result rest) => Success  (f result) rest
    (Failed  rest) => Failed  rest)

||| Given two parser p and q applies p to l. If succeeds apllies q to the rest and outputs the combined result
(++) : {a : Type} -> {b: Type} -> Parser a -> Parser b -> Parser (Pair a b)
(++) p q l = (case p l of
    (Success result1 rest1) => (case (q rest1) of
        (Success result2 rest2) => Success ((result1, result2)) rest2
        (Failed rest2) => Failed l)
    (Failed rest) => Failed rest)

||| Matches a list of characters A to another list of characters B. If A is the beginning of B succeeds.
charsLit: (List Char) -> Parser (List Char)
charsLit []  l = Success [] l
charsLit (x :: xs) [] = Failed []
charsLit (x :: xs) (a :: bs) =
    (case charLit x (a :: bs) of
        (Success result1 rest) => (case (charsLit xs bs) of
            (Success result2 rest) => Success (result1 :: result2) rest
            (Failed rest) => Failed (a :: bs))
        (Failed rest) => Failed rest)

||| Uses charLit to match a string. Also gives strings as output.
S: String -> Parser String
S s = map (charsLit (unpack s)) pack

||| Given to parsers p and q applies p to input. If succeeds then outputs the result. If fails applies
||| q to the result and outputs the result.

(||) : {a: Type} -> Parser a -> Parser a -> Parser a
(||) p q l = (case (p l) of
                       (Success result rest) => Success result rest
                       (Failed rest) => q rest)

||| Helper method to repeatedly apply a Parser.
repParse: {a: Type} -> Parser a -> (inp: List Char) -> (accum: List a) -> ParseResult (List a)
repParse p inp accum = case (p inp) of
                            (Success result rest) => repParse p rest (result :: accum)
                            (Failed rest) => Success accum inp

||| Gives a Parser for a list of type A given a Parser of type A.
repRev : {a: Type} -> Parser a -> Parser (List a)
repRev p l =  repParse p l []

||| Applies the Parser zero or more times and outputs the result in reverse. Notice that due to
||| Structure of the List the output of repRev is actually the reverse of what we want.
rep : {a: Type} -> Parser a -> Parser (List a)
rep p = map (repRev p) reverse

||| Same as rep except it runs the Parser for one or more times, so that it does not take empty
||| inputs as valid ones
rep1 : {a: Type} -> Parser a -> Parser (List a)
rep1 p = map (p ++ (repRev p)) (\pair => (case pair of
                                            (a, b) => a :: reverse(b)))

||| Helper method to get the natural number from the corresponding reversed list of characters.
natFromRev : List Char -> Double -> Double
natFromRev [] n = 0
natFromRev (x :: xs) n =
  let
  d : Double = n * (cast ( (ord x) - (ord '0')))
  in
  d + (natFromRev xs (10 * n))

||| Helper method to get the number after the decimal
floatFromCharHelper : List Char -> (exp : Double) -> (accum : Double) -> Double
floatFromCharHelper [] n accum = accum
floatFromCharHelper (x :: xs) n accum =
    let
    d : Double = n * (cast ( (ord x) - (ord '0') ))
    in
    (floatFromCharHelper xs (n * 0.1) (d + accum))

||| Method to get the number after the decimal
floatAfterDecimal : List Char -> Double
floatAfterDecimal l = (floatFromCharHelper l 0.1 0)

||| Method to get the number corresponding to the list of characters
natFromChars : (List Char) -> Double
natFromChars l = natFromRev (reverse l) 1

||| Checks if there is a natural number in the beginning of the list of characters. And outputs
||| the result, which is the maximum consumable input along with the unconsumed part
nat : Parser Double
nat = map (rep1 (charPred isDigit)) (natFromChars)

||| Gives the float assuming it is after the decimal point. It does not accept non zero inputs
floatAfter : Parser Double
floatAfter = map (rep1 (charPred isDigit)) (floatAfterDecimal)

||| Checks if the character is equal to '.'
isDot : Char -> Bool
isDot a = a == '.'

||| Helper method to get the number from the string
floatFromCharHelper1 : List Char -> ParseResult Double
floatFromCharHelper1 [] = Failed []
floatFromCharHelper1 (x :: xs) = case (isDot x) of
    True => (floatAfter xs)
    False => Failed (x :: xs)

||| Gets the double from the string. Note that input has to be of the form "a.b" where both a and
||| b are non empty strings of characters 0 - 9
float : Parser Double
float expr = case (nat expr) of
    (Success before rest) => case (floatFromCharHelper1 rest) of
        (Success after rest) => Success (before + after) rest
        (Failed rest) => Failed expr
    (Failed rest) => (Failed rest)


text:
module Markdown.Format.Text

import Extra.String
import Markdown.Data

-- toTextEl : MarkdownEl -> String
-- toTextEl (Header level text) = "#" ++ text -- TODO: Level
-- toTextEl (Paragraph text) = text

-- ||| Convert a Markdown value into its string representation.
-- public export
-- toText : Markdown -> String
-- toText (Doc els) =
--   join "\n" (map toTextEl els)

public export
toText : Markdown -> String
toText x = "TODO"

ext: idr

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Dart.FFI.Enums

import Dart.Core

public export
interface IsEnum a where

namespace Enum

  %inline
  export
  equals : IsEnum a => a -> a -> Bool
  equals = prim__dart_eq

export
IsEnum a => Eq a where
  (==) = Enum.equals


text:
data Tree elem = Empty | Node (Tree elem) elem (Tree elem)
%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left value right) = case compare x value of
                                        LT => Node (insert x left) value right
                                        EQ => orig
                                        GT => Node left value (insert x right)

insert_helper : Ord a => (x : a) -> Tree a -> Tree a
insert_helper x t = insert x t

listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = let inserted = listToTree xs  in
                         insert_helper x inserted

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = let leftList  = (treeToList left)
                                     rightList = x :: treeToList right
                                     in leftList ++ rightList

Foldable Tree where
  foldr func acc Empty = acc
  foldr func acc (Node left value right) = let leftFold = foldr func acc left
                                               rightFold = foldr func leftFold right in
                                               func value rightFold

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


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

||| More Quantifiers for Lists, but keeping them out of the prelude so
||| need a new module name.
module Data.List.Predicates

import public Data.List
import public Data.List.Predicates.Unique
import public Data.List.Predicates.Interleaving
import public Data.List.Predicates.Pairs
import public Data.List.Predicates.Thinning

%default total
%access public export

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module DataStore

import Data.Vect

infixr 5 .+.

public export
data Schema = SString
            | SInt
            | (.+.) Schema Schema

public export
SchemaType: Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

export
record DataStore(schema: Schema) where
  constructor MkData
  size: Nat
  items: Vect size (SchemaType schema)

export
empty: DataStore schema
empty = MkData 0 []

export
addToStore : (value: SchemaType schema) -> (store: DataStore schema) -> DataStore schema
addToStore value (MkData size items) = MkData _ (value :: items)

public export
data StoreView : DataStore schema -> Type where
  SNil : StoreView empty
  SAdd: (rec: StoreView store) -> StoreView (addToStore value store)

storeViewHelp : (items: Vect size (SchemaType schema)) -> StoreView (MkData size items)
storeViewHelp [] = SNil
storeViewHelp (val :: xs) = SAdd (storeViewHelp xs)

export
storeView : (store : DataStore schema) -> StoreView store
storeView (MkData size items) = storeViewHelp items

listItems : DataStore schema -> List (SchemaType schema)
listItems input with (storeView input)
  listItems empty                    |  SNil      = []
  listItems (addToStore value store) | (SAdd rec) = value :: (listItems store | rec)

filterKeys : (test : SchemaType schema -> Bool) -> DataStore (SString .+. schema) -> List String
filterKeys test input with (storeView input)
  filterKeys test empty                           |  SNil      = []
  filterKeys test (addToStore (key, value) store) | (SAdd rec) =
    if test value
    then key :: (filterKeys test store | rec)
    else filterKeys test store | rec

getValues : DataStore (SString .+. schema) -> List (SchemaType schema)
getValues input with (storeView input)
  getValues input                       |  SNil      = []
  getValues (addToStore (_, val) store) | (SAdd rec) = val :: (getValues store | rec)

testStore : DataStore (SString .+. SString .+. SInt)
testStore = addToStore ("Mercury", "Mariner 10",  1974) $
            addToStore ("Venus",   "Venera",      1961) $
            addToStore ("Uranus",  "Voyager 2",   1986) $
            addToStore ("Pluto",   "New Horizons",2015) $
            empty

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
> module Unique.Predicates -- from an idea by Tim Richter

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

> Unique : Type -> Type
> Unique t = (p : t) -> (q : t) -> p = q

> Unique0 : Type -> Type
> Unique0 = Unique

> Unique1 : {A : Type} -> (A -> Type) -> Type
> Unique1 {A} P = (a : A) -> Unique0 (P a)

> UniqueEq0 : Type -> Type
> UniqueEq0 A = (a1 : A) -> (a2 : A) -> Unique (a1 = a2)

> UniqueEq1 : {A : Type} -> (P : A -> Type) -> Type
> UniqueEq1 {A} P = (a : A) -> UniqueEq0 (P a)

> {- Maybe implement via a type class ?

> class Unique t where
>   unique : (p : t) -> (q : t) -> p = q

> -}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module GRIN.Error

import System.File

import GRIN.AST

public export
data Error
    = FileErr String FileError
    | MissingVar Var

export
Show Error where
    show (FileErr f err) = "File error with file " ++ show f ++ "\n" ++ show err ++ "\n\n"
    show (MissingVar (MkVar v)) = "Missing variable from VarMap (v" ++ show v ++ ")\n\n"


text:
module Instructions

import Hardware

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Dec3

import Data.Vect

%default total

data Orientation = Up | Left | Down | Right

data MoverState : (position : (Int, Int)) -> (orientation : Orientation) -> Type where
     MkMoverState : (history : Vect n (Int, Int)) -> (values : Vect n Int) ->
                    MoverState position orientation

sumOfNeighbours : (history : Vect n (Int, Int)) -> (values : Vect n Int) -> (x, y : Int) -> Int
sumOfNeighbours history values x y = foldl f 0 $ zip history values
  where
    f : Int -> ((Int, Int), Int) -> Int
    f agg (h, v) = case (abs (x - fst h), abs (y - snd h)) of
      (0, 1) => v + agg
      (1, 0) => v + agg
      (1, 1) => v + agg
      _ => agg

move : MoverState (x, y) orientation ->
       Either (MoverState (x, y) orientation)
              (Either (MoverState (x, y+1) Up)
                      (Either (MoverState (x-1, y) Left)
                              (Either (MoverState (x, y-1) Down)
                                      (MoverState (x+1, y) Right))))
move {x} {y} {orientation} (MkMoverState history values) =
  case orientation of
    -- (x, y), Up, left-turn possible => (x-1, y), Left
    -- (x, y), Up, left-turn impossible, up possible => (x, y+1), Up
    -- (x, y), Up, left-turn impossible, up impossible => (x, y), Up
    Up => case elem (x-1, y) history of
      False => Right (Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values))))
      True => case elem (x, y+1) history of
        False => Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))
        True => Left (MkMoverState history values)
    -- (x, y), Left, left-turn possible => (x, y-1), Downs
    -- (x, y), Left, left-turn impossible, left possible => (x-1, y), Left
    -- (x, y), Left, left-turn impossible, left impossible => (x, y), Left
    Left => case elem (x, y-1) history of
      False => Right (Right (Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))))
      True => case elem (x-1, y) history of
        False => Right (Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values))))
        True => Left (MkMoverState history values)
    -- (x, y), Down, left-turn possible => (x+1, y), Right
    -- (x, y), Down, left-turn impossible, down possible => (x, y-1), Down
    -- (x, y), Down, left-turn impossible, down impossible => (x, y), Down
    Down => case elem (x+1, y) history of
      False => Right (Right (Right (Right (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))))
      True => case elem (x, y-1) history of
        False => Right (Right (Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))))
        True => Left (MkMoverState history values)
    -- (x, y), Right, left-turn possible => (x, y+1), Up
    -- (x, y), Right, left-turn impossible, right possible => (x+1, y), Right
    -- (x, y), Right, left-turn impossible, right impossible => (x, y), Right
    Right => case elem (x, y+1) history of
      False => Right (Left (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))
      True => case elem (x+1, y) history of
        False => Right (Right (Right (Right (MkMoverState ((x, y) :: history) ((sumOfNeighbours history values x y) :: values)))))
        True => Left (MkMoverState history values)

manhattanDistance : (Int, Int) -> (Int, Int) -> Int
manhattanDistance (x1, y1) (x2, y2) = abs (x1 - x2) + abs (y1 - y2)

walkDistance : (steps: Nat) -> MoverState (x, y) orientation -> Int
walkDistance Z (MkMoverState [] []) = 0
walkDistance Z (MkMoverState (h :: hs) (v :: vs)) = manhattanDistance h $ last (h :: hs)
walkDistance (S k) state = case move state of
  Left state => walkDistance k state -- walkDistance state Z doesn't preserve totality for some reason
  Right (Left (state)) => walkDistance k state
  Right (Right (Left (state))) => walkDistance k state
  Right (Right (Right (Left (state)))) => walkDistance k state
  Right (Right (Right (Right (state)))) => walkDistance k state

dec3a : Int
dec3a = walkDistance {x = 0} {y = 0} {orientation = Down} 361527 (MkMoverState [] [])

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

walkUntil : Fuel -> (p : Int -> Bool) -> MoverState (x, y) orientation -> Maybe Int
walkUntil Dry p state = Nothing
walkUntil (More fuel) p state = case move state of
    Left state' => recurse state'
    Right (Left (state')) => recurse state'
    Right (Right (Left (state'))) => recurse state'
    Right (Right (Right (Left (state')))) => recurse state'
    Right (Right (Right (Right (state')))) => recurse state'
  where
    recurse : (MoverState (x', y') orientation') -> Maybe Int
    recurse state = case state of
      MkMoverState _ [] => walkUntil fuel p state
      MkMoverState _ (v :: vs) => if p v then walkUntil fuel p state else Just v

dec3b : Fuel -> Maybe Int
dec3b fuel = walkUntil {x = 1} {y = 0} {orientation = Right} fuel (\i => i <= 361527) (MkMoverState [(0, 0)] [1])


text:
import Data.Vect

length : Vect n elem -> Nat
length {n} xs = n

empties : Vect n (Vect 0 a)
empties {n = Z} = []
empties {n = (S k)} = [] :: empties

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.Compress.GZip

import Data.Compress.Utils.Parser
import Data.Compress.Utils.Bytes
import Data.Compress.Utils.Misc
import Data.Compress.Interface
import Data.Vect
import Data.Bits
import Data.List
import Data.SnocList
import Data.Stream
import Data.Compress.CRC
import Control.Monad.Error.Either

import public Data.Compress.Inflate

public export
data GZipParserState'
  = GZipHead
  | GZipFoot
  | GZipInflate

public export
data GZipParserState : GZipParserState' -> Type where
  AtGHeader : GZipParserState GZipHead
  AtInflate : (isize : Bits32) -> (crc32 : Bits32) -> InflateState -> GZipParserState GZipInflate
  AtGFooter : (isize : Bits32) -> (crc32 : Bits32) -> GZipParserState GZipFoot

public export
data GZipState
  = MkState (List Bits8) (DPair GZipParserState' GZipParserState)

nul_term_string : Semigroup e => Parser (List Bits8) e String
nul_term_string = map ascii_to_string $ take_until (0 ==) token

record GZipFooter where
  constructor MkGZipFooter
  crc32 : Bits32
  isize : Bits32

export
parse_gzip_header : Parser (List Bits8) (SimpleError String) ()
parse_gzip_header = do
  [0x1f, 0x8b] <- count 2 token
  | x => fail $ msg "gzip magic number expected, got \{show x}"
  0x08 <- token
  | x => fail $ msg "deflate method magic number expected, got \{show x}"
  flag <- token
  mtime <- count 4 token
  xfl <- token
  os <- token

  fextra <- ifA (testBit flag 2) $ do
    xlen <- p_nat 2
    toList <$> count xlen token

  fname <- ifA (testBit flag 3) nul_term_string

  fcomment <- ifA (testBit flag 4) nul_term_string

  fhcrc <- ifA (testBit flag 1) (count 2 token)

  pure ()

export
parse_gzip_footer : Parser (List Bits8) (SimpleError String) GZipFooter
parse_gzip_footer = do
  crc32 <- cast <$> p_nat 4
  isize <- cast <$> p_nat 4
  pure (MkGZipFooter crc32 isize)

feed_gzip' : SnocList Bits8 -> DPair GZipParserState' GZipParserState -> List Bits8 -> Either String (SnocList Bits8, GZipState)
feed_gzip' acc (_ ** AtGHeader) [] = Right (acc, MkState [] (_ ** AtGHeader))
feed_gzip' acc (_ ** AtGHeader) content =
  case feed content parse_gzip_header of
    Pure leftover header => feed_gzip' acc (_ ** AtInflate 0 0 init) leftover
    Fail err => Left $ show err
    _ => Right (acc, MkState content (_ ** AtGHeader))
feed_gzip' acc (_ ** AtInflate isize crc32 inflate_state) content =
  case feed inflate_state content of
    Left err => Left err
    Right (uncompressed, (MkState _ _ (_ ** AtEnd leftover))) =>
      let isize = isize + (cast $ length uncompressed)
          crc32 = update_crc32 crc32 uncompressed
      in feed_gzip' (acc <>< uncompressed) (_ ** AtGFooter isize crc32) (toList leftover)
    Right (uncompressed, inflate_state) => -- underfed
      let isize = isize + (cast $ length uncompressed)
          crc32 = update_crc32 crc32 uncompressed
      in Right (acc <>< uncompressed, MkState [] (_ ** AtInflate isize crc32 inflate_state))
feed_gzip' acc (_ ** AtGFooter isize crc32) content =
  case feed content parse_gzip_footer of
    Pure leftover footer =>
      if footer.crc32 /= crc32 then Left "crc32 mismatch"
        else if footer.isize /= isize then Left "isize mismatch"
        else feed_gzip' acc (_ ** AtGHeader) leftover
    Fail err => Left $ show err
    _ => Right (acc, MkState content (_ ** AtGFooter isize crc32))

export
Decompressor GZipState where
  feed (MkState leftover state) input = mapFst toList <$> feed_gzip' Lin state (leftover <+> input)
  done (MkState [] (_ ** AtGHeader)) = Right []
  done (MkState _ (_ ** AtGHeader)) = Left "gzip: leftover data after header"
  done _ = Left "gzip: underfed"
  init = MkState [] (_ ** AtGHeader)


text:
||| Functions for the processing of received request and notifications.
|||
||| (C) The Idris Community, 2021
module Server.ProcessMessage

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.OneOf
import Idris.ModTree
import Idris.Package
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.IDEMode.Holes
import Language.LSP.CodeAction.CaseSplit
import Language.LSP.CodeAction.ExprSearch
import Language.JSON
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Capabilities
import Server.Configuration
import Server.Log
import Server.Response
import Server.Utils
import System

displayType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayType defs (n, i, gdef)
    = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
                pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm))
            (\num => prettyHole defs [] n num (type gdef))
            (isHole gdef)

displayTerm : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> ClosedTerm ->
              Core (Doc IdrisAnn)
displayTerm defs tm
    = do ptm <- resugar [] !(normaliseHoles defs [] tm)
         pure (prettyTerm ptm)

||| Guard for messages that requires a successful initialization before being allowed.
whenInitialized : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenInitialized k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => sendUnknownResponseMessage serverNotInitialized

||| Guard for messages that cannot be sent after the shutdown protocol.
whenNotShutdown : Ref LSPConf LSPConfiguration => Core () -> Core ()
whenNotShutdown k =
  if !(gets LSPConf isShutdown)
     then sendUnknownResponseMessage (invalidRequest "Server has been shutdown")
     else k

||| Process a parsed LSP message received from a client.
export
processMessage : Ref LSPConf LSPConfiguration
              => Ref Ctxt Defs
              => Ref UST UState
              => Ref Syn SyntaxInfo
              => Ref MD Metadata
              => Ref ROpts REPLOpts
              => {type : MethodType}
              -> (method : Method Client type)
              -> Message type method
              -> Core ()
processMessage Initialize msg@(MkRequestMessage id Initialize params) = do
  -- TODO: Here we should analyze the client capabilities.
  let response = Success (getResponseId msg) (MkInitializeResult serverCapabilities (Just serverInfo))
  -- The compiler does not work with the same root directory model that LSP operates with,
  -- may be a point of friction in particular with the location of generated binary files.
  let Just fpath = path <$> toMaybe params.rootUri
    | _ => do logString Error $ "Error in initialize expected valid root uri"
              sendUnknownResponseMessage (invalidParams "Expected valid root uri")
  fname <- fromMaybe fpath <$> findIpkg (Just fpath)
  setSourceDir (Just fname)
  sendResponseMessage Initialize response
  update LSPConf (record {initialized = Just params})

processMessage Shutdown msg@(MkRequestMessage _ Shutdown _) = do
  -- In a future multithreaded model, we must guarantee that all pending request are still executed.
  let response = Success (getResponseId msg) (the (Maybe Null) Nothing)
  sendResponseMessage Shutdown response
  update LSPConf (record {isShutdown = True})

processMessage Exit (MkNotificationMessage Exit _) = do
  let status = if !(gets LSPConf isShutdown) then ExitSuccess else ExitFailure 1
  coreLift $ exitWith status

processMessage TextDocumentDidOpen msg@(MkNotificationMessage TextDocumentDidOpen params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Just (params.textDocument.uri, params.textDocument.version)})
    -- TODO: the compiler works directly with the file, we should upstream some changes to allow it to work with the
    --       source passed by the client.
    resetContext
    let fpath = params.textDocument.uri.path
    fname <- fromMaybe fpath <$> findIpkg (Just fpath)
    errs <- buildDeps fname -- FIXME: the compiler always dumps the errors on stdout, requires
                            --        a compiler change.
    setSource params.textDocument.text
    resetProofState
    sendDiagnostics params.textDocument.uri (Just params.textDocument.version) errs

processMessage TextDocumentDidSave msg@(MkNotificationMessage TextDocumentDidSave params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Just (params.textDocument.uri, 0)})
    -- TODO: same issue of TextDocumentDidOpen
    resetContext
    let fpath = params.textDocument.uri.path
    fname <- fromMaybe fpath <$> findIpkg (Just fpath)
    let Just source = params.text
      | _  => do logString Error $ "Error in textDocument/didSave expected format"
                 sendUnknownResponseMessage (invalidParams "Expected full text after save")
    errs <- buildDeps fname -- FIXME: add string version to the compiler (requires upstream change, probably)
                            -- FIXME: stop emitting errors on stdout (requires upstream change)
    logString Debug $ "errors : \{show errs}"
    setSource source
    resetProofState
    sendDiagnostics params.textDocument.uri Nothing errs

processMessage TextDocumentDidClose msg@(MkNotificationMessage TextDocumentDidClose params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Nothing})
    logString Info $ "File \{params.textDocument.uri.path} closed"

processMessage TextDocumentHover msg@(MkRequestMessage id TextDocumentHover params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    let fpath = params.textDocument.uri.path
    fname <- fromMaybe fpath <$> findIpkg (Just fpath)
    res <- loadMainFile fname

    defs <- get Ctxt
    meta <- get MD

    let name = findInTree (params.position.line, params.position.character) (nameLocMap meta)
    -- Lookup the name globally
    globals <- maybe (pure []) (\n => lookupCtxtName n (gamma defs)) name
    globalResult <- the (Core $ Maybe $ Doc IdrisAnn) $ case globals of
      [] => pure Nothing
      ts => do tys <- traverse (displayType defs) ts
               pure $ Just (vsep tys)
    localResult <- findTypeAt $ anyAt $ within (params.position.line, params.position.character)
    line <- case (globalResult, localResult) of
      -- Give precedence to the local name, as it shadows the others
      (_, Just (n, _, type)) => pure $ renderString $ unAnnotateS $ layoutUnbounded $ pretty (nameRoot n) <++> colon <++> !(displayTerm defs type)
      (Just globalDoc, Nothing) => pure $ renderString $ unAnnotateS $ layoutUnbounded globalDoc
      (Nothing, Nothing) => pure ""
    let response = Success (getResponseId msg) (make $ MkHover (make $ MkMarkupContent PlainText line) Nothing)
    sendResponseMessage TextDocumentHover response

processMessage TextDocumentCodeAction msg@(MkRequestMessage id TextDocumentCodeAction params) =
  whenNotShutdown $ whenInitialized $ \_ => do
    splitAction <- caseSplit (getResponseId msg) params
    exprSearchAction <- map Just <$> exprSearch params
    let resp = flatten (splitAction :: exprSearchAction)
    sendResponseMessage TextDocumentCodeAction (Success (getResponseId msg) (make resp))
    where
      flatten : List (Maybe CodeAction) -> List (OneOf [Command, CodeAction])
      flatten [] = []
      flatten (Nothing :: xs) = flatten xs
      flatten ((Just x) :: xs) = make x :: flatten xs

processMessage {type = Request} method msg =
  whenNotShutdown $ whenInitialized $ \conf => do
    logString Warning $ "received a not supported \{show (toJSON method)} request"
    sendResponseMessage method (methodNotFound msg)
processMessage {type = Notification} method msg =
  whenNotShutdown $ whenInitialized $ \conf =>
    logString Warning "unhandled notification"


text:
isEven' : Nat -> Bool
isEven' Z = True
isEven' (S k) = not (isEven' k)

mutual
  isEven : Nat -> Bool
  isEven Z = True
  isEven (S k) = isOdd k

  isOdd : Nat -> Bool
  isOdd Z = False
  isOdd (S k) = isEven k

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module API

import Test.API
import Test.API3
import Test.API2


text:
> module Math
> import Data.Vect
> import Data.HVect
> import Data.List
> import Data.Fin

We take some tricks from https://boxbase.org/entries/2019/sep/16/grabbag-of-idris-tricks/ and http://firsov.ee/finset/finset.pdf.

Use Pauli group as small example:

> data PauliGroup : Type where
>   X : PauliGroup
>   Y : PauliGroup
>   Zp : PauliGroup
>   I : PauliGroup

We provide a complete list of PauliGroup elements:

> listPauli : List PauliGroup
> listPauli = [X,Y,Zp,I]

> allPauli : (x: PauliGroup) -> Data.List.Elem x Math.listPauli
> allPauli X = Here
> allPauli Y = There Here
> allPauli Zp = There (There Here)
> allPauli I = There (There (There Here))

> xIsNotY : (X = Y) -> Void
> xIsNotY Refl impossible
> xIsNotZ : (X = Zp) -> Void
> xIsNotZ Refl impossible
> xIsNotI : (X = I) -> Void
> xIsNotI Refl impossible
> yIsNotZ : (Y = Zp) -> Void
> yIsNotZ Refl impossible
> yIsNotI : (Y = I) -> Void
> yIsNotI Refl impossible
> zIsNotI : (Zp = I) -> Void
> zIsNotI Refl impossible

> DecEq PauliGroup where
>   decEq X X = Yes Refl
>   decEq X Y = No xIsNotY
>   decEq X Zp = No xIsNotZ
>   decEq X I = No xIsNotI
>   decEq Y X = No (\c => xIsNotY (sym c))
>   decEq Y Y = Yes Refl
>   decEq Y Zp = No yIsNotZ
>   decEq Y I = No yIsNotI
>   decEq Zp X = No (\c => xIsNotZ (sym c))
>   decEq Zp Y = No (\c => yIsNotZ (sym c))
>   decEq Zp Zp = Yes Refl
>   decEq Zp I = No zIsNotI
>   decEq I X = No (\c => xIsNotI (sym c))
>   decEq I Y = No (\c => yIsNotI (sym c))
>   decEq I Zp = No (\c => zIsNotI (sym c))
>   decEq I I = Yes Refl

And we give the group structure:

> multPauli : PauliGroup -> PauliGroup -> PauliGroup
> multPauli X X = I
> multPauli X Y = Zp
> multPauli X Zp = Y
> multPauli X I = X
> multPauli Y X = Zp
> multPauli Y Y = I
> multPauli Y Zp = X
> multPauli Y I = Y
> multPauli Zp X = Y
> multPauli Zp Y = X
> multPauli Zp Zp = I
> multPauli Zp I = Zp
> multPauli I X = X
> multPauli I Y = Y
> multPauli I Zp = Zp
> multPauli I I = I

> commPauli : (x:PauliGroup) -> (y:PauliGroup) -> (multPauli x y = multPauli y x)
> commPauli X X = Refl
> commPauli X Y = Refl
> commPauli X Zp = Refl
> commPauli X I = Refl
> commPauli Y X = Refl
> commPauli Y Y = Refl
> commPauli Y Zp = Refl
> commPauli Y I = Refl
> commPauli Zp X = Refl
> commPauli Zp Y = Refl
> commPauli Zp Zp = Refl
> commPauli Zp I = Refl
> commPauli I X = Refl
> commPauli I Y = Refl
> commPauli I Zp = Refl
> commPauli I I = Refl

Obviously there are a number of shortcomings with this approach.... and associativity
would take 64 lines to prove...

> Injective : {t,u:Type} -> (t -> u) -> Type
> Injective f {t} = (x,y:t) -> (f x = f y) -> (x = y)

> Surjective : {t,u:Type} -> (t -> u) -> Type
> Surjective f {t} {u} = (y:u) -> (x:t ** f x = y)

> getInverse : {t,u:Type} -> {func: t -> u} -> (Injective func) -> (Surjective func) -> (u -> t)
> getInverse {t} {u} {func} inj surj = \y => fst (surj y)

> Bijective : {t,u : Type} -> (t -> u) -> Type
> Bijective f {t} {u} = ?bij

Proofs that a list contain all possible elements of a type:

> All : {t : Type} -> List t -> Type
> All xs {t} = (x:t) -> Elem x xs

Given a type t and a proof of t, it is a contradiction to have a proof that the
empty list contains all elements of t.

> allNotEmpty : All {t} [] -> t -> Void
> allNotEmpty f x = absurd (f x)

> voidEmptyAll : Uninhabited t => All {t} []
> voidEmptyAll = \c => absurd c

Decidable list membership:

> DecIn : (t: Type) -> Type
> DecIn t = (x:t) -> (xs : List t) -> Dec (Elem x xs)

Decidable equality and decidable list membership are equivalent:

> decInToDeqEq : DecIn t -> (x:t) -> (y:t) -> Dec (x = y)
> decInToDeqEq f x y = case (f x [y]) of
>   Yes Here => Yes Refl
>   No contra => No (\eq => contra (rewrite eq in Here))

Little helper lemmas:

> matchingSingleton : Data.List.Elem x [y] -> (x = y)
> matchingSingleton Here = Refl
> matchingSingleton (There later) impossible

> deqEqToDeqIn : DecEq t => DecIn t
> deqEqToDeqIn x [] = No absurd
> deqEqToDeqIn x (y::ys) with (deqEqToDeqIn x ys)
>   deqEqToDeqIn x (y::ys) | No notLater = case decEq x y of
>       Yes Refl => Yes Here
>       No contra => No (\later =>
>                           case later of
>                               Here => contra (matchingSingleton Here)
>                               (There t) => notLater t)
>   deqEqToDeqIn x (y::ys) | Yes later = Yes (There later)

Proof that a given type is a "mere proposition" (i.e. it only has one element)

> Prop : (t:Type) -> Type
> Prop t = (p1:t) -> (p2:t) -> (p1=p2)

We also have a notion of a List with no duplicates:

> NoDupes : {t:Type} -> List t -> Type
> NoDupes {t} xs = (x:t) -> Prop (Elem x xs)

Some trivial helper lemmas:

> noDupesInHeadLemma : Elem x xs -> NoDupes (x :: xs) -> Void
> noDupesInHeadLemma {x = x} {xs = []} _ _ impossible
> noDupesInHeadLemma {x} a b = hereIsNotThere (b x Here (There a))

If a type has decidable equality, then All and NoDupes are decidable.
We need a (somewhat metamathematical) lemma to start stating that any two
void values of the same type are equal (there are in fact zero of them - this
is just a wrapper for "void can prove anything")

> voidsAreEquivalent : {t: Type} -> (t -> Void) -> (a:t) -> (b:t) -> (a=b)
> voidsAreEquivalent f a b = void (f a)

> sameTheresLemma : {a: Data.List.Elem x xs} -> (There a = There a)
> sameTheresLemma = Refl

To avoid an awkward workaround with Void types, we force the caller to prove that
the type isn't void by providing some item. This might need some work...

> deqEqToAllIncomplete : DecEq t => (xs:List t) -> t -> Dec (All xs)
> deqEqToAllIncomplete [] someItem = No (\c => allNotEmpty c someItem)
> deqEqToAllIncomplete (x :: xs) someitem = Yes (\c =>
>   case (decEq x c) of
>       Yes pf => rewrite pf in Here
>       No contra => ?newh2)

After some reflection, I don't think this will work. We need to know *ahead of time*
that All {t} [xs] exists. This method will always fail to converge for Nats.

> thereLemma1 : {a: Data.List.Elem x xs} -> {b : Data.List.Elem x xs} -> (a = b) -> There a = There b
> thereLemma1 {a = Here} {b = Here} Refl = Refl
> thereLemma1 {a = Here} {b = (There _)} Refl impossible
> thereLemma1 {a = (There _)} {b = Here} Refl impossible
> thereLemma1 {a = (There x)} {b = (There x)} Refl = Refl

> thereLemma2 : {a: Data.List.Elem x xs} -> {b : Data.List.Elem x xs} -> (There a = There b) -> a = b
> thereLemma2 {a = Here} {b = Here} pf = Refl
> thereLemma2 {a = Here} {b = (There _)} Refl impossible
> thereLemma2 {a = (There _)} {b = Here} Refl impossible
> thereLemma2 {a = (There x)} {b = (There x)} Refl = Refl

> consNoDupes : DecEq t => {x : t} -> NoDupes {t} xs -> (Not (Elem x xs)) -> NoDupes (x :: xs)
> consNoDupes {x = x} noDupesSublist notIn y pf1 pf2 with (decEq x y)
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | Yes pf = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | Yes pf = absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | Yes pf = absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | Yes pf = absurd (notIn (rewrite pf in later)) --rewrite (noDupesSublist y later z) in Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | No contra = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | No contra = absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | No contra = absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | No contra = let ndupes = (noDupesSublist y later z) in thereLemma1 ndupes

> dupeCons : NoDupes (x :: xs) -> NoDupes xs
> dupeCons dupeBiglist item pf1 pf2 = thereLemma2 (dupeBiglist item (There pf1) (There pf2))

> deqEqToDupe : DecEq t => (xs:List t) -> Dec (NoDupes xs)
> deqEqToDupe [] = Yes (\a => (\b => (\c => (voidsAreEquivalent uninhabited b c))))
> deqEqToDupe (x :: xs) with (isElem x xs)
>   deqEqToDupe (x :: xs) | Yes pf = No (noDupesInHeadLemma pf)
>   deqEqToDupe (x :: xs) | No contra = case deqEqToDupe xs of
>       Yes noDupes => Yes (consNoDupes noDupes contra)
>       No areDupes => No (\c => areDupes (dupeCons c))

If P is a decidable proposition, we can quotient P by the total equivalence relation
and get a "squashed" type {what is this relation?}

> squash : {p:Type} -> Dec p -> Type
> squash (Yes _) = Unit
> squash (No _) = Void

An example: Elem x [x,y,x] is decidable:

> exSquash1 : Dec (Data.List.Elem X [X,Y,X])
> exSquash1 = Yes Here

> exSquash2 : Dec (Data.List.Elem X [X,Y,X])
> exSquash2 = Yes (There (There Here))

Both "squash" to Unit. Note that any two squashed values are trivially equal:

> propSquash : {p: Type} -> (d : Dec p) -> Prop (squash d)
> propSquash (Yes prf) () () = Refl
> propSquash (No contra) v1 _ = absurd v1

> fromSquash : {p:Type} -> (d : Dec p) -> squash d -> p
> fromSquash (Yes prf) () = prf

makeAllFin : (k:Nat) -> (xs:(List (Fin (S k))) ** All (Fin (S k)) xs)
makeAllFin Z = ([FZ] ** (IsAll (\x => Here)))

Kuratowski finiteness:

> Listable : (t : Type) -> Type
> Listable t = (xs ** (All {t} xs))

An alternative idea is to require a surjection Fin n to t for some Nat n:

> FinSurjective : (t: Type) -> Type
> FinSurjective ty = (n:Nat ** (fromFin : (Fin n -> ty) ** (Surjective fromFin)))

These notions are equivalent. We need some helper lemmas... it is quite likely
that these can be cleaned up considerably...

> getIndexOfElem : Data.List.Elem x xs -> Fin (length xs)
> getIndexOfElem Here = FZ
> getIndexOfElem (There later) = FS (getIndexOfElem later)

> getIndexFromAll : All {t} xs -> t -> Fin (length xs)
> getIndexFromAll {xs = []} pf x = absurd (pf x)
> getIndexFromAll {xs = (y :: xs)} pf x = getIndexOfElem (pf x)

> finIndexList : (l:List t) -> Fin (length l) -> t
> finIndexList [] _ impossible
> finIndexList (x :: _) FZ = x
> finIndexList (_ :: xs) (FS y) = finIndexList xs y

> getIndexOfElemLemma : (pf : Data.List.Elem x xs) -> finIndexList xs (getIndexOfElem pf) = x
> getIndexOfElemLemma {xs = (x :: ys)} Here = Refl
> getIndexOfElemLemma {xs = (y :: ys)} (There later) = getIndexOfElemLemma later

> getIndexOfAllLemma : (pf : All {t} xs) -> (x : t) -> finIndexList xs (getIndexFromAll pf x) = x
> getIndexOfAllLemma {xs} pf x with (pf x)
>   getIndexOfAllLemma {xs= x :: ys} pf x | Here = getIndexOfElemLemma (pf x)
>   getIndexOfAllLemma {xs= y :: ys} pf x | (There later) = getIndexOfElemLemma (pf x)

> finIndexListSurjectiveIfAll : All {t} xs -> Surjective (finIndexList xs)
> finIndexListSurjectiveIfAll {xs} pf = \y => ((getIndexFromAll pf y) ** (getIndexOfAllLemma pf y))

> indexIntoAll : All {t} xs -> (f : (Fin (length xs) -> t) ** Surjective f)
> indexIntoAll {xs} pf = ((finIndexList xs) ** (finIndexListSurjectiveIfAll pf))

> natToListFin : (n : Nat) -> List (Fin n)
> natToListFin Z = []
> natToListFin (S n) = (the (Fin (S n)) last) :: (map weaken (natToListFin n))

> lastFinLemma : {n: Nat} -> (((FS k) = last {n=n}) -> Void) -> ((k = last {n=n}) -> Void)
> lastFinLemma {n = Z} {k=_} _ impossible
> lastFinLemma {n = (S Z)} {k = FZ} contra = absurd (contra Refl)
> lastFinLemma {n = (S (S k))} {k = FZ} contra = ?lastFinLemma_rhs_4
> lastFinLemma {n = (S j)} {k = (FS x)} contra = ?lastFinLemma_rhs_3

 lastFinLemma {n = Z} {k = FZ} _ impossible
 lastFinLemma {n = Z} {k = (FS _)} _ impossible

> safeStrengthen : (f : Fin (S n)) -> (contra : (f = last {n=n}) -> Void) -> Fin n
> safeStrengthen {n=Z} FZ contra = absurd (contra Refl)
> safeStrengthen {n=(S k)} FZ contra = FZ
> safeStrengthen {n=(S k)} (FS x) contra = ?ssh_2

> natToListFinIsAll : (n : Nat) -> (All (natToListFin n))
> natToListFinIsAll Z = voidEmptyAll
> natToListFinIsAll (S n) = \f =>
>   case (decEq (the (Fin (S n)) last) f) of
>       Yes pf => rewrite pf in Here
>       No _ => ?newhole -- There (natToListFinIsAll n (safeStrengthen f))

natToListFinIsAll (S Z) = (\FZ => Here)

> getAllFins : (n : Nat) -> (xs : (List (Fin n)) ** All xs)
> getAllFins n = ((natToListFin n) ** (natToListFinIsAll n))

 getAllFins (S k) = ((getAllFinsInner (S k)) ** )

> listableIsFinSurjective : Listable t -> FinSurjective t
> listableIsFinSurjective (xs ** pf) = ((length xs) ** (indexIntoAll pf))

> finSurjectiveToList : FinSurjective t -> List t
> finSurjectiveToList (bd ** (surj ** pf)) = map surj (fst (getAllFins bd))

> finSurjectiveIsListable : FinSurjective t -> Listable t
> finSurjectiveIsListable (bound ** (surj ** pf)) = ?finSurjectiveIsListable_rhs_2

> contrapositive : (a -> b) -> Not b -> Not a
> contrapositive f nb a = nb (f a)

makeAllFin (S k) = ?makeAllFin_rhs_2

> interface Countable t where
>   FromNat : Nat -> t
>   ToNat : t -> Nat

> Countable Nat where
>   FromNat = id
>   ToNat = id

An $n$-place relation on a collection of sets $S_1, S_2,\dots,S_n$ is a set $R\subset
S_1 \times S_2 \times \dots \times S_n$. We say $s_1\in S_1,s_2\in S_2,\dots, s_n\in S_n$
are related by $R$ if $(s_1,s_2,\dots,s_n)\in R$.

> NaryRelation : Vect n Type -> Type
> NaryRelation xs = List (HVect xs) -- for our purposes it is fine to use lists instead of sets

> BinaryRelation : Vect 2 Type -> Type
> BinaryRelation = NaryRelation

> domain : BinaryRelation [xt,yt] -> List yt
> domain [] = []
> domain ([x,y] :: xs) = y :: (domain xs)

> codomain : BinaryRelation [xt,yt] -> List xt
> codomain [] = []
> codomain ([x,y] :: xs) = x :: (codomain xs)

> data PartialFunction : BinaryRelation [xy,yt] -> Type where
>

max_stars_repo_name: nicklecompte/CSLearning

max_issues_repo_name: nicklecompte/CSLearning

max_forks_repo_name: nicklecompte/CSLearning


text:
module Runner

-- Based on https://arxiv.org/pdf/1910.11629.pdf
--          https://github.com/danelahman/haskell-coop

import Src.Eff

data User : (sig : List (Type -> Type)) -> (a : Type) -> Type where
  UC : Eff sig a -> User sig a

Functor (User sig) where
  map f (UC eff) = UC $ eff >>= (\x => Pure $ f x)

Applicative (User sig) where
  pure a = UC $ Pure a

  (UC effF) <*> (UC eff) = UC $ eff >>= (\x => effF >>= (\f => Pure $ f x))

Monad (User sig) where
  (UC eff) >>= f = UC $ eff >>= (\x => let (UC eff') = f x in eff')

data Kernel : (sig : List (Type -> Type)) -> (c : Type) -> (a : Type) -> Type where
  KC : (c -> Eff sig (a, c)) -> Kernel sig c a

Functor (Kernel sig c) where
  map f (KC k) = KC (\c => k c >>= (\(x, c) => Pure (f x, c)))

Applicative (Kernel sig c) where
  pure a = KC (\c => Pure (a, c))

  (KC f) <*> (KC k) = KC (\c => do (f', c') <- f c
                                   (x, c'') <- k c'
                                   Pure (f' x, c''))

Monad (Kernel sig c) where
  (KC k) >>= f = KC (\c => do (x, c') <- k c
                              let (KC k') = f x
                              k' c')

getUserEff : User sig a -> Eff sig a
getUserEff (UC eff) = eff

getKernelEff : c -> Kernel sig c a -> Eff sig (a, c)
getKernelEff c (KC k) = k c

getEnv : Kernel sig c c
getEnv = KC (\c => Pure (c, c))

setEnv : c -> Kernel sig c ()
setEnv c' = KC (\c => Pure ((), c'))

kernel : Kernel sig c a -> c -> (a -> c -> User sig b) -> User sig b
kernel (KC k) c f = UC $ do (x, c') <- k c
                            let (UC eff) = f x c'
                            eff

performU : {auto e : Exists sig eff} -> eff a -> User sig a
performU op = UC (send op)

performK : {auto e : Exists sig eff} -> eff a -> Kernel sig c a
performK op = KC (\c => send op >>= (\x => Pure (x,c)))

data Runner : (sig : List (Type -> Type)) -> (sig' : List (Type -> Type)) -> (c : Type) -> Type where
  Empty : Runner [] sig' c
  CoOps : ({b : Type} -> eff b -> Kernel sig' c b) -> Runner sig sig' c -> Runner (eff :: sig) sig' c

mkRunner : ({b : Type} -> eff b -> Kernel sig c b) -> Runner [eff] sig c
mkRunner coops = CoOps coops Empty

runOp : Runner sig sig' c -> Exists sig eff -> eff b -> Kernel sig' c b
runOp Empty Here _ impossible
runOp Empty (There _) _ impossible
runOp (CoOps coop coops) Here eff = coop eff
runOp (CoOps coop coops) (There e) eff = runOp coops e eff

runAux : Runner sig sig' c -> c -> User sig a -> (a -> c -> User sig' b) -> User sig' b
runAux r c (UC (Pure x)) uf = uf x c
runAux r c (UC (Bind {e} eff f)) uf = kernel (runOp r e eff) c (\x, c' => runAux r c' (UC $ f x) uf)

run : Runner sig sig' c -> User sig' c -> User sig a -> (a -> c -> User sig' b) -> User sig' b
run r ui u uf = ui >>= (\c => runAux r c u uf)

-- Example

testKernel : Kernel [State Int] Int Int
testKernel = do c <- performK Get
                performK (Put (c + 1))
                pure c

testRunner : Runner [Reader Int] [State Int] Int
testRunner = mkRunner  (\Ask => testKernel)

testInit : User [State Int] Int
testInit = do c <- performU Get
              pure (c + 1)

testUser : User [Reader Int] Int
testUser = do x <- performU Ask
              pure x

testFinaliser : Int -> Int -> User [State Int] Int
testFinaliser x c = pure x

testRun : User [State Int] Int
testRun = run testRunner testInit testUser testFinaliser

test : (Int, Int)
test = run $ runState 0 $ getUserEff testRun

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Data.Vect

tri : Vect 3 (Double, Double)
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

Position : Type
Position = (Double, Double)

tri' : Vect 3 Position
tri' = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

Polygon : Nat -> Type
Polygon n = Vect n Position

tri'' : Polygon 3
tri'' = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]


text:
import Data.List

-- Taken from http://nicolas.biri.name/posts/2016-07-26-union-type-in-idris-part-1.html
data Union : List Type -> Type where
  MemberHere : ty -> Union (ty::ts)
  MemberThere : Union ts -> Union (ty::ts)

member : ty -> {auto e: Elem ty ts} -> Union ts
member x {e = Here} = MemberHere x
member x {e = There later} =
    MemberThere (member x {e = later})

x : Union [String, Nat, List String]
x = member "Ahoy!"

y : Union [String, Nat, List String]
y = member (S Z)

max_stars_repo_name: janschultecom/seo-router

max_issues_repo_name: janschultecom/seo-router

max_forks_repo_name: janschultecom/seo-router


text:
> module Exists.Operations

> import Pairs.Operations

> %default total

> %access public export

> |||
> outl : {A : Type} -> {P : A -> Type} -> Exists {a = A} P -> A
> outl = getWitness

> |||
> outr : {A : Type} -> {P : A -> Type} -> (s : Exists {a = A} P) -> P (outl s)
> outr = getProof


text:
module Libra.CLI

import Effects
import Effect.File
import Effect.StdIO
import Effect.System

%access export

help : String
help = """
  libra-cli v0.1 - A Lisp Parser

  Usage:

      libra-cli path/to/file.lisp
"""

cli : Eff () [SYSTEM, STDIO, FILE_IO]
cli = do [program, fileName] <- getArgs | _ => putStrLn help
         source <- readFile fileName
         putStrLn $ source

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module Effekt.IteratedStaged

import Effekt.CpsStaged
import Effekt.IteratedUnstaged

STM : List Type -> Type -> Type
STM [] a = Exp a
STM (r :: rs) a = (Exp a -> STM rs r) -> STM rs r

pure : Exp a -> STM rs a
pure{  rs= []}         a = a
pure{  rs= r :: rs}  a = \k => k a

push : (Exp a -> STM (r :: rs) b) -> (Exp b -> STM rs r) -> (Exp a -> STM rs r)
push f k = \a => f a k

bind : STM rs a -> (Exp a -> STM rs b) -> STM rs b
bind{  rs= []}         m f = f m
bind{  rs= r :: rs}  m f = \k => m (push f k)

(>>=) : STM rs a -> (Exp a -> STM rs b) -> STM rs b
(>>=) = bind

lift : STM rs a -> STM (r :: rs) a
lift = bind

shift0 : ((Exp a -> STM rs r) -> STM rs r) -> STM (r :: rs) a
shift0 = id

runIn0 : STM (r :: rs) a -> (Exp a -> STM rs r) -> STM rs r
runIn0 = id

reset0 : STM (a :: rs) a -> STM rs a
reset0 m = runIn0 m pure

mutual
  reify : STM rs a -> Exp (Stm rs a)
  reify {rs = []} m = m
  reify {rs = (q :: qs)} m =
    (Lam $ \ k =>  reify (m (\a => reflect {a = q} {rs = qs} (App k  a))))

  reflect : Exp (Stm rs a) -> STM rs a
  reflect {rs = []} m = m
  reflect {rs = (q :: qs)} m =
    \k => reflect (App m  ((Lam $ \ a =>  reify (k a))))

emit : Exp Int -> STM (List Int :: rs) ()
emit {rs} a = shift0 (\c => do
  as <- c Uni
  pure {rs} (Con a as))

emitTwice : Exp Int -> STM (List Int :: List Int :: rs) ()
emitTwice {rs} a =
  bind {rs=List Int::List Int::rs} (emit {rs=List Int::rs} a) (\u =>
  lift {r=List Int} {rs=List Int::rs} (emit a))

export
reifiedEmitTwice : Exp (Int -> Stm [List Int,List Int] ())
reifiedEmitTwice = Lam (\x => reify {rs=[List Int,List Int]} (emitTwice x))

export
reifiedEmitTwice' : Exp (Int -> Stm [List Int,List Int,()] ())
reifiedEmitTwice' = Lam (\x => reify {rs=[List Int,List Int,()]} (emitTwice {rs=[()]} x))

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
module Replica.TestConfig.Core

import public Data.List
import Data.Strings

public export
Path : Type
Path = DPair (List String) NonEmpty

public export
record TestConfigM (m : Type -> Type) where

  constructor MkTestConfig

  exec : m String
  path : m Path
  params : m String
  inputFile : m (Maybe String)
  outputFile : m String

public export
TestConfig : Type
TestConfig = TestConfigM id

public export
BuildTestConfig : Type
BuildTestConfig = TestConfigM List

public export
data BuildError = CantBuild

defaultOutput : String
defaultOutput = "output"

public export
emptyBuilder : BuildTestConfig
emptyBuilder = MkTestConfig [] [] [] [] []

public export
implementation Semigroup BuildTestConfig where
  (<+>) x y
    = MkTestConfig
        (x.exec <+> y.exec)
        (x.path <+> y.path)
        (x.params <+> y.params)
        (x.inputFile <+> y.inputFile)
        (x.outputFile <+> y.outputFile)

public export
implementation Monoid BuildTestConfig where
  neutral = emptyBuilder

public export
build : BuildTestConfig -> Either BuildError TestConfig
build (MkTestConfig [exec] [path] params mInput mOutputFile) = do
  let Just inputFile = case mInput of
                        [] => Just Nothing
                        [x] => Just x
                        _ => Nothing
    | _ => Left CantBuild
  let Just outputFile = case mOutputFile of
                             [] => Just defaultOutput
                             [x] => Just x
                             _ => Nothing
    | _ => Left CantBuild
  pure $ MkTestConfig exec path (unwords params) inputFile outputFile
build _ = Left CantBuild

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
removeFromList: Eq a => (elem: a) -> List a -> List a
removeFromList elem [] = []
removeFromList elem (head :: tail) =
  if   elem == head
  then removeFromList elem tail
  else head :: (removeFromList elem tail)

example1: List Int
example1 = [1,2,3,1,2,3]


text:
module Part2.Sez10_2e
import Data.List.Views
import Data.Nat.Views

%default total

{- some excrcises from sec 10.2 -}

{- equalSuffix excercise, should convert to Haskell (using slower snocList from Sez10_2a_snoc) -}
equalSuffixHelper : Eq a => List a -> List a -> List a
equalSuffixHelper input1 input2 with (snocList input1)
    equalSuffixHelper [] input2 | Empty = []
    equalSuffixHelper (xs ++ [x]) input2 | (Snoc rec1) with (snocList input2)
        equalSuffixHelper (xs ++ [x]) [] | (Snoc rec1) | Empty = []
        equalSuffixHelper (xs ++ [x]) (ys ++ [y]) | (Snoc rec1) | (Snoc rec2)
              = if x == y then x :: equalSuffixHelper xs ys | rec1 | rec2 else []

equalSuffix : Eq a => List a -> List a -> List a
equalSuffix xs ys = reverse (equalSuffixHelper xs ys)

{-
idris repl
*Part2/Sez10_2e> equalSuffix [1,2,4,5] [1..5]
[4, 5] : List Integer
-}

{- other excercises use even more advanced views, I expect harder time to create
performant Haskell version -}

{- toBinary
uses

data HalfRec : Nat -> Type where
     HalfRecZ : HalfRec Z
     HalfRecEven : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (n + n)
     HalfRecOdd : {n : Nat} -> (rec : Lazy (HalfRec n)) -> HalfRec (S (n + n))
-}
-- TODO the following compiles and prints out gibberish  when executed
-- toBinary' : Nat -> String
-- toBinary' n with (halfRec n)
--   toBinary' Z | HalfRecZ = "0"
--   toBinary' (x + x) |  HalfRecEven rec = (toBinary' x | rec) ++ "0"
--   toBinary' (S (x + x)) | HalfRecOdd rec = if x == Z then "1" else (toBinary' x | rec) ++ "1"

toBinary : (n : Nat) -> String
toBinary Z = "0"
toBinary k = go k []
  where
    go : (n : Nat) -> (acc : List Char) -> String
    go n acc with (halfRec n)
      go Z acc | HalfRecZ = pack acc
      go (x + x) acc | (HalfRecEven rec) = go x ('0' :: acc) | rec
      go (S (x + x)) acc | (HalfRecOdd rec) = go x ('1' :: acc) | rec

{-
*Part2/Sez10_2e> toBinary 42
"101010" : String
-}

{- palindrome, I expect linear cost vList will be hard to implement -}
palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
   palindrome [] | VNil = True
   palindrome [x] | VOne = True
   palindrome (x :: xs ++ [y]) | VCons rec
       = if x == y then palindrome xs | rec else False

{-
idris repl
*Part2/Sez10_2e> :l Part2/Sez10_2e
Type checking ./Part2/Sez10_2e.idr
*Part2/Sez10_2e> palindrome (unpack "abccba")
True : Bool
*Part2/Sez10_2e> palindrome (unpack "abcba")
True : Bool
*Part2/Sez10_2e> palindrome (unpack "abccb")
False : Bool
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Data.Time.Calendar.OrdinalDate

import Data.Time.Calendar.Days
import public Data.Time.Calendar.Types

import Text.Format.Decimal

%default total

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

export isLeapYear : Year -> Bool
isLeapYear y = (y `mod` 4 == 0) && ((y `mod` 400 == 0) || (y `mod` 100 /= 0))

||| Convert to ISO 8601 Ordinal Date format.
export toOrdinalDate : Day -> (Year, DayOfYear)
toOrdinalDate (ModifiedJulianDay mjd) =
  let a        = mjd + 678575
      quadcent = a `div` 146097
      b        = a `mod` 146097
      cent     = min (b `div` 36524) 3
      c        = b - (cent * 36524)
      quad     = c `div` 1461
      d        = mod c 1461
      y        = min (d `div` 365) 3
   in (quadcent * 400 + cent * 100 + quad * 4 + y + 1,
       fromInteger (d - (y * 365) + 1))

showOrdinalDate : Day -> String
showOrdinalDate x with (toOrdinalDate x)
  showOrdinalDate x | (y, dy) = format' (zeroPad 4) y ++ format' (zeroPad 2) dy

||| Convert from ISO 8601 Ordinal Date format.
||| Invalid day numbers will be clipped to the correct range (1 to 365 or 366).
export fromOrdinalDate : Year -> DayOfYear -> Day
fromOrdinalDate year day =
  let y  = year - 1
      yl = if isLeapYear year then 366 else 365
      d' = cast $ if day < 1 then 1 else if day > yl then yl else day
    in ModifiedJulianDay $ d' + (365 * y) + (y `div` 4) - (y `div` 100) + (y `div` 400) - 678576

||| Convert from ISO 8601 Ordinal Date format.
||| Invalid day numbers return 'Nothing'
export fromOrdinalDateValid : Year -> DayOfYear -> Maybe Day
fromOrdinalDateValid year day =
  let y  = year - 1
      yl = if isLeapYear year then 366 else 365
    in if day < 0 || day > yl then Nothing
       else Just $ ModifiedJulianDay $ cast day + (365 * y) + (y `div` 4) - (y `div` 100) + (y `div` 400) - 678576

-- ||| Show in ISO 8601 Ordinal Date format (yyyy-ddd)
-- showOrdinalDate :: Day -> String
-- showOrdinalDate date = (show4 y) ++ "-" ++ (show3 d)
--   where
--         (y, d) = toOrdinalDate date

||| Get the number of the Monday-starting week in the year and the day of the week.
||| The first Monday is the first day of week 1, any earlier days in the year are week 0 (as @%W@ in 'Data.Time.Format.formatTime').
|||  Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
export mondayStartWeek : Day -> (WeekOfYear, Int)
mondayStartWeek date =
  let yd = snd $ toOrdinalDate date
      d = date.modifiedJulianDay + 2
      k = d - cast yd
   in (fromInteger ((d `mod` 7) - (k `div` 7)), fromInteger (d `mod` 7) + 1)

||| Get the number of the Sunday-starting week in the year and the day of the week.
||| The first Sunday is the first day of week 1, any earlier days in the year are week 0 (as @%U@ in 'Data.Time.Format.formatTime').
||| Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
export sundayStartWeek : Day -> (WeekOfYear, Int)
sundayStartWeek date =
  let yd = snd $ toOrdinalDate date
      d  = date.modifiedJulianDay + 3
      k = d - cast yd
   in (fromInteger ((d `div` 7) - (k `div` 7)), fromInteger (mod d 7))

||| The inverse of 'mondayStartWeek'. Get a 'Day' given the year,
||| the number of the Monday-starting week, and the day of the week.
||| The first Monday is the first day of week 1, any earlier days in the year
||| are week 0 (as @%W@ in 'Data.Time.Format.formatTime').
export
fromMondayStartWeek : Year -- ^ Year.
                    -> WeekOfYear -- ^ Monday-starting week number (as @%W@ in 'Data.Time.Format.formatTime').
                    -> Int -- ^ Day of week.
                           -- Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
                    -> Day
fromMondayStartWeek year w d =
  let firstDay = fromOrdinalDate year 1 -- first day of the year
      zbFirstMonday = (5 - firstDay.modifiedJulianDay) `mod` 7 -- 0-based year day of first monday of the year
      zbWeek = w - 1 -- 0-based week of year
      zbDay = d - 1 -- 0-based day of week
      zbYearDay = zbFirstMonday + 7 * cast zbWeek + cast zbDay -- 0-based day in year
   in addDays zbYearDay firstDay

export
fromMondayStartWeekValid : Year -- ^ Year.
                         -> WeekOfYear -- ^ Monday-starting week number (as @%W@ in 'Data.Time.Format.formatTime').
                         -> Int -- ^ Day of week.
                                -- Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
                         -> Maybe Day
fromMondayStartWeekValid year w d =
 if d < 1 || d > 7 then Nothing
 else
   let firstDay = fromOrdinalDate year 1 -- first day of the year
       zbFirstMonday = (5 - firstDay.modifiedJulianDay) `mod` 7 -- 0-based week of year
       zbWeek = w - 1 -- 0-based week number
       zbDay = d - 1 -- 0-based day of week
       zbYearDay = zbFirstMonday + 7 * cast zbWeek + cast zbDay -- 0-based day in year
     in if zbYearDay < 0 || zbYearDay > (if isLeapYear year then 365 else 364)
           then Nothing
           else Just $ addDays zbYearDay firstDay

||| The inverse of 'sundayStartWeek'. Get a 'Day' given the year and
||| the number of the day of a Sunday-starting week.
||| The first Sunday is the first day of week 1, any earlier days in the
||| year are week 0 (as @%U@ in 'Data.Time.Format.formatTime').
export
fromSundayStartWeek : Year -- ^ Year.
                    -> WeekOfYear -- ^ Sunday-starting week number (as @%U@ in 'Data.Time.Format.formatTime').
                    -> Int -- ^ Day of week
                           -- Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
                    -> Day
fromSundayStartWeek year w d =
 let firstDay = fromOrdinalDate year 1 -- first day of the year
     zbFirstSunday = (4 - firstDay.modifiedJulianDay) `mod` 7 -- 0-based year day of first monday of the year
     zbWeek = w - 1 -- 0-based week of year
     zbDay = d -- 0-based day of week
     zbYearDay = zbFirstSunday + 7 * cast zbWeek + cast zbDay -- 0-based day in year
  in addDays zbYearDay firstDay

export
fromSundayStartWeekValid : Year -- ^ Year.
                         -> WeekOfYear -- ^ Sunday-starting week number (as @%U@ in 'Data.Time.Format.formatTime').
                         -> Int -- ^ Day of week.
                                -- Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
                         -> Maybe Day
fromSundayStartWeekValid year w d =
  if d < 0 || d > 6 then Nothing
  else
    let firstDay = fromOrdinalDate year 1 -- first day of the year
        zbFirstSunday = (4 - firstDay.modifiedJulianDay) `mod` 7 -- 0-based week of year
        zbWeek = w - 1 -- 0-based week number
        zbYearDay = zbFirstSunday + 7 * cast zbWeek + cast d -- 0-based day in year
     in if zbYearDay < 0 || zbYearDay > (if isLeapYear year then 365 else 364)
           then Nothing
           else Just $ addDays zbYearDay firstDay

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


text:
module Main

import Effect.Random
import Effect.StdIO
import Effects
import Data.Vect

-- import Probability.Core
-- import Probability.Monad

%default total

{- Probabilistic programming -}

data Prob : Type -> Type where
  Binomial : Nat -> Double -> Prob Nat
  Certainly : a -> Prob a
  Bind : (Prob a) -> (a -> Prob b) -> Prob b
  CustomDist : Vect (S n) (a, Double) -> Prob a

Show a => Show (Prob a) where
  show (Binomial n p) = "Binomial " ++ (show n) ++ " " ++ (show p)
  show (Certainly a) = "Certainly " ++ (show a)
  show (Bind (Binomial n p) _) = "Bind (" ++ (show $ Binomial n p) ++ ") <function>"
  show (Bind a _) = "Bind <dist> <function>"
  show (CustomDist d) = "CustomDist " ++ (show d)

-- NOTE: It seems Idris won't accept this as total unless I handle the
-- 'impossible' case (that's also why choose wasn't reducing at compile time).
zeroSum : {a: Nat} -> {b: Nat} -> (a + b = 0) -> Either Void ((a = 0), (b = 0))
zeroSum {a = Z} Refl = Right (Refl, Refl)
zeroSum {a} {b = Z} prf = Right (replace {P = \x => x = 0} (plusZeroRightNeutral a) prf, Refl)
zeroSum {a = S a} {b = S b} prf = Left $ SIsNotZ prf

factNZ : {k: Nat} -> Not (fact k = Z)
factNZ {k = Z} p = SIsNotZ p
factNZ {k = (S k)} p = case zeroSum p of
  Left v => v
  Right (q1, _) => factNZ q1

-- factBetween : Nat -> Nat -> Nat
-- factBetween n m = if n == m then n else if n > m then 0 else  (factBetween n (pred m)) * (m)

total
choose : Nat -> Nat -> Nat
choose _ Z = 1
choose (S n) (S Z) = S n
choose Z (S _) = 0
-- if n < k then n `choose` k = 0
choose n k = divNatNZ (divNatNZ (fact n) (fact (n `minus` k)) factNZ) (fact k) factNZ

chooseZero : {n: Nat} -> choose n Z = 1
chooseZero = Refl

chooseOne : {n: Nat} -> choose (S n) 1 = S n
chooseOne = Refl

-- chooseNLessK : choose n (n + m + 1) = 0
-- chooseNLessK = ?csdvsd

total
binomialPMF : Nat -> Double -> Nat -> Double
binomialPMF n p k = cast (n `choose` k) * (p `pow` k) * ((1.0 - p) `pow` (n `minus` k))

splitBy : (a -> Bool) -> List a -> (List a, List a)
splitBy _ [] = ([], [])
splitBy pred (x::xs) = let (s, t) = splitBy pred xs in
  if pred x then (x::s, t) else (s, x::t)

gatherer : (Eq a, Eq p, Num p) => List (a,p) -> List (a,p) -- copied from https://github.com/lambdacasserole/probability/blob/master/src/Probability/Core.idr
gatherer [] = []
gatherer ((x,p) :: xs) = assert_total $  -- why is assert_total needed?
   let lyln = splitBy (\(z,_) => z == x) xs
       newp = (+) p . sum $ map snd (fst lyln)
   in  (x,newp) :: gatherer (snd lyln)

-- vectNatEnumFromTo : (a, b: Nat) -> {auto prf: LTE a b} -> Vect (b - a + 1) Nat
-- vectNatEnumFromTo a b = vectNatEnumFromTo' a (b - a) where
--   vectNatEnumFromTo' a Z = [a]
--   vectNatEnumFromTo' a (S n) = a :: vectNatEnumFromTo' (a + 1) n

-- cartesianProduct : Vect n a -> (a -> Vect m b) -> Vect (n * m) (a, b)
-- cartesianProduct [] _ = []
-- cartesianProduct {n} {m = Z} _ _ = rewrite multZeroRightZero n in []
-- cartesianProduct (x::xs) fys = ((\y => (x, y)) <$> fys x) ++ cartesianProduct xs fys
--
-- cartesianProduct' : Vect n a -> (a -> (m: Nat ** Vect m b)) -> Vect (n * m) (a, b)
-- cartesianProduct' xs fys = cartesianProduct xs (DPair.snd . fys)

concatNonempty' : Vect n (m: Nat ** Vect (S m) a) -> (k: Nat ** Vect k a)
concatNonempty' [] = (_ ** [])
concatNonempty' (x1::xs) = (_ ** (snd x1) ++ (snd (concatNonempty' xs)))

concatNonempty : Vect (S n) (m: Nat ** Vect (S m) a) -> (k: Nat ** Vect (S k) a)
concatNonempty [x] = x
-- concatNonempty [x1, x2] = (_ ** (snd x1) ++ (snd x2))
concatNonempty (x1::xs) = (_ ** (snd x1) ++ (snd (concatNonempty' xs)))

total
runProb : Prob a -> (k: Nat ** Vect (S k) (a, Double))
runProb (Binomial n p) = (_ ** (\k => (k, binomialPMF n p k)) <$> 0 :: fromList [1..n])
runProb (Certainly a) = (_ ** [(a, 1.0)])
-- runProb {a} (Bind probA f) = (_ ** (\((_,w),(y,q)) => (y, q*w)) <$> cartesianProduct {m = m} (DPair.snd {x = runProb probA}) f'') where
--   f' : (a: Type) -> (b, Double) -> (l: Nat ** Vect (S l) (a, Double))
--   f' a (y,_) = runProb {a = a} ?dxdv --(f x)
--   f'' y' = DPair.snd {x = (f' a y')}
--   m = S $ DPair.fst (f' (head (DPair.snd (runProb probA))))
runProb {a} (Bind probA f) =
  concatNonempty (snd joinedPartly) -- unjoined = (\(pA,p) => (runProb pA, p)) <$> probfAs in
  where
    probfAs : (k: Nat ** Vect (S k) ((l: Nat ** Vect (S l) (a, Double)), Double))
    probfAs = assert_total (_ ** (\(x,p) => (runProb (f x), p)) <$> snd (runProb (assert_smaller (Bind probA f) probA)))
    joinedPartly : (k: Nat ** Vect (S k) (l: Nat ** Vect (S l) (a, Double)))
    joinedPartly = (_ ** (\((_**dist),p) => (_ ** (\(x,q) => (x, p*q)) <$> dist)) <$> snd probfAs)
    -- joinedPartly = (_ ** ?cbfdbdb <$> probfAs)
runProb (CustomDist d) = (_ ** d)

Functor Prob where
  map f (Certainly a) = Certainly $ f a
  map f (Bind a g) = Bind a (\x => f <$> g x)
  map f (CustomDist d) = CustomDist $ (\(x, p) => (f x, p)) <$> d
  map f p = CustomDist $ (\(x, p) => (f x, p)) <$> (snd $ runProb p)

Applicative Prob where
  pure = Certainly
  (Certainly f) <*> p = f <$> p
  (Bind pa f) <*> p = Bind pa (\a => (f a) <*> p)
  -- (CustomDist d) <*> p = CustomDist [ (f x, q*w) | (f,w) <- d, (x,q) <- runProb p ] -- copied from https://github.com/lambdacasserole/probability/blob/master/src/Probability/Core.idr
  (CustomDist d) <*> p = Bind (CustomDist d) (\f => Bind p (pure . f))

Monad Prob where
  (Certainly a) >>= f = f a
  (Bind fa f) >>= g = fa >>= (\a => (f a) >>= g)
  fa >>= f = Bind fa f

gather : (Eq a) => Prob a -> Prob a
-- FIXME: Adapt this function for vects
-- gather (CustomDist d) = CustomDist (gatherer d)
-- gather (Bind pa f) = pa >>= (\a => gather $ f a) -- FIXME: Might not gather completely because pa not gathered
gather p = p

mortalityRate : Double
mortalityRate = 0.03

binomial : Nat -> Double -> Prob Nat
binomial = Binomial

kill : (population: Nat) -> Double -> Prob Nat
kill = binomial

replace : Nat -> Nat -> Prob (Nat, Nat)
replace n1 n2 = gather $ replace' <$> binomial (n1 + n2) ((cast n1) / (cast (n1 + n2))) where
  replace' n1' = (n1', (n1 + n2) `minus` n1')

step : Nat -> Nat -> Prob (Nat, Nat)
step n1 n2 = gather $ do
  dead1 <- kill n1 mortalityRate
  dead2 <- kill n2 mortalityRate
  gather $ (\(new1,new2) => ((n1 `minus` dead1) + new1, (n2 `minus` dead2) + new2)) <$> replace dead1 dead2

simulate : Nat -> Nat -> Nat -> Prob (Nat, Nat)
simulate species1Initial species2Initial Z = pure (species1Initial, species2Initial)
simulate species1Initial species2Initial (S k) = gather $ do
  (n1, n2) <- step species1Initial species2Initial
  gather $ simulate n1 n2 k

{- Error propagation -}

data Uncertain value = MkUncertain value value

interface SquareRootable a where
  sqrt : a -> a

SquareRootable Double where
  sqrt = Doubles.sqrt

square : Num a => a -> a
square a = a * a

norm : (Num a, SquareRootable a) => List a -> a
norm values = sqrt $ sum (square <$> values)

(Fractional value, SquareRootable value) => Num (Uncertain value) where
  -- FIXME: Account for correlation
  (+) (MkUncertain a aUncertainty) (MkUncertain b bUncertainty) = MkUncertain (a + b) (norm [aUncertainty, bUncertainty])
  (*) (MkUncertain a aUncertainty) (MkUncertain b bUncertainty) = (MkUncertain (a * b) (a * b * norm [aUncertainty/a, bUncertainty/b]))
  fromInteger i = MkUncertain (fromInteger i) 0

(SquareRootable value, Fractional value) => Fractional (Uncertain value) where
  (MkUncertain a aUncertainty) / (MkUncertain b bUncertainty) = MkUncertain (a / b) (a / b * norm [aUncertainty/a, bUncertainty/b])

Show value => Show (Uncertain value) where
  show (MkUncertain a aUncertainty) = show a ++ " +- " ++ show aUncertainty

interface Scalable a where
  (*) : a -> Double -> a

Scalable Double where
  (*) = Interfaces.(*)

mean : (Scalable a, Num a) => (prob: Prob a) -> a
mean (Binomial n p) = (Main.(*) n p) -- probably not what you want
mean (Certainly a) = a
mean (CustomDist d) = sum [x * p | (x, p) <- d]
mean (Bind pa f) = sum [x * p | (x, p) <- snd $ runProb (pa >>= f)]

-- population standardDeviation (QUESTION: should it be sample instead?)
standardDeviation : (SquareRootable a, Scalable a, Neg a) => (prob: Prob a) -> a
standardDeviation (Binomial n p) = sqrt (Main.(*) (Main.(*) n p) (1.0 - p)) -- probably not what you want
standardDeviation (Certainly _) = 0
standardDeviation (CustomDist d) = let mu = mean (CustomDist d) in
  sqrt $ sum [square (mu - x) * p | (x, p) <- d]
standardDeviation (Bind pa f) = let mu = mean (Bind pa f) in
  sqrt $ sum [square (mu - x) * p | (x, p) <- snd $ runProb (pa >>= f)]

probToUncertain : (SquareRootable a, Scalable a, Neg a, Fractional a) => (prob: Prob a) -> Uncertain a
probToUncertain dist = MkUncertain (mean dist) (Main.(*) (standardDeviation dist) 0.5)

{- Estimate distributions by sampling (Monte Carlo) -}

select : Double -> Vect (S n) (a, Double) -> Double -> a
select _ [(x, p)] _ = x
select target ((x, p)::xps) current =
  if target >= current + p
    then x
    else case xps of
      [] => x
      (xp::xps') => select target (xp::xps') (current + p)

-- Copied from https://bl.ocks.org/justinmanley/f2e169feb32e06e06c2f
||| Naively generate a (pseudo)-random float between 0 and 1.
rndDouble : Integer -> Eff Double [RND]
rndDouble max = do
	rnd <- assert_total $ rndInt 0 max
	pure (fromInteger rnd / fromInteger max)

sample : Prob a -> Eff a [RND, STDIO]
sample (Bind prob f) = do
  observedFromProb <- sample prob
  putStrLn "Bind: sampled prob"
  result <- sample (f observedFromProb)
  putStrLn "Bind: sampled f _"
  pure result
sample prob = do
  putStrLn "Sampling from an arbitrary distribution"
  probability <- rndDouble (2 `pow` 20)
  (_ ** dist) <- pure (runProb prob)
  pure $ select probability dist 0.0

Applicative (Pair Int) where
  pure a = (0, a)

  f <*> fa = (fst fa, (snd f) (snd fa))

main : IO ()
main = do
  dist <- pure (simulate 1 1 3)
  putStrLn "dist"
  printLn dist
  printLn (gatherer $ toList (snd (runProb dist)))
  printLn $ (MkUncertain 0.172807 0.000008) / ((MkUncertain 13.7 0.3) * (MkUncertain 1.0 0.1)) -- 0.013 ± 0.001 (https://chem.libretexts.org/Bookshelves/Analytical_Chemistry/Supplemental_Modules_(Analytical_Chemistry)/Quantifying_Nature/Significant_Digits/Propagation_of_Error)
  printLn $ probToUncertain (cast {to=Double} <$> binomial 5 0.5) -- 2.5 +- 0.559
  -- printLn (run $ sample (simulate 1 1 3))


text:
-- IO is what we use to sequence of interactions, a bit like Future in
-- Java, but there's no .get(), and it's not started yet when our function runs.

-- IO is a generic type, so a String -> IO Int function is one that takes a
-- String as an input and gives a description of an interactive program that
-- produces an Int, e.g., readAndGetLength, displays the input as a prompt,
-- reads another String from the console and gives the length of that String.

-- There's notation to make sequencing the operations easier.

module Main

import System
import Data.Vect

main : IO ()
main = do
  putStr "Enter your name: "
  x <- getLine
  putStrLn ("Hello " ++ x ++ "!")

-- Equivalent to something like:
main2 : IO ()
main2 =
  putStr "Enter your name: " >>=
  (\_ => getLine >>= (\x =>
    putStrLn ("Hello " ++ x ++ "!")))

-- Or in Java:
-- public static Future<Void> main() {
--   return putStr("Enter your name: ")
--     .flatMap(ignored -> getLine()
--       .flatMap(x -> putStrLn("Hello " + x + "!")));
-- }

-- In the REPL, :c hello produces a binary, hello.

-- >>= (bind, flatMap) works for other types too, not just IO, e.g., List, Vect.
-- That's due to it being defined for Monad or Applicative.

-- Exercise 1 - read two strings and print the length of the longer
printLonger : IO ()
printLonger = do
  putStr "First: "
  first <- getLine
  putStr "second: "
  second <- getLine
  putStrLn ("Max length: " ++ show (if length first > length second then length first else length second))

-- Exercise 2 - same usin >>= instead of do
printLonger2 : IO ()
printLonger2 =
  putStr "First: " >>=
  (\_ => getLine >>=
  (\first => putStr "second: " >>=
  (\_ => getLine >>=
  (\second => putStrLn ("Max length: " ++ show (if length first > length second then length first else length second))))))

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

--readNumbers: IO (Maybe (Nat, Nat))
--readNumbers = do
--  num1 <- readNumber
--  case num1 of
--    Nothing => pure Nothing
--    Just num1_ok => do
--      num2 <- readNumber
--      case num2 of
--        Nothing => pure Nothing
--        Just num2_ok => pure (Just (num1_ok, num2_ok))

readPair : IO (String, String)
readPair = do
  str1 <- getLine
  str2 <- getLine
  pure (str1, str2)

usePair : IO ()
usePair = do
  (str1, str2) <- readPair
  putStrLn ("You entered " ++ str1 ++ " and " ++ str2)

readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
  Just num1_ok <- readNumber | Nothing => pure Nothing
  Just num2_ok <- readNumber | Nothing => pure Nothing
  pure (Just (num1_ok, num2_ok))

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Lift off!"
countdown (S k) = do
  putStrLn (show (S k))
  usleep 1000000
  countdown k

countdowns : IO ()
countdowns = do
  putStr "Enter starting number: "
  Just startNum <- readNumber | Nothing => do
    putStrLn "Invalid input"
    countdowns
  countdown startNum
  putStr "Another (y/n)? "
  yn <- getLine
  if yn == "y" then countdowns else pure ()

-- Exercises 1, 2, 3 - guessing game

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses = do
  putStr ("Guess " ++ (show guesses) ++ ": ")
  Just guessed <- readNumber | Nothing => do
    putStrLn "Invalid guess"
    guess target guesses
  if guessed < target then do
    putStrLn "Too low"
    guess target (guesses + 1)
  else if guessed > target then do
    putStrLn "Too high"
    guess target (guesses + 1)
  else do
    putStrLn "That's right!"
    pure ()

guessGame : IO ()
guessGame = do
  x <- time
  guess (cast (mod x 100 + 1)) 1

-- Exercise 4 - own versions of repl and replWith
-- Prelude.Interactive.repl : (prompt : String) ->
--    (onInput : String -> String) -> IO ()
--    A basic read-eval-print loop
--    Arguments:
--        prompt : String  -- the prompt to show

--        onInput : String -> String  -- the function to run on reading input,
--        returning a String to output
intr : (prompt : String) -> (onInput : String -> String) -> IO ()
intr prompt onInput = do
  putStrLn prompt
  input <- getLine
  putStrLn (onInput input)
  intr prompt onInput

-- Prelude.Interactive.replWith : (state : a) ->
--    (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> IO ()
--    A basic read-eval-print loop, maintaining a state
--    Arguments:
--        state : a  -- the input state

--        prompt : String  -- the prompt to show

--        onInput : a -> String -> Maybe (String, a)  -- the function to run on
--        reading input, returning a String to output and a new state. Returns
--        Nothing if the repl should exit

intrWith : (state : a) -> (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> IO ()
intrWith state prompt onInput = do
  putStrLn prompt
  input <- getLine
  let Just (toOutput, newState) = onInput state input | Nothing => do pure ()
  putStrLn toOutput
  intrWith newState prompt onInput

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do
  line <- getLine
  xs <- readVectLen k
  pure (line :: xs)

data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

readVect : IO (VectUnknown String)
readVect = do
  putStr "Number of elements: "
  Just len <- readNumber | Nothing => do
    putStrLn "Invalid length"
    readVect
  values <- readVectLen len
  pure (MkVect len values)

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")")

-- dependent pair - a pair where the second value's type is related to the
-- first value.
anyVect : (n : Nat ** Vect n String)
anyVect = (2 ** ["hello", "world"])

readVect2 : IO (n : Nat ** Vect n String)
readVect2 = do
  x <- getLine
  if x == ""
    then pure (_ ** [])
    else do
      (_ ** xs) <- readVect2
      pure (_ ** x :: xs)

zipInputs : IO ()
zipInputs = do
  (len1 ** vec1) <- readVect2
  (len2 ** vec2) <- readVect2
  case exactLength len1 vec2 of
    Nothing => putStrLn "Vectors are of different lengths"
    Just vec2' => printLn (zip vec1 vec2')

-- Exercise 1 - write readToBlank, reads input until user enters a blank line
readToBlank : IO (List String)
readToBlank = do
  line <- getLine
  if line == ""
    then pure []
    else do
      tail <- readToBlank
      pure (line :: tail)

-- Exercise 2 - write a function to read input until user enters a blank line,
-- then reads a filename and saves it to that file
readToFile : IO ()
readToFile = do
  list <- readToBlank
  filename <- getLine
  Right () <- writeFile filename (show list) | Left err => putStrLn (show err)
  pure ()

-- Exercise 3 - write a function that reads the contents of a file into a
-- dependent pair containing a length and a Vect of that length. Any errors =>
-- empty vector.
readVectHandle : (file : File) -> IO (n ** Vect n String)
readVectHandle file = do
  Right text <- fGetLine file | Left err => pure (_ ** [])
  if text == ""
    then pure (_ ** [])
    else do
      (n ** xs) <- readVectHandle file
      pure (1 + n ** text :: xs)

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
  Right handle <- openFile filename Read | Left err => pure (_ ** [])
  result <- readVectHandle handle
  closeFile handle
  pure result

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
--    Copyright 2017, the blau.io contributors
--
--    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.

module API.Web.DOM.EventTarget

import API.Web.DOM.Document
import API.Web.DOM.DocumentType
import API.Web.DOM.Element
import API.Web.DOM.Event
import API.Web.DOM.EventListener
import API.Web.DOM.Node
import API.Web.HTML.Document
import API.Web.HTML.Window
import API.Web.XHR.XMLHttpRequest
import API.Web.XHR.XMLHttpRequestEventTarget
import IdrisScript

%access public export
%default total

||| An EventTarget represents the target to which an event is dispatched when
||| something has occured.
|||
||| The original interface specification can be found at
||| https://dom.spec.whatwg.org/#interface-eventtarget
data EventTarget : Type where
  FromNode   : Node                      -> EventTarget
  FromWindow : Window                    -> EventTarget
  FromXHR    : XMLHttpRequestEventTarget -> EventTarget

record EventListenerOptions where
  constructor NewEventListenerOptions
  ||| When set to true, capture prevents **callback** from being invoked when
  ||| the event's `eventPhase` attribute value is `BUBBLING_PHASE`. When false,
  ||| **callback** will not be invoked when event's `eventPhase` attribute value
  ||| is `CAPTURING_PHASE`. Either way, **callback** will be invoked if event's
  ||| `eventPhase` attribute value is `AT_TARGET`. Default is `false`.
  capture : Bool

||| AddEventListenerOptions sets listener-specific options.
record AddEventListenerOptions where
  constructor NewAddEventListenerOptions
  eventListenerOptions : EventListenerOptions
  ||| When set to true, passive indicates that the **callback** will not cancel
  ||| the event by invoked `preventDefault`. This is used to enable performace
  ||| optimizations described in
  ||| [§2.7 Observing event listeners](https://dom.spec.whatwg.org/#observing-event-listeners.
  ||| Default is false.
  passive : Bool
  ||| When set to true, once indicates that the **callback** will only be
  ||| invoked once after which the event listener will be removed.
  once    : Bool

addEL : (ref : JSRef) -> (type : String) -> (listener : EventListener) ->
      (options : EventListenerOptions) -> JS_IO ()
addEL ref type (New _ callback) options = ?rhs_2
  -- jscall "%0.addEventListener(%1, %2, %3)"
  -- (JSRef -> JSFn (JSRef -> JS_IO()) -> JS_IO ())

addEventListener : EventTarget -> (type : String) ->
                   (listener : EventListener) ->
                   (options : EventListenerOptions) -> JS_IO ()
addEventListener (FromXHR (FromXMLHttpRequest (NewXMLRequest ref))) = addEL ref
addEventListener (FromWindow (New _ ref))                           = addEL ref
addEventListener (FromNode   (FromDocument     (New _ ref)))        = addEL ref
addEventListener (FromNode   (FromDocumentType (New _ _ _ ref)))    = addEL ref
addEventListener (FromNode   (FromElement      (New _ ref)))        = addEL ref
addEventListener (FromNode (FromDocument (FromHTMLDocument _ (New ref)))) =
  addEL ref

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module Main

import GRIN.GrinCG
import Idris.Driver
import Compiler.Common

main : IO ()
main = mainWithCodegens [("grin", grin)]


text:
module Inigo.Package.PackageIndex

import Data.List
import Data.Maybe
import Extra.Either
import Extra.List
import Extra.String
import Inigo.Package.ParseHelpers
import Inigo.Package.Package
import SemVar
import Toml

||| Information about a package in the index
public export
record PackageMeta where
  constructor MkPackageMeta
  ns : String
  package : String
  description : Maybe String
  version : Version

public export
PackageIndex : Type
PackageIndex = List PackageMeta

public export
Show PackageMeta where
  show (MkPackageMeta ns package description version) =
    "MkPackageMeta{ns=" ++ ns ++ ",package=" ++ package ++ ",description=" ++ (show description) ++ ",version=" ++ show version ++ "}"

public export
Eq PackageMeta where
  (MkPackageMeta ns0 package0 description0 version0) == (MkPackageMeta ns1 package1 description1 version1) =
    ns0 == ns1 && package0 == package1 && description0 == description1 && version0 == version1

parsePackageMetaToml : Toml -> Either String PackageMeta
parsePackageMetaToml toml =
  do
    ns <- string ["ns"] toml
    package <- string ["package"] toml
    description <- maybe (string ["description"] toml)
    versionStr <- string ["version"] toml
    version <- expect ("Invalid version: " ++ versionStr) (parseVersion versionStr)
    pure $ MkPackageMeta ns package description version

parsePackageIndexToml : Toml -> Either String PackageIndex
parsePackageIndexToml toml =
  case get ["pkg"] toml of
    Just (ArrTab arr) =>
      map reverse (foldl parseIndex (Right []) arr)
    _ =>
      Left "invalid package index `pkg` key"
  where
    parseIndex : Either String PackageIndex -> Toml -> Either String PackageIndex
    parseIndex accE toml =
      do
        acc <- accE
        packageMeta <- parsePackageMetaToml toml
        pure $ (packageMeta :: acc)

export
parsePackageIndex : String -> Either String PackageIndex
parsePackageIndex pkgIndexToml =
  do
    toml <- expect "Failed to parse PackageIndex Toml" $ parseToml pkgIndexToml
    parsePackageIndexToml toml

export
toToml : PackageIndex -> Toml
toToml pkgIndex =
  [ (["pkg"], ArrTab $ map toTomlPkg pkgIndex) ]
  where
    toTomlPkg : PackageMeta -> Toml
    toTomlPkg pkgMeta =
      mapMaybe id
        [ Just (["ns"], Str (ns pkgMeta))
        , Just (["package"], Str (package pkgMeta))
        , map (\desc => (["description"], Str desc)) (description pkgMeta)
        , Just (["version"], Str (show . version $ pkgMeta))
        ]

export
searchPackageIndex : String -> PackageIndex -> PackageIndex
searchPackageIndex search index =
  filter (\x => searchMany (cleanup search) [package x, fromMaybe "" (description x)]) index
  where
    cleanup : String -> List Char
    cleanup =
      (map toLower) . unpack

    doSearch : String -> List Char -> Bool
    doSearch str lookup =
      findAll (cleanup str) lookup /= []

    searchMany : List Char -> List String -> Bool
    searchMany lookup [] = False
    searchMany lookup (x :: xs) = (doSearch x lookup) || (searchMany lookup xs)

||| Encode a package, for instance, after adding a new dep
export
encodePackageIndex : PackageIndex -> String
encodePackageIndex = encode . toToml

export
fromPackage : Package -> PackageMeta
fromPackage pkg =
  MkPackageMeta (ns pkg) (package pkg) (description pkg) (version pkg)

export
updatePackageMeta : PackageIndex -> Package -> PackageIndex
updatePackageMeta pkgIndex pkg =
  let
    meta = fromPackage pkg
    (found, res) = foldl (accumulate meta) (False, []) pkgIndex
  in
    if found then
      reverse res
    else
      reverse (meta :: res)
  where
    accumulate : PackageMeta -> (Bool, PackageIndex) -> PackageMeta -> (Bool, PackageIndex)
    accumulate meta (True, acc) el = (True, el :: acc)
    accumulate meta (False, acc) el =
      if ns el == ns pkg && package el == package pkg then
        (True, meta :: acc)
      else
        (False, el :: acc)

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module AddAllN

-- The idea from Thorsten Altenkirch's "Why Type Theory matters" at Lambda Days 2019 --

public export
NatFun : Nat -> Type
NatFun Z = Nat
NatFun (S n) = Nat -> NatFun n

liftUnary : (Nat -> Nat) -> {n : Nat} -> NatFun n -> NatFun n
liftUnary f {n=Z}   nf = f nf
liftUnary f {n=S k} nf = liftUnary f . nf

-- You can also lift binary and `const`

export
add : {n : Nat} -> NatFun n
add {n=Z}   = 0
add {n=S k} = \n => liftUnary (n+) add

x : Nat
x = add 2 3 4 5

x' : Nat
x' = add (the Nat 2) (the Nat 3) (the Nat 4) (the Nat 5)

y : Nat
y = add 1 2

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Web.Internal.FilePrim

import JS
import Web.Internal.Types

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

namespace Blob

  export
  %foreign "browser:lambda:(a,b)=> new Blob(a,b)"
  prim__new :  UndefOr (Array (Union13 Int8Array
                                       Int16Array
                                       Int32Array
                                       UInt8Array
                                       UInt8Array
                                       UInt8Array
                                       UInt8ClampedArray
                                       Float32Array
                                       Float64Array
                                       DataView
                                       ArrayBuffer
                                       Blob
                                       String))
            -> UndefOr BlobPropertyBag
            -> PrimIO Blob

  export
  %foreign "browser:lambda:x=>x.size"
  prim__size : Blob -> PrimIO JSBits64

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : Blob -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.arrayBuffer()"
  prim__arrayBuffer : Blob -> PrimIO (Promise ArrayBuffer)

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.slice(a,b,c)"
  prim__slice :  Blob
              -> UndefOr JSInt64
              -> UndefOr JSInt64
              -> UndefOr String
              -> PrimIO Blob

  export
  %foreign "browser:lambda:x=>x.stream()"
  prim__stream : Blob -> PrimIO ReadableStream

  export
  %foreign "browser:lambda:x=>x.text()"
  prim__text : Blob -> PrimIO (Promise String)

namespace File

  export
  %foreign "browser:lambda:(a,b,c)=> new File(a,b,c)"
  prim__new :  Array (Union13 Int8Array
                              Int16Array
                              Int32Array
                              UInt8Array
                              UInt8Array
                              UInt8Array
                              UInt8ClampedArray
                              Float32Array
                              Float64Array
                              DataView
                              ArrayBuffer
                              Blob
                              String)
            -> String
            -> UndefOr FilePropertyBag
            -> PrimIO File

  export
  %foreign "browser:lambda:x=>x.lastModified"
  prim__lastModified : File -> PrimIO JSInt64

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : File -> PrimIO String

namespace FileList

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : FileList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : FileList -> Bits32 -> PrimIO (Nullable File)

namespace FileReader

  export
  %foreign "browser:lambda:()=> new FileReader()"
  prim__new : PrimIO FileReader

  export
  %foreign "browser:lambda:x=>x.error"
  prim__error : FileReader -> PrimIO (Nullable DOMException)

  export
  %foreign "browser:lambda:x=>x.onabort"
  prim__onabort : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onabort = v}"
  prim__setOnabort : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onload"
  prim__onload : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onload = v}"
  prim__setOnload : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onloadend"
  prim__onloadend : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onloadend = v}"
  prim__setOnloadend : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onloadstart"
  prim__onloadstart : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onloadstart = v}"
  prim__setOnloadstart : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onprogress"
  prim__onprogress : FileReader -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onprogress = v}"
  prim__setOnprogress : FileReader -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readyState"
  prim__readyState : FileReader -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.result"
  prim__result : FileReader -> PrimIO (Nullable (Union2 String ArrayBuffer))

  export
  %foreign "browser:lambda:x=>x.abort()"
  prim__abort : FileReader -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.readAsArrayBuffer(a)"
  prim__readAsArrayBuffer : FileReader -> Blob -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.readAsBinaryString(a)"
  prim__readAsBinaryString : FileReader -> Blob -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.readAsDataURL(a)"
  prim__readAsDataURL : FileReader -> Blob -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.readAsText(a,b)"
  prim__readAsText : FileReader -> Blob -> UndefOr String -> PrimIO ()

namespace FileReaderSync

  export
  %foreign "browser:lambda:()=> new FileReaderSync()"
  prim__new : PrimIO FileReaderSync

  export
  %foreign "browser:lambda:(x,a)=>x.readAsArrayBuffer(a)"
  prim__readAsArrayBuffer : FileReaderSync -> Blob -> PrimIO ArrayBuffer

  export
  %foreign "browser:lambda:(x,a)=>x.readAsBinaryString(a)"
  prim__readAsBinaryString : FileReaderSync -> Blob -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.readAsDataURL(a)"
  prim__readAsDataURL : FileReaderSync -> Blob -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b)=>x.readAsText(a,b)"
  prim__readAsText : FileReaderSync -> Blob -> UndefOr String -> PrimIO String

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace BlobPropertyBag

  export
  %foreign "browser:lambda:(a,b)=> {type: a,endings: b}"
  prim__new : UndefOr String -> UndefOr String -> PrimIO BlobPropertyBag

  export
  %foreign "browser:lambda:x=>x.endings"
  prim__endings : BlobPropertyBag -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.endings = v}"
  prim__setEndings : BlobPropertyBag -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : BlobPropertyBag -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : BlobPropertyBag -> UndefOr String -> PrimIO ()

namespace FilePropertyBag

  export
  %foreign "browser:lambda:(a)=> {lastModified: a}"
  prim__new : UndefOr JSInt64 -> PrimIO FilePropertyBag

  export
  %foreign "browser:lambda:x=>x.lastModified"
  prim__lastModified : FilePropertyBag -> PrimIO (UndefOr JSInt64)

  export
  %foreign "browser:lambda:(x,v)=>{x.lastModified = v}"
  prim__setLastModified : FilePropertyBag -> UndefOr JSInt64 -> PrimIO ()


text:
module Control.Comonad.Store

import public Control.Comonad.Store.Store as Control.Comonad.Store
import public Control.Comonad.Store.Interface as Control.Comonad.Store


text:
module TicTacToe

import public TicTacToe.GameState
import public TicTacToe.Player
import public TicTacToe.Simple

max_stars_repo_name: ShinKage/DT-TicTacToe

max_issues_repo_name: ShinKage/DT-TicTacToe

max_forks_repo_name: ShinKage/DT-TicTacToe


text:
module Main

import Data.Vect

infixr 5 .+.

data Schema = SString | SInt | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore (size : Nat) where
  constructor MkData
  schema : Schema
  items : Vect size (SchemaType schema)

setSchema : DataStore 0 -> Schema -> DataStore 0
setSchema (MkData schema []) schema' = MkData schema' []

data Command : Schema -> Type where
     SetSchema : Schema -> Command schema
     Add : SchemaType schema -> Command schema
     Get : Integer -> Command schema
     Quit : Command schema


text:
repl' : (prompt : String) -> (onInput : String -> String) -> IO ()
repl' prompt onInput =
    do
        putStr prompt
        input <- getLine
        let output = onInput input
        putStrLn output
        repl' prompt onInput

replWith' : (state : a) -> (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> IO ()
replWith' state prompt onInput =
    do
        putStr prompt
        input <- getLine
        let next = onInput state input
        case next of
            Nothing => pure ()
            (Just (output, newState)) =>
                do
                    putStrLn output
                    replWith' newState prompt onInput