text:
||| Game server for Bautzen 1945
module Bautzen.Server

import Bautzen.Options

import Bautzen.Game
import Bautzen.Network
import Bautzen.REPL

import Data.Strings.Extra

import Builtin
import Prelude
import Data.Nat
import Data.List
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
import System

Logger : Type
Logger = String -> IO ()

mkLogger : Verbosity -> Logger
mkLogger Quiet _ = pure ()
mkLogger (Verbose name) msg =
  putStrLn  $ "[" ++ name ++ "] " ++ msg

handleClient : Logger -> Socket -> SocketAddress -> Game -> IO ()
handleClient log socket addr game = do
  log "waiting for input"
  Right (str, _) <- recv socket 6 -- receive 6 characters representing the length of message to read
    | Left err => do log ("failed to receive length of message " ++ show err) ; close socket -- TODO error handling
  log $ "received  " ++ str
  case parseInteger (unpack str) 0 of
    Nothing => do log ("fail to parse '" ++ str ++ "' to expected number of characters, ignoring") ; handleClient log socket addr game
    Just len => do Right (msg, _) <- recv socket (fromInteger len)
                     | Left err => do log ("failed to read message " ++ show err) ; handleClient log socket addr game
                   log $ "received '" ++ msg ++ "'"
                   let (res, game') = commandHandler game msg
                   log $ "result is '" ++ show res ++ "'"
                   let lens = padWith0 (cast $ length res)
                   log $ "sending " ++ lens ++ " chars"
                   Right l <- send socket (lens ++ res)
                     | Left err => do log ("failed to send message " ++ show err) ; close socket -- TODO error handling
                   log $ "sent result"
                   handleClient log socket addr game'

serve : Logger -> Socket -> IO (Either String ())
serve log sock = do
  log "awaiting clients"
  Right (s, addr) <- accept sock
    | Left err => pure (Left $ "Failed to accept on socket with error: " ++ show err)
  log $ "client connecting from " ++ show addr
  pid <- fork (handleClient log s addr initialGame)
  log $ "forked client handler"
  serve log sock

export
server : Options -> IO (Either String ())
server (MkOptions port host _ verbosity) = do
  Right sock <- socket AF_INET Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- bind sock (Just (Hostname host)) port
  if res /= 0
    then pure (Left $ "Failed to bind socket with error: " ++ show res)
    else do
      res <- listen sock
      if res /= 0
        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
        else serve (mkLogger verbosity) sock

max_stars_repo_name: abailly/hsgames

max_issues_repo_name: abailly/acquire

max_forks_repo_name: abailly/acquire


text:
import Data.Vect

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

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

total
removeElem : (value: a) -> (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem {n = Z} value (y :: []) {prf = There later} = absurd later
removeElem {n = (S k)} value (y :: ys) {prf = There later}
                                          = y :: removeElem value ys

data ValidInput : List Char -> Type where
  Letter : (c : Char) -> ValidInput [c]

nilFailure : (s : String) -> ValidInput [] -> Void
nilFailure _ (Letter _) impossible

twoFailure : (s : String) -> ValidInput (x :: (y :: xs)) -> Void
twoFailure _ (Letter _) impossible

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s) where
  isValidInput : (cs : List Char) -> Dec (ValidInput cs)
  isValidInput [] = No (nilFailure s)
  isValidInput (x :: []) = Yes (Letter x)
  isValidInput (x :: (y :: xs)) = No (twoFailure s)

readGuess : IO (x ** ValidInput x)
readGuess = do putStr "Guess:"
               x <- getLine
               case isValidString (toUpper x) of
                    Yes prf => pure (_ ** prf)
                    No contra => do putStr "Invalid guess"
                                    readGuess

processGuess : (letter : Char) ->
               WordState (S guesses) (S letters) ->
               Either (WordState guesses (S letters))
                      (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
                                                      (Yes prf) => Right (MkWordState word (removeElem letter missing))
                                                      (No contra) => Left (MkWordState word missing)

game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st
     = do (_ ** Letter letter) <- readGuess
          case processGuess letter st of
               Left l => do putStrLn "Wrong!"
                            case guesses of
                                 Z => pure (Lost l)
                                 S k => game l
               Right r => do putStrLn "Right!"
                             case letters of
                                  Z => pure (Won r)
                                  S k => game r

main : IO ()
main = do result <- game {guesses = 2}
                 (MkWordState "Test" ['T','E', 'S'])
          case result of
               Lost (MkWordState word missing) =>
                    putStrLn ("You lose. The word was " ++ word)
               Won game =>
                   putStrLn "You win!"

ext: idr


text:
module HEff

-- Based on https://github.com/effectfully/Eff/blob/master/Resources/Core.agda

import Data.HVect

Effect : Type -> Type
Effect r = r -> (a : Type) -> (a -> r) -> Type

Effects : (Type -> Type) -> Vect n Type -> Vect n Type
Effects f [] = []
Effects f (x :: xs) = f x :: Effects f xs

data Exists' : {t : Type} -> {rs : Vect n Type} ->
               HVect rs -> t -> HVect (Effects Effect rs) -> Effect t -> Type where
  Here : Exists' (x :: xs) x (y :: ys) y
  There : Exists' xs x ys y -> Exists' (_ :: xs) x (_ :: ys) y

update' : {t : Type} -> (r : HVect rs) -> (e : Exists' {t = t} r s effs eff) -> t -> HVect rs
update' [] Here _ impossible
update' [] (There _) _ impossible
update' (x :: xs) Here v = v :: xs
update' (x :: xs) (There e) v = x :: update' xs e v

HEffect : Type
HEffect = {n : Nat} -> (rs : Vect n Type) -> HVect (Effects Effect rs) -> Effect (HVect rs)

data HEff : HEffect where
  Pure : (x : a) -> HEff rs effs (r' x) a r'
  Bind : (e : Exists' r s effs eff) ->
          eff s a s' ->
          ((x : a) -> HEff rs effs (update' r e (s' x)) b r'') -> HEff rs effs r b r''

(>>=) : HEff rs effs r a r' -> ((x : a) -> HEff rs effs (r' x) b r'') -> HEff rs effs r b r''
(>>=) (Pure x) f = f x
(>>=) (Bind e x f) g = Bind e x (\y => f y >>= g)

data Access = LoggedOut | LoggedIn
data Store : Access -> (ty : Type) -> (ty -> Access) -> Type where
  Login : Store LoggedOut () (const LoggedIn)
  Logout : Store LoggedIn () (const LoggedOut)

login : {auto e : Exists' r LoggedOut effs Store} ->
         HEff rs effs r () (\_ => update' r e LoggedIn)
login {e} = Bind e Login Pure

logout : {auto e : Exists' r LoggedIn effs Store} ->
         HEff rs effs r () (\_ => update' r e LoggedOut)
logout {e} = Bind e Logout Pure

data State : Type -> (a : Type) -> (a -> Type) -> Type where
  Get : State s s (const s)
  Put : s' -> State s () (const s')

get : {auto e : Exists' r s effs State} ->
      HEff rs effs r s (\_ => update' r e s)
get {e} = Bind e Get Pure

put : {auto e : Exists' r s effs State} -> s' ->
      HEff rs effs r () (\_ => update' r e s')
put {e} s' = Bind  e (Put s') Pure

run : HEff [] [] r a r' -> a
run (Pure x) = x
run (Bind Here _ _) impossible
run (Bind (There _) _ _) impossible

head' : HVect xs -> head xs
head' (x :: _) = x
tail' : HVect xs -> HVect (tail xs)
tail' (x :: xs) = xs

runStore : HEff (Access :: rs) (Store :: effs) r a r' -> HEff rs effs (tail' r) a (\x => tail' $ r' x)
runStore (Pure x) = Pure x
runStore (Bind Here Login f) = runStore $ f ()
runStore (Bind Here Logout f) = runStore $ f ()
runStore (Bind (There e) eff f) = Bind e eff (\x => runStore $ f x)

runState : (head' r) -> HEff (Type :: rs) (State :: effs) r a r' ->  HEff rs effs (tail' r) (DPair a (\x => head' $ r' x)) (\x => tail' $ r' (fst x))
runState s (Pure x) = Pure (x ** s)
runState s (Bind Here Get f) = runState s $ f s
runState s (Bind Here (Put s') f) = runState s' $ f ()
runState s (Bind (There e) eff f) = Bind e eff (\x => runState s $ f x)

example : HEff [Access, Type] [Store, State] [LoggedOut, Nat] Nat (\n => [LoggedOut, Vect n Bool])
example = do login
             n <- get
             put (replicate n True)
             logout
             Pure n

test : DPair Nat (\n => Vect n Bool)
test = run . runState 3 . runStore $ example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
infixr 5 ::

export
data List a = Nil | (::) a (List a)
export
data Nat = Z | S Nat

export
data Vect : Type -> Type where
export
data Set : Type -> Type where

namespace Vect
  export
  toList : Vect a -> List a
  export
  fromList : List a -> Vect a

namespace Set
  export
  toList : Set a -> List a
  export
  fromList : List a -> Set a

keepUnique : List b -> List b
keepUnique {b} xs = toList (fromList xs)


text:
module Text.Markup.Edda.LaTeX

import public Text.Markup.Edda.Model
import public Text.Markup.Edda.Walk
import public Text.Markup.Edda.Query

import public Text.Markup.Edda.Writer.LaTeX

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
||| Vim for Idris Cheatcodes
|||
||| Ctrl-wv split window vertically
||| Ctrl-ww switch windows
|||
||| Ref : http://www.worldtimzone.com/res/vi.html
|||
||| :VimShell -> start a shell
||| idris  -> Start a REPL
|||
||| From the other windows (Idris vim mode)
|||
||| \d adds a template definition for the name declared on the current line (using :addclause).
||| \c case splits the variable at the cursor (using :casesplit).
||| \m adds the missing cases for the name at the cursor (using :addmissing).
||| \w adds a with clause (using :makewith).
||| \o invokes a proof search to solve the hole under the cursor (using :proofsearch).
||| \p invokes a proof search with additional hints to solve the hole under the cursor (using :proofsearch).
|||
||| There are also commands to invoke the type checker and evaluator:
|||
||| \t displays the type of the (globally visible) name under the cursor. In the case of a hole, this displays the context and the expected type.
||| \e prompts for an expression to evaluate.
||| \r reloads and type checks the buffer.
|||
||| Ref : http://docs.idris-lang.org/en/latest/tutorial/interactive.html#interactive-editing-in-vim
|||
||| Idris syntax : https://github.com/idris-lang/Idris-dev/blob/master/docs/reference/syntax-guide.rst
|||

|||
||| Kleene logic
||| inspied from Bool.idr
|||
module Kleene

import Fool
import Data.Vect

||| Defining a type for a list of possible values
Fools : Type
Fools = Vect 3 Fool

--defiing aliases for convenienve
FF : Fool
FF = Just False

FT : Fool
FT = Just True

FU : Fool
FU = Nothing

||| Three values for Kleene logic as data (useful ? can we infer it from the Fool type definition ?)
fool : Fools
fool = [FF, FU, FT]

||| For simple representation of unary operators
truth_vector : (op: Fool -> Fool) -> Fools
truth_vector op = [op FF, op FU, op FT]

-- TODO : express this with Pair (ie product) ?

||| For simple representation of dual operators
truth_table : (dop: Fool -> Fool -> Fool) -> Vect 3 Fools
truth_table dop = [ truth_vector (dop FF), truth_vector (dop FU), truth_vector (dop FT)]

-- TODO : for more complex stuff
-- truth_hyper : (op n-ary)

-- TODO : how ot make that generic ?? any type, any number of value, any arity in operator ?
--        answer : dependent functions, dependent types...
-- TODO : pretty print of that table ?

-- ||| Truth Table Proof
-- TT: Kool -> Lazy Kool -> Kool -> Kool -> Kools
-- TT op = [ op F, op U, op T ]

-- TT and F = [ F, F, F ]
-- TT and U = [ F, U, U ]
-- TT and T = [ F, U, T ]

-- Check for more : Working with universes : https://www.youtube.com/watch?v=AWeT_G04a0A -> interpret PPM...

max_stars_repo_name: asmodehn/idris-playground

max_issues_repo_name: asmodehn/idris-playground

max_forks_repo_name: asmodehn/idris-playground


text:
module Test.Extra.StringTest

import IdrTest.Test
import IdrTest.Expectation

import Extra.String

export
suite : Test
suite =
  describe "String Extra Tests"
    [ test "Replace String" (\_ => assertEq
        (replace "abba" "oodle" "My String Yabba Dabba")
        "My String Yoodle Doodle"
      ),
      test "Quote String" (\_ => assertEq
        (quote "my string\nis cool")
        "\"my string\\nis cool\""
      ),
      test "Unquote String" (\_ => assertEq
        (unquote "\"my string\\nis cool\"")
        "my string\nis cool"
      ),
      test "Limit Limited" (\_ => assertEq
        (limit 4 "this is cool")
        "this..."
      ),
      test "Limit Unlimited" (\_ => assertEq
        (limit 40 "this is cool")
        "this is cool"
      )
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Language.Reflection

%language ElabReflection

elabTry : Elab ()
elabTry
    = try (declare `[ x : 94
                      x = 94 ])
          (declare `[ x : Int
                      x = 94 ])

%runElab elabTry


text:
||| A heterogeneous list. This was introduced in
||| chapter *Functor and Friends* and is also used in
||| later chapters
module Data.HList

import Data.Fin

%default total

public export
data HList : (ts : List Type) -> Type where
  Nil  : HList Nil
  (::) : (v : t) -> (vs : HList ts) -> HList (t :: ts)

public export
head : HList (t :: ts) -> t
head (v :: _) = v

public export
tail : HList (t :: ts) -> HList ts
tail (_ :: t) = t

public export
(++) : HList xs -> HList ys -> HList (xs ++ ys)
[]        ++ ws = ws
(v :: vs) ++ ws = v :: (vs ++ ws)

public export
indexList : (as : List a) -> Fin (length as) -> a
indexList (x :: _)   FZ    = x
indexList (_ :: xs) (FS y) = indexList xs y
indexList []        x impossible

public export
index : (ix : Fin (length ts)) -> HList ts -> indexList ts ix
index FZ     (v :: _)  = v
index (FS x) (_ :: vs) = index x vs
index ix [] impossible


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 12, section 3

-- check that all functions are total
%default total

record Votes where
  constructor MkVotes
  upvotes : Integer
  downvotes : Integer

record Article where
  constructor MkArticle
  title : String
  url : String
  score : Votes

initPage : (title : String) -> (url : String) -> Article
initPage title url = MkArticle title url (MkVotes 0 0)

getScore : Article -> Integer
getScore a = let s = score a in (upvotes s) - (downvotes s)

badSite : Article
badSite = MkArticle "Bad Page" "http://example.com/bad" $ MkVotes 5 47

goodSite : Article
goodSite = MkArticle "Good Page" "http://example.com/good" $ MkVotes 101 7

addUpVote : Article -> Article
addUpVote = record { score->upvotes $= (+1) }

addDownVote : Article -> Article
addDownVote = record { score->downvotes $= (+1) }

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Case

listId : List a -> List a
listId xs = case xs of
  [] => []
  (x :: xs) => x :: listId xs

listRev : List a -> List a
listRev = \case
  [] => []
  (x :: xs) => listRev xs ++ [x]

listFilter2 : (p, q : a -> Bool) -> List a -> List a
listFilter2 p q xs
  = do x <- xs
       -- let pat
       let True = p x
         | False => []
       -- do pat
       True <- pure (q x)
         | False => []
       pure x


text:
module Attributes

import public Mrk.Languages
import public Mrk.LinkTypes
import public Mrk.MimeTypes
import public Mrk.Charsets

%default total
%access public export

URI : Type
URI = String

interface AttributeValue a where
  toAttr : a -> String

data Attribute : Type where
  ClassNames : AttributeValue a => List a -> Attribute
  Href : URI -> Attribute
  Lang : Language -> Attribute
  Rel : LinkType -> Attribute
  MimeType : MimeType -> Attribute
  Src : URI -> Attribute
  Alt : String -> Attribute
  Charset : Charset -> Attribute
%name Attribute attr

showAttr : (name : String) -> (value : String) -> String
showAttr name value = name ++ "=\"" ++ value ++ "\""

Show Attribute where
  show (ClassNames names) = showAttr "class" (unwords (map toAttr names))
  show (Href uri) = showAttr "href" uri
  show (Lang lang) = showAttr "lang" (show lang)
  show (Rel linkType) = showAttr "rel" (show linkType)
  show (MimeType mt) = showAttr "type" (show mt)
  show (Src uri) = showAttr "src" uri
  show (Alt alt) = showAttr "alt" alt
  show (Charset UTF8) = showAttr "charset" "utf-8"

Eq Attribute where
  (ClassNames xs) == (ClassNames ys) =
    map toAttr xs == map toAttr ys
  (Href x) == (Href y) =
    x == y
  (Rel x) == (Rel y) =
    x == y
  _ == _ =
    False

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module City

public export
record City where
  constructor CreateCity
  id : Integer
  title : String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
-- --------------------------------------------------------------- [ RCard.idr ]
-- Module    : RCard.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Frigg.RCard

%access export

public export
data LetterScale = A | B | C | D | E

public export
data GBUScale = Good | Bad | Ugly

public export
data Grade : Type -> Type where
  MkGrade : (value : a) -> (remark : String) -> Grade a

value : Grade a -> a
value (MkGrade val _) = val

remark : Grade a -> String
remark (MkGrade _ rmk) = rmk

public export
record RCard where
  constructor MkRCard
  coherency   : Maybe (Grade LetterScale)
  atomicity   : Maybe (Grade LetterScale)
  problemIndy : Maybe (Grade LetterScale)
  soltApprops : Maybe (Grade Float)
  soltComplex : Maybe (Grade GBUScale)
  soltEff     : Maybe (Grade LetterScale)
  pattStruct  : Maybe (Grade Float)
  presLeg     : Maybe (Grade Float)
  presAccess  : Maybe (Grade LetterScale)

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Cordial.Model.Interface.Ports

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import Cordial.Model.Common
import Cordial.Model.Specification
import Cordial.Model.Projection

import Cordial.Model.Interface.Kinds

%default total
%access public export

--@TODO make width better.

||| Physical manifestation of a port on an IP Core interface.
|||
||| @annot Some annotation.
||| @labelTy Universe that logical names arise from.
||| @endpoint Are we producing/consuming information.
||| @pportTy  The originating projected port type that constrains the value level values.
|||
data Port : (annot    : Type)
         -> (labelTy    : Type)
         -> (portTy   : PortTy annot labelTy)
         -> (pportTy  : ProjectedPortTy labelTy endpoint portTy)
         -> (endpoint : Endpoint)
         -> (endian   : Maybe Endian)
         -> Type
  where

    General : (info        : annot)
           -> (doc         : DocString)
           -> (origin      : Origin)
           -> (sensitivity : Sensitivity)
           -> (label       : Name nKind labelTy)
           -> (width       : PortWidth wty dwidth)
           -> (direction   : Direction endpoint flow)
           -> (dendian     : DataEndian endian)
           -> Port annot labelTy
                   (PortDesc  info' wty label General flow      dwidth sensitivity opt      origin vorigin doc')
                   (PPortDesc       wty label General direction dwidth sensitivity required origin vorigin)
                   endpoint endian

    Information : (info        : annot)
               -> (doc         : DocString)
               -> (origin      : Origin)
               -> (sensitivity : Sensitivity)
               -> (label       : Name nKind labelTy)
               -> (width       : PortWidth wty dwidth)
               -> (direction   : Direction endpoint flow)
               -> (dendian     : DataEndian endian)
               -> Port annot labelTy
                       (PortDesc  info' wty label Information flow      dwidth sensitivity opt      origin vorigin doc')
                       (PPortDesc       wty label Information direction dwidth sensitivity required origin vorigin)
                       endpoint endian

    Clock : (info        : annot)
         -> (doc         : DocString)
         -> (origin      : Origin)
         -> (width       : PortWidth WIRE dwidth)
         -> (label       : Name nKind labelTy)
         -> (direction   : Direction endpoint flow)
         -> (sensitivity : Sensitivity)
         -> (clockInfo   : ClockInfo (Clock mce md mtc) direction)
         -> Port annot labelTy
                 (PortDesc  info' WIRE label (Clock mce md mtc) flow      dwidth sensitivity opt      origin vorigin doc')
                 (PPortDesc       WIRE label (Clock mce md mtc) direction dwidth sensitivity required origin vorigin)
                 endpoint endian

    Address : (info        : annot)
           -> (doc         : DocString)
           -> (origin      : Origin)
           -> (sensitivity : Sensitivity)
           -> (label       : Name nKind labelTy)
           -> (width       : PortWidth ARRAY dwidth)
           -> (direction : Direction endpoint flow)
           -> (dendian : DataEndian endian)
           -> Port annot labelTy
                   (PortDesc  info' ARRAY  label AddressWire flow      dwidth sensitivity opt      origin vorigin doc')
                   (PPortDesc        ARRAY label AddressWire direction dwidth sensitivity required origin vorigin)
                   endpoint endian

    Data : (info        : annot)
        -> (doc         : DocString)
        -> (origin      : Origin)
        -> (sensitivity : Sensitivity)
        -> (label       : Name nKind labelTy)
        -> (width       : PortWidth ARRAY dwidth)
        -> (direction   : Direction endpoint flow)
        -> (dendian     : DataEndian endian)
        -> Port annot labelTy
                (PortDesc  info' ARRAY label DataWire flow      dwidth sensitivity opt      origin vorigin doc')
                (PPortDesc       ARRAY label DataWire direction dwidth sensitivity required origin vorigin)
                endpoint endian

    Reset : (info        : annot)
         -> (doc         : DocString)
         -> (origin      : Origin)
         -> (size        : PortWidth WIRE dwidth)
         -> (label       : Name nKind labelTy)
         -> (direction   : Direction endpoint flow)
         -> (sensitivity : Sensitivity)
         -> Port annot labelTy
                  (PortDesc  info' WIRE label Reset flow      dwidth sensitivity opt      origin vorigin doc')
                  (PPortDesc       WIRE label Reset direction dwidth sensitivity required origin vorigin)
                  endpoint endian

    Interrupt : (info        : annot)
             -> (doc         : DocString)
             -> (origin      : Origin)
             -> (size        : PortWidth WIRE dwidth)
             -> (label       : Name nKind labelTy)
             -> (direction   : Direction endpoint flow)
             -> (sensitivity : Sensitivity)
             -> Port annot labelTy
                      (PortDesc  info' WIRE label Interrupt flow      dwidth sensitivity opt      origin vorigin doc')
                      (PPortDesc       WIRE label Interrupt direction dwidth sensitivity required origin vorigin)
                      endpoint endian

    Control : (info        : annot)
           -> (doc         : DocString)
           -> (origin      : Origin)
           -> (size        : PortWidth WIRE dwidth)
           -> (label       : Name nKind labelTy)
           -> (direction   : Direction endpoint flow)
           -> (sensitivity : Sensitivity)
           -> Port annot labelTy
                    (PortDesc info' WIRE label Control flow      dwidth sensitivity opt      origin vorigin doc')
                    (PPortDesc      WIRE label Control direction dwidth sensitivity required origin vorigin)
                    endpoint endian

namespace Calculated
  Port : (annot : Type)
      -> (labelTy : Type)
      -> (endpoint : Endpoint)
      -> (endian : Maybe Endian)
      -> (portType : PortTy annot labelTy)
      -> Type
  Port x labelTy endpoint endian portType =
    Ports.Port x labelTy portType (projectPort endpoint portType) endpoint endian

data OptionalPort : (p : Port annot labelTy type projectedType endpoint endian) -> Type where
  PortIsOptional : (prfType : OptionalPortType endpoint type)
                -> (prfProjection : OptionalProjectedPort type endpoint projectedType)
                -> (port : Port annot labelTy type projectedType endpoint endian)
                -> OptionalPort port

data SystemPort : (p : Port annot labelTy type projectedType endpoint endian) -> Type where
  PortIsSystem : (port : Port annot labelTy type projectedType endpoint endian)
              -> (prfProjection : SystemProjectedPort type projectType)
              -> SystemPort port

data IPPort : (p : Port annot labelTy type projectedType endpoint endian) -> Type where
  PortIsIP : (port : Port annot labelTy type projectedType endpoint endian)
          -> (prfProjection : IPProjectedPort type projectedType)
          -> IPPort port

isSystemPort_rhs_rhs_2 : (contra : SystemProjectedPort type projectedType -> Void) -> SystemPort p -> Void
isSystemPort_rhs_rhs_2 contra (PortIsSystem p prfProjection) = contra (ProjectedPortIsSystem ?isSystemPort_rhs_rhs_2_rhs_2)

isSystemPort : (p : Port annot labelTy type projectedType endpoint endian)
            -> Dec (SystemPort p)
isSystemPort p {projectedType} with (isProjectedPortSystem projectedType)
  isSystemPort p {projectedType = projectedType} | (Yes prf) = Yes (PortIsSystem p prf)
  isSystemPort p {projectedType = projectedType} | (No contra) = No (isSystemPort_rhs_rhs_2 contra)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Compiler.PrepareCode

import Data.Maybe

import Core.Name
import Compiler.VMCode
import Libraries.Data.SortedMap

%default covering

mutual
  collectConstructorNames : List VMInst -> List Name
  collectConstructorNames is = concatMap constructorNamesInst is

  constructorNamesInst : VMInst -> List Name
  constructorNamesInst (MKCON _ (Right n) _) = [n]
  constructorNamesInst (CASE _ alts def) = concatMap constructorNamesAlt alts ++ collectConstructorNames (fromMaybe [] def)
  constructorNamesInst _ = []

  constructorNamesAlt : (Either Int Name, List VMInst) -> List Name
  constructorNamesAlt (Left _, is) = collectConstructorNames is
  constructorNamesAlt (Right n, is) = n :: (collectConstructorNames is)

getNames : VMDef -> List Name
getNames (MkVMFun _ is) = collectConstructorNames is
getNames (MkVMError is) = collectConstructorNames is

export
getNameMap : List VMDef -> (SortedMap Name Int)
getNameMap vms =
  let conNames = concatMap getNames vms in
      fst $ foldl insertName (empty, 1) conNames
      where
        insertName : (SortedMap Name Int, Int) -> Name -> (SortedMap Name Int, Int)
        insertName (m, i) n = case lookup n m of
                                   Just _ => (m, i)
                                   Nothing => (insert n i m, i+1)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
safeDivide : Double -> Double -> Maybe Double
safeDivide x y = if y == 0 then Nothing
                           else Just (x/y)


text:
> module SequentialDecisionProblems.applications.LowHigh

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

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

* Low / High emissions:

> data LowHigh = Low | High

* |LowHigh| is finite and non-empty:

> to : LowHigh -> Fin 2
> to Low  =    FZ
> to High = FS FZ

> from : Fin 2 -> LowHigh
> from             FZ   = Low
> from         (FS FZ)  = High
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : LowHigh) -> from (to a) = a
> fromTo Low  = Refl
> fromTo High = Refl

> |||
> finiteLowHigh : Finite LowHigh
> finiteLowHigh = MkSigma 2 (MkIso to from toFrom fromTo)

> |||
> cardNotZLowHigh : CardNotZ finiteLowHigh
> cardNotZLowHigh = cardNotZLemma finiteLowHigh Low

* |LowHigh| is in |DecEq|:

> lowNotHigh : Low = High -> Void
> lowNotHigh Refl impossible

> implementation [DecEqLowHigh] DecEq LowHigh where
>   decEq Low  Low  = Yes Refl
>   decEq Low  High = No lowNotHigh
>   decEq High Low  = No (negEqSym lowNotHigh)
>   decEq High High = Yes Refl

* |LowHigh| is in |Eq|:

> implementation Eq LowHigh where
>   (==)  Low  Low = True
>   (==)  Low High = False
>   (==) High  Low = False
>   (==) High High = True

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Ex6

import Data.Vect

%default total

Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [1, 2, 3]]

data Format = Integ Format
            | Dbl Format
            | Chr Format
            | Str Format
            | Lit String Format
            | End

PrintfType : (fmt : Format) -> Type
PrintfType (Integ fmt) = (i : Int) -> PrintfType fmt
PrintfType (Dbl fmt) = (d : Double) -> PrintfType fmt
PrintfType (Chr fmt) = (c : Char) -> PrintfType fmt
PrintfType (Str fmt) = (s : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printfFmt : Num ty => (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Integ fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Dbl fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Lit str fmt) acc = printfFmt fmt (acc ++ str)
printfFmt End acc = acc

toFormat : List Char -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Integ (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dbl (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chr (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

printf : (inp : String) -> PrintfType (toFormat (unpack inp))
printf fmt = printfFmt (toFormat (unpack fmt)) ""

{-

  TupleVect 0 ty = ()
  TupleVect 1 ty = (ty, ())
  TupleVect 2 ty = (ty, (ty, ()))
  ...

-}

TupleVect : (nesting : Nat) -> (elemType : Type) -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

test : TupleVect 5 Nat
test = (1, 2, 3, 4, 5, ())

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:
-- This shows python style string multiplication
-- 'xy_' * 5 = 'xy_xy_xy_xy_xy_'
--
module Main
import Data.Strings

myStrMult : String -> Nat -> String
myStrMult str 0 = ""
myStrMult str (S k) = str ++ myStrMult str k

main : IO ()
main = do printLn $ myStrMult "xy_" 5
          putStr "Enter a String: "
          str <- getLine
          putStr "Enter a positive Integer: "
          num <- getLine
          printLn $ myStrMult str (stringToNatOrZ num)


text:
module Main

import Cairo

public export
%foreign
    "linear_implicits:range_check_ptr, pedersen_ptr"
    "imports:starkware.cairo.common.pow pow, starkware.cairo.common.hash hash2, starkware.cairo.common.cairo_builtins HashBuiltin"
    """
    code:
    # Important notes:
    # - Parameters are untyped
    # - Implicit paramters come first in the same order as listed aboove in "linear_implicits"
    # - The results come first, followed by the implicits, again in the same order
    func Main_externalfn(range_check_ptr, pedersen_ptr, a, b) -> (res, range_check_ptr, pedersen_ptr):
        let (p) = pow{range_check_ptr=range_check_ptr}(a,b)
        let pedersen_ptr_cast = cast(pedersen_ptr, HashBuiltin*)
        let (res) = hash2{hash_ptr=pedersen_ptr_cast}(p,p)
        return (res, range_check_ptr, cast(pedersen_ptr_cast, felt))
    end
    """
externalfn : Felt -> Felt -> Felt

%noinline
main : Cairo ()
main = output $ externalfn 2 3

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Rhone.Canvas.Shape

import Control.MonadRec
import Data.Iterable
import JS
import Rhone.Canvas.Angle
import Web.Html

%default total

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

namespace PathType
  public export
  data PathType = Fill | Stroke

public export
data Segment : Type where
  Move  :  (x,y : Double) -> Segment
  Line  :  (x,y : Double) -> Segment
  Arc   :  (x,y,radius       : Double)
        -> (start,stop       : Angle)
        -> (counterclockwise : Bool)
        -> Segment
  ArcTo :  (x1,y1,x2,y2,radius : Double) -> Segment

namespace RectType
  public export
  data RectType = Fill | Stroke | Clear

public export
data Shape : Type where
  Rect   : (x,y,w,h : Double) -> RectType -> Shape
  Path   : List Segment -> PathType -> Shape
  Shapes : List Shape -> Shape

export
circle : (x,y,radius : Double) -> PathType -> Shape
circle x y r = Path [Arc x y r (rad 0) (rad $ 2 * pi) False]

export
polyLine : List (Double,Double) -> Shape
polyLine []           = Path [] Stroke
polyLine ((x,y) :: t) = Path (Move x y :: map (uncurry Line) t) Stroke

export
Semigroup Shape where
  x         <+> Shapes [] = x
  Shapes [] <+> y         = y
  Shapes xs <+> Shapes ys = Shapes $ xs ++ ys
  x         <+> Shapes ys = Shapes $ x :: ys
  x         <+> y         = Shapes [x,y]

export
Monoid Shape where
  neutral = Shapes []

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

applySegment : CanvasRenderingContext2D -> Segment -> JSIO ()
applySegment ctxt (Move x y) = moveTo ctxt x y
applySegment ctxt (Line x y) = lineTo ctxt x y
applySegment ctxt (Arc x y r start stop ccw) = do
  arc ctxt x y r (toRadians start) (toRadians stop) (Def ccw)
applySegment ctxt (ArcTo x1 y1 x2 y2 radius) =
  arcTo ctxt x1 y1 x2 y2 radius

mutual
  export
  applyAll : CanvasRenderingContext2D -> List Shape -> JSIO ()
  applyAll ctxt = assert_total $ forM_ (apply ctxt)

  export
  apply : CanvasRenderingContext2D -> Shape -> JSIO ()
  apply ctxt (Rect x y w h Fill)   = fillRect ctxt x y w h
  apply ctxt (Rect x y w h Stroke) = strokeRect ctxt x y w h
  apply ctxt (Rect x y w h Clear)  = clearRect ctxt x y w h
  apply ctxt (Path ss st)          = do
    beginPath ctxt
    forM_ (applySegment ctxt) ss
    case st of
      Fill   => fill ctxt Undef
      Stroke => stroke ctxt
  apply ctxt (Shapes xs)           = applyAll ctxt xs


text:
module Task

import public Control.Monad.Ref
import        Control.Monad.Trace

import public Task.Semantics
import public Task.Internal

%default total
%access export

infixr 4 #
infixl 3 <*>, <&>
infixr 2 <|>, <?>
infixl 1 >>=, >>?

-- Running ---------------------------------------------------------------------

public export
Task : Ty -> Type
Task = TaskT IO

public export
Loc : (b : Ty) -> Type
Loc b = IORef (typeOf b)

covering
run : Task a -> Input -> IO (Task a)
run = drive

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

-- Functor --

(<$>) : (typeOf a -> typeOf b) -> TaskT m a -> TaskT m b
(<$>) f t =
  Then t (\x => Edit (Just (f x)))

-- Monoidal --

pure : (typeOf a) -> TaskT m a
pure = Edit . Just

(<&>) : TaskT m a -> TaskT m b -> TaskT m (PAIR a b)
(<&>) = And

unit : TaskT m (PRIM UNIT)
unit = pure ()

-- (<*>) : TaskT m (FUN a b) -> TaskT m a -> TaskT m b
-- (<*>) t1 t2 = (\f,x => f x) <$> t1 <&> t2

-- Alternative --

(<|>) : TaskT m a -> TaskT m a -> TaskT m a
(<|>) = Or

(<?>) : TaskT m a -> TaskT m a -> TaskT m a
(<?>) = Xor

fail : TaskT m a
fail = Fail

-- Monad --

(>>=) : TaskT m a -> (typeOf a -> TaskT m b) -> TaskT m b
(>>=) = Then

(>>?) : TaskT m a -> (typeOf a -> TaskT m b) -> TaskT m b
(>>?) = Next

-- infixl 1 >>*
-- (>>*) : TaskT m a -> List (typeOf a -> (Bool, TaskT m b)) -> TaskT m b
-- (>>*) t fs            = t >>- convert fs where
--   convert : List (Universe.typeOf a -> (Bool, TaskT m b)) -> Universe.typeOf a -> TaskT m b
--   convert [] x        = fail
--   convert (f :: fs) x =
--     let
--       ( guard, next ) = f x
--     in
--     (if guard then next else fail) <|> convert fs x

-- Transformer --

lift : Monad m => m (typeOf a) -> TaskT m a
lift = Lift

ref : (b : Ty) -> typeOf b -> Task (LOC b)
ref _ x = lift $ ref x

deref : (b : Ty) -> Loc b -> Task b
deref _ l = lift $ deref l

assign : (b : Ty) -> Loc b -> typeOf b -> Task (PRIM UNIT)
assign _ l x = lift $ assign l x

modify : (b : Ty) -> Loc b -> (typeOf b -> typeOf b) -> Task (PRIM UNIT)
modify _ l f = lift $ modify l f

-- Labels --

||| Infix operator to label a task
(#) : Label -> TaskT m a -> TaskT m a
(#) = Label

-- Extras --

ask : (b : Ty) -> TaskT m b
ask _ = Edit Nothing

watch : MonadRef l m => l (typeOf b) -> TaskT m b
watch = Store

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Effects

import Language.Reflection
import Control.Catchable

%access public

---- Effects

Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type

data EFFECT : Type where
     MkEff : Type -> Effect -> EFFECT

class Handler (e : Effect) (m : Type -> Type) where
     handle : res -> (eff : e t res resk) ->
              ((x : t) -> resk x -> m a) -> m a

-- A bit of syntactic sugar ('syntax' is not very flexible so we only go
-- up to a small number of parameters...)

syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
syntax "{" [inst] "}" [eff] = eff inst (\result => inst)

---- Properties and proof construction

using (xs : List a, ys : List a)
  data SubList : List a -> List a -> Type where
       SubNil : SubList {a} [] []
       Keep   : SubList xs ys -> SubList (x :: xs) (x :: ys)
       Drop   : SubList xs ys -> SubList xs (x :: ys)

  subListId : SubList xs xs
  subListId {xs = Nil} = SubNil
  subListId {xs = x :: xs} = Keep subListId

data Env  : (m : Type -> Type) -> List EFFECT -> Type where
     Nil  : Env m Nil
     (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)

data EffElem : Effect -> Type ->
               List EFFECT -> Type where
     Here : EffElem x a (MkEff a x :: xs)
     There : EffElem x a xs -> EffElem x a (y :: xs)

-- make an environment corresponding to a sub-list
dropEnv : Env m ys -> SubList xs ys -> Env m xs
dropEnv [] SubNil = []
dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
dropEnv (v :: vs) (Drop rest) = dropEnv vs rest

updateWith : (ys' : List a) -> (xs : List a) ->
             SubList ys xs -> List a
updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
updateWith ys        (x :: xs) (Drop rest) = x :: updateWith ys xs rest
updateWith []        []        SubNil      = []
updateWith (y :: ys) []        SubNil      = y :: ys
updateWith []        (x :: xs) (Keep rest) = []

-- put things back, replacing old with new in the sub-environment
rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
             Env m xs -> Env m (updateWith ys' xs prf)
rebuildEnv []        SubNil      env = env
rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
rebuildEnv xs        (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
rebuildEnv (x :: xs) SubNil      [] = x :: xs

---- The Effect EDSL itself ----

-- some proof automation

%reflection
reflectListEffElem : List a -> Tactic
reflectListEffElem [] = Refine "Here" `Seq` Solve
reflectListEffElem (x :: xs)
     = Try (Refine "Here" `Seq` Solve)
           (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))
-- TMP HACK! FIXME!
-- The evaluator needs a 'function case' to know its a reflection function
-- until we propagate that information! Without this, the _ case won't get
-- matched.
reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve
reflectListEffElem _ = Refine "Here" `Seq` Solve

%reflection
reflectSubList : List a -> Tactic
reflectSubList [] = Refine "SubNil" `Seq` Solve
reflectSubList (x :: xs)
     = Try (Refine "subListId" `Seq` Solve)
           (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))
                (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))
reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve
reflectSubList _ = Refine "subListId" `Seq` Solve

%reflection
reflectEff : (P : Type) -> Tactic
reflectEff (EffElem m a xs)
     = reflectListEffElem xs `Seq` Solve
reflectEff (SubList xs ys)
     = reflectSubList ys `Seq` Solve

updateResTy : (val : t) ->
              (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
              List EFFECT
updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
updateResTy     val (x :: xs)    (There p) n = x :: updateResTy val xs p n

-- updateResTyImm : (xs : List EFFECT) -> EffElem e a xs -> Type ->
--                  List EFFECT
-- updateResTyImm (MkEff a e :: xs) Here b = (MkEff b e) :: xs
-- updateResTyImm (x :: xs)    (There p) b = x :: updateResTyImm xs p b

infix 5 :::, :-, :=

data LRes : lbl -> Type -> Type where
     (:=) : (x : lbl) -> res -> LRes x res

(:::) : lbl -> EFFECT -> EFFECT
(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e

private
unlabel : {l : ty} -> Env m [l ::: x] -> Env m [x]
unlabel {m} {x = MkEff a eff} [l := v] = [v]

private
relabel : (l : ty) -> Env m xs -> Env m (map (\x => l ::: x) xs)
relabel {xs = []} l [] = []
relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

-- the language of Effects

data Eff : (m : Type -> Type) ->
           (x : Type) ->
           List EFFECT -> (x -> List EFFECT) -> Type where
     value   : a -> Eff m a xs (\v => xs)
     (>>=)   : Eff m a xs xs' ->
               ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''
     effect  : (prf : EffElem e a xs) ->
               (eff : e t a b) ->
               Eff m t xs (\v => updateResTy v xs prf eff)

     lift    : (prf : SubList ys xs) ->
               Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)
     new     : Handler e m =>
               res ->
               Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->
               Eff m a xs (\v => xs')
     catch   : Catchable m err =>
               Eff m a xs xs' -> (err -> Eff m a xs xs') ->
               Eff m a xs xs'

     (:-)    : (l : ty) ->
               Eff m t [x] xs' -> -- [x] (\v => xs) ->
               Eff m t [l ::: x] (\v => map (l :::) (xs' v))

{-
syntax [tag] ":!" [val] = !(tag :- val)

--   Eff : List (EFFECT m) -> Type -> Type
-}

implicit
lift' : Eff m t ys ys' ->
        {default tactics { byReflection reflectEff; }
           prf : SubList ys xs} ->
        Eff m t xs (\v => updateWith (ys' v) xs prf)
lift' e {prf} = lift prf e

implicit
effect' : {a, b: _} -> {e : Effect} ->
          (eff : e t a b) ->
          {default tactics { byReflection reflectEff; }
             prf : EffElem e a xs} ->
         Eff m t xs (\v => updateResTy v xs prf eff)
effect' e {prf} = effect prf e

return : a -> Eff m a xs (\v => xs)
return x = value x

-- for idiom brackets

infixl 2 <$>

pure : a -> Eff m a xs (\v => xs)
pure = value

(<$>) : Eff m (a -> b) xs (\v => xs) ->
        Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)
(<$>) prog v = do fn <- prog
                  arg <- v
                  return (fn arg)

-- an interpreter

private
execEff : Env m xs -> (p : EffElem e res xs) ->
          (eff : e a res resk) ->
          ((v : a) -> Env m (updateResTy v xs p eff) -> m t) -> m t
execEff (val :: env) Here eff' k
    = handle val eff' (\v, res => k v (res :: env))
execEff (val :: env) (There p) eff k
    = execEff env p eff (\v, env' => k v (val :: env'))

-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state
-- updates can be propagated even through failing computations?

eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
eff env (value x) k = k x env
eff env (prog >>= c) k
   = eff env prog (\p', env' => eff env' (c p') k)
eff env (effect prf effP) k = execEff env prf effP k
eff env (lift prf effP) k
   = let env' = dropEnv env prf in
         eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))
eff env (new r prog) k
   = let env' = r :: env in
         eff env' prog (\p' => \ (v :: envk) => k p' envk)
eff env (catch prog handler) k
   = catch (eff env prog k)
           (\e => eff env (handler e) k)
-- FIXME:
-- xs is needed explicitly because otherwise the pattern binding for
-- 'l' appears too late. Solution seems to be to reorder patterns at the
-- end so that everything is in scope when it needs to be.
eff {xs = [l ::: x]} env (l :- prog) k
   = let env' = unlabel env in
         eff env' prog (\p', envk => k p' (relabel l envk))

run : Applicative m => Env m xs -> Eff m a xs xs' -> m a
run env prog = eff env prog (\r, env => pure r)

runEnv : Applicative m => Env m xs -> Eff m a xs xs' ->
         m (x : a ** Env m (xs' x))
runEnv env prog = eff env prog (\r, env => pure (r ** env))

runPure : Env id xs -> Eff id a xs xs' -> a
runPure env prog = eff env prog (\r, env => r)

-- runPureEnv : Env id xs -> Eff id a xs xs' -> (x : a ** Env id (xs' x))
-- runPureEnv env prog = eff env prog (%unifyLog (\r, env => id (r ** env)))

runWith : (a -> m a) -> Env m xs -> Eff m a xs xs' -> m a
runWith inj env prog = eff env prog (\r, env => inj r)

-- some higher order things

mapE : Applicative m => (a -> {xs} Eff m b) -> List a -> {xs} Eff m (List b)
mapE f []        = pure []
mapE f (x :: xs) = [| f x :: mapE f xs |]

when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
when True  e = e
when False e = pure ()

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
module Control.Monad.Identity

public export
record Identity (a : Type) where
  constructor Id
  runIdentity : a

public export
Functor Identity where
    map fn (Id a) = Id (fn a)

public export
Applicative Identity where
    pure x = Id x
    (Id f) <*> (Id g) = Id (f g)

public export
Monad Identity where
    (Id x) >>= k = k x

public export
Show a => Show (Identity a) where
  showPrec d (Id x) = showCon d "Id" $ showArg x

public export
Eq a => Eq (Identity a) where
  (Id x) == (Id y) = x == y

public export
Ord a => Ord (Identity a) where
  compare (Id x) (Id y) = compare x y

-- public export
-- Enum a => Enum (Identity a) where
--   toNat (Id x) = toNat x
--   fromNat n = Id $ fromNat n
--   pred (Id n) = Id $ pred n

public export
(Semigroup a) => Semigroup (Identity a) where
  (<+>) x y = Id (runIdentity x <+> runIdentity y)

public export
(Monoid a) => Monoid (Identity a) where
  neutral = Id (neutral)


text:
module QPF

import Linear.Types
import Linear.Equality
import FunExt

{-
   This file implements quantitative polynomial functors as a type
   Desc with interpretation qpf, and shows that initiality implies
   induction for them.
-}

-- Grammar of polynomial functors

public export
data Desc : Type where
  Id' : Desc
  Const' : Type -> Desc
  Prod' : Desc -> Desc -> Desc
  Sum' : Desc -> Desc -> Desc
  With' : Desc -> Desc -> Desc
  Arr' : Type -> Desc -> Desc

-- Interpretation

public export
0 qpf : Desc -> Type -> Type
qpf Id' x = x
qpf (Const' a) _  = a
qpf (Prod' f g) x = LPair (qpf f x) (qpf g x)
qpf (Sum' f g) x = Sum (qpf f x) (qpf g x)
qpf (With' f g) x = With (qpf f x) (qpf g x)
qpf (Arr' a f) x = a -<> qpf f x

public export
fmap : (d : Desc) -> (f : a -<> b) -> qpf d a -<> qpf d b
fmap Id' f x = f x
fmap (Const' _) _ x = x
fmap (Prod' c d) f x = bimap (fmap c f) (fmap d f) x
fmap (Sum' c d) f x = bimap (fmap c f) (fmap d f) x
fmap (With' c d) f x = bimap (fmap c f) (fmap d f) x
fmap (Arr' a c) f x = \ y => fmap c f (x y)

-- Functor laws
0 fmap_id : {d : Desc} -> (1 x : qpf d a) -> x = fmap {b = a} d (\1 x => x) x
fmap_id {d = Id'} x = Refl
fmap_id {d = (Const' _)} _ = Refl
fmap_id {d = (Prod' c d)} (x # y) = lcong2 (#) (fmap_id x) (fmap_id y)
fmap_id {d = (Sum' c d)} (Inl x) = lcong Inl (fmap_id x)
fmap_id {d = (Sum' c d)} (Inr y) = lcong Inr (fmap_id y)
fmap_id {d = (With' c d)} x = funext (\b => if b then fmap_id (x True) else fmap_id (x False))
fmap_id {d = (Arr' a c)} g = funext (\ y => fmap_id (g y))

0 fmap_comp : (d : Desc) -> {f : a -<> b} -> {g : b -<> c} ->
              (1 x : qpf d a) -> fmap d g (fmap d f x) = fmap d (\ x => g (f x)) x
fmap_comp Id' x = Refl
fmap_comp (Const' a) _ = Refl
fmap_comp (Prod' c d) (x # y) = lcong2 (#) (fmap_comp c {f} {g} x) (fmap_comp d {f} {g} y)
fmap_comp (Sum' c d) (Inl x) = lcong Inl (fmap_comp c x)
fmap_comp (Sum' c d) (Inr y) = lcong Inr (fmap_comp d y)
fmap_comp (With' c d) x = funext (\b => if b then fmap_comp c (x True) else fmap_comp d (x False))
fmap_comp (Arr' a c) g = funext (\ y => fmap_comp c (g y))

-- Predicate lifting

public export
0 lift : (d : Desc) -> (p : x -> Type) -> qpf d x -> Type
lift Id' p f = p f
lift (Const' a) p x = Sigma1 a (\ y => x = y)
lift (Prod' c d) p z = LPair (lift c p (LPair.fst z)) (lift d p (LPair.snd z))
lift (Sum' c d) p z = Sum (Sigma0 (qpf c x) (\ z1 => LPair (z = Inl z1) (lift c p z1))) (Sigma0 (qpf d x) (\ z2 => LPair (z = Inr z2) (lift d p z2)))
lift (With' c d) p f = With (lift c p (f True)) (lift d p (f False))
lift (Arr' a c) p f = (1 y : a) -> lift c p (f y)

-- Lifting fuses with fmap (we only provide the useful direction)

0 liftcomp : (d : Desc) -> (p : x -> Type) -> (g : x' -<> x) ->
           (y : qpf d x') -> lift d p (fmap d g y) -> lift d (\ w => p (g w)) y
liftcomp Id' p g y z = z
liftcomp (Const' a) p g y z = z
liftcomp (Prod' c d) p g (x # y) (z1 # z2) = (liftcomp c p g x z1) # (liftcomp d p g y z2)
liftcomp (Sum' c d) p g (Inl y) (Inl (_ # (Refl # z))) = Inl (y # (Refl # liftcomp c p g y z))
liftcomp (Sum' c d) p g (Inl y) (Inr (_ # (leqr # z))) = absurd leqr
liftcomp (Sum' c d) p g (Inr y) (Inl (_ # (leqr # z))) = absurd (sym leqr)
liftcomp (Sum' c d) p g (Inr y) (Inr (_ # (Refl # z))) = Inr (y # (Refl # liftcomp d p g y z))
liftcomp (With' c d) p g y z = \ b => if b then liftcomp c p g (y True) (z True) else liftcomp d p g (y False) (z False)
liftcomp (Arr' a c) p g f z = \ y => liftcomp c p g (f y) (z y)

liftfmap : (d : Desc) -> {p : x -> Type} ->
           ((1 y : x) -> p y) -> (1 z : qpf d x) -> lift d p z
liftfmap Id' f z = f z
liftfmap (Const' a) f z = z # Refl
liftfmap (Prod' c d) f (z1 # z2) = liftfmap c f z1 # liftfmap d f z2
liftfmap (Sum' c d) f (Inl z) = Inl (z # (Refl # liftfmap c f z))
liftfmap (Sum' c d) f (Inr z) = Inr (z # (Refl # liftfmap d f z))
liftfmap (With' c d) f z = \ b => if b then liftfmap c f (z True) else liftfmap d f (z False)
liftfmap (Arr' a c) f z = \ y => liftfmap c f (z y)

0 liftfmap_comp : {x : Type} -> {x' : Type} -> (d : Desc) -> {p : x -> Type} ->
                (f : (1 y : x) -> p y) -> (g : x' -<> x) ->
                (1 z : qpf d x') ->
                liftcomp d p g z (liftfmap d {p} f (fmap d g z)) = liftfmap d {p = \ w => p (g w)} (\ x => f (g x)) z

liftfmap_comp Id' f g y = Refl
liftfmap_comp (Const' a) f g y = Refl
liftfmap_comp (Prod' c d) f g (x # y) = lcong2 (#) (liftfmap_comp c f g x) (liftfmap_comp d f g y)
liftfmap_comp (Sum' c d) f g (Inl y) = lcong (\ z => Inl (y # (Refl # z))) (liftfmap_comp c f g y)
liftfmap_comp (Sum' c d) f g (Inr y) = lcong (\ z => Inr (y # (Refl # z))) (liftfmap_comp d f g y)
liftfmap_comp (With' c d) f g y =  funext (\ b => if b then liftfmap_comp c f g (y True) else liftfmap_comp d f g (y False))
liftfmap_comp (Arr' a c) f g h = funext (\ y => liftfmap_comp c f g (h y))

-- qpf d distributes over Sigma0

public export
dist : {0 x : Type} -> {0 y : x -> Type} ->
       (d : Desc) -> qpf d (Sigma0 x y) -<> Sigma0 (qpf d x) (lift d y)
dist Id' (x # y)  = x # y
dist (Const' _) x = x # (x # Refl)
dist (Prod' c d) (x # y) =
  let (f # lf) = dist c x
      (g # lg) = dist d y
  in  (f # g) # (lf # lg)
dist (Sum' c d) (Inl f) =
  let (f # lf) = dist c f
  in  (Inl f) # (Inl (f # (Refl # lf)))
dist (Sum' c d) (Inr g) =
  let (g # lg) = dist d g
  in  (Inr g) # (Inr (g # (Refl # lg)))
dist (With' c d) w =
   (h w) # (j w) where
    0 h : With (qpf c (Sigma0 x y)) (qpf d (Sigma0 x y)) -> With (qpf c x) (qpf d x)
    h u True  = fst (dist c (u True))
    h u False = fst (dist d (u False))

    j : (1 u : With (qpf c (Sigma0 x y)) (qpf d (Sigma0 x y))) ->
        With (lift c y (h u True)) (lift d y (h u False))
    j u True  = snd (dist c (u True))
    j u False = snd (dist d (u False))
dist (Arr' a c) w =
   (h w) # (j w) where
    0 h : (a -<> qpf c (Sigma0 x y)) -> (a -<> qpf c x)
    h g z = fst (dist c (g z))

    j : (1 g : a -<> qpf c (Sigma0 x y)) ->
        ((1 z : a) -> (lift c y (h g z)))
    j g z = snd (dist c (g z))

-- The first projection of dist is fmap fst
0 distfst : (d : Desc) -> {0 x : Type} -> {0 p : x -> Type} ->
          (y : qpf d (Sigma0 x p)) -> fst {b = lift d p} (dist {y = p} d y) = fmap {b = x} d (fst {b = p}) y
distfst Id' (x # y) = Refl
distfst (Const' a) y = Refl
distfst (Prod' c d) (x # y) with (distfst c x)
  distfst (Prod' c d) (x # y) | r with (distfst d y)
    distfst (Prod' c d) (x # y) | r | q with (dist c x)
      distfst (Prod' c d) (x # y) | r | q | (f # lf) with (dist d y)
         distfst (Prod' c d) (x # y) | r | q | (f # lf) | (g # lg) = lcong2 (#) r q
distfst (Sum' c d) (Inl y) with (distfst c y)
  distfst (Sum' c d) (Inl y) | q with (dist c y)
    distfst (Sum' c d) (Inl y) | q | (f # lf) = lcong Inl q
distfst (Sum' c d) (Inr y) with (distfst d y)
  distfst (Sum' c d) (Inr y) | q with (dist d y)
    distfst (Sum' c d) (Inr y) | q | (f # lf) = lcong Inr q
distfst (With' c d) y = funext (\ b => if b then distfst c (y True) else distfst d (y False))
distfst (Arr' a c) y = funext (\ z => distfst c (y z))

-- Algebra

public export
data W : (0 u : Desc) -> Type where
  Con : qpf u (W u)  -<> W u
  -- Note: we only use pattern matching on Con to define fold and prove its properties

-- The notion of algebra morphism

0 morphism : (d : Desc) -> (alg1 : qpf d a -<> a) -> (alg2 : qpf d b -<> b) ->
             a -<> b -> Type
morphism d alg1 alg2 f = (1 y : qpf d a) -> f (alg1 y) = alg2 (fmap d f y)

0 morphism_id : (alg : qpf d a -<> a) -> morphism d alg alg (\ x => x)
morphism_id alg y = lcong alg (fmap_id y)

0 morphism_comp : {d : Desc} ->
                  (alg1 : qpf d a -<> a) ->
                  (alg2 : qpf d b -<> b) ->
                  (alg3 : qpf d c -<> c) ->
                  {f : a -<> b} -> {g : b -<> c} ->
                  morphism d alg1 alg2 f ->
                  morphism d alg2 alg3 g ->
                  morphism d alg1 alg3 (\ x => g (f x))
morphism_comp {d} alg1 alg2 alg3 {f} {g} m12 m23 y =
  trans (lcong g (m12 y)) (trans (m23 (fmap d f y)) (lcong alg3 (fmap_comp d y)))

-- Unique mediating morphism

mutual
  fold_h : {c : Desc} -> (d : Desc) -> (qpf c x -<> x) -> qpf d (W c) -<> qpf d x
  fold_h Id' alg (Con w) = alg (fold_h c alg w)
  fold_h (Const' y) alg w = w
  fold_h (Prod' c d) alg w = bimap (fold_h c alg) (fold_h d alg) w
  fold_h (Sum' c d) alg w = bimap (fold_h c alg) (fold_h d alg) w
  fold_h (With' c d) alg w = with With.bimap (bimap (fold_h c alg) (fold_h d alg) w)
  fold_h (Arr' a c) alg w = \ y => fold_h c alg (w y)

  fold : (d : Desc) -> (qpf d x -<> x) -> W d -<> x
  fold d alg (Con w) = alg (fold_h d alg w)

mutual
  0 uniq_h : {c : Desc} -> (d : Desc) ->
             (h : W c -<> x) ->
             (alg : qpf c x -<> x) ->
             morphism c Con alg h ->
             (w : qpf d (W c)) -> fmap d h w = fold_h {c = c} d alg w
  uniq_h Id' h alg commutes (Con y) = trans (commutes y) (lcong alg (uniq_h c h alg commutes y))
  uniq_h (Const' y) h calg commutes z = Refl
  uniq_h (Prod' c' d') h calg commutes (f' # g') =
    let uc' = uniq_h c' h calg commutes f'
        ud' = uniq_h d' h calg commutes g'
    in lcong2 (#) uc' ud'
  uniq_h (Sum' c' d') h calg commutes (Inl f') = lcong Inl (uniq_h c' h calg commutes f')
  uniq_h (Sum' c' d') h calg commutes (Inr g') = lcong Inr (uniq_h d' h calg commutes g')
  uniq_h (With' c' d') h calg commutes z =
    funext (\x => if x then uniq_h c' h calg commutes (z True)
                       else uniq_h d' h calg commutes (z False))
  uniq_h (Arr' a c') h calg commutes z = funext (\ y => uniq_h c' h calg commutes (z y))

  0 uniq : {d : Desc} ->
           (alg : qpf d x -<> x) ->
           (h : W d -<> x) ->
           ((1 y : qpf d (W d)) -> h (Con y) = alg (fmap d h y)) ->
           (w : W d) -> h w = fold d alg w
  uniq alg h commutes (Con y) =
    trans (commutes y) (lcong alg (uniq_h d h alg commutes y))

0 foldCon_id : (1 w : W d) -> w = fold d Con w
foldCon_id w = uniq Con (\x => x) (\y => lcong Con (fmap_id y)) w

0 foldCommutes : (d : Desc) -> (alg : qpf d x -<> x) ->
                 morphism d Con alg (fold d alg)
foldCommutes Id' alg (Con x) = Refl
foldCommutes (Const' _) alg x = Refl
foldCommutes (Prod' c d) alg (x # y) =
  let commutesC = uniq_h c (fold (Prod' c d) alg) alg (foldCommutes (Prod' c d) alg) x
      commutesD = uniq_h d (fold (Prod' c d) alg) alg (foldCommutes (Prod' c d) alg) y
  in lcong alg (lcong2 (#) (sym commutesC) (sym commutesD))

foldCommutes (Sum' c d) alg (Inl x) =
  let commutesC = uniq_h c (fold (Sum' c d) alg) alg (foldCommutes (Sum' c d) alg) x
  in lcong alg (lcong Inl (sym commutesC))

foldCommutes (Sum' c d) alg (Inr y) =
  let commutesD = uniq_h d (fold (Sum' c d) alg) alg (foldCommutes (Sum' c d) alg) y
  in lcong alg (lcong Inr (sym commutesD))

foldCommutes (With' c d) alg x =
  lcong alg (funext (\b => if b then sym (uniq_h c (fold (With' c d) alg) alg (foldCommutes (With' c d) alg) (x True))
                else sym (uniq_h d (fold (With' c d) alg) alg (foldCommutes (With' c d) alg) (x False))
     ))
foldCommutes (Arr' a c) alg g =
   lcong alg (funext (\ y => sym (uniq_h c (fold (Arr' a c) alg) alg (foldCommutes (Arr' a c) alg) (g y))))

-- Induction from initiality

pAlg : {d : Desc} -> {0 p : x -> Type} -> (alg : qpf d x -<> x) ->
       (step : (1 w : Sigma0 (qpf d x) (lift d p)) -> p (alg (fst w))) ->
       qpf d (Sigma0 x p) -<> Sigma0 x p
pAlg alg step y = let z = dist d y in alg (fst z) # step z

0 fstCommutes : (d : Desc) -> {0 p : x -> Type} -> {alg : qpf d x -<> x} ->
                {step : (1 w : Sigma0 (qpf d x) (lift d p)) -> p (alg (fst w))} ->
                morphism d (pAlg {d} {p} alg step) alg Sigma0.fst
fstCommutes d z = lcong alg (distfst d z)

public export
induction : {d : Desc} -> {0 p : W d -> Type} ->
            (step : (1 w : Sigma0 (qpf d (W d)) (lift d p)) -> p (Con (fst w))) ->
            (1 w : W d) -> p w
induction step w =
  let
    h : W d -<> Sigma0 (W d) p
    h = fold d (pAlg Con step)
    0 eq : (w : W d) -> fst (h w) = w
    eq w = trans (uniq Con (\w => fst (h w)) (\ y => morphism_comp Con (pAlg Con step) Con (foldCommutes d (pAlg Con step)) (fstCommutes {alg = Con} {step} d) y) w) (sym (foldCon_id w))
  in replace {x = fst (h w)} {p = p} (eq w) (snd (h w))

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Main

maybechoice : Maybe a -> Maybe a -> Maybe a
maybechoice (Just x) _ = Just x
maybechoice Nothing r = r

unused : a -> a -> a
unused _ s = s

doTest : Maybe Nat
doTest = do
  a <- Nothing
  unused a (pure 3)
 `maybechoice` pure 2

main : IO ()
main = putStrLn . show $ doTest

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
{-
1
reading
2
writing
3
writing
-}
module Main

import CIL.FFI
import CIL.Elab.Enums

%language ElabReflection

{-

  [Flags]
  enum System.IO.FileAccess {
    Read  = 1,
    Write = 2,
    ReadWrite = Read + Write
  }

-}

namespace System.IO.FileAccess

  FileAccessTy : CILTy
  FileAccessTy = corlibTyVal "System.IO.FileAccess"

  %runElab
    cilEnum FileAccess FileAccessTy Bits32
            [ cilField Read  1
            , cilField Write 2
            ]

  IsA Object FileAccess where {}

  ReadWrite :  FileAccess
  ReadWrite = Read + Write

describe : Bits32 -> String
describe 1 = "reading"
describe _ = "writing"

testEnumAsObject : FileAccess -> CIL_IO ()
testEnumAsObject e = putStrLn !(ToString e)

testFromEnum : FileAccess -> CIL_IO ()
testFromEnum e = putStrLn (describe (fromEnum e))

main : CIL_IO ()
main = do
  for_ [Read, Write, ReadWrite] $
    \e => do testEnumAsObject e
             testFromEnum e

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

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Java.Nio

import IdrisJvm.IO

%access public export

namespace OpenOption
    openOptionClass : String
    openOptionClass = "java/nio/file/OpenOption"

    OpenOption : Type
    OpenOption = JVM_Native (Interface openOptionClass)

namespace StandardOpenOption
    standardOpenOptionClass : String
    standardOpenOptionClass = "java/nio/file/StandardOpenOption"

    StandardOpenOptionClass : JVM_NativeTy
    StandardOpenOptionClass = Class standardOpenOptionClass

    StandardOpenOption : Type
    StandardOpenOption = JVM_Native StandardOpenOptionClass

    Inherits OpenOption StandardOpenOption where {}

    append : StandardOpenOption
    append = unsafePerformIO $ getStaticField StandardOpenOptionClass "APPEND" (JVM_IO StandardOpenOption)

    create : StandardOpenOption
    create = unsafePerformIO $ getStaticField StandardOpenOptionClass "CREATE" (JVM_IO StandardOpenOption)

    createNew : StandardOpenOption
    createNew = unsafePerformIO $ getStaticField StandardOpenOptionClass "CREATE_NEW" (JVM_IO StandardOpenOption)

    deleteOnClose: StandardOpenOption
    deleteOnClose = unsafePerformIO $ getStaticField StandardOpenOptionClass "DELETE_ON_CLOSE" (JVM_IO StandardOpenOption)

    dsync : StandardOpenOption
    dsync = unsafePerformIO $ getStaticField StandardOpenOptionClass "DSYNC" (JVM_IO StandardOpenOption)

    read : StandardOpenOption
    read = unsafePerformIO $ getStaticField StandardOpenOptionClass "READ" (JVM_IO StandardOpenOption)

    sparse : StandardOpenOption
    sparse = unsafePerformIO $ getStaticField StandardOpenOptionClass "SPARSE" (JVM_IO StandardOpenOption)

    sync : StandardOpenOption
    sync = unsafePerformIO $ getStaticField StandardOpenOptionClass "SYNC" (JVM_IO StandardOpenOption)

    truncateExisting : StandardOpenOption
    truncateExisting = unsafePerformIO $ getStaticField StandardOpenOptionClass "TRUNCATE_EXISTING" (JVM_IO StandardOpenOption)

    write : StandardOpenOption
    write = unsafePerformIO $ getStaticField StandardOpenOptionClass "WRITE" (JVM_IO StandardOpenOption)

namespace Path
    pathClass : String
    pathClass = "java/nio/file/Path"

    Path : Type
    Path = JVM_Native (Interface pathClass)

Show Path where
    show path = unsafePerformIO $ invokeInstance "toString" (Path -> JVM_IO String) path

namespace Files
    filesClass : String
    filesClass = "java/nio/file/Files"

    FilesClass : JVM_NativeTy
    FilesClass = Class filesClass

    Files : Type
    Files = JVM_Native FilesClass

namespace Files
    pathsClass : String
    pathsClass = "java/nio/file/Paths"

    PathsClass : JVM_NativeTy
    PathsClass = Class pathsClass

    Paths : Type
    Paths = JVM_Native PathsClass

namespace Channel
    channelClass : String
    channelClass = "java/nio/channels/Channel"

    ChannelClass : JVM_NativeTy
    ChannelClass = Interface channelClass

    Channel : Type
    Channel = JVM_Native ChannelClass

    close : Inherits Channel channel => channel -> JVM_IO ()
    close channel = invokeInstance "close" (Channel -> JVM_IO ()) (believe_me channel)

namespace SeekableByteChannel
    seekableByteChannelClass : String
    seekableByteChannelClass = "java/nio/channels/SeekableByteChannel"

    SeekableByteChannel : Type
    SeekableByteChannel = JVM_Native (Interface seekableByteChannelClass)

    Inherits Channel SeekableByteChannel where {}

 namespace FileChannel
     fileChannelClass : String
     fileChannelClass = "java/nio/channels/FileChannel"

     FileChannel : Type
     FileChannel = JVM_Native (Class fileChannelClass)

     Inherits Channel FileChannel where {}
     Inherits SeekableByteChannel FileChannel where {}

namespace FileAttribute
    fileAttributeClass : String
    fileAttributeClass = "java/nio/file/attribute/FileAttribute"

    FileAttribute : Type
    FileAttribute = JVM_Native (Interface fileAttributeClass)

namespace BasicFileAttributes
    basicFileAttributesClass : String
    basicFileAttributesClass = "java/nio/file/attribute/BasicFileAttributes"

    BasicFileAttributes : Type
    BasicFileAttributes = JVM_Native (Interface basicFileAttributesClass)

namespace LinkOption
    linkOptionClass : String
    linkOptionClass = "java/nio/file/LinkOption"

    LinkOption : Type
    LinkOption = JVM_Native (Class "java/nio/file/LinkOption")

namespace FileTime
    fileTimeClass : String
    fileTimeClass = "java/nio/file/attribute/FileTime"

    FileTime : Type
    FileTime = JVM_Native (Class fileTimeClass)

max_stars_repo_name: alaendle/idris-jvm

max_issues_repo_name: alaendle/idris-jvm

max_forks_repo_name: alaendle/idris-jvm


text:
||| Additional functions about vectors
module Data.Vect.Extra

import Data.Vect
import Data.Fin
import Data.Vect.Elem

||| Version of `map` with access to the current position
public export
mapWithPos : (f : Fin n -> a -> b) -> Vect n a -> Vect n b
mapWithPos f [] = []
mapWithPos f (x :: xs) = f 0 x :: mapWithPos (f . FS) xs

||| Version of `map` with runtime-irrelevant information that the
||| argument is an element of the vector
public export
mapWithElem : (xs : Vect n a)
  -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
  -> Vect n b
mapWithElem []        f = []
mapWithElem (x :: xs) f
  = f x Here :: mapWithElem xs
                (\x,pos => f x (There pos))


text:
module GRIN.Parser

import Control.Monad.State
import Data.String.Parser

import GRIN.AST

%hide Data.String.Parser.space
%hide Data.String.Parser.spaces
%hide Data.String.Parser.lexeme
%hide Data.String.Parser.Parser

Parser : Type -> Type
Parser = ParseT (State Nat)

MonadState Nat Parser where
    get = lift get
    put = lift . put
    state = lift . state

space : Parser Char
space = char ' '

newlines : Parser ()
newlines =
    ignore $ many
        (satisfy (\c => c == '\n' || c == '\r') <?> "newline")

pVar : Parser Var
pVar = char 'v' *> (MkVar . cast <$> integer)

pRef : Parser String
pRef = takeWhile isAlpha

pTagType : Parser TagType
pTagType = choice
    [ Con <$ char 'C'
    , Partial <$ char 'P' <*> natural
    , NUThunk <$ string "FNU"
    , UThunk <$ char 'F'
    , UThunk <$ string "FU"
    ]

pTag : Parser (Tag String)
pTag = [| MkTag pTagType (takeWhile isAlphaNum) |]

pLit : Parser Lit
pLit = choice
    [ LInt . cast <$> integer
    ]

pIntPrec : Parser IntPrec
pIntPrec = optional (string "T_") *> choice
    [ Signed <$ string "Int" <*> natural
    , Unsigned <$ string "Word" <*> natural
    ]


text:
eq1 : (x : Nat) -> (x = S x) -> Nat
eq1 x p impossible

eq2 : (x : Nat) -> (S x = Z) -> Nat
eq2 x p impossible

eq3 : (x : Nat) -> (S (S x) = (S x)) -> Nat
eq3 x p impossible

eq4 : (x : Nat) -> (S x = x) -> Nat
eq4 x p impossible

eq5 : (x : Nat) -> (Z = S x) -> Nat
eq5 x p impossible

eq6 : (x : Nat) -> (S x = (S (S x))) -> Nat
eq6 x p impossible

eqL1 : (xs : List a) -> (x :: xs = []) -> Nat
eqL1 xs p impossible

eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
eqL2 xs p impossible

badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
badeq x y p impossible

badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
badeqL xs ys p impossible


text:
module QuotingShadowed

import Data.Vect

import Language.Reflection

%language ElabReflection

X : (Nat -> Nat) -> Type
X f = Vect (f 2) Unit

--------------------------
--- Shadowing using UN ---
--------------------------

-- (x : Nat) -> (y : X (\x -> S x)) -> Nat
tyExpr : TTImp
tyExpr =
  IPi EmptyFC MW ExplicitArg (Just `{x}) `(Prelude.Types.Nat) $
  IPi EmptyFC MW ExplicitArg (Just `{y}) (
    IApp EmptyFC `(QuotingShadowed.X) $
      ILam EmptyFC MW ExplicitArg (Just $ UN $ Basic "x") `(Prelude.Types.Nat) $
        IApp EmptyFC `(Prelude.Types.S) $ IVar EmptyFC `{x}
  ) $
  `(Prelude.Types.Nat)

ty : Elab Type
ty = check tyExpr

T : Type
T = %runElab ty

f : T
f n [(), (), ()] = 4

--------------------------------
--- Pseudo-shadowing with MN ---
--------------------------------

tyExpr' : TTImp
tyExpr' =
  IPi EmptyFC MW ExplicitArg (Just `{x}) `(Prelude.Types.Nat) $
  IPi EmptyFC MW ExplicitArg (Just `{y}) (
    IApp EmptyFC `(QuotingShadowed.X) $
      ILam EmptyFC MW ExplicitArg (Just $ MN "x" 0) `(Prelude.Types.Nat) $
        IApp EmptyFC `(Prelude.Types.S) $ IVar EmptyFC `{x}
  ) $
  `(Prelude.Types.Nat)

ty' : Elab Type
ty' = check tyExpr'

T' : Type
T' = %runElab ty'

f' : T'
f' Z     [()]     = 4
f' (S x) (()::xs) = S $ f' x xs

--------------------------------
--- Requoted the one with UN ---
--------------------------------

tyExpr'' : TTImp
tyExpr'' = %runElab quote T

ty'' : Elab Type
ty'' = check tyExpr''

T'' : Type
T'' = %runElab ty''

f'' : T''
f'' Z     [()]     = 4
f'' (S x) (()::xs) = S $ f'' x xs
-- T'' is a requoted T, thus f'' shall be able to be equal to f, not to f'
--f'' n [(), (), ()] = 4

-- check that T'' has really `MN _ 0` --

N'' : Nat
N'' = case tyExpr'' of
        (IPi _ _ _ _ _ $ IPi _ _ _ _ (IApp _ _ $ ILam _ _ _ (Just n) _ _) _) =>
          case n of
            UN _     => 1
            MN "x" 0 => 2
            _        => 3
        _ => 0

n''value : N'' = 2
n''value = Refl

--------------------
--- Printing out ---
--------------------

%runElab logSugaredTerm "shdw" 0 "tyExpr  " tyExpr
%runElab logSugaredTerm "shdw" 0 "tyExpr' " tyExpr'
%runElab logSugaredTerm "shdw" 0 "tyExpr''" tyExpr''

%runElab logSugaredTerm "shdw" 0 "quoted T  " !(quote T  )
%runElab logSugaredTerm "shdw" 0 "quoted T' " !(quote T' )
%runElab logSugaredTerm "shdw" 0 "quoted T''" !(quote T'')

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module IdrisPrelude

%hide Prelude.Nat.Nat

data Nat : Type where
  Zero : Nat
  Succ : Nat -> Nat

natElim : (m : Nat -> Type) -> (mz : m Zero) -> (ms : (l : Nat) -> m l -> m (Succ l)) -> (k : Nat) -> m k
natElim m mz ms Zero = mz
natElim m mz ms (Succ k) = ms k (natElim m mz ms k)

data Vec : Type -> Nat -> Type where
  Nil : (a : Type) -> Vec a Zero
  Cons : (a : Type) -> (n : Nat) -> (x : a) -> (xs : Vec a n) -> Vec a (Succ n)

data Eq : (a : Type) -> a -> a -> Type where
  Refl : (a : Type) -> (x : a) -> Eq a x x

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module Main

data Vector : Nat -> Type -> Type where
    Nil : Vector Z a
    (::) : a -> Vector k a -> Vector (S k) a

{-
interface Functor (f : Type -> Type) where
    fmap : (a -> b) -> (f a -> f b)
-}
implementation Functor (Vector Z) where
    map f = const Nil

implementation Functor (Vector n) => Functor (Vector (S n)) where
    map f (x :: xs) = f x :: map f xs

implementation Applicative (Vector Z) where
    pure _ = Nil
    (<*>) v = const Nil

implementation Applicative (Vector n) => Applicative (Vector (S n)) where
    pure a = a :: pure a
    (<*>) (f :: fs) (a :: as) = f a :: (fs <*> as)

tail : Vector n a -> Vector (pred n) a
tail (x :: xs) = xs

length : ( xs : Vector n a ) -> Nat
length Nil = 0
length x = succ . Main.length . Main.tail $ x

main : IO ()
main = print $ Main.length (0::1::2::3::4::5::Nil)


text:
module GTK

import public GTK.GTK
import public GTK.GLib


text:
module Data.Verified.Zifunctor

import Data.Zifunctor

%default total
%access public export

||| Verified Zifunctor
||| A Zifunctor for which identity and composition laws are verified
interface Zifunctor t => VerifiedZifunctor (t : Type -> Type -> Type -> Type) where
  zifunctorIdentity : {a : Type} -> {b : Type} -> {c : Type} ->
                     (x : t a b c) ->
                     zimap Basics.id Basics.id Basics.id x = x
  zifunctorComposition : {a : Type} -> {b : Type} -> {c : Type} ->
                         {a1 : Type} -> {b1 : Type} -> {c1 : Type} ->
                         (x : t a b c) ->
                         (fa1 : a1 -> a) -> (fb1 : b -> b1) -> (fc1 : c -> c1) ->
                         (fa2 : a2 -> a1) -> (fb2 : b1 -> b2) -> (fc2 : c1 -> c2) ->
                         (zimap (fa1 . fa2) (fb2 . fb1) (fc2 . fc1) x) =
                         (zimap fa2 fb2 fc2 . zimap fa1 fb1 fc1) x

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
-- ------------------------------------------------------- [ StateMachines.idr ]
-- Module      : Chapter.StateMachines
-- Description : Definitions from Chapter 13 of Edwin Brady's book,
--               "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Chapter.StateMachines

import public Control.Monad.State

-- NOTE: See 13.2.1
import Data.Vect

-- ------------------------------------------------- [ 13.1.1 Modelling a Door ]

namespace BadDoor

  public export
  data DoorCmd : Type -> Type where
       Open : DoorCmd ()
       Close : DoorCmd ()
       RingBell : DoorCmd ()

       Pure : ty -> DoorCmd ty
       (>>=) : DoorCmd a -> (a -> DoorCmd b) -> DoorCmd b

  export
  doorProg : DoorCmd ()
  doorProg = do RingBell
                Open
                Close

  doorProgBad : DoorCmd ()
  doorProgBad = do Open
                   Open
                   RingBell

namespace Door

  ||| A door is either open or closed.
  public export
  data DoorState = ||| The door is closed.
                   DoorClosed
                 | ||| The door is open.
                   DoorOpen

  ||| A sequence of door actions which produces a value of type `ty`, begins with
  ||| the door in the state `beforeState`, and ends with the door in the state
  ||| `afterState`.
  ||| @ ty The type of the produced value.
  ||| @ beforeState The initial door state.
  ||| @ afterState The resulting door state.
  public export
  data DoorCmd  : (ty : Type) ->
                  (beforeState, afterState : DoorState) ->
                  Type where

       ||| Open a closed door.
       Open     : DoorCmd () DoorClosed DoorOpen

       ||| Close an open door.
       Close    : DoorCmd () DoorOpen   DoorClosed

       ||| Ring the bell of a closed door.
       RingBell : DoorCmd () state state -- NOTE: Exercise 13.1.5.1

       ||| Lift a value.
       Pure : ty -> DoorCmd ty state state

       ||| Sequentially compose two door actions, passing any value produced by
       ||| the first as an argument to the second.
       (>>=) : DoorCmd a state1 state2 ->
               (a -> DoorCmd b state2 state3) ->
               DoorCmd b state1 state3

  ||| Starting with a closed door, ring the bell, open the door, ring the bell,
  ||| and close the door, resulting in a closed door and producing ().
  export
  doorProg : DoorCmd () DoorClosed DoorClosed
  doorProg = do RingBell
                Open
                RingBell
                Close

-- -------------------------------------- [ 13.1.3 Modelling a Vending Machine ]

namespace VendingMachine

  export
  VendState : Type
  VendState = (Nat, Nat)

  public export
  data Input = COIN
             | VEND
             | CHANGE
             | REFILL Nat

  public export
  data MachineCmd : (ty : Type) ->
                    (beforeState, afterState : VendState) ->
                    Type where

       InsertCoin : MachineCmd () (  pounds,   chocs) (S pounds, chocs)

       Vend       : MachineCmd () (S pounds, S chocs) (  pounds, chocs)

       GetCoins   : MachineCmd () (  pounds,   chocs) (  Z,      chocs)

       Refill : (bars : Nat) -> MachineCmd () (Z, chocs) (Z, bars + chocs)

       Display : String -> MachineCmd () state state

       GetInput : MachineCmd (Maybe Input) state state

       ||| Lift a value.
       Pure : ty -> MachineCmd ty state state

       (>>=) : MachineCmd a state1 state2 ->
               (a -> MachineCmd b state2 state3) ->
               MachineCmd b state1 state3

  public export
  data MachineIO : VendState -> Type where
       Do : MachineCmd a state1 state2 ->
            (a -> Inf (MachineIO state2)) -> MachineIO state1

namespace MachineDo

  public export
  (>>=) : MachineCmd a state1 state2 ->
          (a -> Inf (MachineIO state2)) -> MachineIO state1
  (>>=) = Do

-- --------------------------------------- [ 13.1.4 A Verified Vending Machine ]

mutual

  vend : MachineIO (pounds, chocs)
  vend {pounds = S _} {chocs = S _} = do Vend
                                         Display "Enjoy!"
                                         machineLoop
  vend {pounds = Z}                 = do Display "Insert a coin"
                                         machineLoop
  vend {chocs = Z}                  = do Display "Out of stock"
                                         machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _                = do Display "Can't refill: Coins in machine"
                               machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop = do Just x <- GetInput
                     | Nothing => do Display "Invalid input"
                                     machineLoop
                   case x of
                        COIN       => do InsertCoin
                                         machineLoop
                        VEND       => vend
                        CHANGE     => do GetCoins
                                         Display "Change returned"
                                         machineLoop
                        REFILL num => refill num

-- ------------------------------------------------- [ 13.2.1 Stack Operations ]

namespace StackOperations

 public export
 data StackCmd : (ty : Type) ->
                 (a : Type) ->
                 (inHeight, outHeight : Nat) ->
                 Type where

      Push : a -> StackCmd () a height (S height)

      Pop : StackCmd a a (S height) height

      Top : StackCmd a a (S height) (S height)

      GetStr : StackCmd String a height height

      PutStr : String -> StackCmd () a height height

      Pure : ty -> StackCmd ty a height height
      (>>=) : StackCmd a elem height1 height2 ->
              (a -> StackCmd b elem height2 height3) ->
              StackCmd b elem height1 height3

-- export
testAdd : StackCmd Integer Integer 0 0
testAdd = do Push 10
             Push 20
             val1 <- Pop
             val2 <- Pop
             Pure (val1 + val2)

-- NOTE: This will not type check.
-- testAdd : StackCmd Integer 0 0
-- testAdd = do Push 10
--              val1 <- Pop
--              val2 <- Pop
--              Pure (val1 + val2)

-- ------------------------------------------- [ 13.2.2 Implementing the Stack ]

runStack : (stk : Vect inHeight a) ->
           StackCmd ty a inHeight outHeight ->
           IO (ty, Vect outHeight a)
runStack stk (Push val)   = pure ((), val :: stk)
runStack (val :: stk) Pop = pure (val, stk)
runStack (val :: stk) Top = pure (val, val :: stk)
runStack stk GetStr       = do x <- getLine
                               pure (x, stk)
runStack stk (PutStr x)   = putStr x *> pure ((), stk)
runStack stk (Pure x)     = pure (x, stk)
runStack stk (x >>= f)    = do (x', newStk) <- runStack stk x
                               runStack newStk (f x')

printResult : StackCmd () Integer (S height) (S height)
printResult = do result <- Top
                 PutStr (show result ++ "\n")

doBinOp : (op : Integer -> Integer -> Integer) ->
          StackCmd () Integer (S (S height)) (S height)
doBinOp op = do val1 <- Pop
                val2 <- Pop
                -- NOTE: The arguments are ordered this way because subtraction
                -- is not commutative, while addition and multiplication are,
                -- e.g. given 2 <RET> 1 <RET> - <RET>, stackCalc should print 1,
                -- i.e. 2 - 1 = 1, as opposed to 1 - 2 = -1.
                Push (val2 `op` val1)
                printResult

public export
data StackIO : Nat -> Type -> Type where
     Do : StackCmd ty a inHeight outHeight ->
          (ty -> Inf (StackIO outHeight a)) ->
          StackIO inHeight a

namespace StackDo

  (>>=) : StackCmd ty a inHeight outHeight ->
          (ty -> Inf (StackIO outHeight a)) ->
          StackIO inHeight a
  (>>=) = Do

public export
data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

export
run : Fuel -> Vect height a -> StackIO height a -> IO ()
run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c
                                  run fuel newStk (f res)
run Dry _ _                  = pure ()

public export
data StkInput = Number Integer
              | Add
              -- NOTE: Exercise 13.2.4.1
              | Subtract
              | Multiply
              -- NOTE: Exercise 13.2.4.2
              | Negate
              -- NOTE: Exercise 13.2.4.3
              | Discard
              -- NOTE: Exercise 13.2.4.4
              | Duplicate

export
strToInput : String -> Maybe StkInput
strToInput ""          = Nothing
strToInput "add"       = Just Add
strToInput "subtract"  = Just Subtract
strToInput "multiply"  = Just Multiply
strToInput "negate"    = Just Negate
strToInput "discard"   = Just Discard
strToInput "duplicate" = Just Duplicate
strToInput x           = if all isDigit (unpack x)
                            then Just (Number (cast x))
                            else Nothing

mutual

  tryBinOp : (op : Integer -> Integer -> Integer) -> StackIO height Integer
  tryBinOp {height = S (S _)} op =
      do doBinOp op
         stackCalc
  tryBinOp _ =
      do PutStr "Fewer than two items on the stack\n"
         stackCalc

  tryAdd : StackIO height Integer
  tryAdd = tryBinOp (+)

-- ------------------------------------------------------- [ Exercise 13.2.4.1 ]

  trySubtract : StackIO height Integer
  trySubtract = tryBinOp (-)

  tryMultiply : StackIO height Integer
  tryMultiply = tryBinOp (*)

-- -------------------------------------------------- [ Unary operation helper ]

  emptyStack : StackIO height Integer
  emptyStack = do PutStr "Stack is empty\n"
                  stackCalc

-- ------------------------------------------------------- [ Exercise 13.4.2.2 ]

  tryNegate : StackIO height Integer
  tryNegate {height = S _} = do Push (negate !Pop)
                                printResult
                                stackCalc
  tryNegate                = emptyStack

-- ------------------------------------------------------- [ Exercise 13.4.2.3 ]

  tryDiscard : StackIO height Integer
  tryDiscard {height = S _} = do PutStr $ "Discarded " ++ show !Pop ++ "\n"
                                 stackCalc
  tryDiscard                = emptyStack

-- ------------------------------------------------------- [ Exercise 13.4.2.4 ]

  tryDuplicate : StackIO height Integer
  tryDuplicate {height = S _} = do val <- Top
                                   Push val
                                   PutStr $ "Duplicated " ++ show val ++ "\n"
                                   stackCalc
  tryDuplicate                = emptyStack

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

  export
  stackCalc : StackIO height Integer
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                      Nothing         => do PutStr "Invalid input\n"
                                            stackCalc
                      Just (Number x) => do Push x
                                            stackCalc
                      Just Add        => tryAdd
                      -- NOTE: Exercise 13.2.4.1
                      Just Subtract   => trySubtract
                      Just Multiply   => tryMultiply
                      -- NOTE: Exercise 13.2.4.2
                      Just Negate     => tryNegate
                      -- NOTE: Exercise 13.2.4.3
                      Just Discard    => tryDiscard
                      -- NOTE: Exercise 13.2.4.4
                      Just Duplicate  => tryDuplicate

namespace StackCalculator

  export
  partial
  main : IO ()
  main = run forever [] stackCalc

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
data Elem	 : 	a -> List a -> Type where
    Here	 : 	Elem x (x :: xs)
    There	 : 	(later : Elem x xs) -> Elem x (y :: xs)

data TypeWithFunction : Type where
    ABC  : (ty_a:Type) -> (ty_b:Type) -> (ty_a -> ty_b) -> TypeWithFunction

isInList : Elem (ABC Bool String (\c => if c then "Foo" else "Bar"))
                [(ABC Bool String (\c => if c then "Foo" else "Bar"))]
isInList = Here

isInListBad : Elem (ABC Bool String (\c => if c then "Foo" else "Bar"))
                  [(ABC Bool String (\c => if c then "Foo" else "Baz"))]
isInListBad = Here


text:
data MyN = MkN Nat Nat

foo : Nat -> Nat -> Nat
foo x y = case MkN x of
               MkN z => y

main : IO ()
main = printLn (foo 2 2)


text:
-- ------------------------------------------------------------- [ Chargen.idr ]
--
-- This RFC specifies a standard for the ARPA Internet community.
-- Hosts on the ARPA Internet that choose to implement a Character
-- Generator Protocol are expected to adopt and implement this
-- standard.

-- A useful debugging and measurement tool is a character generator
-- service. A character generator service simply sends data without
-- regard to the input.
--
-- The data may be anything.  It is recommended that a recognizable
-- pattern be used in tha data.
--
-- One popular pattern is 72 chraracter lines of the ASCII printing
-- characters.  There are 95 printing characters in the ASCII
-- character set.  Sort the characters into an ordered sequence and
-- number the characters from 0 through 94.  Think of the sequence as
-- a ring so that character number 0 follows character number 94.  On
-- the first line (line 0) put the characters numbered 0 through
-- 71. On the next line (line 1) put the characters numbered 1 through
-- 72.  And so on.  On line N, put characters (0+N mod 95) through
-- (71+N mod 95).  End each line with carriage return and line feed.
--
-- http://tools.ietf.org/html/rfc864
-- --------------------------------------------------------------------- [ EOH ]
module RFC.CharGen

import Effects

import Effect.Default
import Effect.StdIO

import System.Protocol

||| A useful debugging and measurement tool is a character generator
||| service. A character generator service simply sends data without
||| regard to the input. The data may be anything.  It is recommended
||| that a recognizable pattern be used in tha data.
total
chargen : Protocol ['Client, 'Server] ()
chargen = do
    msg <- 'Client ==> 'Server | Maybe String
    case msg of
      Just m => do
        'Server ==> 'Client | String
        Rec chargen
      Nothing => Done

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Circuits.Idealised.Terms

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Data.Whole

import Circuits.Idealised.Types
import Circuits.Split

%default total

namespace Circuits

  public export
  data Term : (old  : List (Ty, Usage))
           -> (type : Ty)
           -> (new  : List (Ty, Usage))
                   -> Type
    where
      Var : (prf : Elem (type, FREE) old)
         -> Use old prf new
         -> Term old type new

      NewSignal : (flow     : Direction)
               -> (datatype : DType)
               -> (body     : Term ((TyPort (flow, datatype), FREE) :: old)
                                   TyUnit
                                   Nil)
                           -> Term old TyUnit Nil

      Wire : (datatype : DType)
          -> (body     : Term ((TyPort (OUTPUT,datatype), FREE)::(TyPort (INPUT,datatype), FREE)::old)
                              TyUnit
                              Nil)
                 -> Term old TyUnit Nil

      Mux : (output  : Term a (TyPort (OUTPUT, datatype)) b)
         -> (control : Term b (TyPort (INPUT,  LOGIC))    c)
         -> (inputA  : Term c (TyPort (INPUT,  datatype)) d)
         -> (inputB  : Term d (TyPort (INPUT,  datatype)) e)
                    -> Term a TyGate e

      Dup : (outA  : Term a (TyPort (OUTPUT, datatype)) b)
         -> (outB  : Term b (TyPort (OUTPUT, datatype)) c)
         -> (input : Term c (TyPort (INPUT,  datatype)) d)
                  -> Term a TyGate d

      Seq : Term a TyGate b
         -> Term b TyUnit Nil
         -> Term a TyUnit Nil

      Not : (output : Term a (TyPort (OUTPUT, LOGIC)) b)
         -> (input  : Term b (TyPort (INPUT,  LOGIC)) c)
                   -> Term a TyGate c

      Gate : (kind   : GateKind)
          -> (output : Term a (TyPort (OUTPUT, LOGIC)) b)
          -> (inputA : Term b (TyPort (INPUT,  LOGIC)) c)
          -> (inputB : Term c (TyPort (INPUT,  LOGIC)) d)
                    -> Term a TyGate d

      IndexSingleton : (output : Term a (TyPort (OUTPUT,                          datatype))  b)
                    -> (input  : Term b (TyPort (INPUT, (BVECT (W (S Z) ItIsSucc) datatype))) c)
                              -> Term a TyGate c

      IndexEdge : (pivot : Nat)
               -> (idx   : Index size pivot free)
               -> (outu  : Term a (TyPort (OUTPUT,             datatype))  b)
               -> (outf  : Term b (TyPort (OUTPUT, (BVECT free datatype))) c)
               -> (input : Term c (TyPort (INPUT,  (BVECT size datatype))) d)
                        -> Term a TyGate d

      IndexSplit : (pivot : Nat)
                -> (idx   : Index Z pivot size sizeA sizeB)
                -> (usedA : Term a (TyPort (OUTPUT,              datatype))  b)
                -> (freeA : Term b (TyPort (OUTPUT, (BVECT sizeA datatype))) c)
                -> (freeB : Term c (TyPort (OUTPUT, (BVECT sizeB datatype))) d)
                -> (input : Term d (TyPort (INPUT,  (BVECT size  datatype))) e)
                         -> Term a TyGate e

      Merge2L2V : (output : Term a (TyPort (OUTPUT, BVECT (W (S (S Z)) ItIsSucc) LOGIC)) b)
               -> (inputA : Term b (TyPort (INPUT,  LOGIC))                              c)
               -> (inputB : Term c (TyPort (INPUT,  LOGIC))                              d)
                         -> Term a TyGate                                                d

      Merge2V2V : (prf    : Plus sizeA sizeB sizeC)
               -> (output : Term a (TyPort (OUTPUT, BVECT sizeC datatype)) b)
               -> (inputA : Term b (TyPort (INPUT,  BVECT sizeA datatype)) c)
               -> (inputB : Term c (TyPort (INPUT,  BVECT sizeB datatype)) d)
                         -> Term a TyGate                                  d

      MergeSingleton : (output : Term a (TyPort (OUTPUT, (BVECT (W (S Z) ItIsSucc) datatype))) b)
                    -> (input  : Term b (TyPort (INPUT,                            datatype))  c)
                              -> Term a TyGate c

      Stop : All Used old -> Term old TyUnit Nil

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- test that await works correctly with buffered signal

import System
import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          let val = 3
          (MkDPair bc recv) <- becomeReceiver Blocking bcRef
          child <- fork $ do (MkDPair bc' buffer) <- becomeBuffer bcRef
                             sleep 1    -- give parent time to call recv.
                             buffer Signal bc' [val, val + 1]
          val' <- recv bc
          if val /= val'
             then putStrLn "ERROR: Value changed in transit."
             else do threadWait child
                     putStrLn "Success!"