text:
||| This module contains an adaptation of the session description language as presented in:
|||
|||     <https://dblp.uni-trier.de/rec/html/journals/corr/abs-1904-01288>
|||
||| This implementation differs from the original in that recursive
||| calls and calling of subprograms are achieved using standard idris
||| constructs. To support his natively in resources, one will need to
||| introduce new primitives. As described in the `Resources` paper,
||| however, this requires that now means to reason about the
||| interaction between the type-level state of the caller and callee
||| programs. It would not be correct to assume anything about said
||| interaction with the framework in its current form.
|||
||| Furthermore, as described in the `Resources` paper, there is no
||| handler program to provide projection capabilities.
module Example.Sessions

import Data.List

import Resources

%access public export
%default total

{- [ Actors]

Here we define actors/roles in a session description, ensuring that we have a means to compare them.

-}
data Actor = MkActor String

Eq Actor where
 (==) (MkActor a) (MkActor b) = a == b

actorNotEqual : ((x = y) -> Void) -> (MkActor x = MkActor y) -> Void
actorNotEqual f Refl = f Refl

actorDecEq : (x,y : Actor) -> Dec (x = y)
actorDecEq (MkActor x) (MkActor y) with (decEq x y)
  actorDecEq (MkActor y) (MkActor y) | (Yes Refl) = Yes Refl
  actorDecEq (MkActor x) (MkActor y) | (No contra) = No (actorNotEqual contra)

DecEq Actor where
  decEq = actorDecEq

Ord Actor where
  compare (MkActor a) (MkActor b) = compare a b

-- Here we describe our type-level states.
namespace TypeLevel

  ||| Channels are born free until they are bound.
  data Usage = Free | Bound

  ||| Variables in Sessions are either paired actors, or data types.
  data Ty = CHAN (Actor, Actor) | DATA Type

  namespace State

    ||| A channel's state is it's usage.
    record ChanState where
      constructor MkChanState
      usage : Usage

    ||| A data types state is the type of message and who has seen the message.
    record DataState where
      constructor MkDataState
      knownBy : List Actor
      type    : Type

    ||| A mapping between variable types and their abstract state.
    CalcStateType : Ty -> Type
    CalcStateType (CHAN _) = ChanState
    CalcStateType (DATA _) = DataState

namespace Predicates

  ||| A predicate to state that all the listed actors are aware of the data item.
  |||
  ||| @actors The actors who know about the item.
  ||| @var    The item the actors know about.
  ||| @item   The abstract state associated with the item.
  data AllKnow : (actors : List Actor)
              -> (var   : Var Ty (DATA type))
              -> (item  : StateItem Ty CalcStateType (DATA type))
              -> Type
     where
       NilKnows : (prf : Elem x actors)
               -> AllKnow [x] msg (MkStateItem (DATA type) msg (MkDataState actors type))
       ConsKnows : (prf : Elem x actors)
                -> (later : AllKnow xs msg (MkStateItem (DATA type) msg (MkDataState actors type)))
                -> AllKnow (x::xs) msg (MkStateItem (DATA type) msg (MkDataState actors type))

  ||| A predicate to state that the given actor knows about the provided data item.
  |||
  ||| @actor The actor who knows about the item.
  ||| @var   The item the actors know about.
  ||| @item  The abstract state associated with the item.
  data KnowsData : (actor : Actor)
                -> (var   : Var Ty (DATA type))
                -> (item  : StateItem Ty CalcStateType (DATA type))
                -> Type
    where
      DoesKnow : (prf : x = y)
              -> (prfE : Elem x actors)
              -> KnowsData y var (MkStateItem (DATA type) var (MkDataState actors type))

  ||| A type-level function to record that a particular message has been used by an actor.
  ExpandWhoKnows : (newActor : Actor)
                -> (oldState : StateItem Ty CalcStateType (DATA type))
                -> (prfState : KnowsData sender label oldState)
                -> StateItem Ty CalcStateType (DATA type)
  ExpandWhoKnows newActor (MkStateItem (DATA type) label (MkDataState actors type)) (DoesKnow Refl prfE) =
    MkStateItem (DATA type) label (MkDataState (newActor::actors) type)

  ||| Proof that the given sender and receiver are valid participants in the protocol.
  data AllowedToConnect : (sender, receiver : Actor)
                       -> (actors : List Actor)
                       -> Type where
    CanConnect : (prfSender   : Elem sender   actors)
              -> (prfReceiver : Elem receiver actors)
              -> AllowedToConnect sender receiver actors

  ||| An assertion that the given channel has the given state.
  data ChannelHasState : (assumedState : Usage)
                      -> (chan         : Var Ty (CHAN (s,r)))
                      -> (actual       : StateItem Ty CalcStateType (CHAN (s,r)))
                      -> Type
    where
      YesChanHasState : ChannelHasState state chan (MkStateItem (CHAN (s,r)) chan (MkChanState state))

  ||| A type-level function to set a channel's state.
  SetChannelState : (newState : Usage)
                 -> (oldState : StateItem Ty CalcStateType (CHAN (s,r)))
                 -> (prfState : ChannelHasState oldState' var oldState)
                 -> StateItem Ty CalcStateType (CHAN (s,r))
  SetChannelState newState (MkStateItem (CHAN (s,r)) var (MkChanState oldState')) YesChanHasState = MkStateItem (CHAN (s,r)) var (MkChanState newState)

  ||| A predicate to describe valid end states for data and connections.
  data EndState : (ty : Ty) -> StateItem Ty CalcStateType ty -> Type where
    ||| We do not care.
    EndData : EndState (DATA type)  state
    ||| Connections must be free.
    EndConn : EndState (CHAN (s,r)) (MkStateItem (CHAN (s,r)) lbl (MkChanState Free))

||| Our algebraic definition of a Session description language.
data Sessions : (participants : List Actor) -> Lang Ty CalcStateType where

  ||| Describe that the given actor `a` creates a message of type `type`.
  |||
  ||| We also need proof that the actor is allowed to participate in the description.
  NewData : (a    : Actor)
         -> (type : Type)
         -> (prf  : Elem a ps)
         -> Sessions ps (Var Ty (DATA type)) old (\lbl => MkStateItem (DATA type) lbl (MkDataState [a] type) :: old)

  ||| Describe that the given actor `a` creates a message that depends on an earlier message that `a` has seen.
  |||
  ||| The resulting message type will be a dependent pair.
  NewDataDep : (a        : Actor)
            -> (dep      : Var Ty (DATA type))
            -> (prfKnows : InContext (DATA type) (KnowsData a dep) old)
            -> (msgType  : (msg : type) -> Type)
            -> Sessions ps (Var Ty (DATA (x ** msgType x)))
                            old
                            (\lbl => MkStateItem (DATA (x ** msgType x))
                                                 lbl
                                                 (MkDataState [a] (x ** msgType x)) :: old)

  ||| Specify a new connection between two valid participants in the session.
  NewConnection : (a,b : Actor)
               -> (prf : AllowedToConnect a b ps)
               -> Sessions ps (Var Ty (CHAN (a,b))) old (\lbl => MkStateItem (CHAN (a,b)) lbl (MkChanState Bound) :: old)

  ||| Close an existing connection.
  EndConnection : (chan : Var Ty (CHAN (a,b)))
               -> (prf  : InContext (CHAN (a,b)) (ChannelHasState Bound chan) old)
               -> Sessions ps () old (const $ update old prf (SetChannelState Free))

  ||| Send a message that the channel sender knows about (either created or received) to the receiver on the given active channel.
  SendLeft : (chan : Var Ty (CHAN (s,r)))
          -> (msg  : Var Ty (DATA type))
          -> (prfActive : InContext (CHAN (s,r))  (ChannelHasState Bound chan) old)
          -> (prfKnows  : InContext (DATA type) (KnowsData s msg) old)
          -> Sessions ps () old (const $ update old prfKnows (ExpandWhoKnows r))

  ||| Send a message that the receiver on the channel knows about (either created or received) to the sending end on the given active channel.
  SendRight : (chan : Var Ty (CHAN (s,r)))
           -> (msg  : Var Ty (DATA type))
           -> (prfActive : InContext (CHAN (s,r))  (ChannelHasState Bound chan) old)
           -> (prfKnows  : InContext (DATA type) (KnowsData r msg) old)
           -> Sessions ps () old (const $ update old prfKnows (ExpandWhoKnows s))

  ||| If all actors in the session have seen the data then we can access the message's value and depend on it.
  ReadMsg : (msg : Var Ty (DATA type))
         -> (prf : InContext (DATA type) (AllKnow ps msg) old)
         -> Sessions ps type old (const old)

  ||| End the session description if all the variables are in the correct end state.
  |||
  ||| This is our check that all channels have been closed.
  StopSession : AllContext EndState old -> Sessions ps () old (const Nil)

{- [ NOTE ]

Here we define the language and high-level friendly API.

-}
||| Define the `SESSIONS` language.
SESSIONS : (ps : List Actor) -> LANG Ty CalcStateType
SESSIONS ps = MkLang Ty CalcStateType (Sessions ps)

||| Define a closed session.
Session : (m : Type -> Type) -> List Actor -> Type
Session m ps = LangM m () (SESSIONS ps) Nil (const Nil)

||| Describe that the given actor `a` creates a message of type `type`.
|||
||| We also need proof that the actor is allowed to participate in the description.
msg : (creator : Actor)
   -> (type : Type)
   -> {auto prf : Elem creator actors}
   -> LangM m (Var Ty (DATA type)) (SESSIONS actors) old (\lbl => MkStateItem (DATA type) lbl (MkDataState ([creator]) type) :: old)
msg creator type {prf} = Expr $ NewData creator type prf

||| Describe that the given actor `a` creates a message that depends on an earlier message that `a` has seen.
|||
||| The resulting message type will be a dependent pair.
msgDep : (creator  : Actor)
      -> (dep      : Var Ty (DATA type))
      -> {auto prfKnows : InContext (DATA type) (KnowsData creator dep) old}
      -> (msgType  : (msg : type) -> Type)
      -> LangM m
               (Var Ty (DATA (x ** msgType x)))
               (SESSIONS actors)
               old
               (\lbl => MkStateItem (DATA (x ** msgType x))
                                    lbl
                                    (MkDataState [creator] (x ** msgType x)) :: old)
msgDep creator dep {prfKnows} msgType = Expr (NewDataDep creator dep prfKnows msgType)

||| If all actors in the session have seen the data then we can access the message's value and depend on it.
read : (msg : Var Ty (DATA type))
    -> {auto prf : InContext (DATA type) (AllKnow actors msg) old}
    -> LangM m type (SESSIONS actors) old (const old)
read msg {prf} = Expr $ ReadMsg msg prf

||| End the session description if all the variables are in the correct end state.
|||
||| This is our check that all channels have been closed.
end : {auto prf : AllContext EndState old} -> LangM m () (SESSIONS actors) old (const Nil)
end {prf} = Expr $ StopSession prf

||| Specify a new connection between two valid participants in the session.
setup : (a, b : Actor)
     -> {auto prf : AllowedToConnect a b actors}
     -> LangM m (Var Ty (CHAN (a,b))) (SESSIONS actors) old (\lbl => MkStateItem (CHAN (a,b)) lbl (MkChanState Bound) :: old)
setup sender receiver {prf} = Expr $ NewConnection sender receiver prf

||| Close an existing connection.
destroy : (chan : Var Ty (CHAN (a,b)))
       -> {auto prf  : InContext (CHAN (a,b)) (ChannelHasState Bound chan) old}
       -> LangM m () (SESSIONS actors) old (const $ update old prf (SetChannelState Free))
destroy chan {prf} = Expr $ EndConnection chan prf

||| Send a message that the channel sender knows about (either created or received) to the receiver on the given active channel.
sendLeft : (chan : Var Ty (CHAN (s,r)))
        -> (msg  : Var Ty (DATA type))
        -> {auto prfActive : InContext (CHAN (s,r))  (ChannelHasState Bound chan) old}
        -> {auto prfKnows  : InContext (DATA type) (KnowsData s msg) old}
        -> LangM m () (SESSIONS actors) old (const $ update old prfKnows (ExpandWhoKnows r))
sendLeft chan msg {prfActive} {prfKnows} = Expr (SendLeft chan msg prfActive prfKnows)

||| Send a message that the receiver on the channel knows about (either created or received) to the sending end on the given active channel.
sendRight : (chan : Var Ty (CHAN (s,r)))
         -> (msg  : Var Ty (DATA type))
         -> {auto prfActive : InContext (CHAN (s,r))  (ChannelHasState Bound chan) old}
         -> {auto prfKnows  : InContext (DATA type) (KnowsData r msg) old}
         -> LangM m () (SESSIONS actors) old (const $ update old prfKnows (ExpandWhoKnows s))
sendRight chan msg {prfActive} {prfKnows} = Expr (SendRight chan msg prfActive prfKnows)

{- [ NOTE ]

Let's define some actors.

-}

Alice : Actor
Alice = MkActor "A"

Bob : Actor
Bob = MkActor "B"

Charlie : Actor
Charlie = MkActor "C"

{- [ NOTE ]

Here we define a value dependent version of the well known TCP Handshake.

Dependent pairs are used to ensure that the sequence numbers sent are the ones previously seen.

There are better ways to encode this, see the PLACES paper linked in the module's documentation.

-}

data Packet

TCPHandshake : Session m [Alice, Bob]
TCPHandshake = do
  chan <- setup Alice Bob

  m1 <- msg Alice (Packet, Nat)
  sendLeft chan m1

  (p,x) <- read m1
  m2 <- msg Bob (Packet, (x' ** x' = x), Nat)

  sendRight chan m2

  (p,xplus,y) <- read m2

  m3 <- msg Alice (Packet, (x' ** x' = x), (y' ** y' = y))
  sendLeft chan m3
  destroy chan
  end

{- [ NOTE ]

Here we define a PingPong protocol. In which Alice sends a Ping to Bob who responds with a Pong, and proof that they send a pong, and calls the session description again. If alice sent a Pong then the session ends.

This is *a* encoding, there are probably better ways to encode this.

-}
data PingPong = Ping | Pong

pingNotPong : (Ping = Pong) -> Void
pingNotPong Refl impossible

DecEq PingPong where
  decEq Ping Ping = Yes Refl
  decEq Pong Pong = Yes Refl
  decEq Ping Pong = No pingNotPong
  decEq Pong Ping = No (negEqSym pingNotPong)

RfcPingPong : Session m [Alice, Bob]
RfcPingPong = do chan <- setup Alice Bob
                 val <- msg Alice PingPong
                 sendLeft chan val
                 res <- read val
                 case res of
                   Pong => do destroy chan
                              end
                   Ping => do val' <- msg Bob (x : PingPong ** x = Pong)
                              sendRight chan val'
                              destroy chan
                              end
                              assert_total $ RfcPingPong

{- [ NOTE ]

Here we define a simple varient of the Echo protocol that uses an optional type to act as a quit message in the Empty case.

-}
Echo : Session m [Alice, Bob]
Echo {m} = do chan <- setup Alice Bob
              val <- msg Alice (Maybe String)
              sendLeft chan val
              res <- read val
              case res of
                Nothing => do destroy chan
                              end
                Just _  => do sendRight chan val
                              destroy chan
                              end
                              assert_total $ Echo {m=m}

{- [ NOTE ]

Here we define a simple Higher-Order-Protocol that emulates an authentication step using a Boolean.

-}

hoppy : Session m [Alice, Bob]
     -> Session m [Alice, Bob]
hoppy p = do chan <- setup Alice Bob
             val <- msg Alice String
             sendLeft chan val
             resp <- msg Bob Bool
             sendRight chan resp
             res <- read resp
             case res of
               False => do destroy chan
                           end
               True => do destroy chan
                          end
                          p

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

max_stars_repo_name: border-patrol/resources

max_issues_repo_name: border-patrol/resources

max_forks_repo_name: border-patrol/resources


text:
module Main

import tipos
import lexer
import parser
import piAutomata

removeJust: (Maybe BExp, List Token) -> BExp
removeJust (Just x, l) = x

chamada: ((List Ctrl, List Val, SortedMap Val Bindable , SortedMap Loc Val, List Loc), List (List Ctrl, List Val, SortedMap Val Bindable , SortedMap Loc Val, List Loc)) -> String
chamada (pi, lista) = show lista

main : IO ()
main = repl "Enter a program: " read_input
  where
    read_input : String -> String
    -- read_input x = show (transformPi(parse(arithExp (read_token (unpack x) "" [])))) ++ "\n"
    read_input x = let exp = (removeJust (boolExp (read_token (unpack x) "" []))) in
    (show chamada (process ([exp],[],empty,empty,[]) ([]) )) ++ "\n"

ext: idr

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
module Tomladris

import public Data.String
import public Data.SortedMap
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

export
data TomlValue =   TComment String
                 | TString String
                 | TInteger Integer
                 | TDouble Double
                 | TBoolean Bool
                 | TArray (List TomlValue)
                 | TTableKV TomlValue TomlValue

private
parseComment : Parser TomlValue
parseComment = TComment . pack <$> (char '#' *> many (noneOf "\n"))

parseNumber : Parser TomlValue
parseNumber = (parseNum . pack) <$> many (oneOf "1234567890.eE+-")
  where
    parseNum : String -> TomlValue
    parseNum s = case parseInteger s of
                 (Just x) => TInteger x
                 Nothing => case parseDouble s of
                            (Just x) => TDouble x
                            Nothing => TDouble 0.0

parseTBoolean : Parser TomlValue
parseTBoolean = toBool <$> (string "true" <|> string "false")
  where
    toBool s = case s of
                 "true" => TBoolean True
                 "false" => TBoolean False

parseTString : Parser TomlValue
parseTString = (TString) <$> (quoted '\'' <|> quoted '\"')

--lazying  '[' ']' match very very important
--else we get infinite loop
mutual
  parseTArray : Parser TomlValue
  parseTArray = TArray <$> (spaces *> (char '[') *>| parsePrimitives <*| (char ']'))

  parsePrimitives : Parser (List TomlValue)
  parsePrimitives = spaces *> (sepBy1 parseNumber (char ',')) <|>|
                    (sepBy1 parseTBoolean (char ',')) <|>|
                    (sepBy1 parseTString (char ',')) <|>|
                    (sepBy1 parseTArray (char ','))

parseTableName : Parser TomlValue
parseTableName = (TString .pack) <$> ((many endOfLine) *> spaces *> (char '[') *>| (many (noneOf "]"))  <*| (char ']'))

parseTKeyVal : Parser TomlValue
parseTKeyVal = (TTableKV) <$>
               (parseTString <|> parseString) <*>
               (char '=' *>
               spaces *> (parseTString <|>
                             parseTArray <|>
                             parseTBoolean <|>
                             parseNumber))
  where
    parseString = (TString . pack) <$>
                  (((many endOfLine) *> spaces *> many (noneOf " [=")) <|>
                  (spaces *> many (noneOf " [=")))

keyMap : (List TomlValue) -> SortedMap String TomlValue
keyMap [] = empty
keyMap (x::xs) = keyMapAux x xs empty
  where
    keyMapAux : TomlValue -> (List TomlValue) -> SortedMap String TomlValue -> SortedMap String TomlValue
    keyMapAux root [] m = m
    keyMapAux root@(TString r) ((TTableKV (TString key) value)::xs) m = keyMapAux root xs (insert (r ++ "." ++ key) value m)

addKeyVal : String -> String -> TomlValue -> SortedMap String TomlValue -> SortedMap String TomlValue
addKeyVal root key value m = if (length root == 0)
                             then insert key value m
                             else insert (root ++ "." ++ key) value m

foldOver : String -> (List TomlValue) -> SortedMap String TomlValue -> SortedMap String TomlValue
foldOver root [] m = m
foldOver root ((TString table)::xs) m = foldOver table xs m
foldOver root ((TTableKV (TString key) value)::xs) m = foldOver root xs (addKeyVal root key value m)

export
parseToml : String -> SortedMap String TomlValue
parseToml s = case parse (many (parseTableName <|> parseTKeyVal)) s of
              (Right lstToml) => foldOver "" lstToml empty
              (Left _) => empty


text:
module Data.List.Lazy

import Data.Fuel
import Data.Stream
import Data.Colist
import Data.Colist1

%default total

-- All functions here are public export
-- because their definitions are pretty much the specification.

public export
data LazyList : Type -> Type where
  Nil : LazyList a
  (::) : (x : a) -> (xs : Lazy (LazyList a)) -> LazyList a

--- Truly lazy functions ---

public export
foldrLazy : (func : elem -> Lazy acc -> acc) -> (init : Lazy acc) -> (input : LazyList elem) -> acc
foldrLazy _  init [] = init
foldrLazy op init (x::xs) = x `op` foldrLazy op init xs

public export
(++) : LazyList a -> Lazy (LazyList a) -> LazyList a
(++) = flip $ foldrLazy (::)

-- Specialized variant of `concatMap` with both `t` and `m` being `LazyList`.
public export
bindLazy : (a -> LazyList b) -> LazyList a -> LazyList b
bindLazy f = foldrLazy ((++) . f) []

public export
choice : Alternative f => LazyList (f a) -> f a
choice = foldrLazy (<|>) empty

public export
choiceMap : Alternative f => (a -> f b) -> LazyList a -> f b
choiceMap g = foldrLazy ((<|>) . g) empty

public export
any : (a -> Bool) -> LazyList a -> Bool
any p = foldrLazy ((||) . p) False

public export
all : (a -> Bool) -> LazyList a -> Bool
all p = foldrLazy ((&&) . p) True

--- Interface implementations ---

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

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

export
Show a => Show (LazyList a) where
  show []       = "[]"
  show (h :: t) = "[" ++ show' "" h t ++ "]"
    where
      -- Idris didn't like the lazyness involved when using the
      -- same implementation as for `List`, therefore, this was
      -- adjusted to first force the head and tail of the list.
      show' : String -> a -> LazyList a -> String
      show' acc h Nil       = acc ++ show h
      show' acc h (x :: xs) = show' (acc ++ show h ++ ", ") x xs

public export
Semigroup (LazyList a) where
  xs <+> ys = xs ++ ys

public export
Monoid (LazyList a) where
  neutral = []

public export
Foldable LazyList where
  foldr op nil [] = nil
  foldr op nil (x :: xs) = x `op` foldr op nil xs

  foldl op acc [] = acc
  foldl op acc (x :: xs) = foldl op (acc `op` x) xs

  foldlM fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init

  null []     = True
  null (_::_) = False

  foldMap f [] = neutral
  foldMap f (x :: xs) = f x <+> foldMap f xs

public export
Functor LazyList where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

public export
Applicative LazyList where
  pure x = [x]
  fs <*> vs = bindLazy (\f => map f vs) fs

public export
Alternative LazyList where
  empty = []
  (<|>) = (++)

public export
Monad LazyList where
  m >>= f = bindLazy f m

-- There is no Traversable instance for lazy lists.
-- The result of a traversal will be a non-lazy list in general
-- (you can't delay the "effect" of an applicative functor).
public export
traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
traverse g [] = pure []
traverse g (x :: xs) = [| g x :: traverse g xs |]

public export %inline
for : Applicative f => LazyList a -> (a -> f b) -> f (List b)
for = flip traverse

public export
sequence : Applicative f => LazyList (f a) -> f (List a)
sequence = traverse id

public export
Zippable LazyList where
  zipWith _ [] _ = []
  zipWith _ _ [] = []
  zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

  zipWith3 _ [] _ _ = []
  zipWith3 _ _ [] _ = []
  zipWith3 _ _ _ [] = []
  zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

  unzip xs = (fst <$> xs, snd <$> xs)
  unzipWith = unzip .: map

  unzip3 xs = (fst <$> xs, fst . snd <$> xs, snd . snd <$> xs)
  unzipWith3 = unzip3 .: map

--- Lists creation ---

public export
fromList : List a -> LazyList a
fromList []      = []
fromList (x::xs) = x :: fromList xs

covering
public export
iterate : (f : a -> Maybe a) -> (x : a) -> LazyList a
iterate f x = x :: case f x of
  Nothing => []
  Just y  => iterate f y

covering
public export
unfoldr : (b -> Maybe (a, b)) -> b -> LazyList a
unfoldr f c = case f c of
  Nothing     => []
  Just (a, n) => a :: unfoldr f n

public export
iterateN : Nat -> (a -> a) -> a -> LazyList a
iterateN Z     _ _ = []
iterateN (S n) f x = x :: iterateN n f (f x)

public export
replicate : (n : Nat) -> (x : a) -> LazyList a
replicate Z     _ = []
replicate (S n) x = x :: replicate n x

--- Functions acquiring parts of list ---

public export
head' : LazyList a -> Maybe a
head' []     = Nothing
head' (x::_) = Just x

public export
tail' : LazyList a -> Maybe (LazyList a)
tail' []      = Nothing
tail' (_::xs) = Just xs

--- Functions for acquiring different types of sublists ---

public export
take : Nat -> LazyList a -> LazyList a
take (S k) (x::xs) = x :: take k xs
take _ _ = []

public export
drop : Nat -> LazyList a -> LazyList a
drop Z     xs      = xs
drop (S _) []      = []
drop (S n) (_::xs) = drop n xs

public export
takeWhile : (a -> Bool) -> LazyList a -> LazyList a
takeWhile p []      = []
takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

public export
dropWhile : (a -> Bool) -> LazyList a -> LazyList a
dropWhile p []      = []
dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

public export
filter : (a -> Bool) -> LazyList a -> LazyList a
filter p []      = []
filter p (x::xs) = if p x then x :: filter p xs else filter p xs

public export
mapMaybe : (a -> Maybe b) -> LazyList a -> LazyList b
mapMaybe f []      = []
mapMaybe f (x::xs) = case f x of
  Nothing => mapMaybe f xs
  Just y  => y :: mapMaybe f xs

namespace Stream

  public export
  take : Fuel -> Stream a -> LazyList a
  take Dry _ = []
  take (More f) (x :: xs) = x :: take f xs

namespace Colist

  public export
  take : Fuel -> Colist a -> LazyList a
  take Dry _ = []
  take _ [] = []
  take (More f) (x :: xs) = x :: take f xs

namespace Colist1

  public export
  take : Fuel -> Colist1 a -> LazyList a
  take fuel as = take fuel (forget as)

--- Functions for extending lists ---

public export
mergeReplicate : a -> LazyList a -> LazyList a
mergeReplicate sep []      = []
mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys

public export
intersperse : a -> LazyList a -> LazyList a
intersperse sep []      = []
intersperse sep (x::xs) = x :: mergeReplicate sep xs

public export
intercalate : (sep : LazyList a) -> (xss : LazyList (LazyList a)) -> LazyList a
intercalate sep xss = choice $ intersperse sep xss

--- Functions converting lazy lists to something ---

public export
toColist : LazyList a -> Colist a
toColist [] = []
toColist (x::xs) = x :: toColist xs


text:
module Main

import System
import System.Info
import System.File
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw

testSocket : String
testSocket = "./idris2_test.socket"

runServer : (net : Bool) -> IO (Either String (if net then Port else ()))
runServer net = do
  Right sock <- socket (if net then AF_INET else AF_UNIX) Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- bind sock (Just (Hostname (if net then "localhost" else testSocket))) 0
  if res /= 0
    then pure (Left $ "Failed to bind socket with error: " ++ show res)
    else do
      port <- if net then getSockPort sock else pure ()
      res <- listen sock
      if res /= 0
         then pure . Left $ "Failed to listen on socket with error: " ++ show res
         else do ignore $ fork (serve sock)
                 pure $ Right port
  where
    serve : Socket -> IO ()
    serve sock = do
      Right (s, _) <- accept sock
        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
      Right  (str, _) <- recv s 1024
        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
      putStrLn ("Received: " ++ str)
      Right n <- send s ("echo: " ++ str)
        | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
      pure ()

runClient : (net : Bool) -> Port -> IO ()
runClient net serverPort = do
  Right sock <- socket (if net then AF_INET else AF_UNIX) Stream 0
    | Left fail => putStrLn ("Failed to open socket: " ++ show fail)
  res <- connect sock (Hostname $ if net then "localhost" else testSocket) serverPort
  if res /= 0
    then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
    else do
      Right n <- send sock ("hello world from a " ++ (if net then "ipv4" else "unix") ++ " socket!")
        | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
      Right (str, _) <- recv sock 1024
        | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
      -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
      -- to be printed after the server prints its own message
      putStrLn ("Received: " ++ str)

main : IO ()
main = do
  Right serverPort <- runServer True
    | Left err => putStrLn $ "[server] " ++ err
  runClient True serverPort
  Right () <- runServer False
    | Left err => putStrLn $ "[server] " ++ err
  runClient False 0
  ignore $ removeFile testSocket


text:
xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Exercices

import Data.Vect

ask : String -> IO String
ask prompt = do
  putStr prompt
  getLine

readToBlank : IO (List String)
readToBlank = do
  line <- ask "input (empty line to finish): "
  if line == ""
  then pure []
  else (line ::) <$> readToBlank

readAndSave : IO ()
readAndSave = do
  contents <- readToBlank
  filepath <- ask "filename: "
  Right () <- writeFile filepath (concat $ intersperse "\n" contents)
    | Left err => putStrLn ("ERROR: " ++ show err)
  pure ()

readVect : File -> IO (Either FileError (n ** Vect n String))
readVect fh = do
  eof <- fEOF fh
  if eof
  then pure (Right (_ ** []))
  else do
    Right x <- fGetLine fh
      | Left error => pure (Left error)
    Right (_ ** xs) <- readVect fh
      | Left error => pure (Left error)
    pure (Right (_ ** (trim x) :: xs))

readVectFile : (filepath : String) -> IO (n ** Vect n String)
readVectFile filepath = do
  Right fh <- openFile filepath Read
  Right ans <- readVect fh
  closeFile fh
  pure ans


text:
module STLCInterp

data HasType : List a -> a -> Type where
  VZ : HasType (t :: env) t
  VS : HasType env t -> HasType (_ :: env) t

data Expr : List Type -> Type -> Type where
  Val : Int -> Expr env Int
  Var : HasType env t -> Expr env t
  Lam : Expr (a :: env) b -> Expr env (a -> b)
  App : Expr env (a -> b) -> Expr env a -> Expr env b

interpEnv : List Type -> Type
interpEnv [] = ()
interpEnv (x :: xs) = (x, interpEnv xs)

lookup : HasType env t -> interpEnv env -> t
lookup VZ (t, _) = t
lookup (VS x) (_, ts) = lookup x ts

eval : interpEnv env -> %static Expr env t -> t
eval env (Val x) = x
eval env (Var x) = lookup x env
eval env (Lam body) = \x => eval (x, env) body
eval env (App f x) = (eval env f) (eval env x)

example : Expr [] Int
example = App (Lam (Var VZ)) (Val 42)

test : Int
test = eval () example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Control.Monad.Reader

import public Control.Monad.Reader.Reader as Control.Monad.Reader
import public Control.Monad.Reader.Interface as Control.Monad.Reader


text:
module ErrNList

import Effect.Select
import Effect.StdIO
import Effects

f : Int -> Eff Int [SELECT, STDIO]
f n = do
    x <- select [n .. 10]
    if x == 2
        then do
          putStrLn "The number is 2, incrementing"
          pure $ x + 1
        else pure x

-- m : Maybe Int
-- m = run $ f 3

-- l : List Int
-- l = run $ f 3

el : List (IO Int)
el = run . run $ f 3

el' : List (IO Int)
el' = run $ f 3

le : IO (List Int)
le = run . run $ f 3

le' : IO (List Int)
le' = run $ f 3

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
--- Day 17: Trick Shot ---

module TrickShot
import System
import System.File
import Data.List
import Data.List1
import Data.String.Parser

Point : Type
Point = (Integer, Integer)

Path : Type
Path = List1 Point

BoundingBox : Type
BoundingBox = (Point, Point)

parsePoint : Parser Point
parsePoint = (,) <$> (string "x=" *> integer) <*> (string ".." *> integer)
         <|> (,) <$> (string "y=" *> integer) <*> (string ".." *> integer)

parseArea : Parser BoundingBox
parseArea = (,) <$> (string "target area: " *> parsePoint) <*> (string ", " *> parsePoint)

inBounds : (point : Point) -> (box : BoundingBox) -> Bool
inBounds (x, y) ((x1, x2), (y1, y2)) = x >= x1 && x <= x2 && y >= y1 && y <= y2

outOfRange : (point : Point) -> (box : BoundingBox) -> Bool
outOfRange (x, y) ((x1, x2), (y1, y2)) = x > x2 || y < y1

sign : Integer -> Integer
sign x = if x > 0 then 1 else if x < 0 then -1 else 0

step : (start : Point) -> (deltas : Point) -> Stream Point
step (x, y) (dx, dy) = (x, y) :: step (x + dx, y + dy) (dx + negate (sign dx), dy - 1)

simulate : (deltas : Point) -> (box : BoundingBox) -> Path
simulate deltas box = go $ step (0, 0) deltas
                            where
                                go : Stream Point -> Path
                                go (pos :: path) = if (inBounds pos box) || (outOfRange pos box)
                                                      then singleton pos
                                                      else (pos ::: (forget . go) path)

getAllPaths : (box: BoundingBox) -> (vels: List Point) -> List Path
getAllPaths box vels = foldl checkPath [] vels
                        where
                            checkPath : (acc : List Path) -> (vel : Point) -> List Path
                            checkPath acc vel = let path = simulate vel box in
                                                if inBounds (last path) box then (path :: acc) else acc

main : IO ()
main = do
        args <- getArgs
        let (file :: _) = drop 1 args | [] => printLn "No file provided!"
        (Right symbols) <- readFile file | (Left error) => printLn error
        let (Right (((x1, x2), (y1, y2)), _)) = parse parseArea symbols | (Left error) => printLn error
        let paths = getAllPaths ((x1, x2), (y1, y2))  [
             (x, y)
            | x <- [(cast . floor . sqrt . cast) (2 * x1)..x2]
            , y <- [y1..abs y1 - 1]
        ]
        printLn $ foldl (\acc, path => max acc $ (foldl1 max . map snd) path) 0 paths
        printLn $ length paths


text:
module Data.Profunctor.Choice

import Data.Profunctor

public export
interface Profunctor p => Choice p where
  left' : p a b -> p (Either a c) (Either b c)
  right' : p a b -> p (Either c a) (Either c b)

  right' = dimap (either Right Left) (either Right Left) . left'
  left' = dimap (either Right Left) (either Right Left) . right'


text:
module Language.Reflection

import public Language.Reflection.TT
import public Language.Reflection.TTImp

import public Control.Monad.Trans

%default total

----------------------------------
--- Elaboration data structure ---
----------------------------------

||| Elaboration scripts
||| Where types/terms are returned, binders will have unique, if not
||| necessarily human readabe, names
export
data Elab : Type -> Type where
     Pure : a -> Elab a
     Bind : Elab a -> (a -> Elab b) -> Elab b
     Fail : FC -> String -> Elab a

     Try : Elab a -> Elab a -> Elab a

     ||| Log a message. Takes a
     ||| * topic
     ||| * level
     ||| * message
     LogMsg : String -> Nat -> String -> Elab ()
     ||| Print and log a term. Takes a
     ||| * topic
     ||| * level
     ||| * message
     ||| * term
     LogTerm : String -> Nat -> String -> TTImp -> Elab ()
     ||| Resugar, print and log a term. Takes a
     ||| * topic
     ||| * level
     ||| * message
     ||| * term
     LogSugaredTerm : String -> Nat -> String -> TTImp -> Elab ()

     -- Elaborate a TTImp term to a concrete value
     Check : TTImp -> Elab expected
     -- Quote a concrete expression back to a TTImp
     Quote : (0 _ : val) -> Elab TTImp

     -- Elaborate under a lambda
     Lambda : (0 x : Type) ->
              {0 ty : x -> Type} ->
              ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))

     -- Get the current goal type, if known
     -- (it might need to be inferred from the solution)
     Goal : Elab (Maybe TTImp)
     -- Get the names of local variables in scope
     LocalVars : Elab (List Name)
     -- Generate a new unique name, based on the given string
     GenSym : String -> Elab Name
     -- Put a name in the current namespace
     InCurrentNS : Name -> Elab Name
     -- Get the types of every name which matches.
     -- There may be ambiguities - returns a list of fully explicit names
     -- and their types. If there's no results, the name is undefined.
     GetType : Name -> Elab (List (Name, TTImp))
     -- Get the metadata associated with a name
     GetInfo : Name -> Elab (List (Name, NameInfo))
     -- Get the type of a local variable
     GetLocalType : Name -> Elab TTImp
     -- Get the constructors of a data type. The name must be fully resolved.
     GetCons : Name -> Elab (List Name)
     -- Check a group of top level declarations
     Declare : List Decl -> Elab ()

export
Functor Elab where
  map f e = Bind e $ Pure . f

export
Applicative Elab where
  pure = Pure
  f <*> a = Bind f (<$> a)

export
Alternative Elab where
  empty = Fail EmptyFC ""
  l <|> r = Try l r

export
Monad Elab where
  (>>=) = Bind

-----------------------------
--- Elaboration interface ---
-----------------------------

public export
interface Monad m => Elaboration m where

  ||| Report an error in elaboration at some location
  failAt : FC -> String -> m a

  ||| Try the first elaborator. If it fails, reset the elaborator state and
  ||| run the second
  try : Elab a -> Elab a -> m a

  ||| Write a log message, if the log level is >= the given level
  logMsg : String -> Nat -> String -> m ()

  ||| Write a log message and a rendered term, if the log level is >= the given level
  logTerm : String -> Nat -> String -> TTImp -> m ()

  ||| Write a log message and a resugared & rendered term, if the log level is >= the given level
  logSugaredTerm : String -> Nat -> String -> TTImp -> m ()

  ||| Check that some TTImp syntax has the expected type
  ||| Returns the type checked value
  check : TTImp -> m expected

  ||| Return TTImp syntax of a given value
  quote : (0 _ : val) -> m TTImp

  ||| Build a lambda expression
  lambda : (0 x : Type) ->
           {0 ty : x -> Type} ->
           ((val : x) -> Elab (ty val)) -> m ((val : x) -> (ty val))

  ||| Get the goal type of the current elaboration
  goal : m (Maybe TTImp)

  ||| Get the names of the local variables in scope
  localVars : m (List Name)

  ||| Generate a new unique name
  genSym : String -> m Name

  ||| Given a name, return the name decorated with the current namespace
  inCurrentNS : Name -> m Name

  ||| Given a possibly ambiguous name, get all the matching names and their types
  getType : Name -> m (List (Name, TTImp))

  ||| Get the metadata associated with a name. Returns all matching namea and their types
  getInfo : Name -> m (List (Name, NameInfo))

  ||| Get the type of a local variable
  getLocalType : Name -> m TTImp

  ||| Get the constructors of a fully qualified data type name
  getCons : Name -> m (List Name)

  ||| Make some top level declarations
  declare : List Decl -> m ()

export %inline
||| Report an error in elaboration
fail : Elaboration m => String -> m a
fail = failAt EmptyFC

||| Log the current goal type, if the log level is >= the given level
export %inline
logGoal : Elaboration m => String -> Nat -> String -> m ()
logGoal str n msg = whenJust !goal $ logTerm str n msg

export
Elaboration Elab where
  failAt         = Fail
  try            = Try
  logMsg         = LogMsg
  logTerm        = LogTerm
  logSugaredTerm = LogSugaredTerm
  check          = Check
  quote          = Quote
  lambda         = Lambda
  goal           = Goal
  localVars      = LocalVars
  genSym         = GenSym
  inCurrentNS    = InCurrentNS
  getType        = GetType
  getInfo        = GetInfo
  getLocalType   = GetLocalType
  getCons        = GetCons
  declare        = Declare

public export
Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
  failAt              = lift .: failAt
  try                 = lift .: try
  logMsg s            = lift .: logMsg s
  logTerm s n         = lift .: logTerm s n
  logSugaredTerm s n  = lift .: logSugaredTerm s n
  check               = lift . check
  quote v             = lift $ quote v
  lambda x            = lift . lambda x
  goal                = lift goal
  localVars           = lift localVars
  genSym              = lift . genSym
  inCurrentNS         = lift . inCurrentNS
  getType             = lift . getType
  getInfo             = lift . getInfo
  getLocalType        = lift . getLocalType
  getCons             = lift . getCons
  declare             = lift . declare


text:
fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl

-- twoPlusTwoBad : 2 + 2 = 5
-- twoPlusTwoBad = Refl

disjoint : (n : Nat) -> Z = S n -> Void
disjoint n prf = replace {p = disjointTy} prf ()
  where
    disjointTy : Nat -> Type
    disjointTy Z = ()
    disjointTy (S k) = Void

plusReduces : (n:Nat) -> plus Z n = n
plusReduces n = Refl

plusReducesR : (n:Nat) -> plus n Z = n
plusReducesR n = Refl

plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)

plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)


text:
module Client.Util

import Data.Buffer
import Extra.Buffer
import Fmt
import Inigo.Async.Base
import Inigo.Async.Promise
import System
import System.File
import System.Path

rejectStatus : String -> Int -> Buffer -> Promise a
rejectStatus url status buf =
  do
    contents <- liftIO $ readAll buf
    let extra = if status == 500 then " -- You may need to login again with `inigo login`" else ""
    reject (fmt "HTTP Failure (%d) from %s: \"%s\"%s" status url contents extra)

export
assertOk : String -> Promise (Int, Buffer) -> Promise Buffer
assertOk url result =
  do
    (200, buf) <- result
      | (status, res) => rejectStatus url status res
    pure buf

||| TODO: Improve home dir
export
getHomeDir : IO (Maybe String)
getHomeDir =
  do
    Nothing <- getEnv "INIGO_HOME"
      | Just home => pure $ Just home
    Nothing <- getEnv "HOME"
      | Just home => pure $ Just home
    pure Nothing

export
inigoSessionFile : IO (Maybe String)
inigoSessionFile =
  do
    Nothing <- getEnv "INIGO_SESSION"
      | Just sessionFile => pure (Just sessionFile)
    Just homeDir <- getHomeDir
      | Nothing => pure Nothing
    pure $ Just (homeDir </> ".inigo_session")

export
readSessionFile : IO (Maybe String)
readSessionFile =
  do
    Just sessionFile <- inigoSessionFile
      | Nothing => pure Nothing
    Right session <- readFile sessionFile
      | Left err => pure Nothing
    pure (Just session)

export
auth : String -> (String, String)
auth session =
  ("Authorization", "Basic " ++ session)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Calc.Div

%default total

export
divide : Int -> Int -> Int
divide x y = if y == 0
             then 0
             else x `div` y

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

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

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


text:
module Test.Main

import Data.List
import Language.CSV
import Text.Token

test : (Eq a, Show a) => a -> a -> IO ()
test a b = if a == b
              then putStrLn "ok"
              else putStrLn $ "Expected " ++ show a ++ " but found " ++ show b

parsesTo : String -> Maybe CSV -> IO ()
parsesTo s e = test e $ parse s

lexesTo : String -> Maybe (List CSVToken) -> IO ()
lexesTo s e = test e $ lexCSV s

parsesLexTo : List CSVToken -> Maybe CSV -> IO ()
parsesLexTo ts e = test e $ parseCSV ts

comma : CSVToken
comma = Tok Comma ","

crlf : CSVToken
crlf = Tok CRLF "\r\n"

dQuote : CSVToken
dQuote = Tok DQuote "\""

textData : String -> CSVToken
textData s = Tok TextData s

makeTokens : CSV -> List CSVToken
makeTokens =
  let
    makeRecord : List String -> List CSVToken
    makeRecord = intersperse comma . map (Tok TextData)
  in
    concat . intersperse [crlf] . map makeRecord

runTriplet : String -> List CSVToken -> CSV -> IO ()
runTriplet s t c = do
  putStrLn $ "Testing " ++ s
  putStr "  Lexer: "
  lexesTo s $ Just t
  putStr "  Parsing Token: "
  parsesLexTo t $ Just c
  putStr "  Parsing: "
  parsesTo s $ Just c

runDuplet : String -> CSV -> IO ()
runDuplet s c = runTriplet s (makeTokens c) c

tests : IO ()
tests = do
  runDuplet "Hello" [["Hello"]]
  runDuplet "Hello,World" [["Hello", "World"]]

  runTriplet "Hello,World\r\n" [textData "Hello", comma, textData "World", crlf] [["Hello", "World"]]
  runTriplet "a,b\r\nc,d" [textData "a", comma, textData "b", crlf, textData "c", comma, textData "d"] [["a", "b"],["c","d"]]
  runTriplet "a,\"b\r\nc\",d" [textData "a", comma, dQuote, textData "b", crlf, textData "c", dQuote, comma, textData "d"] [["a", "b\r\nc","d"]]
  runTriplet "a,\"b\"" [textData "a", comma, dQuote, textData "b", dQuote] [["a", "b"]]

main : IO ()
main = tests

max_stars_repo_name: wchresta/csv-parser

max_issues_repo_name: wchresta/csv-parser

max_forks_repo_name: wchresta/csv-parser


text:
module ContriverText.JsUtil

import Data.SortedMap
import Language.Reflection

import ContriverText.Util

-- This is based on jscall from
-- <http://docs.idris-lang.org/en/latest/reference/ffi.html>.
%inline
jsft : (t : Type) -> String -> {auto fty : FTy FFI_JS [] t} -> t
jsft t code = foreign FFI_JS code t

class HasJsPtr a where
  jsptr : a -> JS_IO Ptr

instance HasJsPtr Ptr where
  jsptr x = return x

instance HasJsPtr String where
  jsptr = jsft _ "%0"

instance HasJsPtr Int where
  jsptr = jsft _ "%0"

instance HasJsPtr Char where
  jsptr = jsft _ "%0"

instance HasJsPtr () where
  jsptr = jsft _ "%0"

instance HasJsPtr Float where
  jsptr = jsft _ "%0"

%inline
jsf0 : String -> JS_IO Ptr
jsf0 code = jsft _ code

%inline
jsf1 : String -> Ptr -> JS_IO Ptr
jsf1 code = jsft _ code

%inline
jsf2 : String -> Ptr -> Ptr -> JS_IO Ptr
jsf2 code = jsft _ code

%inline
jsf3 : String -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsf3 code = jsft _ code

%inline
jsf4 : String -> Ptr -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsf4 code = jsft _ code

%inline
jsf5 : String -> Ptr -> Ptr -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsf5 code = jsft _ code

jsc0 : Ptr -> JS_IO Ptr
jsc0 = jsf1 """
  %0()
"""

jsc1 : Ptr -> Ptr -> JS_IO Ptr
jsc1 = jsf2 """
  %0( %1 )
"""

jsc2 : Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsc2 = jsf3 """
  %0( %1, %2 )
"""

jsc3 : Ptr -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsc3 = jsf4 """
  %0( %1, %2, %3 )
"""

jsc4 : Ptr -> Ptr -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsc4 = jsf5 """
  %0( %1, %2, %3, %4 )
"""

jsn0 : Ptr -> JS_IO Ptr
jsn0 = jsf1 """
  new %0()
"""

jsn1 : Ptr -> Ptr -> JS_IO Ptr
jsn1 = jsf2 """
  new %0( %1 )
"""

jsn2 : Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsn2 = jsf3 """
  new %0( %1, %2 )
"""

jsn3 : Ptr -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsn3 = jsf4 """
  new %0( %1, %2, %3 )
"""

jsm0 : HasJsPtr a => Ptr -> a -> JS_IO Ptr
jsm0 obj meth = jsf2 """
  %0[ %1 ]()
""" obj !(jsptr meth)

jsm1 : HasJsPtr a => Ptr -> a -> Ptr -> JS_IO Ptr
jsm1 obj meth a0 = jsf3 """
  %0[ %1 ]( %2 )
""" obj !(jsptr meth) a0

jsm2 : HasJsPtr a => Ptr -> a -> Ptr -> Ptr -> JS_IO Ptr
jsm2 obj meth a0 a1 = jsf4 """
  %0[ %1 ]( %2, %3 )
""" obj !(jsptr meth) a0 a1

jsm3 : HasJsPtr a => Ptr -> a -> Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsm3 obj meth a0 a1 a2 = jsf5 """
  %0[ %1 ]( %2, %3, %4 )
""" obj !(jsptr meth) a0 a1 a2

jsa0 : JS_IO Ptr
jsa0 = jsf0 """
  []
"""

jsa1 : Ptr -> JS_IO Ptr
jsa1 = jsf1 """
  [ %0 ]
"""

jsa2 : Ptr -> Ptr -> JS_IO Ptr
jsa2 = jsf2 """
  [ %0, %1 ]
"""

jsa3 : Ptr -> Ptr -> Ptr -> JS_IO Ptr
jsa3 = jsf3 """
  [ %0, %1, %2 ]
"""

-- The g is for "get."
jsg : HasJsPtr a => Ptr -> a -> JS_IO Ptr
jsg obj prop = jsf2 """
  (0, %0[ %1 ])
""" obj !(jsptr prop)

-- The p is for "put."
jsp : HasJsPtr a => Ptr -> a -> Ptr -> JS_IO ()
jsp obj prop val = jsft (Ptr -> Ptr -> Ptr -> JS_IO ()) """
  %0[ %1 ] = %2
""" obj !(jsptr prop) val

jso0 : JS_IO Ptr
jso0 = jsf0 """
  ({})
"""

jsint : Int -> JS_IO Ptr
jsint = jsptr

-- The e is for "eval."
-- The _f is for "sensitive to (f)ree variable clobbering."
jse0_f : String -> JS_IO Ptr
jse0_f code = jsc0 !(jsc1 !(jsf0 "Function") !(jsptr code))

jse1_f : String -> Ptr -> String -> JS_IO Ptr
jse1_f k0 v0 code =
  jsc1 !(jsc2 !(jsf0 "Function") !(jsptr k0) !(jsptr code)) v0

jse2_f : String -> Ptr -> String -> Ptr -> String -> JS_IO Ptr
jse2_f k0 v0 k1 v1 code =
  jsc2
    !(jsc3 !(jsf0 "Function") !(jsptr k0) !(jsptr k1) !(jsptr code))
    v0 v1

jse3_f :
  String -> Ptr ->
  String -> Ptr ->
  String -> Ptr ->
    String -> JS_IO Ptr
jse3_f k0 v0 k1 v1 k2 v2 code =
  jsc3
    !(jsc4 !(jsf0 "Function")
        !(jsptr k0) !(jsptr k1) !(jsptr k2) !(jsptr code))
    v0 v1 v2

-- The a is for "Array."
-- The _i is for "sensitive to (i)nitial value clobbering."
jsa_i : List Ptr -> JS_IO Ptr
jsa_i elements = do
  result <- jsa0
  for_ elements $ \element =>
    jsm1 result "push" element
  return result

-- The o is for "object."
-- The _i is for "sensitive to (i)nitial value clobbering."
jso_i : SortedMap String Ptr -> JS_IO Ptr
jso_i elements = do
  result <- jso0
  for_ {b=()} (Data.SortedMap.toList elements) $ \(k, v) => do
    jsp result k v
  return result

jso1_i : String -> Ptr -> JS_IO Ptr
jso1_i k0 v0 = jso_i (dic1 k0 v0)

jso2_i : String -> Ptr -> String -> Ptr -> JS_IO Ptr
jso2_i k0 v0 k1 v1 = jso_i (dic2 k0 v0 k1 v1)

jso3_i : String -> Ptr -> String -> Ptr -> String -> Ptr -> JS_IO Ptr
jso3_i k0 v0 k1 v1 k2 v2 = jso_i (dic3 k0 v0 k1 v1 k2 v2)

jso4_i :
  String -> Ptr ->
  String -> Ptr ->
  String -> Ptr ->
  String -> Ptr ->
    JS_IO Ptr
jso4_i k0 v0 k1 v1 k2 v2 k3 v3 = jso_i (dic4 k0 v0 k1 v1 k2 v2 k3 v3)

jsfn0 : JS_IO Ptr -> JS_IO Ptr
jsfn0 f = jsft (JsFn (() -> Ptr) -> JS_IO Ptr) """
  %0
""" (MkJsFn (\() => unsafePerformIO f))

jsfn1 : (Ptr -> JS_IO Ptr) -> JS_IO Ptr
jsfn1 f = jsft (JsFn (Ptr -> Ptr) -> JS_IO Ptr) """
  %0
""" (MkJsFn (\a0 => unsafePerformIO (f a0)))

-- NOTE: Surprisingly, this definition of jsfn2 receives both
-- arguments and sucessfully performs its side effects, but it doesn't
-- succeed at returning its result.
{-
jsfn2 : (Ptr -> Ptr -> JS_IO Ptr) -> JS_IO Ptr
jsfn2 f = jsft (JsFn (Ptr -> Ptr -> Ptr) -> JS_IO Ptr) """
  %0
""" (MkJsFn (\a0, a1 => unsafePerformIO (f a0 a1)))
-}

jsfn2_f : (Ptr -> Ptr -> JS_IO Ptr) -> JS_IO Ptr
jsfn2_f f = jse1_f
  "f" !(jsfn1 $ \args =>
          f !(jsg args !(jsint 0)) !(jsg args !(jsint 1)))
  """
    return function ( var_args ) {
        return f( arguments );
    };
  """

jsfn3_f : (Ptr -> Ptr -> Ptr -> JS_IO Ptr) -> JS_IO Ptr
jsfn3_f f = jse1_f
  "f" !(jsfn1 $ \args =>
          f !(jsg args !(jsint 0))
            !(jsg args !(jsint 1))
            !(jsg args !(jsint 2)))
  """
    return function ( var_args ) {
        return f( arguments );
    };
  """

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module Main

import Js.Dom
import Control.ST

data Input = Set
           | Change String

Gui : Dom m => Type
Gui {m} = DomRef {m} () (const String) (const Input) ()

vw : () -> String -> Html Input
vw () s = div [] [form [] Set [input [onchange Change]], div [] [text s]]

procInput : Dom m => (d: Var) -> (s:Var) -> Input -> ST m () [s:::State String, d:::Gui {m}]
procInput d s Set =
  do
    inp <- read s
    call $ domPut d inp
procInput d s (Change new) =
    write s new

pageLoop : Dom m => (d: Var) -> (s:Var) -> ST m () [s:::State String, d:::Gui {m}]
pageLoop d s =
  do
    x <- call $ getInput d
    procInput d s x
    pageLoop d s

page : Dom m => ST m () []
page =
  do
    dom <- initBody [] vw () "ola"
    txt <- new ""
    pageLoop dom txt
    delete txt
    clearDom dom

main : JS_IO ()
main = setASync_ $ run page

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Adjoint
import Data.Morphisms

interface (Functor f, Functor g) => Adjoint (f : Type -> Type) (g : Type -> Type) where
  unit : a -> g (f a)
  counit : f (g a) -> a

phi : Adjoint f g => (f a -> b) -> a -> g b
phi f = map f . unit

psi : Adjoint f g => (a -> g b) -> f a -> b
psi f = counit . map f

Adjoint (Pair a) (Morphism a) where
  unit x = Mor (\y => (y, x))
  counit (x, Mor f) = f x

record Compose (f : Type -> Type) (g : Type -> Type) (a : Type) where
  constructor Comp
  getComp : f (g a)

(Functor f, Functor g) => Functor (Compose f g) where
  map f = Comp . map (map f) . getComp

interface Functor m => Monad' (m : Type -> Type) where
  eta : a -> m a
  mu  : m (m a) -> m a

  (>>=) : m a -> (a -> m b) -> m b
  ma >>= f = (mu . map f) ma

Adjoint f g => Monad' (Compose g f) where
  eta x = Comp (unit x)
  mu = Comp . map (counit . map getComp) . getComp

get : Compose (Morphism s) (Pair s) s
get = (Comp (Mor (\st => (st, st))))

set : s -> Compose (Morphism s) (Pair s) ()
set st = (Comp (Mor (\_ => (st, ()))))

example : Monad' (Compose (Morphism Int) (Pair Int)) => Compose (Morphism Int) (Pair Int) ()
example = do st <- get
             set (st + 1)
             eta ()

test : Int -> (Int, ())
test = applyMor (getComp example)


text:
module Chapter10

import Data.Vect

-- describeList : List Int -> String
-- describeList [] = "Empty"
-- describeList (x::xs) = "Non-empty, tail " ++ show xs

-- data ListLast : List a -> Type where
--   Empty : ListLast []
--   NonEmpty: (xs: List a)-> (x:a) -> ListLast (xs ++ [x])

-- describeHelper : (input: List Int) -> (form: ListLast input) -> String
-- describeHelper [] Empty = ?describeHelper_rhs_1
-- describeHelper (xs ++ [x]) (NonEmpty xs x) = ?describeHelper_rhs_2

-- describeHelper [] form = ?describeHelper_rhs_1
-- describeHelper (_ :: _) Empty impossible
-- describeHelper (_ :: _) (NonEmpty _ _) impossible

--describeHelper [] Empty = "Empty"
--describeHelper (xs ++ [x]) (NonEmpty xs x) = ?hole

-- total
-- listLast : (xs: List a) -> ListLast xs
-- listLast [] = Empty
-- listLast (x :: xs) = case listLast xs of
--   Empty => NonEmpty [] x
--   NonEmpty ys y => NonEmpty (x::ys) y

-- describeListEnd : List Int -> String
-- describeListEnd input with (listLast input)
-- describeListEnd [] | Empty = "test"
-- describeListEnd (xs ++ [x]) | NonEmpty xs x = "test2"

-- recursive views
--data SnocList ty = Empty | Snoc (SnocList ty) ty

--reverseSnoc : SnocList ty -> List ty
--reverseSnoc Empty = []
--reverseSnoc (Snoc xs x) = x :: reverseSnoc xs

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

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

snocList : (input : List a) -> SnocList input
snocList xs = snocListHelp 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 = myReverseHelper input (snocList input)

--myReverse : List a -> List a
--myReverse xs = myReverseHelper xs (snocList input)

-- myReverseHelper (xs ++ [x]) (Snoc rec) = ?myReverseHelper_2

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Implicit

import Data.Vect

-- n, m, elem are unbound implicits
-- Below is converted interanally by Idris into Bound implicits like below.
-- reverse : List elem -> List elem
-- append : Vect n elem -> Vect m elem -> Vect (n + m) elem

-- n, m, elem are bound implicits
reverse : {elem : Type} -> List elem -> List elem
append : {elem : Type} -> {n : Nat} -> {m : Nat} ->  Vect n elem -> Vect m elem -> Vect (n + m) elem

my_length : Vect n elem -> Nat
my_length [] = Z
my_length (x :: xs) = 1 + length xs

-- We can refer to n directly using implicit syntax
my_implicit_length : Vect n elem -> Nat
my_implicit_length {n} xs = n

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module System.File.Types

%default total

||| A pointer to a file.
public export
FilePtr : Type
FilePtr = AnyPtr

||| A file handle.
public export
data File : Type where
     FHandle : FilePtr -> File


text:
module Issue524

%logging totality 20

data Bad = MkBad (Not Bad)

hmmm : Bad -> Not Bad
hmmm (MkBad n) = n

ok : Not Bad
ok bad = hmmm bad bad

bad : Bad
bad = MkBad ok

total
ohno : Void
ohno = ok bad

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module ProofColDivSeqBase
-- module Main -- ビルドするときはこっち > idris ProofColDivSeqBase.idr -o run

%default total
-- %language ElabReflection
%access export

-- mod2
public export
data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd  : Parity (S (n + n))
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

-- mod3
public export
data Mod3 : Nat -> Type where
  ThreeZero : Mod3 (n + n + n)
  ThreeOne  : Mod3 (S (n + n + n))
  ThreeTwo  : Mod3 (S (S (n + n + n)))
helpThreeZero : (j:Nat) -> (plus (plus (S j) (S j)) (S j)) = S (S (S (plus (plus j j) j)))
helpThreeZero j = rewrite sym $ plusSuccRightSucc j j in
                  rewrite sym $ plusSuccRightSucc (plus j j) j in Refl
helpThreeOne : (j:Nat) -> S (plus (plus (S j) (S j)) (S j)) = S (S (S (S (plus (plus j j) j))))
helpThreeOne j = cong {f=S} $ helpThreeZero j
helpThreeTwo : (j:Nat) -> S (S (plus (plus (S j) (S j)) (S j))) = S (S (S (S (S (plus (plus j j) j)))))
helpThreeTwo j = cong {f=S} $ helpThreeOne j
mod3 : (n:Nat) -> Mod3 n
mod3 Z         = ThreeZero {n=Z}
mod3 (S Z)     = ThreeOne {n=Z}
mod3 (S (S Z)) = ThreeTwo {n=Z}
mod3 (S (S (S k))) with (mod3 k)
  mod3 (S (S (S (j + j + j))))         | ThreeZero =
    rewrite sym $ helpThreeZero j in ThreeZero {n=S j}
  mod3 (S (S (S (S (j + j + j)))))     | ThreeOne =
    rewrite sym $ helpThreeOne j in ThreeOne {n=S j}
  mod3 (S (S (S (S (S (j + j + j)))))) | ThreeTwo =
    rewrite sym $ helpThreeTwo j in ThreeTwo {n=S j}
-- ---------------------------------

-- allDivSeqの実装に必要な関数
-- ----- from libs/contrib/Data/CoList.idr -----
public export
codata CoList : Type -> Type where
  Nil : CoList a
  (::) : a -> CoList a -> CoList a

implementation Functor CoList where
  map f []      = []
  map f (x::xs) = f x :: map f xs

implementation Show a => Show (CoList a) where
  show xs = "[" ++ show' "" 20 xs ++ "]" where
    show' : String -> (n : Nat) -> (xs : CoList a) -> String
    show' acc Z _             = acc ++ "..."
    show' acc (S n) []        = acc
    show' acc (S n) [x]       = acc ++ show x
    show' acc (S n) (x :: xs) = show' (acc ++ (show x) ++ ", ") n xs

unfoldr : (a -> Maybe (b, a)) -> a -> CoList b
unfoldr f x =
  case f x of
    Just (y, new_x) => y :: (unfoldr f new_x)
    _               => []
-- ----- from libs/contrib/Data/CoList.idr -----

-- ----- from libs/base/Data/List/Quantifiers.idr -----
public export
data Any : (P : a -> Type) -> List a -> Type where
  Here  : {P : a -> Type} -> {xs : List a} -> P x -> Any P (x :: xs)
  There : {P : a -> Type} -> {xs : List a} -> Any P xs -> Any P (x :: xs)

anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
anyNilAbsurd (Here _)  impossible
anyNilAbsurd (There _) impossible

implementation Uninhabited (Any p Nil) where
  uninhabited = anyNilAbsurd

public export
data All : (P : a -> Type) -> List a -> Type where
  NilA : {P : a -> Type} -> All P Nil
  Cons : {P : a -> Type} -> {xs : List a} -> P x -> All P xs -> All P (x :: xs)
-- ----- from libs/base/Data/List/Quantifiers.idr -----

dsp : List Integer -> Maybe (CoList Integer) -> Maybe (CoList Integer)
dsp xs                 Nothing          = Nothing
dsp xs                 (Just [])        = Nothing
dsp []                 (Just (y :: ys)) = Nothing
dsp (x :: [])          (Just (y :: ys)) = Nothing
dsp (x1 :: (x2 :: xs)) (Just (y :: ys)) = Just (x1 :: (x2+y) :: ys)

dsp2 : List Integer -> Maybe (CoList Integer) -> Maybe (CoList Integer)
dsp2 xs        Nothing          = Nothing
dsp2 xs        (Just [])        = Nothing
dsp2 []        (Just (y :: ys)) = Nothing
dsp2 (x :: xs) (Just (y :: ys)) = Just ((x+y) :: ys)

countEven : Nat -> Nat -> Nat -> (Nat, Nat)
countEven n Z      acc = (acc, n)
countEven n (S nn) acc =
  if (modNatNZ n 2 SIsNotZ) == 1
    then (acc, n)
    else countEven (divNatNZ n 2 SIsNotZ) nn (acc+1)

-- odd only!
divSeq : Nat -> CoList Integer
divSeq = (map toIntegerNat) .
  unfoldr (\b => if b==1 then Nothing
                         else Just (countEven (b*3+1) (b*3+1) 0) )
-- ---------------------------------

-- allDivSeqの実装
mutual
  allDivSeq : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeq x Z = if (modNatNZ x 2 SIsNotZ) == 0 then [Nothing]
    else [Just (divSeq x)]
      ++ (if (modNatNZ (x+7) 4 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+7) 4 SIsNotZ) 2 SIsNotZ) == 1 then [[6,-4] `dsp` (Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ)))] else [])
      ++ (if (modNatNZ (x*6+3) 2 SIsNotZ) == 1 then [[1,-2] `dsp` (Just (divSeq (x*6+3)))] else [])
      ++ (if (modNatNZ (x*3+6) 2 SIsNotZ) == 1 then [[4,-4] `dsp` (Just (divSeq (x*3+6)))] else [])
      ++ (if (modNatNZ (x+1) 2 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+1) 2 SIsNotZ) 2 SIsNotZ) == 1 then [[3,-2] `dsp` (Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ)))] else [])
      ++ (if (modNatNZ (x*12+9) 2 SIsNotZ) == 1 then [[2,-4] `dsp` (Just (divSeq (x*12+9)))] else [])
      ++ (if (modNatNZ (x+3) 8 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+3) 8 SIsNotZ) 2 SIsNotZ) == 1 then [[5,-2] `dsp` (Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ)))] else [])
      ++ (if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21 && (modNatNZ (modNatNZ (x `minus` 21) 64 SIsNotZ) 2 SIsNotZ) == 1 then [[6] `dsp2` (Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ)))] else [])
  allDivSeq x (S lv) = allDivSeq x lv
                    ++ allDivSeqA x lv
                    ++ allDivSeqB x lv
                    ++ allDivSeqC x lv
                    ++ allDivSeqD x lv
                    ++ allDivSeqE x lv
                    ++ allDivSeqF x lv
                    ++ allDivSeqG x lv

  allDivSeqA : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqA x Z =
    if (modNatNZ (x+7) 4 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+7) 4 SIsNotZ) 2 SIsNotZ) == 1
      then [[6,-4] `dsp` (Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ)))]
      else []
  allDivSeqA x (S lv) =
    if (modNatNZ (x+7) 4 SIsNotZ) == 0
      then map ([6,-4] `dsp`) $ allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) (S lv)
      else []

  allDivSeqB : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqB x Z =
    if (modNatNZ (x*6+3) 2 SIsNotZ) == 1
      then [[1,-2] `dsp` (Just (divSeq (x*6+3)))]
      else []
  allDivSeqB x (S lv) =
      map ([1,-2] `dsp`) $ allDivSeq (x*6+3) (S lv)

  allDivSeqC : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqC x Z =
    if (modNatNZ (x*3+6) 2 SIsNotZ) == 1
      then [[4,-4] `dsp` (Just (divSeq (x*3+6)))]
      else []
  allDivSeqC x (S lv) =
      map ([4,-4] `dsp`) $ allDivSeq (x*3+6) (S lv)

  allDivSeqD : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqD x Z =
    if (modNatNZ (x+1) 2 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+1) 2 SIsNotZ) 2 SIsNotZ) == 1
      then [[3,-2] `dsp` (Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ)))]
      else []
  allDivSeqD x (S lv) =
    if (modNatNZ (x+1) 2 SIsNotZ) == 0
      then map ([3,-2] `dsp`) $ allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) (S lv)
      else []

  allDivSeqE : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqE x Z =
    if (modNatNZ (x*12+9) 2 SIsNotZ) == 1
      then [[2,-4] `dsp` (Just (divSeq (x*12+9)))]
      else []
  allDivSeqE x (S lv) =
      map ([2,-4] `dsp`) $ allDivSeq (x*12+9) (S lv)

  allDivSeqF : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqF x Z =
    if (modNatNZ (x+3) 8 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+3) 8 SIsNotZ) 2 SIsNotZ) == 1
      then [[5,-2] `dsp` (Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ)))]
      else []
  allDivSeqF x (S lv) =
    if (modNatNZ (x+3) 8 SIsNotZ) == 0
      then map ([5,-2] `dsp`) $ allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) (S lv)
      else []

  allDivSeqG : Nat -> Nat -> List (Maybe (CoList Integer))
  allDivSeqG x Z =
    if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21 && (modNatNZ (modNatNZ (x `minus` 21) 64 SIsNotZ) 2 SIsNotZ) == 1
      then [[6] `dsp2` (Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ)))]
      else []
  allDivSeqG x (S lv) =
    if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21
      then map ([6] `dsp2`) $ allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) (S lv)
      else []
-- ---------------------------------

-- その他関数
defini : (x, lv:Nat) -> allDivSeq x (S lv) = allDivSeq x lv
                                          ++ allDivSeqA x lv
                                          ++ allDivSeqB x lv
                                          ++ allDivSeqC x lv
                                          ++ allDivSeqD x lv
                                          ++ allDivSeqE x lv
                                          ++ allDivSeqF x lv
                                          ++ allDivSeqG x lv
defini x lv = Refl

definiA0 : (x : Nat) -> (allDivSeqA x Z) =
  (if (modNatNZ (x+7) 4 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+7) 4 SIsNotZ) 2 SIsNotZ) == 1
  then [[6,-4] `dsp` (Just (divSeq (divNatNZ ((x+7)*3) 4 SIsNotZ)))]
  else [])
definiA0 x = Refl
definiA : (x, lv:Nat) -> (allDivSeqA x (S lv)) =
  (if (modNatNZ (x+7) 4 SIsNotZ) == 0
  then map ([6,-4] `dsp`) $ allDivSeq (divNatNZ ((x+7)*3) 4 SIsNotZ) (S lv)
  else [])
definiA x lv = Refl

definiB0 : (x : Nat) -> (allDivSeqB x Z) =
  (if (modNatNZ (x*6+3) 2 SIsNotZ) == 1
  then [[1,-2] `dsp` (Just (divSeq (x*6+3)))]
  else [])
definiB0 x = Refl
definiB : (x, lv:Nat) -> (allDivSeqB x (S lv)) =
  map ([1,-2] `dsp`) $ allDivSeq (x*6+3) (S lv)
definiB x lv = Refl

definiC0 : (x : Nat) -> (allDivSeqC x Z) =
  (if (modNatNZ (x*3+6) 2 SIsNotZ) == 1
  then [[4,-4] `dsp` (Just (divSeq (x*3+6)))]
  else [])
definiC0 x = Refl
definiC : (x, lv:Nat) -> (allDivSeqC x (S lv)) =
  map ([4,-4] `dsp`) $ allDivSeq (x*3+6) (S lv)
definiC x lv = Refl

definiD0 : (x : Nat) -> (allDivSeqD x Z) =
  (if (modNatNZ (x+1) 2 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+1) 2 SIsNotZ) 2 SIsNotZ) == 1
  then [[3,-2] `dsp` (Just (divSeq (divNatNZ ((x+1)*3) 2 SIsNotZ)))]
  else [])
definiD0 x = Refl
definiD : (x, lv:Nat) -> (allDivSeqD x (S lv)) =
  (if (modNatNZ (x+1) 2 SIsNotZ) == 0
  then map ([3,-2] `dsp`) $ allDivSeq (divNatNZ ((x+1)*3) 2 SIsNotZ) (S lv)
  else [])
definiD x lv = Refl

definiE0 : (x : Nat) -> (allDivSeqE x Z) =
  (if (modNatNZ (x*12+9) 2 SIsNotZ) == 1
  then [[2,-4] `dsp` (Just (divSeq (x*12+9)))]
  else [])
definiE0 x = Refl
definiE : (x, lv:Nat) -> (allDivSeqE x (S lv)) =
  map ([2,-4] `dsp`) $ allDivSeq (x*12+9) (S lv)
definiE x lv = Refl

definiF0 : (x : Nat) -> (allDivSeqF x Z) =
  (if (modNatNZ (x+3) 8 SIsNotZ) == 0 && (modNatNZ (modNatNZ (x+3) 8 SIsNotZ) 2 SIsNotZ) == 1
  then [[5,-2] `dsp` (Just (divSeq (divNatNZ ((x+3)*3) 8 SIsNotZ)))]
  else [])
definiF0 x = Refl
definiF : (x, lv:Nat) -> (allDivSeqF x (S lv)) =
  (if (modNatNZ (x+3) 8 SIsNotZ) == 0
  then map ([5,-2] `dsp`) $ allDivSeq (divNatNZ ((x+3)*3) 8 SIsNotZ) (S lv)
  else [])
definiF x lv = Refl

definiG0 : (x : Nat) -> (allDivSeqG x Z) =
  (if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21 && (modNatNZ (modNatNZ (x `minus` 21) 64 SIsNotZ) 2 SIsNotZ) == 1
  then [[6] `dsp2` (Just (divSeq (divNatNZ (x `minus` 21) 64 SIsNotZ)))]
  else [])
definiG0 x = Refl
definiG : (x, lv:Nat) -> (allDivSeqG x (S lv)) =
  (if (modNatNZ (x `minus` 21) 64 SIsNotZ) == 0 && x > 21
  then map ([6] `dsp2`) $ allDivSeq (divNatNZ (x `minus` 21) 64 SIsNotZ) (S lv)
  else [])
definiG x lv = Refl

-- myAny : (a->Bool) -> List a -> Bool
-- myAny pp [] = False
-- myAny pp (x :: xs) = (pp x) || myAny pp xs

limitedNStep : Maybe (CoList Integer) -> Nat -> Bool
limitedNStep Nothing          _     = True
limitedNStep (Just [])        _     = True
limitedNStep (Just (_ :: _))  Z     = False
limitedNStep (Just (_ :: xs)) (S n) = limitedNStep (Just xs) n

public export
data Limited : Maybe (CoList Integer) -> Type where
  IsLimited : (n : Nat ** limitedNStep xs n = True) -> Limited xs

P : Nat -> Nat -> Type
P n lv = Not $ All Limited $ allDivSeq (n+n+n) lv

definiP : (n, lv : Nat)
  -> P n lv = Not $ All Limited $ allDivSeq (n+n+n) lv
definiP n lv = Refl
-- ---------------------------------

-- allDivSeq 0 2が有限項である事を示すため、mainを使う（ビルドして）
main : IO ()
main = traverse_ (putStrLn . show) $ allDivSeq 0 2


text:
module Props.Nat

import Props.Util

%access public export

Greater : Nat -> Nat -> Type
--Greater n m = GT m n
Greater = flip GT

GreaterEqual : Nat -> Nat -> Type
GreaterEqual = flip GTE

Less : Nat -> Nat -> Type
Less = flip LT

LessEqual : Nat -> Nat -> Type
LessEqual = flip LTE

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module ReverseVec

import Data.Nat
import Data.Vect

%default total

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse { n = S k } (x :: xs) = let rev = myReverse xs ++ [x] in
                          rewrite plusCommutative 1 k in rev

ourReverse : Vect n elem -> Vect n elem
ourReverse [] = []
ourReverse (x :: xs) = reverseProof (ourReverse xs ++ [x]) where
  reverseProof : Vect (len + 1) elem -> Vect (S len) elem
  reverseProof { len } xs = rewrite plusCommutative 1 len in xs

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Main

import System
import System.File

main : IO ()
main = do
  efh <- openFile "temporarytestfile" Read
  case efh of
    Right fh => do
      printLn $ "mtime: " ++ show !(fileModifiedTime fh)
      printLn $ "atime: " ++ show !(fileAccessTime fh)
      printLn $ "ctime: " ++ show !(fileStatusTime fh)
      closeFile fh
    Left err => putStrLn $ "file error: " ++ show err

  ignore $ writeFile "temporarytestfile" "#!/usr/bin/env true\n"
  ignore $ chmodRaw "temporarytestfile" 0o755
  rc1 <- system "/usr/bin/true"
  rc2 <- system "ls -la ./temporarytestfile"
  printLn $ the (List Int) [rc1, rc2]

  path <- getEnv "PATH"
  putStrLn $ "$PATH = " ++ show path

  path <- getEnv "NOTEXISTINGENVVAR"
  putStrLn $ "$NOTEXISTINGENVVAR = " ++ show path

  the (IO ()) exitSuccess

  ignore $ fPutStr stdout "to:stdout\n"
  ignore $ fPutStr stderr "to:stderr\n"
  line <- getLine
  putStrLn $ "input was: " ++ show line
  putStrLn $ "please press any key to continue..."
  ch <- fGetChar stdin
  putStrLn $ "thanks for pressing " ++ show ch
  fourChars <- fGetChars stdin 4
  putStrLn $ "thanks for entering " ++ show fourChars
  rest <- fGetChars stdin 1024
  putStrLn $ "rest was: " ++ show rest

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Examples

-- Walk
toCaps : Inline Prime -> Inline Prime
toCaps (Text str) = Text $ toUpper str
toCaps (Sans str) = Sans $ toUpper str
toCaps (Scap str) = Scap $ toUpper str
toCaps (Mono str) = Mono $ toUpper str
toCaps x             = x

modHeader : Block Prime -> Block Prime
modHeader (Header Prime n l xs) = if n <= 3
                                    then Para Prime (map toCaps xs)
                                    else Header Prime n l xs
modHeader x = x

modHeaders : EddaDoc -> EddaDoc
modHeaders = walk modHeader

-- Query

extractURL : Inline Prime -> List String
extractURL (Hyper uri _) = [uri]
extractURL _            = Nil

getURLs : EddaDoc -> List String
getURLs = query extractURL

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
data MyVect : (len: Nat) -> (elem: Type) -> Type where
  Nil  : MyVect 0 elem
  (::) : (e: elem) -> (tail: MyVect len elem) -> MyVect (S len) elem

Eq elem => Eq (MyVect n elem) where
  (==) Nil Nil = True
  (==) (head :: tail) (head' :: tail') = head == head' && tail == tail'

Foldable (MyVect n) where
  foldr func acc Nil = acc
  foldr func acc (e :: tail) =
    let
      foldedTail = foldr func acc tail
    in
      func e foldedTail

data EqNat: (num1: Nat) -> (num2: Nat) -> Type where
  Same: (num: Nat) -> EqNat num num

sameS : (k: Nat) -> (j: Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

-- checkEqNat: (num1: Nat) -> (num2: Nat) -> Maybe (num1 = num2)
-- checkEqNat Z Z = Just Refl
-- checkEqNat Z (S k) = Nothing
-- checkEqNat (S k) Z = Nothing
-- checkEqNat (S k) (S j) =
--   case checkEqNat k j of
--     Nothing => Nothing
--     Just prf => Just (cong prf)

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

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

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

checkEqNat: (num1: Nat) -> (num2: Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSuc
checkEqNat (S k) Z = No sucNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
  Yes prf => Yes (cong prf)
  No contra => No (noRec contra)

exactLength: (len: Nat) -> (input: MyVect m a) -> Maybe (MyVect len a)
exactLength {m} len input =
  case decEq m len of
    Yes Refl  => Just input
    No contra => Nothing

total headUnequal: {xs: MyVect n a} -> {ys: MyVect n a} -> (contra: (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

total tailUnequal: {xs: MyVect n a} -> {ys: MyVect n a} -> (contra: (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (MyVect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) = case decEq x y of
    Yes Refl => case decEq xs ys of
      Yes Refl  => Yes Refl
      No contra => No (tailUnequal contra)
    No contra => No (headUnequal contra)

example1: MyVect 4 Integer
example1 = 1 :: 2 :: 3 :: 4 :: Nil

example1': MyVect 4 Integer
example1' = 1 :: 2 :: 3 :: 4 :: Nil

example2: MyVect 3 Integer
example2 = 1 :: 2 :: 3 :: Nil

example3: MyVect 4 Integer
example3 = 4 :: 3 :: 2 :: 1 :: Nil

natEqual: (x: Nat) -> (y: Nat) -> Maybe(x = y)
natEqual Z Z = Just Refl
natEqual Z (S k) = Nothing
natEqual (S k) Z = Nothing
natEqual (S k) (S j) = case natEqual k j of
  Nothing => Nothing
  (Just prf) => Just (cong prf)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Average

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

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


text:
module Test.Vec

import Test.Assertions
import Idrlisp.Vec

%default covering

export
test : IO ()
test = describe "Idrlisp.Vec" $ do
  describe "empty, new, fromList, toList" $ do
    Vec.toList (the (Vec ()) Vec.empty)
      `shouldBe'` []
    vec <- Vec.new 3 "foo"
    Vec.toList vec
      `shouldBe'` ["foo", "foo", "foo"]
    vec <- Vec.fromList (the (List ()) [])
    Vec.toList vec
      `shouldBe'` []
    vec <- Vec.fromList ["a", "b", "c"]
    Vec.toList vec
      `shouldBe'` ["a", "b", "c"]
  describe "length" $ do
    Vec.length (the (Vec ()) Vec.empty)
      `shouldBe` 0
    vec <- Vec.new 3 "foo"
    Vec.length vec
      `shouldBe` 3
  describe "read" $ do
    vec <- Vec.fromList ["a", "b", "c"]
    Vec.read 0 vec
      `shouldBe'` Just "a"
    Vec.read 1 vec
      `shouldBe'` Just "b"
    Vec.read 2 vec
      `shouldBe'` Just "c"
    Vec.read 3 vec
      `shouldBe'` Nothing
  describe "write" $ do
    vec <- Vec.fromList ["a", "b", "c"]
    Vec.write 0 "x" vec
      `shouldBe'` True
    Vec.write 2 "y" vec
      `shouldBe'` True
    Vec.write 4 "z" vec
      `shouldBe'` False
    Vec.toList vec
      `shouldBe'` ["x", "b", "y"]
  describe "copy" $ do
    src <- Vec.fromList ["a", "b", "c", "d"]
    dest <- Vec.fromList ["1", "2", "3", "4", "5"]
    Vec.copy src 1 dest 2 3
      `shouldBe'` True
    Vec.toList src
      `shouldBe'` ["a", "b", "c", "d"]
    Vec.toList dest
      `shouldBe'` ["1", "2", "b", "c", "d"]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
%default total

test : (f : () -> Bool) -> f () = True
test (\x => True) = Refl

bad : False = True
bad = test (\() => False)


text:
import Data.Vect

maryInVector : Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector = There (There Here)

elemOfEmptyAbsurd : Elem a [] -> Void
elemOfEmptyAbsurd Here impossible
elemOfEmptyAbsurd (There _) impossible

removeElem : (elem : a) -> (v : Vect (S n) a) -> Elem elem v -> Vect n a
removeElem elem (elem :: xs) Here = xs
removeElem {n = Z} elem (x :: []) (There later) = absurd later
removeElem {n = (S k)} elem (x :: xs) (There later) = x :: removeElem elem xs later

removeElem_auto : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem_auto value xs {prf} = removeElem value xs prf

isElem' : DecEq a => (elem : a) -> (v : Vect n a) -> Dec (Elem elem v)
isElem' elem [] = No absurd
isElem' elem (x :: xs) = case decEq elem x of
                              (Yes Refl) => Yes Here
                              (No contraHead) => case isElem' elem xs of
                                                      (Yes prf) => Yes (There prf)
                                                      (No contraTail) => No (\prf => (case prf of
                                                                                Here => contraHead Refl
                                                                                (There later) => contraTail later))

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

data Last : List a -> a -> Type where
  LastOne : Last [a] a
  LastCons : Last as a -> Last (x :: as) a

noLastElemForEmptyList : Last [] a -> Void
noLastElemForEmptyList LastOne impossible
noLastElemForEmptyList (LastCons _) impossible

isLast : DecEq a => (xs : List a) -> (elem : a) -> Dec (Last xs elem)
isLast [] elem = No noLastElemForEmptyList
isLast [e] elem = case decEq elem e of
                       (Yes Refl) => Yes LastOne
                       (No contra) => No (\prf => (case prf of
                                                        LastOne => contra Refl
                                                        (LastCons x) => noLastElemForEmptyList x))
isLast (_ :: y :: ys) elem = case isLast (y::ys) elem of
                               (Yes prf) => Yes $ LastCons prf
                               (No contra) => No (\prf => (case prf of
                                                                (LastCons x) => contra x))