text:
module Streaming.Network.Curl

import Streaming

import Data.LazyList as L

import Data.IORef

import Data.Buffer

import Control.Monad.Trans
import Control.Monad.Managed
import Network.Curl.Easy

import Streaming.API as S
import Streaming.Encoding.UTF8

-- This is just an experiment right now, don't take it as the right way to go

-- ioref seems good still
streamCallback : IORef (LazyList String) -> (Buffer -> Int -> Int -> AnyPtr -> PrimIO Int)
streamCallback ref str s len _ = toPrim $ do
  got <- rawSize str
  gr <- map (cast {to=Bits8}) <$> bufferData str
  xs :> Right _ <- S.toList $ decodeUtf8 (each'' gr)
    | _ => pure 0
  modifyIORef ref (pack xs ::)
  pure got

mGlobalInit : Managed CurlECode
mGlobalInit = managed $ \f => do
  ctx <- curlGlobalInit
  r <- f ctx
  curlGlobalCleanup
  pure r

mEasyInit : Managed (Maybe (CurlHandle Easy))
mEasyInit = managed $ \f => do
  h <- curlEasyInit
  case h of
    Nothing => f h
    Just h' => do r <- f h
                  curlEasyCleanup h'
                  pure r

-- I need to set my callback and then call perform
export
curl : String -> Stream (Of Bits8) Managed (Either String ())
curl url = effect $ do
    CURLE_OK <- mGlobalInit
      | r => pure (pure (Left $ "global init not ok: " ++ show r))
    Just h <- mEasyInit
      | Nothing => pure (pure (Left $ "easy init not ok"))
    CURLE_OK <- curlEasySetopt h CURLOPT_URL url
      | r => pure (pure (Left $ "setopt not ok: " ++ show r))
    CURLE_OK <- curlEasySetopt h CURLOPT_URL url
      | r => pure (pure (Left $ "setopt not ok: " ++ show r))
    -- easy_to_bytes h
    ref <- newIORef {a=LazyList String} []
    CURLE_OK <- curlEasySetopt h CURLOPT_WRITEFUNCTION (streamCallback ref)
      | r => pure (pure (Left $ "setopt not ok: " ++ show r))
    CURLE_OK <- curlEasyPerform h
      | r => pure (pure (Left $ "perform not ok: " ++ show r))
    dat <- readIORef ref
    pure $ the (Stream (Of Bits8) Managed (Either String ()))
         $ each dat
        &$ mapf (\(x :> r) => each {m=Managed} (unpack x) *> pure r)
        |> concats
        |> maps (cast . cast {to=Int})
        |> (*> pure (Right ()))


text:
import Js.Node.Module
import Js.Electron.App
import Js.Electron.Window

%lib Node "electron"

%default total

win : String -> Options
win dir = record {title = Just "Hello Electron", url = Just ("file://" ++ dir ++ "/view.html"), width = Just 800, height = Just 600} defaults

main : JS_IO ()
main = onReady $ do centre !(create $ win !dir)

ext: idr

max_stars_repo_name: jheiling/idris-electron-react-scaffold

max_issues_repo_name: jheiling/idris-electron-react-scaffold

max_forks_repo_name: jheiling/idris-electron-react-scaffold


text:
module Main

import Data.Maybe
import Data.List
import Data.List1
import Data.Strings

import System
import System.Directory
import System.File
import System.Info
import System.Path

%default covering

------------------------------------------------------------------------
-- Test cases

dartTests : List String
dartTests
  = [ "dart001", "dart002", "dart003"
    , "dart015", "dart021", "dart022"
    , "ffi001", "ffi002", "ffi003", "ffi004"
    , "idiom001", "lazy001", "tailrec001"
    , "reg001"
    , "perf006"
    ]

------------------------------------------------------------------------
-- Options

||| Options for the test driver.
record Options where
  constructor MkOptions
  ||| Name of the idris2 executable
  idris2      : String
  ||| Should we only run some specific cases?
  onlyNames   : List String
  ||| Should we run the test suite interactively?
  interactive : Bool

usage : String
usage = "Usage: runtests <idris2 path> [--interactive] [--only [NAMES]]"

options : List String -> Maybe Options
options args = case args of
    (_ :: idris2 :: rest) => go rest (MkOptions idris2 [] False)
    _ => Nothing

  where

    go : List String -> Options -> Maybe Options
    go rest opts = case rest of
      []                      => pure opts
      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
      _ => Nothing

------------------------------------------------------------------------
-- Actual test runner

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

-- on Windows, we just ignore backslashes and slashes when comparing,
-- similarity up to that is good enough. Leave errors that depend
-- on the confusion of slashes and backslashes to unix machines.
normalize : String -> String
normalize str =
    if isWindows
      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
      else str

runTest : Options -> String -> IO Bool
runTest opts testPath
    = do changeDir testPath
         isSuccess <- runTest'
         changeDir "../.."
         pure isSuccess
    where
        getAnswer : IO Bool
        getAnswer = do
          str <- getLine
          case str of
            "y" => pure True
            "n" => pure False
            _   => do putStrLn "Invalid Answer."
                      getAnswer

        printExpectedVsOutput : String -> String -> IO ()
        printExpectedVsOutput exp out = do
          putStrLn "Expected:"
          printLn exp
          putStrLn "Given:"
          printLn out

        mayOverwrite : Maybe String -> String -> IO ()
        mayOverwrite mexp out = do
          the (IO ()) $ case mexp of
            Nothing => putStr $ unlines
              [ "Golden value missing. I computed the following result:"
              , out
              , "Accept new golden value? [yn]"
              ]
            Just exp => do
              putStrLn "Golden value differs from actual value."
              code <- system "git diff --no-index --exit-code --word-diff=color expected output"
              when (code < 0) $ printExpectedVsOutput exp out
              putStrLn "Accept actual value as new golden value? [yn]"
          b <- getAnswer
          when b $ do Right _ <- writeFile "expected" out
                          | Left err => print err
                      pure ()
        runTest' : IO Bool
        runTest'
            = do putStr $ testPath ++ ": "
                 system $ "sh ./run " ++ idris2 opts ++ " | tr -d '\\r' > output"
                 Right out <- readFile "output"
                     | Left err => do print err
                                      pure False
                 Right exp <- readFile "expected"
                     | Left FileNotFound => do
                         if interactive opts
                           then mayOverwrite Nothing out
                           else print FileNotFound
                         pure False
                     | Left err => do print err
                                      pure False
                 let result = normalize out == normalize exp
                 if result
                    then putStrLn "success"
                    else do
                      putStrLn "FAILURE"
                      if interactive opts
                         then mayOverwrite (Just exp) out
                         else printExpectedVsOutput exp out

                 pure result

exists : String -> IO Bool
exists f
    = do Right ok <- openFile f Read
             | Left err => pure False
         closeFile ok
         pure True

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

pathLookup : List String -> IO (Maybe String)
pathLookup names = do
  path <- getEnv "PATH"
  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
  let candidates = [p ++ "/" ++ x | p <- pathList,
                                    x <- names]
  firstExists candidates

findDart : IO (Maybe String)
findDart
    = do Just dart <- getEnv "DART" | Nothing => pathLookup ["dart"]
         pure $ Just dart

runDartTests : Options -> List String -> IO (List Bool)
runDartTests opts tests
    = do dartexec <- findDart
         maybe (do putStrLn "dart not found"
                   pure [])
               (\c => do putStrLn $ "Found dart at " ++ c
                         traverse (runTest opts) tests)
               dartexec

filterTests : Options -> List String -> List String
filterTests opts = case onlyNames opts of
  [] => id
  xs => filter (\ name => any (`isInfixOf` name) xs)

main : IO ()
main
    = do args <- getArgs
         let (Just opts) = options args
              | _ => do print args
                        putStrLn usage
         let filteredDartTests = filterTests opts (testPaths "dart" dartTests)
         dartTestRes <- if length filteredDartTests > 0
              then runDartTests opts filteredDartTests
              else pure []
         let res = dartTestRes
         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
                       ++ " tests successful")
         if (any not res)
            then exitWith (ExitFailure 1)
            else exitWith ExitSuccess
    where
         testPaths : String -> List String -> List String
         testPaths dir tests = map (\test => dir ++ "/" ++ test) tests


text:
module TypedNBE

-- Typed NBE, based on https://hal.inria.fr/hal-01397929/document

import Data.Vect

data Ty = Base String | Arrow Ty Ty

data Syn : Vect n Ty -> Ty -> Type where
  Var : Elem a ctx -> Syn ctx a
  Lam : Syn (a :: ctx) b -> Syn ctx (Arrow a b)
  App : Syn ctx (Arrow a b) -> Syn ctx a -> Syn ctx b

V : Ty -> Type

mutual
  data Nf : Ty -> Type where
    NLam : (V a -> Nf b) -> Nf (Arrow a b)
    NAt : At (Base a) -> Nf (Base a)

  data At : Ty -> Type where
    AApp : At (Arrow a b) -> Nf a -> At b
    AVar : V a -> At a

data Sem : Ty -> Type where
  Fun : (Sem a -> Sem b) -> Sem (Arrow a b)
  Base' : At (Base a) -> Sem (Base a)

data Env : Vect n Ty -> Type where
  Nil  : Env Nil
  (::) : Sem ty -> Env ctx -> Env (ty :: ctx)

lookup' : Elem ty ctx -> Env ctx -> Sem ty
lookup' Here (x :: _) = x
lookup' (There later) (x :: xs) = lookup' later xs

eval : Env ctx -> Syn ctx ty -> Sem ty
eval env (Var x) = lookup' x env
eval env (Lam body) = Fun (\x => eval (x :: env) body)
eval env (App f x) with (eval env f)
  eval env (App f x) | (Fun f') = f' (eval env x)

mutual
  reflect : At ty -> Sem ty
  reflect {ty = (Base _)} at = Base' at
  reflect {ty = (Arrow a b)} at = Fun (\x => reflect (AApp at (reify x)))

  reify : Sem ty -> Nf ty
  reify {ty = (Base _)} (Base' base) = NAt base
  reify {ty = (Arrow a b)} (Fun f) = NLam (\x => reify (f (reflect (AVar x))))

nbe : Syn [] ty -> Nf ty
nbe syn = reify (eval [] syn)

example : Syn [] (Arrow (Base "a") (Base "a"))
example = Lam (App (Lam (Var Here)) (Var Here))

test : Nf (Arrow (Base "a") (Base "a"))
test = nbe example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module StreamAntiDiag

import Data.List
import Data.Nat
import Data.Stream
import Data.Stream.Extra

antidiag2 : Stream a -> Stream b -> Stream (a, b)
antidiag2 xs ys = map (bimap (flip index xs) (flip index ys)) $ flattenStreamOfLists $ allSums <$> iterate S Z
  where
    allSums : Nat -> List (Nat, Nat)
    allSums n = iterateN n (\(a, b) => (S a, pred b)) (0, n)

    flattenStreamOfLists : forall a. Stream (List a) -> Stream a
    flattenStreamOfLists (xs::xxs) = startWith xs $ flattenStreamOfLists xxs

antidiag2With : (a -> b -> c) -> Stream a -> Stream b -> Stream c
antidiag2With f = map (uncurry f) .: antidiag2

-- Applicative's `(<*>) = antidiag2With apply` wouldn't satisfy `pure id <*> v = v` when `pure = repeat`.

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Conway.Graphics

import Data.Vect
import Graphics.SDL
import Conway.Conway

-- | Performs a sequence of IO actions
sequenceIO : List (IO ()) -> IO ()
sequenceIO Nil = pure ()
sequenceIO (x::xs) =
  do x
     sequenceIO xs

-- | Converts fin to int
finToInt : Fin m -> Int
finToInt = toIntNat . finToNat

-- | Display the current conway state on the given SDL surface
displayConway : Int -> Int -> Conway m n -> SDLSurface -> IO ()
displayConway {m} {n} screenX screenY (MkConway v) s =
  do
     sequenceIO $ toList $ map displayRow (sequenceFin m)
     flipBuffers s

    where
        iterY : Int
        iterY = screenY `div` (toIntNat m)

        iterX : Int
        iterX = screenX `div` (toIntNat n)

        drawCell : Int -> Int -> (Int, Int, Int) -> IO ()
        drawCell py px (r,g,b) = filledRect s (iterX * px) (iterY * py) iterX iterY r g b 128

        displayRow : Fin m -> IO ()
        displayRow y = sequenceIO $ toList $ map displayPoint (sequenceFin n)

        where displayPoint : Fin n -> IO ()
              displayPoint x with (index x (index y v))
                    | Alive = drawCell (finToInt y) (finToInt x) (0x00, 0x00, 0x00)
                    | Dead  = drawCell (finToInt y) (finToInt x) (0xFF, 0xFF, 0xFF)

-- | Given an initial Conway State, constantly updates
--   and displays the Conway State
export
conwayLoop : Conway m n -> IO ()
conwayLoop cw {m} {n} =
  do
    surface <- startSDL screenX screenY
    case surface of
      Just surface' => conwayLoop' cw surface'
      Nothing => print "Unable to get SDL surface\n"

  where
        screenX : Int
        screenX = cast $ n * 16

        screenY : Int
        screenY = cast $ m * 16

        conwayLoop' : Conway m n -> SDLSurface -> IO ()
        processEvent : Conway m n -> SDLSurface -> Maybe Event -> IO (Maybe (Conway m n))

        conwayLoop' cw surface = do
            displayConway screenX screenY cw surface
            flipBuffers surface
            event <- pollEvent
            eventPResult <- processEvent cw surface event

            case eventPResult of
              Just nextCw => conwayLoop' nextCw surface
              Nothing     => pure ()

        processEvent cw surface (Just (KeyDown KeyEnter))
                = do
                    let nextCw = iterateGame cw
                    displayConway screenX screenY nextCw surface
                    flipBuffers surface
                    pure $ Just nextCw

        processEvent _ _ (Just AppQuit)
                = pure Nothing

        processEvent cw _ _
                = pure $ Just cw

max_stars_repo_name: RossMeikleham/Idris-Conway

max_issues_repo_name: RossMeikleham/Idris-Conway

max_forks_repo_name: RossMeikleham/Idris-Conway


text:
module Koans.Tuples

-- Complete the following functions

firstPair : Bool
firstPair = ?fillme1 == fst ("First", "Pair")

secondPair : Bool
secondPair = ?fillme2 == snd ("Second", "Pair")

whatAmI : Vect 5 (Int, Bool)
whatAmI = ?fillme3

ws : Vect 5 String
ws = ["zip", "a", "dee", "doo", "dah"]

is : Vect 5 Int
is = ?fillme4

myFirstZip : Bool
myFirstZip = zip ws is == ?fillme5

whatIsMyResult : Bool
whatIsMyResult = ?fillme6 == Vect.zipWith (+) is is

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
f : Nat -> Nat
f n = case n of case_val => ?f_rhs

g : Nat -> Nat
g n = (case n of case_val => ?g_rhs)

h : Nat -> Nat
h n = (case n of
            case_val => ?h_rhs     )

data Test = One
          | Two Nat
          | Three String Nat
          | Four

toTest : Nat -> Test

i : Nat -> Nat
i n = case toTest n of case_val => ?i_rhs

j : Nat -> Nat
j n = j_Where n where
  j_Where : Nat -> Nat
  j_Where k = (case toTest k of case_val => ?j_Where_rhs    )

k : Nat -> Nat
k n = (case toTest n of
            case_val => ?k_rhs)

l : Nat -> Nat -> Unit
l n m = case n of foo => case toTest m of case_val => ?l_rhs

m : Nat -> Nat -> Unit
m n k = (case n of foo => case toTest k of case_val => ?m_rhs  )

n : Nat -> Nat -> Unit
n k m = case k of foo => case toTest m of
                              case_val => ?n_rhs

o : Nat -> Nat -> Unit
o n m = (case n of foo => case toTest m of
                               case_val => ?o_rhs   )


text:
{-
Copyright 2018, 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.
-}

{-
  ported from kernel/libsel4/arch_include/<arch>/sel4/arch/functions.h
-}

module seL4.Arch.Functions

%access public export
%default total

-- seL4_Word seL4_GetMR(int i)
-- void seL4_SetMR(int i, seL4_Word mr)
-- seL4_Word seL4_GetUserData(void)
-- void seL4_SetUserData(seL4_Word data)
-- seL4_CapData_t seL4_GetBadge(int i)
-- seL4_CPtr seL4_GetCap(int i)
-- void seL4_SetCap(int i, seL4_CPtr cptr)
-- void seL4_GetCapReceivePath(seL4_CPtr* receiveCNode, seL4_CPtr* receiveIndex, seL4_Word* receiveDepth)
-- void seL4_SetCapReceivePath(seL4_CPtr receiveCNode, seL4_CPtr receiveIndex, seL4_Word receiveDepth)
-- seL4_IPCBuffer* seL4_GetIPCBuffer(void)


text:
{-------------------------}
-- These should be
-- ignored
{- {---------------} -}

-- Comments should have the right to be empty:
--

-- This is a valid comment {-
-- It should not lead to a parse error if nested in a
-- multiline comment

{- Hence this test

-- This is a valid comment {-
-- It should not lead to a parse error if nested in a
-- multiline comment

-}

myString : String
myString = "Similarly, this is a valid string literal {- "
-- So we should be able to put it in a multiline comment

{- Hence this test

myString : String
myString = "Similarly, this is a valid string literal {- "
-- So we should be able to put it in a multiline comment

-}

{------------- Some people {---- like ---}
  {- comments with
     weird
 ----------}
 closing delimiters
 --}


text:
module Test

export
data Main : Type


text:
module Numeric.Floating

public export
interface Fractional ty => Floating ty where
  constructor MkFloating
  pi : ty
  euler : ty
  exp : ty -> ty
  log : ty -> ty
  pow : ty -> ty -> ty -- (**)
  sin : ty -> ty
  cos : ty -> ty
  tan : ty -> ty
  asin : ty -> ty
  acos : ty -> ty
  atan : ty -> ty
  sinh : ty -> ty
  cosh : ty -> ty
  tanh : ty -> ty
  sqrt : ty -> ty

export
Floating Double where
  pi = Prelude.Types.pi
  euler = Prelude.Types.euler
  exp = Prelude.Types.exp
  log = Prelude.Types.log
  pow = Prelude.Types.pow
  sin = Prelude.Types.sin
  cos = Prelude.Types.cos
  tan = Prelude.Types.tan
  asin = Prelude.Types.asin
  acos = Prelude.Types.acos
  atan = Prelude.Types.atan
  sinh = Prelude.Types.sinh
  cosh = Prelude.Types.cosh
  tanh = Prelude.Types.tanh
  sqrt = Prelude.Types.sqrt

-- export
-- Floating Double where
--   pi = 3.14159265358979323846
--   euler = 2.7182818284590452354
--   exp x = prim__doubleExp x
--   log x = prim__doubleLog x
--   pow x y = exp (y * log x) -- prim__doublePow x y
--   sin x = prim__doubleSin x
--   cos x = prim__doubleCos x
--   tan x = prim__doubleTan x
--   asin x = prim__doubleASin x
--   acos x = prim__doubleACos x
--   atan x = prim__doubleATan x
--   sinh x = (exp x - exp (-x)) / 2
--   cosh x = (exp x + exp (-x)) / 2
--   tanh x = sinh x / cosh x -- can this NaN via cosh = 0? can cosh even be 0?
--   sqrt x = prim__doubleSqrt x
--   floor x = prim__doubleFloor x
--   ceiling x = prim__doubleCeiling x

max_stars_repo_name: MarcelineVQ/sarray


text:
module ReflNotRefl2

import Data.Fin

import ReflNotRefl1

prop : ind 3 (B 4 `W` (3, True)) = True
prop = Refl


text:
module TypeTrans.AST

import Data.Vect

-- Define Type Aliases
Rule : Type
Rule = String

Name : Type
Name = String

Value : Type
Value = String

Assoc : Type
Assoc = Bool

Performance : Type
Performance = Float

Cost : Type
Cost = Float

data Variant = Par | Seq | Stream | Tree

implementation Show Variant where
  show Par = "Par"
  show Seq = "Seq"
  show Stream = "Stream"
  show Tree = "Tree"

data TypeT =
    Vec Nat TypeT |
    Tuple (List TypeT) |
    IntT |
    ByteT |
    BitT |
    LongT |
    FloatT |
    DoubleT |
    BoolT |
    T1 |
    T2 |
    T3

implementation Show TypeT where
  show (Vec i t) = "Vec " ++ show i ++ " (" ++ show t ++ ")"
  show (Tuple xs) = "Tuple " ++ show xs
  show IntT = "Int"
  show ByteT = "Byte"
  show BitT = "Bit"
  show LongT = "Long"
  show FloatT = "Float"
  show DoubleT = "Double"
  show BoolT = "Bool"
  show T1 = "T1"
  show T2 = "T2"
  show T3 = "T3"

-- Vector with description of its dimensions in the type
--NVec : Vect n Nat -> TypeT -> TypeT
--NVec Nil t = t
--NVec (v::vs) t = Vec v (NVec vs t)

-- Calculate the dimension of the given type
getDimension : TypeT -> Nat
getDimension (Vec i t) = (S Z) + getDimension t
getDimension _ = Z -- Non vector types have dimension 0

mutual
-- Argument is not a very good name. I mean something of type a as opposed to a -> b for the actions
  data Argument =
       Arg Name TypeT |
       Val Value TypeT |
       Res Action Argument |
       Let (List (Argument,Argument)) Argument --  let like this is not an action, it's only an action if I do  \x -> let ... x ... in ... i.e. Lambda x (let ...)

  implementation Show Argument where
    show (Arg n t) = "Arg " ++ n ++ " " ++ show t
    show (Val v t) = "Val " ++ v ++ " " ++ show t
    show (Res act arg) = "Res " ++ show act ++ " " ++ show arg
    show (Let xs arg) = "Let " ++ show xs ++ " " ++ show arg

  data Action =
      Opaque Name (List Argument) Argument TypeT (Performance,Cost) | -- [Type] is for constant args to map or fold, the first Type is the input arg, the last Type the return type
      OpaqueBin Assoc Name (List Argument) Argument Argument (Performance,Cost) |
      Map Variant Action |
      Fold Variant Action Argument | -- Argument here is the accumulator, and action must be a binary operation, not unary
      Compose (List Action) |
      -- Lambda (List Argument) (Action) ?
      Lambda (List Argument) Argument | -- (\(x,y) -> map (g x) y) becomes Lambda [x,y] (Map g x) y so the last Argument is usually a Res
      Loop Action Action |
      Split Int |
      Merge Int |
      Distr Int Int |
      Group (List (Argument, List Rule)) |
      Ungroup (List (Argument, List Rule)) |
      Zip (List TypeT) | -- this should really only work on a set of vectors and return a Vec (Tuple [Type]) Int
      Unzip TypeT  -- This should really only work on a Tuple [Vec Type Int]

  implementation Show Action where
    show (Opaque n xs arg t pc) = "Opaque " ++ n ++ " " ++ show xs ++ " " ++
                                  show arg ++ " "++ show t ++ " " ++ show pc
    show (OpaqueBin a n xs arg1 arg2 pc) = "Opaque " ++ show a ++ " " ++ n ++ " " ++
                                         show arg1 ++ " " ++ show arg2 ++ " " ++ show pc
    show (Map v act) = "Map " ++ show v ++ " " ++ show act
    show (Fold v act arg) = "Fold " ++ show v ++ " " ++ show act ++ " " ++ show arg
    show (Compose xs) = "Compose " ++ show xs
    show (Lambda xs act) = "Lambda " ++ show xs ++ " " ++ show act
    show (Loop act1 act2) = "Loop " ++  show act1 ++ " " ++ show act2
    show (Split i) = "Split " ++ show i
    show (Merge i) = "Merge " ++ show i
    show (Distr i1 i2) = "Distr " ++ show i1 ++ " " ++ show i2
    show (Group xs) = "Group " ++ show xs
    show (Ungroup xs) = "Ungroup " ++ show xs
    show (Zip xs) = "Zip " ++ show xs
    show (Unzip t) = "Unzip " ++ show t

-- We also need Zip, Unzip and Let
--data FoldAction =  deriving Show-- No need for return type as it's b -> a  -> b

data Program = Prog Action Argument  -- So actually Prog is identical to Res

implementation Show Program where
  show (Prog act arg) = "Prog " ++ show act ++ " " ++ show arg

-- I also need to represent a while-loop
-- We assume we have a loop primitive in the language
-- let loop cond action v  = (let res = action v in if (cond res) then res else loop cond action res)
-- This becomes Loop (Opaque "cond" [] (Arg "res" T2) BoolT) (Opaque "action" [] (Arg "v" T1))
-- and a way to extract values from a tuple, maybe a let?
{-

let
    (err, p', p_avg) = fold (0, [], 0) sor p
in
    map (stage3 p_avg) p'
    rather than simply (map stage3) $ (fold acc stage2) $ (map stage1) p
 this would be
 (\(v_in,stage1,stage2) -> let  (err, p', p_avg) = fold (0, [], 0) stage1 v_in in map (stage2 p_avg) p') $ map stage1 p
 The best way is to add a Lambda action

(\(x,y) -> map (g x) y) . (foldl f acc ) $ v -- [4,5,6]
-}

-- (Tuple [IntT,Vec IntT 3])
{-
p : Program
p = Prog  (Compose [
            Lambda [Arg "x" IntT, Arg "y" (Vec 3 IntT)]
                   (Map Seq (Opaque "g" [Arg "x" IntT] (Arg "a1" IntT) IntT (0,0)))
                   ]
          ) {- (Arg "y" (Vec IntT 3)),
        Fold Seq (OpaqueBin True "f" [] (Arg "acc" (Tuple [IntT,Vec IntT 3])) (Arg "a2" IntT) (0,0)) (Arg "acc" (Tuple [IntT,Vec IntT 3]))
        ])  -}
    (Arg "v" (Vec 3 IntT))

-}

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module ex_3_2_4

import Data.Vect

-- interactive editing mode
-- ctrl+alt+a
-- ctrl+alt+c
-- ctrl+alt+l
-- ctrl+alt+s

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

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

length' : List a -> Nat
length' [] = 0
length' (x :: xs) = S $ length' xs

-- *ex_3_2_4> length' []
-- (input):Can't infer argument a to length', Can't infer argument a to []
-- Can't infer argument
-- need explicit type, using `the`
-- *ex_3_2_4> length' $ the (List Int) []
-- 0 : Nat

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

-- *ex_3_2_4> reverse' [1,2,3]
-- [3, 2, 1] : List Integer


text:
module Data.Bitraversable

import Control.Monad.Identity
import Data.Functor.Const
import Data.Morphisms

public export
bimapDefault : Bitraversable p => (a -> c) -> (b -> d) -> p a b -> p c d
bimapDefault f g = runIdentity . bitraverse (Id . f) (Id . g)

public export
bifoldrDefault : Bitraversable p =>
                 (a -> acc -> acc) -> (b -> acc -> acc) -> acc -> p a b -> acc
bifoldrDefault f g acc t =
  (applyEndo . getConst $ bitraverse (endo f) (endo g) t) acc
  where endo : forall x,y . (x -> y -> y) -> x -> Const (Endomorphism y) ()
        endo f = MkConst . Endo . f


text:
module Minecraft.Core.Univ

import public Minecraft.Data.Deserialize
import public Minecraft.Data.Type.Ctx
import public Minecraft.Data.Type.Vtbl

%default total

public export
record Univ where
  constructor MkUniv
  exists : String -> Maybe (Ctx Deserialize)
  reflect : (ty : Type) -> Maybe (Vtbl ty)

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module RLE

import Decidable.Equality

rep : Nat -> a -> List a

data RunLength : List a -> Type where
     Empty : RunLength []
     Run : (n : Nat) -> (x : a) -> (rest : RunLength more) ->
           RunLength (rep n x ++ more)

data Singleton : a -> Type where
     Val : (x : a) -> Singleton x

uncompress : RunLength xs -> Singleton xs

{-

rle : DecEq a => (xs : List a) -> RLE xs
rle [] = Empty
rle (x :: xs) with (rle xs)
  rle (x :: []) | Empty = Run 1 x Empty
  rle (x :: (rep n y ++ more)) | (Run n y comp) with (decEq x y)
    rle (y :: (rep n y ++ more)) | (Run n y comp) | (Yes Refl)
        = Run (S n) y comp
    rle (x :: (rep n y ++ more)) | (Run n y comp) | (No contra)
        = Run 1 x $ Run n y comp

data Singleton : a -> Type where
     Val : (x : a) -> Singleton x

uncompress : RLE xs -> Singleton xs

-- uncompress Empty = Val []
-- uncompress (Run n x comp)
--     = let Val rec = uncompress comp in
--           Val (rep n x ++ rec)

uncompressHelp : (x : a) -> RLE more -> (n : Nat) -> Singleton more -> Singleton (rep n x ++ more)
uncompressHelp x comp n (Val _) = Val (rep n x ++ more)

uncompress' : RLE xs -> Singleton xs
uncompress' Empty = Val []
uncompress' (Run n x comp)
    = let rec = uncompress' comp in
          uncompressHelp x comp n rec

{-
rle [] = Empty
rle (x :: xs) with (rle xs)
  rle (x :: []) | Empty = Run 1 x Empty
  rle (x :: (rep n y ++ more)) | (Run n y comp) with (decEq x y)
    rle (y :: (rep n y ++ more)) | (Run n y comp) | (Yes Refl)
        = Run (S n) y comp
    rle (x :: (rep n y ++ more)) | (Run n y comp) | (No contra)
        = Run 1 x $ Run n y comp

uncompress Empty = Val []
uncompress (Run n x comp)
   = let Val uncomp = uncompress comp in
         Val (rep n x ++ uncomp)
-}
-}


text:
module A

import B
import C

-- %logging 10
foo : Char
foo = bar
%logging 0


text:
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe (Just x) (Just y) = case compare x y of
                                  LT => Just y
                                  EQ => Just x
                                  GT => Just x

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Control.Eff.State

import Control.Eff.Internal

%default total

public export
data StateL : (lbl : k) -> (s : Type) -> (a : Type) -> Type where
  [search lbl]
  Get : StateL lbl s s
  Put : (vs : s) -> StateL lbl s ()

public export
State : (s,a : Type) -> Type
State = StateL ()

export
getAt : (0 lbl : k) -> Has (StateL lbl s) fs => Eff fs s
getAt lbl = send $ Get {lbl}

export %inline
get : Has (State s) fs => Eff fs s
get = getAt ()

export
putAt : (0 lbl : k) -> Has (StateL lbl s) fs => s -> Eff fs ()
putAt lbl vs = send $ Put {lbl} vs

export %inline
put : Has (State s) fs => s -> Eff fs ()
put = putAt ()

export
modifyAt : (0 lbl : k) -> Has (StateL lbl s) fs => (s -> s) -> Eff fs ()
modifyAt lbl f = getAt lbl >>= putAt lbl . f

export %inline
modify : Has (State s) fs => (s -> s) -> Eff fs ()
modify = modifyAt ()

--------------------------------------------------------------------------------
--          Running State
--------------------------------------------------------------------------------

export
handleState :  {0 m : Type -> Type}
            -> (get : m s)
            -> (put : s -> m ())
            -> StateL lbl s a
            -> m a
handleState get _   Get      = get
handleState _   put (Put vs) = put vs

unState : s -> StateL lbl s a -> (a,s)
unState vs Get     = (vs,vs)
unState _ (Put s2) = ((),s2)

export
runStateAt :  (0 lbl : k)
           -> Has (StateL lbl s) fs
           => s
           -> Eff fs t
           -> Eff (fs - StateL lbl s) (t,s)
runStateAt _ vs =
  handleRelayS vs (\x,y => pure (y,x)) $ \vs2,st,f =>
    let (vv,vs3) = unState vs2 st
     in f vs3 vv

export %inline
runState : Has (State s) fs => s -> Eff fs t -> Eff (fs - State s) (t,s)
runState = runStateAt ()


text:
module Main
import Data.SortedMap
import Invincy

data JsonValue = JsonString String
               | JsonNumber Double
               | JsonBool Bool
               | JsonNull
               | JsonArray (List JsonValue)
               | JsonObject (SortedMap String JsonValue)

-- can't generate it with elaborator reflection yet
data JsonType = JTString
              | JTNumber
              | JTBool
              | JTNull
              | JTArray
              | JTObject

-- derivation with Pruviloj.Derive.DecEq leads to strange errors
implementation DecEq JsonType where
  decEq JTString JTString = Yes Refl
  decEq JTNumber JTNumber = Yes Refl
  decEq JTBool JTBool = Yes Refl
  decEq JTNull JTNull = Yes Refl
  decEq JTArray JTArray = Yes Refl
  decEq JTObject JTObject = Yes Refl
  decEq x y = No $ believe_me (x = y -> Void) -- won't need those

jcArgs : JsonType -> (x ** x -> JsonValue)
%runElab (cArgs (NS (UN "jcArgs") ["Main"]))

dsJson : JsonValue -> (x ** getWitness (jcArgs x))
%runElab (dArgs `(\x => getWitness (jcArgs x)) (NS (UN "dsJson") ["Main"]))

jsonNull' : PP String ()
jsonNull' = raw' "null"

jsonBool' : PP String Bool
jsonBool' = choices' {f=const ()} {e=Bool} (const {b=()}) (\b => (b ** ()))
  [(True ** raw' "true"),
   (False ** raw' "false")]

jsonNumber' : PP String Double
jsonNumber' = (jsonNumber, MkPrinter $ fromString . show)
  where
    jsonNumber : Parser String Double
    jsonNumber = do
      x <- getWitness <$> some digit
      y <- option $ Prelude.Applicative.(*>) (val '.') (getWitness <$> some digit)
      return $ cast . pack $ x ++ (maybe neutral ('.' ::) y)

jsonString' : PP String String
jsonString' = (jsonString, MkPrinter $ fromString . show)
  where
    jsonStr : Parser String String
    jsonStr = (val '"' *> pure neutral) <|> do
      c <- sat (/= '"')
      if (c == '\\')
      then cons <$> oneOf ['"', '\\', '/', '\b', '\f', '\n', '\r', '\t'] <*> jsonStr
      else (cons c) <$> jsonStr
    jsonString : Parser String String
    jsonString = val '"' *> jsonStr

mutual
  jsonValue' : PP String JsonValue
  jsonValue' = choices dsJson
    [ (JTString ** jsonString')
    , (JTNumber ** jsonNumber')
    , (JTBool ** jsonBool')
    , (JTNull ** jsonNull')
    , (JTArray ** jsonArray')
    , (JTObject ** jsonObject')
    ]

  jsonArray' : PP String (List JsonValue)
  jsonArray' =
    val' '[' *> spaces' *>
    sepBy' jsonValue' (spaces' *> val' ',' <* spaces')
    <* spaces' <* val' ']'

  jsonObject' : PP String (SortedMap String JsonValue)
  jsonObject' = (fromList, toList) <$>
    (val' '{' *> spaces' *>
     sepBy' (jsonString' <* spaces' <* val' ':' <* spaces' <*> jsonValue')
            (spaces' *> val' ',' <* spaces')
     <* spaces' <* val' '}')

json' : PP String JsonValue
json' = choices dsJson
  [ (JTArray ** jsonArray')
  , (JTObject ** jsonObject')
  ]

main : IO ()
main = do
  putStrLn "Type some JSON here:"
  v <- parseWith' (spaces' *> json') $ (++ "\n") <$> getLine
  case v of
    Done i x => do
      putStrLn "Parsed! Printing:"
      putStrLn $ print' json' x
    Failure s => putStrLn $ "Failure: " ++ s
    Partial _ => putStrLn "Uh oh, partial"
  main

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
module Idris.Env

--- All environment variables accessed by the compiler are enumerated in this module.

import public Data.List
import public Data.Maybe

import System

%default total

||| Environment variable used by Idris2 compiler
public export
record EnvDesc where
  constructor MkEnvDesc
  name : String
  help : String

||| All environment variables used by Idris2 compiler
public export
envs : List EnvDesc
envs = [
         MkEnvDesc "EDITOR"        "Editor used in REPL :e command",
         MkEnvDesc "IDRIS2_PREFIX" "Idris2 installation prefix",
         MkEnvDesc "IDRIS2_PATH"   "Places Idris2 looks for import files",
         MkEnvDesc "IDRIS2_PACKAGE_PATH" "Places Idris2 looks for packages",
         MkEnvDesc "IDRIS2_DATA"   "Places Idris2 looks for data files",
         MkEnvDesc "IDRIS2_LIBS"   "Places Idris2 looks for libraries (for code generation)",
         MkEnvDesc "IDRIS2_CG"     "Codegen backend",
         MkEnvDesc "IDRIS2_INC_CGS" "Code generators to use (comma separated) when compiling modules incrementally",
         MkEnvDesc "CHEZ"          "chez executable used in Chez codegen",
         MkEnvDesc "RACKET"        "racket executable used in Racket codegen",
         MkEnvDesc "RACKET_RACO"   "raco executable used in Racket codegen",
         MkEnvDesc "GAMBIT_GSI"    "gsi executable used in Gambit codegen",
         MkEnvDesc "GAMBIT_GSC"    "gsc executable used in Gambit codegen",
         MkEnvDesc "GAMBIT_GSC_BACKEND" "gsc executable backend argument",
         MkEnvDesc "IDRIS2_CC"     "C compiler executable used in RefC codegen",
         MkEnvDesc "CC"            "C compiler executable used in RefC codegen",
         MkEnvDesc "NODE"          "node executable used in Node codegen",
         MkEnvDesc "PATH"          "PATH variable is used to search for executables in certain codegens"
       ]

--- `public export` only for `auto` to work in `idrisGetEnv`
public export
envNames : List String
envNames = map (.name) envs

||| Query documented environment variable
public export
idrisGetEnv : HasIO io => (name : String) ->
  {auto known : IsJust (find (name ==) Env.envNames)}
  -> io (Maybe String)
idrisGetEnv name = getEnv name


text:
module Main

f : String -> Bool
f "yes" = True
f _ = False

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.Num

||| integral power
export
power : Num a => a -> Nat -> a
power a Z = 1
power a (S i) = a * power a i

export
square : Num a => a -> a
square x = power x 2

export
cube : Num a => a -> a
cube x = power x 3


text:
module Parser.Lexer.Package

import public Parser.Lexer.Common
import public Text.Lexer
import public Text.Parser
import public Text.Bounded
import Text.PrettyPrint.Prettyprinter

import Data.List
import Data.List1
import Data.Strings
import Data.String.Extra
import Utils.String

import Core.Name.Namespace

%default total

public export
data Token
  = Comment String
  | EndOfInput
  | Equals
  | DotSepIdent (Maybe Namespace) String
  | Separator
  | Space
  | StringLit String

public export
Show Token where
  show (Comment str) = "Comment: " ++ str
  show EndOfInput = "EndOfInput"
  show Equals = "Equals"
  show (DotSepIdent ns n) = "DotSepIdentifier: " ++ show ns ++ "." ++ show n
  show Separator = "Separator"
  show Space = "Space"
  show (StringLit s) = "StringLit: " ++ s

public export
Pretty Token where
  pretty (Comment str) = "Comment:" <++> pretty str
  pretty EndOfInput = "EndOfInput"
  pretty Equals = "Equals"
  pretty (DotSepIdent ns n) = "DotSepIdentifier:" <++> pretty ns <+> dot <+> pretty n
  pretty Separator = "Separator"
  pretty Space = "Space"
  pretty (StringLit s) = "StringLit:" <++> pretty s

equals : Lexer
equals = is '='

separator : Lexer
separator = is ','

rawTokens : TokenMap Token
rawTokens =
  [ (equals, const Equals)
  , (comment, Comment . drop 2)
  , (namespacedIdent, uncurry DotSepIdent . mkNamespacedIdent)
  , (identAllowDashes, DotSepIdent Nothing)
  , (separator, const Separator)
  , (spacesOrNewlines, const Space)
  , (stringLit, \s => StringLit (stripQuotes s))
  ]

export
lex : String -> Either (Int, Int, String) (List (WithBounds Token))
lex str =
  case lexTo (const False) rawTokens str of
       (tokenData, (l, c, "")) =>
         Right $ (filter (useful . val) tokenData) ++ [MkBounded EndOfInput False l c l c]
       (_, fail) => Left fail
  where
    useful : Token -> Bool
    useful (Comment c) = False
    useful Space       = False
    useful _ = True


text:
module Prelude.Bound

public export
interface Ord b => MinBound b where
  ||| The lower bound for the type
  minBound : b

public export
interface Ord b => MaxBound b where
  ||| The upper bound for the type
  maxBound : b

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Optimisation.DeadArgumentEliminator

import Core.Context
import Data.List
import Data.SortedSet
import Data.SortedMap

import CommonDef
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Optimisation.DeadCodeElimination
import CairoCode.Traversal.Base
import CairoCode.Traversal.ValueTracker
import Utils.Lens
import Utils.Helpers

import Debug.Trace

%hide Prelude.toList

-- Note: Initially a DeadReturnEliminator was planned alongside this.
--       However, it would only work after Untuppling (as Idris is single return)
--       Further, most idris code would not profit from it (as tuple returns are rare)
--       Last, a data flow based dead constructor argument could do the same and more (so if needed a data flow analysis is more viable)

ArgUsageState : Type
ArgUsageState = SortedMap Name (List Bool)

collectUsedRegisters : (Name, CairoDef) -> ArgUsageState -> SortedSet CairoReg
collectUsedRegisters def state = snd $ runVisitConcatCairoDef (traversal $ valueCollector idLens (dbgDef def) weakGeneralizedTrack returnCollector) def
    where dbgDef : (Name, CairoDef) -> CairoReg -> SortedSet CairoReg
          dbgDef (name, def) reg = trace "Register not bound in \{show name}: \{show reg}" (singleton reg)
          returnCollector : InstVisit  (SortedSet CairoReg) -> Traversal (ScopedBindings (SortedSet CairoReg)) (SortedSet CairoReg)
          returnCollector (VisitReturn res impls) = pure $ foldl union empty (res ++ (values impls))
          returnCollector _ = pure empty
          weakGeneralizedTrack : (v:(InstVisit (SortedSet CairoReg))) -> Traversal  (ScopedBindings (SortedSet CairoReg)) (ValBindType v (SortedSet CairoReg))
          weakGeneralizedTrack (VisitCall res linImpls name args) = registerTracker (VisitCall res linImpls name neededArgs)
            where neededArgs : List (SortedSet CairoReg)
                  neededArgs = case (lookup name state) of
                    Nothing => args
                    (Just argUse) => map snd (filter fst (zip argUse args))
          weakGeneralizedTrack inst = registerTracker inst

updateUsedArgumentsDef : (Name, CairoDef) -> ArgUsageState -> (Bool, ArgUsageState)
updateUsedArgumentsDef def@(name, FunDef params _ _ _) state = integrate (lookup name state) (collectUsedRegisters def state)
    where argsNeeded : SortedSet CairoReg -> List Bool
          argsNeeded req = map (\reg => contains reg req) params
          integrate : Maybe (List Bool) -> SortedSet CairoReg -> (Bool, ArgUsageState)
          integrate Nothing req = (True, insert name (argsNeeded req) state)
          integrate (Just oldArgs) req = (newNeeded /= oldArgs,  insert name newNeeded state)
              where newNeeded : List Bool
                    newNeeded = zipWith (\a,b => a || b) oldArgs (argsNeeded req)
updateUsedArgumentsDef _ state = (False, state)

singleUsedArgumentsPass : List (Name, CairoDef) -> ArgUsageState -> (Bool, ArgUsageState)
singleUsedArgumentsPass defs state = foldl process (False,state) defs
    where process : (Bool, ArgUsageState) -> (Name, CairoDef) -> (Bool, ArgUsageState)
          process (changed, state) def = let (nChanged, nState) = updateUsedArgumentsDef def state
            in (changed || nChanged, nState)

-- runs singleUsedArgumentsPass until nothing changed
iterUsedArguments : List (Name, CairoDef) -> ArgUsageState -> ArgUsageState
iterUsedArguments defs state = continueCheck (singleUsedArgumentsPass defs state)
    where continueCheck : (Bool, ArgUsageState) -> ArgUsageState
          continueCheck (False, state) = state
          continueCheck (True, state) = iterUsedArguments defs state

collectNonClosures : List (Name, CairoDef) -> List (Name, CairoDef)
collectNonClosures defs = filter (\(n,_) => not $ contains n allClosureCalls) defs
 where closureCollector : InstVisit CairoReg -> SortedSet Name
       closureCollector (VisitMkClosure _ name _ _) = singleton name
       closureCollector _ = empty
       allClosureCalls : SortedSet Name
       allClosureCalls = snd $ runVisitConcatCairoDefs (pureTraversal closureCollector) defs

collectUsedArguments : List (Name, CairoDef) -> ArgUsageState
collectUsedArguments defs = iterUsedArguments defs initialArgUseState
    where buildEntry : (Name, CairoDef) -> (Name, List Bool)
          buildEntry (name, FunDef params _ _ _) = (name, replicate (length params) False)
          buildEntry (name, ForeignDef _ args _ ) =  (name, replicate args True)
          initialArgUseState: ArgUsageState
          initialArgUseState = fromList $ map buildEntry defs

removeCallArguments : ArgUsageState -> (Name, CairoDef) -> (Name, CairoDef)
removeCallArguments argsNeeded def = snd $ runVisitTransformCairoDef (pureTraversal eliminateCallArgs) def
    where neededArgs : Name -> List CairoReg ->  List Bool
          neededArgs name regs = fromMaybe (map (\_ => True) regs) (lookup name argsNeeded)
          filterArgs : Name -> List CairoReg -> List CairoReg
          filterArgs name regs = map snd (filter fst (zip (neededArgs name regs) regs))
          eliminateCallArgs : InstVisit CairoReg -> List (InstVisit CairoReg)
          eliminateCallArgs (VisitCall res impls name args) = [(VisitCall res impls name (filterArgs name args))]
          eliminateCallArgs inst = [inst]

removeFunArguments : ArgUsageState -> (Name, CairoDef) ->  (Name, CairoDef)
removeFunArguments argsNeeded (name, FunDef params impls rets body) = if name == entry_name
    then (name, FunDef params impls rets body)                -- leave the main alone to preserve signature
    else (name, FunDef neededParams impls rets body)
    where neededArgs : List Bool
          neededArgs = fromMaybe (map (\_ => True) params) (lookup name argsNeeded)
          neededParams : List CairoReg
          neededParams = map snd (filter fst (zip neededArgs params))
removeFunArguments _ def = def

public export
eliminateDeadArgumentsDefs : List (Name, CairoDef) ->  List (Name, CairoDef)
eliminateDeadArgumentsDefs defs = map processDef defs
    where usedArguments : ArgUsageState
          usedArguments = collectUsedArguments (collectNonClosures defs)
          processDef : (Name, CairoDef) -> (Name, CairoDef)
          processDef = (removeFunArguments usedArguments) . eliminateDeadCode . (removeCallArguments usedArguments)

-- Note: To be certain we need to do 1 again as 2 can enable 1 and repeat until we are done

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module gcd

import ZZ
import Bezout

--isDivisible a b can be constucted if b divides a
isDivisible : Nat -> Nat -> Type
isDivisible a b = (n : Nat ** a = b * n)

--1 divides everything
oneDiv : (a : Nat) -> isDivisible a 1
oneDiv a = (a ** rewrite plusZeroRightNeutral a in Refl)

--If 1|a => 1*c | a*c
mulDiv : (a, c : Nat) -> isDivisible a 1 -> isDivisible (a * c) c
mulDiv a c x = (a ** rewrite multCommutative c a in Refl)

gcdBya : (a : Nat) -> (b : Nat) -> NotBothZero a b -> Nat
gcdBya a b prf = div a (gcd a b {ok=prf})

gcdByb : (a : Nat) -> (b : Nat) -> NotBothZero a b -> Nat
gcdByb a b prf = div b (gcd a b {ok=prf})

|||Genetes a proof of (a+b) = d*(n+m) from (a=d*n)and (b=d*m)
DistributeProof: (a:Nat)->(b:Nat)->(d:Nat)->(n:Nat)->(m:Nat)->(a=d*n)->(b=d*m)->((a+b) = d*(n+m))
DistributeProof a b d n m pf1 pf2 = rewrite  (multDistributesOverPlusRight d n m) in(trans (the (a+b=(d*n)+b) (v1)) v2) where
  v1 =plusConstantRight a (d*n) b pf1
  v2 =plusConstantLeft b (d*m) (d*n) pf2

|||The theorem d|a =>d|ac
MultDiv:(isDivisible a d) ->(c:Nat)->(isDivisible (a*c) d)
MultDiv {d} (n**Refl) c =((n*c)** (rewrite sym (multAssociative d n c) in (Refl)))

|||The theorem d|a and d|b =>d|(a+b)
PlusDiv : (isDivisible a d)->(isDivisible b d)->(isDivisible (a+b) d)
PlusDiv {d}{a}{b} (n**prf1) (m**prf2) = ((n+m)**(DistributeProof a b d n m prf1 prf2))
{-

gcdDiva : (a : Nat) -> (b : Nat) -> NotBothZero a b -> isDivisible a (gcd a b)
gcdDiva a b prf = mulDiv (gcdBya a b prf)
  (gcd a b {ok=prf})
  (oneDiv (gcdBya a b prf))
-}
{-
gcdDivb : (a : Nat) -> (b : Nat) -> NotBothZero a b -> isDivisible b (gcd a b)
gcdDivb a b prf = mulDiv (gcdByb a b prf)
  (gcd a b {ok=prf})
  (oneDiv (gcdByb a b prf))
-}
--gcd is already implemented in the standard library
gcdproof : (a : Nat) -> (b : Nat) -> NotBothZero a b ->
  (d : Nat ** ((k : Nat ** a = d*k),(l : Nat ** b = d*l)))
gcdproof a b prf =
  (gcd a b {ok=prf} ** (?parta, ?partb))

--Proof to finish euclidDivide, couldn't add it as a where clause within euclidDivide. If someone knows how to do that, please do so.
extendedEqualityProof : (a : Nat) -> (b : Nat) -> (q : Nat) -> (r : Nat)-> (S r = b) -> (a = r + (q * b)) -> (S a = (S q) * b)
extendedEqualityProof (r + (q * (S r))) (S r) q r Refl Refl = Refl

--Given a, b, and a proof that b != 0, returns (q, r) and proofs that a = bq + r, r < b  {removed possible problems with Rohit's}
euclidDivide : (a : Nat) -> (b : Nat) -> (b = Z -> Void) -> (q : Nat ** (r : Nat ** ((a = r + (q * b)), LT r b)))
euclidDivide Z (S k) SIsNotZ = (Z ** (Z ** (Refl, LTESucc LTEZero)))
euclidDivide (S n) (S k) SIsNotZ = case (euclidDivide n (S k) SIsNotZ) of
								(q ** (r ** (equalityProof, ltproof))) => case (proofLTimplieseqorLT r (S k) ltproof) of
																	(Right proofSrLTSk) => (q ** ((S r) ** ((functionExtendEquality S n (r + (q * (S k))) equalityProof), proofSrLTSk)))
																	(Left proofSreqSk) => ((S q) ** (Z ** ((extendedEqualityProof n (S k) q r proofSreqSk equalityProof), LTESucc LTEZero)))

--Bezout
{-
--if gcd a b = d, d = ax + by for some x,y Integers (Given by Bezout)
bezproof : (a : Nat) -> (b : Nat) -> NotBothZero a b ->
  (x : (ZZ,ZZ) ** ((cast{from=Nat}{to=ZZ} a)*(fst x) +
                   (cast{from=Nat}{to=ZZ} b)*(snd x) = cast (gcd a b)))
bezproof a b x = (Bezout a b ** ?help)
-}


text:
module VirtualDom

import Js.ASync

%include JavaScript "js/virtualdom.js"

export
data Node : Type -> Type -> Type where
  MkNode : Ptr -> Node a b

export
data Attribute : Type -> Type -> Type where
  MkAttribute : Ptr -> Attribute a b

export
node : String -> List (Attribute b a) -> List (Node c a) -> Node c a
node tag attrs childs =
  let attrsPtr =
      unsafePerformIO $
        (makeJSList $ map (\(MkAttribute x) => x) attrs) >>=
          jscall "$JSLIB$virtualdom.attributesListToObj(%0)" (Ptr -> JS_IO Ptr)
      childsPtr = unsafePerformIO $ makeJSList $ map (\(MkNode x) => x) childs
  in MkNode $ unsafePerformIO $ jscall "{type: 'n', tag: %0, attrs: %1, childs: %2}" (String -> Ptr -> Ptr -> JS_IO Ptr) tag attrsPtr childsPtr

export
nodeNS : String -> String -> List (Attribute b a) -> List (Node c a) -> Node c a
nodeNS ns tag attrs childs =
  let attrsPtr =
      unsafePerformIO $
        (makeJSList $ map (\(MkAttribute x) => x) attrs) >>=
          jscall "$JSLIB$virtualdom.attributesListToObj(%0)" (Ptr -> JS_IO Ptr)
      childsPtr = unsafePerformIO $ makeJSList $ map (\(MkNode x) => x) childs
  in MkNode $ unsafePerformIO $ jscall "{type: 'nn', ns: %0 , tag: %1, attrs: %2, childs: %3}" (String -> String -> Ptr -> Ptr -> JS_IO Ptr) ns tag attrsPtr childsPtr

export
text : String -> Node c a
text txt =
  MkNode $ unsafePerformIO $ jscall "{type: 't', text: %0}" (String -> JS_IO Ptr) txt

export
stringAttribute : String -> String -> Attribute a b
stringAttribute name value =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'r',name:%0, value:%1}"
      (String -> String -> JS_IO Ptr)
      name
      value

export
stringAttributeNS : String -> String -> String -> Attribute a b
stringAttributeNS ns name value =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'rn', ns: %0, n:%1, name:%0+':'+%1, value:%2}"
      (String -> String -> String -> JS_IO Ptr)
      ns
      name
      value

export
propertyAttribute : String -> String -> Attribute a b
propertyAttribute name value =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'p', name:%0, value:%1}"
      (String -> String -> JS_IO Ptr)
      name
      value

export
booleanAttribute : String -> Bool -> Attribute a b
booleanAttribute name value =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'b', name:%0, value:%1}"
      (String -> Int -> JS_IO Ptr)
      name
      (if value then 1 else 0)

export
data Style = MkStyle Ptr

export
mkStyle : String -> String -> Style
mkStyle n v =
  MkStyle $ unsafePerformIO $
    jscall
      "$JSLIB$virtualdom.mkStyle(%0,%1)"
      (String -> String -> JS_IO Ptr)
      n
      v

export
Nil : Style
Nil =
  MkStyle $ unsafePerformIO $
    jscall
      "{}"
      (JS_IO Ptr)

export
(::) : Style -> Style -> Style
(::) (MkStyle x) (MkStyle y) =
  MkStyle $ unsafePerformIO $
    jscall
      "Object.assign(%0,%1)"
      (Ptr -> Ptr -> JS_IO Ptr)
      y
      x

export
style : Style -> Attribute a b
style (MkStyle stl) =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'s', name: 'style', value:%0}"
      (Ptr -> JS_IO Ptr)
      stl

export
eventListenerAttribute : String -> (Ptr -> JS_IO b) -> Attribute a b
eventListenerAttribute name read =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'e', name:%0, read: %1}"
      (String -> JsFn (Ptr -> JS_IO Ptr) -> JS_IO Ptr)
      name
      (MkJsFn $ believe_me read)

export
customEventListenerAttribute : String -> (Ptr -> JS_IO ()) -> (Ptr -> JS_IO b) -> Attribute a b
customEventListenerAttribute name initE read =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'ec', name:%0, init: %1 , read: %2}"
      (String -> JsFn (Ptr -> JS_IO ()) -> JsFn (Ptr -> JS_IO Ptr) -> JS_IO Ptr)
      name
      (MkJsFn $ initE)
      (MkJsFn $ believe_me read)

export
eventListenerAttributePreventDefault : String -> (Ptr -> JS_IO b) -> Attribute a b
eventListenerAttributePreventDefault event convert =
  MkAttribute $ unsafePerformIO $
    jscall
      "{type:'ep', name:%0, read: %1}"
      (String -> JsFn (Ptr -> JS_IO Ptr) -> JS_IO Ptr)
      event
      (MkJsFn $ believe_me convert)

export
implementation Functor (Attribute a) where
  map f (MkAttribute x) =
    assert_total $ MkAttribute $ unsafePerformIO $
      jscall
        "$JSLIB$virtualdom.mapAttribute(%0, %1)"
        (JsFn (Ptr -> Ptr) -> Ptr -> JS_IO Ptr)
        (MkJsFn $ believe_me f)
        x

export
implementation Functor  (Node a) where
  map f (MkNode x) =
    assert_total $ MkNode $ unsafePerformIO $
      jscall
        "$JSLIB$virtualdom.mapNode(%0, %1)"
        (JsFn (Ptr -> Ptr) -> Ptr -> JS_IO Ptr)
        (MkJsFn $ believe_me f)
        x

export
initialyzeBody : JSIOFifoQueue b -> Node a b -> JS_IO ()
initialyzeBody q (MkNode x) =
  jscall
   "$JSLIB$virtualdom.initialyzeBody(%0, %1)"
   (Ptr -> Ptr -> JS_IO ())
   (getQueuePtr q)
   x

export
updateNode : Node a b -> Node a b -> JS_IO ()
updateNode (MkNode x) (MkNode y) =
  jscall
    "$JSLIB$virtualdom.update(%0,%1)"
    (Ptr -> Ptr -> JS_IO ())
    x
    y

export
updateNodeM : JSIOFifoQueue b -> Node a c -> Node a b -> JS_IO (Node a b)
updateNodeM q (MkNode x) (MkNode y) =
  do
    jscall
      "$JSLIB$virtualdom.updateQueue(%0, %1)"
      (Ptr -> Ptr -> JS_IO ())
      (getQueuePtr q)
      x
    jscall
      "$JSLIB$virtualdom.update(%0,%1)"
      (Ptr -> Ptr -> JS_IO ())
      x
      y
    pure $ MkNode x

export
clearNode : Node a b -> JS_IO ()
clearNode (MkNode x) = jscall "$JSLIB$virtualdom.clear(%0)" (Ptr -> JS_IO ()) x

public export
data AnimationOption : Type where
  Duration : Nat -> AnimationOption

readAnimationOptions : List AnimationOption -> JS_IO Ptr
readAnimationOptions [] =
  jscall "{'fill':'both'}" (JS_IO Ptr)
readAnimationOptions ((Duration d)::r) =
  readAnimationOptions r >>= \x => jscall "Object.assign(%0,{'duration':%1})" (Ptr -> Int -> JS_IO Ptr) x (cast d)

export
animateNode : List AnimationOption -> Node a b -> Node a b -> JS_IO ()
animateNode animOpts (MkNode x) (MkNode y) =
  do
    opts <- readAnimationOptions animOpts
    jscall
      "$JSLIB$virtualdom.animate(%0,%1,%2)"
      (Ptr -> Ptr -> Ptr -> JS_IO ())
      opts
      x
      y

export
duration : Nat -> AnimationOption
duration = Duration

export
availableHeight_ : JS_IO Double
availableHeight_ = jscall "$JSLIB$virtualdom.availableHeight()" (JS_IO Double)

export
availableWidth_ : JS_IO Double
availableWidth_ = jscall "$JSLIB$virtualdom.availableWidth()" (JS_IO Double)

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Data.Crypto.Encryption.TDEA

import Data.Vect

import Data.Crypto.Encryption.Block
import Data.Crypto.Encryption.Block.DEA
import Data.Fin

%default total
%access public export

TDEA1Key : Type
TDEA1Key = Vect 3 DEAKey

TDEA2Key : Type
TDEA2Key = Vect 2 DEAKey

data TripleDataEncryptionAlgorithm : Fin 2 -> Type where
  TDEA1 : TDEA1Key -> TripleDataEncryptionAlgorithm 0
  TDEA2 : TDEA2Key -> TripleDataEncryptionAlgorithm 1

implementation BlockCipher (TripleDataEncryptionAlgorithm 0) 64 (power 2 32) where
  encryptBlock (TDEA1 key) block =
    encryptBlock (DEA (index 2 key))
                 (decryptBlock (DEA (index 1 key))
                               (encryptBlock (DEA (index 0 key)) block))
  decryptBlock (TDEA1 key) block =
    decryptBlock (DEA (index 0 key))
                 (encryptBlock (DEA (index 1 key))
                               (decryptBlock (DEA (index 2 key)) block))

implementation BlockCipher (TripleDataEncryptionAlgorithm 1) 64 (power 2 20) where
  encryptBlock (TDEA2 key) = encryptBlock (TDEA1 (key ++ [index 0 key]))
  decryptBlock (TDEA2 key) = decryptBlock (TDEA1 (key ++ [index 0 key]))

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:
{-
42
4.2
it works!
True
00000000-0000-0000-0000-000000000000
VoidFunction : Void
exportedBoolToString : (p0 : Boolean) -> String
printMethod : (t : Type) -> (n : String) -> Void
take5 : (defaultValue : String) -> (flag : Boolean) -> (c : Char) -> (i : Int32) -> (d : Double) -> String
before exportedVoidIO
exported!
after exportedVoidIO
exportedBoolToStringIO True
exportedBoolToStringIO => True
Alan Kay
Kay, Alan
3
createPerson, exportedBoolToString, exportedBoolToStringIO, exportedIncInt, firstName, lastName, printMethod, take5, VoidFunction
-}

module Main

import CIL.System.Reflection
import Data.Vect

%inline
objectArrayFor : Vect _ Object -> CIL_IO ObjectArray
objectArrayFor xs = arrayOf CILTyObj xs

testValueType : CIL_IO ()
testValueType = do
  guid  <- Guid.NewGuid
  guid' <- Guid.Parse !(ToString guid)
  printLn !(Equals guid guid')
  ToString !Guid.Empty >>= putStrLn

invokeStaticMethod : RuntimeType -> String -> Maybe ObjectArray -> CIL_IO (Maybe Object)
invokeStaticMethod type methodName args =
  maybe (pure Nothing) (\method => Just <$> Invoke method Nothing args) !(type `GetMethod` methodName)

testExportedVoidFunction : RuntimeType -> CIL_IO ()
testExportedVoidFunction type = do
  putStrLn "before exportedVoidIO"
  invokeStaticMethod type "VoidFunction" Nothing
  putStrLn "after exportedVoidIO"

testExportedBoolToStringIO : RuntimeType -> CIL_IO ()
testExportedBoolToStringIO type = do
  ret <- invokeStaticMethod type "exportedBoolToStringIO" (Just !(objectArrayFor [upcast True]))
  retString <- maybe (pure "ERROR") ToString ret
  putStrLn $ "exportedBoolToStringIO => " ++ retString

record Person where
  constructor MkPerson
  firstName, lastName : String

-- And now for something completely different...
-- Let's use the IMPORTING FFI to test the EXPORTING FFI

||| Descriptor for the type hosting all exported functions.
TheExportsTy : CILTy
TheExportsTy = CILTyRef "" "TheExports"

||| The foreign view of the exported type Person
||| is a struct with a single field `ptr`.
ExportedPerson : Type
ExportedPerson = CIL $ CILTyVal "" "Person"

||| Converts a foreign reference to an exported data type
||| into its internal representation.
unForeign : ExportedPerson -> CIL_IO Person
unForeign ep = do
  ptr <- invoke (CILInstanceField "ptr") (ExportedPerson -> CIL_IO Ptr) ep
  pure $ believe_me ptr

||| Invokes the exported function `createPerson` via the FFI.
invokeCreatePerson : String -> String -> CIL_IO ExportedPerson
invokeCreatePerson =
  invokeStatic TheExportsTy "createPerson" (String -> String -> CIL_IO ExportedPerson)

%inline
invokeAccessor : String -> ExportedPerson -> CIL_IO String
invokeAccessor n =
  invokeStatic TheExportsTy n (ExportedPerson -> CIL_IO String)

testExportedRecord : CIL_IO ()
testExportedRecord = do
  -- exercise the foreign view of the record
  ep <- invokeCreatePerson "Alan" "Kay"
  putStrLn $ !(invokeAccessor "firstName" ep) ++ " " ++ !(invokeAccessor "lastName" ep)
  -- internal view should work just the same
  p  <- unForeign ep
  putStrLn $ lastName p ++ ", " ++ firstName p

testOverloadedStaticMethod : CIL_IO ()
testOverloadedStaticMethod = do
  Max (the Int 42) (the Int 1) >>= printLn
  Max 4.2 1.0 >>= printLn

testInstanceMethods : CIL_IO ()
testInstanceMethods = do
  sb <- new (CIL_IO StringBuilder)
  Append sb "it "
  AppendLine sb "works!"
  ToString sb >>= Write

showParameter : ParameterInfo -> CIL_IO String
showParameter p = do
  n <- get_Name p
  t <- get_ParameterType p >>= get_Name
  pure $ "(" ++ n ++ " : " ++ t ++ ")"

showMethod : MethodInfo -> CIL_IO String
showMethod m = do
  name <- get_Name m
  ps   <- foldr (\p, acc => (:: acc) <$> showParameter p) (the (List _) []) !(GetParameters m)
  ret  <- get_ReturnType m >>= get_Name
  let sig = ps ++ [ret]
  pure $ name ++ " : " ++ (concat . intersperse " -> " $ sig)

printMethod : RuntimeType -> String -> CIL_IO ()
printMethod t n = do
  m <- t `GetMethod` n
  maybe (pure "method not found") showMethod m >>= putStrLn

testBoxingUnboxing : RuntimeType -> CIL_IO ()
testBoxingUnboxing type = do
  ret <- invokeStaticMethod type "exportedIncInt" (Just !(objectArrayFor [upcast 2]))
  maybe (pure "ERROR") ToString ret >>= putStrLn

getExportsType : CIL_IO RuntimeType
getExportsType = do
  asm <- GetExecutingAssembly
  GetType asm "TheExports" True

testGetMethodsWithBindingFlags : CIL_IO ()
testGetMethodsWithBindingFlags = do
  type <- getExportsType
  methods <- type `GetMethods` (Public + Static)
  methodNames <- foldr (\m, acc => (:: acc) <$> get_Name m) (the (List String) []) methods
  putStrLn . concat . intersperse ", " . sort $ methodNames

main : CIL_IO ()
main = do
  testOverloadedStaticMethod
  testInstanceMethods
  testValueType

  type <- getExportsType
  for_ (the (List _) ["VoidFunction", "exportedBoolToString", "printMethod", "take5"]) $
    printMethod type

  testExportedVoidFunction type
  testExportedBoolToStringIO type
  testExportedRecord
  testBoxingUnboxing type
  testGetMethodsWithBindingFlags

-- Exports

createPerson : String -> String -> Person
createPerson = MkPerson

exportedVoidIO : CIL_IO ()
exportedVoidIO = putStrLn "exported!"

exportedBoolToString : Bool -> String
exportedBoolToString = show

exportedBoolToStringIO : Bool -> CIL_IO String
exportedBoolToStringIO b = do
  putStrLn $ "exportedBoolToStringIO " ++ show b
  pure $ show b

exportedIncInt : Int -> Int
exportedIncInt i = i + 1

parameters (defaultValue: String, flag: Bool)

  take5 : Char -> Int -> Double -> String
  take5 c i d = if flag then defaultValue else show $ cast (ord c) + cast i + d

exports : FFI_Export FFI_CIL "TheExports" [] -- declare exported functions on a type with given name
exports =
  Data Person "Person" $
  Fun createPerson CILDefault $ -- export function under original name
  Fun firstName CILDefault $ -- record field accessors are just functions and can be as easily exported
  Fun lastName CILDefault $
  Fun exportedVoidIO (CILExport "VoidFunction") $ -- export function under custom name
  Fun exportedBoolToString CILDefault $
  Fun exportedBoolToStringIO CILDefault $ -- export IO with return value
  Fun exportedIncInt CILDefault $ -- pass and get back value type
  Fun printMethod CILDefault $ -- export signature containing CIL type
  Fun take5 CILDefault
  End

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Control.Effect.State

import Control.EffectAlgebra
import Control.HigherOrder

import Control.Monad.State

import public Control.Effect.Reader
import public Control.Effect.Writer

||| State effect - the union of Reader and Writer effects.
public export
StateE : Type -> (Type -> Type) -> (Type -> Type)
StateE s = ReaderE s :+: WriterE s

public export
Inj (StateE s) sig => Inj (ReaderE s) sig where
  inj = inj {sub = StateE s, sup = sig} . Inl

public export
Inj (StateE s) sig => Inj (WriterE s) sig where
  inj = inj {sub = StateE s, sup = sig} . Inr

-- public export
-- get : Algebra sig m => Inj (StateE s) sig => m s
-- get = send {sig} {eff = StateE s} (Inl Ask)

-- public export
-- put : Algebra sig m => Inj (StateE s) sig => s -> m ()
-- put x = send {sig} {eff = StateE s} (Inr (Tell x))

namespace Algebra
  public export
  [State] Algebra sig m => Algebra (StateE s :+: sig) (StateT s m) where
    alg ctxx hdl (Inl (Inl Ask)) =
      ST $ \s => pure {f = m} (s, (s <$ ctxx))
    alg ctxx hdl (Inl (Inr (Tell s))) =
      ST $ \_ => pure {f = m} (s, ctxx)
    alg ctxx hdl (Inr x) = ST $ \r => do
     res <- alg
       {f = Functor.Compose}
       (r, ctxx) h x
     pure res
     where
      h : Handler ((s,) . ctx) n m
      h =
         (~<~)
          {ctx1 = (s,), ctx2 = ctx}
          {l = n}
          {m = StateT s m} {n = m} (uncurry runStateT) hdl

  %hint public export
  HintState : Algebra sig m => Algebra (StateE s :+: sig) (StateT s m)
  HintState = State


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Chunk

import public Text.PrettyPrint.WL

%default total
%access public export

Chunk : Type -> Type
Chunk = Maybe

nonEmptyChunk : Chunk a -> Bool
nonEmptyChunk = isJust

chunked : (a -> a -> a)
        -> Chunk a -> Chunk a -> Chunk a
chunked _ Nothing  y        = y
chunked _ x        Nothing  = x
chunked f (Just x) (Just y) = Just $ f x y

extractChunk : Monoid a => Chunk a -> a
extractChunk = fromMaybe neutral

combine : Chunk Doc -> Chunk Doc -> Chunk Doc
combine = chunked (|++|)

tabulate' : Int -> List (Doc, Doc) -> Chunk Doc
tabulate' _    []    = Nothing
tabulate' size table = pure $ vcat
  [ indent 2 (fillBreak size key |+| value)
  | (key, value) <- table ]

-- | Display pairs of strings in a table.
tabulate : List (Doc, Doc) -> Chunk Doc
tabulate = tabulate' 24

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

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
import Effects
import Effect.Logging.Default

doubleFunc : Nat -> Eff Nat [LOG]
doubleFunc x = do
  warn $ unwords ["Doing the double with", show x ]
  pure (x+x)

main : IO ()
main = do
   x <- runInit [MkLogRes ALL] (doubleFunc 3)
   printLn x
   y <- run (doubleFunc 4)
   printLn y

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


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

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

zero_not_succ : (0 = S k) -> Void
zero_not_succ Refl impossible

succ_not_zero : (S k = 0) -> Void
succ_not_zero Refl impossible

no_rec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
no_rec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zero_not_succ
checkEqNat (S k) Z = No succ_not_zero
checkEqNat (S k) (S j) = case checkEqNat k j of
                              (Yes prf) => Yes (cong prf)
                              (No contra) => No (no_rec contra)

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 Sorted
import Data.Vect
import Card

||| Given vector of cards is sorted by value
||| in descending order
public export data Sorted: Vect n Card -> Type where
  SortEmpty :
    Sorted (the (Vect 0 Card) [])
  SortSingle:
    Sorted [x]
  SortMany:
    (x:Card) -> Sorted (y :: ys) -> (cardValue x) `GTE` (cardValue y) -> Sorted(x::y::ys)

--------------------------------------------------------------------------------
-- HeadIs, HeadIsEither

-- Proof that the specified vector has the specified head.
public export data HeadIs : Vect n e -> e -> Type where
    MkHeadIs : HeadIs (x::xs) x

-- Proof that the specified vector has one of the two specified heads.
--
-- NOTE: Could implement this as an `Either (HeadIs xs x) (HeadIs xs y)`,
--       but an explicit formulation feels cleaner.
public export data HeadIsEither : Vect n e -> (x:e) -> (y:e) -> Type where
    HeadIsLeft  : HeadIsEither (x::xs) x y
    HeadIsRight : HeadIsEither (x::xs) y x

export chooseGte: (x: Nat) -> (y:Nat) -> Either (x `GTE` y) (y `GTE` x)
chooseGte Z Z = Left LTEZero
chooseGte Z (S k) = Right LTEZero
chooseGte (S k) Z = Left LTEZero
chooseGte (S k) (S j) = case chooseGte k j of
                             (Left l) => Left (LTESucc l)
                             (Right r) => Right (LTESucc r)

export tailIsSortedToo : (p1 : Sorted (x :: xs)) -> Sorted xs
tailIsSortedToo SortSingle = SortEmpty
tailIsSortedToo (SortMany x SortSingle _) = SortSingle
tailIsSortedToo (SortMany x (SortMany y z w) _) = SortMany y z w

--=======================================================================================================
-- isSorted
--=======================================================================================================
singleNotSorted : (contra : LTE (cardValue y) (cardValue x) -> Void) -> Sorted (x :: (y :: xs)) -> Void
singleNotSorted contra (SortMany x xs p) = contra p

restNotSorted : (contra : Sorted (y :: xs) -> Void) -> Sorted (x :: (y :: xs)) -> Void
restNotSorted contra (SortMany u v p) = contra v

export isSorted: (y: Vect n Card) -> Dec (Sorted y)
isSorted [] = Yes (SortEmpty)
isSorted (x :: []) = Yes SortSingle
isSorted (x :: y :: xs) = case isLTE (cardValue y) (cardValue x) of
                            (Yes prf_single) => (case isSorted (y::xs) of
                                               (Yes prf_rest) => Yes (SortMany x prf_rest prf_single)
                                               (No contra) => No (restNotSorted contra))
                            (No contra) => No (singleNotSorted contra)


text:
> module SequentialDecisionGames.CoreTheory

> import Sigma.Sigma
> import Sigma.Operations

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

* Preliminaries

For the time being, we just consider two players: player 1 and player 2

* Sequential decision processes

> State : (t : Nat) -> Type

|Ctrl1 t x| and |Ctrl2 t x| are the controls available to player 1 and
 to player 2 at decision step |t| and in state |x|:

> Ctrl1 : (t : Nat) -> (x : State t) -> Type

> Ctrl2 : (t : Nat) -> (x : State t) -> Type

> Ctrls : (t : Nat) -> (x : State t) -> Type
> Ctrls t x = (Ctrl1 t x, Ctrl2 t x)

> M : Type -> Type

> nexts : (t : Nat) -> (x : State t) -> (ys : Ctrls t x) -> M (State (S t))

> fmap  :  {A, B : Type} ->
>          (A -> B) -> M A -> M B
> postulate functorSpec1  :  fmap . id = id
> postulate functorSpec2  :  {A, B, C : Type} -> {f : B -> C} -> {g : A -> B} ->
>                            fmap (f . g) = (fmap f) . (fmap g)

* Sequential decision problems

> Val : Type

> Vals : Type
> Vals = (Val, Val)

> reward : (t : Nat) -> (x : State t) ->  (ys : Ctrls t x) -> (x' : State (S t)) -> Vals

> plus : Val -> Val -> Val

> zero : Val

> LTE : Val -> Val -> Type

> meas1 : M Val -> Val

> meas2 : M Val -> Val

* Solving sequential decision problems

> Elem     : {A : Type} -> A -> M A -> Type
> NotEmpty : {A : Type} -> M A -> Type
> All      : {A : Type} -> (P : A -> Type) -> M A -> Type
> tagElem  : {A : Type} -> (ma : M A) -> M (Sigma A (\ a => a `Elem` ma))

> allElemSpec0                 :  {A : Type} -> {P : A -> Type} ->
>                                 (a : A) -> (ma : M A) -> All P ma -> a `Elem` ma -> P a

> postulate elemNotEmptySpec0  :  {A : Type} ->
>                                 (a : A) -> (ma : M A) -> a `Elem` ma -> NotEmpty ma

> postulate elemNotEmptySpec1  :  {A : Type} ->
>                                 (ma : M A) -> NotEmpty ma -> Sigma A (\ a => a `Elem` ma)

> postulate tagElemSpec        :  {A : Type} -> (ma : M A) -> fmap outl (tagElem ma) = ma

* Viability

> Viable : {t : Nat} -> (n : Nat) -> State t -> Type

> postulate viableSpec0 : {t : Nat} ->
>                         (x : State t) -> Viable Z x

> Good : (t : Nat) -> (x : State t) -> (n : Nat) -> (ys : Ctrls t x) -> Type
> Good t x n ys = (NotEmpty (nexts t x ys), All (Viable {t = S t} n) (nexts t x ys))

> GoodCtrls : (t : Nat) -> (x : State t) -> (n : Nat) -> Type
> GoodCtrls t x n = Sigma (Ctrls t x) (Good t x n)

> viableSpec1 : {t : Nat} -> {n : Nat} ->
>               (x : State t) -> Viable (S n) x -> GoodCtrls t x n

> postulate viableSpec2 : {t : Nat} -> {n : Nat} ->
>                         (x : State t) -> GoodCtrls t x n -> Viable (S n) x

> ctrls : {t, n : Nat} -> {x : State t} -> GoodCtrls t x n -> Ctrls t x
> ctrls (MkSigma ys _) = ys

> allViable : {t, n : Nat} -> {x : State t} ->
>             (gys : GoodCtrls t x n) ->
>             All (Viable {t = S t} n) (nexts t x (ctrls gys))
> allViable (MkSigma _ p) = snd p

* Reachability

> Reachable : {t' : Nat} -> State t' -> Type

> postulate reachableSpec0 : (x : State Z) -> Reachable x

> reachableSpec1  :  {t : Nat} ->
>                    (x : State t) ->
>                    Reachable x ->
>                    (ys : Ctrls t x) ->
>                    All Reachable (nexts t x ys)

> {-

> Pred : {t : Nat} -> State t -> State (S t) -> Type
> Pred {t} x x'  =  Sigma (Ctrl t x) (\ y => x' `Elem` nexts t x y)

> ReachablePred : {t : Nat} -> State t -> State (S t) -> Type
> ReachablePred x x'  = (Reachable x, x `Pred` x')

> postulate reachableSpec2  :  {t : Nat} -> (x' : State (S t)) -> Reachable x' -> Sigma (State t) (\ x => x `ReachablePred` x')

* Policies and policy sequences

Policies are functions that associate to every state |x| at decision
step |t| which is reachable and viable for |S m| steps (from which |S
m| more decision steps are doable) a good control:

> Policy : (t : Nat) -> (n : Nat) -> Type
> Policy t Z      =  Unit
> Policy t (S m)  =  (x : State t) -> Reachable x -> Viable (S m) x -> GoodCtrl t x m

A policy sequence for making |n| decision steps starting from some
(reachable, viable for |n| steps) state at decision step |t| is a list
of policies of length |n|, one for each decision step:

> data PolicySeq : (t : Nat) -> (n : Nat) -> Type where
>   Nil   :  {t : Nat} ->
>            PolicySeq t Z
>   (::)  :  {t, n : Nat} ->
>            Policy t (S n) -> PolicySeq (S t) n -> PolicySeq t (S n)

Fold for |PolicySeq|:

> foldPolicySeq : {X : (t : Nat) -> (n : Nat) -> Type} ->
>                 ((t : Nat) -> X t Z) ->
>                 ((t : Nat) -> (n : Nat) -> Policy t (S n) -> X (S t) n -> X t (S n)) ->
>                 (t : Nat) -> (n : Nat) -> PolicySeq t n -> X t n
> foldPolicySeq e f t Z Nil = e t
> foldPolicySeq e f t (S n) (p :: ps) = f t n p (foldPolicySeq e f (S t) n ps)

* The value of policy sequences

As mentioned before, the idea of a decision problem is that the
decision maker seeks controls that maximize the sum of the rewards
obtained in a decision process.

Thus, in order to meaningfully define a notion of optimality for policy
sequences, we have to compute the value (in terms of possible sums of
rewards) of making decisions according to a given policy sequence.

Specifically, for a policy sequence |ps : PolicySeq tn| and a reachable,
viable for |n| steps state |x : State t|, we have to compute the value
(in terms of possible sums of rewards) of making |n| decision steps with
|ps| starting from |x|:

<   val : {t : Nat} -> {n : Nat} ->
<         (x : State t) -> Reachable x -> Viable n x -> PolicySeq t n -> Val

The case |n = Z| (and |ps = Nil|) is trivial. Here, we are not making
any decision step. Thus, we do not collect any reward and the value is
just zero:

<   val {t} {n = Z} x r v ps = zero

If |n = S m| and |ps| consists of a policy |p : Policy t (S m)| and of a
policy sequence |ps : PolicySeq (S t) m|, things are more complicated:

<   val {t} {n = S m} x r v (p :: ps) = ?

Here, we first have to compute the rewards obtained by selecting the
control |y = ctrl (p x r v)| in the first decision step. We get one
possible reward for each state in |nexts t x y|. Thus, if |x' `Elem`
(nexts t x y)|, its corresponding reward is

< reward t x y x'

Next, we have to add to all these rewards (one for every |x'|) the
values of making |m| further decision steps with |ps| starting from
|x'|:

< val x' r' v' ps

To do so, we have to provide reachability and viability evidences |r'|
and |v'| for |x'|. Finally, we have to reduce all possible values to a
single aggregated value. Here is where the measure |meas| comes into
place.

It is useful to introduce the notion of those possible states that can
be obtained by selecting the control |y : Ctrl t x| in |x : State t|:

> PossibleNextState  :  {t : Nat} ->
>                       (x  : State t) -> (y : Ctrl t x) -> Type
> PossibleNextState {t} x y = Sigma (State (S t)) (\ x' => x' `Elem` (nexts t x y))

With this notion in place and assuming

<   val : {t : Nat} -> {n : Nat} ->
<         (x : State t) -> Reachable x -> Viable n x -> PolicySeq t n -> Val

to be available, we can implement

> mutual

>   sval  :  {t, m : Nat} ->
>            (x  : State t) -> (r  : Reachable x) -> (v  : Viable (S m) x) ->
>            (gy  : GoodCtrl t x m) -> (ps : PolicySeq (S t) m) ->
>            PossibleNextState x (ctrl gy) -> Val
>   sval {t} {m} x r v gy ps (MkSigma x' x'emx') = reward t x y x' `plus` val x' r' v' ps where
>     y   : Ctrl t x
>     y   = ctrl gy
>     mx' : M (State (S t))
>     mx' = nexts t x y
>     ar' : All Reachable mx'
>     ar' = reachableSpec1 x r y
>     av' : All (Viable m) mx'
>     av' = allViable gy
>     r'  : Reachable x'
>     r'  = allElemSpec0 x' mx' ar' x'emx'
>     v'  : Viable m x'
>     v'  = allElemSpec0 x' mx' av' x'emx'

And finally

>   val  :  {t, n : Nat} ->
>           (x : State t) -> (r : Reachable x) -> (v : Viable n x) -> PolicySeq t n -> Val
>   val {t} {n = Z} x r v ps = zero
>   val {t} {n = S m} x r v (p :: ps) = meas (fmap (sval x r v gy ps) (tagElem mx')) where
>     gy   :  GoodCtrl t x m
>     gy   =  p x r v
>     y    :  Ctrl t x
>     y    =  ctrl gy
>     mx'  :  M (State (S t))
>     mx'  =  nexts t x y

* Optimality of policy sequences

With a function for computing the value (in terms of "possible" sums
of rewards) of making |n| decision steps with a policy sequence
starting from some specific state, we can formalise what it means for
one such sequence to be optimal.

Informally, we say that a policy sequence |ps| for making |n| decision
steps starting from states in |State t| which are reachable and viable
for |n| steps is optimal if its value is at least as good as the value
of any other policy sequence for making |n| decision steps starting
from states in |State t|. Formally:

> |||
> OptPolicySeq  :  {t, n : Nat} ->
>                  PolicySeq t n -> Type
>
> {-
> OptPolicySeq {t} {n} ps  =  (ps' : PolicySeq t n) ->
>                             (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                             val x r v ps' `LTE` val x r v ps
> -}
> OptPolicySeq {t} {n} ps  =  (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                             (ps' : PolicySeq t n) ->
>                             val x r v ps' `LTE` val x r v ps

Notice that the above notion of optimality is very strong. It entails a
quantification over all (viable and reachable) states of |Stete t| to
which the first policy of the sequence can be applied.

Thus, if we manage to compute an optimal policy sequence of length |n|
for making |n| decisions starting from step |t|, we have the guarantee
that, no matter which state we will happen to be at decision step |t|,
there is no better way to make |n| decision steps than that encoded by
our policy.

In other words, we have |n| rules for making ``best'' (in terms of
``possible'' sums of rewards) decisions.

Thus, an obvious question is whether it is at all possible to compute
sequences of policies that are optimal in the above sense. As we shall
see in |FullTheory|, if the assumptions put forward here and in
|ExtraAssumptions| are fulfilled, the answer to this question is
positive.

In the rest of this file, we implement a generic backwards induction
algorithm for computing optimal policy sequences for an arbitrary number
of decision steps.

* Optimal extensions of policy sequences

The computation at the core of backwards induction is the computation
of an optimal extension of a policy sequence. An extension of a policy
sequence for making |m| decision steps starting from states at
decision step |S t| is just a policy for taking decisions at step |t|,
that is, a policy that is put *in front* of the list of policies that
will deal with any resulting future states.

Informally, a policy |p| is an optimal extension of a policy sequence
|ps| if there is no better way than |p :: ps| to make |S m| decision
steps at step |t|. Formally:

> |||
> OptExt  :  {t, m : Nat} ->
>            PolicySeq (S t) m -> Policy t (S m) -> Type
> {-
> OptExt {t} {m} ps p  =  (p' : Policy t (S m)) ->
>                         (x : State t) -> (r : Reachable x) -> (v : Viable (S m) x) ->
>                         val x r v (p' :: ps) `LTE` val x r v (p :: ps)
> -}
> OptExt {t} {m} ps p  =  (x : State t) -> (r : Reachable x) -> (v : Viable (S m) x) ->
>                         (p' : Policy t (S m)) ->
>                         val x r v (p' :: ps) `LTE` val x r v (p :: ps)

The idea behind the notion of optimal extension is that if |p| is an
optimal extension of |ps| and |ps| is optimal, then |p :: ps| is
optimal.  This is Bellman's principle of optimality [1] which we will
implement in |FullTheory|.

The strong requirement of optimality implies that |p| is optimal for
every state, therefore, the control obtained by applying |p| to a given
state |x| must be optimal, i.e., it must maximise the function |cval x r
v ps|:

> |||
> cval  :  {t, n : Nat} ->
>          (x : State t) -> (r : Reachable x) -> (v : Viable (S n) x) ->
>          (ps : PolicySeq (S t) n) -> GoodCtrl t x n -> Val
> cval {t} x r v ps gy = meas (fmap (sval x r v gy ps) (tagElem mx')) where
>   y    :  Ctrl t x
>   y    =  ctrl gy
>   mx'  :  M (State (S t))
>   mx'  =  nexts t x y

Let |cvalargmax| be a function that delivers the control that leads to
the maximal value of |cval x r v ps|:

> cvalargmax  :  {t, n : Nat} ->
>                (x  : State t) -> (r : Reachable x) -> (v : Viable (S n) x) ->
>                (ps : PolicySeq (S t) n) -> GoodCtrl t x n

The controls obtained by maximising |cval x r v ps| for each of the
states |x : State t| will deliver a policy which is an optimal extension
of |ps|.  Thus, the problem of maximising |val| has been reduced to the
maximisation of |cval| for the states at time |t|.  Therefore, the
function that computes this optimal extension is:

> |||
> optExt  :  {t, n : Nat} ->
>            PolicySeq (S t) n -> Policy t (S n)
> optExt {t} {n} ps = p where
>   p : Policy t (S n)
>   p x r v = cvalargmax x r v ps

* Generic machine checkable backwards induction

If |LTE| is reflexive, it is straightforward to show that empty policy
sequences (that is, sequences for performing zero decision steps) are
optimal. Therefore, we have a starting point for the recursive process
of extending optimal policy sequences. This suggests the following
implementations of backwards induction:

> backwardsInduction : (t : Nat) -> (n : Nat) -> PolicySeq t n
> backwardsInduction t  Z     =  Nil
> backwardsInduction t (S n)  =  optExt ps :: ps where
>   ps : PolicySeq (S t) n
>   ps = backwardsInduction (S t) n

> {-

> take : {t : Nat} -> (n : Nat) -> (m : Nat) -> PolicySeq t n -> Sigma Nat (\ m' => PolicySeq t m')
> take {t}    Z   m          ps  = MkSigma Z Nil
> take {t} (S n)  Z          ps  = MkSigma Z Nil
> take {t} (S n) (S m) (p :: ps) = MkSigma (S m') (p' :: ps') where
>   mps' : Sigma Nat (\ m' => PolicySeq (S t) m')
>   mps' = take n m ps
>   m'   : Nat
>   m'   = outl mps'
>   ps'  : PolicySeq (S t) m'
>   ps'  = outr mps'
>   p'   : Policy t (S m')
>   p'   = ?this_might_work -- p

> bi : (t : Nat) -> (n : Nat) -> (m : Nat) -> PolicySeq t n
> bi t  Z    m  =  Nil
> bi t (S n) m  =  p :: ps where
>   ps        : PolicySeq (S t) n
>   ps        = bi (S t) n m
>   m'        : Nat
>   m'        = outl (take n m ps)
>   ps'       : PolicySeq (S t) m'
>   ps'       = outr (take n m ps)
>   p         : Policy t (S n)
>   p         = ?this_will_not_work -- optExt ps'

> -}

This file contains all the *computational* elements that the user must
specify in order to be able to run |backwardsInduction|.  The results
are going to fulfill the condition of optimality only if several
assumptions hold, some of which we have introduced only informally (and
others not at all).  For example, we have not formalised the requirement
that |cvalargmax| delivers an optimal control, or that |LTE| is
reflexive (and we haven't even mentioned its transitivity, which is also
required).

These additional assumptions are formulated in the file |FullTheory|,
where we also implement a machine-checked proof of the correctness of
|backwardsInduction| under these assumptions.

This separation has been introduced in order to enable users that do not
want to deal with formal proofs to use the framework for computing
optimal policies.  Of course, the optimality of the results will, in
this case, not be machine-checked.

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
{-
foo
bar
baz
-}
module Main

main : IO ()
main = do
  putStrLn . pack $ ['f', 'o', 'o']
  for_ (words "bar baz ") putStrLn

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Core.Options.Log

import Data.List
import Data.List1
import Data.Maybe
import Data.StringMap
import Data.StringTrie
import Data.Strings
import Data.These
import Text.PrettyPrint.Prettyprinter

%default total

||| Log levels are characterised by two things:
||| * a dot-separated path of ever finer topics of interest e.g. scope.let
||| * a natural number corresponding to the verbosity level e.g. 5
|||
||| If the user asks for some logs by writing
|||
|||     %log scope 5
|||
||| they will get all of the logs whose path starts with `scope` and whose
||| verbosity level is less or equal to `5`. By combining different logging
||| directives, users can request information about everything (with a low
||| level of details) and at the same time focus on a particular subsystem
||| they want to get a lot of information about. For instance:
|||
|||     %log 1
|||     %log scope.let 10
|||
||| will deliver basic information about the various phases the compiler goes
||| through and deliver a lot of information about scope-checking let binders.

----------------------------------------------------------------------------------
-- INDIVIDUAL LOG LEVEL

||| An individual log level is a pair of a list of non-empty strings and a number.
||| We keep the representation opaque to force users to call the smart constructor
export
data LogLevel : Type where
  MkLogLevel : List String -> Nat -> LogLevel

||| If we have already processed the input string into (maybe) a non-empty list of
||| non-empty topics we can safely make a `LogLevel`.
export
mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel
mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n

||| The smart constructor makes sure that the empty string is mapped to the empty
||| list. This bypasses the fact that the function `split` returns a non-empty
||| list no matter what.
export
mkLogLevel : String -> Nat -> LogLevel
mkLogLevel "" = mkLogLevel' Nothing
mkLogLevel ps = mkLogLevel' (Just (split (== '.') ps))

||| The unsafe constructor should only be used in places where the topic has already
||| been appropriately processed.
export
unsafeMkLogLevel : List String -> Nat -> LogLevel
unsafeMkLogLevel = MkLogLevel

||| The topics attached to a `LogLevel` can be reconstructed from the list of strings.
export
topics : LogLevel -> List String
topics (MkLogLevel ps _) = ps

||| The verbosity is provided by the natural number
export
verbosity : LogLevel -> Nat
verbosity (MkLogLevel _ n) = n

||| When writing generic functions we sometimes want to keep the same topic but
||| change the verbosity.
export
withVerbosity : Nat -> LogLevel -> LogLevel
withVerbosity n (MkLogLevel ps _) = MkLogLevel ps n

||| A log level is show as `P.Q.R:N` where `P`, `Q` and `R` are topics and `N` is
||| a verbosity level. If there are no topics then we simply print `N`.
export
Show LogLevel where

  show (MkLogLevel ps n) = case ps of
    [] => show n
    _  => fastAppend (intersperse "." ps) ++ ":" ++ show n

export
Pretty LogLevel where

  pretty = pretty . show

export
parseLogLevel : String -> Maybe LogLevel
parseLogLevel str = do
  (c, n) <- case split (== ':') str of
             n ::: [] => pure (MkLogLevel [], n)
             ps ::: [n] => pure (mkLogLevel ps, n)
             _ => Nothing
  lvl <- parsePositive n
  pure $ c (fromInteger lvl)

----------------------------------------------------------------------------------
-- COLLECTION OF LOG LEVELS

||| We store the requested log levels in a Trie which makes it easy to check
||| whether a given log level is captured by the user's request for information.
export
LogLevels : Type
LogLevels = StringTrie Nat

||| By default we log everything but with very few details (i.e. next to nothing)
export
defaultLogLevel : LogLevels
defaultLogLevel = singleton [] 0

export
insertLogLevel : LogLevel -> LogLevels -> LogLevels
insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))

----------------------------------------------------------------------------------
-- CHECKING WHETHER TO LOG

||| We keep a log if there is a prefix of its path associated to a larger number
||| in the LogLevels.
export
keepLog : LogLevel -> LogLevels -> Bool
keepLog (MkLogLevel path n) levels = go path levels where

  go : List String -> StringTrie Nat -> Bool
  go path (MkStringTrie current) = here || there where

    here : Bool
    here = case fromThis current of
      Nothing => False
      Just m  => n <= m

    there : Bool
    there = case path of
      [] => False
      (p :: rest) => fromMaybe False $ do
        assoc <- fromThat current
        next  <- lookup p assoc
        pure $ go rest next


text:
module App

import VNode
import Render
import Diff

record App msg model where
  constructor MkApp
  view : model -> DOM V
  update : model -> msg -> model
  state : model

-- We'll want to abstract this into an interface, but for now let's just make it work in the
-- simple case

create : AnyPtr -> App msg model -> IO (DOM L)
create root app = do
  let vdom = app.view app.state
  render root vdom

doUpdate : AnyPtr -> DOM L -> model -> msg -> App msg model -> IO (DOM L)
doUpdate root old model msg app = do
  let newModel = app.update model msg
  let newVDOM = app.view newModel
  diff

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder