text:
> module InfiniteHorizonSequentialDecisionProblems.Theory

> import Data.Vect

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Vect.Operations

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

* Sequential decision processes

> State  :  Type
> Ctrl   :  (x : State) -> Type
> M      :  Type -> Type
> nexts  :  (x : State) -> (y : Ctrl x) -> M State
> fmap   :  {A, B : Type} -> (A -> B) -> M A -> M B

* Sequential decision problems

> Val              :  Type
> reward           :  (x : State) -> (y : Ctrl x) -> (x' : State) -> Val
> plus             :  Val -> Val -> Val
> LTE              :  Val -> Val -> Type
> meas             :  M Val -> Val

* Policies

> Policy  :  Type
> Policy  =  (x : State) -> Ctrl x

* The value of policies

> ||| A value function ...
> val : State -> Policy -> Val

> ||| ... that fulfils the specification
> valSpec  :  Type
> valSpec  =  (x : State) -> (p : Policy) ->
>             val x p
>             =
>             meas (fmap (\ x' => reward x (p x) x' `plus` val x' p) (nexts x (p x)))

* Optimality of policies

> |||
> Opt    :  Policy -> Type
> Opt p  =  (x : State) -> (p' : Policy) -> val x p' `LTE` val x p

* Optimal policies

> |||
> cval        :  (x : State) -> Ctrl x -> (p : Policy) -> Val
> cval x y p  =  meas (fmap (\ x' => reward x y x' `plus` val x' p) (nexts x y))

> cvalargmax      :  (x : State) -> (p : Policy) -> Ctrl x

> ||| A policy ...
> opt : Policy

> ||| ... that fulfils Bellman's equation
> optSpec  :  Type
> optSpec  =  (x : State) -> opt x = cvalargmax x opt

* Optimality of |opt|

** Additional assumptions

> reflexiveLTE     :  (a : Val) -> a `LTE` a
> transitiveLTE    :  {a, b, c : Val} -> a `LTE` b -> b `LTE` c -> a `LTE` c
> monotonePlusLTE  :  {a, b, c, d : Val} -> a `LTE` b -> c `LTE` d -> (a `plus` c) `LTE` (b `plus` d)
> measMon          :  {A : Type} ->
>                     (f : A -> Val) -> (g : A -> Val) ->
>                     ((a : A) -> (f a) `LTE` (g a)) ->
>                     (ma : M A) -> meas (fmap f ma) `LTE` meas (fmap g ma)

> cvalmax         :  (x : State) -> (p : Policy) -> Val
> cvalargmaxSpec  :  (x : State) -> (p : Policy) -> cvalmax x p = cval x (cvalargmax x p) p
> cvalmaxSpec     :  (x : State) -> (y : Ctrl x) -> (p : Policy) -> (cval x y p) `LTE` (cvalmax x p)

** |opt| is optimal

> mutual

>   ||| ... is an optimal policy
>   optLemma1  :  (vs : valSpec) -> (os : optSpec) ->
>                 (x : State) -> (y : Ctrl x) -> (p : Policy) ->
>                 cval x y p `LTE` cval x y opt
>   optLemma1 vs os x y p = s9 where
>     f' : State -> Val
>     f' = \ x' => reward x y x' `plus` val x' p
>     f  : State -> Val
>     f  = \ x' => reward x y x' `plus` val x' opt
>     s1 : (x' : State) -> val x' p `LTE` val x' opt
>     s1 x' = assert_total (optLemma2 vs os) x' p
>     s2 : (x' : State) -> (f' x') `LTE` (f x')
>     s2 x' = monotonePlusLTE (reflexiveLTE (reward x y x')) (s1 x')
>     s3 : meas (fmap f' (nexts x y)) `LTE` meas (fmap f (nexts x y))
>     s3 = measMon f' f s2 (nexts x y)
>     s9 : cval x y p `LTE` cval x y opt
>     s9 = s3

>   ||| ... is an optimal policy
>   optLemma2 : (vs : valSpec) -> (os : optSpec) -> Opt opt
>   optLemma2 vs os x p' = s9 where
>     s1 : val x p' = cval x (p' x) p'
>     s1 = vs x p'
>     s2 : cval x (p' x) p' `LTE` cval x (p' x) opt
>     s2 = assert_total optLemma1 vs os x (p' x) p'
>     s3 : cval x (p' x) opt `LTE` cvalmax x opt
>     s3 = cvalmaxSpec x (p' x) opt
>     s4 : cvalmax x opt = cval x (cvalargmax x opt) opt
>     s4 = cvalargmaxSpec x opt
>     s5 : cval x (cvalargmax x opt) opt = cval x (opt x) opt
>     s5 = replace {P = \ U => cval x U opt = cval x (opt x) opt} (os x) Refl
>     s6 : cval x (opt x) opt = val x opt
>     s6 = sym (vs x opt)
>     s7 : cval x (p' x) p' `LTE` cvalmax x opt
>     s7 = transitiveLTE s2 s3
>     s8 : val x p' `LTE` cvalmax x opt
>     s8 = replace {P = \ W => W `LTE` cvalmax x opt} (sym s1) s7
>     s9 : val x p' `LTE` val x opt
>     s9 = replace {P = \ W => val x p' `LTE` W} (trans (trans s4 s5) s6) s8

* Can one compute optimal policies?

If |State| is finite

> finiteState : Finite State

we can compute the number of values of type |State| and collect them in
a vector

> cardState : Nat
> cardState = card finiteState

> vectState : Vect cardState State
> vectState = toVect finiteState

For a fixed policy |p|, we can represent the value of |p| by a value table

> vt : Policy -> Vect cardState Val

> val x p = index k (vt p) where
>   k : Fin cardState
>   k = lookup x vectState (toVectComplete finiteState x)

In this case, the specification of |val|

< valSpec  =  (x : State) -> (p : Policy) ->
<             val x p
<             =
<             meas (fmap (\ x' => reward x (p x) x' `plus` val x' p) (nexts x (p x)))

defines a linear, implicit problem for the components |vt p|. Let

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Verified.Trifunctor

import Data.Trifunctor

%default total
%access public export

||| Verified Trifunctor
||| A Trifunctor for which identity and composition laws are verified
interface Trifunctor t => VerifiedTrifunctor (t : Type -> Type -> Type -> Type) where
  trifunctorIdentity : {a : Type} -> {b : Type} -> {c : Type} ->
                       (x : t a b c) ->
                       timap Basics.id Basics.id Basics.id x = x
  trifunctorComposition : {a : Type} -> {b : Type} -> {c : Type} ->
                          {a1 : Type} -> {b1 : Type} -> {c1 : Type} ->
                          (x : t a b c) ->
                          (fa1 : a -> a1) -> (fb1 : b -> b1) -> (fc1 : c -> c1) ->
                          (fa2 : a1 -> a2) -> (fb2 : b1 -> b2) -> (fc2 : c1 -> c2) ->
                          (timap (fa2 . fa1) (fb2 . fb1) (fc2 . fc1) x) =
                          (timap fa2 fb2 fc2 . timap fa1 fb1 fc1) x

ext: idr

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module Prelude.Uninhabited

import Builtin
import Prelude.Basics

%default total

||| A canonical proof that some type is empty.
public export
interface Uninhabited t where
  ||| If I have a t, I've had a contradiction.
  ||| @ t the uninhabited type
  uninhabited : t -> Void

||| The eliminator for the `Void` type.
%extern
public export
void : (0 x : Void) -> a

export
Uninhabited Void where
  uninhabited = id

||| Use an absurd assumption to discharge a proof obligation.
||| @ t some empty type
||| @ a the goal type
||| @ h the contradictory hypothesis
public export
absurd : Uninhabited t => (h : t) -> a
absurd h = void (uninhabited h)

public export
Uninhabited (True = False) where
  uninhabited Refl impossible

public export
Uninhabited (False = True) where
  uninhabited Refl impossible


text:
module Control.Monad.List

import Control.HigherOrder

import Control.Monad.Trans

public export
data ListM : (Type -> Type) -> (Type -> Type) where
  Nil : ListM m a
  (::) : a -> m (ListM m a) -> ListM m a

public export
0
ListT : (Type -> Type) -> (Type -> Type)
ListT m a = m (ListM m a)

namespace Semigroup

  export
  [ListT] Monad m => Semigroup (ListT m a) where
    xs <+> ys =
      case !xs of
        [] => ys -- No idea it can't find the instance automatically.
        (x :: xs) => pure $ x :: ((<+>) @{ListT} xs ys)

  export
  [ListM] Monad m => Semigroup (ListM m a) where
    [] <+> ys = ys
    (x :: xs) <+> ys = x :: (<+>) @{ListT} xs (pure ys)

  %hint export
  ListTSemigroup : Monad m => Semigroup (ListT m a)
  ListTSemigroup = Semigroup.ListT

namespace Monoid
  %hint
  export
  ListT : Monad m => Monoid (ListT m a)
  ListT = MkMonoid @{Semigroup.ListT} (pure [])

  %hint
  export
  ListM : Monad m => Monoid (ListM m a)
  ListM = MkMonoid @{Semigroup.ListM} []

namespace Functor
  mutual
    export
    [ListM] Functor m => Functor (ListM m) where
      map f [] = []
      map f (x :: xs) = f x :: map @{ListT} f xs

    export
    [ListT] Functor m => Functor (ListT m) where
      map f x = map (map @{ListM} f) x

namespace Applicative
  %hint export
  ListT : Monad m => Applicative (ListT m)
  ListT = MkApplicative @{Functor.ListT}
    (pure . (:: pure Nil))
    $
    \fs, ys =>
      case !fs of
        [] => pure []
        f :: fs => (<+>) @{Semigroup.ListT}
          (map @{Functor.ListT} f ys)
          ((<*>) @{Applicative.ListT} fs ys)

namespace Monad

  bind : Monad m => ListT m a -> (a -> ListT m b) -> ListT m b
  bind xs f = do
    case !xs of
      [] => pure []
      x :: xs => (<+>) @{ListT} (f x) (bind xs f)

  %hint export
  ListT : Monad m => Monad (ListT m)
  ListT = MkMonad @{Applicative.ListT}
    (bind {m})
    (flip (bind {m}) id)

namespace Alternative
  %hint public export
  ListT : Monad m => Alternative (ListT m)
  ListT = MkAlternative @{Applicative.ListT} (pure []) (\x, y => (<+>) @{ListT} x y)

export
MonadTrans ListT where
  lift = (>>= pure @{ListT})

export
runListT' : Monad m => ListT m a -> m (Maybe a)
runListT' x = do
  case !x of
    [] => pure Nothing
    x :: xs => pure (Just x)

export
runListT : Monad m => ListT m a -> m (List a)
runListT x = do
  case !x of
    [] => pure []
    x :: xs => map (x ::) (runListT xs)

export
liftList : Applicative m => List a -> ListT m a
liftList [] = pure []
liftList (x :: xs) = pure (x :: liftList xs)


text:
> module Identity.Operations

> import Control.Monad.Identity

> import Sigma.Sigma

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

> |||
> unwrap : Identity a -> a
> unwrap {a} (Id x) = x

* |Identity| is a functor:

> ||| fmap
> fmap : {A, B : Type} -> (A -> B) -> Identity A -> Identity B
> fmap = map {f = Identity}

* |Identity| is a monad:

> ||| ret
> ret : {A : Type} -> A -> Identity A
> ret = pure

> ||| bind
> bind : {A, B : Type} -> Identity A -> (A -> Identity B) -> Identity B
> bind = (>>=)

* |Identity| is a container monad:

> ||| Membership
> Elem : {A : Type} -> A -> Identity A -> Type
> Elem a1 (Id a2) = a1 = a2

> ||| Non emptiness
> NonEmpty : {A : Type} -> Identity A -> Type
> NonEmpty _ = Unit

> |||
> All : {A : Type} -> (P : A -> Type) -> Identity A -> Type
> All P = P . unwrap

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

> |||
> unwrapElemLemma : (ia : Identity a) -> Elem (unwrap ia) ia
> unwrapElemLemma (Id a) = Refl


text:
||| Spec: http://webassembly.github.io/spec/core/syntax/types.html#function-types
module WebAssembly.Structure.Types.FunctionTypes

import WebAssembly.Structure.Types.ValueTypes
import WebAssembly.Structure.Types.ResultTypes

import Decidable.Equality

-- Definition

infixr 6 ->>

public export
data FuncType : Type where
  (->>) : ResultType -> ResultType -> FuncType

-- Equality

total public export
lemma_functype__inputs_injective : ((in1 = in2) -> Void) -> ((in1 ->> out1) = (in2 ->> out2)) -> Void
lemma_functype__inputs_injective in1_not_in2 Refl = in1_not_in2 Refl

total public export
lemma_functype__outputs_injective : ((out1 = out2) -> Void) -> ((in1 ->> out1) = (in2 ->> out2)) -> Void
lemma_functype__outputs_injective out1_not_out2 Refl = out1_not_out2 Refl

-- Decidable Equality

public export
implementation DecEq FuncType where
  decEq (in1 ->> out1) (in2 ->> out2) = case (decEq in1 in2) of
    No in1_not_in2 => No $ lemma_functype__inputs_injective in1_not_in2
    Yes Refl  => case (decEq out1 out2) of
      No out1_not_out2 => No $ lemma_functype__outputs_injective out1_not_out2
      Yes Refl         => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Deriving

import Deriving.Show
import Deriving.Eq

public export
data Deriver = MkDeriver (TTName -> Datatype -> Elab ())

export
derive : List Deriver -> TTName -> Elab ()
derive derivers name = do
  qname <- quorifyName name
  dt <- lookupDatatypeExact qname
  for_ {b=()} derivers $ \(MkDeriver d) => d qname dt
where
  quorifyName : TTName -> Elab TTName
  quorifyName (UN un) = do
    ns <- currentNamespace
    pure $ NS (UN un) ns
  quorifyName n = pure n

export
Show : Deriver
Show = MkDeriver deriveShow

export
Eq : Deriver
Eq = MkDeriver deriveEq

max_stars_repo_name: KeenS/idris-deriving

max_issues_repo_name: KeenS/idris-deriving

max_forks_repo_name: KeenS/idris-deriving


text:
module Js.RethinkDB
{-
import Effects
import Js.ASync
import public Js.Json
import public Js.SimpleData
import Js.Node

require : String -> JS_IO Ptr
require s = jscall "require(%0)" (String -> JS_IO Ptr) s

export
data Connection = MkConnection Ptr Ptr

export
connect' : String -> Int -> ASync Connection
connect' host port =
  do
    r <- liftJS_IO $ require "rethinkdb"
    c <- handleErr $ MkASync $ \proc =>
      jscall
        "%0.connect({'host': %1,'port': %2}, function(e,c){%3([e,c])}  ) "
        (Ptr -> String -> Int -> JsFn (Ptr -> JS_IO ()) -> JS_IO () )
        r
        host
        port
        (MkJsFn proc)
    pure $ MkConnection r c

export
connect : String -> ASync Connection
connect host = connect' host 28015

export
data Table : SDataObj -> Type where
  MkTable : String -> String -> (a : SDataObj) -> Table a

export
table : String -> String -> Table a
table {a} x y = MkTable x y a

export
data Query : SDataTy -> Type where
  Values : Table a -> Query (SObj a)

mkQuery : Ptr -> Query a -> JS_IO Ptr
mkQuery p (Values (MkTable database name ptype)) =
  jscall "%0.db(database).table()" (Ptr -> String -> String -> JS_IO Ptr) p database name

procRethinkRes : (a:SDataTy) -> ASync Ptr -> ASync (Either String (ISDataTy a))
procRethinkRes a y =
  decodeRes $ err2Either y
  where
    decodeRes : ASync (Either String Ptr) -> ASync (Either String (ISDataTy a))
    decodeRes x =
      case !x of
          Left e => pure $ Left e
          Right y => liftJS_IO $ decodeJS a y

toErrAsync : ASync (Either String x) -> ASync x
toErrAsync x =
  x >>= xtoErr
  where
    xtoErr (Left z) = debugError z
    xtoErr (Right z) = pure z

--export
runQuery' : Connection -> Int -> Query a -> ASync (Either String (ISDataTy a))
runQuery' {a} (MkConnection r c) limit q =
  do
    qq <- liftJS_IO $ mkQuery r q
    procRethinkRes a $ MkASync $ \proc =>
      jscall "%0.limit(%3).run(%1,function(e,c){%2([e,c])})"
        (Ptr -> Ptr -> JsFn (Ptr -> JS_IO ()) -> Int -> JS_IO () )
        qq
        c
        (MkJsFn proc)
        limit

--export
runQuery : Connection -> Int -> Query a -> ASync (ISDataTy a)
runQuery conn lim q = toErrAsync $ runQuery' conn lim q

--export
--getFeed' : Connection -> Query a -> ASync (Either String Cursor (ISDataTy a))

--export
createTableRaw' : String -> Connection -> String -> ASync (Either String ())
createTableRaw' database (MkConnection r c) tableName =
    (map $ map $ \_=> ()) $ err2Either $ MkASync $ \proc =>
      jscall
        "%0.db(%1).tableCreate(%2).run(%3, function(e,c){%4([e,c])}  ) "
        (Ptr -> String -> String -> Ptr -> JsFn (Ptr -> JS_IO ()) -> JS_IO () )
        r
        database
        tableName
        c
        (MkJsFn proc)

createTableRaw : String -> Connection -> String -> ASync ()
createTableRaw db c tbl = toErrAsync $ createTableRaw' db c tbl

--export
insert : Connection -> Table a -> List (ISDataObj a) -> ASync (Either String (HVect []))
insert (MkConnection r c) (MkTable database name ptype) vals =
  do
    v <- liftJS_IO $ encodeJS (SList $ SObj ptype) vals
    procRethinkRes (SObj []) $ MkASync $ \proc =>
      jscall
        "%2.db(%0).table(%1).insert(%3).run(%4, function(e,c){%5([e,c])} )"
        (String -> String -> Ptr -> Ptr -> Ptr -> JsFn (Ptr -> JS_IO ()) -> JS_IO ())
        database
        name
        r
        v
        c
        (MkJsFn proc)

--export
--insert1 : Table a -> ISDataObj a -> ASync (Either)
--insert1 x y = Insert x [y]

export
values : Table a -> Query (SObj a)
values = Values

export
data RethinkDB : Effect where
  CreatTable : String -> String -> sig RethinkDB () Connection

public export
RETHINKDB : (ty : Type) -> EFFECT
RETHINKDB t = MkEff t RethinkDB

export
implementation Handler RethinkDB ASync where
  handle c (CreatTable db tbl) k = do createTableRaw db c tbl ; k () c

export
createTable : String -> String -> Eff () [RETHINKDB Connection]
createTable db tbl = call $ CreatTable db tbl
-}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Text.WebIDL.Encoder

import Data.SOP
import Data.List
import Data.String
import Text.WebIDL.Types

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

public export
0 Encoder : Type -> Type
Encoder a = a -> String

runEnc : forall a . Encoder a -> a -> String
runEnc = apply

export
ident : Encoder Identifier
ident = value

inParens : Encoder a -> Encoder a
inParens f a = "(" ++ f a ++ ")"

inBrackets : Encoder a -> Encoder a
inBrackets f a = "[" ++ f a ++ "]"

inBraces : Encoder a -> Encoder a
inBraces f a = "{" ++ f a ++ "}"

inAngles : Encoder a -> Encoder a
inAngles f a = "<" ++ f a ++ ">"

emaybe : Encoder a -> Encoder (Maybe a)
emaybe f = maybe "" f

sepList' : (sep : String) -> List String -> String
sepList' sep = fastConcat . intersperse sep

sepList : (sep : String) -> Encoder a -> Encoder (List a)
sepList sep f = sepList' sep . map f

emptyIfNull : Foldable f =>  Encoder (f a) -> Encoder (f a)
emptyIfNull f as = if null as then "" else f as

spaced : List String -> String
spaced = fastConcat . intersperse " "

--------------------------------------------------------------------------------
--          Literals
--------------------------------------------------------------------------------

toHexDigit : Integer -> Char
toHexDigit 0 = '0'
toHexDigit 1 = '1'
toHexDigit 2 = '2'
toHexDigit 3 = '3'
toHexDigit 4 = '4'
toHexDigit 5 = '5'
toHexDigit 6 = '6'
toHexDigit 7 = '7'
toHexDigit 8 = '8'
toHexDigit 9 = '9'
toHexDigit 10 = 'A'
toHexDigit 11 = 'B'
toHexDigit 12 = 'C'
toHexDigit 13 = 'D'
toHexDigit 14 = 'E'
toHexDigit 15 = 'F'
toHexDigit _ = '_'

export
toDigits : (pre : String) -> (base : Integer) -> Nat -> String
toDigits pre base n = pre ++ fastPack(run (natToInteger n) [])
  where run : Integer -> List Char -> List Char
        run n cs = let n'  = n `div` base
                       cs' = (toHexDigit $ n `mod` base) :: cs
                    in if n' == 0 then cs' else run n' cs'

export
intLit : Encoder IntLit
intLit (Hex k) = toDigits "0x" 16 k
intLit (Oct k) = toDigits "0" 8 k
intLit (I x)   = show x

sig : Encoder Signum
sig Plus  = ""
sig Minus = "-"

export
floatLit : Encoder FloatLit
floatLit Infinity          = "Infinity"
floatLit NegativeInfinity  = "-Infinity"
floatLit NaN               = "NaN"
floatLit (NoExp s bd ad)   = fastConcat [sig s,show bd,".",show ad]
floatLit (Exp s bd ad exp) =
  fastConcat [sig s,show bd,maybe "" (("." ++) . show) ad,"e",show exp]

export
stringLit : Encoder StringLit
stringLit = value

export
keyword : Encoder Keyword
keyword = value

export
symbol : Encoder Symbol
symbol Ellipsis = "..."
symbol (Symb c) = singleton c

--------------------------------------------------------------------------------
--          Attribute
--------------------------------------------------------------------------------

export
other : Encoder Other
other = collapseNS
      . hliftA2 runEnc [intLit,floatLit,stringLit,ident,keyword,symbol]

export
eaInner : Encoder EAInner
eaInner (EAIParens ip eai) = inParens eaInner ip ++ " " ++ eaInner eai
eaInner (EAIOther o eai)   = other o ++ " " ++ eaInner eai
eaInner EAIEmpty           = ""

export
extAttribute : Encoder ExtAttribute
extAttribute (EAParens i r) = inParens eaInner i ++ emaybe extAttribute r
extAttribute (EAOther o r)  = other o ++ " " ++ emaybe extAttribute r

export
attributes : Encoder ExtAttributeList
attributes = emptyIfNull . inBrackets $ sepList "," extAttribute

export
attributed : Encoder a -> Encoder (Attributed a)
attributed f (as,a) = attributes as ++ " " ++ f a

--------------------------------------------------------------------------------
--          Type
--------------------------------------------------------------------------------

export
bufferRelated : Encoder BufferRelatedType
bufferRelated = show

export
stringType : Encoder StringType
stringType = show

export
intType : Encoder IntType
intType Short    = "short"
intType Long     = "long"
intType LongLong = "long long"

export
floatType : Encoder FloatType
floatType Float = "float"
floatType Dbl   = "double"

export
primitive : Encoder PrimitiveType
primitive (Unsigned x)     = "unsigned " ++ intType x
primitive (Signed x)       = intType x
primitive (Unrestricted x) = "unrestricted " ++ floatType x
primitive (Restricted x)   = floatType x
primitive Undefined        = "undefined"
primitive Boolean          = "boolean"
primitive Byte             = "byte"
primitive Octet            = "octet"
primitive BigInt           = "bigint"

export
constType : Encoder ConstType
constType (CP x) = primitive x
constType (CI x) = ident x

export
nullable : Encoder a -> Encoder (Nullable a)
nullable f (MaybeNull x) = f x ++ "?"
nullable f (NotNull x)   = f x

mutual
  export
  idlType : Encoder IdlType
  idlType Any         = "any"
  idlType (D x)       = nullable distinguishable x
  idlType (U x)       = nullable union x
  idlType (Promise x) = "Promise" ++ inAngles idlType x

  export
  unionMember : Encoder UnionMemberType
  unionMember (MkUnionMember a x) = attributed distinguishable (a,x)

  export
  union : Encoder UnionType
  union (UT fst snd rest) =
    inParens (sepList " or " unionMember) (fst :: snd :: rest)

  export
  distinguishable : Encoder Distinguishable
  distinguishable (P x) = primitive x
  distinguishable (S x) = stringType x
  distinguishable (I x) = ident x
  distinguishable (B x) = bufferRelated x
  distinguishable (Sequence a x) =
    "sequence" ++ inAngles (attributed idlType) (a,x)
  distinguishable (FrozenArray a x) =
    "FrozenArray" ++ inAngles (attributed idlType) (a,x)
  distinguishable (ObservableArray a x) =
    "ObservableArray" ++ inAngles (attributed idlType) (a,x)
  distinguishable (Record x a y) =
    "record<" ++ stringType x ++ "," ++ attributed idlType (a,y) ++ ">"
  distinguishable Object = "object"
  distinguishable Symbol = "symbol"

optionalType : Encoder OptionalType
optionalType = maybe "" (\p => "," ++ attributed idlType p)

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

export
constValue : Encoder ConstValue
constValue (B True)  = "true"
constValue (B False) = "false"
constValue (F x)     = floatLit x
constValue (I x)     = intLit x

export
defaultV : Encoder Default
defaultV None      = ""
defaultV EmptyList = "= []"
defaultV EmptySet  = "= {}"
defaultV Null      = "= null"
defaultV (S x)     = "= " ++ stringLit x
defaultV (C x)     = "= " ++ constValue x

arg : Encoder Arg
arg (MkArg as t n) = spaced [attributes as, idlType t, n.value]

vararg : Encoder Arg
vararg (MkArg as t n) = spaced [attributes as, idlType t ++ "...", n.value]

optArg : Encoder OptArg
optArg (MkOptArg as tas t n d) = spaced [ attributes as
                                        , "optional"
                                        , attributed idlType (tas,t)
                                        , n.value
                                        , defaultV d
                                        ]

export
argumentList : Encoder ArgumentList
argumentList (VarArg args va) =
  sepList' "," (map arg args ++ [vararg va])

argumentList (NoVarArg args optArgs) =
  sepList' "," (map arg args ++ map optArg optArgs)

optArgList : Encoder ArgumentList
optArgList (NoVarArg Nil Nil) = ""
optArgList x                  = inParens argumentList x

--------------------------------------------------------------------------------
--          Members
--------------------------------------------------------------------------------

member : (key : String) -> List String -> String
member "" vs = spaced vs ++ ";"
member k vs  = spaced (k :: vs) ++ ";"

export
const : Encoder Const
const (MkConst t n v) = member "const" [constType t,n.value,"=",constValue v]

export
special : Encoder Special
special Getter  = "getter"
special Setter  = "setter"
special Deleter = "deleter"

export
op : Encoder a -> Encoder (Op a)
op f (MkOp s t n a) =
  member "" [f s, idlType t, maybe "" value n, inParens argumentList a]

export
regularOperation : Encoder RegularOperation
regularOperation = op (const "")

export
specialOperation : Encoder SpecialOperation
specialOperation = op special

export
operation : Encoder Operation
operation = op (maybe "" special)

callbackInterfaceMember : Encoder CallbackInterfaceMember
callbackInterfaceMember = collapseNS . hliftA2 runEnc [const,regularOperation]

callbackInterfaceMembers : Encoder CallbackInterfaceMembers
callbackInterfaceMembers = sepList " " $ attributed callbackInterfaceMember

inheritance : Encoder Inheritance
inheritance = maybe "" $ \i => " : " ++ i.value

dictMemberRest : Encoder DictionaryMemberRest
dictMemberRest (Required as t n) =
  member "required" [attributes as,idlType t,n.value]
dictMemberRest (Optional t n d) =
  member "" [idlType t, n.value, defaultV d]

dictMembers : Encoder DictionaryMembers
dictMembers = sepList " " $ attributed dictMemberRest

readonly : Encoder a -> Encoder (Readonly a)
readonly f = ("readonly " ++) . f . value

inherit : Encoder a -> Encoder (Inherit a)
inherit f = ("inherit " ++) . f . value

attribute : Encoder Attribute
attribute (MkAttribute as t n) =
  member "attribute" [attributes as, idlType t, n.value]

stringifier : Encoder Stringifier
stringifier = ("stringifier " ++)
            . collapseNS
            . hliftA2 runEnc [attribute,readonly attribute,regularOperation,const ";"]

static : Encoder StaticMember
static = ("static " ++)
       . collapseNS
       . hliftA2 runEnc [attribute,readonly attribute,regularOperation]

maplike : Encoder Maplike
maplike (MkMaplike l r) =
  member "maplike" ["<",attributed idlType l,",",attributed idlType r,">"]

setlike : Encoder Setlike
setlike (MkSetlike p) = member "setlike" ["<",attributed idlType p,">"]

namespaceMember : Encoder NamespaceMember
namespaceMember = collapseNS
                . hliftA2 runEnc [regularOperation,readonly attribute]

namespaceMembers : Encoder NamespaceMembers
namespaceMembers = sepList " " $ attributed namespaceMember

constructor_ : Encoder Constructor
constructor_ (MkConstructor args) =
  member "constructor" [inParens argumentList args]

partialInterfaceMember : Encoder PartialInterfaceMember
partialInterfaceMember (IConst x)       = const x
partialInterfaceMember (IOp x)          = operation x
partialInterfaceMember (IAttr x)        = attribute x
partialInterfaceMember (IAttrRO x)      = readonly attribute x
partialInterfaceMember (IAttrInh x)     = inherit attribute x
partialInterfaceMember (IMap x)         = maplike x
partialInterfaceMember (IMapRO x)       = readonly maplike x
partialInterfaceMember (ISet x)         = setlike x
partialInterfaceMember (ISetRO x)       = readonly setlike x
partialInterfaceMember (IStr x)         = stringifier x
partialInterfaceMember (IStatic x)      = static x
partialInterfaceMember (IIterable p o)  =
  member "iterable" ["<",attributed idlType p,optionalType o,">"]
partialInterfaceMember (IAsync p o a)   =
  member "async iterable"
    ["<",attributed idlType p,optionalType o,">",optArgList a]

mixinMember : Encoder MixinMember
mixinMember (MConst x)       = const x
mixinMember (MOp x)          = regularOperation x
mixinMember (MAttr x)        = attribute x
mixinMember (MAttrRO x)      = readonly attribute x
mixinMember (MStr x)         = stringifier x

partialInterfaceMembers : Encoder PartialInterfaceMembers
partialInterfaceMembers = sepList " " $ attributed partialInterfaceMember

mixinMembers : Encoder MixinMembers
mixinMembers = sepList " " $ attributed mixinMember

export
interfaceMember : Encoder InterfaceMember
interfaceMember = collapseNS
                . hliftA2 runEnc [constructor_,partialInterfaceMember]

interfaceMembers : Encoder InterfaceMembers
interfaceMembers = sepList " " $ attributed interfaceMember

--------------------------------------------------------------------------------
--          Definition
--------------------------------------------------------------------------------

def : ExtAttributeList -> (key : String) -> List String -> String
def as ""  ss = attributes as ++ spaced ss ++ ";"
def as key ss = attributes as ++ spaced (key :: ss) ++ ";"

callback : Encoder Callback
callback (MkCallback as n t args) =
  def as "callback" [n.value, "=", idlType t, inParens argumentList args]

callbackInterface : Encoder CallbackInterface
callbackInterface (MkCallbackInterface as n ms) =
  def as "callback interface"
  [n.value, inBraces callbackInterfaceMembers ms]

dictionary : Encoder Dictionary
dictionary (MkDictionary as n i ms) =
  def as "dictionary"
  [n.value, inheritance i, inBraces dictMembers ms]

enum : Encoder Enum
enum (MkEnum as n vs) =
  def as "enum" [n.value, inBraces (sepList "," stringLit) (forget vs)]

iface : Encoder Interface
iface (MkInterface as n i ms) =
  def as "interface" [n.value, inheritance i, inBraces interfaceMembers ms]

includes : Encoder Includes
includes (MkIncludes as a b) = def as "" [a.value,"includes",b.value]

mixin : Encoder Mixin
mixin (MkMixin as n ms) =
  def as "interface mixin" [n.value, inBraces mixinMembers ms]

nspace : Encoder Namespace
nspace (MkNamespace as n ms) =
  def as "namespace" [n.value, inBraces namespaceMembers ms]

pdictionary : Encoder PDictionary
pdictionary (MkPDictionary as n ms) =
  def as "partial dictionary" [n.value, inBraces dictMembers ms]

pinterface : Encoder PInterface
pinterface (MkPInterface as n ms) =
  def as "partial interface" [n.value, inBraces partialInterfaceMembers ms]

pmixin : Encoder PMixin
pmixin (MkPMixin as n ms) =
  def as "partial interface mixin" [n.value, inBraces mixinMembers ms]

pnamespace : Encoder PNamespace
pnamespace (MkPNamespace as n ms) =
  def as "partial namespace" [n.value, inBraces namespaceMembers ms]

typedef : Encoder Typedef
typedef (MkTypedef as tas t n) =
  def as "typedef" [attributes tas, idlType t, n.value]

export
definition : Encoder Definition
definition = collapseNS
           . hliftA2 runEnc [ callback
                            , callbackInterface
                            , dictionary
                            , enum
                            , includes
                            , iface
                            , mixin
                            , nspace
                            , typedef
                            ]

export
part : Encoder Part
part = collapseNS . hliftA2 runEnc [pdictionary,pinterface,pmixin,pnamespace]


text:
||| Implementation of ordering relations for `Nat`ural numbers
module Data.Nat.Order

import Control.Relation
import Data.Nat
import Data.Fun
import Data.Rel
import Decidable.Decidable
import Decidable.Equality

%default total

public export
zeroNeverGreater : Not (LTE (S n) Z)
zeroNeverGreater LTEZero     impossible
zeroNeverGreater (LTESucc _) impossible

public export
zeroAlwaysSmaller : {n : Nat} -> LTE Z n
zeroAlwaysSmaller = LTEZero

public export
ltesuccinjective : {0 n, m : Nat} -> Not (LTE n m) -> Not (LTE (S n) (S m))
ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
ltesuccinjective disprf LTEZero         impossible

public export
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decideLTE    Z      y  = Yes LTEZero
decideLTE (S x)     Z  = No  zeroNeverGreater
decideLTE (S x)   (S y) with (decEq (S x) (S y))
  decideLTE (S x)   (S y) | Yes eq      = rewrite eq in Yes (reflexive {rel = LTE})
  decideLTE (S x)   (S y) | No _ with (decideLTE x y)
    decideLTE (S x)   (S y) | No _   | Yes nLTEm = Yes (LTESucc nLTEm)
    decideLTE (S x)   (S y) | No _   | No  nGTm  = No (ltesuccinjective nGTm)

public export
Decidable 2 [Nat,Nat] LTE where
  decide = decideLTE

public export
Decidable 2 [Nat,Nat] LT where
  decide m = decideLTE (S m)

public export
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

public export
shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
shift m n mLTEn = LTESucc mLTEn


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

import Data.Vect

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

removeElemPrf :
  (value : a) ->
  (xs : Vect (S n) a) ->
  (prf : Elem value xs) ->
  Vect n a
removeElemPrf value (value :: ys) Here = ys
removeElemPrf {n = Z} value (y :: []) (There later) = absurd later
removeElemPrf {n = (S k)} value (y :: ys) (There later) = y :: removeElemPrf value ys later

removeElem :
  (value : a) ->
  (xs : Vect (S n) a) ->
  {auto prf : Elem value xs} ->
  Vect n a
removeElem x xs {prf} = removeElemPrf x xs prf

notInTail : (notHere : (value = x) -> Void) -> (notThere : Elem value xs -> Void) -> Elem value (x :: xs) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

isYes : Dec a -> Bool
isYes (Yes prf) = True
isYes (No contra) = False

isElem' : DecEq ty => (value : ty) -> (xs : Vect n ty) -> Dec (Elem value xs)
isElem' value [] = No notInNil
isElem' value (x :: xs) = case decEq value x of
  Yes Refl   => Yes Here
  No notHere => case isElem' value xs of
    Yes prf => Yes (There prf)
    No notThere => No (notInTail notHere notThere)

data LElem : a -> List a -> Type where
  LHere : LElem a (a :: as)
  LThere : LElem a as -> LElem a (b :: as)

data Last : List a -> a -> Type where
  LOne : Last [value] value
  LCons : (prf : Last xs value) -> Last (x :: xs) value

noLast1 : (notLast : (x = value) -> Void) -> Last [x] value -> Void
noLast1 notLast LOne = notLast Refl
noLast1 _ (LCons LOne) impossible
noLast1 _ (LCons (LCons _)) impossible

noLast2 : (noLast : Last (y :: ys) value -> Void) -> Last (x :: (y :: ys)) value -> Void
noLast2 noLast (LCons prf) = noLast prf

noLast0 : Last [] value -> Void
noLast0 LOne impossible
noLast0 (LCons _) impossible

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No noLast0
isLast (x :: []) value = case decEq x value of
  Yes Refl => Yes LOne
  No notLast => No (noLast1 notLast)
isLast (x :: y :: ys) value = case isLast (y :: ys) value of
  Yes prf => Yes (LCons prf)
  No noLast => No (noLast2 noLast)

main : IO ()
main = do
  printLn $ removeElem 3 [1,2,3]
  printLn $ isYes $ isElem' 3 [1,2,3]
  printLn $ isYes $ isElem' 10 [1,2,3,4,5,6,7,8,9]
--  printLn $ isYes $ isLast 10 [1,2,3,4,5,6,7,8,9] -- Idris bug: Infinite loop

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp =
  let val = cast inp in
      if val < 0
         then Nothing
         else let newVal = tot + val in
                  Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

main : IO ()
main = replWith 0 "Value: " sumInputs


text:
module WTypes

data W : (t : Type) -> (p : t -> Type) -> Type where
  Sup : (x : t) -> (p x -> W t p) -> W t p

ind : {t : Type} -> {p : t -> Type} -> (pred : W t p -> Type) ->
      ((v : t) -> (f : p v -> W t p) -> ((t' : p v) -> pred (f t')) -> pred (Sup v f)) ->
      (w : W t p) -> pred w
ind _ p (Sup x f) = p x f (\t => ind _ p (f t))

efq : {a : Type} -> Void -> a

-- Nat encoding
N : Type
N = W Bool (\b => if b then () else Void)

zero : N
zero = Sup False efq

succ : N -> N
succ n = Sup True (const n)

plus : N -> N -> N
plus (Sup False f) b = b
plus (Sup True f) b = Sup True (\() => plus (f ()) b)

-- Tree encoding
Tree : Type
Tree = W Bool (\b => if b then Bool else Void)

leaf : Tree
leaf = Sup False efq

branch : Tree -> Tree -> Tree
branch l r = Sup True (\b => if b then l else r)

size : Tree -> N
size (Sup False f) = zero
size (Sup True f) = plus (size (f True)) (size (f False))

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
f : (Int -> Bool) -> Int
f p = case (p 0, p 1) of
        (False, False) => 0
        (False, True)  => 1
        (True , False) => 2
        (True , True)  => 4

il : Int
il = f $ \x => x > 0

lc : Int
lc = f $ \case 0 => True ; _ => False

ilc : Int
ilc = f (\case 0 => True; _ => False)


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

%name InfList xs, ys, zs

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

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

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


text:
module JS.Boolean

import JS.Marshall
import JS.Inheritance
import JS.Util

export
data Boolean : Type where [external]

export
%foreign "javascript:lambda:()=>true"
true : Boolean

export
%foreign "javascript:lambda:()=>false"
false : Boolean

export
ToFFI Bool Boolean where
  toFFI True  = true
  toFFI False = false

export
FromFFI Bool Boolean where
  fromFFI v = if eqv v true then Just True
              else if eqv v false then Just False
              else Nothing

export
SafeCast Boolean where
  safeCast = unsafeCastOnTypeof "boolean"


text:
module Data.Music.Test

import Data.Music

import Specdris.Spec

%access export

Show Ordering where
  show LT = "lower"
  show EQ = "equal"
  show GT = "higher"

pitchOrdSpec : SpecTree
pitchOrdSpec =
  describe "Pitches are ordered correctly" $ do
    it "Chromatic: D0 < C1" $ do
      let compare = compare@{PitchOrd}
      compare (D, 0) (C, 1) === LT
    it "Diatonic:  D0 < C1" $ do
      let compare = compare@{DiatonicPitchOrd}
      compare (D, 0) (C, 1) === LT

runTests : IO ()
runTests = spec pitchOrdSpec

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
module TypedContainers.RBTree.Insert

import Data.Nat
import Data.DPair
import Data.List
import TypedContainers.In
import TypedContainers.LawfulOrd
import TypedContainers.RBTree.Base
import TypedContainers.RBTree.Balance
import TypedContainers.Util.Filter

%default total

GoodBadTree :
  {height : Nat} ->
  {kt : Type} ->
  {kord : LawfulOrd kt} ->
  {keys : List kt} ->
  {vt : kt -> Type} ->
  Color ->
  Type
GoodBadTree c = case c of
  Black => Exists \color' => GoodTree {color = color', height, kt, kord, vt, keys}
  Red => BadTree {height, kt, kord, vt, keys}

mutual
  insertLeft :
    (kord : LawfulOrd kt) =>
    {0 colorLeft : Color} ->
    (k : kt) ->
    vt k ->
    (k' : kt) ->
    {0 kp : In (k' ==) keys} ->
    vt k' ->
    {0 ltEq : compare k k' = LT} ->
    {0 keyslEq : keysl = filter (k' >) keys} ->
    GoodTree {height, color = colorLeft, kt, kord, keys = keysl, vt} ->
    {0 keysrEq : keysr = filter (k' <) keys} ->
    GoodTree {height, color = colorRight, kt, kord, keys = keysr, vt} ->
    (
      GoodBadTree colorLeft {height, kt, kord, vt, keys = filter (k' >) (k :: keys)},
      GoodTree {color = colorRight, height, kt, kord, vt, keys = filter (k' <) (k :: keys)}
    )
  insertLeft k v k' v' l r =
    let l' = insertG' k v l in
    let 0 p1 = reversion1 k k' ltEq in
    let 0 p2 = cong (\case { GT => True; _ => False }) p1 in
    let 0 p3 : (k :: filter (k' >) keys = filter (k' >) (k :: keys)) = rewrite p2 in Refl in
    let l'' : GoodBadTree colorLeft {height, kt, kord, vt, keys = filter (k' >) (k :: keys)} =
      rewrite sym p3 in rewrite sym keyslEq in l'
    in
    let 0 p4 : (k' < k = False) = cong (\case { LT => True; _ => False }) p1 in
    let 0 p5 : (filter (k' <) keys = filter (k' <) (k :: keys)) = rewrite p4 in Refl in
    let r' : GoodTree {color = colorRight, height, kt, kord, vt, keys = filter (k' <) (k :: keys)} =
      rewrite sym p5 in rewrite sym keysrEq in r
    in
    (l'', r')

  insertRight :
    (kord : LawfulOrd kt) =>
    {0 colorLeft : Color} ->
    (k : kt) ->
    vt k ->
    (k' : kt) ->
    {0 kp : In (k' ==) keys} ->
    vt k' ->
    {0 gtEq : compare k k' = GT} ->
    {0 keyslEq : keysl = filter (k' >) keys} ->
    GoodTree {height, color = colorLeft, kt, kord, keys = keysl, vt} ->
    {0 keysrEq : keysr = filter (k' <) keys} ->
    GoodTree {height, color = colorRight, kt, kord, keys = keysr, vt} ->
    (
      GoodTree {color = colorLeft, height, kt, kord, vt, keys = filter (k' >) (k :: keys)},
      GoodBadTree colorRight {height, kt, kord, vt, keys = filter (k' <) (k :: keys)}
    )
  insertRight k v k' v' l r =
    let r' = insertG' k v r in
    let 0 p1 = reversion2 k k' gtEq in
    let 0 p2 = cong (\case { LT => True; _ => False }) p1 in
    let 0 p3 : (k :: filter (k' <) keys = filter (k' <) (k :: keys)) = rewrite p2 in Refl in
    let r'' : GoodBadTree colorRight {height, kt, kord, vt, keys = filter (k' <) (k :: keys)} =
      rewrite sym p3 in rewrite sym keysrEq in r'
    in
    let 0 p4 : (k' > k = False) = cong (\case { GT => True; _ => False }) p1 in
    let 0 p5 : (filter (k' >) keys = filter (k' >) (k :: keys)) = rewrite p4 in Refl in
    let l' : GoodTree {color = colorLeft, height, kt, kord, vt, keys = filter (k' >) (k :: keys)} =
      rewrite sym p5 in rewrite sym keyslEq in l
    in
    (l', r'')

  insertG' :
    {0 color : Color} ->
    (kord : LawfulOrd kt) =>
    (k : kt) ->
    vt k ->
    GoodTree {kt, height, color, kord, vt, keys} ->
    GoodBadTree color {height, kt, kord, vt, keys = k :: keys}
  insertG' k v (Empty Refl) =
    let 0 kp : (In (k ==) (k :: [])) = MkIn k (cong (\case {EQ => True; _ => False}) $ reflexivity k) [] in
    Evidence Red (
      RedNode k v
        (rewrite reflexivity k in Empty Refl)
        (rewrite reflexivity k in Empty Refl)
        {keys = k :: [], kp}
    )
  insertG' k v (RedNode k' v' l r {kp}) =
    case the (Subset Ordering (compare k k' ===)) $ Element (compare k k') Refl of
      Element LT ltEq =>
        let (Evidence color' l', r') = insertLeft k v k' v' l r {ltEq, kp, keyslEq = Refl, keysrEq = Refl} in
        BadRedNode k' v' l' r' {kp = MkInCons k keys kp}
      Element EQ p0 =>
        let
          0 p5 : (x : kt) -> (k > x = k' > x)
          p5 x = cong (\case { GT => True; _ => False }) $ equality1 k k' x p0

          0 p6 : (x : kt) -> (k < x = k' < x)
          p6 x = cong (\case { LT => True; _ => False }) $ equality1 k k' x p0
        in
        let 0 p1 : (filter (k >) keys = (filter (k' >) keys)) = filterExtensionality p5 in
        let 0 p2 : (filter (k >) (k :: keys) = filter (k >) keys)
            = rewrite reflexivity k in Refl in
        let 0 p3 : (filter (k <) keys = (filter (k' <) keys)) = filterExtensionality p6 in
        let 0 p4 : (filter (k <) (k :: keys) = filter (k <) keys)
            = rewrite reflexivity k in Refl in
        let l' : GoodTree {kt, kord, vt, keys = filter (k >) (k :: keys)} =
            rewrite trans p2 p1 in l
        in
        let r' : GoodTree {kt, kord, vt, keys = filter (k <) (k :: keys)} =
            rewrite trans p4 p3 in r
        in
        BadRedNode k v l' r' {kp = MkIn k (cong (\case { EQ => True; _ => False }) (reflexivity k)) keys}
      Element GT gtEq =>
        let (l', Evidence color' r') = insertRight k v k' v' l r {gtEq, kp, keyslEq = Refl, keysrEq = Refl} in
        BadRedNode k' v' l' r' {kp = MkInCons k keys kp}
  insertG' k v (BlackNode k' v' l r {kp, height = height', colorLeft, colorRight}) = case the (Subset Ordering (compare k k' ===)) $ Element (compare k k') Refl of
    Element LT ltEq =>
      case l of
        Empty _ =>
          let (Evidence color' l', r') = insertLeft k v k' v' l r {ltEq, kp, keyslEq = Refl, keysrEq = Refl} in
          Evidence Black $ BlackNode k' v' l' r' {kp = MkInCons k keys kp}
        BlackNode _ _ _ _ =>
          let (Evidence color' l', r') = insertLeft k v k' v' l r {ltEq, kp, keyslEq = Refl, keysrEq = Refl} in
          Evidence Black $ BlackNode k' v' l' r' {kp = MkInCons k keys kp}
        RedNode _ _ _ _ =>
          let (l', r') = insertLeft k v k' v' l r {kp, ltEq, keyslEq = Refl, keysrEq = Refl} in
          balanceLeft k' v' l' r' {kord, zkp = MkInCons _ _ kp}
    Element EQ p0 =>
        let
          0 p5 : (x : kt) -> (k > x = k' > x)
          p5 x = cong (\case { GT => True; _ => False }) $ equality1 k k' x p0

          0 p6 : (x : kt) -> (k < x = k' < x)
          p6 x = cong (\case { LT => True; _ => False }) $ equality1 k k' x p0
        in
        let 0 p1 : (filter (k >) keys = (filter (k' >) keys)) = filterExtensionality p5 in
        let 0 p2 : (filter (k >) (k :: keys) = filter (k >) keys)
            = rewrite reflexivity k in Refl in
        let 0 p3 : (filter (k <) keys = (filter (k' <) keys)) = filterExtensionality p6 in
        let 0 p4 : (filter (k <) (k :: keys) = filter (k <) keys)
            = rewrite reflexivity k in Refl in
        let l' : GoodTree {color = colorLeft, height = height', kt, kord, vt, keys = filter (k >) (k :: keys)} =
            rewrite trans p2 p1 in l
        in
        let r' : GoodTree {color = colorRight, height = height', kt, kord, vt, keys = filter (k <) (k :: keys)} =
            rewrite trans p4 p3 in r
        in
        Evidence Black $ BlackNode k v l' r' {kp = MkIn k (cong (\case { EQ => True; _ => False }) (reflexivity k)) keys}
    Element GT gtEq =>
      case r of
        Empty _ =>
          let (l', Evidence color' r') = insertRight k v k' v' l r {gtEq, kp, keyslEq = Refl, keysrEq = Refl} in
          Evidence Black $ BlackNode k' v' l' r' {kp = MkInCons k keys kp}
        BlackNode _ _ _ _ =>
          let (l', Evidence color' r') = insertRight k v k' v' l r {gtEq, kp, keyslEq = Refl, keysrEq = Refl} in
          Evidence Black $ BlackNode k' v' l' r' {kp = MkInCons k keys kp}
        RedNode _ _ _ _ =>
          let (l', r') = insertRight k v k' v' l r {kp, gtEq, keyslEq = Refl, keysrEq = Refl} in
          balanceRight k' v' l' r' {kord, xkp = MkInCons _ _ kp}

public export
insertG :
  {0 color : Color} ->
  (kord : LawfulOrd kt) =>
  (k : kt) ->
  vt k ->
  GoodTree {kt, height, color, kord, vt, keys} ->
  Exists \color' => Exists \height' => GoodTree {color = color', height = height', kt, kord, vt, keys = k :: keys}
insertG k v tree@(Empty Refl) =
  let Evidence color' tree' = insertG' k v tree in
  Evidence color' $ Evidence 0 tree'
insertG k v tree@(BlackNode _ _ _ _ {height = height'}) =
  let Evidence color' tree' = insertG' k v tree in
  Evidence color' $ Evidence (S height') tree'
insertG k v tree@(RedNode _ _ _ _) =
  let BadRedNode k' v' l r {height = height', kp} = insertG' k v tree in
  Evidence Black $ Evidence (S height') $ BlackNode k' v' l r {kp}

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module Main

test : List (Maybe Integer)
test = [Just 1]

-- using (.) from prelude
test1 : (List . Maybe) Integer
test1 = [Just 1]

-- using (.) and ($) from prelude
test2 : List . Maybe $ Integer
test2 = [Just 1]

main : IO ()
main = do
  print test
  print test1
  print test2

max_stars_repo_name: srghma/hask-test

max_issues_repo_name: BjornMelgaard/hask-test

max_forks_repo_name: BjornMelgaard/hask-test


text:
module Foo

%deprecate
export
dep1 : String
dep1 = "hello"

||| Just use the string "world" directly from now on.
%deprecate
export
dep2 : String
dep2 = "world"

%deprecate
export
dep3 : String -> String
dep3 x = x ++ "!"

%deprecate
public export
0 foo : (0 a : Type) -> Type
foo x = List x


text:
module Typing.Util

import Typing.Common

-- 8YYYY 0   0  o8o  0    0   0  o8o  YY8YY 8YYYY
-- 8___  0   0 8   8 0    0   0 8   8   0   8___
-- 8"""  "o o" 8YYY8 0    0   0 8YYY8   0   8"""
-- 8oooo  "8"  0   0 8ooo "ooo" 0   0   0   8oooo

export
evaluate : Term -> TypeChecker Term
evaluate m = do
	defs <- definitions {s=TCState}
	let scope = fromList $ [ (x,m') | (x,m',_) <- toList defs ]
	let evalResult = runReaderT (eval m) scope
	case evalResult of
		Left e   => throw e
		Right m' => pure m'

-- Y8Y 8o  0 oYYYo YY8YY  o8o  8o  0 YY8YY Y8Y  o8o  YY8YY 8YYYY 8_   _8 8YYYY YY8YY  o8o  oYYYo
--  0  8Yo 8 %___    0   8   8 8Yo 8   0    0  8   8   0   8___  8"o_o"8 8___    0   8   8 %___
--  0  8 Yo8 `"""p   0   8YYY8 8 Yo8   0    0  8YYY8   0   8"""  0  8  0 8"""    0   8YYY8 `"""p
-- o8o 0   8 YoooY   0   0   0 0   8   0   o8o 0   0   0   8oooo 0     0 8oooo   0   0   0 YoooY

export
instantiateMetas : Substitution -> Term -> Term

export
instantiateClause : Substitution -> Clause -> Clause

export
instantiateMetasCaseMotive : Substitution -> CaseMotive -> CaseMotive

export
instantiateMetasPat : Substitution -> Pattern -> Pattern
instantiateMetas _ (Var x) = Var x
instantiateMetas subs (Meta i) = case lookup i subs of
      Nothing => Meta i
      Just t  => instantiateMetas subs t
instantiateMetas _ (DottedVar m x) = DottedVar m x
instantiateMetas _ (AbsoluteDottedVar m x) = AbsoluteDottedVar m x
instantiateMetas subs (Ann m t) = Ann (instantiateMetas subs m) (instantiateMetas subs t)
instantiateMetas _ Star = Star
instantiateMetas subs (Pi plic a sc) = Pi plic
	(instantiateMetas subs a)
	(instantiateMetas subs <$> sc)
instantiateMetas subs (Lam plic sc) = Lam plic (instantiateMetas subs <$> sc)
instantiateMetas subs (App plic f a) = App plic
	(instantiateMetas subs f)
	(instantiateMetas subs a)
instantiateMetas subs (Con c as) = Con c (map (\(plic, a) => (plic, instantiateMetas subs a)) as)
instantiateMetas subs (Case as mot cs) = Case (map (instantiateMetas subs) as)
	(instantiateMetasCaseMotive subs mot)
	(map (instantiateClause subs) cs)

instantiateMetas subs (RecordType tele) = RecordType (instantiateMetasTelescope tele)
where
	instantiateMetasTelescope TelescopeNil = TelescopeNil
	instantiateMetasTelescope (TelescopeCons t sc) = TelescopeCons
		(instantiateMetas subs t)
		(instantiateMetasTelescope <$> sc)
instantiateMetas subs (RecordCon fields) = RecordCon [ (x,instantiateMetas subs m) | (x,m) <- fields ]
instantiateMetas subs (Project m x) = Project (instantiateMetas subs m) x

instantiateClause subs (NewClause psc sc) = NewClause
	(map (instantiateMetasPat subs) <$> psc)
	(instantiateMetas subs <$> sc)

instantiateMetasCaseMotive subs (CaseMotiveNil a) = CaseMotiveNil (instantiateMetas subs a)
instantiateMetasCaseMotive subs (CaseMotiveCons a sc) = CaseMotiveCons
	(instantiateMetas subs a)
	(instantiateMetasCaseMotive subs <$> sc)

instantiateMetasPat _ (VarPat x) = VarPat x
instantiateMetasPat subs (ConPat c ps) = ConPat c (map (\(plic,p) => (plic,instantiateMetasPat subs p)) ps)
instantiateMetasPat subs (AssertionPat m) = AssertionPat (instantiateMetas subs m)
instantiateMetasPat _ MakeMeta = MakeMeta

-- 0   0 8o  0  o8o  0    Y8Y  o8o  oYYYo
-- 0   0 8Yo 8 8   8 0     0  8   8 %___
-- 0   0 8 Yo8 8YYY8 0     0  8YYY8 `"""p
-- "ooo" 0   8 0   0 8ooo o8o 0   0 YoooY

export
unalias : String \/ FullName -> TypeChecker FullName
unalias (Left n) = do
	als <- aliases
	case lookup (Left n) als of
		Nothing => throw $ "The symbol " ++ n ++ " is not an alias for any "
							++ "module-declared symbol."
		Just p  => pure p
unalias (Right (m,n)) = do
	als <- aliases
	case lookup (Right (m,n)) als of
		Nothing => throw $ "The symbol " ++ m ++ "." ++ n ++ " is not an alias for any "
							++ "module-declared symbol."
		Just p  => pure p

-- YY8YY 0   0 8YYYo 8YYYY      Y8Y 8o  0
--   0   "o o" 8___P 8___  ____  0  8Yo 8
--   0     0   8"""  8"""  """"  0  8 Yo8
--   0     0   0     8oooo      o8o 0   8

export
typeInSignature : Constructor -> TypeChecker (Constructor >< ConSig Term)
typeInSignature (BareCon n0) = do
	consigs <- signature {s=TCState}
	(m,n) <- unalias (Left n0)
	case lookup (m,n) consigs of
		Nothing => throw $ "Unknown constructor: " ++ show (DottedCon m n)
		Just t  => pure (AbsoluteDottedCon m n, t)
typeInSignature (DottedCon m n) = do
	consigs <- signature {s=TCState}
	(m',n') <- unalias (Right (m,n))
	case lookup (m',n') consigs of
		Nothing => throw $ "Unknown constructor: " ++ show (DottedCon m' n')
		Just t  => pure (AbsoluteDottedCon m' n', t)
typeInSignature (AbsoluteDottedCon m n) = do
	consigs <- signature {s=TCState}
	case SortedMap.lookup (m,n) consigs of
		Nothing => throw $ "Unknown constructor: " ++ show (AbsoluteDottedCon m n)
		Just t  => pure (AbsoluteDottedCon m n, t)

export
absoluteDottedTypeInDefinitions : String -> String -> TypeChecker (FullName >< Term)
absoluteDottedTypeInDefinitions m x = do
	defs <- definitions
	case find (\(mx,_,_) => mx == (m,x)) (toList defs) of
		Nothing      => throw $ "Unknown constant/defined term: " ++ m ++ "." ++ x
		Just (_,_,t) => pure ((m, x), t)

export
dottedTypeInDefinitions : String -> String -> TypeChecker (FullName >< Term)
dottedTypeInDefinitions m x = do
	(m',x') <- unalias (Right (m,x))
	absoluteDottedTypeInDefinitions m' x'

export
typeInDefinitions : String -> TypeChecker (FullName >< Term)
typeInDefinitions x0 = do
	(m,x) <- unalias (Left x0)
	defs <- definitions
	case find (\(mx,_,_) => mx == (m,x)) (toList defs) of
		Nothing      => throw $ "Unknown constant/defined term: " ++ m ++ "." ++ x
		Just (_,_,t) => pure ((m,x),t)

export
typeInContext : Int -> TypeChecker Term
typeInContext i = do
	ctx <- context
	case find (\(j,_,_) => j == i) ctx of
		Nothing      => throw "Unbound automatically generated variable."
		Just (_,_,t) => pure t

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module XML.Lexer

import Text.Lexer

import public Commons.Text.Lexer.Run

%default total
%access private

public export
data Token = Entity String
           | Struct String
           | Symbol String
           | Word String
           | Text String
           | Comment String
           | CData String
           | StringLit String
           | WS String
           | NotRecognised String
           | EndInput

public export
Eq Token where
  (==) (Entity x)         (Entity y)        = x == y
  (==) (Struct x)         (Struct y)        = x == y
  (==) (Symbol x)         (Symbol y)        = x == y
  (==) (Word x)           (Word y)          = x == y
  (==) (Text x)           (Text y)          = x == y
  (==) (Comment x)        (Comment y)       = x == y
  (==) (CData x)          (CData y)         = x == y
  (==) (StringLit x)      (StringLit y)     = x == y
  (==) (WS x)             (WS y)            = x == y
  (==) (NotRecognised x)  (NotRecognised y) = x == y
  (==) EndInput           EndInput          = True
  (==) _ _ = False

public export
Show Token where
  show (Entity s)           =  "(Entity " ++ s ++ ")"
  show (Struct s)           =  "(Struct " ++ s ++ ")"
  show (Symbol s)           =  "(Symbol " ++ s ++ ")"
  show (Word s)             =  "(Word " ++ s ++ ")"
  show (Text s)             =  "(Text " ++ s ++ ")"
  show (Comment s)          =  "(Comment " ++ s ++ ")"
  show (CData s)            =  "(CData " ++ s ++ ")"
  show (StringLit s)        =  "(StringLit " ++ s ++ ")"
  show (WS s)               =  "(WS " ++ s ++ ")"
  show (NotRecognised s)    =  "(NotRecognised " ++ s ++ ")"
  show (EndInput)           =  "(EndInput)"

word : Lexer
word = alphaNums

pathChar : Lexer
pathChar = oneOf "\\.:#=?-!"

url : Lexer
url = some pathChar

validSymbol : Lexer
validSymbol = pathChar --<|> (non (oneOf "\"&'<>"))

entity : Lexer
entity = exact "&"
      <+> ((exact "quot")
       <|> (exact "amp")
       <|> (exact "apos")
       <|> (exact "lt")
       <|> (exact "gt"))
      <+> exact ";"

nodeSymbol : Lexer
nodeSymbol = exact "<" <|> exact ">" <|> exact "/"

comment : Lexer
comment = blockComment (exact "<!--") (exact "-->")

cdata : Lexer
cdata = blockComment (exact "<![CDATA[") (exact "]]>")

xmlChar : Lexer
xmlChar = entity <|> non (oneOf "\"&'<>") <|> space

xmlText : Lexer
xmlText = (entity <|> non (oneOf "\"&'<>")) <+> some xmlChar <+> reject (exact "<")

tokenMap : TokenMap Token
tokenMap =
  [ (space, WS)
  , (comment, Comment)
  , (cdata, CData)
  , (stringLit, StringLit)
  , (nodeSymbol, Struct)
  , (entity, Entity)
  , (validSymbol, Symbol)
  , (word, Word)
  , (xmlText, Text)
  , (any, NotRecognised)
  ]

keep : TokenData Token -> Bool
keep t = case tok t of
  WS _ => False
  _ => True

export
XMLLexer : Lexer Token
XMLLexer = MkLexer tokenMap keep EndInput

export
lexXMLStr : String -> Either LexError (List (TokenData Token))
lexXMLStr = lexString XMLLexer

export
lexXMLFile : String -> IO $ Either LexFail (List (TokenData Token))
lexXMLFile = lexFile XMLLexer

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Cordial.Model.Common.Hacks

%default total
%access public export

fromDoubleToNat : Double -> Nat
fromDoubleToNat x =
  let x_int = cast {to=Int} x
  in cast {to=Nat} x_int

calcBits : Double -> Double
calcBits d = (ceiling ((log (d / 8)) / (log 2))) - 1

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Pipes.Prelude

import Control.Monad.Trans
import Pipes.Core

%access export

-- Helper functions to construct Sources more easily
-- * `stdinLn` lifts the standard output to a Source
-- * `iterating` creates an infinite series of value f(f(f(f(...))))
-- * `unfolding` creates a possibly infinite series of value from a seed

stdinLn : String -> Source IO String
stdinLn promptLine = recur where
  recur = do
    lift (putStr promptLine)
    lift getLine >>= yield
    recur

streamFile : File -> Source IO (Either FileError String)
streamFile f = recur f where
  recur f = do
    end <- lift (fEOF f)
    if end
      then lift (closeFile f)
      else do
        l <- lift (fGetLine f)
        yieldOr l (closeFile f)
        recur f

readFile : String -> Source IO (Either FileError String)
readFile fileName = do
  Right f <- lift (openFile fileName Read)
    | Left err => yield (Left err)
  streamFile f

iterating : (Monad m) => (a -> a) -> a -> Source m a
iterating f = recur where
  recur a = do
    yield a
    recur (f a)

unfolding : (Monad m) => (seed -> Maybe (a, seed)) -> seed -> Source m a
unfolding f = recur . f where
  recur Nothing = pure ()
  recur (Just (a, seed)) = do
    yield a
    recur (f seed)

replicating : (Monad m) => Nat -> a -> Source m a
replicating times x = recur times where
  recur Z = pure ()
  recur (S n) = do yield x; recur n

-- Helper functions to construct pipes more easily
-- * `mapping` lifts a function as a pipe transformation
-- * `filtering` lifts a predicate into a pipe filter
-- * `takingWhile` lifts a predicate into a pipe breaker
-- * `droppingWhile` lifts a predicate into a pipe delayed starter

mapping : (Monad m) => (a -> b) -> Pipe a m b
mapping f = awaitForever (yield . f)

mappingM : (Monad m) => (a -> m b) -> Pipe a m b
mappingM f = awaitForever $ \x => lift (f x) >>= yield

concatting : (Monad m, Foldable f) => Pipe (f a) m a
concatting = awaitForever each

concatMapping : (Monad m, Foldable f) => (a -> f b) -> Pipe a m b
concatMapping f = mapping f .| concatting

filtering : (Monad m) => (a -> Bool) -> Pipe a m a
filtering p = awaitForever $ \x => if p x then yield x else pure ()

filteringJust : (Monad m) => Pipe (Maybe a) m a
filteringJust = awaitForever $ maybe (pure ()) yield

taking : (Monad m) => Nat -> PipeM a a r m (Maybe r)
taking = recur where
  recur Z = pure Nothing
  recur (S n) = do
    x <- awaitOr
    case x of
      Left r => pure (Just r)
      Right x => do yield x; taking n

dropping : (Monad m) => Nat -> Pipe a m a
dropping Z = idP
dropping (S n) = awaitOne $ \x => dropping n

takingWhile : (Monad m) => (a -> Bool) -> PipeM a a r m (Maybe r)
takingWhile p = recur where
  recur = do
    mx <- awaitOr
    case mx of
      Left r => pure (Just r)
      Right x => if p x
        then do yield x; recur
        else pure Nothing

droppingWhile : (Monad m) => (a -> Bool) -> Pipe a m a
droppingWhile p = recur where
  recur = awaitOne $ \x =>
    if p x
      then recur
      else do yield x; idP

deduplicating : (Eq a, Monad m) => Pipe a m a
deduplicating = recur (the (a -> Bool) (const True)) where
  recur isDifferent =
    awaitOne $ \x => do
      when (isDifferent x) (yield x)
      recur (/= x)

repeating : (Monad m) => Nat -> Pipe a m a
repeating n = awaitForever $ \x => sequence_ (replicate n (yield x))

tracing : (Monad m) => (a -> m b) -> Pipe a m a
tracing trace = mappingM (\x => trace x *> pure x)

groupingBy : (Monad m) => (a -> a -> Bool) -> Pipe a m (List a)
groupingBy sameGroup = recur (the (List a) []) where
  recur xs = do
    mx <- awaitOr
    case mx of
      Left r => do
        when (length xs > 0) (yield (reverse xs))
        pure r
      Right y => do
        case xs of
          [] => recur [y]
          (x::_) =>
            if sameGroup x y
                then recur (y::xs)
                else do
                  yield (reverse xs)
                  recur [y]

grouping : (Monad m, Eq a) => Pipe a m (List a)
grouping = groupingBy (==)

chunking : (Monad m) => (n: Nat) -> {auto prf: GTE n 0} -> Pipe a m (List a)
chunking chunkSize = recur (the (List a -> List a) id) chunkSize where
  recur diffList Z = do
    yield (diffList [])
    recur id chunkSize
  recur diffList (S n) = do
    x <- awaitOr
    case x of
      Left r => do yield (diffList []); pure r
      Right x => recur (diffList . (x ::)) n

splittingBy : (Monad m) => (a -> Bool) -> Pipe a m (List a)
splittingBy p = recur (the (List a) []) where
  recur xs = do
    x <- awaitOr
    case x of
      Left r => do yield (reverse xs); pure r
      Right x => if p x
        then do yield (reverse xs); recur []
        else recur (x :: xs)

scanning : (Monad m) => (a -> b -> b) -> b -> Pipe a m b
scanning f initial = do
    yield initial
    recur initial
  where
    recur acc = awaitOne $ \x => do
      let acc' = f x acc
      yield acc'
      recur acc'

-- Helper functions to construct Sinks more easily
-- * `stdoutLn` lifts the standard output to a Sink
-- * `discard` consumes all outputs and ignore them

discard : (Monad m) => SinkM a m r r
discard = awaitForever $ \_ => pure ()

stdoutLn : SinkM String IO r r
stdoutLn = tracing putStrLn .| discard

summing : (Monad m, Num a) => Sink a m a
summing = fold (+) 0

multiplying : (Monad m, Num a) => Sink a m a
multiplying = fold (*) 1

consuming : (Monad m) => Sink a m (List a)
consuming = recur (the (List a -> List a) id) where
  recur diffList = do
    mx <- await
    case mx of
      Just x => recur (diffList . (x ::))
      Nothing => pure (diffList [])

--

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
module Language.LSP.Message.CodeAction

import Language.JSON
import Language.LSP.Message.Command
import Language.LSP.Message.Derive
import Language.LSP.Message.Diagnostics
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

namespace CodeActionKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
  public export
  data CodeActionKind
    = Empty
    | QuickFix
    | Refactor
    | RefactorExtract
    | RefactorInline
    | RefactorRewrite
    | Source
    | SourceOrganizeImport
    | Other String

export
ToJSON CodeActionKind where
  toJSON Empty                = JString ""
  toJSON QuickFix             = JString "quickfix"
  toJSON Refactor             = JString "refactor"
  toJSON RefactorExtract      = JString "refactor.extract"
  toJSON RefactorInline       = JString "refactor.inline"
  toJSON RefactorRewrite      = JString "refactor.rewrite"
  toJSON Source               = JString "source"
  toJSON SourceOrganizeImport = JString "source.organizeImports"
  toJSON (Other act)          = JString act

export
FromJSON CodeActionKind where
  fromJSON (JString "")                       = pure Empty
  fromJSON (JString "quickfix")               = pure QuickFix
  fromJSON (JString "refactor")               = pure Refactor
  fromJSON (JString "refactor.extract")       = pure RefactorExtract
  fromJSON (JString "refactor.inline")        = pure RefactorInline
  fromJSON (JString "refactor.rewrite")       = pure RefactorRewrite
  fromJSON (JString "source")                 = pure Source
  fromJSON (JString "source.organizeImports") = pure SourceOrganizeImport
  fromJSON (JString act)                      = pure (Other act)
  fromJSON _ = neutral

namespace CodeActionClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
  public export
  record CodeActionKindValueSet where
    constructor MkCodeActionKindValueSet
    valueSet : List CodeActionKind
  %runElab deriveJSON defaultOpts `{CodeActionKindValueSet}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
  public export
  record CodeActionLiteralSupport where
    constructor MkCodeActionLiteralSupport
    codeActionKind : CodeActionKindValueSet
  %runElab deriveJSON defaultOpts `{CodeActionLiteralSupport}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
  public export
  record ResolveSupport where
    constructor MkResolveSupport
    properties : List String
  %runElab deriveJSON defaultOpts `{ResolveSupport}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeActionClientCapabilities where
  constructor MkCodeActionClientCapabilities
  dynamicRegistration      : Maybe Bool
  codeActionLiteralSupport : Maybe CodeActionLiteralSupport
  isPreferredSupport       : Maybe Bool
  disabledSupport          : Maybe Bool
  dataSupport              : Maybe Bool
  resolveSupport           : Maybe ResolveSupport
  honorsChangeAnnotations  : Maybe Bool
%runElab deriveJSON defaultOpts `{CodeActionClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeActionOptions where
  constructor MkCodeActionOptions
  workDoneProgress : Maybe Bool
  codeActionKinds  : Maybe (List CodeActionKind)
  resolveProvider  : Maybe Bool
%runElab deriveJSON defaultOpts `{CodeActionOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeActionRegistrationOptions where
  constructor MkCodeActionRegistrationOptions
  workDoneProgress : Maybe Bool
  codeActionKinds  : Maybe (List CodeActionKind)
  resolveProvider  : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{CodeActionRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeActionContext where
  constructor MkCodeActionContext
  diagnostics : List Diagnostic
  only        : Maybe (List CodeActionKind)
%runElab deriveJSON defaultOpts `{CodeActionContext}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeActionParams where
  constructor MkCodeActionParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  range              : Range
  context            : CodeActionContext
%runElab deriveJSON defaultOpts `{CodeActionParams}

namespace CodeAction
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
  public export
  record Disabled where
    constructor MkDisabled
    reason : String
  %runElab deriveJSON defaultOpts `{Disabled}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeAction
public export
record CodeAction where
  constructor MkCodeAction
  title       : String
  kind        : Maybe CodeActionKind
  diagnostics : Maybe (List Diagnostic)
  isPreferred : Maybe Bool
  disabled    : Maybe Disabled
  edit        : Maybe WorkspaceEdit
  command     : Maybe Command
  data_       : Maybe JSON
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{CodeAction}


text:
module NormalModeParser

import Keys

%default total
%access public

data Token = Register KeyChord
           | Multiplier Nat
           | KeyChordT KeyChord

parseMultiplier : Digit -> List KeyChord -> (Nat, List KeyChord)
parseMultiplier digit keycs =
  let (digitKeys, keycs') = span isDigit keycs
      digits = reverse $ catMaybes $ map toDigit digitKeys
      n = foldr (\d,acc => acc*10+cast d) (cast digit) digits
  in (n, keycs')

private
parseOne : List KeyChord -> (Maybe Token, List KeyChord)
parseOne [] = (Nothing, [])
parseOne ((KC SingleQuote Shift _ _ _ _) :: (keyc :: keycs)) = (Just $ Register keyc, keycs)
parseOne ((KC (DigitKey digit) NoShift _ _ _ _) :: keycs) =
  let (n, keycs') = parseMultiplier digit keycs
  in (Just $ Multiplier n, keycs')
parseOne (keyc :: keycs) = (Just $ KeyChordT keyc, keycs)

parse : List KeyChord -> List Token
parse [] = []
parse (x :: xs) = []


text:
module Erlang.System

import public Data.So
import Data.Maybe
import Data.Strings

import Erlang

%default total

||| Sleep for a given duration.
|||
||| The duration is specified in milliseconds.
export
sleep : HasIO io => (ms : Int) -> io ()
sleep ms = do
  pure $ erlUnsafeCall ErlTerm "timer" "sleep" [ms]
  pure ()

||| Get arguments provided when launching the program.
export
getArgs : HasIO io => io (List String)
getArgs = do
  args <- pure $ erlUnsafeCall (List ErlCharlist) "init" "get_plain_arguments" []
  pure $ map (\(MkCharlist x) => x) args

||| Get all environment variables.
export
getEnvironment : HasIO io => io (List (String, String))
getEnvironment = do
  envPairs <- pure $ erlUnsafeCall (List ErlCharlist) "os" "getenv" []
  pure $ map (\(MkCharlist x) => splitEq x) envPairs
  where
    splitEq : String -> (String, String)
    splitEq str =
      let (key, str') = break (== '=') str
          (_, value) = break (/= '=') str'
      in  (key, value)

||| Try to get the value of the given environment variable.
export
getEnv : HasIO io => (key : String) -> io (Maybe String)
getEnv key = do
  result <- pure $ erlUnsafeCall ErlCharlist "os" "getenv" [MkCharlist key]
  let Right (MkCharlist str) = erlDecode charlist result
    | Left _ => pure Nothing
  pure $ Just str

||| Set an environment variable to a value.
|||
||| If `overwrite` is given the value `False`, the environment variable will
||| only be set if it is not already set.
export
setEnv : HasIO io => (key : String) -> (value : String) -> (overwrite : Bool) -> io Bool
setEnv key value overwrite = do
  shouldSetEnv <- case overwrite of
    True => pure True
    False => isNothing <$> getEnv key
  when shouldSetEnv $ do
    pure $ erlUnsafeCall ErlTerm "os" "putenv" [MkCharlist key, MkCharlist value]
    pure ()
  pure True

||| Unset a given environment variable.
|||
||| Always returns true.
export
unsetEnv : HasIO io => (key : String) -> io Bool
unsetEnv key = do
  result <- pure $ erlUnsafeCall ErlTerm "os" "unsetenv" [MkCharlist key]
  pure True

||| Run a system command.
|||
||| The return value is the exit code of the command.
-- TODO: Implement with exit code
export
system : HasIO io => String -> io Int
system cmd = do
  MkCharlist output <- pure $ erlUnsafeCall ErlCharlist "os" "cmd" [MkCharlist cmd]
  putStr output
  pure 0

||| Get the number of seconds since Epoch.
|||
||| Epoch is defined as: 00:00:00 GMT, January 1, 1970
|||
||| Read more at:
||| https://pubs.opengroup.org/onlinepubs/9699919799/xrat/V4_xbd_chap03.html#tag_21_03_00_17
export
time : HasIO io => io Integer
time = do
  result <- pure $ erlUnsafeCall Integer "erlang" "system_time" []
  pure $ result `div` 1000000000

||| Programs can either terminate successfully, or end in a caught
||| failure.
public export
data ExitCode : Type where
  ||| Terminate successfully.
  ExitSuccess : ExitCode
  ||| Program terminated for some prescribed reason.
  |||
  ||| @errNo A non-zero numerical value indicating failure.
  ||| @prf   Proof that the int value is non-zero.
  ExitFailure : (errNo : Int) -> (So (not $ errNo == 0)) => ExitCode

||| Halt the run-time system.
partial
halt : HasIO io => Int -> io a
halt code = do
  MkRaw x <- pure $ erlUnsafeCall (Raw a) "erlang" "halt" [code]
  pure x

||| Exit the program with the given exit code.
export partial
exitWith : HasIO io => ExitCode -> io a
exitWith ExitSuccess = halt 0
exitWith (ExitFailure code) = halt code

||| Exit the program indicating failure.
export partial
exitFailure : HasIO io => io a
exitFailure = exitWith (ExitFailure 1)

||| Exit the program after a successful run.
export partial
exitSuccess : HasIO io => io a
exitSuccess = exitWith ExitSuccess


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Main

import StarterWareFree.Drivers
import StarterWareFree.Platform

%include c "busywait.h"

GPIO_INSTANCE_ADDRESS : Int
GPIO_INSTANCE_ADDRESS = 0x4804C000

GPIO_INSTANCE_PIN_NUMBER : Int
GPIO_INSTANCE_PIN_NUMBER = 23

setupGpio : IO ()
setupGpio = do
    -- Enabling functional clocks for GPIO1 instance
    GPIO1ModuleClkConfig

    -- Selecting GPIO1[23] pin for use
    GPIO1Pin23PinMuxSetup

    -- Enabling the GPIO module
    GPIOModuleEnable GPIO_INSTANCE_ADDRESS

    -- Resetting the GPIO module
    GPIOModuleReset GPIO_INSTANCE_ADDRESS

    -- Setting the GPIO pin as an output pin
    GPIODirModeSet
        GPIO_INSTANCE_ADDRESS
        GPIO_INSTANCE_PIN_NUMBER
        GPIO_DIR_OUTPUT

ONOFFTIME : Int
ONOFFTIME = 50000000

delay : Int -> IO ()
delay loops = foreign FFI_C "busywait" (Int -> IO ()) loops

blinkLed : IO ()
blinkLed = do
    -- Driving a logic HIGH on the GPIO pin
    GPIOPinWrite
        GPIO_INSTANCE_ADDRESS
        GPIO_INSTANCE_PIN_NUMBER
        GPIO_PIN_HIGH

    delay ONOFFTIME

    -- Driving a logic LOW on the GPIO pin
    GPIOPinWrite
        GPIO_INSTANCE_ADDRESS
        GPIO_INSTANCE_PIN_NUMBER
        GPIO_PIN_LOW

    delay ONOFFTIME

    -- Repeat blink
    blinkLed

main : IO ()
main = do
    setupGpio
    blinkLed

max_stars_repo_name: mokshasoft/bare-metal-idris

max_issues_repo_name: mokshasoft/bare-metal-idris

max_forks_repo_name: mokshasoft/bare-metal-idris


text:
module TTImp.Elab.Dot

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

import TTImp.Elab.Check
import TTImp.Elab.ImplicitBind
import TTImp.TTImp

import Data.NameMap

%default covering

export
checkDot : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           RigCount -> ElabInfo ->
           NestedNames vars -> Env Term vars ->
           FC -> DotReason -> RawImp -> Maybe (Glued vars) ->
           Core (Term vars, Glued vars)
checkDot rig elabinfo nest env fc reason tm Nothing
    = throw (GenericMsg fc ("Dot pattern not valid here (unknown type) "
                            ++ show tm))
checkDot rig elabinfo nest env fc reason tm (Just gexpty)
    = case elabMode elabinfo of
        InLHS _ =>
          do (wantedTm, wantedTy) <- check rig
                                              (record { elabMode = InExpr }
                                                  elabinfo)
                                              nest env
                                              tm (Just gexpty)
             nm <- genName "dotTm"
             expty <- getTerm gexpty
             metaval <- metaVar fc rig env nm expty
             addDot fc env nm wantedTm reason metaval
             pure (metaval, gexpty)
        _ => throw (GenericMsg fc ("Dot pattern not valid here (Not LHS) "
                                   ++ show tm))


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

%name Vect xs, ys, zs

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys
    = case xs of
           foo => ?bar

data Foo a = MkFoo a | MkBar (a -> a)

Functor Foo where
  map f thing = ?baz


text:
||| CSS Rules for the Math Game Example
module Examples.CSS.MathGame

import Data.Vect
import Examples.CSS.Colors
import public Examples.CSS.Core
import Rhone.JS
import Text.CSS

--------------------------------------------------------------------------------
--          IDs
--------------------------------------------------------------------------------

||| Where the message about the correct result
||| is printed to.
public export
out : ElemRef Div
out = Id Div "mathgame_out"

||| Select box where users choose the language.
public export
langIn : ElemRef Select
langIn = Id Select "mathgame_language"

||| Text field where users enter their result.
public export
resultIn : ElemRef Input
resultIn = Id Input "mathgame_input"

||| Button to check the entered result
public export
checkBtn : ElemRef Button
checkBtn = Id Button "mathgame_check_btn"

||| Button to start a new game
public export
newBtn : ElemRef Button
newBtn = Id Button "mathgame_newbtn"

||| ID of the picture canvas
public export
pic : ElemRef Canvas
pic = Id Canvas "mathgame_pic"

||| ID of the calculation label
public export
calc : ElemRef Div
calc = Id Div "mathgame_calc"

--------------------------------------------------------------------------------
--          CSS
--------------------------------------------------------------------------------

||| Message field class if answer is correct
export
correct : String
correct = "correct"

||| Message field class if answer is wrong
export
wrong : String
wrong = "wrong"

export
mathContent : String
mathContent = "mathgame_content"

export
lblLang : String
lblLang = "mathgame_lbllang"

data Tag = LLan | ILan | OClc | IRes | BChk | ORep | BNew | OPic | Dot

AreaTag Tag where
  showTag LLan = "LLan"
  showTag ILan = "ILan"
  showTag OClc = "OClc"
  showTag IRes = "IRes"
  showTag BChk = "BChk"
  showTag ORep = "ORep"
  showTag BNew = "BNew"
  showTag OPic = "OPic"
  showTag Dot  = "."

export
css : List (Rule 1)
css =
  [ Media "min-width: 300px"
      [ class mathContent !!
          [ Display             .= Area
              (replicate 6 MinContent)
              [MaxContent, MaxContent]
              [ [LLan, ILan]
              , [OClc, IRes]
              , [Dot,  BChk]
              , [Dot,  BNew]
              , [ORep, ORep]
              , [OPic, OPic]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , Media "min-width: 800px"
      [ class mathContent !!
          [ Display             .= Area
              (replicate 6 MinContent)
              [MaxContent, MaxContent, fr 1]
              [ [LLan, ILan, OPic]
              , [OClc, IRes, OPic]
              , [Dot,  BChk, OPic]
              , [Dot,  BNew, OPic]
              , [ORep, ORep, OPic]
              , [Dot,  Dot,  OPic]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , class lblLang !! [ GridArea .= LLan ]

  , idRef langIn  !!
      [ GridArea        .= ILan
      , FontSize        .= Large
      , TextAlign       .= End
      ]

  , idRef calc  !!
      [ GridArea        .= OClc
      , FontSize        .= Large
      , TextAlign       .= Start
      ]

  , idRef resultIn  !!
      [ GridArea        .= IRes
      , FontSize        .= Large
      , TextAlign       .= End
      ]

  , idRef checkBtn  !! [ GridArea .= BChk ]

  , idRef newBtn  !! [ GridArea .= BNew ]

  , idRef out  !!
      [ GridArea        .= ORep
      , FontSize        .= Large
      , TextAlign       .= Start
      ]

  , idRef pic  !!
      [ BackgroundSize  .= perc 100
      , JustifySelf     .= Center
      , GridArea        .= OPic
      , MaxWidth        .= px 500
      , Width           .= px 500
      ]

  , class correct !!
      [ Color           .= green ]

  , class wrong !!
      [ Color           .= red ]
  ]


text:
import Data.List

Input : Type
Input = ((Int, Int), (Int, Int))

part1 : Input -> IO String
part1 (_, (ymin, _)) = pure $ show $ (\v => (v * (v + 1)) `div` 2) $ abs $ ymin + 1

inTarget : (Int, Int) -> Input -> (Int, Int) -> Bool
inTarget (x, y) i@((xmin, xmax), (ymin, ymax)) (vx, vy) =
  (xmin <= x && x <= xmax && ymin <= y && y <= ymax) ||
  (x <= xmax && y >= ymin && inTarget (x + vx, y + vy) i (max 0 (vx - 1), vy - 1))

part2 : Input -> IO String
part2 i@((xmin, xmax), (ymin, ymax)) = do let xs = rangeFromTo 0 xmax
                                          let ys = rangeFromTo ymin (abs $ ymin + 1)
                                          pure $ show $ length $ filter (inTarget (0,0) i) $ join $ (\x => (x,) <$> ys) <$> xs

main : IO ()
main = do let a = ((14, 50), (-267, -225))
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
{-
then
else
-}
module Main

test : Bool -> IO ()
test b =
  putStrLn $
    if b
      then "then"
      else "else"

main : IO ()
main = do
  test True
  test False

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Ord

import Data.List

%default total

{-
  interface Eq ty => Ord ty where
    compare : ty -> ty -> Ordering -- required
    (<) : ty -> ty -> Ordering
    (>) : ty -> ty -> Ordering
    (<=) : ty -> ty -> Ordering
    (>=) : ty -> ty -> Ordering
    max : ty -> ty -> ty
    min : ty -> ty -> ty
-}

record Album where
  constructor MkAlbum
  artist : String
  title : String
  year : Integer

help : Album
help = MkAlbum "The Beatles" "Help" 1965

rubbersoul : Album
rubbersoul = MkAlbum "The Beatles" "Rubber Soul" 1965

clouds : Album
clouds = MkAlbum "Joni Mitchell" "Clouds" 1969

hunkydory : Album
hunkydory = MkAlbum "David Bowie" "Hunky Dory" 1971

heroes : Album
heroes = MkAlbum "David Bowie" "Heroes" 1977

collection : List Album
collection = [help, rubbersoul, clouds, hunkydory, heroes]

Eq Album where
  (==) (MkAlbum artist title year) (MkAlbum artist' title' year') =
    artist == artist' && title == title' && year == year'
  (==) _ _  = False

Ord Album where
  compare (MkAlbum artist title year) (MkAlbum artist' title' year') =
    case compare artist artist' of
         EQ => case compare year year' of
                    EQ => compare title title'
                    diffYear => diffYear
         diffArtist => diffArtist

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module FreeRTOS.Task.Control

%default total
%include C "FreeRTOS.h"
%include C "task.h"
%include C "FreeRTOS/idris_FreeRTOS.h"

||| An identifier of a Task
public export
data TID : Type where
     MkTID : (tid : Ptr) -> TID

||| Create a new task and add it to the list of tasks that are ready to run.
||| Returns `Nothing` if required memory couldn't be allocated.
export
create : (function : IO ()) -> IO (Maybe TID)
create func = do
    ptr <- fork func
    if !(nullPtr ptr)
        then pure Nothing
        else pure (Just (MkTID ptr))

||| Remove a task from the RTOS kernels management.
export
delete : IO ()
delete = do
    vm <- getMyVM
    foreign FFI_C "idris_stopThread" (Ptr -> IO ()) vm

||| Delay the task `ms` number of milliseconds.
export
delay : Int -> IO ()
delay ms =
    foreign FFI_C "wrapper_vTaskDelay" (Int -> IO ()) ms

||| Obtain the priority of any task.
getPriority : TID -> IO Int
getPriority (MkTID ptr) = do
    foreign FFI_C "uxTaskPriorityGet" (Ptr -> IO Int) ptr

||| Set the priority of any task.
setPriority : TID -> Int -> IO ()
setPriority (MkTID ptr) prio =
    foreign FFI_C "vTaskPrioritySet" (Ptr -> Int -> IO ()) ptr prio

||| Suspend any task. When suspended a task will never get any microcontroller processing time, no
||| matter what its priority.
suspend : TID -> IO ()
suspend (MkTID ptr) =
    foreign FFI_C "vTaskSuspend" (Ptr -> IO ()) ptr

||| Resumes a suspended task.
resume : TID -> IO ()
resume (MkTID ptr) =
    foreign FFI_C "vTaskResume" (Ptr -> IO ()) ptr

max_stars_repo_name: mokshasoft/FreeRTOS-community-ports

max_issues_repo_name: mokshasoft/FreeRTOS-community-ports

max_forks_repo_name: mokshasoft/FreeRTOS-community-ports


text:
module Leap

export
isLeap : Int -> Bool
isLeap year = ?isLeap_rhs

export
version : String
version = "1.0.0"


text:
module Main

import Baseline

loop : IO ()
loop = do
  str <- baseline "$> "
  case str of
       Nothing => putStrLn "Exit!"
       Just "" => loop
       Just s  => do
         putStrLn ("You typed: " ++ s)
         loop

main : IO ()
main = do
  addDictEntries
    [ "multidiscipline"
    , "multivitamin"
    , "multiplex"
    , "monocrystalline"
    , "streamline"
    , "waterline"
    , "skyline"
    , "online"
    , "byline" ]
  loop

max_stars_repo_name: laserpants/baseline-idris

max_issues_repo_name: laserpants/baseline-idris

max_forks_repo_name: laserpants/baseline-idris


text:
totalLen : List String -> Nat
totalLen xs = foldr (\el, acc  => length el  + acc) 0 xs


text:
module Replica.Other.Validation

%default total

public export
data Validation : (err, a : Type) -> Type where
  Valid : (x : a) -> Validation err a
  Error : (e : err) -> Validation err a

export
Functor (Validation err) where
  map f (Valid x) = Valid $ f x
  map f (Error x) = Error x

export
(Semigroup err) => Applicative (Validation err) where
  pure = Valid
  (Valid f)  <*> (Valid x)  = Valid $ f x
  (Valid _)  <*> (Error e)  = Error e
  (Error e)  <*> (Valid x)  = Error e
  (Error e1) <*> (Error e2) = Error $ e1 <+> e2

export
(Monoid err) => Alternative (Validation err) where
  empty = Error neutral
  (<|>) (Valid x) y = Valid x
  (<|>) (Error e) (Valid y) = Valid y
  (<|>) (Error e) (Error r) = Error $ e <+> r

export
fromEither : Applicative f =>  Either err a -> Validation (f err) a
fromEither = either (Error . pure) Valid

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
-- check that reorder works correctly

import System.Concurrency.Queue

main : IO ()
main =
  do q <- makeQueue
     let val1 = 1
     let val2 = 2
     let val3 = 3
     -- enqueue 2 values, which go on the rear stack
     enqueue q val1
     enqueue q val2
     -- dequeue to reorder
     (Just val1') <- dequeue q
       | Nothing => putStrLn "ERROR: First two values disappeared."
     if val1' == val2
        then putStrLn "ERROR: Queue behaved like a stack (broken reorder)."
        else do enqueue q val3    -- should go on rear; front contains val2
                (Just val2') <- dequeue q
                   | Nothing => putStrLn "ERROR: Second value disappeared."
                if val2' /= val2
                   then putStrLn "ERROR: Second value changed."
                   else do (Just val3') <- dequeue q
                              | Nothing =>
                                    putStrLn "ERROR: Third value disappeared."
                           if (val1 == val1')
                               && (val2 == val2')
                               && (val3 == val3')
                              then putStrLn "Success!"
                              else putStrLn "ERROR: Got different values back."


text:
module OStream -- If just "Stream", inrreconsilable conflict with names from PRelude.Stream

%default total
%access private

mutual
  public export
  data StreamCell a = Nil | (::) a (OStream a)
  infixr 7 ::

  {-
  I haven't figured out how define Stream at the top-level and not conflict with the version from
  Prelude.
  -}
  public export
  OStream : Type -> Type
  OStream a = Lazy (StreamCell a)

mutual
  append' : OStream a -> OStream a -> OStream a
  append' []       t = t
  append' (x :: s) t = x :: OStream.append s t
  -- elaborated Delayed prevents type-directed name resolution AND you can't qualify operators

  export
  append : OStream a -> OStream a -> OStream a
  append s t = Delay (Force (append' s t))

  export
  (++) : OStream a -> OStream a -> OStream a
  (++) = append

mutual
  take' : Int -> OStream a -> OStream a
  take' 0 s        = []
  take' n []       = []
  take' n (x :: s) = x :: OStream.take (n - 1) s
  -- elaborated Delayed prevents type-directed name resolution

  export
  take : Int -> OStream a -> OStream a
  take n s = Delay (Force (take' n s))

drop' : Int -> OStream a -> OStream a
drop' 0 s        = s
drop' n []       = []
drop' n (x :: s) = drop' (n - 1) s

export
drop : Int -> OStream a -> OStream a
drop n s = Delay (Force (drop' n s))

reverse' : OStream a -> OStream a -> OStream a
reverse' []       r = r
reverse' (x :: s) r = reverse' s (x :: r)

export
reverse : OStream a -> OStream a
reverse s = Delay (Force (reverse' s []))


text:
module Data.BVect

%default total
%access public export

data BVect : (u,c : Nat) -> Type -> Type where
  Nil : BVect n 0 type
  Add : (x : type)
     -> (prf : LTE (S c) n)
     -> BVect n c type
     -> BVect n (S c) type

namespace API
  (::) : (x : type) -> {auto prf : LTE (S c) n} -> BVect n c type -> BVect n (S c) type
  (::) x rest {prf} = Add x prf rest

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers