text:
||| FFI binding to the low-Level C Sockets bindings for Idris.
|||
||| Modified (C) The Idris Community, 2020
module Network.FFI

import Network.Socket.Data

-- From idris_net.h

%foreign "C:idrnet_socket, libidris2_support, idris_net.h"
export
prim__idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int

%foreign "C:idrnet_close, libidris2_support, idris_net.h"
export
prim__idrnet_close : (sockdes : SocketDescriptor) -> PrimIO Int

%foreign "C:idrnet_bind, libidris2_support, idris_net.h"
export
prim__idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                    (host : String) -> (port : Port) -> PrimIO Int

%foreign "C:idrnet_connect, libidris2_support, idris_net.h"
export
prim__idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                       (host : String) -> (port : Port) -> PrimIO Int

%foreign "C:idrnet_listen, libidris2_support, idris_net.h"
export
prim__idrnet_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int

%foreign "C:idrnet_fdopen, libidris2_support, idris_net.h"
export
prim__idrnet_fdopen : Int -> String -> PrimIO AnyPtr

%foreign "C:idrnet_sockaddr_family, libidris2_support, idris_net.h"
export
prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_sockaddr_ipv4, libidris2_support, idris_net.h"
export
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_unix, libidris2_support, idris_net.h"
export
prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_ipv4_port, libidris2_support, idris_net.h"
export
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_sockaddr_port, libidris2_support, idris_net.h"
export
prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int

%foreign "C:idrnet_create_sockaddr, libidris2_support, idris_net.h"
export
prim__idrnet_create_sockaddr : PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_accept, libidris2_support, idris_net.h"
         "C:idrnet_accept, libidris2_support, idris_net.h"
export
prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_send, libidris2_support, idris_net.h"
export
prim__idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int

%foreign "C:idrnet_send_buf, libidris2_support, idris_net.h"
export
prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign "C__collect_safe:idrnet_recv, libidris2_support, idris_net.h"
         "C:idrnet_recv, libidris2_support, idris_net.h"
export
prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_recv_buf, libidris2_support, idris_net.h"
         "C:idrnet_recv_buf, libidris2_support, idris_net.h"
export
prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign "C:idrnet_sendto, libidris2_support, idris_net.h"
export
prim__idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) ->
                      (port : Port) -> (family : Int) -> PrimIO Int

%foreign "C:idrnet_sendto_buf, libidris2_support, idris_net.h"
export
prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
                          (buf_len : Int) -> (host : String) -> (port : Port) ->
                          (family : Int) -> PrimIO Int

%foreign "C__collect_safe:idrnet_recvfrom, libidris2_support, idris_net.h"
         "C:idrnet_recvfrom, libidris2_support, idris_net.h"
export
prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
         "C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
export
prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr

%foreign "C:idrnet_get_recv_res, libidris2_support, idris_net.h"
export
prim__idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_get_recv_payload, libidris2_support, idris_net.h"
export
prim__idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign "C:idrnet_free_recv_struct, libidris2_support, idris_net.h"
export
prim__idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign "C:idrnet_get_recvfrom_res, libidris2_support, idris_net.h"
export
prim__idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign "C:idrnet_get_recvfrom_payload, libidris2_support, idris_net.h"
export
prim__idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign "C:idrnet_get_recvfrom_sockaddr, libidris2_support, idris_net.h"
export
prim__idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr

%foreign "C:idrnet_free_recvfrom_struct, libidris2_support, idris_net.h"
export
prim__idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign "C:idrnet_geteagain, libidris2_support, idris_net.h"
export
prim__idrnet_geteagain : PrimIO Int

%foreign "C:idrnet_errno, libidris2_support, idris_net.h"
export
prim__idrnet_errno : PrimIO Int

%foreign "C:idrnet_peek, libidris2_support, idris_net.h"
export
prim__idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int

%foreign "C:idrnet_poke, libidris2_support, idris_net.h"
export
prim__idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) ->
                    (val : Int {- should be Char? -}) -> PrimIO ()


text:
module Data.Hashable

%access public
%default total

class Hashable a where
  hash : a -> Nat

finHash : Hashable a => a -> Fin (S n)
finHash {n} x with (natToFin ((hash x) `modNat` (S n)) (S n))
  | Just m = m
  | Nothing = 0 -- impossible

instance Hashable Int where hash = cast . abs
instance Hashable Integer where hash = cast . abs
instance Hashable Char where hash = cast . abs . the Int . cast
instance Hashable Float where hash = cast .abs . the Int . cast
instance Hashable Nat where hash = id
instance Hashable a => Hashable (Vect n a) where
  hash = sum . map hash
instance (Hashable a, Foldable f) => Hashable (f a) where
  hash = foldr (\a => (+ hash a)) 0
instance Hashable () where hash _ = 0
instance (Hashable a,Hashable b) => Hashable (a,b) where hash (a,b) = hash a * hash b

ext: idr

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module Main
import Data.Vect

infixr 5 .+.
data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

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

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

addToStore : (store:DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size items) newitem = MkData schema _ (addToData items)
  where
    addToData : Vect old (SchemaType schema) -> Vect (S old) (SchemaType schema)
    addToData [] = [newitem]
    addToData (x :: xs) = newitem :: x :: xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp = let val = cast inp in
                        if val < 0
                           then Nothing
                        else let newVal = tot + val in
                            Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

data Command : Schema -> Type where
  SetSchema : (newschema : Schema) -> Command schema
  Add : SchemaType schema -> Command schema
  Get : Integer -> Command schema
  GetAll : Command schema
  Size : Command schema
  --Search : String -> Command schema
  Quit : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input) where
  getQuoted : List Char -> Maybe (String, String)
  getQuoted ('"' :: xs)  = case span (/= '"') xs of
                                (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                                _ => Nothing
  getQuoted _ = Nothing
parsePrefix SChar input = case unpack input of
                               (c :: rest ) => Just (c, ltrim (pack rest))
                               _ => Nothing
parsePrefix SInt input = case span isDigit input of
                             ("", rest) => Nothing
                             (num,rest) => Just (cast num, ltrim rest)
parsePrefix (leftSchema .+. rightSchema) input = case parsePrefix leftSchema input of
                                                      Nothing => Nothing
                                                      Just (l_val, input') => case parsePrefix rightSchema input' of
                                                                                Nothing => Nothing
                                                                                Just (r_val, input'') => Just ((l_val,r_val), input'')

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

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

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                              Z => Just (MkData schema _ [])
                              S k => Nothing

parseCommand : (schema:Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "add" rest = case parseBySchema schema rest of
                                      Nothing => Nothing
                                      Just restok => Just (Add restok)
--parseCommand schema "search" str = Just (Search str)
parseCommand schema "list" _ = Just GetAll
parseCommand schema "get" val = case all isDigit (unpack val) of
                            False => Just GetAll
                            True => Just (Get (cast val))
parseCommand schema "quit" "" = Just Quit
parseCommand schema "size" "" = Just Size
parseCommand schema "schema" rest = case parseSchema (words rest) of
                                         Nothing => Nothing
                                         Just schemaok => Just (SetSchema schemaok)
parseCommand _ _ _ = Nothing

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

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

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

stringify : SchemaType schema -> String
stringify schemaType = (display schemaType) ++ "\n"

getAll : (store:DataStore) -> Maybe (String, DataStore)
getAll store = let stringified = map stringify (items store)
               in Just (show stringified, store)

{-searchEntryHelper : (searchStr : String) -> (store : Vect n String) -> (currentResults : List (Nat,String)) -> List (Nat, String)
searchEntryHelper searchStr [] res = res
searchEntryHelper {n = S k} searchStr (x :: xs) res =
 let newResults =
   case Strings.isInfixOf searchStr x of
        True => (k,x) :: res
        False => res
 in searchEntryHelper searchStr xs newResults

searchEntry : (value : String) -> (store : DataStore) -> Maybe (String, DataStore)
searchEntry value store @ (MkData size items) = let search_result = searchEntryHelper value items Nil in
                                           Just ("Search results " ++ show (search_result) ++ "\n", store)
-}

processCmd : (store:DataStore) -> (command : Command (schema store)) -> Maybe (String, DataStore)
processCmd store (SetSchema schema') = case setSchema store schema' of
                                            Nothing => Just ("Can't update schema\n", store)
                                            Just store' => Just ("OK\n", store')
processCmd store (Add value) = Just ("ID " ++ show (size store) ++ "\n", addToStore store value)
processCmd store (Get pos)  = getEntry pos store
processCmd store GetAll = getAll store
processCmd store Quit = Nothing
processCmd store Size = Just ("Size " ++ show (size store) ++ "\n", store)
--processCmd store (Search value) = searchEntry value store

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse (schema store) input of
                             Just cmd => processCmd store cmd --cmd store
                             Nothing => Just ("Invalid command\n", store)

main : IO ()
main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
---
pandoc-minted:
  language: idris
---

= Bathroom Security

[Link](https://adventofcode.com/2016/day/2)

You arrive at *Easter Bunny Headquarters* under cover of darkness. However, you
left in such a rush that you forgot to use the bathroom! Fancy office buildings
like this one usually have keypad locks on their bathrooms, so you search the
front desk for the code.

"In order to improve security," the document you find says, "bathroom codes will
no longer be written down. Instead, please memorize and follow the procedure
below to access the bathrooms."

The document goes on to explain that each button to be pressed can be found by
starting on the previous button and moving to adjacent buttons on the keypad:
`U` moves up, `D` moves down, `L` moves left, and `R` moves right. Each line of
instructions corresponds to one button, starting at the previous button (or, for
the first line, *the "5" button*); press whatever button you're on at the end of
each line. If a move doesn't lead to a button, ignore it.

You can't hold it much longer, so you decide to figure out the code as you walk
to the bathroom. You picture a keypad like this:

```text
1 2 3
4 5 6
7 8 9
```

Suppose your instructions are:

```text
ULL
RRDDD
LURDL
UUUUD
```

- You start at "5" and move up (to "2"), left (to "1"), and left (you can't, and
  stay on "1"), so the first button is `1`.
- Starting from the previous button ("1"), you move right twice (to "3") and
  then down three times (stopping at "9" after two moves and ignoring the
  third), ending up with `9`.
- Continuing from "9", you move left, up, right, down, and left, ending with
  `8`.
- Finally, you move up four times (stopping at "2"), then down once, ending with
  `5`.

So, in this example, the bathroom code is `1985`.

Your puzzle input is the instructions from the document you found at the front
desk.

== Module Declaration and Imports

> ||| Day 2: Bathroom Security
> module Data.Advent.Day02
>
> import public Data.Advent.Day
> import public Data.Ix
>
> import Data.Vect
>
> import public Lightyear
> import public Lightyear.Char
> import public Lightyear.Strings

== Data Types

> %access public export
>
> ||| Up, down, left or right.
> data Instruction = ||| Up
>                    U
>                  | ||| Down
>                    D
>                  | ||| Left
>                    L
>                  | ||| Right
>                    R
>
> ||| A single digit, i.e. a number strictly less than ten.
> Digit : Type
> Digit = Fin 10
>
> implementation Show Digit where
>   show = show . finToInteger
>
> implementation [showDigits] Show (List Digit) where
>   show = concatMap show
>
> ||| A pair of coordinates on the keypad, `(x, y)`.
> Coordinates : Type
> Coordinates = (Fin 3, Fin 3)

\newpage

== Parsers

> %access export
>
> up : Parser Instruction
> up = char 'U' *> pure U <?> "up"
>
> down : Parser Instruction
> down = char 'D' *> pure D <?> "down"
>
> left : Parser Instruction
> left = char 'L' *> pure L <?> "left"
>
> right : Parser Instruction
> right = char 'R' *> pure R <?> "right"
>
> instruction : Parser Instruction
> instruction = up <|> down <|> left <|> right <?> "up, down, left or right"
>
> partial instructions : Parser (List Instruction)
> instructions = some instruction <* (skip endOfLine <|> eof)

== Part One

\begin{quote}
  What is the bathroom code?
\end{quote}

> namespace PartOne
>
>   ||| A keypad like this:
>   |||
>   ||| ```
>   ||| 1 2 3
>   ||| 4 5 6
>   ||| 7 8 9
>   ||| ```
>   keypad : Vect 3 (Vect 3 Digit)
>   keypad = [ [1, 2, 3],
>              [4, 5, 6],
>              [7, 8, 9] ]
>
>   move : Coordinates -> Instruction -> Coordinates
>   move (x, y) U = (x, pred y)
>   move (x, y) D = (x, succ y)
>   move (x, y) L = (pred x, y)
>   move (x, y) R = (succ x, y)

\newpage

>   button : Coordinates -> List Instruction -> (Coordinates, Digit)
>   button loc@(x, y) [] = (loc, index x (index y keypad))
>   button loc (i :: is) = button (move loc i) is
>
> partial partOne : List (List Instruction) -> String
> partOne = show @{showDigits} . go ((1,1), [])
>   where
>     go : (Coordinates, List Digit) -> List (List Instruction) -> List Digit
>     go (_, ds) []            = reverse ds
>     go (loc, ds) (is :: iis) = let (loc', d) = PartOne.button loc is in
>                                    go (loc', d :: ds) iis
>
> namespace PartOne
>
>   ||| ```idris example
>   ||| example
>   ||| ```
>   partial example : String
>   example = fromEither $ partOne <$>
>             parse (some instructions) "ULL\nRRDDD\nLURDL\nUUUUD"

== Part Two

You finally arrive at the bathroom (it's a several minute walk from the lobby so
visitors can behold the many fancy conference rooms and water coolers on this
floor) and go to punch in the code. Much to your bladder's dismay, the keypad is
not at all like you imagined it. Instead, you are confronted with the result of
hundreds of man-hours of bathroom-keypad-design meetings:

```text
    1
  2 3 4
5 6 7 8 9
  A B C
    D
```

You still start at "5" and stop when you're at an edge, but given the same
instructions as above, the outcome is very different:

- You start at "5" and don't move at all (up and left are both edges), ending at
  `5`.
- Continuing from "5", you move right twice and down three times (through "6",
  "7", "B", "D", "D"), ending at `D`.
- Then, from "D", you move five more times (through "D", "B", "C", "C", "B"),
  ending at `B`.
- Finally, after five more moves, you end at `3`.

\newpage

So, given the actual keypad layout, the code would be `5DB3`.

\begin{quote}
  Using the same instructions in your puzzle input, what is the correct
  \textit{bathroom code}?
\end{quote}

> namespace PartTwo
>
>   keypad : Vect 5 (n ** Vect n Char)
>   keypad = [ (1 **           ['1'])
>            , (3 **      ['2', '3', '4'])
>            , (5 ** ['5', '6', '7', '8', '9'])
>            , (3 **      ['A', 'B', 'C'])
>            , (1 **           ['D'])
>            ]
>
>   -- NOTE: This will wrap at the bounds, which might be unexpected.
>   partial convert : (n : Nat) -> Fin m -> Fin n
>   convert (S j) fm {m} =
>       let delta = half $ if S j > m
>                             then S j `minus` m
>                             else m `minus` S j in
>           the (Fin (S j)) $ fromNat $ finToNat fm `f` delta
>     where
>       f : Nat -> Nat -> Nat
>       f = if S j > m then plus else minus
>       partial half : Nat -> Nat
>       half = flip div 2
>
>   canMoveVertically : (Fin (S k), Fin 5) -> Instruction -> Bool
>   canMoveVertically (x, y) i with ((finToNat x, finToNat y))
>     canMoveVertically (x, y) U | (col, row) =
>         case row of
>              Z                   => False
>              S Z                 => col == 1
>              S (S Z)             => inRange (1,3) col
>              _                   => True
>     canMoveVertically (x, y) D | (col, row) =
>         case row of
>              S (S Z)             => inRange (1,3) col
>              S (S (S Z))         => col == 1
>              S (S (S (S Z)))     => False
>              _                   => True
>     canMoveVertically _ _ | _ = True

\newpage

>   partial move : (Fin (S k), Fin 5) -> Instruction ->
>     ((n ** Fin n), Fin 5)
>   move (x, y) U = if canMoveVertically (x, y) U
>                      then let n = fst (index (pred y) keypad) in
>                               ((n ** convert n x), pred y)
>                      else ((_ ** x), y)
>   move (x, y) D = if canMoveVertically (x, y) D
>                      then let n = fst (index (succ y) keypad) in
>                               ((n ** convert n x), succ y)
>                      else ((_ ** x), y)
>   move (x, y) L = let n = fst (index y keypad) in
>                       ((n ** convert n (pred x)), y)
>   move (x, y) R = let n = fst (index y keypad) in
>                       ((n ** convert n (succ x)), y)
>
>   partial button : (Fin (S k), Fin 5) -> List Instruction ->
>     (((n ** Fin n), Fin 5), Char)
>   button loc@(x, y) [] =
>       let (n ** row) = index y PartTwo.keypad
>           xx = convert n x in
>           (((n ** xx), y), index xx row)
>   button loc (i :: is) =
>       let ((S _ ** x), y) = move loc i in
>           button (x, y) is
>
> partial partTwo : List (List Instruction) -> String
> partTwo = go (((5 ** 0),2), [])
>   where
>     partial go : (((n ** Fin n), Fin 5), List Char) ->
>       List (List Instruction) -> String
>     go (_, cs) []            = pack $ reverse cs
>     go (loc, cs) (is :: iis) =
>         let ((S k ** xx), y) = loc
>             (loc', c) = PartTwo.button (xx, y) {k=k} is in
>             go (loc', c :: cs) iis
>
> namespace PartTwo
>
>   ||| ```idris example
>   ||| PartTwo.example
>   ||| ```
>   partial example : String
>   example = fromEither $ partTwo <$>
>             parse (some instructions) "ULL\nRRDDD\nLURDL\nUUUUD"

== Main

> namespace Main
>
>   partial main : IO ()
>   main = runDay $ MkDay 2 (some instructions)
>          (pure . partOne)
>          (pure . partTwo)

ext: lidr

max_stars_repo_name: yurrriq/advent-of-code


text:
module Adder

%default total

||| Calculate the type of an adder function
||| that expected `numargs` arguments (in addition
||| to the initial value argument)
AdderType : (numargs : Nat) -> Type
AdderType Z = Int
AdderType (S k) = (next : Int) -> AdderType k

adder : (numargs : Nat) -> (acc : Int) -> AdderType numargs
adder Z acc = acc
adder (S k) acc = \next => adder k (acc + next)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Complete

import Graph

data Complete : Graph a b -> Type where
  MkComplete : (graph : Graph a b) -> Complete graph

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
import System
import Data.String

main : IO ()
main = do systime <- time
          -- sanity checks on time value
          if systime > 1630268000 && systime < 10000000000
             then putStrLn "Retrieved unix timestamp from time function."
             else putStrLn "Failed to retrieve a unix timestamp from time function."


text:
module BinomialHeap

import Heap

%default total
%access private

data Tree a = Node Int a (List (Tree a))

export
data BinomialHeap a = BH (List (Tree a))

rank : Tree a -> Int
rank (Node r x c) = r

root : Tree a -> a
root (Node r x c) = x

link : Ord a => Tree a -> Tree a -> Tree a
link t1@(Node r x1 c1) t2@(Node _ x2 c2) =
  if x1 <= x2 then Node (r + 1) x1 (t2 :: c1) else Node (r + 1) x2 (t1 :: c2)

insTree : Ord a => Tree a -> List (Tree a) -> List (Tree a)
insTree t []             = [t]
insTree t ts@(t' :: ts') =
  if rank t < rank t' then t :: ts else insTree (link t t') ts'

mrg : Ord a => List (Tree a) -> List (Tree a) -> List (Tree a)
mrg ts1                  []           = ts1
mrg     []           ts2              = ts2
mrg ts1@(t1 :: ts1') ts2@(t2 :: ts2') = case compare (rank t1) (rank t2) of
  LT => t1 :: mrg ts1' ts2
  GT => t2 :: mrg ts1 ts2'
  EQ => insTree (link t1 t2) (mrg ts1' ts2')

removeMinTree : Ord a => List (Tree a) -> (Tree a, List (Tree a))
removeMinTree [] = idris_crash "empty heap"
removeMinTree [t] = (t, [])
removeMinTree (t :: ts) = let (t', ts') = removeMinTree ts in
  if root t < root t' then (t, ts) else (t', t :: ts')

Heap BinomialHeap where
  empty = BH []
  isEmpty (BH ts) = isNil ts

  insert x (BH ts) = BH (insTree (Node 0 x []) ts)

  merge (BH ts1) (BH ts2) = BH (mrg ts1 ts2)

  findMin (BH ts) = root (fst (removeMinTree ts))

  deleteMin (BH ts) = let (Node _ x ts1, ts2) = removeMinTree ts
    in BH (mrg (reverse ts1) ts2)


text:
module IR.StackSet

import IR
import IR.Lens

manage : Eq wid => wid -> Workspace wid -> Workspace wid
manage wid (MkWorkspace l Nothing) = MkWorkspace l (Just (MkStack wid [] []))
manage wid (MkWorkspace l (Just (MkStack wid' a b))) = MkWorkspace l (Just (MkStack wid a (wid' :: b)))

integrate : (s : Stack wid) -> Vect (stackLength s) wid
integrate (MkStack x ys zs) =
  rewrite plusSuccRightSucc (length ys) (length zs)
  in reverse (fromList ys) ++ x :: fromList zs

member : Eq wid => wid -> StackSet wid sid -> Bool
member wid s =
  maybe False (\stack => elem wid (integrate stack)) (workspaceStack' . screenWorkspace' . stackSetCurrent' ^$ s)

filter : (wid -> Bool) -> Stack wid -> Maybe (Stack wid)
filter p (MkStack f ls rs) = case filter p (f::rs) of
  f'::rs' => Just (MkStack f' (filter p ls) rs')
  [] => case filter p ls of
    f'::ls' => Just (MkStack f' ls' [])
    [] => Nothing

stackSetStack : Lens (StackSet wid sid) (Maybe (Stack wid))
stackSetStack = workspaceStack' . screenWorkspace' . stackSetCurrent'

-- TODO: Use more than stackSetCurrent'
delete : Eq wid => wid -> StackSet wid sid -> StackSet wid sid
delete wid = stackSetStack ^%= (>>= filter (/= wid))

insertUp : Eq wid => wid -> StackSet wid sid -> StackSet wid sid
insertUp wid s = if member wid s then s else insert
  where insert = workspaceStack' . screenWorkspace' . stackSetCurrent' ^%= Just . maybe (MkStack wid [] []) (\(MkStack t l r) => MkStack wid l (t::r)) $ s

modify' : (Stack wid -> Stack wid) -> StackSet wid sid -> StackSet wid sid
modify' f = stackSetStack ^%= map f

stackSetPeek : StackSet wid sid -> Maybe wid
stackSetPeek ss = map (\s => stackFocus' ^$ s) (stackSetStack ^$ ss)

reverseStack : Stack wid -> Stack wid
reverseStack (MkStack t ls rs) = MkStack t rs ls

focusUp' : Stack wid -> Stack wid
focusUp' (MkStack t [] []) = MkStack t [] []
focusUp' (MkStack t (l::ls) rs) = MkStack l ls (t::rs)
focusUp' (MkStack t [] rs) =
  let (x::xs) = reverse (t::fromList rs)
  in MkStack x (toList xs) []

focusDown' : Stack wid -> Stack wid
focusDown' = reverseStack . focusUp' . reverseStack

focusDown : StackSet wid sid -> StackSet wid sid
focusDown = modify' focusDown'

focusUp : StackSet wid sid -> StackSet wid sid
focusUp = modify' focusUp'

focusWindow : Eq wid => wid -> StackSet wid sid -> StackSet wid sid
focusWindow wid s = fromMaybe s (find ((== Just wid) . stackSetPeek) (take (maybe 0 stackLength (stackSetStack ^$ s)) (iterate focusUp s)))

swapUp' : Stack wid -> Stack wid
swapUp' (MkStack t (l::ls) rs) = MkStack t ls (l::rs)
swapUp' (MkStack t []     rs) = MkStack t (reverse rs) []

swapUp : StackSet wid sid -> StackSet wid sid
swapUp = modify' swapUp'

swapDown : StackSet wid sid -> StackSet wid sid
swapDown = modify' (reverseStack . swapUp' . reverseStack)

windows : (StackSet wid sid -> StackSet wid sid) -> { [IR wid sid, STATE (IRState wid sid)] } Eff ()
windows f = do
  update (irStateStackSet' ^%= f)
  runLayout

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


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

-- ----------------------------------------------------------------- [ Imports ]
import Effects
import Effect.File
import Effect.Logging.Default

import Lightyear
import Lightyear.Strings
import Lightyear.StringFile

import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution

import Sif.Types
import Sif.AbsSyntax
import Sif.Error

-- -------------------------------------------------------------- [ Directives ]

%default partial
%access export

-- ------------------------------------------------------------- [ File Reader ]

readSifFile : Parser a
           -> String
           -> Eff (Either SifError a) [FILE_IO (), LOG]
readSifFile p fname = do
    trace $ unwords ["Parsing file:", show fname]
    res <- parseFile FileMissing ParseError p fname
    case res of
      Left err => pure $ Left err
      Right  r => pure $ Right r

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Sub02Apply54x12

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

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

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


text:
interface X a where

interface X a => Y a where

[SomeX] X a => X (List a) where

[SomeY] {- X a => -} Y (List a) using SomeX where

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.DOM.EventListener

import API.Web.DOM.Event

%access public export
%default total

||| An EventListener can be used to observe a specific event.
|||
||| The original specification can be found at
||| https://dom.spec.whatwg.org/#concept-event-listener
record EventListener where
  constructor New
  type     : String
  ||| The *callback* arguments sets the **callback** that will be invoked when
  ||| the event get dispatched.
  callback : Event -> IO ()

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
import Data.Vect

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

notInTail : (notHere : (value = x) -> Void) -> (notThere : Elem value xs -> Void) -> Elem value (x :: xs) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later

myIsElem: DecEq a => (value: a) -> (xs: Vect n a) -> Dec(Elem value xs)
myIsElem value [] = No notInNil
myIsElem value (x :: xs) = case decEq value x of
  (Yes Refl)    => Yes Here
  (No  notHere) => case myIsElem value xs of
    (Yes prf) => Yes (There prf)
    (No notThere) => No (notInTail notHere notThere)

removeElem: (value: a) -> (xs: Vect (S n) a) -> (prf: Elem value xs) -> Vect n a
removeElem             value (value :: ys) Here         = ys
removeElem {n = Z}     value (y     :: []) (There later) = absurd later
removeElem {n = (S k)} value (y     :: ys) (There later) = y :: removeElem value ys later

maryInVector: Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector =  There (There Here)

data Last: List a -> a -> Type where
  LastOne: Last [value] value
  LastCons: (prf: Last xs value) -> Last (x :: xs) value

last123: Last [1, 2, 3] 3
last123 = LastCons (LastCons LastOne)

notInEmpty : Last [] value -> Void
notInEmpty LastOne impossible
notInEmpty (LastCons _) impossible

notTheLastOne : (notLast : (x = value) -> Void) -> Last [x] value -> Void
notTheLastOne notLast LastOne = notLast Refl
notTheLastOne _ (LastCons LastOne) impossible
notTheLastOne _ (LastCons (LastCons _)) impossible

notInListTail : (notInTail : Last (mid :: tail) value -> Void) -> Last (x :: (mid :: tail)) value -> Void
notInListTail notInTail (LastCons prf) = notInTail prf

total isLast: DecEq a => (xs: List a) -> (value: a) -> Dec(Last xs value)
isLast [] value = No notInEmpty
isLast (last :: []) value = case decEq last value of
  (Yes Refl) => Yes LastOne
  (No contra) => No (notTheLastOne contra)
isLast (head :: mid :: tail) value = case isLast (mid :: tail) value of
  (Yes prf) => Yes (LastCons prf)
  (No notInTail) => No (notInListTail notInTail)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Lambdapants.Term

||| In the lambda calculus, a term is one of three things:
||| * A variable is a term;
||| * Application of two terms is a term; and
||| * A lambda abstraction is a term.
|||
||| Nothing else is a term. Application is left-associative, so the term
||| `(s t u)` is the same as `(s t) u`. One often omits outermost parentheses.
||| In abstractions, the body extends as far to the right as possible.
public export
data Term : Type where
  ||| Variable
  Var : String -> Term
  ||| Lambda abstraction
  Lam : String -> Term -> Term
  ||| Application
  App : Term -> Term -> Term

export
Eq Term where
  (Var a)   == (Var b)   = a == b
  (Lam x t) == (Lam y u) = x == y && t == u
  (App t u) == (App v w) = t == v && u == w
  _         == _         = False

export
Show Term where
  show (Var v)   = "Var "  ++ show v
  show (App t u) = "App (" ++ show t ++ ") ("
                           ++ show u ++ ")"
  show (Lam x t) = "Lam "  ++ show x ++ " ("
                           ++ show t ++ ")"

mutual
  lam : Term -> String
  lam (Lam x t) = "\x03BB" ++ x ++ "." ++ lam t
  lam term = app term

  app : Term -> String
  app (App t u) = app t ++ " " ++ pretty u
  app term = pretty term

  ||| Translate the given term to a pretty-printed string.
  export
  pretty : Term -> String
  pretty term =
    case term of
         Lam _ _ => "(" ++ lam term ++ ")"
         App _ _ => "(" ++ app term ++ ")"
         Var var => var

||| Return a list of all variables which appear free in the term *t*.
export total
freeVars : (t : Term) -> List String
freeVars (Var v)   = [v]
freeVars (Lam v t) = delete v (freeVars t)
freeVars (App t u) = freeVars t `union` freeVars u

||| Return a boolean to indicate whether the variable *v* appears free in the
||| term *t*.
export total
isFreeIn : (v : String) -> (t : Term) -> Bool
isFreeIn var term = elem var (freeVars term)

||| De Bruijn-indexed intermediate representation for more convenient alpha
||| comparison of terms.
data Indexed : Type where
  ||| Bound variable (depth indexed)
  Bound : Nat -> Indexed
  ||| Free variable
  Free  : String -> Indexed
  ||| Application
  IxApp : Indexed -> Indexed -> Indexed
  ||| Lambda abstraction
  IxLam : Indexed -> Indexed

Show Indexed where
  show (Bound n)   = "Bound "  ++ show n
  show (Free v)    = "Free "   ++ show v
  show (IxApp t u) = "IxApp (" ++ show t ++ ") ("
                               ++ show u ++ ")"
  show (IxLam t)   = "IxLam (" ++ show t ++ ")"

Eq Indexed where
  (Bound m)   == (Bound n)   = m == n
  (Free v)    == (Free w)    = v == w
  (IxApp t u) == (IxApp v w) = t == v && u == w
  (IxLam t)   == (IxLam u)   = t == u
  _           == _           = False

||| Translate the term *t* to a canonical De Bruijn (depth-indexed) form.
total
toIndexed : (t : Term) -> Indexed
toIndexed = indexed [] where
  indexed : List String -> Term -> Indexed
  indexed bound (Var x)   = maybe (Free x) Bound (elemIndex x bound)
  indexed bound (App t u) = IxApp (indexed bound t) (indexed bound u)
  indexed bound (Lam x t) = IxLam (indexed (x :: bound) t)

||| Return a boolean to indicate whether two terms are alpha equivalent; that
||| is, whether one can be converted to the other purely by renaming of bound
||| variables.
export total
alphaEq : Term -> Term -> Bool
alphaEq t u = toIndexed t == toIndexed u

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module Loop

import Loop


text:
module Main

mutual
  -- N.B. isOdd call gets inlined and the resulting self-recursive
  -- tailcall will result in a goto
  isEven : Nat -> Bool
  isEven Z = True
  isEven (S k) = isOdd k

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

main : IO ()
main = do
  printLn (isOdd 1234567)
  printLn (sum [1..50000])

max_stars_repo_name: Trundle/idris-go

max_issues_repo_name: Trundle/idris-go

max_forks_repo_name: Trundle/idris-go


text:
module Data.Colist1

import Data.Colist
import Data.List
import Data.List1
import Data.Nat
import Data.Stream
import public Data.Zippable

%default total

||| A possibly finite, non-empty Stream.
public export
data Colist1 : (a : Type) -> Type where
  (:::) : a -> Colist a -> Colist1 a

--------------------------------------------------------------------------------
--          Creating Colist1
--------------------------------------------------------------------------------

||| Convert a `List1` to a `Colist1`.
public export
fromList1 : List1 a -> Colist1 a
fromList1 (h ::: t) = h ::: fromList t

||| Convert a stream to a `Colist1`.
public export
fromStream : Stream a -> Colist1 a
fromStream (x :: xs) = x ::: fromStream xs

||| Try to convert a `Colist` to a `Colist1`. Returns `Nothing` if
||| the given `Colist` is empty.
public export
fromColist : Colist a -> Maybe (Colist1 a)
fromColist Nil       = Nothing
fromColist (x :: xs) = Just (x ::: xs)

||| Try to convert a list to a `Colist1`. Returns `Nothing` if
||| the given list is empty.
public export
fromList : List a -> Maybe (Colist1 a)
fromList = fromColist . fromList

||| Create a `Colist1` of only a single element.
public export
singleton : a -> Colist1 a
singleton a = a ::: Nil

||| An infinite `Colist1` of repetitions of the same element.
public export
repeat : a -> Colist1 a
repeat v = v ::: repeat v

||| Create a `Colist1` of `n` replications of the given element.
public export
replicate : (n : Nat) -> {auto 0 prf : IsSucc n} -> a -> Colist1 a
replicate 0     _ impossible
replicate (S k) x = x ::: replicate k x

||| Produce a `Colist1` by repeating a sequence
public export
cycle : List1 a -> Colist1 a
cycle (x ::: xs) = x ::: cycle (xs ++ [x])

||| Generate an infinite `Colist1` by repeatedly applying a function.
public export
iterate : (f : a -> a) -> a -> Colist1 a
iterate f a  = a ::: iterate f (f a)

||| Generate a `Colist1` by repeatedly applying a function.
||| This stops once the function returns `Nothing`.
public export
iterateMaybe : (f : a -> Maybe a) -> a -> Colist1 a
iterateMaybe f a  = a ::: iterateMaybe f (f a)

||| Generate a `Colist1` by repeatedly applying a function
||| to a seed value.
||| This stops once the function returns `Nothing`.
public export
unfold : (f : s -> Maybe (s,a)) -> s -> a -> Colist1 a
unfold f s a = a ::: unfold f s

--------------------------------------------------------------------------------
--          Basic Functions
--------------------------------------------------------------------------------

||| Convert a `Colist1` to a `Colist`
public export
forget : Colist1 a -> Colist a
forget (h ::: t) = h :: t

||| Convert an `Inf (Colist1 a)` to an `Inf (Colist a)`
public export
forgetInf : Inf (Colist1 a) -> Inf (Colist a)
forgetInf (h ::: t) = h :: t

||| Prepends an element to a `Colist1`.
public export
cons : (x : a) -> (xs : Colist1 a) -> Colist1 a
cons x xs = x ::: forget xs

||| Concatenate two `Colist1`s
public export
append : Colist1 a -> Colist1 a -> Colist1 a
append (h ::: t) ys = h ::: append t (forget ys)

||| Append a `Colist1` to a `List`.
public export
lappend : List a -> Colist1 a -> Colist1 a
lappend Nil       ys = ys
lappend (x :: xs) ys = x ::: lappend xs (forget ys)

||| Append a `List` to a `Colist1`.
public export
appendl : Colist1 a -> List a -> Colist1 a
appendl (x ::: xs) ys = x ::: appendl xs ys

||| Take a `Colist1` apart
public export
uncons : Colist1 a -> (a, Colist a)
uncons (h ::: tl) = (h, tl)

||| Extract the first element from a `Colist1`
public export
head : Colist1 a -> a
head (h ::: _) = h

||| Drop the first element from a `Colist1`
public export
tail : Colist1 a -> Colist a
tail (_ ::: t) = t

||| Take up to `n` elements from a `Colist1`
public export
take : (n : Nat) -> {auto 0 prf : IsSucc n} -> Colist1 a -> List1 a
take 0     _          impossible
take (S k) (x ::: xs) = x ::: take k xs

||| Take elements from a `Colist1` up to and including the
||| first element, for which `p` returns `True`.
public export
takeUntil : (p : a -> Bool) -> Colist1 a -> Colist1 a
takeUntil p (x ::: xs) = if p x then singleton x else x ::: takeUntil p xs

||| Take elements from a `Colist1` up to (but not including) the
||| first element, for which `p` returns `True`.
public export
takeBefore : (p : a -> Bool) -> Colist1 a -> Colist a
takeBefore p = takeBefore p . forget

||| Take elements from a `Colist1` while the given predicate `p`
||| returns `True`.
public export
takeWhile : (p : a -> Bool) -> Colist1 a -> Colist a
takeWhile p = takeWhile p . forget

||| Extract all values wrapped in `Just` from the beginning
||| of a `Colist1`. This stops, once the first `Nothing` is encountered.
public export
takeWhileJust : Colist1 (Maybe a) -> Colist a
takeWhileJust = takeWhileJust . forget

||| Drop up to `n` elements from the beginning of the `Colist1`.
public export
drop : (n : Nat) -> Colist1 a -> Colist a
drop n = drop n . forget

||| Try to extract the `n`-th element from a `Colist1`.
public export
index : (n : Nat) -> Colist1 a -> Maybe a
index n = index n . forget

||| Produce a `Colist1` of left folds of prefixes of the given `Colist1`.
||| @ f the combining function
||| @ acc the initial value
||| @ xs the `Colist1` to process
export
scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist1 b) -> Colist1 a
scanl f acc (x ::: xs) = acc ::: scanl f (f acc x) xs

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

public export
Semigroup (Colist1 a) where
  (<+>) = append

public export
Functor Colist1 where
  map f (x ::: xs) = f x ::: map f xs

public export
Applicative Colist1 where
  pure = repeat

  (f ::: fs) <*> (a ::: as) = f a ::: (fs <*> as)

public export
Zippable Colist1 where
  zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith f xs ys

  zipWith3 f (x ::: xs) (y ::: ys) (z ::: zs) =
    f x y z ::: zipWith3 f xs ys zs

  unzip xs = (map fst xs, map snd xs)

  unzip3 xs = ( map (\(a,_,_) => a) xs
              , map (\(_,b,_) => b) xs
              , map (\(_,_,c) => c) xs
              )

  unzipWith f = unzip . map f

  unzipWith3 f = unzip3 . map f

--------------------------------------------------------------------------------
-- Interleavings
--------------------------------------------------------------------------------

-- zig, zag, and cantor are taken from the paper
-- Applications of Applicative Proof Search
-- by Liam O'Connor

public export
zig : List1 (Colist1 a) -> Colist (Colist1 a) -> Colist a

public export
zag : List1 a -> List (Colist1 a) -> Colist (Colist1 a) -> Colist a

zig xs = zag (head <$> xs) (mapMaybe (fromColist . tail) $ forget xs)

zag (x ::: []) [] [] = x :: []
zag (x ::: []) (z :: zs) [] = x :: zig (z ::: zs) []
zag (x ::: []) zs (l :: ls) = x :: zig (l ::: zs) ls
zag (x ::: (y :: xs)) zs ls = x :: zag (y ::: xs) zs ls

public export
cantor : Colist1 (Colist1 a) -> Colist1 a
cantor (xxs ::: []) = xxs
cantor ((x ::: xs) ::: (yys :: zzss))
  = x ::: zig (yys ::: mapMaybe fromColist [xs]) zzss

namespace Colist

  public export
  cantor : List (Colist a) -> Colist a
  cantor xs =
    let Just (l ::: ls) = List.toList1' $ mapMaybe fromColist xs
          | Nothing => []
    in zig (l ::: []) (fromList ls)

  -- Exploring the (truncated) Nat*Nat top right quadrant of the plane
  -- using Cantor's zig-zag traversal:
  example :
     let nats : Colist Nat; nats = fromStream Stream.nats in
     take 10 (Colist.cantor [ map (0,) nats
                            , map (1,) nats
                            , map (2,) nats
                            , map (3,) nats])
     === [ (0, 0)
         , (1, 0), (0, 1)
         , (2, 0), (1, 1), (0, 2)
         , (3, 0), (2, 1), (1, 2), (0, 3)
         ]
  example = Refl

namespace DPair

  ||| Explore the plane corresponding to all possible pairings
  ||| using Cantor's zig zag traversal
  public export
  planeWith : {0 p : a -> Type} ->
              ((x : a) -> p x -> c) ->
              Colist1 a -> ((x : a) -> Colist1 (p x)) ->
              Colist1 c
  planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)

  ||| Explore the plane corresponding to all possible pairings
  ||| using Cantor's zig zag traversal
  public export
  plane : {0 p : a -> Type} ->
          Colist1 a -> ((x : a) -> Colist1 (p x)) ->
          Colist1 (x : a ** p x)
  plane = planeWith (\ x, prf => (x ** prf))

namespace Pair

  ||| Explore the plane corresponding to all possible pairings
  ||| using Cantor's zig zag traversal
  public export
  planeWith : (a -> b -> c) ->
              Colist1 a -> (a -> Colist1 b) ->
              Colist1 c
  planeWith k as f = cantor (map (\ x => map (k x) (f x)) as)

  ||| Explore the plane corresponding to all possible pairings
  ||| using Cantor's zig zag traversal
  public export
  plane : Colist1 a -> (a -> Colist1 b) -> Colist1 (a, b)
  plane = Pair.planeWith (,)

--------------------------------------------------------------------------------
-- Example
--------------------------------------------------------------------------------

-- Exploring the Nat*Nat top right quadrant of the plane
-- using Cantor's zig-zag traversal:
example :
     let nats1 = fromStream Stream.nats in
     Colist1.take 10 (Pair.plane nats1 (const nats1))
     === (0, 0) :::
         [ (1, 0), (0, 1)
         , (2, 0), (1, 1), (0, 2)
         , (3, 0), (2, 1), (1, 2), (0, 3)
         ]
example = Refl


text:
module Tail

import Data.Strings

main : IO ()
main = assert_total $ do
  putStrLn $ strTail ""
  putStrLn $ strTail " Hello World!"

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
import Data.String.Parser

main : IO ()
main = do
    let res = parse (satisfy isDigit) "100"
    printLn res


text:
module Rats

import ZZ
import ZZUtils
import Rationals

data Rats : Type where
  Rat : (p : ZZ) -> (q: ZZ) -> (pf: NotZero q) -> Rats

numerator: Rats-> ZZ
numerator (Rat p q pf) = p

denominator : Rats -> ZZ
denominator(Rat p q pf) = q

addRats : Rats -> Rats -> Rats
addRats (Rat p q x) (Rat y z w) =
  let
    num = (p * z) + (q * y)
    den = q * z
    pf : NotZero den = productNonZero x w
  in
    Rat num den pf

multRats : Rats -> Rats-> Rats
multRats (Rat p q x) (Rat y z w) =
  let
    num = p * y
    den = q * z
    pf : NotZero den = productNonZero x w
  in
    Rat num den pf

ZZtoRats : ZZ -> Rats
ZZtoRats x = Rat x (Pos(S Z)) PositiveZ

InttoRats : Integer -> Rats
InttoRats x = ZZtoRats (fromInt x)

implementation Num Rats where
  (+) = addRats
  (*) = multRats
  fromInteger = InttoRats

EqualRats : Rats -> Rats-> Type
EqualRats (Rat p q r) (Rat x y z) = (p*y = x*q)

rewriteNonZero : (k : ZZ) -> NotZero k -> NotZero (k*1) = NotZero k
rewriteNonZero k pf = rewrite ( multOneRightNeutralZ k) in Refl
{-
NonZeroIdentity: {a:ZZ}->{x: NotZero (Pos(S Z))}-> (r: NotZero a)-> ((productNonZero r x) = r)
NonZeroIdentity {a=Pos (S q)} {x=(PositiveZ{k=Z})} (PositiveZ{k=q}) =
  rewrite blah Pos(S q)  in Refl
NonZeroIdentity {a= NegS q} {x=(PositiveZ{k=Z})} (NegativeZ{k=q}) = rewrite multOneRightNeutralZ (NegS q) in Refl

ZIsIdentity:(a: Rats) -> ((a + (Rat 0 1 x)) = a )
ZIsIdentity (Rat p (Pos(S k)) PositiveZ) =
  rewrite multOneRightNeutralZ p in
  rewrite multZeroRightZeroZ (Pos(S k)) in
  rewrite plusZeroRightNeutralZ p in
  rewrite multOneRightNeutralZ (Pos(S k)) in
  Refl
ZIsIdentity (Rat p (NegS k) NegativeZ) =
  rewrite multOneRightNeutralZ p in
  rewrite multZeroRightZeroZ (NegS k) in
  rewrite plusZeroRightNeutralZ p in
  rewrite multOneRightNeutralZ (NegS k) in
  Refl

--PostulateEquality : EqualRats x y -> (x=y)
  -}


text:
main:IO()
main=let(s1,s2,s3)=("main:IO()\nmain=let(s1,s2,s3)=(",",",")in putStrLn$concat[s1,show s1,s2,show s2,s2,show s3,s3]")in putStrLn$concat[s1,show s1,s2,show s2,s2,show s3,s3]

max_stars_repo_name: MakeNowJust/quine

max_issues_repo_name: makenowjust/quine

max_forks_repo_name: makenowjust/quine


text:
import DataStore

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

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

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

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

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Test.IxArray

import Data.IxArray
import Data.IxRel

assertEq : Eq a => a -> a -> String -> IO ()
assertEq actual expected msg =
  if actual == expected
    then pure ()
    else do
      idris_crash ("Failed: " ++ msg ++ "\n")

testSimple : IO ()
testSimple = do
  arr <- replicate 1 "a"
  elem <- index 0 arr
  assertEq elem "a" "read what we write"

export
testAll : IO ()
testAll = do
  testSimple
  putStrLn "Succeeded"

max_stars_repo_name: ejconlon/idris-array

max_issues_repo_name: ejconlon/ixarray

max_forks_repo_name: ejconlon/ixarray


text:
module GRIN.Analysis.MaxVar

import Data.SortedMap
import GRIN.AST

Semigroup Var where
    MkVar x <+> MkVar y = MkVar (max x y)

Monoid Var where
    neutral = MkVar 0

maxVarSVal : SVal -> Var
maxVarSVal (SVar v) = v
maxVarSVal _ = neutral

maxVarVal : Val name -> Var
maxVarVal (SimpleVal v) = maxVarSVal v
maxVarVal (ConstTagNode _ vs) = foldMap maxVarSVal vs
maxVarVal (VarTagNode v vs) = v <+> foldMap maxVarSVal vs
maxVarVal _ = neutral

maxVarCPat : CasePat name -> Var
maxVarCPat (NodePat _ vs) = concat vs
maxVarCPat _ = neutral

mutual
    maxVarSExp : SExp name -> Var
    maxVarSExp (Do e) = maxVarExp e
    maxVarSExp (App _ vs) = concat vs
    maxVarSExp (Pure v) = maxVarVal v
    maxVarSExp (Store v) = maxVarVal v
    maxVarSExp (Fetch _ v) = v
    maxVarSExp (FetchI _ _ v) = v
    maxVarSExp (Update v1 v2) = v1 <+> maxVarVal v2

    maxVarExp : Exp name -> Var
    maxVarExp (SimpleExp e) = maxVarSExp e
    maxVarExp (Bind v rhs rest) = maxVarVal v <+> maxVarSExp rhs <+> maxVarExp rest
    maxVarExp (Case v alts) = maxVarVal v <+> foldMap maxVarAlt alts

    maxVarAlt : Alt name -> Var
    maxVarAlt (MkAlt pat exp) = maxVarCPat pat <+> maxVarExp exp

maxVarDef : Def name -> Var
maxVarDef (MkDef _ as e _) = concat as <+> maxVarExp e

export
maxVar : Prog name -> Var
maxVar (MkProg _ defs _) = foldMap maxVarDef defs


text:
module Main

import Erlang

||| Get the length of a string.
||| Implemented using the Erlang function `string:length/1`.
stringLength : String -> Integer
stringLength str = erlUnsafeCall Integer "string" "length" [str]

||| Get the length of string and print the result.
|||
||| Output:
||| ```idris
||| 5
||| ```
main : IO ()
main = do
  let result = stringLength "Hello"
  printLn result

-- `erlUnsafeCall` requires that the passed arguments and the return type are
-- members of `ErlType`. One way to create a generic function is to forward
-- this constraint to the caller of `reverseList`.

||| Reverse a list of values that conform to `ErlType`.
||| Implemented using the Erlang function `lists:reverse/1`.
reverseList : ErlType a => List a -> List a
reverseList xs = erlUnsafeCall (List a) "lists" "reverse" [xs]

||| Reverse a list of strings and print the result.
||| String is a member of `ErlType` so this works.
|||
||| Output:
||| ```idris
||| ["c", "b", "a"]
||| ```
main2 : IO ()
main2 = do
  let result = reverseList ["a", "b", "c"]
  printLn result

-- We can write a more generic reverse list function by wrapping the value in
-- the `Raw` type. When doing this, one need to be sure that the value we pass
-- to Erlang is sensible. In the following example, we know that the `List` is
-- mapped to an Erlang list, and the values contained in the list does not
-- matter to `lists:reverse/1`.

||| Reverse a list of values of any type.
||| Implemented using the Erlang function `lists:reverse/1`.
reverseListGeneric : List a -> List a
reverseListGeneric xs =
  let MkRaw val = erlUnsafeCall (Raw (List a)) "lists" "reverse" [MkRaw xs]
  in val

||| A data type that has no meaning to Erlang.
data Custom = MkCustom String

Show Custom where
  show (MkCustom str) = "MkCustom " ++ show str

||| Reverse a list of `Custom` values and print the result.
|||
||| Output:
||| ```idris
||| [MkCustom "type", MkCustom "this", MkCustom "about", MkCustom "know",
||| MkCustom "not", MkCustom "does", MkCustom "Erlang"]
||| ```
main3 : IO ()
main3 = do
  let result = reverseListGeneric
        [MkCustom "Erlang", MkCustom "does", MkCustom "not", MkCustom "know",
        MkCustom "about", MkCustom "this", MkCustom "type"]
  printLn result

-- It is possible to pass functions as arguments to Erlang functions as well.

-- The signature of `foldl` in Erlang is as following:
-- ```erlang
-- foldl(Fun, Acc0, List) -> Acc1
--
-- Fun = fun((Elem :: T, AccIn) -> AccOut)
-- Acc0 = Acc1 = AccIn = AccOut = term()
-- List = [T]
-- T = term()
-- ```

-- When wrapping an Erlang function we still want to provide a convenient
-- signature to Idris programs, i.e. a curried function:

||| A fold-left function that takes a pure step-function.
||| Implemented using the Erlang function `lists:foldl/3`.
pureFoldl : (ErlType a, ErlType b) => (a -> b -> b) -> b -> List a -> b
pureFoldl func acc xs =
  erlUnsafeCall b "lists" "foldl" [MkFun2 func, acc, xs]

||| Calculate the sum of integer values and print the result.
|||
||| Output:
||| ```idris
||| 6
||| ```
main4 : IO ()
main4 = do
  let result = pureFoldl (+) 0 [1, 2, 3]
  printLn result

-- The function that we provide to Erlang may also contain IO actions.
-- When we pass a function that performs side-effects to `lists:foldl/1`, it
-- means the resulting function call will also perform side-effects. To make
-- sure that we are being honest in our types, the retun type of `impureFoldl`
-- be of the type `IO`.

||| A fold-left function that takes a step-function that may perform
||| side-effects.
||| Implemented using the Erlang function `lists:foldl/3`.
impureFoldl : (ErlType a, ErlType b) => (a -> b -> IO b) -> b -> List a -> IO b
impureFoldl func acc xs =
  pure $ erlUnsafeCall b "lists" "foldl" [MkIOFun2 func, acc, xs]

||| Calculate the sum of integer values and print the result. Also print
||| the value at every step.
|||
||| Output:
||| ```idris
||| Next: 4
||| Next: 5
||| Next: 6
||| Sum: 15
||| ```
main5 : IO ()
main5 = do
  result <- impureFoldl (\x, acc => do { putStrLn ("Next: " ++ show x); pure (x + acc) }) 0 [4, 5, 6]
  putStrLn ("Sum: " ++ show result)


text:
-- Challenge 229 Hard In Idris

-- | Reverses a number
reverse : Integer -> Integer
reverse = cast . reverse . show

solution : Integer -> Integer
solution max = solution' 0 0
  where solution' : Integer -> Integer -> Integer
        solution' n sum =
          if nextN > max
            then sum
            else solution' nextN newSum
          where nextN = n + 7
                newSum = if ((reverse nextN) `mod` 7) == 0
                          then sum + nextN
                          else sum
main : IO()
main = print $ solution $ cast $ power 10 11

max_stars_repo_name: RossMeikleham/DailyProgrammer

max_issues_repo_name: RossMeikleham/DailyProgrammer

max_forks_repo_name: RossMeikleham/DailyProgrammer


text:
module Data.So

import Data.Bool

%default total

||| Ensure that some run-time Boolean test has been performed.
|||
||| This lifts a Boolean predicate to the type level. See the function `choose`
||| if you need to perform a Boolean test and convince the type checker of this
||| fact.
|||
||| If you find yourself using `So` for something other than primitive types,
||| it may be appropriate to define a type of evidence for the property that you
||| care about instead.
public export
data So : Bool -> Type where
  Oh : So True

export
Uninhabited (So False) where
  uninhabited Oh impossible

||| Perform a case analysis on a Boolean, providing clients with a `So` proof
export
choose : (b : Bool) -> Either (So b) (So (not b))
choose True  = Left Oh
choose False = Right Oh

export
eqToSo : b = True -> So b
eqToSo Refl = Oh

export
soToEq : So b -> b = True
soToEq Oh = Refl

||| If `b` is True, `not b` can't be True
export
soToNotSoNot : So b -> Not (So (not b))
soToNotSoNot Oh = uninhabited

||| If `not b` is True, `b` can't be True
export
soNotToNotSo : So (not b) -> Not (So b)
soNotToNotSo = flip soToNotSoNot

export
soAnd : {a : Bool} -> So (a && b) -> (So a, So b)
soAnd soab with (choose a)
  soAnd {a=True}  soab | Left Oh = (Oh, soab)
  soAnd {a=True}  soab | Right prf = absurd prf
  soAnd {a=False} soab | Right prf = absurd soab

export
andSo : (So a, So b) -> So (a && b)
andSo (Oh, Oh) = Oh

export
soOr : {a : Bool} -> So (a || b) -> Either (So a) (So b)
soOr soab with (choose a)
  soOr {a=True}  _    | Left Oh = Left Oh
  soOr {a=False} _    | Left Oh impossible
  soOr {a=False} soab | Right Oh = Right soab
  soOr {a=True}  _    | Right Oh impossible

export
orSo : Either (So a) (So b) -> So (a || b)
orSo (Left Oh)  = Oh
orSo (Right Oh) = rewrite orTrueTrue a in
                  Oh


text:
module Js.Console

import Js

%default total

export
log : (text : String) -> JS_IO ()
log = js "console.log(%0)" (String -> JS_IO ())

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module Data.DPair

import Decidable.Equality

%default total

namespace DPair

  public export
  curry : {0 p : a -> Type} -> ((x : a ** p x) -> c) -> (x : a) -> p x -> c
  curry f x y = f (x ** y)

  public export
  uncurry : {0 p : a -> Type} -> ((x : a) -> p x -> c) -> (x : a ** p x) -> c
  uncurry f s = f s.fst s.snd

  public export
  bimap : {0 p : a -> Type} -> {0 q : b -> Type} -> (f : a -> b) -> (forall x. p x -> q (f x)) -> (x : a ** p x) -> (y : b ** q y)
  bimap f g (x ** y) = (f x ** g y)

  public export
  DecEq k => ({x : k} -> Eq (v x)) => Eq (DPair k v) where
    (k1 ** v1) == (k2 ** v2) = case decEq k1 k2 of
                                 Yes Refl => v1 == v2
                                 No _     => False

namespace Exists

  ||| A dependent pair in which the first field (witness) should be
  ||| erased at runtime.
  |||
  ||| We can use `Exists` to construct dependent types in which the
  ||| type-level value is erased at runtime but used at compile time.
  ||| This type-level value could represent, for instance, a value
  ||| required for an intrinsic invariant required as part of the
  ||| dependent type's representation.
  |||
  ||| @type The type of the type-level value in the proof.
  ||| @this The dependent type that requires an instance of `type`.
  public export
  record Exists {0 type : Type} this where
    constructor Evidence
    0 fst : type
    snd : this fst

  public export
  curry : {0 p : a -> Type} -> (Exists p -> c) -> ({0 x : a} -> p x -> c)
  curry f = f . Evidence _

  public export
  uncurry : {0 p : a -> Type} -> ({0 x : a} -> p x -> c) -> Exists p -> c
  uncurry f ex = f ex.snd

  export
  evidenceInjectiveFst : Evidence x p = Evidence y q -> x = y
  evidenceInjectiveFst Refl = Refl

  export
  evidenceInjectiveSnd : Evidence x p = Evidence x q -> p = q
  evidenceInjectiveSnd Refl = Refl

  public export
  bimap : (0 f : a -> b) -> (forall x. p x -> q (f x)) -> Exists {type=a} p -> Exists {type=b} q
  bimap f g (Evidence x y) = Evidence (f x) (g y)

namespace Subset

  ||| A dependent pair in which the second field (evidence) should not
  ||| be required at runtime.
  |||
  ||| We can use `Subset` to provide extrinsic invariants about a
  ||| value and know that these invariants are erased at
  ||| runtime but used at compile time.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  public export
  record Subset type pred where
    constructor Element
    fst : type
    0 snd : pred fst

  public export
  curry : {0 p : a -> Type} -> (Subset a p -> c) -> (x : a) -> (0 _ : p x) -> c
  curry f x y = f $ Element x y

  public export
  uncurry : {0 p : a -> Type} -> ((x : a) -> (0 _ : p x) -> c) -> Subset a p -> c
  uncurry f s = f s.fst s.snd

  export
  elementInjectiveFst : Element x p = Element y q -> x = y
  elementInjectiveFst Refl = Refl

  export
  elementInjectiveSnd : Element x p = Element x q -> p = q
  elementInjectiveSnd Refl = Refl

  public export
  bimap : (f : a -> b) -> (0 _ : forall x. p x -> q (f x)) -> Subset a p -> Subset b q
  bimap f g (Element x y) = Element (f x) (g y)

  public export
  Eq type => Eq (Subset type pred) where
    (==) = (==) `on` fst

  public export
  Ord type => Ord (Subset type pred) where
    compare = compare `on` fst

  ||| This Show implementation replaces the (erased) invariant
  ||| with an underscore.
  export
  Show type => Show (Subset type pred) where
    showPrec p (Element v _) = showCon p "Element" $ showArg v ++ " _"


text:
import Data.Vect

--myReverse : Vect n a -> Vect n a
--myReverse [] = []
--myReverse {n=S k} (x :: xs) = reverseProof $ myReverse xs ++ [x]
--  where
--    reverseProof : Vect (plus len 1) a -> Vect (S len) a
--    reverseProof {len} xs = rewrite plusCommutative 1 len in xs

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m =  m + n
myPlusCommutes Z m = rewrite sym (plusZeroRightNeutral m) in Refl
myPlusCommutes (S k) m = let rec = cong {f=S} (myPlusCommutes k m)
                         in rewrite sym (plusSuccRightSucc m k) in rec

vectLenPlusZero : Vect n a -> Vect (n + 0) a
vectLenPlusZero {n} xs = rewrite plusZeroRightNeutral n in xs

vectLenPlusSuccRight : Vect (S (n + len)) a -> Vect (n + (S len)) a
vectLenPlusSuccRight {n} {len} xs = rewrite sym (plusSuccRightSucc n len) in xs

reverse' : Vect n a -> Vect m a -> Vect (n+m) a
reverse' xs [] = vectLenPlusZero xs
reverse' xs (x :: ys) = vectLenPlusSuccRight $ reverse' (x :: xs) ys

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs


text:
import Data.Vect

readToBlank : IO (List String)
readToBlank = do
  line <- getLine
  if (line == "")
    then pure []
    else do
      lines <- readToBlank
      pure (line :: lines)

readAndSave : IO ()
readAndSave = do
  content <- readToBlank
  filename <- getLine
  Right _ <- (writeFile filename (unlines content))
    | Left err => (putStrLn ("ERR" ++ show err))
  pure ()

readLinesFile : (file : File) -> IO (Either FileError (n ** Vect n String))
readLinesFile file = do
  eof <- fEOF file
  if eof
    then pure (Right (_ ** []))
    else do
      Right line <- fGetLine file
        | Left err => pure (Left err)
      Right (n ** lines) <- readLinesFile file
        | Left err => pure (Left err)
      pure (Right (_ ** line :: lines))

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
  Right file <- openFile filename Read
    | Left _ => pure (_ ** [])
  Right vec <- readLinesFile file
    | Left _ => pure (_ ** [])
  pure vec


text:
import Effects
import Effect.StdIO
import IdrisNet.UDP.UDPServer
import DNSParser
import DNS
import IdrisNet.Socket

dnsTest : List DomainFragment ->
          SocketAddress ->
          Port ->
          { [UDPSERVER UDPBound, STDIO, DNSPARSER ()] ==>
            [UDPSERVER (), STDIO, DNSPARSER ()] } Eff IO ()
dnsTest domain remote_host remote_port = with Eff do
  let dns_pckt = mkDNSRequest 1337 domain DNSQTypeA DNSQClassIN
  case encodeDNS dns_pckt of
    Left err => with Eff do putStr $ "Error encoding DNS packet... " ++ show err
                            udpClose
    Right pckt => with Eff do
      UDPSuccess w_len <- udpWritePacket remote_host remote_port dns pckt
        | UDPFailure err => with Eff do putStr ("Error sending packet: " ++ (show err))
                                        udpFinalise
        | UDPRecoverableError err => with Eff do putStr ("Error sending packet: " ++ (show err) ++ "\n")
                                                 udpClose
      UDPSuccess (addr, Just (dns_pckt, len, ptr)) <- udpReadPacket' dns 1024
        | UDPSuccess (addr, Nothing) => with Eff do putStr "Error in readPacket... :'(\n"
                                                    udpClose
        | UDPFailure err => with Eff do putStr ("Error receiving: " ++ (show err) ++ "\n")
                                        udpFinalise
        | UDPRecoverableError err => with Eff do putStr ("Error receiving: " ++ (show err) ++ "\n")
                                                 udpClose
      parsed_dns <- parseDNS ptr len dns_pckt
      case parsed_dns of
        Left err => with Eff do putStr $ "Error decoding: " ++ show err ++ "\n"
                                udpClose
        Right decoded_dns => with Eff do putStr $ "Decoded successfully! " ++ (show decoded_dns)
                                         udpClose

dnsRespTest : List DomainFragment ->
              Port ->
              SocketAddress ->
              Port ->
              { [UDPSERVER (), STDIO, DNSPARSER ()] } Eff IO ()
dnsRespTest domain local_port remote_host remote_port =
  case !(udpBind Nothing local_port) of
    UDPSuccess _ => dnsTest domain remote_host remote_port
    UDPFailure err => putStr ("Error connecting: " ++ (show err))
    UDPRecoverableError err => putStr ("Error connecting: " ++ (show err))

getDomainFragment : IO (List DomainFragment)
getDomainFragment = do
  putStrLn "Enter a domain name:"
  map ((split ((==) '.')) . trim) getLine

main : IO ()
main = run (dnsRespTest !getDomainFragment 4099 (IPv4Addr 138 251 206 2) 53) *> main


text:
module Utils.Show

import Data.List

export
show_record : String -> List (String, String) -> String
show_record adt_name fields = adt_name <+> " { " <+> (concat $ intersperse "; " $ map (\(a,b) => a <+> " = " <+> b) $ fields) <+> " }"