text:
module System.File.ReadWrite

import public Data.Fuel

import Data.List

import System.File.Handle
import public System.File.Error
import System.File.Support
import public System.File.Types
import System.FFI

%default total

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_seekLine"
         "node:support:seekLine,support_system_file"
         jvm' fileClass ".seekLine" fileClass "int"
prim__seekLine : FilePtr -> PrimIO Int

%foreign support "idris2_readLine"
         "node:support:readLine,support_system_file"
         jvm' fileClass "readLine" fileClass "String"
prim__readLine : FilePtr -> PrimIO (Ptr String)

%foreign support "idris2_readChars"
         jvm' fileClass "readChars" ("int " ++ fileClass) "String"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign "C:fgetc,libc 6"
         jvm' fileClass "readChar" fileClass "char"
prim__readChar : FilePtr -> PrimIO Int

%foreign support "idris2_writeLine"
         "node:lambda:(filePtr, line) => require('fs').writeSync(filePtr.fd, line, undefined, 'utf-8')"
         jvm' fileClass "writeLine" (fileClass ++ " String") "int"
prim__writeLine : FilePtr -> String -> PrimIO Int

%foreign support "idris2_eof"
         "node:lambda:x=>(x.eof?1:0)"
         jvm' fileClass "isEof" fileClass "int"
prim__eof : FilePtr -> PrimIO Int

%foreign support "idris2_removeFile"
         jvm' fileClass "delete" "String" "int"
prim__removeFile : String -> PrimIO Int

||| Seek through the next newline.
||| This is @fGetLine@ without the overhead of copying
||| any characters.
export
fSeekLine : HasIO io => (h : File) -> io (Either FileError ())
fSeekLine (FHandle f)
    = do res <- primIO (prim__seekLine f)
         if res /= 0
            then returnError
            else ok ()

export
fGetLine : HasIO io => (h : File) -> io (Either FileError String)
fGetLine (FHandle f)
    = do res <- primIO (prim__readLine f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String)
fGetChars (FHandle f) max
    = do res <- primIO (prim__readChars max f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChar : HasIO io => (h : File) -> io (Either FileError Char)
fGetChar h@(FHandle f)
    = do c <- primIO (prim__readChar f)
         ferr <- fileError h
         if ferr
            then returnError
            else ok (cast c)

export
fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStr (FHandle f) str
    = do res <- primIO (prim__writeLine f str)
         if res == 0
            then returnError
            else ok ()

export
fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStrLn f str = fPutStr f (str ++ "\n")

export
fEOF : HasIO io => (h : File) -> io Bool
fEOF (FHandle f)
    = do res <- primIO (prim__eof f)
         pure (res /= 0)

export
removeFile : HasIO io => String -> io (Either FileError ())
removeFile fname
    = do res <- primIO (prim__removeFile fname)
         if res == 0
            then ok ()
            else returnError

readLinesOnto : HasIO io => (acc : List String) ->
                            (offset : Nat) ->
                            (fuel : Fuel) ->
                            File ->
                            io (Either FileError (Bool, List String))
readLinesOnto acc _ Dry h = pure (Right (False, reverse acc))
readLinesOnto acc offset (More fuel) h
  = do False <- fEOF h
         | True => pure $ Right (True, reverse acc)
       case offset of
            (S offset') => (fSeekLine h *> readLinesOnto acc offset' (More fuel) h) @{Applicative.Compose}
            0           => (fGetLine h >>= \str => readLinesOnto (str :: acc) 0 fuel h) @{Monad.Compose}

||| Read a chunk of a file in a line-delimited fashion.
||| You can use this function to read an entire file
||| as with @readFile@ by reading until @forever@ or by
||| iterating through pages until hitting the end of
||| the file.
|||
||| The @limit@ function can provide you with enough
||| fuel to read exactly a given number of lines.
|||
||| On success, returns a tuple of whether the end of
||| the file was reached or not and the lines read in
||| from the file.
|||
||| Note that each line will still have a newline
||| character at the end.
|||
||| Important: because we are chunking by lines, this
||| function's totality depends on the assumption that
||| no single line in the input file is infinite.
export
readFilePage : HasIO io => (offset : Nat) -> (until : Fuel) -> String -> io (Either FileError (Bool, List String))
readFilePage offset fuel file
  = withFile file Read pure $
      readLinesOnto [] offset fuel

export
partial
readFile : HasIO io => String -> io (Either FileError String)
readFile = (map $ map (fastConcat . snd)) . readFilePage 0 forever

||| Write a string to a file
export
writeFile : HasIO io =>
            (filepath : String) -> (contents : String) ->
            io (Either FileError ())
writeFile file contents
  = withFile file WriteTruncate pure $
      (flip fPutStr contents)


text:
top_ten : Ord a => List a -> List a
top_ten [] = []
top_ten xs =
  let sortedList = reverse (sort xs) in
  take 10 sortedList

ext: idr

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
||| Logging utilities for the LSP server implementation.
|||
||| (C) The Idris Community, 2021
module Server.Log

import Core.Core
import Core.Directory
import Server.Configuration
import Server.Utils
import System.Directory
import System.File
import System.Path

%default total

-- TODO: Very crude logging, we should probably adopt a more flexible logging mechanism.
--       Maybe comonads, à la Haskell co-log package?

||| Type for the severity of logging messages.
public export
data Severity = Debug | Info | Warning | Error | Critical

Cast Severity Integer where
  cast Debug    = 0
  cast Info     = 1
  cast Warning  = 2
  cast Error    = 3
  cast Critical = 4

export
Eq Severity where
  Debug    == Debug    = True
  Info     == Info     = True
  Warning  == Warning  = True
  Error    == Error    = True
  Critical == Critical = True
  _ == _ = False

export
Show Severity where
  show Debug    = "DEBUG"
  show Info     = "INFO"
  show Warning  = "WARNING"
  show Error    = "ERROR"
  show Critical = "CRITICAL"

export
Ord Severity where
  compare x y = compare (cast {to = Integer} x) (cast y)

||| Logs a string with the provided severity level.
export
logString : Ref LSPConf LSPConfiguration => Severity -> String -> Core ()
logString severity msg = do
  logHandle <- gets LSPConf logHandle
  ignore $ coreLift $ fPutStrLn logHandle ("LOG " ++ show severity ++ ": " ++ msg)
  coreLift $ fflush logHandle

||| Logs a showable value with the provided severity level.
export
logShow : Ref LSPConf LSPConfiguration => Show a => Severity -> a -> Core ()
logShow severity = logString severity . show

||| Changes the log file location, if possible.
export covering
changeLogFile : Ref LSPConf LSPConfiguration => String -> Core ()
changeLogFile fname = do
  let True = isAbsolute fname
    | False => logString Error "Unable to change log file location: \{fname} is not an absolute path"
  case parent fname of
       Just dir => do Right _ <- coreLift $ mkdirAll dir
                        | Left err => logString Error "Unable to create directory \{dir}: \{show err}"
                      logString Debug "Created new log directory \{dir}"
       Nothing => pure ()
  Right handle <- coreLift $ openFile fname Append
    | Left err => logString Error "Unable to updated log file location \{fname}: \{show err}"
  modify LSPConf (record { logHandle = handle })
  logString Debug "Log file location updated to \{fname}"


text:
import CommonTestingStuff
import Program

export
main : HasIO io => io ()
main = do
  putStrLn beforeString
  traverse_ putStrLn $ execW program
  putStrLn "after coop"


text:
module Parse

import DataTypes
import ParseNumber
import ParserCombinator
import Util

%access public export

symbol : Parser Char
symbol = oneOf "!#$%&|*+-/:<=>?@^_~"

matchBracket : Char -> Parser Char
matchBracket open =
    case open of
        '(' => char ')'
        '[' => char ']'
        '{' => char '}'

bracketed : Parser a -> Parser a
bracketed p = do
    open <- char '(' <|> char '[' <|> char '{'
    v <- p
    matchBracket open
    pure v

--------------
-- String
--------------
parseString : Parser LispVal
parseString =
    do char '"'
       x <- many' (escapedChar <|> noneOf "\"\\")
       char '"'
       pure $ LispString (pack x)
    where
        escapedChar : Parser Char
        escapedChar =
            do char '\\'
               x <- oneOf "\\\"nrt"
               pure $ case x of
                    '\\' => x
                    '"' => x
                    'n' => '\n'
                    'r' => '\r'
                    't' => '\t'

--------------
-- Atom
--------------
parseAtom : Parser LispVal
parseAtom = do
  first <- letter <|> symbol
  rest <- many' (letter <|> digit <|> symbol)
  let atom = pack (first :: rest)
  pure $
    case atom of
      "#t" => LispBool True
      "#f" => LispBool False
      _ => LispAtom atom

--------------
-- Char
--------------
parseCharacter : Parser LispVal
parseCharacter = do
    -- TODO: Meta-, bucky-bit stuff
    string "#\\"
    c <- many1 letter
    let s = pack (map Prelude.Chars.toLower c)
    pure $
        if length s == 1 then LispCharacter $ strHead s else
        case s of
            "newline" => LispCharacter '\n'
            "space" => LispCharacter ' '
            "altmode" => LispCharacter $ chr 27
            "backnext" => LispCharacter $ chr 31
            "backspace" => LispCharacter $ chr 8
            "call" => LispCharacter $ chr 26
            "linefeed" => LispCharacter $ chr 10
            "page" => LispCharacter $ chr 12
            "return" => LispCharacter $ chr 13
            "rubout" => LispCharacter $ chr 127
            "tab" => LispCharacter $ chr 9

--------------
-- Comment
--------------
parseLineComment : Parser LispVal
parseLineComment =
    do char ';'
       skipUntil (char '\n') item
       pure LispVoid -- TODO: This seems wrong

parseBlockComment : Parser LispVal
parseBlockComment =
    do string "#|"
       skipUntil (string "|#") (parseBlockComment <|> takeAnything)
       pure LispVoid
  where
      takeAnything : Parser LispVal
      takeAnything =
        do item
           pure LispVoid

parseComment : Parser LispVal
parseComment = parseLineComment <|> parseBlockComment -- TODO: Fix

mutual
    --------------
    -- Vector
    --------------
    parseVector : Parser LispVal
    parseVector =
        do char '#'
           rawList <- bracketed parseRawList
           let len = toIntNat $ length rawList
           pure $ LispVector len rawList

    --------------
    -- Quoted
    --------------
    parseQuoted : Parser LispVal
    parseQuoted =
        do char '\''
           x <- parseExpr
           pure $ LispList [LispAtom "quote", x]

    --------------
    -- Backquote
    --------------
    parseQuasiQuote : Parser LispVal
    parseQuasiQuote =
        do char '`'
           x <- parseExpr
           pure $ LispList [LispAtom "quasiquote", x]

    parseUnquote : Parser LispVal
    parseUnquote =
        do try (char ',')
           x <- parseExpr
           pure $ LispList [LispAtom "unquote", x]

    parseUnquoteSplicing : Parser LispVal
    parseUnquoteSplicing =
        do try (string ",@")
           x <- parseExpr
           pure $ LispList [LispAtom "unquote-splicing", x]

    --------------
    -- Lists
    --------------
    parseRawList : Parser (List LispVal)
    parseRawList =
        do skipMany spaces
           list <- sepBy parseExpr spaces
           skipMany spaces
           pure list

    parseList : Parser LispVal
    parseList = do
        rawList <- parseRawList
        pure $ LispList rawList

    parseLists : Parser LispVal
    parseLists = bracketed (parseTwoDot <|> parseDottedList <|> parseList)

    parseTwoDot : Parser LispVal
    parseTwoDot = do
        skipMany spaces
        h <- endBy parseExpr spaces
        char '.'
        spaces
        m <- parseExpr
        spaces
        char '.'
        spaces
        t <- sepBy parseExpr spaces
        skipMany spaces
        case (h, m, t) of
            ([], _, _) => failure $ "Illegal use of `.`"
            (_, _, []) => failure $ "Illegal use of `.`"
            (xs, _, ys) => pure $ LispList (m :: h ++ t)
            _ => failure $ "Illegal use of `.`"

    parseDottedList : Parser LispVal
    parseDottedList = do
        skipMany spaces
        h <- endBy parseExpr spaces
        char '.'
        spaces
        t <- parseExpr
        skipMany spaces
        case t of
            LispDottedList xs x => pure $ LispDottedList (h ++ xs) x
            LispList xs => pure $ LispList (h ++ xs)
            _ => pure $ LispDottedList h t

    parseExpr : Parser LispVal
    parseExpr =
        parseVector <|> parseComment <|> parseNumber <|> parseCharacter <|> parseAtom <|>
        parseString <|> parseQuoted <|> parseLists

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
-- ------------------------------------------------------------ [ Messages.idr ]
-- Module      : Messages
-- Description : Types for Crypto Messages
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Message

||| Representation if Messages
data Message : Nat -> Type where
  MkMsgData : Vect n Bits32 -> Message n

||| Representation of a ciphertext.
data Encrypted : Nat -> Type where
  MkEncData : Vect n Bits32 -> Encrypted n

||| Representation of a digital signature.
data Signed : Nat -> Type where
  MkSigData : Vect n Bits32 -> Signed n

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

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Mem

import Data.Vect

-- Effectively (size : Nat ** Vect size a)
record Region a where
  constructor MkRegion
  regionSize : Nat
  regionData : Vect regionSize a

-- Effectively (regs : Nat ** Vect regs (Region a))
record RegionsOfType a where
  constructor MkRegOfType
  regionCnt : Nat
  regionsOfType : Vect regs $ Region a

record Memory where
  constructor MkMemReg
  regionsByType : (a : Type) -> RegionsOfType a

record Pointer where
  constructor MkPointer
  type : Type
  regionNum : Nat
  idxInRegion : Nat

data CorrectPointer : Pointer -> Memory -> Type where

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Learn.Elab

import Language.Reflection.Utils

mkId : Elab ()
mkId = do x <- gensym "x"
          attack
          intro x
          fill (Var x)
          solve
          solve

%language ElabReflection

idNat : Nat -> Nat
idNat = %runElab mkId

idNat2 : Nat -> Nat
idNat2 = %runElab (do intro `{{x}}
                      fill (Var `{{x}})
                      solve)

idNat3 : Nat -> Nat
idNat3 = ?myhole

--total
quicksort : List Nat -> List Nat
quicksort [] = []
quicksort (x::xs) =
  quicksort (filter (< x) xs) ++ x :: quicksort (filter (>= x) xs)

---------- Proofs ----------

Learn.Elab.myhole = %runElab (do x <- gensym "x"
                                 attack
                                 intro x
                                 fill (Var x)
                                 solve
                                 solve)

data QSAcc : List Nat -> Type where
  QSAccCase0 : QSAcc []
  QSAccCase1 : QSAcc (filter (< x) xs) ->
               QSAcc (filter (>= x) xs) ->
               QSAcc (x :: xs)

qs' : (xs : List Nat) -> QSAcc xs -> List Nat
qs' [] QSAccCase0 = []
qs' (x :: xs) (QSAccCase1 l r) =
  qs' (filter (< x) xs) l ++
  x :: qs' (filter (>= x) xs) r

{- bc : (inFun, outFun, accPred : TTName) -> Elab ()
bc inFun outFun accPred = do
  (inFun', Ref, inTy) <- lookupTyExact inFun
     | _ => fail [TextPart "Not a function"]
  (_, args, res) <- lookupArgsExact inFun'
  declareDatatype $ Declare accPred args `(Type)
  let accArg = MkFunArg `{{acc}}
                (mkApp (Var accPred)
                   (map (Var . name) args))
                Explicit
                NotErased
  declareType $
    Declare outFun (args ++ [accArg]) res
  DefineFun _ oldClauses <- lookupFunDefnExact inFun'
  (newClauses, ctors) <-
    unzip <$> ?processClauses Z oldClauses
  defineDatatype $ DefineDatatype accPred ctors
  defineFunction $ DefineFun outFun newClauses

--%runElab (bc `{quicksort} `{{qs'}} `{{QSAcc}})
-}

-- foo : Nat -> Nat
-- foo k = ?foo_rhs

-- getAllNames : TT -> List TTName
-- getAllNames (P Bound (UN x) tm) = ?getAllNames_rhs_1
-- getAllNames (P Bound (NS n xs) tm) = ?getAllNames_rhs_13
-- getAllNames (P Bound (MN x y) tm) = ?getAllNames_rhs_14
-- getAllNames (P Bound (SN sn) tm) = ?getAllNames_rhs_15
-- getAllNames (P Ref n tm) = ?getAllNames_rhs_10
-- getAllNames (P (DCon x y) n tm) = ?getAllNames_rhs_11
-- getAllNames (P (TCon x y) n tm) = ?getAllNames_rhs_12
-- getAllNames (V x) = ?getAllNames_rhs_2
-- getAllNames (Bind n b tm) = ?getAllNames_rhs_3
-- getAllNames (App tm tm') = ?getAllNames_rhs_4
-- getAllNames (TConst c) = ?getAllNames_rhs_5
-- getAllNames Erased = ?getAllNames_rhs_6
-- getAllNames (TType uexp) = ?getAllNames_rhs_7
-- getAllNames (UType x) = ?getAllNames_rhs_8

data Foo = Fee | Food


text:
module Extra.Prelude

||| Zip, but it works on Streams
export
zip : Stream a -> List b -> List (a, b)
zip _ [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys


text:
> module Decidable.Properties

> import Decidable.Predicates

> %default total

> %access public export

> ||| If |P| is decidable, |Not P| is decidable
> decNot : {P : Type} -> Dec P -> Dec (Not P)
> decNot {P} (Yes prf) = No contra where
>   contra : Not P -> Void
>   contra np = np prf
> decNot {P} (No contra) = Yes contra
> %freeze decNot -- frozen

> ||| If |P| and |Q| are decidable, |(P , Q)| is decidable
> decPair : {P, Q : Type} -> Dec P -> Dec Q -> Dec (P , Q)
> decPair (Yes p) (Yes q) = Yes (p , q)
> decPair (Yes p) (No nq) = No (\ pq => nq (snd pq))
> decPair (No np) (Yes q) = No (\ pq => np (fst pq))
> decPair (No np) (No nq) = No (\ pq => np (fst pq))
> %freeze decPair -- frozen

> ||| If |P| and |Q| are decidable, |Either P Q| is decidable
> decEither : {P, Q : Type} -> Dec P -> Dec Q -> Dec (Either P Q)
> decEither (Yes p) _       = Yes (Left p)
> decEither (No np) (Yes q) = Yes (Right q)
> decEither {P} {Q} (No np) (No nq) = No contra where
>   contra : Either P Q -> Void
>   contra (Left  p) = np p
>   contra (Right q) = nq q
> %freeze decEither -- frozen

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
isSorted : Ord a => List a -> Bool
isSorted []  = True
isSorted [x] = True
isSorted (x :: t @ (y :: ys)) = x <= y && isSorted t

minElem : Ord a => (l : List a) -> { auto p : isSorted l = True } -> Maybe a
minElem l = head' l

prove : Ord a => (l : List a) -> Maybe (isSorted l = True)
prove []  = Just $ Refl
prove [x] = Just $ Refl
prove (x :: y :: ys) with (x <= y)
  | True  = prove (y :: ys)
  | False = Nothing

main : IO ()
main = do
  line <- getLine
  let list = map (cast { to = Integer }) $ words line
  case prove list of
       Just _  => printLn $ minElem list
       Nothing => printLn "input list is not sorted"

max_stars_repo_name: fthomas/tdd-talk

max_issues_repo_name: fthomas/tdd-talk

max_forks_repo_name: fthomas/tdd-talk


text:
module Language.LSP.BrowseNamespace

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Name
import Data.List
import Idris.Doc.String
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.LSP.Definition
import Language.LSP.Message
import Libraries.Data.NameMap
import Parser.Source
import Parser.Rule.Source
import Server.Configuration
import Server.Log
import Server.Utils

visible : Defs -> Name -> Core Bool
visible defs n = do
  Just def <- lookupCtxtExact n (gamma defs)
    | Nothing => pure False
  pure $ visibility def /= Private

inNS : Namespace -> Name -> Bool
inNS ns (NS xns (UN _)) = ns `isParentOf` xns
inNS _ _ = False

getNames : Ref ROpts REPLOpts
        => Ref Ctxt Defs
        => Ref Syn SyntaxInfo
        => Namespace -> Core (List Name)
getNames ns = do
  defs <- get Ctxt
  names <- allNames defs.gamma
  let allNames = filter (inNS ns) names
  allNames <- filterM (visible defs) allNames
  pure $ sort allNames

buildDocumentSymbol : Ref Ctxt Defs
                   => Ref LSPConf LSPConfiguration
                   => Ref Syn SyntaxInfo
                   => Name -> Core (Maybe SymbolInformation)
buildDocumentSymbol n = do
  defs <- get Ctxt
  Just def <- lookupCtxtExact n defs.gamma
    | _ => pure Nothing
  Just loc <- mkLocation def.location
    | _ => pure Nothing
  let isDeprecated = Deprecate `elem` def.flags
  let kind = case def.definition of
                  (PMDef {}) => Function
                  (ExternDef {}) => Function
                  (ForeignDef {}) => Function
                  (Builtin {}) => Function
                  (DCon {}) => EnumMember
                  (TCon {}) => Constructor
                  (Hole {}) => Variable
                  _ => Null
  ty <- resugar [] =<< normaliseHoles defs [] def.type
  pure $ Just $ MkSymbolInformation
    { name = "\{show $ dropNS n} : \{show ty}"
    , kind = kind
    , tags = if isDeprecated then Just [Deprecated] else Nothing
    , deprecated = Nothing
    , location = loc
    , containerName = Nothing
    }

||| Returns the list of functions visible in the given namespace.
||| The response in the same format as a textDocument/documentSymbol request.
export
browseNamespaceCmd : Ref Ctxt Defs
                  => Ref Syn SyntaxInfo
                  => Ref ROpts REPLOpts
                  => Ref LSPConf LSPConfiguration
                  => String -> Core (List SymbolInformation)
browseNamespaceCmd str = do
  let Right (_, _, ns) = runParser (Virtual Interactive) Nothing str namespaceId
    | _ => pure []
  logI Browse "Browsing namespace \{show ns}"
  names <- getNames ns
  logI Browse "Names in \{show ns} fetched, found \{show $ length names}"
  catMaybes <$> traverse buildDocumentSymbol names


text:
module FTCQueue

-- Based on http://okmij.org/ftp/Haskell/AlgorithmsH1.html#FTCQueue
%access public export

data FTCQueue : (r : Type -> Type -> Type) -> Type -> Type -> Type where
  Leaf : r a b -> FTCQueue r a b
  Node : FTCQueue r a x -> FTCQueue r x b -> FTCQueue r a b

tsingleton : r a b -> FTCQueue r a b
tsingleton r = Leaf r

infixl 9 |>
(|>) : FTCQueue r a x -> r x b -> FTCQueue r a b
t |> r = Node t (Leaf r)

infixl 9 ><
(><) : FTCQueue r a x -> FTCQueue r x b -> FTCQueue r a b
t1 >< t2 = Node t1 t2

infixl 9 :|
data ViewL : (r : Type -> Type -> Type) -> Type -> Type -> Type where
  TOne  : r a b -> ViewL r a b
  (:|)  : r a x -> FTCQueue r x b -> ViewL r a b

tviewl : FTCQueue r a b -> ViewL r a b
tviewl (Leaf r) = TOne r
tviewl (Node t1 t2) = go t1 t2
 where
   go : FTCQueue r a x -> FTCQueue r x b -> ViewL r a b
   go (Leaf r) tr = r :| tr
   go (Node tl1 tl2) tr = go tl1 (Node tl2 tr)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Backprop.Node

import Backprop.CanBack
import Backprop.MathUtils
import Control.Optics
import Data.Floating
import public Data.List.Quantifiers

%hide Data.Morphisms.Op

public export
Op : (args : List Type) -> (o : Type) -> Type
Op args o = HList args -> Pair o (o -> HList args)

export
data Node : (i : Type) -> (o : Type) -> Type where
  ||| the input itself
  Input : Node a a
  ||| an operation
  Oper : {args : _} -> All CanBack args => Op args o -> All (Node i) args -> Node i o

public export
interface Functor f => NodeDistributive f where
  collect : {o : _} -> CanBack o => f (Node i o) -> Node i (f o)

public export
interface Functor f => NodeTraversable f where
  sequence : {o : _} -> CanBack o => Node i (f o) -> f (Node i o)

public export
NodeFunctor : (Type -> Type) -> Type
NodeFunctor f = (NodeTraversable f, NodeDistributive f)

export
map : {a, b : _} -> (CanBack a, CanBack b, NodeFunctor f) => (Node i a -> Node i b) -> Node i (f a) -> Node i (f b)
map f = collect . map f . sequence

export
input : Node a a
input = Input

export
op1 : {a1 : _} -> CanBack a1 => Op [a1] o -> Node i a1 -> Node i o
op1 op x = Oper op [x]

export
op2 : {a1, a2 : _} -> CanBack a1 => CanBack a2 => Op [a1, a2] o -> Node i a1 -> Node i a2 -> Node i o
op2 op x y = Oper op [x, y]

||| lift a constant into a `Node`
export
const : a -> Node i a
const x = Oper (\[] => (x, const [])) []

export
FromDouble a => FromDouble (Node i a) where
  fromDouble = const . fromDouble

export
{a : _} -> (CanBack a, Num a) => Num (Node i a) where
  (+) = op2 $ \[x, y] => (x + y, \d => [d, d])
  (*) = op2 $ \[x, y] => (x * y, \d => [d * y, x * d])
  fromInteger = const . fromInteger

export
{a : _} -> (CanBack a, Neg a) => Neg (Node i a) where
  (-) = op2 $ \[x, y] => (x - y, \d => [d, -d])
  negate = op1 $ \[x] => (-x, \d => [-d])

export
{a : _} -> (CanBack a, Ord a, Neg a, Abs a) => Abs (Node i a) where
  abs = op1 $ \[x] => (abs x, \d => [d * signum_zero x])

export
{a : _} -> (CanBack a, Neg a, Fractional a) => Fractional (Node i a) where
  (/) = op2 $ \[x, y] => (x / y, \d => [d / y, -d * x / (y * y)])
  recip = op1 $ \[x] => (recip x, \d => [-d / (x * x)])

export
{a : _} -> (CanBack a, Neg a, Floating a, Fractional (Node i a)) => Floating (Node i a) where
  pi = const pi
  sqrt = op1 $ \[x] => (sqrt x, \d => [d / (2 * sqrt x)])
  exp = op1 $ \[x] => (exp x, \d => [d * exp x])
  ln = op1 $ \[x] => (ln x, \d => [d / x])
  log base x = ln x / ln base
  pow = op2 $ \[x, y] =>
    ( pow x y
    , \d => let k = d * pow x (y - 1) in [k * y, k * x * ln x]
    )
  sin = op1 $ \[x] => (sin x, \d => [d * cos x])
  cos = op1 $ \[x] => (cos x, \d => [d * -sin x])
  tan = op1 $ \[x] => (tan x, \d => let cos' = cos x in [d / (cos' * cos')])
  asin = op1 $ \[x] => (asin x, \d => [d / sqrt (1 - x * x)])
  acos = op1 $ \[x] => (acos x, \d => [-d / sqrt (1 - x * x)])
  atan = op1 $ \[x] => (atan x, \d => [d / (1 - x * x)])
  sinh = op1 $ \[x] => (sinh x, \d => [d * cosh x])
  cosh = op1 $ \[x] => (cosh x, \d => [d * sinh x])
  tanh = op1 $ \[x] => (tanh x, \d => let cosh' = cosh x in [d / (cosh' * cosh')])

mutual
  run_all : {as : _} -> {auto prf : All CanBack as} -> CanBack i => All (Node i) as -> i -> (HList as, All (\b => b -> i -> i) as)
  run_all [] input = ([], [])
  run_all {prf = prf :: prfs} (arg :: args) input =
    let (x, y) = run arg input in bimap (x ::) (y ::) (run_all {prf = prfs} args input)

  combine_all : (backs : All (\b => b -> i -> i) as) -> HList as -> i -> i
  combine_all [] [] = id
  combine_all (back :: backs) (x :: xs) = combine_all backs xs . back x

  export
  run : {o : _} -> {auto prf : CanBack i} -> CanBack o => Node i o -> i -> (o, o -> i -> i)
  run Input input = (input, \d => add @{prf} d)
  run (Oper op arg_nodes) input =
    let
      (args, backs) = run_all arg_nodes input
      (output, back) = op args
    in
      (output, combine_all backs . back)

||| output: (the value, the gradient of inputs)
export
backprop : {o : _} -> (CanBack i, CanBack o) => Node i o -> i -> (o, i)
backprop node input = let (y, back) = run node input in (y, back one zero)

||| `backprop` but discards output value
export
grad : {o : _} -> (CanBack i, CanBack o) => Node i o -> i -> i
grad node input = snd $ backprop node input

mutual
  eval_all : All (Node i) as -> i -> HList as
  eval_all [] input = []
  eval_all (x :: xs) input = eval x input :: eval_all xs input

  ||| evaluates a `Node`, more efficient than `run` as gradient calculations are skipped
  |||
  ||| input: inputs, output node
  ||| output: output value
  export
  eval : Node i o -> i -> o
  eval Input input = input
  eval (Oper op args) input = fst $ op (eval_all args input)


text:
module Compiler.Scheme.Common

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline

import Core.Context
import Core.Name
import Core.TT

import Data.Bool.Extra
import Data.List
import Data.Vect

import System.Info

%default covering

export
firstExists : List String -> IO (Maybe String)
firstExists [] = pure Nothing
firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs

schString : String -> String
schString s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar c = if isAlphaNum c || c =='_'
                  then cast c
                  else "C-" ++ show (cast {to=Int} c)

export
schName : Name -> String
schName (NS ns n) = showNSWithSep "-" ns ++ "-" ++ schName n
schName (UN n) = schString n
schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n
schName (DN _ n) = schName n
schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
schName (Resolved i) = "fn--" ++ show i

export
schConstructor : (String -> String) -> Name -> Maybe Int -> List String -> String
schConstructor _ _ (Just t) args
    = "(vector " ++ show t ++ " " ++ showSep " " args ++ ")"
schConstructor schString n Nothing args
    = "(vector " ++ schString (show n) ++ " " ++ showSep " " args ++ ")"

||| Generate scheme for a plain function.
op : String -> List String -> String
op o args = "(" ++ o ++ " " ++ showSep " " args ++ ")"

||| Generate scheme for a boolean operation.
boolop : String -> List String -> String
boolop o args = "(or (and " ++ op o args ++ " 1) 0)"

||| Generate scheme for a primitive function.
schOp : PrimFn arity -> Vect arity String -> String
schOp (Add IntType) [x, y] = op "b+" [x, y, "63"]
schOp (Sub IntType) [x, y] = op "b-" [x, y, "63"]
schOp (Mul IntType) [x, y] = op "b*" [x, y, "63"]
schOp (Div IntType) [x, y] = op "b/" [x, y, "63"]
schOp (Add Bits8Type) [x, y] = op "b+" [x, y, "8"]
schOp (Sub Bits8Type) [x, y] = op "b-" [x, y, "8"]
schOp (Mul Bits8Type) [x, y] = op "b*" [x, y, "8"]
schOp (Div Bits8Type) [x, y] = op "b/" [x, y, "8"]
schOp (Add Bits16Type) [x, y] = op "b+" [x, y, "16"]
schOp (Sub Bits16Type) [x, y] = op "b-" [x, y, "16"]
schOp (Mul Bits16Type) [x, y] = op "b*" [x, y, "16"]
schOp (Div Bits16Type) [x, y] = op "b/" [x, y, "16"]
schOp (Add Bits32Type) [x, y] = op "b+" [x, y, "32"]
schOp (Sub Bits32Type) [x, y] = op "b-" [x, y, "32"]
schOp (Mul Bits32Type) [x, y] = op "b*" [x, y, "32"]
schOp (Div Bits32Type) [x, y] = op "b/" [x, y, "32"]
schOp (Add Bits64Type) [x, y] = op "b+" [x, y, "64"]
schOp (Sub Bits64Type) [x, y] = op "b-" [x, y, "64"]
schOp (Mul Bits64Type) [x, y] = op "b*" [x, y, "64"]
schOp (Div Bits64Type) [x, y] = op "b/" [x, y, "64"]
schOp (Add ty) [x, y] = op "+" [x, y]
schOp (Sub ty) [x, y] = op "-" [x, y]
schOp (Mul ty) [x, y] = op "*" [x, y]
schOp (Div IntegerType) [x, y] = op "quotient" [x, y]
schOp (Div ty) [x, y] = op "/" [x, y]
schOp (Mod ty) [x, y] = op "remainder" [x, y]
schOp (Neg ty) [x] = op "-" [x]
schOp (ShiftL IntType) [x, y] = op "blodwen-bits-shl" [x, y, "63"]
schOp (ShiftL Bits8Type) [x, y] = op "blodwen-bits-shl" [x, y, "8"]
schOp (ShiftL Bits16Type) [x, y] = op "blodwen-bits-shl" [x, y, "16"]
schOp (ShiftL Bits32Type) [x, y] = op "blodwen-bits-shl" [x, y, "32"]
schOp (ShiftL Bits64Type) [x, y] = op "blodwen-bits-shl" [x, y, "64"]
schOp (ShiftL ty) [x, y] = op "blodwen-shl" [x, y]
schOp (ShiftR ty) [x, y] = op "blodwen-shr" [x, y]
schOp (BAnd ty) [x, y] = op "blodwen-and" [x, y]
schOp (BOr ty) [x, y] = op "blodwen-or" [x, y]
schOp (BXOr ty) [x, y] = op "blodwen-xor" [x, y]
schOp (LT CharType) [x, y] = boolop "char<?" [x, y]
schOp (LTE CharType) [x, y] = boolop "char<=?" [x, y]
schOp (EQ CharType) [x, y] = boolop "char=?" [x, y]
schOp (GTE CharType) [x, y] = boolop "char>=?" [x, y]
schOp (GT CharType) [x, y] = boolop "char>?" [x, y]
schOp (LT StringType) [x, y] = boolop "string<?" [x, y]
schOp (LTE StringType) [x, y] = boolop "string<=?" [x, y]
schOp (EQ StringType) [x, y] = boolop "string=?" [x, y]
schOp (GTE StringType) [x, y] = boolop "string>=?" [x, y]
schOp (GT StringType) [x, y] = boolop "string>?" [x, y]
schOp (LT ty) [x, y] = boolop "<" [x, y]
schOp (LTE ty) [x, y] = boolop "<=" [x, y]
schOp (EQ ty) [x, y] = boolop "=" [x, y]
schOp (GTE ty) [x, y] = boolop ">=" [x, y]
schOp (GT ty) [x, y] = boolop ">" [x, y]
schOp StrLength [x] = op "string-length" [x]
schOp StrHead [x] = op "string-ref" [x, "0"]
schOp StrTail [x] = op "substring" [x, "1", op "string-length" [x]]
schOp StrIndex [x, i] = op "string-ref" [x, i]
schOp StrCons [x, y] = op "string-cons" [x, y]
schOp StrAppend [x, y] = op "string-append" [x, y]
schOp StrReverse [x] = op "string-reverse" [x]
schOp StrSubstr [x, y, z] = op "string-substr" [x, y, z]

-- `e` is Euler's number, which approximates to: 2.718281828459045
schOp DoubleExp [x] = op "exp" [x] -- Base is `e`. Same as: `pow(e, x)`
schOp DoubleLog [x] = op "log" [x] -- Base is `e`.
schOp DoubleSin [x] = op "sin" [x]
schOp DoubleCos [x] = op "cos" [x]
schOp DoubleTan [x] = op "tan" [x]
schOp DoubleASin [x] = op "asin" [x]
schOp DoubleACos [x] = op "acos" [x]
schOp DoubleATan [x] = op "atan" [x]
schOp DoubleSqrt [x] = op "sqrt" [x]
schOp DoubleFloor [x] = op "floor" [x]
schOp DoubleCeiling [x] = op "ceiling" [x]

schOp (Cast IntType StringType) [x] = op "number->string" [x]
schOp (Cast IntegerType StringType) [x] = op "number->string" [x]
schOp (Cast Bits8Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits16Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits32Type StringType) [x] = op "number->string" [x]
schOp (Cast Bits64Type StringType) [x] = op "number->string" [x]
schOp (Cast DoubleType StringType) [x] = op "number->string" [x]
schOp (Cast CharType StringType) [x] = op "string" [x]

schOp (Cast IntType IntegerType) [x] = x
schOp (Cast Bits8Type IntegerType) [x] = x
schOp (Cast Bits16Type IntegerType) [x] = x
schOp (Cast Bits32Type IntegerType) [x] = x
schOp (Cast Bits64Type IntegerType) [x] = x
schOp (Cast DoubleType IntegerType) [x] = op "exact-floor" [x]
schOp (Cast CharType IntegerType) [x] = op "char->integer" [x]
schOp (Cast StringType IntegerType) [x] = op "cast-string-int" [x]

schOp (Cast IntegerType IntType) [x] = x
schOp (Cast Bits8Type IntType) [x] = x
schOp (Cast Bits16Type IntType) [x] = x
schOp (Cast Bits32Type IntType) [x] = x
schOp (Cast DoubleType IntType) [x] = op "exact-floor" [x]
schOp (Cast StringType IntType) [x] = op "cast-string-int" [x]
schOp (Cast CharType IntType) [x] = op "char->integer" [x]

schOp (Cast IntType Bits8Type) [x] = op "integer->bits8" [x]
schOp (Cast IntType Bits16Type) [x] = op "integer->bits16" [x]
schOp (Cast IntType Bits32Type) [x] = op "integer->bits32" [x]
schOp (Cast IntType Bits64Type) [x] = op "integer->bits64" [x]

schOp (Cast IntegerType Bits8Type) [x] = op "integer->bits8" [x]
schOp (Cast IntegerType Bits16Type) [x] = op "integer->bits16" [x]
schOp (Cast IntegerType Bits32Type) [x] = op "integer->bits32" [x]
schOp (Cast IntegerType Bits64Type) [x] = op "integer->bits64" [x]

schOp (Cast Bits8Type Bits16Type) [x] = x
schOp (Cast Bits8Type Bits32Type) [x] = x
schOp (Cast Bits8Type Bits64Type) [x] = x

schOp (Cast Bits16Type Bits8Type) [x] = op "bits16->bits8" [x]
schOp (Cast Bits16Type Bits32Type) [x] = x
schOp (Cast Bits16Type Bits64Type) [x] = x

schOp (Cast Bits32Type Bits8Type) [x] = op "bits32->bits8" [x]
schOp (Cast Bits32Type Bits16Type) [x] = op "bits32->bits16" [x]
schOp (Cast Bits32Type Bits64Type) [x] = x

schOp (Cast Bits64Type Bits8Type) [x] = op "bits64->bits8" [x]
schOp (Cast Bits64Type Bits16Type) [x] = op "bits64->bits16" [x]
schOp (Cast Bits64Type Bits32Type) [x] = op "bits64->bits32" [x]

schOp (Cast IntegerType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast IntType DoubleType) [x] = op "exact->inexact" [x]
schOp (Cast StringType DoubleType) [x] = op "cast-string-double" [x]

schOp (Cast IntType CharType) [x] = op "cast-int-char" [x]

schOp (Cast from to) [x] = "(blodwen-error-quit \"Invalid cast " ++ show from ++ "->" ++ show to ++ "\")"

schOp BelieveMe [_,_,x] = x
schOp Crash [_,msg] = "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"

||| Extended primitives for the scheme backend, outside the standard set of primFn
public export
data ExtPrim = NewIORef | ReadIORef | WriteIORef
             | NewArray | ArrayGet | ArraySet
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
             | OnCollect
             | OnCollectAny
             | Unknown Name

export
Show ExtPrim where
  show NewIORef = "NewIORef"
  show ReadIORef = "ReadIORef"
  show WriteIORef = "WriteIORef"
  show NewArray = "NewArray"
  show ArrayGet = "ArrayGet"
  show ArraySet = "ArraySet"
  show GetField = "GetField"
  show SetField = "SetField"
  show VoidElim = "VoidElim"
  show SysOS = "SysOS"
  show SysCodegen = "SysCodegen"
  show OnCollect = "OnCollect"
  show OnCollectAny = "OnCollectAny"
  show (Unknown n) = "Unknown " ++ show n

||| Match on a user given name to get the scheme primitive
toPrim : Name -> ExtPrim
toPrim pn@(NS _ n)
    = cond [(n == UN "prim__newIORef", NewIORef),
            (n == UN "prim__readIORef", ReadIORef),
            (n == UN "prim__writeIORef", WriteIORef),
            (n == UN "prim__newArray", NewArray),
            (n == UN "prim__arrayGet", ArrayGet),
            (n == UN "prim__arraySet", ArraySet),
            (n == UN "prim__getField", GetField),
            (n == UN "prim__setField", SetField),
            (n == UN "void", VoidElim),
            (n == UN "prim__os", SysOS),
            (n == UN "prim__codegen", SysCodegen),
            (n == UN "prim__onCollect", OnCollect),
            (n == UN "prim__onCollectAny", OnCollectAny)
            ]
           (Unknown pn)
toPrim pn = Unknown pn

export
mkWorld : String -> String
mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes

schConstant : (String -> String) -> Constant -> String
schConstant _ (I x) = show x
schConstant _ (BI x) = show x
schConstant _ (B8 x) = show x
schConstant _ (B16 x) = show x
schConstant _ (B32 x) = show x
schConstant _ (B64 x) = show x
schConstant schString (Str x) = schString x
schConstant _ (Ch x)
   = if (the Int (cast x) >= 32 && the Int (cast x) < 127)
        then "#\\" ++ cast x
        else "(integer->char " ++ show (the Int (cast x)) ++ ")"
schConstant _ (Db x) = show x
schConstant _ WorldVal = "#f"
schConstant _ IntType = "#t"
schConstant _ IntegerType = "#t"
schConstant _ Bits8Type = "#t"
schConstant _ Bits16Type = "#t"
schConstant _ Bits32Type = "#t"
schConstant _ Bits64Type = "#t"
schConstant _ StringType = "#t"
schConstant _ CharType = "#t"
schConstant _ DoubleType = "#t"
schConstant _ WorldType = "#t"

schCaseDef : Maybe String -> String
schCaseDef Nothing = ""
schCaseDef (Just tm) = "(else " ++ tm ++ ")"

export
schArglist : List Name -> String
schArglist [] = ""
schArglist [x] = schName x
schArglist (x :: xs) = schName x ++ " " ++ schArglist xs

mutual
  used : Name -> NamedCExp -> Bool
  used n (NmLocal fc n') = n == n'
  used n (NmRef _ _) = False
  used n (NmLam _ _ sc) = used n sc
  used n (NmLet _ _ v sc) = used n v || used n sc
  used n (NmApp _ f args) = used n f || anyTrue (map (used n) args)
  used n (NmCon _ _ _ args) = anyTrue (map (used n) args)
  used n (NmOp _ _ args) = anyTrue (toList (map (used n) args))
  used n (NmExtPrim _ _ args) = anyTrue (map (used n) args)
  used n (NmForce _ t) = used n t
  used n (NmDelay _ t) = used n t
  used n (NmConCase _ sc alts def)
      = used n sc || anyTrue (map (usedCon n) alts)
            || maybe False (used n) def
  used n (NmConstCase _ sc alts def)
      = used n sc || anyTrue (map (usedConst n) alts)
            || maybe False (used n) def
  used n _ = False

  usedCon : Name -> NamedConAlt -> Bool
  usedCon n (MkNConAlt _ _ _ sc) = used n sc

  usedConst : Name -> NamedConstAlt -> Bool
  usedConst n (MkNConstAlt _ sc) = used n sc

parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
            schString : String -> String)
  showTag : Name -> Maybe Int -> String
  showTag n (Just i) = show i
  showTag n Nothing = schString (show n)

  mutual
    schConAlt : Int -> String -> NamedConAlt -> Core String
    schConAlt i target (MkNConAlt n tag args sc)
        = pure $ "((" ++ showTag n tag ++ ") "
                      ++ bindArgs 1 args !(schExp i sc) ++ ")"
      where
        bindArgs : Int -> (ns : List Name) -> String -> String
        bindArgs i [] body = body
        bindArgs i (n :: ns) body
            = if used n sc
                 then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
                    ++ bindArgs (i + 1) ns body ++ ")"
                 else bindArgs (i + 1) ns body

    schConUncheckedAlt : Int -> String -> NamedConAlt -> Core String
    schConUncheckedAlt i target (MkNConAlt n tag args sc)
        = pure $ bindArgs 1 args !(schExp i sc)
      where
        bindArgs : Int -> (ns : List Name) -> String -> String
        bindArgs i [] body = body
        bindArgs i (n :: ns) body
            = if used n sc
                 then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
                    ++ bindArgs (i + 1) ns body ++ ")"
                 else bindArgs (i + 1) ns body

    schConstAlt : Int -> String -> NamedConstAlt -> Core String
    schConstAlt i target (MkNConstAlt c exp)
        = pure $ "((equal? " ++ target ++ " " ++ schConstant schString c ++ ") " ++ !(schExp i exp) ++ ")"

    -- oops, no traverse for Vect in Core
    schArgs : Int -> Vect n NamedCExp -> Core (Vect n String)
    schArgs i [] = pure []
    schArgs i (arg :: args) = pure $ !(schExp i arg) :: !(schArgs i args)

    export
    schExp : Int -> NamedCExp -> Core String
    schExp i (NmLocal fc n) = pure $ schName n
    schExp i (NmRef fc n) = pure $ schName n
    schExp i (NmLam fc x sc)
       = do sc' <- schExp i  sc
            pure $ "(lambda (" ++ schName x ++ ") " ++ sc' ++ ")"
    schExp i (NmLet fc x val sc)
       = do val' <- schExp i val
            sc' <- schExp i sc
            pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")"
    schExp i (NmApp fc x [])
        = pure $ "(" ++ !(schExp i x) ++ ")"
    schExp i (NmApp fc x args)
        = pure $ "(" ++ !(schExp i x) ++ " " ++ showSep " " !(traverse (schExp i) args) ++ ")"
    schExp i (NmCon fc x tag args)
        = pure $ schConstructor schString x tag !(traverse (schExp i) args)
    schExp i (NmOp fc op args)
        = pure $ schOp op !(schArgs i args)
    schExp i (NmExtPrim fc p args)
        = schExtPrim i (toPrim p) args
    schExp i (NmForce fc t) = pure $ "(" ++ !(schExp i t) ++ ")"
    schExp i (NmDelay fc t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
    schExp i (NmConCase fc sc [] def)
        = do tcode <- schExp (i+1) sc
             defc <- maybe (pure "'erased") (schExp i) def
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) "
                     ++ defc ++ ")"
    schExp i (NmConCase fc sc [alt] Nothing)
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++
                    !(schConUncheckedAlt (i+1) n alt) ++ ")"
    schExp i (NmConCase fc sc alts Nothing)
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) "
                     ++ !(showAlts n alts) ++
                     "))"
      where
        showAlts : String -> List NamedConAlt -> Core String
        showAlts n [] = pure ""
        showAlts n [alt]
           = pure $ "(else " ++ !(schConUncheckedAlt (i + 1) n alt) ++ ")"
        showAlts n (alt :: alts)
           = pure $ !(schConAlt (i + 1) n alt) ++ " " ++
                    !(showAlts n alts)
    schExp i (NmConCase fc sc alts def)
        = do tcode <- schExp (i+1) sc
             defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) "
                     ++ showSep " " !(traverse (schConAlt (i+1) n) alts)
                     ++ schCaseDef defc ++ "))"
    schExp i (NmConstCase fc sc alts Nothing)
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "
                      ++ !(showConstAlts n alts)
                      ++ "))"
      where
        showConstAlts : String -> List NamedConstAlt -> Core String
        showConstAlts n [] = pure ""
        showConstAlts n [MkNConstAlt c exp]
           = pure $ "(else " ++ !(schExp (i + 1) exp) ++ ")"
        showConstAlts n (alt :: alts)
           = pure $ !(schConstAlt (i + 1) n alt) ++ " " ++
                    !(showConstAlts n alts)
    schExp i (NmConstCase fc sc alts def)
        = do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
             tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "
                      ++ showSep " " !(traverse (schConstAlt (i+1) n) alts)
                      ++ schCaseDef defc ++ "))"
    schExp i (NmPrimVal fc c) = pure $ schConstant schString c
    schExp i (NmErased fc) = pure "'erased"
    schExp i (NmCrash fc msg) = pure $ "(blodwen-error-quit " ++ show msg ++ ")"

  -- Need to convert the argument (a list of scheme arguments that may
  -- have been constructed at run time) to a scheme list to be passed to apply
  readArgs : Int -> NamedCExp -> Core String
  readArgs i tm = pure $ "(blodwen-read-args " ++ !(schExp i tm) ++ ")"

  fileOp : String -> String
  fileOp op = "(blodwen-file-op (lambda () " ++ op ++ "))"

  -- External primitives which are common to the scheme codegens (they can be
  -- overridden)
  export
  schExtCommon : Int -> ExtPrim -> List NamedCExp -> Core String
  schExtCommon i NewIORef [_, val, world]
      = pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")"
  schExtCommon i ReadIORef [_, ref, world]
      = pure $ mkWorld $ "(unbox " ++ !(schExp i ref) ++ ")"
  schExtCommon i WriteIORef [_, ref, val, world]
      = pure $ mkWorld $ "(set-box! "
                           ++ !(schExp i ref) ++ " "
                           ++ !(schExp i val) ++ ")"
  schExtCommon i NewArray [_, size, val, world]
      = pure $ mkWorld $ "(make-vector " ++ !(schExp i size) ++ " "
                                         ++ !(schExp i val) ++ ")"
  schExtCommon i ArrayGet [_, arr, pos, world]
      = pure $ mkWorld $ "(vector-ref " ++ !(schExp i arr) ++ " "
                                        ++ !(schExp i pos) ++ ")"
  schExtCommon i ArraySet [_, arr, pos, val, world]
      = pure $ mkWorld $ "(vector-set! " ++ !(schExp i arr) ++ " "
                                         ++ !(schExp i pos) ++ " "
                                         ++ !(schExp i val) ++ ")"
  schExtCommon i VoidElim [_, _]
      = pure "(display \"Error: Executed 'void'\")"
  schExtCommon i SysOS []
      = pure $ "(blodwen-os)"
  schExtCommon i (Unknown n) args
      = throw (InternalError ("Can't compile unknown external primitive " ++ show n))
  schExtCommon i prim args
      = throw (InternalError ("Badly formed external primitive " ++ show prim
                                ++ " " ++ show args))

  schDef : {auto c : Ref Ctxt Defs} ->
           Name -> NamedDef -> Core String
  schDef n (MkNmFun args exp)
     = pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") "
                      ++ !(schExp 0 exp) ++ "))\n"
  schDef n (MkNmError exp)
     = pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 exp) ++ ")\n"
  schDef n (MkNmForeign _ _ _) = pure "" -- compiled by specific back end
  schDef n (MkNmCon t a _) = pure "" -- Nothing to compile here

-- Convert the name to scheme code
-- (There may be no code generated, for example if it's a constructor)
export
getScheme : {auto c : Ref Ctxt Defs} ->
            (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String) ->
            (schString : String -> String) ->
            (Name, FC, NamedDef) -> Core String
getScheme schExtPrim schString (n, fc, d)
    = schDef schExtPrim schString n d


text:
counts: String -> (Nat, Nat)
counts str = (length (words str), length str)

top_ten : Ord a => List a -> List a
top_ten l = take 10 (reverse (sort l))

over_length : Nat -> List String -> Nat
over_length n l = length (filter (> 3) (map length l))


text:
module IdrisProject

||| document
export
plus_reduces : (n : Nat) -> Z + n = n
plus_reduces n = Refl

export
plus_right_id : (n : Nat) -> n + 0 = n
plus_right_id Z = Refl
plus_right_id (S n) = cong S (plus_right_id n)

export
plus_reduces_S : (n : Nat) -> (m : Nat) -> n + (S m) = S (n + m)
plus_reduces_S Z m = cong S Refl
-- cong: congruence, take `f` to show `a = b` iff `(f a) = (f b)`
plus_reduces_S (S k) m = cong S (plus_reduces_S k m)

export
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z 0 = Refl
plus_commutes_Z (S k) = cong S (plus_commutes_Z k)

export
plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k 0 = Refl
plus_commutes_S k (S j) = cong S (plus_commutes_S k j)

export
plus_commutes : (n, m : Nat) -> n + m = m + n
plus_commutes Z m = (plus_commutes_Z m)
plus_commutes (S k) m = rewrite plus_commutes k m in (plus_commutes_S k m)

export
sym : forall x, y . (0 rule : x = y) -> y = x
sym Refl = Refl

export
trans : forall x, y, z . (0 l : x = y) -> (0 r : y = z) -> x = z
trans Refl Refl = Refl

max_stars_repo_name: dannypsnl/idris-project

max_issues_repo_name: dannypsnl/idris-project

max_forks_repo_name: dannypsnl/idris-project


text:
module Main

import Data.Vect

%default total

addRow :  Num numType
       => (x : Vect cols numType)
       -> (y : Vect cols numType)
       -> Vect cols numType
addRow       []        []  = []
addRow (x :: xs) (y :: ys) = x + y :: addRow xs ys

addMatrix :  Num numType
          => Vect rows (Vect cols numType)
          -> Vect rows (Vect cols numType)
          -> Vect rows (Vect cols numType)
addMatrix       []        []  = []
addMatrix (x :: xs) (y :: ys) = addRow x y :: addMatrix xs ys

tam : Vect 3 (Vect 2 Int)
tam = addMatrix [[ 1, 2]
                ,[ 3, 4]
                ,[ 5, 6]]
                [[ 7, 8]
                ,[ 9,10]
                ,[11,12]]

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

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

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

ttm1 : Vect 2 (Vect 3 Integer)
ttm1 = transposeMat [ [1,2]
                    , [3,4]
                    , [5,6] ]

ttm2 : Vect 4 (Vect 3 Integer)
ttm2 = transposeMat [ [1, 2, 3, 4]
                    , [5, 6, 7, 8]
                    , [9,10,11,12] ]

tmmil : Vect 3 (Vect 2 Integer)
tmmil =        [[ 1,  2]
               ,[ 3,  4]
               ,[ 5,  6]]

tmmir : Vect 2 (Vect 4 Integer)
tmmir = [[ 7, 8, 9,10]
        ,[11,12,13,14]]

ttm3 : Vect 4 (Vect 2 Integer)
ttm3 = transposeMat tmmir

ttm4 : Bool
ttm4 = ttm3    == [[ 7, 11]
                  ,[ 8, 12]
                  ,[ 9, 13]
                  ,[10, 14]]

multRow' :  Num numType
         => (x : Vect m numType)
         -> (y : Vect m numType)
         -> numType
multRow'       []        []  = 0
multRow' (x :: xs) (y :: ys) = x * y + multRow' xs ys

multRow :  Num numType
        => (x : Vect m numType)
        -> (ysTrans : Vect p (Vect m numType))
        -> Vect p numType
multRow x       []  = []
multRow x (y :: ys) = multRow' x y :: multRow x ys

multMatrix :  Num numType
           => Vect n (Vect m numType)
           -> Vect m (Vect p numType)
           -> Vect n (Vect p numType)
multMatrix       []  ys = []
multMatrix (x :: xs) ys =
  let ysTrans = transposeMat ys
  in ((multRow x ysTrans) :: multMatrix xs ys)

tmmr : Vect 3 (Vect 4 Integer)
tmmr = [[ 29, 32, 35, 38]
       ,[ 65, 72, 79, 86]
       ,[101,112,123,134]]

tmm : Bool
tmm = multMatrix tmmil tmmir == tmmr

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Main

import Data.List

data Tree a = Empty
            | Node (Tree a) a (Tree a)

Show a => Show (Tree a) where
  show Empty = "Empty"
  show (Node left val right) = "(Node " ++ show left ++ " " ++ show val ++ " " ++ show right ++ ")"

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty)
                      "Fred"
                      (Node Empty "Sheila" Empty))
                "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

treeLabelWith
  : Stream labelType
  -> Tree a
  -> (Stream labelType, Tree (labelType, a))
treeLabelWith lbls Empty = (lbls, Empty)
treeLabelWith lbls (Node left val right)
  = let (lblThis :: lblsLeft, leftLabelled) = treeLabelWith lbls left
        (lblRight, rightLabelled) = treeLabelWith lblsLeft right
    in (lblRight, Node leftLabelled (lblThis, val) rightLabelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = snd (treeLabelWith [1..] tree)

main : IO ()
main = do
  printLn $ flatten testTree
  printLn $ flatten $ treeLabel testTree

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith lbls [] = []
labelWith (lbl :: lbls) (x :: xs) = (lbl, x) :: labelWith lbls xs

label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
import Data.List
import Data.List1
import Data.String

import System.File

simulate1 : Nat -> Nat -> Nat
simulate1 0 c = 1
simulate1 (S n) 0 = simulate1 n 6 + simulate1 n 8
simulate1 (S n) (S c) = simulate1 n c

run : String -> IO ()
run s = do let l = group $ sort $ catMaybes $ parsePositive {a=Nat} <$> (forget $ split (== ',') s)
           let n = sum $ (\l@(c ::: _) => (length $ forget $ l) * simulate1 256 c) <$> l
           putStrLn $ show n

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Data.JSON

import public Data.JSON.Value
import Data.JSON.FromString
import Data.JSON.ToString

public export
interface ToJSON a where
  toJSON : a -> JSONValue

encode : ToJSON a => a -> String
encode = toString . toJSON

public export
interface FromJSON a where
  fromJSON : JSONValue -> Maybe a

decode : FromJSON a => String -> Maybe a
decode = fromJSON . fromString


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

equalityEq : Bool
equalityEq = ?fillme1 == True

equalityNeq : Bool
equalityNeq = ?fillme2 /= 3

equalityGeq : Bool
equalityGeq = ?fillme3 >= 4

equalityGtr : Bool
equalityGtr = ?fillme4 > 4

equalityLeq : Bool
equalityLeq = ?fillme5 <= 5

equalityLess : Bool
equalityLess = ?fillme6 < 6

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

max_stars_repo_name: yurrriq/idris-koans

max_issues_repo_name: TheWizardTower/idris-koans

max_forks_repo_name: yurrriq/idris-koans


text:
--- Data declarations ---

data (.ah) a = Ah (List a)

g : Int .ah -> Int
g (Ah xs) = sum xs

--- Records ---

record (.aah) a where
  constructor Aah
  unaah : List a

h : Num a => a.aah -> a
h = sum . unaah

--- Interfaces ---

interface (.defaultable) a where
  defa : a

(.defaultable) Int where
  defa = 0

f : Num a => a.defaultable => a -> a
f x = x + defa


text:
-- Reverse.idr
-- Reversing string interactively, using 'repl'

module Main

main : IO ()
main = repl "> " reverse

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
\iffalse
SPDX-License-Identifier: AGPL-3.0-only

This file is part of `idris-ct` Category Theory in Idris library.

Copyright (C) 2019 Stichting Statebox <https://statebox.nl>

This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Affero General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU Affero General Public License for more details.

You should have received a copy of the GNU Affero General Public License
along with this program.  If not, see <https://www.gnu.org/licenses/>.
\fi

> module Monoid.MonoidMorphismAsFunctor
>
> import Basic.Category
> import Basic.Functor
> import Monoid.Monoid
> import Monoid.MonoidAsCategory
> import Monoid.MonoidMorphism
>
> -- contrib
> import Interfaces.Verified
>
> %access public export
> %default total
>
> monoidMorphismToFunctor :
>      (monoid1, monoid2 : Monoid)
>   -> MonoidMorphism monoid1 monoid2
>   -> CFunctor (monoidAsCategory monoid1) (monoidAsCategory monoid2)
> monoidMorphismToFunctor monoid1 monoid2 (MkMonoidMorphism fun frOp frId) =
>   MkCFunctor
>     id
>     (\_, _ => fun)
>     (\_ => frId)
>     (\_, _, _, f, g => frOp f g)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Effect.Baseline

import Effects
import Baseline

%access public export

data Baseline : Effect where
  Readline : String -> sig Baseline (Maybe String)
  AddDictEntry : String -> sig Baseline ()
  AddDictEntries : Traversable t => t String -> sig Baseline ()
  ReadHistory : String -> sig Baseline ()
  WriteHistory : String -> sig Baseline ()

Handler Baseline IO where
  handle () (Readline p)        k = do x <- baseline p; k x ()
  handle () (AddDictEntry e)    k = do addDictEntry e; k () ()
  handle () (AddDictEntries es) k = do sequence_ (map addDictEntry es); k () ()
  handle () (ReadHistory file)  k = do readHistory file; k () ()
  handle () (WriteHistory file) k = do writeHistory file; k () ()

BASELINE : EFFECT
BASELINE = MkEff () Baseline

||| Run the readline prompt and save input to history.
baseline : (prompt : String) -> Eff (Maybe String) [BASELINE]
baseline prompt = call (Readline prompt)

||| Add an entry to tab completion dictionary.
addDictEntry : (entry : String) -> Eff () [BASELINE]
addDictEntry entry = call (AddDictEntry entry)

||| Add multiple entries to tab completion dictionary.
addDictEntries : Traversable t => (entries : t String) -> Eff () [BASELINE]
addDictEntries entries = call (AddDictEntries entries)

||| Recover saved history from file.
readHistory : (filename : String) -> Eff () [BASELINE]
readHistory file = call (ReadHistory file)

||| Save history to file.
writeHistory : (filename : String) -> Eff () [BASELINE]
writeHistory file = call (WriteHistory file)

max_stars_repo_name: laserpants/baseline-idris

max_issues_repo_name: laserpants/baseline-idris

max_forks_repo_name: laserpants/baseline-idris


text:
module Python.Lib.Numpy

import Python
import Python.Prim
import Data.Erased

%default total
%access public export

NDArray : Signature
NDArray f = case f of
  "__str__" => [] ~~> String
  _ => Object f

Arr : Type
Arr = Obj NDArray

ArithT : Type -> Signature
ArithT a f = case f of
  "__add__" => [a, a] ~~> a
  "__mul__" => [a, a] ~~> a
  "__sub__" => [a, a] ~~> a
  "__div__" => [a, a] ~~> a
  "__str__" => [a] ~~> String
  _ => PyType f

Mat : Nat -> Nat -> Maybe a -> Signature
Mat _ _ _ = Object

NDArrayT : Signature
NDArrayT f = case f of
  "transpose" => [Arr] ~~> Arr
  _ => ArithT Arr f

  "transpose_fulldep" => fun $
    forall r : Nat .
      forall c : Nat .
        forall a : Type .
          forall dtype : (Maybe a) .
            pi m : (Obj $ Mat r c dtype) .
              Return (Obj $ Mat c r dtype)

Numpy : Signature
Numpy f = case f of

  "array" => PAttr _ $ \a : Type =>
      [Obj (PyList (Obj (PyList a))), String] ~> Arr

  "reshape" => [Arr, (Nat, Nat)] ~~> Arr
  "abs" => [Arr] ~~> Arr
  "dot" => [Arr, Arr] ~~> Arr
  "transpose" => [Arr] ~~> Arr
  "tile" => [Dyn, (Nat, Nat)] ~~> Arr
  "ndarray" => Attr $ Obj NDArrayT
  _ => Module f

import_ : PIO $ Obj Numpy
import_ = importModule "numpy"

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Equis.Regression.LeastSquares

import Solver
import Matrix.Numeric
import Data.Matrix.Numeric

%access private

||| Calculates a length-n vector of powers of some number, smallest power first.
|||
||| @ord the length of the vector to calculate
||| @x the number
powers : Num a => (ord : Nat) -> (x : a) -> Vect (S ord) a
powers ord x = reverse (powers' ord x) where
  ||| Calculates a length-n vector of powers of some number, largest power first.
  |||
  ||| @ord the length of the vector to calculate
  ||| @x the number
  powers' : (ord : Nat) -> (x : a) -> Vect (S ord) a
  powers' Z _ = 1
  powers' (S Z) x = [x, 1]
  powers' (S k) x = let y@(n :: _) = powers' k x in (n * x) :: y

||| Performs least-squares polynomial fitting on the given independent and dependent values, returning the resulting
||| coefficients.
|||
||| @ord the order of the polynomial
||| @ind the values of the independent variable
||| @dep the values of the dependent variable
export
leastSquares : Neg a => Fractional a => (ord : Nat) -> (ind : Vect (S n) a) -> (dep : Vect (S n) a) -> Vect (S ord) a
leastSquares ord ind dep = leastSquares' (map (powers ord) ind) dep where
  ||| Performs least-squares polynomial fitting on the given independent and dependent values, returning the resulting
  ||| coefficients.
  |||
  ||| @ind the values of the independent variable
  ||| @dep the values of the dependent variable
  leastSquares' : (ind : Matrix (S n) (S m) a) -> (dep : Vect (S n) a) -> Vect (S m) a
  leastSquares' ind dep = ((inverseGram ind) <> (transpose ind)) </> dep

||| Performs least-squares polynomial fitting on the given independent and dependent values, returning the resulting
||| function.
|||
||| @ord the order of the polynomial
||| @ind the values of the independent variable
||| @dep the values of the dependent variable
export
leastSquaresFn : (ord : Nat) -> (ind : Vect (S n) Double) -> (dep : Vect (S n) Double) -> (Double -> Double)
leastSquaresFn ord ind dep = (\i => sum (zipWith (*) (powers ord i) (leastSquares ord ind dep)))

max_stars_repo_name: lambdacasserole/equis

max_issues_repo_name: lambdacasserole/equis

max_forks_repo_name: lambdacasserole/equis


text:
module Cordial.EDSL.Description.Lang

import Data.Vect
import Data.List.Quantifiers
import Data.Ranged

import Text.Markup.Edda

import Language.EDSL.SingleStateVar

import Cordial.Model.Specification

%default total
%access public export

-- ------------------------------------------------- [ Important Language Defs ]

data Used = FREE | USED

||| State associated with labels.
record State (labelType : Type) where
  constructor MkState
  used  : Used
  label : labelType

VarState : Type -> Type
VarState labelTy = StateItem (State labelTy)

Gamma : Type -> Type
Gamma labelTy = Context (State labelTy)

-- -------------------------------------------------------------- [ Predicates ]

namespace Predicates

  data CanUseVar : (labelTy : Type) -> Var -> VarState labelTy -> Type where
    FreeName : CanUseVar type lbl (MkStateItem lbl $ MkState FREE val)

  data UsedVar : (labelTy : Type) -> VarState labelTy -> Type where
    NameIsUsed : UsedVar type (MkStateItem lbl $ MkState USED val)

  VarsAllUsed : (labelTy : Type) -> (ctxt : Gamma labelTy) -> Type
  VarsAllUsed labelTy ctxt =
    AllContext (UsedVar labelTy) ctxt

  data VarIsNotNamed : (labelTy : Type)
                    -> (label : labelTy)
                    -> VarState labelTy
                    -> Type where
    IsNotNamed : Eq labelTy
              => {l,r : labelTy}
              -> (prf : l /= r = True)
              -> VarIsNotNamed labelTy l (MkStateItem lbl (MkState u r))

  CanUseName : (label : labelTy) -> (ctxt : Gamma labelTy) -> Type
  CanUseName {labelTy} label =
    AllContext (VarIsNotNamed labelTy label)

-- ----------------------------------------------------------------- [ Updates ]

namespace Functions
  Consume : (item : VarState labelTy)
         -> (bewijs : CanUseVar labelTy lbl item)
         -> VarState labelTy
  Consume item bewijs with (bewijs)
    Consume (MkStateItem lbl (MkState FREE val)) bewijs | FreeName =
      MkStateItem lbl (MkState USED val)

-- ------------------------------------------------------------- [ Expressions ]

record Metadata where
  constructor MkMetadata
  mvendor  : Maybe String
  mlibrary : Maybe String
  mname    : Maybe String
  mversion : Maybe String
  mmaxp    : Maybe Whole
  mmaxc    : Maybe Whole
  mcstyle  : Maybe CommStyle
  mdoc     : Maybe DocString

processMetadata : Metadata -> (VLNV, (Whole, Whole), CommStyle, DocString)
processMetadata (MkMetadata mvendor mlibrary mname mversion mmax mmin mcstyle mdoc) =
  let vlnv = MkVLNV (fromMaybe "Default Vendor" mvendor)
                    (fromMaybe "Default Library" mlibrary)
                    (fromMaybe "Default Name" mname)
                    (fromMaybe "Default Version" mversion) in
  let a = (fromMaybe (fromNat 1) mmin, fromMaybe (fromNat 1) mmax) in
  let c = fromMaybe Unicast mcstyle in
  let d = fromMaybe Empty mdoc in
    (vlnv, a,c,d)

defaultMetadata : Metadata
defaultMetadata =
  MkMetadata
     Nothing
     Nothing
     Nothing
     Nothing
     Nothing
     Nothing
     Nothing
     Nothing

data ExprTy = DECL | MDATA | NAME | END

data IDescribe : (labelTy : Type) -> Lang ExprTy (State labelTy) where
   NewName : (name : labelTy)
          -> (prf  : CanUseName name old)
          -> IDescribe labelTy NAME Var old (\lbl => MkStateItem lbl (MkState FREE name)::old)

   Stop : (prf : VarsAllUsed labelTy old)
       -> IDescribe labelTy END () old (const Nil)

   SetMetadata : (Metadata -> Metadata)
              -> IDescribe labelTy MDATA () old (const old)

   DeclareSignal : (label  : Var)
                -> (kind  : PortShape)
                -> (wirety : WireTy)
                -> (flow  : Flow)
                -> (width : PortWidthDesc kind)

                -> (sense : Sensitivity)

                -> (required : OptionalTy)
                -> (origin   : Origin)

                -> (vorigin : ValueOrigin width)
                -> (doc : DocString)

                -> (prf : InContext (CanUseVar labelTy label) old)

                -> IDescribe labelTy DECL () old (const $ update Consume old prf)

   Replicate : (n : Nat)
            -> (var : Var)
            -> (kind : PortShape)
            -> (wirety : WireTy)
            -> (flow  : Flow)
            -> (width : PortWidthDesc kind)

            -> (sense : Sensitivity)

            -> (required : OptionalTy)
            -> (origin   : Origin)

            -> (vorigin : ValueOrigin width)
            -> (doc : DocString)
            -> (prf : InContext (CanUseVar labelTy var) old)
            -> IDescribe labelTy DECL () old (const $ update Consume old prf)

LangIDL : (labelTy : Type) -> LANG ExprTy (State labelTy)
LangIDL labelTy = MkLang ExprTy
                         (State labelTy)
                         (Name WHOLE labelTy)
                         (IDescribe labelTy)

namespace API
  IDL' : (labelTy : Type) -> (m : Type -> Type) -> Type
  IDL' ty m = LangM m () (LangIDL ty) (TyStmt) Nil (const Nil)

  label : (name : labelTy)
         -> {auto prf : CanUseName name old}
         -> LangM m Var (LangIDL labelTy) (TyExpr NAME) old (\lbl => MkStateItem lbl (MkState FREE name)::old)
  label n {prf} = Expr $ NewName n prf

  stop : {auto prf : VarsAllUsed labelTy old}
      -> LangM m () (LangIDL labelTy) (TyExpr END) old (const Nil)
  stop {prf} = Expr (Stop prf)

  setMetadata : (Metadata -> Metadata) -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setMetadata f = Expr (SetMetadata f)

  signal : (label  : Var)
        -> (kind  : PortShape)
        -> (wirety : WireTy)
        -> (flow  : Flow)
        -> (width : PortWidthDesc kind)

        -> (sense : Sensitivity)

        -> (required : OptionalTy)
        -> (origin   : Origin)

        -> (vorigin : ValueOrigin width)
        -> (doc : DocString)

        -> (prf : InContext (CanUseVar labelTy label) old)
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old prf)
  signal label kind wirety flow width sense required origin vorigin doc prf =
    Expr $ DeclareSignal label kind wirety flow width sense required origin vorigin doc prf

  replicateExpr : (n : Nat)
           -> (var : Var)
           -> (kind : PortShape)
           -> (wirety : WireTy)
           -> (flow  : Flow)
           -> (width : PortWidthDesc kind)

           -> (sense : Sensitivity)

           -> (required : OptionalTy)
           -> (origin   : Origin)

           -> (vorigin : ValueOrigin width)
           -> (doc : DocString)
           -> {auto prf : InContext (CanUseVar labelTy var) old}

           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old prf)
  replicateExpr n var kind wirety flow width sense required origin vorigin doc {prf} =
    Expr $ Replicate n var kind wirety flow width sense required origin vorigin doc prf

nCopies : (c : Nat)
       -> (n : Name WHOLE labelTy)
       -> (kind  : PortShape)
       -> (wirety : WireTy)
       -> (flow  : Flow)
       -> (width : PortWidthDesc kind)

       -> (sense : Sensitivity)

       -> (required : OptionalTy)
       -> (origin   : Origin)

       -> (vorigin : ValueOrigin width)
       -> (doc : DocString)
       -> PortGroupTy () labelTy
nCopies c (WName xs x) k ty f w s r o vo doc =
    map (\i => PortDesc () k (IName xs x i) ty f w s r o vo doc) (countdown c)
  where
    countdown : Nat -> List Nat
    countdown Z     = [Z]
    countdown (S j) = S j :: countdown j

namespace Pure
  Builder (LangIDL labelTy) (Metadata, PortGroupTy () labelTy) Basics.id where
    build env (NewName name prf) (mdata,pg) cont =
      cont MkVar (MkTag (WName Nil name) :: env) (mdata,pg)

    build env (Stop prf) (mdata, acc) cont =
      cont () Nil (mdata, acc)

    build env (SetMetadata f) (mdata,acc) cont =
      cont () env ((f mdata),acc)

    build env (DeclareSignal label kind wirety flow width sense required origin vorigin doc prf) (mdata,acc) cont with (lookup env prf)
      build env (DeclareSignal label kind wirety flow width sense required origin vorigin doc prf) (mdata,acc) cont | (MkTag (WName xs x)) =
        cont () (update env prf Consume) (mdata,(PortDesc () kind (WName xs x) wirety flow width sense required origin vorigin doc :: acc))

    build env (Replicate n var kind wirety flow width sense required origin vorigin doc prf) (mdata, acc) cont with (lookup env prf)
      build env (Replicate n var kind wirety flow width sense required origin vorigin doc prf) (mdata, acc) cont | (MkTag (WName xs x)) =
        let ports = nCopies n (WName xs x) kind wirety flow width sense required origin vorigin doc in
          cont () (update env prf Consume) (mdata, ports ++ acc)

  IDL : (labelTy : Type) -> Type
  IDL ty = IDL' ty Basics.id

  buildSpec : IDL labelTy
           -> InterfaceTy () labelTy
  buildSpec expr =
      let (MkResult () (mdata,ps)) = runPure (defaultMetadata, List.Nil) expr in
      let (vlnv, (minA, minB), cstyle, doc) = processMetadata mdata in
        MkInterfaceTy vlnv () cstyle minA minB ps Nil doc

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
-- Copyright (c) 2017, Matthew Morris
--
-- Permission to use, copy, modify, and/or distribute this software for any
-- purpose with or without fee is hereby granted, provided that the above
-- copyright notice and this permission notice appear in all copies.
--
-- THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
-- WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
-- MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
-- ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
-- WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
-- ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
-- OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.

module Main

fizzbuzz : Integer -> String
fizzbuzz n with (mod n 3, mod n 5)
  fizzbuzz n | (0, 0) = "fizzbuzz"
  fizzbuzz n | (0, _) = "fizz"
  fizzbuzz n | (_, 0) = "buzz"
  fizzbuzz n | _ = show n

main : IO ()
main =
  traverse_ putStrLn $ map fizzbuzz [1..100]


text:
module Control.EffectAlgebra

import public Control.HigherOrder
import public Control.Effect.Misc

||| Structure that dispatches an effect.
public export
interface Monad m => Algebra sig m | m where
  constructor MkAlgebra
  alg : (f : Functor ctx)
     => ctx ()
     -> Handler ctx n m
     -> sig n a
     -> m (ctx a)

||| Apply an effect within a monadic context that supports it.
public export
send : Inj eff sig => Algebra sig m => eff m a -> m a
send eff = alg {ctx = id} () id (inj eff)


text:
module Web.Raw.Url

import JS
import Web.Internal.UrlPrim
import Web.Internal.Types

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

namespace URL

  export
  new : (url : String) -> (base : Optional String) -> JSIO URL
  new a b = primJS $ URL.prim__new a (toFFI b)

  export
  new' : (url : String) -> JSIO URL
  new' a = primJS $ URL.prim__new a undef

  export
  createObjectURL : (obj : NS I [ Blob , MediaSource ]) -> JSIO String
  createObjectURL a = primJS $ URL.prim__createObjectURL (toFFI a)

  export
  createObjectURL1 : (mediaSource : MediaSource) -> JSIO String
  createObjectURL1 a = primJS $ URL.prim__createObjectURL1 a

  export
  revokeObjectURL : (url : String) -> JSIO ()
  revokeObjectURL a = primJS $ URL.prim__revokeObjectURL a

  export
  hash : URL -> Attribute True I String
  hash v = fromPrim "URL.gethash" prim__hash prim__setHash v

  export
  host : URL -> Attribute True I String
  host v = fromPrim "URL.gethost" prim__host prim__setHost v

  export
  hostname : URL -> Attribute True I String
  hostname v = fromPrim "URL.gethostname" prim__hostname prim__setHostname v

  export
  href : URL -> Attribute True I String
  href v = fromPrim "URL.gethref" prim__href prim__setHref v

  export
  origin : (obj : URL) -> JSIO String
  origin a = primJS $ URL.prim__origin a

  export
  password : URL -> Attribute True I String
  password v = fromPrim "URL.getpassword" prim__password prim__setPassword v

  export
  pathname : URL -> Attribute True I String
  pathname v = fromPrim "URL.getpathname" prim__pathname prim__setPathname v

  export
  port : URL -> Attribute True I String
  port v = fromPrim "URL.getport" prim__port prim__setPort v

  export
  protocol : URL -> Attribute True I String
  protocol v = fromPrim "URL.getprotocol" prim__protocol prim__setProtocol v

  export
  search : URL -> Attribute True I String
  search v = fromPrim "URL.getsearch" prim__search prim__setSearch v

  export
  searchParams : (obj : URL) -> JSIO URLSearchParams
  searchParams a = primJS $ URL.prim__searchParams a

  export
  username : URL -> Attribute True I String
  username v = fromPrim "URL.getusername" prim__username prim__setUsername v

  export
  toJSON : (obj : URL) -> JSIO String
  toJSON a = primJS $ URL.prim__toJSON a

namespace URLSearchParams

  export
  new :  (init : Optional (NS I [ Array (Array String)
                                , Record String String
                                , String
                                ]))
      -> JSIO URLSearchParams
  new a = primJS $ URLSearchParams.prim__new (toFFI a)

  export
  new' : JSIO URLSearchParams
  new' = primJS $ URLSearchParams.prim__new undef

  export
  append :  (obj : URLSearchParams)
         -> (name : String)
         -> (value : String)
         -> JSIO ()
  append a b c = primJS $ URLSearchParams.prim__append a b c

  export
  delete : (obj : URLSearchParams) -> (name : String) -> JSIO ()
  delete a b = primJS $ URLSearchParams.prim__delete a b

  export
  getAll : (obj : URLSearchParams) -> (name : String) -> JSIO (Array String)
  getAll a b = primJS $ URLSearchParams.prim__getAll a b

  export
  get : (obj : URLSearchParams) -> (name : String) -> JSIO (Maybe String)
  get a b = tryJS "URLSearchParams.get" $ URLSearchParams.prim__get a b

  export
  has : (obj : URLSearchParams) -> (name : String) -> JSIO Bool
  has a b = tryJS "URLSearchParams.has" $ URLSearchParams.prim__has a b

  export
  set :  (obj : URLSearchParams)
      -> (name : String)
      -> (value : String)
      -> JSIO ()
  set a b c = primJS $ URLSearchParams.prim__set a b c

  export
  sort : (obj : URLSearchParams) -> JSIO ()
  sort a = primJS $ URLSearchParams.prim__sort a

  export
  toString : (obj : URLSearchParams) -> JSIO String
  toString a = primJS $ URLSearchParams.prim__toString a


text:
import Control.Monad.Coop

import System.Clock

millis : HasIO io => io Integer
millis = liftIO $ composeTime <$> clockTime Monotonic where
  composeTime : Clock Monotonic -> Integer
  composeTime (MkClock secs nanos) = secs * 1000 + nanos `div` 1000000

Timed IO where
  currentTime = fromInteger <$> millis

printTime : HasIO io => (offset : Integer) -> String -> io Unit
printTime offset s = printLn $ "[time: " ++ show (!millis - offset) ++ "] " ++ s

forever : Monad m => m a -> m b
forever x = do x; forever x

export
main : IO Unit
main = do printLn "before coop"
          runCoop $ do
  offset <- millis
  printTime offset "start"
  (<||>)
    (forever $ do
      printTime offset "proc 1, before 1000"
      sleepFor 1000
      printTime offset "proc 1, before 2000"
      sleepFor 2000)
    (forever $ do
      printTime offset "                     proc 2, before 350"
      sleepFor 350
      printTime offset "                     proc 2, before 750"
      sleepFor 750)

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Core.TT.Traversals

import Core.TT
import Core.Ord

import Data.DPair
import Data.SnocList
import Libraries.Data.NameMap
import Libraries.Data.SortedSet

%default covering

export
unBinds : Term vars -> Exists (\ outer => Term (outer <>> vars))
unBinds (Bind _ x _ scope) = let (Evidence outer t) = unBinds scope in
                             Evidence (outer :< x) t
unBinds t = Evidence [<] t

export
onPRefs : Monoid m =>
          (Name      -> m) ->
          (Term vars -> m)
onPRefs f = go neutral where

  go  : m -> Term vars' -> m
  gos : m -> List (Term vars') -> m

  go acc (Local fc isLet idx p) = acc
  go acc (Ref fc x name) = acc <+> f name
  go acc (Meta fc x y xs) = gos acc xs
  go acc (Bind fc x b scope) = go (acc <+> concatMap (onPRefs f) b) scope
  go acc (App fc fn arg) = go (go acc fn) arg
  go acc (As fc x as pat) = go (go acc as) pat
  go acc (TDelayed fc x y) = go acc y
  go acc (TDelay fc x ty arg) = go (go acc ty) arg
  go acc (TForce fc x y) = go acc y
  go acc (PrimVal fc c) = acc
  go acc (Erased fc imp) = acc
  go acc (TType fc u) = acc

  gos acc [] = acc
  gos acc (x :: xs) = gos (go acc x) xs

export
allGlobals : Term vars -> NameMap ()
allGlobals = onPRefs (\ n => singleton n ())

export
onConstants : Monoid m =>
          (Constant  -> m) ->
          (Term vars -> m)
onConstants f = go neutral where

  go  : m -> Term vars' -> m
  gos : m -> List (Term vars') -> m

  go acc (Local fc isLet idx p) = acc
  go acc (Ref fc x name) = acc
  go acc (Meta fc x y xs) = gos acc xs
  go acc (Bind fc x b scope) = go (acc <+> concatMap (onConstants f) b) scope
  go acc (App fc fn arg) = go (go acc fn) arg
  go acc (As fc x as pat) = go (go acc as) pat
  go acc (TDelayed fc x y) = go acc y
  go acc (TDelay fc x ty arg) = go (go acc ty) arg
  go acc (TForce fc x y) = go acc y
  go acc (PrimVal fc c) = acc <+> f c
  go acc (Erased fc imp) = acc
  go acc (TType fc u) = acc

  gos acc [] = acc
  gos acc (x :: xs) = gos (go acc x) xs

export
allConstants : Term vars -> SortedSet Constant
allConstants = onConstants @{MkMonoid @{MkSemigroup union} empty} singleton

export
mapTermM : Monad m =>
           ({vars : _} -> Term vars -> m (Term vars)) ->
           ({vars : _} -> Term vars -> m (Term vars))
mapTermM f t = act t where

  act : {vars : _} -> Term vars -> m (Term vars)
  go  : {vars : _} -> Term vars -> m (Term vars)

  act t = f =<< go t

  go t@(Local fc isLet idx p) = pure t
  go t@(Ref fc x name) = pure t
  go t@(Meta fc x y xs) = Meta fc x y <$> traverse act xs
  go t@(Bind fc x b scope) = Bind fc x <$> traverse act b <*> act scope
  go t@(App fc fn arg) = App fc <$> act fn <*> act arg
  go t@(As fc x as pat) = As fc x <$> act as <*> act pat
  go t@(TDelayed fc x y) = TDelayed fc x <$> act y
  go t@(TDelay fc x ty arg) = TDelay fc x <$> act ty <*> act arg
  go t@(TForce fc x y) = pure t
  go t@(PrimVal fc c) = pure t
  go t@(Erased fc imp) = pure t
  go t@(TType fc u) = pure t


text:
even'' : Nat -> Bool
even'' Z = True
even'' (S k) = ?even_rhs

-- :t even_rhs
-- k : Nat
--------------
-- even_rhs : Bool

main : IO ()
main = putStrLn ?greeting

-- :l hole
-- :t greeting
--------------
-- greeting : String

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
module Sub03Apply54x30

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(18x+10) --A[6,-4]->C[4,-4]--> 3(8x+3)
ac54x30To24x9 :
  (l:Nat) -> P (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) 2
    -> P (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) 2
ac54x30To24x9 l prf =
  let prf2 = lvDown (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) 2
                    prf in
    let prf3 = ac54x30To24x9' l prf2 in lvDown (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) 3 prf3

export
apply54x30 : P (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))),
         P m 2))
apply54x30 {l} col = let col2 = ac54x30To24x9 l col in ((S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) ** (lte54x30 l, col2)) where
  lte54x30 : (l:Nat) -> LTE (S (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))
                            (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                           (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))
  lte54x30 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte54x30 (S k) = let lemma = lte54x30 k in
    rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (S (S (plus (plus k k) (plus k k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (S (plus (plus k k) (plus k k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (plus (plus k k) (plus k k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (plus (plus k k) (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) k)) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (plus (plus k k) k)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


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

%access export

public export
data RTy = FUNC | USAB | RELI | PERF | SUPP

implementation Cast RTy String where
  cast FUNC = "functional"
  cast USAB = "usability"
  cast RELI = "reliability"
  cast PERF = "performance"
  cast SUPP = "supportability"

implementation Show RTy where
  show FUNC = "FUNC"
  show USAB = "USAB"
  show RELI = "RELI"
  show PERF = "PERF"
  show SUPP = "SUPP"

readRTy : String -> Maybe RTy
readRTy s =
  case s of
    "functional"     => Just FUNC
    "usability"      => Just USAB
    "reliability"    => Just RELI
    "performance"    => Just PERF
    "supportability" => Just SUPP
    otherwise        => Nothing

public export
data TTy = ADV  | DIS | GEN

implementation Show TTy where
  show ADV = "ADVANTAGE"
  show DIS = "DISADVANTAGE"
  show GEN = "GENERAL"

implementation Cast TTy String where
  cast ADV = "advantage"
  cast DIS = "disadvantage"
  cast GEN = "general"

readTTy : String -> Maybe TTy
readTTy s =
  case s of
    "advantage"    => Just ADV
    "disadvantage" => Just DIS
    "general"      => Just GEN
    otherwise      => Nothing

public export
data MTy = STRUCT | DYN

implementation Show MTy where
  show STRUCT = "STRUCT"
  show DYN    = "DYN"

implementation Cast MTy String where
  cast STRUCT = "structure"
  cast DYN    = "dynamic"

readMTy : String -> Maybe MTy
readMTy s =
  case s of
    "structure" => Just STRUCT
    "dynamic"   => Just DYN
    otherwise   => Nothing

public export
data LTy = SPECIAL | IMPL | USES | LINK

implementation Show LTy where
  show SPECIAL = "SPECIAL"
  show IMPL    = "IMPL"
  show USES    = "USES"
  show LINK    = "LINK"

public export
implementation Cast LTy String where
  cast SPECIAL = "specialises"
  cast IMPL    = "implements"
  cast USES    = "requires"
  cast LINK    = "linked"

readLTy : String -> Maybe LTy
readLTy s =
  case s of
    "specialises" => Just SPECIAL
    "implements"  => Just IMPL
    "requires"    => Just USES
    "linked"      => Just LINK
    otherwise     => Nothing

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module Minecraft.Client.Main

import Minecraft.Base.PreClassic
import Minecraft.Core.Univ.Level

%default total

public export
it : As Item
it = new Stone.Item MkItem

public export
blk : As Tangible
blk = case castApp Put it putItem of
  Just blk' => blk'
  Nothing   => believe_me ()

public export
es : Maybe (List (As Entity))
es = castApp Break blk breakBlk

public export
e : As Entity
e = case es of
  Just (x :: xs) => x
  _ => believe_me ()

public export
it' : As Item
it' = case castApp Pickup e collect of
  Just x  => x
  Nothing => believe_me "nothing"

public export
b1 : As Block
b1 = new Cobblestone.Block MkBlock

public export
b2 : As Block
b2 = new Cobblestone.Block MkBlock

public export
main : IO ()
main = do
  pure ()

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- ------------------------------------------------------ [ Commands.idr<Test> ]
-- Module    : Commands.idr<Test>
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Test.Commands

import Lightyear
import Lightyear.Strings

import Sif.Parser.Common
import Sif.Parser.Utils

import Sif.Pattern
import Sif.Commands

import Test.Utils
import Test.Parsing

testChkPattern : IO ()
testChkPattern = do
    parseTestG (Just "Parse :chkPattern") cmd
        ":chkPattern \"problem.p.sif\" \"solution.s.sif\""
        (CheckExtPattern "problem.p.sif" "solution.s.sif")
        (==)

testHelp : IO ()
testHelp = do
  putStrLn $ heading "Testing Help Command"
  parseTestG Nothing cmd ":?"    (Help) (==)
  parseTestG Nothing cmd ":help" (Help) (==)

testEvalPatt : IO ()
testEvalPatt = do
  putStrLn $ heading "Testing Eval Pattern"
  parseTestG Nothing cmd ":eval 1" (EvalPattern 1) (==)

testQuit : IO ()
testQuit = do
  putStrLn $ heading "Testing Quit Command"
  parseTestG Nothing cmd ":q" (Quit) (==)
  parseTestG Nothing cmd ":quit" (Quit) (==)
  parseTestG Nothing cmd ":exit" (Quit) (==)

testSave : IO ()
testSave = do
  putStrLn $ heading "Testing Save Command"
  parseTestB Nothing cmd ":saveAs 1 grl"
  parseTestG Nothing cmd
      ":saveAs 1 grl pattern.grl"
      (ShowPattern 1 (Just API.GRL) (Just "pattern.grl")) (==)

testList : IO ()
testList = do
  putStrLn $ heading "Testing List Command"
  parseTestG Nothing cmd ":list" (ListLib) (==)

testShow : IO ()
testShow = do
  putStrLn $ heading "Testing Show"
  parseTestG Nothing cmd ":show 2" (ShowPattern (S (S Z)) Nothing Nothing) (==)
  parseTestG Nothing cmd ":showAs 2 xml"
      (ShowPattern 2 (Just API.XML) Nothing)
      (==)

export
runTests : IO ()
runTests = do
  putStrLn $ heading "Testing Command Parsing"
  testChkPattern
  testQuit
  testHelp
  testEvalPatt
  testSave
  testList
  testShow

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module ParseIntegerList

import Oyster.Core

nats : Parser (List Int)
nats = do symbol "["
          d <- integer
          ds <- many (do symbol "," ; integer)
          symbol "]"
          pure (d :: ds)

partial
main : IO ()
main =  do input <- getLine
           printLn (parse nats input)

max_stars_repo_name: timmyjose-compilers/oyster

max_issues_repo_name: timmyjose-compilers/oyster

max_forks_repo_name: timmyjose-compilers/oyster


text:
module Minecraft.Base.PreClassic.Cobblestone.Item.Export

import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Base.PreClassic.Cobblestone.Block
import public Minecraft.Base.PreClassic.Cobblestone.Item
import public Minecraft.Base.PreClassic.Cobblestone.ItemEntity

%default total

[cobblestoneItem']
Item Cobblestone.Item where
  id = "minecraft:cobblestone"
  stackable = Just 64
  givenName = \x => x.base.givenName
  proj = \x => new Cobblestone.ItemEntity Cobblestone.MkItemEntity

[putCobblestone']
Put Cobblestone.Item where
  putItem self = new Cobblestone.Block Cobblestone.MkBlock

[cobblestoneVtbl']
Vtbl Cobblestone.Item where
  vtable (Item Cobblestone.Item) = Just cobblestoneItem
  vtable (Put  Cobblestone.Item) = Just putCobblestone
  vtable _ = Nothing

cobblestoneItem = cobblestoneItem'
putCobblestone  = putCobblestone'
cobblestoneVtbl = cobblestoneVtbl'


text:
record Foo where
  constructor MkFoo
  a : Nat
  b : Nat

foo1 : Foo
foo1 = MkFoo
  { a = 1
  , a = 2
  , b = 3
  }

foo2 : Foo
foo2 =
  { a := 3
  , a := 4
  , b := 2
  , b := 1
  } foo1


text:
printRange : (t : Type) -> (Show t, Num t, Enum t) => IO ()
printRange t = do printLn [(the t 1)..10]
                  printLn [(the t 10),9..1]
                  printLn (take 10 [(the t 1)..])
                  printLn (take 10 [(the t 1),3..])

main : IO ()
main = do printRange Nat
          printRange Int
          printRange Integer

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Tuple

Tup: Nat -> Type
Tup Z = Unit
Tup (S k) = (Nat, Tup k)

ct: (n: Nat) -> Tup n
ct Z = ()
ct (S k) = (S k, ct k)