text:
module Main

import Control.App
import Control.App.Console

import Test.Unit.Spec
import Foreign.Memory.Alloc
import Foreign.Memory.Storable

%default total

partial
testStorable : {ty:Type} -> (Storable ty, Show ty, Eq ty)
            => Has [PrimIO, Spec, Console] e
            => (title:String) -> (v0:ty) -> (v1:ty)
            -> App e ()
testStorable {ty=ty} title v0 v1 =
  describe ("testStorable (" ++ title ++ ")") $ do
    tests "simple load-store" $ do
      let p = unsafePerformIO $ unsafeAllocateMemory 128
      let _ = unsafePerformIO $ do
        unsafeStore 0 v0 p
        unsafeStore 64 v1 p
      assertEqual v0 $ unsafePerformIO (unsafeLoad 0 p)
      assertEqual v1 $ unsafePerformIO (unsafeLoad 64 p)

      let _ = unsafePerformIO $ do
        unsafeStore 0 v1 p
        unsafeStore 64 v0 p
      assertEqual v1 $ unsafePerformIO (unsafeLoad 0 p)
      assertEqual v0 $ unsafePerformIO (unsafeLoad 64 p)
      let _ = unsafePerformIO $ unsafeFreeMemory p
      pure ()

partial main : IO ()
main = run $ consoleRunSpecSimple $ do
  testStorable{ty=Int} "Int" 0 1

ext: idr


text:
module Quicksort

import Data.Vect

partitionVect :  Ord elem => {n : Nat} -> (elem) -> (Vect n elem) -> (l1 : Nat ** (l2 : Nat ** (n = (l1 + l2), (Vect l1 elem, Vect l2 elem))))
partitionVect pivot [] = (0 ** 0 ** (Refl, [], []))
partitionVect pivot (x :: xs) with (partitionVect pivot xs)
 partitionVect pivot (x :: xs) | (l1 ** l2 ** ( equality, v1, v2)) = if (x <= pivot) then (S (l1) ** l2 ** (cong {f = S} equality, (x :: v1), v2)) else
   (l1 ** S (l2) ** (trans (cong {f = S} equality) (plusSuccRightSucc l1 l2), v1, x :: v2))

nLTESn : (n : Nat) -> LTE n (S n)
nLTESn Z = LTEZero
nLTESn (S k) = LTESucc (nLTESn k)

-- qsort : Ord elem => Vect n elem -> (l1 ** l2 ** (Vect (l1 + l2) elem, (l1 + l2) = n))
data PreOrder : (a : Type) -> (a -> a -> Type)-> Type where
  PreOrd : {rel : a -> a -> Type} -> ((x : a) -> rel x x) -> ((x : a) -> (y : a) -> (z : a) -> rel x y -> rel y z -> rel x z) -> PreOrder a rel

data TotalOrder : (a : Type) -> (a -> a -> Type) -> Type where
  TotOrd : {rel : a -> a -> Type} -> PreOrder a rel -> ((x : a) -> (y : a) -> Either (rel x y) (rel y x)) -> TotalOrder a rel

data ForAll : (elem -> Type) -> List elem -> Type where
  None: ForAll p []
  Append: p x -> ForAll p xs -> ForAll p (x :: xs)

forAllConcat : (xs : List elem) -> (ForAll p xs) -> (ys : List elem) -> (ForAll p ys) -> (ForAll p (xs ++ ys))
forAllConcat [] None ys pfys = pfys
forAllConcat (x :: xs) (Append px pfxs) ys pfys = Append px (forAllConcat xs pfxs ys pfys)

forAllBreak : (xs : List elem) -> (ys : List elem) -> (ForAll p (xs ++ ys)) -> (ForAll p xs, ForAll p ys)
forAllBreak [] ys pf = (None, pf)
forAllBreak (x :: xs) ys (Append px pfxs) = let (faxs, fays) = forAllBreak xs ys pfxs in (Append px faxs, fays)

forAllMap : (p : elem -> Type) -> (q : elem -> Type) -> (f : (x : elem) -> p x -> q x) -> (xs : List elem) -> ForAll p xs -> ForAll q xs
forAllMap p q f [] None = None
forAllMap p q f (x :: xs) (Append px pfxs) = Append (f x px) (forAllMap p q f xs pfxs)

data LTEforList : List elem -> List elem -> Type where
  LTEEmpty : LTEforList [] xs
  LTEAppend : LTEforList xs ys -> LTEforList (x :: xs) (y :: ys)

lemma1 : LTEforList xs ys -> LTEforList xs (y :: ys)
lemma1 LTEEmpty = LTEEmpty
lemma1 (LTEAppend pf) = LTEAppend (lemma1 pf)

lemma2 : (xs : List elem) -> LTEforList xs xs
lemma2 [] = LTEEmpty
lemma2 (x :: xs) = LTEAppend (lemma2 xs)

lemma3 : LTEforList xs ys -> LTEforList ys zs -> LTEforList xs zs
lemma3 LTEEmpty _ = LTEEmpty
lemma3 (LTEAppend pf1) (LTEAppend pf2) = LTEAppend (lemma3 pf1 pf2)

data IsSortedAlternate : (elem -> elem -> Type) -> List elem -> Type where
  EmptySorted : IsSortedAlternate lte []
  AppendSorted : {lte : elem -> elem -> Type} -> ForAll (lte x) xs -> IsSortedAlternate lte xs -> IsSortedAlternate lte (x :: xs)

data Permutation : List elem -> List elem -> Type where
  Empty : Permutation [] []
  Split : (xs : List elem) -> (ys : List elem) -> (zs : List elem) -> Permutation xs (ys ++ zs) -> Permutation (x :: xs) (ys ++ (x :: zs))
  Compos : Permutation xs ys -> Permutation ys zs -> Permutation xs zs
  Cat : Permutation ws ys -> Permutation xs zs -> Permutation (ws ++ xs) (ys ++ zs)

forAllPerm : (xs : List elem) -> ForAll p xs -> (ys : List elem) -> Permutation xs ys -> ForAll p ys
forAllPerm [] None [] Empty = None
forAllPerm (x :: xs) (Append px faxs) (ws ++ (x :: ys)) (Split xs ws ys pfperm) =
  let (faws,fays) = forAllBreak ws ys (forAllPerm xs faxs (ws ++ ys) pfperm) in forAllConcat ws faws (x :: ys) (Append px fays)
forAllPerm xs {p} pfxs zs (Compos {ys} permxsys permyszs) = forAllPerm ys (forAllPerm xs pfxs ys permxsys) zs permyszs
forAllPerm (ws ++ xs) pfwscatxs (ys ++ zs) (Cat pfwsys pfxszs) =
  let (pfws,pfxs) = (forAllBreak ws xs pfwscatxs) in forAllConcat ys (forAllPerm ws pfws ys pfwsys) zs (forAllPerm xs pfxs zs pfxszs)

partitionFunc : {p : elem -> Type} -> {q : elem -> Type} -> (f : (x : elem) -> Either (p x) (q x)) ->
                (xs : List elem) -> (ys : List elem ** (zs : List elem ** (LTEforList ys xs,LTEforList zs xs , ForAll p ys, ForAll q zs, Permutation xs (ys ++ zs))))
partitionFunc f [] = ([] ** ([] ** (LTEEmpty, LTEEmpty, None, None, Empty)))
-- partitionFunc f (x :: xs) =
--   let (ys ** (zs ** (pfmn, pfkn, pfys, pfzs, pfperm))) = partitionFunc f xs in
--   case (f x) of
--     (Left px) => ((x :: ys) ** (zs ** (LTESucc pfmn, lteTransitive pfkn (nLTESn (length xs)), Append px pfys, pfzs, Split [] (ys ++ zs) xs (permAddEmpty pfperm))))


text:
> module SimpleProb.Measures

> import SimpleProb.SimpleProb
> import SimpleProb.BasicOperations
> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties

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

* Measures

> ||| Expected value
> expectedValue : SimpleProb NonNegRational -> NonNegRational
> expectedValue = Prelude.Foldable.sum . (map (uncurry (*))) . toList

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module PQ.SQL.Type

import public Data.List.Elem

public export
data SQLType_ : (canWrap : Bool) -> Type where
  VarChar  : Nat -> SQLType_ canWrap
  Text     : SQLType_ canWrap
  SmallInt : SQLType_ canWrap
  SQLInt   : SQLType_ canWrap
  BigInt   : SQLType_ canWrap
  Boolean  : SQLType_ canWrap
  Array    : {0 canWrap1 : _ } -> SQLType_ canWrap1 -> SQLType_ canWrap
  Nullable : SQLType_ True -> SQLType_ False

public export
SQLType : Type
SQLType = SQLType_ False

public export
0 Repr : SQLType_ canWrap -> Type
Repr (VarChar k)  = String
Repr Text         = String
Repr SmallInt     = Int16
Repr SQLInt       = Int32
Repr BigInt       = Int64
Repr Boolean      = Bool
Repr (Array x)    = List (Repr x)
Repr (Nullable x) = Maybe (Repr x)

public export
record Attribute where
  constructor MkAttribute
  name : String
  type : SQLType

infixl 4 <->

public export %inline
(<->) : String -> SQLType -> Attribute
(<->) = MkAttribute

public export
Row : Type
Row = List Attribute

public export
data IsFieldName : (name : String) -> (row : Row) -> Type where
  Here  : (type : SQLType) -> IsFieldName name (MkAttribute name type :: attrs)
  There : IsFieldName name attrs -> IsFieldName name (attr :: attrs)

0 FieldType : IsFieldName name row -> SQLType
FieldType (Here tpe)  = tpe
FieldType (There fld) = FieldType fld

infixr 5 `And`
infixr 4 `Or`

public export
data Expr : (row : Row) -> SQLType -> Type where
  Null : {0 any : SQLType_ True} -> Expr row (Nullable any)

  Lit : {t : SQLType} -> Repr t -> Expr row t

  Field :  (name : String)
        -> {auto 0 prf : IsFieldName name row}
        -> Expr row (FieldType prf)

  (==) : Expr s t -> Expr s t -> Expr s Boolean
  (/=) : Expr s t -> Expr s t -> Expr s Boolean
  (>)  : Expr s t -> Expr s t -> Expr s Boolean
  (>=) : Expr s t -> Expr s t -> Expr s Boolean
  (<)  : Expr s t -> Expr s t -> Expr s Boolean
  (<=) : Expr s t -> Expr s t -> Expr s Boolean
  And  : Expr s Boolean -> Expr s Boolean -> Expr s Boolean
  Or   : Expr s Boolean -> Expr s Boolean -> Expr s Boolean
  Not  : Expr s Boolean -> Expr s Boolean
  IsNull    : Expr s (Nullable t) -> Expr s Boolean
  IsNotNull : Expr s (Nullable t) -> Expr s Boolean

  PlusSI  : Expr s SmallInt -> Expr s SmallInt -> Expr s SmallInt
  PlusI   : Expr s SQLInt   -> Expr s SQLInt   -> Expr s SQLInt
  PlusBI  : Expr s BigInt   -> Expr s BigInt   -> Expr s BigInt
  TimesSI : Expr s SmallInt -> Expr s SmallInt -> Expr s SmallInt
  TimesI  : Expr s SQLInt   -> Expr s SQLInt   -> Expr s SQLInt
  TimesBI : Expr s BigInt   -> Expr s BigInt   -> Expr s BigInt
  DivSI   : Expr s SmallInt -> Expr s SmallInt -> Expr s SmallInt
  DivI    : Expr s SQLInt   -> Expr s SQLInt   -> Expr s SQLInt
  DivBI   : Expr s BigInt   -> Expr s BigInt   -> Expr s BigInt
  ModSI   : Expr s SmallInt -> Expr s SmallInt -> Expr s SmallInt
  ModI    : Expr s SQLInt   -> Expr s SQLInt   -> Expr s SQLInt
  ModBI   : Expr s BigInt   -> Expr s BigInt   -> Expr s BigInt

--------------------------------------------------------------------------------
--          Expr Interface Implementations
--------------------------------------------------------------------------------

public export
FromString (Expr row Text) where
  fromString = Lit

public export
FromString (Expr row $ Nullable Text) where
  fromString = Lit . Just

public export
Num (Expr row SmallInt) where
  fromInteger = Lit . fromInteger
  (+) = PlusSI
  (*) = TimesSI

public export
Num (Expr row SQLInt) where
  fromInteger = Lit . fromInteger
  (+) = PlusI
  (*) = TimesI

public export
Num (Expr row BigInt) where
  fromInteger = Lit . fromInteger
  (+) = PlusBI
  (*) = TimesBI

--------------------------------------------------------------------------------
--          Queries
--------------------------------------------------------------------------------

public export
record NamedExpr (row : Row) where
  constructor MkNamedExpr
  0 tpe : SQLType
  name  : String
  expr  : Expr row tpe

public export %inline
as : Expr row tpe -> String -> NamedExpr row
as expr name = MkNamedExpr tpe name expr

public export
0 RowType : List (NamedExpr row) -> Row
RowType Nil = Nil
RowType (MkNamedExpr tpe name _ :: t) = MkAttribute name tpe :: RowType t

public export
data RowExpr : (row : Row) -> Type where
  Table : (tableName : String) -> (row : Row) -> RowExpr row
  Select :  (from   : RowExpr row)
         -> (filter : Expr row Boolean)
         -> (select : List (NamedExpr row))
         -> RowExpr (RowType select)

--------------------------------------------------------------------------------
--          Syntax and Tests
--------------------------------------------------------------------------------

Customer : Row
Customer = [ MkAttribute "customer.id" BigInt
           , MkAttribute "customer.name" Text
           , MkAttribute "customer.age" SmallInt
           , MkAttribute "customer.orders" SmallInt
           , MkAttribute "customer.city" Text
           ]

Customers : RowExpr Customer
Customers = Table "customers" Customer

aStringLit : Expr Customer Text
aStringLit = "foo"

aFieldRef : Expr Customer SmallInt
aFieldRef = Field "customer.age"

compExpr : Expr Customer Boolean
compExpr = Field "customer.name" == "foo"                     `And`
           Field "customer.id" >= 12                          `And`
           Field "customer.age" * 2 < Field "customer.orders"

topCustomers : RowExpr [ "name" <-> Text, "city" <-> Text, "age" <-> SmallInt ]
topCustomers = Select {
                 from   = Customers
               , filter = Field "customer.orders" >= 100 `And`
                          Field "customer.age" < 18
               , select = [ Field "customer.name" `as` "name"
                          , Field "customer.city" `as` "city"
                          , Field "customer.age"  `as` "age"
                          ]
               }


text:
module Minecraft.Data.Deserialize

import public Minecraft.Data.Serialize

%default total

public export
interface Serialize a => Deserialize a where
  deserialize : JSON -> Maybe a

public export
deserializeSerialize : Deserialize a -> Serialize a
deserializeSerialize = %search

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
{-
Foreign collections
  - FList   : foreign List
  - FVect   : foreign Vector
  - FHVect  : foreign Heterogeneous Vector

If your language supports some of them, just make sure
the relatedc builtins functions should be implemented in
your language, like
  python: `cam-python/idris_cam/rumtime.py'
  julia:  `cam-julia/src/Runtime.jl`
-}

module FCollections
import Data.Vect
import Data.HVect
import Cam.Data.Collections
import Cam.FFI
import Cam.IO

%access public export
%hide Vect.index
%hide HVect.index

-- maybe overflow
%inline
indexRawOF : String -> Int -> Unsafe -> Unsafe
indexRawOF s i v = let builtin = Builtin s in
                   let i = believe_me i in
                   let box = fcall FFun2 builtin i v in
                   believe_me $ unsafePerformIO box

%inline
indexRaw : String -> Integer -> Unsafe -> Unsafe
indexRaw s i v = let builtin = Builtin s in
                 let i = believe_me i in
                 let box = fcall FFun2 builtin i v in
                 believe_me $ unsafePerformIO box

-- using `nat` data structure to index
%inline
indexRawNat : String -> Nat -> Unsafe -> Unsafe
indexRawNat s i v = let builtin = Builtin s in
                    let i = believe_me i in
                    let box = fcall FFun2 builtin i v in
                    believe_me $ unsafePerformIO box

-- Implementations for FList
%inline
sizeFList : FList a -> Integer
sizeFList lst = assert_total $
    let builtin = Builtin "size_flist" in
    let box = fcall FFun1 builtin (believe_me lst) in
    believe_me $ unsafePerformIO box

implementation Sized (FList t) where
 -- It seems that using `size = sizeFlist` causes bad properties, not sure yet
  size lst = fromInteger $ sizeFList lst

implementation Indexable (FList t) Integer where
  eltype {t} _ _ = Boxed t
  index {t} i xs = believe_me e
    where
      src : Unsafe
      src = believe_me xs
      e : Unsafe
      e = indexRaw "index_flist" i src

reverseFList : FList a -> FList a
reverseFList lst = let builtin = Builtin "reverse_flist" in
                   let box = fcall FFun1 builtin (believe_me lst) in
                   believe_me $ unsafePerformIO box

implementation Reversable (FList a) (FList a) where
  reverse = reverseFList

-- Implementations for FVect

sizeFVect : FVect n a -> Nat
sizeFVect {n} _ = n

implementation StaticSized (FVect n a) where
  typeSize {n} _ = n

implementation Sized (FVect n a) where
  size vec = sizeFVect vec

implementation Indexable (FVect n t) (Fin n) where
  eltype {t} _ _ = Boxed t
  index fin vec = believe_me e
    where
      i : Integer
      i = finToInteger fin
      src : Unsafe
      src = believe_me vec
      e : Unsafe
      e = indexRaw "index_fvect" i src

reverseFVect : FVect n a -> FVect n a
reverseFVect {n} vec = let builtin = Builtin "reverse_fvect" in
                       let box = fcall FFun1 builtin $ believe_me vec in
                       believe_me $ unsafePerformIO box

implementation Reversable (FVect n a) (FVect n a) where
  reverse vec = reverseFVect vec

-- Implementations for FHVect

sizeFHVect : {xs: Vect n Type} -> FHVect xs -> Nat
sizeFHVect {n} _ = n

implementation StaticSized (FHVect xs) where
  typeSize {xs} _ = size xs

implementation Sized (FHVect xs) where
  size vec = sizeFHVect vec

-- It's tricky here for there're still some bugs in Idris.
-- related: https://github.com/idris-lang/Idris-dev/issues/3136

implementation Indexable (FHVect xs) (Fin (size xs)) where
  eltype {xs} fin _ = Boxed (index fin xs)
  index fin vec = believe_me e
    where
      i : Integer
      i = finToInteger fin
      src : Unsafe
      src = believe_me vec
      e : Unsafe
      e = indexRaw "index_fhvect" i src

reverseFHVect : FHVect xs -> FHVect (reverseVect xs)
reverseFHVect {xs} vec = let builtin = Builtin "reverse_fvect" in
                         let box = fcall FFun1 builtin $ believe_me vec in
                         believe_me $ unsafePerformIO box

implementation Reversable (FHVect xs) (FHVect (reverseVect xs)) where
  reverse vec = reverseFHVect vec

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
module FPH

import Data.List
import Data.String

square : Int -> Int
square x = x * x

hword : String -> Bool
hword xs = hwAcc (unpack xs)  where
  hwAcc : List Char -> Bool
  hwAcc Nil       = False
  hwAcc (x :: xs) = (x == 'h') || hwAcc xs

gen : Int -> String
gen 0 = "Sentence go on"
gen n = gen (n-1) ++ " and on"
genS : Int -> String
genS n = gen n ++ "."
genS2 : Int -> String
genS2 n    = genrec n ++ "." where
  genrec : Int -> String
  genrec 0 = "Sentence go on"
  genrec n = genrec (n-1) ++ " and on"

story : Int -> String
story n    = (storec n) where
  storec : Int -> String
  storec 0 = "Let's cook and eat that final missionary, and off to bed."
  storec k = "The night was pitch dark, mysterious and deep.\n"
             ++ "Ten cannibals were seated around a boiling cauldron.\n"
             ++ "Their leader got up and addressed them like this:\n'"
             ++ story (k-1) ++ "'"

reversal : String -> String
reversal xs = reversAcc (unpack xs) "" where
  reversAcc : List Char -> String -> String
  reversAcc Nil       ys = ys
  reversAcc (x :: xs) ys = reversAcc xs (strCons x ys)

sonnet18 : String
sonnet18 =
 "Shall I compare thee to a summer's day? \n"
 ++ "Thou art more lovely and more temperate: \n"
 ++ "Rough winds do shake the darling buds of May, \n"
 ++ "And summer's lease hath all too short a date: \n"
 ++ "Sometime too hot the eye of heaven shines, \n"
 ++ "And often is his gold complexion dimm'd; \n"
 ++ "And every fair from fair sometime declines, \n"
 ++ "By chance or nature's changing course untrimm'd; \n"
 ++ "But thy eternal summer shall not fade \n"
 ++ "Nor lose possession of that fair thou owest; \n"
 ++ "Nor shall Death brag thou wander'st in his shade, \n"
 ++ "When in eternal lines to time thou growest: \n"
 ++ "  So long as men can breathe or eyes can see, \n"
 ++ "  So long lives this and this gives life to thee."

sonnet73 : String
sonnet73 =
 "That time of year thou mayst in me behold\n"
 ++ "When yellow leaves, or none, or few, do hang\n"
 ++ "Upon those boughs which shake against the cold,\n"
 ++ "Bare ruin'd choirs, where late the sweet birds sang.\n"
 ++ "In me thou seest the twilight of such day\n"
 ++ "As after sunset fadeth in the west,\n"
 ++ "Which by and by black night doth take away,\n"
 ++ "Death's second self, that seals up all in rest.\n"
 ++ "In me thou see'st the glowing of such fire\n"
 ++ "That on the ashes of his youth doth lie,\n"
 ++ "As the death-bed whereon it must expire\n"
 ++ "Consumed with that which it was nourish'd by.\n"
 ++ "This thou perceivest, which makes thy love more strong,\n"
 ++ "To love that well which thou must leave ere long."

count : Eq a => a -> List a -> Int
count x []                  = 0
count x (y::ys) = if x == y then 1 + (count x ys)
                  else count x ys

average : List Int -> Maybe Double
average [] = Nothing
average xs = Just (cast (sum xs) / cast (length xs))

prefix' : Eq a => List a -> List a -> Bool
prefix' []      ys      = True
prefix' (x::xs) []      = False
prefix' (x::xs) (y::ys) = (x==y) && prefix' xs ys
{-
prefixString : String -> String -> Bool
prefixString "" _ = True
prefixString _ "" = False
prefixString xstr ystr = (prim__strHead xstr) == (prim__strHead ystr) && prefixString (strTail xstr) (strTail ystr)
-}

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

notElem : Eq a => a -> List a -> Bool
notElem x xs = not (elem x xs)

puncfilter : List Char -> List Char
puncfilter = filter (\x => notElem x ['?', ';', ':', ',', '.'])

preprocess : String -> String
preprocess = pack . map toLower . puncfilter . unpack

process : String -> List String
process = sort . nub . words

cnt : String -> List (String, Int)
cnt sonnet = [ (x,n)| x <- (process . preprocess) sonnet,
                 n <- [count x (words (preprocess sonnet))],
                 n > 1
             ]


text:
module Circuits.NetList.Linear.Usage.Item

import Decidable.Equality

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

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra
import Toolkit.Data.DVect

import Circuits.Common

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage.DataType
import Circuits.NetList.Linear.Usage.DataType.Use.Full
import Circuits.NetList.Linear.Usage.DataType.Use.Partial

import Circuits.NetList.Linear.Usage.TermType
import Circuits.NetList.Linear.Usage.TermType.Use.Port
import Circuits.NetList.Linear.Usage.TermType.Use.Channel

%default total

public export
record Item where
  constructor I
  getType : Ty
  getUsage : Usage getType

public export
data FreePort : (flow : Direction)
             -> (type : DType)
             -> (item : Item)
                      -> Type
  where
    FP : (u : Usage type) -> (prf : IsFree type u) -> FreePort flow type (I (TyPort (flow, type)) (TyPort u))

public export
freePort : (flow : Direction)
        -> (type : DType)
                -> DPair Item (FreePort flow type)
freePort flow type with (init type)
  freePort flow type | (MkDPair u prf)
    = MkDPair (I (TyPort (flow, type)) (TyPort u)) (FP u prf)

public export
data FreeChan : (type : DType) -> (item : Item) -> Type where
  FC : (u : Usage type) -> (prf : IsFree type u) -> FreeChan type (I (TyChan type) (TyChan u u))

public export
freeChan : (type : DType) -> DPair Item (FreeChan type)
freeChan type with (init type)
  freeChan type | (MkDPair u prf)
    = MkDPair (I (TyChan type) (TyChan u u)) (FC u prf)

-- I (TyPort (flow,type)) ?as)

public export
data CanStop : Item -> Type where
  StopG : CanStop (I TyGate TyGate)
  StopU : CanStop (I TyUnit TyUnit)

  StopP : (prf : IsUsed     (TyPort (flow,dtype)) u)
              -> CanStop (I (TyPort (flow,dtype)) u)

  StopC : (prf : IsUsed     (TyChan type) u)
              -> CanStop (I (TyChan type) u)

portIsFree : (IsUsed (TyPort x) u -> Void) -> CanStop (I (TyPort x) u) -> Void
portIsFree f (StopP prf) = f prf

chanOutIsFree : (IsUsed x eout -> Void) -> CanStop (I (TyChan x) (TyChan ein eout)) -> Void
chanOutIsFree f (StopC (UsedC uin uou)) = f uou

chanInIsFree : (IsUsed x ein -> Void) -> CanStop (I (TyChan x) (TyChan ein eout)) -> Void
chanInIsFree f (StopC (UsedC uin uou)) = f uin

export
canStop : (i : Item) -> Dec (CanStop i)
canStop (I TyUnit TyUnit)
  = Yes StopU

canStop (I (TyPort x) u) with (isUsed u)
  canStop (I (TyPort (flow, type)) (TyPort u)) | (Yes (UsedP y))
    = Yes (StopP (UsedP y))

  canStop (I (TyPort x) u) | (No contra)
    = No (portIsFree contra)

canStop (I (TyChan x) (TyChan ein eout)) with (isUsed ein)
  canStop (I (TyChan x) (TyChan ein eout)) | (Yes prfIN) with (isUsed eout)
    canStop (I (TyChan x) (TyChan ein eout)) | (Yes prfIN) | (Yes prfOUT)
      = Yes (StopC (UsedC prfIN prfOUT))

    canStop (I (TyChan x) (TyChan ein eout)) | (Yes prfIN) | (No contra)
      = No (chanOutIsFree contra)

  canStop (I (TyChan x) (TyChan ein eout)) | (No contra)
    = No (chanInIsFree contra)

canStop (I TyGate TyGate)
  = Yes StopG

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Control.Optics.Vect

import Data.Vect
import Control.Optics.Setter
import Control.Optics.Lens

export
at : Fin n -> Simple Lens (Vect n a) a
at i = lens (index i) (\s, b => replaceAt i b s)


text:
module Test.Suite

import IdrTest.Test

import Test.Markdown.Format.HtmlTest
import Test.Markdown.LexerTest
import Test.MarkdownTest

suite : IO ()
suite = do
  runSuites
    [ Test.Markdown.LexerTest.suite
    , Test.MarkdownTest.suite
    , Test.Markdown.Format.HtmlTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Data.Iterable

import Data.List1
import Data.SnocList

import public Control.MonadRec

--------------------------------------------------------------------------------
--          Iterable
--------------------------------------------------------------------------------

refl : {k : Nat} -> LTE k k
refl = reflexive {x = k}

public export
interface Iterable container element | container where
  iterM :  MonadRec m
        => (accum : element -> st -> m st)
        -> (done  : st -> res)
        -> (ini   : st)
        -> (seed  : container)
        -> m res

export
forM_ :  Iterable container element
      => MonadRec m
      => (run  : element -> m ())
      -> (seed : container)
      -> m ()
forM_ run = iterM (\e,_ => run e) (const ()) ()

export
foldM :  Iterable container element
      => MonadRec m
      => Monoid mo
      => (calc : element -> m mo)
      -> (seed : container)
      -> m mo
foldM calc = iterM (\e,acc => (<+> acc) <$> calc e) id neutral

--------------------------------------------------------------------------------
--          Iterable Implementations
--------------------------------------------------------------------------------

export
Iterable Nat Nat where
  iterM accum done ini seed =
    trSized seed ini $
      \case Z       => pure . Done . done
            v@(S k) => map (Cont k refl) . accum v

export
Iterable (List a) a where
  iterM accum done ini seed =
    trSized seed ini $
      \case Nil    => pure . Done . done
            h :: t => map (Cont t refl) . accum h

export
Iterable (List1 a) a where
  iterM accum done ini = iterM accum done ini . forget

export
Iterable Fuel () where
  iterM accum done ini seed =
    trSized seed ini $
      \case Dry    => pure . Done . done
            More f => map (Cont f refl) . accum ()

export
Iterable (SnocList a) a where
  iterM accum done ini seed =
    trSized seed ini $
      \case [<]     => pure . Done . done
            sx :< x => map (Cont sx refl) . accum x


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

Functor InfList where
    map func (value :: xs) = func value :: Delay (map func xs)

%name InfList xs, ys, zs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
-- Based on the code questioned at https://discord.com/channels/827106007712661524/834611018775789568/918166736153501696

a : String -> String -> Elab ()
a fn fd = declare
  `[ %foreign ~(IPrimVal EmptyFC $ Constant $ Str fd)
     ~(IVar EmptyFC $ UN $ Basic fn) : Int -> Int
   ]

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Data.Vect.Quantifiers

import Data.Vect

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

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

||| Eliminator for `Any`
public export
anyElim : {0 xs : Vect n a} -> {0 p : a -> Type} -> (Any p xs -> b) -> (p x -> b) -> Any p (x :: xs) -> b
anyElim _ f (Here p) = f p
anyElim f _ (There p) = f p

||| Given a decision procedure for a property, determine if an element of a
||| vector satisfies it.
|||
||| @ p the property to be satisfied
||| @ dec the decision procedure
||| @ xs the vector to examine
export
any : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n 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 prf =
    case any p xs of
      Yes prf' => Yes (There prf')
      No prf' => No (anyElim prf' prf)

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

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

export
notAllHere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (p x) -> All p (x :: xs) -> Void
notAllHere _ Nil impossible
notAllHere np (p :: _) = np p

export
notAllThere : {0 p : a -> Type} -> {xs : Vect n a} -> Not (All p xs) -> All p (x :: xs) -> Void
notAllThere _ Nil impossible
notAllThere np (_ :: ps) = np ps

||| Given a decision procedure for a property, decide whether all elements of
||| a vector satisfy it.
|||
||| @ p the property
||| @ dec the decision procedure
||| @ xs the vector to examine
export
all : (dec : (x : a) -> Dec (p x)) -> (xs : Vect n a) -> Dec (All p xs)
all _ Nil = Yes Nil
all d (x::xs) with (d x)
  all d (x::xs) | No prf = No (notAllHere prf)
  all d (x::xs) | Yes prf =
    case all d xs of
      Yes prf' => Yes (prf :: prf')
      No prf' => No (notAllThere prf')


text:
module elem

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

isElem : DecEq a => (x : a) -> (xs : List a) -> Maybe (Elem x xs)
isElem x [] = Nothing
isElem x (y :: xs) with (decEq x y)
  isElem x (x :: xs) | (Yes refl) = return Here
  isElem x (y :: xs) | (No f) = return (There !(isElem x xs))

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Verified.Applicative.Maybe

import Verified.Applicative
import Verified.Functor
import Verified.Functor.Maybe

instance VerifiedApplicative Maybe where
  applicativeMap Nothing g = Refl
  applicativeMap (Just x) g = Refl
  applicativeIdentity Nothing = Refl
  applicativeIdentity (Just x) = Refl
  applicativeComposition Nothing g1 g2 = Refl
  applicativeComposition (Just x) Nothing g2 = Refl
  applicativeComposition (Just x) (Just g1) Nothing = Refl
  applicativeComposition (Just x) (Just g1) (Just g2) = Refl
  applicativeHomomorphism x g = Refl
  applicativeInterchange x Nothing = Refl
  applicativeInterchange x (Just g) = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Test

data Dummy : (lbl : Type) -> (st : List lbl) -> Type -> Type where
  MkDummy : a -> Dummy b st a

public export
interface IxPure (f : (lbl : Type) -> (st : List lbl) -> Type -> Type)
          where
  ixPure : a -> f lbl st a

IxPure Dummy where
  ixPure = MkDummy

pure12 : Dummy String xs Nat
pure12 = ixPure Z


text:
module Chapter11

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

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 :: x) = value :: getPrefix k ?hole

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Data.Rel

import Data.Fun

||| Build an n-ary relation type from a Vect of Types
public export
Rel : Vect n Type -> Type
Rel ts = Fun ts Type

||| Universal quantification of a n-ary Relation over its
||| arguments to build a (function) type from a `Rel` type
|||
||| ```
||| λ> All [Nat,Nat] LTE
||| (x : Nat) -> (x : Nat) -> LTE x x
||| ```
public export
All : (ts : Vect n Type) -> (p : Rel ts) -> Type
All [] p = p
All (t :: ts) p = (x : t) -> All ts (p x)

||| Existential quantification of a n-ary relation over its
||| arguments to build a dependent pair (eg. Sigma type).
|||
||| Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are
||| types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r`
||| For example:
||| ```
||| λ> Ex [Nat,Nat] LTE
||| (x : Nat ** (x : Nat ** LTE x x))
||| ```
||| Which is the type of a pair of natural numbers along with a proof that the first
||| is smaller or equal than the second.
public export
Ex : (ts : Vect n Type) -> (p : Rel ts) -> Type
Ex [] p = p
Ex (t :: ts) p = (x : t ** Ex ts (p x))

||| Map a type-level function over the co-domain of a n-ary Relation
public export
liftRel : (ts : Vect n Type) -> (p : Rel ts) -> (Type -> Type) -> Type
liftRel ts p f = All ts $ map @{Nary} f p


text:
module Group.FiniteGenerate

import Group

%access public export

--proof that one element divides another in a group

-- element is generator if it is in the group and there is no element in the group that divides it

-- Create the collection of generators with their order

-- generates g^n given a group element g and n : Nat
Pow : (grp : Type) -> ((*) : grp -> grp -> grp) -> IsGroup grp (*) -> (g : grp) -> (n : Nat) -> grp
Pow grp (*) pfgrp g Z = fst (Group_id grp (*) pfgrp)
Pow grp (*) pfgrp g (S k) = g*(Pow grp (*) pfgrp g k)

-- check that group is finitely generated
HasFiniteOrder : (grp : Type) -> ((*) : grp -> grp -> grp) -> IsGroup grp (*) -> (g : grp) -> Type
HasFiniteOrder grp (*) pfgrp g = (n : Nat ** (LT Z n, Pow grp (*) pfgrp g n = fst (Group_id grp (*) pfgrp)))


text:
module Shenanigans

double : Num a => a -> a
double x = x + x

add : Num a => a -> a -> a
add x y = ?todo

id : a -> a
id x = x

||| Apply a function two times
||| @f The function to apply
||| @x The argument to supply
twice : (f : a -> a) -> (x : a) -> a
twice f x = f (f x)

Shape : Type
-- this function has a hole! (no definition)
rotate : Shape -> Shape

turn_around : Shape -> Shape
turn_around = twice rotate

pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (square x + square y)
  where
    square : Double -> Double
    square x = x*x

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.Time.Calendar.Gregorian

import public Data.Time.Calendar.Types
import Data.Time.Calendar.OrdinalDate
import Data.Time.Calendar.MonthDay
import Data.Time.Calendar.Days
import Data.Time.Calendar.CalendarDiffDays

import Text.Format.Decimal

%default total

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

||| Convert to proleptic Gregorian calendar.
export toGregorian : Day -> (Year, MonthOfYear, DayOfMonth)
toGregorian date =
  let (y, yd) = toOrdinalDate date
      (m, md) = dayOfYearToMonthAndDay (isLeapYear y) yd
      in (y, m, md)

||| Convert from proleptic Gregorian calendar.
||| Invalid values will be clipped to the correct range, month first, then day.
export fromGregorian : Year -> MonthOfYear -> DayOfMonth -> Day
fromGregorian year month day =
 fromOrdinalDate year (monthAndDayToDayOfYear (isLeapYear year) month day)

||| Convert from proleptic Gregorian calendar.
||| Invalid values will return Nothing
export fromGregorianValid : Year -> MonthOfYear -> DayOfMonth -> Maybe Day
fromGregorianValid year month day =
  case monthAndDayToDayOfYearValid (isLeapYear year) month day of
    Nothing => Nothing
    Just yd => fromOrdinalDateValid year yd

||| Show in ISO 8601 format (yyyy-mm-dd)
export showGregorian : Day -> String
showGregorian x with (toGregorian x)
  showGregorian x | (y, m, d) =
    format' (zeroPad 4) y ++ "-" ++ format' (zeroPad 2) m ++ "-" ++ format' (zeroPad 2) d

public export Show Day where show = showGregorian -- orphaned instance

||| The number of days in a given month according to the proleptic Gregorian calendar.
export gregorianMonthLength : Year -> MonthOfYear -> DayOfMonth
gregorianMonthLength year = monthLength $ isLeapYear year

export rolloverMonths : (Year, Integer) -> (Year, MonthOfYear)
rolloverMonths (y, m) = (y + ((m - 1) `div` 12), cast ((m - 1) `mod` 12) + 1)

export addGregorianMonths : Integer -> Day -> (Year, MonthOfYear, DayOfMonth)
addGregorianMonths n day =
  let (y, m, d) = toGregorian day
      (y', m') = rolloverMonths (y, cast m + n)
   in (y', m', d)

||| Add months, with days past the last day of the month clipped to the last day.
||| For instance, 2005-01-30 + 1 month = 2005-02-28.
export addGregorianMonthsClip : Integer -> Day -> Day
addGregorianMonthsClip n day =
  let (y, m, d) = addGregorianMonths n day
   in fromGregorian y m d

||| Add months, with days past the last day of the month rolling over to the next month.
||| For instance, 2005-01-30 + 1 month = 2005-03-02.
export addGregorianMonthsRollOver : Integer -> Day -> Day
addGregorianMonthsRollOver n day =
  let (y, m, d) = addGregorianMonths n day
   in addDays (cast d - 1) (fromGregorian y m 1)

||| Add years, matching month and day, with Feb 29th clipped to Feb 28th if necessary.
||| For instance, 2004-02-29 + 2 years = 2006-02-28.
export addGregorianYearsClip : Integer -> Day -> Day
addGregorianYearsClip n = addGregorianMonthsClip (n * 12)

||| Add years, matching month and day, with Feb 29th rolled over to Mar 1st if necessary.
||| For instance, 2004-02-29 + 2 years = 2006-03-01.
export addGregorianYearsRollOver : Integer -> Day -> Day
addGregorianYearsRollOver n = addGregorianMonthsRollOver (n * 12)

||| Add months (clipped to last day), then add days
export addGregorianDurationClip : CalendarDiffDays -> Day -> Day
addGregorianDurationClip x day =
  addDays x.day $ addGregorianMonthsClip x.month day

||| Add months (rolling over to next month), then add days
addGregorianDurationRollOver : CalendarDiffDays -> Day -> Day
addGregorianDurationRollOver x day =
  addDays x.day $ addGregorianMonthsRollOver x.month day

||| Calendrical difference, with as many whole months as possible
diffGregorianDurationClip : Day -> Day -> CalendarDiffDays
diffGregorianDurationClip day2 day1 =
  let (y1, m1, d1) = toGregorian day1
      (y2, m2, d2) = toGregorian day2
      ym1 = y1 * 12 + cast m1
      ym2 = y2 * 12 + cast m2
      ymdiff = ym2 - ym1
      ymAllowed = if day2 >= day1 then if d2 >= d1 then ymdiff else ymdiff - 1
                  else if d2 <= d1 then ymdiff
                  else ymdiff + 1
      dayAllowed = addGregorianDurationClip (MkCalendarDiffDays ymAllowed 0) day1
   in MkCalendarDiffDays ymAllowed $ diffDays day2 dayAllowed

||| Calendrical difference, with as many whole months as possible.
||| Same as 'diffGregorianDurationClip' for positive durations.
diffGregorianDurationRollOver : Day -> Day -> CalendarDiffDays
diffGregorianDurationRollOver day2 day1 =
  let (y1, m1, d1) = toGregorian day1
      (y2, m2, d2) = toGregorian day2
      ym1 = y1 * 12 + cast m1
      ym2 = y2 * 12 + cast m2
      ymdiff = ym2 - ym1
      ymAllowed = if day2 >= day1 then if d2 >= d1 then ymdiff else ymdiff - 1
                  else if d2 <= d1 then ymdiff
                  else ymdiff + 1
      dayAllowed = addGregorianDurationRollOver (MkCalendarDiffDays ymAllowed 0) day1
   in MkCalendarDiffDays ymAllowed $ diffDays day2 dayAllowed

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


text:
module Extra.GLFW.Core

import Extra.GLFW.FFI
import public Extra.C.Types
import Control.Linear.LIO

%foreign libglfw "glfwInit"
export
prim__glfwInit : PrimIO CInt

%foreign libglfw "glfwTerminate"
export
prim__glfwTerminate : PrimIO ()

%foreign libglfw "glfwGetVersion"
export
prim__glfwGetVersion : Ptr CInt -> Ptr CInt -> Ptr CInt -> PrimIO ()

export
data GLFWmonitor : Type where

export
data GLFWwindow : Type where

%foreign libglfw "glfwCreateWindow"
export
prim__glfwCreateWindow : CInt -> CInt -> CString -> Ptr GLFWmonitor -> Ptr GLFWwindow -> PrimIO (Ptr GLFWwindow)

%foreign libglfw "glfwWindowShouldClose"
export
prim__glfwWindowShouldClose : Ptr GLFWwindow -> PrimIO CInt

%foreign libglfw "glfwSetWindowShouldClose"
export
prim__glfwSetWindowShouldClose : Ptr GLFWwindow -> CInt -> PrimIO ()

%foreign libglfw "glfwSwapBuffers"
export
prim__glfwSwapBuffers : Ptr GLFWwindow -> PrimIO ()

%foreign libglfw "glfwPollEvents"
export
prim__glfwPollEvents : PrimIO ()


text:
module ExactLength

import EqNat

data Vect : Nat -> Type -> Type where
     Nil : Vect Z ty
     (::) : ty -> Vect n ty -> Vect (S n) ty

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 Just (Same len) => Just input


text:
data Vect : Nat -> Type -> Type where
    Nil : Vect Z a
    (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

%name Vect xs, ys, zs

append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] [] = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Main

import Data.Vect
import System

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

readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
  Just num1_ok <- readNumber | Nothing => pure Nothing
  Just num2_ok <- readNumber | Nothing => pure Nothing
  pure (Just (num1_ok, num2_ok))

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Left off!"
countdown (S secs) = do
  putStrLn (show (S secs))
  usleep 1000000
  countdown secs

countdowns : IO ()
countdowns = do
  putStr "Enter a starting number: "
  Just startNum <- readNumber
     | Nothing => do putStrLn "Invalid input"
                     countdowns
  countdown startNum
  putStr "Another (y/n)? "
  yn <- getLine
  if yn == "y"
    then countdowns
    else pure ()

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do
  x <- getLine
  xs <- readVectLen k
  pure (x :: xs)

anyVect : (n : Nat ** Vect n String)
anyVect = (3 **  ["a", "b", "c"])

readVect : IO (n : Nat ** Vect n String)
readVect = do
  x <- getLine
  if x == ""
    then pure (0 ** [])
    else do
      (k ** xs) <- readVect
      pure (S k ** x :: xs)

zipInputs : IO ()
zipInputs = do
  putStrLn "Enter the first vector (blank line to end): "
  (len1 ** vect1) <- readVect
  putStrLn "Enter the second vector (blank line to end): "
  (len2 ** vect2) <- readVect
  case exactLength len1 vect2 of
    Nothing => putStrLn "Vectors are different lengths"
    Just vect2' => printLn (zip vect1 vect2')

main : IO ()
main = do
  countdowns
  res3 <- readVectLen 3
  print res3
  print anyVect
  zipInputs

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module LightClick.IR.Channel.Normalise

import Data.List
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect

import LightClick.Types
import LightClick.Terms

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric

import public LightClick.IR.Channel.Normalise.Error
import LightClick.IR.Channel.Normalise.LetFloat
import LightClick.IR.Channel.Normalise.Merge
import LightClick.IR.Channel.Normalise.FreshBinders

%default total

export
covering -- comes from Merge runMerge not being total.
normalise : ChannelIR UNIT -> Either Normalise.Error (ChannelIR UNIT)
normalise expr =
  do e'   <- runLetFloat expr
     em'  <- runMerge e'
     emb' <- freshBinders em'
     pure emb'

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Decidable.Decidable.Extra

import Data.Rel
import Data.Rel.Complement
import Data.Fun
import Data.Vect
import Data.HVect
import Data.Fun.Extra
import Decidable.Decidable

%default total

public export
NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
NotNot r = map @{Nary} (Not . Not) r

[DecidablePartialApplication] {x : t} -> (tts : Decidable (S n) (t :: ts) r) => Decidable n ts (r x) where
  decide = decide @{tts} x

public export
doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
  (witness : HVect ts) ->
  uncurry (NotNot {ts} r) witness ->
  uncurry              r  witness
doubleNegationElimination {ts = []} @{dec} [] prfnn =
  case decide @{dec} of
    Yes prf  => prf
    No  prfn => absurd $ prfnn prfn
doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
  doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn

doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
  All ts (NotNot {ts} r) -> All ts r
doubleNegationForall @{dec} forall_prf =
  let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
      prfnn = uncurryAll forall_prf
      prf   : (witness : HVect ts) -> uncurry              r  witness
      prf witness = doubleNegationElimination @{dec} witness (prfnn witness)
  in curryAll prf

public export
doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
  Ex ts (NotNot {ts} r) ->
  Ex ts r
doubleNegationExists @{dec} nnxs =
  let witness : HVect ts
      witness = extractWitness nnxs
      witnessingnn : uncurry (NotNot {ts} r) witness
      witnessingnn = extractWitnessCorrect nnxs
      witnessing   : uncurry              r  witness
      witnessing   = doubleNegationElimination @{dec} witness witnessingnn
  in introduceWitness witness witnessing

decideTransform :
  {n : Nat}
  -> {ts : Vect n Type}
  -> {r : Rel ts}
  -> {t : Type -> Type}
  -> (tDec : {a : Type} -> Dec a -> Dec (t a))
  -> (posDec : IsDecidable n ts r)
  -> IsDecidable n ts (chain {ts} t r)
decideTransform tDec posDec =
  curryAll $ \xs =>
    replace {p = id} (chainUncurry (chain t r) Dec xs) $
      replace {p = Dec} (chainUncurry r t xs) $
        tDec $ replace {p = id} (sym $ chainUncurry r Dec xs) $
          uncurryAll posDec xs

||| Convert a decision about a decidable property into one about its negation.
public export
negateDec : (dec : Dec a) -> Dec (Not a)
negateDec (Yes pf) = No ($ pf)
negateDec (No npf) = Yes npf

||| We can turn (Not (Exists Not)) into Forall for decidable types
public export
notExistsNotForall :
  {0 p : a -> Type}
  -> ((x : a) -> Dec (p x))
  -> Dec (x : a ** Not (p x))
  -> Dec ((x : a) -> p x)
notExistsNotForall dec decEx =
  case decEx of
    Yes (x ** nx) => No $ \f => nx $ f x
    No notNot => Yes $ \x => case (dec x) of
      Yes px => px
      No nx => void $ notNot $ (x ** nx)

||| If a relation is decidable, then so is its complement
public export
[DecidableComplement] {n : Nat} -> {ts : Vect n Type} -> {r : Rel ts} -> (posDec : Decidable n ts r) =>
  Decidable n ts (complement {ts} r) where
    decide = decideTransform negateDec (decide @{posDec})


text:
module TTImp.Elab.Lazy

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

%default covering

export
checkDelayed : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               {auto e : Ref EST (EState vars)} ->
               RigCount -> ElabInfo ->
               NestedNames vars -> Env Term vars ->
               FC -> LazyReason -> RawImp -> Maybe (Glued vars) ->
               Core (Term vars, Glued vars)
checkDelayed rig elabinfo nest env fc r tm exp
    = do (tm', gty) <- check rig elabinfo nest env tm (Just (gType fc))
         pure (TDelayed fc r tm', gty)

export
checkDelay : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             RigCount -> ElabInfo ->
             NestedNames vars -> Env Term vars ->
             FC -> RawImp -> Maybe (Glued vars) ->
             Core (Term vars, Glued vars)
checkDelay rig elabinfo nest env fc tm mexpected
    = do expected <- maybe (do nm <- genName "delayTy"
                               ty <- metaVar fc erased env nm (TType fc)
                               pure (gnf env ty))
                           pure mexpected
         let solvemode = case elabMode elabinfo of
                              InLHS c => inLHS
                              _ => inTerm
         solveConstraints solvemode Normal
         -- Can only check if we know the expected type already because we
         -- need to infer the delay reason
         delayOnFailure fc rig env (Just expected) delayError LazyDelay
            (\delayed =>
                 case !(getNF expected) of
                      NDelayed _ r expnf =>
                         do defs <- get Ctxt
                            (tm', gty) <- check rig elabinfo nest env tm
                                                (Just (glueBack defs env expnf))
                            tynf <- getNF gty
                            ty <- getTerm gty
                            pure (TDelay fc r ty tm',
                                  glueBack defs env (NDelayed fc r tynf))
                      ty => do logNF "elab.delay" 5 "Expected delay type" env ty
                               throw (GenericMsg fc ("Can't infer delay type")))
  where
    delayError : Error -> Bool
    delayError (GenericMsg _ _) = True
    delayError _ = False

export
checkForce : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             RigCount -> ElabInfo ->
             NestedNames vars -> Env Term vars ->
             FC -> RawImp -> Maybe (Glued vars) ->
             Core (Term vars, Glued vars)
checkForce rig elabinfo nest env fc tm exp
    = do defs <- get Ctxt
         expf <- maybe (pure Nothing)
                       (\gty => do tynf <- getNF gty
                                   pure (Just (glueBack defs env
                                         (NDelayed fc LUnknown tynf))))
                       exp
         (tm', gty) <- check rig elabinfo nest env tm expf
         tynf <- getNF gty
         case tynf of
              NDelayed _ r expnf =>
                 pure (TForce fc r tm', glueBack defs env expnf)
              _ => throw (GenericMsg fc "Forcing a non-delayed type")


text:
module Data.Crypto.Encryption

import Data.Bits
import Data.Crypto.Util

%default total
%access public export

interface Cipher c (bitsPerChunk : Nat) | c where

interface Cipher e bitsPerChunk => Encrypter e (bitsPerChunk : Nat) | e where
  encryptMessage : e -> List (Bits bitsPerChunk) -> List (Bits bitsPerChunk)

interface Cipher d bitsPerChunk => Decrypter d (bitsPerChunk : Nat) | d where
  decryptMessage : d -> List (Bits bitsPerChunk) -> List (Bits bitsPerChunk)

encrypt : (Encrypter c _, Serializable pt, Serializable ct) => c -> pt -> ct
encrypt cipher = decode . encryptMessage cipher . encode

decrypt : (Decrypter c _, Serializable pt, Serializable ct) => c -> pt -> ct
decrypt cipher = decode . decryptMessage cipher . encode

interface (Encrypter c bitsPerChunk, Decrypter c bitsPerChunk) =>
  SymmetricCipher c (bitsPerChunk : Nat) | c where

interface (Encrypter p pb, Decrypter v vb) =>
  AsymmetricCipher p v (pb : Nat) (vb : Nat) | p, v where

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


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

import Data.List.Views

data SnocList0 ty = Empty0 | Snoc0 (SnocList0 ty) ty

reverseSnoc : SnocList0 a -> List a
reverseSnoc Empty0 = []
reverseSnoc (Snoc0 xs y) = y :: reverseSnoc xs

data SnocList1 : List a -> Type where
  Empty1 : SnocList1 []
  Snoc1 : (rec : SnocList1 xs) -> SnocList1 (xs ++ [x])

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

snocList1 : (xs : List a) -> SnocList1 xs
snocList1 = snocListHelper Empty1

myReverseHelper : (input : List a) -> SnocList1 input -> List a
myReverseHelper [] Empty1 = []
myReverseHelper (xs ++ [x]) (Snoc1 rec) = x :: myReverseHelper xs rec

total
myReverse : List a -> List a
myReverse input = myReverseHelper input (snocList1 input)

total
myReverse2 : List a -> List a
myReverse2 xs with (snocList1 xs)
  myReverse2 [] | Empty1 = []
  myReverse2 (ys ++ [x]) | (Snoc1 rec) = x :: myReverse2 ys | rec

total
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList1 input1)
  isSuffix [] ys | Empty1 = True
  isSuffix (xs ++ [x]) input2 | (Snoc1 xsrec) with (snocList1 input2)
    isSuffix (xs ++ [x]) [] | (Snoc1 xsrec) | Empty1 = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc1 xsrec) | (Snoc1 ysrec) =
      case x == y of
        False => False
        True => isSuffix xs ys | xsrec | ysrec

total
mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) =
    (mergeSort lefts | lrec) `merge` (mergeSort rights | rrec)

main : IO ()
main = do
  printLn $ reverseSnoc (Snoc0 Empty0 1)
  printLn $ myReverse [1]
  printLn $ myReverse [1..10]
  printLn $ myReverse2 [1..10]
  printLn $ isSuffix [7,8,9,10] [1..10]
  printLn $ isSuffix [7,8,9] [1..10]
  printLn $ mergeSort [3,2,1]
  printLn $ mergeSort [5,1,4,3,2,6,8,7,9]


text:
module Rings

import Monoid
import Group

%access public export

||| Distributive Law
total
IsDistributive : (typ : Type) -> ((+) : typ -> typ -> typ)
                  -> ((*) : typ -> typ -> typ) -> Type
IsDistributive typ (+) (*) = (a,b,c : typ) -> ( (a*(b + c) = (a*b) + (a*c)), ((b + c)*a = (b*a) + (b*c)) )

total
IsRing : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsRing ring (+) (*) = (IsAbelianGrp ring (+), (IsMonoid ring (*), IsDistributive ring (+) (*)))

total
IsCommRing : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsCommRing ring (+) (*) = (IsRing ring (+) (*) , Commutative ring (+))

||| Gives the additive identity of the ring
RingAdditive_id : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) ->
                  (IsRing ring (+) (*)) -> (IdentityExists ring (+))
RingAdditive_id ring (+) (*) ((pfGrp,pfAb), pfElse) = Group_id ring (+) pfGrp

||| Non Zero elements in a ring
Ring_NonZero_Elements : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) ->
                        (IsRing ring (+) (*)) -> Type
Ring_NonZero_Elements ring (+) (*) pfRing = (a : ring ** ((a = e) -> Void)) where
                                             e = fst (RingAdditive_id ring (+) (*) pfRing)
||| Type of rings with identity
total
IsRing_with_identity : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsRing_with_identity ring (+) (*) = (pfRing : IsRing ring (+) (*) **
                                    ( iden : (Ring_NonZero_Elements ring (+) (*) pfRing) **
                                      (a : ring) -> ((a*(fst iden) = a) , ((fst iden)*a = a))))

||| Useful rings - i.e commutative rings with identity
total
IsUsefulRing :  (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsUsefulRing ring (+) (*) = (IsRing_with_identity ring (+) (*), IsCommRing ring (+) (*))


text:
||| Test if :typeat correctly shows types within !(...)

n : List a -> List a
n xs = pure !xs

f : (a -> List b) -> a -> (b -> List c) -> List c
f g a j = j !(g a)


text:
module HetTree

import Semiring

%default total
%access public export

data Tree a = Nil | End a | (::) (Tree a) (Tree a)

data BiVect : Tree Type -> Type where
  Leaf : BiVect Nil
  Node : a -> BiVect (End a)
  Branch : BiVect ls -> BiVect rs -> BiVect (ls::rs)

using (x : a, ls : Tree a, rs : Tree a)
  data Elem : a -> Tree a -> Type where
    Here  : Elem x (End x)
    Left  : Elem x ls -> Elem x (ls::rs)
    Right : Elem x rs -> Elem x (ls::rs)

remove : (x : a) -> (xs : Tree a) -> Elem x xs -> Tree a
remove x (End x) Here = Nil
remove x (ls :: rs) (Left  p) = remove x ls p :: rs
remove x (ls :: rs) (Right p) = ls :: remove x rs p

addBack
  : {xs : Tree Type}
  -> {x : Type}
  -> {auto elem : Elem x xs}
  -> (val : x)
  -> (vec : BiVect (remove x xs elem))
  -> BiVect xs
addBack {elem = Here} val vec = Node val
addBack {elem = (Left  x)} val (Branch ls rs) = Branch (addBack val ls) rs
addBack {elem = (Right x)} val (Branch ls rs) = Branch ls (addBack val rs)

data AllFinite : Tree Type -> Type where
  Empty : AllFinite Nil
  Both
    : (lhs : AllFinite ls)
    -> (rhs : AllFinite rs)
    -> AllFinite (ls::rs)
  Extra
    : (MinBound x, MaxBound x, Enum x)
    => AllFinite (End x)

marg : (Semiring n, MinBound a, MaxBound a, Enum a) => (a -> n) -> n
marg f = sum (map f [minBound .. maxBound])

margBiVec
: Semiring n
=> {xs : Tree Type}
-> {auto prf : AllFinite xs}
-> (BiVect xs -> n) -> n
margBiVec {xs=Nil} f = f Leaf
margBiVec {xs=End x} {prf=Extra} f = marg (\y => f (Node y))
margBiVec {xs=ls::rs} {prf=Both lp rp} f = margBiVec (\lhs => margBiVec (\rhs => f (Branch lhs rhs)))

margOnce : (Semiring n, Enum x, MinBound x, MaxBound x) => {xs : Tree Type} -> {auto elem : Elem x xs} -> (BiVect xs -> n) -> BiVect (remove x xs elem) -> n
margOnce {elem} f tr = marg (\x => f (addBack x tr))

split : {auto elem : Elem x xs} -> BiVect xs -> (x, BiVect (remove x xs elem))
split {elem = Here} (Node x) = (x, Leaf)
split {elem = (Left  p)} (Branch ls rs) = let (el,rm) = split {elem=p} ls in (el, Branch rm rs)
split {elem = (Right p)} (Branch ls rs) = let (el,rm) = split {elem=p} rs in (el, Branch ls rm)

pop : {auto elem : Elem x xs} -> BiVect xs -> BiVect (remove x xs elem)
pop {elem = Here} (Node x) = Leaf
pop {elem = (Left  p)} (Branch ls rs) = Branch (pop ls) rs
pop {elem = (Right p)} (Branch ls rs) = Branch ls (pop rs)

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module NN.Dense

import Backprop
import Control.Optics
import Linear.Backprop
import Linear.V
import Utils.String

public export
record Dense (i : Nat) (o : Nat) (a : Type) where
  constructor MkDense
  weights : T [i, o] a
  biases : T [o] a

export
lweights : Simple Lens (Dense i o a) (T [i, o] a)
lweights = lens weights (\s, b => { weights := b } s)

export
lbiases : Simple Lens (Dense i o a) (T [o] a)
lbiases = lens biases (\s, b => { biases := b } s)

export
{i : _} -> {o : _} -> FromDouble a => FromDouble (Dense i o a) where
  fromDouble x = MkDense (fromDouble x) (fromDouble x)

export
{i : _} -> {o : _} -> CanBack a => CanBack (Dense i o a) where
  zero = MkDense zero zero
  one = MkDense one one
  add x1 x2 = MkDense (add x1.weights x2.weights) (add x1.biases x2.biases)

export
{i : _} -> {o : _} -> Num a => Num (Dense i o a) where
  x1 + x2 = MkDense (x1.weights + x2.weights) (x1.biases + x2.biases)
  x1 * x2 = MkDense (x1.weights * x2.weights) (x1.biases * x2.biases)
  fromInteger x = MkDense (fromInteger x) (fromInteger x)

export
{i : _} -> {o : _} -> Neg a => Neg (Dense i o a) where
  x1 - x2 = MkDense (x1.weights - x2.weights) (x1.biases - x2.biases)
  negate x = MkDense (negate x.weights) (negate x.biases)

export
Show a => Show (Dense i o a) where
  show x = show_record "MkDense" [("weights", show x.weights), ("biases", show x.biases)]

export
apply : {i, o, n, a : _} -> CanBack a => Num a => Node s (Dense i o a) -> Node s (T [n, i] a) -> Node s (T [n, o] a)
apply layer x = x <> (layer ^. lweights) + konst (layer ^. lbiases)


text:
module Gen.Common

infixr 3 /\
public export
(/\) : Type -> Type -> Type
(/\) = Pair

infixr 3 ><
public export
(><) : Type -> Type -> Type
(><) = Pair

infixr 2 \/
public export
(\/) : Type -> Type -> Type
(\/) = Either

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Series

public export
data Series a = ?hole


text:
module Arduino.Wrapper

import Arduino.Boards
import Arduino.Util

import Control.Monad.Syntax

%default total

----------------------------------------------
----------------------------------------------
---  Compile-time board state description  ---
----------------------------------------------
----------------------------------------------

public export
Fact : Type
Fact = ((objType : Type ** objType), (factType : Type ** factType))

infix 6 `withFact`
infixl 5 `Then`, `Then1`

public export
withFact : (obj : objType) -> (fact : factType) -> Fact
withFact obj fact = ((_ ** obj), (_ ** fact))

-- Specialized list is used to make used to not be able to append the wrong side and similar things.
public export
data FactsList : Type where
  NoFacts : FactsList
  Then1   : FactsList -> Fact -> FactsList

-- TODO To think of adding `ThenAtomic : FactsList -> List Fact -> FactsList` or similar constructor.
--      This is to give an ability to add two facts at once ("atomically")
--      without any need to check parallel computation on each separate added fact.

-- TODO To think of `Then1` constructor that actually adds only when added stuff differs from the last known for the given object and fact type.
--      Think of forever spinning: this shouldn't add infinite amount of new facts if only one fact happens constantly.

--- Building ---

public export
oneFact : (obj : objType) -> (fact : factType) -> FactsList
oneFact = Then1 NoFacts .. withFact

public export
Then : FactsList -> FactsList -> FactsList
Then fs NoFacts        = fs
Then fs (ss `Then1` x) = (fs `Then` ss) `Then1` x

||| Type-level conjunction of two preconditions with a modification of input between.
public export
ConseqConj : (FactsList -> Type) -> FactsList -> (FactsList -> Type) -> FactsList -> Type
ConseqConj preL afterL preR fs = (preL fs, preR $ fs `Then` afterL)

-- TODO To make the "conjunction" above to have a single canonical form, e.g. to have `Conseq p NoFact p` be actually equal to `p` itself.
--      This is important e.g. for having non-hacking way for implementing `forever`.

--- Querying ---

public export
data LastFactEq : (obj : objType) -> (expectedFact : factType) -> FactsList -> Type where
  LastMatches : (facts : FactsList)
             -> (obj : objType)
             -> (fact : factType)
             -> LastFactEq obj fact $ facts `Then1` obj `withFact` fact
  AnotherFactType : {fact : factType}
                 -> LastFactEq obj fact facts
                 -> (another : anotherFactType)
                 -> Uninhabited (factType = anotherFactType)
                 => LastFactEq obj fact $ facts `Then1` obj `withFact` another
  AnotherObj : {obj : objType}
            -> LastFactEq obj ft facts
            -> (anotherObj : objType)
            -> Uninhabited (obj = anotherObj)
            => LastFactEq obj ft $ facts `Then1` anotherObj `withFact` someFact
  AnotherObjType : {obj : objType}
                -> LastFactEq obj ft facts
                -> (anotherObj : anotherObjType)
                -> Uninhabited (objType = anotherObjType)
                => LastFactEq obj ft $ facts `Then1` anotherObj `withFact` someFact

  -- Well, `AnotherObj` and `AnotherObjType` can be joined, but I'm afraid of applying `=` to stuff with different types?

------------------------------------------------------------------------
------------------------------------------------------------------------
---  Data structure embedding effect and its type-level description  ---
------------------------------------------------------------------------
------------------------------------------------------------------------

export
data Ard : (board : Board)
        -> (precond : FactsList -> Type)
        -> (afterFacts : FactsList)
        -> (m : Type -> Type) -> Type -> Type where
  Wrapped : m a -> Ard board precond afterFacts m a

export
ard : m a -> Ard board precond afterFacts m a
ard = Wrapped

-------------------------
--- Functor for `Ard` ---
-------------------------

export
Functor m => Functor (Ard board precond afterFacts m) where
  map f (Wrapped act) = Wrapped $ map f act

--------------------------------------------
--- Applicative-like functions for `Ard` ---
--------------------------------------------

export
pure : Applicative m => a -> Ard board (const Unit) NoFacts m a
pure = Wrapped . pure

export
(<*>) : Applicative m => Ard board preL afL m (a -> b) -> Ard board preR afL m a -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m b
(Wrapped f) <*> (Wrapped x) = Wrapped $ f <*> x

--- Additional applicative-like syntax ---

export
(*>) : Applicative m => Ard board preL afL m a -> Ard board preR afR m b -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m b
(Wrapped l) *> (Wrapped r) = Wrapped $ l *> r

export
(<*) : Applicative m => Ard board preL afL m a -> Ard board preR afR m b -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m a
(Wrapped l) <* (Wrapped r) = Wrapped $ l <* r

--------------------------------------------
--- Alternative-like functions for `Ard` ---
--------------------------------------------

export
empty : Alternative m => Ard board (const Unit) NoFacts m a
empty = Wrapped empty

||| Means that given condition is true on given `facts` prepended with all prefixes (incl. empty) of `addition` list.
public export
data WithAllAdditions : (cond : FactsList -> Type) -> (facts : FactsList) -> (addition : FactsList) -> Type where
  Nil  : {auto ev : cond facts} -> WithAllAdditions cond facts NoFacts
  (::) : (fact : Fact) -> {auto ev : cond $ facts `Then` addition `Then1` fact} -> WithAllAdditions cond facts addition -> WithAllAdditions cond facts (addition `Then1` fact)

-- TODO to replace those above with a check on a full interleaving of after-fact prefixes.

export
(<|>) : Alternative m => Ard board preL afL m a
                      -> Ard board preR afR m a
                      -> Ard board (\fs => (WithAllAdditions preL fs afR, WithAllAdditions preR fs afL)) (afL `Then` afR) m a
(Wrapped l) <|> (Wrapped r) = Wrapped $ l <|> r

-- TODO to think whether sequential composition of facts (i.e., ``afL `Then` afR``) is enough for the resulting after-facts of parallel composition.

--------------------------------------
--- Monad-like functions for `Ard` ---
--------------------------------------

export
(>>=) : Monad m => Ard board preL afL m a -> (a -> Ard board preR afR m b) -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m b
(Wrapped l) >>= f = Wrapped $ l >>= \x => let Wrapped r = f x in r

export
join : Monad m => Ard board preL afL m (Ard board preR afR m a) -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m a
join (Wrapped l) = Wrapped $ l >>= \ard => let Wrapped r = ard in r

export covering
forever : Monad m => Ard board pre NoFacts m a -> Ard board pre NoFacts m b
forever (Wrapped x) = Wrapped foreverX
  where foreverX = x >>= \_ => foreverX

--- Additional monad-like syntax ---

export
(=<<) : Monad m => (a -> Ard board preR afR m b) -> Ard board preL afL m a -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m b
(=<<) = flip (>>=)

export
(>=>) : Monad m => (a -> Ard board preL afL m b) -> (b -> Ard board preR afR m c) -> a -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m c
(>=>) fl fr x = fl x >>= fr

export
(<=<) : Monad m => (b -> Ard board preR afR m c) -> (a -> Ard board preL afL m b) -> a -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m c
(<=<) = flip (>=>)

infixl 1 *>>
||| Applicative-like `*>` operator but with lazy right argument
export
(*>>) : Monad m => Ard board preL afL m a -> Lazy (Ard board preR afR m b) -> Ard board (ConseqConj preL afL preR) (afL `Then` afR) m b
l *>> r = l >>= \_ => r

----------------------
--- `Ard`'s runner ---
----------------------

-- Top-level (at the end of the day) runner for the `Ard`
export
runArd : (board : Board) -> Ard board precond af m a -> {auto prf : precond NoFacts} -> m a
runArd _ (Wrapped act) = act

-- TODO `board` argument should be compile-time only, i.e. have quantity of `0`.

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:
-- Minimal propositional logic, PHOAS approach, final encoding

module Pf.Mp

%default total

-- Types

infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty
  (:&&) : Ty -> Ty -> Ty
  (:||) : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 :<=>
(:<=>) : Ty -> Ty -> Ty
(:<=>) a b = (a :=> b) :&& (b :=> a)

NOT : Ty -> Ty
NOT a = a :=> FALSE

TRUE : Ty
TRUE = FALSE :=> FALSE

-- Context and truth judgement

Cx : Type
Cx = Ty -> Type

isTrue : Ty -> Cx -> Type
isTrue a tc = tc a

-- Terms

TmRepr : Type
TmRepr = Cx -> Ty -> Type

infixl 1 :$
class ArrMpTm (tr : TmRepr) where
  var  : isTrue a tc                -> tr tc a
  lam' : (isTrue a tc -> tr tc b)   -> tr tc (a :=> b)
  (:$) : tr tc (a :=> b) -> tr tc a -> tr tc b

lam'' : {tr : TmRepr} -> ArrMpTm tr => (tr tc a -> tr tc b) -> tr tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

syntax "lam" {a} ":=>" [b] = lam'' (\a => b)

class ArrMpTm tr => MpTm (tr : TmRepr) where
  pair  : tr tc a         -> tr tc b -> tr tc (a :&& b)
  fst   : tr tc (a :&& b)            -> tr tc a
  snd   : tr tc (a :&& b)            -> tr tc b
  left  : tr tc a                    -> tr tc (a :|| b)
  right : tr tc b                    -> tr tc (a :|| b)
  case' : tr tc (a :|| b) -> (isTrue a tc -> tr tc c) -> (isTrue b tc -> tr tc c) -> tr tc c

case'' : {tr : TmRepr} -> MpTm tr => tr tc (a :|| b) -> (tr tc a -> tr tc c) -> (tr tc b -> tr tc c) -> tr tc c
case'' xy f g = case' xy (\x => f (var x)) (\y => g (var y))

syntax "["    [a]  ","  [b] "]" = pair a b
syntax "case" [ab] "of" {a} ":=>" [c1] or {b} ":=>" [c2] = case'' ab (\a => c1) (\b => c2)

Thm : Ty -> Type
Thm a = {tr : TmRepr} -> {tc : Cx} -> MpTm tr => tr tc a

-- Example theorems

c1 : Thm (a :&& b :<=> b :&& a)
c1 =
  [ lam xy :=> [ snd xy , fst xy ]
  , lam yx :=> [ snd yx , fst yx ]
  ]

c2 : Thm (a :|| b :<=> b :|| a)
c2 =
  [ lam xy :=>
      case xy
        of x :=> right x
        or y :=> left y
  , lam yx :=>
      case yx
        of y :=> right y
        or x :=> left x
  ]

i1 : Thm (a :&& a :<=> a)
i1 =
  [ lam xx :=> fst xx
  , lam x  :=> [ x , x ]
  ]

i2 : Thm (a :|| a :<=> a)
i2 =
  [ lam xx :=>
      case xx
        of x :=> x
        or x :=> x
  , lam x :=> left x
  ]

l3 : Thm ((a :=> a) :<=> TRUE)
l3 =
  [ lam x :=> lam nt :=> nt
  , lam b :=> lam x  :=> x
  ]

l1 : Thm (a :&& (b :&& c) :<=> (a :&& b) :&& c)
l1 =
  [ lam xyz :=>
      (let yz = snd xyz in
        [ [ fst xyz , fst yz ] , snd yz ])
  , lam xyz :=>
      (let xy = fst xyz in
        [ fst xy , [ snd xy , snd xyz ] ])
  ]

l2 : Thm (a :&& TRUE :<=> a)
l2 =
  [ lam xt :=> fst xt
  , lam x  :=> [ x , lam nt :=> nt ]
  ]

l4 : Thm (a :&& (b :|| c) :<=> (a :&& b) :|| (a :&& c))
l4 =
  [ lam xyz :=>
      (let x = fst xyz in
        case snd xyz
          of y :=> left  [ x , y ]
          or z :=> right [ x , z ])
  , lam xyxz :=>
      case xyxz
        of xy :=> ([ fst xy , left  (snd xy) ])
        or xz :=> [ fst xz , right (snd xz) ]
  ]

l6 : Thm (a :|| (b :&& c) :<=> (a :|| b) :&& (a :|| c))
l6 =
  [ lam xyz :=>
      case xyz
        of x  :=> ([ left x , left x ])
        or yz :=> [ right (fst yz) , right (snd yz) ]
  , lam xyxz :=>
      case fst xyxz
        of x :=> left x
        or y :=>
          case snd xyxz
            of x :=> left x
            or z :=> right [ y , z ]
  ]

l7 : Thm (a :|| TRUE :<=> TRUE)
l7 =
  [ lam xt :=> lam nt :=> nt
  , lam t  :=> right t
  ]

l9 : Thm (a :|| (b :|| c) :<=> (a :|| b) :|| c)
l9 =
  [ lam xyz :=>
      case xyz
        of x  :=> left (left x)
        or yz :=>
          case yz
            of y :=> left (right y)
            or z :=> right z
  , lam xyz :=>
      case xyz
        of xy :=>
          case xy
            of x :=> left x
            or y :=> right (left y)
        or z :=> right (right z)
  ]

l11 : Thm ((a :=> (b :&& c)) :<=> (a :=> b) :&& (a :=> c))
l11 =
  [ lam xyz :=>
      [ lam x :=> fst (xyz :$ x)
      , lam x :=> snd (xyz :$ x)
      ]
  , lam xyxz :=>
      lam x :=> [ fst xyxz :$ x , snd xyxz :$ x ]
  ]

l12 : Thm ((a :=> TRUE) :<=> TRUE)
l12 =
  [ lam f :=> lam nt :=> nt
  , lam t :=> lam f  :=> t
  ]

l13 : Thm ((a :=> (b :=> c)) :<=> ((a :&& b) :=> c))
l13 =
  [ lam xyz :=>
      lam xy :=> xyz :$ fst xy :$ snd xy
  , lam xyz :=>
      lam x :=>
        lam y :=> xyz :$ [ x , y ]
  ]

l16 : Thm (((a :&& b) :=> c) :<=> (a :=> (b :=> c)))
l16 =
  [ lam xyz :=>
      lam x :=>
        lam y :=> xyz :$ [ x , y ]
  , lam xyz :=>
      lam xy :=> xyz :$ fst xy :$ snd xy
  ]

l17 : Thm ((TRUE :=> a) :<=> a)
l17 =
  [ lam tx :=> tx :$ (lam nt :=> nt)
  , lam x  :=> lam tx :=> x
  ]

l19 : Thm (((a :|| b) :=> c) :<=> (a :=> c) :&& (b :=> c))
l19 =
  [ lam xyz :=>
      [ lam x :=> xyz :$ left x
      , lam y :=> xyz :$ right y
      ]
  , lam xzyz :=>
      lam xy :=>
        case xy
          of x :=> fst xzyz :$ x
          or y :=> snd xzyz :$ y
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Scenes.Main

import API.Web.Console
import API.Web.DOM.Document
import API.Web.DOM.DocumentType
import API.Web.DOM.Element
import API.Web.DOM.NonElementParentNode
import API.Web.HTML.HTMLElement
import API.Web.HTML.HTMLCanvasElement
import API.Web.HTML.Document
import API.Web.HTML.Window
import API.WebGL.Context
import IdrisScript
import Interfaces

%access public export

record Scene where
  constructor Init
  window : Window
  context : RenderingContext

FrameRequest Scene where
  requestFrame scene callback =
    requestAnimationFrame (window scene) callback >>= discardInt where
      discardInt : Maybe Int -> JS_IO ()
      discardInt n = pure ()

Updatable Scene where
  update scene = paint scene >>= \x => log "test" >>= \x => pure scene where
    getContext : Scene -> WebGLRenderingContext
    getContext scene = case (context scene) of
                            (FromWebGLRenderingContext ctx) => ctx

    paint : Scene -> JS_IO ()
    paint scene = clearColor (getContext scene) 1 0 0 1 >>= \x =>
                  clear (getContext scene) COLOR_BUFFER_BIT

export
initSceneWith : Window -> JS_IO $ Maybe Scene
initSceneWith window = case !context of
    Nothing                 => pure Nothing
    (Just renderingContext) => pure $ Just $ Init window renderingContext
  where
    elm : NonElementParentNode
    elm = FromDocument $ FromHTMLDocument (New "html" "0" "0") (document window)

    canvas : JS_IO $ Maybe HTMLCanvasElement
    canvas = case !(getElementById elm "canvas") of
      Nothing => log "Could not get canvas" >>= \x => pure Nothing
      (Just (FromHTMLElement (FromHTMLCanvasElement cElm))) => pure $ Just cElm
      (Just (FromHTMLElement (New _ self))) => htmlCanvasElementFromPointer self
      (Just (New _ self))                   => htmlCanvasElementFromPointer self

    context : JS_IO $ Maybe RenderingContext
    context = case !canvas of
      Nothing           => pure Nothing
      (Just canvasElem) => getContext canvasElem "webgl"


text:
foo : String
foo = "nested: \{ " \{ 1 +  } " }"


text:
module Js.React.Element

import Control.Monad.Syntax
import Data.Foldable.Extras
import Js
import Js.Array
import Js.Object

%default total
%access export

public export
data Element = MkElement Ptr

Class Element where
    ptr (MkElement p) = p

public export
data Child = ChildElement Element
           | Text String

private
childrenArray : Foldable f => f Child -> JS_IO Ptr
childrenArray = createWith appendChild >=> pure . ptr
    where appendChild : Child -> Array -> JS_IO ()
          appendChild (ChildElement (MkElement p)) = append p
          appendChild (Text t) = append t

private
%inline
jsElement : (ty : Type) -> {auto fty : FTy FFI_JS [] ty} -> ty
jsElement ty = js "React.createElement(%0, %1, ...%2)" ty

%inline
tag : (Class p, Foldable f) => (name : String) -> (props : p) -> (children : f Child) -> JS_IO Element
tag name props = childrenArray >=> jsElement (String -> Ptr -> Ptr -> JS_IO Ptr) name (ptr props) >=> pure . MkElement

%inline
simple : Member a => (display : a -> JS_IO Element) -> (arg : a) -> JS_IO Element
simple display arg = assert_total (MkElement <$> js "React.createElement(%0, %1)"
                                                 (JsFn (Ptr -> JS_IO Ptr) -> Ptr -> JS_IO Ptr)
                                                 (MkJsFn $ get "v" . MkObject >=> (display >=> pure . ptr))
                                                 (ptr !(wrap "v" arg)))

%inline
class' : (Class c, Class p, Foldable f) => (cl : c) -> (props : p) -> (children : f Child) -> JS_IO Element
class' cl props = childrenArray >=> jsElement (Ptr -> Ptr -> Ptr -> JS_IO Ptr) (ptr cl) (ptr props) >=> pure . MkElement

%inline
div : (Class p, Foldable f) => (props : p) -> (children : f Child) -> JS_IO Element
div = tag "div"

%inline
button : (Class p, Foldable f) => (props : p) -> (children : f Child) -> JS_IO Element
button = tag "button"

max_stars_repo_name: jheiling/idris-react

max_issues_repo_name: jheiling/idris-react

max_forks_repo_name: jheiling/idris-react


text:
module Language.JSON.Parser

import Language.JSON.Data
import Text.Parser
import Text.Token
import Data.List

import public Language.JSON.Tokens

%default total

private
punct : Punctuation -> Grammar state JSONToken True ()
punct p = match $ JTPunct p

private
rawString : Grammar state JSONToken True String
rawString = do mstr <- match JTString
               the (Grammar _ _ False _) $
                   case mstr of
                        Just str => pure str
                        Nothing => fail "invalid string"

mutual
  private
  json : Grammar state JSONToken True JSON
  json = object
     <|> array
     <|> string
     <|> boolean
     <|> number
     <|> null

  private
  object : Grammar state JSONToken True JSON
  object = do punct $ Curly Open
              commit
              props <- properties
              punct $ Curly Close
              pure $ JObject props
    where
      properties : Grammar state JSONToken False (List (String, JSON))
      properties = sepBy (punct Comma) $
                         do key <- rawString
                            punct Colon
                            value <- json
                            pure (key, value)

  private
  array : Grammar state JSONToken True JSON
  array = do punct (Square Open)
             commit
             vals <- values
             punct (Square Close)
             pure (JArray vals)
    where
      values : Grammar state JSONToken False (List JSON)
      values = sepBy (punct Comma) json

  private
  string : Grammar state JSONToken True JSON
  string = map JString rawString

  private
  boolean : Grammar state JSONToken True JSON
  boolean = map JBoolean $ match JTBoolean

  private
  number : Grammar state JSONToken True JSON
  number = map JNumber $ match JTNumber

  private
  null : Grammar state JSONToken True JSON
  null = map (const JNull) $ match JTNull

export
parseJSON : List (WithBounds JSONToken) -> Maybe JSON
parseJSON toks = case parse json $ filter (not . ignored) toks of
                      Right (j, []) => Just j
                      _ => Nothing


text:
import System.Signal
import System

main : IO ()
main = do
  Right () <- collectSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "before"
  Right () <- raiseSignal SigABRT
    | Left (Error code) => putStrLn $ "got non-zero exit from system call: " ++ (show code)
  sleep 1
  Just SigABRT <- handleNextCollectedSignal
    | Just _  => putStrLn "received the wrong signal."
    | Nothing => putStrLn "did not receive expected signal."
  putStrLn "after"
  Right () <- defaultSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "done."


text:
import DataStore
import Shape

testStore : DataStore (SString .+. SInt)
testStore = addToStore ("First", 1) $
            addToStore ("Second", 2) $
            empty

getValues : DataStore (SString .+. valSchema) -> List (SchemaType valSchema)
getValues x with (storeView x)
  getValues x | SNil = []
  getValues (addToStore (key, value) store) | (SAdd rec) = value :: getValues store

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | (STriangle base height) = 0.5 * base * height
  area (rectangle width height) | (SRectangle width height) = width * height
  area (circle radius) | (SCircle radius) = pi * radius * radius


text:
module Term

-- Simply-typed lambda calculus with
--   (1) natural numbers as the only base type, and
--   (2) general recursion.
-- This calculus is also referred to as PCF.
--
-- Note that variables in the lambda calculus are not
-- named but identified by their de Bruijn index.

%default total
%access public export

---------------------------------------------------
-- Begin: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS

-- Data type 'Ty' represents the types in the
-- simply-typed lambda calculus:
--   (1) Base type 'TyNat' of natural numbers.
--   (2) Type constructor 'TyFun' for forming
--       function types.
data Ty = TyNat | TyFun Ty Ty

-- Simplified syntax for function types:
infixr 10 :->:
(:->:) : Ty -> Ty -> Ty
(:->:) t1 t2 = TyFun t1 t2

-- End: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS
-------------------------------------------------

---------------------------------------------------------
-- Begin: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS

Context : Type
Context = List Ty

-- de Bruijn indices constitute proofs that type
-- 't' occurs at a certain position in context 'ctx':
data HasType : Context -> Ty -> Type where
  First : HasType (t::ctx) t
  Next  : HasType ctx t -> HasType (s::ctx) t

remove : (ctx : Context) -> HasType ctx t -> Context
remove (_::ctx') First     = ctx'
remove (s::ctx') (Next ht) = s::remove ctx' ht

-- End: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS
-------------------------------------------------------

-------------------------------------------------
-- Begin: WELL-TYPED TERMS OF THE LAMBDA CALCULUS

-- Data type of well-typed terms in the
-- simply-typed lambda calculus:
data Term : Context -> Ty -> Type where
  -- Variable:
  -- The data constructor for variables ('Var') takes as
  -- argument a de Bruijn index (of type 'HasType ctx t'),
  -- which is proof that the context 'ctx' contains type
  -- 't' at the position given by the de Bruijn index:
  TVar  : HasType ctx t ->
          Term ctx t
  -- Abstraction:
  -- The data constructor for abstractions ('Abs')
  -- takes as its first (implicit) argument the
  -- type of the variable that is bound by this
  -- abstraction.
  TAbs  : {s : Ty} -> Term (s::ctx) t ->
          Term ctx (s :->: t)
  -- Application:
  TApp  : Term ctx (s :->: t) -> Term ctx s ->
          Term ctx t
  -- Fix-point operator:
  TFix  : Term ctx (t :->: t) ->
          Term ctx t
  -- Constant 'Zero' (natural number):
  TZero : Term ctx TyNat
  -- Successor:
  TSucc : Term ctx TyNat ->
          Term ctx TyNat
  -- Predecessor:
  TPred : Term ctx TyNat ->
          Term ctx TyNat
  -- Test for equality with 'Zero'
  -- (with terms for the "then" and
  -- "else" branches):
  TIfz  : Term ctx TyNat -> Term ctx t -> Term ctx t ->
          Term ctx t

-- End: WELL-TYPED TERMS OF THE LAMBDA CALCULUS
-----------------------------------------------

---------------------------------------
-- Begin: VALUES IN THE LAMBDA CALCULUS

-- The following lambda calculus terms
-- are values (i.e. normal forms for
-- reduction under the "Step" relation):
--   (1) lambda abstractions (that are
--       not applied),
--   (2) the constant 'Zero',
--   (3) the natural number constants
--       (formed by applying 'Succ' to
--       another value).
data Value : Term [] t -> Type where
  VZero : Value TZero
  VSucc : Value e -> Value (TSucc e)
  VAbs  : Value (TAbs e)

valueTerm : {e : Term [] t} -> Value e -> Term [] t
valueTerm {e = e} _ = e

-- End: VALUES IN THE LAMBDA CALCULUS
-------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Data.Algebraic.Graph

%default total
%access public export

data Graph : Type -> Type where
  Empty  : Graph type
  Vertex : (elem : type) -> Graph type
  Overlay : Graph type -> Graph type -> Graph type
  Connect : Graph type -> Graph type -> Graph type

Show type => Show (Graph type) where
  show Empty = "Empty"
  show (Vertex elem) = unwords ["Vertex", show elem]
  show (Overlay x y) = unwords ["Overlay", show x, show y]
  show (Connect x y) = unwords ["Connect", show x, show y]

Functor Graph where
  map func Empty = Empty
  map func (Vertex elem) = Vertex $ func elem
  map func (Overlay x y) = Overlay (map func x) (map func y)
  map func (Connect x y) = Connect (map func x) (map func y)

Foldable Graph where
  foldr func init Empty = init
  foldr func init (Vertex x) = func x init
  foldr func init (Overlay x y) = foldr func (foldr func init y) x
  foldr func init (Connect x y) = foldr func (foldr func init y) x

Traversable Graph where
  traverse func Empty = pure Empty
  traverse func (Vertex elem) = [| Vertex (func elem)|]
  traverse func (Overlay x y) = [| Overlay (traverse func x) (traverse func y) |]
  traverse func (Connect x y) = [| Connect (traverse func x) (traverse func y) |]

Num type => Num (Graph type) where
  fromInteger x = Vertex (fromInteger x)
  (+) = Overlay
  (*) = Connect

-- Do we need abs, negate, and signum?

empty : Graph a
empty = Empty

vertex : a -> Graph a
vertex a = Vertex a

connect : Graph a -> Graph a -> Graph a
connect = Connect

edge : a -> a -> Graph a
edge x y = connect (vertex x) (vertex y)

combine : Graph a -> Graph a -> Graph a
combine = Overlay

overlay : Graph a -> Graph a -> Graph a
overlay = combine

foldg : (init : type)
     -> (whenVertex  : a -> type)
     -> (whenOverlay : type -> type -> type)
     -> (whenConnect : type -> type -> type)
     -> (graph : Graph a)
     -> type
foldg init whenVertex whenOverlay whenConnect = go
  where
    go : Graph a -> type
    go Empty = init
    go (Vertex elem) = whenVertex elem
    go (Overlay x y) = whenOverlay (go x) (go y)
    go (Connect x y) = whenConnect (go x) (go y)

overlays : List (Graph a) -> Graph a
overlays = foldr overlay empty

vertices : List a -> Graph a
vertices = overlays . map vertex

connects : List (Graph a) -> Graph a
connects = foldr connect empty

edges : List (a,a) -> Graph a
edges = overlays . map (uncurry edge)

graph : List a -> List (a,a) -> Graph a
graph vs es = overlay (vertices vs) (edges es)

data HasVertex : (elem : type) -> Graph type -> Type where
  Here : HasVertex e (Vertex e)
  ThereOL : HasVertex e l
         -> HasVertex e (Overlay l r)
  ThereOR : HasVertex e r
         -> HasVertex e (Overlay l r)
  ThereCL : HasVertex e l
         -> HasVertex e (Connect l r)
  ThereCR : HasVertex e r
         -> HasVertex e (Connect l r)

graphIsEmpty : HasVertex e Empty -> Void
graphIsEmpty Here impossible
graphIsEmpty (ThereOL _) impossible
graphIsEmpty (ThereOR _) impossible
graphIsEmpty (ThereCL _) impossible
graphIsEmpty (ThereCR _) impossible

notSameVertex : (contra : (e = x) -> Void) -> HasVertex e (Vertex x) -> Void
notSameVertex contra Here = contra Refl

notOverlay : (contra : HasVertex e x -> Void)
         -> (f : HasVertex e y -> Void)
         -> HasVertex e (Overlay x y)
         -> Void
notOverlay contra f x with (x)
  notOverlay contra f x | (ThereOL y) = contra y
  notOverlay contra f x | (ThereOR y) = f y

notConnect : (contra : HasVertex e x -> Void)
          -> (f : HasVertex e y -> Void)
          -> HasVertex e (Connect x y)
          -> Void
notConnect contra f x with (x)
  notConnect contra f x | (ThereCL y) = contra y
  notConnect contra f x | (ThereCR y) = f y

hasVertex : DecEq type => (elem : type) -> (graph : Graph type) -> Dec (HasVertex elem graph)
hasVertex elem Empty = No graphIsEmpty
hasVertex elem (Vertex x) with (decEq elem x)
  hasVertex x (Vertex x) | (Yes Refl) = Yes Here
  hasVertex elem (Vertex x) | (No contra) = No (notSameVertex contra)

hasVertex elem (Overlay x y) with (hasVertex elem x)
  hasVertex elem (Overlay x y) | (Yes prf) = Yes (ThereOL prf)
  hasVertex elem (Overlay x y) | (No contra) with (hasVertex elem y)
    hasVertex elem (Overlay x y) | (No contra) | (Yes prf) = Yes (ThereOR prf)
    hasVertex elem (Overlay x y) | (No contra) | (No f) = No (notOverlay contra f)

hasVertex elem (Connect x y) with (hasVertex elem x)
  hasVertex elem (Connect x y) | (Yes prf) = Yes (ThereCL prf)
  hasVertex elem (Connect x y) | (No contra) with (hasVertex elem y)
    hasVertex elem (Connect x y) | (No contra) | (Yes prf) = Yes (ThereCR prf)
    hasVertex elem (Connect x y) | (No contra) | (No f) = No (notConnect contra f)

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Datatypes

data Nat = Z | S Nat

data List a = Ni | (::) a (List a)

infixr 10 ::

max_stars_repo_name: aztecrex/try-idris

max_issues_repo_name: aztecrex/try-idris

max_forks_repo_name: aztecrex/try-idris


text:
module Main

import Data.Vect

%flag C "-g3"
%flag C "-ggdb"
%flag C "-O0"

rep : (n : Nat) -> Char -> Vect n Char
rep Z     x = []
rep (S k) x = x :: rep k x

data RLE : Vect n Char -> Type where
     REnd  : RLE []
     RChar : .{k : Nat}
             -> {xs : Vect k Char}
             -> (n : Nat)
             -> (x : Char)
             -> RLE xs
             -> RLE (rep (S n) x ++ xs)

eq : (x : Char) -> (y : Char) -> Maybe (x = y)
eq x y = if x == y then Just (believe_me (Refl {x})) else Nothing

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

rle : (xs : Vect n Char) -> RLE xs
rle [] = REnd
rle (x :: xs) with (rle xs)
   rle (x :: Vect.Nil)             | REnd = RChar Z x REnd
   rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)
     rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just Refl
           = RChar (S n) x rs
     rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing
           = RChar Z x (RChar n y rs)

compress : Vect n Char -> String
compress xs with (rle xs)
  compress Nil                 | REnd         = ""
  compress (rep (S n) x ++ xs) | RChar _ _ rs
         = let ni : Integer = cast (S n) in
               show ni ++ strCons x (compress xs)

{-
fmt : {xs : Vect n Char} -> RLE xs -> String
fmt  REnd          = ""
fmt (RChar n c xs) = show n ++ show c ++ fmt xs
-}

compressString : String -> String
compressString xs = compress (fromList (unpack xs))

main : IO ()
main = putStrLn (compressString "foooobaaaarbaaaz")

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 Main

import Control.App
import Control.App.Console
import Test.Unit.Spec

main : IO ()
main = run $ consoleRunSpec $ do
  describe "test0" $ do
    describe "test0-1" $ do
      tests "aaaaa" $ do
        pure 1 >>= assertEqual 1
      tests "bbb" $ do
        pure True >>= assertTrue
    describe "test0-2" $ do
      tests "aaaaa" $ do
        pure 1 >>= assertEqual 1
      tests "bbb" $ do
        pure True >>= assertTrue
    describe "Boolean" $ do
      describe "Expecting True" $ do
        tests "it is" $ pure True >>= assertTrue
        tests "it isn't" $ pure False >>= assertTrue
      describe "Expecting False" $ do
        tests "it isn't" $ pure True >>= assertFalse
        tests "it is" $ pure False >>= assertFalse
    describe "Maybe" $ do
      describe "Expecting Nothing" $ do
        tests "it is" $ do
          pure (the (Maybe Int) Nothing) >>= assertNothing
        tests "it isn't" $ do
          pure (Just 2) >>= assertNothing
      describe "Expecting Just" $ do
        tests "it isn't" $ do
          pure (the (Maybe Int) Nothing) >>= assertJust
        tests "it is" $ do
          pure (Just 2) >>= assertJust


text:
data Bad = MkBad (Bad -> Int) Int
         | MkBad' Int

foo : Bad -> Int
foo (MkBad f i) = f (MkBad' i)
foo (MkBad' x) = x

foo2 : Bad -> Int
foo2 b = case b of
              MkBad f i => f (MkBad' i)
              MkBad' x => x

data T : Type -> Type where
     MkT : T (T a) -> T a

mutual
  data Bad1 = MkBad1 (Bad2 -> Int)
  data Bad2 = MkBad2 (Bad1 -> Int)

data T2 : Type -> Type where
     MkT2 : T a -> T2 a