text:
module JS.Attribute

import Control.Monad.Either
import Data.SOP
import JS.Callback
import JS.Marshall
import JS.Nullable
import JS.Undefined
import JS.Util

||| A read-write attribute of a JS object.
|||
||| @alwaysReturns : Bool index if the attribute's getter can
|||                  always return a value that is neither
|||                  `null` nor `undefined`. This means, that the
|||                  attribute is non-nullable and either mandatory
|||                  or optional with a proper default value.
|||
||| @f             : Context of values represented by the attribute.
|||                  This is `Maybe` if the attribute is nullable,
|||                  `Optional` if it is an optional attribute on
|||                  a dictionary type, or `I` if it is mandatory
|||                  and non-nullable.
|||
||| @              : Type of values stored in the attribute
public export
data Attribute :  (alwaysReturns : Bool)
               -> (f : Type -> Type)
               -> (a : Type)
               -> Type where

  ||| A non-optional attribute.
  |||
  ||| This is for data types, which are guaranteed to always return
  ||| a value that is neither `null` nor `undefined`.
  Attr : (get : JSIO a) -> (set : a -> JSIO ()) -> Attribute True I a

  ||| A nullable, non-optional attribute.
  NullableAttr :  (get : JSIO (Maybe a))
               -> (set : Maybe a -> JSIO ())
               -> Attribute False Maybe a

  ||| An optional attribute with a predefined default value.
  OptionalAttr :  (get : JSIO (Optional a))
               -> (set : Optional a -> JSIO ())
               -> (def : a)
               -> Attribute True Optional a

  ||| An optional attribute without default value.
  OptionalAttrNoDefault :  (get : JSIO (Optional a))
                        -> (set : Optional a -> JSIO ())
                        -> Attribute False Optional a

||| Returns the value of an attribute in its proper context.
||| Typically used in infix notation.
|||
||| ```idris example
||| textField `get` value
||| ```
export
get : (o : obj) -> (attr : obj -> Attribute b f a) -> JSIO $ f a
get o g = case g o of
               Attr                  gt _   => gt
               NullableAttr          gt _   => gt
               OptionalAttr          gt _ _ => gt
               OptionalAttrNoDefault gt _   => gt

||| Maps a function over the value retrieved from an `Attribute`.
export
over : (a -> b) -> (attr : Attribute x f a) -> JSIO $ f b
over f (Attr gt _)                  = map f gt
over f (NullableAttr gt _)          = map f <$> gt
over f (OptionalAttr gt _ _)        = map f <$> gt
over f (OptionalAttrNoDefault gt _) = map f <$> gt

||| Flipped version of `get`. This is useful when
||| combined with the bind operator:
|||
||| ```idris example
||| body >>= to className
||| ```
export
to : (attr : obj -> Attribute b f a) -> (o : obj) -> JSIO $ f a
to = flip get

||| Sets the value of an `Attribute`.
export
set' : (attr : Attribute b f a) -> f a -> JSIO ()
set' (Attr                  _ s)   = s
set' (NullableAttr          _ s)   = s
set' (OptionalAttr          _ s _) = s
set' (OptionalAttrNoDefault _ s)   = s

||| Gets the value of an `Attribute`. Since this operates
||| on an `Attribute True`, it is guaranteed to always yield
||| a non-nullable value.
export
getDef : (o : obj) -> (attr : obj -> Attribute True f a) -> JSIO a
getDef o g = case g o of
                  Attr         gt _     => gt
                  OptionalAttr gt _ def => map (fromOptional def) gt

||| Maps a function over the value retrieved from an `Attribute`.
||| Since this operates
||| on an `Attribute True`, it is guaranteed to always yield
||| a non-nullable value.
export
overDef : (a -> b) -> (attr : Attribute True f a) -> JSIO b
overDef f a = f <$> getDef () (const a)

||| Flipped version of `getDef`.
export
toDef : (attr : obj -> Attribute True f a) -> (o : obj) -> JSIO a
toDef = flip getDef

||| Sets the value of an `Attribute`.
|||
||| ```idris example
||| disabled btn `set` True
||| ```
export
set : Attribute b f a -> a -> JSIO ()
set (Attr         _ s)          y = s y
set (NullableAttr _ s)          y = s (Just y)
set (OptionalAttr _ s _)        y = s (Def y)
set (OptionalAttrNoDefault _ s) y = s (Def y)

||| Modifies the stored value of an `Attribute`.
|||
||| Please note, that this will NOT change the attribute's
||| values, if the attribute is unset or `null`.
export
mod : Attribute b f a -> (a -> a) -> JSIO ()
mod (Attr         g s)          f = g >>= s . f
mod (NullableAttr g s)          f = g >>= s . map f
mod (OptionalAttr g s _)        f = g >>= s . map f
mod (OptionalAttrNoDefault g s) f = g >>= s . map f

||| Unsets the value of an optional or nullable attribute.
export
unset : Alternative f => (o : obj) -> (obj -> Attribute b f a) -> JSIO ()
unset o g = set' (g o) empty

infix 1 .=, =., %=, =%

||| Operator version of `set`.
|||
||| ```idris example
||| disabled btn .= True
||| ```
export
(.=) : Attribute b f a -> a -> JSIO ()
(.=) = set

||| Operator version of `mod`.
|||
||| As with `mod`, this will NOT change the attribute's
||| values, if the attribute is unset or `null`.
|||
||| ```idris example
||| toggleCheckBox : HTMLInputElement -> JSIO ()
||| toggleCheckBox cbx = checked cbx %= not
||| ```
export
(%=) : Attribute b f a -> (a -> a) -> JSIO ()
(%=) = mod

||| Like `set`, but useful when the object, on which
||| an attribute should operate, is supposed to
||| be the last argument (for instance, when
||| iterating over a foldable):
|||
||| ```idris example
||| disableAll : List HTMLButtonElement -> JSIO ()
||| disableAll buttons = for_ buttons $ disabled =. True
||| ```
export
(=.) : (obj -> Attribute b f a) -> a -> obj -> JSIO ()
(=.) f v o = set (f o) v

||| Like `mod`, but useful when the object, on which
||| an attribute should operate, is supposed to
||| be the last argument (for instance, when
||| iterating over a foldable):
|||
||| ```idris example
||| toggleAll : List HTMLInputElement -> JSIO ()
||| toggleAll cbxs = for_ cbxs $ checked =% not
||| ```
export
(=%) : (obj -> Attribute b f a) -> (a -> a) -> obj -> JSIO ()
(=%) f g o = mod (f o) g

infixr 0 !>, ?>

||| Sets a callback function at an attribute.
|||
||| ```idris
||| onclick btn !> consoleLog . jsShow
||| ```
export
(!>) : Callback a fun => Attribute b f a -> fun -> JSIO ()
a !> cb = callback cb >>= set a

||| Sets a callback action at an attribute. This is like `(!>)`
||| but ignores its input.
|||
||| ```idris
||| onclick btn ?> consoleLog "Boom!"
||| ```
export
(?>) : Callback a (x -> y) => Attribute b f a -> y -> JSIO ()
a ?> v = a !> const v

--------------------------------------------------------------------------------
--          Creating Attributes
--------------------------------------------------------------------------------

export
fromPrim :  (ToFFI a b, FromFFI a b)
         => String
         -> (obj -> PrimIO b)
         -> (obj -> b -> PrimIO ())
         -> obj
         -> Attribute True I a
fromPrim msg g s o =
  Attr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))

export
fromNullablePrim :  (ToFFI a b, FromFFI a b)
                 => String
                 -> (obj -> PrimIO $ Nullable b)
                 -> (obj -> Nullable b -> PrimIO ())
                 -> obj
                 -> Attribute False Maybe a
fromNullablePrim msg g s o =
  NullableAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))

export
fromUndefOrPrim :  (ToFFI a b, FromFFI a b)
                => String
                -> (obj -> PrimIO $ UndefOr b)
                -> (obj -> UndefOr b -> PrimIO ())
                -> a
                -> obj
                -> Attribute True Optional a
fromUndefOrPrim msg g s def o =
  OptionalAttr (tryJS msg $ g o) (\a => primJS $ s o (toFFI a)) def

export
fromUndefOrPrimNoDefault :  (ToFFI a b, FromFFI a b)
                         => String
                         -> (obj -> PrimIO $ UndefOr b)
                         -> (obj -> UndefOr b -> PrimIO ())
                         -> obj
                         -> Attribute False Optional a
fromUndefOrPrimNoDefault msg g s o =
  OptionalAttrNoDefault (tryJS msg $ g o) (\a => primJS $ s o (toFFI a))

ext: idr


text:
module Main

-- base
import Data.Nat

record InputData where
  constructor MkInputData
  publicKeyCard : Nat
  publicKeyDoor : Nat

inputData : InputData
inputData = MkInputData 5290733 15231938

namespace Part1
  transformSubjectNumberStep : (subjectNumber : Integer) -> (value : Integer) -> Integer
  transformSubjectNumberStep subjectNumber value = (subjectNumber * value) `mod` 20201227

  export
  loopSize : (publicKeyCard : Nat) -> (subjectNumber : Nat) -> Nat
  loopSize publicKey subjectNumber = try 1 where
    publicKey' : Integer
    publicKey' = natToInteger publicKey
    subjectNumber' : Integer
    subjectNumber' = natToInteger subjectNumber
    try : (value : Integer) -> Nat
    try value = if publicKey' == value
                   then Z
                   else S $ try $ transformSubjectNumberStep subjectNumber' value

  transformSubjectNumber' : (loopSize : Nat) -> (subjectNumber : Integer) -> (value : Integer) -> Integer
  transformSubjectNumber' Z subjectNumber value = value
  transformSubjectNumber' (S k) subjectNumber value =
    transformSubjectNumber' k subjectNumber $ transformSubjectNumberStep subjectNumber value

  export
  transformSubjectNumber : (loopSize : Nat) -> (subjectNumber : Nat) -> Nat
  transformSubjectNumber loopSize subjectNumber =
    integerToNat $ transformSubjectNumber' loopSize (natToInteger subjectNumber) 1

loopSizeCard : Nat
loopSizeCard = loopSize inputData.publicKeyCard 7

encryptionKey1 : Nat
encryptionKey1 = transformSubjectNumber loopSizeCard inputData.publicKeyDoor

loopSizeDoor : Nat
loopSizeDoor = loopSize inputData.publicKeyDoor 7

encryptionKey2 : Nat
encryptionKey2 = transformSubjectNumber loopSizeDoor inputData.publicKeyCard

main : IO ()
main = do
  putStrLn . show $ encryptionKey1
  putStrLn . show $ encryptionKey2
  pure ()


text:
-- My answer to the question in Slack https://functionalprogramming.slack.com/archives/C043A0KTY/p1613365432408100

import Syntax.PreorderReasoning

import Data.Nat

mult_plus_distr : (n, m, p : Nat) -> (n + m) * p = (n * p) + (m * p)
mult_plus_distr 0 m p = Refl
mult_plus_distr (S k) m p =
  let ih = mult_plus_distr k m p
  in rewrite ih in plusAssociative p (mult k p) (mult m p)

mult_assoc : (n, m, p : Nat) -> n * (m * p) = (n * m) * p
mult_assoc Z m p = Refl
mult_assoc (S k) m p = Calc $
  |~ (S k) * (m * p)
  ~~ (m * p) + k * (m * p) ... ( Refl )
  ~~ (m * p) + (k * m) * p ... ( cong ((m * p) +) $ mult_assoc k m p )
  ~~ (m + k * m) * p       ... ( sym $ mult_plus_distr m (k * m) p )

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Idris.IDEMode.CaseSplit

import Core.Context
import Core.Context.Log
import Core.Env
import Core.Metadata
import Core.TT
import Core.Value

import Parser.Lexer.Source
import Parser.Unlit

import TTImp.Interactive.CaseSplit
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Utils

import Idris.IDEMode.TokenLine
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax

import Data.List
import Data.List1
import Libraries.Data.List.Extra
import Libraries.Data.String.Extra
import Data.String
import System.File

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

||| A series of updates is a mapping from `RawName` to `String`
||| `RawName` is currently just an alias for `String`
||| `String` is a rendered `List SourcePart`
Updates : Type
Updates = List (RawName, String)

||| Convert a RawImp update to a SourcePart one
toStrUpdate : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              (Name, RawImp) -> Core Updates
toStrUpdate (UN (Basic n), term)
    = do clause <- pterm (map defaultKindedName term) -- hack
         pure [(n, show (bracket clause))]
  where
    bracket : PTerm' nm -> PTerm' nm
    bracket tm@(PRef _ _) = tm
    bracket tm@(PList _ _ _) = tm
    bracket tm@(PSnocList _ _ _) = tm
    bracket tm@(PPair _ _ _) = tm
    bracket tm@(PUnit _) = tm
    bracket tm@(PComprehension _ _ _) = tm
    bracket tm@(PPrimVal _ _) = tm
    bracket tm = PBracketed emptyFC tm
toStrUpdate _ = pure [] -- can't replace non user names

data UPD : Type where

||| Given a list of definitions, a list of mappings from `RawName` to `String`,
||| and a list of tokens to update, work out the updates to do, apply them, and
||| return the result.
doUpdates : {auto u : Ref UPD (List String)} ->
            Defs -> Updates -> List SourcePart ->
            Core (List SourcePart)
doUpdates defs ups [] = pure []   -- no more tokens to update, so we are done
-- if we have an LBrace (i.e. `{`), handle its contents
doUpdates defs ups (LBrace :: xs)
    -- the cases we care about are easy to detect w/o whitespace, so separate it
    = let (ws, nws) = span isWhitespace xs in
        case nws of
          -- handle potential whitespace in the other parts
          Name n :: rest =>
             let (ws', nws') = span isWhitespace rest in
               case nws' of
                  -- brace is immediately closed, so generate a new
                  -- pattern-match on the values the name can have, e.g.
                  -- { x}  where x : Nat would become { x = Z}
                  --                       (and later { x = (S k)})
                  RBrace :: rest' =>
                    pure (LBrace :: ws ++
                          Name n :: Whitespace " " :: Equal :: Whitespace " " ::
                          !(doUpdates defs ups (Name n :: ws' ++ RBrace :: rest'))
                          )
                  -- preserve whitespace before (and after) the Equal
                  Equal :: rest' =>
                    let (ws'', nws'') = span isWhitespace rest' in
                    pure (LBrace :: ws ++
                          Name n :: ws' ++ Equal :: ws'' ++
                          !(doUpdates defs ups nws'')
                          )
                  -- handle everything else as usual, preserving whitespace
                  _ => pure (LBrace :: ws ++ Name n :: ws' ++
                             !(doUpdates defs ups rest)
                             )
          -- not a special case: proceed as normal
          _ => pure (LBrace :: [] ++ !(doUpdates defs ups xs))
  where
    isWhitespace : SourcePart -> Bool
    isWhitespace (Whitespace _) = True
    isWhitespace _              = False
-- if we have a name, look up if it's a name we're updating. If it isn't, keep
-- the old name, otherwise update the name, i.e. replace with the new name
doUpdates defs ups (Name n :: xs)
    = case lookup n ups of
           Nothing => pure (Name n :: !(doUpdates defs ups xs))
           Just up => pure (Other up :: !(doUpdates defs ups xs))
-- if we have a hole, get the used names, generate+register a new unique name,
-- and change the hole's name to the new one
doUpdates defs ups (HoleName n :: xs)
    = do used <- get UPD
         n' <- uniqueName defs used n
         put UPD (n' :: used)
         pure $ HoleName n' :: !(doUpdates defs ups xs)
-- if it's not a thing we update, leave it and continue working on the rest
doUpdates defs ups (x :: xs)
    = pure $ x :: !(doUpdates defs ups xs)

-- State here is a list of new hole names we generated (so as not to reuse any).
-- Update the token list with the string replacements for each match, and return
-- the newly generated strings.
updateAll : {auto u : Ref UPD (List String)} ->
            Defs -> List SourcePart -> List Updates ->
            Core (List String)
updateAll defs l [] = pure []
updateAll defs l (rs :: rss)
    = do l' <- doUpdates defs rs l
         rss' <- updateAll defs l rss
         pure (concatMap toString l' :: rss')

-- Turn the replacements we got from 'getSplits' into a list of actual string
-- replacements
getReplaces : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
              List (Name, RawImp) -> Core Updates
getReplaces updates
    = do strups <- traverse toStrUpdate updates
         pure (concat strups)

showImpossible : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 (indent : Nat) -> RawImp -> Core String
showImpossible indent lhs
    = do clause <- pterm (map defaultKindedName lhs) -- hack
         pure (fastPack (replicate indent ' ') ++ show clause ++ " impossible")

-- Given a list of updates and a line and column, find the relevant line in
-- the source file and return the lines to replace it with
export
updateCase : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto o : Ref ROpts REPLOpts} ->
             List ClauseUpdate -> Int -> Int ->
             Core (List String)
updateCase splits line col
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => throw (InternalError "No file loaded")
              Just f =>
                do Right file <- coreLift $ readFile f
                       | Left err => throw (FileErr f err)
                   let thisline = elemAt (forget $ lines file) (integerToNat (cast line))
                   case thisline of
                        Nothing => throw (InternalError "File too short!")
                        Just l =>
                            do let valid = mapMaybe getValid splits
                               let bad = mapMaybe getBad splits
                               log "interaction.casesplit" 3 $ "Valid: " ++ show valid
                               log "interaction.casesplit" 3 $ "Bad: " ++ show bad
                               if isNil valid
                                  then do let indent = getIndent 0 $ fastUnpack l
                                          traverse (showImpossible indent) bad
                                  else do rs <- traverse getReplaces valid
                                          let stok = tokens l
                                          defs <- get Ctxt
                                          u <- newRef UPD []
                                          updateAll defs stok rs
  where
    getValid : ClauseUpdate -> Maybe (List (Name, RawImp))
    getValid (Valid _ ups) = Just ups
    getValid _ = Nothing

    getBad : ClauseUpdate -> Maybe RawImp
    getBad (Impossible lhs) = Just lhs
    getBad _ = Nothing

    getIndent : (acc : Nat) -> List Char -> Nat
    getIndent acc [] = acc
    getIndent acc (' ' :: xs) = getIndent (acc + 1) xs
    getIndent acc _ = acc

fnName : Bool -> Name -> String
fnName lhs (UN (Basic n))
    = if isIdentNormal n then n
      else if lhs then "(" ++ n ++ ")"
      else "op"
fnName lhs (NS _ n) = fnName lhs n
fnName lhs (DN s _) = s
fnName lhs n = nameRoot n

export
getClause : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            Int -> Name -> Core (Maybe String)
getClause l n
    = do defs <- get Ctxt
         Just (loc, nidx, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p)
             | Nothing => pure Nothing
         n <- getFullName nidx
         argns <- getEnvArgNames defs envlen !(nf defs [] ty)
         Just srcLine <- getSourceLine l
           | Nothing => pure Nothing
         let (mark, src) = isLitLine srcLine
         pure (Just (indent mark loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                  " = ?" ++ fnName False n ++ "_rhs"))
  where
    indent : Maybe String -> NonEmptyFC -> String
    indent (Just mark) fc
        = relit (Just mark) $ pack (replicate (integerToNat (cast (max 0 (snd (startPos fc) - 1)))) ' ')
    indent Nothing fc = pack (replicate (integerToNat (cast (snd (startPos fc)))) ' ')


text:
import Drahko

foo : Promise ()
foo = do
    tooltip "Clicking"
    sleep 50
    sendInput "{Click}"
    sleep 50
    sendInput "{Click}"
    sleep 150

main : Promise ()
main = do
  hotkey "F11" $ do
    tooltip "Reloading"
    sleep 500
    reload ()

  hotkey "F12" foo

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/idris-autohotkey

max_forks_repo_name: drahko/drahko


text:
module Main

import Effects
import Effect.StdIO
import Effect.Random

data GameState = NotRunning
               | Running Nat

data GameInfo : GameState -> Type where
     Number : (guesses : Nat) ->
              (answer : Int) -> GameInfo (Running (S guesses))
     Lost : (answer : Int) -> GameInfo (Running Z)
     Init : GameInfo NotRunning

data Result = TooLow | Correct | TooHigh

data GuessNumber : Effect where
     GuessNum : Int ->
             sig GuessNumber Result
                 (GameInfo (Running (S k)))
                 (\guess =>
                       GameInfo (case guess of
                                      Correct => NotRunning
                                      _ => Running k))
     Quit : sig GuessNumber Int (GameInfo (Running Z)) (GameInfo NotRunning)

GUESS : GameState -> EFFECT
GUESS t = MkEff (GameInfo t) GuessNumber

guess : Int -> { [GUESS (Running (S k))] ==>
                 {guess} [GUESS (case guess of
                                      Correct => NotRunning
                                      _ => Running k)] } Eff Result
guess n = call $ GuessNum n

quit : Eff Int [GUESS (Running Z)] [GUESS NotRunning]
quit = call Quit

Handler GuessNumber m where
    handle (Number g n) (GuessNum i) k with (compare i n)
      handle (Number (S g) n) (GuessNum i) k | LT = k TooLow (Number g n)
      handle (Number Z n) (GuessNum i) k | LT = k TooLow (Lost n)
      handle (Number g n) (GuessNum i) k | EQ = k Correct Init
      handle (Number Z n) (GuessNum i) k | GT = k TooHigh (Lost n)
      handle (Number (S g) n) (GuessNum i) k | GT = k TooHigh (Number g n)
    handle (Lost n) Quit k = k n Init

game : Eff () [GUESS (Running n), STDIO] [GUESS NotRunning, STDIO]
game {n=Z} = do putStrLn "You lose"
                ans <- quit
                putStrLn $ "The answer was " ++ show ans
game {n=S g}
     = do putStr "Guess: "
          let num = cast (trim !getStr)
          case !(guess num) of
               TooLow => do putStrLn "Too low"
                            game
               Correct => putStrLn "You win!"
               TooHigh => do putStrLn "Too high"
                             game

main : IO ()
main = runInit [Number 5 42, ()] game

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
import Aoc
import Data.List
import Data.SortedMap
import Data.Strings
%default total

play : List Int -> Nat -> Int
play input finalTurn =
    let n = length input
        d0 = fromList $ zip input [1..cast n]
    in go d0 (cast n+1) 0 (minus finalTurn (n+1))
  where
    ||| We're on turn `t`, and its number is `n`.
    ||| `d` maps numbers to the last turn they were said.
    ||| The game ends `fuel` turns from now.
    go : SortedMap Int Int -> (turn : Int) -> (num : Int) -> (fuel : Nat) -> Int
    go d t n Z = n
    go d t n (S k) = go (insert n t d) (t+1) (maybe 0 (t-) (lookup n d)) k

main : IO ()
main = do
  input <- parseLines parseInteger
  putStr "*   "; printLn (play input 2020)
  putStr "**  "; printLn (play input 30000000)


text:
module Skeletons.Farm

import System
import Data.List

import System.Concurrency.BufferedChannel

%default total

||| A worker can either get another task or an indication that there is no more
||| work so it should stop.
public export
data WorkUnit : Type -> Type where
  TASK : Lazy task -> WorkUnit task
  STOP : WorkUnit _

||| A work result is either a value resulting from running the work, or an
||| indication that the worker is done (i.e. that it received a `STOP`
||| @WorkUnit@).
public export
data WorkResult : Type -> Type where
  RES : val -> WorkResult val
  DONE : WorkResult _

||| A Farm is a skeleton consisting of a maximum number of workers/threads to
||| use, and a list of independent work-units to be done. Since each work-unit
||| is self-contained, they can be run in parallel with workers picking up new
||| work-units as they finish their current one. This repeats until all the
||| work-units have been computed.
export
data Farm : Type -> Type where
  MkFarm : (nWorkers : Nat)
         -> (work : List (WorkUnit resTy))
         -> Farm resTy

||| Create a new farm which uses the specified number of workers and does the
||| specified work.
|||
||| @nWorkers The number of workers (threads) the farm can use.
||| @work     A list of `WorkUnit`s that the workers need to do.
export
initFarm : (nWorkers : Nat) -> (work : List (WorkUnit resTy)) -> Farm resTy
initFarm = MkFarm

||| A basic unit of work in a farm. Retrieves work from the channel referenced
||| in workRef, sending the results to outRef, until a `STOP` instruction is
||| received.
worker : (workRef : IORef (BufferedChannel (WorkUnit a)))
       -> (outRef : IORef (BufferedChannel (WorkResult a)))
       -> IO ()
worker workRef outRef =
  do (MkDPair workChan recv) <- becomeReceiver Blocking workRef
     (MkDPair outChan send) <- becomeSender outRef
     (TASK task) <- recv workChan
        | STOP => send Signal outChan DONE
     send Signal outChan (RES task)
     --                   ^ TASK is Lazy, but RES is not  => evaluation!
     let workRef' = assert_smaller workRef workRef
     --             ^ Idris cannot know recv reduces the size of shared channel
     worker workRef' outRef

||| Given a list of ThreadIDs, fork a single thread whose sole purpose is
||| waiting on all those threads to finish.
waitOnThreadBundle : (ts : List ThreadID)
                   -> IO ThreadID
waitOnThreadBundle ts = fork $ ignore (traverse (\t => threadWait t) ts)

||| Given a farm containing a list of work, create a BufferedChannel containing
||| all the work and a number of `STOP` instructions equal to the number of
||| workers in the farm.
|||
||| @farm The farm whose work needs to be loaded into a BufferedChannel.
loadWork : (farm : Farm a)
         -> IO (IORef (BufferedChannel (WorkUnit a)))
loadWork (MkFarm nWorkers work) =
  do putStr "Loading work... "
     workRef <- makeBufferedChannel
     (MkDPair workChan flexSend) <- becomeSender workRef
     let send = flexSend Signal
     ignore $ traverse (\w => send workChan w) work
     ignore $ for (replicate nWorkers STOP) (\stop => send workChan stop)
     putStrLn "Done."
     pure workRef

||| Given a number of workers, a referenence to a channel on which to receive
||| work, and a reference to a channel on which the workers can put their
||| result(s), spawns @nWorkers@ many threads wired up to the channels as
||| appropriate.
|||
||| @nWorkers The number of worker threads to spawn.
||| @workRef  An IORef to a BufferedChannel on which to receive work units.
||| @outRef   An IORef to a BufferedChannel on which to send the work results.
spawnWorkers : (nWorkers : Nat)
             -> (workRef : IORef (BufferedChannel (WorkUnit a)))
             -> (outRef : IORef (BufferedChannel (WorkResult a)))
             -> IO (List ThreadID)
spawnWorkers 0 _ _ = pure []
spawnWorkers (S k) workRef outRef =
  do workerThreadID <- fork $ worker workRef outRef
     workerThreadIDs <- spawnWorkers k workRef outRef
     pure (workerThreadID :: workerThreadIDs)

||| Run a farm, spawning n threads where n is the number of workers in the farm.
||| Returns a @ThreadID@ representing a thread waiting on all the workers in the
||| farm, and an @IORef@ to a @BufferedChannel@ over which to receive the work
||| results.
|||
||| @farm The farm to run.
export
runFarm : (farm : Farm a)
        -> IO (ThreadID, IORef (BufferedChannel (WorkResult a)))
runFarm farm@(MkFarm nWorkers work) =
  do outRef <- makeBufferedChannel
     workRef <- loadWork farm
     workerThreadIDs <- spawnWorkers nWorkers workRef outRef
     putStrLn $ "Spawned " ++ show nWorkers ++ " workers."
     bundleThreadID <- waitOnThreadBundle workerThreadIDs
     pure (bundleThreadID, outRef)

||| Retrieve all the output from a farm that has been run.
|||
||| @farm   The farm that was run.
||| @runRes The pair that was returned from calling `runFarm` on the farm.
export
collect : (farm : Farm a)
        -> (runRes : (ThreadID, IORef (BufferedChannel (WorkResult a))))
        -> IO (List a)
collect (MkFarm nWorkers _) (bundleThreadID, resRef) =
  do resList <- collect' [] nWorkers resRef
     putStrLn "Collected all results, waiting for worker threads to stop..."
     threadWait bundleThreadID
     putStrLn "All workers stopped, returning results."
     pure resList
  where
    collect' : List a -> Nat -> IORef (BufferedChannel (WorkResult a)) -> IO (List a)
    collect' acc 0 _ = pure acc
    collect' acc (S k) resRef =
      do (MkDPair resChan recv) <- becomeReceiver Blocking resRef
         workRes <- recv resChan
         -- (note: having `assert_smaller` here doesn't work)
         case workRes of
              (RES val) => do let resRef' = assert_smaller resRef resRef
                              collect' (val :: acc) (S k) resRef'
              DONE => do let resRef' = assert_smaller resRef resRef
                         collect' acc k resRef'   -- one worker done, so reduce k


text:
module Main

-- Required by usleep
import System

import Data.String

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

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

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

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
import SimpleDataRealizedFunction
%default total

-- module Main

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)

rlz_incrementer : SimpleDataRealizedFunction (Int -> Int)  100 1.0
rlz_incrementer = MkSimpleDataRealizedFunction incrementer 100 1.0

-- Realized twicer
twicer : Int -> Int
twicer = (*2)

rlz_twicer : SimpleDataRealizedFunction (Int -> Int)  500 0.9
rlz_twicer = MkSimpleDataRealizedFunction twicer 500 0.9

-- Realized (twicer . incrementer).
rlz_composition : SimpleDataRealizedFunction (Int -> Int)  600 0.9
-- The following does not work because 601 ≠ 100+500 and 1.0 ≠ (min 1.0 0.9)
-- rlz_composition : SimpleDataRealizedFunction (Int -> Int) 601 1.0
rlz_composition = compose rlz_twicer rlz_incrementer

-- Simple test, result should be (3+1)*2 = 8
rslt : Int -> Int
rslt = apply rlz_composition

rsltTest : (rslt 3) = 8
rsltTest = Refl

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible


text:
module Flexidisc.OrdList.SubWithKeys

import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Sub
import Flexidisc.OrdList.Type

import Data.List

import public Data.List

%default total

||| Proof that an `OrdList` has some given `keys` and is a sublist of an other
public export
data SubWithKeys : (keys : List k) -> (xs, ys : OrdList k v o) -> Type where
  ||| The empty `Ordlist` is a sublist of the empty `OrdList`
  Empty : SubWithKeys [] [] []
  ||| Making the second list larger don't change the property
  Skip  : SubWithKeys keys xs ys -> SubWithKeys keys xs (y::ys)
  ||| To add an element to the first list, we need to add it to the second one
  Keep  : (loc : Elem k keys) -> SubWithKeys (dropElem keys loc) xs ys ->
          SubWithKeys keys ((k, ty)::xs) ((k, ty)::ys)

Uninhabited (SubWithKeys (x::xs) sub []) where
  uninhabited Empty impossible
  uninhabited (Skip _) impossible
  uninhabited (Keep _ _) impossible

%name SubWithKeys sub, issub, ss

export
toSub : SubWithKeys keys xs ys -> Sub xs ys
toSub Empty = Empty
toSub (Skip sub) = Skip (toSub sub)
toSub (Keep x sub) = Keep (toSub sub)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Data.Crypto.Util

import Data.Bits
import Data.Fin
import Data.Vect

import Data.Mod

%default total

trim : Bits (1 + n) -> Bits n
trim b = truncate (shiftRightLogical (intToBits 1) b)

public export
bitsToFin : Bits n -> Fin (power 2 n)
bitsToFin {n=Z}   _ = FZ
--bitsToFin {n=S _} b = let x = FS (FS FZ) * (bitsToFin (trim b))
--                      in if (b `and` (intToBits 1)) == (intToBits 0)
--                         then x
--                         else FS x
bitsToFin {n=S n} bits = fromMaybe (rewrite snd $ pow2NotZ n in FZ) (integerToFin (bitsToInt bits) (power 2 (S n)))
  where
  pow2NotZ : (n: Nat) -> (k ** power 2 n = S k)
  pow2NotZ  Z    = (Z**Refl)
  pow2NotZ (S n) = let (k**prf) = pow2NotZ n in
                   rewrite prf in
                   (k+(S (k+0))**Refl)

partial
divCeil : Nat -> Nat -> Nat
divCeil x y = case x `mod` y of
                Z   => x `div` y
                S _ => S (x `div` y)

public export
natToFi : (i : Nat) -> LTE i n -> Fin (S n)
natToFi  Z     LTEZero    = FZ
natToFi (S k) (LTESucc p) = FS (natToFi k p)

public export
finToBits : Fin n -> Bits (nextPow2 n)
finToBits = intToBits . finToInteger

public export
modToBits : Mod n -> Bits (nextPow2 n)
modToBits = intToBits . modToInteger

public export
rotateLeft : Nat -> Bits n -> Bits n
rotateLeft {n=n} rot bits =
  let norm = modNatNZ rot (S n) (uninhabited . sym)
  in shiftLeft bits (intToBits (cast norm)) `or` shiftRightLogical bits (intToBits (cast ((S n) `minus` norm)))

-- FIXME: This is rotateLeft currently. Need to change the impl
public export
rotateRight : Nat -> Bits n -> Bits n
rotateRight {n=n} rot bits =
  let norm = modNatNZ rot (S n) (uninhabited . sym)
  in shiftLeft bits (intToBits (cast norm)) `or` shiftRightLogical bits (intToBits (cast ((S n) `minus` norm)))

public export
swap : Fin n -> Fin n -> Vect n a -> Vect n a
swap i j v = replaceAt j (index i v) (replaceAt i (index j v) v)

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

public export
tightmod : Nat -> (m : Nat) -> {default () ok : notZero m} -> Fin m
tightmod _ Z {ok=prf} = void prf
tightmod left (S modulus) = tightmod' left left modulus
  where
    tightmod' : Nat -> Nat -> (n : Nat) -> Fin (S n)
    tightmod' Z center right = fromMaybe FZ (natToFin center (S right))
    tightmod' (S left) center right =
      if lte center right
      then fromMaybe FZ (natToFin center (S right))
      else tightmod' left (center `minus` (S right)) right

public export
Byte : Type
Byte = Bits 8

public export
interface Serializable a where
  encode : a -> List (Bits n)
  decode : List (Bits n) -> a

-- Arrow defined for functions
infixr 3 ***
infixr 3 &&&
public export first : (a -> c) -> (a, b) -> (c, b)
first f = \(a, b) => (f a, b)
public export second : (b -> d) -> (a, b) -> (a, d)
second f = \(a, b) => (a, f b)
public export (***) : (a -> c) -> (b -> d) -> (a, b) -> (c, d)
f *** g = \(a, b) => (f a, g b)
public export (&&&) : (a -> c) -> (a -> d) -> a -> (c, d)
f &&& g = \a => (f a, g a)

postulate minusPlusIdentity : (m, n : Nat) -> (m `minus` n) + n = m
postulate plusMinusIdentity : (m, n : Nat) -> n + (m `minus` n) = m

public export
partition : Bits (m * n) -> Vect m (Bits n)
partition {m=Z}       _    = []
partition {m=S m} {n} bits =
  truncate (replace (plusCommutative n (m*n)) bits)
   :: partition (truncate (shiftRightLogical bits (intToBits (cast n))))

public export
partition' : Bits m -> (List (Bits n), (p : Nat ** Bits p))
partition' {m} {n} bits = part m bits
  where part : Nat -> Bits r -> (List (Bits n), (p : Nat ** Bits p))
        part      Z    bits = ([], (0 ** intToBits 0))
        part {r} (S q) bits =
          if r < n
          then ([], (r ** bits))
          else
            first (List.(::) (truncate (replace (sym (minusPlusIdentity r n)) (shiftRightLogical bits (intToBits (cast (r `minus` n)))))))
                  (part q (truncate (replace (sym (plusMinusIdentity r n)) bits)))

public export
append : Bits m -> Bits n -> Bits (m + n)
append {m} {n} a b = shiftLeft (zeroExtend a) (intToBits (cast n)) `or` (rewrite plusCommutative m n in zeroExtend b)

public export
concat : Vect m (Bits n) -> Bits (m * n)
concat {m=Z}       _         = intToBits 0
concat {m=S Z} {n} [bits]    = rewrite plusZeroRightNeutral n in bits
concat {m=S _}     (b::rest) = append b (concat rest)

public export
repartition : Vect m (Bits n) -> List (Bits q)
repartition = fst . partition' . Data.Crypto.Util.concat -- not at all efficient

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module Decidable.Equality.Core

%default total

--------------------------------------------------------------------------------
-- Decidable equality
--------------------------------------------------------------------------------

||| Decision procedures for propositional equality
public export
interface DecEq t where
  ||| Decide whether two elements of `t` are propositionally equal
  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

--------------------------------------------------------------------------------
-- Utility lemmas
--------------------------------------------------------------------------------

||| The negation of equality is symmetric (follows from symmetry of equality)
export
negEqSym : Not (a = b) -> Not (b = a)
negEqSym p h = p (sym h)

||| Everything is decidably equal to itself
export
decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
decEqSelfIsYes with (decEq x x)
  decEqSelfIsYes | Yes Refl = Refl
  decEqSelfIsYes | No contra = absurd $ contra Refl

||| If you have a proof of inequality, you're sure that `decEq` would give a `No`.
export
decEqContraIsNo : DecEq a => {x, y : a} -> Not (x = y) -> (p ** decEq x y = No p)
decEqContraIsNo uxy with (decEq x y)
  decEqContraIsNo uxy | Yes xy = absurd $ uxy xy
  decEqContraIsNo _   | No uxy = (uxy ** Refl)


text:
module average

export

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

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

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
module Js.BrowserForeigns

import public Js.ASync

%access export

lenChilds : Ptr -> JS_IO Int
lenChilds node = jscall "%0.childNodes.length" (Ptr -> JS_IO Int) node

clearContents : Ptr -> JS_IO ()
clearContents x =
  jscall
  "function(z){while(z.lastChild){z.removeChild(z.lastChild);}}(%0)"
  (Ptr -> JS_IO ())
  x

removeChildNode : Ptr -> Ptr -> JS_IO ()
removeChildNode node child = jscall "%0.removeChild(%1)" (Ptr -> Ptr -> JS_IO ()) node child

childNode : Int -> Ptr -> JS_IO Ptr
childNode pos node = jscall "%0.childNodes[%1]" (Ptr -> Int -> JS_IO Ptr) node pos

setTextContent : Ptr -> String -> JS_IO ()
setTextContent node s = jscall "%0.textContent = %1" (Ptr -> String -> JS_IO ()) node s

appendChild : Ptr -> Ptr -> JS_IO Ptr
appendChild node child = jscall "%0.appendChild(%1)" (Ptr -> Ptr -> JS_IO Ptr) node child

insertBeforeNode : Ptr -> Ptr -> Ptr -> JS_IO Ptr
insertBeforeNode node new next = jscall "%0.insertBefore(%1,%2)" (Ptr -> Ptr -> Ptr -> JS_IO Ptr) node new next

parentNode : Ptr -> JS_IO Ptr
parentNode node = jscall "%0.parentNode" (Ptr -> JS_IO Ptr) node

docBody : JS_IO Ptr
docBody = jscall "document.body" (() -> JS_IO Ptr) ()

replaceChild : Ptr -> Ptr -> Ptr -> JS_IO ()
replaceChild parent new old = jscall "%0.replaceChild(%1, %2)" (Ptr -> Ptr -> Ptr -> JS_IO ()) parent new old

createElement : String -> JS_IO Ptr
createElement s = jscall "document.createElement(%0)" (String -> JS_IO Ptr) s

createElementNS : String -> String -> JS_IO Ptr
createElementNS n s = jscall "document.createElementNS(%0,%1)" (String -> String -> JS_IO Ptr) n s

setAttr : Maybe String -> Ptr -> (String, String) -> JS_IO ()
setAttr Nothing node (k,v) = jscall "%0.setAttribute(%1, %2)" (Ptr -> String -> String -> JS_IO ()) node k v
setAttr (Just ns) node (k,v) = jscall "%0.setAttributeNS(%3,%1, %2)" (Ptr -> String -> String -> String -> JS_IO ()) node k v ns

removeAttr : Ptr -> String -> JS_IO ()
removeAttr node k = jscall "%0.removeAttribute(%1)" (Ptr -> String -> JS_IO ()) node k

addEventListener : Ptr -> String -> (Ptr -> JS_IO ()) -> JS_IO ()
addEventListener node evt action =
  jscall
    "%0.addEventListener(%1, %2)"
    (Ptr -> String -> (JsFn (Ptr -> JS_IO ())) -> JS_IO ())
    node
    evt
    (MkJsFn action)

getElementById : String -> JS_IO Ptr
getElementById x = jscall "document.getElementById(%0)" (String -> JS_IO Ptr) x

setVal : Ptr -> String -> JS_IO ()
setVal node val = jscall "%0.value = %1" (Ptr->String->JS_IO ()) node val

setClass : Ptr -> String -> JS_IO ()
setClass node val = jscall "%0.className = %1" (Ptr->String->JS_IO ()) node val

setSelected : Ptr -> Bool -> JS_IO ()
setSelected node True = jscall "%0.selected = true" (Ptr->JS_IO ()) node
setSelected node False = jscall "%0.selected = false" (Ptr->JS_IO ()) node

------ Network -------

httpGet_raw : String -> (String -> JS_IO ()) -> JS_IO ()
httpGet_raw url callback =
  jscall
    ("function(){var xmlhttp=new XMLHttpRequest();console.log(%0);"++
    "xmlhttp.onreadystatechange=function(){if(xmlhttp.readyState==4){"++
    "if(xmlhttp.status==200){console.log(xmlhttp.responseText);%1(xmlhttp.responseText)}} };"++
    "xmlhttp.open('GET',%0, true);"++
    "xmlhttp.send(null);}()")
    (String -> (JsFn (String -> JS_IO ())) -> JS_IO ())
    url
    (MkJsFn callback)

httpPost_raw : String -> String -> (String -> JS_IO ()) -> JS_IO ()
httpPost_raw url body callback =
  jscall
    ("function(){var xmlhttp=new XMLHttpRequest();"++
    "xmlhttp.onreadystatechange=function(){if(xmlhttp.readyState==4){"++
    "if(xmlhttp.status==200){%2(xmlhttp.responseText)}} };"++
    "xmlhttp.open('POST',%0, true);"++
    "xmlhttp.send(%1);}()")
    (String -> String -> (JsFn (String -> JS_IO ())) -> JS_IO ())
    url
    body
    (MkJsFn callback)

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
import System
import Fuel
import Arith

import Command

data Input = Answer Int
           | QuitCmd

data Score = MkScore Nat Nat

Show Score where
  show (MkScore y n) = (show y ++ " / " ++ show (y + n))

addCorrect : Score -> Score
addCorrect (MkScore k j) = MkScore (k + 1) j

addWrong : Score -> Score
addWrong (MkScore k j) = MkScore k (j + 1)

readInput : (prompt : String) -> Command Input
readInput prompt = do
  PutStr prompt
  answer <- GetLine
  if toLower answer == "quit"
    then Pure QuitCmd
    else Pure (Answer (cast answer))

mutual
  correct : Stream Int -> (score : Score) -> ConsoleIO Score
  correct nums score
    = do PutStr "Correct!\n"
         quiz nums (addCorrect score)

  wrong : Stream Int -> Int -> (score : Score) -> ConsoleIO Score
  wrong nums answer score
    = do PutStr ("Wrong, the answer is " ++ show answer ++ "\n")
         quiz nums (addWrong score)

  quiz : Stream Int -> (score : Score) -> ConsoleIO Score
  quiz (num1 :: num2 :: nums) score
    = do PutStr ("Score: " ++ show score ++ "\n")
         input <- readInput (show num1 ++ " * " ++ show num2 ++ " ")
         case input of
           Answer answer => if (answer == num1 * num2)
                             then correct nums score
                             else wrong nums (num1 * num2) score
           QuitCmd => Quit score

partial
main : IO ()
main = do
  seed <- time
  Just score <- run forever (quiz (arithInputs (fromInteger seed)) (MkScore 0 0))
       | Nothing => putStrLn "Out Of Fuel"

  putStrLn ("Final Score: " ++ show score)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
> module Equality.Properties

> import Unique.Predicates

> %default total

> %access public export

> ||| If |P| and |Q| are equality decidable, |(P , Q)| is equality decidable
> decPair : {P, Q : Type} -> DecEq P -> DecEq Q -> DecEq (P , Q)
> decPair {P} {Q} dp dq = %implementation
> {-
> decPair {P} {Q} dp dq = d where
>   implementation [d] DecEq (P, Q) where
>     decEq _ _ = ?kiku
> -}

> ||| Equality is unique
> uniqueEq : {A : Type} -> (a1 : A) -> (a2 : A) -> Unique (a1 = a2)
> uniqueEq a a Refl Refl = Refl
> %freeze uniqueEq -- frozen

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module HintFunction

import Data.Fuel

import HintFunctionGen

export %hint
listOfLim : Fuel -> Gen a => Gen (List a)
listOfLim Dry      @{genA} = pure [] <|> pure <$> genA
listOfLim (More f) @{genA} = let sub = listOfLim f in sub <|> [| genA :: sub |]

export
al : (Fuel -> Gen (List a)) => Gen a
al @{genList} = do
  xs <- genList $ limit 2
  choiceMap pure xs

export
al' : (Fuel -> Gen (List Int)) => String
al' @{genList} = show $ genList $ limit 2

export %hint
genNat : Gen Int
genNat = pure 0 <|> pure 1

export
xx : Gen Int
xx = al

export
yy : String
yy = al' -- @{listOfLim}


text:
module Libgit.Types

import System.FFI

||| A simple type alias for Git results which can either return a non-zero
||| integer error code or a result.
public export
GitResult : Type -> Type
GitResult a = Either Int a

||| Given an error code and some object, create a GitResult.
export
toGitResult : Int -> a -> GitResult a
toGitResult err x = case err < 0 of
  True => Left err
  False => Right x

||| An opaque type representing a Git repository.
public export
data GitRepository : Type where
  MkGitRepository : AnyPtr -> GitRepository

||| An opaque type representing a Git object id.
public export
data GitOid : Type where
  MkGitOid : AnyPtr -> GitOid

||| Git object types
public export
data GitObjectType = GitObjectAny
                   | GitObjectBad
                   | GitObjectCommit
                   | GitObjectTree
                   | GitObjectBlob
                   | GitObjectTag
                   | GitObjectOfsDelta
                   | GitObjectRefDelta

public export
data IsCommitish : GitObjectType -> Type where
  IsCommitishCommit : IsCommitish GitObjectCommit
  IsCommitishTag : IsCommitish GitObjectTag

export
gitObjectTypeToInt : GitObjectType -> Int
gitObjectTypeToInt GitObjectAny = -2
gitObjectTypeToInt GitObjectBad = -1
gitObjectTypeToInt GitObjectCommit = 1
gitObjectTypeToInt GitObjectTree = 2
gitObjectTypeToInt GitObjectBlob = 3
gitObjectTypeToInt GitObjectTag = 4
gitObjectTypeToInt GitObjectOfsDelta = 6
gitObjectTypeToInt GitObjectRefDelta = 7

export
gitObjectTypeFromInt : Int -> GitObjectType
gitObjectTypeFromInt x = case x of
  1 => GitObjectCommit
  2 => GitObjectTree
  3 => GitObjectBlob
  4 => GitObjectTag
  6 => GitObjectOfsDelta
  7 => GitObjectRefDelta
  _ => if x == -2
         then GitObjectAny
         else GitObjectBad -- This is kind of a hack, but kind of not.

public export
data GitObject : (typ : GitObjectType) -> Type where
  MkGitObject : AnyPtr -> GitObject typ

public export
data GitRemote : Type where
  MkGitRemote : AnyPtr -> GitRemote

max_forks_repo_name: bigs/libgit-idris


text:
module Control.Applicative.Syntax

--------------------------------------------------------------------------------
--          mapN etc
--------------------------------------------------------------------------------

public export
map2 : Functor f => Functor g => (a -> b) -> (f . g) a -> (f . g) b
map2 = map . map

public export
map3 :  Functor f => Functor g => Functor h
     => (a -> b) -> (f . g . h) a -> (f . g . h) b
map3 = map . map . map

public export
map4 :  Functor f => Functor g => Functor h => Functor i
     => (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
map4 = map . map . map . map

infixr 4 <$$>, <$$$>, <$$$$>
infixl 3 <**>, <***>, <****>

public export
(<$$>) : Functor f => Functor g => (a -> b) -> (f . g) a -> (f . g) b
(<$$>) = map . map

public export
(<$$$>) :  Functor f => Functor g => Functor h
        => (a -> b) -> (f . g . h) a -> (f . g . h) b
(<$$$>) = map . map . map

public export
(<$$$$>) :  Functor f => Functor g => Functor h => Functor i
         => (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
(<$$$$>) = map . map . map . map

public export
(<**>) :  Applicative f => Applicative g
       => (f . g) (a -> b) -> (f . g) a -> (f . g) b
x <**> y = [| x <*> y |]

public export
(<***>) :  Applicative f => Applicative g => Applicative h
        => (f . g . h) (a -> b) -> (f . g . h) a -> (f . g . h) b
x <***> y = [| x <**> y |]

public export
(<****>) :  Applicative f => Applicative g => Applicative h => Applicative i
         => (f . g . h . i) (a -> b) -> (f . g . h . i) a -> (f . g . h . i) b
x <****> y = [| x <***> y |]

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export
record Comp2 (f,g : Type -> Type) (a : Type) where
  constructor C2
  c2 : f (g a)

public export
Functor f => Functor g => Functor (Comp2 f g) where
  map f (C2 v) = C2 $ map2 f v

public export
Applicative f => Applicative g => Applicative (Comp2 f g) where
  pure = C2 . pure . pure
  C2 vf <*> C2 va = C2 $ [| vf <*> va |]

public export
Foldable f => Foldable g => Foldable (Comp2 f g) where
  foldr fun acc (C2 v) =
    foldr (flip $ foldr fun) acc v
  foldl fun acc (C2 v) =
    foldl (foldl fun) acc v

public export
Traversable f => Traversable g => Traversable (Comp2 f g) where
  traverse fun = map C2 . (traverse . traverse) fun . c2


text:
module EffFTCQueue

import src.FTCQueue
import Data.Morphisms

data Exists : List a -> a -> Type where
    Here : Exists (x :: xs) x
    There : Exists xs x -> Exists (y :: xs) x

data Eff : List (Type -> Type) -> Type -> Type where
  Pure : a -> Eff xs a
  Bind : {e : Exists xs f} -> f a -> FTCQueue (Kleislimorphism (Eff xs)) a b -> Eff xs b

(>>=) : Eff xs a -> (a -> Eff xs b) -> Eff xs b
(>>=) (Pure x) f = f x
(>>=) (Bind {e} x g) f = Bind {e} x (g |> (Kleisli f))

-- Reader effect
data Reader : (e : Type) -> Type -> Type where
  Ask : Reader e e

ask : {auto e : Exists xs (Reader en)} -> Eff xs en
ask {e} = Bind {e} Ask (tsingleton (Kleisli Pure))

qApp : FTCQueue (Kleislimorphism (Eff r)) b w -> b -> Eff r w
qApp q x with (tviewl q)
  qApp q x | (TOne (Kleisli k)) = k x
  qApp q x | ((Kleisli k) :| w) with (k x)
    qApp q x | ((Kleisli k) :| w) | (Pure y) = qApp w y
    qApp q x | ((Kleisli k) :| w) | (Bind {e} y z) = Bind {e} y (z >< w)

qComp : FTCQueue (Kleislimorphism (Eff r)) a b -> (Eff r b -> Eff r' c) -> Kleislimorphism (Eff r') a c
qComp g h = Kleisli (\a => (h . qApp g) a)

runReader : en -> Eff ((Reader en) :: xs) a -> Eff xs a
runReader en (Pure x) = Pure x
runReader en (Bind {e = Here} Ask f) = runReader en (qApp f en)
runReader en (Bind {e = (There e')} fa f) = Bind {e = e'} fa  (tsingleton (qComp f (runReader en)))

run : Eff [] a -> a
run (Pure x) = x
run (Bind {e = Here} _ _) impossible
run (Bind {e = (There _)} _ _) impossible

example : Eff [Reader Int] Int
example = do a <- ask
             Pure (1 + a)

test : Int
test = (run . runReader 1) example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Package.IpkgAst

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

%default total
%access public export

ipkgPackage : String->String
ipkgPackage x = "package " ++x

{-      <|> clause "main" (iName []) (\st v -> st { idris_main = Just v })
      <|> clause "sourcedir" identifier (\st v -> st { sourcedir = v })
      <|> clause "opts" pOptions (\st v -> st { idris_opts = v ++ idris_opts st })
      <|> clause "pkgs" (commaSep (pPkgName <* someSpace)) (\st ps ->
      <|> clause "modules" (commaSep moduleName) (\st v -> st { modules = modules st ++ v })
      <|> clause "libs" (commaSep identifier) (\st v -> st { libdeps = libdeps st ++ v })
      <|> clause "objs" (commaSep identifier) (\st v -> st { objs = objs st ++ v })
      <|> clause "makefile" (iName []) (\st v -> st { makefile = Just (show v) })
      <|> clause "tests" (commaSep (iName [])) (\st v -> st { idris_tests = idris_tests st ++ v })
      <|> clause "version" textUntilEol (\st v -> st { pkgversion = Just v })
      <|> clause "readme" textUntilEol (\st v -> st { pkgreadme = Just v })
      <|> clause "license" textUntilEol (\st v -> st { pkglicense = Just v })
      <|> clause "homepage" textUntilEol (\st v -> st { pkghomepage = Just v })
      <|> clause "sourceloc" textUntilEol (\st v -> st { pkgsourceloc = Just v })
      <|> clause "bugtracker" textUntilEol (\st v -> st { pkgbugtracker = Just v })
      <|> clause "brief" stringLiteral (\st v -> st { pkgbrief = Just v })
      <|> clause "author" textUntilEol (\st v -> st { pkgauthor = Just v })
      <|> clause "maintainer" textUntilEol (\st v -> st { pkgmaintainer = Just v })-}
data Clause =  Imain String
           | Isourcedir String
           | Ipkgs (List String)
           | Iopts String
           | Ideps (List String)
--           | Ipkgs (List String)

IpkgAst : Type
IpkgAst = List Clause

Clause2cmdStr : Clause -> String
Clause2cmdStr x = "main"

partial
pNames : Parser String
pNames = (many $ noneOf "," )>>= pure . pack
partial
pClause : String -> Parser Clause
pClause x@"main" = do
  string x
  pure $ Imain x
pClause x@"pkgs" = do
  string x
  spaces
  string "="
  l<-pNames `sepBy` (string ",")
  pure $ Ipkgs l

pClause x = pure $ Imain ""

max_stars_repo_name: renpillay/ikan

max_issues_repo_name: renpillay/ikan

max_forks_repo_name: renpillay/ikan


text:
module ProofSorted

checkSorted: Ord ty => List ty -> Bool
checkSorted []  = True
checkSorted [x] = True
checkSorted (x :: xs) =
    case xs of
        []       => True
        (y :: _) => if x <= y
            then checkSorted xs
            else False

data IsLte : (smaller: ty) -> (bigger: ty) -> Type where
    Lte: IsLte smaller bigger

proveLessThen: Ord ty => (smaller: ty) -> (bigger: ty) -> Dec (IsLte smaller bigger)
proveLessThen smaller bigger =
    case smaller <= bigger of
        False => No  fails
        True  => Yes holds
    where
        fails: IsLte smaller bigger -> Void
        fails prf = believe_me {b = Void} ()
        holds: IsLte smaller bigger
        holds = really_believe_me (Lte {smaller = smaller} {bigger = bigger})

data Sorted : List ty -> Type where
    SortedNil: Sorted []
    SortedOne: (head: ty) -> Sorted [head]
    SortedMany: {tl: List ty} -> (elem: ty) -> Sorted (hd :: tl) -> (prf: IsLte elem hd) -> Sorted (elem :: hd :: tl)

keepsUnsorted : (tailUnsorted : Sorted (second :: tail) -> Void) -> Sorted (first :: (second :: tail)) -> Void
keepsUnsorted tailUnsorted (SortedMany _ tailSort _) = tailUnsorted tailSort

prependUnsorted : (unsorted : IsLte first second -> Void) -> Sorted (first :: (second :: tail)) -> Void
prependUnsorted unsorted (SortedMany _ _ fsSorted) = unsorted fsSorted

proveSorted: Ord ty => (input: List ty) -> Dec(Sorted input)
proveSorted []    = Yes SortedNil
proveSorted [one] = Yes (SortedOne one)
proveSorted (first :: second :: tail) = case proveLessThen first second of
    (Yes fsSorted)  => case proveSorted (second :: tail) of
        (Yes tailSorted)   => Yes (SortedMany first tailSorted fsSorted)
        (No  tailUnsorted) => No  (keepsUnsorted tailUnsorted)
    (No fsUnsorted) => No (prependUnsorted fsUnsorted)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Main

import Data.HVect

record J r x where
    constructor j
    unJ : (x -> r) -> x

bind : J r x -> (x -> J r y) -> J r y
bind m k = j (\ p : (y -> r) => unJ (k (unJ m (p . flip (unJ . k) p))) p)

return : x -> J r x
return a = j (\_ => a)

ap : (J r (x -> y)) -> J r x -> J r y
ap f a = bind f (\xf => bind a (\xa => return (xf xa)))

fmap : (a -> b) -> J r a -> J r b
fmap f fa = ap (return f) fa

implementation Functor (J r) where
    map = fmap

implementation Applicative (J r) where
    pure  = return
    (<*>) = ap

implementation Monad (J r) where
    (>>=) = bind

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

jify : Type -> (Vect a Type) -> (Vect a Type)
jify r = map (J r)

jsequence : {auto a : Vect x Type} -> HVect (jify r a) -> J r (HVect a)
jsequence {a = []} []         = return []
jsequence {a = t::ts} (xm::xms) = do x  <- xm
                                     xs <- jsequence xms
                                     return (x::xs)

jsequence' : {auto a : Vect x Type} -> HVect (jify r a) -> J r (HVect a)
jsequence' {a = []} []           = j $ \p => []
jsequence' {a = t::ts} (xm::xms) = j $ \p => let z = unJ xm (\y => p (y :: (unJ (jsequence' xms) (\a => p (y :: a))))) in
                                                 z :: unJ (jsequence' xms) (\x => p (z :: x))


text:
module Text.Markup.Edda.Query

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

%access export

interface Queryable a b where
  query : Monoid res => (a -> res) -> b -> res

Queryable a b => Queryable a (List b) where
  query f xs = foldr (<+>) neutral $ map (query f) xs

(Queryable a b, Queryable a c) => Queryable a (b,c) where
  query f (x,y) = (query f x) <+> (query f y)

Queryable (Edda INLINE) (Edda INLINE) where
  -- INLINE -> INLINE
  query f (Emph xs)   = f (Emph xs) <+> (query f xs)
  query f (Bold xs)   = f (Bold xs) <+> (query f xs)
  query f (Strike xs) = f (Strike xs) <+> (query f xs)
  query f (Uline xs)  = f (Uline xs) <+> (query f xs)

  query f (Quote ty xs)  = f (Quote ty xs) <+> (query f xs)
  query f (Parens ty xs) = f (Parens ty xs) <+> (query f xs)

  query f (Hyper l xs)  = f (Hyper l xs) <+> (query f xs)
  query f (FNote l xs)  = f (FNote l xs) <+> (query f xs)
  query f inline  = f inline

Queryable (Edda INLINE) (Edda BLOCK) where
  -- INLINE to BLOCK
  query f (Section d l t as bs) = query f t <+> query f bs
  query f (Figure l c as fig) = query f c <+> query f fig
  query f (DList kvs)         = query f kvs

  query f (OList xs)  = query f xs
  query f (BList xs)  = query f xs

  query f (Literal l c ss)      = neutral <+> query f c
  query f (Listing l c ty ops as s) = neutral <+> query f c

  query f (Para xs)        = query f xs
  query f (Quotation l xs) = query f xs

  query f (Theorem l c xs)     = query f xs <+> query f c
  query f (Corollary l c xs)   = query f xs <+> query f c
  query f (Lemma l c xs)       = query f xs <+> query f c
  query f (Proposition l c xs) = query f xs <+> query f c
  query f (Proof l c xs)       = query f xs <+> query f c
  query f (Definition l c xs)  = query f xs <+> query f c
  query f (Exercise l c xs)    = query f xs <+> query f c
  query f (Note l c xs)        = query f xs <+> query f c
  query f (Remark l c xs)      = query f xs <+> query f c
  query f (Problem l c xs)     = query f xs <+> query f c
  query f (Question l c xs)    = query f xs <+> query f c
  query f (Solution l c xs)    = query f xs <+> query f c
  query f (Example l c xs)     = query f xs <+> query f c
  query f block = neutral

Queryable (Edda BLOCK) (Edda INLINE) where
  -- BLOCK to INLINE

  query f (Emph xs)   = query f xs
  query f (Bold xs)   = query f xs
  query f (Strike xs) = query f xs
  query f (Uline xs)  = query f xs

  query f (Quote ty xs)  = query f xs
  query f (Parens ty xs) = query f xs

  query f (Ref l)      = neutral
  query f (Cite ty l)  = neutral
  query f (Hyper l xs) = neutral <+> query f xs
  query f (FNote l xs) = neutral <+> query f xs
  query f (MiscPunc c) = neutral

  query f inline = neutral

Queryable (Edda BLOCK) (Edda BLOCK) where
  -- BLOCK to BLOCK
  query f (Section d l t as bs) = f (Section d l t as bs) <+> (query f t) <+> query f bs
  query f (Figure l c as fig)   = f (Figure l c as fig) <+> (query f fig) <+> query f c
  query f (DList kvs)           = f (DList kvs) <+> (query f kvs)

  query f (OList xs)  = f (OList xs) <+> (query f xs)
  query f (BList xs)  = f (BList xs) <+> (query f xs)

  query f (Literal l c ss)      = f (Literal l c ss) <+> query f c
  query f (Listing l c ty ops as s) = f (Listing l c ty ops as s) <+> query f c

  query f (Para xs)        = f (Para xs) <+> query f xs
  query f (Quotation l xs) = f (Quotation l xs) <+> (query f xs)

  query f (Theorem l c xs)     = f (Theorem l c xs) <+> (query f xs) <+> query f c
  query f (Corollary l c xs)   = f (Corollary l c xs) <+> (query f xs) <+> query f c
  query f (Lemma l c xs)       = f (Lemma l c xs) <+> (query f xs) <+> query f c
  query f (Proposition l c xs) = f (Proposition l c xs) <+> (query f xs) <+> query f c
  query f (Proof l c xs)       = f (Proof l c xs) <+> (query f xs) <+> query f c
  query f (Definition l c xs)  = f (Definition l c xs) <+> (query f xs) <+> query f c
  query f (Exercise l c xs)    = f (Exercise l c xs) <+> (query f xs) <+> query f c
  query f (Note l c xs)        = f (Note l c xs) <+> (query f xs) <+> query f c
  query f (Remark l c xs)      = f (Remark l c xs) <+> (query f xs) <+> query f c
  query f (Problem l c xs)     = f (Problem l c xs) <+> (query f xs) <+> query f c
  query f (Question l c xs)    = f (Question l c xs) <+> (query f xs) <+> query f c
  query f (Solution l c xs)    = f (Solution l c xs) <+> (query f xs) <+> query f c
  query f (Example l c xs)     = f (Example l c xs) <+> (query f xs) <+> query f c

  query f block = f block

Queryable (Edda BLOCK) (Edda DOC) where
  -- BLOCK to DOC
  query f (Doc t as body) = query f body

Queryable (Edda INLINE) (Edda DOC) where
  -- INLINE to DOC
  query f (Doc t as body) = query f body

  -- DOC tp DOC
Queryable (Edda DOC) (Edda DOC) where
  query f doc = f doc

Queryable (Edda BLOCK) (Edda SNIPPET) where
  -- BLOCK to SNIPPET
  query f (Snippet snippet prf) with (prf)
    query f (Snippet snippet prf) | IsInLine = query f snippet
    query f (Snippet snippet prf) | IsBlock = query f snippet

Queryable (Edda INLINE) (Edda SNIPPET) where
  -- INLINE to SNIPPET
  query f (Snippet snippet prf) with (prf)
    query f (Snippet snippet prf) | IsInLine = query f snippet
    query f (Snippet snippet prf) | IsBlock = query f snippet

Queryable (Edda SNIPPET) (Edda SNIPPET) where
  -- snippet to snippet
  query f snip = f snip

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Data.Universe

%default total

public export
interface DecEq t => Universe t where
  typeOf : t -> Type

  show : (b : t) -> Show (typeOf b)
  eq : (b : t) -> Eq (typeOf b)

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
{- vector append in reverse order -}
module Sec8_2_5_vappd
import Data.Vect

%default total

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

{- reversed order -}
myAppend2_xs_lemma : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
myAppend2_xs_lemma {m} {k} xs = rewrite sym
                       (plusSuccRightSucc m k) in xs

myAppend2 : Vect n elem -> Vect m elem -> Vect (m + n) elem
myAppend2 {m} [] ys = rewrite plusZeroRightNeutral m in ys
myAppend2 (x :: xs) ys = myAppend2_xs_lemma (x :: myAppend2 xs ys)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Main

import System.Concurrency.Channels
import BareMetal.Utils

data Message = Add Int Int

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

sendAdd : Channel -> Int -> Int -> IO Int
sendAdd ch i1 i2 = do
    ok <- unsafeSend ch (Add i1 i2)
    Just sum <- unsafeRecv Int ch | Nothing => pure 0
    pure sum

main : IO ()
main = do
    Just idAdder <- spawn adder | Nothing => uartWrite "spawn failed\n"
    Just ch <- connect idAdder | Nothing => uartWrite "connect failed\n"
    sum <- sendAdd ch 1 1
    uartWrite $ show sum
    uartWrite "\n"

max_stars_repo_name: mokshasoft/bare-metal-idris-apps

max_issues_repo_name: mokshasoft/bare-metal-idris-apps

max_forks_repo_name: mokshasoft/bare-metal-idris-apps


text:
module Control.HigherOrder

infixr 0 ~>
infixr 0 ~~>

||| Type of natural transformations between two functors.
public export
0
(~>) : (Type -> Type) -> (Type -> Type) -> Type
f ~> g = forall a. f a -> g a

||| As above, but with explicit 0-morphisms.
public export
0
(~~>) : (Type -> Type) -> (Type -> Type) -> (Type -> Type)
(f ~~> g) a = f a -> g a

||| Higher-order functor, i.e. a functor
||| in the category of functors and natural transformations.
public export
interface HFunctor h where
  hmap : (Functor f, Functor g)
      =>   f ~>   g
      -> h f ~> h g

infixr 8 :+:

||| Higher-order disjoint union.
||| Effects are composed via this datatype.
public export
data (:+:) : (sig1 : (Type -> Type) -> (Type -> Type))
          -> (sig2 : (Type -> Type) -> (Type -> Type))
          -> (m : Type -> Type)
          -> (a : Type)
          -> Type where
  Inl : sig1 m a -> (:+:) sig1 sig2 m a
  Inr : sig2 m a -> (:+:) sig1 sig2 m a

public export
HFunctor sig1 => HFunctor sig2 => HFunctor (sig1 :+: sig2) where
  hmap t (Inl op) = Inl (hmap t op)
  hmap t (Inr op) = Inr (hmap t op)

||| Higher order projections.
||| Prj forms a category.
public export
interface Prj (0 sup : (Type -> Type) -> (Type -> Type))
              (0 sub : (Type -> Type) -> (Type -> Type)) | sub where
  constructor MkPrj
  prj : sup m a -> sub m a

||| Higher order injections.
||| Inj forms a category.
public export
interface Inj (0 sub : (Type -> Type) -> (Type -> Type))
              (0 sup : (Type -> Type) -> (Type -> Type)) | sub where
  constructor MkInj
  inj : sub m a -> sup m a

export
Prj sub' sub => Inj sub sup => Inj sub' sup where
  inj = inj . prj {sup = sub', sub}

namespace Inj
  ||| Identity injection.
  ||| Example: `a :+: b ↦ a :+: b`
  public export
  [S] Inj sig sig where
     inj = id

  ||| Inject to a Sum from the left.
  ||| Example: `a ↦ a :+: b`
  public export
  [L] Inj sig1 (sig1 :+: sig2) where
    inj = Inl

  ||| Inject to a Sum from the right.
  ||| Example: `b ↦ a :+: b`
  public export
  [R] Inj sig2 (sig1 :+: sig2) where
    inj = Inr

  ||| Composition of injections.
  ||| Example: `b ↦ (a :+: b) :+: c`
  public export
  [Trans] (inner : Inj siga sigb) => (outer : Inj sigb sigc) => Inj siga sigc where
    inj = inj {sub = sigb, sup = sigc}
        . inj {sub = siga, sup = sigb}

  ||| Same as `Trans`, but the two arguments are explicit.
  public export
  T : (inner : Inj siga sigb) -> (outer : Inj sigb sigc) -> Inj siga sigc
  T inner outer = Trans @{inner} @{outer}

||| State-preserving transformation of
||| a computation in one monad into a computation
||| in another monad, whose value is annotated with the final state.
||| Handler is a natural transformation.
public export
0
Handler : (Type -> Type)
       -> (Type -> Type)
       -> (Type -> Type)
       -> Type
Handler s m n = s . m ~> n . s

||| Handler with explicit 0-morphism.
public export
0
HandlerX : (Type -> Type)
        -> (Type -> Type)
        -> (Type -> Type)
        -> (Type -> Type)
HandlerX s m n = s . m ~~> n . s

public export
interface HFunctor sig => Syntax sig where
  ||| Extend the continuation.
  emap : forall m. (m a -> m b) -> (sig m a -> sig m b)
  ||| Generically thread a handler through a higher-order
  ||| signature.
  weave : (m1 : Monad m) => (m2 : Monad n) => (fs : Functor s)
       => s ()
       -> Handler s m n
       -> (sig m a -> sig n (s a))

public export
Syntax sig1 => Syntax sig2 => Syntax (sig1 :+: sig2) where
  emap f (Inl op) = Inl (emap f op)
  emap f (Inr op) = Inr (emap f op)

  weave s hdl (Inl op) = Inl (weave s hdl op)
  weave s hdl (Inr op) = Inr (weave s hdl op)

||| Lift a first-order functor to a second-order one.
public export
data Lift : (sig : (Type -> Type))
         -> ((Type -> Type) -> (Type -> Type)) where
  MkLift : sig (m a) -> Lift sig m a

public export
unlift : Lift sig m a -> sig (m a)
unlift (MkLift x) = x

||| Alias for use as an effect.
public export
LiftE : (sig : Type -> Type) -> (Type -> Type) -> (Type -> Type)
LiftE = Lift

public export
Functor sig => HFunctor (Lift sig) where
  hmap t (MkLift op) = MkLift (map t op)

public export
Functor sig => Syntax (Lift sig) where
  emap f (MkLift op) = MkLift (map f op)

  weave s hdl (MkLift op) = MkLift $
    map (\p => hdl (map (const p) s)) op

infixr 1 ~<~

-- hdl1 : ctxt1 . m ~> n . ctxt1
-- hdl2 : ctxt2 . l ~> m . ctxt2
-- ?    : (ctxt1 . ctxt2) . l ~> n . (ctxt1 . ctxt2)
--
--  (ctxt1 . ctxt2) . l ===
--  ctxt1 . (ctxt2 . l) ==>
--  ctxt1 . (m . ctxt2) ===
--  (ctxt1 . m) . ctxt2 ==>
--  (n . ctxt1) . ctxt2 ===
--  n . (ctxt1 . ctxt2)
||| Fuse two handlers.
public export
(~<~) : (f : Functor n)
     => (g : Functor ctx1)
     => (forall q. HandlerX ctx1 m n q)
     -> (forall t. HandlerX ctx2 l m t)
     -> (forall p. HandlerX (ctx1 . ctx2) l n p)
hdl1 ~<~ hdl2 = hdl1 . map hdl2


text:
module Verified.Monad.Maybe

import Verified.Applicative
import Verified.Monad
import Verified.Applicative.Maybe

instance VerifiedMonad Maybe where
  monadApplicative Nothing Nothing = Refl
  monadApplicative Nothing (Just x) = Refl
  monadApplicative (Just f) Nothing = Refl
  monadApplicative (Just f) (Just x) = Refl
  monadLeftIdentity x f = Refl
  monadRightIdentity (Just x) = Refl
  monadRightIdentity Nothing = Refl
  monadAssociativity Nothing f g = Refl
  monadAssociativity (Just x) f g = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
> 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 xs ys
>     = case xs of
>            [] => ?bar_3
>            (x :: zs) => ?bar_4


text:
module Main

rec : Int -> Int -> Int
rec 0 y = y
rec 1 y = y
rec x y =
   rec (y-1) (x-2)

main : JS_IO ()
main = putStr' $ show $ rec 10 10


text:
module SimpleFFI.Spec

mutual
  public export
  data DartType
    = IntType
    | BoolType
    | StringType
    | DoubleType
    | VoidType
    | NamedType String
    | FunctionType (List DartType) DartType
    | ListType DartType

  public export
  data Field
    = Var String DartType
    | Final String DartType

  public export
  data Parameter
    = P String DartType
    | N String DartType

  public export
  data Function
    = Fun String (List Parameter) DartType

  public export
  data Member
    = FieldMember Field
    | Method Function
    | Static Function
    | Constructor String (List Parameter)
    | Extends String
    | Const String DartType

  public export
  record Class where
    constructor MkClass
    name : String
    members : List Member

public export
data Declaration
  = ClassDecl Class
  | EnumDecl String (List String)

public export
record Lib where
  constructor MkLib
  name : String
  package : String

public export
record LibDef where
  constructor MkLibDef
  lib : Lib
  declarations : List Declaration

public export
record Module where
  constructor MkModule
  name : String
  libs : List LibDef

export
FromString DartType where
  fromString = NamedType

export
string : DartType
string = StringType

export
double : DartType
double = DoubleType

export
int : DartType
int = IntType

export
bool : DartType
bool = BoolType

export
void : DartType
void = VoidType

export
function : List DartType -> DartType -> DartType
function = FunctionType

export
listOf : DartType -> DartType
listOf = ListType

export
var : DartType -> String -> Member
var ty n = FieldMember $ Var n ty

export
final : DartType -> String -> Member
final ty n = FieldMember $ Final n ty

export
positional : DartType -> String -> Parameter
positional ty n = P n ty

export
defConst : DartType -> String -> Member
defConst ty n = Const n ty

export
named : DartType -> String -> Parameter
named ty n = N n ty

export
defConstructor : String -> List Parameter -> Member
defConstructor = Constructor

export
defIO : String -> List Parameter -> DartType -> Member
defIO n ps ret = Method $ Fun n ps ret

export
defStatic : String -> List Parameter -> DartType -> Member
defStatic n ps ret = Static $ Fun n ps ret

export
defClass : String -> List Member -> Declaration
defClass n ms =
  ClassDecl (MkClass n ms)

export
defEnum : String -> List String -> Declaration
defEnum = EnumDecl

export
defLib : Lib -> List Declaration -> LibDef
defLib = MkLibDef

export
defModule : String -> List LibDef -> Module
defModule = MkModule

export
extends : String -> Member
extends = Extends


text:
module Specdris.ShuffleTreeTest

import Specdris.Spec

import Specdris.TestUtil

%access private

Eq SpecTree where
  (==) (Node l0 r0) (Node l1 r1) = (l0 == l1) && (r0 == r1)
  (==) (Leaf (Left (Describe lMsg))) (Leaf (Left (Describe rMsg))) = lMsg == rMsg
  (==) (Leaf (Left (It lMsg))) (Leaf (Left (It rMsg))) = lMsg == rMsg
  (==) (Leaf (Right _)) (Leaf (Right _)) = True
  (==) _ _ = False

Show SpecTree where
  show (Node l r) = "node(" ++ show l ++ " , " ++ show r ++ ")"
  show (Leaf (Left (Describe msg))) = "describe = " ++ msg
  show (Leaf (Left (It msg))) = "it = " ++ msg
  show (Leaf (Right _)) = "test case"

original : SpecTree
original =
  describe "a" $ do
    describe "b" $ do
      it "c1" (1 === 1)
      it "c2" (1 === 1)
    it "d" (2 === 2)

shuffled : SpecTree
shuffled =
  describe "a" $ do
    it "d" (2 === 2)
    describe "b" $ do
      it "c2" (1 === 1)
      it "c1" (1 === 1)

testShuffle : IO ()
testShuffle = testAndPrint "shuffle" (shuffle {rand = \_ => 0.0} original 1) shuffled (==)

export
specSuite : IO ()
specSuite = do putStrLn "\n  shuffle:"
               testShuffle

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Data.ZZ.ModuloVerification

import Control.Algebra
import Classes.Verified

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.AlgebraicVerified	-- For (groupDivisionAddLToSubR)

import Control.Algebra.ZZDivisors

import Data.Fin.FinOrdering
import Data.Fin.Structural

-- For (groupDivisionAddLToSubR)
import Control.Algebra.DiamondInstances

{-
Table of contents

* ZZ algebraic theorems
* Lemmas for (modNatFnIsRemainder)
* (modNatFnIsRemainder)
	Generate proofs of the quotient-remainder relation for binary
	modulo operations on naturals from simpler properties.
* modZGen - generate a verified ZZ modulo from a verified Nat modulo.
-}

{-
ZZ algebraic theorems
-}

total
invertByNegativity : ZZ -> ZZ -> ZZ
invertByNegativity x (Pos y) = x
invertByNegativity x (NegS y) = inverse x

total
timesToAbs :
	(x, y : ZZ)
	-> (x `invertByNegativity` y) <.> y = x <.> Pos (absZ y)
timesToAbs (Pos x') (Pos y') = Refl
timesToAbs (Pos x') (NegS y') =
	trans ( cong {f=((inverse $ Pos x')<.>) . NegS}
		$ sym $ multOneRightNeutral y' )
	$ ringNegationCancelsWithMult (Pos x') (Pos (S y'))
timesToAbs (NegS x') (Pos y') = Refl
timesToAbs (NegS x') (NegS y') = rewrite multOneRightNeutral x' in Refl

{- (modNatFnIsRemainder) parameters -}

parameters (
	modNatFn : Nat -> Nat -> Nat
	, modNatFnIdModZero :
		(x : Nat)
		-> x `modNatFn` Z = x
	, modNatFnCharizLT :
		(x, m : Nat)
		-> (x `LT` m)
		-> x `modNatFn` m = x
	, modNatFnCharizGTE :
		(x, m : Nat)
		-> (m `plus` x) `modNatFn` m = x `modNatFn` m
	){

{-
Lemmas for (modNatFnIsRemainder)

* (modNatFnPreservesZero)
* What to do with induction on constructed quotient-remainder pairs.
-}

total
modNatFnPreservesZero :
	(m : Nat) -> Z `modNatFn` m = Z
modNatFnPreservesZero Z = modNatFnIdModZero Z
modNatFnPreservesZero (S predm) = modNatFnCharizLT Z (S predm) $ LTESucc LTEZero

total
modNatFnCharizModulusPlus2 :
	(x, m, k : Nat)
	-> x = (k `mult` m) `plus` (x `modNatFn` m)
	-> m `plus` x = (S k `mult` m) `plus` (x `modNatFn` m)
modNatFnCharizModulusPlus2 x m k pr
	= trans (cong {f=plus m} pr)
	$ plusAssociative m _ _

-- by (modNatFnCharizModulusPlus2) & (modNatFnCharizGTE)
total
modNatFnCharizModulusPlus :
	(x, m, k : Nat)
	-> x = (k `mult` m) `plus` (x `modNatFn` m)
	-> m `plus` x = (S k `mult` m) `plus` ((m `plus` x) `modNatFn` m)
modNatFnCharizModulusPlus x m k pr
	= trans (modNatFnCharizModulusPlus2 x m k pr)
	$ cong $ sym $ modNatFnCharizGTE x m

total
modNatFnLTToDiffZ :
	(x, m : Nat)
	-> (x `LT` m)
	-> (Z `mult` m) `plus` (x `modNatFn` m) = x
modNatFnLTToDiffZ = modNatFnCharizLT

{-
(modNatFnIsRemainder):
Proof of the quotient-remainder expression for (modNatFn)

Proof of the quotient-remainder expression
for any natural in terms of any modulus
-}

{-
Proof sketch:

Either x < m or x of the form m+x' for some x.
(lteToSumExpr)

If m+x' then (modNatFnCharizModulusPlus):

x = (k `mult` m) `plus` (x `modNatFn` m)
-> m `plus` x = (S k `mult` m) `plus` ((m `plus` x) `modNatFn` m)

so that (modNatFnCharizModulusPlus x' m)
applied to
the divisor-remainder factorization for x'
gives a divisor-remainder factorization for (m `plus` x')
which by transitivity with the proof (x = m `plus` x')
gives the divisor-remainder factorization for x.
wwtbd.

(multDistributesOverPlusRight), implicitly.
(modNatFnLTToDiffZ)

---

Totality:

This proof recurses from an (x) of the form (m+x') into (x') when (m <= x).
However, it only does so in cases where (m > 0).
Thus,
m + x' = x
==>
x' = x - m < x

---

Structure:

Note that the proof itself follows the recursion pattern of one modulo proof.

Thus, given a better modulo algorithm, there should be a corresponding
better proof of the quotient-remainder property.

-}

%reflection
modNatFnIsRemainder :
	(x, m : Nat)
	-> (d : Nat ** (d `mult` m) `plus` (x `modNatFn` m) = x)
modNatFnIsRemainder Z _ = (0 ** modNatFnPreservesZero _)
modNatFnIsRemainder x Z = (0 ** modNatFnIdModZero _)
modNatFnIsRemainder x m
	= either
		(\ltXM => (Z ** modNatFnLTToDiffZ x m ltXM))
		(\gteXM =>
			let gteXM' = lteRelToLTE $ either (Right . sym) Left gteXM
			in let xAsMPlus = lteToSumExpr x m gteXM'
			in let divremx' = modNatFnIsRemainder (getWitness xAsMPlus) m
			in let prevNatTChariz
				= modNatFnCharizModulusPlus
					(getWitness xAsMPlus)
					m
					(getWitness divremx')
					$ sym $ getProof divremx'
			in (S $ getWitness divremx'
				** sym
				$ trans (getProof xAsMPlus)
				$ trans prevNatTChariz
				$ rewrite (sym $ getProof xAsMPlus) in Refl))
	$ trichotomy x m

} {- (modNatFnIsRemainder) parameters -}

{- modZGen parameters -}
parameters (
	modN : Nat -> Nat -> Nat
	, quotientPartN : (x, m : Nat)
		-> (d : Nat ** (d `mult` m) `plus` (x `modN` m) = x)
	) {

total
modZGenFn2 : ZZ -> ZZ -> ZZ
modZGenFn2 x m = Pos (absZ x `modN` absZ m)

total
modZGenFn : ZZ -> ZZ -> ZZ
modZGenFn x@(Pos x') m = x `modZGenFn2` m
modZGenFn x@(NegS x') m = inverse $ inverse x `modZGenFn2` m

{-
Bug: Registers as "possibly not total due to recursive path" in self,
but the pattern-matching recursion graph is

case NegS
 |
 v
case Pos (no call to (modZGenQuot) from Pos)

-}
modZGenQuot : (x : ZZ) -> (m : ZZ)
	-> (x <-> (x `modZGenFn` m)) `quotientOverZZ` m
modZGenQuot x@(Pos x') m =
	let quotientPartN' = quotientPartN x' (absZ m)
	in let witty = Pos (getWitness quotientPartN') `invertByNegativity` m
	in (witty
		** groupDivisionAddLToSubR
			(witty <.> m)
			(x `modZGenFn` m)
			x
		$ trans (cong {f=(<+>(Pos $ x' `modN` absZ m))}
			$ timesToAbs (Pos $ getWitness quotientPartN') m)
		$ cong {f=Pos} $ getProof quotientPartN'
		)
modZGenQuot x@(NegS x') m =
	quotientOverZZtrans
	(inverse Algebra.unity
		**
		trans (ringOpIsDistributiveL (inverse Algebra.unity) (Pos $ S x') _)
		$ bileibniz (<+>)
			(cong $ plusZeroRightNeutral x')
			(trans (ringOpIsCommutative_ZZ _ _)
			$ cong {f=inverse . inverse . Pos . (\t => t `modN` absZ m) . S}
			$ sym $ multOneRightNeutral x'
			)
		)
	$ modZGenQuot (Pos $ S x') m

} {- modZGen parameters -}


text:
module WhoStoleTheTarts

import WhoStoleTheTarts.TheFirstTale

max_stars_repo_name: yurrriq/alice-in-puzzleland

max_issues_repo_name: yurrriq/alice-in-puzzleland

max_forks_repo_name: yurrriq/alice-in-puzzleland


text:
module Proof.DeMorgan

%access  public export
%default total

syntax "($" [x] ")" = \f => f x

infixl 8 .:
(.:) : (c -> d) -> (a -> b -> c) -> (a -> b -> d)
(.:) = (.) . (.)

using (P: Type, Q : Type, R : Type)

  ||| https://proofwiki.org/wiki/Rule_of_Addition/Proof_Rule#Proof_Rule
  add1 : P -> Either P Q
  add1 = Left

  add2 : Q -> Either P Q
  add2 = Right

  ||| https://proofwiki.org/wiki/Double_Negation/Double_Negation_Introduction/Proof_Rule
  doubleNegation : P -> Not (Not P)
  doubleNegation = flip id

  -- doubleNegation' : Not (Not P) -> P
  -- doubleNegation' = believe_me P

  idempotenceAnd : P -> (P, P)
  idempotenceAnd p = (p, p)

  idempotenceAnd' : (P, P) -> P
  idempotenceAnd' = fst

  idempotenceOr : P -> Either P P
  idempotenceOr = Right

  idempotenceOr' : Either P P -> P
  idempotenceOr' = fromEither

  contrapositive : (P -> Q) -> (Not Q -> Not P)
  contrapositive = flip (.)

  notE : P -> Not P -> Void
  notE = flip id

  notE' : Not P -> P -> Void
  notE' = flip notE

  -- notE_and : (P, Q) -> Not P -> Void
  -- notE_and = notE . fst

  ||| https://proofwiki.org/wiki/Modus_Ponendo_Ponens/Proof_Rule
  modusPonendoPonens : (P -> Q) -> P -> Q
  modusPonendoPonens = id

  modusTollendoPonens : (Either P Q) -> Not P -> Q
  modusTollendoPonens = either (void .: notE) const

  excludedMiddle : P -> Either P (Not P)
  excludedMiddle = Left

  excludedMiddle2 : Not (Not P -> Q) -> Not (Either P Q)
  excludedMiddle2 = (. modusTollendoPonens)

  ||| https://proofwiki.org/wiki/Rule_of_Material_Implication/Formulation_1/Forward_Implication
  materialImplication1F : P -> Q -> Either (Not P) Q
  materialImplication1F p q = Right q

  ||| https://proofwiki.org/wiki/Rule_of_Material_Implication/Formulation_1/Reverse_Implication
  materialImplication1R : Either (Not P) Q -> P -> Q
  materialImplication1R = (. doubleNegation) . modusTollendoPonens

  ||| https://proofwiki.org/wiki/Implication_Equivalent_to_Negation_of_Conjunction_with_Negative/Formulation_1/Forward_Implication
  implEquivNegConjWithNeg : (P -> Q) -> Not (P, Not Q)
  implEquivNegConjWithNeg f (p, notQ) = notE (modusPonendoPonens f p) notQ

  ||| https://proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic)/Conjunction_of_Negations/Formulation_1/Forward_Implication
  deMorganConjNeg1F : (Not P, Not Q) -> Not (Either P Q)
  deMorganConjNeg1F (f, g) = notE' (either f g)

  ||| https://proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic)/Conjunction_of_Negations/Formulation_1/Reverse_Implication
  deMorganConjNeg1R : Not (Either P Q) -> (Not P, Not Q)
  deMorganConjNeg1R f = (notE' f . add1, notE' f . add2)
  -- TODO: Arrows?

  ||| https://proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic)/Disjunction_of_Negations/Formulation_1/Forward_Implication
  deMorganDisjNeg1F : Either (Not P) (Not Q) -> Not (P, Q)
  deMorganDisjNeg1F e (p, q) = either ($ p) ($ q) e

  ||| https://proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic)/Disjunction_of_Negations/Formulation_1/Reverse_Implication
  -- deMorganDisjNeg1R : Not (P, Q) -> Either (Not P) (Not Q)
  -- deMorganDisjNeg1R x = ?deMorganDisjNeg1R_rhs

  ||| https://proofwiki.org/wiki/De_Morgan%27s_Laws_(Logic)/Conjunction_of_Negations/Formulation_2
  deMorganConjNeg2F : (Not P, Not Q) -> Not (Either P Q)
  deMorganConjNeg2F (notP, notQ) =
    either (deMorganDisjNeg1F (Left notP) . idempotenceAnd) notQ

  deMorganConjNeg2R : Not (Either P Q) -> (Not P, Not Q)
  deMorganConjNeg2R = deMorganConjNeg1R


text:
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

valueNotSuc : (x : Nat) -> x = S x -> Void
valueNotSuc _ Refl impossible


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/instructions.html#numeric-instructions
module WebAssembly.Structure.Instructions.Definition

import WebAssembly.Structure.Values
import WebAssembly.Structure.Types
import WebAssembly.Structure.Modules.Indices
import WebAssembly.Structure.Instructions.Control
import WebAssembly.Structure.Instructions.Memory

import Decidable.Equality

-- Definition

public export
data Instr : Type where
  Unreachable       : Instr
  Nop               : Instr
  Block             : BlockType -> (List Instr) -> Instr
  Loop              : BlockType -> (List Instr) -> Instr
  If                : BlockType -> (List Instr) -> (List Instr) -> Instr
  Else              : Instr
  End               : Instr
  Br                : LabelIdx -> Instr
  BrIf              : LabelIdx -> Instr
  BrTable           : List LabelIdx -> LabelIdx -> Instr
  Return            : Instr
  Call              : FuncIdx -> Instr
  CallIndirect      : TypeIdx -> Instr
  Drop              : Instr
  Select            : Instr
  LocalGet          : LocalIdx -> Instr
  LocalSet          : LocalIdx -> Instr
  LocalTee          : LocalIdx -> Instr
  GlobalGet         : GlobalIdx -> Instr
  GlobalSet         : GlobalIdx -> Instr
  I32Load           : MemArg -> Instr
  I64Load           : MemArg -> Instr
  F32Load           : MemArg -> Instr
  F64Load           : MemArg -> Instr
  I32Load8S         : MemArg -> Instr
  I32Load8U         : MemArg -> Instr
  I32Load16S        : MemArg -> Instr
  I32Load16U        : MemArg -> Instr
  I64Load8S         : MemArg -> Instr
  I64Load8U         : MemArg -> Instr
  I64Load16S        : MemArg -> Instr
  I64Load16U        : MemArg -> Instr
  I64Load32S        : MemArg -> Instr
  I64Load32U        : MemArg -> Instr
  I32Store          : MemArg -> Instr
  I64Store          : MemArg -> Instr
  F32Store          : MemArg -> Instr
  F64Store          : MemArg -> Instr
  I32Store8         : MemArg -> Instr
  I32Store16        : MemArg -> Instr
  I64Store8         : MemArg -> Instr
  I64Store16        : MemArg -> Instr
  I64Store32        : MemArg -> Instr
  MemorySize        : Instr
  MemoryGrow        : Instr
  I32Const          : I32 -> Instr
  I64Const          : I64 -> Instr
  F32Const          : F32 -> Instr
  F64Const          : F64 -> Instr
  I32Eqz            : Instr
  I32Eq             : Instr
  I32Ne             : Instr
  I32LtS            : Instr
  I32LtU            : Instr
  I32GtS            : Instr
  I32GtU            : Instr
  I32LeS            : Instr
  I32LeU            : Instr
  I32GeS            : Instr
  I32GeU            : Instr
  I64Eqz            : Instr
  I64Eq             : Instr
  I64Ne             : Instr
  I64LtS            : Instr
  I64LtU            : Instr
  I64GtS            : Instr
  I64GtU            : Instr
  I64LeS            : Instr
  I64LeU            : Instr
  I64GeS            : Instr
  I64GeU            : Instr
  F32Eq             : Instr
  F32Ne             : Instr
  F32Lt             : Instr
  F32Gt             : Instr
  F32Le             : Instr
  F32Ge             : Instr
  F64Eq             : Instr
  F64Ne             : Instr
  F64Lt             : Instr
  F64Gt             : Instr
  F64Le             : Instr
  F64Ge             : Instr
  I32Clz            : Instr
  I32Ctz            : Instr
  I32Popcnt         : Instr
  I32Add            : Instr
  I32Sub            : Instr
  I32Mul            : Instr
  I32DivS           : Instr
  I32DivU           : Instr
  I32RemS           : Instr
  I32RemU           : Instr
  I32And            : Instr
  I32Or             : Instr
  I32Xor            : Instr
  I32Shl            : Instr
  I32ShrS           : Instr
  I32ShrU           : Instr
  I32Rotl           : Instr
  I32Rotr           : Instr
  I64Clz            : Instr
  I64Ctz            : Instr
  I64Popcnt         : Instr
  I64Add            : Instr
  I64Sub            : Instr
  I64Mul            : Instr
  I64DivS           : Instr
  I64DivU           : Instr
  I64RemS           : Instr
  I64RemU           : Instr
  I64And            : Instr
  I64Or             : Instr
  I64Xor            : Instr
  I64Shl            : Instr
  I64ShrS           : Instr
  I64ShrU           : Instr
  I64Rotl           : Instr
  I64Rotr           : Instr
  F32Abs            : Instr
  F32Neg            : Instr
  F32Ceil           : Instr
  F32Floor          : Instr
  F32Trunc          : Instr
  F32Nearest        : Instr
  F32Sqrt           : Instr
  F32Add            : Instr
  F32Sub            : Instr
  F32Mul            : Instr
  F32Div            : Instr
  F32Min            : Instr
  F32Max            : Instr
  F32Copysign       : Instr
  F64Abs            : Instr
  F64Neg            : Instr
  F64Ceil           : Instr
  F64Floor          : Instr
  F64Trunc          : Instr
  F64Nearest        : Instr
  F64Sqrt           : Instr
  F64Add            : Instr
  F64Sub            : Instr
  F64Mul            : Instr
  F64Div            : Instr
  F64Min            : Instr
  F64Max            : Instr
  F64Copysign       : Instr
  I32WrapI64        : Instr
  I32TruncF32S      : Instr
  I32TruncF32U      : Instr
  I32TruncF64S      : Instr
  I32TruncF64U      : Instr
  I64ExtendI32S     : Instr
  I64ExtendI32U     : Instr
  I64TruncF32S      : Instr
  I64TruncF32U      : Instr
  I64TruncF64S      : Instr
  I64TruncF64U      : Instr
  F32ConvertI32S    : Instr
  F32ConvertI32U    : Instr
  F32ConvertI64S    : Instr
  F32ConvertI64U    : Instr
  F32DemoteF64      : Instr
  F64ConvertI32S    : Instr
  F64ConvertI32U    : Instr
  F64ConvertI64S    : Instr
  F64ConvertI64U    : Instr
  F64PromoteF32     : Instr
  I32ReinterpretF32 : Instr
  I64ReinterpretF64 : Instr
  F32ReinterpretI32 : Instr
  F64ReinterpretI64 : Instr
  I32Extend8S       : Instr
  I32Extend16S      : Instr
  I64Extend8S       : Instr
  I64Extend16S      : Instr
  I64Extend32S      : Instr
  I32TruncSatF32S   : Instr
  I32TruncSatF32U   : Instr
  I32TruncSatF64S   : Instr
  I32TruncSatF64U   : Instr
  I64TruncSatF32S   : Instr
  I64TruncSatF32U   : Instr
  I64TruncSatF64S   : Instr
  I64TruncSatF64U   : Instr

public export
Expr : Type
Expr = List Instr

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Main

import System

-- Copied from: https://github.com/edwinb/Blodwen/blob/master/tests/Main.idr

%default covering

tests : List String
tests =
  ["test001", "test002"]

chdir : String -> IO Bool
chdir dir = do
  ok <- foreign FFI_C "chdir" (String -> IO Int) dir
  pure (ok == 0)

fail : String -> IO ()
fail err = do
  putStrLn err
  exitWith (ExitFailure 1)

runTest : String -> String -> String -> IO Bool
runTest dir prog test = do
  chdir (dir ++ "/" ++ test)
  putStr $ dir ++ "/" ++ test ++ ": "
  system $ "sh ./run " ++ prog ++ " > output"
  Right out <- readFile "output"
    | Left err => do
      print err
      pure False
  Right exp <- readFile "expected"
    | Left err => do
      print err
      pure False
  if (out == exp)
    then putStrLn "success"
    else putStrLn "FAILURE"
  chdir "../.."
  pure (out == exp)

main : IO ()
main = do
  [_, deps] <- getArgs
    | _ => do putStrLn "Usage: runtests [depsPath]"
  results <- traverse (runTest "deps" deps) tests
  if any not results
    then exitWith (ExitFailure 1)
    else exitWith ExitSuccess

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
-- ------------------------------------------------------ [ GettingStarted.idr ]
-- Module      : Exercises.GettingStarted
-- Description : Solutions to the Chapter 2 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.GettingStarted

%access export

-- ----------------------------------------------------------- [ 2.5 Exercises ]

exercise1_1 : (String, String, String)
exercise1_1 = ("A", "B", "C")

exercise1_2 : List String
exercise1_2 = ["A", "B", "C"]

exercise1_3 : ((Char, String), Char)
exercise1_3 = (('A', "B"), 'C')

namespace Simple

  ||| Determine whether a string reads the same backwards as forwards.
  ||| @ str a string to analyze
  palindrome : (str : String) -> Bool
  palindrome str = str == reverse str

namespace CaseInsensitive

  ||| Determine, case insensitively, whether a string reads the same backwards
  ||| as forwards.
  ||| @ str a string to analyze
  palindrome : (str : String) -> Bool
  palindrome = Simple.palindrome . toLower

namespace LongerThanN

  ||| Return `True` iff `str` is longer than `len` characters and
  ||| case-insensitively reads the same backwards as forwards.
  ||| @ len the lower bound (exclusive) of string length
  ||| @ str a string to analyze
  palindrome : (len : Nat) -> (str : String) -> Bool
  palindrome n str = length str > n && CaseInsensitive.palindrome str

namespace LongerThan10

  ||| Return `True` iff `str` is longer than 10 characts and case-insensitively
  ||| reads the same backwards as forwards.
  ||| @ str a string to analyze
  palindrome : (str : String) -> Bool
  palindrome = LongerThanN.palindrome 10

||| Compute the number of words and number of characters in a string.
||| @ str a string to analyze
counts : (str : String) -> (Nat, Nat)
counts str =
  let wordCount = length (words str)
      charCount = length str
  in  (wordCount, charCount)

||| Return the largest ten values in a list.
||| @ list a list of values contstrained by `Ord`
topTen : Ord a => (list : List a) -> List a
topTen = take 10 . sortBy (flip compare)

-- NOTE: This is a bit like Clojure's cond->.
syntax "cond$" [x] [b] [f] = if b then x else f x

||| Count the number of strings in list that are over a given length.
||| @ len the lower bound (exclusive) of string length
overLength : (len : Nat) -> List String -> Nat
overLength len = foldr go 0
  where
    go : String -> Nat -> Nat
    go str n = cond$ n (length str > len) S

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris