text:
> module Subset.Properties

> import Data.Fin
> import Data.Vect
> import Control.Isomorphism

> import Decidable.Predicates
> import Finite.Predicates
> import Unique.Predicates
> import Sigma.Sigma
> import Pairs.Operations
> import Subset.Operations
> import Vect.Operations
> import Vect.Properties
> import Finite.Operations
> import Finite.Properties
> import Fin.Operations
> -- import Isomorphism.Operations
> import Isomorphism.Properties
> import Basic.Operations
> import Basic.Properties

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

Equality of projections:

> ||| Equality of first projections
> getWitnessPreservesEq : {A  : Type} ->
>                         {P  : A -> Type} ->
>                         {s1 : Subset A P} ->
>                         {s2 : Subset A P} ->
>                         (s1 = s2) -> (getWitness s1 = getWitness s2)
> getWitnessPreservesEq {s1 = (Element a p)} {s2 = (Element a p)} Refl = Refl
> %freeze getWitnessPreservesEq

> ||| Equality of second projections
> getProofPreservesEq : {A  : Type} ->
>                       {P  : A -> Type} ->
>                       {s1 : Subset A P} ->
>                       {s2 : Subset A P} ->
>                       (s1 = s2) -> (getProof s1 = getProof s2)
> getProofPreservesEq {s1 = (Element a p)} {s2 = (Element a p)} Refl = Refl
> %freeze getProofPreservesEq

Equality of Subset types:

> ||| Introduction
> subsetEqLemma2 : {A : Type} ->
>                  {P : A -> Type} ->
>                  {s1: Subset A P} ->
>                  {s2: Subset A P} ->
>                  (getWitness s1 = getWitness s2) ->
>                  (getProof s1 = getProof s2) ->
>                  s1 = s2
> subsetEqLemma2 {A} {P} {s1 = (Element a p)} {s2 = (Element a p)} Refl Refl = Refl
> %freeze subsetEqLemma2

> ||| Elimination and formation
> subsetEqLemma0 : {A : Type} ->
>                  {P : A -> Type} ->
>                  (s : Subset A P) ->
>                  s = (Element (getWitness s) (getProof s))
> subsetEqLemma0 (Element a p) = Refl
> %freeze subsetEqLemma0

> ||| Equality for singleton predicates
> subsetEqLemma1 : {A  : Type} ->
>                  {P  : A -> Type} ->
>                  (s1 : Subset A P) ->
>                  (s2 : Subset A P) ->
>                  getWitness s1 = getWitness s2 ->
>                  Unique0 (P (getWitness s1)) ->
>                  s1 = s2
> subsetEqLemma1 (Element a p) (Element a q) Refl uP = cong (uP p q)
> %freeze subsetEqLemma1

Decidability of Subset equality:

> ||| Decidability of equality 1
> subsetDecEqLemma1 : {A : Type} ->
>                     {P : A -> Type} ->
>                     (DecEq0 A) ->
>                     (DecEq1 P) ->
>                     (s1 : Subset A P) ->
>                     (s2 : Subset A P) ->
>                     Dec (s1 = s2)
> subsetDecEqLemma1 da d1p (Element a1 pa1) (Element a2 pa2)     with (da a1 a2)
>   subsetDecEqLemma1 da d1p (Element a1 pa1) (Element a1 pa2)   | (Yes Refl) with ((d1p a1) pa1 pa2)
>     subsetDecEqLemma1 da d1p (Element a1 pa1) (Element a1 pa1) | (Yes Refl) | (Yes Refl) = Yes Refl
>     subsetDecEqLemma1 da d1p (Element a1 pa1) (Element a1 pa2) | (Yes Refl) | (No contra) = No (\ eq => contra (getProofPreservesEq eq))
>   subsetDecEqLemma1 da d1p (Element a1 pa1) (Element a2 pa2)   | (No contra) = No (\ eq => contra (getWitnessPreservesEq eq))
> %freeze subsetDecEqLemma1

> ||| Decidability of equality 2
> subsetDecEqLemma2 : {A : Type} ->
>                     {P : A -> Type} ->
>                     (DecEq A) ->
>                     (Unique1 P) ->
>                     (s1 : Subset A P) ->
>                     (s2 : Subset A P) ->
>                     Dec (s1 = s2)
> subsetDecEqLemma2 da p1P s1 s2 with (decEq (getWitness s1) (getWitness s2))
>   | (Yes prf)   = Yes (subsetEqLemma1 s1 s2 prf (p1P (getWitness s1)))
>   | (No contra) = No (\ eq => contra (getWitnessPreservesEq eq))
> %freeze subsetDecEqLemma2

We want to show that |toVect| is complete

< toVectSubsetComplete : {A   : Type} ->
<                        {P   : A -> Type} ->
<                        (fA  : Finite A) ->
<                        (d1P : Dec1 P) ->
<                        (Unique1 {t0 = A} P) ->
<                        (s   : Subset A P) ->
<                        Elem s (getProof (toVectSubset fA d1P))

We start by deriving two auxiliary results. The first one is

> toVectSubsetLemma : {A : Type} ->
>                     {P : A -> Type} ->
>                     (fA : Finite A) ->
>                     (d1P : Dec1 P) ->
>                     (a : A) ->
>                     (p : P a) ->
>                     Elem a (map Subset.getWitness (Sigma.getProof (toVectSubset fA d1P)))
> toVectSubsetLemma {A} {P} fA d1P a p =
>   filterTagSubsetLemma d1P a (toVect fA) (toVectComplete fA a) p
> %freeze toVectSubsetLemma

The proof is computed by applying |VectProperties.filterTagSubsetLemma|:

< filterTagSubsetLemma : {A : Type} -> {P : A -> Type} ->
<                       (d1P : Dec1 P) ->
<                       (a : A) ->
<                       (as : Vect n A) ->
<                       (Elem a as) ->
<                       (p : P a) ->
<                       Elem a (map getWitness (getProof (filterTagSubset d1P as)))

to |d1P|, |a|, to the vector-based representation of |A| associated to
|fA| provided by |FiniteOperations.toVect fA| and to a proof that |a| is
an element of |FiniteOperations.toVect fA|. The latter follows from
completeness of |toVect|, see |FiniteProperties.toVectComplete|. In this
form, |toVectLemma| does not type check.

The second result is

> subsetUniqueLemma1 : {A   : Type} ->
>                      {P   : A -> Type} ->
>                      (Unique1 P) ->
>                      (a : A) ->
>                      (p : P a) ->
>                      (ss : Vect n (Subset A P)) ->
>                      (Elem a (map Subset.getWitness ss)) ->
>                      Elem (Element a p) ss
> subsetUniqueLemma1 u1P a p Nil prf = absurd prf
> subsetUniqueLemma1 u1P a p ((Element a q) :: ss) (Here {x = a}) with (u1P a p q)
>   subsetUniqueLemma1 u1P a p ((Element a p) :: ss) (Here {x = a}) | Refl =
>     Here {x = (Element a p)} {xs = ss}
> subsetUniqueLemma1 u1P a1 p1 ((Element a2 p2) :: ss) (There prf) =
>   There (subsetUniqueLemma1 u1P a1 p1 ss prf)
> %freeze subsetUniqueLemma1

With |toVectLemma| and |subsetUniqueLemma1|, it is easy to show that
|toVect| is complete:

> toVectSubsetComplete : {A   : Type} ->
>                        {P   : A -> Type} ->
>                        (fA  : Finite A) ->
>                        (d1P : Dec1 P) ->
>                        (Unique1 P) ->
>                        (s   : Subset A P) ->
>                        Elem s (getProof (toVectSubset fA d1P))
> toVectSubsetComplete fA d1P u1P (Element a p) = s1 where
>   s0 : Elem a (map Subset.getWitness (getProof (toVectSubset fA d1P)))
>   s0 = toVectSubsetLemma fA d1P a p
>   s1 : Elem (Element a p) (getProof (toVectSubset fA d1P))
>   s1 = subsetUniqueLemma1 u1P a p (getProof (toVectSubset fA d1P)) s0
> %freeze toVectSubsetComplete

> {-
> toVectSubsetInjective1 : {A   : Type} ->
>                          {P   : A -> Type} ->
>                          (fA  : Finite A) ->
>                          (d1P : Dec1 P) ->
>                          (Unique1 {t0 = A} P) ->
>                          Injective1 (getProof (toVectSubset fA d1P))
> toVectSubsetInjective1 fA dP uP =
>   injectiveFilterTagSubsetLemma dP (toVect fA) (toVectInjective1 fA)
> -}

Subset Fin properties:

> using (P : Fin Z -> Type)
>   implementation Uninhabited (Subset (Fin Z) P) where
>     uninhabited (Element k _) = absurd k

> |||
> isoReplaceLemma1 : {A, A' : Type} ->  {B : A -> Type} -> {B' : A' -> Type} ->
>                    (isoA : Iso A A') ->
>                    (isoBa  : (a : A) -> Iso (B a) (B' (to isoA a)) ) ->
>                    (a' : A') -> (b' : B' a') ->
>                    to (isoBa (from isoA a')) (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b'))
>                    =
>                    b'
> isoReplaceLemma1 isoA isoBa a' b' = trans s1 s2 where
>   s1 : to (isoBa (from isoA a')) (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b'))
>        =
>        (replace (sym (toFrom isoA a')) b')
>   s1 = toFrom (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')
>   s2 : replace (sym (toFrom isoA a')) b' = b'
>   s2 = replaceLemma (sym (toFrom isoA a')) b'
> %freeze isoReplaceLemma1

> |||
> isoReplaceLemma2 : {A, A' : Type} ->  {B : A -> Type} -> {B' : A' -> Type} ->
>                    (isoA : Iso A A') ->
>                    (isoBa  : (a : A) -> Iso (B a) (B' (to isoA a)) ) ->
>                    (a : A) -> (b : B a) ->
>                    from (isoBa (from isoA (to isoA a))) (replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b))
>                    =
>                    b
> isoReplaceLemma2 {A} {A'} {B} {B'} isoA isoBa a b = trans s2 s3 where
>   s1 : replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)
>        =
>        to (isoBa a) b
>   s1 = replaceLemma (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)
>   s2 : from (isoBa (from isoA (to isoA a))) (replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b))
>        =
>        from (isoBa a) (to (isoBa a) b)
>   s2 = depCong2' {alpha = A}
>                  {P = \ a => B' (to isoA a)}
>                  {Q = \ a => \ pa => B a}
>                  {a1 = from isoA (to isoA a)}
>                  {a2 = a}
>                  {Pa1 = replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)}
>                  {Pa2 = to (isoBa a) b}
>                  {f = \ x => \ y => from (isoBa x) y}
>                  (fromTo isoA a)
>                  s1
>   s3 : from (isoBa a) (to (isoBa a) b) = b
>   s3 = fromTo (isoBa a) b
> %freeze isoReplaceLemma2

> |||
> subsetIsoLemma :  (A : Type) -> (A' : Type) ->  (B : A -> Type) -> (B' : A' -> Type) ->
>                   (isoA : Iso A A') ->
>                   (isoBa  : (a : A) -> Iso (B a) (B' (to isoA a)) ) ->
>                   Iso (Subset A B) (Subset A' B')
> subsetIsoLemma A A' B B' isoA isoBa = MkIso toQ fromQ toFromQ fromToQ
>   where toQ      : Subset A  B  -> Subset A' B'
>         toQ   (Element a b)   = (Element (to isoA a) (to (isoBa a) b))
>
>         fromQ    : Subset A' B' -> Subset A  B
>         fromQ (Element a' b') = (Element a b) where
>           a : A
>           a = from isoA a'
>           b : B a
>           b = from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')
>
>         toFromQ  : (ab' : Subset A' B') -> toQ (fromQ ab') = ab'
>         toFromQ  (Element a' b') = trans s1 (trans s2 s3) where
>           s1 : toQ (fromQ (Element a' b'))
>                =
>                toQ (Element (from isoA a') (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')))
>           s1 = Refl
>           s2 : toQ (Element (from isoA a') (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')))
>                =
>                Element (to isoA (from isoA a'))
>                        (to (isoBa (from isoA a')) (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')))
>           s2 = Refl
>           s3 : Element (to isoA (from isoA a'))
>                        (to (isoBa (from isoA a')) (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')))
>                =
>                (Element a' b')
>           s3 = subsetEqLemma2 {s1 = Element (to isoA (from isoA a'))
>                                             (to (isoBa (from isoA a')) (from (isoBa (from isoA a')) (replace (sym (toFrom isoA a')) b')))}
>                               {s2 = (Element a' b')}
>                               (toFrom isoA a')
>                               (isoReplaceLemma1 isoA isoBa a' b')
>
>         fromToQ : (ab  : Subset A  B) -> fromQ (toQ ab) = ab
>         fromToQ (Element a b) = trans s1 (trans s2 s3) where
>           s1 : fromQ (toQ (Element a b))
>                =
>                fromQ (Element (to isoA a) (to (isoBa a) b))
>           s1 = Refl
>           s2 : fromQ (Element (to isoA a) (to (isoBa a) b))
>                =
>                Element (from isoA (to isoA a))
>                        (from (isoBa (from isoA (to isoA a))) (replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)))
>           s2 = Refl
>           s3 : Element (from isoA (to isoA a))
>                        (from (isoBa (from isoA (to isoA a))) (replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)))
>                =
>                (Element a b)
>           s3 = subsetEqLemma2 {s1 = Element (from isoA (to isoA a))
>                                             (from (isoBa (from isoA (to isoA a))) (replace (sym (toFrom isoA (to isoA a))) (to (isoBa a) b)))}
>                               {s2 = (Element a b)}
>                               (fromTo isoA a)
>                               (isoReplaceLemma2 isoA isoBa a b)
> %freeze subsetIsoLemma

> ||| |Subset (Fin Z) P| are void
> voidSubsetFinZ : {P : Fin Z -> Type} -> Iso (Subset (Fin Z) P) Void
> voidSubsetFinZ = MkIso (\x => void (uninhabited x))
>                        (\x => void x)
>                        (\x => void x)
>                        (\x => void (uninhabited x))
> %freeze voidSubsetFinZ

> ||| Decomposition lemma
> subsetEitherLemma : {n : Nat} ->
>                    {P : Fin (S n) -> Type} ->
>                    Iso (Subset (Fin (S n)) P) (Either (P FZ) (Subset (Fin n) (tail P)))
> subsetEitherLemma {n} {P} = MkIso to from toFrom fromTo where
>   to :   Subset (Fin (S n)) P -> Either (P FZ) (Subset (Fin n) (tail P))
>   to (Element FZ j) = Left j
>   to (Element (FS k) j) = Right (Element k j)
>   from : Either (P FZ) (Subset (Fin n) (tail P)) -> Subset (Fin (S n)) P
>   from (Left j) = (Element FZ j)
>   from (Right (Element k j)) = (Element (FS k) j)
>   toFrom : (e : Either (P FZ) (Subset (Fin n) (tail P))) -> to (from e) = e
>   toFrom (Left j) = Refl
>   toFrom (Right (Element k j)) = Refl
>   fromTo : (s : Subset (Fin (S n)) P) -> from (to s) = s
>   fromTo (Element FZ j) = Refl
>   fromTo (Element (FS k) j) = Refl
> %freeze subsetEitherLemma

> |||
> subsetFinEitherLemma : {n : Nat} -> {f : Fin (S n) -> Nat} ->
>                       Iso
>                       (Subset (Fin (S n)) (Fin . f))
>                       (Either (Fin (f FZ)) (Subset (Fin n) (Fin . (tail f))))
> subsetFinEitherLemma {n} {f} =
>     ( Subset (Fin (S n)) (Fin . f)                                     )
>   ={ subsetEitherLemma {n = n} {P = Fin . f} }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (tail (Fin . f)))            )
>   -- ={ isoCong {P = \ X => Either (Fin (f FZ)) (Subset (Fin n) X)} (sym (lambdaLemma1 (tail (Fin . f)))) }=
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (\ k => (tail (Fin . f)) k)) )
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (\ k => (Fin . f) (FS k)))   )
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (\ k => Fin (f (FS k))))     )
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (\ k => Fin ((tail f) k)))   )
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (\ k => (Fin . (tail f)) k)) )
>   -- ={ isoCong {P = \ X => Either (Fin (f FZ)) (Subset (Fin n) X)} (lambdaLemma1 (Fin . (tail f))) }=
>   ={ isoRefl }=
>     ( Either (Fin (f FZ)) (Subset (Fin n) (Fin . (tail f)))            )
>   QED
> %freeze subsetFinEitherLemma

> ||| |finDepPairTimes| for dependent pairs
> finDepPairTimes : {n : Nat} -> {f : Fin n -> Nat} ->
>                   Iso (Subset (Fin n) (Fin . f))
>                       (Fin (sum f))
> finDepPairTimes {n = Z} {f} =
>     ( Subset (Fin Z) (Fin . f)          )
>   ={ voidSubsetFinZ }=
>     ( Void                             )
>   ={ isoSym finZeroBot }=
>     ( Fin Z                            )
>   QED
> finDepPairTimes {n = S m} {f} =
>     ( Subset (Fin (S m)) (Fin . f)                                   )
>   ={ subsetFinEitherLemma }=
>     ( Either (Fin (f FZ)) (Subset (Fin m) (Fin . (tail f)))          )
>   ={ eitherCongRight (finDepPairTimes {n = m} {f = tail f}) }=
>     ( Either (Fin (f FZ)) (Fin (sum (tail f)))                      )
>   ={ eitherFinPlus }=
>     ( Fin (f FZ + sum (tail f))                                     )
>   ={ isoRefl }=
>     ( Fin (sum f)                                                   )
>   QED
> %freeze finDepPairTimes

Subset Exists properties

> |||
> subsetExistsLemma : {A : Type} -> {P : A -> Type} ->
>                    Iso (Subset A P) (Exists P)
> subsetExistsLemma {A} {P} = MkIso to from toFrom fromTo where
>   to : Subset A P -> Exists P
>   to (Element _ p) = Evidence _ p
>   from : Exists P -> Subset A P
>   from (Evidence _ p) = Element _ p
>   toFrom : (e : Exists P) -> to (from e) = e
>   toFrom (Evidence _ _) = Refl
>   fromTo : (s : Subset A P) -> from (to s) = s
>   fromTo (Element _ _) = Refl
> %freeze subsetExistsLemma

Finitess properties

> ||| For finite predicates, Subset types of finite types are finite
> finiteSubsetLemma0 : {A : Type} -> {P : A -> Type} ->
>                      Finite A -> Finite1 P -> Finite (Subset A P)
> finiteSubsetLemma0 {A} {P} (MkSigma n isoA) f1P = MkSigma sumf (isoTrans step1 step2)
>   where  f' : A     -> Nat
>          f' a = card (f1P a)
>          f  : Fin n -> Nat
>          f = f' . from isoA
>          sumf : Nat
>          sumf = sum f
>          step1 : Iso (Subset A P) (Subset (Fin n) (Fin . f))
>          step1 = subsetIsoLemma A (Fin n) P (Fin . f) isoA s5 where -- s6 where
>            s1 : (a : A) -> Iso (P a) (Fin (f' a))
>            s1 a =  iso (f1P a)
>            s2 : (a : A) -> Iso (P a) (Fin (f' (from isoA (to isoA a))))
>            s2 a = replace {P = \ x => Iso (P a) (Fin (f' x))} prf (s1 a) where
>              prf : a = from isoA (to isoA a)
>              prf = sym (fromTo isoA a)
>            s3 : (a : A) -> Iso (P a) (Fin ((f' . (from isoA)) (to isoA a)))
>            s3 = s2
>            s4 : (a : A) -> Iso (P a) (Fin (f (to isoA a)))
>            s4 = s3
>            s5 : (a : A) -> Iso (P a) ((Fin . f) (to isoA a))
>            s5 = s4
>            -- s6 : (k : Fin n) -> Iso (P (from isoA k)) ((Fin . f) k)
>            -- s6 k = iso (f1P (from isoA k))
>          step2 : Iso (Subset (Fin n) (Fin . f)) (Fin sumf)
>          step2 = finDepPairTimes {n} {f}
> %freeze finiteSubsetLemma0

> |||
> finiteExistsLemma : {A : Type} -> {P : A -> Type} ->
>                     Finite A -> Finite1 P -> Finite (Exists {a = A} P)
> finiteExistsLemma {A} {P} fA f1P = MkSigma n iE where
>   fS : Finite (Subset A P)
>   fS = finiteSubsetLemma0 fA f1P
>   n  : Nat
>   n  = card fS
>   iS : Iso (Subset A P) (Fin n)
>   iS = iso fS
>   iE : Iso (Exists {a = A} P) (Fin n)
>   iE = isoTrans (isoSym (subsetExistsLemma {A} {P})) iS
> %freeze finiteExistsLemma

Finite  A           ~= (n ** Iso A (Fin n))
Finite1 P           ~= (a : A) -> (na ** Iso (P a) (Fin na))
Finite (Subset A P)  ~= (sum na ** Iso (Subset A P) (Fin (sum na)))


text:
module Web.Internal.MediasourcePrim

import JS
import Web.Internal.Types

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

namespace MediaSource

  export
  %foreign "browser:lambda:()=> new MediaSource()"
  prim__new : PrimIO MediaSource

  export
  %foreign "browser:lambda:(a)=>MediaSource.isTypeSupported(a)"
  prim__isTypeSupported : String -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.activeSourceBuffers"
  prim__activeSourceBuffers : MediaSource -> PrimIO SourceBufferList

  export
  %foreign "browser:lambda:x=>x.duration"
  prim__duration : MediaSource -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.duration = v}"
  prim__setDuration : MediaSource -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onsourceclose"
  prim__onsourceclose : MediaSource -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onsourceclose = v}"
  prim__setOnsourceclose :  MediaSource
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onsourceended"
  prim__onsourceended : MediaSource -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onsourceended = v}"
  prim__setOnsourceended :  MediaSource
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onsourceopen"
  prim__onsourceopen : MediaSource -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onsourceopen = v}"
  prim__setOnsourceopen :  MediaSource
                        -> Nullable EventHandlerNonNull
                        -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readyState"
  prim__readyState : MediaSource -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.sourceBuffers"
  prim__sourceBuffers : MediaSource -> PrimIO SourceBufferList

  export
  %foreign "browser:lambda:(x,a)=>x.addSourceBuffer(a)"
  prim__addSourceBuffer : MediaSource -> String -> PrimIO SourceBuffer

  export
  %foreign "browser:lambda:x=>x.clearLiveSeekableRange()"
  prim__clearLiveSeekableRange : MediaSource -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.endOfStream(a)"
  prim__endOfStream : MediaSource -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.removeSourceBuffer(a)"
  prim__removeSourceBuffer : MediaSource -> SourceBuffer -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.setLiveSeekableRange(a,b)"
  prim__setLiveSeekableRange : MediaSource -> Double -> Double -> PrimIO ()

namespace SourceBuffer

  export
  %foreign "browser:lambda:x=>x.appendWindowEnd"
  prim__appendWindowEnd : SourceBuffer -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.appendWindowEnd = v}"
  prim__setAppendWindowEnd : SourceBuffer -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.appendWindowStart"
  prim__appendWindowStart : SourceBuffer -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.appendWindowStart = v}"
  prim__setAppendWindowStart : SourceBuffer -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.audioTracks"
  prim__audioTracks : SourceBuffer -> PrimIO AudioTrackList

  export
  %foreign "browser:lambda:x=>x.buffered"
  prim__buffered : SourceBuffer -> PrimIO TimeRanges

  export
  %foreign "browser:lambda:x=>x.mode"
  prim__mode : SourceBuffer -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.mode = v}"
  prim__setMode : SourceBuffer -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onabort"
  prim__onabort : SourceBuffer -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onabort = v}"
  prim__setOnabort : SourceBuffer -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror : SourceBuffer -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror : SourceBuffer -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onupdate"
  prim__onupdate : SourceBuffer -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onupdate = v}"
  prim__setOnupdate : SourceBuffer -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onupdateend"
  prim__onupdateend : SourceBuffer -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onupdateend = v}"
  prim__setOnupdateend :  SourceBuffer
                       -> Nullable EventHandlerNonNull
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onupdatestart"
  prim__onupdatestart : SourceBuffer -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onupdatestart = v}"
  prim__setOnupdatestart :  SourceBuffer
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.textTracks"
  prim__textTracks : SourceBuffer -> PrimIO TextTrackList

  export
  %foreign "browser:lambda:x=>x.timestampOffset"
  prim__timestampOffset : SourceBuffer -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.timestampOffset = v}"
  prim__setTimestampOffset : SourceBuffer -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.updating"
  prim__updating : SourceBuffer -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.videoTracks"
  prim__videoTracks : SourceBuffer -> PrimIO VideoTrackList

  export
  %foreign "browser:lambda:x=>x.abort()"
  prim__abort : SourceBuffer -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.appendBuffer(a)"
  prim__appendBuffer :  SourceBuffer
                     -> Union11 Int8Array
                                Int16Array
                                Int32Array
                                UInt8Array
                                UInt8Array
                                UInt8Array
                                UInt8ClampedArray
                                Float32Array
                                Float64Array
                                DataView
                                ArrayBuffer
                     -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.remove(a,b)"
  prim__remove : SourceBuffer -> Double -> Double -> PrimIO ()

namespace SourceBufferList

  export
  %foreign "browser:lambda:(o,x)=>o[x]"
  prim__get : SourceBufferList -> Bits32 -> PrimIO SourceBuffer

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SourceBufferList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.onaddsourcebuffer"
  prim__onaddsourcebuffer :  SourceBufferList
                          -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onaddsourcebuffer = v}"
  prim__setOnaddsourcebuffer :  SourceBufferList
                             -> Nullable EventHandlerNonNull
                             -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onremovesourcebuffer"
  prim__onremovesourcebuffer :  SourceBufferList
                             -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onremovesourcebuffer = v}"
  prim__setOnremovesourcebuffer :  SourceBufferList
                                -> Nullable EventHandlerNonNull
                                -> PrimIO ()

ext: idr


text:
module Libgit.FFI

import Prelude
import System.FFI

import Libgit.Types

-- FFI string builders

public export
libgit : String -> String
libgit fn = "C:" ++ fn ++ ",libgit2"

public export
libgitWrapper : String -> String
libgitWrapper fn = "C:" ++ fn ++ ",libgit_idris_wrapper"

-- Structs

export
CGitResult : Type
CGitResult = Struct "git_result" [
  ("obj", AnyPtr),
  ("result", Int)
]

export
%foreign "C:free,libc"
prim_free : AnyPtr -> PrimIO ()

%foreign (libgitWrapper "identity")
derefResult : Ptr CGitResult -> CGitResult

export
getGitResultPair : Ptr CGitResult -> IO (Int, AnyPtr)
getGitResultPair cgrPtr = do
  let cgr : CGitResult = derefResult cgrPtr
      err : Int = getField cgr "result"
      ptr : AnyPtr = getField cgr "obj"
  primIO (prim_free (prim__forgetPtr cgrPtr))
  pure (err, ptr)

export
getGitResult : Ptr CGitResult -> IO (GitResult AnyPtr)
getGitResult cgrPtr = do
  (err, ptr) <- getGitResultPair cgrPtr
  case err of
    0 => pure (Right ptr)
    _ => pure (Left err)

public export
CGitError : Type
CGitError = Struct "git_error" [
  ("message", Ptr String),
  ("klass", Int)
]

export
%foreign (libgitWrapper "identity")
derefGitError : Ptr CGitError -> CGitError

-- System info helpers
---- These should be generated by the build system until type providers exist

CUInt : Type
CUInt = Bits32

CSizeT : Type
CSizeT = Bits32

-- FFI functions

export
%foreign (libgitWrapper "make_string")
make_string : String -> Ptr String

export
%foreign (libgitWrapper "is_null")
is_null_string : Ptr String -> Int

export
%foreign (libgitWrapper "is_null")
is_null_ptr : AnyPtr -> Int

export
%foreign (libgitWrapper "get_string")
getString : Ptr String -> String

export
%foreign (libgitWrapper "null_string")
null_string : Ptr String

export
%foreign (libgitWrapper "null_string")
null_ptr : AnyPtr

export
%foreign (libgit "git_libgit2_init")
prim_libgit_init : PrimIO Int

export
%foreign (libgit "git_libgit2_shutdown")
prim_libgit_shutdown : PrimIO Int

export
%foreign (libgitWrapper "apply_clone_options")
prim_apply_clone_options : AnyPtr -> String -> Int -> PrimIO ()

export
%foreign (libgitWrapper "make_clone_options")
prim_init_clone_options : PrimIO AnyPtr

export
%foreign (libgitWrapper "git_clone_options_version")
git_clone_options_version : Int

export
%foreign (libgit "git_clone_init_options")
prim_git_clone_init_options : AnyPtr -> Int -> PrimIO Int

export
%foreign (libgitWrapper "git_clone_repository")
prim_git_clone_repository :  String -> String -> AnyPtr -> PrimIO (Ptr CGitResult)

export
%foreign (libgit "git_repository_free")
prim_git_repository_free : AnyPtr -> PrimIO ()

export
%foreign (libgitWrapper "git_open_repository")
prim_git_open_repository : String -> PrimIO (Ptr CGitResult)

export
%foreign (libgitWrapper "git_checkout_options_init")
git_checkout_options_init : Ptr CGitResult

export
%foreign (libgitWrapper "git_fetch_options_init")
git_fetch_options_init : Ptr CGitResult

export
%foreign (libgit "git_reset")
prim_git_reset : AnyPtr -> AnyPtr -> Int -> AnyPtr -> PrimIO Int

export
%foreign (libgitWrapper "git_oid_from_string")
git_oid_from_string : String -> Ptr CGitResult

export
%foreign (libgitWrapper "git_oid_to_string")
git_oid_to_string : AnyPtr -> String

export
%foreign (libgitWrapper "git_lookup_object")
git_lookup_object : AnyPtr -> AnyPtr -> Int -> Ptr CGitResult

export
%foreign (libgitWrapper "git_single_revparse")
prim_git_single_revparse : AnyPtr -> String -> PrimIO (Ptr CGitResult)

export
%foreign (libgit "git_object_free")
prim_git_object_free : AnyPtr -> PrimIO ()

export
%foreign (libgit "git_object_type")
git_object_type : AnyPtr -> Int

export
%foreign (libgitWrapper "git_lookup_remote")
git_lookup_remote : AnyPtr -> String -> Ptr CGitResult

export
%foreign (libgit "git_remote_free")
prim_git_remote_free : AnyPtr -> PrimIO ()

export
%foreign (libgit "git_remote_fetch")
prim_git_remote_fetch : AnyPtr -> AnyPtr -> AnyPtr -> Ptr String -> PrimIO Int

export
%foreign (libgit "giterr_last")
git_error_last : Ptr CGitError

export
liftPIO : (HasIO m) => PrimIO a -> m a
liftPIO action = liftIO (primIO action)

export
cBool : Bool -> Int
cBool True = 1
cBool False = 0

max_forks_repo_name: bigs/libgit-idris


text:
module Main

import Helper

allowedChars : List Char
allowedChars = ['a'..'z'] ++ ['0'..'9'] ++ ['-']

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

--validLiteral : Test LiteralRoute
--validLiteral = Check ( Literal "seo-friendly" ) -- must compile

--emptyLiteral : Test LiteralRoute
--emptyLiteral = Check ( Literal "" ) -- must not compile

--invalidLiteral : Test LiteralRoute
--invalidLiteral = Check ( Literal "not-$sEo-{fRi3ndLy}" ) -- must not compile

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
module Control.Monad.Ideal.Free

import Control.Monad.Ideal

%access public
%default total

Free : (Type -> Type) -> (Type -> Type) -- 大文字で始まるシンボルは前方参照解決してくれないっぽい？

data Liberty : (Type -> Type) -> Type -> Type where
  ToLiberty : {f : Type -> Type} -> {a : Type} -> (f (Free f a)) -> Liberty f a

Free f = Ideal $ Liberty f

free : Functor f => f (Free f a) -> Free f a
free f = I $ ToLiberty f

instance Functor f => Functor (Liberty f) where
  map g (ToLiberty fa) = ToLiberty $ map (?gg) fa

instance Functor f => Mu' (Liberty f) where
  mu' (ToLiberty fa) = ToLiberty $ map (?ff) fa

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module Data.Time.LocalTime.TimeOfDay

import Data.So
import Data.Maybe

import Data.Fixed
import Data.Rational
import Data.Time.Clock.DiffTime
import Data.Time.LocalTime.TimeZone
import Text.Format.Decimal

import Generics.Derive

%default total
%language ElabReflection

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

public export
record TimeOfDay where
  constructor MkTimeOfDay
  hour : Int
  min : Int
  sec : Fixed 12
%runElab derive "TimeOfDay" [Generic, Eq, Ord, DecEq]

public export
Show TimeOfDay where
  show x = let fmt = zeroPad 2
    in format' fmt x.hour ++ (format' fmt x.min) ++ (format' fmt x.sec)

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

||| Hour zero
export midnight : TimeOfDay
midnight = MkTimeOfDay 0 0 0

||| Hour twelve
export midday : TimeOfDay
midday = MkTimeOfDay 12 0 0

export makeTimeOfDayValid : Int -> Int -> Fixed 12 -> Maybe TimeOfDay
makeTimeOfDayValid h m s =
  toMaybe (h < 0 || h > 22 || m < 0 || m > 59 || s < 0 || s >= 61) $ MkTimeOfDay h m s

||| Convert a period of time into a count of days and a time of day since midnight.
||| The time of day will never have a leap second.
export timeToDaysAndTimeOfDay : DiffTime' isnominal -> (Integer, TimeOfDay)
timeToDaysAndTimeOfDay dt = let
  sixty = the (Fixed 12) 60
  m  = dt.seconds `div'` sixty
  h  = m `div` 60
  d  = h `div` 24
  in (d, MkTimeOfDay (cast $ h `mod` 24) (cast $ m `mod` 60) (dt.seconds `mod'` sixty))

||| Convert a count of days and a time of day since midnight into a period of time.
export daysAndTimeOfDayToTime : Integer -> TimeOfDay -> NominalDiffTime
daysAndTimeOfDayToTime d (MkTimeOfDay dh hm ms) =
  SecondsToDiffTime $ ms + fromInteger (cast hm * 60 + cast dh * 3600 + d * (24 * 3600))

||| Convert a time of day in UTC to a time of day in some timezone, together with a day adjustment.
export utcToLocalTimeOfDay : TimeZone -> TimeOfDay -> (Integer, TimeOfDay)
utcToLocalTimeOfDay zone (MkTimeOfDay h m s) = let
  m' = m + zone.minutes
  h' = h + (div m' 60)
  in (cast (div h' 24), MkTimeOfDay (mod h' 24) (mod m' 60) s)

||| Convert a time of day in some timezone to a time of day in UTC, together with a day adjustment.
export localToUTCTimeOfDay : TimeZone -> TimeOfDay -> (Integer, TimeOfDay)
localToUTCTimeOfDay zone = utcToLocalTimeOfDay (minutesToTimeZone (negate zone.minutes))

||| Get the time of day given a time since midnight.
||| Time more than 24h will be converted to leap-seconds.
export timeToTimeOfDay : DiffTime' isnominal -> TimeOfDay
timeToTimeOfDay dt =
  if dt.seconds >= nominalDay.seconds
     then MkTimeOfDay 23 59 $ 60 + (dt.seconds - nominalDay.seconds)
     else let
       m = dt.seconds `div'` 60
       in MkTimeOfDay (cast $ m `div` 60) (cast $ m `mod` 60) (dt.seconds `mod'` 60)

||| Same as 'timeToTimeOfDay'.
export pastMidnight : DiffTime -> TimeOfDay
pastMidnight = timeToTimeOfDay

||| Get the time since midnight for a given time of day.
export timeOfDayToTime : TimeOfDay -> DiffTime
timeOfDayToTime (MkTimeOfDay h m s) =
  SecondsToDiffTime $ s + fromInteger (cast m * 60 + cast h * 3600)

||| Same as 'timeOfDayToTime'.
export sinceMidnight : TimeOfDay -> DiffTime
sinceMidnight = timeOfDayToTime

||| Get the time of day given the fraction of a day since midnight.
export dayFractionToTimeOfDay : Rational -> Maybe TimeOfDay
dayFractionToTimeOfDay df =
  map (timeToTimeOfDay . the NominalDiffTime . SecondsToDiffTime) $ cast (df * 86400)

||| Get the fraction of a day since midnight given a time of day.
export timeOfDayToDayFraction : TimeOfDay -> Rational
timeOfDayToDayFraction tod = let
  MkFixed num = (timeOfDayToTime tod).seconds
  MkFixed den = nominalDay.seconds
  _ = the (So (den /= 0)) $ believe_me Oh
  in num %: den

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


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.HTML.HTMLScriptElement

import IdrisScript

%access public export
%default total

record HTMLScriptElement where
  constructor New
  text : String

htmlScriptElementFromPointer : (ref : JSRef) -> JS_IO $ Maybe HTMLScriptElement
htmlScriptElementFromPointer ref = case !maybeText of
    Nothing     => pure Nothing
    (Just text) => pure $ Just $ New text
  where
    maybeText : JS_IO $ Maybe String
    maybeText = let
        getText = jscall "%0.text" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getText) of
             (JSString ** str) => pure $ Just $ fromJS str
             _                 => pure Nothing

max_stars_repo_name: blau-io/idris-html

max_issues_repo_name: blau-io/idris-html

max_forks_repo_name: blau-io/idris-html


text:
module Rationals

import NonZeroInt

-- contrib
import Control.Algebra

%access export
%default total

private
record FreeRational where
  constructor MkFreeRational
  num : Int
  den : NonZeroInt

Rational : Type
Rational = FreeRational

rational : Int -> NonZeroInt -> Rational
rational = MkFreeRational

intAsRational : Int -> Rational
intAsRational n = rational n (MkNonZeroInt 1 oneNotZero)
  where
    distinguish : Int -> Type
    distinguish 0 = Void
    distinguish _ = ()
    oneNotZero = \oneEqualsZero => replace {P=distinguish} oneEqualsZero ()

postulate
rationalQuotient :
     (num1, num2 : Int)
  -> (den1, den2 : NonZeroInt)
  -> (num1 * (num den2) = num2 * (num den1))
  -> rational num1 den1 = rational num2 den2

fold :
     (map : Int -> NonZeroInt -> a)
  -> ( (num1, num2 : Int)
    -> (den1, den2 : NonZeroInt)
    -> (num1 * (num den2) = num2 * (num den1))
    -> map num1 den1 = map num2 den2)
  -> Rational
  -> a
fold map mapCoherence (MkFreeRational num den) = map num den

-- operations on rationals

rationalEq : Rational -> Rational -> Bool
rationalEq (MkFreeRational num1 den1) (MkFreeRational num2 den2) = num1 * (num den2) == num2 * (num den1)

implementation Eq Rational where
  (==) = rationalEq

rationalCompare : Rational -> Rational -> Ordering
rationalCompare (MkFreeRational num1 den1) (MkFreeRational num2 den2) = compare (num1 * (num den2)) (num2 * (num den1))

implementation Ord Rational where
  compare = rationalCompare

rationalAddition : Rational -> Rational -> Rational
rationalAddition (MkFreeRational num1 den1) (MkFreeRational num2 den2) = MkFreeRational
  (num1 * (num den2) + num2 * (num den1)) (productOfNonZeroIsNonZero den1 den2)

[additiveRationalSemigroup] Semigroup Rational where
  (<+>) = rationalAddition

-- the additive monoid is actually unlawful
-- because, in Rational, 0/m + 0/n = 0/(m * n)
-- so the identity laws do not hold
[additiveRationalMonoid] Monoid Rational using additiveRationalSemigroup where
  neutral = intAsRational 0

rationalOpposite : Rational -> Rational
rationalOpposite (MkFreeRational num1 den1) = MkFreeRational (-num1) den1

[additiveRationalGroup] Group Rational using additiveRationalMonoid where
  inverse = rationalOpposite

[additiveRationalAbelianGroup] AbelianGroup Rational using additiveRationalGroup where

rationalMultiplication : Rational -> Rational -> Rational
rationalMultiplication (MkFreeRational num1 den1) (MkFreeRational num2 den2) =
  MkFreeRational (num1 * num2) (productOfNonZeroIsNonZero den1 den2)

[multiplicativeRationalSemigroup] Semigroup Rational where
  (<+>) = rationalMultiplication

[multiplicativeRationalMonoid] Monoid Rational using multiplicativeRationalSemigroup where
  neutral = intAsRational 1

[rationalRing] Ring Rational using additiveRationalAbelianGroup where
  (<.>) = rationalMultiplication

[rationalRingWithUnity] RingWithUnity Rational using rationalRing where
  unity = intAsRational 1

IsNonZero : Rational -> Type
IsNonZero (MkFreeRational 0 den) = Void
IsNonZero a                      = Not (num a = 0)

rationalReciprocal : (a : Rational) -> {auto isNonZero : IsNonZero a} -> Rational
rationalReciprocal (MkFreeRational num1 den1) {isNonZero} = MkFreeRational (num den1) den
  where
    den = MkNonZeroInt num1 (\num1IsZero => replace {P=\n => IsNonZero (MkFreeRational n den1)} num1IsZero isNonZero)

-- the fact that the additive monoid in unlawful forbids us to define a field instance
-- because we have more that one zero

max_stars_repo_name: marcosh/idris-rationals

max_issues_repo_name: marcosh/idris-rationals

max_forks_repo_name: marcosh/idris-rationals


text:
module Data.Fuel

%default total

||| Fuel for running total operations potentially indefinitely.
public export
data Fuel = Dry | More (Lazy Fuel)

||| Provide `n` units of fuel.
export
limit : Nat -> Fuel
limit  Z    = Dry
limit (S n) = More (limit n)

||| Provide fuel indefinitely.
||| This function is fundamentally partial.
partial
export
forever : Fuel
forever = More forever


text:
module Main

import Data.Buffer
import System.File

import Sixel
import Sixel.Library

%foreign (c "fwrite")
fwrite : (buf : AnyPtr) -> (size : Int) -> (elems : Int) -> (file : AnyPtr) -> PrimIO Int

||| Writer callback for sixel_output_new.
writer : (buf : AnyPtr) -> (size : Int) -> (priv : AnyPtr) -> PrimIO Int
writer buf size priv = fwrite buf 1 size priv

||| Get the FILE* handle of an Idris file.
getHandle : File -> FilePtr
getHandle (FHandle fh) = fh

||| Swaps the endianness of a buffer.
swap : Buffer -> IO ()
swap buf = if !(getByte buf 7) == 0xFF then pure () else do
  size <- rawSize buf
  go buf 0 (size - 1)
  where go : Buffer -> Int -> Int -> IO ()
        go buf start end =
          if start >= end
             then pure ()
             else do
               first <- getBits8 buf start
               last  <- getBits8 buf end
               setBits8 buf end first
               setBits8 buf start last
               go buf (start + 1) (end - 1)

||| Frees unmanaged memory for main.
cleanup : List Buffer -> IO ()
cleanup bufs = do
  _ <-  traverse freeBuffer bufs
  pure ()

||| File input.
filename : String
filename = "sample_1920×1280.bmp"

main : IO ()
main = do
  Right image <- createBufferFromFile filename
    | Left error => putStrLn ("Could not open sample bitmap: " ++ show error)

  offset <- cast {to=Int} <$> getBits32 image 14
  width  <- cast {to=Int} <$> getBits32 image 18
  height <- cast {to=Int} <$> getBits32 image 22

  Just (header, pixels) <- splitBuffer image offset
    | Nothing => cleanup [image] >> putStrLn ("Could not extract pixel data from " ++ filename)
  swap pixels

  Right output <- MkOutput writer {priv=getHandle stdout}
    | Left error => cleanup [pixels, header, image] >> putStrLn getAdditionalMessage
  Right dither <- MkDither {ncolors=256}
    | Left error => cleanup [pixels, header, image] >> putStrLn getAdditionalMessage
  Right _ <- initialize dither pixels width height PixelFormatRgb888 LargeNorm RepAverageColors QualityFull
    | Left error => cleanup [pixels, header, image] >> putStrLn getAdditionalMessage
  Right _ <- encode pixels width height 1 dither output
    | Left error => cleanup [pixels, header, image] >> putStrLn getAdditionalMessage

  cleanup [pixels, header, image]

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
import Data.List -- for testing using sort

data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False

occurrences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurrences item [] = 0
occurrences item (x :: xs) = case item == x of
                                  False => occurrences item xs
                                  True => 1 + occurrences item xs

-- 7.1 exercises

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

area : Shape -> Double
area (Triangle b h) = b * h * 0.5
area (Rectangle w h) = w * h
area (Circle r) = pi * pow r 2

Eq Shape where
    (==) (Triangle b h) (Triangle b' h') = b == b' && h == h'
    (==) (Rectangle w h) (Rectangle w' h') = w == w' && h == h'
    (==) (Circle r) (Circle r') = r == r'
    (==) _ _ = False

Ord Shape where
    compare x y = compare (area x) (area y)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]


text:
module Main

import Vimscript.FFI
import Vimscript.List
import Vimscript.Builtins

printWith : (String -> VIM_IO ()) -> String -> VIM_IO ()
printWith f s =
  f (s ++ "!")

numbers : VimList Int
numbers =
  let l1 = cons 1 (cons 2 empty)
      l2 = snoc (snoc empty 3) 4
  in concat l1 l2

-- Construct a regular List of Strings.
idrisList : List String
idrisList = do
  hi <- ["Hi", "Hello", "Greetings"]
  who <- ["world", "Vim", "Idris"]
  pure (hi ++ ", " ++ who ++ "!")

l3 : VimList (VimList String)
l3 = fromFoldable (map fromFoldable (the (List (List String)) [["Hi", "there"]]))

main : VIM_IO ()
main = do
  -- THINGS YOU CAN DO:

  -- Weird shit like this:
  set (Background Dark)

  -- Or even more scary:
  execute "echo 'Any Vim code!'"

  -- Regular Vimmy stuff:
  l <- line "$"
  s <- getline (l - 1)
  let sl = length s

  -- Of course, higher-order functions:
  printWith echo (substr 3 (3 + sl) s)

  -- Echo things:
  echo numbers

  -- Convert an Idris List to a VimList:
  let greetings = fromFoldable (the (List String) idrisList)

  -- Add the to end of the current buffer:
  appendLines l greetings

  -- Echo a nested listed:
  echo l3

max_stars_repo_name: owickstrom/idris-vimscript

max_issues_repo_name: owickstrom/idris-vimscript

max_forks_repo_name: owickstrom/idris-vimscript


text:
module Test.Test

import IdrTest.Test
import IdrTest.Expectation

import Main

export
suite : Test
suite =
  describe "Idris2Rust tests"
    [ test "1 == 1" (\_ => assertEq 1 1 )
    ]


text:
module OfficialCrashCourse.FTypes

import OfficialCrashCourse.DTypes

-- Function Types

isHero : NatNum -> Bool
isHero Hero = True
isHero _ = False

isSucc : NatNum -> Bool
isSucc (Succ _) = True
isSucc _ = False

equalNum : NatNum -> NatNum -> Bool
equalNum Hero Hero = True
equalNum Hero (Succ x) = False
equalNum (Succ x) Hero = False
equalNum (Succ x) (Succ y) = equalNum x y

toNumeric : NatNum -> Integer
toNumeric Hero = 0
toNumeric (Succ x) = 1 + toNumeric x

fromNumeric : Integer -> NatNum
fromNumeric x =  case x <= 0 of
                    True => Hero
                    False => Succ (fromNumeric (x - 1))

pred: NatNum -> Maybe NatNum
pred (Succ Hero) = Just Hero
pred Hero = Nothing
pred (Succ x) = Just x

min : NatNum -> NatNum -> NatNum
min Hero y = Hero
min (Succ x) Hero = Hero
min (Succ x) (Succ y) = Succ (min x y)

max: NatNum -> NatNum -> NatNum
max x y = let small = min x y in if equalNum small x then y else x

max' : NatNum -> NatNum -> NatNum
max' Hero y = y
max' (Succ x) Hero = Succ x
max' (Succ x) (Succ y) = Succ (max' x y)

addition : NatNum -> NatNum -> NatNum
addition Hero y = y  -- adding a Nat to Zero yields the same Nat
addition (Succ x) y = Succ (addition x y)
-- adding a Successor of a Nat to another Nat
-- is the same as Successor of addition of those same Nats

nthFibonacci : NatNum -> NatNum
nthFibonacci Hero = Hero
nthFibonacci (Succ Hero) = Succ Hero
nthFibonacci (Succ (Succ x)) = let succFib = nthFibonacci (Succ x);
                                    xFib = nthFibonacci x
                                in addition succFib xFib

multiplication : NatNum -> NatNum -> NatNum
multiplication Hero y = Hero
multiplication (Succ x) y = addition y (multiplication x y)

exponentiation : NatNum -> NatNum -> NatNum
exponentiation _ Hero = Succ Hero
exponentiation x (Succ Hero) = x
exponentiation x (Succ y) = multiplication x (exponentiation x y)

nthFactorial : NatNum -> NatNum
nthFactorial Hero = Succ Hero
nthFactorial (Succ Hero) = Succ Hero
nthFactorial (Succ x) = multiplication (Succ x) (nthFactorial x)

--inequalities
--ordering
--n-tiered pascal's triangle

-- where clause for local definitions
reversal : List a -> List a
reversal xs = revAcc [] xs where
    revAcc: List a -> List a -> List a
    revAcc acc [] = acc
    revAcc acc (x :: xs) = revAcc (x :: acc) xs

-- type constraint for equality check guarantee
zipEq : Eq a => List a -> List a -> Bool
zipEq [] [] = True
zipEq [] (x :: xs) = False
zipEq (x :: xs) [] = False
zipEq (x :: xs) (y :: ys) = if x == y then zipEq xs ys else False

-- more flexible version of zipEq
zipWith : Ord a => (a -> a -> Bool) -> List a -> List a -> Bool
zipWith f [] [] = True
zipWith f [] xs = False
zipWith f xs [] = False
zipWith f (x :: xs) (y :: ys) = if f x y then zipWith f xs ys else False

equal: Eq a => a -> a -> Bool
equal x y = x == y

isNonEmpTea : List a -> Bool
isNonEmpTea [] = False
isNonEmpTea _ = True

-- List String = [], List Num = []
headElem: List a -> Maybe a  -- such that a is the first element of the list
headElem [] = Nothing
headElem (x :: xs) = Just x

listLen : List a -> Integer
listLen [] = 0
listLen (x :: xs) = 1 + listLen xs

lastElem: List a -> Maybe a
lastElem [] = Nothing
lastElem (x :: xs) = if (listLen xs > 0) then lastElem xs else Just x
-- to optimize, use if xs == [] then ...
-- adjusting the value to some number other than 0 e.g. to get the elem at nth place needs some thought to be put into it
-- think of the extra checks you might be missing regarding the list index and being within the bounds

isPalindrome : Ord a => List a -> Bool
isPalindrome [] = True
isPalindrome xs = zipWith equal xs (reversal xs) -- or zipEq xs (reversal xs)

gt: Ord a => a -> a -> Bool
gt x y = x > y

-- Given two lists, find out whether every element of
-- first list is greater than the corresponding element of the second list
isItemwiseGreater : Ord a => List a -> List a -> Bool
isItemwiseGreater [] [] = True
isItemwiseGreater xs ys = zipWith gt xs ys

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
module Python.Lib.Os

import Python

%access public export
%default total

Os : Signature
Os f = case f of
  "mkdir" => [String] ~~> Unit
  _ => Module f

import_ : PIO (Obj Os)
import_ = importModule "os"

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
||| `Flexidisc` is an implementation of extensible records in Idris.
|||
||| It's goal is to provide easy to write extensible record functions that
||| ensure the following:
|||
||| - **Type safety:** operation on row and access to row data is type safe.
||| - **Compile time validation:** row existence and unicity of row
|||   declarations are checked at compile time.
||| - **Lean syntax:** Take advantage of the list syntax as much as possible,
|||   minimize the type declarations as well.
||| - **Custom keys:** Row labels can be any type that implements the `DecEq`
|||   and `Ord` interface.
module Flexidisc

import public Flexidisc.Record
import public Flexidisc.Record.Connection
import public Flexidisc.Record.Transformation
import public Flexidisc.RecordList

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Dart.Core.Set

import Dart.FFI.Elab
import Dart.Core

%language ElabReflection

%runElab importDart [
  package "dart:core" [
    partial' $
      generic ["e"] $
        class' "Set" [
          io "bool" "contains" ["element" :: "e"]
        ]
  ]
]


text:
module Web.Raw.Visibility

import JS
import Web.Internal.VisibilityPrim
import Web.Internal.Types


text:
module NCurses

import public Data.So
import NCurses.Core
import public NCurses.Types

%default total

||| The current state of the NCurses configuration
public export
record Config where
  constructor MkConfig
  noDelayEnabled : Bool
  keypadEnabled  : Bool
  colorEnabled   : Bool

public export
setNoDelay : (enable : Bool) -> Config -> Config
setNoDelay b (MkConfig _ ke ce) = MkConfig b ke ce

public export
setKeypad : (enable : Bool) -> Config -> Config
setKeypad b (MkConfig nd _ ce) = MkConfig nd b ce

public export
setColor : Config -> Config
setColor (MkConfig nd ke _) = MkConfig nd ke True

namespace Config

  ||| Initial configuration when you start running a freshly initialised
  ||| ncurses computation
  public export
  init : Config
  init = MkConfig
    { noDelayEnabled = False
    , keypadEnabled  = False
    , colorEnabled   = False
    }

||| An `io a` computation involving ncurses primitives.
||| @ noDelayIn  records whether `noDelay` is `True` before the action is run
||| @ noDelayOut records whether `noDelay` is `True` after the action was run
|||
||| This is not `public export` *on purpose* so that the only way to run such
||| a computation is via `runNCurses` which makes sure things are properly
||| initialised and cleaned up afterwards.
export
record NCursesT
  (io : Type -> Type)
  (inC, outC : Config)
  (a : Type) where
  constructor MkNCurses
  getNCurses : io a

||| The constructor is not exported so we provide a `lift` function to embed an
||| `io a` computation into an `NCursesT` one.
export
lift : io a -> NCursesT io i i a
lift = MkNCurses

||| The function to use to turn a computation using ncurses primitives into an
||| IO computation that properly initialises & deinitialises the ncurses lib.
||| Note that we know that we always start with `noDelay` off and do not care
||| about the end state.
export
runNCurses : HasIO io => NCursesT io Config.init i a -> io a
runNCurses (MkNCurses act) = withNCurses act

||| Convenient alias when the underlying IO monad is IO itself and the indices
||| can be inferred.
public export
NCurses : (inC, outC : Config) -> Type -> Type
NCurses = NCursesT IO

--------------------------------------------------------------------------------
-- Indexed Functor, Applicative, Monad
-- These do not fit the usual hierarchy so unfortunately we cannot reuse the
-- existing interfaces. We could perhaps define `IFunctor` & friends.
--------------------------------------------------------------------------------

||| Mapping a function over the result of an ncurses computation.
||| If the `io` abides by the functor laws then so will this.
export
map : Functor io => (a -> b) -> NCursesT io i j a -> NCursesT io i j b
map f (MkNCurses act) = MkNCurses (f <$> act)

||| Alias for `map`
export
(<$>) : Functor io => (a -> b) -> NCursesT io i j a -> NCursesT io i j b
(<$>) = map

||| Returning a constant value after running the ncurses computation
export
(<$) : Functor io => b -> NCursesT io i j a -> NCursesT io i j b
(<$) = map . const

||| Ignoring the returned value of an ncurses computation. We cannot use the
||| standard libraries' `ignore` because it relies on `Functor`.
export
ignore : Functor io => NCursesT io i j a -> NCursesT io i j ()
ignore = (() <$)

||| Returning a pure value as a trivial ncurses computation.
||| If the `io` abides by the applicative laws then so will this.
export
pure : Applicative io => a -> NCursesT io i i a
pure = MkNCurses . pure

||| Only run the ncurses computation if the boolean is True.
export
when : Applicative io => Bool -> Lazy (NCursesT io i i ()) -> NCursesT io i i ()
when True act = act
when False _ = pure ()

||| Combining an ncurses computation returning a function and one returning an
||| argument for it.
||| We are using a `Monad io` constraint so that we can guarantee that the the
||| computation returning the function is run first. This specific ordering is
||| crucial to ensure that the i-to-j-to-k ordering demanded by the indices is
||| respected.
export
(<*>) : Monad io =>
        NCursesT io i j (a -> b) -> NCursesT io j k a ->
        NCursesT io i k b
MkNCurses mf <*> MkNCurses mx = MkNCurses (mf >>= \ f => (f $) <$> mx)

||| Sequencing two ncurses computations.
export
(>>=) : Monad io =>
        NCursesT io i j a -> (a -> NCursesT io j k b) ->
        NCursesT io i k b
MkNCurses mx >>= f = MkNCurses (mx >>= getNCurses . f)

||| Sequencing two ncurses computations, the first of which only computes
||| a value of type Unit.
export
(>>) : Monad io =>
       NCursesT io i j a -> NCursesT io j k b ->
       NCursesT io i k b
ma >> mb = ma >>= const mb

--------------------------------------------------------------------------------
-- Ncurses primitives. This time with interesting indices!
--------------------------------------------------------------------------------

||| Return type of `getCh`.
||| 1. Return either a character or potentially a key if the keypad is enabled
||| 2. Block until an input arrives or return immediately if noDelay is enalbed
|||    In that second scenario, if the FIFO is empty then return `Nothing`.
public export
GetCh : Config -> Type
GetCh cfg = ifThenElse cfg.noDelayEnabled Maybe Prelude.id
          $ ifThenElse cfg.keypadEnabled  (Either Key Char) Char

asKey : HasIO io => (b : Bool) -> Char ->
        io (ifThenElse b (Either Key Char) Char)
asKey False c = pure c
asKey True c = do Nothing <- isKey c
                    | Just k => pure (Left k)
                  pure (Right c)

||| Get a character from the FIFO. The return type is heavily dependent on the
||| current configuration of the ncurses computation. See `GetCh` for more
||| information.
export
getCh : {i : Config} -> HasIO io => NCursesT io i i (GetCh i)
getCh {i = MkConfig True b _}  = MkNCurses $ do
   i <- Core.getChAsInt8
   let True = 0 <= i
       | False => pure Nothing
   Just <$> asKey b (cast i)
getCh {i = MkConfig False b _} = MkNCurses $ do
  c <- Core.getCh
  asKey b c

||| Set `noDelay` to the boolean value passed.
||| This will have an action on the type of any `getCh` action run afterwards.
export
noDelay : HasIO io => (b : Bool) -> NCursesT io i (setNoDelay b i) ()
noDelay b = MkNCurses  (Core.noDelay b)

||| Turn echoing off so that user-inputed characters do not show up in the
||| terminal.
export
noEcho : HasIO io => NCursesT io i i ()
noEcho = MkNCurses Core.noEcho

||| Switch keyboard input to cbreak mode. That is to say that the FIFO of input
||| characters is filled in as soon as they are typed rather than on every
||| newline character.
export
cBreak : HasIO io => NCursesT io i i ()
cBreak = MkNCurses Core.cBreak

||| Get the standard window's size
export
getSize : HasIO io => NCursesT io i i Size
getSize = MkNCurses $ do Core.getSize !stdWindow

||| Refresh the standard window.
export
refresh : HasIO io => NCursesT io i i ()
refresh = MkNCurses Core.refresh

||| Clear the standard window.
export
clear : HasIO io => NCursesT io i i ()
clear = MkNCurses Core.clear

||| Move the cursor in the standard window.
export
nMoveCursor : HasIO io => Position -> NCursesT io i i ()
nMoveCursor pos = MkNCurses (Core.nMoveCursor pos.row pos.col)

||| Move the cursor and insert a char in the standard window
export
mvAddCh : HasIO io => Position -> Char -> NCursesT io i i ()
mvAddCh pos c = MkNCurses (Core.mvAddCh pos.row pos.col c)

||| Move the cursor and get the char under it in the standard window
export
mvInCh : HasIO io => Position -> NCursesT io i i Char
mvInCh pos = MkNCurses (Core.mvInCh pos.row pos.col)

||| Print a horizontal line in the standard window
||| @ c is the character the line is made of
||| @ n is the length of the line
export
hLine : HasIO io => (c : Char) -> (n : Nat) -> NCursesT io i i ()
hLine c n = MkNCurses (Core.hLine c n)

||| Print a vertical line in the standard window
||| @ c is the character the line is made of
||| @ n is the length of the line
export
vLine : HasIO io => (c : Char) -> (n : Nat) -> NCursesT io i i ()
vLine c n = MkNCurses (Core.vLine c n)

||| Move the cursor and print a horizontal line in the standard window
||| @ c is the character the line is made of
||| @ n is the length of the line
export
mvHLine : HasIO io => Position -> (c : Char) -> (n : Nat) -> NCursesT io i i ()
mvHLine pos c n = MkNCurses (Core.mvHLine pos.row pos.col c n)

||| Move the cursor and print a vertical line in the standard window
||| @ c is the character the line is made of
||| @ n is the length of the line
export
mvVLine : HasIO io => Position -> (c : Char) -> (n : Nat) -> NCursesT io i i ()
mvVLine pos c n = MkNCurses (Core.mvVLine pos.row pos.col c n)

||| Move the cursor
export
move : HasIO io => Position -> NCursesT io i i ()
move pos = MkNCurses (Core.nMoveCursor pos.row pos.col)

||| Move the cursor and print to the standard window.
export
mvPrint : HasIO io => Position -> String -> NCursesT io i i ()
mvPrint pos str = MkNCurses (Core.mvPrint pos.row pos.col str)

||| Set the visibility of the cursor.
export
setCursorVisibility : HasIO io => CursorVisibility -> NCursesT io i i ()
setCursorVisibility vis = MkNCurses (Core.setCursorVisibility vis)

||| Turn keypad mode on or off for the std window.
||| When on, function keys (F0, F1, ...) and arrow keys are
||| transformed into single chars that can be compared against
||| the result of passing a particular key to the fnKeyChar
||| function.
export
keypad : HasIO io => (b : Bool) -> NCursesT io i (setKeypad b i) ()
keypad enable = MkNCurses (Core.keypad enable)

export
ColorPair : Type
ColorPair = Core.ColorPair

%hide Core.ColorPair

export
startColor : HasIO io => NCursesT io i (setColor i) ()
startColor = MkNCurses Core.startColor

export
initColorPair : HasIO io => So i.colorEnabled =>
                Nat -> (fg, bg : Color) -> NCursesT io i i ColorPair
initColorPair n fg bg = MkNCurses (Core.initColorPair n fg bg)

public export
Attribute : Type
Attribute = Attribute' ColorPair

%hide Core.Attribute

||| Set an attribute to be applied in the standard window
||| until it is cleared or overwritten.
|||
||| See @nSetAttr'@ for a version that works on
||| any given window.
export
nSetAttr : HasIO io => Attribute -> NCursesT io i i ()
nSetAttr att = MkNCurses (Core.nSetAttr att)

--------------------------------------------------------------------------------
-- These are not the best because they're for computations that do not change
-- the  `noDelay` value. They are declared because they can be useful to call
-- existing functions such as `for_`.
--------------------------------------------------------------------------------

namespace Functor

  export
  [NCURSES] Functor io => Functor (NCursesT io i i) where
    map = NCurses.map

namespace Applicative

  export
  [NCURSES] Monad io => Applicative (NCursesT io i i)
    using Functor.NCURSES
    where
      pure = NCurses.pure
      (<*>) = NCurses.(<*>)

namespace Monad

  export
  [NCURSES] Monad io => Monad (NCursesT io i i)
    using Applicative.NCURSES
    where
      (>>=) = NCurses.(>>=)
      join mmx = NCurses.(>>=) mmx id

namespace HasIO

  export
  [NCURSES] HasIO io => HasIO (NCursesT io i i)
    using Monad.NCURSES
    where
      liftIO = MkNCurses . liftIO

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module GRIN.Analysis.Inline

import Data.List
import Data.Num.Implementations
import Data.SortedMap as Map
import Data.SortedMap.Extra
import Data.SortedSet as Set

import GRIN.AST
import GRIN.GrinM

[SemigroupMergeLeft] Semigroup (SortedMap k v) where
    (<+>) = mergeLeft

[MonoidMergeLeft] Ord k => Monoid (SortedMap k v) using SemigroupMergeLeft where
    neutral = empty

simpleDef : Ord name => Def name -> SortedMap name (Def name)
simpleDef (MkDef fn _ (SimpleExp (Do _)) _) = empty
simpleDef def@(MkDef fn _ (SimpleExp _) _) = singleton fn def
simpleDef _ = empty

export
inlineSimpleDefs : Ord name => Monad m => GrinT name m ()
inlineSimpleDefs = do
    MkProg _ defs m <- gets prog
    modify $ record { toInline =
        delete m $ foldMap @{%search} @{MonoidMergeLeft} simpleDef defs }

calledSExp : Eq name => name -> SExp name -> Nat
calledExp : Eq name => name -> Exp name -> Nat

calledSExp fn (Do e) = calledExp fn e
calledSExp fn (App fn' _) = if fn == fn' then 1 else 0
calledSExp _ _ = 0

calledExp fn (SimpleExp e) = calledSExp fn e
calledExp fn (Bind _ rhs rest) = calledSExp fn rhs + calledExp fn rest
calledExp fn (Case _ alts) = foldMap @{%search} @{Additive} (calledExp fn . altExp) alts

export
inlineUsedOnce : Ord name => Monad m => GrinT name m ()
inlineUsedOnce = do
    ds <- gets $ defs . prog
    cg <- getCalls
    let toInline = foldr (addOne ds) empty $ Map.toList cg
    modify $ record { toInline = toInline }
  where
    addOne : SortedMap name (Def name) -> (name, SortedSet name) -> SortedMap name (Def name) -> SortedMap name(Def name)
    addOne ds (fn, callers) ins = case Set.toList callers of
        [caller] => case lookup caller ds of
            Just callerDef => if calledExp fn (callerDef.body) <= 1
                then case lookup fn ds of
                    Just def => insert fn def ins
                    Nothing => ins
                else ins
            Nothing => ins
        _ => ins


text:
module Data.Traversable

import Control.Monad.Identity
import Data.Functor.Const
import Data.Morphisms

public export
mapDefault : Traversable t => (a -> b) -> t a -> t b
mapDefault f = runIdentity . traverse (Id . f)

public export
foldrDefault : Traversable t => (a -> acc -> acc) -> acc -> t a -> acc
foldrDefault f acc t =
  (applyEndo . getConst $ traverse (MkConst {b = ()} . Endo . f) t) acc


text:
||| Provide Do-Notation support for Indexed Monad. Withouth this, the Indexed interfaces use
||| operators that do not collide with the non-Indexed interfaces.
module Control.Monad.Indexed.Do

import Control.Monad.Indexed

public export
(>>=) : IndexedMonad z m => m a i j -> (a -> m b j k) -> m b i k
(>>=) = (>>>=)

public export
(>>) : IndexedMonad z m => m () i j -> Lazy (m b j k) -> m b i k
(>>) = (>>>)

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module C

import B

foo : BFunc x
foo1 : BFunc x
foo2 : BFunc x
foo3 : BFunc x


text:
module Sessions.Projection

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta

import Sessions.Global
import Sessions.Global.Involved

import Sessions.Local
import Sessions.Local.Same
import Sessions.Local.Same.All

import public Sessions.Projection.Error

%hide Data.List.merge

%default total

mutual

  namespace Term
    public export
    data Project : (tyHowMerge : {rs : List Ty}
                              -> {g  :      Ty}
                              -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> (that  :                      Local typeR typeL typeM rs g)
                                       -> Type)
                -> (role  : typeR)
                -> (termG : Global typeR typeL typeM rs g)
                -> (termL : Local  typeR typeL typeM rs g)
                        -> Type
      where
        End : {merge : {rs    : List Ty}
                    -> {g     :      Ty}
                    -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                    -> (that  :                      Local typeR typeL typeM rs g)
                             -> Type}
                    -> Project merge whom End End

        Call : {merge : {rs    : List Ty}
                     -> {g     :      Ty}
                     -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                     -> (that  :                      Local typeR typeL typeM rs g)
                              -> Type}
                     -> Project merge whom (Call idx) (Call idx)

        Rec : {merge : {rs    : List Ty}
                    -> {g     :      Ty}
                    -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                    -> (that  :                      Local typeR typeL typeM rs g)
                             -> Type}
            -> (rec : Term.Project merge whom      x       y)
                   -> Term.Project merge whom (Rec x) (Rec y)

        ChoiceSelect : {merge : {rs    : List Ty}
                             -> {g     :      Ty}
                             -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                             -> (that  :                      Local typeR typeL typeM rs g)
                                      -> Type}
                    -> (prfS : whom = s)
                    -> (ss   : List1.Project merge whom bs cs)

                            -> Project merge whom (Choice        s r notsr bs)
                                                  (Choice SELECT   r       cs)

        ChoiceBranch : {merge : {rs    : List Ty}
                             -> {g     :      Ty}
                             -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                             -> (that  :                      Local typeR typeL typeM rs g)
                                      -> Type}
                    -> (prfR : whom = r)
                    -> (cs   : List1.Project merge whom bs bs')
                            -> Term.Project  merge whom (Choice        s r notsr bs)
                                                        (Choice BRANCH s         bs')

        ChoiceMerge : {merge : {rs    : List Ty}
                            -> {g     :      Ty}
                            -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                            -> (that  :                      Local typeR typeL typeM rs g)
                                     -> Type}
                   -> (prfWS : Not (whom = s))
                   -> (prfWR : Not (whom = r))

                   -> (ss    : List1.Project merge whom bs ((cl,cm,c):::cs))

                   -> (prf   : merge ((cl,cm,c):::cs) d)
                            -> Project merge whom (Choice s r notsr bs)
                                                  d

  namespace List

    public export
    data Project : (tyHowMerge : {rs    : List Ty}
                              -> {g     :      Ty}
                              -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> (that  :                      Local typeR typeL typeM rs g)
                                       -> Type)
                -> (role : typeR)
                -> (bs   : List (typeL, typeM, Global typeR typeL typeM rs g))
                -> (bs'  : List (typeL, typeM, Local  typeR typeL typeM rs g))
                        -> Type
      where
        Empty : {merge : {rs    : List Ty}
                      -> {g     :      Ty}
                      -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                      -> (that  :                      Local typeR typeL typeM rs g)
                               -> Type}
                      -> Project merge whom Nil Nil

        Ext : {merge : {rs    : List Ty}
                    -> {g     :      Ty}
                    -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                    -> (that  :                      Local typeR typeL typeM rs g)
                             -> Type}
           -> (this : Term.Project merge whom         x               y)
           -> (rest : List.Project merge whom             xs              ys)
                   -> List.Project merge whom ((xl,xm,x)::xs) ((xl,xm,y)::ys)

  namespace List1

    public export
    data Project : (tyHowMerge : {rs : List Ty}
                              -> {g  :      Ty}
                              -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> (that  :                      Local typeR typeL typeM rs g)
                                       -> Type)
                -> (role : typeR)
                -> (bs   : List1 (typeL, typeM, Global typeR typeL typeM rs g))
                -> (bs'  : List1 (typeL, typeM, Local  typeR typeL typeM rs g))
                        -> Type
      where
        Proj : {merge : {rs    : List Ty}
                    -> {g     :      Ty}
                    -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                    -> (that  :                      Local typeR typeL typeM rs g)
                             -> Type}
            -> (what  : List.Project  merge whom (b ::bs) (c ::cs))
                     -> List1.Project merge whom (b:::bs) (c:::cs)

mutual
  namespace Term

    public export
    project : DecEq typeR typeL typeM
           => {mergeTy : {rs    : List Ty}
                      -> {g     :      Ty}
                      -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                      -> (that  :                      Local typeR typeL typeM rs g)
                               -> Type}
           -> (mergeOp : {rs   : List Ty}
                      -> {g    :      Ty}
                      -> (this : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> Maybe (that ** mergeTy this that))
           -> {rs    : List Ty}
           -> {g     :      Ty}
           -> (role  : typeR)
           -> (termG : Global typeR typeL typeM rs g)
                    -> Maybe (termL ** Project mergeTy role termG termL)

    project _ _ End
      = Just (End ** End)

    project _ _ (Call x)
      = Just (Call x ** Call)

    project mergeOp role (Rec x)
      = do (x' ** prf) <- project mergeOp role x
           pure (Rec x' ** Rec prf)

    project mergeOp role (Choice s r notSR cs) with (involved role s r notSR)
      project mergeOp role (Choice role r notSR cs) | (Sends Refl)
        = do (cs' ** prf) <- project mergeOp role cs
             pure (Choice SELECT r cs' ** ChoiceSelect Refl prf)

      project mergeOp role (Choice s role notSR cs) | (Recvs Refl)
        = do (cs' ** prf) <- project mergeOp role cs
             pure (Choice BRANCH s cs' ** ChoiceBranch Refl prf)

      project mergeOp role (Choice s r notSR cs) | (Skips prfSNot prfRNot)
        = do ((l,(m,c')) ::: tail ** prfProj) <- project mergeOp role cs
             (c ** prfMerge) <- mergeOp ((l,(m,c')) ::: tail)
             pure (c ** ChoiceMerge prfSNot prfRNot prfProj prfMerge)

  namespace List

    public export
    project : DecEq typeR typeL typeM
           => {mergeTy : {rs    : List Ty}
                      -> {g     :      Ty}
                      -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                      -> (that  :                      Local typeR typeL typeM rs g)
                               -> Type}
           -> (mergeOp : {rs   : List Ty}
                      -> {g    :      Ty}
                      -> (this : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> Maybe (that ** mergeTy this that))

           -> {rs   : List Ty}
           -> {g    :      Ty}
           -> (role : typeR)
           -> (bs   : List (typeL, typeM, Global typeR typeL typeM rs g))
                   -> Maybe (bs' ** List.Project mergeTy role bs bs')

    project _ _ []
      = pure (Nil ** Empty)

    project mergeOp role ((l,(m,x)) :: xs)

      = do (x'  ** prfX)  <- Term.project mergeOp role x
           (xs' ** prfXs) <- List.project mergeOp role xs

           pure ((l,(m,x')) :: xs' ** Ext prfX prfXs)

  namespace List1

    public export
    project : DecEq typeR typeL typeM
           => {mergeTy : {rs    : List Ty}
                      -> {g     :      Ty}
                      -> (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                      -> (that  :                      Local typeR typeL typeM rs g)
                               -> Type}
           -> (mergeOp : {rs   : List Ty}
                      -> {g    :      Ty}
                      -> (this : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                              -> Maybe (that ** mergeTy this that))

           -> {rs    : List Ty}
           -> {g     :      Ty}
           -> (role  : typeR)
           -> (termG : List1 (typeL, typeM, Global typeR typeL typeM rs g))
                    -> Maybe (termL ** Project mergeTy role termG termL)

    project mergeOp role (head ::: tail)
      = do (x::xs ** prf) <- List.project mergeOp role (head::tail)
           pure (x:::xs ** Proj prf)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Test.Example

import Test.Assert

export
main : IO ()
main = do
  assertEq "show 3 and '3' are equal" (show 3) "3"
  assertEq "True and False are equal" True False

  assertNotEq "1 + 1 is not 3" (1 + 1) 3
  assertNotEq "1 + 1 is not 2" (1 + 1) 2

  assertTrue "Something is something" (isJust (Just 3))
  assertTrue "Something is nothing" (isJust $ the (Maybe String) Nothing)

  assertFalse "True && False is False" (True && False)
  assertFalse "True || False is False" (True || False)

max_stars_repo_name: Risto-Stevcev/idris-assert

max_issues_repo_name: Risto-Stevcev/idris-assert

max_forks_repo_name: Risto-Stevcev/idris-assert


text:
public export
data X : Type where
  [noHints]
  U : X
  W : X

public export %hint
xHint : X
-- Intentionally unimplemented

f : Int -> X => Int
f a = a + 1

g : Int
g = f 4
-- Typechecks even when `xHint` is unimplemented.

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
import Data.Vect

four_eq : 4 = 4
four_eq = Refl

-- four_eq_five : 4 = 5
-- four_eq_five = Refl

twoplustwo_eq_four : 2 + 2 = 4
twoplustwo_eq_four = Refl

plus_reduces_Z : (m : Nat) -> plus Z m = m
plus_reduces_Z m = Refl

plus_reduces_Sk : (k, m : Nat) -> plus (S k) m = S (plus k m)
plus_reduces_Sk k m = Refl

idris_not_php : Z = "Z"

vect_eq_length : (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> n = m
vect_eq_length xs xs Refl = Refl


text:
module Data.MSF.Event

%default total

||| A data type isomorphic to `Maybe` used to signal
||| occurences of discrete events.
public export
data Event : (a : Type) -> Type where
  NoEv : Event a
  Ev   : (v : a) -> Event a

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export
maybeToEvent : Maybe a -> Event a
maybeToEvent Nothing  = NoEv
maybeToEvent (Just x) = Ev x

public export
eventToMaybe : Event a -> Maybe a
eventToMaybe NoEv   = Nothing
eventToMaybe (Ev v) = Just v

public export
fromEvent : Lazy a -> Event a -> a
fromEvent x NoEv   = x
fromEvent _ (Ev v) = v

public export
toEvent : Bool -> Lazy a -> Event a
toEvent False _  = NoEv
toEvent True  va = Ev va

public export
event : Lazy b -> Lazy (a -> b) -> Event a -> b
event v _ NoEv   = v
event _ f (Ev x) = f x

public export
unionL : Event a -> Event a -> Event a
unionL (Ev x) _ = Ev x
unionL _      y = y

public export
unionR : Event a -> Event a -> Event a
unionR _ (Ev y) = Ev y
unionR x _      = x

public export
unionWith : (a -> a -> a) -> Event a -> Event a -> Event a
unionWith f (Ev x) (Ev y) = Ev $ f x y
unionWith _ x      y      = unionL x y

public export
filter : (a -> Bool) -> Event a -> Event a
filter f NoEv    = NoEv
filter f (Ev va) = if f va then Ev va else NoEv

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

export
Show a => Show (Event a) where
  showPrec p NoEv   = "NoEv"
  showPrec p (Ev v) = showCon p "Ev" $ showArg v

public export
Eq a => Eq (Event a) where
  NoEv == NoEv = True
  Ev x == Ev y = x == y
  _    == _    = False

public export
Ord a => Ord (Event a) where
  compare NoEv   NoEv   = EQ
  compare NoEv   (Ev _) = LT
  compare (Ev _) NoEv   = GT
  compare (Ev x) (Ev y) = compare x y

public export
Functor Event where
  map _ NoEv   = NoEv
  map f (Ev a) = Ev $ f a

public export
Applicative Event where
  pure = Ev
  Ev f <*> Ev a = Ev $ f a
  _    <*> _    = NoEv

public export
Monad Event where
  NoEv >>= _ = NoEv
  Ev a >>= f = f a

public export
Foldable Event where
  foldr _ v NoEv   = v
  foldr f v (Ev a) = f a v

  foldl _ v NoEv   = v
  foldl f v (Ev a) = f v a

  foldMap _ NoEv   = neutral
  foldMap f (Ev a) = f a

  null NoEv   = True
  null (Ev a) = False

public export %inline
Traversable Event where
  traverse _ NoEv   = pure NoEv
  traverse f (Ev a) = Ev <$> f a

public export %inline
Alternative Event where
  empty = NoEv
  x <|> y = unionL x y

public export %inline
Semigroup a => Semigroup (Event a) where
  (<+>) = unionWith (<+>)

public export %inline
Semigroup a => Monoid (Event a) where
  neutral = NoEv

--------------------------------------------------------------------------------
--          More Utilities
--------------------------------------------------------------------------------

public export
mapMaybe : (a -> Maybe b) -> Event a -> Event b
mapMaybe f ev = ev >>= maybeToEvent . f