text:
||| A `Sink` is a monadic streaming function that consumes
||| data but produces no relevant output.
module Rhone.JS.Sink

import Control.Category
import Control.Monad.Dom
import Data.Maybe
import Data.MSF
import JS
import Text.Html
import Web.Dom
import Web.Html

%default total

||| Sets the innerHTML property of the referenced node to
||| the input string value.
export %inline
innerHtml : LiftJSIO m => ElemRef t -> MSF m String ()
innerHtml = arrM . rawInnerHtmlAt

||| Replaces the target's child nodes with a `Text` node
||| displaying the input `String`. The `String` will be
||| properly escaped before being inserted.
export
text : LiftJSIO m => ElemRef t -> MSF m String ()
text ref = escape ^>> innerHtml ref

--------------------------------------------------------------------------------
--          Attributes
--------------------------------------------------------------------------------

||| Sets or removes the attribute of the given name
||| at the given target element.
export
attribute :  LiftJSIO m
          => (name : String)
          -> MSF m (NP I [ElemRef t, Maybe String]) ()
attribute name =
  arrM $ \[ref,m] => liftJSIO $ do
    el <- castElementByRef {t2 = Element} ref
    case m of
      Just s  => setAttribute el name s
      Nothing => removeAttribute el name

||| Sets or unsets the attribute of the given element.
export %inline
attributeAt :  LiftJSIO m
            => (name : String)
            -> ElemRef t
            -> MSF m (Maybe String) ()
attributeAt = firstArg . attribute

||| Sets the attribute of the given name at the given target element.
export
attribute_ :  LiftJSIO m
           => (name : String)
           -> MSF m (NP I [ElemRef t, String]) ()
attribute_ name = (\[a,b] => [a,Just b]) ^>> attribute name

||| Sets or unsets the attribute of the given element.
export %inline
attributeAt_ :  LiftJSIO m
             => (name : String)
             -> ElemRef t
             -> MSF m String ()
attributeAt_ = firstArg . attribute_

||| Sets or unsets the boolean attribute of the given name at
||| the given target element.
export
boolAttribute :  LiftJSIO m
              => (name : String)
              -> MSF m (NP I [ElemRef t, Bool]) ()
boolAttribute name = (\[a,b] => [a,toMaybe b ""]) ^>> attribute name

||| Sets or unsets the `disabled` attribute of the given element.
export %inline
disabled : LiftJSIO m => MSF m (NP I [ElemRef t, Bool]) ()
disabled = boolAttribute "disabled"

||| Sets or unsets the `disabled` attribute of the given element.
export %inline
disabledAt : LiftJSIO m => ElemRef t -> MSF m Bool ()
disabledAt = firstArg disabled

||| Sets or unsets the `hidden` attribute of the given element.
export %inline
hidden : LiftJSIO m => MSF m (NP I [ElemRef t, Bool]) ()
hidden = boolAttribute "hidden"

||| Sets or unsets the `hidden` attribute of the given element.
export %inline
hiddenAt : LiftJSIO m => ElemRef t -> MSF m Bool ()
hiddenAt = firstArg hidden

||| Sets the `class` attribute of the given element.
export %inline
class : LiftJSIO m => MSF m (NP I [ElemRef t, String]) ()
class = attribute_ "class"

||| Sets the `class` attribute of the given element.
export %inline
classAt : LiftJSIO m => ElemRef t -> MSF m String ()
classAt = firstArg class

--------------------------------------------------------------------------------
--          Input Validation
--------------------------------------------------------------------------------

||| Interface for DOM elements that can have a custom
||| validity message set.
public export
interface SafeCast t => SetValidity t where
  setValidityMessage : t -> String -> JSIO ()

export
SetValidity HTMLButtonElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLFieldSetElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLInputElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLObjectElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLOutputElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLSelectElement where
  setValidityMessage = setCustomValidity

export
SetValidity HTMLTextAreaElement where
  setValidityMessage = setCustomValidity

export
setValidityMessageAt : SetValidity t => LiftJSIO m => ElemRef t -> String -> m ()
setValidityMessageAt ref s =
  liftJSIO (getElementByRef ref >>= (`setValidityMessage` s))

||| Sets a custom validity message at the given target element
export
validityMessageAt : SetValidity t => LiftJSIO m => ElemRef t -> MSF m String ()
validityMessageAt = arrM . setValidityMessageAt

||| Sets or unsets a custom validity message at the given target element
||| depending on whether the input value is a `Left`.
export
leftInvalid : SetValidity t => LiftJSIO m => ElemRef t -> MSF m (Either String x) ()
leftInvalid ref = either id (const "") ^>> validityMessageAt ref

--------------------------------------------------------------------------------
--          Value
--------------------------------------------------------------------------------

public export
interface SafeCast t => SetValue t where
  setValue' : String -> t -> JSIO ()

public export
SetValue HTMLButtonElement where
  setValue' = (value =.)

public export
SetValue HTMLDataElement where
  setValue' = (value =.)

public export
SetValue HTMLInputElement where
  setValue' = (value =.)

public export
SetValue HTMLOptionElement where
  setValue' = (value =.)

public export
SetValue HTMLOutputElement where
  setValue' = (value =.)

public export
SetValue HTMLParamElement where
  setValue' = (value =.)

public export
SetValue HTMLSelectElement where
  setValue' = (value =.)

public export
SetValue HTMLTextAreaElement where
  setValue' = (value =.)

public export
SetValue RadioNodeList where
  setValue' = (value =.)

export
setValue : LiftJSIO m => SetValue t => ElemRef t -> String -> m ()
setValue r s = getElementByRef r >>= liftJSIO . setValue' s

export
value : LiftJSIO m => SetValue t => MSF m (NP I [ElemRef t,String]) ()
value = arrM $ \[r,s] => setValue r s

export %inline
valueOf : LiftJSIO m => SetValue t => ElemRef t -> MSF m String ()
valueOf = firstArg value

export
setChecked : LiftJSIO m => Bool -> HTMLInputElement -> m ()
setChecked b el = liftJSIO $ set (checked el) b

export
checked : LiftJSIO m => MSF m (NP I [ElemRef HTMLInputElement,Bool]) ()
checked = arrM $ \[r,b] => getElementByRef r >>= setChecked b

export %inline
isChecked : LiftJSIO m => ElemRef HTMLInputElement -> MSF m Bool ()
isChecked = firstArg checked

namespace LocalStorage
  export
  setItem : LiftJSIO m => MSF m (NP I [String,String]) ()
  setItem = arrM $ \[k,v] =>
    liftJSIO (window >>= localStorage >>= (\s => setItem s k v))

  export %inline
  setItemAt : LiftJSIO m => (key : String) -> MSF m String ()
  setItemAt = firstArg setItem


text:
doit3times : (f : x -> x) -> (n : x) -> x
doit3times f = f . f . f

test_doit3times1 : doit3times (\n => n + 2) 3 = 9
test_doit3times1 = Refl

test_doit3times2 : doit3times (\b => not b) True = False
test_doit3times2 = Refl

fltr : (test : a -> Bool) -> (l : List a) -> List a
fltr test [] = []
fltr test (x :: xs) =
    if test x
        then x :: fltr test xs
        else fltr test xs

evenb : (n : Nat) -> Bool
evenb Z = True
evenb (S (S k)) = evenb k
evenb k = False

test_filter1 : fltr Main.evenb [1, 2, 3, 4] = [2, 4]
test_filter1 = Refl

test_filter2 : fltr (\l => length l == 1) [[1, 2], [3], [4], [5, 6, 7], [], [8]] = [[3], [4], [8]]
test_filter2 = Refl

oddb : (n : Nat) -> Bool
oddb Z = False
oddb (S Z) = True
oddb (S (S k)) = oddb k

count_oddmembers : (l : List Nat) -> Nat
count_oddmembers l = length $ fltr oddb l

test_count_oddmembers1 : count_oddmembers [1, 0, 3, 1, 4, 5] = 4
test_count_oddmembers1 = Refl

test_count_oddmembers2 : count_oddmembers [0, 2, 4] = 0
test_count_oddmembers2 = Refl

test_count_oddmembers3 : count_oddmembers [] = 0
test_count_oddmembers3 = Refl

test_anon_fn : doit3times (\n => mult n n) 2 = 256
test_anon_fn = Refl

filter_even_gt7 : (l : List Nat) -> List Nat
filter_even_gt7 = filter evenb . filter (\n => n > 7)

test_filter_even_gt7_1 : filter_even_gt7 [1, 2, 6, 9, 10, 3, 12, 8] = [10, 12, 8]
test_filter_even_gt7_1 = Refl

test_filter_even_gt7_2 : filter_even_gt7 [5, 2, 6, 19, 129] = []
test_filter_even_gt7_2 = Refl

partn : (test : a -> Bool) -> (l : List a) -> (List a, List a)
partn test [] = ([], [])
partn test (x :: xs) =
    let
        (ts, fs) = partn test xs
    in
        if test x
            then (x :: ts, fs)
            else (ts, x :: fs)

test_partition1 : partn Main.oddb [1, 2, 3, 4, 5] = ([1, 3, 5], [2, 4])
test_partition1 = Refl

test_partition2 : partn (\x => False) [5, 9, 0] = ([], [5, 9, 0])
test_partition2 = Refl

test_map1 : map (\x => 3 + x) [2, 0, 2] = [5, 3, 5]
test_map1 = Refl

test_map2 : map Main.oddb [2, 1, 2, 5] = [False, True, False, True]
test_map2 = Refl

test_map3 : map (\n => [evenb n, oddb n]) [2, 1, 2, 5] = [[True, False], [False, True], [True, False], [False, True]]
test_map3 = Refl

ext: idr


text:
module Main

putFizzbuzz : Int -> IO ()
putFizzbuzz num = putStrLn putFizzOrBuzz where
  putFizzOrBuzz =  if mod num 15 == 0
                then "fizzbuzz"
                else if mod num 3 == 0
                then "fizz"
                else if mod num 5 == 0
                then "buzz"
                else cast num

fizzbuzz : Int -> IO ()
fizzbuzz num = fizzbuzzes [1..num] where
  fizzbuzzes Nil = putStrLn ""
  fizzbuzzes (x :: xs) = do putFizzbuzz x
                            fizzbuzzes xs

main : IO ()
main = fizzbuzz 15

max_stars_repo_name: britter/fizzbuzz-idris

max_issues_repo_name: britter/fizzbuzz-idris

max_forks_repo_name: britter/fizzbuzz-idris


text:
||| In this Kata you'll learn Bisimulation
module BisiProof

%default total
%access export

namespace Bisimulation

	--This is the definition of Bisimulation: the inductive parts should
	--equivalent, and the coinductive parts should bisimulate.
	--With Cubical Model we can prove that Bisimulation is an equivlance,
	--aka Coinductive Proof Principle.
	--However, you don't have Cubical Model in Idris :(

	infixr 10 :=:
	public export
	codata Bisimulation : (x : Stream a) -> (y : Stream a) -> Type where
		(:=:) : {x : Stream a} -> {y : Stream a} ->
						(head x = head y) ->
						(Bisimulation (tail x) (tail y)) ->
						(Bisimulation x y)

||| Example: consider an infinite list of ones
Ones : Stream Nat
Ones = 1 :: Ones

onesBisimulation : Bisimulation Ones Ones
onesBisimulation = Refl :=: onesBisimulation

public export
Odd : Stream a -> Stream a
Odd l = head (tail l) :: Odd (tail (tail l))

public export
Even : Stream a -> Stream a
Even l = head l :: Even (tail (tail l))

public export
Merge : Stream a -> Stream a -> Stream a
Merge a b = head a :: head b :: Merge (tail a) (tail b)

public export
MergeOddEvenIsBisimulation : (x : Stream a) -> Bisimulation (Merge (Even x) (Odd x)) x
MergeOddEvenIsBisimulation x = Refl :=: Refl :=: MergeOddEvenIsBisimulation (tail . tail $ x)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Cordova

import Js.Utils

export
onDeviceReady : JS_IO () -> JS_IO ()
onDeviceReady x =
  jscall "document.addEventListener('deviceready', %0, false)" (JsFn (() -> JS_IO ()) -> JS_IO ()) (MkJsFn (\() => x))

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Control.Monad.Codensity

import Control.Monad.Free

%access public export
%default total

data Codensity : (m : Type -> Type) -> (a : Type) -> Type where
  Codense : ({b : Type} -> (a -> m b) -> m b) -> Codensity m a

runCodensity : Codensity m a -> ({b : Type} -> (a -> m b) -> m b)
runCodensity (Codense c) = c

Functor (Codensity f) where
  map f (Codense c) = Codense (\k => c (k . f))

Applicative (Codensity f) where
  pure x = Codense (\k => k x)
  (Codense f) <*> (Codense x) = Codense (\k => x (\x' => f (\f' => k (f' x'))))

Monad (Codensity f) where
  (Codense x) >>= f = Codense (\k => x (\x' => runCodensity (f x') k))

liftCodensity : Monad m => m a -> Codensity m a
liftCodensity x = Codense (x >>=)

lowerCodensity : Monad m => Codensity m a -> m a
lowerCodensity (Codense c) = c pure

Functor f => MonadFree (Codensity (Free f)) f where
  wrap x = Codense (\k => wrap (map (>>= k) (map lowerCodensity x)))

max_stars_repo_name: ajhamwood/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
import Data.Vect

myZipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
myZipWith f [] [] = []
myZipWith f (x :: xs) (y :: ys) = f x y :: myZipWith f xs ys

-- ctrl alt a on zipWith
-- ctrl alt c on first Vect argument
-- ctrl alt c on second Vect argument
-- ctrl alt s on first hole
-- ctrl alt c on second Vect argument in second pattern
-- ctrl alt s on last hole
-- DONE

myAppend : Vect n a -> Vect m a -> Vect (n + m) a
myAppend [] ys = ys
myAppend (x :: xs) ys = x :: myAppend xs ys

-- type: write or extract a top-level function signature
-- define: doing stuff on the left
-- refine: doing stuff on the right

myTake : (m : Nat) -> Vect (m + n) a -> Vect m a
myTake Z xs = []
myTake (S k) (x :: xs) = x :: (myTake k xs) -- findet Idris nicht automatisch

myDrop : (m : Nat) -> Vect (m + n) a -> Vect n a
myDrop Z xs = xs
myDrop (S k) (x :: xs) = ?hole_2

myReplicate : (n : Nat) -> a -> Vect n a
myReplicate Z x = []
myReplicate (S k) x = x :: myReplicate k x -- wird automatisch gefunden

max_stars_repo_name: fthomas/tdd-talk

max_issues_repo_name: fthomas/tdd-talk

max_forks_repo_name: fthomas/tdd-talk


text:
module InsSort

import Data.Vect

%default total

insert : Ord a => a -> Vect n a -> Vect (S n) a
insert x [] = [x]
insert x (y :: ys) = case compare x y of
                          GT => y :: insert x ys
                          _ => x  :: y :: ys

isort : Ord a => Vect n a -> Vect n a
isort [] = []
isort (x :: xs) = insert x (isort xs)

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 Chapter3

import TypesAndFunctions
import Category
import Isomorphism
import Universality
import Naturality

%default total

Exercise_3_1_1 : {cat : Category} -> {a, b, c : Object cat} ->
  Isomorphic {cat} a b -> Bijection (Morphism cat a c) (Morphism cat b c)
Exercise_3_1_1 {cat}
  (abIsomorphism ** (baIsomorphism ** ((isLeftInverse, isRightInverse)))) =
    ((\f : Morphism cat a c => f .* baIsomorphism) **
     ((\g : Morphism cat b c => g .* abIsomorphism) **
     ((\f' : Morphism cat a c =>
       let
         assoc = Associativity cat f' baIsomorphism abIsomorphism
         rightId = RightIdentity cat f'
       in
       replace {p=(\f'' => f'' = f')} (sym assoc)
         (replace {p=(\z => f' .* z = f')} (sym isLeftInverse) rightId),
      \g' : Morphism cat b c =>
       let
         assoc = Associativity cat g' abIsomorphism baIsomorphism
         rightId = RightIdentity cat g'
       in
       replace {p=(\g'' => g'' = g')} (sym assoc)
         (replace {p=(\z => g' .* z = g')} (sym isRightInverse) rightId)))))

Exercise_3_1_2 : {cat : Category} -> (a : Object cat) -> Isomorphic {cat} a a
Exercise_3_1_2 a =
  (catId a ** (catId a ** (LeftIdentity _ _, LeftIdentity _ _)))

Exercise_3_1_3 : {cat : Category} -> {a, b : Object cat} ->
  IsTerminal {cat} a -> IsTerminal {cat} b -> Isomorphic {cat} a b
Exercise_3_1_3 aIsTerminal bIsTerminal =
  (fst (bIsTerminal a) ** (fst (aIsTerminal b) **
    (IdOnlyTerminalEndomorphism aIsTerminal
      (fst (aIsTerminal b) .* fst (bIsTerminal a)),
    (IdOnlyTerminalEndomorphism bIsTerminal
      (fst (bIsTerminal a) .* fst (aIsTerminal b))))))

Exercise_3_1_4 : {cat : Category} -> {a, b : Object cat} ->
  (aIsTerminal : IsTerminal {cat} a) -> (bIsTerminal : IsTerminal {cat} b) ->
  IsUnique {cat} {a} {b}
    (IsIsomorphism {cat} {a} {b})
    (fst (Exercise_3_1_3 {cat} {a} {b} aIsTerminal bIsTerminal))
Exercise_3_1_4 {cat} {a} {b} aIsTerminal bIsTerminal =
  ((fst (aIsTerminal b) **
   (IdOnlyTerminalEndomorphism aIsTerminal _,
    IdOnlyTerminalEndomorphism bIsTerminal _)),
   \g : Morphism cat a b,
    g' : DPair (Morphism cat b a) (IsInverse {cat} g) =>
      snd (snd (bIsTerminal a)) g ())

Exercise_3_2_1_left : {cat : Category} -> {a, b, x, y : Object cat} ->
  (fInv : Morphism cat b a) -> (g : Morphism cat x y) ->
  (h : Morphism cat a x) ->
  ((preCompose {cat} {a=b} {b=a} {c=y} fInv) .
    (postCompose {cat} {a} {b=x} {c=y} g)) h =
  After cat {a=b} {b=x} {c=y} g (After cat {a=b} {b=a} {c=x} h fInv)
Exercise_3_2_1_left fInv g h = Associativity cat g h fInv

Exercise_3_2_1_right : {cat : Category} -> {a, b, x, y : Object cat} ->
  (fInv : Morphism cat b a) -> (g : Morphism cat x y) ->
  (h : Morphism cat a x) ->
  ((postCompose {cat} {a=b} {b=x} {c=y} g) .
    (preCompose {cat} {a=b} {b=a} {c=x} fInv)) h =
  After cat {a=b} {b=x} {c=y} g (After cat {a=b} {b=a} {c=x} h fInv)
Exercise_3_2_1_right fInv g h = Refl

Exercise_3_3_1 : {cat : Category} ->
  {observerA, observerB : Object cat} ->
  (beta : ObserverChange {cat} observerA observerB) ->
  Morphism cat observerB observerA
Exercise_3_3_1 = ObserverChangeInducedMorphism

Exercise_3_3_2 : {cat : Category} ->
  {observerA, observerB : Object cat} ->
  (beta : ObserverChange {cat} observerA observerB) ->
  (natural : ObserverChangeIsNatural {cat} {observerA} {observerB} beta) ->
  (y : Object cat) -> (g : Morphism cat observerA y) ->
  beta y g =
    After cat {a=observerB} {b=observerA} {c=y}
      g (Exercise_3_3_1 {cat} {observerA} {observerB} beta)
Exercise_3_3_2 beta natural y g =
  appEq {x=g} (ObserverChangeIsPreComposition beta natural y)

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
module Main

%default total

data RunIO : Type -> Type where
  Quit : a -> RunIO a
  Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b

(>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b
(>>=) = Do

greet : RunIO ()
greet = do
  putStrLn "Enter your name: "
  name <- getLine
  if name == ""
    then do putStrLn "Bye bye!"
            Quit ()
    else do putStrLn ("Hello " ++ name)
            greet

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> RunIO a -> IO (Maybe a)
run Dry _ = pure Nothing
run _ (Quit value) = pure (Just value)
run (More fuel) (Do c f) = do
  res <- c
  run fuel (f res)

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = do
  run forever greet
  pure ()

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
import Data.Vect
import Data.Vect.Elem
import Data.List
import Data.Strings

import Decidable.Equality

%default total

public export
data GameState : Type where
  NotRunning : GameState
  Running : (guesses : Nat) -> (letters : Nat) -> GameState

letters : String -> List Char
letters str = nub (map toUpper (unpack str))

data GuessResult = Correct | Incorrect

export
data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
  NewGame : (word : String) ->
            GameCmd () NotRunning (const (Running 6 (length (letters word))))

  Won :  GameCmd () (Running (S guesses) 0) (const NotRunning)
  Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning)

  Guess : (c : Char) ->
          GameCmd GuessResult
                  (Running (S guesses) (S letters))
                  (\res => case res of
                                Correct => Running (S guesses) letters
                                Incorrect => Running guesses (S letters))

  ShowState : GameCmd () state (const state)
  Message : String -> GameCmd () state (const state)
  ReadGuess : GameCmd Char state (const state)

  Pure : (res : ty) -> GameCmd ty (state_fn res) state_fn
  (>>=) : GameCmd a state1 state2_fn ->
          ((res : a) -> GameCmd b (state2_fn res) state3_fn) ->
          GameCmd b state1 state3_fn

namespace Loop
  public export
  data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
    (>>=) : GameCmd a state1 state2_fn ->
            ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) ->
            GameLoop b state1 state3_fn
    Exit : GameLoop () NotRunning (const NotRunning)

gameLoop : {letters : _} -> {guesses : _} ->
           GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
gameLoop {guesses} {letters} = do ShowState
                                  g <- ReadGuess
                                  ok <- Guess g
                                  case ok of
                                       Correct => case letters of
                                                       Z => do Won
                                                               ShowState
                                                               Exit
                                                       S k => do Message "Correct"
                                                                 gameLoop
                                       Incorrect => case guesses of
                                                         Z => do Lost
                                                                 ShowState
                                                                 Exit
                                                         S k => do Message "Incorrect"
                                                                   gameLoop

hangman : GameLoop () NotRunning (const NotRunning)
hangman = do NewGame "testing"
             gameLoop

data Game : GameState -> Type where
  GameStart : Game NotRunning
  GameWon : (word : String) -> Game NotRunning
  GameLost : (word : String) -> Game NotRunning
  InProgress : {letters : _} -> (word : String) -> (guesses : Nat) ->
               (missing : Vect letters Char) -> Game (Running guesses letters)

Show (Game g) where
  show GameStart = "Starting"
  show (GameWon word) = "Game won: word was " ++ word
  show (GameLost word) = "Game lost: word was " ++ word
  show (InProgress word guesses missing) = "\n" ++ pack (map hideMissing (unpack word))
                                        ++ "\n" ++ show guesses ++ " guesses left "
  where
    hideMissing : Char -> Char
    hideMissing c = if c `elem` missing then '-' else c

data Fuel = Dry | More (Lazy Fuel)

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

data GameResult : (ty : Type) -> (ty -> GameState) -> Type where
  OK : (res : ty) -> Game (outState_fn res) -> GameResult ty outState_fn
  OutOfFuel : GameResult ty outState_fn

ok : (res : ty) -> Game (outstate_fn res) -> IO (GameResult ty outstate_fn)
ok res st = pure (OK res st)

runCmd : Fuel -> Game inState -> GameCmd ty inState outState_fn -> IO (GameResult ty outState_fn)
runCmd fuel state (NewGame word) = ok () (InProgress (toUpper word) _ (fromList (letters word)))
runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word)
runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word)
runCmd fuel (InProgress word _ missing) (Guess c) = case isElem c missing of
                                                         Yes prf => ok Correct (InProgress word _ (removeElem c missing))
                                                         No contra => ok Incorrect (InProgress word _ missing)
runCmd fuel state ShowState = do printLn state
                                 ok () state
runCmd fuel state (Message str) = do putStrLn str
                                     ok () state
runCmd (More fuel) state ReadGuess = do putStr "Guess: "
                                        input <- getLine
                                        case unpack input of
                                             [x] => if isAlpha x
                                                       then ok (toUpper x) state
                                                       else do putStrLn "Invalid input"
                                                               runCmd fuel state ReadGuess
                                             _ => do putStrLn "Invalid input"
                                                     runCmd fuel state ReadGuess
runCmd fuel state (Pure res) = ok res state
runCmd fuel state (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel state cmd
                                                         | OutOfFuel => pure OutOfFuel
                                      runCmd fuel newSt (next cmdRes)
runCmd Dry _ _ = pure OutOfFuel

run : Fuel -> Game inState -> GameLoop ty inState outState_fn -> IO (GameResult ty outState_fn)
run Dry _ _ = pure OutOfFuel
run (More fuel) st Exit = ok () st
run (More fuel) st (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel st cmd
                                                          | OutOfFuel => pure OutOfFuel
                                       run fuel newSt (next cmdRes)

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = do run forever GameStart hangman
          pure ()


text:
module Protocol.IDE.FileContext

import Protocol.SExp

import public Libraries.Text.Bounded

%default total

public export
record FileContext where
  constructor MkFileContext
  file : String
  range : Bounds

export
SExpable FileContext where
  toSExp fc =
    SExpList [ SExpList
               [ SymbolAtom "filename", toSExp fc.file ]
             , SExpList [ SymbolAtom "start"
                        , IntegerAtom (cast fc.range.startLine)
                        , IntegerAtom (cast fc.range.startCol)
                        ]
             , SExpList [ SymbolAtom "end"
                        , IntegerAtom (cast fc.range.endLine)
                        , IntegerAtom (cast fc.range.endCol)
                        ]
             ]

export
FromSExpable FileContext where
  fromSExp (SExpList [ SExpList
               [ SymbolAtom "filename", filenameSExp ]
             , SExpList [ SymbolAtom "start"
                        , IntegerAtom startLine
                        , IntegerAtom startCol
                        ]
             , SExpList [ SymbolAtom "end"
                        , IntegerAtom endLine
                        , IntegerAtom endCol
                        ]
             ]) = do file <- fromSExp filenameSExp
                     pure $ MkFileContext {file, range = MkBounds
                       { startLine = cast startLine
                       , startCol  = cast startCol
                       , endLine   = cast endLine
                       , endCol    = cast endCol
                       }}
  fromSExp _ = Nothing


text:
-- ---------------------------------------------------------------- [ Dict.idr ]
-- Module    : Dict.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

module Data.AVL.Test.Dict

import Test.Unit
import Test.Random.Values

import Data.AVL.Dict

%access export

kvlist1 : List (Integer, Integer)
kvlist1 = rndListIntKVU 123456789 (0,100) 20

-- ------------------------------------------------------------ [ Construction ]

testBuilding : IO Bool
testBuilding = genericTest
    (Just "List, Building" )
    (Dict.size $ Dict.fromList kvlist1)
    20
    (==)

-- ---------------------------------------------------------------- [ Updating ]
partial
testUpdate : IO Bool
testUpdate = genericTest
    (Just "Update")
    (Dict.toList $ Dict.update 2 (*2) $ Dict.fromList [(1,2), (2,3), (3,4), (5,3)])
    [(1,2), (2,6), (3,4), (5,3)]
    (==)

partial
testHas : IO Bool
testHas = genericTest
   (Just "Has value")
   (hasValue 6 $ Dict.fromList [(1,2), (2,6), (3,4)])
   (True)
   (==)

-- ----------------------------------------------------------------- [ Queries ]
partial
testLookup : IO Bool
testLookup = genericTest
    (Just "Lookup")
    (Dict.lookup 1 $ Dict.fromList [(1,2), (2,3), (3,4)])
    (Just 2)
    (==)

partial
testKVs : IO Bool
testKVs = genericTest
    (Just "KV Pair Extraction")
    (keys given, values given)
    ([1,2,3], [5,6,7])
    (==)
  where
    given : Dict Int Int
    given = Dict.fromList [(1,5), (2,6), (3,7)]

-- --------------------------------------------------------- [ Implementations ]

partial
testFunctorWorksOnValues : IO Bool
testFunctorWorksOnValues = genericTest
    (Just "Functor works on values")
    (Dict.toList $ (* 2) <$> Dict.fromList [("a", 1), ("b", 2)])
    [("a", 2), ("b", 4)]
    (==)

partial
testTraversableTraversesOnValues : IO Bool
testTraversableTraversesOnValues = genericTest
    (Just "Traversable works on values")
    (traverse Just $ Dict.fromList [("a", 1), ("b", 2)])
    (Just $ Dict.fromList [("a", 1), ("b", 2)])
    (==)

partial
runTest : IO ()
runTest = do
  putStrLn "Testing Dict"
  putStrLn infoLine
  NonReporting.runTests [
      testBuilding
    , testLookup
    , testUpdate
    , testHas
    , testKVs
    , testFunctorWorksOnValues
    , testTraversableTraversesOnValues
  ]

-- --------------------------------------------------------------------- [ 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 Cgi

sayHello : CGIProg [] ()
sayHello = output "Hello, world!"

main : IO ()
main = runCGI [initCGIState] sayHello

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module System.File.Handle

import public System.File.Error
import public System.File.Mode
import System.File.Support
import public System.File.Types

%default total

%foreign support "idris2_openFile"
         "node:support:openFile,support_system_file"
prim__open : String -> String -> PrimIO FilePtr

%foreign support "idris2_closeFile"
         "node:lambda:(fp) => require('fs').closeSync(fp.fd)"
prim__close : FilePtr -> PrimIO ()

||| Open the given file name with the specified mode.
|||
||| @ f the file name to open
||| @ m the mode to open the file with
export
openFile : HasIO io => (f : String) -> (m : Mode) -> io (Either FileError File)
openFile f m
    = do res <- primIO (prim__open f (modeStr m))
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (FHandle res)

||| Close the given file handle.
|||
||| @ fh the file handle to close
export
closeFile : HasIO io => (fh : File) -> io ()
closeFile (FHandle f) = primIO (prim__close f)

||| Perform a given operation on successful file open
||| and ensure the file is closed afterwards or perform
||| a different operation if the file fails to open.
export
withFile : HasIO io => (filename : String) ->
                       Mode ->
                       (onError : FileError -> io a) ->
                       (onOpen  : File -> io (Either a b)) ->
                       io (Either a b)
withFile filename mode onError onOpen =
  do Right h <- openFile filename mode
       | Left err => Left <$> onError err
     res <- onOpen h
     closeFile h
     pure res


text:
module Http.RawResponse

%access public export

data RawResponse a = MkRawResponse a

implementation Eq a => Eq (RawResponse a) where
  (MkRawResponse a) == (MkRawResponse b) = a == b
  (MkRawResponse a) /= (MkRawResponse b) = a /= b

implementation Show a => Show (RawResponse a) where
  show (MkRawResponse a) = show a

implementation Functor RawResponse where
  map f (MkRawResponse a) = MkRawResponse (f a)

implementation Applicative RawResponse where
  pure = MkRawResponse
  (MkRawResponse f) <*> (MkRawResponse a) = MkRawResponse (f a)

implementation Monad RawResponse where
  (MkRawResponse a) >>= f = f a

implementation Foldable RawResponse where
  foldr f z (MkRawResponse a) = f a z

implementation Traversable RawResponse where
  traverse f (MkRawResponse x) = [| MkRawResponse (f x) |]

implementation Semigroup a => Semigroup (RawResponse a) where
  (MkRawResponse a) <+> (MkRawResponse b) = MkRawResponse (a <+> b)

implementation Monoid a => Monoid (RawResponse a) where
  neutral = MkRawResponse neutral

implementation Cast a (RawResponse a) where
  cast = pure
implementation Cast (RawResponse a) a where
  cast (MkRawResponse a) = a

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
module Equivalence

-- Proof that small-step and big-step semantics for
-- the simply-typed lambda calculus are equivalent.

import BigStep
import Step
import Subst
import Term

%default total
%access export

--------------------------
-- Begin: STEP => BIG-STEP

stepToBigStep : Step e1 e2 -> BigStep e2 e3 ->
                BigStep e1 e3
-- case split in the following order: (Step e1 e2), (BigStep e2 e3)
stepToBigStep (StApp1 x) (BStValue v) impossible
--
stepToBigStep (StApp1 x) (BStApp w s1 t1) = let ih = stepToBigStep x w
                                            in BStApp ih s1 t1
--
stepToBigStep (StApp2 x z) (BStValue v) impossible
--
stepToBigStep (StApp2 x z) (BStApp s1 t1 u) = let ih = stepToBigStep z t1
                                              in BStApp s1 ih u
--
stepToBigStep (StBeta x) y = BStApp (BStValue VAbs) (BStValue x) y
--
stepToBigStep (StFix x) (BStValue v) impossible
--
stepToBigStep (StFix x) (BStFix z w) = let ih = stepToBigStep x z
                                       in BStFix ih w
--
stepToBigStep StFixBeta y = BStFix (BStValue VAbs) y
--
stepToBigStep (StSucc x) (BStValue v) = case v of
  VAbs     impossible
  VZero    impossible
  VSucc v' => BStSucc $ stepToBigStep x (BStValue v')
--
stepToBigStep (StSucc x) (BStSucc y) = BStSucc $ stepToBigStep x y
--
stepToBigStep (StPred x) (BStValue v) impossible
--
stepToBigStep (StPred x) (BStPredZero z) = BStPredZero $ stepToBigStep x z
--
stepToBigStep (StPred x) (BStPredSucc y) = let ih = stepToBigStep x y
                                           in BStPredSucc ih
--
stepToBigStep StPredZero (BStValue v) = BStPredZero (BStValue VZero)
--
stepToBigStep (StPredSucc x) y = BStPredSucc (BStSucc y)
--
stepToBigStep (StIfz x) (BStValue v) impossible
--
stepToBigStep (StIfz x) (BStIfzZero z w) = let ih = stepToBigStep x z
                                           in BStIfzZero ih w
--
stepToBigStep (StIfz x) (BStIfzSucc w s) = let ih = stepToBigStep x w
                                           in BStIfzSucc ih s
--
stepToBigStep StIfzZero y = BStIfzZero (BStValue VZero) y
--
stepToBigStep (StIfzSucc x) y = BStIfzSucc (BStValue (VSucc x)) y

-- End: STEP => BIG-STEP
------------------------

-------------------------------
-- Begin: TRANSSTEP => BIG-STEP

transStepToBigStep : (TransStep e1 e2) -> (v : Value e2) ->
                     BigStep e1 e2
transStepToBigStep (TStRefl _)    v = BStValue v
transStepToBigStep (TStTrans x y) v = let ih = transStepToBigStep y v
                                      in stepToBigStep x ih

-- End: TRANSSTEP => BIG-STEP
-----------------------------

-------------------------------
-- Begin: BIG-STEP => TRANSSTEP

-- Congruence lemma for '(TApp _ e)':
congApp1 : TransStep e1 e2 -> TransStep (TApp e1 e) (TApp e2 e)
congApp1 (TStRefl e1)   = TStRefl (TApp e1 _)
congApp1 (TStTrans x y) = TStTrans (StApp1 x) (congApp1 y)

-- Congruence lemma for '(TApp e _)':
congApp2 : {v : Value e} ->
           TransStep e1 e2 -> TransStep (TApp e e1) (TApp e e2)
congApp2         (TStRefl e1)   = TStRefl (TApp _ e1)
congApp2 {v = v} (TStTrans x y) = TStTrans (StApp2 v x) (congApp2 {v = v} y)

-- Congruence lemma for '(Fix _)':
total congFix : TransStep e1 e2 -> TransStep (TFix e1) (TFix e2)
congFix (TStRefl e1)   = TStRefl (TFix e1)
congFix (TStTrans x y) = TStTrans (StFix x) (congFix y)

-- Congruence lemma for '(Succ _)':
congSucc : TransStep e1 e2 -> TransStep (TSucc e1) (TSucc e2)
congSucc (TStRefl e1)   = TStRefl (TSucc e1)
congSucc (TStTrans x y) = TStTrans (StSucc x) (congSucc y)

-- Congruence lemma for '(Pred _)':
congPred : TransStep e1 e2 -> TransStep (TPred e1) (TPred e2)
congPred (TStRefl e1)   = TStRefl (TPred e1)
congPred (TStTrans x y) = TStTrans (StPred x) (congPred y)

-- Congruence lemma for '(Ifz _ ez es)':
congIfz : TransStep e1 e2 -> TransStep (TIfz e1 ez es) (TIfz e2 ez es)
congIfz (TStRefl e1)   = TStRefl (TIfz e1 _ _)
congIfz (TStTrans x y) = TStTrans (StIfz x) (congIfz y)

bigStepToTransStep : BigStep e1 e2 -> (TransStep e1 e2, Value e2)
--
bigStepToTransStep (BStValue v) = (TStRefl _, v)
--
bigStepToTransStep (BStApp z w t1) =
  let (tst1, v1) = bigStepToTransStep z
      (tst2, v2) = bigStepToTransStep w
      (tst3, v3) = bigStepToTransStep t1
      tst = (congApp1 tst1) .++. (congApp2 {v = VAbs} tst2) .+. (StBeta v2) .++. tst3
  in (tst, v3)
--
bigStepToTransStep (BStFix y z) =
  let (tst1, v1) = bigStepToTransStep y
      (tst2, v2) = bigStepToTransStep z
      tst = (congFix tst1) .+. StFixBeta .++. tst2
  in (tst, v2)
--
bigStepToTransStep (BStSucc x) =
  let (tst1, v1) = bigStepToTransStep x
  in (congSucc tst1, VSucc v1)
--
bigStepToTransStep (BStPredZero y) =
  let (tst1, v1) = bigStepToTransStep y
      tst = congPred tst1 .+. StPredZero
  in (tst, VZero)
--
bigStepToTransStep (BStPredSucc x) =
  let (tst1, VSucc v1) = bigStepToTransStep x
      tst = (congPred tst1) .+. (StPredSucc v1)
  in (tst, v1)

bigStepToTransStep (BStIfzZero z w) =
  let (tst1, v1) = bigStepToTransStep z
      (tst2, v2) = bigStepToTransStep w
      tst = (congIfz tst1) .+. StIfzZero .++. tst2
  in (tst, v2)

bigStepToTransStep (BStIfzSucc w s) =
  let (tst1, VSucc v1) = bigStepToTransStep w
      (tst2, v2) = bigStepToTransStep s
      tst = (congIfz tst1) .+. (StIfzSucc v1) .++. tst2
  in (tst, v2)

-- End: BIG-STEP => TRANSSTEP
-----------------------------

-------------------------------------
-- Begin: CO-BIG-STEP => CO-TRANSSTEP

-- The relations 'CoTransStep' and 'CoBigStep' are not equivalent;
-- only one direction of the equivalence holds. To establish the
-- one-directional equivalence, the following lemma is needed, which
-- has the flavour of a progress lemma for big-step semantics:
-- (cf. the proof of Lemma 36 in "Coinductive big-step operational
-- semantics" by X. Leroy and H. Grall)
coBigStepProgress : (e1 : Term [] t) -> (e2 : Term [] t) ->
                    CoBigStep e1 e2 ->
                    Either (Value e1) (b : Term [] t ** (Step e1 b, CoBigStep b e2))
coBigStepProgress (TVar _) e2 cbst impossible
--
coBigStepProgress (TAbs _) e2 cbst = Left VAbs
--
coBigStepProgress (TApp x y) (TApp x y) (CoBStValue v) impossible
coBigStepProgress (TApp x y) e2 (CoBStApp {e=e2} {e1'=e1'} {e2'=e2'} cbst1 cbst2 cbst3) =
  case coBigStepProgress x (TAbs e1') cbst1 of
       Left v => case v of
                      VAbs => case cbst1 of
                                   (CoBStValue {e=(TAbs e)} v') => case coBigStepProgress y e2' cbst2 of
                                                                        Left v'' => let eq     = coBigStepValueIrreducible cbst2 v''
                                                                                cbst3' = replace {P = \z => CoBigStep (subst z First e) e2} (sym eq) cbst3
                                                                                in Right (_ ** (StBeta v'', cbst3'))
                                                                        Right (b ** (st, cbst)) => let cbst' = CoBStApp (CoBStValue v) cbst cbst3
                                                                                in Right (_ ** (StApp2 VAbs st, cbst'))
       Right (b ** (st, cbst)) => let st'   = StApp1 st
                                      cbst' = CoBStApp cbst cbst2 cbst3
                                  in Right (_ ** (st', cbst'))
--
coBigStepProgress (TFix x) (TFix x) (CoBStValue v) impossible
coBigStepProgress (TFix x) e2 (CoBStFix {e'=e'} cbst1 cbst2) =
  case coBigStepProgress x (TAbs e') cbst1 of
       Left v => case v of
                      VAbs => case cbst1 of
                                   (CoBStValue {e=(TAbs e)} v) => Right (_ ** (StFixBeta, cbst2))
       Right (b ** (st, cbst)) => let st'   = StFix st
                                      cbst' = CoBStFix cbst cbst2
                                  in Right (_ ** (st', cbst'))
--
coBigStepProgress TZero e2 _ = Left VZero
--
coBigStepProgress (TSucc x) (TVar y) cbst impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStValue _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStApp _ _ _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStFix _ _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStSucc _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStPredZero _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStPredSucc _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStIfzZero _ _) impossible
coBigStepProgress (TSucc _) (TApp _ _) (CoBStIfzSucc _ _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStValue _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStApp _ _ _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStFix _ _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStSucc _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStPredZero _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStPredSucc _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStIfzZero _ _) impossible
coBigStepProgress (TSucc _) (TFix _) (CoBStIfzSucc _ _) impossible
coBigStepProgress (TSucc _) TZero (CoBStValue _) impossible
coBigStepProgress (TSucc _) TZero (CoBStApp _ _ _) impossible
coBigStepProgress (TSucc _) TZero (CoBStFix _ _) impossible
coBigStepProgress (TSucc _) TZero (CoBStSucc _) impossible
coBigStepProgress (TSucc _) TZero (CoBStPredZero _) impossible
coBigStepProgress (TSucc _) TZero (CoBStPredSucc _) impossible
coBigStepProgress (TSucc _) TZero (CoBStIfzZero _ _) impossible
coBigStepProgress (TSucc _) TZero (CoBStIfzSucc _ _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStValue _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStApp _ _ _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStFix _ _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStSucc _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStPredZero _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStPredSucc _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStIfzZero _ _) impossible
coBigStepProgress (TSucc _) (TPred _) (CoBStIfzSucc _ _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStValue _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStApp _ _ _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStFix _ _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStSucc _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStPredZero _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStPredSucc _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStIfzZero _ _) impossible
coBigStepProgress (TSucc _) (TIfz _ _ _) (CoBStIfzSucc _ _) impossible
coBigStepProgress (TSucc y) (TSucc y) (CoBStValue v) = Left v
coBigStepProgress (TSucc x) (TSucc y) (CoBStSucc cbst) =
  case coBigStepProgress x y cbst of
       Left v => Left (VSucc v)
       Right (b ** (st, cbst)) => let st'   = StSucc st
                                      cbst' = CoBStSucc cbst
                                  in Right (_ ** (st', cbst'))
--
coBigStepProgress (TPred x) (TPred x) (CoBStValue v) impossible
coBigStepProgress (TPred x) TZero (CoBStPredZero cbst) =
  case coBigStepProgress x TZero cbst of
       Left v => case v of
                      VZero    => Right (_ ** (StPredZero, CoBStValue VZero))
                      VSucc v' => case coBigStepValueIrreducible cbst v of
                                       Refl impossible
       Right (b ** (st, cbst)) => let st'   = StPred st
                                      cbst' = CoBStPredZero cbst
                                  in Right (_ ** (st', cbst'))
coBigStepProgress (TPred x) e2 (CoBStPredSucc cbst) =
  case coBigStepProgress x (TSucc e2) cbst of
       Left v => case v of
                      VZero => case coBigStepValueIrreducible cbst v of
                                    Refl impossible
                      VSucc v' => case coBigStepValueIrreducible cbst v of
                                       Refl => Right (_ ** (StPredSucc v', CoBStValue v'))
       Right (b ** (st, cbst)) => let st' = StPred st
                                  in Right (_ ** (st', CoBStPredSucc cbst))
--
coBigStepProgress (TIfz x y z) (TIfz x y z) (CoBStValue v) impossible
coBigStepProgress (TIfz x y z) e2 (CoBStIfzZero cbst1 cbst2) =
  case coBigStepProgress x TZero cbst1 of
       Left v => case coBigStepValueIrreducible cbst1 v of
                      Refl => Right (_ ** (StIfzZero, cbst2))
       Right (b ** (st, cbst)) => let st'   = StIfz st
                                      cbst' = CoBStIfzZero cbst cbst2
                                  in Right (_ ** (st', cbst'))
coBigStepProgress (TIfz x y z) e2 (CoBStIfzSucc cbst1 cbst2) =
  case coBigStepProgress x (TSucc _) cbst1 of
       Left v => case coBigStepValueIrreducible cbst1 v of
                      Refl => case v of
                                   VSucc v' => Right (_ ** (StIfzSucc v', cbst2))
       Right (b ** (st, cbst)) => let st'   = StIfz st
                                      cbst' = CoBStIfzSucc cbst cbst2
                                  in Right (_ **(st', cbst'))

-- With the previous lemma, one can finally prove the
-- implication 'CoBigStep' => 'CoTransStep':
-- (i.e. Lemma 36 in "Coinductive big-step operational semantics"
-- by X. Leroy and H. Grall)
coBigStepToTransStep : (e1 : Term [] t) -> (e2 : Term [] t) ->
                       CoBigStep e1 e2 -> CoTransStep e1 e2
coBigStepToTransStep e1 e2 cbst =
  case coBigStepProgress e1 e2 cbst of
       Left v => case coBigStepValueIrreducible cbst v of
                      Refl => CoTStRefl e1
       Right (b ** (st, cbst)) => CoTStTrans st $ coBigStepToTransStep b e2 cbst

-- End: CO-BIG-STEP => CO-TRANSSTEP
-----------------------------------

---------------------------------------
-- Begin: CO-TRANSSTEP =/=> CO-BIG-STEP

-- The following application serves to show that the relations
-- 'CoTransStep' and 'CoBigStep' are not equivalent:
-- (This example follows Lemma 36 in "Coinductive big-step
-- operational semantics" by X. Leroy and H. Grall.)
appOmega : Term [] TyNat
appOmega = TApp (TAbs {s=TyNat} TZero) (Subst.omega {t=TyNat})

-- Under 'CoTransStep' the term 'appOmega' evaluates to anything:
appOmegaCoTransStepAny : (e : Term [] TyNat) -> CoTransStep Equivalence.appOmega e
appOmegaCoTransStepAny e = let st = StApp2 {v=(TAbs TZero)} VAbs StFixBeta
                           in CoTStTrans st (appOmegaCoTransStepAny e)

-- The following re-states a result from 'Determinism.idr'
-- (in order to avoid importing 'Determinism.idr', which
-- would lead to a cycle of imports):
coBigStepOmegaAny : CoBigStep Subst.omega e
coBigStepOmegaAny = CoBStFix (CoBStValue VAbs) Equivalence.coBigStepOmegaAny

appOmegaCoBigStepZero : CoBigStep Equivalence.appOmega TZero
appOmegaCoBigStepZero = let cbst1  = CoBStValue {e=(TAbs TZero)} VAbs
                            cbst2  = Equivalence.coBigStepOmegaAny {e=Subst.omega}
                            cbst3  = CoBStValue VZero
                        in CoBStApp cbst1 cbst2 cbst3

-- Under 'CoBigStep' the term 'appOmega' only evaluates
-- to 'TZero' (and to nothing else):
appOmegaCoBigStepOnlyZero : (e : Term [] TyNat) ->
                            CoBigStep Equivalence.appOmega e ->
                            e = TZero
appOmegaCoBigStepOnlyZero _ (CoBStValue VZero)     impossible
appOmegaCoBigStepOnlyZero _ (CoBStValue (VSucc _)) impossible
appOmegaCoBigStepOnlyZero _ (CoBStValue VAbs)      impossible
appOmegaCoBigStepOnlyZero e (CoBStApp cbst1 cbst2 cbst3) =
  case coBigStepValueIrreducible cbst1 VAbs of
       Refl => sym $ coBigStepValueIrreducible cbst3 VZero

-- End: CO-TRANSSTEP =/=> CO-BIG-STEP
-------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Server.Template.Template

import Extra.String

-- Simple template library, can be vastly improved

ident : String -> String
ident k =
  "<%% " ++ k ++ " %%>"

export
template : String -> List (String, String) -> String
template tmpl =
  foldl (\acc, (k, v) => replace (ident k) v acc) tmpl

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
{-
data Nat = Z | S Nat

plus : Nat -> Nat -> Nat
plus Z y = y
plus (S x) y = S (plus x y)
-}

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

%name Vect xs, ys, zs

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith f [] ys = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

create_empties : Vect m (Vect 0 elem)
create_empties {m = Z} = []
create_empties {m = (S k)} = [] :: create_empties

transpose_helper : (row : Vect m elem) -> (rest_trans : Vect m (Vect k elem)) ->
                   Vect m (Vect (S k) elem)
transpose_helper [] [] = []
transpose_helper (rowval :: xs) (restrow :: ys) = (rowval :: restrow) :: transpose_helper xs ys

transpose_vec : Vect n (Vect m elem) -> Vect m (Vect n elem)
transpose_vec [] = create_empties
transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in
                                  transpose_helper row rest_trans

------- A main program to read dimensions, generate and tranpose a vector

implementation Functor (Vect m) where
    map m [] = []
    map m (x :: xs) = m x :: map m xs

implementation Show a => Show (Vect m a) where
    show x = show (toList x)
      where
        toList : Vect m a -> List a
        toList [] = []
        toList (y :: xs) = y :: toList xs

countTo : (m : Nat) -> Vect m Int
countTo Z = []
countTo (S k) = 0 :: map (+1) (countTo k)

mkVect : (n, m : Nat) -> Vect n (Vect m Int)
mkVect Z m = []
mkVect (S k) m = countTo m :: map (map (+ cast m)) (mkVect k m)

main : IO ()
main = do putStr "Rows: "
          let r : Nat = 5
          putStr "Columns: "
          let c : Nat = 6
          printLn (mkVect r c)
          putStrLn "Transposed:"
          printLn (transpose_vec (mkVect r c))

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
mutual
  caseTest : Nat -> Bool
  caseTest p with (dummy)
   caseTest p | _ = True

  dummy : Nat
  dummy = case (caseTest 0) of
             True => 0
             _ => 0


text:
module Minecraft.Base.PreClassic.Dirt.ItemEntity

import public Minecraft.Base.PreClassic.Dirt
import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint dirtItemEntity : Pickup Dirt.ItemEntity
  public export %hint dirtVtbl       : Vtbl   Dirt.ItemEntity

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module ArithExp.SmallStep
import ArithExp.AST

||| Definition of a relation, adapted from *Software Foundations*
Relation : Type -> Type
Relation a = a -> a -> Type

deterministic : Relation a -> Type
deterministic {a=a} Ra = {x, y, z : a} -> Ra x y -> Ra x z -> y = z

||| Used or defining the "transitive closure" used in TAPL.
|||
||| This is also taken from *Software Foundations*
data MultiStep : Relation a -> Relation a where
  Reflexive   : MultiStep r x x
  Transitive  : r x y -> MultiStep r y z -> MultiStep r x z

syntax [x] THEN   [y] = x `Transitive` (y)
syntax [a] "=>>"  [b]  = SmallStep a b
syntax [a] "=>>*" [b]  = MultiStep SmallStep a b

||| 'SmallStep' is the small step OS relation
data SmallStep : ArithBool -> ArithBool -> Type where

  IfTrue     : (IF Tru a b)  =>> a

  IfFalse    : (IF Fals a b) =>> b

  IfStep     : (t =>> t')
            -> (IF t a b) =>> (IF t' a b)

  SuccStep   : (t =>> t')
            -> (Succ t) =>> (Succ t')

  IsZeroStep : (t =>> t')
            -> (IsZero t) =>> (IsZero t')

  IsZeroZero : (IsZero Zero) =>> Tru

  IsZeroSucc : {auto prf : NV n} -> (IsZero (Succ n)) =>> Fals

  PredStep   : (t =>> t')
            -> (Pred t) =>> (Pred t')

  PredZero   : (Pred Zero) =>> Zero

  PredSucc   : {prf : NV n} -> (Pred (Succ n)) =>> n

test1 : (IF (IF Tru Fals Fals) Tru (IsZero (Succ (Succ Zero)))) =>>* Fals
test1 = (IfStep IfTrue)   THEN
        IfFalse           THEN
        IsZeroSucc        THEN
        Reflexive

max_stars_repo_name: ezrosent/TAPL-idris

max_issues_repo_name: ezrosent/TAPL-idris

max_forks_repo_name: ezrosent/TAPL-idris


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

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

%default total


text:
-- BearSSL's "adding holes" algorithm for XOR multiplication
-- Based on BearSSL ghash_ctmul64.c

module Crypto.Hash.GHash

import Utils.Bytes
import Data.Bits
import Data.List
import Data.Vect
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.Nat.Order.Properties
import Utils.Misc
import Crypto.Hash

HValues : Type
HValues = (Bits64, Bits64, Bits64, Bits64, Bits64, Bits64)

-- Carryless multiplication with "holes"
bmul : Bits64 -> Bits64 -> Bits64
bmul x y =
  let x0 = x .&. 0x1111111111111111
      x1 = x .&. 0x2222222222222222
      x2 = x .&. 0x4444444444444444
      x3 = x .&. 0x8888888888888888
      y0 = y .&. 0x1111111111111111
      y1 = y .&. 0x2222222222222222
      y2 = y .&. 0x4444444444444444
      y3 = y .&. 0x8888888888888888
      z0 = (x0 * y0) `xor` (x1 * y3) `xor` (x2 * y2) `xor` (x3 * y1)
      z1 = (x0 * y1) `xor` (x1 * y0) `xor` (x2 * y3) `xor` (x3 * y2)
      z2 = (x0 * y2) `xor` (x1 * y1) `xor` (x2 * y0) `xor` (x3 * y3)
      z3 = (x0 * y3) `xor` (x1 * y2) `xor` (x2 * y1) `xor` (x3 * y0)
  in (z0 .&. 0x1111111111111111) .|.
     (z1 .&. 0x2222222222222222) .|.
     (z2 .&. 0x4444444444444444) .|.
     (z3 .&. 0x8888888888888888)

rms : Bits64 -> Index {a=Bits64} -> Bits64 -> Bits64
rms m s x = (shiftL (x .&. m) s) .|. ((shiftR x s) .&. m)

rev64 : Bits64 -> Bits64
rev64 x =
  let x' =
      (rms 0x0000FFFF0000FFFF 16) $
      (rms 0x00FF00FF00FF00FF 8 ) $
      (rms 0x0F0F0F0F0F0F0F0F 4 ) $
      (rms 0x3333333333333333 2 ) $
      (rms 0x5555555555555555 1 ) x
  in (shiftL x' 32) .|. (shiftR x' 32)

gmult_core : Bits64 -> Bits64 -> HValues -> (Bits64, Bits64)
gmult_core y1 y0 (h0, h0r, h1, h1r, h2, h2r) =
  let y1r = rev64 y1
      y0r = rev64 y0
      y2 = xor y0 y1
      y2r = xor y0r y1r
      -- Karatsuba decomposition
      -- Here we decompose the 128 bit multiplication into
      -- 3 64-bits multiplication
      -- The h-suffixed variables are just multiplication for
      -- reversed bits, which is necessary because we want the
      -- high bits
      z0 = bmul y0 h0
      z1 = bmul y1 h1
      z2 = bmul y2 h2
      z0h = bmul y0r h0r
      z1h = bmul y1r h1r
      z2h = bmul y2r h2r
      z2  = xor (xor z0 z1) z2
      z2h = xor (xor z0h z1h) z2h
      z0h = shiftR (rev64 z0h) 1
      z1h = shiftR (rev64 z1h) 1
      z2h = shiftR (rev64 z2h) 1
      -- Since the operation is done in big-endian, but GHASH spec
      -- needs small endian, we flip the bits
      v0 = z0
      v1 = xor z0h z2
      v2 = xor z1 z2h
      v3 = z1h
      v3 = (shiftL v3 1) .|. (shiftR v2 63)
      v2 = (shiftL v2 1) .|. (shiftR v1 63)
      v1 = (shiftL v1 1) .|. (shiftR v0 63)
      v0 = (shiftL v0 1)
      -- Modular reduction to GF[128]
      v2 = v2 `xor` v0              `xor` (shiftR v0 1)  `xor` (shiftR v0 2) `xor` (shiftR v0 7)
      v1 = v1 `xor` (shiftL v0 63) `xor` (shiftL v0 62) `xor` (shiftL v0 57)
      v3 = v3 `xor` v1             `xor` (shiftR v1 1)  `xor` (shiftR v1 2) `xor` (shiftR v1 7)
      v2 = v2 `xor` (shiftL v1 63) `xor` (shiftL v1 62) `xor` (shiftL v1 57)
  in (v3, v2)

gcm_mult : HValues -> Vect 16 Bits8 -> Vect 16 Bits8
gcm_mult h y =
  let y1 = from_be $ take 8 y
      y0 = from_be $ drop 8 y
      (y1', y0') = gmult_core y1 y0 h
  in to_be {n=8} y1' ++ to_be y0'

mk_h_values : Vect 16 Bits8 -> HValues
mk_h_values h =
  let h1  = from_be $ take 8 h
      h0  = from_be $ drop 8 h
      h0r = rev64 h0
      h1r = rev64 h1
      h2  = xor h0 h1
      h2r = xor h0r h1r
  in (h0, h0r, h1, h1r, h2, h2r)

export
data GHash : Type where
  MkGHash : List Bits8 -> HValues -> Vect 16 Bits8 -> GHash

hash_until_done : GHash -> GHash
hash_until_done ghash@(MkGHash buffer hval state) =
  case splitAtExact 16 buffer of
    Just (a, b) => hash_until_done $ MkGHash b hval (gcm_mult hval (zipWith xor a state))
    Nothing => ghash

export
Digest GHash where
  digest_nbyte = 16
  update message (MkGHash buffer hval state) =
    hash_until_done (MkGHash (buffer <+> message) hval state)
  finalize (MkGHash buffer hval state) =
    let (MkGHash _ _ state) = hash_until_done (MkGHash (pad_zero 16 buffer) hval state)
    in state

export
MAC (Vect 16 Bits8) GHash where
  initialize_mac key = MkGHash [] (mk_h_values key) (replicate _ 0)


text:
data Option a = None | Some a

total safeDiv : Double -> Double -> Option Double
safeDiv x 0.0 = None
safeDiv x y = Some (x/y)

data Result a b = Ok a | Error b

total run : (f : (a -> c)) -> (g : (b -> c)) -> Result a b -> c
run f g (Ok x) = f x
run f g (Error x) = g x

data BSTree : Type -> Type where
  Empty : Ord elem => BSTree elem
  Node : Ord elem => (left : BSTree elem) ->
                     (val : elem) ->
                     (right : BSTree elem) ->
                     BSTree elem

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

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Test.Inigo.Account.AccountTest

import IdrTest.Test
import IdrTest.Expectation

import Inigo.Account.Account
import Inigo.Async.SubtleCrypto.SubtleCrypto

simpleAccount : Account
simpleAccount =
  MkAccount "tom" "tom@example.com" (PBKDF2 Sha512 "salt" 1000) "aaa"

simpleAccountToml : String
simpleAccountToml ="""
ns=\"tom\"
email=\"tom@example.com\"
kdf.type=\"PBKDF2\"
kdf.sha=\"SHA-512\"
kdf.salt=\"salt\"
kdf.iterations=1000
hash=\"aaa\"
"""

export
suite : Test
suite =
  describe "Account" [
    test "Account Encode" (\_ => assertEq
      (encode simpleAccount)
      simpleAccountToml
    ),
    test "Simple Decode" (\_ => assertEq
      (decode simpleAccountToml)
      (Just simpleAccount)
    )
  ]


text:
> module Nat.DivisorOperations

> import Nat.Divisor

> %default total

> %access public export

> ||| Exact integer division
> quotient : (m : Nat) -> (d : Nat) -> d `Divisor` m -> Nat
> quotient _ _ (Element q _) = q

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| Additional properties/lemmata of Nats
module Data.Nat.Properties

import Data.Nat
import Syntax.PreorderReasoning

%default total

export
unfoldDouble : {0 n : Nat} -> (2 * n) === (n + n)
unfoldDouble = irrelevantEq $ cong (n +) (plusZeroRightNeutral _)

export
unfoldDoubleS : {0 n : Nat} -> (2 * S n) === (2 + 2 * n)
unfoldDoubleS = irrelevantEq $ Calc $
  |~ 2 * S n
  ~~ S n + S n   ...( unfoldDouble {n = S n} )
  ~~ 2 + (n + n) ...( sym (plusSuccRightSucc (S n) n) )
  ~~ 2 + 2 * n   ...( cong (2 +) (sym unfoldDouble) )

export
multRightCancel : (a,b,r : Nat) -> (0 _ : NonZero r) -> a*r = b*r -> a = b
multRightCancel a      b    0           r_nz ar_eq_br = void (absurd r_nz)
multRightCancel 0      0    r@(S predr) r_nz ar_eq_br = Refl
multRightCancel 0     (S b) r@(S predr) r_nz ar_eq_br impossible
multRightCancel (S a)  0    r@(S predr) r_nz ar_eq_br impossible
multRightCancel (S a) (S b) r@(S predr) r_nz ar_eq_br =
  cong S $ multRightCancel a b r r_nz
         $ plusLeftCancel r (a*r) (b*r) ar_eq_br


text:
module Main

import OCaml.IO

f : String -> (String, Maybe Double)
f x = (x ++ x, Just (1.3 + 1.3))

main : OCaml_IO ()
main = do
     min_int <- ocamlCall "Pervasives.min_int" (OCaml_IO Int)
     printLn min_int
     ic <- ocamlCall "Pervasives.open_in" (String -> OCaml_IO Ptr) "Foo.idr"
     str <- ocamlCall "Pervasives.input_line" (Ptr -> OCaml_IO String) ic
     l <- ocamlCall "List.length" (List Int -> OCaml_IO Int) [1,2,3]
     ll <- ocamlCall "List.flatten" ((List (List Int)) -> OCaml_IO (List Int)) [[1,2,3], [9,10,11]]
     printLn l
     printLn ll
     printLn str
     ys <- ocamlCall "List.map" ((Int -> Int) -> List Int -> OCaml_IO (List Int)) ((+1)) [1..10]
     printLn ys
     zs <- ocamlCall "List.map" ((String -> (String, Maybe Double)) -> List String -> OCaml_IO (List (String, Maybe Double))) f ["hello", "world"]
     printLn zs
     ocamlCall "List.iter" ((Double -> OCaml_IO ()) -> List Double -> OCaml_IO ())
        printLn'
        [1.1,213.321]
     ocamlCall "List.iter2"
        ((Int -> Int -> OCaml_IO ()) -> List Int -> List Int -> OCaml_IO ())
        (\a => \b => printLn' (a + b))
        [1..10]
        [11..20]
     ocamlCall "List.init"
       (Int -> (Int -> OCaml_IO ()) -> OCaml_IO (List ()))
       4
       (\x => printLn' x)
     pure ()

      --   printLn is

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Language.LSP.Message.Location

import Data.URI
import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%hide Prelude.Range
%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#position
public export
record Position where
  constructor MkPosition
  line      : Int
  character : Int
%runElab deriveJSON defaultOpts `{Position}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#range
public export
record Range where
  constructor MkRange
  start : Position
  end   : Position
%runElab deriveJSON defaultOpts `{Range}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#location
public export
record Location where
  constructor MkLocation
  uri   : URI
  range : Range
%runElab deriveJSON defaultOpts `{Location}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#locationLink
public export
record LocationLink where
  constructor MkLocationLink
  originSelectionRange : Maybe Range
  targetUri            : URI
  targetRange          : Range
  targetSelectionRange : Range
%runElab deriveJSON defaultOpts `{LocationLink}


text:
module Main

import Data.Fin

data Direction = North | South | East | West

Position : Type
Position = (Nat, Nat)

record MarsRover where
       constructor MkRover
       upperBound : Position
       currentPosition : (Fin (fst upperBound), Fin (snd upperBound))
       direction : Direction
%name MarsRover rover, rover1, rover2

turnRight : MarsRover -> MarsRover
turnRight rover = MkRover (upperBound rover) (currentPosition rover) newDirection
          where newDirection = case direction rover of
                                    North => East
                                    South => West
                                    East  => South
                                    West  => North

turnLeft : MarsRover -> MarsRover
turnLeft rover = MkRover (upperBound rover) (currentPosition rover) newDirection
          where newDirection = case direction rover of
                                    North => West
                                    South => East
                                    East  => North
                                    West  => South

getPosition : MarsRover -> (Integer, Integer)
getPosition rover = let pos = currentPosition rover in (finToInteger (fst pos), finToInteger (snd pos))

move : MarsRover -> MarsRover
move = ?todo

max_stars_repo_name: balajisivaraman/mars-rover-idris

max_issues_repo_name: balajisivaraman/mars-rover-idris

max_forks_repo_name: balajisivaraman/mars-rover-idris


text:
module Main

import Exercises.GettingStarted

%access export

private
boolToString : Bool -> String
boolToString True  = "is"
boolToString False = "is not"

private
showPalindrome : String -> String
showPalindrome str =
  let mightBe = boolToString (CaseInsensitive.palindrome str) in
      unwords [ str, mightBe, "a palindrome.\n" ]

partial
main : IO ()
main = repl "Enter a potential palindrome: "
            showPalindrome

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 Combinator

import Lightyear.Combinators
import Lightyear.Core

export
skipMany : Monad m => ParserT str m a -> ParserT str m ()
skipMany p = do many p
                return ()

export
skipMany1 : Monad m => ParserT str m a -> ParserT str m ()
skipMany1 p = do p
                 skipMany p

export
many1 : Monad m => ParserT str m a -> ParserT str m (List a)
many1 p = return $ !p :: !(many p)

sepBy : Monad m => (p : ParserT str m a)
                -> (s : ParserT str m b)
                -> ParserT str m (List a)
sepBy p s = (p `sepBy1` s) <|> pure List.Nil

export
endBy : Monad m => (p : ParserT str m a)
                -> (s : ParserT str m b)
                -> ParserT str m (List a)
endBy p s = many (do x <- p; s; return x)


text:
module Data.Functor.Const

public export
record Const (a : Type) (b : Type) where
  constructor MkConst
  getConst : a

public export
Eq a => Eq (Const a b) where
  (==) = (==) `on` getConst

public export
Ord a => Ord (Const a b) where
  compare = compare `on` getConst

public export
Show a => Show (Const a b) where
  showPrec p = showCon p "MkConst" . showArg . getConst

public export
Functor (Const a) where
  map _ (MkConst a)= MkConst a

public export
Monoid a => Applicative (Const a) where
  pure _ = MkConst neutral
  MkConst f <*> MkConst a = MkConst $ f <+> a

public export
Foldable (Const a) where
  foldr _ acc _ = acc
  foldl _ acc _ = acc
  null        _ = True

public export
Traversable (Const a) where
  traverse _ (MkConst v) = pure (MkConst v)

public export
Bifunctor Const where
  bimap f _ (MkConst a) = MkConst (f a)

public export
Bifoldable Const where
  bifoldl f _ acc (MkConst a) = f acc a
  bifoldr f _ acc (MkConst a) = f a acc
  binull _ = False

public export
Bitraversable Const where
  bitraverse f _ (MkConst a) = MkConst <$> f a


text:
import Data.Vect

-- Page 50

-- Exercise 2
{- reversei : List Char -> List Char
reversei [] = []
reversei (x :: xs) = reversei xs ++ [x]

reverse : String -> String
reverse x = pack $ reversei $ unpack x -}

-- Exercise 2
palindrome2 : String -> Bool
palindrome2 x = x == reverse x

-- Exercise 3
palindrome3 : String -> Bool
palindrome3 x = toLower x == (reverse $ toLower x)

-- Exercise 6
counts : String -> (Nat, Nat)
counts x = (length $ words x, length x)

-- Exercise 7
top_ten : Ord a => List a -> List a
top_ten xs = take 10 $ reverse $ sort xs

-- Page 75
length_ : List a -> Nat
length_ [] = 0
length_ (x :: xs) = S (length_ xs)

reverse_ : List a -> List a
reverse_ [] = []
reverse_ (x :: xs) = reverse xs ++ [x]

map1_ : (a -> b) -> List a -> List b
map1_ f [] = []
map1_ f (x :: xs) = f x :: (map1_ f xs)

map2_ : (a -> b) -> Vect n a -> Vect n b
map2_ f [] = []
map2_ f (x :: xs) = f x :: (map2_ f xs)

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

--transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
--transposeMat [] = createEmpties
--transposeMat (x :: xs) = ?transposeMat_rhs_2

dotProduct : Num a => Vect m a -> Vect m a -> Vect m a
dotProduct = zipWith (+)

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix l1 l2 = zipWith dotProduct l1 l2

-- Extra
double : Vect n a -> Vect (n * 2) a
double [] = []
double (x :: xs) = [x, x] ++ double xs

-- countTo : (m : Nat) -> Vect m Nat
-- countTo Z = []
-- countTo (S k) = countTo k ++ [S k]

addOrNothing : a -> Maybe (Vect k a) -> Maybe (Vect (S k) a)
addOrNothing x Nothing = Nothing
addOrNothing x (Just xs) = Just (x :: xs)

takeList : (n : Nat) -> List a -> Maybe (Vect n a)
takeList Z xs = Just []
takeList (S k) [] = Nothing
takeList (S k) (x :: xs) = addOrNothing x (takeList k xs)

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
-- vim: set ft=idris sw=2 ts=2:
--
-- perfect_number.idr
-- Calculate 'perfect' numbers in the Idris programming language
--

module PerfectNumber

-- predicate to check whether given number is perfect
export
is_perfect : (Integral a, Ord a) => a -> Bool
is_perfect n = if n > 0 then loop n 1 0 else False
where
  loop : a -> a -> a -> Bool
  loop n i sum = if n == i then (sum == n) else
    if (n `mod` i) == 0 then loop n (i + 1) (sum + i) else loop n (i + 1) sum

-- generate 'perfect' numbers until given limit
export
perfect_numbers : Nat -> List Nat
perfect_numbers n = filter (\x => is_perfect x) $ natRange n

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Libraries.Text.Lexer.Core

import Data.List
import Data.Maybe
import Data.Nat
import Data.String

import public Libraries.Control.Delayed
import public Libraries.Text.Bounded

%default total

||| A language of token recognisers.
||| @ consumes If `True`, this recogniser is guaranteed to consume at
|||            least one character of input when it succeeds.
export
data Recognise : (consumes : Bool) -> Type where
     Empty : Recognise False
     Fail : Recognise c
     Lookahead : (positive : Bool) -> Recognise c -> Recognise False
     Pred : (Char -> Bool) -> Recognise True
     SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
     SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
     SeqSame : Recognise e -> Recognise e -> Recognise e
     Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)

||| A token recogniser. Guaranteed to consume at least one character.
public export
Lexer : Type
Lexer = Recognise True

||| Sequence two recognisers. If either consumes a character, the sequence
||| is guaranteed to consume a character.
export %inline
(<+>) : {c1 : Bool} ->
        Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
(<+>) {c1 = False} = SeqEmpty
(<+>) {c1 = True} = SeqEat

||| Alternative recognisers. If both consume, the combination is guaranteed
||| to consume a character.
export
(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)
(<|>) = Alt

||| A recogniser that always fails.
export
fail : Recognise c
fail = Fail

||| Recognise no input (doesn't consume any input)
export
empty : Recognise False
empty = Empty

||| Recognise a character that matches a predicate
export
pred : (Char -> Bool) -> Lexer
pred = Pred

||| Positive lookahead. Never consumes input.
export
expect : Recognise c -> Recognise False
expect = Lookahead True

||| Negative lookahead. Never consumes input.
export
reject : Recognise c -> Recognise False
reject = Lookahead False

||| Sequence the recognisers resulting from applying a function to each element
||| of a list. The resulting recogniser will consume input if the produced
||| recognisers consume and the list is non-empty.
export
concatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (isCons xs && c)
concatMap _ []                 = Empty
concatMap f (x :: [])          = f x
concatMap f (x :: xs@(_ :: _)) = SeqSame (f x) (concatMap f xs)

data StrLen : Type where
     MkStrLen : String -> Nat -> StrLen

getString : StrLen -> String
getString (MkStrLen str n) = str

strIndex : StrLen -> Nat -> Maybe Char
strIndex (MkStrLen str len) i
    = if cast {to = Integer} i >= cast len then Nothing
      else Just (assert_total (prim__strIndex str (cast i)))

mkStr : String -> StrLen
mkStr str = MkStrLen str (length str)

strTail : Nat -> StrLen -> StrLen
strTail start (MkStrLen str len)
    = MkStrLen (substr start len str) (minus len start)

-- If the string is recognised, returns the index at which the token
-- ends
export
scan : Recognise c -> List Char -> List Char -> Maybe (List Char, List Char)
scan Empty tok str = pure (tok, str)
scan Fail tok str = Nothing
scan (Lookahead positive r) tok str
    = if isJust (scan r tok str) == positive
         then pure (tok, str)
         else Nothing
scan (Pred f) tok [] = Nothing
scan (Pred f) tok (c :: str)
    = if f c
         then Just (c :: tok, str)
         else Nothing
scan (SeqEat r1 r2) tok str
    = do (tok', rest) <- scan r1 tok str
         -- TODO: Can we prove totality instead by showing idx has increased?
         assert_total (scan r2 tok' rest)
scan (SeqEmpty r1 r2) tok str
    = do (tok', rest) <- scan r1 tok str
         scan r2 tok' rest
scan (SeqSame r1 r2) tok str
    = do (tok', rest) <- scan r1 tok str
         scan r2 tok' rest
scan (Alt r1 r2) tok str
    = maybe (scan r2 tok str) Just (scan r1 tok str)

||| A mapping from lexers to the tokens they produce.
||| This is a list of pairs `(Lexer, String -> tokenType)`
||| For each Lexer in the list, if a substring in the input matches, run
||| the associated function to produce a token of type `tokenType`
public export
TokenMap : (tokenType : Type) -> Type
TokenMap tokenType = List (Lexer, String -> tokenType)

tokenise : (a -> Bool) ->
           (line : Int) -> (col : Int) ->
           List (WithBounds a) -> TokenMap a ->
           List Char -> (List (WithBounds a), (Int, Int, List Char))
tokenise pred line col acc tmap str
    = case getFirstToken tmap str of
           Just (tok, line', col', rest) =>
           -- assert total because getFirstToken must consume something
               if pred tok.val
                  then (reverse acc, (line, col, []))
                  else assert_total (tokenise pred line' col' (tok :: acc) tmap rest)
           Nothing => (reverse acc, (line, col, str))
  where
    countNLs : List Char -> Nat
    countNLs str = List.length (filter (== '\n') str)

    getCols : List Char -> Int -> Int
    getCols x c
         = case span (/= '\n') (reverse x) of
                (incol, []) => c + cast (length incol)
                (incol, _) => cast (length incol)

    getFirstToken : TokenMap a -> List Char ->
                    Maybe (WithBounds a, Int, Int, List Char)
    getFirstToken [] str = Nothing
    getFirstToken ((lex, fn) :: ts) str
        = case scan lex [] str of
               Just (tok, rest) =>
                 let line' = line + cast (countNLs tok)
                     col' = getCols tok col in
                     Just (MkBounded (fn (fastPack (reverse tok))) False (MkBounds line col line' col'),
                           line', col', rest)
               Nothing => getFirstToken ts str

||| Given a mapping from lexers to token generating functions (the
||| TokenMap a) and an input string, return a list of recognised tokens,
||| and the line, column, and remainder of the input at the first point in the
||| string where there are no recognised tokens.
export
lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
lex tmap str
    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
          (ts, (l, c, fastPack str'))

export
lexTo : (a -> Bool) ->
        TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
lexTo pred tmap str
    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
          (ts, (l, c, fastPack str'))


text:
module Java.Nio

import IdrisJvm.IO

%access public export

namespace OpenOption
    openOptionClass : String
    openOptionClass = "java/nio/file/OpenOption"

    OpenOption : Type
    OpenOption = JVM_Native (Interface openOptionClass)

namespace StandardOpenOption
    standardOpenOptionClass : String
    standardOpenOptionClass = "java/nio/file/StandardOpenOption"

    StandardOpenOptionClass : JVM_NativeTy
    StandardOpenOptionClass = Class standardOpenOptionClass

    StandardOpenOption : Type
    StandardOpenOption = JVM_Native StandardOpenOptionClass

    Inherits OpenOption StandardOpenOption where {}

    append : StandardOpenOption
    append = unsafePerformIO $ getStaticField StandardOpenOptionClass "APPEND" (JVM_IO StandardOpenOption)

    create : StandardOpenOption
    create = unsafePerformIO $ getStaticField StandardOpenOptionClass "CREATE" (JVM_IO StandardOpenOption)

    createNew : StandardOpenOption
    createNew = unsafePerformIO $ getStaticField StandardOpenOptionClass "CREATE_NEW" (JVM_IO StandardOpenOption)

    deleteOnClose: StandardOpenOption
    deleteOnClose = unsafePerformIO $ getStaticField StandardOpenOptionClass "DELETE_ON_CLOSE" (JVM_IO StandardOpenOption)

    dsync : StandardOpenOption
    dsync = unsafePerformIO $ getStaticField StandardOpenOptionClass "DSYNC" (JVM_IO StandardOpenOption)

    read : StandardOpenOption
    read = unsafePerformIO $ getStaticField StandardOpenOptionClass "READ" (JVM_IO StandardOpenOption)

    sparse : StandardOpenOption
    sparse = unsafePerformIO $ getStaticField StandardOpenOptionClass "SPARSE" (JVM_IO StandardOpenOption)

    sync : StandardOpenOption
    sync = unsafePerformIO $ getStaticField StandardOpenOptionClass "SYNC" (JVM_IO StandardOpenOption)

    truncateExisting : StandardOpenOption
    truncateExisting = unsafePerformIO $ getStaticField StandardOpenOptionClass "TRUNCATE_EXISTING" (JVM_IO StandardOpenOption)

    write : StandardOpenOption
    write = unsafePerformIO $ getStaticField StandardOpenOptionClass "WRITE" (JVM_IO StandardOpenOption)

namespace Path
    pathClass : String
    pathClass = "java/nio/file/Path"

    Path : Type
    Path = JVM_Native (Interface pathClass)

Show Path where
    show path = unsafePerformIO $ invokeInstance "toString" (Path -> JVM_IO String) path

namespace Paths
    pathsClass : String
    pathsClass = "java/nio/file/Paths"

    PathsClass : JVM_NativeTy
    PathsClass = Class pathsClass

    Paths : Type
    Paths = JVM_Native PathsClass

namespace Channel
    channelClass : String
    channelClass = "java/nio/channels/Channel"

    ChannelClass : JVM_NativeTy
    ChannelClass = Interface channelClass

    Channel : Type
    Channel = JVM_Native ChannelClass

    close : Inherits Channel channel => channel -> JVM_IO ()
    close channel = invokeInstance "close" (Channel -> JVM_IO ()) (believe_me channel)

namespace ReadableByteChannel
    readableByteChannelClass : String
    readableByteChannelClass = "java/nio/channels/ReadableByteChannel"

    ReadableByteChannelClass : JVM_NativeTy
    ReadableByteChannelClass = Interface readableByteChannelClass

    ReadableByteChannel : Type
    ReadableByteChannel = JVM_Native ReadableByteChannelClass

    Inherits Channel ReadableByteChannel where {}

namespace WritableByteChannel
    writableByteChannelClass : String
    writableByteChannelClass = "java/nio/channels/WritableByteChannel"

    WritableByteChannelClass : JVM_NativeTy
    WritableByteChannelClass = Interface writableByteChannelClass

    WritableByteChannel : Type
    WritableByteChannel = JVM_Native WritableByteChannelClass

    Inherits Channel WritableByteChannel where {}

namespace SeekableByteChannel
    seekableByteChannelClass : String
    seekableByteChannelClass = "java/nio/channels/SeekableByteChannel"

    SeekableByteChannel : Type
    SeekableByteChannel = JVM_Native (Interface seekableByteChannelClass)

    Inherits Channel SeekableByteChannel where {}

namespace SocketChannel
    socketChannelClass : String
    socketChannelClass = "java/nio/channels/SocketChannel"

    SocketChannel : Type
    SocketChannel = JVM_Native (Class socketChannelClass)

    Inherits Channel SocketChannel where {}
    Inherits ReadableByteChannel SocketChannel where {}
    Inherits WritableByteChannel SocketChannel where {}

namespace FileChannel
    fileChannelClass : String
    fileChannelClass = "java/nio/channels/FileChannel"

    FileChannelClass : JVM_NativeTy
    FileChannelClass = Interface fileChannelClass

    FileChannel : Type
    FileChannel = JVM_Native FileChannelClass

    Inherits Channel FileChannel where {}
    Inherits ReadableByteChannel FileChannel where {}
    Inherits WritableByteChannel FileChannel where {}

namespace FileAttribute
    fileAttributeClass : String
    fileAttributeClass = "java/nio/file/attribute/FileAttribute"

    FileAttribute : Type
    FileAttribute = JVM_Native (Interface fileAttributeClass)

namespace BasicFileAttributes
    basicFileAttributesClass : String
    basicFileAttributesClass = "java/nio/file/attribute/BasicFileAttributes"

    BasicFileAttributes : Type
    BasicFileAttributes = JVM_Native (Interface basicFileAttributesClass)

namespace LinkOption
    linkOptionClass : String
    linkOptionClass = "java/nio/file/LinkOption"

    LinkOption : Type
    LinkOption = JVM_Native (Class "java/nio/file/LinkOption")

namespace FileTime
    fileTimeClass : String
    fileTimeClass = "java/nio/file/attribute/FileTime"

    FileTime : Type
    FileTime = JVM_Native (Class fileTimeClass)


text:
module Data.Compress.Utils.Parser

import Data.List
import Data.List.Elem
import Data.List1
import Data.Vect
import Data.Void
import Data.Bits
import Data.SnocList
import Decidable.Equality
import Syntax.WithProof
import Data.Compress.Utils.Bytes

public export
interface Cons a s | s where
  singleton : a -> s
  uncons : s -> Maybe (a, s)

public export
Cons Char String where
  singleton = cast
  uncons = strUncons

public export
Cons a (List a) where
  singleton = pure
  uncons [] = Nothing
  uncons (x :: xs) = Just (x, xs)

public export
record Bitstream where
  constructor MkBitstream
  content : List (Fin 8, Bits8)

export
fromBits8 : List Bits8 -> Bitstream
fromBits8 = MkBitstream . map (FZ,)

export
toBits8 : Bitstream -> List Bits8
toBits8 bs = mapMaybe (\(i,x) => (guard (i == 0)) $> x) bs.content

export
Semigroup Bitstream where
  a <+> b = MkBitstream (a.content <+> b.content)

export
Monoid Bitstream where
  neutral = MkBitstream []

export
is_byte_aligned : Bitstream -> Bool
is_byte_aligned bs = all (\(i,_) => 0 == i) bs.content

public export
Cons Bool Bitstream where
  singleton x = MkBitstream [(0, if x then 1 else 0)]
  uncons bitstream =
    case bitstream.content of
      [] => Nothing
      (i, x) :: xs =>
        case strengthen (FS i) of
          Just i' => Just (testBit x i, MkBitstream ((i', x) :: xs))
          Nothing => Just (testBit x i, MkBitstream xs)

public export
data Parser : (input : Type) -> (error : Type) -> (a : Type) -> Type where
  Fail : e -> Parser i e a
  Pure : (leftover : i) -> a -> Parser i e a
  More : (on_feed : (i -> Parser i e a)) -> Parser i e a
  Alt : Parser i e a -> Lazy (Parser i e a) -> Parser i e a

public export
Functor (Parser i e) where
  map f (Fail e) = Fail e
  map f (Pure leftover x) = Pure leftover (f x)
  map f (More on_feed) = More (map f . on_feed)
  map f (Alt p1 p2) = Alt (map f p1) (map f p2)

public export
transform : (i -> Either e i') -> (i' -> Either e i) -> Parser i e a -> Parser i' e a
transform f g (Fail e) = Fail e
transform f g (Alt p1 p2) = Alt (transform f g p1) (transform f g p2)
transform f g (Pure leftover x) =
  case f leftover of
    Right leftover' => Pure leftover' x
    Left err => Fail err
transform f g (More on_feed) = More $ \x =>
  let Right x' = g x
      | Left err => Fail err
  in transform f g $ on_feed x'

||| maps over the errors of the parser
public export
map_error : (e -> e') -> Parser i e a -> Parser i e' a
map_error f (Fail e) = Fail (f e)
map_error f (Pure leftover x) = Pure leftover x
map_error f (More on_feed) = More (map_error f . on_feed)
map_error f (Alt p1 p2) = Alt (map_error f p1) (map_error f p2)

public export
(<|>) : Semigroup e => Parser i e a -> Lazy (Parser i e a) -> Parser i e a
Fail e <|> p = map_error (e <+>) p
Pure leftover x <|> p = Pure leftover x
p <|> q = Alt p q

||| fail with an error
public export
fail : e -> Parser i e a
fail = Fail

||| feed input into the parser incrementally
public export
feed : (Semigroup e, Semigroup i) => i -> Parser i e a -> Parser i e a
feed input (Fail e) = Fail e
feed input (Pure leftover x) = Pure (leftover <+> input) x
feed input (More on_feed) = on_feed input
feed input (Alt p1 p2) = feed input p1 <|> feed input p2

apply : (Semigroup e, Semigroup i) => (Parser i e a -> Parser i e b) -> Parser i e a -> Parser i e b
apply f (Fail msg) = Fail msg
apply f (Alt p1 p2) = Alt (f p1) (f p2)
apply f (More on_feed) = More (f . on_feed)
apply f parser = More (\input => f $ feed input parser)

public export
pure : Monoid i => a -> Parser i e a
pure x = Pure neutral x

public export
(<*>) : (Semigroup e, Monoid i) => Parser i e (a -> b) -> Lazy (Parser i e a) -> Parser i e b
Pure leftover f <*> p = map f $ feed leftover p
p1 <*> p2 = apply (<*> p2) p1

public export
(<*) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e a
x <* y = map const x <*> y

public export
(*>) : (Semigroup e, Monoid i) => Parser i e a -> Parser i e b -> Parser i e b
x *> y = map (const id) x <*> y

public export
(>>=) : (Semigroup e, Monoid i) => Parser i e a -> (a -> Parser i e b) -> Parser i e b
(>>=) (Pure leftover x) f = feed leftover $ f x
(>>=) p f = apply (>>= f) p

public export
more : (i -> Parser i e a) -> Parser i e a
more = More

||| peek into the next token without consuming it
public export
peek : Cons c i => Parser i e c
peek = more $ \input =>
  case uncons input of
    Just (x, _) => Pure input x
    Nothing => peek

||| reads the next token
public export
token : Cons c i => Parser i e c
token = more $ \input =>
  case uncons input of
    Just (x, xs) => Pure xs x
    Nothing => token

||| run `p` `k` times and collect the results
public export
count : (Semigroup e, Monoid i) => (k : Nat) -> (p : Parser i e a) -> Parser i e (Vect k a)
count Z parser = pure []
count (S k) parser = pure $ !parser :: !(count k parser)

||| return the result of `p` if it succeeds, otherwise return `x`
public export
option : (Semigroup e, Monoid i) => (x : a) -> (p : Parser i e a) -> Parser i e a
option x p = p <|> pure x

mutual
  public export
  some : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List1 a)
  some p = pure $ !p ::: !(many p)

  public export
  many : (Semigroup e, Monoid i) => Parser i e a -> Parser i e (List a)
  many p = option [] (forget <$> some p)

namespace Error
  ||| example: `SimpleError String`
  public export
  data SimpleError : Type -> Type where
    Msg : a -> SimpleError a
    Alt : SimpleError a -> SimpleError a -> SimpleError a
    Under : a -> SimpleError a -> SimpleError a

  public export
  Semigroup (SimpleError a) where
    (<+>) = Alt

  public export
  Show a => Show (SimpleError a) where
    show (Msg x) = show x
    show (Alt a b) = "(" <+> show a <+> " <|> " <+> show b <+> ")"
    show (Under x a) = "(" <+> show x <+> ": " <+> show a <+> ")"

  public export
  msg : e -> SimpleError e
  msg = Msg

  public export
  under : e -> Parser i (SimpleError e) a -> Parser i (SimpleError e) a
  under = map_error . Under

export
bit_getbyte : Parser Bitstream e Bits8
bit_getbyte = more $ \(MkBitstream input) => f input
  where
  f : List (Fin 8, Bits8) -> Parser Bitstream e Bits8
  f ((FZ, x) :: xs) = Pure (MkBitstream xs) x
  f ((_ , x) :: xs) = f xs
  f [] = bit_getbyte

||| parse the next `n` bytes as a natural number in big endian style
export
p_nat : Semigroup e => (n : Nat) -> Parser (List Bits8) e Nat
p_nat n = cast {to = Nat} . le_to_integer <$> count n token

export
p_be_nat : Semigroup e => (n : Nat) -> Parser (List Bits8) e Nat
p_be_nat n = cast {to = Nat} . le_to_integer . reverse <$> count n token

export
le_nat : Semigroup e => (n : Nat) -> Parser Bitstream e Nat
le_nat n = cast {to = Nat} . le_to_integer <$> count n bit_getbyte

||| make sure that `p` MUST consume at least `n` tokens, fails otherwise
public export
p_exact : (Cons c i, Monoid i) => (n : Nat) -> (p : Parser i (SimpleError String) a) -> Parser i (SimpleError String) a
p_exact Z (Pure leftover x) = pure x
p_exact (S i) (Pure leftover x) = fail $ msg $ "over fed, " <+> show (S i) <+> " bytes more to go"
p_exact i (Fail msg) = fail msg
p_exact Z parser = fail $ msg $ "under fed, wants more"
p_exact (S i) parser = do
  b <- token
  p_exact i (feed (singleton b) parser)

record LazyParser i e a where
  constructor Lazify
  parser : Lazy (Parser i e a)

Functor (LazyParser i e) where
  map f p = Lazify $ delay $ map {f=Parser i e} f p.parser

(Semigroup e, Monoid i) => Applicative (LazyParser i e) where
  pure a = Lazify $ delay $ pure a
  a <*> b = Lazify $ delay (Parser.(<*>) a.parser b.parser)

export
ifA : Monoid i => Bool -> Lazy (Parser i e a) -> Parser i e (Maybe a)
ifA cond action = if cond then map Just (Force action) else pure Nothing

export
for : {i,e: _} -> (Semigroup e, Monoid i, Traversable f) => f a -> (a -> Lazy (Parser i e b)) -> Parser i e (f b)
for f p = Force (for f (Lazify . p)).parser

export
take_until : (Semigroup e, Monoid i) => (a -> Bool) -> Parser i e a -> Parser i e (List a)
take_until f parser = loop Lin where
  loop : SnocList a -> Parser i e (List a)
  loop acc = do
    t <- parser
    if not $ f t then loop (acc :< t) else pure $ toList acc

export
get_bit : Num n => Parser Bitstream (SimpleError String) n
get_bit = map (\b => if b then 1 else 0) token

fin_range : (n : Nat) -> List (Fin n)
fin_range _ = toList Fin.range

read_bits : (List Bool -> List Bool) -> Fin 32 -> Parser Bitstream (SimpleError String) Bits32
read_bits f n = do
  bits <- toList <$> count (finToNat n) token
  pure $ foldl (\a,(i,b) => if b then setBit a i else a) 0 $ zip (fin_range 32) (f bits)

export
get_bits : ?
get_bits = read_bits id

export
get_huff : ?
get_huff = read_bits reverse


text:
module Parser.Package

import public Parser.Lexer.Package
import public Parser.Rule.Package
import public Text.Lexer
import public Text.Parser
import public Parser.Support

import System.File
import Utils.Either

%default total

export
runParser : String -> Rule ty -> Either (ParseError Token) ty
runParser str p
    = do toks   <- mapError LexFail $ lex str
         parsed <- mapError toGenericParsingError $ parse p toks
         Right (fst parsed)

export
covering
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
    = do Right str <- readFile fn
             | Left err => pure (Left (FileFail err))
         pure (runParser str p)


text:
isSingleton : Bool -> Type
isSingleton True  = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Nat
sum True  x       = x
sum False []      = 0
sum False (x::xs) = x + sum False xs


text:
public export
interface Do (m : Type) where
  Next : m -> Type
  bind : (x : m) -> Next x

-- Test that the implicits don't turn into as patterns on the LHS - they
-- shouldn't, because the elaborator hasn't got that far yet
foom : Int -> {a, b : Type} -> (a -> b) -> a -> b
foom = ?thurlingdrome

-- Similarly, for bind (we can't just implement it as >>= because of where
-- the implicits end up...)
public export
Monad m => Do (m a) where
  Next x = {b : Type} -> (a -> m b) -> m b
  bind = ?oops -- (>>=)


text:
module Sub04Apply54x48

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(18x+16) --A[6,-4]->B[1,-2]--> 3(4x+3)
export
apply54x48 : (Not . P) (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                            (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                               (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))),
         (Not . P) m))
apply54x48 {l} col = ((S (S (S (plus (plus l l) (plus l l))))) ** (lte54x48 l, ab54x30To12x9 l col)) where
  lte54x48 : (l:Nat) -> LTE (S (S (S (S (plus (plus l l) (plus l l))))))
                            (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                              (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))
  lte54x48 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte54x48 (S k) = let lemma = lte54x48 k in
    rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
    rewrite (sym (plusSuccRightSucc (plus k k) k)) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (S (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))  (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (S (plus (plus k k) k)))) (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))  (S (S (S (plus (plus (plus k k) k) (S (S (plus (plus k k) k))))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Main

import System.File

main : IO ()
main = do
  fr <- openFile "rapid003_testfile.txt" WriteTruncate
  case fr of
       Right f => do
         putStrLn "file opened"
         ignore $ fPutStr f "FileWriteNumber1"
         ignore $ fPutStr f "FileWriteNumber2"
         putStrLn "written twice"
         ignore $ closeFile f
         putStrLn "file closed"
         fr2 <- openFile "/thisShouldNotWork/invalidPath/rapid003_testfile.txt" WriteTruncate
         case fr2 of
              Right f => do putStrLn "file2 opened"
                            ignore $ closeFile f
                            putStrLn "file2 closed"
              Left err => putStrLn ("error opening file2: " ++ show err)
       Left err => do
         putStrLn ("error opening file: " ++ show err)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Depling.Incr

import Depling
import Data.Fin
import Data.Vect

total
incr_var : Fin (S n) -> Fin n -> Fin (S n)
incr_var FZ FZ = FS FZ
incr_var FZ (FS v) = FS $ incr_var FZ v
incr_var (FS i) FZ = FZ
incr_var (FS i) (FS v) = FS $ incr_var i v

mutual
	total
	export
	incr : Fin (S n) -> DAST n -> DAST (S n)
	incr {n = Z} i (ʌ v) = void $ FinZAbsurd v
	incr {n = S n} i (ʌ v) = ʌ $ incr_var i v
	incr i (λ at b) = λ (incr i at) (incr (FS i) b)
	incr i (λT at rt) = λT (incr i at) (incr (FS i) rt)
	incr i (f =!= a) = incr i f =!= incr i a
	incr i 𝕋 = 𝕋
	incr i (𝔽 at rt b) = 𝔽 (incr i at) (incr (FS i) rt) (incr (FS$ FS$ i) b)
	incr i (𝕌 n t) = 𝕌 n (incr i t)
	incr i (ℂ cn as) = assert_total $ ℂ cn $ map (incr i) as
	incr {n} i (ℙ {a} v cn t f) = ℙ (incr i v) cn (replace (plusSuccRightSucc a n) $ incr (replace (sym $ plusSuccRightSucc a n) $ shift a i) t) (incr i f)
	incr i (𝔹 t) = 𝔹 $ incr i t

	total
	export
	incr' : DAST n -> DAST (a + n)
	incr' {a = Z} ast = ast
	incr' {a = S a} ast = incr 0 $ incr' ast

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling