text:
module Lambdapants.Command

import Effect.Baseline
import Effect.State
import Effect.StdIO
import Effect.System
import Effects
import Lambdapants.Environment
import Lambdapants.Term
import Lambdapants.Term.Nats
import Lambdapants.Term.Reduction

public export
data Command =
  ||| `:help` `:h` `:?`    -- Show help
  Help |
  ||| `:env`               -- List environment
  Env |
  ||| `:aq`                -- Test two terms for alpha equality
  AlphaEq Term Term |
  ||| `:eq`                -- Compare the normal forms (if reduction
  |||                         terminates) of two terms.
  Eq Term Term |
  ||| `:reduce` `:r`       -- Apply one beta reduction step to the expression
  |||                         to derive a new term
  Reduce Term |
  -- TODO: Step |                   -- Repeated reduction
  ||| `:whatis` `:w`       -- Look up a term (up to alpha equivalence) in the
  |||                         environment)
  Whatis Term |
  ||| `:set` `:s`          -- Add a term to the environment
  Set String Term |
  ||| `:unset` `:u`        -- Remove a term from the environment
  Unset String |
  ||| `:limit`             -- Set maximum number of reductions
  Limit Nat |
  ||| `:eval`              -- Set/show evaluation strategy
  Eval (Maybe Strategy) |
  ||| '!'                  -- Run shell command
  Shell String |
  ||| `:quit` `:q`         -- Exit
  Quit

export
Eq Command where
  (AlphaEq s t) == (AlphaEq u v) = s == u && t == v
  (Eq s t)      == (Eq u v)      = s == u && t == v
  (Reduce s)    == (Reduce t)    = s == t
  (Whatis s)    == (Whatis t)    = s == t
  (Set s t)     == (Set u v)     = s == u && t == v
  (Unset s)     == (Unset t)     = s == t
  (Limit m)     == (Limit n)     = m == n
  (Eval s)      == (Eval t)      = s == t
  (Shell a)     == (Shell b)     = a == b
  Env           == Env           = True
  Help          == Help          = True
  Quit          == Quit          = True
  _             == _             = False

public export
record Repl where
  constructor ReplState
  dict  : Environment
  limit : Nat
  eval  : Strategy

mapE_ : (a -> EffM m b xs (\underscore => xs))
     -> List a
     -> EffM m () xs (\underscore => xs)
mapE_ f xs = mapE f xs *> pure ()

highlight : String -> String
highlight s = "\ESC[0;92m" ++ s ++ "\ESC[0m"

deleteTerm : String -> Eff () [STATE Repl, STDIO, BASELINE]
deleteTerm symbol = do
  let xs = dict !get
  if isJust (lookup symbol xs)
     then do update (set_dict (filter ((/= symbol) . fst) xs))
             putStrLn (highlight "Deleted!")
     else putStrLn "There is no term with that name."

updateEnv : String -> Term -> Eff () [STATE Repl, STDIO]
updateEnv symbol term = do
  update (set_dict ((symbol, term) :: dict !get))
  putStrLn (highlight "Saved!")

saveTerm : String -> Term -> Eff () [STATE Repl, STDIO, BASELINE]
saveTerm symbol term = save (closed term (dict !get)) where
  save : Term -> Eff () [STATE Repl, STDIO, BASELINE]
  save closed_term =
    case lookup symbol (dict !get) of
         Nothing => updateEnv symbol closed_term
         Just this =>
           if this `alphaEq` closed_term
              then putStrLn "This term already exists."
              else do
                what <- baseline "Replace existing entry (y[es] to confirm)? "
                when (Just "y" == what || Just "yes" == what)
                  (updateEnv symbol closed_term)

updateLimit : Nat -> Eff () [STATE Repl]
updateLimit lim = update (set_limit lim)

setEvalOrder : Maybe Strategy -> Eff () [STDIO, STATE Repl]
setEvalOrder strategy = do
  set strategy
  putStrLn ("Evaluation is set to " ++ toLower (show (eval !get)) ++ " order.")
where
  set : Maybe Strategy -> Eff () [STATE Repl]
  set Nothing  = pure ()
  set (Just s) = update (set_eval s)

printEnv : List (String, Term) -> Eff () [STDIO]
printEnv xs = mapE_ (\s => entry s) xs where
  spaces : Nat -> String
  spaces n = pack (replicate n ' ')
  colWidth : Nat
  colWidth = 2 + foldr (max . Prelude.Strings.length . fst) 0 xs
  entry : (String, Term) -> Eff () [STDIO]
  entry (symb, term) = do
    putStr symb
    putStr (spaces (colWidth `minus` length symb))
    putStrLn (pretty term)

termWhatis : Term -> Eff () [STDIO, STATE Repl]
termWhatis term =
  case map fst (filter (alphaEq term . snd) (dict !get)) of
         [] => case decoded term of
                    Just nat => putStrLn (show nat)
                    Nothing  => putStrLn "This term is not defined."
         xs => mapE_ (\s => putStrLn s) xs

reduce : Term -> Eff () [STDIO, STATE Repl]
reduce term = do
  let term' = closed term (dict !get)
  putStrLn (pretty term')
  putStrLn ("\x21d2 " ++ pretty (evaluate (eval !get) term'))

evalAndCompare : Term -> Term -> Eff () [STDIO, STATE Repl]
evalAndCompare s t = do
  putStrLn "TODO"
  pure ()

printHelp : Eff () [STDIO]
printHelp = putStrLn "\
  \Command     Arguments            Description                                                                           \n\
  \-----------------------------------------------------------------------------------------------------------------------\n\
  \<expr>                           Evaluate an expression of the form <term> := <var> | \\<var>.<term> | (<term> <term>).\n\
  \:!                               Run a shell command.                                                                  \n\
  \:h :? :help                      Show this help.                                                                       \n\
  \:env                             List environment.                                                                     \n\
  \:aq         <term> <term>        Test two terms for alpha equality.                                                    \n\
  \:eq         <term> <term>        Compare the normal forms (if reduction terminates) of two terms.                      \n\
  \:r :reduce  <term>               Apply one beta reduction step to the expression.                                      \n\
  \:w :whatis  <term>               Look up a term (up to alpha equivalence) in the environment.                          \n\
  \:s :set     <symbol> <term>      Add a term to the environment.                                                        \n\
  \:u :unset   <symbol>             Remove a term from the environment.                                                   \n\
  \:limit      <number>             Set maximum number of reductions.                                                     \n\
  \:eval       [normal|applicative] Set or show evaluation strategy.                                                      \n\
  \:q :quit                         Exit"

export
execute : Command -> Eff () [STATE Repl, STDIO, SYSTEM, BASELINE]
execute Help          = printHelp
execute Env           = printEnv (dict !get)
execute (AlphaEq a b) = putStrLn (toLower (show (alphaEq a b)))
execute (Eq a b)      = evalAndCompare a b
execute (Reduce t)    = reduce t
execute (Whatis t)    = termWhatis t
execute (Set s t)     = saveTerm s t *> addDictEntry s
execute (Unset term)  = deleteTerm term
execute (Limit max)   = updateLimit max
execute (Shell cmd)   = system cmd *> pure ()
execute (Eval arg)    = setEvalOrder arg
execute _ = pure ()


text:
-- Enumerated type example.
data Direction = North
               | East
               | South
               | West

turnClockwise : Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North

ext: idr


text:
module DataStructures

%access public export
data BBinOp = And | Or
Show BBinOp where
  show And = "AND"
  show Or = "OR"

data RBinOp = Greater | Less
Show RBinOp where
  show Greater = "GREATER"
  show Less = "LESS"

data ABinOp = Add
            | Subtract
            | Multiply
            | Divide
Show ABinOp where
  show Add = "ADD"
  show Subtract = "SUBTRACT"
  show Multiply = "MULTIPLY"
  show Divide = "DIVIDE"

data AExpr = Var String
           | IntConst Integer
           | Neg AExpr
           | ABinary ABinOp AExpr AExpr
Show AExpr where
  show (Var a) = "(VAR " ++ a ++ ")"
  show (IntConst i) = "(INTCONST " ++ (show i) ++ ")"
  show (Neg a) = "(NEG " ++ (show a) ++ ")"
  show (ABinary o l r) = "(ABINARY (" ++ (show o) ++ " " ++ (show l) ++ (show r) ++ "))"

data BExpr = BoolConst Bool
           | BNot BExpr
           | BBinary BBinOp BExpr BExpr
           | RBinary RBinOp AExpr AExpr
Show BExpr where
  show (BoolConst b) = "(BOOLCONST " ++ (show b) ++ ")"
  show (BNot b) = "(BNOT " ++ (show b) ++ ")"
  show (BBinary o l r) = "(BBINARY (" ++ (show o) ++ " " ++ (show l) ++ (show r) ++ "))"
  show (RBinary o l r) = "(RBINARY (" ++ (show o) ++ " " ++ (show l) ++ (show r) ++ "))"

data Stmt = Seq (List Stmt)
          | Assign AExpr AExpr
          | If BExpr Stmt Stmt
          | While BExpr Stmt
          | Skip
Show Stmt where
  show (Seq x) = concatMap (\s => show s ++ "\n") x ++ ")"
  show (Assign s a) = "(ASSIGN " ++ (show s) ++ (show a) ++ ")"
  show (If b t f) = "(IF " ++ (show b) ++ (show t) ++ (show f) ++ ")"
  show (While b s) = "(While " ++ (show b) ++ (show s) ++ ")"
  show Skip = "(SKIP" ++ ")"

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
||| Compiling of expressions
|||
||| Experssions track their type along with the generated Rust code.
||| Because Rust is a statically typeed language and some primitive types in
||| Idris map nicely to Rust it makes sense to keep this information around to
||| only inseert the casts that are necessary.
module Idris2Rust.Expr

import Compiler.Common
import Compiler.CompileExpr

import Core.Context

import Data.List
import Data.Maybe
import Data.Vect

rustKeywords : List String
rustKeywords = [
    "as", "break", "const", "continue",
    "crate", "else", "enum", "extern",
    "false", "fn", "for", "if",
    "impl", "in", "let", "loop",
    "match", "mod", "move", "mut",
    "pub", "ref", "return", "self",
    "Self", "static", "struct", "super",
    "trait", "true", "type", "unsafe",
    "use", "where", "while", "async",
    "await", "dyn", "abstract", "become",
    "box", "do", "final", "macro",
    "override", "priv", "typeof", "unsized",
    "virtual", "yield", "try", "union"
]


text:
module Records

import Data.Vect

%default total

record Person where
  constructor MkPerson
  firstName, middleName, lastName : String
  age : Int

bob : Person
bob = MkPerson "Bob" "H" "Fox" 42

dave : Person
dave = MkPerson "Dave" "H." "Chad" 49

record Class where
  constructor ClassInfo
  students : Vect n Person
  className : String

emptyClass : Class
emptyClass = ClassInfo [] ""

addStudent : Person -> Class -> Class
addStudent p c = record { students = p :: students c } c

addStudent' : Person -> Class -> Class
addStudent' p c = record { students $= (p ::) } c

changeClassName : String -> Class -> Class
changeClassName n c = record { className = n } c

record Employee where
  constructor MkEmployee
  id : Int
  person : Person

record Department where
  constructor MkDepartment
  id : Int
  manager : Employee
  employees : Vect n Employee

sales : Department
sales = MkDepartment 1 (MkEmployee 100 dave) [MkEmployee 1 (MkPerson "Susan" "L." "Weinberger" 23), MkEmployee 2 bob]

-- dependent records

record Prod a b where
  constructor Times
  fst : a
  snd : b

record SizedClass (size : Nat) where
  constructor SizedClassInfo
  students : Vect size Person
  className : String

addSizedStudent : Person -> SizedClass n -> SizedClass (S n)
addSizedStudent p c = record { students $= (p ::) } c

record Dpair a (p : a -> Type) where
  constructor MkDPair
  fst : a
  snd : p fst

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Main

import Effects

import Effect.SDL
import Effect.State
import Effect.StdIO

import Rnd
import Starfield
import Gamestate

data Frames : Type where -- empty type, just for labelling

-------
-- SDL effect is parameterised by an underyling 'surface' resource which
-- only exists when initialised.

-- The program supports SDL, carries state, and supports random number
-- generation and console I/O

Prog : Type -> Type -> Type
Prog i t = { [SDL i,
              Frames ::: STATE Integer,
              Gamestate ::: STATE Gamestate,
              Starfield ::: STATE (List (Int, Int)),
              RND,
              STDIO] } Eff IO t

-- Convenient shorthand for initialised SDL
Running : Type -> Type
Running t = Prog SDLSurface t

-------
emain : Prog () ()
emain = do initialise 640 480
           initStarfield [] 200
           eventLoop
           quit
  where
        draw : Running ()
        draw = with Effects do
                  rectangle black 0 0 640 480
                  drawStarfield !(Starfield :- get)
                  gs <- Gamestate :- get
                  drawBullets (bullets gs)
                  drawBombs (bombs gs)
                  drawAliens (aliens gs)
                  p <- getPos
                  let (x, y) = p
                  rectangle blue (x-10) (y-10) 20 20
                  rectangle blue (x-1) (y-20) 2 10
                  flip

        -- update the world state by moving the ellipse to a new position
        -- and scrolling the starfield. Also print the number of frames
        -- drawn so far every so often.

        updateWorld : Running ()
        updateWorld = do f <- Frames :- get
                         Frames :- put (f + 1)
                         when ((f `mod` 100) == 0) (putStrLn (show f))
                         updateStarfield
                         updateGamestate

        -------
        -- Event loop simply has to draw the current state, update the
        -- state according to how the ellipse is moving, then process
        -- any incoming events

        eventLoop : Running ()
        eventLoop = do draw
                       updateWorld
                       when !(process !poll) eventLoop

main : IO ()
main = runInit [(), Frames := 0,
                Gamestate := initState,
                Starfield := List.Nil,
                1234567890,
                ()] emain

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
import Data.Nat
import Data.Vect

myReverse1 : Vect n a -> Vect n a
myReverse1 [] = []
myReverse1 {n = S k} (x :: xs)
        = let result = myReverse1 xs ++ [x] in
              rewrite plusCommutative 1 k in result

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


text:
module Language.LSP.CodeAction.MakeCase

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.MakeClause
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.CaseSplit

currentLineRange : Int -> String -> Range
currentLineRange i origLine =
  MkRange (MkPosition i 0)
          (MkPosition i (cast $ Prelude.String.length origLine))

isHole : Defs -> Name -> Core Bool
isHole defs n
    = do Just def <- lookupCtxtExact n (gamma defs)
              | Nothing => do pure False
         case definition def of
              Hole _ _ => pure True
              _ => pure False

export
handleMakeCase : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => CodeActionParams -> Core (Maybe CodeAction)
handleMakeCase params = do
  logI MakeCase "Checking for \{show params.textDocument.uri} at \{show params.range}"
  withSingleLine MakeCase params (pure Nothing) $ \line => do
    withSingleCache MakeCase params MakeCase $ do

      meta <- get MD
      let col = params.range.start.character
      let Just (loc, name) = findPointInTreeLoc (line, col) (nameLocMap meta)
        | Nothing => do logD MakeCase "No name found at \{show line}:\{show col}}"
                        pure Nothing

      logD MakeCase "Found name \{show name}"
      defs <- get Ctxt
      True <- isHole defs name -- should only work on holes
        | _ => do logD MakeCase "\{show name} is not a metavariable"
                  pure Nothing

      Just original <- getSourceLine (line + 1)
        | Nothing => do logE MakeCase "Error while fetching the referenced line"
                        pure Nothing
      let name' = dropAllNS name
      let newText = makeCase False name' original -- TODO sort out brackets arg
      let rng = currentLineRange line original
      let edit = MkTextEdit rng newText

      let docURI = params.textDocument.uri
      let workspaceEdit = MkWorkspaceEdit
            { changes           = Just (singleton docURI [edit])
            , documentChanges   = Nothing
            , changeAnnotations = Nothing
            }
      let codeAction = MkCodeAction
            { title       = "Make case for hole ?\{show name'}"
            , kind        = Just RefactorRewrite
            , diagnostics = Just []
            , isPreferred = Just False -- not a quickfix
            , disabled    = Nothing
            , edit        = Just workspaceEdit
            , command     = Nothing
            , data_       = Nothing
            }
      pure $ Just (cast loc, codeAction)


text:
module Main
import Cgi
import Effects
import Session
import SessionUtils

incrementAndGetCount : SessionData -> Eff IO [SESSION (SessionRes SessionInitialised)] Int
incrementAndGetCount sd = case lookup "counter" sd of
                            Just (SInt c) => do updateSession $ updateVar "counter" (SInt (c + 1)) sd
                                                return (c + 1)
                            _ => do updateSession $ updateVar "counter" (SInt 1) sd -- Start a new counter
                                    return 1

-- TODO: Update CGIProg to the EffM definition instead of the Eff definition
useSession : Maybe (SessionID, SessionData) -> EffM IO [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionInitialised)]
                                          [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionUninitialised)]
                                          ()
useSession (Just (si, sd)) = do count <- lift' (incrementAndGetCount sd)
                                lift' (output $ "You have visited this page " ++ (show count) ++ " time(s)!")
                                lift' writeSessionToDB
                                Effects.pure ()
useSession Nothing = do output "There was a problem retrieving your session."
                        -- Delete the session for good measure
                        -- whoops, haven't written this yet
                        discardSession
                        Effects.pure ()

doCGIStuff : Eff IO [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionUninitialised)] ()
doCGIStuff = do lift' (output "Hello, world!\n")
                session <- getOrCreateSession
                useSession session

main : IO ()
main = do
  runCGI [initCGIState, InvalidSession] doCGIStuff
  pure ()

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Main

import Data.String
import Data.Vect
import Data.List
import CFFI
import Control.ST
import Control.ST.ImplicitCall
import Control.ST.File

%link C "pq-idr.o"
%include C  "pq-idr.h"
%lib C "pq"

%dynamic "pq-idr.so"

data ResultPtr = MkResultPtr Ptr

data DbPtr = MkDbPtr Ptr

dbPtrInjective : {x, y: Ptr} -> (MkDbPtr x = MkDbPtr y) -> x = y
dbPtrInjective Refl = Refl

implementation DecEq DbPtr where
  decEq (MkDbPtr ptr1) (MkDbPtr ptr2) with (decEq ptr1 ptr2)
    | Yes p = Yes $ cong p
    | No p  = No $ \h : MkDbPtr ptr1 = MkDbPtr ptr2 => p $ dbPtrInjective h

record DbConn where
  constructor MkDbConn
  user, password, hostname : String
  port : Int
  dbname : String

breakMaybe : (Char -> Bool) -> String -> Maybe (String, String)
breakMaybe f s =
  let (before, after) = break f s
  in case before of
      "" => Nothing
      _  => Just (before, after)

psqlUriPrefix : String
psqlUriPrefix = "postgresql://"

serializeDbConn : DbConn -> String
serializeDbConn (MkDbConn usr pass host p db) =
  psqlUriPrefix ++ usr ++ ":" ++ pass ++ "@" ++ host ++ ":" ++ show p ++ "/" ++ db

data Query = Commit | Rollback | Prepare String | Stop

implementation Show Query where
  show Commit   = "COMMIT PREPARED 'foobar';"
  show Rollback = "ROLLBACK PREPARED 'foobar';"
  show (Prepare q) = "BEGIN; PREPARE TRANSACTION 'foobar';\n" ++ q

pqConnectDb : DbConn -> IO DbPtr
pqConnectDb dbConn = do
    ptr <- foreign FFI_C "connect" (String -> IO Ptr) (serializeDbConn dbConn)
    pure $ MkDbPtr ptr

pqErrorMessage : DbPtr -> IO String
pqErrorMessage (MkDbPtr p) = foreign FFI_C "dbErrorMessage" (Ptr -> IO String) p

pqResultErrorMessage : ResultPtr -> IO String
pqResultErrorMessage (MkResultPtr p) = foreign FFI_C "resultErrorMessage" (Ptr -> IO String) p

-- Closes the connection to the server. Also frees memory used by the PGconn object.
pqFinish : DbPtr -> IO ()
pqFinish (MkDbPtr p) = foreign FFI_C "dbClose" (Ptr -> IO ()) p

pqExec : DbPtr -> Query -> IO ResultPtr
pqExec (MkDbPtr p) q = do
  ptr <- foreign FFI_C "exec" (Ptr -> String -> IO Ptr) p (show q)
  pure $ (MkResultPtr ptr)

pqClear : ResultPtr -> IO ()
pqClear (MkResultPtr p) = foreign FFI_C "clearResult" (Ptr -> IO ()) p

data ConnectionStatus
  = Ok
  | Bad
  | Started
  | Made
  | AwaitingResponse
  | AuthOk
  | Setenv
  | SslStartup
  | Needed
  | OtherConn Int

data DbError : Type where
  ConnErr : ConnectionStatus -> String -> DbError
  FileErr : FileError -> DbError
  UriParseError : String -> DbError

parseDbConn : String -> Maybe DbConn
parseDbConn str =
  if isPrefixOf psqlUriPrefix str
  then do
    let rest = pack $ drop (length psqlUriPrefix) (unpack str)
    (usr, rest) <- breakMaybe (== ':') rest
    (pass, rest) <- breakMaybe (== '@') (strTail rest)
    (host, rest) <- breakMaybe (== ':') (strTail rest)
    (portStr, rest) <- breakMaybe (== '/') (strTail rest)
    port <- parsePositive portStr
    let db = strTail rest
    pure $ MkDbConn usr pass host port db
  else Nothing

parseDbConn' : String -> Either DbError DbConn
parseDbConn' str = case parseDbConn str of
                        Just c  => Right c
                        Nothing => Left (UriParseError str)

connErrNotFileErr : (ConnErr x y = FileErr z) -> Void
connErrNotFileErr Refl impossible

connErrNotUriParseError : (ConnErr x y = UriParseError s) -> Void
connErrNotUriParseError Refl impossible

fileErrNotUriParseError : (FileErr f = UriParseError s) -> Void
fileErrNotUriParseError Refl impossible

mkConnectionStatus: Int -> ConnectionStatus
mkConnectionStatus i = case i of
  0 => Ok
  1 => Bad
  2 => Started
  3 => Made
  4 => AwaitingResponse
  5 => AuthOk
  6 => Setenv
  7 => SslStartup
  8 => Needed
  _ => OtherConn i

pqStatus : DbPtr -> IO ConnectionStatus
pqStatus (MkDbPtr p) = do
  statusCode <- foreign FFI_C "PQstatus" (Ptr -> IO Int) p
  pure $ mkConnectionStatus statusCode

getConnection : DbConn -> IO (Either DbError DbPtr)
getConnection dbConn = do
  dbPtr <- pqConnectDb dbConn
  connStatus <- pqStatus dbPtr
  case connStatus of
    Ok => pure (Right dbPtr)
    otherStatus => do
      msg <- pqErrorMessage dbPtr
      pqFinish dbPtr
      pure $ Left (ConnErr otherStatus msg)

Show ConnectionStatus where
  show x = case x of
    Ok               => "OK"
    Bad              => "BAD"
    Started          => "STARTED"
    Made             => "MADE"
    AwaitingResponse => "AWAITING_RESPONSE"
    AuthOk           => "AUTH_OK"
    Setenv           => "SETENV"
    SslStartup       => "SSL_STARTUP"
    Needed           => "NEEDED"
    OtherConn i      => "OTHER " ++ show i

Show DbError where
  show (ConnErr status msg) = show status ++ ": " ++ msg
  show (FileErr err) = show err
  show (UriParseError input) = "Unable to parse `" ++ input ++ "` as uri."

data ResultStatus
  = EmptyQuery
  | CommandOk
  | TuplesOk
  | CopyOut
  | CopyIn
  | BadResponse
  | NonFatalError
  | FatalError
  | CopyBoth
  | SingleTuple
  | OtherRes Int

data ResultError = MkResultError ResultStatus String

mkResultStatus : Int -> ResultStatus
mkResultStatus i = case i of
  0 => EmptyQuery
  1 => CommandOk
  2 => TuplesOk
  3 => CopyOut
  4 => CopyIn
  5 => BadResponse
  6 => NonFatalError
  7 => CopyBoth
  8 => SingleTuple
  i => OtherRes i

pqResultStatus : ResultPtr -> IO ResultStatus
pqResultStatus (MkResultPtr p) = do
  statusCode <- foreign FFI_C "PQresultStatus" (Ptr -> IO Int) p
  pure $ mkResultStatus statusCode

Show ResultStatus where
  show x = case x of
    EmptyQuery    => "EmptyQuery"
    CommandOk     => "CommandOk"
    TuplesOk      => "TuplesOk "
    CopyOut       => "CopyOut"
    CopyIn        => "CopyIn"
    BadResponse   => "BadResponse"
    NonFatalError => "NonFatalError"
    FatalError    => "FatalError"
    CopyBoth      => "CopyBoth"
    SingleTuple   => "SingleTuple"
    OtherRes i       => "Unknown exit code: " ++ show i

implementation Show ResultError where
  show (MkResultError code msg) = "ResultError: Code " ++ show code ++ ": Msg:" ++ msg

execQuery : DbPtr -> Query -> IO (Either ResultError ResultStatus)
execQuery dbPtr query = do
  resPtr <- pqExec dbPtr query
  resultStatus <- pqResultStatus resPtr
  errMsg <- pqResultErrorMessage resPtr
  pqClear resPtr
  case errMsg of
    "" => pure $ Right resultStatus
    msg => pure $ Left (MkResultError resultStatus msg)

interface Database (m : Type -> Type) where
  Db : Nat -> Type

  connect : DbConn -> ST m (Either DbError Var) [addIfRight (Db 1)]
  disconnect : (db : Var) -> ST m () [remove db (Db 1)]
  query : (db : Var) -> Query -> ST m (Either ResultError ResultStatus) [db ::: Db 1]

  connectMany : Vect n DbConn -> ST m (Either (List DbError) Var) [addIfRight (Db n)]
  disconnectMany : (db: Var) -> ST m () [remove db (Db n)]
  queryMany : (db : Var) -> Query -> ST m (Either (List ResultError) (Vect n ResultStatus)) [db ::: Db n]

getRight : Either a b -> Maybe b
getRight e = case e of
                  Right x => Just x
                  Left _  => Nothing

aggErrors : Vect n (Either a b) -> Either (List a, List b) (Vect n b)
aggErrors {n} eithers = let (MkDPair len vec) = mapMaybe getRight eithers
                        in case exactLength n vec of
                                Just v  => Right v
                                Nothing => Left (partitionEithers $ toList eithers)

implementation Database IO where
  Db n = State (Vect n DbPtr)

  connect dbConn = do
    eitherPtr <- lift $ getConnection dbConn
    case eitherPtr of
      Right ptr => do var <- new (ptr :: Vect.Nil)
                      pure $ Right var
      Left err => pure $ Left err

  disconnect db = do
    dbPtr <- read db
    lift $ pqFinish (head dbPtr)
    delete db

  query db query = do
    dbPtr <- read db
    lift $ execQuery (head dbPtr) query

  connectMany conns = do
    eithers <- lift $ traverse getConnection conns
    case aggErrors eithers of
         Right vec => do var <- new vec
                         pure $ Right var
         Left (errs, ptrs) => do lift $ traverse pqFinish ptrs
                                 pure (Left errs)

  disconnectMany db = do
    dbPtrs <- read db
    lift $ traverse pqFinish dbPtrs
    delete db

  queryMany db query = do
    dbPtrs <- read db
    eithers <- lift $ traverse (\dbPtr => execQuery dbPtr query) dbPtrs
    case aggErrors eithers of
         Right vec      => pure $ Right vec
         Left (errs, _) => pure $ Left errs

------- End Database Module -------
------- Start Two PC Module -------

data CoordState = Init | Abort | Persist

interface Coord (m : Type -> Type) where
  MkCoord : Nat -> CoordState -> Type

  connectPeers : Vect n DbConn -> ST m (Either (List DbError) Var) [addIfRight (MkCoord n Init)]
  disconnectPeers : (coord : Var) -> ST m () [remove coord (MkCoord n Init)]

  prepare : (coord : Var) -> Query -> ST m (Either (List ResultError) ()) [coord ::: MkCoord n Init :->
                                                                            (\res => MkCoord n (case res of
                                                                                Right _ => Persist
                                                                                Left  _ => Abort))]

  persist : ConsoleIO m => (coord : Var) -> ST m () [coord ::: MkCoord n Persist :-> MkCoord n Init]

  abort : ConsoleIO m => (coord : Var) -> ST m () [coord ::: MkCoord n Abort :-> MkCoord n Init]

Database m => Coord m where
  MkCoord n x = Db n {m}

  connectPeers connVec = do
    Right db <- connectMany connVec | Left errs => pure (Left errs)
    pure (Right db)

  disconnectPeers coord = do
    disconnectMany coord

  prepare coord query = do
    Right _ <- queryMany coord query | Left errs => pure (Left errs)
    pure (Right ())

  persist coord = do
    status <- queryMany coord Commit
    case status of
       Right _   => putStrLn "Persist succeeded."
       Left errs => putStrLn ("Persist failed:\n" ++ unlines (map show errs))

  abort coord = do
    status <- queryMany coord Rollback
    case status of
       Right _   => putStrLn "Abort succeeded."
       Left errs => putStrLn ("Abort failed:\n" ++ unlines (map show errs))

transact : (ConsoleIO m, Coord m) => (coord : Var) -> Query -> ST m () [coord ::: MkCoord n {m} Init]
transact coord query = do
  status <- prepare coord query
  case status of
       Right _   => do putStrLn "Prepare succeeded. Commiting transaction..."
                       persist coord
       Left errs => do putStrLn ("Prepare failed:\n" ++ unlines (map show errs))
                       abort coord

getString : ConsoleIO m => ST m String []
getString = go "" where
  go str = do
    line <- getStr
    case line of
      "" => pure str
      ln => go $ str ++ ln

getQuery : ConsoleIO m => ST m Query []
getQuery = do
  maybeQuery <- getString
  case maybeQuery of
       "END" => pure Stop
       query => pure (Prepare query)

transactQueries : (ConsoleIO m, Coord m) => (coord : Var) -> ST m () [coord ::: MkCoord n {m} Init]
transactQueries coord = do
  putStrLn "Input query or END to Stop:"
  maybeQuery <- getQuery
  case maybeQuery of
       Stop => pure ()
       query => do transact coord query
                   transactQueries coord

session : (ConsoleIO m, Coord m) => Vect n DbConn -> ST m () []
session conns = do
  Right coord <- connectPeers conns | Left errs => putStrLn ("Connection failed:\n" ++ unlines (map show errs))
  putStrLn "Connected to peers."
  transactQueries coord
  disconnectPeers coord

fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListOfLength n xs with (decEq (length xs) n)
  fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
  fromListOfLength n xs | (No _) = Nothing

parseConnectionFile : File m => String -> ST m (Either DbError (List DbConn)) []
parseConnectionFile path = do
  Right str <- readFile path | Left err => pure (Left $ FileErr err)
  let eitherConns = traverse parseDbConn' (map trim $ lines str)
  case eitherConns of
    Left err => pure (Left err)
    Right conns => pure (Right conns)

main : IO ()
main = do
  args <- getArgs
  case fromListOfLength 2 args of
    Nothing => putStrLn $ "Bad Usage: " ++ unwords args ++ "\nUsage: ./<executable> path-to-config"
    Just vec => do
      Right connLs <- run (parseConnectionFile (last vec)) | Left err => putStrLn (show err)
      case fromListOfLength (length connLs) connLs of
           Nothing => ?nothing
           Just vec => run (session vec)

max_stars_repo_name: davlum/two-pc-idr

max_issues_repo_name: davlum/two-pc-idr

max_forks_repo_name: davlum/two-pc-idr


text:
module Idris.Package.Init

import Core.FC
import Core.Name.Namespace

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

import Idris.Package.Types
import System.Directory

import Libraries.Utils.Path
import Libraries.System.Directory.Tree
import Libraries.Text.PrettyPrint.Prettyprinter

%default total

isModuleIdent : String -> Bool
isModuleIdent str = case unpack str of
  [] => False
  cs@(hd :: _) => isUpper hd && all isAlphaNum cs

packageTree : (root : Path) -> IO (Tree root)
packageTree root = filter validFile validDirectory <$> explore root where

  validFile : {root : _} -> FileName root -> Bool
  validFile f
    = let (fname, fext) = splitFileName (fileName f) in
      isModuleIdent fname && elem fext ["idr", "lidr"]

  validDirectory : {root : _} -> FileName root -> Bool
  validDirectory = isModuleIdent . fileName

covering
findModules : (start : Maybe String) -> IO (List (ModuleIdent, String))
findModules start = do
  let prfx = fromMaybe "" start
  Just dir <- maybe currentDir (pure . Just) start
    | Nothing => pure []
  let root = parse dir
  tree <- packageTree root
  mods <- go [] [([], (root ** pure tree))]
  pure (sortBy (\ a, b => compare (snd a) (snd b)) mods)

  where

    go : List (ModuleIdent, String) ->
         List (List String, (root : Path ** IO (Tree root))) ->
         IO (List (ModuleIdent, String))
    go acc [] = pure acc
    go acc ((path, (root ** iot)) :: iots) = do
      t <- liftIO iot
      let mods = flip map t.files $ \ entry =>
                   let fname = fst (splitFileName (fileName entry)) in
                   let mod = unsafeFoldModuleIdent (fname :: path) in
                   let fp  = toFilePath entry in
                   (mod, fp)
      let dirs = flip map t.subTrees $ \ (dir ** iot) =>
                   (fileName dir :: path, (_ ** iot))
      go (mods ++ acc) (dirs ++ iots)

export
covering
interactive : IO PkgDesc
interactive = do
  pname    <- putStr "Package name: " *> getLine
  pauthors <- putStr "Package authors: " *> getLine
  poptions <- putStr "Package options: " *> getLine
  psource  <- putStr "Source directory: " *> getLine
  let sourcedir = mstring psource
  modules  <- findModules sourcedir
  let pkg : PkgDesc =
        { authors   := mstring pauthors
        , options   := (emptyFC,) <$> mstring poptions
        , modules   := modules
        , sourcedir := sourcedir
        } (initPkgDesc (fromMaybe "project" (mstring pname)))
  pure pkg

  where

    mstring : String -> Maybe String
    mstring str = case trim str of
      "" => Nothing
      str => Just str


text:
module Data.List.Alternating

import Data.Bifoldable
import Data.List

infixl 5 +>
infixr 5 <+

%default total

mutual
    namespace Odd
        ||| Non-empty list, starting and ending with an a, where adjacent elements alternate
        ||| between types a and b.
        ||| We can think of this type as:
        ||| - A fence, with the `a`s as fence-posts, and the `b`s as panels.
        ||| - A non-empty list of `a`s, separated by `b`s
        ||| - A list of `b`s, separated by, and surrounded by, `a`s
        ||| - The free extension of a monoid `a`, with variables in `b`
        public export
        data Odd a b = (::) a (Even b a)

    namespace Even
        ||| A list, starting with an a, and ending with a b; where adjacent elements
        ||| alternate between types a and b.
        ||| Equivalent to List (a, b)
        public export
        data Even a b = Nil | (::) a (Odd b a)

%name Odd xs, ys, zs
%name Even xs, ys, zs

mutual
    public export
    Eq a => Eq b => Eq (Odd a b) where
        x :: xs == y :: ys = x == y && assert_total (xs == ys)

    public export
    Eq a => Eq b => Eq (Even a b) where
        [] == [] = True
        x :: xs == y :: ys = x == y && xs == ys
        _ == _ = False

mutual
    public export
    Ord a => Ord b => Ord (Odd a b) where
        compare (x :: xs) (y ::ys)
           = case compare x y of
                  EQ => assert_total (compare xs ys)
                  c => c

    public export
    Ord a => Ord b => Ord (Even a b) where
        compare [] [] = EQ
        compare [] (x :: xs) = LT
        compare (x :: xs) [] = GT
        compare (x :: xs) (y ::ys)
           = case compare x y of
                  EQ => compare xs ys
                  c => c

mutual
    public export
    Bifunctor Odd where
        bimap f g (x :: xs) = (f x) :: assert_total (bimap g f xs)

    public export
    Bifunctor Even where
        bimap f g [] = []
        bimap f g (x :: xs) = (f x) :: (bimap g f xs)

mutual
    public export
    Bifoldable Odd where
        bifoldr f g acc (x :: xs) = f x (assert_total $ bifoldr g f acc xs)

        bifoldl f g acc (x :: xs) = assert_total $ bifoldl g f (f acc x) xs

    public export
    Bifoldable Even where
        bifoldr f g acc [] = acc
        bifoldr f g acc (x :: xs) = f x (bifoldr g f acc xs)

        bifoldl f g acc [] = acc
        bifoldl f g acc (x :: xs) = bifoldl g f (f acc x) xs

mutual
    public export
    Bitraversable Odd where
        bitraverse f g (x :: xs) = [| f x :: assert_total (bitraverse g f xs) |]

    public export
    Bitraversable Even where
        bitraverse f g [] = [| [] |]
        bitraverse f g (x :: xs) = [| f x :: bitraverse g f xs |]

namespace Snd
    public export
    Functor (Odd a) where
        map = mapSnd

namespace Fst
    public export
    [FstFunctor] Functor (\a => Odd a b) where
        map = mapFst

mutual
    namespace Odd
        public export
        (++) : Odd a b -> Odd b a -> Even a b
        (x :: xs) ++ ys = x :: xs ++ ys

    namespace EvenOdd
        public export
        (++) : Even a b -> Odd a b -> Odd a b
        [] ++ ys = ys
        (x :: xs) ++ ys = x :: xs ++ ys

mutual
    namespace Even
        public export
        (++) : Even a b -> Even a b -> Even a b
        [] ++ ys = ys
        (x :: xs) ++ ys = x :: xs ++ ys

    namespace OddEven
        public export
        (++) : Odd a b -> Even b a -> Odd a b
        (x :: xs) ++ ys = x :: xs ++ ys

||| The semigroup structure induced by treating Odd as the free extension of a
||| monoid `a`, with variables in `b`
public export
Semigroup a => Semigroup (Odd a b) where
    [x] <+> (y :: ys) = (x <+> y) :: ys
    (x :: y :: xs) <+> ys = x :: y :: xs <+> ys

namespace Odd
    public export
    (+>) : Semigroup a => Odd a b -> a -> Odd a b
    [x] +> z = [x <+> z]
    x :: y :: xs +> z = x :: y :: (xs +> z)

    public export
    (<+) : Semigroup a => a -> Odd a b -> Odd a b
    x <+ y :: ys = (x <+> y) :: ys

public export
Semigroup (Even a b) where
    (<+>) = (++)

public export
Monoid a => Monoid (Odd a b) where
    neutral = [neutral]

public export
Monoid (Even a b) where
    neutral = []

public export
Foldable (Odd a) where
    foldr = bifoldr (flip const)
    foldl = bifoldl const

public export
singleton : a -> Odd a b
singleton x = [x]

namespace Snd
    public export
    Monoid a => Applicative (Odd a) where
        pure x = [neutral, x, neutral]
        fs <*> xs = biconcatMap singleton (flip map xs) fs

public export
flatten : Odd (Odd a b) b -> Odd a b
flatten [x] = x
flatten (x :: y :: xs) = x ++ (y :: flatten xs)

namespace Fst
    public export
    [FstApplicative] Applicative (\a => Odd a b) using FstFunctor where
        pure x = [x]
        fs <*> xs = flatten $ bimap (flip mapFst xs) id fs

public export
Monoid a => Alternative (Odd a) where
    empty = [neutral]
    xs <|> ys = xs <+> ys

namespace Snd
    public export
    [SndMonad] Monoid a => Monad (Odd a) where
        x >>= f = assert_total $ biconcatMap singleton f x

    public export
    (>>=) : Monoid a => Odd a b -> (b -> Odd a c) -> Odd a c
    (>>=) = (>>=) @{SndMonad}

namespace Fst
    public export
    [FstMonad] Monad (\a => Odd a b) using FstApplicative where
        x >>= f = flatten $ mapFst f x
        join = flatten

    public export
    (>>=) : Odd a c -> (a -> Odd b c) -> Odd b c
    (>>=) = (>>=) @{FstMonad}

public export
Traversable (Odd a) where
    traverse = bitraverse pure

mutual
    namespace Odd
        public export
        odds : Odd a b -> List a
        odds (x :: xs) = x :: evens xs

    namespace Even
        public export
        evens : Even a b -> List b
        evens [] = []
        evens (x :: xs) = odds xs

mutual
    namespace Odd
        public export
        evens : Odd a b -> List b
        evens (x :: xs) = odds xs

    namespace Even
        public export
        odds : Even a b -> List a
        odds [] = []
        odds (x :: xs) = x :: evens xs

mutual
    namespace Odd
        public export
        forget : Odd a a -> List a
        forget (x :: xs) = x :: forget xs

    namespace Even
        public export
        forget : Even a a -> List a
        forget [] = []
        forget (x :: xs) = x :: forget xs

export
Show a => Show b => Show (Odd a b) where
    show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"

export
Show a => Show b => Show (Even a b) where
    show xs = "[\{concat $ intersperse ", " $ forget $ bimap show show xs}]"


text:
module Sorting

import NatOrder
import Decidable.Order

%default total

data SortedList : Type
data ListLTE : Nat -> SortedList -> Type

data SortedList : Type where
    Nil : SortedList
    Cons : (x : Nat) -> (rest : SortedList) -> ListLTE x rest -> SortedList

data ListLTE : Nat -> SortedList -> Type where
    NilLTE : (x : Nat) -> ListLTE x Nil
    ConsLTE : (b : Nat) -> (x : Nat) -> (rest : SortedList) ->
                LTE b x -> (x_lte_rest : ListLTE x rest) ->
                ListLTE b (Cons x rest x_lte_rest)

-- data Elem : Nat -> List Nat -> Type where
--     Here : Elem x xs
--     There : (later : Elem x rest) -> Elem x (y :: rest)
--
-- data ElemS : Nat -> SortedList -> Type where
--     HereS : ElemS x (Cons x rest x_lte_rest)
--     ThereS : (later : ElemS x rest) -> ElemS x (Cons y rest y_lte_rest)

data ElemCount : Nat -> List Nat -> Nat -> Type where
    NilNone : ElemCount e [] 0
    HereAnother : ElemCount x rest c -> ElemCount x (x :: rest) (S c)
    ThereSome : ElemCount e rest c -> Not (e = x) -> ElemCount e (x :: rest) c

data ElemCountS : Nat -> SortedList -> Nat -> Type where
    NilNoneS : ElemCountS e Nil 0
    HereAnotherS : ElemCountS x rest c -> ElemCountS x (Cons x rest x_lte_rest) (S c)
    ThereSomeS : ElemCountS e rest c -> Not (e = x) -> ElemCountS e  (Cons x rest x_lte_rest) c

-- data SameElemCounts : List Nat -> SortedList -> Type where
--     AllSame : (xs : List Nat) -> (xs' : SortedList) ->
--         ((e : Nat) -> (c : Nat) -> (ElemCount e xs c -> ElemCountS e xs' c, ElemCountS e xs' c -> ElemCount e xs c))
--         -> SameElemCounts xs xs'

SameElemCounts : List Nat -> SortedList -> Type
SameElemCounts xs xs' = (e : Nat) -> (c : Nat) -> ElemCount e xs c -> ElemCountS e xs' c

SameElemCountsBack : List Nat -> SortedList -> Type
SameElemCountsBack xs xs' = (e : Nat) -> (c : Nat) -> ElemCountS e xs' c -> ElemCount e xs c

equivMetrics : (xs : List Nat) -> (xs' : SortedList) -> SameElemCounts xs xs' -> SameElemCountsBack xs xs'

-- [1, 2, 3, 4]   vs  [1, 2, 3]
-- 4 ~> 1              -- 4 ~> 0

elemCountNil : ElemCount e [] c -> c = 0
elemCountNil NilNone = Refl

elemCountSNil : ElemCountS e Nil c -> c = 0
elemCountSNil NilNoneS = Refl

sameCountsNil : SameElemCounts [] Nil
sameCountsNil e c e_c =
        rewrite elemCountNil e_c in
        NilNoneS

listOrderTrans : LTE b1 b2 -> ListLTE b2 zs -> ListLTE b1 zs
listOrderTrans {zs = []} {b1} b1_lte_b2 (NilLTE b2) = NilLTE b1
listOrderTrans {b1} {b2} {zs = (Cons z rest z_lte_rest)} b1_lte_b2 (ConsLTE b2 z rest b2_lte_z z_lte_rest) =
    ConsLTE b1 z rest (lteTransitive b1_lte_b2 b2_lte_z) z_lte_rest

listConsLTE : (h_lte_rest : ListLTE h rest) -> ListLTE h (Cons h rest h_lte_rest)
listConsLTE {h} {rest} h_lte_rest = ConsLTE h h rest lteRefl h_lte_rest

listLTEZero : ListLTE 0 xs
listLTEZero {xs = []} = NilLTE 0
listLTEZero {xs = (Cons x rest x_lte_rest)} = ConsLTE 0 x rest LTEZero x_lte_rest

-- listUnConsLTE : ListLTE b (Cons h rest h_lte_rest) -> ListLTE b rest
-- listUnConsLTE (ConsLTE b h rest b_lte_h h_lte_rest) = listOrderTrans b_lte_h h_lte_rest

-- -- data MySortedList : Type where
-- --     Nil : MySortedList
-- --     Cons : (x : Nat) -> (h : Nat) -> (rest : SortedList) -> ()
--
-- data Sorted : List Nat -> Type where
--     NilSorted : Sorted Nil
--     ConsSorted : (x : Nat) -> (h : Nat) -> (rest : List Nat) -> Sorted (h :: rest) -> LTE x h -> Sorted (x :: h :: rest)
--
-- SortedList : Type
-- SortedList = (xs : List Nat ** Sorted xs)

-- lte_gt_trans : LTE small med -> Not (LTE med big) -> LTE

    -- ConsLTE : (b : Nat) -> (x : Nat) -> (rest : SortedList) ->
    --             LTE b x -> (x_lte_rest : ListLTE x rest) ->
    --             ListLTE b (Cons x rest x_lte_rest)

insertBounded : (xs : SortedList) -> (x : Nat) -> (b : Nat) -> LTE b x -> ListLTE b xs -> (res : SortedList ** ListLTE b res)
insertBounded [] x b b_lte_x b_lte_xs = (Cons x Nil (NilLTE x) ** ConsLTE b x Nil b_lte_x (NilLTE x))
insertBounded (Cons h rest h_lte_rest) x b b_lte_x (ConsLTE b h rest b_lte_h h_lte_rest) =
    case decideLTE x h of
        (Yes x_lte_h) =>
            let h_lte_hrest = listConsLTE h_lte_rest in
            let x_lte_hrest = listOrderTrans x_lte_h h_lte_hrest in
            let x_lte_xhrest = listConsLTE x_lte_hrest in
            let b_lte_xhrest = listOrderTrans b_lte_x x_lte_xhrest in
            (Cons x (Cons h rest h_lte_rest) x_lte_hrest ** b_lte_xhrest)
        (No x_gt_h) =>
            let h_lte_x : LTE h x = ?poiuqwer in
            let (ins ** h_lte_ins) = insertBounded rest x h h_lte_x h_lte_rest in
            let h_lte_hins = listConsLTE h_lte_ins in
            (Cons h ins h_lte_ins ** listOrderTrans b_lte_h h_lte_hins)

insert : (xs : SortedList) -> (x : Nat) -> SortedList
insert xs x = fst (insertBounded xs x 0 LTEZero listLTEZero)

insertionSort : (input : List Nat) -> (res : SortedList ** SameElemCounts input res)
insertionSort [] = (Nil ** ?ssameCountsNil)
insertionSort (x :: xs) =
    let (res_tail ** res_tail_prf) = insertionSort xs in
    (insert res_tail x ** ?poiweuwereyyyee)

half : Nat -> Nat
half Z = Z
half (S Z) = Z
half (S (S k)) = S (half k)

dropListLen : (xs : List Nat) -> (n : Nat) -> LTE n (length xs) -> length (drop n xs) = length xs - n
dropListLen xs Z n_lte_xs = sym $ minusZeroRight (length xs)
dropListLen [] (S k) n_lte_xs = absurd n_lte_xs
dropListLen (x :: xs) (S k) n_lte_xs = dropListLen xs k (fromLteSucc n_lte_xs)

dropListNonEmpty : (xs : List Nat) -> (n : Nat) -> LT n (length xs) -> NonEmpty (drop n xs)
dropListNonEmpty [] Z lt_prf = absurd lt_prf
dropListNonEmpty (x :: xs) Z lt_prf = IsNonEmpty
dropListNonEmpty [] (S k) lt_prf = absurd lt_prf
dropListNonEmpty (x :: xs) (S k) lt_prf = dropListNonEmpty xs k (fromLteSucc lt_prf)

halfLT : (x : Nat) -> Not (x = 0) -> LT (half x) x
halfLT Z y = void $ y $ Refl
halfLT (S Z) x_not_0 = LTESucc LTEZero
halfLT (S (S Z)) x_not_0 = LTESucc (LTESucc LTEZero)
halfLT (S (S (S k))) x_not_0 =
    let ih = halfLT (S k) SIsNotZ in
    let ih' = LTESucc ih in
    lteSuccRight ih'

nonEmptyLen : NonEmpty xs -> Not (length xs = 0)
nonEmptyLen {xs = (x :: ys)} IsNonEmpty = SIsNotZ

dropHalfNE : (xs : List Nat) -> NonEmpty xs -> NonEmpty (drop (half (length xs)) xs)
dropHalfNE xs ne =
    let lenNZ = nonEmptyLen ne in
    let halfLenLT = halfLT (length xs) lenNZ in
    dropListNonEmpty xs (half (length xs)) halfLenLT

splitList : (xs : List Nat) -> NonEmpty xs -> (List Nat, Nat, List Nat)
splitList xs nonempty =
    let n = half (length xs) in
    let left = take n xs in
    let right' = drop n xs in
    let ne : NonEmpty (right') = dropHalfNE xs nonempty in
    let middle = head {ok=ne} right' in
    let right = drop 1 right' in
    (left, middle, right)

headCombine : (xs : List Nat) -> (ne : NonEmpty xs) -> (head xs {ok=ne}) :: (drop 1 xs) = xs
headCombine [] IsNonEmpty impossible
headCombine (x :: xs) ne = Refl

takeCombine : (xs : List Nat) -> (n : Nat) -> take n xs ++ drop n xs = xs
takeCombine [] Z = Refl
takeCombine [] (S k) = Refl
takeCombine (x :: xs) Z = Refl
takeCombine (x :: xs) (S k) =
    rewrite takeCombine xs k in
    Refl

splitListCombine : (xs : List Nat) -> (ne : NonEmpty xs) ->
    let (left, middle, right) = splitList xs ne in left ++ (middle :: right) = xs
splitListCombine xs ne =
    let dropNonEmpty = dropHalfNE xs ne in
    rewrite headCombine (drop (half (length xs)) xs) dropNonEmpty in
    takeCombine xs (half (length xs))

binarySearch : (xs : SortedList) -> (y : Nat) -> Bool
-- binarySearch ([] ** xs_sorted) y = False

-- binarySearch (x :: rest ** xs_sorted) y =
--     let (left, middle, right) = splitList (x :: rest) IsNonEmpty in
--     case decideOrder x middle of
--         (LessThan x_lt_m) => ?iupoquwer_1
--         (Equal x_m) => ?iupoquwer_2
--         (GreaterThan x_gt_m) => ?iupoquwer_3

-- data BinaryElem : Nat -> List Nat -> Type where
--     ElemSingle : (y : Nat) -> BinaryElem y (left ++ (y :: right))
--     ElemLeft : (left : List Nat) -> (y : Nat) -> (right : List Nat) -> BinaryElem y left -> BinaryElem y (left ++ right)
--     ElemRight : (left : List Nat) -> (y : Nat) -> (right : List Nat) -> BinaryElem y left -> BinaryElem y (left ++ right)


text:
module Main

import Data.Vect

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

data UnknownVect : Type -> Type where
  UVect : (len : Nat) -> Vect len a -> UnknownVect a

readUVect : IO (UnknownVect String)
readUVect = do x <- getLine
               if (x == "")
                  then pure (UVect _ [])
                  else do UVect _ xs <- readUVect
                          pure (UVect _ (x :: xs))

printVect : Show a => UnknownVect a -> IO ()
printVect (UVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")")

readVect : IO (len ** Vect len String)
readVect = do x <- getLine
              if (x == "")
                 then pure (_ ** [])
                 else do (_ ** xs) <- readVect
                         pure (_ ** x :: xs)

zipInputs : IO ()
zipInputs = do putStrLn "Enter vector #1 (blank line to end): "
               (len1 ** vec1) <- readVect
               putStrLn "Enter vector #2 (blank line to end): "
               (len2 ** vec2) <- readVect
               case exactLength len1 vec2 of
                    Nothing => do putStrLn "Vector are of different length. Try again"
                                  zipInputs
                    Just vec2' => do printLn (zip vec1 vec2')
                                     zipInputs

main : IO ()
main = ?main_rhs

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Client.Action.Build

import Inigo.Async.Base
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.CodeGen
import Inigo.Package.Package
import Inigo.Async.Package
import Inigo.Paths

export
writeIPkgFile : Promise Package
writeIPkgFile =
  do
    pkg <- Inigo.Async.Package.currPackage
    -- TODO: Only build if not exists ?
    fs_writeFile inigoIPkgPath (Package.Package.generateIPkg True Nothing pkg)
    pure pkg

export
runBuild : CodeGen -> Promise ()
runBuild codeGen =
    ignore $ system "idris2" ["--build", inigoIPkgPath, "--cg", toString codeGen] Nothing False True

export
build : CodeGen -> Promise ()
build codeGen =
  do
    pkg <- writeIPkgFile
    runBuild codeGen

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

import public Eval
import public Lexer as L
import public Parser as P
import public Syntax

import Control.Monad.Identity
import Lightyear
import Lightyear.Strings

quit : String
quit = ":q"

prompt : String
prompt = "calc> "

welcome : String
welcome = "A simple arithmetic calculator. Use " ++ quit ++ " or ^D to quit."

farewell : String
farewell = "Goodbye."

implementation Layout (List Lexeme) where
  lineLengths xs = map (toIntNat . Prelude.Strings.length) . lines $ show xs

lex : String -> Either String (List Lexeme)
lex i = let Id r = execParserT L.lexer i in
  case r of
    Success "" lexemes => Right lexemes
    Success left _     => Left $ "Unexpected EOS while lexing: " ++ (show left)
    Failure es         => Left $ formatError i es

parse : List Lexeme -> Either String Expression
parse i = let Id r = execParserT P.toplevel i in
  case r of
    Success [] expr    => Right expr
    Success lexemes _  => Left ("Unexpected EOS while parsing: " ++ (show lexemes))
    Failure es         => Left $ formatError i es

evaluate : String -> Either String Integer
evaluate s = do
  lexemes <- lex s
  expression <- parse lexemes
  return (eval expression)

repl : IO ()
repl = do
  putStr prompt
  line <- getLine
  isEof <- fEOF stdin
  when (isEof) $ putStrLn ""
  when (isEof == False && line /= quit) (do
    when (line /= "") (
      case evaluate line of
        Left err => putStrLn $ "Error: " ++ err
        Right n  => putStrLn $ show n
      )
    repl
  )

main : IO ()
main = do
  putStrLn welcome
  repl
  putStrLn farewell

max_stars_repo_name: steshaw/idris-calc

max_issues_repo_name: steshaw/idris-calc

max_forks_repo_name: steshaw/idris-calc


text:
module Prelude.Num

import Builtin
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Ops

%default total

------------------------
-- NUMERIC INTERFACES --
------------------------

%integerLit fromInteger

||| The Num interface defines basic numerical arithmetic.
public export
interface Num ty where
  constructor MkNum
  (+) : ty -> ty -> ty
  (*) : ty -> ty -> ty
  ||| Conversion from Integer.
  fromInteger : Integer -> ty

%allow_overloads fromInteger

||| The `Neg` interface defines operations on numbers which can be negative.
public export
interface Num ty => Neg ty where
  constructor MkNeg
  ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
  negate : ty -> ty
  (-) : ty -> ty -> ty

||| Numbers for which the absolute value is defined should implement `Abs`.
public export
interface Num ty => Abs ty where
  constructor MkAbs
  ||| Absolute value.
  abs : ty -> ty

public export
interface Num ty => Fractional ty where
  constructor MkFractional
  partial
  (/) : ty -> ty -> ty
  partial
  recip : ty -> ty

  recip x = 1 / x

public export
interface Num ty => Integral ty where
  constructor MkIntegral
  partial
  div : ty -> ty -> ty
  partial
  mod : ty -> ty -> ty

----- Instances for primitives

-- Integer

%inline
public export
Num Integer where
  (+) = prim__add_Integer
  (*) = prim__mul_Integer
  fromInteger = id

%inline
public export
Neg Integer where
  negate x = prim__sub_Integer 0 x
  (-) = prim__sub_Integer

public export
Abs Integer where
  abs x = if x < 0 then -x else x

public export
Integral Integer where
  div x y
      = case y == 0 of
             False => prim__div_Integer x y
  mod x y
      = case y == 0 of
             False => prim__mod_Integer x y

-- This allows us to pick integer as a default at the end of elaboration if
-- all other possibilities fail. I don't plan to provide a nicer syntax for
-- this...
%defaulthint
%inline
public export
defaultInteger : Num Integer
defaultInteger = %search

-- Int

%inline
public export
Num Int where
  (+) = prim__add_Int
  (*) = prim__mul_Int
  fromInteger = prim__cast_IntegerInt

%inline
public export
Neg Int where
  negate x = prim__sub_Int 0 x
  (-) = prim__sub_Int

public export
Abs Int where
  abs x = if x < 0 then -x else x

public export
Integral Int where
  div x y
      = case y == 0 of
             False => prim__div_Int x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int x y

-- Int8

%inline
public export
Num Int8 where
  (+) = prim__add_Int8
  (*) = prim__mul_Int8
  fromInteger = prim__cast_IntegerInt8

%inline
public export
Neg Int8 where
  negate x = prim__sub_Int8 0 x
  (-) = prim__sub_Int8

public export
Abs Int8 where
  abs x = if x < 0 then -x else x

public export
Integral Int8 where
  div x y
      = case y == 0 of
             False => prim__div_Int8 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int8 x y

-- Int16

%inline
public export
Num Int16 where
  (+) = prim__add_Int16
  (*) = prim__mul_Int16
  fromInteger = prim__cast_IntegerInt16

%inline
public export
Neg Int16 where
  negate x = prim__sub_Int16 0 x
  (-) = prim__sub_Int16

public export
Abs Int16 where
  abs x = if x < 0 then -x else x

public export
Integral Int16 where
  div x y
      = case y == 0 of
             False => prim__div_Int16 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int16 x y

-- Int32

%inline
public export
Num Int32 where
  (+) = prim__add_Int32
  (*) = prim__mul_Int32
  fromInteger = prim__cast_IntegerInt32

%inline
public export
Neg Int32 where
  negate x = prim__sub_Int32 0 x
  (-) = prim__sub_Int32

public export
Abs Int32 where
  abs x = if x < 0 then -x else x

public export
Integral Int32 where
  div x y
      = case y == 0 of
             False => prim__div_Int32 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int32 x y

-- Int64

%inline
public export
Num Int64 where
  (+) = prim__add_Int64
  (*) = prim__mul_Int64
  fromInteger = prim__cast_IntegerInt64

%inline
public export
Neg Int64 where
  negate x = prim__sub_Int64 0 x
  (-) = prim__sub_Int64

public export
Abs Int64 where
  abs x = if x < 0 then -x else x

public export
Integral Int64 where
  div x y
      = case y == 0 of
             False => prim__div_Int64 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int64 x y

-- Bits8

%inline
public export
Num Bits8 where
  (+) = prim__add_Bits8
  (*) = prim__mul_Bits8
  fromInteger = prim__cast_IntegerBits8

%inline
public export
Neg Bits8 where
  negate x = prim__sub_Bits8 0 x
  (-) = prim__sub_Bits8

public export
Abs Bits8 where
  abs x = if x < 0 then -x else x

public export
Integral Bits8 where
  div x y
      = case y == 0 of
             False => prim__div_Bits8 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits8 x y

-- Bits16

%inline
public export
Num Bits16 where
  (+) = prim__add_Bits16
  (*) = prim__mul_Bits16
  fromInteger = prim__cast_IntegerBits16

%inline
public export
Neg Bits16 where
  negate x = prim__sub_Bits16 0 x
  (-) = prim__sub_Bits16

public export
Abs Bits16 where
  abs x = if x < 0 then -x else x

public export
Integral Bits16 where
  div x y
      = case y == 0 of
             False => prim__div_Bits16 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits16 x y

-- Bits32

%inline
public export
Num Bits32 where
  (+) = prim__add_Bits32
  (*) = prim__mul_Bits32
  fromInteger = prim__cast_IntegerBits32

%inline
public export
Neg Bits32 where
  negate x = prim__sub_Bits32 0 x
  (-) = prim__sub_Bits32

public export
Abs Bits32 where
  abs x = if x < 0 then -x else x

public export
Integral Bits32 where
  div x y
      = case y == 0 of
             False => prim__div_Bits32 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits32 x y

-- Bits64

%inline
public export
Num Bits64 where
  (+) = prim__add_Bits64
  (*) = prim__mul_Bits64
  fromInteger = prim__cast_IntegerBits64

%inline
public export
Neg Bits64 where
  negate x = prim__sub_Bits64 0 x
  (-) = prim__sub_Bits64

public export
Abs Bits64 where
  abs x = if x < 0 then -x else x

public export
Integral Bits64 where
  div x y
      = case y == 0 of
             False => prim__div_Bits64 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits64 x y

-- Double

public export
Num Double where
  (+) = prim__add_Double
  (*) = prim__mul_Double
  fromInteger = prim__cast_IntegerDouble

%inline
public export
Neg Double where
  negate x = prim__negate_Double x
  (-) = prim__sub_Double

public export
Abs Double where
  abs x = if x < 0 then -x else x

public export
Fractional Double where
  (/) = prim__div_Double


text:
module TTImp.ProcessDecls

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Options
import Core.Termination
import Core.UnifyState

import Parser.Source

import TTImp.BindImplicits
import TTImp.Elab.Check
import TTImp.Parser
import TTImp.ProcessBuiltin
import TTImp.ProcessData
import TTImp.ProcessDef
import TTImp.ProcessParams
import TTImp.ProcessRecord
import TTImp.ProcessRunElab
import TTImp.ProcessTransform
import TTImp.ProcessType
import TTImp.TTImp

import Data.List
import Data.Maybe
import Libraries.Data.NameMap

%default covering

-- Implements processDecl, declared in TTImp.Elab.Check
process : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          List ElabOpt ->
          NestedNames vars -> Env Term vars -> ImpDecl -> Core ()
process eopts nest env (IClaim fc rig vis opts ty)
    = processType eopts nest env fc rig vis opts ty
process eopts nest env (IData fc vis ddef)
    = processData eopts nest env fc vis ddef
process eopts nest env (IDef fc fname def)
    = processDef eopts nest env fc fname def
process eopts nest env (IParameters fc ps decls)
    = processParams nest env fc ps decls
process eopts nest env (IRecord fc ns vis rec)
    = processRecord eopts nest env ns vis rec
process eopts nest env (INamespace fc ns decls)
    = withExtendedNS ns $
         traverse_ (processDecl eopts nest env) decls
process eopts nest env (ITransform fc n lhs rhs)
    = processTransform eopts nest env fc n lhs rhs
process eopts nest env (IRunElabDecl fc tm)
    = processRunElab eopts nest env fc tm
process eopts nest env (IPragma _ act)
    = act nest env
process eopts nest env (ILog lvl)
    = addLogLevel (uncurry unsafeMkLogLevel <$> lvl)
process eopts nest env (IBuiltin fc type name)
    = processBuiltin nest env fc type name

TTImp.Elab.Check.processDecl = process

export
checkTotalityOK : {auto c : Ref Ctxt Defs} ->
                  Name -> Core (Maybe Error)
checkTotalityOK (NS _ (MN _ _)) = pure Nothing -- not interested in generated names
checkTotalityOK (NS _ (CaseBlock _ _)) = pure Nothing -- case blocks checked elsewhere
checkTotalityOK n
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure Nothing
         let fc = location gdef

         -- #524: need to check positivity even if we're not in a total context
         -- because a definition coming later may need to know it is positive
         case definition gdef of
           (TCon _ _ _ _ _ _ _ _) => ignore $ checkPositive fc n
           _ => pure ()

         -- Once that is done, we build up errors if necessary
         let treq = fromMaybe !getDefaultTotalityOption (findSetTotal (flags gdef))
         let tot = totality gdef
         log "totality" 3 $ show n ++ " must be: " ++ show treq
         case treq of
            PartialOK => pure Nothing
            CoveringOnly => checkCovering fc (isCovering tot)
            Total => checkTotality fc
  where
    checkCovering : FC -> Covering -> Core (Maybe Error)
    checkCovering fc IsCovering = pure Nothing
    checkCovering fc cov
        = pure (Just (NotCovering fc n cov))

    checkTotality : FC -> Core (Maybe Error)
    checkTotality fc
        = do ignore $ logTime ("+++ Checking Termination " ++ show n) (checkTotal fc n)
             -- ^ checked lazily, so better calculate here
             t <- getTotality fc n
             err <- checkCovering fc (isCovering t)
             maybe (case isTerminating t of
                         NotTerminating p => pure (Just (NotTotal fc n p))
                         _ => pure Nothing)
                   (pure . Just) err

-- Check totality of all the names added in the file, and return a list of
-- totality errors.
-- Do this at the end of processing a file (or a batch of definitions) since
-- they might be mutually dependent so we need all the definitions to be able
-- to check accurately.
export
getTotalityErrors : {auto c : Ref Ctxt Defs} ->
                    Core (List Error)
getTotalityErrors
    = do defs <- get Ctxt
         errs <- traverse checkTotalityOK (keys (toSave defs))
         pure (mapMaybe id errs)

export
processDecls : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool
processDecls nest env decls
    = do traverse_ (processDecl [] nest env) decls
         pure True -- TODO: False on error

processTTImpDecls : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    {auto m : Ref MD Metadata} ->
                    {auto u : Ref UST UState} ->
                    NestedNames vars -> Env Term vars -> List ImpDecl -> Core Bool
processTTImpDecls {vars} nest env decls
    = do traverse_ (\d => do d' <- bindNames d
                             processDecl [] nest env d') decls
         pure True -- TODO: False on error
  where
    bindConNames : ImpTy -> Core ImpTy
    bindConNames (MkImpTy fc nameFC n ty)
        = do ty' <- bindTypeNames fc [] vars ty
             pure (MkImpTy fc nameFC n ty')

    bindDataNames : ImpData -> Core ImpData
    bindDataNames (MkImpData fc n t opts cons)
        = do t' <- bindTypeNames fc [] vars t
             cons' <- traverse bindConNames cons
             pure (MkImpData fc n t' opts cons')
    bindDataNames (MkImpLater fc n t)
        = do t' <- bindTypeNames fc [] vars t
             pure (MkImpLater fc n t')

    -- bind implicits to make raw TTImp source a bit friendlier
    bindNames : ImpDecl -> Core ImpDecl
    bindNames (IClaim fc c vis opts (MkImpTy tfc nameFC n ty))
        = do ty' <- bindTypeNames fc [] vars ty
             pure (IClaim fc c vis opts (MkImpTy tfc nameFC n ty'))
    bindNames (IData fc vis d)
        = do d' <- bindDataNames d
             pure (IData fc vis d')
    bindNames d = pure d

export
processTTImpFile : {auto c : Ref Ctxt Defs} ->
                   {auto m : Ref MD Metadata} ->
                   {auto u : Ref UST UState} ->
                   String -> Core Bool
processTTImpFile fname
    = do modIdent <- ctxtPathToNS fname
         Right (ws, decor, tti) <- logTime "Parsing" $
                            coreLift $ parseFile fname (PhysicalIdrSrc modIdent)
                            (do decls <- prog (PhysicalIdrSrc modIdent)
                                eoi
                                pure decls)
               | Left err => do coreLift (putStrLn (show err))
                                pure False
         traverse_ recordWarning ws
         logTime "Elaboration" $
            catch (do ignore $ processTTImpDecls (MkNested []) [] tti
                      Nothing <- checkDelayedHoles
                          | Just err => throw err
                      pure True)
                  (\err => do coreLift_ (printLn err)
                              pure False)


text:
module Chapter3

%default total

describeList : List Int -> String
describeList [] = "Empty"
describeList (_ :: xs) = "Non-Empty with tail " ++ show xs

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

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

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Control.Optics.State

import Control.Monad.State
import Control.Optics.Pair
import public Control.Optics.Getter
import public Control.Optics.Lens
import public Control.Optics.Setter

export
use : MonadState s m => Getting a s a -> m a
use l = gets (view l)

export
data Zooming : (Type -> Type) -> Type -> Type -> Type where
  MkZooming : m (a, c) -> Zooming m c a

export
unZooming : Zooming m c a -> m (a, c)
unZooming (MkZooming x) = x

export
Monad m => Functor (Zooming m c) where
  map f (MkZooming m) = MkZooming (map (mapFst f) m)

export
zoom : (Monad m) => Simple (LensLike (Zooming m c)) s a -> StateT a m c -> StateT s m c
zoom l (ST m) = ST $ unZooming . applyMor (l (Mor (MkZooming . m)))

export
setting : MonadState s m => Setter s s a b -> b -> m ()
setting l b = modify (set l b)

export
modifying : MonadState s m => Setter s s a b -> (a -> b) -> m ()
modifying l f = modify (over l f)

infix 4 .=
export
(.=) : MonadState s m => Setter s s a b -> b -> m ()
(.=) = setting

infix 4 %=
export
(%=) : MonadState s m => Setter s s a b -> (a -> b) -> m ()
(%=) = modifying

infix 4 +=
export
(+=) : (MonadState s m, Num a) => Simple Setter s a -> a -> m ()
l += x = l %= (+ x)


text:
module Hedgehog.Internal.Config

import Generics.Derive
import System

%language ElabReflection

%default total

--------------------------------------------------------------------------------
--          Config
--------------------------------------------------------------------------------

||| Whether to render output using ANSI colors or not.
public export
data UseColor = DisableColor | EnableColor

%runElab derive "UseColor" [Generic,Meta,Show,Eq,Ord]

||| How verbose should the report output be.
public export
data Verbosity = Quiet | Normal

%runElab derive "Verbosity" [Generic,Meta,Show,Eq,Ord]

--------------------------------------------------------------------------------
--          Detecting Config Settings
--------------------------------------------------------------------------------

lookupBool : HasIO io => String -> io (Maybe Bool)
lookupBool key =
  getEnv key >>= \case Just "0"     => pure $ Just False
                       Just "no"    => pure $ Just False
                       Just "false" => pure $ Just False

                       Just "1"     => pure $ Just True
                       Just "yes"   => pure $ Just True
                       Just "true"  => pure $ Just True

                       _            => pure Nothing

export
detectColor : HasIO io => io UseColor
detectColor =
  do Just True <- lookupBool "HEDGEHOG_COLOR"
       | _ => pure DisableColor
     pure EnableColor

export
detectVerbosity : HasIO io => io Verbosity
detectVerbosity =
  do Just "0" <- getEnv "HEDGEHOG_VERBOSITY"
       | _ => pure Normal
     pure Quiet

export
resolveColor : HasIO io => Maybe UseColor -> io UseColor
resolveColor = maybe detectColor pure

export
resolveVerbosity : HasIO io => Maybe Verbosity -> io Verbosity
resolveVerbosity = maybe detectVerbosity pure