text:
module Main

import Data.Vect

data Box = X | O | Empty

isEmpty : Box -> Bool
isEmpty Empty = True
isEmpty _ = False

Board : (size : Nat) -> Type
Board size = Vect size (Vect size Box)

newBoard : (size : Nat) -> Board size
newBoard size = replicate size (replicate size Empty)

markColumn : Box -> Vect x Box -> Fin x -> Maybe (Vect x Box)
markColumn mark (x :: xs) FZ = case x of
                                    Empty => Just (mark :: xs)
                                    _ => Nothing
markColumn mark (x :: xs) (FS y) = case markColumn mark xs y of
                                        Nothing => Nothing
                                        Just rest => Just (x :: rest)

markSquare : Vect x (Vect y Box) -> Box -> Fin x -> Fin y -> Maybe (Vect x (Vect y Box))
markSquare (x :: xs) mark FZ j = case markColumn mark x j of
                                      Nothing => Nothing
                                      Just new_x => Just (new_x :: xs)
markSquare (x :: xs) mark (FS i) j = case markSquare xs mark i j of
                                          Nothing => Nothing
                                          Just rest => Just (x :: rest)

checkVect : Vect x Box -> Maybe Box
checkVect [] = Just Empty
checkVect (x :: xs) = let rest = checkVect xs in
                          match x rest where
                           match : Box -> Maybe Box -> Maybe Box
                           match x Nothing = Nothing
                           match X (Just X) = Just X
                           match X (Just O) = Nothing
                           match X (Just Empty) = Just X
                           match O (Just X) = Nothing
                           match O (Just O) = Just O
                           match O (Just Empty) = Just O
                           match Empty (Just y) = Nothing

checkRows : Vect x (Vect y Box) -> Maybe Box
checkRows [] = Nothing
checkRows (x :: xs) = case checkVect x of
                           Just X => Just X
                           Just Y => Just Y
                           _ => checkRows xs

checkCols : Vect x (Vect y Box) -> Maybe Box
checkCols board = checkRows (transpose board)

checkDiags : Board size -> Maybe Box
checkDiags {size} board = case checkVect (diag board) of
                              Just a => Just a
                              Nothing => case checkVect (diag (reverse board)) of
                                              Just a => Just a
                                              Nothing => Nothing

findLegalMoves : Vect x (Vect y Box) -> Nat -> List (Nat, Nat)
findLegalMoves [] i = []
findLegalMoves (x :: xs) i = let hits = the (List Nat) (findIndices isEmpty (toList x)) in
                                 (zip (replicate (length hits) i) hits) ++ (findLegalMoves xs (i+1))

checkDraw : Board size -> Bool
checkDraw board  = (length (findLegalMoves board 0)) == 0

checkVictory : Board size -> Maybe Box
checkVictory b = case checkRows b of
                      Just X => Just X
                      Just O => Just O
                      Nothing => case checkCols b of
                                      Just X => Just X
                                      Just O => Just O
                                      Nothing => case checkDiags b of
                                                      Just X => Just X
                                                      Just O => Just O
                                                      Nothing => case checkDraw b of
                                                                      True => Just Empty
                                                                      False => Nothing
readNumber : IO (Maybe Nat)
readNumber = do input <- getLine
                if all isDigit (unpack input)
                   then pure (Just (cast input))
                   else pure Nothing

getMove : Board size -> IO (Fin size, Fin size)
getMove board {size} = do putStr "Enter row: "
                          Just row <- readNumber | Nothing => getMove board
                          let fRow = natToFin row size
                          putStr "Enter col: "
                          Just col <- readNumber | Nothing => getMove board
                          let fCol = natToFin col size
                          case finalizeMove fRow fCol of
                               Nothing => getMove board
                               Just move => pure move
            where
              finalizeMove : Maybe (Fin b) -> Maybe (Fin b) -> Maybe (Fin b, Fin b)
              finalizeMove Nothing y = Nothing
              finalizeMove (Just x) Nothing = Nothing
              finalizeMove (Just x) (Just y) = Just (x, y)

formattedRow : Vect n String -> String
formattedRow [] = ""
formattedRow (x :: xs) = x ++ (formattedRow xs)

stringify : Box -> String
stringify X = "X"
stringify O = "O"
stringify Empty = " "

showBoard : Vect n (Vect m Box) -> String
showBoard [] = ""
showBoard (x :: xs) {m} = (formattedRow (intersperse "|" (map stringify x))) ++ "\n" ++
                        rest xs where
                        rest : Vect n' (Vect m Box) -> String
                        rest [] = showBoard xs
                        rest xs = (formattedRow (replicate (2 * m) "-")) ++ "\n" ++ (showBoard xs)

flipPlayer : Box -> Box
flipPlayer X = O
flipPlayer O = X
flipPlayer Empty = Empty

runGame : Board size -> Box -> IO ()
runGame [] player  = putStrLn "weird board!"
runGame board player = do putStrLn (showBoard board)
                          putStrLn ((stringify player) ++ "'s turn: ")
                          move <- getMove board
                          case markSquare board player (fst move) (snd move) of
                               Nothing => runGame board player
                               Just new_board => case checkVictory new_board of
                                                      Nothing => runGame new_board (flipPlayer player)
                                                      Just Empty => putStrLn "Draw"
                                                      Just b => putStrLn ((stringify b) ++ " wins!")

main : IO ()
main = do runGame (newBoard 3) X

max_stars_repo_name: scotthellman/tictactoe

max_issues_repo_name: scotthellman/tictactoe

max_forks_repo_name: scotthellman/tictactoe


text:
module Toolkit.Data.List.Occurs.Does

import Decidable.Equality

import Data.Nat

import Toolkit.Decidable.Informative

import public Toolkit.Data.List.Occurs.Error

%default total

namespace Exactly
  public export
  data Occurs : (type : Type)
             -> (p    : type -> Type)
             -> (xs   : List type)
             -> (cy   : Nat)
                     -> Type
    where
      End : Occurs type p Nil Z

      Yes : (holds : p x)
         -> (rest  : Occurs type p     xs     cy)
                  -> Occurs type p (x::xs) (S cy)

      No : (nope : Not (p x))
        -> (rest : Occurs type p     xs  cy)
                -> Occurs type p (x::xs) cy

  export
  Uninhabited (Occurs type p Nil (S x)) where
    uninhabited End impossible
    uninhabited (Yes holds rest) impossible
    uninhabited (No nope rest) impossible

  namespace Check
    shouldHaveOneMore : (p x)
                     -> (Occurs type p       xs     k  -> Void)
                     ->  Occurs type p (x :: xs) (S k) -> Void
    shouldHaveOneMore prf f (Yes holds rest) = f rest
    shouldHaveOneMore prf f (No nope rest) = nope prf

    wrongOccurs : (Occurs type p       xs  cy -> Void)
               -> (p x -> Void)
               ->  Occurs type p (x :: xs) cy -> Void
    wrongOccurs f g (Yes holds rest) = g holds
    wrongOccurs f g (No nope rest) = f rest

    namespace Exactly
      export
      occurs : {type : Type}
            -> {p    : type -> Type}
            -> (f    : (this : type) -> Dec (p this))
            -> (xs   : List type)
            -> (cy   : Nat)
                    -> DecInfo Occurs.Error
                               (Occurs type p xs cy)
      occurs f [] Z
        = Yes End

      occurs f [] (S k)
        = No (MkError (S k) Z) absurd

      occurs f (x :: xs) cy with (f x)
        occurs f (x :: xs) cy | (Yes prf) with (cy)
          occurs f (x :: xs) cy | (Yes prf) | Z
            = No (MkError Z 1)
                 (\(No f x) => f prf)

          occurs f (x :: xs) cy | (Yes prf) | (S k) with (occurs f xs k)
            occurs f (x :: xs) cy | (Yes prf) | (S k) | (Yes y)
              = Yes (Yes prf y)

            occurs f (x :: xs) cy | (Yes prf) | (S k) | (No msg contra)
              = No (MkError (S k) (S $ found msg))
                   (shouldHaveOneMore prf contra)

        occurs f (x :: xs) cy | (No contra) with (occurs f xs cy)
          occurs f (x :: xs) cy | (No contra) | (Yes prf)
            = Yes (No contra prf)

          occurs f (x :: xs) cy | (No contra) | (No msg g)
            = No (MkError cy (found msg))
                 (wrongOccurs g contra)

  namespace Discover

    namespace Exactly
      export
      occurs : {type : Type}
            -> {p    : type -> Type}
            -> (f    : (this : type) -> Dec (p this))
            -> (xs   : List type)
                    -> DPair Nat (Occurs type p xs)
      occurs f []
        = MkDPair 0 End
      occurs f (x :: xs) with (f x)
        occurs f (x :: xs) | (Yes prf) with (Discover.Exactly.occurs f xs)
          occurs f (x :: xs) | (Yes prf) | (MkDPair fst snd)
            = MkDPair (S fst) (Yes prf snd)
        occurs f (x :: xs) | (No contra) with (Discover.Exactly.occurs f xs)
          occurs f (x :: xs) | (No contra) | (MkDPair fst snd)
            = MkDPair fst (No contra snd)

namespace AtLeast

  public export
  data Occurs : (type : Type)
             -> (p    : type -> Type)
             -> (xs   : List type)
             -> (ym   : Nat)
                     -> Type
    where
      EndY : (holds : p x) -> AtLeast.Occurs type p (x::xs) (S Z)

      Yes : (holds : p x)
         -> (rest  : AtLeast.Occurs type p     xs     cy)
                  -> AtLeast.Occurs type p (x::xs) (S cy)

      No : (nope : Not (p x))
        -> (rest : AtLeast.Occurs type p     xs  (S cy))
                -> AtLeast.Occurs type p (x::xs) (S cy)

  export
  Uninhabited (AtLeast.Occurs type p Nil (S x)) where
    uninhabited (EndY holds) impossible
    uninhabited (Yes holds rest) impossible
    uninhabited (No nope rest) impossible

  export
  Uninhabited (AtLeast.Occurs type p xs Z) where
    uninhabited (EndY holds) impossible
    uninhabited (Yes holds rest) impossible
    uninhabited (No nope rest) impossible

  namespace Check

    namespace AtLeast

      shouldBeAtLeastOne : (AtLeast.Occurs type p       xs 1 -> Void)
                        -> (p x -> Void)
                        ->  AtLeast.Occurs type p (x :: xs) 1 -> Void
      shouldBeAtLeastOne f g (EndY holds) = g holds
      shouldBeAtLeastOne f g (Yes holds rest) = g holds
      shouldBeAtLeastOne f g (No nope rest) = f rest

      shouldBeAtLeastOneMore : (AtLeast.Occurs type p    xs        (S k)  -> Void)
                            -> p x
                            ->  AtLeast.Occurs type p (x :: xs) (S (S k)) -> Void
      shouldBeAtLeastOneMore f y (Yes holds rest) = f rest
      shouldBeAtLeastOneMore f y (No nope rest) = nope y

      shouldBeAtLeastN : (AtLeast.Occurs type p       xs  (S (S k)) -> Void)
                      -> (p x -> Void)
                      ->  AtLeast.Occurs type p (x :: xs) (S (S k)) -> Void
      shouldBeAtLeastN f g (Yes holds rest) = g holds
      shouldBeAtLeastN f g (No nope rest) = f rest

      export
      occurs : {type : Type}
            -> {p    : type -> Type}
            -> (f    : (this : type) -> Dec (p this))
            -> (xs   : List type)
            -> (cy   : Nat)
                    -> DecInfo (Maybe Occurs.Error)
                               (AtLeast.Occurs type p xs cy)
      occurs f xs 0
        = No Nothing absurd

      occurs f [] (S k)
        = No (Just (MkError (S k) Z))
             absurd

      occurs f (x :: xs) (S 0) with (f x)
        occurs f (x :: xs) (S 0) | (Yes prf)
          = Yes (EndY prf)

        occurs f (x :: xs) (S 0) | (No contra) with (AtLeast.occurs f xs (S 0))
          occurs f (x :: xs) (S 0) | (No contra) | (Yes prfWhy)
            = Yes (No contra prfWhy)

          occurs f (x :: xs) (S 0) | (No contra) | (No msgWhyNot prfWhyNot)
            = No (map ({ expected := 1}) msgWhyNot)
                 (shouldBeAtLeastOne prfWhyNot contra)

      occurs f (x :: xs) (S (S k)) with (f x)
        occurs f (x :: xs) (S (S k)) | (Yes prf) with (AtLeast.occurs f xs (S k))
          occurs f (x :: xs) (S (S k)) | (Yes prf) | (Yes prfWhy)
            = Yes (Yes prf prfWhy)

          occurs f (x :: xs) (S (S k)) | (Yes prf) | (No msgWhyNot prfWhyNot)
            = No (map ({ expected := S (S k), found $= S}) msgWhyNot)
                 (shouldBeAtLeastOneMore prfWhyNot prf)

        occurs f (x :: xs) (S (S k)) | (No contra) with (AtLeast.occurs f xs (S (S k)))
          occurs f (x :: xs) (S (S k)) | (No contra) | (Yes prfWhy)
            = Yes (No contra prfWhy)

          occurs f (x :: xs) (S (S k)) | (No contra) | (No msgWhyNot prfWhyNot)
            = No (map ({ expected := S (S k)}) msgWhyNot)
                 (shouldBeAtLeastN prfWhyNot contra)

-- [ EOF ]

ext: idr

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
> module Ordering.Properties

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

> |||
> Uninhabited (LT = EQ) where
>   uninhabited Refl impossible

> |||
> Uninhabited (Prelude.Interfaces.LT = GT) where
>   uninhabited Refl impossible

> |||
> Uninhabited (EQ = GT) where
>   uninhabited Refl impossible

> |||
> Uninhabited (EQ = LT) where
>   uninhabited Refl impossible

> |||
> Uninhabited (Prelude.Interfaces.GT = LT) where
>   uninhabited Refl impossible

> |||
> Uninhabited (GT = EQ) where
>   uninhabited Refl impossible

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module GenericZipWith

import Data.Vect

Id : Type -> Type
Id x = x

Func : (args : Vect n Type) -> (ret : Type) -> (Type -> Type) -> Type
Func [] r f = f r
Func (x :: xs) r f = (a : f x) -> Func xs r f

gApp : Applicative f => f (Func v r Id) -> Func v r f
gApp {v = []} fs = fs
gApp {v = (x :: xs)} fs = \vs => gApp (fs <*> vs)

gZipWith : Applicative f => Func v r Id -> Func v r f
gZipWith {f} f' = gApp {f = f} (pure f')

zipWith' : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
zipWith' f = gZipWith {v = [a, b]} f

zipWith3' : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
zipWith3' f = gZipWith {v = [a, b, c]} f

map' : (a -> b) -> Vect n a -> Vect n b
map' f = gZipWith {v = [a]} f

repeat' : b -> Vect n b
repeat' b = gZipWith {v = []} b

example : Vect 2 (Int, Bool)
example = zipWith' (\i, b => (i, b)) [1, 2] [True, False]

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
data BNat = BZ | O BNat | E BNat

data BLT : BNat -> BNat -> Type where
  BLT_ZO : BLT BZ (O bn)
  BLT_ZE : BLT BZ (E bn)
  BLT_OO : BLT bn bm -> BLT (O bn) (O bm)
  BLT_OE : BLT bn bm -> BLT (O bn) (E bm)
  BLT_OE_Eq : BLT (O bn) (E bn)
  BLT_EO : BLT bn bm -> BLT (E bn) (O bm)
  BLT_EE : BLT bn bm -> BLT (E bn) (E bm)

notLtz : BLT bn BZ -> Void
notLtz x = ?notLtz_rhs


text:
module Minecraft.Data.Serialize

import public Language.JSON

%default total

public export
interface Serialize a where
  identifier : String
  serialize : a -> JSON

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Inigo.Package.CodeGen

import Data.List.Elem
import Extra.List

-- TODO: When we support external backends use idris2's `CG` for this.
public export
data CodeGen : Type where
  Chez : CodeGen
  ChezSep : CodeGen
  Racket : CodeGen
  Gambit : CodeGen
  Node : CodeGen
  Javascript : CodeGen
  RefC : CodeGen

export
toString : CodeGen -> String
toString Chez = "chez"
toString ChezSep = "chez-sep"
toString Racket = "racket"
toString Gambit = "gambit"
toString Node = "node"
toString Javascript = "javascript"
toString RefC = "refc"

export
getCodeGen : String -> Maybe CodeGen
getCodeGen "chez" = Just Chez
getCodeGen "chez-sep" = Just ChezSep
getCodeGen "racket" = Just Racket
getCodeGen "gambit" = Just Gambit
getCodeGen "node" = Just Node
getCodeGen "javascript" = Just Javascript
getCodeGen "refc" = Just RefC
getCodeGen _ = Nothing

export
cmdArgs : CodeGen -> String -> (String, List String)
cmdArgs Node target = ("node", [target])
cmdArgs Javascript target = ("node", [target])
cmdArgs _ target = (target, [])

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
%default total

--------------------------------------------------------
-- Shrunk

data D : List (List a) -> Type where
  C1 : D [ts]
  C2 : D [ts]

f : D [[Maybe a]] -> Nat
f C1 = 0
f C2 = 0

--------------------------------------------------------
-- Original bug report

data NP : (ts : List Type) -> Type where
  Nil  : NP []
  (::) : (v : t) -> (vs : NP ts) -> NP (t :: ts)

data NS : (kss : List $ List Type) -> Type where
  Z : (vs : NP ts) -> NS (ts :: tss)
  S : NS tss -> NS (ts :: tss)

Uninhabited (NS []) where
  uninhabited (Z _) impossible
  uninhabited (S _) impossible

data Funny : (a : Type) -> (f : Type -> Type) -> Type where
  A : List a -> f a -> Funny a f
  B : Funny a f

decode : NS [[List a, f a], []] -> Funny a f
decode (Z [a,b])  = A a b
decode (S (Z [])) = B


text:
data Tag = MkTag

data Elem :  a -> List a ->Type where
  Z : Elem a (a :: as)
  S : Elem a as -> Elem a (b :: as)

toNat : Elem as a -> Nat
toNat Z = 0
toNat (S n) = 1 + toNat n

Show (Elem as a) where
  show = show . toNat

data Subset : List a -> List a -> Type where
  Nil  : Subset [] bs
  (::) : Elem a bs -> Subset as bs -> Subset (a :: as) bs

toList : Subset as bs -> List Nat
toList [] = []
toList (n :: ns) = toNat n :: toList ns

Show (Subset as bs) where
  show = show . toList

search : {auto prf : a} -> a
search = prf

test : String
test =
  let x : Tag := MkTag
      y : Tag := MkTag

      as : List Tag
      as = [y,x]

      bs : List Tag
      bs = [x,y,y]

      prf : Subset as bs
      prf = search

      prf' : Subset as bs := search

      eq : prf === [S (S Z), Z] := Refl

--      eq' : prf' === [S (S Z), Z] := Refl
-- ^ does not work because  prf' is opaque

  in show prf

reverse : List a -> List a
reverse xs =
  let revOnto : List a -> List a -> List a
      revOnto acc [] = acc
      revOnto acc (x :: xs) = revOnto (x :: acc) xs

      rev := revOnto []

      result := rev xs

  in result


text:
module Network

import Data.Vect

TensorDim : Nat -> Type
TensorDim n = Vect n Nat

data Layer : TensorDim i -> TensorDim o -> Type where
  Dense : Layer [i] [o]
  Flatten : Layer i [foldr (*) 1 i]
  Relu : Layer i i
  Sigmoid : Layer i i
  Softmax : Layer i i

data Network : TensorDim i -> Vect n (k : Nat ** TensorDim k) -> TensorDim o -> Type where
  Out : Layer i o -> Network i [] o
  (::) : {h : (k : Nat ** TensorDim k)} -> Layer i (snd h) -> Network (snd h) hs o -> Network i (h :: hs) o

mnist : Network [28, 28, 1] [(1 ** [784]), (1 ** [42]), (1 ** [42]), (1 ** [10])] [10]
mnist = Flatten ::
        Dense ::
        Relu ::
        Dense ::
        Out Sigmoid


text:
data Foo = A | B | C

Eq Foo where
   A == A = True
   B == B = True
   C == C = True
   _ == _ = False

interface Read a where
  readPrefix : String -> Maybe (a, String)

  read : String -> Maybe a
  read str = case readPrefix str of
    Just (a, "") => pure a
    Nothing => Nothing

Read Foo where

  read "A" = A
  read "B" = B
  read "C" = C


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

invert : Bool- > Bool
invert False = True
invert True = False

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


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

import Data.DList
import GRL.Lang.GLang

import Edda
import Edda.Reader.Org

import XML.DOM
import XML.Reader
import XML.XPath

import Freyja

import public Freyja.Error

import Freyja.Fetch
import Freyja.Utils

import Debug.Trace

%access private
-- ---------------------------------------------------------------- [ MetaData ]

metadata : XMLDoc -> Extract Metadata
metadata doc = do
  as    <- getEddaStrings doc ("/pattern/metadata/aliases/alias")
  ts    <- getEddaStrings doc ("/pattern/metadata/tags/tag")
  auths <- getEddaStrings doc ("/pattern/metadata/authors/author")
  es    <- getEddaStrings doc ("/pattern/metadata/auditors/auditor")
  c     <- getTextNode  doc ("/pattern/metadata/created")
  m     <- getTextNode  doc ("/pattern/metadata/modified")
  e     <- getTextNode  doc ("/pattern/metadata/evaluated")
  t     <- getNamedAttr doc "id" ("/pattern")

  pure $ MkMData as ts auths es c m e t

-- ------------------------------------------------------------ [ Requirements ]

requirement : (ty : RTy) -> XMLNode -> Extract (DPair RTy Requirement)
requirement ty (Node e@(Element _ _ _)) = do
  n <- getEddaString e "name"
  d <- getEddaBlock  e "description"
  pure $ (ty ** MkReq ty n d)
requirement _ _ = Left $ GeneralError "error"

requirements : XMLDoc -> Extract (ts ** DList RTy Requirement ts)
requirements doc = do
  fs <- getNodes doc "/pattern/problem/requirements/functional"
  us <- getNodes doc "/pattern/problem/requirements/usability"
  rs <- getNodes doc "/pattern/problem/requirements/reliability"
  ps <- getNodes doc "/pattern/problem/requirements/performance"
  ss <- getNodes doc "/pattern/problem/requirements/supportability"

  fs' <- mapEither (\x => requirement FUNC x) fs
  us' <- mapEither (\x => requirement USAB x) us
  rs' <- mapEither (\x => requirement RELI x) rs
  ps' <- mapEither (\x => requirement PERF x) ps
  ss' <- mapEither (\x => requirement SUPP x) ss

  let res = fs' ++ us' ++ rs' ++ ps' ++ ss'

  pure $ DList.fromLDP res

-- ----------------------------------------------------------------- [ Problem ]

problem : XMLDoc -> Extract Problem
problem doc = do
  rs <- requirements doc
  n <- getEddaString doc "/pattern/problem/name"
  d <- getEddaBlock  doc "/pattern/problem/description"
  pure $ MkProblem n d (snd rs)

-- ----------------------------------------------------------------- [ Context ]

context : XMLDoc -> Extract Context
context doc = do
  n <- getEddaString doc "/pattern/context/name"
  d <- getEddaBlock  doc "/pattern/context/description"
  pure $ MkContext n d

-- ----------------------------------------------------------------- [ Affects ]

tryGetReq : XMLElem -> Maybe (DPair RTy Requirement)
tryGetReq x = do
  naam <- getNodeName x
  ty   <- readRTy naam
  case requirement ty (Node x) of
    Left err => Nothing
    Right r  => pure r

getReqByID : String -> List XMLNode -> Extract (DPair RTy Requirement)
getReqByID ival ns =
    case foldl doFind Nothing ns of
      Nothing => Left $ GeneralError ("Requirement not found.")
      Just r  => pure r
  where
    doFind : Maybe (DPair RTy Requirement)
          -> XMLNode
          -> Maybe (DPair RTy Requirement)
    doFind res (Node e@(Element _ _ _)) =
      case getAttribute "id" e of
        Nothing => res
        Just y  =>
          if ival == y
            then tryGetReq e
            else res
    doFind res _ = res

affect : XMLDoc -> XMLNode -> Extract Affect
affect doc n@(Node e@(Element _ _ _)) = do
  c <- getNamedAttr e "cvalue" "//affect"
  l <- getNamedAttr e "id" "//affect"
  rs <- getNodes doc "/pattern/problem/requirements/*"
  (_ ** r)  <- getReqByID l rs

  let d = case getEddaBlock e "//affect" of
            Left err  => Nothing
            Right res => Just res
  pure $ MkAffect (cast c) r d
affect _ _ = Left $ GeneralError "error"

-- ------------------------------------------------------------------ [ Traits ]

trait : XMLDoc -> TTy -> XMLNode -> Extract (DPair TTy Trait)
trait doc ty (Node e@(Element _ _ _)) = do
  n   <- getEddaString e "//name"
  d   <- getEddaBlock  e "//description"
  s   <- getNamedAttr  e "svalue" (with List concat ["//", cast ty ])
  as  <- getNodes      e "//affects/affect"
  as' <- mapEither (\x => affect doc x) as
  pure $ (ty ** MkTrait ty n d (cast s) as')
trait _ _ _ = Left $ GeneralError "error"

-- ---------------------------------------------------------------- [ Property ]

property : XMLDoc -> XMLNode -> Extract Property
property doc (Node e@(Element _ _ _)) = do
  n  <- getEddaString e "/property/name"
  d  <- getEddaBlock  e "/property/description"

  as <- getNodes e "/property/traits/advantage"
  ds <- getNodes e "/property/traits/disadvantage"
  gs <- getNodes e "/property/traits/general"

  as' <- mapEither (\x => trait doc ADV x) as
  ds' <- mapEither (\x => trait doc DIS x) ds
  gs' <- mapEither (\x => trait doc GEN x) gs

  let ts' = as' ++ ds' ++ gs'

  pure $ MkProperty n d (snd $ DList.fromLDP ts')
property _ _ = Left $ GeneralError "error"

properties : XMLDoc -> Extract (List Property)
properties doc = do
  ps  <- getNodes doc "/pattern/solution/properties/property"
  ps' <- mapEither (\p => property doc p) ps
  pure ps'

-- ------------------------------------------------------------------ [ Models ]

model : MTy -> XMLNode -> Extract (DPair MTy Model)
model ty (Node e@(Element _ _ _)) = do
  n <- getEddaString e "//name"
  d <- getEddaBlock  e "//description"
  m <- getCDataNode  e "//model"

  pure $ (ty ** MkModel n ty d m)
model _ _ = Left $ GeneralError "error"

models : XMLDoc -> Extract (ms ** DList MTy Model ms)
models doc = do
  ss <- getNodes doc "/pattern/solution/models/structure"
  ds <- getNodes doc "/pattern/solution/models/dynamic"

  ss' <- mapEither (\x => model STRUCT x) ss
  ds' <- mapEither (\x => model DYN x)    ds

  let res = ss' ++ ds'

  pure $ DList.fromLDP res

-- ---------------------------------------------------------------- [ Solution ]

solution : XMLDoc -> Extract Solution
solution doc = do
  n <- getEddaString doc "/pattern/solution/name"
  d <- getEddaBlock  doc "/pattern/solution/description"

  ms <- models doc
  ps <- properties doc

  pure $ MkSolution n d (snd ms) ps

-- ----------------------------------------------------------------- [ Studies ]

study : XMLNode -> Extract Study
study (Node e@(Element _ _ _)) = do
  n <- getEddaString e "/study/name"
  b <- getEddaBlock e "/study/before"
  a <- getEddaBlock e "/study/after"
  pure $ MkStudy n b a
study _ = Left $ GeneralError "Error"

studies : XMLDoc -> Extract (List Study)
studies doc = do
  ss <- getNodes doc "/pattern/studies/study"
  ss' <- mapEither study ss
  pure $ ss'

-- --------------------------------------------------------------- [ Relations ]

getMaybeDesc : XMLElem -> Maybe EddaBody
getMaybeDesc n = do
    naam <- getNodeName n
    case getEddaBlock n naam of
        Left  err => Nothing
        Right res => Just res

relation : XMLNode -> Extract (DPair LTy Relation)
relation (Node e@(Element _ _ _)) = do
    ty <- extractTy e
    f <- getNamedAttr e "patternID" (with List concat ["//", cast ty ])
    let d = getMaybeDesc e
    pure $ (ty ** MkRelation ty f d)
  where
    getTy : XMLElem -> Maybe LTy
    getTy x = do
        naam <- getNodeName x
        ty   <- readLTy naam
        pure ty
    extractTy : XMLElem -> Extract LTy
    extractTy x =
      case getTy x of
        Nothing => Left $ GeneralError "Error"
        Just n  => pure $ n

relation _ = Left $ GeneralError "Error"

relations : XMLDoc -> Extract (ls ** DList LTy Relation ls)
relations doc = do
    ls <- getNodes doc "/pattern/relations/*"
    ls' <- mapEither relation ls
    pure $ DList.fromLDP ls'

-- ---------------------------------------------------------------- [ Document ]
export
document : XMLDoc -> Extract PatternDoc
document doc = do
  n <- getEddaString doc "/pattern/name"
  d <- getEddaBlock  doc "/pattern/description"
  e <- getEddaBlock  doc "/pattern/evidence"
  m <- metadata doc
  c <- context  doc
  p <- problem  doc
  s <- solution doc
  ss <- studies doc
  rs <- relations doc
  pure $ MkPDoc n d m c p s e ss (snd rs)

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
not : (arg1 : Bool) -> {auto arg2 : Bool}
not = ?a


text:
import Libraries.Utils.Term

main : IO ()
main = do
  setupTerm
  putStrLn $ "cols:  " ++ show !(getTermCols)
  putStrLn $ "lines: " ++ show !(getTermLines)

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Text.Show.PrettyVal

import Data.List
import Data.List1
import Data.Vect
import Text.Show.Value
import Text.Lexer

import Generics.Derive
import System.Clock
import System.File

%language ElabReflection

public export total
PName : Type
PName = Text.Show.Value.Name

||| A class for types that may be reified into a value.
||| Instances of this class may be derived automatically,
||| for datatypes that support `Generics`.
public export
interface PrettyVal a where
  constructor MkPrettyVal
  prettyVal : a -> Value

--------------------------------------------------------------------------------
--          Generics
--------------------------------------------------------------------------------

-- Displays an applied constructer in record syntax.
-- This is called, if all arguments have user-defined names.
rec : PName -> NP (K Value) ks -> NP (K String) ks -> Value
rec con vs ns = Rec con (collapseNP $ hliftA2 named vs ns)
  where named : Value -> String -> (PName,Value)
        named v name = (MkName name, v)

-- Displays an applied constructer with unnamed arguments.
other : PName -> NP (K Value) ks -> Value
other con = Con con . collapseNP

-- Displays a single applied constructor
valC : NP (PrettyVal . f) ks => ConInfo ks -> NP f ks -> Value
valC info args =
  let con   = MkName (wrapOperator info.conName)
      names = argNames info
      vals  = hcmap (PrettyVal . f) prettyVal args
      val   = maybe (other con vals) (rec con vals) names
   in case vals of
        []    => Con con []
        [a,b] => if isOperator info.conName
                    then binOp (MkName info.conName) a b
                    else val
        _     => val

prettySOP :  (all : POP (PrettyVal . f) kss)
          => TypeInfo kss -> SOP f kss -> Value
prettySOP {all = MkPOP _} (MkTypeInfo _ _ cons) =
  collapseNS . hcliftA2 (NP $ PrettyVal . f) valC cons . unSOP

||| Generic version of `prettyVal`.
public export total
genPrettyVal : Meta t code => POP PrettyVal code => t -> Value
genPrettyVal = prettySOP (metaFor t) . from

--------------------------------------------------------------------------------
--          Auto Deriving
--------------------------------------------------------------------------------

namespace Derive

  ||| Derives a `PrettyVal` implementation for the given data type
  ||| and visibility.
  export total
  PrettyValVis : Visibility -> DeriveUtil -> InterfaceImpl
  PrettyValVis vis g = MkInterfaceImpl "PrettyVal" vis []
                         `(MkPrettyVal genPrettyVal)
                         (implementationType `(PrettyVal) g)

  ||| Alias for `PrettyValVis Public`.
  export total
  PrettyVal : DeriveUtil -> InterfaceImpl
  PrettyVal = PrettyValVis Public

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

public export
PrettyVal Value where
  prettyVal v = v

public export
PrettyVal () where
  prettyVal _ = Con "()" []

public export
PrettyVal Bits8 where
  prettyVal = Natural . show

public export
PrettyVal Bits16 where
  prettyVal = Natural . show

public export
PrettyVal Bits32 where
  prettyVal = Natural . show

public export
PrettyVal Bits64 where
  prettyVal = Natural . show

public export
PrettyVal Nat where
  prettyVal = Natural . show

mkNum :  (Ord a, Neg a, Num a, Show a)
      => (String -> Value) -> a -> Value
mkNum c x = if x >= 0 then c (show x)
                      else Neg . c . show $ negate x

public export
PrettyVal Int where
  prettyVal = mkNum Natural

public export
PrettyVal Int8 where
  prettyVal = mkNum Natural

public export
PrettyVal Int16 where
  prettyVal = mkNum Natural

public export
PrettyVal Int32 where
  prettyVal = mkNum Natural

public export
PrettyVal Int64 where
  prettyVal = mkNum Natural

public export
PrettyVal Integer where
  prettyVal = mkNum Natural

public export
PrettyVal Double where
  prettyVal = mkNum Dbl

public export
PrettyVal Char where
  prettyVal = Chr . show

public export
PrettyVal String where
  prettyVal = Str

public export
PrettyVal a => PrettyVal (List a) where
  prettyVal = Lst . map prettyVal

public export
PrettyVal a => PrettyVal (Vect n a) where
  prettyVal = Lst . toList . map prettyVal

public export
(PrettyVal a, PrettyVal b) => PrettyVal (a,b) where
  prettyVal (a,b) = case prettyVal b of
                         Tuple v1 v2 vs => Tuple (prettyVal a) v1 (v2 :: vs)
                         val            => Tuple (prettyVal a) val []

public export
NP (PrettyVal . f) ks => PrettyVal (NP_ k f ks) where
  prettyVal np = Lst . collapseNP $ hcmap (PrettyVal . f) prettyVal np

public export
NP (PrettyVal . f) ks => PrettyVal (NS_ k f ks) where
  prettyVal ns = run $ hcmap (PrettyVal . f) prettyVal ns
    where run : NS_ k (K Value) xs -> Value
          run (Z v) = Con "Z" [v]
          run (S x) = Con "S" [run x]

public export
POP (PrettyVal . f) kss => PrettyVal (POP_ k f kss) where
  prettyVal (MkPOP nps) = Con "MkPOP" [prettyVal nps]

public export
POP (PrettyVal . f) kss => PrettyVal (SOP_ k f kss) where
  prettyVal (MkSOP nss) = Con "MkSOP" [prettyVal nss]

%runElab derive "Bool" [PrettyVal]

%runElab derive "Ordering" [PrettyVal]

%runElab derive "Maybe" [PrettyVal]

%runElab derive "Either" [PrettyVal]

%runElab derive "List1" [PrettyVal]

%runElab derive "Prec" [PrettyVal]

-- System

%runElab derive "Mode" [PrettyVal]

%runElab derive "FileError" [PrettyVal]

%runElab derive "FileMode" [PrettyVal]

%runElab derive "Permissions" [PrettyVal]

%runElab derive "ClockType" [PrettyVal]

-- Reflection

%runElab derive "ModuleIdent" [PrettyVal]

%runElab derive "VirtualIdent" [PrettyVal]

%runElab derive "OriginDesc" [PrettyVal]

%runElab derive "FC" [PrettyVal]

%runElab derive "NameType" [PrettyVal]

%runElab derive "Constant" [PrettyVal]

%runElab derive "Namespace" [PrettyVal]

%runElab derive "UserName" [PrettyVal]

%runElab derive "Language.Reflection.TT.Name" [PrettyVal]

%runElab derive "NoMangleDirective" [PrettyVal]

%runElab derive "Count" [PrettyVal]

%runElab derive "PiInfo" [PrettyVal]

%runElab derive "LazyReason" [PrettyVal]

%runElab derive "TotalReq" [PrettyVal]

%runElab derive "Visibility" [PrettyVal]

%runElab derive "BindMode" [PrettyVal]

%runElab derive "UseSide" [PrettyVal]

%runElab derive "DotReason" [PrettyVal]

%runElab derive "DataOpt" [PrettyVal]

%runElab derive "WithFlag" [PrettyVal]

%runElab derive "BuiltinType" [PrettyVal]

%runElab deriveMutual [ ("TTImp",        [PrettyVal])
                      , ("IField",       [PrettyVal])
                      , ("IFieldUpdate", [PrettyVal])
                      , ("AltType",      [PrettyVal])
                      , ("FnOpt",        [PrettyVal])
                      , ("ITy",          [PrettyVal])
                      , ("Data",         [PrettyVal])
                      , ("Record",       [PrettyVal])
                      , ("Clause",       [PrettyVal])
                      , ("Decl",         [PrettyVal])
                      ]

-- Pretty

%runElab derive "ShowToken" [PrettyVal]

%runElab derive "Bounds" [Generic, Meta, PrettyVal]

%runElab derive "WithBounds" [Generic, Meta, PrettyVal]

%runElab derive "Err" [PrettyVal]


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  (<|>) (sleepFor 1.seconds) $
    ignore $ zip {a=Unit} {b=Unit}
      (forever $ do
        printTime offset "proc 1, one"
        printTime offset "proc 1, another")
      (forever $ do
        printTime offset "                     proc 2, one"
        printTime offset "                     proc 2, another")

  printTime offset "end"


text:
module Main

import System

alu : String
alu = "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGATCACCTGAGG\
    \TCAGGAGTTCGAGACCAGCCTGGCCAACATGGTGAAACCCCGTCTCTACTAAAAATACAAAAATTAGCCGGG\
    \CGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGGAGGC\
    \GGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCCAGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"

iub : List (Char, Double)
iub = [('a',0.27),('c',0.12),('g',0.12),('t',0.27),('B',0.02)
      ,('D',0.02),('H',0.02),('K',0.02),('M',0.02),('N',0.02)
      ,('R',0.02),('S',0.02),('V',0.02),('W',0.02),('Y',0.02)]

homosapiens : List (Char, Double)
homosapiens = [('a',0.3029549426680),('c',0.1979883004921)
              ,('g',0.1975473066391),('t',0.3015094502008)]

takeRepeat : Int -> String -> String
takeRepeat n s = if n > m
                 then s ++ takeRepeat (n-m) s
                 else pack $ take (cast n) $ unpack s
  where
    m = cast $ length s

splitAt' : Nat -> String -> (String, String)
splitAt' n s = let s' = unpack s in (pack $ take n s', pack $ drop n s')

writeAlu : String -> String -> IO ()
writeAlu name s0 = putStrLn name *> go s0
  where
    go "" = pure ()
    go s  = let (h,t) = splitAt' 60 s in putStrLn h *> go t

replicate : Int -> Char -> String
replicate 0 c = ""
replicate n c = singleton c <+> replicate (n-1) c

-- scanl : (f : acc -> a -> acc) -> acc -> List a -> List acc
-- scanl f q ls = q :: (case ls of
--                         []    => []
--                         x::xs => scanl f (f q x) xs)

accum : (Char,Double) -> (Char,Double) -> (Char,Double)
accum (_,p) (c,q) = (c,p+q)

make : String -> Int -> List (Char, Double) -> Int -> IO Int
make name n0 tbl seed0 = do
    putStrLn name
    make' n0 0 seed0 ""
  where
    modulus : Int
    modulus = 139968

    fill : List (Char,Double) -> Int -> List String
    fill ((c,p) :: cps) j =
      let k = min modulus (cast (cast modulus * p + 1))
      in replicate (k - j) c :: fill cps k
    fill _ _ = []

    lookupTable : String
    lookupTable = Foldable.concat (fill (scanl accum ('a',0) tbl) 0)

    make' : Int -> Int -> Int -> String -> IO Int
    make' 0 col seed buf = when (col > 0) (putStrLn buf) *> pure seed
    make' n col seed buf = do
      let newseed  = modInt (seed * 3877 + 29573) modulus
      let nextchar = strIndex lookupTable newseed
      let newbuf   = buf <+> singleton nextchar
      if col+1 >= 60
        then putStrLn newbuf *> make' (n-1) 0 newseed ""
        else make' (n-1) (col+1) newseed newbuf

main : IO ()
main = do
    (_ :: n :: _) <- getArgs
    writeAlu ">ONE Homo sapiens alu" (takeRepeat (fromInteger (cast n)*2) alu)
    nseed <- make ">TWO IUB ambiguity codes" (fromInteger (cast n)*3) iub 42
    make ">THREE Homo sapiens frequency" (fromInteger (cast n)*5) homosapiens nseed
    pure ()

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
AdderType: (numargs: Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next: numType) -> AdderType k numType

adder: Num numType => (numargs: Nat) -> numType -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)
----------------------------------------------------------------------------
data Format = Number Format
            | Str Format
            | Character Format
            | FNumber Format
            | Lit String Format
            | End
----------------------------------------------------------------------------
PrintfType: Format -> Type
PrintfType (Number fmt) = (i: Int) -> PrintfType fmt
PrintfType (Str fmt) = (str: String) -> PrintfType fmt
PrintfType (Character fmt) = (str: Char) -> PrintfType fmt
PrintfType (FNumber fmt) = (str: Double) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String
----------------------------------------------------------------------------
printfFmt: (fmt: Format) -> (acc: String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Character fmt) acc = \char => printfFmt fmt (acc ++ show char)
printfFmt (FNumber fmt) acc = \fnum => printfFmt fmt (acc ++ show fnum)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc
----------------------------------------------------------------------------
toFormat: (xs: List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Character (toFormat chars)
toFormat ('%' :: 'f' :: chars) = FNumber (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
  Lit lit fmt => Lit (strCons c lit) fmt
  fmt => Lit (strCons c "") fmt
----------------------------------------------------------------------------
printf: (fmt: String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""
----------------------------------------------------------------------------
TupleVect: (len: Nat) -> (elemType: Type) -> Type
TupleVect Z elemType = ()
TupleVect (S k) elemType = (elemType, TupleVect k elemType)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module NDArray

public export
data NDArray a = ?hole


text:
> module Identity.Properties

> import Control.Monad.Identity

> import Identity.Operations
> import Sigma.Sigma
> import Decidable.Predicates
> import Unique.Predicates
> import Finite.Predicates
> import Unit.Properties

> %default total

> %access public export

> ||| Id is injective
> injectiveId : {a : Type} -> {left : a} -> {right : a} -> (Id left) = (Id right) -> left = right
> injectiveId Refl = Refl
> %freeze injectiveId -- frozen

* |Identity| is a functor:

> -- functorSpec1 : fmap . id = id

> -- functorSpec2 : fmap (f . g) = (fmap f) . (fmap g)

* |Identity| is a monad:

> -- monadSpec1 : (fmap f) . ret = ret . f

> -- monadSpec21 : bind (ret a) f = f a

> -- monadSpec22 : bind ma ret = ma

> -- monadSpec23 : {A, B, C : Type} -> {f : A -> M B} -> {g : B -> M C} ->
> --                bind (bind ma f) g = bind ma (\ a => bind (f a) g)

* |Identity| is a container monad:

> |||
> elemNonEmptySpec0 : {A : Type} ->
>                     (a : A) -> (ia : Identity A) ->
>                     a `Elem` ia -> NonEmpty ia
> elemNonEmptySpec0 a (Id a) Refl = ()

> |||
> elemNonEmptySpec1 : {A : Type} ->
>                     (ia : Identity A) ->
>                     NonEmpty ia ->
>                     Sigma A (\ a => a `Elem` ia)
> elemNonEmptySpec1 (Id a) _ = (MkSigma a Refl)

> |||
> containerMonadSpec1 : {A : Type} -> {a : A} -> a `Elem` (ret a)
> containerMonadSpec1 {A} {a} = Refl

> -- containerMonadSpec2 : {A : Type} -> (a : A) -> (ma : M A) -> (mma : M (M A)) ->
> --                       a `Elem` ma -> ma `Elem` mma -> a `Elem` (join mma)

> -- containerMonadSpec2 : {A : Type} -> (a : A) -> (ma : M A) -> (mma : M (M A)) ->
> --                       a `Elem` ma -> ma `Elem` mma -> a `Elem` (join mma)

> containerMonadSpec3 : {A : Type} -> {P : A -> Type} ->
>                       (a : A) -> (ia : Identity A) -> All P ia -> a `Elem` ia -> P a
> containerMonadSpec3 {A} {P} a1 (Id a2) pa2 a1eqa2 = replace (sym a1eqa2) pa2

> -- containerMonadSpec4 : {A : Type} -> (ia : Identity A) -> fmap outl (tagElem ia) = ia

> -- containerMonadSpec5 : {A : Type} -> {P : A -> Type} ->
> --                       (ia : Identity A) -> ((a : A) -> a `Elem` ia -> P a) -> All P ia

* Specific container monad properties

> |||
> -- uniqueAllLemma : {A : Type} -> {P : A -> Type} ->
> --                  Unique1 P -> (ia : Identity A) -> Unique (All P ia)

> ||| All is finite
> finiteAll : {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (ia : Identity A) -> Finite (All P ia)
> finiteAll f1P (Id a) = f1P a

> ||| All is decidable
> decidableAll : {A : Type} -> {P : A -> Type} ->
>                (dec : (a : A) -> Dec (P a)) -> (ia : Identity A) -> Dec (All P ia)
> decidableAll dec ia = dec (unwrap ia)

> ||| NotEmpty is finite
> finiteNonEmpty : {A : Type} -> (ia : Identity A) -> Finite (NonEmpty ia)
> finiteNonEmpty _ = finiteUnit

> ||| NonEmpty is decidable
> decidableNonEmpty : {A : Type} -> (ia : Identity A) -> Dec (NonEmpty ia)
> decidableNonEmpty _ = Yes ()

> ||| Values of type |Identity A| are never empty
> nonEmptyLemma : {A : Type} -> (ia : Identity A) -> NonEmpty ia
> nonEmptyLemma (Id a) = elemNonEmptySpec0 a (Id a) Refl

> ||| |Elem| is decidable
> decElem : {A : Type} -> DecEq0 A -> (a : A) -> (ma : Identity A) -> Dec (a `Elem` ma)
> decElem dec a1 (Id a2) with (dec a1 a2)
>   | (Yes prf)   = Yes prf
>   | (No contra) = No contra
> %freeze decElem -- frozen

> ||| |Elem| is unique
> uniqueElem : {A : Type} -> UniqueEq0 A -> (a : A) -> (ma : Identity A) -> Unique (a `Elem` ma)
> uniqueElem unique a1 (Id a2) p q = unique a1 a2 p q
> %freeze uniqueElem -- frozen

> {-

These properties are already defined in base/Control/Monad/Identity.idr

> using (A : Type)
>   implementation (Eq A) => Eq (Identity A) where
>     (Id a) == (Id b) = a == b

> using (A : Type)
>   implementation (Show A) => Show (Identity A) where
>     show (Id a) = show a

> ---}


text:
TupleVect : (n : Nat) -> Type -> Type
TupleVect 0 _ = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

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


text:
module TestLib

import Postgres
import System
import Data.String
import Data.String.Extra
import Data.List
import Data.List1

export
databaseUrl : HasIO io => io (Maybe String)
databaseUrl = getEnv "TEST_DATABASE_URL"

||| Strip the database name off the end of the database URL
||| and append the test database.
testDatabaseUrl : String -> String
testDatabaseUrl url =
  let splitUrl = split (== '/') url
      allButDatabase = init splitUrl
  in
      join "/" $ (allButDatabase `snoc` "pg_idris_test")

public export
record Config where
  constructor MkConfig
  databaseUrl : String

export
getTestConfig : HasIO io => io (Either String Config)
getTestConfig = do
  Just url <- databaseUrl
    | Nothing => pure $ Left "Missing TEST_DATABASE_URL environment variable needed for testing."
  pure $ Right $ MkConfig url

export
dbSetup : Database () Open (const Open)
dbSetup = do
  liftIO' $ putStrLn "Setting database up"
  res1 <- exec $ perform "drop database if exists pg_idris_test"
  liftIO' . putStrLn $ show res1
  res2 <- exec $ perform "create database pg_idris_test"
  liftIO' . putStrLn $ show res2
  liftIO' $ putStrLn "test database created"

export
withTestDB : HasIO io => {default False setup : Bool} -> (run : Database () Open (const Open)) -> io Bool
withTestDB {setup} run = do
  Right config <- getTestConfig
    | Left err => do putStrLn err
                     pure False
  let databaseUrl : String = if setup then config.databaseUrl else testDatabaseUrl config.databaseUrl
  Right () <- withDB databaseUrl run
    | Left err => do putStrLn err
                     pure False
  pure True

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Happle

import Nope

%access public export
%default total

data HappleKeyword
  = LambdaDot
  | Name String
  --| NameLet
  --| TypeDecl

tokenize : String -> HappleKeyword
tokenize "." = LambdaDot
tokenize x = Name x

max_stars_repo_name: PolyglotSymposium/nosh

max_issues_repo_name: PolyglotSymposium/nosh

max_forks_repo_name: PolyglotSymposium/nosh


text:
module Main

import Cairo

flip : (a,b) -> (b,a)
flip (a,b) = (b,a)

%noinline
main : Cairo ()
main = output $ fst (flip (1,2))

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Parser.Rule.Source

import public Parser.Lexer.Source
import public Parser.Support

import Core.Context
import Core.TT
import Core.Metadata
import Data.List1
import Data.String
import Libraries.Data.List.Extra
import Libraries.Data.String.Extra

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default total

public export
Rule : Type -> Type
Rule ty = Grammar SemanticDecorations Token True ty

public export
EmptyRule : Type -> Type
EmptyRule ty = Grammar SemanticDecorations Token False ty

export
eoi : EmptyRule ()
eoi = ignore $ nextIs "Expected end of input" isEOI
  where
    isEOI : Token -> Bool
    isEOI EndInput = True
    isEOI _ = False

export
constant : Rule Constant
constant
    = terminal "Expected constant" $ \case
        CharLit c    =>  Ch <$> getCharLit c
        DoubleLit d  => Just (Db d)
        IntegerLit i => Just (BI i)
        Ident s      => isConstantType (UN $ Basic s) >>=
                             \case WorldType => Nothing
                                   c         => Just c
        _            => Nothing

documentation' : Rule String
documentation' = terminal "Expected documentation comment" $
                          \case
                            DocComment d => Just d
                            _ => Nothing

export
documentation : Rule String
documentation = (unlines . forget) <$> some documentation'

export
intLit : Rule Integer
intLit
    = terminal "Expected integer literal" $
               \case
                 IntegerLit i => Just i
                 _ => Nothing

export
onOffLit : Rule Bool
onOffLit
    = terminal "Expected on or off" $
               \case
                 Ident "on" => Just True
                 Ident "off" => Just False
                 _ => Nothing

export
strLit : Rule String
strLit
    = terminal "Expected string literal" $
               \case
                 StringLit n s => escape n s
                 _ => Nothing

||| String literal split by line wrap (not striped) before escaping the string.
export
strLitLines : Rule (List1 String)
strLitLines
    = terminal "Expected string literal" $
               \case
                 StringLit n s =>
                   traverse (escape n . fastPack)
                            (splitAfter isNL (fastUnpack s))
                 _ => Nothing

export
strBegin : Rule ()
strBegin = terminal "Expected string begin" $
                    \case
                      StringBegin Single => Just ()
                      _ => Nothing

export
multilineBegin : Rule ()
multilineBegin = terminal "Expected multiline string begin" $
                          \case
                            StringBegin Multi => Just ()
                            _ => Nothing

export
strEnd : Rule ()
strEnd = terminal "Expected string end" $
                  \case
                    StringEnd => Just ()
                    _ => Nothing

export
interpBegin : Rule ()
interpBegin = terminal "Expected string interp begin" $
                       \case
                         InterpBegin => Just ()
                         _ => Nothing

export
interpEnd : Rule ()
interpEnd = terminal "Expected string interp end" $
                     \case
                       InterpEnd => Just ()
                       _ => Nothing

export
simpleStr : Rule String
simpleStr = strBegin *> commit *> (option "" strLit) <* strEnd

export
aDotIdent : Rule String
aDotIdent = terminal "Expected dot+identifier" $
                     \case
                       DotIdent s => Just s
                       _ => Nothing

export
postfixProj : Rule Name
postfixProj = UN . Field <$> aDotIdent

export
symbol : String -> Rule ()
symbol req
    = terminal ("Expected '" ++ req ++ "'") $
               \case
                 Symbol s => if s == req then Just () else Nothing
                 _ => Nothing

export
keyword : String -> Rule ()
keyword req
    = terminal ("Expected '" ++ req ++ "'") $
               \case
                 Keyword s => if s == req then Just () else Nothing
                 _ => Nothing

export
exactIdent : String -> Rule ()
exactIdent req
    = terminal ("Expected " ++ req) $
               \case
                 Ident s => if s == req then Just () else Nothing
                 _ => Nothing

export
pragma : String -> Rule ()
pragma n =
  terminal ("Expected pragma " ++ n) $
    \case
      Pragma s =>
        if s == n
          then Just ()
          else Nothing
      _ => Nothing

export
builtinType : Rule BuiltinType
builtinType =
    BuiltinNatural <$ exactIdent "Natural"
    <|> NaturalToInteger <$ exactIdent "NaturalToInteger"
    <|> IntegerToNatural <$ exactIdent "IntegerToNatural"

operatorCandidate : Rule Name
operatorCandidate
    = terminal "Expected operator" $
               \case
                 Symbol s => Just (UN $ Basic s) -- TODO: have an operator construct?
                 _ => Nothing

export
operator : Rule Name
operator
    = terminal "Expected operator" $
               \case
                 Symbol s =>
                   if s `elem` reservedSymbols
                   then Nothing
                   else Just (UN $ Basic s) -- TODO: have an operator construct?
                 _ => Nothing

identPart : Rule String
identPart
    = terminal "Expected name" $
               \case
                 Ident str => Just str
                 _ => Nothing

export
namespacedIdent : Rule (Maybe Namespace, String)
namespacedIdent
    = terminal "Expected namespaced name" $
               \case
                 DotSepIdent ns n => Just (Just ns, n)
                 Ident i => Just (Nothing, i)
                 _ => Nothing

isCapitalisedIdent : WithBounds String -> EmptyRule ()
isCapitalisedIdent str =
  let val = str.val
      loc = str.bounds
      err : EmptyRule ()
          = failLoc loc ("Expected a capitalised identifier, got: " ++ val)
  in case strM val of
       StrNil => err
       StrCons c _ => if (isUpper c || c > chr 160) then pure () else err

export
namespaceId : Rule Namespace
namespaceId = do
  nsid <- bounds namespacedIdent
  isCapitalisedIdent (snd <$> nsid)
  pure (uncurry mkNestedNamespace nsid.val)

export
moduleIdent : Rule ModuleIdent
moduleIdent = nsAsModuleIdent <$> namespaceId

export
unqualifiedName : Rule String
unqualifiedName = identPart

export
holeName : Rule String
holeName
    = terminal "Expected hole name" $
               \case
                 HoleIdent str => Just str
                 _ => Nothing

reservedNames : List String
reservedNames
    = [ "Type", "Int", "Int8", "Int16", "Int32", "Int64", "Integer"
      , "Bits8", "Bits16", "Bits32", "Bits64"
      , "String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"
      ]

isNotReservedName : WithBounds String -> EmptyRule ()
isNotReservedName x
    = if x.val `elem` reservedNames
      then failLoc x.bounds $ "Can't use reserved name \{x.val}"
      else pure ()

isNotReservedSymbol : WithBounds String -> EmptyRule ()
isNotReservedSymbol x
    = if x.val `elem` reservedSymbols
      then failLoc x.bounds $ "Can't use reserved symbol \{x.val}"
      else pure ()

export
opNonNS : Rule Name
opNonNS = do
  symbol "("
  commit
  id <- bounds (operatorCandidate <|> postfixProj)
  isNotReservedSymbol (nameRoot <$> id)
  symbol ")"
  pure id.val

identWithCapital : (capitalised : Bool) -> WithBounds String ->
                   EmptyRule ()
identWithCapital b x = if b then isCapitalisedIdent x else pure ()

nameWithCapital : (capitalised : Bool) -> Rule Name
nameWithCapital b = opNonNS <|> do
  nsx <- bounds namespacedIdent
  opNS nsx <|> nameNS nsx
 where

  nameNS : WithBounds (Maybe Namespace, String) -> EmptyRule Name
  nameNS nsx = do
    let id = snd <$> nsx
    identWithCapital b id
    isNotReservedName id
    pure $ uncurry mkNamespacedName (map Basic nsx.val)

  opNS : WithBounds (Maybe Namespace, String) -> Rule Name
  opNS nsx = do
    isCapitalisedIdent (snd <$> nsx)
    let ns = uncurry mkNestedNamespace nsx.val
    symbol ".("
    n <- (operator <|> postfixProj)
    symbol ")"
    pure (NS ns n)

export
name : Rule Name
name = nameWithCapital False

export
capitalisedName : Rule Name
capitalisedName = nameWithCapital True

export
capitalisedIdent : Rule String
capitalisedIdent = do
  id <- bounds identPart
  isCapitalisedIdent id
  isNotReservedName id
  pure id.val

export
dataConstructorName : Rule Name
dataConstructorName = opNonNS <|> (UN . Basic) <$> capitalisedIdent

export %inline
dataTypeName : Rule Name
dataTypeName = opNonNS <|> capitalisedName

export
IndentInfo : Type
IndentInfo = Int

export
init : IndentInfo
init = 0

continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
continueF err indent
    = do eoi; err
  <|> do keyword "where"; err
  <|> do col <- column
         when (col <= indent)
            err

||| Fail if this is the end of a block entry or end of file
export
continue : (indent : IndentInfo) -> EmptyRule ()
continue = continueF (fail "Unexpected end of expression")

||| As 'continue' but failing is fatal (i.e. entire parse fails)
export
mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
mustContinue indent Nothing
   = continueF (fatalError "Unexpected end of expression") indent
mustContinue indent (Just req)
   = continueF (fatalError ("Expected '" ++ req ++ "'")) indent

data ValidIndent =
  |||  In {}, entries can begin in any column
  AnyIndent |
  ||| Entry must begin in a specific column
  AtPos Int |
  ||| Entry can begin in this column or later
  AfterPos Int |
  ||| Block is finished
  EndOfBlock

Show ValidIndent where
  show AnyIndent = "[any]"
  show (AtPos i) = "[col " ++ show i ++ "]"
  show (AfterPos i) = "[after " ++ show i ++ "]"
  show EndOfBlock = "[EOB]"

checkValid : ValidIndent -> Int -> EmptyRule ()
checkValid AnyIndent c = pure ()
checkValid (AtPos x) c = if c == x
                            then pure ()
                            else fail "Invalid indentation"
checkValid (AfterPos x) c = if c >= x
                               then pure ()
                               else fail "Invalid indentation"
checkValid EndOfBlock c = fail "End of block"

||| Any token which indicates the end of a statement/block/expression
isTerminator : Token -> Bool
isTerminator (Symbol ",") = True
isTerminator (Symbol "]") = True
isTerminator (Symbol ";") = True
isTerminator (Symbol "}") = True
isTerminator (Symbol ")") = True
isTerminator (Symbol "|") = True
isTerminator (Symbol "**") = True
isTerminator (Keyword "in") = True
isTerminator (Keyword "then") = True
isTerminator (Keyword "else") = True
isTerminator (Keyword "where") = True
isTerminator InterpEnd = True
isTerminator EndInput = True
isTerminator _ = False

||| Check we're at the end of a block entry, given the start column
||| of the block.
||| It's the end if we have a terminating token, or the next token starts
||| in or before indent. Works by looking ahead but not consuming.
export
atEnd : (indent : IndentInfo) -> EmptyRule ()
atEnd indent
    = eoi
  <|> do ignore $ nextIs "Expected end of block" isTerminator
  <|> do col <- column
         when (not (col <= indent))
            $ fail "Not the end of a block entry"

-- Check we're at the end, but only by looking at indentation
export
atEndIndent : (indent : IndentInfo) -> EmptyRule ()
atEndIndent indent
    = eoi
  <|> do col <- column
         when (not (col <= indent))
            $ fail "Not the end of a block entry"

-- Parse a terminator, return where the next block entry
-- must start, given where the current block entry started
terminator : ValidIndent -> Int -> EmptyRule ValidIndent
terminator valid laststart
    = do eoi
         pure EndOfBlock
  <|> do symbol ";"
         pure (afterSemi valid)
  <|> do col <- column
         afterDedent valid col
  <|> pure EndOfBlock
 where
   -- Expected indentation for the next token can either be anything (if
   -- we're inside a brace delimited block) or anywhere after the initial
   -- column (if we're inside an indentation delimited block)
   afterSemi : ValidIndent -> ValidIndent
   afterSemi AnyIndent = AnyIndent -- in braces, anything goes
   afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
   afterSemi (AfterPos c) = AfterPos c
   afterSemi EndOfBlock = EndOfBlock

   -- Expected indentation for the next token can either be anything (if
   -- we're inside a brace delimited block) or in exactly the initial column
   -- (if we're inside an indentation delimited block)
   afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
   afterDedent AnyIndent col
       = if col <= laststart
            then pure AnyIndent
            else fail "Not the end of a block entry"
   afterDedent (AfterPos c) col
       = if col <= laststart
            then pure (AtPos c)
            else fail "Not the end of a block entry"
   afterDedent (AtPos c) col
       = if col <= laststart
            then pure (AtPos c)
            else fail "Not the end of a block entry"
   afterDedent EndOfBlock col = pure EndOfBlock

-- Parse an entry in a block
blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
             Rule (ty, ValidIndent)
blockEntry valid rule
    = do col <- column
         checkValid valid col
         p <- rule col
         valid' <- terminator valid col
         pure (p, valid')

blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
               EmptyRule (List ty)
blockEntries valid rule
     = do eoi; pure []
   <|> do res <- blockEntry valid rule
          ts <- blockEntries (snd res) rule
          pure (fst res :: ts)
   <|> pure []

export
block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
block item
    = do symbol "{"
         commit
         ps <- blockEntries AnyIndent item
         symbol "}"
         pure ps
  <|> do col <- column
         blockEntries (AtPos col) item

||| `blockAfter col rule` parses a `rule`-block indented by at
||| least `col` spaces (unless the block is explicitly delimited
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
blockAfter mincol item
    = do symbol "{"
         commit
         ps <- blockEntries AnyIndent item
         symbol "}"
         pure ps
  <|> do col <- column
         ifThenElse (col <= mincol)
            (pure [])
            $ blockEntries (AtPos col) item

export
blockWithOptHeaderAfter :
   (column : Int) ->
   (header : IndentInfo -> Rule hd) ->
   (item : IndentInfo -> Rule ty) ->
   EmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
    = do symbol "{"
         commit
         hidt <- optional $ blockEntry AnyIndent header
         restOfBlock hidt
  <|> do col <- column
         ifThenElse (col <= mincol)
            (pure (Nothing, []))
            $ do hidt <- optional $ blockEntry (AtPos col) header
                 ps <- blockEntries (AtPos col) item
                 pure (map fst hidt, ps)
  where
  restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
  restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
                                   symbol "}"
                                   pure (Just h, ps)
  restOfBlock Nothing = do ps <- blockEntries AnyIndent item
                           symbol "}"
                           pure (Nothing, ps)

export
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List1 ty)
nonEmptyBlock item
    = do symbol "{"
         commit
         res <- blockEntry AnyIndent item
         ps <- blockEntries (snd res) item
         symbol "}"
         pure (fst res ::: ps)
  <|> do col <- column
         res <- blockEntry (AtPos col) item
         ps <- blockEntries (snd res) item
         pure (fst res ::: ps)

||| `nonEmptyBlockAfter col rule` parses a non-empty `rule`-block indented
||| by at least `col` spaces (unless the block is explicitly delimited
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
nonEmptyBlockAfter : Int -> (IndentInfo -> Rule ty) -> Rule (List1 ty)
nonEmptyBlockAfter mincol item
    = do symbol "{"
         commit
         res <- blockEntry AnyIndent item
         ps <- blockEntries (snd res) item
         symbol "}"
         pure (fst res ::: ps)
  <|> do col <- column
         let False = col <= mincol
            | True => fail "Expected an indented non-empty block"
         res <- blockEntry (AtPos col) item
         ps <- blockEntries (snd res) item
         pure (fst res ::: ps)


text:
module Part2.Sez10_2b
import Part2.Sez10_2a_snoc

%default total

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

{-
idris repl:
*Part2/Sez10_2b> isSuffix [7,8,9,10] [1..10]
True : Bool
*Part2/Sez10_2b> isSuffix [7,8,9] [1..10]
False : Bool
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module NewEden.Implementations.Int64

import Prelude

import NewEden.Algebra
import NewEden.NaturalAxioms

{- Int64

   Axioms for assuming that your processor's native Int64 instructions
   behave as natural numbers.

   Unlike GMP, this assumption is absolutely false.

   Int64 will exhibit unnatural behavior when used on large numbers, so
   use at your own risk!

-}

data UInt : Type where
  MkUInt : (a : Int) -> (isNonNegative : a < 0 = False)  -> UInt

instance Show UInt where
  show (MkUInt x _) = show x

UIntplus : UInt -> UInt -> UInt
UIntplus (MkUInt a _) (MkUInt b _) = MkUInt (a + b) (believe_me ())

minus : UInt -> UInt -> UInt
minus (MkUInt a _) (MkUInt b _) = MkUInt (a - b) (believe_me ())

UIntmultiply : UInt -> UInt -> UInt
UIntmultiply (MkUInt a _) (MkUInt b _) = MkUInt (a * b) (believe_me ())

UIntzero : UInt
UIntzero = MkUInt 0 Refl

UIntone : UInt
UIntone = MkUInt 1 Refl

UIntplusAssociative : AssociativeFunction UInt UIntplus
UIntplusAssociative = MkAssociativeFunction UIntplus (\_,_,_ => believe_me ())

UIntplusMonoid : Monoid UInt UIntplus UIntzero
UIntplusMonoid = MkMonoid UIntplusAssociative UIntzero (\_ => believe_me ()) (\_ => believe_me ())

UIntmultiplyAssociative : AssociativeFunction UInt UIntmultiply
UIntmultiplyAssociative = MkAssociativeFunction UIntmultiply (\_,_,_ => believe_me ())

UIntmultiplyMonoid : Monoid UInt UIntmultiply UIntone
UIntmultiplyMonoid = MkMonoid UIntmultiplyAssociative UIntone (\_ => believe_me ()) (\_ => believe_me ())

UIntcompare : (a:UInt) -> (b:UInt) -> Either (a = b) (Either ((c ** ((UIntplus a c = b, (c = UIntzero -> Void))))) (c ** ((UIntplus b c = a, (c = UIntzero -> Void)))))
UIntcompare (MkUInt x xp) (MkUInt y yp) =
  case x == y of
    True => Left (believe_me ())
    _ => case x < y of
           True => Right $ Left ((minus (MkUInt y yp) (MkUInt x xp)) ** (believe_me (), believe_me ()))
           False => Right $ Right ((minus (MkUInt x xp) (MkUInt y yp)) ** (believe_me (), believe_me ()))

Int64 : NaturalProperties UInt
Int64 =
  ProofNaturalProperties
      UIntzero
      UIntone
      (believe_me ())
      UIntplus
      (MkCommutativeFunction UIntplus (believe_me ()))
      UIntplusMonoid
      (MkStrictMonoid UIntplusMonoid (\_,_,_ => believe_me ()))
      (\x => MkMonomorphicFunction (UIntplus x) (\_,_,_ => believe_me ()))
      UIntmultiply
      (MkCommutativeFunction UIntmultiply (believe_me ()))
      UIntmultiplyMonoid
      (MkStrictMonoid UIntmultiplyMonoid (\_,_,_ => believe_me ()))
      (\x => MkMonomorphicFunction (UIntmultiply x) (\_,_,_ => believe_me ()))
      (\_ => believe_me ())
      (\_,_,_ => believe_me ())
      (\_,_,_,_ => believe_me ())
      UIntcompare

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module Main

import Data.Fin
import Effects
import Effect.StdIO
import Graphics.Color
import Graphics.Shape
import Graphics.SDL2.SDL
import Graphics.SDL2.Effect
import Graphics.Cairo.Cairo
import Graphics.Cairo.Effect

Prog : (sdl: Type) -> (cairo: Type) -> (stdio : Type) -> Type
Prog sdl cairo t = { [SDL sdl,      -- the SDL effect
                      CAIRO cairo,  -- Cairo effect
                      STDIO]        -- a std io effect
                     } Eff t

-- Convenient shorthand for initialised SDL
Running : Type -> Type
Running t = Prog SDLCtx () t

draw : Running ()
draw = with Effects do
  renderClear white
  ctx <- getSdlCtx
  getCanvas ctx
  setSourceRGBA (RGBA 128 250 128 255)
  center
  --line (0,0) (100, 100)
  triangle (-100,0) (100, 0) (0,100)
  --polygon $ (Line (-100, 0) (100, 0)) `Append` (0, 100)
  fill
  closeCanvas
  render

process : Maybe Event -> Bool
process (Just (KeyDown KeyEsc)) = False
process (Just (AppQuit))        = False
process _                       = True

emain : Prog () () ()
emain = do putStrLn "Initialising"
           putStrLn "..."
           initialise "SDL2 Test" 800 600
           putStrLn "Initialised"
           eventLoop
           quit
           pure ()
        where
          eventLoop : Running ()
          eventLoop = do draw
                         when (process (!poll)) eventLoop
main : IO ()
main = runInit [(), -- initial state for the SDL2 effect (nothing needs to go in here)
                (),
                ()  -- initial state for the StdIO effect
                ]
       emain

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


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

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

max_stars_repo_name: yurrriq/idris-time

max_issues_repo_name: yurrriq/idris-time

max_forks_repo_name: yurrriq/idris-time


text:
module Sort

Smaller : Nat -> Nat -> Nat
Smaller Z n = Z
Smaller  m Z = Z
Smaller  (S m) (S n) = (S (Smaller m n))

Min : (m: Nat) -> (n: Nat) -> Either (LTE m n) (LTE n m)
Min Z n = Left LTEZero
Min m Z = Right LTEZero
Min (S a) (S b) = case (Min a b) of
                       (Left l) => Left (LTESucc l)
                       (Right r) => Right (LTESucc r)

Insert: (n: Nat) -> List Nat -> List Nat
Insert n [] = [n]
Insert n (x :: xs) = case (Min n x) of
                        (Left l) => ([n] ++ [x]) ++ xs
                        (Right r) => [x] ++ (Insert n xs)

Sort: List Nat -> List Nat
Sort [] = []
Sort (x :: xs) = Insert x (Sort xs)


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import System.Concurrency.Channels

-- check that all functions are total
%default total

data Message = Add Nat Nat

AdderType : Message -> Type
AdderType (Add x y) = Nat

data ListAction : Type where
  Length : List elem -> ListAction
  Append : List elem -> List elem -> ListAction

ListType : ListAction -> Type
ListType (Length xs) = Nat
ListType (Append {elem} xs ys) = List elem

NoRecv : Void -> Type
NoRecv = const Void

data MessagePID : (iface : reqType -> Type) -> Type where
  MkMessage : PID -> MessagePID iface

data ProcState = NoRequest | Sent | Complete

data Process : (iface : reqType -> Type) ->
               Type ->
               (in_state : ProcState) ->
               (out_state : ProcState) ->
               Type where
  Action : IO a -> Process iface a st st
  Pure : a -> Process iface a st st
  (>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) ->
          Process iface b st1 st3
  Spawn : Process service_iface () NoRequest Complete ->
          Process iface (Maybe (MessagePID service_iface)) st st
  Request : MessagePID service_iface ->
            (msg : service_reqType) ->
            Process iface (service_iface msg) st st
  Respond : ((msg : reqType) ->
                Process iface (iface msg) NoRequest NoRequest) ->
            Process iface (Maybe reqType) st Sent
  Loop : Inf (Process iface a NoRequest Complete) ->
         Process iface a Sent Complete

data Fuel = Dry | More (Lazy Fuel)

run : Fuel -> Process iface t in_state out_state -> IO (Maybe t)
run Dry _ = pure Nothing
run fuel (Request {service_iface} (MkMessage pid) msg)
  = do Just chan <- connect pid
       | _ => pure Nothing
       ok <- unsafeSend chan msg
       if ok then do Just x <- unsafeRecv (service_iface msg) chan
                     | Nothing => pure Nothing
                     pure (Just x)
              else pure Nothing
run fuel (Respond {reqType} f)
  = do Just sender <- listen 1
       | Nothing => pure (Just Nothing)
       Just msg <- unsafeRecv reqType sender
       | Nothing => pure (Just Nothing)
       Just res <- run fuel (f msg)
       | Nothing => pure Nothing
       unsafeSend sender res
       pure (Just (Just msg))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                             | Nothing => pure Nothing
                             run fuel (next x)
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                           | Nothing => pure Nothing
                           pure (Just (Just (MkMessage pid)))
run (More fuel) (Loop act) = run fuel act

partial
forever : Fuel
forever = More forever

partial
runProc : Process iface () in_state out_state -> IO ()
runProc proc = do run forever proc
                  pure ()

Service : (iface : reqType -> Type) -> Type -> Type
Service iface a = Process iface a NoRequest Complete

Client : Type -> Type
Client a = Process NoRecv a NoRequest NoRequest

procAdder : Service AdderType ()
procAdder = do Respond (\msg => case msg of
                                  Add x y => Pure (x + y))
               Loop procAdder

procMain : Client ()
procMain = do Just adder_id <- Spawn procAdder
              | Nothing => Action (putStrLn "Spawn failed")
              answer <- Request adder_id (Add 2 3)
              Action (printLn answer)

-- run with:
-- :exec runProc procMain

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Compiler.Jvm.ExtPrim

import Core.Context
import Core.Name

||| Extended primitives for the scheme backend, outside the standard set of primFn
public export
data ExtPrim = JvmStaticMethodCall | JvmInstanceMethodCall
             | NewIORef | ReadIORef | WriteIORef
             | NewArray | ArrayGet | ArraySet
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
             | MakeFuture
             | Unknown Name

export
Show ExtPrim where
  show JvmStaticMethodCall = "JvmStaticMethodCall"
  show JvmInstanceMethodCall = "JvmInstanceMethodCall"
  show NewIORef = "NewIORef"
  show ReadIORef = "ReadIORef"
  show WriteIORef = "WriteIORef"
  show NewArray = "NewArray"
  show ArrayGet = "ArrayGet"
  show ArraySet = "ArraySet"
  show GetField = "GetField"
  show SetField = "SetField"
  show VoidElim = "VoidElim"
  show SysOS = "SysOS"
  show SysCodegen = "SysCodegen"
  show MakeFuture = "MakeFuture"
  show (Unknown n) = "Unknown " ++ show n

||| Match on a user given name to get the scheme primitive
export
toPrim : Name -> ExtPrim
toPrim pn@(NS _ n)
    = cond [(n == UN "prim__jvmStatic", JvmStaticMethodCall),
            (n == UN "prim__jvmInstance", JvmInstanceMethodCall),
            (n == UN "prim__newIORef", NewIORef),
            (n == UN "prim__readIORef", ReadIORef),
            (n == UN "prim__writeIORef", WriteIORef),
            (n == UN "prim__newArray", NewArray),
            (n == UN "prim__arrayGet", ArrayGet),
            (n == UN "prim__arraySet", ArraySet),
            (n == UN "prim__getField", GetField),
            (n == UN "prim__setField", SetField),
            (n == UN "void", VoidElim),
            (n == UN "prim__os", SysOS),
            (n == UN "prim__codegen", SysCodegen),
            (n == UN "prim__makeFuture", MakeFuture)
            ]
           (Unknown pn)
toPrim pn = Unknown pn

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm