text:
module Main

%default total

-- Data type

data BF : Char -> Type where
  Next : BF '>'
  Prev : BF '<'
  Increment : BF '+'
  Decrement : BF '-'
  Output : BF '.'
  Accept : BF ','
  Forward : BF '['
  Backward : BF ']'

-- Interpreter

data Tape a = MkTape (Stream a) a (Stream a)

right : Tape a -> Tape a
right (MkTape ls c (r :: rs)) = MkTape (c :: ls) r rs

left : Tape a -> Tape a
left (MkTape (l :: ls) c rs) = MkTape ls l (c :: rs)

emptyTape : Tape Int
emptyTape = MkTape (repeat 0) 0 (repeat 0)

Instruction : Type
Instruction = Maybe (Sigma Char BF)

mutual
  partial
  nextInstruction : Tape Int -> Tape Instruction -> IO ()
  nextInstruction dat ins = bf' dat (right ins)

  partial
  runInstruction : Tape Int -> Tape Instruction -> BF c -> IO ()

  runInstruction dat ins Next =
    nextInstruction (right dat) ins

  runInstruction dat ins Prev =
    nextInstruction (left  dat) ins

  runInstruction (MkTape ls c rs) ins Increment =
    nextInstruction (MkTape ls (succ c) rs) ins

  runInstruction (MkTape ls c rs) ins Decrement =
    nextInstruction (MkTape ls (pred c) rs) ins

  runInstruction dat@(MkTape _ c _) ins Output = do
    putChar (chr c)
    nextInstruction dat ins

  runInstruction (MkTape ls _ rs) ins Access = do
    c <- getChar
    nextInstruction (MkTape ls (ord c) rs) ins

  runInstruction dat@(MkTape _ n _) ins Forward = do
    if n == 0
    then loopRight Z dat ins
    else nextInstruction dat ins

  runInstruction dat@(MkTape _ n _) ins Backward = do
    if n /= 0
    then loopLeft Z dat ins
    else nextInstruction dat ins

  runInstruction dat ins _ =
    nextInstruction dat ins

  partial
  loopRight' : Nat -> Tape Int -> Tape Instruction -> BF c -> IO ()
  loopRight' (S Z) dat ins Backward =
    nextInstruction dat ins
  loopRight' n dat ins Backward =
    loopRight (pred n) dat (right ins)
  loopRight' n dat ins Forward =
    loopRight (succ n) dat (right ins)
  loopRight' n dat ins _ =
    loopRight n dat (right ins)

  partial
  loopRight : Nat -> Tape Int -> Tape Instruction -> IO ()
  loopRight n dat ins@(MkTape _ (Just p) _) =
    loopRight' n dat ins (getProof p)
  loopRight n dat ins =
    loopRight n dat (right ins)

  partial
  loopLeft' : Nat -> Tape Int -> Tape Instruction -> BF c -> IO ()
  loopLeft' (S Z) dat ins Forward =
    nextInstruction dat ins
  loopLeft' n dat ins Forward =
    loopLeft (pred n) dat (left ins)
  loopLeft' n dat ins Backward =
    loopLeft (succ n) dat (left ins)
  loopLeft' n dat ins _ =
    loopLeft n dat (left ins)

  partial
  loopLeft : Nat -> Tape Int -> Tape Instruction -> IO ()
  loopLeft n dat ins@(MkTape _ (Just p) _) =
    loopLeft' n dat ins (getProof p)
  loopLeft n dat ins =
    loopLeft n dat (left ins)

  partial
  bf' : Tape Int -> Tape Instruction -> IO ()
  bf' _     (MkTape _ Nothing  _) = return ()
  bf' dat ins@(MkTape _ (Just p) _) = runInstruction dat ins (getProof p)

-- Literals

data Every : List a -> Type where

partial
bf : (s : String) -> { auto p : Every (unpack s) } -> IO ()

partial
main : IO ()
main = do
  bf"++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-."


text:
module Control.Monad.RWS.Interface

import Control.Monad.RWS.CPS
import Control.Monad.Reader.Interface
import Control.Monad.State.Interface
import Control.Monad.Writer.Interface

%default total

public export
interface (MonadReader r m, MonadWriter w m, MonadState s m) =>
  MonadRWS r w s m | m where

public export
(Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where

ext: idr


text:
||| An interactive data store.
module Main

import Control.Arrow
import Control.Category
import Data.Morphisms
import Data.Vect

%access export

-- ---------------------------------------- [ Exercise 6.3.1 // Revised 10.3.2 ]

infixr 5 .+.

public export
data Schema = ||| A schema containing a single character.
              SChar
            | ||| A schema containing a single string.
              SString
            | ||| A schema containing a single integer.
              SInt
            | ||| A schema combining two smaller schemas.
              (.+.) Schema Schema

||| Convert a schema to a concrete type.
public export
SchemaType : Schema -> Type
SchemaType SChar     = Char
SchemaType SString   = String
SchemaType SInt      = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

||| A sized data store for strings, referable by numeric identifier.
record DataStore (schema : Schema) where
  constructor MkData
  ||| The number or stored items.
  size : Nat                    -- N.B. This covers Exercise 4.3.5.1.
  ||| The contents of the store.
  items : Vect size (SchemaType schema)

%name DataStore store

empty : DataStore schema
empty = MkData 0 []

||| Add an item to a data store.
||| @ item  the item to add.
||| @ store the store to add to.
addToStore : (item : SchemaType schema) -> (store : DataStore schema) ->
             DataStore schema
addToStore item (MkData _ items) = MkData _ (item :: items)

-- ------------------------------------------------------------------ [ 10.3.3 ]

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

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

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

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

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

||| An data store command.
data Command : Schema -> Type where
   -- ||| Set the schema.
   -- ||| @ newschema the schema to set.
   -- SetSchema : (newschema : Schema)            -> Command schema
   ||| Add an item.
   ||| @ item an item to add.
   Add : (item : SchemaType schema) -> Command schema
   ||| Get an item by ID.
   ||| @ id an ID to look up.
   Get : (id : Integer) -> Command schema
   ||| Search the data store for entries containing a substring.
   ||| @ query a substring to match.
   Search : (query : String) -> Command schema
   ||| Quit the REPL.
   Quit : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SChar input with (unpack input)
  | ('\'' :: xs) with (span (/= '\'') xs)
    | ([char], '\'' :: rest) = Just (char, ltrim (pack rest))
    | _ = Nothing
  | _ = Nothing
parsePrefix SString input with (unpack input)
  | ('"' :: xs) with (span (/= '"') xs)
    | (quoted, '"' :: rest) = Just (pack quoted, ltrim (pack rest))
    | _                     = Nothing
  | _ = Nothing
parsePrefix SInt    input with (span isDigit input)
  | ("",  rest) = Nothing
  | (num, rest) = Just (cast num, ltrim rest)
parsePrefix (schemaL .+. schemaR) input = do
  (left,  input')  <- parsePrefix schemaL input
  (right, input'') <- parsePrefix schemaR input'
  pure ((left, right), input'')

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input with (parsePrefix schema input)
  | Just (res, "") = Just res
  | Just _         = Nothing
  | Nothing        = Nothing

parseSchema : List String -> Maybe Schema
parseSchema ("Char"   :: []) = Just  SChar
parseSchema ("Char"   :: xs) = Just (SChar .+.) <*> parseSchema xs
parseSchema ("String" :: []) = Just  SString
parseSchema ("String" :: xs) = Just (SString .+.) <*> parseSchema xs
parseSchema ("Int"    :: []) = Just  SInt
parseSchema ("Int"    :: xs) = Just (SInt    .+.) <*> parseSchema xs
parseSchema _ = Nothing

||| Parse a command from the interactive prompt.
||| @ cmd  a string to attempt to parse as a command.
||| @ args arguments to pass to a parsed command.
parseCommand : (schema : Schema) -> (cmd, args : String) ->
               Maybe (Command schema)
parseCommand schema "add" str      = pure Add <*> parseBySchema schema str
parseCommand schema "get" val      = if all isDigit (unpack val)
                                        then Just $ Get (cast val)
                                        else Nothing
parseCommand schema "search" ""    = Nothing
parseCommand schema "search" query = Just (Search query)
parseCommand schema "quit" _       = Just Quit
{-
parseCommand schema "schema" rest  = pure SetSchema <*> parseSchema (words rest)
-}
parseCommand _ _ _                 = Nothing

||| Attempt to parse a string as a command.
||| @ schema the schema of a data store.
||| @ input  a string to attempt to parse.
parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input with (span (/= ' ') input)
  | (cmd, args) = parseCommand schema cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SChar} item       = show item
display {schema = SString} item     = show item
display {schema = SInt} item        = show item
display {schema = (x .+. y)} (a, b) = display a ++ ", " ++ display b

||| Add an item to a data store and return a REPL response.
||| @ item  an item to add.
||| @ store a store to add to.
addItem : (item : SchemaType schema) -> (store : DataStore schema) ->
          Maybe (String, DataStore schema)
addItem item store =
  Just ("ID " ++ show (size store) ++ "\n", addToStore item store)

||| Get an entry from a data store by ID and return a REPL response.
||| @ id    an ID to look up.
||| @ store a store possibly containing a matching entry.
getEntry : (id : Integer) -> (store : DataStore schema) ->
           Maybe (String, DataStore schema)
getEntry id store with (integerToFin id (size store))
  | Nothing = Just ("Out of range\n", store)
  | Just i  = Just (display (index i (items store)) ++ "\n", store)

-- -------------------------------------------------------- [ Exercise 6.3.8.2 ]

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

||| Pretty print all entries in a data store and return a REPL response.
||| @ store a data store whose entries to pretty print
getAllEntries : (store : DataStore schema) -> Maybe (String, DataStore schema)
getAllEntries store@(MkData Z []) = Just ("No entries\n", store)
getAllEntries store = Just (unlines (reverse (go 0 (showItems store))), store)
  where
    go : Nat -> List (SchemaType schema) -> List String
    go _ []      = []
    go n (x::xs) = (show n ++ " => " ++ display x) :: (go (S n) xs)

-- --------------------------------------------------------- [ Exercise 10.3.4 ]

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

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

doSearch : (query : String) -> (store : Vect n (SchemaType schema)) ->
           List (Nat, String)
doSearch query [] = []
doSearch query (item :: items) =
  let matches = go <$> doSearch query items
      itemStr = display item in
      if query `isInfixOf` toLower itemStr
         then (0,itemStr) :: matches
         else matches
  where
    go = applyMor $ first (arrow S)

search : (query : String) -> (store : DataStore schema) ->
         Maybe (String, DataStore schema)
search query store with (doSearch query (items store))
  | []      = Just ("Not found\n", store)
  | matches = Just (unwords (map format matches) ++ "\n", store)
      where format (k,x) = "(" ++ show k ++ ", " ++ x ++ ")"

{-
setSchema : (schema' : Schema) -> (store : DataStore schema) ->
            Maybe (DataStore schema')
setSchema _ (MkData Z _) = Just (MkData _ [])
setSchema _ _            = Nothing
-}

||| Process user input from the REPL.
||| @ store a data store
||| @ input a user-entered string, possibly representing a valid command.
processInput : (store : DataStore schema) -> (input : String) ->
               Maybe (String, DataStore schema)
-- FIXME: This is smelly, but gets the job done.
processInput store "get" = getAllEntries store
processInput {schema} store input with (parse schema input)
  | Nothing              = Just ("Invalid command\n", store)
  | Just (Add item)      = addItem item store
  | Just (Get id)        = getEntry id store
  | Just (Search query)  = search (toLower query) store
  -- | Just (SetSchema schema') =
  --     (pure (MkPair "OK\n") <*> setSchema schema' store) <|>
  --      pure ("Can't update schema\n", store)
  | Just Quit                = Nothing

||| Run a REPL, processing commands and maintaing a data store.
partial
main : IO ()
main = replWith (the (DataStore (SString .+. SString .+. SInt)) empty)
                "> " processInput

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Main

import NBody
import Data.Vect
import System
import Prelude.Providers
import Data.String

main : IO ()
main = nbodyFunc

max_stars_repo_name: jappeace/idris-age-of-conquerors

max_issues_repo_name: jappeace/idris-age-of-conquerors

max_forks_repo_name: jappeace/idris-age-of-conquerors


text:
module Data.Profunctor.Class

import Data.Morphisms

public export
interface Profunctor (0 p : Type -> Type -> Type) where
  dimap : (a -> b) -> (c -> d) -> p b c -> p a d
  dimap f g = lmap f . rmap g

  lmap : (a -> b) -> p b c -> p a c
  lmap f = dimap f id

  rmap : (c -> d) -> p b c -> p b d
  rmap f = dimap id f

public export
Profunctor Morphism where
  dimap f g (Mor h) = Mor (g . h . f)

  lmap f (Mor h) = Mor (h . f)

  rmap g (Mor h) = Mor (g . h)


text:
module Text.PrettyPrint.Leijen.Test

import System

import Text.PrettyPrint.Leijen

%default total

--%access private

data SExpr = Symbol String
           | Cons SExpr SExpr
           | Nil
           | IntLit Int

consp : SExpr -> Bool
consp (Cons _ _) = True
consp _ = False

mutual
  pprint : SExpr -> Doc
  pprint (Symbol str) = text str
  pprint (IntLit i)   = text (show i)
  pprint (Cons x y)   = enclose lparen rparen (align $ listContents x y)
  pprint Nil          = lparen |+| rparen

  listContents : SExpr -> SExpr -> Doc
  listContents car Nil = pprint car
  listContents car (Symbol str) = pprint car |++| dot |++| pprint (Symbol str)
  listContents car (IntLit i) = pprint car |++| dot |++| pprint (IntLit i)
  listContents car (Cons cadr cddr) = group $ pprint car |$| listContents cadr cddr

implicit
fromList : List SExpr -> SExpr
fromList = foldr Cons Nil

implicit
fromString : String -> SExpr
fromString x = Symbol x

omega : SExpr
omega = [["lambda", ["f"], ["f", "f"]], ["lambda", ["f"], ["f", "f"]]]

covering
test : Int -> SimpleDoc
test w = renderPretty 0.8 w (pprint omega)

covering
test1 : String
test1 = displayS (test 80) ""

covering
test2 : String
test2 = displayS (test 40) ""

covering
test3 : String
test3 = displayS (test 20) ""

covering
test4 : String
test4 = displayS (test 10) ""

doTest : String -> String -> IO ()
doTest output expected =
  if output == expected
    then putStrLn "ok"
    else do putStrLn $ "Expected: " ++ expected
            putStrLn $ "Got: " ++ output
            exit 1

covering
runTest : IO ()
runTest = traverse_ (uncurry doTest)
            [ (test1, "((lambda (f) (f f)) (lambda (f) (f f)))")
            , (test2, "((lambda (f) (f f))\n (lambda (f) (f f)))")
            , (test3, "((lambda\n  (f) (f f))\n (lambda\n  (f) (f f)))")
            , (test4, "((lambda\n  (f)\n  (f f))\n (lambda\n  (f)\n  (f f)))")
            ]

max_stars_repo_name: HuwCampbell/wl-pprint

max_issues_repo_name: HuwCampbell/wl-pprint

max_forks_repo_name: HuwCampbell/wl-pprint


text:
module Test.Suite

import IdrTest.Test

import Test.Toml.DataTest
import Test.Toml.LexerTest
import Test.TomlTest

suite : IO ()
suite = do
  runSuites
    [ Test.Toml.LexerTest.suite
    , Test.Toml.DataTest.suite
    , Test.TomlTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Uri

import Uri.Parser
import Uri.Types
import Debug.Time

public export
decodeRelativeURI : String -> Maybe RelativeURI
decodeRelativeURI str =
    case run parseRelativeURI (0, str) of
        Right (uri, pos) => Just uri
        Left err => Nothing

public export
decodeURI : String -> Maybe URI
decodeURI str =
    case run parseURI (0, str) of
        Right (uri, pos) => Just uri
        Left err => Nothing

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


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

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

%default total

[cobblestoneItemEntity']
Pickup Cobblestone.ItemEntity where
  collect self = new Cobblestone.Item self.base.item

[cobblestoneVtbl']
Vtbl Cobblestone.ItemEntity where
  vtable (Pickup   Cobblestone.ItemEntity) = Just cobblestoneItemEntity
  vtable (Entity   Cobblestone.ItemEntity) = Just %search
  vtable (Tangible Cobblestone.ItemEntity) = Just %search
  vtable _ = Nothing

cobblestoneItemEntity = cobblestoneItemEntity'
cobblestoneVtbl = cobblestoneVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Average

export
average : String -> Double
average str = let numWords = wordCount str
                  totalLength = sum (allLengths (words str)) in
			      cast totalLength / cast numWords
	where
		wordCount: String -> Nat
		wordCount str = length (words str)

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

add : Int -> Int -> Int
add x y = x + y

identity: ty -> ty
identity x = x

double: Num ty => ty -> ty
double x = x + x

twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape

quadruple : Num a => a -> a
quadruple = twice double

turn_around : Shape -> Shape
turn_around = twice rotate

longer : String -> String -> String
longer word1 word2
	= let len1 = length word1
	      len2 = length word2 in
              if len1 > len2 then word1 else word2

pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (square x + square y)
  where
    square: Double -> Double
    square x = x * x

wordCount : String -> Nat
wordCount str = length (words str)

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

-- single line comment

{-
Multiple
Line
Comment
-}


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Applicative
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Prism
import Control.Lens.Types
import Control.Monad.Identity
import Data.Profunctor

%default total
%access public export

||| Create a `Prism`
prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
prism bt seta = dimap seta (either pure (map bt)) . right'

prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' bs sma = prism bs (\s => maybe (Left s) Right (sma s))

_Left : Prism (Either a c) (Either b c) a b
_Left = prism Left $ either Right (Left . Right)

_Right : Prism (Either c a) (Either c b) a b
_Right = prism Right $ either (Left . Left) Right

_Just : Prism (Maybe a) (Maybe b) a b
_Just = prism Just $ maybe (Left Nothing) Right

_Nothing : Prism' (Maybe a) ()
_Nothing = prism' (const Nothing) $ maybe (Just ()) (const Nothing)

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

max_stars_repo_name: andrevidela/idris-lens

max_issues_repo_name: andrevidela/idris-lens

max_forks_repo_name: andrevidela/idris-lens


text:
module Parser.Lexer.Source

import public Parser.Lexer.Common

import Data.List1
import Data.List
import Data.Maybe
import Data.String
import Libraries.Data.String.Extra
import public Libraries.Text.Bounded
import Libraries.Text.Lexer.Tokenizer
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util

import Libraries.Utils.Hex
import Libraries.Utils.Octal
import Libraries.Utils.String

import Core.Name

%default total

public export
data IsMultiline = Multi | Single

public export
data Token
  -- Literals
  = CharLit String
  | DoubleLit Double
  | IntegerLit Integer
  -- String
  | StringBegin IsMultiline -- Whether is multiline string
  | StringEnd
  | InterpBegin
  | InterpEnd
  | StringLit Nat String
  -- Identifiers
  | HoleIdent String
  | Ident String
  | DotSepIdent Namespace String -- ident.ident
  | DotIdent String               -- .ident
  | Symbol String
  -- Comments
  | Comment
  | DocComment String
  -- Special
  | CGDirective String
  | EndInput
  | Keyword String
  | Pragma String
  | Unrecognised String

export
Show Token where
  -- Literals
  show (CharLit x) = "character " ++ show x
  show (DoubleLit x) = "double " ++ show x
  show (IntegerLit x) = "literal " ++ show x
  -- String
  show (StringBegin Single) = "string begin"
  show (StringBegin Multi) = "multiline string begin"
  show StringEnd = "string end"
  show InterpBegin = "string interp begin"
  show InterpEnd = "string interp end"
  show (StringLit n x) = "string" ++ Extra.replicate n '#' ++ " " ++ show x
  -- Identifiers
  show (HoleIdent x) = "hole identifier " ++ x
  show (Ident x) = "identifier " ++ x
  show (DotSepIdent ns n) = "namespaced identifier " ++ show ns ++ "." ++ show n
  show (DotIdent x) = "dot+identifier " ++ x
  show (Symbol x) = "symbol " ++ x
  -- Comments
  show Comment = "comment"
  show (DocComment c) = "doc comment: \"" ++ c ++ "\""
  -- Special
  show (CGDirective x) = "CGDirective " ++ x
  show EndInput = "end of input"
  show (Keyword x) = x
  show (Pragma x) = "pragma " ++ x
  show (Unrecognised x) = "Unrecognised " ++ x

export
Pretty Token where
  -- Literals
  pretty (CharLit x) = pretty "character" <++> squotes (pretty x)
  pretty (DoubleLit x) = pretty "double" <++> pretty x
  pretty (IntegerLit x) = pretty "literal" <++> pretty x
  -- String
  pretty (StringBegin Single) = reflow "string begin"
  pretty (StringBegin Multi) = reflow "multiline string begin"
  pretty StringEnd = reflow "string end"
  pretty InterpBegin = reflow "string interp begin"
  pretty InterpEnd = reflow "string interp end"
  pretty (StringLit n x) = pretty ("string" ++ Extra.replicate n '#') <++> dquotes (pretty x)
  -- Identifiers
  pretty (HoleIdent x) = reflow "hole identifier" <++> pretty x
  pretty (Ident x) = pretty "identifier" <++> pretty x
  pretty (DotSepIdent ns n) = reflow "namespaced identifier" <++> pretty ns <+> dot <+> pretty n
  pretty (DotIdent x) = pretty "dot+identifier" <++> pretty x
  pretty (Symbol x) = pretty "symbol" <++> pretty x
  -- Comments
  pretty Comment = pretty "comment"
  pretty (DocComment c) = reflow "doc comment:" <++> dquotes (pretty c)
  -- Special
  pretty (CGDirective x) = pretty "CGDirective" <++> pretty x
  pretty EndInput = reflow "end of input"
  pretty (Keyword x) = pretty x
  pretty (Pragma x) = pretty "pragma" <++> pretty x
  pretty (Unrecognised x) = pretty "Unrecognised" <++> pretty x

mutual
  ||| The mutually defined functions represent different states in a
  ||| small automaton.
  ||| `toEndComment` is the default state and it will munch through
  ||| the input until we detect a special character (a dash, an
  ||| opening brace, or a double quote) and then switch to the
  ||| appropriate state.
  toEndComment : (k : Nat) -> Recognise (k /= 0)
  toEndComment Z = empty
  toEndComment (S k)
               = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
                        <+> toEndComment (S k)
             <|> is '{' <+> singleBrace k
             <|> is '-' <+> singleDash k
             <|> stringLit <+> toEndComment (S k)

  ||| After reading a single brace, we may either finish reading an
  ||| opening delimiter or ignore it (e.g. it could be an implicit
  ||| binder).
  singleBrace : (k : Nat) -> Lexer
  singleBrace k
     =  is '-' <+> many (is '-')    -- opening delimiter
               <+> singleDash (S k) -- handles the {----} special case
    <|> toEndComment (S k)          -- not a valid comment

  ||| After reading a single dash, we may either find another one,
  ||| meaning we may have started reading a line comment, or find
  ||| a closing brace meaning we have found a closing delimiter.
  singleDash : (k : Nat) -> Lexer
  singleDash k
     =  is '-' <+> doubleDash k    -- comment or closing delimiter
    <|> is '}' <+> toEndComment k  -- closing delimiter
    <|> toEndComment (S k)         -- not a valid comment

  ||| After reading a double dash, we are potentially reading a line
  ||| comment unless the series of uninterrupted dashes is ended with
  ||| a closing brace in which case it is a closing delimiter.
  doubleDash : (k : Nat) -> Lexer
  doubleDash k = with Prelude.(::)
      many (is '-') <+> choice            -- absorb all dashes
        [ is '}' <+> toEndComment k                      -- closing delimiter
        , many (isNot '\n') <+> toEndComment (S k)       -- line comment
        ]

blockComment : Lexer
blockComment = is '{' <+> is '-' <+> toEndComment 1

docComment : Lexer
docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n')

holeIdent : Lexer
holeIdent = is '?' <+> identNormal

dotIdent : Lexer
dotIdent = is '.' <+> identNormal

pragma : Lexer
pragma = is '%' <+> identNormal

doubleLit : Lexer
doubleLit
    = digits <+> is '.' <+> digits <+> opt
           (is 'e' <+> opt (is '-' <|> is '+') <+> digits)

stringBegin : Lexer
stringBegin = many (is '#') <+> (is '"')

stringEnd : Nat -> String
stringEnd hashtag = "\"" ++ Extra.replicate hashtag '#'

multilineBegin : Lexer
multilineBegin = many (is '#') <+> (exact "\"\"\"") <+>
                    manyUntil newline space <+> newline

multilineEnd : Nat -> String
multilineEnd hashtag = "\"\"\"" ++ Extra.replicate hashtag '#'

-- Do this as an entire token, because the contents will be processed by
-- a specific back end
cgDirective : Lexer
cgDirective
    = exact "%cg" <+>
      ((some space <+>
           some (pred isAlphaNum) <+> many space <+>
           is '{' <+> many (isNot '}') <+>
           is '}')
         <|> many (isNot '\n'))

mkDirective : String -> Token
mkDirective str = CGDirective (trim (substr 3 (length str) str))

-- Reserved words
keywords : List String
keywords = ["data", "module", "where", "let", "in", "do", "record",
            "auto", "default", "implicit", "mutual", "namespace",
            "parameters", "with", "proof", "impossible", "case", "of",
            "if", "then", "else", "forall", "rewrite",
            "using", "interface", "implementation", "open", "import",
            "public", "export", "private",
            "infixl", "infixr", "infix", "prefix",
            "total", "partial", "covering"]

-- Reserved words for internal syntax
special : List String
special = ["%lam", "%pi", "%imppi", "%let"]

export
symbols : List String
symbols = [",", ";", "_", "`"]

export
groupSymbols : List String
groupSymbols = [".(", -- for things such as Foo.Bar.(+)
    "@{", "[|", "(", "{", "[<", "[>", "[", "`(", "`{", "`["]

export
groupClose : String -> String
groupClose ".(" = ")"
groupClose "@{" = "}"
groupClose "[|" = "|]"
groupClose "(" = ")"
groupClose "[" = "]"
groupClose "[<" = "]"
groupClose "[>" = "]"
groupClose "{" = "}"
groupClose "`(" = ")"
groupClose "`{" = "}"
groupClose "`[" = "]"
groupClose _ = ""

export
isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")

export
||| Test whether a user name begins with an operator symbol.
isOpUserName : UserName -> Bool
isOpUserName (Basic n) = fromMaybe False $ do
   c <- fst <$> strUncons n
   guard (isOpChar c)
   pure True
isOpUserName (Field _) = False
isOpUserName Underscore = False

export
||| Test whether a name begins with an operator symbol.
isOpName : Name -> Bool
isOpName = maybe False isOpUserName . userNameRoot

validSymbol : Lexer
validSymbol = some (pred isOpChar)

-- Valid symbols which have a special meaning so can't be operators
export
reservedSymbols : List String
reservedSymbols
    = symbols ++ groupSymbols ++ (groupClose <$> groupSymbols) ++
      ["%", "\\", ":", "=", ":=", "|", "|||", "<-", "->", "=>", "?", "!",
       "&", "**", "..", "~", "@"]

fromBinLit : String -> Integer
fromBinLit str
    = if length str <= 2
         then 0
         else let num = assert_total (strTail (strTail str)) in
                fromBin . reverse . map castBin . unpack $ num
    where
      castBin : Char -> Integer
      castBin '1' = 1; castBin _ = 0 -- This can only be '1' and '0' once lexed
      fromBin : List Integer -> Integer
      fromBin [] = 0
      fromBin (0 :: xs) = 2 * fromBin xs
      fromBin (x :: xs) = x + (2 * fromBin xs)

fromHexLit : String -> Integer
fromHexLit str
  = if length str <= 2
       then 0
       else let num = assert_total (strTail (strTail str)) in
             fromMaybe 0 (fromHex (reverse num))
             --        ^-- can't happen if the literal was lexed correctly

fromOctLit : String -> Integer
fromOctLit str
  = if length str <= 2
       then 0
       else let num = assert_total (strTail (strTail str)) in
             fromMaybe 0 (fromOct (reverse num))
             --        ^-- can't happen if the literal lexed correctly

mutual
  stringTokens : Bool -> Nat -> Tokenizer Token
  stringTokens multi hashtag
      = let escapeChars = "\\" ++ Extra.replicate hashtag '#'
            interpStart = escapeChars ++ "{"
            escapeLexer = escape (exact escapeChars) any
            charLexer = non $ exact (if multi then multilineEnd hashtag else stringEnd hashtag)
          in
            match (someUntil (exact interpStart) (escapeLexer <|> charLexer)) (\x => StringLit hashtag x)
        <|> compose (exact interpStart)
                    (const InterpBegin)
                    (const ())
                    (\_ => rawTokens)
                    (const $ is '}')
                    (const InterpEnd)

  rawTokens : Tokenizer Token
  rawTokens =
          match comment (const Comment)
      <|> match blockComment (const Comment)
      <|> match docComment (DocComment . removeOptionalLeadingSpace . drop 3)
      <|> match cgDirective mkDirective
      <|> match holeIdent (\x => HoleIdent (assert_total (strTail x)))
      <|> compose (choice $ exact <$> groupSymbols)
                  Symbol
                  id
                  (\_ => rawTokens)
                  (exact . groupClose)
                  Symbol
      <|> match (choice $ exact <$> symbols) Symbol
      <|> match doubleLit (DoubleLit . cast)
      <|> match binUnderscoredLit (IntegerLit . fromBinLit . removeUnderscores)
      <|> match hexUnderscoredLit (IntegerLit . fromHexLit . removeUnderscores)
      <|> match octUnderscoredLit (IntegerLit . fromOctLit . removeUnderscores)
      <|> match digitsUnderscoredLit (IntegerLit . cast . removeUnderscores)
      <|> compose multilineBegin
                  (const $ StringBegin Multi)
                  countHashtag
                  (stringTokens True)
                  (exact . multilineEnd)
                  (const StringEnd)
      <|> compose stringBegin
                  (const $ StringBegin Single)
                  countHashtag
                  (stringTokens False)
                  (\hashtag => exact (stringEnd hashtag) <+> reject (is '"'))
                  (const StringEnd)
      <|> match charLit (CharLit . stripQuotes)
      <|> match dotIdent (\x => DotIdent (assert_total $ strTail x))
      <|> match namespacedIdent parseNamespace
      <|> match identNormal parseIdent
      <|> match pragma (\x => Pragma (assert_total $ strTail x))
      <|> match space (const Comment)
      <|> match validSymbol Symbol
      <|> match symbol Unrecognised
    where
      parseIdent : String -> Token
      parseIdent x = if x `elem` keywords then Keyword x
                     else Ident x

      parseNamespace : String -> Token
      parseNamespace ns = case mkNamespacedIdent ns of
                               (Nothing, ident) => parseIdent ident
                               (Just ns, n)     => DotSepIdent ns n

      countHashtag : String -> Nat
      countHashtag = count (== '#') . unpack

      removeOptionalLeadingSpace : String -> String
      removeOptionalLeadingSpace str = case strM str of
                                            StrCons ' ' tail => tail
                                            _ => str

      removeUnderscores : String -> String
      removeUnderscores s = fastPack $ filter (/= '_') (fastUnpack s)

export
lexTo : Lexer ->
        String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))
lexTo reject str
    = case lexTo reject rawTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
                                      [MkBounded EndInput False (MkBounds l c l c)])
           (_, fail) => Left fail
    where
      notComment : WithBounds Token -> Bool
      notComment t = case t.val of
                          Comment => False
                          _ => True

export
lex : String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))
lex = lexTo (pred $ const False)


text:
module Eval

import Effects
import Effect.Exception
import Effect.State
import Effect.StdIO

import Prelude.List as L
import Prelude.Bool as B

import Parser
import LispVal
import Utils

export
Prim : Type
Prim = List (String, LispVal)

Unary : Type
Unary = LispVal -> Eval LispVal

Binary : Type
Binary = LispVal -> LispVal -> Eval LispVal

binop : Binary -> List LispVal -> Eval LispVal
binop op args = case args of
                     [x, y] => op x y
                     _ => raise $ NumArgs 2 args

numOp : (Integer -> Integer -> Integer) -> LispVal -> LispVal -> Eval LispVal
numOp op (Number x) (Number y) = pure $ Number $ op x  y
numOp op (Number x) y          = raise $ TypeMismatch "Number" y
numOp op x          _          = raise $ TypeMismatch "Number" x

numBoolBinop : (Integer -> Integer -> B.Bool) -> LispVal -> LispVal -> Eval LispVal
numBoolBinop op (Number x) (Number y) = pure $ Bool $ op x  y
numBoolBinop op (Number x) y          = raise $ TypeMismatch "bool" y
numBoolBinop op x          _          = raise $ TypeMismatch "bool" x

-- todo: more ops
export
primEnv : Prim
primEnv = [ ("+", Fun $ MkFun $ binop $ numOp (+))
            , ("-", Fun $ MkFun $ binop $ numOp (-))
            , ("*", Fun $ MkFun $ binop $ numOp (*))
            , ("/", Fun $ MkFun $ binop $ numOp div)
            , ("mod", Fun $ MkFun $ binop $ numOp mod)
            , ("quotient", Fun $ MkFun $ binop $ numOp divBigInt)
            , ("remainder", Fun $ MkFun $ binop $ numOp modBigInt)
            , ("=", Fun $ MkFun $ binop $ numBoolBinop (==))
            , ("<", Fun $ MkFun $ binop $ numBoolBinop (<))
            , (">", Fun $ MkFun $ binop $ numBoolBinop (>))
            , ("/=", Fun $ MkFun $ binop $ numBoolBinop (/=))
            , (">=", Fun $ MkFun $ binop $ numBoolBinop (>=))
            , ("<=", Fun $ MkFun $ binop $ numBoolBinop (<=))]

mutate : String -> LispVal -> (String, LispVal) -> (String, LispVal)
mutate atom exp (a, b) = if a == atom
                         then (a, exp)
                         else (a, b)

addToEnv : String -> LispVal -> EnvCtx -> EnvCtx
addToEnv n v ls = (n, v) :: ls

mutual
  eval : LispVal -> Eval LispVal
  eval val@(Number n)  = pure val
  eval val@(Str s)     = pure val
  eval val@(Bool b)    = pure val
  eval (List Nil)      = pure Nil
  eval Nil             = pure Nil
  eval val@(Atom atom) = getVar val
  eval (List [Atom "quote", val]) = pure val
  eval (List [Atom "if", pred, conseq, alt]) = case !(eval pred) of
                                                    Bool False => eval alt
                                                    _  => eval conseq
  eval (List [Atom "def", (Atom val), exp]) = defineVar (Atom val) exp
  eval (List [Atom "define", (Atom val), exp]) = defineVar (Atom val) exp
  eval (List [Atom "lambda", params, exp]) = do p <- evalToList params
                                                pure $ Lambda (MkFun (\args => (evalArgsExpEnv args p exp))) !get
  eval (List [(Atom fn), a, b]) =
    do
      func <- getVar $ Atom fn
      case func of
           (Fun (MkFun f)) => f [!(eval a), !(eval b)]
           (Lambda (MkFun f) boundEnv) => do put boundEnv
                                             f [!(eval a), !(eval b)]
           _ => raise $ NotFunction "Unrecognized primitive function" $ show func
  eval somethingElse = raise $ Default $ "unmatched case " ++ show somethingElse

  evalArgsExpEnv : List LispVal -> List LispVal -> LispVal -> Eval LispVal
  evalArgsExpEnv args params exp =
    do bindVars $ zipWith MkPair params args
       eval exp

  setLocal : String -> LispVal -> EnvCtx -> Eval LispVal
  setLocal atom exp env = do update (addToEnv atom exp)
                             eval exp

  setVar : LispVal -> LispVal -> Eval LispVal
  setVar n@(Atom atom) exp = do env <- get
                                case lookup atom env of
                                     Just x => setLocal atom exp env
                                     Nothing => raise $ UnboundVar "unbound variable" n
  setVar _  exp = raise $ LispErr "variables can only be assigned to atoms"

  defineVar : LispVal -> LispVal -> Eval LispVal
  defineVar (Atom atom) exp = setLocal atom exp !get
  defineVar _  exp = raise $ LispErr "can only bind to Atom type valaues"

  getVar : LispVal -> Eval LispVal
  getVar n@(Atom atom) = case lookup atom !get of
                              Nothing => raise $ UnboundVar "unbound variable" n
                              Just val => pure val
  getVar _             = raise $ LispErr "variables can only be assigned to atoms"

  evalToList : LispVal -> Eval (L.List LispVal)
  evalToList expr =
    do
      val <- eval expr
      case val of
           List x => pure x
           _      => raise $ Default "error evaluating into list"

  cons : L.List LispVal -> Eval LispVal
  cons [x, y@(List _)] =
    do
      v <- eval x
      v' <- evalToList y
      pure $ List $ v :: v'
  cons [c] =
    do
      _ <- eval c
      pure $ List [c]
  cons []  = pure $ List []

  -- traverse
  traverse' : L.List LispVal -> Eff (List LispVal) [STATE EnvCtx, EXCEPTION LispError]
  traverse' [x]       = pure [x]
  traverse' (x :: xs) = do x' <- eval x
                           pure $ x' :: !(traverse' xs)
  traverse' []        = raise $ Default "empty body"

  uncurryDef : (LispVal, LispVal) -> Eval LispVal
  uncurryDef = uncurry defineVar

  bindVars : L.List (LispVal, LispVal) -> Eval ()
  bindVars [] = pure ()
  bindVars (x :: xs) =
    do uncurryDef x
       bindVars xs

-- end mutual

runParse_ : String -> Either LispError LispVal
runParse_ = mapLeft (\_ => Default "parser error") . readExpr

testEnv : EnvCtx
testEnv = ("x", Number 42) :: primEnv

textToEval : String -> Eval LispVal
textToEval input =
  case runParse_ input of
       Right val => eval val
       Left err  => raise $ err

runApp : EnvCtx -> Eval b -> Eff (EnvCtx, b) [STATE EnvCtx, STDIO, EXCEPTION LispError]
runApp code action =
  do
    put code
    v <- action
    pure (!get, v)

-- fix me
export
evalExpr : EnvCtx -> String -> IO EnvCtx
evalExpr env expr =
  do
    case the (Either LispError LispVal) $ runInit (env :: () :: []) $ textToEval expr of
      Left err => do putStrLn $ show err
                     pure $ env
      Right val => do (e, v) <- run $ runApp env $ textToEval expr
                      putStrLn $ show v
                      pure $ e


text:
import Control.Monad.State

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

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

testStream : Stream Int
testStream = [1..]

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

labelTreeWith : Stream label -> Tree elem -> (Stream label, Tree (label, elem))
labelTreeWith lbls Empty        = (lbls, Empty)
labelTreeWith lbls (Node l e r) =
  let
    (forThis :: forRight, lbldLeft) = labelTreeWith lbls l
    (forNext, lbldRight) = labelTreeWith forRight r
  in
    (forNext, Node lbldLeft (forThis, e) lbldRight)

labelTreeWith2 : Tree a -> State (Stream label) (Tree (label, a))
labelTreeWith2 Empty                  = pure Empty
labelTreeWith2 (Node left elem right) =
  do
    lbldLeft <- labelTreeWith2 left
    (this :: rest) <- get
    put rest
    lbldRight <- labelTreeWith2 right
    pure (Node lbldLeft (this, elem) lbldRight)

deepFirst : Tree elem -> Tree (Int, elem)
deepFirst tree = snd (labelTreeWith testStream tree)

deepFirst2 : Tree elem -> Tree (Int, elem)
deepFirst2 tree = evalState (labelTreeWith2 tree) [1..]

countEmpty : Tree elem -> State Nat ()
countEmpty Empty =
  do
    curr <- get
    put (S curr)
countEmpty (Node left _ right) =
  do
    countEmpty left
    countEmpty right

countEmptyNode : Tree elem -> State (Nat, Nat) ()
countEmptyNode Empty =
  do
    (currEmpties, currFull) <- get
    put (S currEmpties, currFull)
countEmptyNode (Node left _ right) =
  do
    countEmptyNode left
    countEmptyNode right
    (currEmpties, currFull) <- get
    put (currEmpties, S currFull)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
%default covering

data Three = Vrai | Faux | Indef

getType : Three -> Type
getType Vrai = Unit
getType Faux = Unit
getType Indef = Void

swap : (t : Three) -> getType t -> Three
swap Indef _ impossible
swap Vrai () = Faux


text:
module Invertible

%default total

-- http://www.informatik.uni-marburg.de/~rendel/unparse/

data PartIso α β = MkPartIso (α -> Maybe β) (β -> Maybe α)

class PartIsoFunctor (f : Type -> Type -> Type) where
  (<$>) : PartIso α β -> (f α γ -> f β γ)

inverse : PartIso α β -> PartIso β α
inverse (MkPartIso f g) = MkPartIso g f

apply : PartIso α β -> α -> Maybe β
apply (MkPartIso f g) = f

unapply : PartIso α β -> β -> Maybe α
unapply = Invertible.apply . inverse

class ProductFunctor (f : Type -> Type -> Type) where
  pf : f α γ -> f β γ -> f (α, β) γ

class Alternative (f : Type -> Type -> Type) where
  alt : f α γ -> f α γ -> f α γ
  empty : f α γ

class (PartIsoFunctor δ, ProductFunctor δ, Invertible.Alternative δ) => Syntax (δ : Type -> Type -> Type) γ where
  -- (<$>) :: Iso α β → δ α → δ β
  -- (<∗>) :: δ α → δ β → δ (α, β )
  -- (<|>) :: δ α → δ α → δ α
  -- empty :: δ α
  pure : Eq α => α -> δ α γ
  token : δ γ γ

nilv : PartIso () (Vect 0 α)
nilv = MkPartIso (const . Just $ Vect.Nil {a=α})
                (\xs => case xs of
                   [] => Just ()
                   _ => Nothing)

consv : PartIso (α, Vect n α) (Vect (S n) α)
consv = MkPartIso c1 c2
  where c1 (x, xs) = Just (x :: xs)
        c2 (x :: xs) = Just (x, xs)

times : Syntax δ γ => {n : Nat} -> δ α γ -> δ (Vect n α) γ
times {n} p with (n)
  | Z = (nilv <$> (Invertible.pure ()))
  | (S k) = (consv <$> (p `pf` (times p)))

nil : PartIso () (List α)
nil = MkPartIso (const . Just $ List.Nil {a=α})
                (\xs => case xs of
                   [] => Just ()
                   _ => Nothing)

cons : PartIso (α, List α) (List α)
cons = MkPartIso c1 c2
  where c1 (x, xs) = Just (x :: xs)
        c2 [] = Nothing
        c2 (x :: xs) = Just (x, xs)

many : Syntax δ γ => (max : Nat) -> δ α γ -> δ (List α) γ
many Z _ = nil <$> pure ()
many (S m) p = nil <$> pure ()
        `alt` cons <$> (pf p (many m p))

data Parser α γ = MkParser (List γ -> List (α, List γ))

parse : Parser α γ -> List γ -> List α
parse (MkParser p) s = [x | (x, _) <- p s]

instance PartIsoFunctor Parser where
  iso <$> (MkParser p) = MkParser (\s => [ (y, s')
                                         | (x, s') <- p s
                                         , y <- toList $ apply iso x])

instance ProductFunctor Parser where
  pf (MkParser p) (MkParser q) = MkParser (\s => [ ((x,y), s'')
                                                  | (x, s') <- p s
                                                  , (y, s'') <- q s'])

instance Invertible.Alternative Parser where
  alt (MkParser p) (MkParser q) = MkParser (\s => (p s) ++ (q s))
  empty = MkParser (\s => List.Nil)

instance Syntax Parser γ where
  pure x = MkParser (\s => [(x, s)])
  token = MkParser f
  where
    f [] = []
    f (x :: xs) = [(x, xs)]

data Printer α γ = MkPrinter (α -> Maybe (List γ))

print : Printer α γ -> α -> Maybe (List γ)
print (MkPrinter p) x = p x

instance PartIsoFunctor Printer where
  iso <$> (MkPrinter p) = MkPrinter (\b => unapply iso b >>= p)

instance ProductFunctor Printer where
  pf (MkPrinter p) (MkPrinter q) = MkPrinter (\(x, y) => Just (++) <$> (p x) <$> (q y))

instance Invertible.Alternative Printer where
  alt (MkPrinter p) (MkPrinter q) = MkPrinter $ \s =>
    case (p s) of
      Nothing => (q s)
      x => x
  empty = MkPrinter (\s => Nothing)

instance Syntax Printer γ where
  pure x = MkPrinter (\y =>
    if x == y
    then Just []
    else Nothing)
  token = MkPrinter (\t => Just [t])

-- Invertible.print (times $ (Invertible.pure {α=Bool} {γ=Bool} True)) [True, True]
-- Invertible.parse (times {n=2} $ (Invertible.pure {α=Bool} {γ=Bool} True)) [True, False, False]
-- Invertible.print (times $ (Invertible.token {γ=Bool})) [True, False]
-- Invertible.parse (times {n=3} $ (Invertible.token {γ=Bool})) [True, False, True, False]
-- Invertible.print (many 2 $ pf (Invertible.token {γ=Bool}) (Invertible.pure {α=Bool} {γ=Bool} True)) [(True, True), (False, True)]
-- Invertible.parse (many 3 $ pf (Invertible.token {γ=Bool}) (Invertible.pure {α=Bool} {γ=Bool} True)) [True, False]

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
||| Helper functions to work with `Data.Bits`.

module Patricia.BitsUtils

import Data.Bits
import Data.Fin

%default total
%access public export

||| Checks if bit at index `i` is set to `0`.
isZeroBit : Fin n -> Bits n -> Bool
isZeroBit i b = not $ getBit i b

||| Sets the indicated bit to zero and all the lesser bits to one.
|||
||| @i Index of bit to set.
||| @b Target bits.
maskInsignificant : (i : Fin n) -> (b : Bits n) -> Bits n
maskInsignificant i b = and (b `or` minus m (cast 1)) (complement m) where
    m : Bits n
    m = intToBits $ pow 2 (finToNat i)  -- TODO: implement more efficiently?

||| Checks if bits key before _branching bit_ matches _prefix_ bits.
|||
||| @i Index of branching bit.
||| @p Prefix bits.
||| @k Key bits.
matchPrefix : (i : Fin n) -> (p : Bits n) -> (k : Bits n) -> Bool
matchPrefix i p k = maskInsignificant i k == p

{-
    // Fast Imperative implementation for 32bits

>>> public static int highestOneBit(int i) {
>>>     i |= (i >>  1);
>>>     i |= (i >>  2);
>>>     i |= (i >>  4);
>>>     i |= (i >>  8);
>>>     i |= (i >> 16);
>>>     return i - (i >>> 1);
>>> }
-}

-- TODO: make it truely total
--   1. Ensure bits value under `b` is not zero
--   2. Ensure `natToFin` returns `Just` (use `fromInteger`?)
--   3. Ensure `shiftGo` returns not zero bits
-- TODO: make it fast
--   1. ¯\_(ツ)_/¯
||| Returns index of highest one bit set in `b`.
highestOneBit : Bits (S n) -> Fin (S n)  -- TODO: support Bits n -> Fin n ?
highestOneBit {n} b = bitsToFin $ shiftGo iterations b oneBit where
    iterations : Nat
    iterations = log2NZ (S n) SIsNotZ

    oneBit : Bits (S n)
    oneBit = cast 1

    shiftGo : Nat -> Bits (S n) -> Bits (S n) -> Bits (S n)
    shiftGo Z     i p = i `minus` (i `shiftRightLogical` oneBit)
    shiftGo (S k) i p = shiftGo k (i `or` (i `shiftRightArithmetic` p)) (p `shiftLeft` oneBit)

    bitsToFin : Bits (S n) -> Fin (S n)
    bitsToFin bits = fromMaybe FZ $ natToFin (log2NZ (toNat $ bitsToInt bits) believe_me) (S n)

branchingBit : Bits (S n) -> Bits (S n) -> Fin (S n)
branchingBit p0 p1 = highestOneBit $ xor p0 p1

max_stars_repo_name: ChShersh/idris-persistent-array

max_issues_repo_name: ChShersh/idris-patricia

max_forks_repo_name: ChShersh/idris-persistent-array


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module      : UML.Class.Model
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Class.Model

data Modifier = Abstract | Static
data Visibility = Private | Protected | Package | Public
data RelationTy = Specialisation | Aggregation | Composition | Association | Realisation
data ClassTy = ClassAbstract | ClassStandard | ClassInterface

-- ------------------------------------------------------------------- [ Model ]

data ElemTy = PARAM | METHOD | ATTR | CLASS | RELA | MODEL

data ClassModel : ElemTy -> Type where
  Param : String -> String -> ClassModel PARAM
  Method : String
         -> String
         -> Maybe Modifier
         -> Visibility
         -> List (ClassModel PARAM)
         -> ClassModel METHOD
  Attribute : String
            -> String
            -> Maybe Modifier
            -> Visibility
            -> ClassModel ATTR
  Clazz : String
        -> ClassTy
        -> List (ClassModel ATTR)
        -> List (ClassModel METHOD)
        -> ClassModel CLASS
  Relation : RelationTy
           -> String
           -> String
           -> Maybe String
           -> ClassModel RELA
  MkClassModel : List (ClassModel CLASS) -> List (ClassModel RELA) -> ClassModel MODEL

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

instance Eq Modifier where
    (==) Abstract Abstract = True
    (==) Static   Static   = True
    (==) _        _        = False

instance Eq Visibility where
    (==) Private   Private   = True
    (==) Protected Protected = True
    (==) Package   Package   = True
    (==) Public    Public    = True
    (==) _         _         = False

instance Eq RelationTy where
    (==) Specialisation Specialisation = True
    (==) Aggregation    Aggregation    = True
    (==) Composition    Composition    = True
    (==) Association    Association    = True
    (==) Realisation    Realisation    = True
    (==) _              _              = False

instance Eq ClassTy where
    (==) ClassAbstract  ClassAbstract  = True
    (==) ClassStandard  ClassStandard  = True
    (==) ClassInterface ClassInterface = True
    (==) _              _              = False

instance Eq ElemTy where
    (==) PARAM  PARAM  = True
    (==) METHOD METHOD = True
    (==) ATTR   ATTR   = True
    (==) CLASS  CLASS  = True
    (==) RELA   RELA   = True
    (==) MODEL  MODEL  = True
    (==) _      _      = False

mutual
  %assert_total
  eqClassModel : ClassModel a -> ClassModel a -> Bool
  eqClassModel (Param x xty)            (Param y yty)            = x == y && xty == yty
  eqClassModel (Method x xrTy xm xv xs) (Method y yrTy ym yv ys) = x == y && xrTy == yrTy && xm == ym && xv == yv && xs == ys
  eqClassModel (Attribute x xty xm xv)  (Attribute y yty ym yv)  = x == y && xty == yty && xm == ym && xv == yv
  eqClassModel (Clazz x xty xas xms)    (Clazz y yty yas yms)    = x == y && xty == yty && xas == yas && xms == yms
  eqClassModel (Relation xty xa xb xs)  (Relation yty ya yb ys)  = xty == yty && xa == ya && xb == yb && xs == ys
  eqClassModel (MkClassModel xcs xrs)   (MkClassModel ycs yrs)   = xcs == ycs && yrs == xrs
  eqClassModel _                        _                        = False

  instance Eq (ClassModel x) where
      (==) = eqClassModel

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

instance Show Modifier where
    show Abstract = "Abstract"
    show Static   = "Static"

instance Show Visibility where
    show Private   = "Private"
    show Protected = "Protected"
    show Package   = "Package"
    show Public    = "Public"

instance Show RelationTy where
    show Association    = "Association"
    show Specialiastion = "Specialisation"
    show Aggregation    = "Aggregation"
    show Composition    = "Composition"
    show Realisation    = "Realisation"

instance Show ClassTy where
    show ClassAbstract  = "ClassAbstract"
    show ClassStandard  = "ClassStandard"
    show ClassInterface = "ClassInterface"

instance Show ElemTy where
    show PARAM  = "PARAM"
    show METHOD = "METHOD"
    show ATTR   = "ATTR"
    show CLASS  = "CLASS"
    show RELA   = "RELA"
    show MODEL  = "MODEL"

instance Show (ClassModel x) where
    show (Param id ty)          = "[Param " ++ id ++ " : " ++ ty ++ "]"
    show (Method id rTy m v ps) = unwords ["[Method", id, ":", rTy, show m, show v, show ps, "]"]
    show (Attribute id ty m v)  = unwords ["[Attribute", id, ":", ty, show m, show v, "]"]
    show (Clazz id ty as ms)    = unwords ["[Class", id, ":", show ty, show as, show ms, "]"]
    show (Relation ty a b desc) = unwords ["[Relation", "(", show a, "->", show b, ")", ":", show ty, show desc, "]"]
    show (MkClassModel cs rs)   = unwords ["[Class", show cs, show rs, "]"]

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Data.Nat.Exponentiation

import Data.Nat as Nat
import Data.Nat.Properties
import Data.Monoid.Exponentiation as Mon
import Data.Num.Implementations as Num
import Data.Nat.Views
import Data.Nat.Order
import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic

%default total

public export
pow : Nat -> Nat -> Nat
pow = Mon.(^)

public export
lpow : Nat -> Nat -> Nat
lpow = linear @{Monoid.Multiplicative}

public export
pow2 : Nat -> Nat
pow2 = (2 ^)

public export
lpow2 : Nat -> Nat
lpow2 = lpow 2

export
modularCorrect : (v : Nat) -> {n : Nat} ->
                 pow v n === lpow v n
modularCorrect
   = Mon.modularCorrect
     @{Monoid.Multiplicative}
     (sym (multAssociative _ _ _))
     (irrelevantEq $ multOneLeftNeutral _)

export
pow2Correct : {n : Nat} -> pow2 n === lpow2 n
pow2Correct = modularCorrect 2

export
unfoldLpow2 : lpow2 (S n) === (lpow2 n + lpow2 n)
unfoldLpow2 = unfoldDouble

export
unfoldPow2 : pow2 (S n) === (pow2 n + pow2 n)
unfoldPow2 = irrelevantEq $ Calc $
  let mon : Monoid Nat; mon = Monoid.Multiplicative
      lpow2 : Nat -> Nat; lpow2 = linear @{mon} 2 in
  |~ pow2 (S n)
  ~~ lpow2 (S n)       ...( pow2Correct )
  ~~ lpow2 n + lpow2 n ...( unfoldLpow2 )
  ~~ (pow2 n + pow2 n) ...( cong2 (+) (sym pow2Correct) (sym pow2Correct) )

export
lteLpow2 : {m : Nat} -> 1 `LTE` lpow2 m
lteLpow2 {m = Z} = reflexive {rel = LTE}
lteLpow2 {m = S m} = CalcWith $
  let ih = lteLpow2 {m} in
  |~ 1
  <~ 2                 ...( ltZero )
  <~ lpow2 m + lpow2 m ...( plusLteMonotone ih ih )
  ~~ lpow2 (S m)       ...( sym (unfoldLpow2) )

export
ltePow2 : {m : Nat} -> 1 `LTE` pow2 m
ltePow2 = CalcWith $
  |~ 1
  <~ lpow2 m ...( lteLpow2 )
  ~~ pow2 m  ...( sym pow2Correct )

export
pow2Increasing : {m : Nat} -> pow2 m `LT` pow2 (S m)
pow2Increasing = CalcWith $
  |~ S (pow2 m)
  <~ pow2 m + pow2 m ...( plusLteMonotoneRight (pow2 m) 1 (pow2 m) ltePow2 )
  ~~ pow2 (S m)      ...( sym unfoldPow2 )


text:
module Shape

export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

export
triangle : Double -> Double -> Shape
triangle = Triangle

export
rectangle : Double -> Double -> Shape
rectangle = Rectangle

export
circle : Double -> Shape
circle = Circle

public export
data ShapeView : Shape -> Type where
  STriangle : ShapeView (triangle _ _)
  SRectangle : ShapeView (rectangle _ _)
  SCircle : ShapeView (circle _)

export
shapeView : (shape : Shape) -> ShapeView shape
shapeView (Triangle _ _)  = STriangle
shapeView (Rectangle _ _) = SRectangle
shapeView (Circle _)      = SCircle


text:
module Ch03.Exercise_3_5_14

import Ch03.Arith

%default total

numValueProofIs : {t : Term} ->
                  (pf : IsNumValue t) ->
                  (nv : NumValue ** (t = nv2t nv, pf = ConvertedFrom nv))
numValueProofIs {t = (v2t (Right nv))} (ConvertedFrom nv) = (nv ** (Refl, Refl))

zeroNotSucc : {t : Term} ->
              (Zero = Succ t) -> Void
zeroNotSucc Refl impossible

succ_inj : {t1, t2 : Term} ->
           (Succ t1 = Succ t2) ->
           (t1 = t2)
succ_inj Refl = Refl

nv2t_inj : {nv1, nv2 : NumValue} ->
           (nv2t nv1 = nv2t nv2) ->
           (nv1 = nv2)
nv2t_inj {nv1=Zero} {nv2=Zero} prf = Refl
nv2t_inj {nv1=Zero} {nv2=Succ x} prf = absurd (zeroNotSucc prf)
nv2t_inj {nv1=Succ x} {nv2=Zero} prf = absurd (zeroNotSucc (sym prf))
nv2t_inj {nv1=Succ x} {nv2=Succ y} prf = cong (nv2t_inj (succ_inj prf))

numValueProofsUnique : {t : Term} ->
                       (pf1 : IsNumValue t) ->
                       (pf2 : IsNumValue t) ->
                       (pf1 = pf2)
numValueProofsUnique pf1 pf2 with (numValueProofIs pf1)
  numValueProofsUnique pf1 pf2 | (nv ** (pf_t, pf_pf)) with (numValueProofIs pf2)
    numValueProofsUnique pf1 pf2 | (nv ** (pf_t, pf_pf)) | (nv' ** (pf_t', pf_pf')) = case nv2t_inj {nv1=nv} {nv2=nv'} (trans (sym pf_t) pf_t') of
                                                                                Refl => trans pf_pf (sym pf_pf')
uniqueEval : (t : Term) ->
             (r : EvalsTo t t') ->
             (r' : EvalsTo t t'') ->
             (r = r')
uniqueEval True EIfTrue _ impossible
uniqueEval True EIfFalse _ impossible
uniqueEval True (EIf _) _ impossible
uniqueEval True (ESucc _) _ impossible
uniqueEval True EPredZero _ impossible
uniqueEval True EPredSucc _ impossible
uniqueEval True (EPred _) _ impossible
uniqueEval True EIsZeroZero _ impossible
uniqueEval True EIsZeroSucc _ impossible
uniqueEval True (EIsZero _) _ impossible
uniqueEval False EIfTrue _ impossible
uniqueEval False EIfFalse _ impossible
uniqueEval False (EIf _) _ impossible
uniqueEval False (ESucc _) _ impossible
uniqueEval False EPredZero _ impossible
uniqueEval False EPredSucc _ impossible
uniqueEval False (EPred _) _ impossible
uniqueEval False EIsZeroZero _ impossible
uniqueEval False EIsZeroSucc _ impossible
uniqueEval False (EIsZero _) _ impossible
uniqueEval (IfThenElse True y z) EIfTrue EIfTrue = Refl
uniqueEval (IfThenElse True y z) EIfTrue (EIf x) impossible
uniqueEval (IfThenElse False y z) EIfFalse EIfFalse = Refl
uniqueEval (IfThenElse False y z) EIfFalse (EIf x) impossible
uniqueEval (IfThenElse True y z) (EIf w) EIfTrue impossible
uniqueEval (IfThenElse False y z) (EIf w) EIfFalse impossible
uniqueEval (IfThenElse x y z) (EIf w) (EIf s) = case uniqueEval x w s of
                                                     Refl => Refl
uniqueEval Zero EIfTrue _ impossible
uniqueEval Zero EIfFalse _ impossible
uniqueEval Zero (EIf _) _ impossible
uniqueEval Zero (ESucc _) _ impossible
uniqueEval Zero EPredZero _ impossible
uniqueEval Zero EPredSucc _ impossible
uniqueEval Zero (EPred _) _ impossible
uniqueEval Zero EIsZeroZero _ impossible
uniqueEval Zero EIsZeroSucc _ impossible
uniqueEval Zero (EIsZero _) _ impossible
uniqueEval (Succ x) (ESucc y) (ESucc z) = case uniqueEval x y z of
                                               Refl => Refl
uniqueEval (Pred Zero) EPredZero EPredZero = Refl
uniqueEval (Pred Zero) EPredZero (EPred x) impossible
uniqueEval (Pred (Succ t')) (EPredSucc {pf=pf1}) (EPredSucc {pf=pf2}) = case numValueProofsUnique pf1 pf2 of
                                                                             Refl => Refl
uniqueEval (Pred (Succ t')) (EPredSucc {pf}) (EPred x) = absurd (valuesDontEvaluate {pf=(numValueIsValue (succNumValueIsNumValue pf))} x)
uniqueEval (Pred Zero) (EPred y) EPredZero = absurd (valuesDontEvaluate {pf=IsValue.ConvertedFrom (Right Zero)} y)
uniqueEval (Pred (Succ t')) (EPred y) (EPredSucc {pf}) = absurd (valuesDontEvaluate {pf=(numValueIsValue (succNumValueIsNumValue pf))} y)

uniqueEval (Pred x) (EPred y) (EPred z) = case uniqueEval x y z of
                                               Refl => Refl
uniqueEval (IsZero Zero) EIsZeroZero EIsZeroZero = Refl
uniqueEval (IsZero Zero) EIsZeroZero (EIsZero x) impossible
uniqueEval (IsZero (Succ nv1)) (EIsZeroSucc {pf=pf1}) (EIsZeroSucc {pf=pf2}) = case numValueProofsUnique pf1 pf2 of
                                                                                Refl => Refl
uniqueEval (IsZero (Succ nv1)) (EIsZeroSucc {pf}) (EIsZero x) = absurd (valuesDontEvaluate {pf=(numValueIsValue (succNumValueIsNumValue pf))} x)
uniqueEval (IsZero Zero) (EIsZero y) EIsZeroZero impossible
uniqueEval (IsZero (Succ nv1)) (EIsZero y) (EIsZeroSucc {pf}) = absurd (valuesDontEvaluate {pf=(numValueIsValue (succNumValueIsNumValue pf))} y)
uniqueEval (IsZero x) (EIsZero y) (EIsZero z) = case uniqueEval x y z of
                                                     Refl => Refl

||| Proof that the one-step evaluation rules of the arithmetic language are deterministic (Ex. 3.5.14).
detVal : {t,t',t'' : Term} ->
         EvalsTo t t' ->
         EvalsTo t t'' ->
         (t' = t'')
detVal {t} pf pf' = case uniqueEval t pf pf' of
                         Refl => Refl

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


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

import XML.XPath

%access public export

data FreyjaError : Type where
  ExtractionError : XPathError -> FreyjaError
  GeneralError    : String -> FreyjaError
  TextConvError   : String -> FreyjaError
  MalformedDocError : String -> String -> FreyjaError

Show FreyjaError where
  show (ExtractionError msg) = unwords ["Extraction Error", show msg]
  show (TextConvError msg)   = unwords ["Text Conversion Error", show msg]
  show (GeneralError msg)    = msg
  show (MalformedDocError qstr msg) =
      unlines [ "Malformed Document Error."
              , " The query:"
              , unwords ["\t", show qstr]
              , "was expected to work,"
              , msg]

Extract : Type -> Type
Extract a = Either FreyjaError a

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module InsertionSort
import Data.Vect

import Sorted
import Card
import ElemsAreSame

restLemma : (s : GTE (cardValue y) (cardValue z)) -> (r_prf : GTE (cardValue y) (cardValue x)) -> (restIsSorted : Sorted rest) -> (restHead : HeadIsEither rest x z) -> (w : Sorted (z :: ys)) -> Sorted (y :: rest)
restLemma {y} s r_prf restIsSorted HeadIsLeft w = SortMany y restIsSorted r_prf
restLemma {y} s r_prf restIsSorted HeadIsRight w = SortMany y restIsSorted s

elemsSwap : (restElems : ElemsAreSame (x :: (z :: ys)) rest) -> ElemsAreSame (x :: (y :: (z :: ys))) (y :: rest)
elemsSwap {y} restElems = swapHeads (PrependXIsPrependX y restElems)

total insert': (x: Card) -> (ys: Vect (S n) Card) -> Sorted ys -> HeadIs ys y ->  (z:Vect (S (S n)) Card **(Sorted z, ElemsAreSame (x::ys) z, HeadIsEither z x y))
insert' x (y::[]) SortSingle MkHeadIs = case chooseGte (cardValue x) (cardValue y) of
                                                  (Left l_prf) => (x::y::[] **(SortMany x SortSingle l_prf, PrependXIsPrependX x (PrependXIsPrependX y NilIsNil), HeadIsLeft))
                                                  (Right r_prf) => (y::x::[] **(SortMany y SortSingle r_prf, PrependXYIsPrependYX x y NilIsNil, HeadIsRight))
insert' x (y::(z :: ys)) (SortMany y w s) MkHeadIs = case chooseGte (cardValue x) (cardValue y) of
                                                (Left l_prf) => (x::y::z::ys ** (SortMany x (SortMany y w s) l_prf,
                                                                                PrependXIsPrependX x (PrependXIsPrependX y (PrependXIsPrependX z (sameListsAreSame ys))),
                                                                                HeadIsLeft))
                                                (Right r_prf) => let (rest ** (restIsSorted, restElems, restHead)) = insert' x (z::ys) (tailIsSortedToo (SortMany y w s)) MkHeadIs in
                                                                     (y::rest ** (restLemma s r_prf restIsSorted restHead w,
                                                                                elemsSwap restElems,
                                                                                HeadIsRight))

insert : (x: Card) -> (xs:Vect n Card) -> Sorted xs -> (z:Vect (S n) Card ** (Sorted z, ElemsAreSame (x::xs) z))
insert x [] sort_pf = ([x] ** (SortSingle, PrependXIsPrependX x NilIsNil))
insert x (y::ys) sort_pf = let (sortedList ** (sort_prf, sort_elems_prf, head_prf)) = insert' x (y::ys) sort_pf MkHeadIs in
                             (sortedList ** (sort_prf, sort_elems_prf))

export insertSort: (x:Vect n Card) -> (y:Vect n Card ** (Sorted y, ElemsAreSame x y))
insertSort [] = ([] ** (SortEmpty, NilIsNil))
insertSort (x :: []) = ([x] ** (SortSingle,(PrependXIsPrependX x NilIsNil)))
insertSort (x :: xs) = let (rest ** (sort, elem)) = insertSort xs
                           (y ** (o_sort, o_elems)) = insert x rest sort
                           elem_prf_new = PrependXIsPrependX x elem
                           o_elems_new = SamenessIsTransitive elem_prf_new o_elems
                           in
                           (y ** (o_sort, o_elems_new))


text:
> module EscadoOliva.Quantifier

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

> ||| Quantifier
> K : Type -> Type -> Type
> K R X = (X -> R) -> R

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Deprecated, use `Prelude.Interfaces` instead
module Data.Num.Implementations


text:
-- --------------------------------------------------------- [ Concurrency.idr ]
-- Module      : Chapter.Concurrency
-- Description : Definitions from Chapter 15 of Edwin Brady's book,
--               "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Chapter.Concurrency

import System.Concurrency.Channels
import Chapter.Concurrency.ProcessLib

-- import Control.Arrow
-- import Control.Category
-- import Data.Morphisms

-- ------------------------------------ [ 15.1.1 Defining Concurrent Processes ]

%access public export

data Message = Add Nat Nat

-- ---------------------------------------- [ 15.1.2 Primitive Message Passing ]

namespace Unsafe

  %access export

  partial adder :IO ()
  adder = do Just chan <- listen 1
               | Nothing => adder
             Just msg <- unsafeRecv Message chan
               | Nothing => adder
             case msg of
                  Add x y => do ok <- unsafeSend chan (x + y)
                                adder

  partial main : IO ()
  main = do Just pid <- spawn adder
              | Nothing => putStrLn "Spawn failed"
            Just chan <- connect pid
              | Nothing => putStrLn "Connection failed"
            ok <- unsafeSend chan (Add 2 3)
            Just answer <- unsafeRecv Nat chan
              | Nothing => putStrLn "Receive failed"
            printLn answer

-- ----------------------------------- [ 15.2.1 Describing Processes in a Type ]

namespace Safe

  %access public export

  data MessagePID = MkMessage PID

  data Process : Type -> Type where
       Request : MessagePID -> Message -> Process (Maybe Nat)
       Respond : ((msg : Message) -> Process Nat) -> Process (Maybe Message)
       Spawn   : Process () -> Process (Maybe MessagePID)
       Loop    : Inf (Process a) -> Process a

       Action  : IO a -> Process a
       Pure    : a -> Process a
       (>>=)   : Process a -> (a -> Process b) -> Process b

  run : Fuel -> Process t -> IO (Maybe t)
  run Dry _                  = pure Nothing
  run fuel (Action act)      = pure (Just !act)
  run fuel (Pure val)        = pure (Just val)
  run fuel (act >>= next)    = do Just x <- run fuel act
                                    | Nothing => pure Nothing
                                  run fuel (next x)
  run (More fuel) (Loop act) = run fuel act
  run fuel (Spawn proc)   = do Just pid <- spawn (run fuel proc *> pure ())
                                 | Nothing => pure Nothing
                               pure (Just (Just (MkMessage pid)))
  -- TODO: encapsulate timeout
  run fuel (Respond calc) = do Just sender <- listen 1
                                 | Nothing => pure (Just Nothing)
                               Just msg <- unsafeRecv Message sender
                                 | Nothing => pure (Just Nothing)
                               Just res <- run fuel (calc msg)
                                 | Nothing => pure Nothing
                               unsafeSend sender res
                               pure (Just (Just msg))
  run fuel (Request (MkMessage proc) msg) =
      do Just chan <- connect proc
           | Nothing => pure (Just Nothing)
         if !(unsafeSend chan msg)
            then do Just x <- unsafeRecv Nat chan
                      | Nothing => pure (Just Nothing)
                    pure (Just (Just x))
            else pure (Just Nothing)

  partial runProc : Process () -> IO ()
  runProc proc = run forever proc *> pure ()

  adder : Process ()
  adder = do Respond go
             Loop adder
    where
      go : Message -> Process Nat
      go (Add x y) = Pure (x + y)

  partial main : Process ()
  main = do Just pid <- Spawn adder
              | Nothing => Action (putStrLn "Spawn failed")
            Just answer <- Request pid (Add 2 3)
              | Nothing => Action (putStrLn "Request failed")
            Action (printLn answer)

  -- NOTE: These two definitions type-check, but don't respond to messages.

  -- adderBad1 : Process ()
  -- adderBad1 = do Action $ putStrLn "I'm out of the office today"
  --                    Loop adderBad1

  -- adderBad2 : Process ()
  -- adderBad2 = Loop adderBad2

namespace Stateful

  -- data AdderAction : Type where
  --      Add : Nat -> Nat -> AdderAction

  public export
  AdderType : Message -> Type
  AdderType (Add x y) = Nat

  export
  adder : Service AdderType ()
  adder = do Respond (\(Add x y) => Pure (x + y))
             Loop adder

namespace ListProcessing

  %access public export

  data ListAction : Type where
       Length : List elem -> ListAction
       Append : List elem -> List elem -> ListAction

  ListType : ListAction -> Type
  ListType (Length xs)           = Nat
  ListType (Append {elem} xs ys) = List elem

  %access export

  procList : Service ListType ()
  procList = do Respond go
                Loop procList
    where
      go : (msg : ListAction) -> Process ListType (ListType msg) Ready Ready
      go (Length xs)    = Pure (length xs)
      go (Append xs ys) = Pure (xs ++ ys)

  procMain : Client ()
  procMain = do Just list <- Spawn procList
                  | Nothing => Action (putStrLn "Spawn failed")
                len <- Request list (Length [1,2,3])
                Action (printLn len)
                app <- Request list (Append [1,2,3] [4,5,6])
                Action (printLn app)

namespace WordCounting

  %access public export

  record WCData where
      constructor MkWCData
      wordCount : Nat
      lineCount : Nat

  implementation Show WCData where
    show (MkWCData wc lc) = unlines [ "Words: " ++ show wc
                                    , "Lines: " ++ show lc
                                    ]

  data WC = CountFile String
          | GetData String

  implementation Show WC where
    show (CountFile fname) = "CountFile " ++ fname
    show (GetData fname) = "GetData " ++ fname

  WCType : WC -> Type
  WCType (CountFile _) = ()
  WCType (GetData _)   = Maybe WCData

  private
  doCount : (content : String) -> WCData
  doCount content = MkWCData (length (lines content))
                             (length (words content))

  -- doCount' : (content : String) -> WCData
  -- doCount' = applyMor $ arrow (length . lines) &&&
  --                       arrow (length . words) >>>
  --                       arrow (uncurry MkWCData)

  countFile : List (String, WCData) -> String ->
              Process WCType (List (String, WCData)) Sent Sent
  countFile files fname =
      do Right content <- Action (readFile fname)
           | Left _ => Pure files
         let count = doCount content
         Action (putStrLn ("Counting complete for " ++ fname))
         Pure ((fname, doCount content) :: files)

  wcService : (loaded : List (String, WCData)) ->
              Service WCType ()
  wcService loaded =
      do msg <- Respond go
         newLoaded <- case msg of
              Just (CountFile fname) => countFile loaded fname
              _                      => Pure loaded
         Loop (wcService newLoaded)
    where
      go : (msg : WC) -> Process WCType (WCType msg) Ready Ready
      go (CountFile fname) = Pure ()
      go (GetData fname)   = Pure (lookup fname loaded)

  procMain : Client ()
  procMain =
      do Just wc <- Spawn (wcService [])
           | Nothing => Action (putStrLn "Spawn failed")
         Action (putStrLn "Counting test.txt")
         let fname = "/Users/mohacker/src/yurrriq/tdd-with-idris/README.org"
         Request wc (CountFile fname)
         Action (putStrLn "Processing")
         Just wcdata <- Request wc (GetData fname)
           | Nothing => Action (putStrLn "File error")
         Action (printLn wcdata)

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


text:
module Main

import Data.Vect
import Data.Stream

foo : List Char
foo = unpack $ pack $ take 4000 (repeat 'a')

factorialAux : Integer -> Integer -> Integer
factorialAux 0 a = a
factorialAux n a = factorialAux (n-1) (a*n)

factorial : Integer -> Integer
factorial n = factorialAux n 1

main : IO ()
main = do
   printLn $ factorial 100
   printLn $ factorial 10000
   printLn $ show $ the (Vect 3 String) ["red", "green", "blue"]
   printLn foo


text:
import Data.Vect

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Integer
interpTy TyBool      = Bool
interpTy (TyFun a t) = interpTy a -> interpTy t

data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: ctxt) t
    Pop  : HasType k ctxt t -> HasType (FS k) (u :: ctxt) t

data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i ctxt t -> Expr ctxt t
    Val : (x : Integer) -> Expr ctxt TyInt
    Lam : Expr (a :: ctxt) t -> Expr ctxt (TyFun a t)
    App : Expr ctxt (TyFun a t) -> Expr ctxt a -> Expr ctxt t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr ctxt a -> Expr ctxt b -> Expr ctxt c
    If  : Expr ctxt TyBool ->
          Lazy (Expr ctxt a) ->
          Lazy (Expr ctxt a) -> Expr ctxt a

data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env ctxt -> Env (a :: ctxt)

lookup : HasType i ctxt t -> Env ctxt -> interpTy t
lookup Stop    (x :: xs) = x
lookup (Pop k) (x :: xs) = lookup k xs

interp : Env ctxt -> Expr ctxt t -> interpTy t
interp env (Var i)     = lookup i env
interp env (Val x)     = x
interp env (Lam sc)    = \x => interp (x :: env) sc
interp env (App f s)   = interp env f (interp env s)
interp env (Op op x y) = op (interp env x) (interp env y)
interp env (If x t e)  = if interp env x then interp env t
                                         else interp env e

add : Expr ctxt (TyFun TyInt (TyFun TyInt TyInt))
add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

fact : Expr ctxt (TyFun TyInt TyInt)
fact = Lam (If (Op (==) (Var Stop) (Val 0))
               (Val 1)
               (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
                       (Var Stop)))

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          printLn (interp [] fact (cast x))


text:
import Double
import Generic
import HOF
import Partial
import Reverse
import AveMain
import Let_Where


text:
module Data.Crypto.Encryption.Stream

import Data.Bits
import Data.Vect

import Data.Crypto.Encryption
import Data.Crypto.Util

%default total
%access public export

interface Cipher k bitsPerChunk => StreamCipher k (bitsPerChunk : Nat) | k where
  generateKeystream : k -> Stream (Bits bitsPerChunk)

-- Stream ciphers are automorphic, so the encryption and decryption algorithms
-- are identical. I don’t know when that would ever be useful, but if it is, you
-- can just use `confound*` to handle whichever way you want.

confoundStream :
  StreamCipher k bitsPerChunk => k -> Stream (Bits bitsPerChunk) -> Stream (Bits bitsPerChunk)
confoundStream key = Stream.zipWith xor (generateKeystream key)
encryptStream :
  StreamCipher k bitsPerChunk => k -> Stream (Bits bitsPerChunk) -> Stream (Bits bitsPerChunk)
encryptStream = confoundStream
decryptStream :
  StreamCipher k bitsPerChunk => k -> Stream (Bits bitsPerChunk) -> Stream (Bits bitsPerChunk)
decryptStream = confoundStream

takeV : (n : Nat) -> (xs : Stream a) -> Vect n a
takeV Z     _         = []
takeV (S n) (x :: xs) = x :: (takeV n xs)

confoundMessage :
  StreamCipher k bitsPerChunk => k -> List (Bits bitsPerChunk) -> List (Bits bitsPerChunk)
confoundMessage key message =
  toList (zipWith xor
                  (takeV (length message) (generateKeystream key))
                  (fromList message))

implementation StreamCipher sc b => Encrypter sc b where
  encryptMessage = confoundMessage

implementation StreamCipher sc b => Decrypter sc b where
  decryptMessage = confoundMessage

implementation (StreamCipher sc b, Encrypter sc b, Decrypter sc b) =>
  SymmetricCipher sc b where

confound : (StreamCipher k _, Serializable i, Serializable o) => k -> i -> o
confound key = decode . confoundMessage key . encode

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module ZZmult

import congruence
import Quotient_Type
import ZZ_alt
import Product_Type_Eq
import ZZplus

%access public export
%default total

mult : ZZ1 -> ZZ1 -> ZZ1
mult (a, b) (c, d) =
    ((plus (mult a c) (mult b d)), (plus (mult b c) (mult a d)))


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

import Effects
import Effect.Random

%access export

-- --------------------------------------------------------- [ List Generators ]

genRndListE : (seed      : Integer)
           -> (len       : Nat)
           -> (generator : Eff a [RND])
           -> Eff (List a) [RND]
genRndListE s l f = do srand s; pure !(doGen l f)
  where
    doGen : (len : Nat)
         -> (generator : Eff a [RND])
         -> Eff (List a) [RND]
    doGen Z     f = pure List.Nil
    doGen (S n) f = pure $ (!f :: !(doGen n f))

genRndListUE : Eq a =>
               (seed      : Integer)
            -> (len       : Nat)
            -> (generator : Eff a [RND])
            -> Eff (List a) [RND]
genRndListUE s l f = do srand s; pure !(doGen l f)
  where
    genElem : Eq a => Eff a [RND] -> List a -> Eff a [RND]
    genElem f xs = do
      x <- f
      if elem x xs
        then genElem f xs
        else pure x

    doGen : Eq a => Nat -> Eff a [RND] -> Eff (List a) [RND]
    doGen Z     f = pure Nil
    doGen (S n) f = do
      xs <- doGen n f
      x  <- genElem f xs
      pure (x::xs)

genKVPair : (genA : Eff a [RND])
         -> (genB : Eff b [RND])
         -> Eff (Pair a b) [RND]
genKVPair f g = pure (!f, !g)

genRndListKVE : (seed : Integer)
             -> (len  : Nat)
             -> (genA : Eff a [RND])
             -> (genB : Eff b [RND])
             -> Eff (List (Pair a b)) [RND]
genRndListKVE s l f g = genRndListE s l (genKVPair f g)

genRndListKVUE : (Eq a, Eq b) =>
                 (seed : Integer)
              -> (len  : Nat)
              -> (genA : Eff a [RND])
              -> (genB : Eff b [RND])
              -> Eff (List (Pair a b)) [RND]
genRndListKVUE s l f g = do srand s; pure !(doGen l (genKVPair f g))
  where
    genElem : (Eq a, Eq b) => Eff (Pair a b) [RND] -> List (Pair a b) -> Eff (Pair a b) [RND]
    genElem f xs = do
      x <- f
      if elem x xs
        then genElem f xs
        else if isJust $ lookup (fst x) xs
          then genElem f xs
          else pure x

    doGen : (Eq a, Eq b) => Nat -> Eff (Pair a b) [RND] -> Eff (List (Pair a b)) [RND]
    doGen Z     f = pure Nil
    doGen (S n) f = do
      xs <- doGen n f
      x  <- genElem f xs
      pure (x::xs)

-- -------------------------------------------------------- [ Random Int Lists ]

rndListIntE : (seed   : Integer)
           -> (bounds : Pair Integer Integer)
           -> (length : Nat)
           -> Eff (List Integer) [RND]
rndListIntE s (l,u) n = genRndListE s n (rndInt l u)

rndListInt : (seed   : Integer)
          -> (bounds : Pair Integer Integer)
          -> (length : Nat)
          -> List (Integer)
rndListInt s bs n = runPure $ rndListIntE s bs n

-- ------------------------------------------------- [ Random Unique Int Lists ]

rndListIntUE : (seed   : Integer)
            -> (bounds : Pair Integer Integer)
            -> (len    : Nat)
            -> Eff (List Integer) [RND]
rndListIntUE s (l,u) n = genRndListUE s n (rndInt l u)

rndListIntU : (seed   : Integer)
           -> (bounds : Pair Integer Integer)
           -> (len    : Nat)
           -> List Integer
rndListIntU s bs n = runPure $ rndListIntUE s bs n

-- ------------------------------------------------- [ Random Int KV Pair List ]

genY : Integer -> Integer -> Eff Integer [RND]
genY l u = do
  x <- rndInt l u
  pure (x + 2*u)

rndListIntKVE : (seed   : Integer)
             -> (bounds : Pair Integer Integer)
             -> (len    : Nat)
             -> Eff (List (Pair Integer Integer)) [RND]
rndListIntKVE s (l,u) n = genRndListKVE s n (rndInt l u) (genY l u)

rndListIntKV : (seed   : Integer)
            -> (bounds : Pair Integer Integer)
            -> (len    : Nat)
            -> List (Pair Integer Integer)
rndListIntKV s bs n = runPure $ rndListIntKVE s bs n

rndListIntKVUE : (seed   : Integer)
              -> (bounds : Pair Integer Integer)
              -> (len    : Nat)
              -> Eff (List (Pair Integer Integer)) [RND]
rndListIntKVUE s (l,u) n = genRndListKVUE s n (rndInt l u) (genY l u)

rndListIntKVU : (seed   : Integer)
             -> (bounds : Pair Integer Integer)
             -> (len    : Nat)
             -> List (Pair Integer Integer)
rndListIntKVU s bs n = runPure $ rndListIntKVUE s bs n

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Main

import Test.Golden

%default covering

allTests : TestPool
allTests = MkTestPool "Name of the pool" [] Default
  [ "test001"
  ]

main : IO ()
main = runner
  [ testPaths "verpackung" allTests
  ] where
    testPaths : String -> TestPool -> TestPool
    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }

max_stars_repo_name: alexhumphreys/verpackung

max_issues_repo_name: alexhumphreys/verpackung

max_forks_repo_name: alexhumphreys/verpackung


text:
module Expr

import Maps

%access public export

%default total

State : Type
State = TotalMap Nat

empty_state : State
empty_state = t_empty 0

A : Id
A = MkId "A"

B : Id
B = MkId "B"

C : Id
C = MkId "C"

D : Id
D = MkId "D"

E : Id
E = MkId "E"

F : Id
F = MkId "F"

W : Id
W = MkId "W"

X : Id
X = MkId "X"

Y : Id
Y = MkId "Y"

Z : Id
Z = MkId "Z"

data AExp : Type where
  ANum : Nat -> AExp
  AId : Id -> AExp
  APlus : AExp -> AExp -> AExp
  AMinus : AExp -> AExp -> AExp
  AMult : AExp -> AExp -> AExp

namespace VariableNames
  A : AExp
  A = AId A

  B : AExp
  B = AId B

  C : AExp
  C = AId C

  D : AExp
  D = AId D

  E : AExp
  E = AId E

  F : AExp
  F = AId F

  W : AExp
  W = AId W

  X : AExp
  X = AId X

  Y : AExp
  Y = AId Y

  Z : AExp
  Z = AId Z

Num AExp where
  (+) = APlus
  (*) = AMult
  fromInteger = ANum . fromIntegerNat

(-) : AExp -> AExp -> AExp
(-) = AMinus

Uninhabited (ANum _ = AId _) where
  uninhabited Refl impossible

Uninhabited (ANum _ = APlus _ _) where
  uninhabited Refl impossible

Uninhabited (ANum _ = AMinus _ _) where
  uninhabited Refl impossible

Uninhabited (ANum _ = AMult _ _) where
  uninhabited Refl impossible

Uninhabited (APlus _ _ = ANum _) where
  uninhabited Refl impossible

Uninhabited (AMinus _ _ = ANum _) where
  uninhabited Refl impossible

Uninhabited (AMult _ _ = ANum _) where
  uninhabited Refl impossible

Uninhabited (AId _ = ANum _) where
  uninhabited Refl impossible

Uninhabited (AId _ = APlus _ _) where
  uninhabited Refl impossible

Uninhabited (AId _ = AMinus _ _) where
  uninhabited Refl impossible

Uninhabited (AId _ = AMult _ _) where
  uninhabited Refl impossible

Uninhabited (APlus _ _ = AId _) where
  uninhabited Refl impossible

Uninhabited (AMinus _ _ = AId _) where
  uninhabited Refl impossible

Uninhabited (AMult _ _ = AId _) where
  uninhabited Refl impossible

aNumInjective : ANum n = ANum m -> n = m
aNumInjective Refl = Refl

aIdInjective : AId x = AId y -> x = y
aIdInjective Refl = Refl

data BExp : Type where
  BTrue : BExp
  BFalse : BExp
  BEq : AExp -> AExp -> BExp
  BLe : AExp -> AExp -> BExp
  BNot : BExp -> BExp
  BAnd : BExp -> BExp -> BExp

(==) : AExp -> AExp -> BExp
(==) = BEq

(<=) : AExp -> AExp -> BExp
(<=) = BLe

not : BExp -> BExp
not = BNot

(&&) : BExp -> BExp -> BExp
(&&) = BAnd

aeval : State -> AExp -> Nat
aeval _ (ANum n) = n
aeval st (AId i) = st i
aeval st (APlus a1 a2) = aeval st a1 + aeval st a2
aeval st (AMinus a1 a2) = aeval st a1 `minus` aeval st a2
aeval st (AMult a1 a2) = aeval st a1 * aeval st a2

beval : State -> BExp -> Bool
beval _ BTrue = True
beval _ BFalse = False
beval st (BEq a1 a2) = aeval st a1 == aeval st a2
beval st (BLe a1 a2) = lte (aeval st a1) (aeval st a2)
beval st (BNot b) = not $ beval st b
beval st (BAnd b1 b2) = beval st b1 && beval st b2


text:
module Printf

data Format = Number Format
            | Str Format
            | Chr Format
            | Doub Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt)  = (i : Int) -> PrintfType fmt
PrintfType (Str fmt)     = (str : String) -> PrintfType fmt
-- `str` is ignored here because we are computing types, not values
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType (Chr fmt)     = (c : Char) -> PrintfType fmt
PrintfType (Doub fmt)    = (d : Double) -> PrintfType fmt
PrintfType End           = String

printFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printFmt (Number fmt) acc  = \i => printFmt fmt (acc ++ (show i))
printFmt (Str fmt) acc     = \s => printFmt fmt (acc ++ s)
printFmt (Lit str fmt) acc = printFmt fmt (acc ++ str)
printFmt (Chr fmt) acc     = \c => printFmt fmt (acc ++ (singleton c))
printFmt (Doub fmt) acc    = \d => printFmt fmt (acc ++ (show d))
printFmt End acc           = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number $ toFormat chars
toFormat ('%' :: 's' :: chars) = Str $ toFormat chars
toFormat ('%' :: 'c' :: chars) = Chr $ toFormat chars
toFormat ('%' :: 'f' :: chars) = Doub $ toFormat chars
toFormat ('%' :: chars)        = Lit "%" $ toFormat chars
-- Below implementation seems to be of an efficiency concern to me
-- If we didn't do strcons here, these literals would be concatenated by printFmt
toFormat (c :: chars)          = case toFormat chars of
                                     Lit lit chars' => Lit (strCons c lit) chars'
                                     fmt            => Lit (strCons c "") fmt

formatString : String -> Format
formatString = toFormat . unpack

printf : (fmt : String) -> PrintfType (formatString fmt)
printf fmt = printFmt _ ""

main : IO ()
main = do
     putStrLn (printf "%d" 1)

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Minecraft.Base.PreClassic.Stone.Export

import public Minecraft.Base.PreClassic.Stone.Block.Export
import public Minecraft.Base.PreClassic.Stone.Item.Export
import public Minecraft.Base.PreClassic.Stone.ItemEntity.Export

%default total


text:
infixl 0  ~~
prefix 1  |~
infix  1  ...

public export
(...) : (x : a) -> (y ~=~ x) -> (z : a ** y ~=~ z)
(...) x pf = (x ** pf)

public export
data FastDerivation : (x : a) -> (y : b) -> Type where
  (|~) : (x : a) -> FastDerivation x x
  (~~) : FastDerivation x y ->
         (step : (z : c ** y ~=~ z)) -> FastDerivation x z

public export
Calc : {x : a} -> {y : b} -> FastDerivation x y -> x = y
Calc (|~ x) = Refl
Calc {y} ((~~) {z=y} {y=y} der (MkDPair y Refl)) = Calc der

bad : Z = S Z
bad = Calc $ |~ Z ~~ Z ...(Refl)


text:
module Main

import Data.Buffer
import Control.Monad.Trans
import Control.Monad.Either
import Control.Monad.Maybe
import Node.HTTP.Server
import TyTTP.Adapter.Node.HTTP
import TyTTP.Adapter.Node.URI
import TyTTP.HTTP
import TyTTP.HTTP.Consumer
import TyTTP.HTTP.Producer
import TyTTP.HTTP.Routing
import TyTTP.URL
import TyTTP.URL.Path
import TyTTP.URL.Search

main : IO ()
main = do
  http <- HTTP.require
  ignore $ HTTP.listen' {e = String} $
      decodeUri' (text "URI decode has failed" >=> status BAD_REQUEST)
      :> parseUrl' (const $ text "URL has invalid format" >=> status BAD_REQUEST)
      :> routes' (text "Resource could not be found" >=> status NOT_FOUND)
          [ get $ path "/query" $ \step =>
              text step.request.url.search step >>= status OK
          , get $ path "/parsed" $ Simple.search $ \step =>
              text (show step.request.url.search) step >>= status OK
          ]

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Internal.CTimespec
-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

import CFFI.Types
import CFFI.Memory

import Data.Bits

%include c "time.h"

  -- struct tm {
  -- int tm_sec;         /* seconds,  range 0 to 59          */
  -- int tm_min;         /* minutes, range 0 to 59           */
  -- int tm_hour;        /* hours, range 0 to 23             */
  -- int tm_mday;        /* day of the month, range 1 to 31  */
  -- int tm_mon;         /* month, range 0 to 11             */
  -- int tm_year;        /* The number of years since 1900   */
  -- int tm_wday;        /* day of the week, range 0 to 6    */
  -- int tm_yday;        /* day in the year, range 0 to 365  */
  -- int tm_isdst;       /* daylight saving time             */
  -- };

tm_spec : Composite
tm_spec = STRUCT [
          mkComposite I8, --sec
          mkComposite I8, --min
          mkComposite I8, --hour
          mkComposite I8, --mday
          mkComposite I8, --mon
          mkComposite I16, --year
          mkComposite I8, --wday
          mkComposite I8, --yday
          mkComposite I8  -- dst
        ]

-- struct timespec {
--   time_t   tv_sec;        /* seconds */
--   long     tv_nsec;       /* nanoseconds */
-- };

time_spec : Composite
time_spec = STRUCT [
  mkComposite I64, --
  mkComposite I64 --min
  ]

public export
record CTimeSpec where
  constructor MkCTimeSpec
  sec : Integer
  nsec : Integer

export
Show CTimeSpec where
  show (MkCTimeSpec sec nsec) = show sec ++ "," ++ show nsec

get_time : Int -> Ptr -> IO Int
get_time clockId ptr = foreign FFI_C "clock_gettime" (Int -> Ptr -> IO Int) clockId ptr

ClockRealTime : IO Int
ClockRealTime = foreign FFI_C "#CLOCK_REALTIME" (IO Int)

export
clock_gettime : IO CTimeSpec
clock_gettime = do
  mem <- alloc time_spec
  result <- foreign FFI_C "clock_gettime" (Int -> Ptr -> IO Int) !ClockRealTime mem
  let (CPt x1 y) = field time_spec 0 mem
  let (CPt x2 y) = field time_spec 1 mem
  pure $ MkCTimeSpec (prim__zextB64_BigInt !(peek I64 x1)) (prim__zextB64_BigInt !(peek I64 x1))

export
clock_getres : IO CTimeSpec
clock_getres = do
  mem <- alloc time_spec
  result <- foreign FFI_C "clock_getres" (Int -> Ptr -> IO Int) !ClockRealTime mem
  let (CPt x1 y) = field time_spec 0 mem
  let (CPt x2 y) = field time_spec 1 mem
  pure $ MkCTimeSpec (prim__zextB64_BigInt !(peek I64 x1)) (prim__zextB64_BigInt !(peek I64 x1))

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the echo protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module EchoNaive

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import RFC.Echo

-- ---------------------------------------------------- [ Naive Echo Processes ]

||| Implementation of the Echo Protocol from the Server end of the
||| Protocol.
|||
||| @client The PID of the client process.
covering
echoServer : (client : PID)
           -> Process (echo') 'Server ['Client := client] [STDIO] ()
echoServer client = do
    msg <- recvFrom 'Client
    sendTo 'Client msg
    return ()

||| Implementation of the Echo Protocol from the Client end of the
||| Protocol.
|||
||| @server The PID of the server process.
covering
echoClient : (server : PID)
           -> Process (echo') 'Client ['Server := server] [STDIO] ()
echoClient server = do
    putStrLn "Enter some text:"
    msg <- getStr
    sendTo 'Server msg
    resp <- recvFrom 'Server
    putStrLn $ show (trim resp)
    return ()

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
doEchoProcess : IO ()
doEchoProcess = forever $ runConc [()] doEcho
  where
    forever : IO () -> IO ()
    forever proc = do proc; forever proc

    doEcho : Process (echo') 'Client [] [STDIO] ()
    doEcho = do
       server <- spawn (echoServer) [()]
       setChan 'Server server
       echoClient server
       dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doEchoProcess

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
import Prelude
%hide Nat
%hide Maybe

data Nat = Z | S Nat

add : Nat -> Nat -> Nat
add Z m = m
add (S n) m = S (add n m)

mul : Nat -> Nat -> Nat
mul Z m = Z
mul (S n) m = add m (mul n m)

-- Extended notation for type declaration
data Nat' : Type where
  Z' : Nat'
  S' : Nat' -> Nat'

data Maybe a = Nothing | Just a

data Maybe' : Type -> Type where
  Nothing' : Maybe' a
  Just' : a -> Maybe' a

-- Expression which returns a type
f : Bool -> Type
f True = Int
f False = String

-- Dependent function
g : (n : Bool) -> f n
g True = 0
g False = "Hello"

-- Implicit arguments
myId : (a : Type) -> a -> a
myId a x = x

myId' : {a : Type} -> a -> a
myId' x = x

myId'' : a -> a
myId'' x = x

-- Useful example
data List' : Type -> Type where
  Nil' : List' a
  Cons' : a -> List' a -> List' a

data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  Cons : a -> Vect n a -> Vect (S n) a

head : Vect (S n) a -> a
head (Cons x _) = x
-- this is not mandatory
head Nil impossible

concat : Vect n a -> Vect m a -> Vect (add n m) a
concat Nil xs = xs
concat (Cons x xs) ys = Cons x (concat xs ys)

length : {n : Nat} -> Vect n a -> Nat
length {n} _ = n

-- The Identity type
--data (=) : a -> b -> Type where
--  Refl : x = x

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

cong' : {f : t -> u} -> x = y -> f x = f y
cong' Refl = Refl

sym' : (x = y) -> (y = x)
sym' Refl = Refl

trans' : (x = y) -> (y = z) -> (x = z)
trans' Refl Refl = Refl

-- Proofs

total
addReducesS : (n : Nat) -> (m : Nat) -> S (add n m) = add n (S m)
addReducesS Z m = Refl
addReducesS (S k) m = cong' (addReducesS k m)

total
notEqual : 2 + 2 = 5 -> Void
notEqual Refl impossible

-- Another cool type
data Elem : List a -> a -> Type where
  Here : Elem (t :: _) t
  There : Elem ts t -> Elem (_ :: ts) t

total
emptyListIsEmpty : Elem [] _ -> Void
emptyListIsEmpty Here impossible
emptyListIsEmpty There impossible

-- Dependent Pair
data DPair' : (a : Type) -> (a -> Type) -> Type where
  MkDPair' : {P : a -> Type} -> (x : a) -> P x -> DPair' a P

-- Notation **
d : DPair Bool Main.f
d = MkDPair False "Hi"

d' : (b : Bool ** f b)
d' = (False ** "Hi")

-- Type of even numbers
T : Type
T = (x : Nat ** add x x = S (S Z))

verifiedSolution : T
verifiedSolution = (S Z ** Refl)

-- Prove no solutions exist
T2 : Type
T2 = (x : Nat ** mul x x = S (S Z))

total
t2IsFalse : T2 -> Void
t2IsFalse (Main.Z ** Refl) impossible