text:
module MonadLogic

-- Based on http://okmij.org/ftp/papers/LogicT.pdf
-- http://hackage.haskell.org/package/logict-0.7.0.1/docs/Control-Monad-Logic.html

import Control.Monad.Identity
import Control.Monad.Trans

interface Monad m => MonadPlus (m : Type -> Type) where
    mplus : m a -> m a -> m a
    mzero : m a

interface MonadPlus m => MonadLogic (m : Type -> Type) where
  msplit : m a -> m (Maybe (a, () -> m a))
  interleave : m a -> m a -> m a
  bind : m a -> (a -> m b) -> m b
  ifte : m a -> (a -> m b) -> m b -> m b
  once : m a -> m a

reflect : MonadLogic m => Maybe (a, () -> m a) -> m a
reflect Nothing = mzero
reflect (Just (a, fk)) = pure a `mplus` (fk ())

interleave' : MonadLogic m => m a -> m a -> m a
interleave' m1 m2 = do r <- msplit m1
                       case r of
                        Nothing => m2
                        Just (a, fk) => (pure a) `mplus` (interleave' m2 (fk ()))

bind' : MonadLogic m => m a -> (a -> m b) -> m b
bind' ma f = do r <- msplit ma
                case r of
                 Nothing => mzero
                 Just (a, fk) => interleave (f a) ((fk ()) `bind'` f)

ifte' : MonadLogic m => m a -> (a -> m b) -> m b -> m b
ifte' t th el = do r <- msplit t
                   case r of
                    Nothing => el
                    Just (a, fk) => (th a) `mplus` ((fk ()) >>= th)

once' : MonadLogic m => m a -> m a
once' m = do r <- msplit m
             case r of
               Nothing => mzero
               Just (a, _) => pure a

data LogicT : (m : Type -> Type) -> (a : Type) -> Type where
    LT : ({r : Type} -> (a -> (() -> m r) -> m r) -> (() -> m r) -> m r) -> LogicT m a

Functor (LogicT m) where
  map f (LT g) = LT $ \sk, fk => g (sk . f) fk

Applicative (LogicT m) where
  pure a = LT $ \sk, fk => sk a fk
  (LT f) <*> (LT g) = LT $ \sk, fk => f (\sk', fk' => g (sk . sk') fk') fk

Monad (LogicT m) where
  (LT g) >>= f = LT $ \sk, fk => g (\a, fk' => let (LT g') = f a in g' sk fk') fk

MonadPlus (LogicT m) where
  mzero = LT $ \sk, fk => fk ()
  mplus (LT f) (LT f') = LT $ \sk, fk => f sk (\() => f' sk fk)

MonadTrans LogicT where
  lift m = LT $ \sk, fk => m >>= \a => sk a fk

Monad m => MonadLogic (LogicT m) where
  msplit (LT f) = lift $ f (\a, fk => pure $ Just (a, \() => lift (fk ()) >>= reflect)) (\() => pure Nothing)
  interleave = interleave'
  bind = bind'
  ifte = ifte'
  once = once'

observe : Monad m => Nat -> LogicT m a -> m (List a)
observe Z _ = pure []
observe (S n) m = let (LT f) = msplit m in f sk (\() => pure [])
  where
    sk : {a : Type, m : Type -> Type} -> Monad m => Maybe (a, () -> LogicT m a) -> (() -> m (List a)) -> m (List a)
    sk Nothing fk = pure []
    sk (Just (a, fk')) fk = map (\xs => a :: xs) (observe n (fk' ()))

ones : MonadPlus m => Int -> m Int
ones n = if n <= 0 then mzero else (pure 1) `mplus` (ones (n - 1))

zeros : MonadPlus m => Int -> m Int
zeros n = if n <= 0 then mzero else (pure 0) `mplus` (zeros (n - 1))

test : List (List Int)
test = observe 10 (ones 5 `interleave` zeros 5)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Lightyear.Combinators
import Lightyear.Core
import Lightyear.Char
import Lightyear.Strings

data Assoc = AssocNone
           | AssocLeft
           | AssocRight

data Operator a = Infix (Parser (a -> a -> a)) Assoc
                | Prefix (Parser (a -> a))
                | Postfix (Parser (a -> a))

LO : Type -> Type
LO a = List (Operator a)

OperatorTable : Type -> Type
OperatorTable a = List (LO a)

BinaryOperator : Type -> Type
BinaryOperator a = List (Parser (a -> a -> a))

UnaryOperator : Type -> Type
UnaryOperator a = List (Parser (a -> a))

data Ops a = BinOp (BinaryOperator a) | UnOp (UnaryOperator a)

ReturnType : Type -> Type
ReturnType a = (BinaryOperator a, BinaryOperator a, BinaryOperator a, UnaryOperator a, UnaryOperator a)

toParserBin : BinaryOperator a -> Parser (a -> a -> a)
toParserBin [] = fail "couldn't create binary parser"
toParserBin (x :: xs) = x <|> toParserBin xs

toParserUn : UnaryOperator a -> Parser (a -> a)
toParserUn [] = fail "couldn't create unary parser"
toParserUn (x :: xs) = x <|> toParserUn xs

ambigious : (assoc : String) -> (op : Parser (a -> a -> a)) -> Parser a
ambigious assoc op = do op
                        fail ("ambiguous use of a " ++ assoc ++ " associative operator")

mutual
  mkRassocP : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkRassocP amLeft amNon rassocOp termP x =
   (do f <- rassocOp
       y <- do z <- termP ; mkRassocP1 amLeft amNon rassocOp termP z
       pure (f x y))
   <|> (amLeft)
   <|> (amNon)

  mkRassocP1 : (amLeft : Parser a) -> (amNon : Parser a) -> (rassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkRassocP1 amLeft amNon rassocOp termP x = (mkRassocP amLeft amNon rassocOp termP x) <|> pure x

mutual
  mkLassocP : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkLassocP amRight amNon lassocOp termP x =
    (do f <- lassocOp
        y <- termP
        mkLassocP1 amRight amNon lassocOp termP (f x y))
    <|> amRight
    <|> amNon

  mkLassocP1 : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
  mkLassocP1 amRight amNon lassocOp termP x = mkLassocP amRight amNon lassocOp termP x <|> pure x

mkNassocP : (amRight : Parser a) -> (amLeft : Parser a) -> (amNon : Parser a) -> (nassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a
mkNassocP amRight amLeft amNon nassocOp termP x =
  do f <- nassocOp
     y <- termP
     amRight <|> amLeft <|> amNon
     pure (f x y)

buildExpressionParser : (a : Type) -> OperatorTable a -> Parser a -> Parser a
buildExpressionParser a operators simpleExpr =
  foldl (makeParser a) simpleExpr operators
  where
    splitOp : (a : Type) -> Operator a -> ReturnType a -> ReturnType a
    splitOp x (Infix op AssocNone) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, op :: nassoc, prefixx, postfix)
    splitOp x (Infix op AssocLeft) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, op :: lassoc, nassoc, prefixx, postfix)
    splitOp x (Infix op AssocRight) (rassoc, lassoc, nassoc, prefixx, postfix) = (op :: rassoc, lassoc, nassoc, prefixx, postfix)
    splitOp x (Prefix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, op :: prefixx, postfix)
    splitOp x (Postfix op) (rassoc, lassoc, nassoc, prefixx, postfix) = (rassoc, lassoc, nassoc, prefixx, op :: postfix)

    makeParser : (a : Type) -> Parser a -> LO a -> Parser a
    makeParser a term ops =
      let (rassoc,lassoc,nassoc
               ,prefixx,postfix) = foldr (splitOp a) ([],[],[],[],[]) ops
          rassocOp = toParserBin rassoc
          lassocOp = toParserBin lassoc
          nassocOp = toParserBin nassoc
          prefixxOp = toParserUn prefixx
          postfixOp = toParserUn postfix

          amRight = ambigious "right" rassocOp
          amLeft = ambigious "left" lassocOp
          amNon = ambigious "non" nassocOp

          prefixxP = prefixxOp <|> pure id

          postfixP = postfixOp <|> pure id

          termP = do pre <- prefixxP
                     x <- term
                     post <- postfixP
                     pure (post (pre x))

          rassocP = mkRassocP amLeft amNon rassocOp termP
          rassocP1 = mkRassocP1 amLeft amNon rassocOp termP

          lassocP = mkLassocP amRight amNon lassocOp termP
          lassocP1 = mkLassocP1 amRight amNon lassocOp termP

          nassocP = mkNassocP amRight amLeft amNon nassocOp termP
          in
          do x <- termP
             rassocP x <|> lassocP  x <|> nassocP x <|> pure x <?> "operator"

mutual
  table : OperatorTable Integer
  table =
    [ [Infix (do token "*"; pure (*) ) AssocLeft]
    , [Infix (do token "+"; pure (+) ) AssocLeft]]

  intConst : Parser Integer
  intConst = do i <- integer
                pure (i)

  term : Parser Integer
  term = intConst <|>| parens expr
         <?> "simple expression"

  expr : Parser Integer
  expr = buildExpressionParser Integer table term

ext: idr

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
-- -------------------------------------------------------- [ Problem.idr<Sif> ]
-- Module    : Problem.idr<Sif>
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Parser problem specifications
module Sif.DSL.Parser.Problem

-- ----------------------------------------------------------------- [ Imports ]
import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Sif.Types
import Sif.AbsSyntax
import Sif.Pattern.Model

import Sif.DSL.Parser.Utils
import Sif.DSL.Parser.Common

-- -------------------------------------------------------------- [ Directives ]

%default partial
%access private

-- ----------------------------------------------------------------- [ Parsers ]

data VariableDecl : Type where
  MkVar : String -> String -> (Maybe String) -> VariableDecl

furpsTy : Parser RTy
furpsTy = (keyword "Functional"     *> return FUNC)
      <|> (keyword "Usability"      *> return USAB)
      <|> (keyword "Reliability"    *> return RELI)
      <|> (keyword "Performance"    *> return PERF)
      <|> (keyword "Supportability" *> return SUPP)
      <?> "Requirement Type"

variable : Parser a -> Parser $ Pair a VariableDecl
variable getTy = do
    d <- opt sifDoc
    i <- ident
    token "<-"
    ty <- getTy
    t <- title
    sifComment
    pure $ MkPair ty (MkVar i t d)
  <?> "Variable"

requirement : Parser $ SifAST TyREQ
requirement = do
    (ty, MkVar i t d) <- variable furpsTy
    spaces
    pure $ AST.Req i ty t d
  <?> "Requirement"

context : Parser $ Pair String SifDomain
context = do
    (_, MkVar i t d) <- variable (keyword "Context")
    pure $ MkPair i $ MkDomain t d
  <?> "Context"

problemDef : Parser $ VariableDecl
problemDef = do
    (_, var) <- variable (keyword "Problem")
    pure var
  <?> "Problem"

export
problem : Parser $ SifAST TyPROBLEM
problem = do
    sifComment
    keyword "sif"
    string "problem"
    endOfLine
    sifComment
    (MkVar i t d) <- problemDef
    c <- opt $ some context
    sifComment
    rs <- many requirement
    sifComment
    case c of
      Nothing  => pure $ (AST.Problem i t d [("std", defaultDomain)] rs)
      Just Nil => pure $ (AST.Problem i t d [("std", defaultDomain)] rs)
      Just cs  => pure $ (AST.Problem i t d cs rs)
  <?> "Problem Specification"

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Verified.Algebra.Nat

import Classes.Verified

%default total

fromAdditive : Additive -> Nat
fromAdditive (getAdditive n) = n

natAndAdditive1 : fromAdditive (getAdditive n) = n
natAndAdditive1 = Refl

natAndAdditive2 : getAdditive (fromAdditive n) = n
natAndAdditive2 {n=getAdditive n'}= Refl

natAndAdditiveOp1 : fromAdditive (getAdditive n <+> getAdditive m) = n + m
natAndAdditiveOp1 = Refl

natAndAdditiveOp2 : getAdditive (fromAdditive n + fromAdditive m) = n <+> m
natAndAdditiveOp2 {n=getAdditive n'} {m=getAdditive m'} = Refl

fromMultiplicative : Multiplicative -> Nat
fromMultiplicative (getMultiplicative n) = n

natAndMultiplicative1 : fromMultiplicative (getMultiplicative n) = n
natAndMultiplicative1 = Refl

natAndMultiplicative2 : getMultiplicative (fromMultiplicative n) = n
natAndMultiplicative2 {n=getMultiplicative n'} = Refl

natAndMultiplicativeOp1 : fromMultiplicative (getMultiplicative n <+> getMultiplicative m) = n * m
natAndMultiplicativeOp1 = Refl

natAndMultiplicativeOp2 : getMultiplicative (fromMultiplicative n * fromMultiplicative m) = n <+> m
natAndMultiplicativeOp2 {n=getMultiplicative n'} {m=getMultiplicative m'} = Refl

instance VerifiedSemigroup Additive where
  semigroupOpIsAssociative (getAdditive l) (getAdditive c) (getAdditive r) =
    ?lemmaAdditiveAssoc

instance VerifiedMonoid Additive where
  monoidNeutralIsNeutralL (getAdditive l) = ?lemmaAdditiveNeutralL
  monoidNeutralIsNeutralR (getAdditive r) = ?lemmaAdditiveNeutralR

instance VerifiedSemigroup Multiplicative where
  semigroupOpIsAssociative (getMultiplicative l) (getMultiplicative c) (getMultiplicative r) =
    ?lemmaMultiplicativeAssoc

instance VerifiedMonoid Multiplicative where
  monoidNeutralIsNeutralL (getMultiplicative l) = ?lemmaMultiplicativeNeutralL
  monoidNeutralIsNeutralR (getMultiplicative r) = ?lemmaMultiplicativeNeutralR

---------- Proofs ----------

Verified.Algebra.Nat.lemmaMultiplicativeNeutralL = proof
  intros
  rewrite multOneRightNeutral l
  exact Refl

Verified.Algebra.Nat.lemmaMultiplicativeNeutralR = proof
  intros
  rewrite multOneLeftNeutral r
  exact Refl

Verified.Algebra.Nat.lemmaMultiplicativeAssoc = proof
  intros
  rewrite multAssociative l c r
  exact Refl

Verified.Algebra.Nat.lemmaAdditiveNeutralL = proof
  intros
  rewrite (plusZeroRightNeutral l)
  exact Refl

Verified.Algebra.Nat.lemmaAdditiveNeutralR = proof
  intros
  exact Refl

Verified.Algebra.Nat.lemmaAdditiveAssoc = proof
  intros
  rewrite (plusAssociative l c r)
  exact Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
foo : Int -> Int
foo x = x

bar : Int -> Int
bar x = let y := (42 in y + x

baz : Int -> Int
baz x = x


text:
import System.File

main : IO ()
main = do
    Right str <- readFile "Main.cases"
        | Left err => putStrLn "Error:" *> printLn err
    putStrLn str


text:
> module NonNegDouble.Postulates

> import NonNegDouble.Properties
> import Double.Predicates
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import List.Operations

> %default total
> %access public export

* Properties of sums of products:

> using implementation NumNonNegDouble
>   |||
>   postulate
>   mapIdRightMultPreservesPositivity :
>     {A : Type} ->
>     (axs : List (A, NonNegDouble)) ->
>     Positive (toDouble (sumMapSnd axs)) ->
>     (y : NonNegDouble) ->
>     Positive (toDouble y) ->
>     Positive (toDouble (sumMapSnd (mapIdRightMult (axs, y))))

> using implementation NumNonNegDouble
>   |||
>   postulate
>   sumMapSndConsLemma1 :
>     {A : Type} ->
>     (a : A) ->
>     (x : Double) ->
>     (px : Positive x) ->
>     (nnx : NonNegative x) ->
>     (axs : List (A, NonNegDouble)) ->
>     Positive (toDouble (sumMapSnd ((a, Element x nnx) :: axs)))

> using implementation NumNonNegDouble
>   |||
>   postulate
>   mvMultLemma : {A, B : Type} ->
>                 (axs : List (A, NonNegDouble)) ->
>                 Positive (toDouble (sumMapSnd axs)) ->
>                 (f : A -> List (B, NonNegDouble)) ->
>                 ((a : A) -> Positive (toDouble (sumMapSnd (f a)))) ->
>                 Positive (toDouble (sumMapSnd (mvMult axs f)))

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Hittable

import Vec3
import Ray
import shapes.Sphere

%access export

public export

record HitRecord where
    constructor MkHitRecord
    p, normal  : Vec3
    t          : Double
    front_face : Bool
    isHitted   : Bool

set_face_normal : Ray -> Vec3 -> HitRecord -> HitRecord
set_face_normal ray outward_normal rec =
    record {
        -- front_face = dot (dir ray) outward_normal < 0.0
        normal = outward_normal
            -- then outward_normal
            -- else -outward_normal
        } rec

public export

interface Hittable s where
    hit : Ray -> Double -> Double -> s -> HitRecord

data HittableList = List (Sphere)

Hittable HittableList where
    hit ray t_min t_max list =
        map (hit ray t_min t_max) list

max_stars_repo_name: MarkMarkyMarkus/YART

max_issues_repo_name: MarkMarkyMarkus/YART

max_forks_repo_name: MarkMarkyMarkus/YART


text:
module RandomAccessList

%default total
%access private

public export
interface RandomAccessList (r : Type -> Type) where
  empty : r a
  isEmpty : r a -> Bool

  cons : a -> r a -> r a
  head : r a -> a
  tail : r a -> r a

  lookup : Int -> r a -> a
  update : Int -> a -> r a -> r a


text:
import Data.Vect as V
import Data.Vect.Extra
import Data.Nat
import Data.List as L
import Data.String.Parser

import System.File

data Cucumber = H | V

isH : Maybe Cucumber -> Bool
isH (Just H) = True
isH _ = False

isV : Maybe Cucumber -> Bool
isV (Just V) = True
isV _ = False

Grid : Nat -> Nat -> Type
Grid x y = Vect (S y) (Vect (S x) (Maybe Cucumber))

cucumberParser : Parser (Maybe Cucumber)
cucumberParser = char '>' $> Just H <|> char 'v' $> Just V <|> char '.' $> Nothing

parser : Parser (x ** y ** Grid x y)
parser = do row <- some cucumberParser <* char '\n'
            let x = length row
            Just v <- pure $ toVect x row
              | Nothing => fail "not length"
            Yes ItIsSucc <- pure $ isItSucc x
              | No _ => fail "Row is zero"
            cs <- some ((ntimes x cucumberParser) <* char '\n')
            let y = length cs
            Just cs <- pure $ toVect y cs
              | Nothing => fail "not column"
            pure $ (_ ** (_ ** v :: cs))

Move : Nat -> Nat -> Type
Move x y = ((Fin (S x), Fin (S y)), (Fin (S x), Fin (S y)))

addWrap : {n : Nat} -> Fin (S n) -> Fin (S n)
addWrap f = case strengthen $ shift 1 f of
               Nothing => 0
               (Just f) => f

hMoves : {x : Nat} -> {y : Nat} -> Grid x y -> List (Move x y)
hMoves g = filter (\(_,(x,y)) => isNothing $ index x $ index y g) $ map (\(x,y,_) => ((x, y), (addWrap x, y))) $ toList $ join $ toList $ (\(y,xs) => filter (isH . snd . snd) $ toList $ mapWithPos (,y,) $ xs) <$> mapWithPos (,) g

vMoves : {x : Nat} -> {y : Nat} -> Grid x y -> List (Move x y)
vMoves g = filter (\(_,(x,y)) => isNothing $ index x $ index y g) $ map (\(x,y,_) => ((x, y), (x, addWrap y))) $ toList $ join $ toList $ (\(y,xs) => filter (isV . snd . snd) $ toList $ mapWithPos (,y,) $ xs) <$> mapWithPos (,) g

steps : {x : Nat} -> {y : Nat} -> Grid x y -> Nat
steps g = steps' 1 g
  where
    doMoves : Grid x y -> List (Move x y) -> Grid x y
    doMoves g [] = g
    doMoves g (((x1, y1), (x2, y2)) :: ms) = let c = index x1 $ index y1 g
                                                 g1 = updateAt y1 (replaceAt x1 Nothing) g
                                                 g2 = updateAt y2 (replaceAt x2 c) g1 in
                                                 doMoves g2 ms

    steps' : Nat -> Grid x y -> Nat
    steps' n g = case hMoves g of
                      [] => case vMoves g of
                                 [] => n
                                 ms => steps' (S n) (doMoves g ms)
                      ms => let g' = doMoves g ms in
                                case vMoves g' of
                                     [] => steps' (S n) g'
                                     ms => steps' (S n) (doMoves g' ms)

part1 : {n : Nat} -> {m : Nat} -> Grid n m -> IO String
part1 a = pure $ show $ steps a

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (MkDPair n (MkDPair m a), _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn


text:
module Specdris.ExpectationsTest

import Specdris.Data.SpecInfo
import Specdris.Data.SpecResult
import Specdris.Data.SpecState

import Specdris.Core
import Specdris.Expectations

import Specdris.TestUtil

%access private
%default total

test : (description : String) -> SpecResult -> SpecTree
test descr spec = Node (Leaf $ Left $ Describe descr)
                       (Leaf $ Right $ pure spec)

showTestCase : String -> String
showTestCase test = "expectation_" ++ test

noAround : IO SpecResult -> IO SpecResult
noAround spec = spec

testPending : IO ()
testPending
  = do state1 <- evaluate noAround False $ test (showTestCase "pending") $ pending
       state2 <- evaluate noAround False $ test (showTestCase "pendingWith") $ pendingWith "test"

       testAndPrint "pending" state1 (MkState 1 0 1 Nothing) (==)
       testAndPrint "pendingWith" state2 (MkState 1 0 1 Nothing) (==)

testEqual : IO ()
testEqual
  = do state1 <- evaluate noAround False $ test (showTestCase "shouldBe") $ 1 `shouldBe` 1
       state2 <- evaluate noAround False $ test (showTestCase "===") $ 1 === 2

       testAndPrint "equal" state1 (MkState 1 0 0 Nothing) (==)
       testAndPrint "===" state2 (MkState 1 1 0 Nothing) (==)

testUnequal : IO ()
testUnequal
  = do state1 <- evaluate noAround False $ test (showTestCase "shouldNotBe") $ 1 `shouldNotBe` 2
       state2 <- evaluate noAround False $ test (showTestCase "/==") $ 1 /== 1

       testAndPrint "unequal" state1 (MkState 1 0 0 Nothing) (==)
       testAndPrint "/==" state2 (MkState 1 1 0 Nothing) (==)

testSatisfy : IO ()
testSatisfy
  = do state1 <- evaluate noAround False $ test (showTestCase "sat") $ 1 `shouldSatisfy` (> 0)
       state2 <- evaluate noAround False $ test (showTestCase "!sat") $ 1 `shouldSatisfy` (> 1)

       testAndPrint "satisfy" state1 (MkState 1 0 0 Nothing) (==)
       testAndPrint "satisfy" state2 (MkState 1 1 0 Nothing) (==)

testShouldBeJust : IO ()
testShouldBeJust
  = do state1 <- evaluate noAround False $ test (showTestCase "shouldBeJust") $ (Just "hello") `shouldBeJust` (=== "hello")
       state2 <- evaluate noAround False $ test (showTestCase "shouldBeJust") $ Nothing `shouldBeJust` (=== "world")

       testAndPrint "shouldBeJust" state1 (MkState 1 0 0 Nothing) (==)
       testAndPrint "shouldBeJust" state2 (MkState 1 1 0 Nothing) (==)

testShouldBeNothing : IO ()
testShouldBeNothing
  = do state1 <- evaluate noAround False $ test (showTestCase "shouldBeNothing") $ (shouldBeNothing (Just "hello"))
       state2 <- evaluate noAround False $ test (showTestCase "shouldBeNothing") $ shouldBeNothing {a = String} Nothing

       testAndPrint "shouldBeNothing" state1 (MkState 1 1 0 Nothing) (==)
       testAndPrint "shouldBeNothing" state2 (MkState 1 0 0 Nothing) (==)

export
specSuite : IO ()
specSuite = do putStrLn "\n  expectations:"
               testPending
               testEqual
               testUnequal
               testSatisfy
               testShouldBeJust
               testShouldBeNothing

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
import Arduino.Lib
import Arduino.Mega

%hint
x : Nat
x = 13

%hint
y : Pin
y = D x

export
main : IO Unit
main = runArd Mega2560 $ do
     pinMode (D 13) Output
     forever $ do
       digitalWrite (D 13) High
       sleepFor 1000
       digitalWrite (D 13) Low
       sleepFor 2000

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
infixr 0 -->
(-->) : (Type -> Type) -> (Type -> Type) -> Type


text:
module Cordial.Model.Common.Essential

%default total
%access public export

infixl 8 #
infixr 6 :=

-- -------------------------------------------------------------- [ Properties ]

data ConnectionTy = BUS | ADHOC

||| With respect to the Comms protocol as a whole, does the IP
||| interface produce or consume signals.
data Endpoint = PRODUCER | CONSUMER

||| Does the bus support broadcasting, or unicast connections.
data CommStyle = Broadcast | Unicast

||| Where does the Port originate from.
data Origin = SYSTEM String | IP

||| For arrays we note the endian value
data Endian = Big | Little

||| Capture wire sensitivity
data Sensitivity = High | Low | Rising | Falling | Insensitive

data Polarity = ActiveHigh | ActiveLow

||| For default signal values
data Value = Zero | One

||| Capture port shape
data PortShape = WIRE | ARRAY

data ClockEdge = Rise | Fall

data Delay = Max Nat | Min Nat

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
||| immutable queue
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Immutable.Queue

import Data.List
import Data.So

%default total

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

export data Queue t = MkQueue (List t) (List t)

export newQueue : Queue t
newQueue = MkQueue [] []

export null : Queue t -> Bool
null (MkQueue [] []) = True
null _ = False

export length : Queue t -> Nat
length (MkQueue ys zs) = length ys + length zs

export push : t -> Queue t -> Queue t
push x (MkQueue ys zs) = MkQueue (x::ys) zs

export pull : Queue t -> (Maybe t, Queue t)
pull q@(MkQueue ys []) =
  case reverse ys of
       []      => (Nothing, q)
       (y::ys) => (Just y, MkQueue [] ys)
pull (MkQueue ys (z::zs)) = (Just z, MkQueue ys zs)

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

export null_length_is_zero : {x:Queue t} -> (pr: So (null x)) -> length x = 0
null_length_is_zero = ?lhs

{-
export push_pop_doesnt_change_length :
  {xs:Queue t} -> (pull (push x xs) == (x, ys) /\ xs = ys)
-}

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Cordial.Model.Interface.Kinds

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

%default total
%access public export

||| What type of interface are we.
data InterfaceKind : (isMonitor : Bool)
                  -> (endpoint  : Endpoint)
                  -> Type
  where
    Producer  : InterfaceKind False PRODUCER
    Consumer  : InterfaceKind False CONSUMER

    System   : (e : Endpoint) -> InterfaceKind False e

    Monitor  : InterfaceKind True CONSUMER

namespace IKinds

   data InterfaceKinds : List (Bool, Endpoint) -> Type where
      Nil : InterfaceKinds Nil
      (::) : InterfaceKind b e
          -> InterfaceKinds kinds
          -> InterfaceKinds ((b,e)::kinds)

   {- [ NOTE ]

   I would rather replace `InterfaceKinds` with a DList. However, type
   checking later on becomes problematic. Idris, for some reason,
   cannot resolve the types.

   -}


text:
module Data.List.Quantifiers

import Data.List
import Data.List.Elem

||| A proof that some element of a list satisfies some property
|||
||| @ p the property to be satisfied
public export
data Any : (0 p : a -> Type) -> List a -> Type where
  ||| A proof that the satisfying element is the first one in the `List`
  Here  : {0 xs : List a} -> p x -> Any p (x :: xs)
  ||| A proof that the satisfying element is in the tail of the `List`
  There : {0 xs : List a} -> Any p xs -> Any p (x :: xs)

export
Uninhabited (Any p Nil) where
  uninhabited (Here _) impossible
  uninhabited (There _) impossible

||| Given a decision procedure for a property, determine if an element of a
||| list satisfies it.
|||
||| @ p the property to be satisfied
||| @ dec the decision procedure
||| @ xs the list to examine
export
any : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (Any p xs)
any _ Nil = No uninhabited
any p (x::xs) with (p x)
  any p (x::xs) | Yes prf = Yes (Here prf)
  any p (x::xs) | No ctra =
    case any p xs of
      Yes prf' => Yes (There prf')
      No ctra' => No $ \case
        Here px => ctra px
        There pxs => ctra' pxs

||| A proof that all elements of a list satisfy a property. It is a list of
||| proofs, corresponding element-wise to the `List`.
public export
data All : (0 p : a -> Type) -> List a -> Type where
  Nil  : All p Nil
  (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs)

||| Given a decision procedure for a property, decide whether all elements of
||| a list satisfy it.
|||
||| @ p the property
||| @ dec the decision procedure
||| @ xs the list to examine
export
all : (dec : (x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs)
all _ Nil = Yes Nil
all d (x::xs) with (d x)
  all d (x::xs) | No ctra = No $ \(p::_) => ctra p
  all d (x::xs) | Yes prf =
    case all d xs of
      Yes prf' => Yes (prf :: prf')
      No ctra' => No $ \(_::ps) => ctra' ps

||| If there does not exist an element that satifies the property, then it is
||| the case that all elements do not satisfy it.
export
negAnyAll : {xs : List a} -> Not (Any p xs) -> All (Not . p) xs
negAnyAll {xs=Nil}   _ = Nil
negAnyAll {xs=x::xs} f = (f . Here) :: negAnyAll (f . There)

||| If there exists an element that doesn't satify the property, then it is
||| not the case that all elements satisfy it.
export
anyNegAll : Any (Not . p) xs -> Not (All p xs)
anyNegAll (Here ctra) (p::_)  = ctra p
anyNegAll (There np)  (_::ps) = anyNegAll np ps

||| Given a proof of membership for some element, extract the property proof for it
export
indexAll : Elem x xs -> All p xs -> p x
indexAll  Here     (p::_  ) = p
indexAll (There e) ( _::ps) = indexAll e ps

||| Modify the property given a pointwise function
export
mapProperty : (f : {0 x : a} -> p x -> q x) -> All p l -> All q l
mapProperty f [] = []
mapProperty f (p::pl) = f p :: mapProperty f pl


text:
module Main

data Free : (f : Type -> Type) -> (a : Type) -> Type where
  Pure : a -> Free f a
  Bind : f (Free f a) -> Free f a

Functor f => Functor (Free f) where
  map f m = assert_total $ case m of
    Pure x => Pure (f x)
    Bind x => Bind (map (map f) x)

Functor f => Applicative (Free f) where
  pure = Pure

  m <*> x = assert_total $ case m of
    Pure f => map f x
    Bind f => Bind (map (<*> x) f)

Functor f => Monad (Free f) where
  m >>= f = assert_total $ case m of
    Pure x => f x
    Bind x => Bind (map (>>= f) x)

liftFree : Functor f => f a -> Free f a
liftFree = assert_total $ Bind . map Pure

foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
foldFree f m = assert_total $ case m of
  Pure x => pure x
  Bind x => f x >>= foldFree f

data FileSystemF next
  = ReadFile (String -> next)

FileSystem : Type -> Type
FileSystem = Free FileSystemF

Functor FileSystemF where
  map f (ReadFile nextFn) = ReadFile (f . nextFn)

readFileF : FileSystem String
readFileF = liftFree $ ReadFile id

interpret2 : FileSystemF a -> IO a
interpret2 (ReadFile nextFn) = do
  contents <- pure "ola"
  pure (nextFn contents)

main : IO ()
main =
  do
    c <- foldFree interpret2 readFileF
    putStrLn' c

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:
module Data.Vect.Extra

import Data.Vect

%default total

public export
asVect : List a -> (n : Nat ** Vect n a)
asVect [] = (0 ** [])
asVect (x :: xs) = let (n ** xs') = asVect xs in (S n ** x :: xs')

public export
mapWithIndex : (Fin n -> a -> b) -> Vect n a -> Vect n b
mapWithIndex f = \case
  [] => []
  x :: xs => f FZ x :: mapWithIndex (f . FS) xs

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Applicative
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens

import public Control.Lens.At
import public Control.Lens.Types
import public Control.Lens.Const
import public Control.Lens.First
import public Control.Lens.Getter
import public Control.Lens.Review
import public Control.Lens.Setter
import public Control.Lens.Prism
import public Control.Lens.Tuple
import public Control.Lens.Maths
import public Control.Lens.Market
import public Control.Lens.Iso
import public Control.Lens.Lens
import public Control.Monad.Identity
import public Data.Bifunctor
import public Data.Bitraversable
import public Data.Contravariant
import public Data.Curried
import public Data.Profunctor
import public Data.Tagged
import public Data.Yoneda

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


text:
module Idris.Main

import Idris.Driver
import Compiler.Common

main : IO ()
main = mainWithCodegens []


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionBroadcast` wakes the child with 1 main and 1 child thread

main : IO ()
main =
  do cvMutex <- makeMutex
     cv <- makeCondition
     t <- fork $ do mutexAcquire cvMutex
                    conditionWait cv cvMutex
                    putStrLn "Hello mother"
     putStrLn "Hello child"
     sleep 1
     conditionBroadcast cv
     threadWait t


text:
module Toolkit.Data.Vect.Extra

import public Decidable.Equality
import        Data.Vect

%default total

namespace Equality
   public export
   vecEq : Eq type => Vect n type -> Vect m type -> Bool
   vecEq [] [] = True
   vecEq [] (x :: xs) = False
   vecEq (x :: xs) [] = False
   vecEq (x :: xs) (y :: ys) = x == y && vecEq xs ys

namespace Decidable
  namespace SameLength
    public export
    decEq : DecEq type
          => (n = m)
          -> (xs : Vect n type)
          -> (ys : Vect m type)
          -> Dec (xs = ys)
    decEq Refl xs ys with (decEq xs ys)
      decEq Refl ys ys | (Yes Refl) = Yes Refl
      decEq Refl xs ys | (No contra) = No contra

  namespace DiffLength

    public export
    vectorsDiffLength : DecEq type
                      => (contra : (n = m) -> Void)
                      -> {xs : Vect n type}
                      -> {ys : Vect m type}
                      -> (xs = ys) -> Void
    vectorsDiffLength contra Refl = contra Refl

    public export
    decEq : DecEq type
         => {n,m : Nat}
         -> (xs : Vect n type)
         -> (ys : Vect m type)
         -> Dec (xs = ys)
    decEq xs ys {n} {m} with (decEq n m)
      decEq xs ys {n = m} {m = m} | (Yes Refl) = decEq Refl xs ys
      decEq xs ys {n = n} {m = m} | (No contra) = No (vectorsDiffLength contra)

namespace Shape

  public export
  data Shape : (xs : Vect n a)
            -> (ys : Vect m a)
            -> Type
    where
      Empty : Shape Nil Nil
      LH    : Shape (x::xs) Nil
      RH    : Shape Nil      (y::ys)
      Both  : Shape (x::xs) (y::ys)

  export
  shape : (xs : Vect n a)
       -> (ys : Vect m a)
       -> Shape xs ys
  shape [] [] = Empty
  shape [] (y :: ys) = RH
  shape (x :: xs) [] = LH
  shape (x :: xs) (y :: ys) = Both

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Gen.Plict

public export
data Plict = Expl | Impl

export
Eq Plict.Plict where
	Expl == Expl = True
	Impl == Impl = True
	_    == _    = False

export
Show Plict.Plict where
	show Expl = "<Explicit>"
	show Impl = "<Implicit>"

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
import System.Concurrency

-- Simple looping thread
consumer : Channel Nat -> IO ()
consumer c =
  do (S k) <- channelGet c
      | Z => pure ()
     consumer c

--  Test that using the same channel with multiple consumers is okay.
main : IO ()
main =
  do c <- makeChannel
     tids <- for [1..7] $ \_ => fork (consumer c)
     ignore $ for [1..100] $ \_ => channelPut c 1
     ignore $ for [1..7] $ \_ => channelPut c Z
     ignore $ traverse (\t => threadWait t) tids
     putStrLn "Success!"


text:
import Data.SortedMap
import Data.List

f : Ord k => SortedMap k v -> List (k, v)
f m = case sortBy (\(x, _), (y, _) => compare x y) (SortedMap.toList m) of
    as => as

g : Ord k => SortedMap k v -> List (k, v)
g m = let kvs = toList m in
          case sortBy (\(x, _), (y, _) => compare x y) kvs of
               as => as


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Files

import Tester

import Language.TOML

import System.Directory
import System.File

parse : String -> TestFunc Table
parse src = do
    Right table <- pure $ parseTOML src
        | Left err => throw (show err)
    pure table

dirEntries : (path : String) -> TestFunc (List String)
dirEntries path = do
    Right dir <- openDir path
        | Left err =>
            throw $ "\nUnable to open dir \"" ++ path ++ "\": " ++ show err
    entries <- listEntries dir
    closeDir dir
    pure entries
    where
        listEntries : Directory -> TestFunc (List String)
        listEntries dir = do
            Right s <- dirEntry dir
                | Left (GenericFileError 22) => pure []
                | Left err => do
                    throw $ show err

            rest <- listEntries dir
            case s of
                "." => pure rest
                ".." => pure rest
                _ => pure $ s :: rest

filesPass : Test
filesPass = test "valid files" $ do
    let basePath = "tests/pass/"
    dirs <- dirEntries basePath
    for_ dirs \path => do
        Right src <- readFile (basePath ++ path)
            | Left err => throw $ show err

        Right _ <- pure $ parseTOML src
            | Left err => throw $ show err

        pure ()

export
tests : List Test
tests = [
    filesPass
]

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
module JSMatrix.JSMatrix

data JSGLMat3 : Type where
  MkMat3 : Ptr -> JSGLMat3

data JSGLMat4 : Type where
  MkMat4 : Ptr -> JSGLMat4

data JSGLVec3 : Type where
  MkVec3 : Ptr -> JSGLVec3

data JSGLVec4 : Type where
  MkVec4 : Ptr -> JSGLVec4

createMat3 : IO JSGLMat3
createMat3 = do
  m <- mkForeign (FFun "mat3.create()" [] FPtr)
  return (MkMat3 m)

createMat4 : IO JSGLMat4
createMat4 = do
  m <- mkForeign (FFun "mat4.create()" [] FPtr)
  return (MkMat4 m)

createVec3 : IO JSGLVec3
createVec3 = do
  v <- mkForeign (FFun "vec3.create()" [] FPtr)
  return (MkVec3 v)

createVec4 : IO JSGLVec4
createVec4 = do
  v <- mkForeign (FFun "vec4.create()" [] FPtr)
  return (MkVec4 v)

-- Create a GL Matrix 3p Vector from a Vect 3 Float
createVec3FromVect : Vect 3 Float -> IO JSGLVec3
createVec3FromVect [x,y,z] = do
  v <- mkForeign (FFun "vec3.fromValues(%0,%1,%2)" [FFloat,FFloat,FFloat] FPtr) x y z
  return (MkVec3 v)

-- Create a GL Matrix 4p Vector from a Vect 4 Float
createVec4FromVect : Vect 4 Float -> IO JSGLVec4
createVec4FromVect [r,g,b,a] = do
  v <- mkForeign (FFun "vec4.fromValues(%0,%1,%2)" [FFloat,FFloat,FFloat,FFloat] FPtr) r g b a
  return (MkVec4 v)

--| {mat4} mat4.translate(out, a, v)
--| Translate a mat4 by the given vector
-- Parameters:
  -- {mat4} a -- the matrix to translate
  -- {vec3} v -- vector to translate by
  -- {mat4} out -- the receiving matrix
-- Returns:
  -- {mat4} out
translateM4 : JSGLVec3 -> JSGLMat4 -> JSGLMat4 -> IO JSGLMat4
translateM4 (MkVec3 v) (MkMat4 out) (MkMat4 a) = do
  translatedM <- mkForeign (FFun "mat4.translate(%0,%1,%2)" [FPtr,FPtr,FPtr] FPtr) out a v
  return (MkMat4 translatedM)

--| {mat4} mat4.perspective(out, fovy, aspect, near, far)
--| Generates a perspective projection matrix with the given bounds
-- Parameters:
  -- {number} fovy -- Vertical field of view in radians
  -- {number} aspect -- Aspect ratio. typically viewport width/height
  -- {number} near -- Near bound of the frustum
  -- {number} far -- Far bound of the frustum
  -- {mat4} out -- mat4 frustum matrix will be written into
-- Returns:
  -- {mat4} out
perspectiveM4 : Float -> Float -> Float -> Float -> JSGLMat4 -> IO JSGLMat4
perspectiveM4 fovy aspect near far (MkMat4 out) = do
  newMat <- mkForeign (FFun "mat4.perspective(%0,%1,%2,%3,%4)"
                       [FPtr,FFloat,FFloat,FFloat,FFloat]
                       FPtr
                      ) out fovy aspect near far
  return (MkMat4 newMat)

--| {vec3} vec3.normalize(out, a)
--| Normalize a vec3
-- Parameters:
  -- {vec3} a -- vector to normalize
  -- {vec3} out -- the receiving vector
-- Returns:
  -- {vec3} out
normaliseV3 : JSGLVec3 -> JSGLVec3 -> IO JSGLVec3
normaliseV3 (MkVec3 a) (MkVec3 out) = do
  normalisedVec <- mkForeign (FFun "vec3.normalize(%0,%1)"
                              [FPtr,FPtr]
                              FPtr
                             ) out a
  return (MkVec3 normalisedVec)

--| {mat4} mat4.rotate(out, a, rad, axis)
--| Rotates a mat4 by the given angle
-- Parameters:
  -- {mat4} a -- the matrix to rotate
  -- {number} rad -- the angle to rotate the matrix by
  -- {vec3} axis -- the axis to rotate around
  -- {mat4} out -- the receiving matrix
-- Returns:
  -- {mat4} out
rotateM4 : JSGLMat4 -> Float -> JSGLVec3 -> JSGLMat4 -> IO JSGLMat4
rotateM4 (MkMat4 a) rad (MkVec3 axis) (MkMat4 out) = do
  rotatedM4 <- mkForeign (FFun "mat4.rotate(%0,%1,%2,%3)"
                          [FPtr,FPtr,FFloat,FPtr]
                          FPtr
                         ) out a rad axis
  return (MkMat4 rotatedM4)

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Proto

import Data.Vect
import VectHelp
import ProcessLib

%default total

namespace DirectedType
  ||| DTy = DirectedTypes = a typed wire that goes up or down
  public export data DTy = Down Type | Up Type

  public export type: DTy -> Type
  type (Down ty) = ty
  type (Up   ty) = ty

  public export dual: DTy -> DTy
  dual (Down x) = Up x
  dual (Up   x) = Down x

namespace Cut
  ||| Cut through n typed wires
  ||| These are the objects of the category
  public export Cut: Nat -> Type
  Cut n = Vect n DTy

  public export dual: Cut n -> Cut n
  dual = map dual

||| A niche is the top and bottom cut representing the full interface
||| to a process
public export data Niche: Nat -> Nat -> Type where
  MkNiche: (top: Cut m) -> (bot: Cut n) -> Niche m n

||| Incoming wires of a niche
public export data InWire: Niche m n -> Type -> Type where
  TopInWire: Elem (Down a) top -> InWire (MkNiche top bot) a
  BotInWire: Elem (Up a)   bot -> InWire (MkNiche top bot) a

||| Outgoing wires of a niche
public export data OutWire: Niche m n -> Type -> Type where
  TopOutWire: Elem (Up a)   top -> OutWire (MkNiche top bot) a
  BotOutWire: Elem (Down a) bot -> OutWire (MkNiche top bot) a

mutual
  ||| The type of messages that can be sent to a process
  public export data Req: Niche m n -> Type where
    ||| A connection request. This asks to connect one of the processes
    ||| out-wires to a specific in-wire of another process
    Conn: {niche: Niche m n} ->
          {niche': Niche m' n'} ->
          OutWire niche a -> ProcPID niche' -> InWire niche' a -> Req niche
    ||| an incoming value, on a specific in-wire
    Val:  {niche: Niche m n} ->
          (inWire: InWire niche a) -> (x: a) -> Req niche

  ||| Responses to incoming values
  public export data ValResp = Accepted | Error

  export Show ValResp where
    show Accepted = "Accepted"
    show Error = "Error"

  ||| Responses to connection requests
  public export data ConnResp = ConnAccepted | Taken

  export Show ConnResp where
    show ConnAccepted = "ConnAccepted"
    show Taken = "Taken"

  public export ProcIF: (niche: Niche m n) -> Req niche -> Type
  ProcIF niche (Conn _ _ _) = ConnResp
  ProcIF niche (Val _ _)    = ValResp

  -- to start functioning a process must have a complete mapping from its
  -- out-wires to: a process and a suitable inWire of that process

  ||| PIDs of processes that respond according to the proc intercase
  public export ProcPID: Niche m n -> Type
  ProcPID niche = MessagePID (ProcIF niche)

||| The morphisms in our category
public export Hom: Cut m -> Cut n -> Type
Hom c0 c1 = Service (ProcIF (MkNiche c0 c1)) ()

public export SubProc: Niche m n -> Type -> Type
SubProc niche a = Process (ProcIF niche) a Ready Ready

||| A slot is a place where a process can register to be sent the output
public export data Slot: Type -> Type where
  EmptySlot: Slot b
  FullSlot: {niche: Niche m n} ->
            ProcPID niche -> InWire niche b -> Slot b

-- some lemmas we need

export dualAddrUp: {c: Cut n} -> Elem (Up a) (map DirectedType.dual c) -> Elem (Down a) c
dualAddrUp {c= (Down _) :: _}  Here         = Here
dualAddrUp {c= _        :: _} (There later) = There (dualAddrUp later)
--
export dualAddrDown: {c: Cut n} -> Elem (Down a) (map DirectedType.dual c) -> Elem (Up a) c
dualAddrDown {c= (Up _) :: _}  Here         = Here
dualAddrDown {c= _      :: _} (There later) = There (dualAddrDown later)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
data InfList : Type -> Type where
     (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

labelWith : InfList Integer -> List a -> List (Integer, a)
labelWith (lbl :: lbls) [] = []
labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals

label : List a -> List (Integer, a)
label = labelWith (countFrom 0)

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Streaming.Encoding.Base64.Alphabet

import Util -- Char instances

import Data.List

import Data.AVL

import Data.AVL

-- Alphabets MUST BE 64 characters, 0-63 not including pad, this is the base64.
public export
record Alphabet where
  constructor MkAlphabet
  toChar : Int -> Char -- to/from the 64
  fromChar : Char -> Maybe Int -- to/from the 64
  pad : Char -- not part of the 64
  whitespace : Char -> Bool -- not part of the 64

-- An array lookup would be better for toChar
-- ['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ ['+','/']
export
standardAlphabet : Alphabet
standardAlphabet
  = let chars = ['A'..'Z'] ++ ['a'..'z'] ++ ['0'..'9'] ++ ['+','/']
        arf1 = fromList (zip [0..63] chars) -- basic BST for log(n) lookup
        arf2 = fromList (zip chars [0..63]) -- basic BST for log(n) lookup
    in MkAlphabet
         (\i => maybe 'A' id (lookup i arf1))
         -- (\c => fst <$> find ((== c) . snd) alph)
         (\c => lookup c arf2)
         '='
         (`elem` ['\n','_'])