text:
module Main

import Data.Primitives.Views

everyOther : Stream ty -> Stream ty
everyOther (e1 :: e2 :: es) = e2 :: everyOther es

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

Functor InfList where
  map f (x :: xs) = f x :: map f xs

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

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

data Face : Type where
  Heads : Face
  Tails : Face

Show Face where
  show Heads = "Heads"
  show Tails = "Tails"

getFace : Int -> Face
getFace n with (divides n 2)
  getFace ((2 * div) + rem) | (DivBy prf) =
    case rem of
      0 => Heads
      _ => Tails

randoms : Int -> Stream Int
randoms seed =
  let seed' = 1664525 * seed + 1013904223
  in (seed' `shiftR` 2) :: randoms seed'

coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips count xs = map getFace (take count xs)

squareRootApprox : (number : Double) -> (approx : Double) -> Stream Double
squareRootApprox number approx = approx :: squareRootApprox number next
  where
    next = (approx + (number / approx)) / 2

squareRootBound : (max : Nat) -> (number : Double) -> (bound : Double) -> (approxs : Stream Double) -> Double
squareRootBound Z number bound (val :: xs) = val
squareRootBound (S k) number bound (val :: xs) =
  case (val * val - number <= bound) of
    True  => val
    False => squareRootBound k number bound xs

squareRoot : (numner : Double) -> Double
squareRoot number = squareRootBound 100 number 0.00000000001 (squareRootApprox number number)

main : IO ()
main = do
  printLn $ take 10 (everyOther [1..]) -- [2,4,6,8,10,12,14,16,18,20]
  printLn $ getPrefix 10 (map (*2) (countFrom 1)) -- [2,4 .. 20]
  printLn $ coinFlips 6 (randoms 12345) -- [T,H,T,T,H,T]
  printLn $ take 3 (squareRootApprox 10 10)
  printLn $ take 3 (squareRootApprox 100 25)
  printLn $ squareRoot 6
  printLn $ squareRoot 2500
  printLn $ squareRoot 2501

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module GCDZZ
import Divisors
import ZZ
import NatUtils
import gcd
import ZZUtils
%default total
%access public export

|||Converts the expression (a=r+(q*b)) to its integer equivalent
total
ExpNatToZZ:{a:Nat}->{b:Nat}->(a=r+(q*b))->((Pos a)=Pos(r)+((Pos q)*(Pos b)))
ExpNatToZZ Refl = Refl

|||Given a nonnegative integer a and positive integer b, it returns quotient and remainder
|||with proof of (a = rem + (quot * b) and that 0<=rem<b
total
QuotRemZ:(a:ZZ)->(b:ZZ)->IsNonNegative a -> IsPositive b ->
(quot : ZZ ** (rem : ZZ ** ((a = rem + (quot * b)), LTZ rem b,(IsNonNegative rem))))
QuotRemZ (Pos j) (Pos (S k)) NonNegative Positive =
  case (euclidDivide j (S k) (SIsNotZ {x=(k)})) of
    (q ** (r ** (equality, rlessb))) =>
         ((Pos q)**((Pos r)**((ExpNatToZZ equality),(ltNatToZZ rlessb),NonNegative)))

|||Returns gcd of a and b with proof when a is positive and b is nonnegative
GCDCalc :(a:ZZ)->(b:ZZ)->(IsPositive a)->(IsNonNegative b)->(d**(GCDZ a b d))
GCDCalc a (Pos Z) x NonNegative = (a**(gcdOfZeroAndInteger a x))
GCDCalc (Pos (S j)) (Pos  (S k)) Positive NonNegative = assert_total $
  case QuotRemZ (Pos (S j)) (Pos  (S k)) NonNegative Positive of
    (quot ** (rem  ** (equality, remLessb,remNonNeg))) =>
       (case GCDCalc (Pos (S k)) rem Positive remNonNeg of
             (x ** pf) => (x**(euclidConservesGcdWithProof equality pf)))

|||Returns Bezout coefficients with proof for a Positive integer a and
|||NonNegative integer b with proofs of GCD and equality
bez:(a:ZZ)->(b:ZZ)->(IsPositive a)->(IsNonNegative b) ->
   (d**((GCDZ a b d),(m:ZZ**n:ZZ**(d=(m*a)+(n*b)))))
bez a (Pos Z) x NonNegative = (a**((gcdOfZeroAndInteger a x),(1**0**prf))) where
  prf = rewrite (multOneLeftNeutralZ a) in
     (rewrite  (plusZeroRightNeutralZ a) in Refl)
bez (Pos (S j)) (Pos  (S k)) Positive NonNegative = assert_total $
  case QuotRemZ (Pos (S j)) (Pos  (S k)) NonNegative Positive of
      (quot ** (rem  ** (equality, remLessb,remNonNeg))) =>
         (case bez (Pos (S k)) rem Positive remNonNeg of
            (g**((gcdprf),(m1**n1**lincombproof))) =>
               (g**((euclidConservesGcdWithProof equality gcdprf),
                    ((n1)**(m1+(n1*(-quot)))**
                          (bezoutReplace equality lincombproof)))))

|||Returns gcd of two integers with proof given that not both of them are zero
gcdZZ:(a:ZZ)->(b:ZZ)->(NotBothZeroZ a b)->(d**(GCDZ a b d))
gcdZZ (Pos (S k)) (Pos j) LeftPositive =
  GCDCalc (Pos (S k)) (Pos j) Positive NonNegative
gcdZZ (Pos (S k)) (NegS j) LeftPositive =
  case GCDCalc (Pos (S k)) (-(NegS j)) Positive NonNegative of
                (x ** pf) => (x**(negatingPreservesGcdRight pf))
gcdZZ (NegS k) (Pos j) LeftNegative =
  case GCDCalc (-(NegS k)) (Pos j) Positive NonNegative of
    (x**pf) =>(x**(negatingPreservesGcdLeft pf))
gcdZZ (NegS k) (NegS j) LeftNegative =
  case GCDCalc (-(NegS k)) (-(NegS j)) Positive NonNegative of
        (x ** pf) => (x**((negatingPreservesGcdLeft
           (negatingPreservesGcdRight pf))))
gcdZZ a (Pos (S k)) RightPositive = assert_total $
  case gcdZZ (Pos (S k)) a LeftPositive of
    (x ** pf) => (x** (gcdSymZ pf))
gcdZZ a (NegS k) RightNegative = assert_total $
  case gcdZZ (NegS k) a LeftNegative of
      (x ** pf) => (x** (gcdSymZ pf))

|||Returns Bezout coefficients with proof for two integers a and b such that
|||not both of them are zero with proofs of GCD and equality
bezoutCoeffs:(a:ZZ)->(b:ZZ)->NotBothZeroZ a b->
   (d**((GCDZ a b d),(m:ZZ**n:ZZ**(d=(m*a)+(n*b)))))
bezoutCoeffs (Pos (S k)) (Pos j) LeftPositive =
  bez (Pos (S k)) (Pos j) Positive NonNegative
bezoutCoeffs (Pos (S k)) (NegS j) LeftPositive =
  case bez (Pos (S k)) (-(NegS j)) Positive NonNegative of
    (x **( pf,(m**n**lproof))) =>
       (x**((negatingPreservesGcdRight pf),(m**(-n)**
           (rewrite multNegNegNeutralZ n (Pos(S j)) in lproof))))
bezoutCoeffs (NegS k) (Pos j) LeftNegative =
  case bez (-(NegS k)) (Pos j) Positive NonNegative of
    (x**(pf,(m**n**lproof))) =>(x**((negatingPreservesGcdLeft pf),((-m)**n**
       (rewrite multNegNegNeutralZ m (Pos (S k)) in lproof))))
bezoutCoeffs (NegS k) (NegS j) LeftNegative =
  case bez (-(NegS k)) (-(NegS j)) Positive NonNegative of
        (x**(pf,(m**n**lproof))) => (x**((((negatingPreservesGcdLeft
          (negatingPreservesGcdRight pf)))),((-m)**(-n)**
            (rewrite  multNegNegNeutralZ m (Pos (S k)) in
             rewrite  multNegNegNeutralZ n (Pos(S j)) in
              lproof))))
bezoutCoeffs a (Pos (S k)) RightPositive = assert_total $
  case bezoutCoeffs (Pos (S k)) a LeftPositive of
    (x**(pf,(m**n**lproof))) => (x** ((gcdSymZ pf),(n**m**
       (rewrite plusCommutativeZ (n*a) (m*(Pos (S k))) in lproof))))
bezoutCoeffs a (NegS k) RightNegative = assert_total $
  case bezoutCoeffs (NegS k) a LeftNegative of
      (x**(pf,(m**n**lproof))) => (x** ((gcdSymZ pf),(n**m**
         (rewrite plusCommutativeZ (n*a) (m*(NegS k)) in lproof))))

|||Proof that if d = ja + kb, then md = jma + kmb
multOnLeft:{a:ZZ}->(m:ZZ)->(d=(j*a)+(k*b))->((m*d)=j*(m*a)+k*(m*b))
multOnLeft {a}{b}{j}{k}{d} m prf =
  rewrite multAssociativeZ j m a in
  rewrite multAssociativeZ k m b in
  rewrite multCommutativeZ j m in
  rewrite multCommutativeZ k m in
  rewrite sym $ multAssociativeZ m j a in
  rewrite sym $ multAssociativeZ m k b in
  rewrite sym $ multDistributesOverPlusRightZ m (j*a) (k*b) in
  cong prf

|||A helper function for gcdOfMultiple
genfunctionGcdOfMultiple:{a:ZZ}->{b:ZZ}->{d:ZZ}->{k:ZZ}->{j:ZZ}->(d=j*a+k*b)->
 (m:ZZ)->
  ({c:ZZ}->(IsCommonFactorZ (m*a) (m*b) c) -> (IsDivisibleZ (m*d) c))
genfunctionGcdOfMultiple{a}{b}{d}{k}{j} prf  m  commonpf =
  linCombDivLeftWithProof {a=(m*a)}{b=(m*b)}{d=(m*d)} (multOnLeft m prf) commonpf

|||The theorem that if m>0 and a and b are not both zero, then gcd(ma,mb) = m *gcd (a,b)
gcdOfMultiple:(m:ZZ)-> (IsPositive m)->(GCDZ a b d) ->NotBothZeroZ a b->
  (GCDZ (m*a) (m*b) (m*d) )
gcdOfMultiple{a}{b}{d} m mPos (dPos, (dDiva,dDivb),fd)  notzero=
  case bezoutCoeffs a b notzero of
        (g**(gisgcd,(j**k**linpf))) =>
            ((posMultPosIsPos mPos dPos),((multBothSidesOfDiv m dDiva),
                 (multBothSidesOfDiv m dDivb)),
                     (genfunctionGcdOfMultiple{d=d} (rewrite (gcdIsUnique gisgcd (dPos, (dDiva,dDivb),fd)) in linpf) m ))

|||The proof that if c = (2*c)*n, then 1 = (2*n)
|||A helper function for gcdZeroZeroContra
helping1: {c:ZZ}->{n:ZZ}->(IsPositive c)->(c = (2*c)*n) ->(1= (2*n))
helping1{n}{c} cPos prf =
  (multRightCancelZ 1 (2*n) c (posThenNotZero cPos) exp) where
    exp = rewrite multOneLeftNeutralZ c in
          rewrite sym $ multAssociativeZ 2 n c in
          rewrite multCommutativeZ n c in
          rewrite multAssociativeZ 2 c n in
          prf
|||Proof that 2=1 is impossible
twoIsNotOne:Pos (S (S Z))= Pos (S Z)->Void
twoIsNotOne Refl impossible
|||Proof that 2= -1 is impossible
twoIsNotMinusOne: (Pos (S (S Z))= (NegS Z))->Void
twoIsNotMinusOne Refl impossible

|||Proof that 1 = (2*n) is impossible
oneIsTwoTimesIntContra:{n:ZZ}-> (1= (2*n))->Void
oneIsTwoTimesIntContra{n} prf =
  (case productOneThenNumbersOne 2 n (sym prf) of
        (Left (a,b )) => twoIsNotOne a
        (Right (a,b)) => twoIsNotMinusOne a)

|||Proof that if c is positive, 2c|c is impossible
twiceDividesOnceContra:IsPositive c ->(IsDivisibleZ  c (2*c) )->Void
twiceDividesOnceContra cPos (n ** pf) =oneIsTwoTimesIntContra( helping1 cPos pf)
|||GCD of 0 and 0 does not exist
gcdZeroZeroContra:{k:ZZ}->(GCDZ 0 0 k)->Void
gcdZeroZeroContra {k} (kPos,(kDivZ1,kDivZ2),fk) =
 twiceDividesOnceContra kPos (fk {c=(2*k)} (zzDividesZero (2*k),zzDividesZero (2*k)))

|||The actual definition of GCD as the 'greatest' common divisor
GCDZr: (a:ZZ) -> (b:ZZ) -> (d:ZZ) -> Type
GCDZr a b d = ((IsCommonFactorZ a b d),
  ({c:ZZ}->(IsCommonFactorZ a b c)->(LTEZ c d)))

|||GCD of 0 and 0 does not exist even in this definition.
gcdrZeroZeroContra:{k:ZZ}->(GCDZr 0 0 k)->Void
gcdrZeroZeroContra{k} ((kDiv1, kDiv2),fk) =
  succNotLteNumZ k (fk((zzDividesZero (1+k)),(zzDividesZero (1+k))))

|||A helper function function for GCDZImpliesGCDZr
helperGCDZImpliesGCDZr:({k:ZZ}->(IsCommonFactorZ a b k)->(IsDivisibleZ d k))->(IsPositive d)->
   {c:ZZ}->(IsCommonFactorZ a b c)->(LTEZ c d)
helperGCDZImpliesGCDZr {d=(Pos (S k))} f Positive {c = (NegS j)} y = NegLessPositive
helperGCDZImpliesGCDZr {d=(Pos (S k))} f Positive {c = (Pos Z)} y = PositiveLTE (LTEZero)
helperGCDZImpliesGCDZr {d=(Pos (S k))} f Positive {c = (Pos (S j))} y =
  posDivPosImpliesLte (f y) Positive Positive

|||Proof that (GCDZ a b d) implies (GCDZr a b d)
GCDZImpliesGCDZr:(GCDZ a b d)->(GCDZr a b d)
GCDZImpliesGCDZr (dPos,cfab,fd) = (cfab,(helperGCDZImpliesGCDZr fd dPos))

|||Rewrites GCDZr a b e as GCDZr c d e , given a prrof that a=c and b=d
gcdReplace:{a:ZZ}->{b:ZZ}->(a=c)->(b=d)->GCDZr a b e -> GCDZr c d e
gcdReplace prf prf1 x = rewrite (sym prf) in
                        rewrite (sym prf1) in
                        x
|||Rewrites GCDZ a b e as GCDZ c d e , given a prrof that a=c and b=d
gcdzReplace:{a:ZZ}->{b:ZZ}->(a=c)->(b=d)->GCDZ a b e -> GCDZ c d e
gcdzReplace prf prf1 x = rewrite (sym prf) in
                        rewrite (sym prf1) in
                        x
|||GCD is unique even in this definition
gcdrIsUnique:(GCDZr a b c)->(GCDZr a b d)->(c=d)
gcdrIsUnique (comfactc,fc) (comfactd,fd) =
  lteAndGteImpliesEqualZ (fc (comfactd)) (fd (comfactc))

|||Proof that (GCDZr a b d) implies (GCDZ a b d)
GCDZrImpliesGCDZ:{a:ZZ}->{b:ZZ}-> (GCDZr a b d)->(GCDZ a b d)
GCDZrImpliesGCDZ {a}{b}{d} gcdr =
  (case checkNotBothZero a b  of
        Left (aZ,bZ) => void (gcdrZeroZeroContra (gcdReplace aZ bZ gcdr))
        Right notZ =>
           (case bezoutCoeffs a b notZ of
                 (g**(gisgcd,(j**k**linpf))) =>
                    rewrite (gcdrIsUnique gcdr (GCDZImpliesGCDZr gisgcd)) in
                        gisgcd))
|||If d = gcd (a,b) then there exists m and n such that d =ma +nb
gcdIsLinComb:(GCDZ a b d)->(m:ZZ**n:ZZ**(d=(m*a)+(n*b)))
gcdIsLinComb {a}{b} gcd =
  (case checkNotBothZero a b  of
        Left (aZ,bZ) => void (gcdZeroZeroContra (gcdzReplace aZ bZ gcd))
        (Right notZ) =>
          (case bezoutCoeffs a b notZ of
                (g**(gisgcd,(j**k**linpf))) =>
                  (j**k**(rewrite (sym(gcdIsUnique gcd gisgcd)) in linpf))))

|||Theorem that if c|ab and gcd (a,c) =1 , then c|b
caCoprimeThencDivb : (IsDivisibleZ (a*b) c)->(GCDZ a c 1)->
   (IsDivisibleZ b c)
caCoprimeThencDivb cDivab gcd1{a}{b}{c} =
  (case gcdIsLinComb gcd1 of
        (m**n**linpf) =>
        linCombDivLeftWithProof {a=(a*b)} {b=(c*b)} {d=b} {c=c} {m=m} {n=n}
             ( rewrite multAssociativeZ m a b in
               rewrite multAssociativeZ n c b in
               rewrite sym $ multDistributesOverPlusLeftZ (m*a) (n*c) b in
               rewrite multCommutativeZ ((m*a)+(n*c)) b in
               (rewriteLeftTimesOneAsLeft (cong linpf)))
                      (cDivab,(multDiv  (selfDivide c) b)))

|||SmallestPosLinComb a b d is a proof that d is the smallest positive
|||linear combination of a and b
SmallestPosLinComb: (a:ZZ)->(b:ZZ)->(d:ZZ)->Type
SmallestPosLinComb a b d = ((IsPositive d),(m**n**(d=(m*a)+(n*b))),
 ({c:ZZ}->{j:ZZ}->{k:ZZ}->(IsPositive c)-> (c=j*a+k*b)->(LTEZ d c)))
|||The theorem that the smallest positive linear combination is unique
smallestPosLinCombIsUnique :(SmallestPosLinComb a b c)->
    (SmallestPosLinComb a b d)->(c=d)
smallestPosLinCombIsUnique (cPos,(m**n**prfc),fc) (dPos,(u**v**prfd),fd) =
  lteAndGteImpliesEqualZ (fd cPos prfc) (fc dPos prfd)

|||Proof that  j+0=j+(n*0) for any integer n
helping2:{j:ZZ}->(n:ZZ)->j+0=j+(n*0)
helping2 n = rewrite  multZeroRightZeroZ n in Refl
|||Proof that any linear combination of 0 and 0 is 0
linCombZeroZeroIsZero: (m:ZZ**n:ZZ**(k=(m*0)+(n*0)))->(k=0)
linCombZeroZeroIsZero (m**n**lprf) =
  rewrite sym $ multZeroRightZeroZ m in
  rewrite sym $ plusZeroRightNeutralZ (m*0) in
  rewrite helping2 {j=(m*0)} n in
   lprf

|||The theorem that smallest positive linear combination of Zero andZero
|||doesnt exist
smallestPosLinCombZeroZeroVoid:{k:ZZ}->(SmallestPosLinComb 0 0 k)->Void
smallestPosLinCombZeroZeroVoid (kPos,(m**n**prfk),fk) =
  zeroNotPos (rewrite sym $(linCombZeroZeroIsZero (m**n**prfk)) in kPos)

|||The theorem that gcd(a,b) is less than or equal to any
|||positive linear combination of a and b
gcdIsSmallerThanLinComb: (GCDZ a b d)->
   ({c:ZZ}->{j:ZZ}->{k:ZZ}->(IsPositive c)-> (c=j*a+k*b)->(LTEZ d c))
gcdIsSmallerThanLinComb (dPos,(dDiva,dDivb),fd) cPos prf =
  posDivPosImpliesLte (linCombDivLeftWithProof prf (dDiva,dDivb)) cPos dPos

|||Theorem that gcd(a,b) is the smallest positive linear combination of
|||a and b
gcdIsSmallestPosLinComb: (GCDZ a b d)->(SmallestPosLinComb a b d)
gcdIsSmallestPosLinComb (dPos,(dDiva,dDivb),fd) =
  (case gcdIsLinComb (dPos,(dDiva,dDivb),fd) of
        (m**n**prf) =>
        (dPos,(m**n**prf),
             (gcdIsSmallerThanLinComb (dPos,(dDiva,dDivb),fd))))

|||Rewrites SmallestPosLinComb a b e to SmallestPosLinComb c d e
|||when given a proof that a=c and b=d
smallestPosLinCombReplace:{a:ZZ}->{b:ZZ}->(a=c)->(b=d)->SmallestPosLinComb a b e ->
    SmallestPosLinComb c d e
smallestPosLinCombReplace prf prf1 x = rewrite (sym prf) in
                                       rewrite (sym prf1) in
                                           x
|||Theorem that the smallest positive linear combination of a and b is
|||the gcd of a and b
smallestPosLinCombIsGcd:(SmallestPosLinComb a b d)->(GCDZ a b d)
smallestPosLinCombIsGcd {a} {b} splc =
  (case checkNotBothZero a b of
        (Left (aZ,bZ)) => void (smallestPosLinCombZeroZeroVoid
             (smallestPosLinCombReplace aZ bZ splc))
        Right notZ =>
        (case bezoutCoeffs a b notZ of
              (g**(gisgcd,(j**k**linpf))) =>
                 rewrite (smallestPosLinCombIsUnique splc (gcdIsSmallestPosLinComb gisgcd)) in
                     gisgcd))

ext: idr


text:
module PasswordCheck

data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect

data ShellCmd : (ty: Type) -> Access -> (ty->Access) -> Type where
  Password: String -> ShellCmd PwdCheck LoggedOut (\pwd => case pwd of
                                                           Correct => LoggedIn
                                                           Incorrect => LoggedOut)
  Logout: ShellCmd () LoggedIn (const LoggedOut)
  GetSecret: ShellCmd String LoggedIn (const LoggedIn)

  PutStr: String -> ShellCmd () state (const state)
  Pure: (res: ty) -> ShellCmd ty (state_fn res) (state_fn)
  (>>=) : ShellCmd a state1 state2_fn -> ((res: a) -> ShellCmd b (state2_fn res) state3_fn) -> ShellCmd b state1 state3_fn

session: ShellCmd () LoggedOut (const LoggedOut)
session = do Correct <- Password "wurzel" | Incorrect => PutStr "Wrong password"
             msg <- GetSecret
             PutStr ("Secret Code")
             --Logout

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
{-
foo
bar
baz
'\t'
'q'
'u'
'x'
'\r'
'\n'
-}
module Main

main : IO ()
main = do
  putStrLn . pack $ ['f', 'o', 'o']
  for_ (words "bar baz ") putStrLn
  for_ (unpack "\tqux\r\n") (putStrLn . show)

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Main

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

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

data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False
    {-
      (/=) x y = not (x == y)
      this definition is actually the default one,
      so no need to redefine it here
    -}

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Empty empty
%name Node node, node1, node2, node3
%name Tree tree, tree1, tree2, tree3

Eq elem => Eq (Tree elem) where
    (==) Empty Empty = True
    (==) (Node left value right) (Node left' value' right') =
      left == left' && value == value' && right == right'
    (==) _ _ = False

Functor Tree where
    map func Empty = Empty
    map func (Node l x r) = (Node (map func l) (func x) (map func r))

Foldable Tree where
    foldr func acc Empty = acc
    foldr func acc (Node left x right)
      = let
          leftFold = foldr func acc left
          rightFold = foldr func leftFold right
        in
          func x rightFold

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Minecraft.Core.Block.Break.Export

import public Minecraft.Core.Block.Break

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
||| Lightweight representation of qualified names.
|||
||| TODO: Look at making names subject to user supplied predicates.
module Commons.Data.QName

import Commons.Text.Display

%default total
%access public export

data Ty = SIMPLE | QUALIFIED

data QName : (ty : Type) -> (shape : Ty) -> Type where
  BN : ty -> QName ty SIMPLE
  QN : ty -> QName ty shape -> QName ty QUALIFIED

fromList : (xs : List ty) -> (prf : NonEmpty xs) -> QName ty (if length xs > 1 then QUALIFIED else SIMPLE)
fromList (x :: []) IsNonEmpty = BN x
fromList (x :: (y :: xs)) IsNonEmpty with (nonEmpty xs)
  fromList (x :: (y :: xs)) IsNonEmpty | (Yes prf) =  QN x $ QN y $ fromList xs prf
  fromList (x :: (y :: xs)) IsNonEmpty | (No contra) = QN x $ BN y

fromList' : (xs : List ty)
         -> {auto prf : NonEmpty xs}
         -> QName ty (if length xs > 1 then QUALIFIED else SIMPLE)
fromList' xs {prf} = fromList xs prf

Show ty => Show (QName ty shape) where
  show (BN x)    = unwords ["BN", show x]
  show (QN x xs) = unwords ["QN", show x, show xs]

Display ty => Display (QName ty shape) where
  display (BN x) = display x
  display (QN x ys) = display x ++ "." ++ display ys

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Nerodu

import Data.SortedSet
import Data.SortedMap

%default total

data NeroduType = NeroduType_

nspace : SortedMap String NeroduType
nspace = insertFrom
  [ ("Unit", NeroduType_)
  ] empty

data Val = Val_

Value : Type
Value = (Val, NeroduType)

max_stars_repo_name: PolyglotSymposium/nerodu

max_issues_repo_name: PolyglotSymposium/nerodu

max_forks_repo_name: PolyglotSymposium/nerodu


text:
module Main

import Data.Vect

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

data VectUnknown : Type -> Type where
     MkVect : (len : Nat) -> Vect len a -> VectUnknown a

-- We can use implicit underscore notation because there is only one valid value for length in the below
readVect : IO (VectUnknown String)
readVect = do x <- getLine
              if (x == "") then pure (MkVect _ [])
              else do MkVect _ xs <- readVect
                      pure (MkVect _ (x :: xs))

readVectPair : IO (len ** Vect len String)
readVectPair = do x <- getLine
                  if (x == "") then pure (_ ** [])
                  else do (_ ** xs) <- readVectPair
                          pure (_ ** (x :: xs))

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) = putStrLn (show xs ++ " (length " ++ show len ++ ")")

-- We cannot use the below format to define VectUnknown because we need to state the length of the Vector
-- data MyVectUnknown = MyMkVect Nat Vect

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

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module JSON

import public JSON.FromJSON
import public JSON.Option
import public JSON.ToJSON
import public JSON.Value


text:
module Pretty

export
Show Really where
  show (Really err) =  ["RR"


text:
module Andb3

andb3 : (a : Bool) -> (b : Bool) -> (c : Bool) -> Bool
andb3 True True True = True
andb3 a b c = False

tabt1 : (andb3 True True True) = True
tabt1 = Refl

tabt2 : (andb3 False True True) = False
tabt2 = Refl

tabt3 : (andb3 True False True) = False
tabt3 = Refl

tabt4 : (andb3 True True False) = False
tabt4 = Refl

tabt5 : (andb3 True False False) = False
tabt5 = Refl

tabt6 : (andb3 False True False) = False
tabt6 = Refl

tabt7 : (andb3 False False True) = False
tabt7 = Refl

tabt8 : (andb3 False False False) = False
tabt8 = Refl

tabt9 : (andb3 False True True) = False
tabt9 = Refl


text:
import Ifui.Html
import Data.Vect
import Data.List

data Action : Nat -> Type where
  SetInput : String -> Action n
  AddTodo : Action n

State : Type
State = (String, (n:Nat ** Vect n String))

ActionTy : State -> Type
ActionTy = \(_, (n ** _)) => Action n

setInput : (s : State) -> String -> ActionTy s
setInput (_, (n ** _)) x = SetInput x

addTodo : (s : State) -> ActionTy s
addTodo (_, (n ** _)) = AddTodo

view : (s : State) -> Html (ActionTy s)
view x = textSpan "ola"

update : (s : State) -> ActionTy s -> State
update (y, (n ** v)) (SetInput s) = (s, (n ** v))
update (y, (n ** v)) AddTodo = ("", (S n ** y :: v))

main : IO ()
main =
  startHtmlView ("", (0 ** [])) update view

max_stars_repo_name: rbarreiro/ifui

max_issues_repo_name: rbarreiro/ifui

max_forks_repo_name: rbarreiro/ifui


text:
module TyTTP.URL.Search

import Control.Monad.Either
import Data.List
import Data.List1
import Data.Maybe
import TyTTP
import TyTTP.URL

%default total

namespace Simple

  public export
  SimpleSearch : Type
  SimpleSearch = List (String, String)

  parseString : String -> SimpleSearch
  parseString = parseSkipQuestionMarks . unpack
    where
      parse : List Char -> SimpleSearch
      parse [] = []
      parse xs =
        let sections = splitOn '&' xs
            params = break (== '=') <$> List.filter (not . null) (forget sections)
        in
          bimap pack (pack . fromMaybe [] . tail') <$> params

      parseSkipQuestionMarks : List Char -> SimpleSearch
      parseSkipQuestionMarks [] = []
      parseSkipQuestionMarks ('?'::xs) = parseSkipQuestionMarks xs
      parseSkipQuestionMarks a@(x::xs) = parse a

  export
  search : Monad m
    => (
      Step me (URL auth pth SimpleSearch) h1 st h2 a b
      -> m $ Step me' (URL auth pth SimpleSearch) h1' st' h2' a' b'
    )
    -> Step me (URL auth pth String) h1 st h2 a b
    -> m $ Step me' (URL auth pth String) h1' st' h2' a' b'
  search handler step = do
    let src = parseString $ URL.search step.request.url
    result <- handler $ { request.url := { search := src } step.request.url } step
    pure $ { request.url := { search := step.request.url.search } result.request.url } result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

import Pruviloj

infixl 9 .>
(.>) : (a -> b) -> (b -> c) -> (a -> c)
(.>) f g = \x => g (f x)

IdempotencyProof : {X : Type} -> (X -> X -> X) -> Type
IdempotencyProof {X} f = (a : X) -> f a a = a

AssociativityProof : {X : Type} -> (X -> X -> X) -> Type
AssociativityProof {X} f = (a : X) ->
                           (b : X) ->
                           (c : X) ->
                           f a (f b c) = f (f a b) c

CommutativityProof : {X : Type} -> (X -> X -> X) -> Type
CommutativityProof {X} f = (a : X) ->
                           (b : X) ->
                           f a b = f b a

LeftUnitalityProof : {X : Type} -> (X -> X -> X) -> X -> Type
LeftUnitalityProof {X} f e = (a : X) -> a = f e a

RightUnitalityProof : {X : Type} -> (X -> X -> X) -> X -> Type
RightUnitalityProof {X} f e = (a : X) -> a = f a e

UnitalityProof : {X : Type} -> (X -> X -> X) -> X -> Type
UnitalityProof {X} f e = (a : X) -> (a = f e a, a = f a e)

record Dual (X : Type) where
  constructor MkDual
  fromDual : X

implementation (Eq x) => Eq (Dual x) where {
  (MkDual x) == (MkDual y) = (x == y)
}

dualInj : (x = y) -> (MkDual x = MkDual y)
dualInj Refl = Refl

interface (Eq X) => MeetSemiLattice (X : Type)
          where {
            meet : X -> X -> X
            meetIsIdempotent  : IdempotencyProof   meet
            meetIsAssociative : AssociativityProof meet
            meetIsCommutative : CommutativityProof meet
          }

interface (Eq X) => JoinSemiLattice (X : Type)
          where {
            join : X -> X -> X
            joinIsIdempotent  : IdempotencyProof   join
            joinIsAssociative : AssociativityProof join
            joinIsCommutative : CommutativityProof join
          }

implementation (JoinSemiLattice t) => MeetSemiLattice (Dual t) where {
  meet a b = MkDual $ join (fromDual a) (fromDual b)
  meetIsIdempotent (MkDual a)
    = dualInj $ joinIsIdempotent a
  meetIsAssociative (MkDual a) (MkDual b) (MkDual c)
    = dualInj $ joinIsAssociative a b c
  meetIsCommutative (MkDual a) (MkDual b)
    = dualInj $ joinIsCommutative a b
}

implementation (MeetSemiLattice t) => JoinSemiLattice (Dual t) where {
  join a b = MkDual $ meet (fromDual a) (fromDual b)
  joinIsIdempotent (MkDual a)
    = dualInj $ meetIsIdempotent a
  joinIsAssociative (MkDual a) (MkDual b) (MkDual c)
    = dualInj $ meetIsAssociative a b c
  joinIsCommutative (MkDual a) (MkDual b)
    = dualInj $ meetIsCommutative a b
}

interface (MeetSemiLattice X)
          => BoundedMeetSemiLattice (X : Type)
          where {
            top : X
            topIsUnital : UnitalityProof meet top
          }

interface (JoinSemiLattice X)
          => BoundedJoinSemiLattice (X : Type)
          where {
            bot : X
            botIsUnital : UnitalityProof join bot
          }

implementation (BoundedMeetSemiLattice t) => BoundedJoinSemiLattice (Dual t)
               where {
                 bot = MkDual top
                 botIsUnital (MkDual a) = let (p1, p2) = topIsUnital a
                                          in (dualInj p1, dualInj p2)
               }

interface (MeetSemiLattice X, JoinSemiLattice X)
          => Lattice (X : Type)
          where {}

interface (BoundedMeetSemiLattice X, BoundedJoinSemiLattice X)
          => BoundedLattice (X : Type)
          where {}

interface (BoundedLattice X)
          => CompleteLattice (X : Type)
          where {
            arbJoin : (I : Type) -> (I -> X) -> X
            arbMeet : (I : Type) -> (I -> X) -> X
            -- LAWS???
          }

ltFromMSL : (M : Type) -> (MeetSemiLattice M) => M -> M -> Bool
ltFromMSL = ?fixme1

interface (MeetSemiLattice X, MeetSemiLattice Y)
          => MonotoneFunction (X : Type) (Y : Type) (f : X -> Y)
          where {
            isMonotone : (a : X) ->
                         (b : X) ->
                         ltFromMSL X a b = ltFromMSL Y (f a) (f b)
          }

implementation (X : Type, CompleteLattice X, MonotoneFunction X X f)
               => CompleteLattice (a : X ** (a = f a))
               where {
               }

main : IO ()
main = pure ()

max_stars_repo_name: taktoa/idris-absint

max_issues_repo_name: taktoa/idris-absint

max_forks_repo_name: taktoa/idris-absint


text:
module Web.Internal.SvgTypes

import JS

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

export data MathMLElement : Type where [external]

export
ToFFI MathMLElement MathMLElement where toFFI = id

export
FromFFI MathMLElement MathMLElement where fromFFI = Just

export
SafeCast MathMLElement where
  safeCast = unsafeCastOnPrototypeName "MathMLElement"

export data SVGAElement : Type where [external]

export
ToFFI SVGAElement SVGAElement where toFFI = id

export
FromFFI SVGAElement SVGAElement where fromFFI = Just

export
SafeCast SVGAElement where
  safeCast = unsafeCastOnPrototypeName "SVGAElement"

export data SVGAngle : Type where [external]

export
ToFFI SVGAngle SVGAngle where toFFI = id

export
FromFFI SVGAngle SVGAngle where fromFFI = Just

export
SafeCast SVGAngle where
  safeCast = unsafeCastOnPrototypeName "SVGAngle"

export data SVGAnimatedAngle : Type where [external]

export
ToFFI SVGAnimatedAngle SVGAnimatedAngle where toFFI = id

export
FromFFI SVGAnimatedAngle SVGAnimatedAngle where fromFFI = Just

export
SafeCast SVGAnimatedAngle where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedAngle"

export data SVGAnimatedBoolean : Type where [external]

export
ToFFI SVGAnimatedBoolean SVGAnimatedBoolean where toFFI = id

export
FromFFI SVGAnimatedBoolean SVGAnimatedBoolean where fromFFI = Just

export
SafeCast SVGAnimatedBoolean where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedBoolean"

export data SVGAnimatedEnumeration : Type where [external]

export
ToFFI SVGAnimatedEnumeration SVGAnimatedEnumeration where toFFI = id

export
FromFFI SVGAnimatedEnumeration SVGAnimatedEnumeration where fromFFI = Just

export
SafeCast SVGAnimatedEnumeration where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedEnumeration"

export data SVGAnimatedInteger : Type where [external]

export
ToFFI SVGAnimatedInteger SVGAnimatedInteger where toFFI = id

export
FromFFI SVGAnimatedInteger SVGAnimatedInteger where fromFFI = Just

export
SafeCast SVGAnimatedInteger where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedInteger"

export data SVGAnimatedLength : Type where [external]

export
ToFFI SVGAnimatedLength SVGAnimatedLength where toFFI = id

export
FromFFI SVGAnimatedLength SVGAnimatedLength where fromFFI = Just

export
SafeCast SVGAnimatedLength where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedLength"

export data SVGAnimatedLengthList : Type where [external]

export
ToFFI SVGAnimatedLengthList SVGAnimatedLengthList where toFFI = id

export
FromFFI SVGAnimatedLengthList SVGAnimatedLengthList where fromFFI = Just

export
SafeCast SVGAnimatedLengthList where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedLengthList"

export data SVGAnimatedNumber : Type where [external]

export
ToFFI SVGAnimatedNumber SVGAnimatedNumber where toFFI = id

export
FromFFI SVGAnimatedNumber SVGAnimatedNumber where fromFFI = Just

export
SafeCast SVGAnimatedNumber where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedNumber"

export data SVGAnimatedNumberList : Type where [external]

export
ToFFI SVGAnimatedNumberList SVGAnimatedNumberList where toFFI = id

export
FromFFI SVGAnimatedNumberList SVGAnimatedNumberList where fromFFI = Just

export
SafeCast SVGAnimatedNumberList where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedNumberList"

export data SVGAnimatedPreserveAspectRatio : Type where [external]

export
ToFFI SVGAnimatedPreserveAspectRatio SVGAnimatedPreserveAspectRatio where toFFI = id

export
FromFFI SVGAnimatedPreserveAspectRatio SVGAnimatedPreserveAspectRatio where fromFFI = Just

export
SafeCast SVGAnimatedPreserveAspectRatio where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedPreserveAspectRatio"

export data SVGAnimatedRect : Type where [external]

export
ToFFI SVGAnimatedRect SVGAnimatedRect where toFFI = id

export
FromFFI SVGAnimatedRect SVGAnimatedRect where fromFFI = Just

export
SafeCast SVGAnimatedRect where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedRect"

export data SVGAnimatedString : Type where [external]

export
ToFFI SVGAnimatedString SVGAnimatedString where toFFI = id

export
FromFFI SVGAnimatedString SVGAnimatedString where fromFFI = Just

export
SafeCast SVGAnimatedString where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedString"

export data SVGAnimatedTransformList : Type where [external]

export
ToFFI SVGAnimatedTransformList SVGAnimatedTransformList where toFFI = id

export
FromFFI SVGAnimatedTransformList SVGAnimatedTransformList where fromFFI = Just

export
SafeCast SVGAnimatedTransformList where
  safeCast = unsafeCastOnPrototypeName "SVGAnimatedTransformList"

export data SVGCircleElement : Type where [external]

export
ToFFI SVGCircleElement SVGCircleElement where toFFI = id

export
FromFFI SVGCircleElement SVGCircleElement where fromFFI = Just

export
SafeCast SVGCircleElement where
  safeCast = unsafeCastOnPrototypeName "SVGCircleElement"

export data SVGDefsElement : Type where [external]

export
ToFFI SVGDefsElement SVGDefsElement where toFFI = id

export
FromFFI SVGDefsElement SVGDefsElement where fromFFI = Just

export
SafeCast SVGDefsElement where
  safeCast = unsafeCastOnPrototypeName "SVGDefsElement"

export data SVGDescElement : Type where [external]

export
ToFFI SVGDescElement SVGDescElement where toFFI = id

export
FromFFI SVGDescElement SVGDescElement where fromFFI = Just

export
SafeCast SVGDescElement where
  safeCast = unsafeCastOnPrototypeName "SVGDescElement"

export data SVGElement : Type where [external]

export
ToFFI SVGElement SVGElement where toFFI = id

export
FromFFI SVGElement SVGElement where fromFFI = Just

export
SafeCast SVGElement where
  safeCast = unsafeCastOnPrototypeName "SVGElement"

export data SVGEllipseElement : Type where [external]

export
ToFFI SVGEllipseElement SVGEllipseElement where toFFI = id

export
FromFFI SVGEllipseElement SVGEllipseElement where fromFFI = Just

export
SafeCast SVGEllipseElement where
  safeCast = unsafeCastOnPrototypeName "SVGEllipseElement"

export data SVGForeignObjectElement : Type where [external]

export
ToFFI SVGForeignObjectElement SVGForeignObjectElement where toFFI = id

export
FromFFI SVGForeignObjectElement SVGForeignObjectElement where fromFFI = Just

export
SafeCast SVGForeignObjectElement where
  safeCast = unsafeCastOnPrototypeName "SVGForeignObjectElement"

export data SVGGElement : Type where [external]

export
ToFFI SVGGElement SVGGElement where toFFI = id

export
FromFFI SVGGElement SVGGElement where fromFFI = Just

export
SafeCast SVGGElement where
  safeCast = unsafeCastOnPrototypeName "SVGGElement"

export data SVGGeometryElement : Type where [external]

export
ToFFI SVGGeometryElement SVGGeometryElement where toFFI = id

export
FromFFI SVGGeometryElement SVGGeometryElement where fromFFI = Just

export
SafeCast SVGGeometryElement where
  safeCast = unsafeCastOnPrototypeName "SVGGeometryElement"

export data SVGGradientElement : Type where [external]

export
ToFFI SVGGradientElement SVGGradientElement where toFFI = id

export
FromFFI SVGGradientElement SVGGradientElement where fromFFI = Just

export
SafeCast SVGGradientElement where
  safeCast = unsafeCastOnPrototypeName "SVGGradientElement"

export data SVGGraphicsElement : Type where [external]

export
ToFFI SVGGraphicsElement SVGGraphicsElement where toFFI = id

export
FromFFI SVGGraphicsElement SVGGraphicsElement where fromFFI = Just

export
SafeCast SVGGraphicsElement where
  safeCast = unsafeCastOnPrototypeName "SVGGraphicsElement"

export data SVGImageElement : Type where [external]

export
ToFFI SVGImageElement SVGImageElement where toFFI = id

export
FromFFI SVGImageElement SVGImageElement where fromFFI = Just

export
SafeCast SVGImageElement where
  safeCast = unsafeCastOnPrototypeName "SVGImageElement"

export data SVGLength : Type where [external]

export
ToFFI SVGLength SVGLength where toFFI = id

export
FromFFI SVGLength SVGLength where fromFFI = Just

export
SafeCast SVGLength where
  safeCast = unsafeCastOnPrototypeName "SVGLength"

export data SVGLengthList : Type where [external]

export
ToFFI SVGLengthList SVGLengthList where toFFI = id

export
FromFFI SVGLengthList SVGLengthList where fromFFI = Just

export
SafeCast SVGLengthList where
  safeCast = unsafeCastOnPrototypeName "SVGLengthList"

export data SVGLineElement : Type where [external]

export
ToFFI SVGLineElement SVGLineElement where toFFI = id

export
FromFFI SVGLineElement SVGLineElement where fromFFI = Just

export
SafeCast SVGLineElement where
  safeCast = unsafeCastOnPrototypeName "SVGLineElement"

export data SVGLinearGradientElement : Type where [external]

export
ToFFI SVGLinearGradientElement SVGLinearGradientElement where toFFI = id

export
FromFFI SVGLinearGradientElement SVGLinearGradientElement where fromFFI = Just

export
SafeCast SVGLinearGradientElement where
  safeCast = unsafeCastOnPrototypeName "SVGLinearGradientElement"

export data SVGMarkerElement : Type where [external]

export
ToFFI SVGMarkerElement SVGMarkerElement where toFFI = id

export
FromFFI SVGMarkerElement SVGMarkerElement where fromFFI = Just

export
SafeCast SVGMarkerElement where
  safeCast = unsafeCastOnPrototypeName "SVGMarkerElement"

export data SVGMetadataElement : Type where [external]

export
ToFFI SVGMetadataElement SVGMetadataElement where toFFI = id

export
FromFFI SVGMetadataElement SVGMetadataElement where fromFFI = Just

export
SafeCast SVGMetadataElement where
  safeCast = unsafeCastOnPrototypeName "SVGMetadataElement"

export data SVGNumber : Type where [external]

export
ToFFI SVGNumber SVGNumber where toFFI = id

export
FromFFI SVGNumber SVGNumber where fromFFI = Just

export
SafeCast SVGNumber where
  safeCast = unsafeCastOnPrototypeName "SVGNumber"

export data SVGNumberList : Type where [external]

export
ToFFI SVGNumberList SVGNumberList where toFFI = id

export
FromFFI SVGNumberList SVGNumberList where fromFFI = Just

export
SafeCast SVGNumberList where
  safeCast = unsafeCastOnPrototypeName "SVGNumberList"

export data SVGPathElement : Type where [external]

export
ToFFI SVGPathElement SVGPathElement where toFFI = id

export
FromFFI SVGPathElement SVGPathElement where fromFFI = Just

export
SafeCast SVGPathElement where
  safeCast = unsafeCastOnPrototypeName "SVGPathElement"

export data SVGPatternElement : Type where [external]

export
ToFFI SVGPatternElement SVGPatternElement where toFFI = id

export
FromFFI SVGPatternElement SVGPatternElement where fromFFI = Just

export
SafeCast SVGPatternElement where
  safeCast = unsafeCastOnPrototypeName "SVGPatternElement"

export data SVGPointList : Type where [external]

export
ToFFI SVGPointList SVGPointList where toFFI = id

export
FromFFI SVGPointList SVGPointList where fromFFI = Just

export
SafeCast SVGPointList where
  safeCast = unsafeCastOnPrototypeName "SVGPointList"

export data SVGPolygonElement : Type where [external]

export
ToFFI SVGPolygonElement SVGPolygonElement where toFFI = id

export
FromFFI SVGPolygonElement SVGPolygonElement where fromFFI = Just

export
SafeCast SVGPolygonElement where
  safeCast = unsafeCastOnPrototypeName "SVGPolygonElement"

export data SVGPolylineElement : Type where [external]

export
ToFFI SVGPolylineElement SVGPolylineElement where toFFI = id

export
FromFFI SVGPolylineElement SVGPolylineElement where fromFFI = Just

export
SafeCast SVGPolylineElement where
  safeCast = unsafeCastOnPrototypeName "SVGPolylineElement"

export data SVGPreserveAspectRatio : Type where [external]

export
ToFFI SVGPreserveAspectRatio SVGPreserveAspectRatio where toFFI = id

export
FromFFI SVGPreserveAspectRatio SVGPreserveAspectRatio where fromFFI = Just

export
SafeCast SVGPreserveAspectRatio where
  safeCast = unsafeCastOnPrototypeName "SVGPreserveAspectRatio"

export data SVGRadialGradientElement : Type where [external]

export
ToFFI SVGRadialGradientElement SVGRadialGradientElement where toFFI = id

export
FromFFI SVGRadialGradientElement SVGRadialGradientElement where fromFFI = Just

export
SafeCast SVGRadialGradientElement where
  safeCast = unsafeCastOnPrototypeName "SVGRadialGradientElement"

export data SVGRectElement : Type where [external]

export
ToFFI SVGRectElement SVGRectElement where toFFI = id

export
FromFFI SVGRectElement SVGRectElement where fromFFI = Just

export
SafeCast SVGRectElement where
  safeCast = unsafeCastOnPrototypeName "SVGRectElement"

export data SVGSVGElement : Type where [external]

export
ToFFI SVGSVGElement SVGSVGElement where toFFI = id

export
FromFFI SVGSVGElement SVGSVGElement where fromFFI = Just

export
SafeCast SVGSVGElement where
  safeCast = unsafeCastOnPrototypeName "SVGSVGElement"

export data SVGScriptElement : Type where [external]

export
ToFFI SVGScriptElement SVGScriptElement where toFFI = id

export
FromFFI SVGScriptElement SVGScriptElement where fromFFI = Just

export
SafeCast SVGScriptElement where
  safeCast = unsafeCastOnPrototypeName "SVGScriptElement"

export data SVGStopElement : Type where [external]

export
ToFFI SVGStopElement SVGStopElement where toFFI = id

export
FromFFI SVGStopElement SVGStopElement where fromFFI = Just

export
SafeCast SVGStopElement where
  safeCast = unsafeCastOnPrototypeName "SVGStopElement"

export data SVGStringList : Type where [external]

export
ToFFI SVGStringList SVGStringList where toFFI = id

export
FromFFI SVGStringList SVGStringList where fromFFI = Just

export
SafeCast SVGStringList where
  safeCast = unsafeCastOnPrototypeName "SVGStringList"

export data SVGStyleElement : Type where [external]

export
ToFFI SVGStyleElement SVGStyleElement where toFFI = id

export
FromFFI SVGStyleElement SVGStyleElement where fromFFI = Just

export
SafeCast SVGStyleElement where
  safeCast = unsafeCastOnPrototypeName "SVGStyleElement"

export data SVGSwitchElement : Type where [external]

export
ToFFI SVGSwitchElement SVGSwitchElement where toFFI = id

export
FromFFI SVGSwitchElement SVGSwitchElement where fromFFI = Just

export
SafeCast SVGSwitchElement where
  safeCast = unsafeCastOnPrototypeName "SVGSwitchElement"

export data SVGSymbolElement : Type where [external]

export
ToFFI SVGSymbolElement SVGSymbolElement where toFFI = id

export
FromFFI SVGSymbolElement SVGSymbolElement where fromFFI = Just

export
SafeCast SVGSymbolElement where
  safeCast = unsafeCastOnPrototypeName "SVGSymbolElement"

export data SVGTSpanElement : Type where [external]

export
ToFFI SVGTSpanElement SVGTSpanElement where toFFI = id

export
FromFFI SVGTSpanElement SVGTSpanElement where fromFFI = Just

export
SafeCast SVGTSpanElement where
  safeCast = unsafeCastOnPrototypeName "SVGTSpanElement"

export data SVGTextContentElement : Type where [external]

export
ToFFI SVGTextContentElement SVGTextContentElement where toFFI = id

export
FromFFI SVGTextContentElement SVGTextContentElement where fromFFI = Just

export
SafeCast SVGTextContentElement where
  safeCast = unsafeCastOnPrototypeName "SVGTextContentElement"

export data SVGTextElement : Type where [external]

export
ToFFI SVGTextElement SVGTextElement where toFFI = id

export
FromFFI SVGTextElement SVGTextElement where fromFFI = Just

export
SafeCast SVGTextElement where
  safeCast = unsafeCastOnPrototypeName "SVGTextElement"

export data SVGTextPathElement : Type where [external]

export
ToFFI SVGTextPathElement SVGTextPathElement where toFFI = id

export
FromFFI SVGTextPathElement SVGTextPathElement where fromFFI = Just

export
SafeCast SVGTextPathElement where
  safeCast = unsafeCastOnPrototypeName "SVGTextPathElement"

export data SVGTextPositioningElement : Type where [external]

export
ToFFI SVGTextPositioningElement SVGTextPositioningElement where toFFI = id

export
FromFFI SVGTextPositioningElement SVGTextPositioningElement where fromFFI = Just

export
SafeCast SVGTextPositioningElement where
  safeCast = unsafeCastOnPrototypeName "SVGTextPositioningElement"

export data SVGTitleElement : Type where [external]

export
ToFFI SVGTitleElement SVGTitleElement where toFFI = id

export
FromFFI SVGTitleElement SVGTitleElement where fromFFI = Just

export
SafeCast SVGTitleElement where
  safeCast = unsafeCastOnPrototypeName "SVGTitleElement"

export data SVGTransform : Type where [external]

export
ToFFI SVGTransform SVGTransform where toFFI = id

export
FromFFI SVGTransform SVGTransform where fromFFI = Just

export
SafeCast SVGTransform where
  safeCast = unsafeCastOnPrototypeName "SVGTransform"

export data SVGTransformList : Type where [external]

export
ToFFI SVGTransformList SVGTransformList where toFFI = id

export
FromFFI SVGTransformList SVGTransformList where fromFFI = Just

export
SafeCast SVGTransformList where
  safeCast = unsafeCastOnPrototypeName "SVGTransformList"

export data SVGUnitTypes : Type where [external]

export
ToFFI SVGUnitTypes SVGUnitTypes where toFFI = id

export
FromFFI SVGUnitTypes SVGUnitTypes where fromFFI = Just

export
SafeCast SVGUnitTypes where
  safeCast = unsafeCastOnPrototypeName "SVGUnitTypes"

export data SVGUseElement : Type where [external]

export
ToFFI SVGUseElement SVGUseElement where toFFI = id

export
FromFFI SVGUseElement SVGUseElement where fromFFI = Just

export
SafeCast SVGUseElement where
  safeCast = unsafeCastOnPrototypeName "SVGUseElement"

export data SVGUseElementShadowRoot : Type where [external]

export
ToFFI SVGUseElementShadowRoot SVGUseElementShadowRoot where toFFI = id

export
FromFFI SVGUseElementShadowRoot SVGUseElementShadowRoot where fromFFI = Just

export
SafeCast SVGUseElementShadowRoot where
  safeCast = unsafeCastOnPrototypeName "SVGUseElementShadowRoot"

export data SVGViewElement : Type where [external]

export
ToFFI SVGViewElement SVGViewElement where toFFI = id

export
FromFFI SVGViewElement SVGViewElement where fromFFI = Just

export
SafeCast SVGViewElement where
  safeCast = unsafeCastOnPrototypeName "SVGViewElement"

export data ShadowAnimation : Type where [external]

export
ToFFI ShadowAnimation ShadowAnimation where toFFI = id

export
FromFFI ShadowAnimation ShadowAnimation where fromFFI = Just

export
SafeCast ShadowAnimation where
  safeCast = unsafeCastOnPrototypeName "ShadowAnimation"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data SVGBoundingBoxOptions : Type where [external]

export
ToFFI SVGBoundingBoxOptions SVGBoundingBoxOptions where toFFI = id

export
FromFFI SVGBoundingBoxOptions SVGBoundingBoxOptions where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data GetSVGDocument : Type where [external]

export
ToFFI GetSVGDocument GetSVGDocument where toFFI = id

export
FromFFI GetSVGDocument GetSVGDocument where fromFFI = Just

export data SVGAnimatedPoints : Type where [external]

export
ToFFI SVGAnimatedPoints SVGAnimatedPoints where toFFI = id

export
FromFFI SVGAnimatedPoints SVGAnimatedPoints where fromFFI = Just

export data SVGElementInstance : Type where [external]

export
ToFFI SVGElementInstance SVGElementInstance where toFFI = id

export
FromFFI SVGElementInstance SVGElementInstance where fromFFI = Just

export data SVGFitToViewBox : Type where [external]

export
ToFFI SVGFitToViewBox SVGFitToViewBox where toFFI = id

export
FromFFI SVGFitToViewBox SVGFitToViewBox where fromFFI = Just

export data SVGTests : Type where [external]

export
ToFFI SVGTests SVGTests where toFFI = id

export
FromFFI SVGTests SVGTests where fromFFI = Just

export data SVGURIReference : Type where [external]

export
ToFFI SVGURIReference SVGURIReference where toFFI = id

export
FromFFI SVGURIReference SVGURIReference where fromFFI = Just


text:
module Bifunctor

||| Bifunctors
||| @p The action of the Bifunctor on pairs of objects
public export
interface Bifunctor (p : Type -> Type -> Type) where
  ||| The action of the Bifunctor on pairs of morphisms
  |||
  ||| ````idris example
  ||| bimap (\x => x + 1) reverse (1, "hello") == (2, "olleh")
  ||| ````
  |||
  bimap : (a -> b) -> (c -> d) -> p a c -> p b d
  bimap f g = first f . second g

  ||| The action of the Bifunctor on morphisms pertaining to the first object
  |||
  ||| ````idris example
  ||| first (\x => x + 1) (1, "hello") == (2, "hello")
  ||| ````
  |||
  first : (a -> b) -> p a c -> p b c
  first = flip bimap id

  ||| The action of the Bifunctor on morphisms pertaining to the second object
  |||
  ||| ````idris example
  ||| second reverse (1, "hello") == (1, "olleh")
  ||| ````
  |||
  second : (a -> b) -> p c a -> p c b
  second = bimap id

implementation Bifunctor Either where
  bimap f _ (Left  a) = Left  $ f a
  bimap _ g (Right b) = Right $ g b

public export
implementation Bifunctor Pair where
  bimap f g (a, b) = (f a, g b)


text:
module Issue735

-- Not allowed to pattern-match on under-applied constructors
isCons : (a -> List a -> List a) -> Bool
isCons (::) = True
isCons _ = False

interface A a where

-- Not allowed to pattern-match on under-applied type constructors
test : (kind : Type -> Type) -> Maybe Nat
test A = Just 1
test _ = Nothing


text:
||| Dependent sorted maps
|||
||| Mostly copied from Data.SortedMap, but with some changes
module Extra.Data.DepMap

import Decidable.Equality

||| Used to report errors when key lookups don't agree
public export
data BadKey : (k : Type) -> (Ord k, DecEq k) => Type where
  KeyIsBad : (Ord k, DecEq k)
    => (x : k) -> (y : k)
    -> (compare x y = EQ)
    -> Not (x = y)
    -> BadKey k

-- Multiplicities are very intentional here, I just haven't gotten around to
-- "linear"-izing the rest of the library
data Tree : Nat -> (k : Type) -> (k -> Type) -> Type where
  Leaf : (x : k) -> (1 _ : p x) -> Tree Z k p
  Branch2 :
    (1 _ : Tree n k p) -> k ->
    (1 _ : Tree n k p) ->
    Tree (S n) k p
  Branch3 :
    (1 _ : Tree n k p) -> k ->
    (1 _ : Tree n k p) -> k ->
    (1 _ : Tree n k p) ->
    Tree (S n) k p

branch4 :
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) ->
  Tree (S (S n)) k p
branch4 a b c d e f g =
  Branch2 (Branch2 a b c) d (Branch2 e f g)

branch5 :
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) ->
  Tree (S (S n)) k p
branch5 a b c d e f g h i =
  Branch2 (Branch2 a b c) d (Branch3 e f g h i)

branch6 :
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) ->
  Tree (S (S n)) k p
branch6 a b c d e f g h i j k =
  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

branch7 :
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) -> k ->
  (1 _ : Tree n k p) ->
  Tree (S (S n)) k p
branch7 a b c d e f g h i j k l m =
  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

merge1 :
  (1 _ : Tree    n  k p) -> k ->
  (1 _ : Tree (S n) k p) -> k ->
  (1 _ : Tree (S n) k p) ->
  Tree (S (S n)) k p
merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge2 :
  (1 _ : Tree (S n) k p) -> k ->
  (1 _ : Tree    n  k p) -> k ->
  (1 _ : Tree (S n) k p) ->
  Tree (S (S n)) k p
merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge3 :
  (1 _ : Tree (S n) k p) -> k ->
  (1 _ : Tree (S n) k p) -> k ->
  (1 _ : Tree    n  k p) ->
  Tree (S (S n)) k p
merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

treeLookup : (Ord k, DecEq k) => (x : k) -> Tree n k p -> Either (BadKey k) (Maybe (p x))
treeLookup k (Leaf k' v) with (KeyIsBad k k')
  treeLookup k (Leaf k' v) | err with (compare k k')
    treeLookup k (Leaf k' v) | err | EQ with (decEq k k')
      treeLookup k (Leaf k  v) | err | EQ | Yes Refl = Right $ Just v
      treeLookup k (Leaf k' v) | err | EQ | No bad = Left $ err Refl bad
    treeLookup k (Leaf k' v) | err | _ = Right Nothing
treeLookup k (Branch2 t1 k' t2) =
  if k <= k' then
    treeLookup k t1
  else
    treeLookup k t2
treeLookup k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    treeLookup k t1
  else if k <= k2 then
    treeLookup k t2
  else
    treeLookup k t3

treeInsert' : Ord k
  => (x : k) -> p x
  -> Tree n k p
  -> Either (Tree n k p) (Tree n k p, k, Tree n k p)
treeInsert' k v (Leaf k' v') =
  case compare k k' of
    LT => Right (Leaf k v, k, Leaf k' v')
    EQ => Left (Leaf k v)
    GT => Right (Leaf k' v', k', Leaf k v)
treeInsert' k v (Branch2 t1 k' t2) =
  if k <= k' then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right (a, b, c) => Left (Branch3 a b c k' t2)
  else
    case treeInsert' k v t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right (a, b, c) => Left (Branch3 t1 k' a b c)
treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
  else
    if k <= k2 then
      case treeInsert' k v t2 of
        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
    else
      case treeInsert' k v t3 of
        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)

treeInsert : Ord k
  => (x : k) -> p x
  -> Tree n k p
  -> Either (Tree n k p) (Tree (S n) k p)
treeInsert k v t =
  case treeInsert' k v t of
    Left t' => Left t'
    Right (a, b, c) => Right (Branch2 a b c)

delType : Nat -> (k : Type) -> (k -> Type) -> Type
delType Z k p = ()
delType (S n) k p = Tree n k p

treeDelete : Ord k => (n : Nat) -> k -> Tree n k p -> Either (Tree n k p) (delType n k p)
treeDelete _ k (Leaf k' v) =
  if k == k' then
    Right ()
  else
    Left (Leaf k' v)
treeDelete (S Z) k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete Z k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right () => Right t2
  else
    case treeDelete Z k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right () => Right t1
treeDelete (S Z) k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete Z k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right () => Left (Branch2 t2 k2 t3)
  else if k <= k2 then
    case treeDelete Z k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right () => Left (Branch2 t1 k1 t3)
  else
    case treeDelete Z k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right () => Left (Branch2 t1 k1 t2)
treeDelete (S (S n)) k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete (S n) k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right t1' =>
        case t2 of
          Branch2 a b c => Right (Branch3 t1' k' a b c)
          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
  else
    case treeDelete (S n) k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right t2' =>
        case t1 of
          Branch2 a b c => Right (Branch3 a b c k' t2')
          Branch3 a b c d e => Left (branch4 a b c d e k' t2')
treeDelete (S (S n)) k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete (S n) k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right t1' => Left (merge1 t1' k1 t2 k2 t3)
  else if k <= k2 then
    case treeDelete (S n) k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right t2' => Left (merge2 t1 k1 t2' k2 t3)
  else
    case treeDelete (S n) k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right t3' => Left (merge3 t1 k1 t2 k2 t3')

treeToList : Tree n k p -> List (DPair k p)
treeToList = treeToList' (:: [])
  where
    -- explicit quantification to avoid conflation with {n} from treeToList
    treeToList' : {0 n : Nat} -> (DPair k p -> List (DPair k p)) -> Tree n k p -> List (DPair k p)
    treeToList' cont (Leaf k v) = cont (k ** v)
    treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
    treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

export
data DepMap : (k : Type) -> (k -> Type) -> Type where
  Empty : DepMap k p
  M : (n : Nat) -> Tree n k p -> DepMap k p

export
empty : DepMap k p
empty = Empty

export
lookup : (Ord k, DecEq k)
  => (x : k)
  -> DepMap k p
  -> Either (BadKey k) (Maybe (p x))
lookup _ Empty = Right Nothing
lookup k (M _ t) = treeLookup k t

export
insert : Ord k
  => (x : k) -> p x
  -> DepMap k p
  -> DepMap k p
insert k v Empty = M Z (Leaf k v)
insert k v (M _ t) =
  case treeInsert k v t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
singleton : Ord k => (x : k) -> p x -> DepMap k p
singleton k v = insert k v empty

export
insertFrom : (Ord k, Foldable f) => f (DPair k p) -> DepMap k p -> DepMap k p
insertFrom = flip $ foldl $ flip insert'
  where insert' : DPair k p -> DepMap k p -> DepMap k p
        insert' (k ** v) = insert k v

export
delete : Ord k => k -> DepMap k p -> DepMap k p
delete _ Empty = Empty
delete k (M Z t) =
  case treeDelete Z k t of
    Left t' => (M _ t')
    Right () => Empty
delete k (M (S n) t) =
  case treeDelete (S n) k t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
fromList : Ord k => List (DPair k p) -> DepMap k p
fromList l = foldl (flip insert') empty l
  where insert' : DPair k p -> DepMap k p -> DepMap k p
        insert' (k ** v) = insert k v

export
toList : DepMap k p -> List (DPair k p)
toList Empty = []
toList (M _ t) = treeToList t

||| Gets the keys of the map.
export
keys : DepMap k p -> List k
keys = map fst . toList

-- Not really that possible
-- ||| Gets the values of the map. Could contain duplicates.
-- export
-- values : DepMap k v -> List v
-- values = map snd . toList

export
null : DepMap k p -> Bool
null Empty = True
null (M _ _) = False

treeMap : ((x : k) -> a x -> b x) -> Tree n k a -> Tree n k b
treeMap f (Leaf k v) = Leaf k (f k v)
treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
treeMap f (Branch3 t1 k1 t2 k2 t3)
    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

treeTraverse : Applicative f
  => ((x : k) -> a x -> f (b x))
  -> Tree n k a
  -> f (Tree n k b)
treeTraverse f (Leaf k v) = Leaf k <$> f k v
treeTraverse f (Branch2 t1 k t2) =
  Branch2
    <$> treeTraverse f t1
    <*> pure k
    <*> treeTraverse f t2
treeTraverse f (Branch3 t1 k1 t2 k2 t3) =
  Branch3
    <$> treeTraverse f t1
    <*> pure k1
    <*> treeTraverse f t2
    <*> pure k2
    <*> treeTraverse f t3

||| Not a Functor, but close enough
||| Still a functor from the category of Idris endofunctors to Idris tho?
export
map : ({x : k} -> a x -> b x) -> DepMap k a -> DepMap k b
map _ Empty = Empty
map f (M n t) = M n (treeMap (\k, v => f v) t)

||| Not a traversable, but close enough
export
traverse : Applicative f
  => ({x : k} -> a x -> f (b x))
  -> DepMap k a -> f (DepMap k b)
traverse _ Empty = pure Empty
traverse f (M n t) = M n <$> treeTraverse (\k, v => f v) t

||| Merge two maps. When encountering duplicate keys, using a function to
||| combine the values.
-- TODO: this could totally have better linearity
export
mergeWith : (Ord k, DecEq k)
  => ({x : k} -> p x -> p x -> p x)
  -> DepMap k p
  -> DepMap k p
  -> Either (BadKey k) (DepMap k p)
mergeWith f x y = flip insertFrom x <$> traverse go (toList y)
  where go : DPair k p -> Either (BadKey k) (DPair k p)
        go (a ** v) with (lookup a x)
          go (a ** v) | Left bad = Left bad
          go (a ** v) | Right Nothing = Right (a ** v)
          go (a ** v) | Right (Just v') = Right (a ** f v v')

||| Left-biased merge
-- TODO: lift DecEq requirement? idk
-- would require a lot of work, so prob not
mergeLeft : (Ord k, DecEq k)
  => DepMap k p
  -> DepMap k p
  -> Either (BadKey k) (DepMap k p)
mergeLeft = mergeWith (\x, y => x)


text:
module Idris.Package.Types

import Core.FC
import Core.Name.Namespace
import Data.Maybe
import Data.String
import Idris.CommandLine
import Idris.Version
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util

%default total

------------------------------------------------------------------------------
-- Versions

public export
data PkgVersion = MkPkgVersion (List1 Nat)

export
Show PkgVersion where
  show (MkPkgVersion vs) = showSep "." (map show (forget vs))

export
Pretty PkgVersion where
  pretty = pretty . show

export
Eq PkgVersion where
  MkPkgVersion p == MkPkgVersion q = p == q

export
Ord PkgVersion where
  -- list ordering gives us what we want
  compare (MkPkgVersion p) (MkPkgVersion q) = compare p q

------------------------------------------------------------------------------
-- Version Bounds

-- version must be >= lowerBound and <= upperBound
-- Do we want < and > as well?
public export
record PkgVersionBounds where
  constructor MkPkgVersionBounds
  lowerBound : Maybe PkgVersion
  lowerInclusive : Bool -- >= if true
  upperBound : Maybe PkgVersion
  upperInclusive : Bool -- <= if true

export
Show PkgVersionBounds where
  show p = if noBounds then "any" else lowerBounds ++ upperBounds

    where

      noBounds : Bool
      noBounds = isNothing p.lowerBound && isNothing p.upperBound

      lowerBounds : String
      lowerBounds = case p.lowerBound of
        Nothing => ""
        Just v  => (if p.lowerInclusive then ">= " else "> ") ++ show v ++ " "

      upperBounds : String
      upperBounds = case p.upperBound of
        Nothing => ""
        Just v  => (if p.upperInclusive then "<= " else "< ") ++ show v

export
anyBounds : PkgVersionBounds
anyBounds = MkPkgVersionBounds Nothing True Nothing True

export
current : PkgVersionBounds
current = let (maj,min,patch) = semVer version
              version = Just (MkPkgVersion (maj ::: [min, patch])) in
              MkPkgVersionBounds version True version True

export
inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool
inBounds mv bounds
   = let v = fromMaybe (MkPkgVersion (0 ::: [])) mv in
     maybe True (\v' => if bounds.lowerInclusive
                           then v >= v'
                           else v > v') bounds.lowerBound &&
     maybe True (\v' => if bounds.upperInclusive
                           then v <= v'
                           else v < v') bounds.upperBound

------------------------------------------------------------------------------
-- Dependencies

public export
record Depends where
  constructor MkDepends
  pkgname : String
  pkgbounds : PkgVersionBounds

export
Show Depends where
  show p = p.pkgname ++ " " ++ show p.pkgbounds

export
Pretty Depends where
  pretty = pretty . show

------------------------------------------------------------------------------
-- Package description

public export
record PkgDesc where
  constructor MkPkgDesc
  name : String
  version : Maybe PkgVersion
  authors : Maybe String
  maintainers : Maybe String
  license : Maybe String
  brief   : Maybe String
  readme  : Maybe String
  homepage : Maybe String
  sourceloc : Maybe String
  bugtracker : Maybe String
  depends : List Depends -- packages to add to search path
  modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
  mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
  executable : Maybe String -- name of executable
  options : Maybe (FC, String)
  sourcedir : Maybe String
  builddir : Maybe String
  outputdir : Maybe String
  prebuild : Maybe (FC, String) -- Script to run before building
  postbuild : Maybe (FC, String) -- Script to run after building
  preinstall : Maybe (FC, String) -- Script to run after building, before installing
  postinstall : Maybe (FC, String) -- Script to run after installing
  preclean : Maybe (FC, String) -- Script to run before cleaning
  postclean : Maybe (FC, String) -- Script to run after cleaning

export
initPkgDesc : String -> PkgDesc
initPkgDesc pname
    = MkPkgDesc pname Nothing Nothing Nothing Nothing
                Nothing Nothing Nothing Nothing Nothing
                [] []
                Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
                Nothing Nothing Nothing Nothing

export
Show PkgDesc where
  show pkg = "Package: " ++ name pkg ++ "\n" ++
             maybe "" (\m => "Version: "     ++ m ++ "\n") (show <$> version pkg) ++
             maybe "" (\m => "Authors: "     ++ m ++ "\n") (authors pkg)     ++
             maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
             maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
             maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
             maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
             maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
             maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
             maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
             "Depends: " ++ show (depends pkg) ++ "\n" ++
             "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
             maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
             maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
             maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
             maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
             maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
             maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
             maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
             maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
             maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
             maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
             maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)

export
Pretty PkgDesc where
  pretty desc = vcat
    [ "package" <++> pretty desc.name
    , verField "version"     desc.version
    , strField "authors"     desc.authors
    , strField "maintainers" desc.maintainers
    , strField "license"     desc.license
    , strField "brief"       desc.brief
    , strField "readme"      desc.readme
    , strField "homepage"    desc.homepage
    , strField "sourceloc"   desc.sourceloc
    , strField "bugtracker"  desc.bugtracker

    , comment  "packages to add to search path"
    , seqField "depends"     desc.depends

    , comment "modules to install"
    , seqField "modules"     (fst <$> desc.modules)

    , comment "main file (i.e. file to load at REPL)"
    , field    "main"        (map (pretty . fst) desc.mainmod)

    , comment "name of executable"
    , strField "executable"  desc.executable
    , strField "opts"        (snd <$> desc.options)
    , strField "sourcedir"   desc.sourcedir
    , strField "builddir"    desc.builddir
    , strField "outputdir"   desc.outputdir

    , comment "script to run before building"
    , strField "prebuild"    (snd <$> desc.prebuild)

    , comment "script to run after building"
    , strField "postbuild"   (snd <$> desc.postbuild)

    , comment "script to run after building, before installing"
    , strField "preinstall"  (snd <$> desc.preinstall)

    , comment "script to run after installing"
    , strField "postinstall" (snd <$> desc.postinstall)

    , comment "script to run before cleaning"
    , strField "preclean"    (snd <$> desc.preclean)

    , comment "script to run after cleaning"
    , strField "postclean"   (snd <$> desc.postclean)
    ]

  where

    comment : String -> Doc ann
    comment str =
      let ws = "--" :: words str in
      let commSoftLine = Union (Chara ' ') (hcat [Line, pretty "-- "]) in
      Line <+> concatWith (\x, y => x <+> commSoftLine <+> y) ws

    field : String -> Maybe (Doc ann) -> Doc ann
    field nm Nothing = hsep [ pretty "--", pretty nm, equals ]
    field nm (Just d) = hsep [ pretty nm, equals, d ]

    verField : String -> Maybe PkgVersion -> Doc ann
    verField nm = field nm . map pretty

    strField : String -> Maybe String -> Doc ann
    strField nm = field nm . map (pretty . show)

    seqField : Pretty a => String -> List a -> Doc ann
    seqField nm [] = hsep [ pretty "--", pretty nm, equals ]
    seqField nm xs = pretty nm
                <++> equals
                <++> align (sep (punctuate comma (map pretty xs)))

------------------------------------------------------------------------------
-- CSS files (used in --mkdoc)

public export
record CSS where
  constructor MkCSS
  stylename : String
  filename  : String

export
cssFiles : List CSS
cssFiles = [ MkCSS "Default"       "default"
           , MkCSS "Alternative"   "alternative"
           , MkCSS "Black & White" "blackandwhite"
           ]


text:
twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape

turn_around : Shape -> Shape
turn_around = twice rotate


text:
lplus : (1 x : Nat) -> (1 y : Nat) -> Nat
lplus Z y = y
lplus (S k) y = S (lplus k y)

foo : (1 x : Nat) -> (1 y : Nat) -> Nat -> Nat
foo x y z
    = let 1 test = the Nat $ case z of
                        Z => Z
                        (S k) => S z
            in
          lplus test x


text:
import Stuff

(>>=) : (Maybe a) -> (a -> Maybe b) -> Maybe b
(>>=) Nothing k = Nothing
(>>=) (Just x) k = k x

mthings : (foo : Maybe (Maybe Int)) -> (bar : Maybe (Maybe Int)) -> Maybe Int
mthings mx my
    = do Just x <- mx
            | Nothing => Just 0
         Just y <- my
            | Nothing => Just 1
         let z : Int -> Int
             z x = prim__add_Int x y
         Just (z (prim__add_Int x x))


text:
module CIL.FFI

%default total

%access public

||| The universe of foreign CIL types.
data CILTy =
  ||| a foreign reference type
  CILTyRef String String |
  ||| a foreign value type
  CILTyVal String String |
  ||| a foreign array type
  CILTyArr CILTy |
  ||| a foreign generic type
  CILTyGen CILTy (List CILTy) |
  ||| a foreign generic parameter
  CILTyGenParam String

instance Eq CILTy where
  (CILTyGen def args) == (CILTyGen def' args') = def  == def' && assert_total (args == args')
  (CILTyRef as tn)    == (CILTyRef as' tn')    = as   == as'  && tn == tn'
  (CILTyVal as tn)    == (CILTyVal as' tn')    = as   == as'  && tn == tn'
  (CILTyArr elTy)     == (CILTyArr elTy')      = elTy == elTy'
  _                   == _                     = False

%inline
CILTyObj : CILTy
CILTyObj = CILTyRef "" "object"

%inline
CILTyStr : CILTy
CILTyStr = CILTyRef "" "string"

%inline
CILTyBool : CILTy
CILTyBool = CILTyVal "" "bool"

||| A foreign CIL type.
data CIL   : CILTy -> Type where
     MkCIL : (ty : CILTy) -> CIL ty

||| A foreign descriptor.
data CILForeign =
  ||| Call the named instance method.
  CILInstance String |
  ||| Call the named instance method with the given signature.
  CILInstanceCustom String (List CILTy) CILTy |
  ||| Read the value of the named instance field.
  CILInstanceField String |
  ||| Call the named static method of the given foreign type.
  CILStatic CILTy String |
  ||| Read the value of the named static field of the given foreign type.
  CILStaticField CILTy String |
  ||| Box the integer value given as a string into the given enum type.
  CILEnumValueOf CILTy String |
  ||| Call a constructor to instantiate an object.
  CILConstructor |
  ||| Load the given runtime type.
  CILTypeOf CILTy |
  ||| Convert a function to a delegate of the given type.
  CILDelegate CILTy |
  ||| Export a function under the given name.
  CILExport String |
  ||| Export a function under its original name.
  CILDefault

mutual
  data CIL_IntTypes  : Type -> Type where
       CIL_IntChar   : CIL_IntTypes Char
       CIL_IntNative : CIL_IntTypes Int

  data CIL_Types : Type -> Type where
       CIL_Str   : CIL_Types String
       CIL_Float : CIL_Types Double
       CIL_Ptr   : CIL_Types Ptr
       CIL_Bool  : CIL_Types Bool
       CIL_Unit  : CIL_Types ()
       CIL_IntT  : CIL_IntTypes i -> CIL_Types i
       CIL_CILT  : CIL_Types (CIL ty)
       CIL_FnT   : CIL_FnTypes fnT -> CIL_Types (CilFn delegateTy fnT)

  data CilFn   : CILTy -> Type -> Type where
       MkCilFn : (delegateTy : CILTy) -> (fn : fnT) -> CilFn delegateTy fnT

  data CIL_FnTypes : Type -> Type where
       CIL_Fn      : CIL_Types s -> CIL_FnTypes t -> CIL_FnTypes (s -> t)
       CIL_FnIO    : CIL_Types t -> CIL_FnTypes (IO' l t)
       CIL_FnBase  : CIL_Types t -> CIL_FnTypes t

%used MkCilFn fn

FFI_CIL : FFI
FFI_CIL = MkFFI CIL_Types CILForeign String

CIL_IO : Type -> Type
CIL_IO a = IO' FFI_CIL a

||| CIL FFI.
invoke : CILForeign -> (ty : Type) ->
         {auto fty : FTy FFI_CIL [] ty} -> ty
invoke ffi ty = foreign FFI_CIL ffi ty

%inline
new : (ty : Type) ->
      {auto fty : FTy FFI_CIL [] ty} -> ty
new ty = invoke CILConstructor ty

%inline
delegate : (ty : CILTy) -> (fnT : Type) -> fnT ->
           {auto fty : FTy FFI_CIL [] (CilFn ty fnT -> CIL_IO (CilFn ty fnT))} ->
           CIL_IO (CilFn ty fnT)
delegate ty fnT fn = invoke (CILDelegate ty)
                            (CilFn ty fnT -> CIL_IO (CilFn ty fnT))
                            (MkCilFn ty fn)

%inline
corlibTy : String -> CILTy
corlibTy = CILTyRef "mscorlib"

%inline
corlibTyVal : String -> CILTy
corlibTyVal = CILTyVal "mscorlib"

%inline
corlib : String -> Type
corlib = CIL . corlibTy

Object : Type
Object = CIL CILTyObj

ObjectArray : Type
ObjectArray = CIL (CILTyArr CILTyObj)

RuntimeType : Type
RuntimeType = corlib "System.Type"

%inline
typeOf : CILTy -> CIL_IO RuntimeType
typeOf t = invoke (CILTypeOf t) (CIL_IO RuntimeType)

-- inheritance can be encoded as class instances or implicit conversions
class IsA a b where {}

instance IsA Object Object where {}
instance IsA Object RuntimeType where {}

ToString : IsA Object o => o -> CIL_IO String
ToString obj =
  invoke (CILInstance "ToString")
         (Object -> CIL_IO String)
         (believe_me obj)

Equals : IsA Object a => a -> a -> CIL_IO Bool
Equals x y =
  invoke (CILInstance "Equals")
         (Object -> Object -> CIL_IO Bool)
         (believe_me x) (believe_me y)

namespace System.Array
  ArrayTy : CILTy
  ArrayTy = corlibTy "System.Array"

  Array : Type
  Array = CIL ArrayTy

  CreateInstance : RuntimeType -> Int -> CIL_IO Array
  CreateInstance =
    invoke (CILStatic ArrayTy "CreateInstance")
           (RuntimeType -> Int -> CIL_IO Array)

  SetValue : Array -> Object -> Int -> CIL_IO ()
  SetValue =
    invoke (CILInstance "SetValue")
           (Array -> Object -> Int -> CIL_IO ())

  partial
  fromList : List a -> CIL_IO ObjectArray
  fromList [v] = do
    array <- CreateInstance !(typeOf CILTyObj) 1
    SetValue array (believe_me v) 0
    return $ believe_me array

namespace System.Convert
  ToInt32 : IsA Object a => a -> CIL_IO Int
  ToInt32 o =
    invoke (CILStatic (corlibTy "System.Convert") "ToInt32")
           (Ptr -> CIL_IO Int)
           (believe_me o)

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil