text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.Vect

data DataStore : Type where
  MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData s i) = s

items : (store : DataStore) -> Vect (size store) String
items (MkData s i) = i

addToStore : DataStore -> String -> DataStore
addToStore (MkData s i) n = MkData _ (addToData i)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [n]
    addToData (i :: is) = i :: addToData is

data Command = Add String
             | Get Integer
             | Size
             | Search String
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str    = Just (Add str)
parseCommand "get" val    = case all isDigit (unpack val) of
                              False => Nothing
                              True  => Just (Get (cast val))
parseCommand "quit" ""    = Just Quit
parseCommand "size" ""    = Just Size
parseCommand "search" str = Just $ Search str
parseCommand _      _     = Nothing

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

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

getSize : (store : DataStore) -> Maybe (String, DataStore)
getSize store = Just ("Size of store: " ++ cast (size store), store)

search : (store : DataStore) -> (str : String) -> Maybe (String, DataStore)
search store str =
  let store_items  = items store in
  let found = foldrImpl
                (\(ix, msg), acc => if (str `isInfixOf` msg)
                  then (cast $ finToInteger ix) ++ ": " ++ msg ++ "\n" ++ acc
                  else acc)
                ""
                (\acc => acc)
                (zip range store_items)
  in Just (found, store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp = case parse inp of
  Nothing           => Just ("Invalid command\n", store)
  Just (Add item)   => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
  Just (Get pos)    => getEntry pos store
  Just Size         => getSize store
  Just (Search str) => search store str
  Just Quit         => Nothing

main : IO ()
main = replWith (MkData _ []) "Command: " processInput

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module Data.Queue1

import Data.List
import Data.List1
import Data.SnocList

%default total

-------------
--- Queue ---
-------------

-- add from right, remove from left
export
record Queue1 a where
  constructor MkQueue
  right : SnocList a
  left  : List1 a

export
singleton : a -> Queue1 a
singleton = MkQueue [<] . singleton

export
add : a -> Queue1 a -> Queue1 a
add x = { right $= (:< x) }

-- Constructs a `Queue1` which has all elements in the left part of the queue reverted
%inline
pureLeftsFromSnoc : SnocList a -> Maybe $ Queue1 a
pureLeftsFromSnoc = map (MkQueue [<]) . fromList . cast

export
remove : Queue1 a -> (a, Lazy (Maybe $ Queue1 a))
remove $ MkQueue r (head ::: l) = (head,) $ delay $ case l of
  []      => pureLeftsFromSnoc r
  (x::xs) => Just $ MkQueue r (x:::xs)

export
Functor Queue1 where
  map f = { left $= map f, right $= map f }

export
filter : (a -> Bool) -> Queue1 a -> Maybe $ Queue1 a
filter f $ MkQueue r l = do
  let filteredR = filter f r
  let Just filteredL = fromList $ filter f $ toList l
    | Nothing => pureLeftsFromSnoc filteredR
  Just $ MkQueue filteredR filteredL

||| Returns a `List1` with newly added elements on the right and older elements in the left
export
toList1 : Queue1 a -> List1 a
toList1 $ MkQueue r l = l `appendl` cast r

ext: idr


text:
module Commons.Test.Unit.Parser

import Text.PrettyPrint.WL

import Text.Lexer
import Text.Parser

%default total
%access export

data TestReport : Type where
  ExpectedSuccess : (title : String) -> TestReport

  Failure : (title, msg : String) -> TestReport

  UnexpectedSuccess : (Show a)
                   => (title : String)
                   -> (made  : a)
                   -> TestReport

  FailureCmp : (Eq a, Show a)
            => (title, input : String)
            -> (expected : a)
            -> (given : a)
            -> TestReport

  WrongError : Show e
            => (title, input : String)
            -> (expected : e)
            -> (given    : e)
            -> TestReport

isSuccess : TestReport -> Bool
isSuccess (ExpectedSuccess _) = True
isSuccess _ = False

parseTest : Show tok
         => (title : String)
         -> (p : String -> Either (ParseError tok) ty)
         -> String
         -> TestReport
parseTest t run i =
  case run i of
    Left (Error err _) => Failure t err
    Right _ => ExpectedSuccess t

parseFail : Show ty
         => (title : String)
         -> (p : String -> Either (ParseError tok) (ty))
         -> String
         -> TestReport
parseFail t run i =
  case run i of
    Left _ => ExpectedSuccess t
    Right (res) => UnexpectedSuccess t res

parseTestAssert : (Eq ty, Show ty)
               => (title : String)
               -> (p : String -> Either (ParseError tok) (ty))
               -> String
               -> ty
               -> (ty -> ty -> Bool)
               -> TestReport
parseTestAssert t run i exp eq =
  case run i of
    Left (Error err _) => Failure t err
    Right (given) =>
      if eq given exp
        then ExpectedSuccess t
        else FailureCmp t i exp given

parseTestError : Show ty
               => (title : String)
               -> (p : String -> Either (ParseError tok) (ty))
               -> String
               -> String
               -> TestReport
parseTestError t run i exp =
  case run i of
    Left (Error err _ ) =>
      if (trim err) == (trim exp)
        then ExpectedSuccess t
        else WrongError t i exp err
    Right (res) => UnexpectedSuccess t res

showReport : TestReport-> Doc
showReport (ExpectedSuccess t) =  text "[PASS]" <+> text t
showReport (Failure t m) =
  vcat [ text "[FAIL] [PARSING]" <+> text t
       , indent 2 $ text "Gave error:"
       , text m
       ]
showReport (UnexpectedSuccess t res) =
  vcat [ text "[FAIL] [RESULT]" <+> text t
       , indent 2 $ text "Unexpectedly made:"
       , indent 4 $ (text . show) res
       ]
showReport (FailureCmp t i e g) =
  vcat [ text "[FAIL] [PARSING]" <+> text t
       , indent 2 $ text "Given input:"
       , indent 4 (text i)
       , indent 2 $ (text "Should have made:")
       , indent 4 $ (text . show) e
       , indent 2 $ (text "but made:")
       , indent 4 $ (text . show) g
       ]
showReport (WrongError t i e g) =
  vcat [ text "[FAIL] [ERROR]" <+> text t
       , indent 2 $ text "Given input:"
       , indent 4 (text i)
       , indent 2 $ (text "Should have errored with:")
       , indent 4 $ (text . show) e
       , indent 2 $ (text "but error was:")
       , indent 4 $ (text . show) g
       ]

runParseTest : Show a => TestReport -> IO Bool
runParseTest r = do putStrLn ((toString . showReport) r)
                    pure (isSuccess r)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Protocol.SExp

import Data.List

%default total

-- should be in base somewhere!
join : String -> List String -> String
join sep xs = concat $ intersperse sep xs

public export
data SExp = SExpList (List SExp)
          | StringAtom String
          | BoolAtom Bool
          | IntegerAtom Integer
          | SymbolAtom String

escape : String -> String
escape = pack . concatMap escapeChar . unpack
  where
    escapeChar : Char -> List Char
    escapeChar '\\' = ['\\', '\\']
    escapeChar '"'  = ['\\', '\"']
    escapeChar c    = [c]

export
Show SExp where
  show (SExpList xs) = assert_total $ "(" ++ join " " (map show xs) ++ ")"
  show (StringAtom str) = "\"" ++ escape str ++ "\""
  show (BoolAtom b) = ":" ++ show b
  show (IntegerAtom i) = show i
  show (SymbolAtom s) = ":" ++ s

public export
interface SExpable a where
  toSExp : a -> SExp

-- TODO: Merge these into 1 interface later
public export
interface FromSExpable a where
  fromSExp : SExp -> Maybe a

export
SExpable SExp where
  toSExp = id

export
SExpable Bool where
  toSExp = BoolAtom

export
FromSExpable Bool where
  fromSExp (BoolAtom b) = Just b
  fromSExp _ = Nothing

export
SExpable String where
  toSExp = StringAtom

export
FromSExpable String where
  fromSExp (StringAtom s) = Just s
  fromSExp _ = Nothing

export
SExpable Integer where
  toSExp = IntegerAtom

export
FromSExpable Integer where
  fromSExp (IntegerAtom a) = Just a
  fromSExp _ = Nothing

export
SExpable Int where
  toSExp = IntegerAtom . cast

export
FromSExpable Int where
  fromSExp a = do Just $ cast {from = Integer }$ !(fromSExp a)

export
SExpable Nat where
  toSExp = IntegerAtom . cast

export
FromSExpable Nat where
  fromSExp a = do Just $ cast {from = Integer }$ !(fromSExp a)

export
(SExpable a, SExpable b) => SExpable (a, b) where
  toSExp (x, y)
      = case toSExp y of
             SExpList xs => SExpList (toSExp x :: xs)
             y' => SExpList [toSExp x, y']

export
(FromSExpable a, FromSExpable b) => FromSExpable (a, b) where
  fromSExp (SExpList xs) = case xs of
    [x,y] => do pure $ (!(fromSExp x), !(fromSExp y))
    (x :: xs) => do pure $ (!(fromSExp x), !(fromSExp $ SExpList xs))
    _ => Nothing
  fromSExp _ = Nothing

export
SExpable a => SExpable (List a) where
  toSExp xs
      = SExpList (map toSExp xs)

export
FromSExpable a => FromSExpable (List a) where
  fromSExp (SExpList sexps) = traverse fromSExp sexps
  fromSExp _ = Nothing

export
SExpable a => SExpable (Maybe a) where
  toSExp Nothing = SExpList []
  toSExp (Just x) = toSExp x


text:
module Quantities.SIBaseUnits

import Quantities.Core
import Quantities.SIPrefixes
import Quantities.SIBaseQuantities

%default total
%access public export

Metre : ElemUnit Length
Metre = MkElemUnit "m" 1
Meter : ElemUnit Length
Meter = Metre
M : ElemUnit Length
M = Meter

Centimetre : Unit Length
Centimetre = centi Metre
Centimeter : Unit Length
Centimeter = Centimetre
Cm : Unit Length
Cm = Centimetre

Kilometre : Unit Length
Kilometre = kilo Metre
Kilometer : Unit Length
Kilometer = Kilometre
Km : Unit Length
Km = Kilometre

Gram : ElemUnit Mass
Gram = MkElemUnit "g" 0.001
G : ElemUnit Mass
G = Gram

Kilogram : Unit Mass
Kilogram = kilo Gram
Kg : Unit Mass
Kg = Kilogram

Second : ElemUnit Time
Second = MkElemUnit "s" 1
S : ElemUnit Time
S = Second

Ampere : ElemUnit ElectricCurrent
Ampere = MkElemUnit "A" 1
A : ElemUnit ElectricCurrent
A = Ampere

Kelvin : ElemUnit Temperature
Kelvin = MkElemUnit "K" 1
K : ElemUnit Temperature
K = Kelvin

Mole : ElemUnit AmountOfSubstance
Mole = MkElemUnit "mol" 1
Mol : ElemUnit AmountOfSubstance
Mol = Mole

Candela : ElemUnit LuminousIntensity
Candela = MkElemUnit "cd" 1
Cd : ElemUnit LuminousIntensity
Cd = Candela

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
data SnocList : List a -> Type where
    Empty : SnocList []
    Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])

snocListHelper : (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
snocListHelper {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelper {input} snoc (x :: xs) =
    rewrite appendAssociative input [x] xs in
        snocListHelper (Snoc snoc {x}) xs

snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelper Empty xs

myReverseHelper : (input : List a) -> SnocList input -> List a
myReverseHelper [] Empty = []
myReverseHelper (xs ++ [x]) (Snoc rec) = x :: myReverseHelper xs rec

myReverse : List a -> List a
myReverse input with (snocList input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (Snoc rec) = x :: myReverse xs | rec

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix [] input2 | Empty = True
  isSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    isSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
        if x == y then isSuffix xs ys | xsrec | ysrec
            else False


text:
module Control.Monad.Coop

import public Arduino.Time
import Arduino.Util

import Data.List

import Control.Monad.Syntax
import Control.Monad.Trans

%default total

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

public export
interface Parallel m where
  -- Alternative-like operator with parallel semantics and unavailable results of separate computations
  (<||>) : m Unit -> m Unit -> m Unit

------------
--- Data ---
------------

export
data Coop : (m : Type -> Type) -> (a : Type) -> Type where
  Point       : (1 _ : m a) -> Coop m a
  Sequential  : Coop m a -> (a -> Coop m b) -> Coop m b
  Cooperative : Coop m a -> Coop m b -> Coop m Unit
  DelayedTill : Time -> Coop m Unit

--------------------------------
--- Basic creation functions ---
--------------------------------

export
atomic : (1 _ : m a) -> Coop m a
atomic = Point

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

export
Timed m => Timed (Coop m) where
  currentTime = Point currentTime

infixl 4 $>

($>) : Applicative m => Coop m a -> b -> Coop m b
(Point _)        $> b = Point $ pure b
(Sequential a f) $> b = Sequential a $ \ar => f ar $> b
x                $> b = Sequential x . const . Point $ pure b

export
Applicative m => Functor (Coop m) where
  map f (Point a)           = Point (map f a)
  map f (Sequential a b)    = Sequential a $ \ar => map f $ b ar
  map f x@(Cooperative _ _) = x $> f ()
  map f x@(DelayedTill t)   = x $> f ()

export
Applicative m => Applicative (Coop m) where
  pure    = Point . pure
  l <*> r = Sequential l (<$> r)
  -- This could be `(<*>) = Cooperative apply`, but it must be consistent with `(>>=)` definition.
  -- Consider code `doSmth *> delayedFor 100 *> doMore` comparing to `(doSmth <||> delayedFor 100) *> doMore`.
  -- Having parallel semantics for the `Applicative`'s `<*>`, those two examples above will mean the same, which seems to be unexpected.

export
Monad m => Monad (Coop m) where
  (>>=) = Sequential

export
Parallel (Coop m) where
  (<||>) = Cooperative

export
Monad m => DelayableTill (Coop m) where
  sleepTill = DelayedTill

export
(Timed m, Monad m) => DelayableFor (Coop m) where
  sleepFor t = sleepTill . (+t) =<< currentTime

export
HasIO (Coop IO) where
  liftIO = atomic

export
MonadTrans Coop where
  lift = atomic

-------------------
--- Interpreter ---
-------------------

Sync : Type
Sync = Nat

-- Two present fences with the same sync are meant to be blocking each other.
-- Postponed `Coop m y` needs to be sheduled only when all events with its sync are over.
-- `Sync` type is a comparable type and is a workaround of uncomparability of `Coop`.
data Fence : (Type -> Type) -> Type where
  No : Fence m
  Sy : Sync -> (postponed : Coop m y) -> (next : Fence m) -> Fence m

record Event m where
  constructor Ev
  time  : Time
  coop  : Coop m x
  fence : Fence m

-- This great function must be somewhere in the standard libraries.
on : (b -> b -> c) -> (a -> b) -> a -> a -> c
on f g x y = g x `f` g y

-- The following comparison is only according to the time; this will incorrectly work for sets.
-- Equally timed events with different actions are considered to be equal with `==` relation.
[TimeOnly_EvEq] Eq (Event m) where
  (==) = (==) `on` time

[TimeOnly_EvOrd] Ord (Event m) using TimeOnly_EvEq where
  compare = compare `on` time

export covering
runCoop : (Monad m, Timed m) => Coop m Unit -> m Unit
runCoop co = runLeftEvents [Ev !currentTime co No] where

  -- TODO to replace list with a sortedness-preserving kinda-list
  covering
  runLeftEvents : List $ Event m -> m Unit
  runLeftEvents [] = pure ()
  runLeftEvents evs@((Ev currEvTime currCoop currFence)::restEvs) = do
    nextEvs <- if !currentTime >= currEvTime
               then do
                 let newLeftEvs = merge @{TimeOnly_EvOrd} restEvs !newEvsAfterRunningCurr
                 pure $ merge @{TimeOnly_EvOrd} newLeftEvs $ awakened newLeftEvs
               else
                 -- TODO else wait for the `currEvTime - !currentTime`; or support and perform permanent tasks
                 pure evs
    runLeftEvents nextEvs

  where
    syncs : List (Event m) -> List Sync
    syncs evs = evs >>= syncsOfFence . fence where
      syncsOfFence : Fence m -> List Sync
      syncsOfFence No          = []
      syncsOfFence (Sy s _ fe) = s :: syncsOfFence fe

    uniqueSync : Lazy Sync
    uniqueSync = case syncs evs of
      []         => 0
      ss@(t::ts) => case foldl min t ts of
        S x => x                  -- either minimal minus 1
        Z   => S $ foldl max 0 ss -- or maximal plus 1

    -- All actions of form `patterm => pure [Ev ..., ...]` can be thought as a rewriting rule upon the list of events.
    newEvsAfterRunningCurr : m (List $ Event m)
    newEvsAfterRunningCurr = case currCoop of
      Point x                        => x $> Nil
      Cooperative l r                => pure [Ev currEvTime l currFence, Ev currEvTime r currFence]
      DelayedTill d                  => pure [Ev d (Point $ pure ()) currFence] -- this enables currFence to be run when appropriate (delayed)
      Sequential (Point y)         f => map (\r => [Ev currEvTime (f r) currFence]) y
      Sequential (Sequential y g)  f => pure [Ev currEvTime (Sequential y $ g >=> f) currFence]
      Sequential (DelayedTill d)   f => pure [Ev d (f ()) currFence]
      Sequential (Cooperative l r) f => let newFence = Sy uniqueSync (f ()) currFence in -- coop in the `currFence` needs to be run after the `f ()`
                                        pure [Ev currEvTime l newFence, Ev currEvTime r newFence]

    awakened : (evsAfterCurr : List $ Event m) -> List $ Event m
    awakened evsAfterCurr = case currFence of
      No                    => []
      Sy sync coop subFence => if sync `elem` syncs evsAfterCurr
                                   then []                            -- then someone else will raise this
                                   else [Ev currEvTime coop subFence] -- no one that blocks is left

------------------------------
--- Interesting properties ---
------------------------------

0 run_unlifts : (Monad m, Timed m) => (x : m ()) -> runCoop (lift x) = x

0 run_seq_dep_lin : (Monad m, Timed m) => (x : m a) -> (y : a -> Coop m ()) -> runCoop (lift x >>= y) = x >>= runCoop . y

0 run_seq_indep_lin : (Monad m, Timed m) => (x, y : Coop m ()) -> runCoop (x >>= const y) = runCoop x >>= const (runCoop y)

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Data.Nat.Algebra

import Control.Algebra
import Data.Nat

%default total

namespace SemigroupV

  public export
  [Additive] SemigroupV Nat using Semigroup.Additive where
    semigroupOpIsAssociative = plusAssociative

namespace MonoidV

  public export
  [Additive] MonoidV Nat using Monoid.Additive SemigroupV.Additive where
    monoidNeutralIsNeutralL = plusZeroRightNeutral
    monoidNeutralIsNeutralR = plusZeroLeftNeutral


text:
module Helpers

export
parseFile : String -> IO (List String)
parseFile path = do file <- readFile path
                    case file of
                      Right content => pure (split (== '\n') content)
                      Left err => pure Nil


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String

import System.File

data LowPoint = L Nat | N Nat

get : LowPoint -> Nat
get (L k) = k
get (N k) = k

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

lowPointsRow : Nat -> List Nat -> List LowPoint
lowPointsRow n [] = []
lowPointsRow n (x :: []) = if x < n then [L x] else [N x]
lowPointsRow n (x :: (y :: xs)) = (if x < n && x < y then L x else N x) :: lowPointsRow x (y :: xs)

comp : Nat -> LowPoint -> LowPoint
comp p (L k) = if k < p then L k else N k
comp _ (N k) = N k

comp3 : Nat -> LowPoint -> Nat -> LowPoint
comp3 p (L k) n = if k < n && k < p then L k else N k
comp3 _ (N k) _ = N k

lowPointsCol : List Nat -> List (List LowPoint) -> List (List LowPoint)
lowPointsCol prev [] = []
lowPointsCol prev (row :: []) = [ (\(p, r) => comp p r) <$> zip prev row ]
lowPointsCol prev (row :: (next :: rows)) = ((\(p, r, n) => comp3 p r (get n)) <$> zip3 prev row next) :: lowPointsCol (get <$> row) (next :: rows)

HMap : Type
HMap = List ((Nat, Nat), Nat)

toMap : (Nat, Nat) -> List (List LowPoint) -> (HMap, List (Nat, Nat))
toMap (x, y) [] = ([], [])
toMap (x, y) ([] :: xs) = toMap (0, y + 1) xs
toMap (x, y) (((L k) :: ys) :: xs) = let (m, ls) = toMap (x + 1, y) (ys :: xs) in
                                       (((x, y), k) :: m, (x,y) :: ls)
toMap (x, y) (((N k) :: ys) :: xs) = let (m, ls) = toMap (x + 1, y) (ys :: xs) in
                                       (((x, y), k) :: m, ls)

basinFrom : HMap -> List (Nat, Nat) -> (Nat, Nat) -> List (Nat, Nat)
basinFrom m p (x, y) = if elem (x, y) p
                          then p
                          else case lookup (x, y) m of
                                    Just k => if k < 9
                                                 then let p0 = (x, y) :: p
                                                          p1 = basinFrom m p0 (x + 1, y)
                                                          p2 = basinFrom m p1 (x, y + 1)
                                                          p3 = basinFrom m p2 (minus x 1, y) in
                                                          basinFrom m p3 (x, minus y 1)
                                                 else p
                                    Nothing => p

run : String -> IO ()
run s = do let l = (\l => catMaybes $ parsePositive {a=Nat} . singleton <$> unpack l) <$> lines s
           let r = lowPointsCol (replicate 100 10) $ lowPointsRow 10 <$> l
           let (m, ls) = toMap (0,0) r
           let c = product $ take 3 $ reverse $ sort $ (length . basinFrom m []) <$> ls
           putStrLn $ show c

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Extra.C.Ptr

import Extra.C.FFI
import public Extra.C.Types

||| `malloc` in C
export
%foreign libc "malloc"
prim__malloc : SizeT -> PrimIO AnyPtr

||| `calloc` in C
export
%foreign libc "calloc"
prim__calloc : SizeT -> PrimIO AnyPtr

||| `free` in C
export
%foreign libc "free"
prim__free : AnyPtr -> PrimIO ()

export
%foreign libextra "ptr_eq"
prim__ptr_eq : AnyPtr -> AnyPtr -> PrimIO Bool

export
%foreign libextra "ptr_plus"
prim__ptr_plus : AnyPtr -> SSizeT -> PrimIO AnyPtr

||| cast pointer
export
castPtr : AnyPtr -> Ptr a
castPtr = prim__castPtr

||| forget pointer
export
forgetPtr : Ptr a -> AnyPtr
forgetPtr = prim__forgetPtr

export
pretendPtr : Ptr a -> Ptr b
pretendPtr = castPtr . forgetPtr

export
Eq AnyPtr where
  a == b = unsafePerformIO $ primIO $ prim__ptr_eq a b

export
Eq (Ptr a) where
  a == b = forgetPtr a == forgetPtr b

||| `nullptr` in C
export
nullanyptr : AnyPtr
nullanyptr = prim__getNullAnyPtr

||| `nullptr` of a `Ptr` in C
export
nullptr : Ptr a
nullptr = castPtr nullanyptr

export
plusAnyPtr : AnyPtr -> (offset : SSizeT) -> AnyPtr
plusAnyPtr ptr ofs = unsafePerformIO $ primIO $ prim__ptr_plus ptr ofs

export
plusPtr : Ptr a -> (offset : SSizeT) -> Ptr a
plusPtr ptr ofs = castPtr $ plusAnyPtr (forgetPtr ptr) ofs


text:
double : Int -> Int
double x = x + x

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
module Crypto.RawSodium

%lib     C "sodium"
%link    C "sodium_glue.o"
%include C "sodium_glue.h"

-- RAW INTERFACE
-- Key and nonce lengths

box_nonceLength : IO Int
box_nonceLength = mkForeign (FFun "box_nonceLength" [] FInt)

box_secretKeyLength : IO Int
box_secretKeyLength = mkForeign (FFun "box_secretKeyLength" [] FInt)

box_publicKeyLength : IO Int
box_publicKeyLength = mkForeign (FFun "box_publicKeyLength" [] FInt)

secretbox_nonceLength : IO Int
secretbox_nonceLength = mkForeign (FFun "box_nonceLength" [] FInt)

secretbox_keyLength : IO Int
secretbox_keyLength = mkForeign (FFun "secretbox_keyLength" [] FInt)

-- Create/read/write keys

do_newKey : Int -> IO ManagedPtr
do_newKey len = do p <- mkForeign (FFun "mkKey" [FInt] FPtr) len
                   return $ registerPtr p (len+16)

do_getKeyLen : ManagedPtr -> IO Int
do_getKeyLen p = mkForeign (FFun "keyLen" [FManagedPtr] FInt) p

do_getKeyIdx : ManagedPtr -> Int -> IO Int
do_getKeyIdx p i = mkForeign (FFun "keyIdx" [FManagedPtr, FInt] FInt) p i

do_setKeyIdx : ManagedPtr -> Int -> Int -> IO ()
do_setKeyIdx p i b
     = mkForeign (FFun "setKeyIdx" [FManagedPtr, FInt, FInt] FUnit) p i b

-- Create/read/write nonces

do_newNonce : Int -> IO ManagedPtr
do_newNonce len = do p <- mkForeign (FFun "mkNonce" [FInt] FPtr) len
                     return $ registerPtr p (len+16)

do_newNonceFromString : String -> IO ManagedPtr
do_newNonceFromString s
     = do p <- mkForeign (FFun "mkNonceFromString" [FString] FPtr) s
          return $ registerPtr p (cast (length s) + 16)

do_setNonceIdx : ManagedPtr -> Int -> Int -> IO ()
do_setNonceIdx p i b
     = mkForeign (FFun "setNonceIdx" [FManagedPtr, FInt, FInt] FUnit) p i b

-- Making/reading boxes

do_newBox : Int -> IO ManagedPtr
do_newBox len = do p <- mkForeign (FFun "newBox" [FInt] FPtr) len
                   return $ registerPtr p (len + 16)

do_newSecretBox : Int -> IO ManagedPtr
do_newSecretBox len = do p <- mkForeign (FFun "newBox" [FInt] FPtr) len
                         return $ registerPtr p (len + 16)

do_getBoxLen : ManagedPtr -> IO Int
do_getBoxLen p = mkForeign (FFun "getEncLen" [FManagedPtr] FInt) p

do_getBoxIdx : ManagedPtr -> Int -> IO Int
do_getBoxIdx p i = mkForeign (FFun "getEncByte" [FManagedPtr, FInt] FInt) p i

do_setBoxIdx : ManagedPtr -> Int -> Int -> IO ()
do_setBoxIdx p i b
     = mkForeign (FFun "setEncByte" [FManagedPtr, FInt, FInt] FUnit) p i b

-- Reading results of operations (symmetric or public key)

do_readBoxOpen : ManagedPtr -> IO String
do_readBoxOpen p = mkForeign (FFun "getDec" [FManagedPtr] FString) p

-- Symmetric keys

do_cryptoSecretBox : (msg : String) ->
                     (nonce : ManagedPtr) ->
                     (key : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoSecretBox m n k
   = do p <- mkForeign (FFun "do_crypto_secretbox"
                       [FString, FManagedPtr, FManagedPtr] FPtr) m n k
        if !(nullPtr p)
           then return Nothing
           else do boxlen <- mkForeign (FFun "getEncSize" [FPtr] FInt) p
                   return $ Just (registerPtr p (boxlen + 16))

do_cryptoSecretBoxOpen : (ciphertext : ManagedPtr) ->
                         (nonce : ManagedPtr) ->
                         (key : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoSecretBoxOpen c n k
   = do p <- mkForeign (FFun "do_crypto_secretbox_open"
                       [FManagedPtr, FManagedPtr, FManagedPtr] FPtr) c n k
        if !(nullPtr p)
           then return Nothing
           else do boxlen <- mkForeign (FFun "getDecSize" [FPtr] FInt) p
                   return $ Just (registerPtr p (boxlen + 16))

-- Public keys

do_newKeyPair : IO Ptr
do_newKeyPair = mkForeign (FFun "newKeyPair" [] FPtr)

do_getPublic : Ptr -> IO ManagedPtr
do_getPublic kp = do p <- mkForeign (FFun "getPublic" [FPtr] FPtr) kp
                     len <- mkForeign (FFun "keyLen" [FPtr] FInt) p
                     return $ registerPtr p (len + 16)

do_getSecret : Ptr -> IO ManagedPtr
do_getSecret kp = do p <- mkForeign (FFun "getSecret" [FPtr] FPtr) kp
                     len <- mkForeign (FFun "keyLen" [FPtr] FInt) p
                     return $ registerPtr p (len + 16)

do_cryptoBox : (msg : String) ->
               (nonce : ManagedPtr) ->
               (pkey : ManagedPtr) ->
               (skey : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoBox m n pk sk
   = do p <- mkForeign (FFun "do_crypto_box"
                       [FString, FManagedPtr, FManagedPtr, FManagedPtr] FPtr) m n pk sk
        if !(nullPtr p)
           then return Nothing
           else do boxlen <- mkForeign (FFun "getEncSize" [FPtr] FInt) p
                   return $ Just (registerPtr p (boxlen + 16))

do_cryptoBoxOpen : (ciphertext : ManagedPtr) ->
                   (nonce : ManagedPtr) ->
                   (pkey : ManagedPtr) ->
                   (skey : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoBoxOpen c n pk sk
   = do p <- mkForeign (FFun "do_crypto_box_open"
                       [FManagedPtr, FManagedPtr, FManagedPtr, FManagedPtr] FPtr) c n pk sk
        if !(nullPtr p)
           then return Nothing
           else do boxlen <- mkForeign (FFun "getDecSize" [FPtr] FInt) p
                   return $ Just (registerPtr p (boxlen + 16))

-- Releasing memory for keys and results of encryption/decryption

-- do_freeBox : Ptr -> IO ()
-- do_freeBox p = mkForeign (FFun "freeEnc" [FPtr] FUnit) p
--
-- do_freeBoxOpen : Ptr -> IO ()
-- do_freeBoxOpen p = mkForeign (FFun "freeDec" [FPtr] FUnit) p
--
-- do_freeKey : Ptr -> IO ()
-- do_freeKey p = mkForeign (FFun "freeKey" [FPtr] FUnit) p

do_freeKeyPair : Ptr -> IO ()
do_freeKeyPair p = mkForeign (FFun "freeKeyPair" [FPtr] FUnit) p

max_stars_repo_name: edwinb/sodium-idris

max_issues_repo_name: edwinb/sodium-idris

max_forks_repo_name: edwinb/sodium-idris


text:
-- test that sendAndBroadcast doesn't block

import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          (MkDPair bc send) <- becomeSender bcRef
          send Broadcast bc 3
          putStrLn "Success!"


text:
-- -------------------------------------------------------------- [ Format.idr ]
-- Module  : Data.Time.Format
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Data.Time.Format

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

max_stars_repo_name: yurrriq/idris-time

max_issues_repo_name: yurrriq/idris-time

max_forks_repo_name: yurrriq/idris-time


text:
module Test.Utils

import System

public export
Test : Type
Test = IO Int

export
assertThat : Bool -> String -> Test
assertThat test errorMsg =
  if test
    then do putStrLn "Test Passed"; pure 0
    else do putStrLn ("Test Failed: " ++ errorMsg); pure 1

export
assertEq : (Eq a, Show a) => (expected : a) -> (given : a) -> Test
assertEq e g =
  assertThat (g == e) $
    "Expected == " ++ show e ++ ", Got: " ++ show g

export
runTests : List Test -> Test
runTests = foldl (\res, t => (+) <$> res <*> t) (pure 0)

export
runTestSuite : List Test -> IO ()
runTestSuite tests = do
  failedCount <- runTests tests
  if failedCount > 0
    then exitFailure
    else pure ()

--

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
module Test.Generate

import Data.Word.Word8
import Data.Bytes
-- import Control.Monad.State -- for making a MonadIO

import System.Random
-- TODO: Later on this should be a seedable prng for reproducable testing, and
-- for making pure values without unsafePerformIO

data PropResult = Error String | Sucess

data Tests : Type where
  MkTests : List PropResult -> Tests

prop : String -> Bool -> PropResult
prop name b = if b then Sucess
                   else Error (name ++ " failure")

runProps : List (String, Tests) -> IO ()
runProps ps = do for ps $ (\(name,p) => ?sdfsd)
                 ?sdsfd

replicateA : Applicative m => Nat -> m a -> m (List a)
replicateA 0 _ = pure []
replicateA (S k) act = [| act :: replicateA k act |]

-- remove the range on this later to test Word8 itself
arbitrary : Word8
arbitrary = unsafePerformIO $
  let r : IO Int = randomRIO (0,255) in cast <$> r

-- forAll : (Word8 -> a -> Bool) -> a -> IO Bool
-- forAll wf x = pure (wf !(arbitraryWord8) x)

test1 : a -> (a -> Bool) -> Bool
test1 x f = f x

test2 : a -> b -> (a -> b -> Bool) -> Bool
test2 x y f = f x y

infixr 0 &&
(&&) : a -> (a -> b) -> b

-- consTests : Tests
-- consTests = MkTests
--   [ prop "cons1" $ arbitrary && \x => cons x empty == singleton x
--   ]
--
-- appendTests : Tests
-- appendTests = MkTests
--   [ prop "append1" $ cons 1 empty == singleton 1
--   , prop "append2" $ cons 3 empty == singleton 3
--   , prop "append3" $ cons 3 (singleton 2) == ?fdssd
--   ]
--
-- test : IO ()
-- test = runProps $ [("cons"  , consTests  )
--                   ,("append", appendTests)
--                   ]

-- :exec replicateA 100000 (arbitraryWord8 >>= printLn)


text:
data Fin : Nat -> Type where
    FZ : Fin (S k)
    FS : Fin k -> Fin (S k)

%builtin Natural Fin

finToInteger : Fin k -> Integer
finToInteger FZ = 0
finToInteger (FS k) = 1 + finToInteger k

%builtin NaturalToInteger finToInteger


text:
module MoodMelvilleQueue

import Queue

%default total
%access private

data RotationState a =
    Idle
  | Reversing Int (List a) (List a) (List a) (List a)
  | Appending Int (List a) (List a)
  | Done (List a)

export
data HoodMelvilleQueue a = HM Int (List a) (RotationState a) Int (List a)

exec : RotationState a -> RotationState a
exec (Reversing ok (x :: f) f' (y :: r) r') = Reversing (ok + 1) f (x :: f') r (y :: r')
exec (Reversing ok []       f' [y]      r') = Appending ok f' (y :: r')
exec (Appending 0  f'        r') = Done r'
exec (Appending ok (x :: f') r') = Appending (ok - 1) f' (x :: r')
exec state = state

invalidate : RotationState a -> RotationState a
invalidate (Reversing ok f f' r r') = Reversing (ok - 1) f f' r r'
invalidate (Appending 0  f' (x :: r')) = Done r'
invalidate (Appending ok f' r'       ) = Appending (ok - 1) f' r'
invalidate state = state

exec2 : Int -> List a -> RotationState a -> Int -> List a -> HoodMelvilleQueue a
exec2 lenf f state lenr r =
  case exec (exec state) of
    (Done newf) => HM lenf newf Idle lenr r
    newstate => HM lenf f newstate lenr r

check : Int -> List a -> RotationState a -> Int -> List a -> HoodMelvilleQueue a
check lenf f state lenr r =
  if lenr <= lenf then exec2 lenf f state lenr r
  else let newstate = Reversing 0 f [] r []
       in exec2 (lenf + lenr) f newstate 0 []

export
Queue HoodMelvilleQueue where
  empty = HM 0 [] Idle 0 []
  isEmpty (HM lenf f state lenr r) = lenf == 0

  snoc (HM lenf f state lenr r) x = check lenf f state (lenr + 1) (x :: r)

  head (HM _ []        _ _ _) = idris_crash "empty queue"
  head (HM _ (x :: f') _ _ _) = x

  tail (HM lenf []        state lenr r) = idris_crash "empty queue"
  tail (HM lenf (x :: f') state lenr r) =
    check (lenf - 1) f' (invalidate state) lenr r


text:
-- | Exercises on Lists
module Koans.Lists

-- | What is the type of this list.
nats : ?someType
nats = [0,1,2,3,4,5,6,7,9]

-- | Reproduce the list [0,1,3,5,7,9,2,4,6,8] using the following functions.
odds : List Int
odds = [1,3,5,7,9]

evens : List Int
evens = [2,4,6,8]

zero : Int
zero = 0

zeroOddsEvens : Bool
zeroOddsEvens = ?fillme2 ++ odds ++ ?fillme3 == [0,1,3,5,7,9,2,4,6,8]

-- | Complete the result of following functions.

headOList : Bool
headOList = ?fillme4 == head [5,4,3,2,1]

tailOList : Bool
tailOList = ?fillme5 == tail [0,1,2,3,4,5]

lastOList : Bool
lastOList = ?fillme6 == last [5,4,3,2,1]

initOList : Bool
initOList = ?fillme7 == init [1,2,3,4,5,6]

lengthOList : Bool
lengthOList = ?fillme8 == length [1,2,3,4,5]

reverseTheList : Bool
reverseTheList = ?fillme9 reverse [1,2,3,4,5]

first3 : Bool
first3 = ?fillme10 == take 3 [1..10]

drop3 : Bool
drop3 = ?fillme11 drop 3 [1..10]

countAllTheNumbers : Bool
countAllTheNumbers = ?fillme12 == sum [1..10]

timesAllTheNnumbers : Bool
timesAllTheNnumbers = ?fillme13 == product [1..10]

elementOrNot : Bool
elementOrNot = elem 4 ?fillme14 == True

-- | Make this function true
stopPete : List Nat
stopPete = ?fillme15 (repeat 3) == [3,3,3,3]

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

max_stars_repo_name: silky/idris-koans

max_issues_repo_name: silky/idris-koans

max_forks_repo_name: silky/idris-koans


text:
module Data.LeftPad

import Data.List
import Data.List.Predicates.Interleaving

%default total
%access public export

data Padding : (s : List Char) -> (target : Nat) -> Type where
  Pad : (pad : Nat) -> Padding s (length s + pad)
  Nop : Padding (ys ++ x :: xs) (length ys)

padding : (s : List Char) -> (target : Nat) -> Padding s target
padding       []     t  = Pad t
padding (x :: xs)    Z  = Nop {ys = []}
padding (x :: xs) (S t) with (padding xs t)
  padding (x :: xs) (S (plus (length xs) p))   | Pad p = Pad p
  padding (y :: ys ++ z :: zs) (S (length ys)) | Nop   = Nop {ys=y::ys}

pad : (s : List Char) -> (c : Char) -> (target : Nat) -> List Char
pad s c target with (padding s target)
  pad s c (length s + pad)          | Pad pad  = replicate pad c ++ s
  pad (ys ++ x :: xs) c (length ys) | Nop {ys} = ys ++ x :: xs

namespace MorePad
  Pad : (s : List Char) -> (c : Char) -> (target : Nat) -> Type
  Pad s c target with (padding s target)
    Pad s c ((length s) + pad) | (Pad pad) = let ps = replicate pad c in Interleaving ps s (ps ++ s)

    Pad (ys ++ (x :: xs)) c (length ys) | Nop = Interleaving Nil (ys ++ (x :: xs)) (ys ++ (x :: xs))

  noPad : (s : List Char) -> Interleaving Nil s s
  noPad [] = Empty
  noPad (x :: xs) = RightAdd x (noPad xs)

  addPadd : (pad : List Char) -> (s : List Char) -> Interleaving pad s (pad ++ s)
  addPadd [] s = noPad s
  addPadd (x :: xs) s = LeftAdd x (addPadd xs s)

  pad : (s : List Char) -> (c : Char) -> (target : Nat) -> Pad s c target
  pad s c target with (padding s target)
    pad s c ((length s) + pad) | (Pad pad) = let ps = replicate pad c in addPadd ps s
    pad (ys ++ (x :: xs)) c (length ys) | Nop = noPad (ys ++ (x::xs))

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module CatList

import CatenableList
import Queue

%default total
%access private

export
data CatList : (Type -> Type) -> Type -> Type where
  E : CatList q a
  C : a -> q (Lazy (CatList q a)) -> CatList q a

link : Queue q => CatList q a -> Lazy (CatList q a) -> CatList q a
link c s = assert_total $ case c of
  (C x q) => C x (snoc q s)
  E => assert_unreachable

linkAll : Queue q => CatList q a -> q (Lazy (CatList q a)) -> CatList q a
linkAll t q' =
  if isEmpty q'
   then t
   else link t (linkAll (Force $ head q') (assert_smaller q' $ tail q'))

export
Queue q => CatenableList (CatList q) where
  empty = E
  isEmpty E = True
  isEmpty _ = False

  xs ++ E  = xs
  E  ++ ys = ys
  xs ++ ys = link xs ys

  cons x xs = (assert_total $ C x empty) ++ xs
  snoc xs x = xs ++ (assert_total $ C x empty)

  head c = assert_total $ case c of
    E => idris_crash "empty list"
    (C x y) => x

  tail c = assert_total $ case c of
    E => idris_crash "empty list"
    (C x q) => if isEmpty q then E else linkAll (Force $ head q) (tail q)


text:
module IdrisJvm.IO

import public IdrisJvm.FFI
import Java.Lang

%access public export

printLn : Show a => a -> JVM_IO ()
printLn = printLn'

putStrLn : String -> JVM_IO ()
putStrLn = putStrLn'

print : Show a => a -> JVM_IO ()
print = print'

putStr : String -> JVM_IO ()
putStr = putStr'

getLine : JVM_IO String
getLine = getLine'

putCh : Char -> JVM_IO ()
putCh ch = PrintStream.printCh System.stdout ch

getCh : JVM_IO Char
getCh = invokeStatic RuntimeClass "readChar" (JVM_IO Char)

putChar : Char -> JVM_IO ()
putChar ch = PrintStream.printCh System.stdout ch

getChar : JVM_IO Char
getChar = invokeStatic RuntimeClass "readChar" (JVM_IO Char)

jputChar : Char -> JVM_IO ()
jputChar ch = PrintStream.printCh System.stdout ch

jgetChar : JVM_IO Char
jgetChar = invokeStatic RuntimeClass "readChar" (JVM_IO Char)


text:
module Crypto.Random.C

import Crypto.Random
import System.FFI
import Data.Vect
import Utils.Misc
import Data.Buffer
import Data.List
import System.Info

%foreign "C:random_buf,libidristls"
prim_io__random_buf : Buffer -> Int -> PrimIO Int

public export
HasIO io => MonadRandom io where
  random_bytes Z = pure []
  random_bytes n = do
    let n' = cast n
    Just buf <- newBuffer n'
    | Nothing => assert_total $ idris_crash "somehow newBuffer failed"
    0 <- primIO $ prim_io__random_buf buf n'
    | _ => assert_total $ idris_crash "random_buf failed"
    traverse (getBits8 buf) (map (cast . finToNat) Fin.range)


text:
module Void

-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
    hd : List a -> a
    hd (x :: xs) = x

-- not terminating
empty2 : Void
empty2 = empty2


text:
module Test

import Salo.Language.Lexer
import Salo.Language.Parser

main : IO ()
main = do Salo.Language.Lexer.Test.test
          Salo.Language.Parser.Test.test

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs

eval: (Abs num, Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = div (eval x) (eval y)
eval (Abs x)   = abs (eval x)

exprShowHelper: Show ty => (left: ty) -> (symb: Char) -> (right: ty) -> String
exprShowHelper left symb right =
  "(" ++ show left ++ " " ++ cast symb ++ " " ++ show right ++ ")"

Show ty => Show (Expr ty) where
  show (Val x) = show x
  show (Add x y) = exprShowHelper x '+' y
  show (Sub x y) = exprShowHelper x '-' y
  show (Mul x y) = exprShowHelper x '*' y
  show (Div x y) = exprShowHelper x '/' y
  show (Abs x) = "|"++ show x ++"|"

(Abs ty, Neg ty, Integral ty, Eq ty) => Eq (Expr ty) where
  (==) x y = eval x == eval y

(Abs ty, Neg ty, Integral ty) => Cast (Expr ty) ty where
  cast = eval

Functor Expr where
  map func (Val x) = Val (func x)
  map func (Add x y) = Add (map func x)(map func y)
  map func (Sub x y) = Sub (map func x)(map func y)
  map func (Mul x y) = Mul (map func x)(map func y)
  map func (Div x y) = Div (map func x)(map func y)
  map func (Abs x) = Abs (map func x)

example1: Expr Integer
example1 = Add (Val 6) (Mul (Val 3) (Abs(Val (-12))))

example2: Expr Integer
example2 = 6 + 3 * 12

example3: Expr Integer
example3 = 6 * 3 + 12

example4: Expr Integer
example4 = 1 + 2 * 3

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
import CatenableDeque
import FiniteMap

import BankersDeque
import ImplicitCatenableDeque

import Trie
import TrieOfTrees

data SizedD : (Type -> Type) -> Type -> Type where
  MkSized : (sz : Int) -> (d : dt a) -> SizedD dt a

ImplicitCatenableDeque.Sized (SizedD d) where
  size (MkSized sz _) = sz

subtract : Neg n => n -> n -> n
subtract y x = x - y

Deque d => Deque (SizedD d) where
  empty = MkSized 0 empty
  isEmpty (MkSized sz _) = 0 == sz
  cons x (MkSized sz d) = MkSized (1 + sz) (cons x d)
  head (MkSized _ d) = head d
  tail (MkSized sz d) = MkSized (subtract 1 sz) (tail d)
  snoc (MkSized sz d) x = MkSized (sz + 1) (snoc d x)
  last (MkSized _ d) = last d
  init (MkSized sz d) = MkSized (sz - 1) (init d)

CatenableDeque d => CatenableDeque (SizedD d) where
  (MkSized sz1 d1) ++ (MkSized sz2 d2) = MkSized (sz1 + sz2) (d1 ++ d2)

data BoolMap : Type -> Type -> Type where
  BM : (Maybe a, Maybe a) -> BoolMap Bool a

FiniteMap BoolMap Bool where
  empty = BM (Nothing, Nothing)
  bind False x (BM t) = BM (Just x, snd t)
  bind True x (BM t) = BM (fst t, Just x)
  lookup False (BM t) = fst t
  lookup True (BM t) = snd t


text:
infixr 5 ::

namespace List
    public export
    data List a = Nil | (::) a (List a)

namespace Stream
    public export
    data Stream a = (::) a (Inf (Stream a))

ones : Stream Integer
ones = num :: ones
  where
    num : Integer -- gratuitous where for a regression test!
    num = 1

data Nat = Z | S Nat

take : Nat -> Stream a -> List a
take Z xs = Nil
take (S k) (x :: xs) = List.(::) x (take k xs)


text:
module Control.Monad.Free

import Control.MonadRec
import Data.Fuel
import Data.TCQueue

%default total

||| The identity function specialized to `Type`.
public export
I : Type -> Type
I t = t

mutual
  ||| A stack safe free monad implementation
  ||| storing sequences of bind operations in
  ||| an efficient type aligned catenable list.
  public export
  data Free : (f : Type -> Type) -> (a : Type) -> Type where
    MkFree :  {0 t : _}
           -> (view : FreeView f t)
           -> (arrs : Arrs f t a)
           -> Free f a

  ||| A *view* on a free monad over functor `f`, describing
  ||| it either as a pure value, or a lifted value of
  ||| type `f a` followed by a bind operation.
  public export
  data FreeView : (f : Type -> Type) -> (a : Type) -> Type where
    Pure : (val : a) -> FreeView f a
    Bind : (f b) -> (b -> Free f a) -> FreeView f a

  ||| A type aligned sequence of bind operations
  ||| over `Free f`.
  public export
  0 Arrs : (f : Type -> Type) -> (a,b : Type) -> Type
  Arrs = TCQueue . Free

||| Converts a view to the corresponding free monad. O(1).
export %inline
fromView : FreeView f a -> Free f a
fromView f = MkFree f empty

concatF : Free f a -> Arrs f a b -> Free f b
concatF (MkFree v r) l = MkFree v (r ++ l)

||| Converts a free monad to a view representing it.
||| Amortized O(1).
export
toView : Free f a -> FreeView f a
toView (MkFree v s) = case v of
  Pure val => case uncons s of
    EmptyV   => Pure val
    (h :| t) => assert_total $ toView (concatF (h val) t)

  Bind x k => Bind x (\va => concatF (k va) s)

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

bind : Free f a -> (a -> Free f b) -> Free f b
bind (MkFree v r) g = MkFree v $ snoc r g

public export
Functor (Free f) where
  map g fr = bind fr (fromView . Pure . g)

public export
Applicative (Free f) where
  pure = fromView . Pure
  f <*> v = bind f (\f => map (f $) v)

public export %inline
Monad (Free f) where
  (>>=) = bind

public export
MonadRec (Free f) where
  tailRecM seed vst (Access rec) step = do
    Cont s2 prf vst2 <- step seed vst
      | Done v => pure v
    tailRecM s2 vst2 (rec s2 prf) step

||| Lift an arbitrary functor into a free monad.
export
lift : f a -> Free f a
lift v = fromView (Bind v pure)

export
HasIO m => HasIO (Free m) where
  liftIO = lift . liftIO

--------------------------------------------------------------------------------
--          Running Computations
--------------------------------------------------------------------------------

export
wrap : f (Free f a) -> Free f a
wrap x = fromView (Bind x id)

export
substFree : (forall x . f x -> Free g x) -> Free f a -> Free g a
substFree k f = case toView f of
  Pure a   => pure a
  Bind g i => assert_total $ bind (k g) (substFree k . i)

||| Unwraps a single layer of `f`, providing the continuation.
||| Amortized O(1).
export
resume' :  (forall b. f b -> (b -> Free f a) -> r)
        -> (a -> r)
        -> Free f a
        -> r
resume' k j fr = case toView fr of
  Pure a   => j a
  Bind g i => k g i

||| Unwraps a single layer of the functor `f`.
||| Amortized O(1).
export
resume : Functor f => Free f a -> Either (f (Free f a)) a
resume fr = case toView fr of
  Pure a   => Right a
  Bind g i => Left $ map i g

||| Apply a morphism to change a free monad's functor.
export
mapK : (f : forall t . m t -> n t) -> Free m a -> Free n a
mapK f = substFree (lift . f)

||| Run a computation described as a free monad in
||| a stack safe manner.
export
foldMap : MonadRec m => (forall x . f x -> m x) -> Free f a -> m a
foldMap k fr = assert_total $ trSized forever fr $ \fu,frm => case fu of
  More x => case toView frm of
    Pure val => Done <$> pure val
    Bind g i => Cont x (reflexive {rel = LTE}) . i <$> k g
  Dry    => idris_crash "Control.Monad.Free.foldFree: ran out of fuel"

||| Run a pure computation in a stack-safe manner.
export
run : Free I a -> a
run fr = case toView fr of
  Pure a   => a
  Bind v f => run (assert_smaller fr $ f v)

export
runM : Functor m => MonadRec n =>
       (m (Free m a) -> n (Free m a)) -> Free m a -> n a
runM g free = assert_total $ trSized forever free $ \fu,fr => case fu of
  More x => case resume fr of
    Right va => pure (Done va)
    Left  ma => Cont x (reflexive {rel = LTE}) <$> g ma
  Dry    => idris_crash "Control.Monad.Free.runM: ran out of fuel"


text:
module IgnoreDo

bound : Maybe () -> Maybe b -> Maybe b
bound m n = do
  x <- m
  let y = Z
  n

ignored : Maybe () -> Maybe b -> Maybe b
ignored m n = do
  _ <- m
  let _ = Z
  n

seqd : Maybe () -> Maybe b -> Maybe b
seqd m n = do
  m
  n


text:
module OTP

data Bit : Type where
    ZeroBit : Bit
    OneBit : Bit

xor : Bit -> Bit -> Bit
xor ZeroBit ZeroBit = ZeroBit
xor ZeroBit OneBit = OneBit
xor OneBit ZeroBit = OneBit
xor OneBit OneBit = ZeroBit

data BitVector : Nat -> Type where
    Nil : BitVector Z
    Cons : Bit -> BitVector n -> BitVector (S n)
%name BitVector xs, ys -- This is unimportant, just gives Idris hints for automatically making variable names.

-- this represents the empty bit vector
emptyBitVect : BitVector Z
emptyBitVect = Nil

-- this represents the bits 101
aBitVect : BitVector 3
aBitVect = Cons OneBit (Cons ZeroBit (Cons OneBit Nil))

-- this represents the bits 110
anotherBitVect : BitVector 3
anotherBitVect = Cons OneBit (Cons OneBit (Cons ZeroBit Nil))

bitwiseXor : (n : Nat) -> BitVector n -> BitVector n -> BitVector n
bitwiseXor Z [] [] = []
bitwiseXor (S k) (Cons x xs) (Cons y ys) = Cons (xor x y) (bitwiseXor k xs ys)

otpEncrypt : (n : Nat) -> (message : BitVector n) -> (key : BitVector n) -> BitVector n
otpEncrypt n message key = bitwiseXor n message key

otpDecrypt : (n : Nat) -> (cipherText : BitVector n) -> (key : BitVector n) -> BitVector n
otpDecrypt n cipherText key = bitwiseXor n cipherText key

total xorCancel : (x : Bit) -> (y : Bit) -> xor (xor x y) y = x
xorCancel ZeroBit ZeroBit = Refl
xorCancel ZeroBit OneBit = Refl
xorCancel OneBit ZeroBit = Refl
xorCancel OneBit OneBit = Refl

total
otpCorrect : (n : Nat) -> (msg : BitVector n) -> (ky : BitVector n) -> otpDecrypt n (otpEncrypt n msg ky) ky = msg
otpCorrect Z [] [] = Refl
otpCorrect (S n) (Cons m ms) (Cons k ks) =
    let xor_eq = xorCancel m k in
    rewrite xor_eq in
    let ih = otpCorrect n ms ks in
    rewrite ih in
    Refl


text:
import Data.Vect

data WordState : (guessesRemaining : Nat) -> (letters : Nat) -> Type where
  MkWordState : (word : String) -> (missing : Vect letters Char) -> WordState guessesRemaining letters

data Finished : Type where
  Lost : (game : WordState 0 (S letters)) -> Finished
  Won  : (game : WordState (S guesses) 0) -> Finished

readSingleChar : IO (Maybe Char)
readSingleChar = [| head' (unpack <$> getLine) |]

--readSingleChar = do
--  line <- getLine
--  pure (head' (unpack line))

game : WordState (S guesses) (S letters) -> IO Finished
game state@(MkWordState word missing) = do
  char <- getLine
  Just guessedChar <- readSingleChar
        | Nothing => putSrlLn >>= ?h --game state
  ?rest


text:
module Network.TLS.Parse.DER

import Data.List1
import Data.Bits
import Data.Vect
import Utils.Bytes
import Utils.Parser
import Network.TLS.Parsing
import Utils.Misc
import public Utils.Time

import Debug.Trace

public export
data TagType : Type where
  Universal : TagType
  Application : TagType
  ContextSpecific : TagType
  Private : TagType

public export
Show TagType where
  show Universal       = "Universal"
  show Application     = "Application"
  show ContextSpecific = "ContextSpecific"
  show Private         = "Private"

public export
record Tag where
  constructor MkTag
  type : TagType
  tag_id : Nat

public export
Show Tag where
  show tag = "(" <+> show tag.type <+> ", " <+> show tag.tag_id <+> ")"

export
is_constructed : Bits8 -> Bool
is_constructed tag = testBit tag 5

public export
record BitArray where
  constructor MkBitArray
  padding : Nat
  bytes : List Bits8

public export
data ASN1 : TagType -> Nat -> Type where
  Boolean : Bool -> ASN1 Universal 0x01
  IntVal : Integer -> ASN1 Universal 0x02
  Bitstring : BitArray -> ASN1 Universal 0x03
  OctetString : List Bits8 -> ASN1 Universal 0x04
  Null : ASN1 Universal 0x05
  OID : List Nat -> ASN1 Universal 0x06
  PrintableString : String -> ASN1 Universal 0x13
  T61String : String -> ASN1 Universal 0x14
  IA5String : String -> ASN1 Universal 0x16
  UTF8String : String -> ASN1 Universal 0x0C
  Sequence : List (t ** n ** ASN1 t n) -> ASN1 Universal 0x10 -- 0x30 & 31
  Set : List (t ** n ** ASN1 t n) -> ASN1 Universal 0x11 -- 0x31 & 31
  UTCTime : DateTime -> ASN1 Universal 0x17
  GeneralizedTime : DateTime -> ASN1 Universal 0x18
  UnknownConstructed : (t : TagType) -> (n : Nat) -> List (t ** n ** ASN1 t n) -> ASN1 t n
  UnknownPrimitive : (t : TagType) -> (n : Nat) -> List Bits8 -> ASN1 t n

public export
Eq BitArray where
  (MkBitArray a b) == (MkBitArray c d) = (a == c) && (b == d)

export
constraint_parse : (Cons (Posed Bits8) i, Monoid i) => (n : Nat) ->
                   (pser : Parser i (SimpleError String) a) ->
                   Parser i (SimpleError String) (List a)
constraint_parse Z pser = pure []
constraint_parse (S len) pser = go (S len) pser
  where
  go : Nat -> Parser i (SimpleError String) a -> Parser i (SimpleError String) (List a)
  go Z (Pure leftover x) = pure [x]
  go (S i) (Pure leftover x) = (x ::) <$> go (S i) pser
  go i (Fail msg) = fail msg
  go Z parser = fail $ msg $ "under fed, want more"
  go (S i) parser = do
    b <- token
    go i (feed (singleton b) parser)

export
parse_length : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) Nat
parse_length = do
  b <- p_get
  let b' = b .&. 0x7F
  if b' == b
     then pure $ cast b
     else p_nat (cast b')

extract_tag_type_bits : Bits8 -> TagType
extract_tag_type_bits x =
  case get_bits x of
    [ False, False ] => Universal
    [ False, True  ] => Application
    [ True,  False ] => ContextSpecific
    [ True,  True  ] => Private
  where
    get_bits : Bits8 -> Vect 2 Bool
    get_bits x = [ (testBit x 7), (testBit x 6) ]

export
parse_tag_id : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) (Bool, Tag)
parse_tag_id = do
  b <- p_get
  let construct = is_constructed b
  let type = extract_tag_type_bits b
  let id = b .&. 31
  if id == 31
    then (\x => (construct, MkTag type x)) <$> parse_length
    else pure (construct, MkTag type $ cast id)

export
signed_be_to_integer : List1 Bits8 -> Integer
signed_be_to_integer l@(x ::: xs) =
  let is_neg = testBit x 7
      v = be_to_integer l
      m = (shiftL 1 (8 * (length l))) - 1 -- 2^n - 1
  in if is_neg then v .|. (complement m) else v

export
decode_oid_nodes : Bits8 -> List Bits8 -> List Nat
decode_oid_nodes first_node nodes =
  let a = first_node `div` 40
      b = first_node `mod` 40
      (_, result) = foldl go (0, []) nodes
      nodes = cast a :: cast b :: reverse result
  in integerToNat <$> nodes
  where
    go : (Integer, List Integer) -> Bits8 -> (Integer, List Integer)
    go (value, result) byte =
      let value = (shiftL value 7) .|. cast (byte .&. 0x7F)
      in if byte >= 0x80 then (value, result) else (0, value :: result)

export
parse_boolean : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) Bool
parse_boolean 1 = map (/= 0) p_get
parse_boolean n = fail $ msg $ "boolean length should be 1, got: " <+> show n

export
parse_integer : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) Integer
parse_integer n = do
  bits <- count n p_get
  case fromList $ toList bits of
    Just x => pure $ signed_be_to_integer x
    Nothing => fail $ msg "integer length is 0"

export
parse_bitarray : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) BitArray
parse_bitarray Z = fail $ msg "bitarray length is 0"
parse_bitarray (S n) = do
  pad_len <- p_get
  bits <- toList <$> count n p_get
  pure $ MkBitArray (cast pad_len) bits

export
parse_null : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) ()
parse_null Z = pure ()
parse_null n = fail $ msg $ "null length should be 0, got: " <+> show n

export
parse_oid : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) (List Nat)
parse_oid Z = fail $ msg "oid length is 0"
parse_oid (S n) = do
  first_node <- p_get
  nodes <- toList <$> count n p_get
  pure $ decode_oid_nodes first_node nodes

export
parse_time : (Cons (Posed Bits8) i, Monoid i) => Nat -> (String -> Either String DateTime) -> Parser i (SimpleError String) DateTime
parse_time len f = do
  str <- count len p_get
  case f $ ascii_to_string $ toList str of
    Right datetime => pure datetime
    Left err => fail $ msg err

export
parse_utf8 : (Cons (Posed Bits8) i, Monoid i) => Nat -> Parser i (SimpleError String) String
parse_utf8 len = do
  str <- count len p_get
  case utf8_decode $ toList str of
    Just str => pure str
    Nothing => fail $ msg "invalid utf8 string"

public export
ASN1Token : Type
ASN1Token = (t ** n ** ASN1 t n)

export
extract_string : ASN1Token -> Maybe String
extract_string (Universal ** 12 ** UTF8String b) = Just b
extract_string (Universal ** 19 ** PrintableString b) = Just b
extract_string (Universal ** 20 ** T61String b) = Just b
extract_string (Universal ** 22 ** IA5String b) = Just b
extract_string _ = Nothing

export
extract_epoch : ASN1Token -> Maybe Integer
extract_epoch (Universal ** 23 ** UTCTime time) = Just $ datetime_to_epoch time
extract_epoch (Universal ** 24 ** GeneralizedTime time) = Just $ datetime_to_epoch time
extract_epoch _ = Nothing

export
parse_asn1 : (Monoid i, Cons (Posed Bits8) i) => Parser i (SimpleError String) ASN1Token
parse_asn1 = do
  tag' <- parse_tag_id
  len <- parse_length
  case tag' of
    (False, MkTag Universal 1) => (\b => (Universal ** 1 ** Boolean b)) <$> parse_boolean len
    (False, MkTag Universal 2) => (\b => (Universal ** 2 ** IntVal b)) <$> parse_integer len
    (False, MkTag Universal 3) => (\b => (Universal ** 3 ** Bitstring b)) <$> parse_bitarray len
    (False, MkTag Universal 4) => (\b => (Universal ** 4 ** OctetString $ toList b)) <$> count len p_get
    (False, MkTag Universal 5) => (\b => (Universal ** 5 ** Null)) <$> parse_null len
    (False, MkTag Universal 6) => (\b => (Universal ** 6 ** OID b)) <$> parse_oid len
    (False, MkTag Universal 12) => (\b => (Universal ** 12 ** UTF8String b)) <$> parse_utf8 len
    (False, MkTag Universal 19) => (\b => (Universal ** 19 ** PrintableString $ ascii_to_string $ toList b)) <$> count len p_get
    (False, MkTag Universal 20) => (\b => (Universal ** 20 ** T61String $ ascii_to_string $ toList b)) <$> count len p_get
    (False, MkTag Universal 22) => (\b => (Universal ** 22 ** IA5String $ ascii_to_string $ toList b)) <$> count len p_get
    (False, MkTag Universal 23) => (\b => (Universal ** 23 ** UTCTime b)) <$> parse_time len parse_utc_time
    (False, MkTag Universal 24) => (\b => (Universal ** 24 ** GeneralizedTime b)) <$> parse_time len parse_generalized_time
    (True,  MkTag Universal 16) => (\b => (Universal ** 16 ** Sequence b)) <$> constraint_parse len parse_asn1
    (True,  MkTag Universal 17) => (\b => (Universal ** 17 ** Set b)) <$> constraint_parse len parse_asn1
    (True,  MkTag t n) => (\b => (t ** n ** UnknownConstructed t n b)) <$> constraint_parse len parse_asn1
    (False, MkTag t n) => (\b => (t ** n ** UnknownPrimitive t n $ toList b)) <$> count len p_get


text:
Shape : Nat -> Type
Shape n = Vect n Nat

Vector : Shape n -> Type -> Type
Vector Nil t = t
Vector (v::vs) t = Vect v (Array vs t)

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Client.Action.Login

import Client.Server
import Client.Util
import Data.Buffer
import Extra.Buffer
import Inigo.Async.Base
import Inigo.Async.Fetch
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Util.Url.Url

loginAccountCall : Server -> String -> String -> Promise ()
loginAccountCall server ns passphrase =
  do
    let url = toString (fromHostPath (host server) (accountLoginUrl ns))
    sessionBuf <- assertOk url $ request url "POST" passphrase []
    session <- liftIO $ readAll sessionBuf
    Just sessionFile <- liftIO $ inigoSessionFile
      | Nothing => reject "Login requires $INIGO_SESSION, $INIGO_HOME or $HOME dir"
    fs_writeFile sessionFile session
    log "You are logged into Inigo"
    pure ()

export
loginAccount : Server -> String -> String -> Promise ()
loginAccount =
  loginAccountCall

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Idris.CommandLine

import IdrisPaths

import Idris.Env
import Idris.Version

import Core.Name.Namespace
import Core.Options

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.Either

import System

%default total

public export
data PkgCommand
      = Build
      | Install
      | InstallWithSrc
      | MkDoc
      | Typecheck
      | Clean
      | REPL
      | Init

export
Show PkgCommand where
  show Build = "--build"
  show Install = "--install"
  show InstallWithSrc = "--install-with-src"
  show MkDoc = "--mkdoc"
  show Typecheck = "--typecheck"
  show Clean = "--clean"
  show REPL = "--repl"
  show Init = "--init"

public export
data DirCommand
      = LibDir | -- show top level package directory
         ||| Show the installation prefix
        Prefix |
        BlodwenPaths

export
Show DirCommand where
  show LibDir = "--libdir"
  show Prefix = "--prefix"
  show BlodwenPaths = "--paths"

||| Help topics
public export
data HelpTopic
  = ||| Interactive debugging topics
    HelpLogging
  | ||| The various pragmas
    HelpPragma

recogniseHelpTopic : String -> Maybe HelpTopic
recogniseHelpTopic "logging"   = pure HelpLogging
recogniseHelpTopic "pragma" = pure HelpPragma
recogniseHelpTopic _ = Nothing

||| CLOpt - possible command line options
public export
data CLOpt
  =
   ||| Only typecheck the given file
  CheckOnly |
   ||| The output file from the code generator
  OutputFile String |
   ||| Execute a given function after checking the source file
  ExecFn String |
   ||| Use a specific code generator
  SetCG String |
   ||| Pass a directive to the code generator
  Directive String |
   ||| Don't implicitly import Prelude
  NoPrelude |
   ||| Set source directory
  SourceDir String |
   ||| Set build directory
  BuildDir String |
   ||| Set output directory
  OutputDir String |
   ||| Generate profile data when compiling (backend dependent)
  Profile |
   ||| Display Idris version
  Version |
   ||| Display help text
  Help (Maybe HelpTopic) |
   ||| Suppress the banner
  NoBanner |
   ||| Run Idris 2 in quiet mode
  Quiet |
   ||| Run Idris 2 in verbose mode (cancels quiet if it's the default)
  Verbose |
   ||| Set the console width for REPL output
  ConsoleWidth (Maybe Nat) |
   ||| Whether to use color in the console output
  Color Bool |
   ||| Set the log level globally
  Logging LogLevel |
   ||| Add a package as a dependency
  PkgPath String |
   ||| List installed packages
  ListPackages |
   ||| Build or install a given package, depending on PkgCommand
  Package PkgCommand (Maybe String) |
   ||| Show locations of data/library directories
  Directory DirCommand |
   ||| The input Idris file
  InputFile String |
   ||| Whether or not to run in IdeMode (easily parsable for other tools)
  IdeMode |
   ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout)
  IdeModeSocket String |
   ||| Run as a checker for the core language TTImp
  Yaffle String |
   ||| Dump metadata from a .ttm file
  Metadata String |
   ||| Dump cases before compiling
  DumpCases String |
   ||| Dump lambda lifted defs before compiling
  DumpLifted String |
   ||| Dump ANF defs before compiling
  DumpANF String |
   ||| Dump VM code defs before compiling
  DumpVMCode String |
   ||| Run a REPL command then exit immediately
  RunREPL String |
  IgnoreMissingIPKG |
  FindIPKG |
  Timing |
  DebugElabCheck |
  AltErrorCount Nat |
   ||| Treat warnings as errors
  WarningsAsErrors |
   ||| Do not print shadowing warnings
  IgnoreShadowingWarnings |
   ||| Use SHA256 hashes to determine if a source file needs rebuilding instead
   ||| of modification time.
  HashesInsteadOfModTime |
   ||| Apply experimental heuristics to case tree generation that
   ||| sometimes improves performance and reduces compiled code
   ||| size.
  CaseTreeHeuristics |
   ||| Use incremental code generation, if the backend supports it
  IncrementalCG String |
   ||| Use whole program compilation - overrides IncrementalCG if set
  WholeProgram |
   ||| Generate bash completion info
  BashCompletion String String |
   ||| Generate bash completion script
  BashCompletionScript String |
   ||| Turn on %default total globally
  Total

||| Extract the host and port to bind the IDE socket to
export
ideSocketModeAddress : List CLOpt -> (String, Int)
ideSocketModeAddress []  = ("localhost", 38398)
ideSocketModeAddress (IdeModeSocket hp :: _) =
  let (h, p) = String.break (== ':') hp
      port = fromMaybe 38398 (portPart p >>= parsePositive)
      host = if h == "" then "localhost" else h
  in (host, port)
  where
    portPart : String -> Maybe String
    portPart p = if p == ""
                    then Nothing
                    else Just $ assert_total $ prim__strTail p
ideSocketModeAddress (_ :: rest) = ideSocketModeAddress rest

formatSocketAddress : (String, Int) -> String
formatSocketAddress (host, port) = host ++ ":" ++ show port

data OptType
  = Required String
   | Optional String
   | RequiredNat String
   | AutoNat String
   | RequiredLogLevel String

Show OptType where
  show (Required a) = "<" ++ a ++ ">"
  show (RequiredNat a) = "<" ++ a ++ ">"
  show (RequiredLogLevel a) = "<" ++ a ++ ">"
  show (Optional a) = "[" ++ a ++ "]"
  show (AutoNat a) = "<" ++ a ++ ">"

ActType : List OptType -> Type
ActType [] = List CLOpt
ActType (Required a :: as) = String -> ActType as
ActType (RequiredNat a :: as) = Nat -> ActType as
ActType (RequiredLogLevel a :: as) = LogLevel -> ActType as
ActType (Optional a :: as) = Maybe String -> ActType as
ActType (AutoNat a :: as) = Maybe Nat -> ActType as

record OptDesc where
  constructor MkOpt
  flags : List String
  argdescs : List OptType
  action : ActType argdescs
  help : Maybe String

optSeparator : OptDesc
optSeparator = MkOpt [] [] [] Nothing

showDefault : Show a => a -> String
showDefault x = "(default " ++ show x ++ ")"

options : List OptDesc
options = [MkOpt ["--check", "-c"] [] [CheckOnly]
              (Just "Exit after checking source file"),
           MkOpt ["--output", "-o"] [Required "file"] (\f => [OutputFile f, Quiet])
              (Just "Specify output file"),
           MkOpt ["--exec", "-x"] [Required "name"] (\f => [ExecFn f, Quiet])
              (Just "Execute function after checking source file"),
           MkOpt ["--no-prelude"] [] [NoPrelude]
              (Just "Don't implicitly import Prelude"),
           MkOpt ["--codegen", "--cg"] [Required "backend"] (\f => [SetCG f])
              (Just $ "Set code generator " ++ showDefault (codegen defaultSession)),
           MkOpt ["--incremental-cg", "--inc"] [Required "backend"] (\f => [IncrementalCG f])
             (Just "Incremental code generation on given backend"),
           MkOpt ["--whole-program", "--wp"] [] [WholeProgram]
             (Just "Use whole program compilation (overrides --inc)"),
           MkOpt ["--directive"] [Required "directive"] (\d => [Directive d])
              (Just $ "Pass a directive to the current code generator"),
           MkOpt ["--package", "-p"] [Required "package"] (\f => [PkgPath f])
              (Just "Add a package as a dependency"),
           MkOpt ["--source-dir"] [Required "dir"] (\d => [SourceDir d])
              (Just $ "Set source directory"),
           MkOpt ["--build-dir"] [Required "dir"] (\d => [BuildDir d])
              (Just $ "Set build directory"),
           MkOpt ["--output-dir"] [Required "dir"] (\d => [OutputDir d])
              (Just $ "Set output directory"),
           MkOpt ["--profile"] [] [Profile]
              (Just "Generate profile data when compiling, if supported"),

           optSeparator,
           MkOpt ["--total"] [] [Total]
              (Just "Require functions to be total by default"),
           MkOpt ["-Werror"] [] [WarningsAsErrors]
              (Just "Treat warnings as errors"),
           MkOpt ["-Wno-shadowing"] [] [IgnoreShadowingWarnings]
              (Just "Do not print shadowing warnings"),

           optSeparator,
           MkOpt ["-Xcheck-hashes"] [] [HashesInsteadOfModTime]
             (Just "Use SHA256 hashes instead of modification time to determine if a source file needs rebuilding"),
           MkOpt ["-Xcase-tree-opt"] [] [CaseTreeHeuristics]
              (Just "Apply experimental optimizations to case tree generation"),

           optSeparator,
           MkOpt ["--prefix"] [] [Directory Prefix]
              (Just "Show installation prefix"),
           MkOpt ["--paths"] [] [Directory BlodwenPaths]
              (Just "Show paths"),
           MkOpt ["--libdir"] [] [Directory LibDir]
              (Just "Show library directory"),
           MkOpt ["--list-packages"] [] [ListPackages]
              (Just "List installed packages"),

           optSeparator,
           MkOpt ["--init"] [Optional "package file"]
              (\ f => [Package Init f])
              (Just "Interactively initialise a new project"),

           MkOpt ["--build"] [Optional "package file"]
               (\f => [Package Build f])
              (Just "Build modules/executable for the given package"),
           MkOpt ["--install"] [Optional "package file"]
              (\f => [Package Install f])
              (Just "Install the given package"),
           MkOpt ["--install-with-src"] [Optional "package file"]
              (\f => [Package InstallWithSrc f])
              (Just "Install the given package"),
           MkOpt ["--mkdoc"] [Optional "package file"]
              (\f => [Package MkDoc f])
              (Just "Build documentation for the given package"),
           MkOpt ["--typecheck"] [Optional "package file"]
              (\f => [Package Typecheck f])
              (Just "Typechecks the given package without code generation"),
           MkOpt ["--clean"] [Optional "package file"] (\f => [Package Clean f])
              (Just "Clean intermediate files/executables for the given package"),
           MkOpt ["--repl"] [Optional "package file"] (\f => [Package REPL f])
              (Just "Build the given package and launch a REPL instance."),
           MkOpt ["--find-ipkg"] [] [FindIPKG]
              (Just "Find and use an .ipkg file in a parent directory."),
           MkOpt ["--ignore-missing-ipkg"] [] [IgnoreMissingIPKG]
              (Just "Fail silently if a dependency is missing."),

           optSeparator,
           MkOpt ["--ide-mode"] [] [IdeMode]
              (Just "Run the REPL with machine-readable syntax"),
           MkOpt ["--ide-mode-socket"] [Optional "host:port"]
                 (\hp => [IdeModeSocket $ fromMaybe (formatSocketAddress (ideSocketModeAddress [])) hp])
              (Just $ "Run the ide socket mode on given host and port " ++
                      showDefault (formatSocketAddress (ideSocketModeAddress []))),

           optSeparator,
           MkOpt ["--client"] [Required "REPL command"] (\f => [RunREPL f])
              (Just "Run a REPL command then quit immediately"),
           MkOpt ["--timing"] [] [Timing]
              (Just "Display timing logs"),

           optSeparator,
           MkOpt ["--no-banner"] [] [NoBanner]
              (Just "Suppress the banner"),
           MkOpt ["--quiet", "-q"] [] [Quiet]
              (Just "Quiet mode; display fewer messages"),
           MkOpt ["--console-width"] [AutoNat "console width"] (\l => [ConsoleWidth l])
              (Just "Width for console output (0 for unbounded) (auto by default)"),
           MkOpt ["--color", "--colour"] [] ([Color True])
              (Just "Forces colored console output (enabled by default)"),
           MkOpt ["--no-color", "--no-colour"] [] ([Color False])
              (Just "Disables colored console output"),
           MkOpt ["--verbose"] [] [Verbose]
              (Just "Verbose mode (default)"),
           MkOpt ["--log"] [RequiredLogLevel "log level"] (\l => [Logging l])
              (Just "Global log level (0 by default)"),

           optSeparator,
           MkOpt ["--version", "-v"] [] [Version]
              (Just "Display version string"),
           MkOpt ["--help", "-h", "-?"] [Optional "topic"] (\ tp => [Help (tp >>= recogniseHelpTopic)])
              (Just "Display help text"),

           -- Internal debugging options
           MkOpt ["--yaffle", "--ttimp"] [Required "ttimp file"] (\f => [Yaffle f])
              Nothing, -- run ttimp REPL rather than full Idris
           MkOpt ["--ttm" ] [Required "ttimp file"] (\f => [Metadata f])
              Nothing, -- dump metadata information from the given ttm file
           MkOpt ["--dumpcases"] [Required "output file"] (\f => [DumpCases f])
              Nothing, -- dump case trees to the given file
           MkOpt ["--dumplifted"] [Required "output file"] (\f => [DumpLifted f])
              Nothing, -- dump lambda lifted trees to the given file
           MkOpt ["--dumpanf"] [Required "output file"] (\f => [DumpANF f])
              Nothing, -- dump ANF to the given file
           MkOpt ["--dumpvmcode"] [Required "output file"] (\f => [DumpVMCode f])
              Nothing, -- dump VM Code to the given file
           MkOpt ["--debug-elab-check"] [] [DebugElabCheck]
              Nothing, -- do more elaborator checks (currently conversion in LinearCheck)
           MkOpt ["--alt-error-count"] [RequiredNat "alternative count"] (\c => [AltErrorCount c])
              (Just "Outputs errors for the given number of alternative parsing attempts."),

           optSeparator,
           -- bash completion
           MkOpt ["--bash-completion"]
                 [ Required "input"
                 , Required "previous input"]
                 (\w1,w2 => [BashCompletion w1 w2])
                 (Just "Print bash autocompletion information"),
           MkOpt ["--bash-completion-script"]
                 [ Required "function name" ]
                 (\n => [BashCompletionScript n])
                 (Just "Generate a bash script to activate autocompletion for Idris2")
           ]

optShow : OptDesc -> (String, Maybe String)
optShow (MkOpt [] _ _ _) = ("", Just "")
optShow (MkOpt flags argdescs action help) = (showSep ", " flags ++ " " ++
                                              showSep " " (map show argdescs),
                                              help)
  where
    showSep : String -> List String -> String
    showSep sep [] = ""
    showSep sep [x] = x
    showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

firstColumnWidth : Nat
firstColumnWidth = let maxOpt = foldr max 0 $ map (length . fst . optShow) options
                       maxEnv = foldr max 0 $ map (length . .name) envs in
                       max maxOpt maxEnv

makeTextFromOptionsOrEnvs : List (String, Maybe String) -> String
makeTextFromOptionsOrEnvs rows = concatMap (optUsage firstColumnWidth) rows
  where
    optUsage : Nat -> (String, Maybe String) -> String
    optUsage maxOpt (optshow, help) = maybe ""  -- Don't show anything if there's no help string (that means
                                                -- it's an internal option)
                                      (\h => "  " ++ optshow ++
                                             pack (List.replicate (minus (maxOpt + 2) (length optshow)) ' ') ++
                                             h ++ "\n")
                                      help

optsUsage : String
optsUsage = makeTextFromOptionsOrEnvs $ map optShow options

envsUsage : String
envsUsage = makeTextFromOptionsOrEnvs $ map (\e => (e.name, Just e.help)) envs

export
versionMsg : String
versionMsg = "Idris 2, version " ++ show version

export
usage : String
usage = versionMsg ++ "\n" ++
        "Usage: idris2 [options] [input file]\n\n" ++
        "Available options:\n" ++
        optsUsage ++
        "\n" ++
        "Environment variables:\n" ++
        envsUsage

checkNat : Integer -> Maybe Nat
checkNat n = toMaybe (n >= 0) (integerToNat n)

processArgs : String -> (args : List OptType) -> List String -> ActType args ->
              Either String (List CLOpt, List String)
processArgs flag [] xs f = Right (f, xs)
-- Missing required arguments
processArgs flag (opt@(Required _) :: as) [] f =
  Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
processArgs flag (opt@(RequiredNat _) :: as) [] f =
  Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
processArgs flag (opt@(RequiredLogLevel _) :: as) [] f =
  Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
processArgs flag (Optional a :: as) [] f =
  processArgs flag as [] (f Nothing)
processArgs flag (opt@(AutoNat _) :: as) [] f =
  Left $ "Missing required argument " ++ show opt ++ " for flag " ++ flag
-- Happy cases
processArgs flag (RequiredNat a :: as) (x :: xs) f =
  do arg <- maybeToEither ("Expected Nat argument " ++ show x ++ " for flag " ++ flag)
                          (parseInteger x >>= checkNat)
     processArgs flag as xs (f arg)
processArgs flag (RequiredLogLevel a :: as) (x :: xs) f =
  do arg <- maybeToEither ("Expected LogLevel argument " ++ show x ++ " for flag " ++ flag)
                          (parseLogLevel x)
     processArgs flag as xs (f arg)
processArgs flag (AutoNat a :: as) ("auto" :: xs) f =
  processArgs flag as xs (f Nothing)
processArgs flag (AutoNat a :: as) (x :: xs) f =
  do arg <- maybeToEither ("Expected Nat or \"auto\" argument " ++ show x ++ " for flag " ++ flag)
                          (parseInteger x >>= checkNat)
     processArgs flag as xs (f (Just arg))
processArgs flag (Required a :: as) (x :: xs) f =
  processArgs flag as xs (f x)
processArgs flag (Optional a :: as) (x :: xs) f =
  processArgs flag as xs (f $ toMaybe (not (isPrefixOf "-" x)) x)

matchFlag : (d : OptDesc) -> List String ->
            Either String (Maybe (List CLOpt, List String))
matchFlag d [] = Right Nothing -- Nothing left to match
matchFlag d (x :: xs)
    = if x `elem` flags d
         then do args <- processArgs x (argdescs d) xs (action d)
                 Right (Just args)
         else Right Nothing

findMatch : List OptDesc -> List String ->
            Either String (List CLOpt, List String)
findMatch [] [] = Right ([], [])
findMatch [] (f :: args) = Right ([InputFile f], args)
findMatch (d :: ds) args
    = case !(matchFlag d args) of
           Nothing => findMatch ds args
           Just res => Right res

parseOpts : List OptDesc -> List String -> Either String (List CLOpt)
parseOpts opts [] = Right []
parseOpts opts args
   = do (cl, rest) <- findMatch opts args
        cls <- assert_total (parseOpts opts rest) -- 'rest' smaller than 'args'
        pure (cl ++ cls)

export
getOpts : List String -> Either String (List CLOpt)
getOpts opts = parseOpts options opts

export covering
getCmdOpts : IO (Either String (List CLOpt))
getCmdOpts = do (_ :: opts) <- getArgs
                    | _ => pure (Left "Invalid command line")
                pure $ getOpts opts

||| List of all command line option flags.
export
optionFlags : List String
optionFlags = options >>= flags


text:
module Main

import System
import CIO
import Idrlisp
import Idrlib
import Idrboot
import TestRunner

%default covering
%language TypeProviders
%provide (bootCode : String) with readBootCode

liftFileIO : IO (Either FileError a) -> CIO String a
liftFileIO x =
  case !(lift x) of
    Right r => pure r
    Left e => throw $ show e

parseAndEvalProgram : Context -> String -> String -> CIO String Value
parseAndEvalProgram ctx name input = do
  let label = name ++ ": "
  program <-
    case parseProgram input of
      Right program => pure program
      Left err => throw $ name ++ ": " ++ err
  result <- lift $ evalProgram ctx program
  case result of
    Right value => pure value
    Left (index, err) => throw $ name ++ "[" ++ show index ++ "]: " ++ err

parseAndEvalFiles : Context -> List String -> CIO String ()
parseAndEvalFiles ctx [] = pure ()
parseAndEvalFiles ctx (file :: files) = do
  input <- liftFileIO $ readFile file
  _ <- parseAndEvalProgram ctx file input
  parseAndEvalFiles ctx files

runRepl : Context -> CIO String ()
runRepl ctx =
  do
    lift $ fPutStrLn stderr "[idrlisp REPL]"
    loop repl
  where
    loop : Monad m => m Bool -> m ()
    loop m = if !m then pure () else loop m

    repl : CIO String Bool
    repl = do
      lift $ fPutStr stderr "> "
      lift $ fflush stderr
      input <- liftFileIO $ fGetLine stdin
      if input == "" then
        pure True
      else do
        result <- (Right <$> parseAndEvalProgram ctx "<stdin>" input) `catch` (pure . Left)
        case result of
          Right r => lift $ showIO r >>= putStrLn
          Left err => ignore $ lift $ fPutStrLn stderr err
        pure False

initContext : List String -> Bool -> CIO String Context
initContext args boot = do
  builtins <- lift $ initIdrlib args
  ctx <- lift $ newContext builtins
  when boot $ ignore $ parseAndEvalProgram ctx "init" bootCode
  pure ctx

main : IO ()
main =
  case !(runCIO $ handleArgs !getArgs) of
    Right () => pure ()
    Left err => do
      fPutStrLn stderr err
      exit 1
  where
    splitArgs : List String -> (List String, List String)
    splitArgs args =
      case splitOn "--" args of
        xs :: xss => (xs, concat $ intersperse ["--"] xss)
        [] => ([], [])

    handleArgs : List String -> CIO String ()
    handleArgs [_] = do
      ctx <- initContext [] True
      runRepl ctx
    handleArgs [_, "-test", test] = do
      ctx <- initContext [] False
      fh <- liftFileIO $ openFile test Read
      testResult <- lift $ TestRunner.run ctx fh
      case testResult of
        Left err => throw err
        Right Z => pure ()
        Right fails => throw $ "Total " ++ show fails ++ " tests failed."
    handleArgs (_ :: args) = do
      let (files, lispArgs) = splitArgs args
      ctx <- initContext lispArgs True
      parseAndEvalFiles ctx files
    handleArgs _ = pure ()

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 5

import System
import Data.Vect

-- check that all functions are total
%default total

--
-- section 5.1
--

printLonger : IO ()
printLonger = do putStr "First string: "
                 str1 <- getLine
                 putStr "Second string: "
                 str2 <- getLine
                 putStrLn $ show (longer str1 str2)
              where
                   longer : String -> String -> Nat
                   longer s1 s2 = max (length s1) (length s2)

printLonger' : IO ()
printLonger' =  putStr "First string: " >>= \_ =>
                getLine >>= \str1 =>
                putStr "Second string: " >>= \_ =>
                getLine >>= \str2 =>
                putStrLn $ show (longer str1 str2)
             where
                  longer : String -> String -> Nat
                  longer s1 s2 = max (length s1) (length s2)

--
-- section 5.2
--

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

partial
guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses =
  do
    putStr "Enter a number: "
    Just try <- readNumber
  | Nothing => (do putStrLn "wrong number"
                   guess target guesses)
    case compare try target of
          LT => (do putStrLn "too small"
                    guess target (S guesses))
          GT => (do putStrLn "too big"
                    guess target (S guesses))
          EQ => putStrLn ("you win in " ++ show guesses ++ " tries!")

partial
random : Nat -> IO Nat
random k = do raw <- time
              pure $ mod (fromIntegerNat . abs $ raw) k

partial
main : IO ()
main = random 100 >>= (flip guess) 1
-- or:
-- main = do target <- random 100
--           guess target 1

-- can be tested using:
-- > :exec test_repl
-- command: foo
-- 0> foo!
-- command: bar
-- 1> bar!
-- command: quit
-- >
partial
my_replWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()
my_replWith state invite f =
  do putStr invite
     input <- getLine
     Just (output, state') <- pure (f state input)
   | Nothing => pure ()
     putStr output
     my_replWith state' invite f

partial
my_repl : String -> (String -> String) -> IO ()
my_repl invite f = my_replWith () invite f'
  where
    f' : a -> String -> Maybe (String, a)
    f' state input = Just (f input, state)

partial
test_repl : IO ()
test_repl = my_replWith 0
                        "command: "
                        (\s,x => if x=="quit"
                                  then Nothing
                                  else Just ((show s) ++ "> " ++ x ++ "!\n", S s))

--
-- section 5.3
--

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

partial
run_readToBlank : IO ()
run_readToBlank = do
                    lines <- readToBlank
                    putStrLn $ show lines

-- version that concat lines and write them at once using writeFile
-- (writeFile opens the file in WriteTruncate mode, writes, and then closes the file)
partial
readAndSave : IO ()
readAndSave = do
               putStrLn "Enter lines: "
               lines <- readToBlank
               putStr "Filename: "
               filename <- getLine
               Right () <- writeFile filename (concat $ intersperse "\n" lines)
             | Left error => putStrLn (show error)
               putStrLn $ "lines saved to file " ++ filename

writeLinesToFile : (file : File) ->
                   (lines : List String) ->
                   IO (Either FileError ())
writeLinesToFile file [] = pure (Right ())
writeLinesToFile file (x :: xs)
  = do
      line <- pure (if isNil xs then x else x ++ "\n")
      Right () <- fPutStr file line | Left error => pure (Left error)
      writeLinesToFile file xs

-- version that writes lines one by one
-- (fPutStrLn writes a single line)
partial
readAndSave2 : IO ()
readAndSave2 = do
               putStrLn "Enter lines: "
               lines <- readToBlank
               putStr "Filename: "
               filename <- getLine
               Right file <- openFile filename WriteTruncate
             | Left error => putStrLn (show error)
               Right () <- writeLinesToFile file lines
             | Left error => putStrLn (show error)
               closeFile file
               putStrLn $ "lines saved to file " ++ filename

partial
readVectFileHelper : (file : File) -> IO (Either FileError (n ** Vect n String))
readVectFileHelper file
  = do
      False <- fEOF file | True => pure (Right (_ ** []))
      Right x <- fGetLine file | Left error => pure (Left error)
      Right (m ** xs) <- readVectFileHelper file | Left error => pure (Left error)
      pure $ Right (S m ** x :: xs)

partial
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename
  = do
       Right file <- openFile filename Read
     | Left error => (do putStrLn (show error)
                         pure (_ ** []))
       Right dp <- readVectFileHelper file
     | Left error => (do putStrLn (show error)
                         pure (_ ** []))
       closeFile file
       pure dp

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Extra.GLFW.FFI

import public Extra.C.Types

public export
libglfw : String -> String
libglfw f = "C:" <+> f <+> ",libglfw"


text:
import CommonTestingStuff
import Program

export
main : IO Unit
main = do
  putStrLn beforeString
  runCoop program
  putStrLn "after coop"


text:
module Prims

x : Int
x = 42

foo : String
foo = "Sausage machine"

bar : Char
bar = 'Z'

quux : Bool
quux = False

max_stars_repo_name: aztecrex/try-idris

max_issues_repo_name: aztecrex/try-idris

max_forks_repo_name: aztecrex/try-idris


text:
module DepSec.Poset

%access public export
%default total
%hide Prelude.Monad.join

||| Verified partial ordering
interface Poset a where
  leq           : a -> a -> Type
  reflexive     : (x : a) -> x `leq` x
  antisymmetric : (x, y : a) -> x `leq` y -> y `leq` x -> x = y
  transitive    : (x, y, z : a) -> x `leq` y -> y `leq` z -> x `leq` z

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module ConcurrentImp

import Expr
import Logic
import Maps
import SmallStepExpr

%access public export

%default total

data Com : Type where
  CSkip : Com
  CAss : Id -> AExp -> Com
  CSeq : Com -> Com -> Com
  CIf : BExp -> Com -> Com -> Com
  CWhile : BExp -> Com -> Com
  CPar : Com -> Com -> Com

SKIP : Com
SKIP = CSkip

infix 5 ::=

(::=) : Id -> AExp -> Com
(::=) = CAss

(>>=) : Com -> (() -> Com) -> Com
(>>=) c f = CSeq c (f ())

WHILE : BExp -> Com -> Com
WHILE = CWhile

syntax IFB [b] THEN [c1] ELSE [c2] FI = CIf b c1 c2

syntax PAR [c1] WITH [c2] END = CPar c1 c2

data CStep : (Com, State) -> (Com, State) -> Type where
  CS_AssStep : AStep st a a' -> CStep (i ::= a, st) (i ::= a', st)
  CS_Ass : CStep (i ::= ANum n, st) (SKIP, t_update i n st)
  CS_SeqStep : CStep (c1, st) (c1', st') ->
               CStep ((do c1; c2), st) ((do c1'; c2), st')
  CS_SeqFinish : CStep ((do SKIP; c2), st) (c2, st)
  CS_IfStep : BStep st b b' -> CStep (CIf b c1 c2, st) (CIf b' c1 c2, st)
  CS_IfTrue : CStep (CIf BTrue c1 c2, st) (c1, st)
  CS_IfFalse : CStep (CIf BFalse c1 c2, st) (c2, st)
  CS_While : CStep (WHILE b c, st) (CIf b (do c; WHILE b c) SKIP, st)
  CS_Par1 : CStep (c1, st) (c1', st') ->
            CStep (CPar c1 c2, st) (CPar c1' c2, st')
  CS_Par2 : CStep (c2, st) (c2', st') ->
            CStep (CPar c1 c2, st) (CPar c1 c2', st')
  CS_ParDone : CStep (CPar SKIP SKIP, st) (SKIP, st)

CMultiStep : Relation (Com, State)
CMultiStep = Multi CStep

syntax [t] "/" [st] "-+>*" [t'] "/" [st'] = Multi CStep (t, st) (t', st')

par_loop : Com
par_loop =
  PAR
    Y ::= 1
  WITH
    WHILE (Y == 0) $ do
      X ::= X + 1
  END

par_loop_example_0 : (st' : State ** ( ConcurrentImp.par_loop / Expr.empty_state
                                       -+>* SKIP / st'
                                     , st' X = 2 ))
par_loop_example_0 = (updatedState ** (execution, Refl))
where updatedState : State
      updatedState = t_update Y 1 $
                     t_update X 2 $
                     t_update X 1 $
                     empty_state
      execution : CMultiStep (ConcurrentImp.par_loop, Expr.empty_state)
                             (SKIP, updatedState)
      execution = MultiStep (CS_Par2 CS_While) $
                  MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
                  MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
                  MultiStep (CS_Par2 CS_IfTrue) $
                  MultiStep (CS_Par2
                              (CS_SeqStep (CS_AssStep (AS_Plus1 AS_Id)))) $
                  MultiStep (CS_Par2 (CS_SeqStep (CS_AssStep AS_Plus))) $
                  MultiStep (CS_Par2 (CS_SeqStep CS_Ass)) $
                  MultiStep (CS_Par2 CS_SeqFinish) $
                  MultiStep (CS_Par2 CS_While) $
                  MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
                  MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
                  MultiStep (CS_Par2 CS_IfTrue) $
                  MultiStep (CS_Par2
                              (CS_SeqStep (CS_AssStep (AS_Plus1 AS_Id)))) $
                  MultiStep (CS_Par2 (CS_SeqStep (CS_AssStep AS_Plus))) $
                  MultiStep (CS_Par2 (CS_SeqStep CS_Ass)) $
                  MultiStep (CS_Par2 CS_SeqFinish) $
                  MultiStep (CS_Par1 CS_Ass) $
                  MultiStep (CS_Par2 CS_While) $
                  MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
                  MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
                  MultiStep (CS_Par2 CS_IfFalse) $
                  MultiStep CS_ParDone $
                  MultiRefl

par_body_n__Sn : (n : Nat) -> (st : State) -> (st X = n, st Y = 0) ->
                 ConcurrentImp.par_loop / st -+>*
                 ConcurrentImp.par_loop / (t_update X (S n) st)
par_body_n__Sn n st (x_prf, y_prf) =
  MultiStep (CS_Par2 CS_While) $
  MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
  rewrite y_prf in
  MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
  MultiStep (CS_Par2 CS_IfTrue) $
  MultiStep (CS_Par2
              (CS_SeqStep (CS_AssStep (AS_Plus1 AS_Id)))) $
  MultiStep (CS_Par2 (CS_SeqStep (CS_AssStep AS_Plus))) $
  MultiStep (CS_Par2 (CS_SeqStep CS_Ass)) $
  MultiStep (CS_Par2 CS_SeqFinish) $
  rewrite plusCommutative (st X) 1 in
  rewrite x_prf in
  MultiRefl

par_body_any_X_helper : (n : Nat) ->
                        (  st' : State
                        ** ( ConcurrentImp.par_loop / Expr.empty_state
                             -+>* ConcurrentImp.par_loop / st'
                           , st' X = n
                           , st' Y = 0 ))
par_body_any_X_helper Z = (empty_state ** (MultiRefl, Refl, Refl))
par_body_any_X_helper (S k) =
  let (st ** (s, x_prf, y_prf)) = par_body_any_X_helper k
  in (  t_update X (S k) st
     ** ( multi_trans s $
          MultiStep (CS_Par2 CS_While) $
          MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
          MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
          rewrite y_prf in
          MultiStep (CS_Par2 CS_IfTrue) $
          MultiStep (CS_Par2
                      (CS_SeqStep (CS_AssStep (AS_Plus1 AS_Id)))) $
          MultiStep (CS_Par2 (CS_SeqStep (CS_AssStep AS_Plus))) $
          MultiStep (CS_Par2 (CS_SeqStep CS_Ass)) $
          MultiStep (CS_Par2 CS_SeqFinish) $
          rewrite plusCommutative (st X) 1 in
          rewrite x_prf in
          MultiRefl
        , Refl
        , y_prf ))

par_body_any_X : (n : Nat) ->
                 (st' : State ** ( ConcurrentImp.par_loop / Expr.empty_state
                                   -+>* SKIP / st'
                                 , st' X = n ))
par_body_any_X n =
  let (st ** (s, x_prf, _)) = par_body_any_X_helper n
  in (t_update Y 1 st ** ( multi_trans s $
                           MultiStep (CS_Par1 CS_Ass) $
                           MultiStep (CS_Par2 CS_While) $
                           MultiStep (CS_Par2 (CS_IfStep (BS_Eq1 AS_Id))) $
                           MultiStep (CS_Par2 (CS_IfStep BS_Eq)) $
                           MultiStep (CS_Par2 CS_IfFalse) $
                           MultiStep CS_ParDone $
                           MultiRefl
                         , x_prf ))


text:
import Data.Fin

foo : Fin 10
foo = 5

0 test : Fin k -> Nat
test i = k

0 baz : Nat
baz = test foo -- fine!

bar : Nat
bar = test foo -- bad!


text:
module Cam.Platform
import Cam.FFI

public export
%inline
platformName : () -> Boxed String
platformName () = believe_me . unsafePerformIO $ fcall1 "platform_name" (believe_me ())

public export
%inline
platformSystem : () -> Boxed String
platformSystem () = believe_me . unsafePerformIO $ fcall1 "platform_system" (believe_me ())

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
%default total

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

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

(>>) : IO () -> Inf (RunIO b) -> RunIO b
(>>) = Seq

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

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> RunIO a -> IO (Maybe a)
run fuel (Quit val) = do pure (Just val)
run (More fuel) (Do c f) = do res <- c
                              run fuel (f res)
run (More fuel) (Seq io k) = do io; run fuel k
run Dry p = pure Nothing

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = ignore $ run forever greet


text:
module HelloWorld

export
hello : String
hello = "Goodbye, Mars!"

export
version : String
version = "1.0.0"