text:
> module Opt.Operations

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

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Rel.TotalPreorder
> import Rel.TotalPreorderOperations
> import Vect.Operations
> import Vect.Properties
> import Fun.Operations
> import Nat.LTProperties

> %default total

> %access public export

> |||
> argmaxMax : {A, B : Type} -> {R : B -> B -> Type} ->
>             TotalPreorder R ->
>             (fA : Finite A) ->
>             (ne : CardNotZ fA) ->
>             (f : A -> B) -> (A, B)
> argmaxMax {A} {B} tp fA nefA f = max (extendLeftLemma tp) abs ltZn where
>   n    : Nat
>   n    = card fA
>   ltZn : LT Z n
>   ltZn = notZisgtZ nefA
>   abs  : Vect n (A,B)
>   abs  = map (pair (id, f)) (toVect fA)

> |||
> max : {A, B : Type} -> {R : B -> B -> Type} ->
>       TotalPreorder R ->
>       (fA : Finite A) ->
>       (ne : CardNotZ fA) ->
>       (f : A -> B) -> B
> max tp fA nefA f = snd (argmaxMax tp fA nefA f)

> |||
> argmax : {A, B : Type} -> {R : B -> B -> Type} ->
>          TotalPreorder R ->
>          (fA : Finite A) ->
>          (ne : CardNotZ fA) ->
>          (f : A -> B) -> A
> argmax tp fA nefA f = fst (argmaxMax tp fA nefA f)

> |||
> maxSpec : {A, B : Type} -> {R : B -> B -> Type} ->
>           (tp : TotalPreorder R) ->
>           (fA : Finite A) ->
>           (nefA : CardNotZ fA) ->
>           (f : A -> B) ->
>           (a : A) -> R (f a) (max tp fA nefA f)
> maxSpec {A} {B} {R} tp fA nefA f a = s4 where
>   n    : Nat
>   n    = card fA
>   ltZn : LT Z n
>   ltZn = notZisgtZ nefA
>   abs  : Vect n (A,B)
>   abs  = map (pair (id, f)) (toVect fA)
>   s1   : Elem (a, f a) abs
>   s1   = mapLemma (toVect fA) (pair (id, f)) a (toVectComplete fA a)
>   s2   : (extendLeft R) (a, f a) (max (extendLeftLemma tp) abs ltZn)
>   s2   = maxLemma (extendLeftLemma tp) (a, f a) abs ltZn s1
>   s3   : R (f a) (snd (max (extendLeftLemma tp) abs ltZn))
>   s3   = s2
>   s4   : R (f a) (max tp fA nefA f)
>   s4   = s3

> |||
> argmaxSpec : {A, B : Type} -> {R : B -> B -> Type} ->
>              (tp : TotalPreorder R) ->
>              (fA : Finite A) ->
>              (nefA : CardNotZ fA) ->
>              (f : A -> B) ->
>              (max tp fA nefA f) = f (argmax tp fA nefA f)
> argmaxSpec {A} {B} tp fA nefA f = s3 where
>   ab : (A,B)
>   ab = argmaxMax tp fA nefA f
>   s1 : Elem ab (map (pair (Prelude.Basics.id, f)) (toVect fA))
>   s1 = maxElemLemma (extendLeftLemma tp) (map (pair (id, f)) (toVect fA)) (notZisgtZ nefA)
>   s2 : f (fst ab) = snd ab
>   s2 = mapIdfLemma (toVect fA) f ab s1
>   s3 : max tp fA nefA f = f (argmax tp fA nefA f)
>   s3 = sym s2

> {-

> argmaxMax : {A, B : Type} ->
>             TotalPreorder B ->
>             (fA : Finite A) ->
>             (ne : CardNotZ fA) ->
>             (f : A -> B) -> (A, B)
> argmaxMax {A} {B} tp fA nefA f = max (fromTotalPreorder2 tp) abs ltZn where
>   n    : Nat
>   n    = card fA
>   ltZn : LT Z n
>   ltZn = notZisgtZ nefA
>   abs  : Vect n (A,B)
>   abs  = map (pair (id, f)) (toVect fA)

> max : {A, B : Type} ->
>       TotalPreorder B ->
>       (fA : Finite A) ->
>       (ne : CardNotZ fA) ->
>       (f : A -> B) -> B
> max tp fA nefA f = snd (argmaxMax tp fA nefA f)

> argmax : {A, B : Type} ->
>          TotalPreorder B ->
>          (fA : Finite A) ->
>          (ne : CardNotZ fA) ->
>          (f : A -> B) -> A
> argmax tp fA nefA f = fst (argmaxMax tp fA nefA f)

> maxSpec : {A, B : Type} ->
>           (tp : TotalPreorder B) ->
>           (fA : Finite A) ->
>           (nefA : CardNotZ fA) ->
>           (f : A -> B) ->
>           (a : A) -> R tp (f a) (max tp fA nefA f)
> maxSpec {A} {B} tp fA nefA f a = s4 where
>   n    : Nat
>   n    = card fA
>   ltZn : LT Z n
>   ltZn = notZisgtZ nefA
>   abs  : Vect n (A,B)
>   abs  = map (pair (id, f)) (toVect fA)
>   s1   : Elem (a, f a) abs
>   s1   = mapLemma (toVect fA) (pair (id, f)) a (toVectComplete fA a)
>   s2   : (from2 (R tp)) (a, f a) (max (fromTotalPreorder2 tp) abs ltZn)
>   s2   = maxLemma (fromTotalPreorder2 tp) (a, f a) abs ltZn s1
>   s3   : R tp (f a) (snd (max (fromTotalPreorder2 tp) abs ltZn))
>   s3   = s2
>   s4   : R tp (f a) (max tp fA nefA f)
>   s4   = s3

> argmaxSpec : {A, B : Type} ->
>              (tp : TotalPreorder B) ->
>              (fA : Finite A) ->
>              (nefA : CardNotZ fA) ->
>              (f : A -> B) ->
>              (max tp fA nefA f) = f (argmax tp fA nefA f)
> argmaxSpec {A} {B} tp fA nefA f = s3 where
>   ab : (A,B)
>   ab = argmaxMax tp fA nefA f
>   s1 : Elem ab (map (pair (Prelude.Basics.id, f)) (toVect fA))
>   s1 = maxElemLemma (fromTotalPreorder2 tp) (map (pair (id, f)) (toVect fA)) (notZisgtZ nefA)
>   s2 : f (fst ab) = snd ab
>   s2 = mapIdfLemma (toVect fA) f ab s1
>   s3 : max tp fA nefA f = f (argmax tp fA nefA f)
>   s3 = sym s2

> {-

> argmaxMax : {A, B : Type} -> {TO : B -> B -> Type} ->
>             Preordered B TO =>
>             (fA : Finite A) -> (ne : CardNotZ fA) ->
>             (f : A -> B) -> (A,B)
> argmaxMax {A} {B} {TO} fA nefA f =
>   VectOperations.max {A = (A,B)} {TO = sndType TO} abs ltZn where
>     n    : Nat
>     n    = card fA
>     ltZn : LT Z n
>     ltZn = notZisgtZ nefA
>     abs  : Vect n (A,B)
>     abs  = map (pair (id, f)) (toVect fA)

> max : {A, B : Type} -> {TO : B -> B -> Type} ->
>       Preordered B TO =>
>       (fA : Finite A) -> (ne : CardNotZ fA) ->
>       (f : A -> B) -> B
> max fA nefA f = snd (argmaxMax fA nefA f)

> argmax : {A, B : Type} -> {TO : B -> B -> Type} ->
>          Preordered B TO =>
>          (fA : Finite A) -> (ne : CardNotZ fA) ->
>          (f : A -> B) -> A
> argmax fA nefA f = fst (argmaxMax fA nefA f)

> maxSpec : {A, B : Type} -> {TO : B -> B -> Type} ->
>           Preordered B TO =>
>           (fA : Finite A) -> (nefA : CardNotZ fA) ->
>           (f : A -> B) ->
>           (a : A) -> TO (f a) (max fA nefA f)
> maxSpec {A} {B} {TO} fA nefA f a = s4 where
>   n    : Nat
>   n    = card fA
>   ltZn : LT Z n
>   ltZn = notZisgtZ nefA
>   abs  : Vect n (A,B)
>   abs  = map (pair (id, f)) (toVect fA)
>   s1   : Elem (a, f a) abs
>   s1   = mapLemma (toVect fA) (pair (id, f)) a (toVectComplete fA a)
>   s2   : (sndType TO) (a, f a) (max abs ltZn)
>   s2   = maxLemma (a, f a) abs ltZn s1
>   s3   : TO (f a) (snd (max abs ltZn))
>   s3   = s2
>   s4   : TO (f a) (max fA nefA f)
>   s4   = s3

> argmaxSpec : {A, B : Type} -> {TO : B -> B -> Type} ->
>              Preordered B TO =>
>              (fA : Finite A) -> (nefA : CardNotZ fA) ->
>              (f : A -> B) ->
>              (max fA nefA f) = f (argmax fA nefA f)
> argmaxSpec {A} {B} fA nefA f = s3 where
>   ab : (A,B)
>   ab = argmaxMax fA nefA f
>   s1 : Elem ab (map (pair (id, f)) (toVect fA))
>   s1 = maxElemLemma (map (pair (id, f)) (toVect fA)) (notZisgtZ nefA)
>   s2 : f (fst ab) = snd ab
>   s2 = mapIdfLemma (toVect fA) f ab s1
>   s3 : max fA nefA f = f (argmax fA nefA f)
>   s3 = sym s2

> -}

> ---}


text:
module Expr

%access public export

data TypeT : Type where
  UnitT : TypeT
  IntT : TypeT
  DoubleT : TypeT
  BoolT : TypeT
  ArrayT : TypeT -> TypeT
  VarT : TypeT -> TypeT
  ArrowT : TypeT -> TypeT -> TypeT

Show TypeT where
  show UnitT = "unit"
  show IntT = "int"
  show DoubleT = "double"
  show BoolT = "bool"
  show (ArrayT typ) = show typ ++ " []"
  show (VarT typ) = show typ ++ " ref"
  show (ArrowT arg res) = "(" ++ show arg ++ " -> " ++ show res ++ ")"

interface Symantics (rep : TypeT -> Type) where
  defaultof : rep a
  int : Int -> rep IntT
  double : Double -> rep DoubleT
  bool : Bool -> rep BoolT
  (==) : rep IntT -> rep IntT -> rep BoolT
  (>) : rep IntT -> rep IntT -> rep BoolT
  (<) : rep IntT -> rep IntT -> rep BoolT
  (&&) : rep BoolT -> rep BoolT -> rep BoolT
  (||) : rep BoolT -> rep BoolT -> rep BoolT
  not : rep BoolT -> rep BoolT
  (+) : rep IntT -> rep IntT -> rep IntT
  (<+>) : rep DoubleT -> rep DoubleT -> rep DoubleT
  (*) : rep IntT -> rep IntT -> rep IntT
  (<*>) : rep DoubleT -> rep DoubleT -> rep DoubleT
  ite : rep BoolT -> rep a -> rep a -> rep a
  it : rep BoolT -> rep UnitT -> rep UnitT
  deref : rep (VarT a) -> rep a
  assign : rep a -> rep (VarT a) -> rep UnitT
  newVar : rep a -> (rep (VarT a) -> rep b) -> rep b
  letVal : rep a -> (rep a -> rep b) -> rep b
  index : rep IntT -> rep (ArrayT a) -> rep a
  length : rep (ArrayT a) -> rep IntT
  while : rep BoolT -> rep UnitT -> rep UnitT
  seq : rep a -> rep b -> rep b
  seqs : List (rep UnitT) -> rep UnitT
  lam : (rep a -> rep b) -> rep (ArrowT a b)
  app : rep (ArrowT a b) -> rep a -> rep b

data Code : TypeT -> Type where
  C : (Int -> String) -> Code a

Symantics Code where
  defaultof {a = UnitT} = C (\_ => "()")
  defaultof {a = IntT} = C (\_ => "0")
  defaultof {a = DoubleT} = C (\_ => "0")
  defaultof {a = BoolT} = C (\_ => "false")
  defaultof {a = (ArrayT x)} = C (\_ => "null")
  defaultof {a = (VarT x)} = C (\_ => "null")
  defaultof {a = (ArrowT x y)} = C (\_ => "null")
  int x = C (\_ => show x)
  double x = C (\_ => show x)
  bool x = C (\_ => if x then "true" else "false")
  (==) (C l) (C r) = C (\v => "( " ++ l v ++ " = " ++ r v ++ " )")
  (>) (C l) (C r) = C (\v => "( " ++ l v ++ " > " ++ r v ++ " )")
  (<) (C l) (C r) = C (\v => "( " ++ l v ++ " < " ++ r v ++ " )")
  (&&) (C l) (C r) = C (\v => "( " ++ l v ++ " && " ++ r v ++ " )")
  (||) (C l) (C r) = C (\v => "( " ++ l v ++ " || " ++ r v ++ " )")
  not (C c) = C (\v => "not (" ++ c v ++ " )")
  (+) (C l) (C r) = C (\v => "( " ++ l v ++ " + " ++ r v ++ " )")
  (<+>) (C l) (C r) = C (\v => "( " ++ l v ++ " + " ++ r v ++ " )")
  (*) (C l) (C r) = C (\v => "( " ++ l v ++ " * " ++ r v ++ " )")
  (<*>) (C l) (C r) = C (\v => "( " ++ l v ++ " * " ++ r v ++ " )")
  ite (C b) (C l) (C r) = C (\v => "(if " ++ b v ++ " then " ++ l v ++ " else " ++ r v ++ ")")
  it (C b) (C t) = C (\v => "(if " ++ b v ++ " then " ++ t v ++ ")")
  deref (C x) = C (\v => "!" ++ x v)
  assign (C val) (C var) = C (\v => var v ++ " := " ++ val v)
  newVar {a} (C s) f = C (\v => let x = "x" ++ show v in
                                let (C c) = f $ the (Code (VarT a)) (C (\_ => x)) in
                                "let " ++ x ++ " = ref " ++ s v ++ " in " ++ c (v + 1))
  letVal (C s) f = C (\v => let x = "x" ++ show v in
                            let (C c) = f $ C (\_ => x) in
                            "let " ++ x ++ " = " ++ s v ++ " in " ++ c (v + 1))
  index (C i) (C arr) = C (\v => arr v ++ ".[" ++ i v ++ "]")
  length (C arr) = C (\v => arr v ++ ".Length")
  while (C p) (C b) = C (\v => "(while " ++ p v ++ " do " ++ b v ++ ")")
  seq (C fs) (C sn) = C (\v => "(" ++ fs v ++ "; " ++ sn v ++ ")")
  seqs steps = foldr seq defaultof steps
  lam {a} f = C (\v => let x = "x" ++ show v in
                       let (C g) = f (C (\_ => x)) in
                       "(fun (" ++ x ++ " : " ++ show a ++ ") -> " ++ g (v + 1) ++ ")")
  app (C f) (C g) = C (\v => "(" ++ f v ++ " " ++ g v ++ ")")

compile : Code a -> String
compile code = let (C c) = code in c 0

ext: idr

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Main
import Cairo

%noinline
main : Cairo ()
main = do
    ptr <- createMemory
    writeMemory 0 42 ptr
    res <- readMemory 0 ptr
    output res

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Language.SystemVerilog.Direction

import Text.PrettyPrint.Prettyprinter

%default total

public export
data Direction = IN | INOUT | OUT

export
prettyDir : Direction
         -> Doc ()
prettyDir IN    = pretty "input"
prettyDir OUT   = pretty "output"
prettyDir INOUT = pretty "inout"

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

data Binary : Nat -> Type where
    BEnd : Binary Z
    BO : Binary n -> Binary (n + n)
    BI : Binary n -> Binary (S (n + n))

Show (Binary n) where
    show (BO x) = show x ++ "0"
    show (BI x) = show x ++ "1"
    show BEnd = ""

data Parity : Nat -> Type where
   Even : Parity (n + n)
   Odd  : Parity (S (n + n))

total
parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
    parity (S (S (j + j)))     | Even ?= Even {n=S j}
    parity (S (S (S (j + j)))) | Odd  ?= Odd {n=S j}

natToBin : (n:Nat) -> Binary n
natToBin Z = BEnd
natToBin (S k) with (parity k)
   natToBin (S (j + j))     | Even  = BI (natToBin j)
   natToBin (S (S (j + j))) | Odd  ?= BO (natToBin (S j))

intToNat : Int -> Nat
intToNat 0 = Z
intToNat x = if (x>0) then (S (intToNat (x-1))) else Z

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          print (natToBin (fromInteger (cast x)))
          putStrLn ""

---------- Proofs ----------

Main.natToBin_lemma_1 = proof
  intros
  rewrite plusSuccRightSucc j j
  rewrite sym (plusSuccRightSucc j j)
  trivial

parity_lemma_1 = proof
    intros
    rewrite sym (plusSuccRightSucc j j)
    trivial

parity_lemma_2 = proof {
    intro;
    intro;
    rewrite sym (plusSuccRightSucc j j);
    trivial;
}

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Implementation

import Data.String

data OneTwoThree a
  = One a
  | Two a a
  | Three a a a

[OTT] Functor OneTwoThree where
  map f = \case
    One x => One (f x)
    Two x y => Two (f x) (f y)
    Three x y z => Three (f x) (f y) (f z)

Show a => Show (OneTwoThree a) where
  show (One x) = "One " ++ show x
  show (Two x y) = unwords ["Two", show x, show y]
  show (Three x y z) = unwords ["Three", show x, show y, show z]

Eq a => Eq (OneTwoThree a) where
  One a == One x = a == x
  Two a b == Two x y = a == x && b == y
  Three a b c == Three x y z = a == x && b == y && c == z
  _ == _ = False


text:
test : String
test = "IDR"


text:
module Effekt.IteratedUnstaged

import Effekt.CpsUnstaged

public export
Stm : List Type -> Type -> Type
Stm [] a = a
Stm (r :: rs) a = Cps (Stm rs r) a

pure : a -> Stm rs a
pure{  rs= []}         a = a
pure{  rs= r :: rs}  a = \k => k a

push : (a -> Stm (r :: rs) b) -> (b -> Stm rs r) -> (a -> Stm rs r)
push f k = \a => f a k

bind : Stm rs a -> (a -> Stm rs b) -> Stm rs b
bind{  rs= []}         m f = f m
bind{  rs= r :: rs}  m f = \k => m (push f k)

(>>=) : Stm rs a -> (a -> Stm rs b) -> Stm rs b
(>>=) = bind

lift : Stm rs a -> Stm (r :: rs) a
lift = bind

shift0 : ((a -> Stm rs r) -> Stm rs r) -> Stm (r :: rs) a
shift0 = id

runIn0 : Stm (r :: rs) a -> (a -> Stm rs r) -> Stm rs r
runIn0 = id

reset0 : Stm (a :: rs) a -> Stm rs a
reset0 m = runIn0 m pure

shift00 : ((a -> Stm rs r) -> Stm rs r) -> Stm (r :: rs) a
shift00 k = shift0 k

shift01 : ((a -> Stm rs r) -> Stm rs r) -> Stm (q :: r :: rs) a
shift01 {r} {rs} k = lift {rs = r::rs} (shift0 {r} {rs} k)

shift02 : ((a -> Stm rs r) -> Stm rs r) -> Stm (p :: q :: r :: rs) a
shift02 {q} {r} {rs} k = lift {rs = q::r::rs} (lift {rs = r::rs} (shift0 {r} {rs} k))

reset01 : Stm (a :: a :: rs) a -> Stm rs a
reset01 {a} {rs} m = reset0 (reset0 {rs=(a :: rs)} m)

shift : ((a -> Stm (r :: rs) r) -> Stm (r :: rs) r) -> Stm (r :: rs) a
shift {r} {rs} body = shift0 (\k => reset0 (body (\a => lift {r} {rs} (k a))))

emit : Int -> Stm (List Int :: rs) ()
emit {rs} a = shift0 {rs} (\c =>
  bind {rs} (c ()) (\as =>
  pure {rs} (the (Int -> List Int -> List Int) (::) a as)))

partition : Int -> List Int -> Stm [List Int, List Int] ()
partition a l = case l of
  [] => do
    pure {rs=[List Int,List Int]} ()
  (h :: t) => if (a < h)
    then (
      bind {rs=[List Int,List Int]} (emit {rs=[List Int]} h) (\u =>
      partition a t))
    else (
      bind {rs=[List Int,List Int]} (lift {rs=[List Int]} (emit {rs=[]} h)) (\u =>
      partition a t))

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
module SQLiteTypes

import Decidable.Equality

%default total

public export data SQLiteType = TEXT | INTEGER | REAL
                | NULLABLE SQLiteType

public export interpSql : SQLiteType -> Type
interpSql TEXT = String
interpSql INTEGER = Integer
interpSql REAL = Double
interpSql (NULLABLE x) = Maybe (interpSql x)

equalSql : (t : SQLiteType) -> (x, y : interpSql t) -> Bool
equalSql TEXT x y = x == y
equalSql INTEGER x y = x == y
equalSql REAL x y = x == y
equalSql (NULLABLE ty) (Just x) (Just y) = equalSql ty x y
equalSql (NULLABLE ty) Nothing Nothing = True
equalSql (NULLABLE ty) _ _ = False

export showSql : (t : SQLiteType) -> (x : interpSql t) -> String
showSql TEXT x = show x
showSql INTEGER x = show x
showSql REAL x = show x
showSql (NULLABLE ty) (Just x) = showSql ty x
showSql (NULLABLE ty) Nothing = "null"

integerNotText : INTEGER = TEXT -> Void
integerNotText Refl impossible

realNotText : REAL = TEXT -> Void
realNotText Refl impossible

nullableNotText : NULLABLE t = TEXT -> Void
nullableNotText Refl impossible

realNotInteger : REAL = INTEGER -> Void
realNotInteger Refl impossible

nullableNotInteger : NULLABLE t = INTEGER -> Void
nullableNotInteger Refl impossible

nullableNotReal : NULLABLE t = REAL -> Void
nullableNotReal Refl impossible

export implementation DecEq SQLiteType where
  decEq TEXT TEXT            = Yes Refl
  decEq INTEGER TEXT         = No integerNotText
  decEq REAL TEXT            = No realNotText
  decEq (NULLABLE x) TEXT    = No nullableNotText
  decEq TEXT INTEGER         = No $ integerNotText . sym
  decEq INTEGER INTEGER      = Yes Refl
  decEq REAL INTEGER         = No realNotInteger
  decEq (NULLABLE x) INTEGER = No nullableNotInteger
  decEq TEXT REAL            = No $ realNotText . sym
  decEq INTEGER REAL         = No $ realNotInteger . sym
  decEq REAL REAL            = Yes Refl
  decEq (NULLABLE x) REAL    = No nullableNotReal
  decEq TEXT (NULLABLE x)    = No $ nullableNotText . sym
  decEq INTEGER (NULLABLE x) = No $ nullableNotInteger . sym
  decEq REAL (NULLABLE x)    = No $ nullableNotReal . sym
  decEq (NULLABLE y) (NULLABLE x) with (decEq y x)
    decEq (NULLABLE x) (NULLABLE x) | (Yes Refl) = Yes Refl
    decEq (NULLABLE y) (NULLABLE x) | (No prf) = No $ prf . inside
      where inside : NULLABLE a = NULLABLE b -> a = b
            inside Refl = Refl

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
{-
  1. Input: Vect n elem
     Output: Vect n elem
     Operations: Cloning the Vect, replacing the elements of the Vect with random elements.

     Input: Vect n elem
     Output: Vect (n * 2) elem
     Operations: Append a Vect with itself, inserting `n` random elements into the Vect.

     Input: Vect (1 + n) elem
     Output: Vect n elem
     Operations: Popping an element from any position in the Vect.

     Input: Bounded n, Vect n elem
     Output: elem
     Operations: Retrieving the element at index `Bounded n` in the Vect.

-}

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:
||| Universal clock - Ported from Haskell time package.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Time.Clock

import Data.Fixed
import Data.Rational

import public Data.Time.Clock.DiffTime
import public Data.Time.Clock.UTCTime
import Data.Time.Calendar

import Generics.Derive

%default total
%language ElabReflection

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

public export
record UniversalTime where
  constructor ModJulianDate
  modJulianDate : Rational
%runElab derive "UniversalTime" [Generic, Eq, Ord, DecEq]

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


text:
import Data.Vect
import Data.Nat

my_filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
my_filter p [] = ( _ ** [] )
my_filter p (x :: xs) with (filter p xs)
  my_filter p (x :: xs) | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

foo : Int -> Int -> Bool
foo n m with (n + 1)
  foo _ m | 2 with (m + 1)
    foo _ _ | 2 | 3 = True
    foo _ _ | 2 | _ = False
  foo _ _ | _ = False

data Parity : Nat -> Type where
     Even : {n : _} -> Parity (n + n)
     Odd  : {n : _} ->Parity (S (n + n))

-- parity : (n : Nat) -> Parity n
-- parity Z = Even {n = Z}
-- parity (S Z) = Odd {n = Z}
-- parity (S (S k)) with (parity k)
--   parity (S (S (j + j))) | Even
--       = rewrite plusSuccRightSucc j j in Even {n = S j}
--   parity (S (S (S (j + j)))) | Odd
--       = rewrite plusSuccRightSucc j j in Odd {n = S j}

helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p

helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p

parity : (n:Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
   natToBin (j + j)     | Even = False :: natToBin j
   natToBin (S (j + j)) | Odd  = True  :: natToBin j


text:
module Language.LSP.Message.Window

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace MessageType
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
  public export
  data MessageType = Error | Warning | Info | Log

export
ToJSON MessageType where
  toJSON Error   = JNumber 1
  toJSON Warning = JNumber 2
  toJSON Info    = JNumber 3
  toJSON Log     = JNumber 4

export
FromJSON MessageType where
  fromJSON (JNumber 1) = pure Error
  fromJSON (JNumber 2) = pure Warning
  fromJSON (JNumber 3) = pure Info
  fromJSON (JNumber 4) = pure Log
  fromJSON _ = Nothing

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
public export
record ShowMessageParams where
  constructor MkShowMessageParams
  type    : MessageType
  message : String
%runElab deriveJSON defaultOpts `{ShowMessageParams}

namespace ShowMessageRequestClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
  public export
  record ShowMessageActionItem where
    constructor MkShowMessageActionItem
    additionalPropertiesSupport : Maybe Bool
  %runElab deriveJSON defaultOpts `{ShowMessageActionItem}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
public export
record ShowMessageRequestClientCapabilities where
  constructor MkShowMessageRequestClientCapabilities
  messageActionItem : Maybe ShowMessageActionItem
%runElab deriveJSON defaultOpts `{ShowMessageRequestClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
public export
record MessageActionItem where
  constructor MkMessageActionItem
  title : String
%runElab deriveJSON defaultOpts `{MessageActionItem}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showMessage
public export
record ShowMessageRequestParams where
  constructor MkShowMessageRequestParams
  type    : MessageType
  message : String
  actions : Maybe (List MessageActionItem)
%runElab deriveJSON defaultOpts `{ShowMessageRequestParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
public export
record ShowDocumentClientCapabilities where
  constructor MkShowDocumentClientCapabilities
  support : Bool
%runElab deriveJSON defaultOpts `{ShowDocumentClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
public export
record ShowDocumentParams where
  constructor MkShowDocumentParams
  uri       : URI
  external_ : Maybe Bool
  takeFocus : Maybe Bool
  selection : Maybe Range
%runElab deriveJSON ({renames := [("external_", "external")]} defaultOpts) `{ShowDocumentParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_showDocument
public export
record ShowDocumentResult where
  constructor MkShowDocumentResult
  success : Bool
%runElab deriveJSON defaultOpts `{ShowDocumentResult}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_logMessage
public export
record LogMessageParams where
  constructor MkLogMessageParams
  type    : MessageType
  message : String
%runElab deriveJSON defaultOpts `{LogMessageParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_create
public export
record WorkDoneProgressCreateParams where
  constructor MkWorkDoneProgressCreateParams
  token : ProgressToken
%runElab deriveJSON defaultOpts `{WorkDoneProgressCreateParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#window_workDoneProgress_cancel
public export
record WorkDoneProgressCancelParams where
  constructor MkWorkDoneProgressCancelParams
  token : ProgressToken
%runElab deriveJSON defaultOpts `{WorkDoneProgressCancelParams}


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

module API.Web.XHR.XMLHttpRequestEventTarget

import API.Web.XHR.XMLHttpRequest

%access public export
%default total

data XMLHttpRequestEventTarget : Type where
  FromXMLHttpRequest : XMLHttpRequest -> XMLHttpRequestEventTarget

max_stars_repo_name: blau-io/idris-xhr

max_issues_repo_name: blau-io/idris-xhr

max_forks_repo_name: blau-io/idris-xhr


text:
module Data.Queue

import Data.Vect
import Data.VectRankedElem
import Decidable.Order

%default total

export
data Queue : (size : Nat) -> (ty : Type) -> Type where
  MkQueue : {n : Nat}
         -> (f : Vect n ty)
         -> {m : Nat}
         -> (r : Vect m ty)
         -> .{auto invariant : LTE m n}
         -> Queue (n + m) ty

queues : {ty : Type} -> Queue _ ty -> ((size1 : Nat ** Vect size1 ty),
                                       (size2 : Nat ** Vect size2 ty))
queues (MkQueue {n} f {m} r) = ((n ** f), (m ** r))

export
data RankedElem : ty -> Queue size ty -> (idx : Nat) -> Type where
  FrontElem : {q : Queue size ty}
           -> {idx : Nat}
           -> RankedElem x (snd $ fst $ queues q) idx
           -> RankedElem x q idx
  BackElem : {q : Queue size ty}
          -> {idx : Nat}
          -> RankedElem x (snd $ snd $ queues q) idx
          -> RankedElem x q (size `minus` S idx)

export
empty : Queue Z _
empty = MkQueue [] []

lteAddRightLemma : LTE r c -> LTE r (l + c)
lteAddRightLemma {l} {r} {c} smaller
  = lteTransitive smaller cLTElc
    where cLTElc : LTE c (l + c)
          cLTElc = rewrite plusCommutative l c in
                   lteAddRight {m = l} c

minusPlusEqualsPlusMinus : (l, c, r: Nat) -> LTE r c -> LTE r (l + c) -> (l + c) - r = l + (c - r)
minusPlusEqualsPlusMinus Z _ _ _ _ = Refl
minusPlusEqualsPlusMinus (S _) Z Z _ _ = Refl
minusPlusEqualsPlusMinus (S _) (S _) Z _ _ = Refl
minusPlusEqualsPlusMinus _ Z (S _) _ _ impossible
minusPlusEqualsPlusMinus l (S c) (S r) smaller _
  = let smaller' = fromLteSucc smaller in
    rewrite sym $ plusSuccRightSucc l c in
    minusPlusEqualsPlusMinus l c r smaller' (lteAddRightLemma smaller')

make_ : {n : Nat}
     -> (f : Vect n ty)
     -> {m : Nat}
     -> (r : Vect m ty)
     -> (ret : Queue (n + m) ty
         ** ({x : ty} -> {idx : Nat} -> RankedElem x f idx -> RankedElem x ret idx,
             {x : ty} -> {idx : Nat} -> RankedElem x r idx -> RankedElem x ret (n + m `minus` S idx)))
make_ {n} f {m} r with (order {to = LTE} m n)
  | Left _ = (MkQueue f r ** (FrontElem, BackElem))
  | Right _ = let (reversed ** rProj) = rev_ r
                  (f' ** (fProj, reversedProj)) = f `concat_` reversed in
              rewrite sym $ plusZeroRightNeutral (n + m) in
              (MkQueue f' [] ** (FrontElem . fProj,
                                 rewrite plusZeroRightNeutral (n + m) in
                                 FrontElem . (proj $ reversedProj . rProj)))
              where proj : {f' : Vect (n + m) ty}
                        -> (trans : {x : ty} -> {idx : Nat} -> RankedElem x r idx -> RankedElem x f' (n + (m `minus` S idx)))
                        -> {x : ty} -> {idx' : Nat} -> RankedElem x r idx'
                        -> RankedElem x f' (n + m `minus` S idx')
                    proj {f'} trans {idx'} elem = let smaller = indexSmallerThanSize elem
                                                      elem' = trans elem in
                                                  rewrite assert_total $
                                                          minusPlusEqualsPlusMinus n m (S idx') smaller (lteAddRightLemma smaller) in
                                                  elem'

export
snoc_ : (q : Queue size ty) -> (x : ty)
     -> (ret : Queue (S size) ty
         ** ({x : ty} -> {idx : Nat} -> RankedElem x q idx -> RankedElem x ret idx,
             RankedElem x ret size))
snoc_ (MkQueue {n} f {m} r) x = rewrite plusSuccRightSucc n m in
                                let (ret ** (fProj, rProj)) = make_ f (x::r) in
                                (ret ** ((\el => case el of
                                                 (FrontElem el) => fProj el
                                                 (BackElem el {idx}) => rewrite sym $ lemma n m (S idx) in
                                                                        rProj $ There el),
                                         rewrite sym $ minusZeroRight (n + m) in
                                         rewrite sym $ lemma n m Z in
                                         rProj Here))
                                where lemma : (l, c, r : Nat) -> l + S c `minus` S r = l + c `minus` r
                                      lemma Z Z _ = Refl
                                      lemma Z (S _) _ = Refl
                                      lemma (S l) c r = rewrite plusSuccRightSucc l c in Refl

export
snoc : Queue size ty -> ty -> Queue (S size) ty
snoc q x = fst $ snoc_ q x

export
head_ : (q : Queue (S _) ty) -> (x : ty ** RankedElem x q Z)
head_ (MkQueue (x :: xs) ys) = (x ** FrontElem Here)

export
head : Queue (S _) ty -> ty
head q = fst $ head_ q

export
tail_ : (q : Queue (S size) ty)
     -> (ret : Queue size ty
         ** {x : ty} -> {idx : Nat} -> RankedElem x q (S idx) -> RankedElem x ret idx)
tail_ (MkQueue (_::fs) r)
  = let (ret ** (fProj, rProj)) = make_ fs r in
    (ret ** \el =>
      case toPattern el of
      (Z ** (_, Refl)) impossible
      (S _ ** (FrontElem (There x), Refl)) => fProj x
      (_ ** (BackElem x, prf)) => rewrite toMinusSuccPredEq prf in rProj x)
    where toPattern : {q : Queue (S _) ty}
                   -> {i : Nat}
                   -> RankedElem x q (S i)
                   -> (i' ** (RankedElem x q i', S i = i'))
          toPattern {i} el = (S i ** (el, Refl))
          toMinusSuccPredEq : S c = x + y `minus` z -> c = x + y `minus` S z
          toMinusSuccPredEq {x} {y} {z} prf = rewrite minusSuccPred (x + y) z in cong {f = Nat.pred} prf

export
tail : Queue (S size) ty -> Queue size ty
tail q = fst $ tail_ q

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
module Data.Time.Calendar.MonthDay

import Data.Vect
import Data.Fin
import public Data.Time.Calendar.Types

%default total

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

export monthLengths : Bool -> Vect 12 DayOfMonth
monthLengths isleap = [
  31, (if isleap then 29 else 28), 31, 30, 31, 30, 31, 31, 30, 31, 30, 31 ]

 -- | The length of a given month in the Gregorian or Julian calendars.
 -- First arg is leap year flag.
export monthLength : Bool -> MonthOfYear -> DayOfMonth
monthLength isLeap month = index (restrict 11 $ cast $ month - 1) $ monthLengths isLeap

||| Convert month and day in the Gregorian or Julian calendars to day of year.
||| First arg is leap year flag.
export monthAndDayToDayOfYear : Bool -> MonthOfYear -> DayOfMonth -> DayOfYear
monthAndDayToDayOfYear isLeap month day =
  let m' = if month < 1 then 1 else if month > 12 then 12 else month
      ml = monthLength isLeap m'
      d' = if day < 1 then 1 else if day > ml then ml else day
      k = if m' <= 2 then 0 else if isLeap then -1 else -2
   in ((367 * m' - 362) `div` 12) + cast k + d'

||| Convert month and day in the Gregorian or Julian calendars to day of year.
-- First arg is leap year flag.
export monthAndDayToDayOfYearValid : Bool -> MonthOfYear -> DayOfMonth -> Maybe DayOfYear
monthAndDayToDayOfYearValid isLeap month day =
  if month < 1 || month > 12
    then Nothing
    else
      let ml = monthLength isLeap month
          k = if month < 2 then 0 else if isLeap then -1 else -2
       in if day < 1 || day > ml
             then Nothing
             else Just $ ((367 * month - 362) `div` 12) + cast k + day

findMonthDay : Int -> Vect _ DayOfMonth -> Int -> (Int, Int)
findMonthDay m (n::ns) yd =
  if yd > n then findMonthDay (m + 1) ns (yd - n)
            else (m, yd)
findMonthDay m [] yd = (m, yd)

||| Convert day of year in the Gregorian or Julian calendars to month and day.
||| First arg is leap year flag.
export dayOfYearToMonthAndDay : Bool -> DayOfYear -> (MonthOfYear, DayOfMonth)
dayOfYearToMonthAndDay isLeap yd =
 let yl = the Int $ if isLeap then 366 else 365
  in findMonthDay 1
                  (monthLengths isLeap)
                  (if yd < 1 then 1 else if yd > yl then yl else yd)

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


text:
import Language.Reflection

%language ElabReflection

mkDecls : TTImp -> Elab ()
mkDecls v
    = declare `[ mkMult : Int -> Int
                 mkMult x = x * ~(v) ]

%runElab mkDecls `(94)

bad : a
bad = %runElab mkDecls `(94)


text:
module lib.Library

export
salute : String
salute = "Hello, library example of idris"


text:
module Inigo.Async.Compress.Brotli

import Data.Buffer
import Extra.Buffer
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Async.Util

-- Compresses a String using Brotli, returning a Buffer
%foreign (promisifyPrim "(datum)=>{return require('util').promisify(require('zlib').brotliCompress)(datum)}")
brotli_compress__prim : Buffer -> promise Buffer

-- Decompresses a buffer encoded in Brotli, returning the original data
%foreign (promisifyPrim "(buf)=>require('util').promisify(require('zlib').brotliDecompress)(buf)")
brotli_decompress__prim : Buffer -> promise Buffer

export
compress: Buffer -> Promise Buffer
compress datum =
  promisify (brotli_compress__prim datum)

export
decompress: Buffer -> Promise Buffer
decompress buf =
  promisify (brotli_decompress__prim buf)

export
compressFile : String -> Promise Buffer
compressFile path =
  do
    contents <- fs_readFileBuf path
    compress contents

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
||| Creating an adventure game
||| Ported from https://www.linuxjournal.com/content/creating-adventure-game-terminal-ncurses

module Adventure

import Data.Nat
import NCurses

%default covering

-- Define symbols for the map
grass    = ' '
empty    = '.'
water    = '~'
mountain = '^'
player   = '*'

isMoveOkay : Position -> NCurses i i Bool
isMoveOkay pos = do c <- mvInCh pos
                    pure (c == grass || c == empty)

CFG = MkConfig False True False

exploring : Size -> Position -> NCurses CFG CFG ()
exploring sz pos@(MkPosition { row, col }) = NCurses.do
  -- display player at position
  mvAddCh pos player
  move pos
  refresh
  -- wait for an input to move
  Left c <- getCh
    | Right 'q' => pure () -- quitting
    | Right _ => exploring sz pos -- invalid input
  case c of
    Up    => do let pos' = up pos
                ok <- isMoveOkay pos'
                when ok $ mvAddCh pos empty
                exploring sz (ifThenElse ok pos' pos)
    Down  => do let pos' = down pos
                let True = pos'.row < pred sz.height
                  | _ => exploring sz pos
                ok <- isMoveOkay pos'
                when ok $ mvAddCh pos empty
                exploring sz (ifThenElse ok pos' pos)
    Left  => do let pos' = left pos
                ok <- isMoveOkay pos'
                when ok $ mvAddCh pos empty
                exploring sz (ifThenElse ok pos' pos)
    Right => do let pos' = right pos
                let True = pos'.col < pred sz.width
                  | _ => exploring sz pos
                ok <- isMoveOkay pos'
                when ok $ mvAddCh pos empty
                exploring sz (ifThenElse ok pos' pos)
    _ => exploring sz pos -- invalid input

main : IO ()
main = runNCurses $ NCurses.do
  -- Initialise curses
  cBreak
  noEcho
  clear
  keypad True

  -- Grab size
  size <- getSize

  -- Draw map
  -- background
  for_ @{NCURSES} [0..size.height] $ \ row =>
    mvHLine (MkRow row) grass size.width

  -- mountain
  for_ @{NCURSES} [half size.width .. threequarter size.width] $ \ col =>
    mvVLine (MkPosition { row = 0, col }) mountain size.height

  -- mountain path
  mvHLine (MkRow $ quarter size.height) grass size.width

  -- lake
  for_ @{NCURSES} [1..half size.height] $ \ row =>
    mvHLine (MkPosition { row, col = 1 }) water (third size.width)

  -- wait for the user quitting
  exploring size (MkRow $ pred size.height)

  where

    quarter : Nat -> Nat
    quarter n = (n `divNatNZ` 4) %search

    third : Nat -> Nat
    third n = (n `divNatNZ` 3) %search

    half : Nat -> Nat
    half n = (n `divNatNZ` 2) %search

    threequarter : Nat -> Nat
    threequarter n = (3 * n `divNatNZ` 4) %search

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module Core.Variable

import Gen.Common

--              0   0  o8o  8YYYo Y8Y  o8o  8888. 0    8YYYY
-- ____ ____    0   0 8   8 8___P  0  8   8 8___Y 0    8___
-- """" """"    "o o" 8YYY8 8""Yo  0  8YYY8 8"""o 0    8"""
--               "8"  0   0 0   0 o8o 0   0 8ooo" 8ooo 8oooo

public export
data Variable = Name String | Generated String Int

export
implementation Interfaces.Eq Variable where
	(Name x) == (Name y)               = x == y
	(Generated _ i) == (Generated _ j) = i == j
	_ == _                             = False

export
implementation Show Variable where
	show (Name x) = x
	show (Generated x _) = x

-- 8YYYY 0   0 0    0    8o  0  o8o  8_   _8 8YYYY
-- 8___  0   0 0    0    8Yo 8 8   8 8"o_o"8 8___
-- 8"""  0   0 0    0    8 Yo8 8YYY8 0  8  0 8"""
-- 0     "ooo" 8ooo 8ooo 0   8 0   0 0     0 8oooo

public export
FullName : Type
FullName = Pair String String

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Data.OrderedSet

import public Data.DistinctElements

%access public export
%default total

data OrderedSet : Nat -> Type -> Type where
    FromVect : (xs : Vect n a) -> {auto p : DistinctElements xs} -> OrderedSet n a

Elem : a -> OrderedSet n a -> Type
Elem x (FromVect xs) = Elem x xs

Nil : OrderedSet Z a
Nil = FromVect []

(::) : (x : a) -> (xs : OrderedSet n a) -> {default absurd p : Not (Elem x xs)} -> OrderedSet (S n) a
(::) x (FromVect xs {p = ps}) {p = p} = FromVect (x::xs) {p = (p,ps)}

tail : OrderedSet (S n) a -> OrderedSet n a
tail (FromVect (_ :: xs) {p = (_, ps)}) = FromVect xs

isElem : DecEq a => (x : a) -> (xs : OrderedSet n a) -> Dec (Elem x xs)
isElem x (FromVect xs) = isElem x xs

toVect : OrderedSet n a -> Vect n a
toVect (FromVect xs) = xs

map : {f : a -> b} -> Injective f -> OrderedSet n a -> OrderedSet n b
map inj (FromVect xs {p}) {f} = FromVect (map f xs) {p = mapInjectiveFunction inj p}


text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#function-types
module WebAssembly.Validation.Types.FunctionTypes

import WebAssembly.Structure

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

public export
data ValidFunctionType : (funcType : FuncType) -> Type where
  MkValidFunctionType : (funcType : FuncType) -> ValidFunctionType funcType

-------------------------------------------------------------------------------
-- Decidablity of Validation
-------------------------------------------------------------------------------

total public export
isFunctionTypeValid : (funcType : FuncType) -> Dec (ValidFunctionType funcType)
isFunctionTypeValid funcType = Yes (MkValidFunctionType funcType)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Accumulate

export
accumulate : (Int -> Int) -> List Int -> List Int
accumulate f xs = ?accumulate_rhs


text:
module Network.HTTP.Client

import Network.HTTP.Pool.ConnectionPool
import Network.HTTP.Scheduler
import Network.HTTP.Protocol
import Network.HTTP.Message
import Network.HTTP.Error
import Network.HTTP.Header
import Network.HTTP.Method
import Network.HTTP.URL
import Network.HTTP.Path
import Network.HTTP.Status
import Network.HTTP.Cookie
import Network.TLS
import Network.TLS.Certificate.System
import Network.TLS.Signature
import Utils.Streaming
import Utils.String
import Utils.Bytes
import Control.Monad.Error.Either
import Control.Monad.Error.Interface
import Control.Monad.Trans
import Data.String
import Data.String.Extra
import Data.Nat
import Data.IORef
import Decidable.Equality

public export
record HttpClient e where
  constructor MkHttpClient
  cookie_jar : IORef CookieJar
  store_cookie : Bool
  follow_redirect : Bool
  pool_manager : PoolManager e

||| Close all existing connections in the HTTP client.
||| A closed client can be reused again.
export
close : {e : _} -> HasIO io => HttpClient e -> io ()
close client = liftIO $ evict_all {m=IO,e=e} $ client.pool_manager

||| Creates a new HTTP client.
||| Arguments:
|||
||| @ cert_checker the function used to verify the website's TLS certificate.
|||                `certificate_check` and `certificate_ignore_check` are provided in `Network.TLS`.
||| @ max_total_connection the maximum alive connections (per protocol) allowed
||| @ max_per_site_connection the maximum alive connections (per protocol) per site allowed
||| @ store_cookie whether the client should store received cookies
||| @ follow_redirect whether the client should follow redirects according to response status codes
export
new_client : HasIO io => (String -> CertificateCheck IO) ->
             (max_total_connection : Nat) -> {auto 0 n01 : NonZero max_total_connection} ->
             (max_per_site_connection: Nat) -> {auto 0 no2 : NonZero max_per_site_connection} ->
             {auto 0 lte : LTE max_per_site_connection max_total_connection} ->
             Bool -> Bool -> io (HttpClient e)
new_client cert_checker max_total_connection max_per_site_connection store_cookie follow_redirect = do
  manager <- new_pool_manager max_per_site_connection max_total_connection cert_checker
  jar <- newIORef $ MkCookieJar []
  pure $ MkHttpClient jar store_cookie follow_redirect manager

||| Create a new HTTP client with default configuration.
||| This would also verify the website's TLS certificate with the system's trusted CAs.
||| max_total_connection = 25
||| max_per_site_connection = 5
||| store_cookie = True
||| follow_redirect = True
export
new_client_default : HasIO io => io (HttpClient e)
new_client_default = do
  Right certs <- liftIO get_system_trusted_certs
  | Left err => assert_total $ idris_crash "error when trying to get system certificats, please report this issue."
  new_client (certificate_check certs) 25 5 True True

replace : Eq a => List (a, b) -> List (a, b) -> List (a, b)
replace original [] = original
replace original ((k, v) :: xs) = replace (loop [] original k v) xs where
  loop : List (a, b) -> List (a, b) -> a -> b -> List (a, b)
  loop acc [] k v = acc
  loop acc ((k', v') :: xs) k v = if k' == k then (k, v) :: (acc <+> xs) else loop ((k', v') :: acc) xs k v

add_if_not_exist : Eq a => (a, b) -> List (a, b) -> List (a, b)
add_if_not_exist (k, v) headers = if any (\(k', v') => k' == k) headers then headers else (k, v) :: headers

unwrap : Functor f => Stream f (EitherT e IO) a -> Stream f IO (Either e a)
unwrap = fold (Return . Right) (go . runEitherT) (\x => Step x) where
  go : IO (Either e (Stream f IO (Either e a))) -> ?
  go stream = case !(lift stream) of
    Left err => Return (Left err)
    Right stream => stream

wrap : (Functor f, MonadError e m) => HasIO m => Stream f IO (Either e ()) -> Stream f m ()
wrap = fold (\case Right a => Return a; Left a => Effect $ throwError a) (Effect . delay . liftIO) (\x => Step x)

||| Send a HTTP request, returns a `HttpResponse` containing the status code and headers,
||| and also a stream of the content body from the response.
||| Arguments:
|||
||| @ client the HTTP client
||| @ method the HTTP method, e.g. GET / POST
||| @ url the URL to of the website to be connected to
||| @ headers the HTTP headers, represented as a list of (key, value)
||| @ length the length of the content to be sent
||| @ input the stream of bytes to be sent, which should be at least `length` bytes
export
request' : {e,m : _} -> MonadError (HttpError e) m => HasIO m => HttpClient e -> Method -> URL -> List (String, String)
  -> (length: Nat)
  -> (input : Stream (Of Bits8) (EitherT e IO) ())
  -> m (HttpResponse, Stream (Of Bits8) m ())
request' client method url headers payload_size payload = do
  let Just protocol = protocol_from_str url.protocol
  | Nothing => throwError (UnknownProtocol url.protocol)

  cookies_jar <- liftIO $ readIORef client.cookie_jar

  let headers_with_missing_info =
        add_if_not_exist ("Host", hostname_string url.host) .
        add_if_not_exist ("User-Agent", "idris2-http") .
        add_if_not_exist ("Content-Length", show payload_size) .
        add_if_not_exist ("Cookie", join "; " $ map serialize_cookie_no_attr cookies_jar.cookies) $ headers

  let message = MkRawHttpMessage method (show url.path <+> url.extensions) headers_with_missing_info
  Right (response, content) <- liftIO $ start_request {m=IO} client.pool_manager protocol message (unwrap payload)
  | Left err => throwError err

  when client.store_cookie $ do
    let cookies = lookup_headers response.headers SetCookie
    liftIO $ modifyIORef client.cookie_jar (\og => foldl add_cookie og cookies)

  if (client.follow_redirect && (Redirection == status_code_class response.status_code.snd))
    then do
      let Just location = lookup_header response.headers Location
      | Nothing => throwError (MissingHeader "Location")

      -- discard responded content to make way for another request
      liftIO $ consume content
      request' client method (add url location) headers payload_size payload
    else
      pure $ map wrap (response, content)

public export
interface Bytestream (a : Type) where
  to_stream : Monad m => a -> (Nat, Stream (Of Bits8) m ())

export
Bytestream () where
  to_stream () = (0, pure ())

export
Bytestream (List Bits8) where
  to_stream list = (length list, fromList_ list)

export
Bytestream String where
  to_stream = to_stream . utf8_unpack

||| Send a HTTP request, returns a `HttpResponse` containing the status code and headers,
||| and also a stream of the content body from the response.
||| Arguments:
|||
||| @ client the HTTP client
||| @ method the HTTP method, e.g. GET / POST
||| @ url the URL to of the website to be connected to
||| @ headers the HTTP headers, represented as a list of (key, value)
||| @ payload the content payload of the request. Use () for empty content.
export
request : {e,m,a : _} -> MonadError (HttpError e) m => HasIO m => Bytestream a =>
          HttpClient e -> Method -> URL -> List (String, String) ->
          a ->
          m (HttpResponse, Stream (Of Bits8) m ())
request client method url headers payload =
  let (len, stream) = to_stream {m=EitherT e IO} payload
  in request' client method url headers len stream


text:
module Language.LSP.Message.Command

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Progress
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#command
public export
record Command where
  constructor MkCommand
  title     : String
  command   : String
  arguments : Maybe (List JSON)
%runElab deriveJSON defaultOpts `{{Command}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
public export
record ExecuteCommandClientCapabilities where
  constructor MkExecuteCommandClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{ExecuteCommandClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
public export
record ExecuteCommandOptions where
  constructor MkExecuteCommandOptions
  workDoneProgress : Maybe Bool
  commands         : List String
%runElab deriveJSON defaultOpts `{{ExecuteCommandOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
public export
record ExecuteCommandRegistrationOptions where
  constructor MkExecuteCommandRegistrationOptions
  workDoneProgress : Maybe Bool
  commands         : List String
%runElab deriveJSON defaultOpts `{{ExecuteCommandRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workspace_executeCommand
public export
record ExecuteCommandParams where
  constructor MkExecuteCommandParams
  partialResultToken : Maybe ProgressToken
  command            : String
  arguments          : Maybe (List JSON)
%runElab deriveJSON defaultOpts `{{ExecuteCommandParams}}


text:
module Language.LSP.CodeAction.ExprSearch

import Core.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.String
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Resugar
import Language.JSON
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Utils
import TTImp.TTImp
import TTImp.Interactive.ExprSearch

dropLams : Nat -> RawImp -> RawImp
dropLams Z tm = tm
dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
dropLams _ tm = tm

dropLamsTm : {vars : _} -> Nat -> Env Term vars -> Term vars -> (vars' ** (Env Term vars', Term vars'))
dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))

nextProofSearch : Ref Ctxt Defs
               => Ref UST UState
               => Ref ROpts REPLOpts
               => Core (Maybe (Name, RawImp))
nextProofSearch = do
  opts <- get ROpts
  let Just (n, res) = psResult opts
    | Nothing => pure Nothing
  Just (res, next) <- nextResult res
    | Nothing => do put ROpts (record { psResult = Nothing } opts)
                    pure Nothing
  put ROpts (record { psResult = Just (n, next) } opts)
  pure (Just (n, res))

fueledRepeat : Nat -> List a -> Core (Maybe a) -> Core (List a)
fueledRepeat Z acc f = pure (reverse acc)
fueledRepeat (S k) acc f = do Just res <- f
                                | Nothing => pure (reverse acc)
                              fueledRepeat k (res :: acc) f

buildCodeAction : Name -> URI -> Range -> String -> CodeAction
buildCodeAction name uri range str =
  let textEdit = MkTextEdit range str
      workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                      , documentChanges   = Nothing
                                      , changeAnnotations = Nothing
                                      }
   in MkCodeAction { title       = "Expression search on \{show name}"
                   , kind        = Just (Other "refactor.rewrite.auto")
                   , diagnostics = Just []
                   , isPreferred = Just False
                   , disabled    = Nothing
                   , edit        = Just workspaceEdit
                   , command     = Nothing
                   , data_       = Nothing
                   }
export
exprSearch : Ref LSPConf LSPConfiguration
          => Ref MD Metadata
          => Ref Ctxt Defs
          => Ref UST UState
          => Ref Syn SyntaxInfo
          => Ref ROpts REPLOpts
          => CodeActionParams -> Core (List CodeAction)
exprSearch params = do
  let True = params.range.start.line == params.range.end.line
    | _ => pure []

  fuel <- gets LSPConf searchLimit
  nameLocs <- gets MD nameLocMap
  let line = params.range.start.line
  let col = params.range.start.character
  let Just ((_, nstart, nend), name) = findInTreeLoc (line, col) nameLocs
    | Nothing => pure []

  context <- gets Ctxt gamma
  toBeBracketed <- gets Syn bracketholes
  let toBrack = elemBy (\x, y => dropNS x == dropNS y) name toBeBracketed
  solutions <- case !(lookupDefName name context) of
                    [(n, nidx, Hole locs _)] => do
                      let searchtm = exprSearch replFC name []
                      ropts <- get ROpts
                      put ROpts (record { psResult = Just (name, searchtm) } ropts)
                      fueledRepeat fuel [] (do Just (_, restm) <- nextProofSearch
                                                 | Nothing => pure Nothing
                                               let tm' = dropLams locs restm
                                               itm <- pterm tm'
                                               let itm' : PTerm = if toBrack then addBracket replFC itm else itm
                                               pure $ Just (show itm'))
                    [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] => case holeInfo pi of
                      NotHole => pure []
                      SolvedHole locs => do
                        let (_ ** (env, tm')) = dropLamsTm locs [] tm
                        itm <- resugar env tm'
                        let itm' : PTerm = if toBrack then addBracket replFC itm else itm
                        pure [show itm']
                    _ => pure []

  let range = MkRange (uncurry MkPosition nstart) (uncurry MkPosition nend)
  pure $ map (buildCodeAction name params.textDocument.uri range) solutions


text:
%default total

data Fix : (Type -> Type) -> Type where
  MkFix : f (Fix f) -> Fix f

F : Type
F = Fix Not

yesF : Not F -> F
yesF nf = MkFix nf

notF : Not F
notF (MkFix f) = f (yesF f)

argh : Void
argh = notF (yesF notF)


text:
module Part2.Sec8_1_eqproof
import Data.Vect

%default total

{-
Returns proof that num1 and num2 are equal

data (=) : a -> b -> Type where
     Refl : x = x
cong : {func : a -> b} -> x = y -> func x = func y
-}
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just prf => Just (cong prf)

{-
Notes: if the last line in defintion of exactLength is changed to
Just prf => ?hole

idris repl:
*Part2/Sec8_1_eqproof> :t hole
  a : Type
  m : Nat
  len : Nat
  prf : len = m
  input : Vect m a
--------------------------------------
hole : Maybe (Vect len a)

When last line is replaced with:
Just prf => Just input
causes compiler error:

./Part2/Sec8_1_eqproof.idr:34:49-58:
   |
34 |                                     Just prf => Just input
   |                                                 ~~~~~~~~~~
When checking right hand side of Part2.Sec8_1_eqproof.case block in exactLength at ./Part2/Sec8_1_eqproof.idr:32:14-29 with expected type
        Maybe (Vect len a)

When checking argument x to constructor Prelude.Maybe.Just:
        Type mismatch between
                Vect m a (Type of input)
        and
                Vect len a (Expected type)

        Specifically:
                Type mismatch between
                        m
                and
                        len

Just prf => ?hole -- Just input

Using rewrite syntax from section 8.2 fixes the problem.
But order of len and m is important
`checkEqNat m len` would not work! (equational profs are not automatically symmetric -
sym function in 8.2)

TODO, also using Dec (section 8.3) fixes the problem, why?
This code compiles fine:

exactLength {m} len input = case decEq m len of
         Yes Refl => Just input
         No contra => Nothing
-}
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input
      = case checkEqNat len m of
                                    Nothing => Nothing
                                    Just prf => rewrite prf in Just input  -- syntax from 8.2

{-
`exactLength` implementation in the book (repeated below) does not need `rewrite` syntax.
Maybe because it keeps nat value in scope (look at SameNat constructor) and is Nat sepecific.
The need to have evidence of type/value being checked in scope seems to be important.
This relates to some of my Haskell experience (see F2 type family and solutions to example 1 and 2).
-}

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
     SameNat : (num : Nat) -> EqNat num num

{- nicely generated by Idris by case splitting on third variable (eq) -}
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (SameNat j) = SameNat (S j)

checkEqNat1 : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat1 Z Z = Just (SameNat Z)
checkEqNat1 Z (S k) = Nothing
checkEqNat1 (S k) Z = Nothing
checkEqNat1 (S k) (S j) = case checkEqNat1 k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)

{- The proof of equality allows this type of method to typecheck and
 rewrite statement is not used. -}
exactLength1 : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength1 {m} len input
      = case checkEqNat1 m len of
                                    Nothing => Nothing
                                    Just (SameNat len) => Just input

{- exercise 1, (x :) is just a function  -}
same_cons : {xs : List a} -> {ys : List a} ->
                      xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf

{- exercise 2, knowing that x's are indentical, this theorem reduces to same_cons -}
same_lists : {xs : List a} -> {ys : List a} ->
                      x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl = same_cons

{- exercise 3, 4 -}
data ThreeEqual : a -> b -> c -> Type where
  Refl3 : ThreeEqual a a a

{- Idris knows that all 3 a's are the same, interstingly no need for cong -}
allSameS : (x, y, z : Nat) -> ThreeEqual x y z -> ThreeEqual (S x) (S y) (S z)
allSameS a a a Refl3 = Refl3

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
import Data.List
import Data.List.Elem

%search_timeout 1000

||| A Place has an ID and a number of tokens
data Place : Type where
  MkPlace : (i : Nat) -> (nTokens : Nat) -> Place

||| A transition has a name
data Transition : Type where
  MkTransition : String -> Transition

||| An Input links a Place and a Transition...
data Input : Type where
  MkInput : (from : Place) -> (to : Transition) -> Input

-- Accessor functions for proof
0 inputFrom : Input -> Place
inputFrom (MkInput p t) = p

0 inputTo : Input -> Transition
inputTo (MkInput p t) = t

data SoundInputFrom : Input -> List Place -> Type where
  MkSoundInputFrom : (i : Input)
                     -> (ps : List Place)
                     -> (prf : Elem (inputFrom i) ps)
                     -> SoundInputFrom i ps

data SoundInputTo : Input -> List Transition -> Type where
  MkSoundInputTo : (i : Input)
                   -> (ts : List Transition)
                   -> (prf : Elem (inputTo i) ts)
                   -> SoundInputTo i ts

data SoundInput : Input -> List Place -> List Transition -> Type where
  MkSoundInput : (i : Input)
                 -> (ps : List Place)
                 -> (ts : List Transition)
                 -> (fromOK : SoundInputFrom i ps)
                 -> (toOK   : SoundInputTo   i ts)
                 -> SoundInput i ps ts

data AllInputsSound : List Input -> List Place -> List Transition -> Type where
  NilInputsIsSound : AllInputsSound [] _ _
  ConsIsSound : (headIsSound : SoundInput i ps ts)
                -> (tailIsSound : AllInputsSound is ps ts)
                -> AllInputsSound (i :: is) ps ts

-- Searching here finds the right answer immediately, but then if we don't
-- have a timeout, it takes ages to explore more non-solutions! So we cut off
-- after a second
tailIsNotSound : (contra : (AllInputsSound is ps ts -> Void))
                 -> AllInputsSound (i :: is) ps ts
                 -> Void


text:
main : IO ()
main = do
  [| (const $ pure MkUnit) (pure ()) |]
  pure ()


text:
module Core.ConSig

import General

import Debug.Error

import Core.Variable

%language ElabReflection

--  oYYo _YYY_ 8o  0 oYYYo Y8Y  oYYo
-- 0   " 0   0 8Yo 8 %___   0  0  __
-- 0   , 0   0 8 Yo8 `"""p  0  0  "8
--  YooY "ooo" 0   8 YoooY o8o  YooY

public export
data ConSig a = ConSigNil a | ConSigCons Plict a (Scope a (ConSig a))

partial export
showConSig : Show a => (String -> a) -> ConSig a -> String
showConSig _ (ConSigNil a) = show a
showConSig f (ConSigCons plic a sc) with (length (names sc) == 1)
	| True = do
		let a0' = unwords (names sc) ++ " : " ++ show a
		let a' = case plic of
			Expl => "(" ++ a0' ++ ") "
			Impl => "{" ++ a0' ++ "} "
		a' ++ showConSig f (instantiate sc (map f (names sc)))
showConSig _ _ = error "ConSigs should have exactly one scope argument."

export
conSigLength : (String -> a) -> ConSig a -> Int
conSigLength _ (ConSigNil _) = 0
conSigLength f (ConSigCons _ _ sc) = 1 + conSigLength f (instantiate sc (map f (names sc)))

public export
Signature : Type -> Type
Signature a = SortedMap FullName (ConSig a)


text:
module Compiler.CaseOpts

-- Case block related transformations

import Compiler.CompileExpr

import Core.CompileExpr
import Core.Context
import Core.FC
import Core.TT

import Data.List
import Data.Vect

%default covering

{-
Lifting out lambdas:

case t of
     C1 => \x1 => e1
     ...
     Cn => \xn = en

  where every branch begins with a lambda, can become:

\x => case t of
           C1 => e1[x/x1]
           ,,,
           Cn => en[x/xn]
-}

shiftUnder : {args : _} ->
             {idx : _} ->
             (0 p : IsVar n idx (x :: args ++ vars)) ->
             NVar n (args ++ x :: vars)
shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)

shiftVar : {outer, args : _} ->
           {idx : _} ->
           (0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
           NVar n (outer ++ (args ++ x :: vars))
shiftVar {outer = []} p = shiftUnder p
shiftVar {outer = (n::xs)} First = MkNVar First
shiftVar {outer = (y::xs)} (Later p)
    = case shiftVar p of
           MkNVar p' => MkNVar (Later p')

mutual
  shiftBinder : {outer, args : _} ->
                (new : Name) ->
                CExp (outer ++ old :: (args ++ vars)) ->
                CExp (outer ++ (args ++ new :: vars))
  shiftBinder new (CLocal fc p)
      = case shiftVar p of
             MkNVar p' => CLocal fc (renameVar p')
    where
      renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
                  IsVar x i (outer ++ (args ++ (new :: rest)))
      renameVar = believe_me -- it's the same index, so just the identity at run time
  shiftBinder new (CRef fc n) = CRef fc n
  shiftBinder {outer} new (CLam fc n sc)
      = CLam fc n $ shiftBinder {outer = n :: outer} new sc
  shiftBinder new (CLet fc n inlineOK val sc)
      = CLet fc n inlineOK (shiftBinder new val)
                           $ shiftBinder {outer = n :: outer} new sc
  shiftBinder new (CApp fc f args)
      = CApp fc (shiftBinder new f) $ map (shiftBinder new) args
  shiftBinder new (CCon fc ci c tag args)
      = CCon fc ci c tag $ map (shiftBinder new) args
  shiftBinder new (COp fc op args) = COp fc op $ map (shiftBinder new) args
  shiftBinder new (CExtPrim fc p args)
      = CExtPrim fc p $ map (shiftBinder new) args
  shiftBinder new (CForce fc r arg) = CForce fc r $ shiftBinder new arg
  shiftBinder new (CDelay fc r arg) = CDelay fc r $ shiftBinder new arg
  shiftBinder new (CConCase fc sc alts def)
      = CConCase fc (shiftBinder new sc)
                    (map (shiftBinderConAlt new) alts)
                    (map (shiftBinder new) def)
  shiftBinder new (CConstCase fc sc alts def)
      = CConstCase fc (shiftBinder new sc)
                      (map (shiftBinderConstAlt new) alts)
                      (map (shiftBinder new) def)
  shiftBinder new (CPrimVal fc c) = CPrimVal fc c
  shiftBinder new (CErased fc) = CErased fc
  shiftBinder new (CCrash fc msg) = CCrash fc msg

  shiftBinderConAlt : {outer, args : _} ->
                (new : Name) ->
                CConAlt (outer ++ (x :: args ++ vars)) ->
                CConAlt (outer ++ (args ++ new :: vars))
  shiftBinderConAlt new (MkConAlt n ci t args' sc)
      = let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
                = rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
        MkConAlt n ci t args' $
           rewrite (appendAssociative args' outer (args ++ new :: vars))
             in shiftBinder new {outer = args' ++ outer} sc'

  shiftBinderConstAlt : {outer, args : _} ->
                (new : Name) ->
                CConstAlt (outer ++ (x :: args ++ vars)) ->
                CConstAlt (outer ++ (args ++ new :: vars))
  shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc

-- If there's a lambda inside a case, move the variable so that it's bound
-- outside the case block so that we can bind it just once outside the block
liftOutLambda : {args : _} ->
                (new : Name) ->
                CExp (old :: args ++ vars) ->
                CExp (args ++ new :: vars)
liftOutLambda = shiftBinder {outer = []}

-- If all the alternatives start with a lambda, we can have a single lambda
-- binding outside
tryLiftOut : (new : Name) ->
             List (CConAlt vars) ->
             Maybe (List (CConAlt (new :: vars)))
tryLiftOut new [] = Just []
tryLiftOut new (MkConAlt n ci t args (CLam fc x sc) :: as)
    = do as' <- tryLiftOut new as
         let sc' = liftOutLambda new sc
         pure (MkConAlt n ci t args sc' :: as')
tryLiftOut _ _ = Nothing

tryLiftOutConst : (new : Name) ->
                  List (CConstAlt vars) ->
                  Maybe (List (CConstAlt (new :: vars)))
tryLiftOutConst new [] = Just []
tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
    = do as' <- tryLiftOutConst new as
         let sc' = liftOutLambda {args = []} new sc
         pure (MkConstAlt c sc' :: as')
tryLiftOutConst _ _ = Nothing

tryLiftDef : (new : Name) ->
             Maybe (CExp vars) ->
             Maybe (Maybe (CExp (new :: vars)))
tryLiftDef new Nothing = Just Nothing
tryLiftDef new (Just (CLam fc x sc))
   = let sc' = liftOutLambda {args = []} new sc in
         pure (Just sc')
tryLiftDef _ _ = Nothing

allLams : List (CConAlt vars) -> Bool
allLams [] = True
allLams (MkConAlt n ci t args (CLam _ _ _) :: as)
   = allLams as
allLams _ = False

allLamsConst : List (CConstAlt vars) -> Bool
allLamsConst [] = True
allLamsConst (MkConstAlt c (CLam _ _ _) :: as)
   = allLamsConst as
allLamsConst _ = False

-- label for next name for a lambda. These probably don't need really to be
-- unique, since we've proved things about the de Bruijn index, but it's easier
-- to see what's going on if they are.
data NextName : Type where

getName : {auto n : Ref NextName Int} ->
          Core Name
getName
    = do n <- get NextName
         put NextName (n + 1)
         pure (MN "clam" n)

-- The transformation itself
mutual
  caseLam : {auto n : Ref NextName Int} ->
            CExp vars -> Core (CExp vars)
  -- Interesting cases first: look for case blocks where every branch is a
  -- lambda
  caseLam (CConCase fc sc alts def)
      = if allLams alts && defLam def
           then do var <- getName
                   -- These will work if 'allLams' and 'defLam' are consistent.
                   -- We only do that boolean check because it saves us doing
                   -- unnecessary work (say, if the last one we try fails)
                   let Just newAlts = tryLiftOut var alts
                            | Nothing => throw (InternalError "Can't happen caseLam 1")
                   let Just newDef = tryLiftDef var def
                            | Nothing => throw (InternalError "Can't happen caseLam 2")
                   newAlts' <- traverse caseLamConAlt newAlts
                   newDef' <- traverseOpt caseLam newDef
                   -- Q: Should we go around again?
                   pure (CLam fc var (CConCase fc (weaken sc) newAlts' newDef'))
           else do sc' <- caseLam sc
                   alts' <- traverse caseLamConAlt alts
                   def' <- traverseOpt caseLam def
                   pure (CConCase fc sc' alts' def')
    where
      defLam : Maybe (CExp vars) -> Bool
      defLam Nothing = True
      defLam (Just (CLam _ _ _)) = True
      defLam _ = False
  -- Next case is pretty much as above. There's a boring amount of repetition
  -- here because ConstCase is just a little bit different.
  caseLam (CConstCase fc sc alts def)
      = if allLamsConst alts && defLam def
           then do var <- getName
                   -- These will work if 'allLams' and 'defLam' are consistent.
                   -- We only do that boolean check because it saves us doing
                   -- unnecessary work (say, if the last one we try fails)
                   let Just newAlts = tryLiftOutConst var alts
                            | Nothing => throw (InternalError "Can't happen caseLam 1")
                   let Just newDef = tryLiftDef var def
                            | Nothing => throw (InternalError "Can't happen caseLam 2")
                   newAlts' <- traverse caseLamConstAlt newAlts
                   newDef' <- traverseOpt caseLam newDef
                   pure (CLam fc var (CConstCase fc (weaken sc) newAlts' newDef'))
           else do sc' <- caseLam sc
                   alts' <- traverse caseLamConstAlt alts
                   def' <- traverseOpt caseLam def
                   pure (CConstCase fc sc' alts' def')
    where
      defLam : Maybe (CExp vars) -> Bool
      defLam Nothing = True
      defLam (Just (CLam _ _ _)) = True
      defLam _ = False
  -- Structural recursive cases
  caseLam (CLam fc x sc)
      = CLam fc x <$> caseLam sc
  caseLam (CLet fc x inl val sc)
      = CLet fc x inl <$> caseLam val <*> caseLam sc
  caseLam (CApp fc f args)
      = CApp fc <$> caseLam f <*> traverse caseLam args
  caseLam (CCon fc n ci t args)
      = CCon fc n ci t <$> traverse caseLam args
  caseLam (COp fc op args)
      = COp fc op <$> traverseVect caseLam args
  caseLam (CExtPrim fc p args)
      = CExtPrim fc p <$> traverse caseLam args
  caseLam (CForce fc r x)
      = CForce fc r <$> caseLam x
  caseLam (CDelay fc r x)
      = CDelay fc r <$> caseLam x
  -- All the others, no recursive case so just return the input
  caseLam x = pure x

  caseLamConAlt : {auto n : Ref NextName Int} ->
                  CConAlt vars -> Core (CConAlt vars)
  caseLamConAlt (MkConAlt n ci tag args sc)
      = MkConAlt n ci tag args <$> caseLam sc

  caseLamConstAlt : {auto n : Ref NextName Int} ->
                    CConstAlt vars -> Core (CConstAlt vars)
  caseLamConstAlt (MkConstAlt c sc) = MkConstAlt c <$> caseLam sc

export
caseLamDef : {auto c : Ref Ctxt Defs} ->
             Name -> Core ()
caseLamDef n
    = do defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
         let Just cexpr =  compexpr def             | Nothing => pure ()
         setCompiled n !(doCaseLam cexpr)
  where
    doCaseLam : CDef -> Core CDef
    doCaseLam (MkFun args def)
        = do n <- newRef NextName 0
             pure $ MkFun args !(caseLam def)
    doCaseLam d = pure d

{-

Case of case:

case (case x of C1 => E1
                C2 => E2
                ...) of
     D1 => F1
     D2 => F2
     ...
     _ => Fd

can become

case x of
     C1 => case E1 of
                D1 => F1
                D2 => F2
                ...
                _ => Fd
     C2 => case E2 of
                D1 => F1
                D2 => F2
                ...
                _ => Fd

to minimise risk of duplication, do this only when E1, E2 are all
constructor headed, or there's only one branch (for now)

-}

doCaseOfCase : FC ->
               (x : CExp vars) ->
               (xalts : List (CConAlt vars)) ->
               (alts : List (CConAlt vars)) ->
               (def : Maybe (CExp vars)) ->
               CExp vars
doCaseOfCase fc x xalts alts def
    = CConCase fc x (map updateAlt xalts) Nothing
  where
    updateAlt : CConAlt vars -> CConAlt vars
    updateAlt (MkConAlt n ci t args sc)
        = MkConAlt n ci t args $
              CConCase fc sc
                       (map (weakenNs (mkSizeOf args)) alts)
                       (map (weakenNs (mkSizeOf args)) def)

doCaseOfConstCase : FC ->
                    (x : CExp vars) ->
                    (xalts : List (CConstAlt vars)) ->
                    (alts : List (CConstAlt vars)) ->
                    (def : Maybe (CExp vars)) ->
                    CExp vars
doCaseOfConstCase fc x xalts alts def
    = CConstCase fc x (map updateAlt xalts) Nothing
  where
    updateAlt : CConstAlt vars -> CConstAlt vars
    updateAlt (MkConstAlt c sc)
        = MkConstAlt c $
              CConstCase fc sc alts def

tryCaseOfCase : CExp vars -> Maybe (CExp vars)
tryCaseOfCase (CConCase fc (CConCase fc' x xalts Nothing) alts def)
    = if canCaseOfCase xalts
         then Just (doCaseOfCase fc' x xalts alts def)
         else Nothing
  where
    conCase : CConAlt vars -> Bool
    conCase (MkConAlt _ _ _ _ (CCon _ _ _ _ _)) = True
    conCase _ = False

    canCaseOfCase : List (CConAlt vars) -> Bool
    canCaseOfCase [] = True
    canCaseOfCase [x] = True
    canCaseOfCase xs = all conCase xs
tryCaseOfCase (CConstCase fc (CConstCase fc' x xalts Nothing) alts def)
    = if canCaseOfCase xalts
         then Just (doCaseOfConstCase fc' x xalts alts def)
         else Nothing
  where
    constCase : CConstAlt vars -> Bool
    constCase (MkConstAlt _ (CPrimVal _ _)) = True
    constCase _ = False

    canCaseOfCase : List (CConstAlt vars) -> Bool
    canCaseOfCase [] = True
    canCaseOfCase [x] = True
    canCaseOfCase xs = all constCase xs
tryCaseOfCase _ = Nothing

export
caseOfCase : CExp vars -> CExp vars
caseOfCase tm = go 5 tm
  where
    go : Nat -> CExp vars -> CExp vars
    go Z tm = tm
    go (S k) tm = maybe tm (go k) (tryCaseOfCase tm)


text:
import Json
import JsonDSL
import Data.Floats
import Inspect

isStructured : Maybe PMJsonValue -> Bool
isStructured (Just (JsonArray _)) = True
isStructured (Just (JsonObject _)) = True
isStructured Nothing = True
isStructured (Just _) = False

isValidID : PMJsonValue -> Bool
isValidID (JsonNumber n) = floor n == n
isValidID (JsonString _) = True
isValidID JsonNull = True
isValidID _ = False

data ErrorCode = ParseError
               | InvalidRequest
               | MethodNotFound
               | InvalidParams
               | InternalError

-- would be nicer to use a bidirectional map for that (todo)
errorCode : ErrorCode -> Float
errorCode ParseError = -32700
errorCode InvalidRequest = -32600
errorCode MethodNotFound = -32601
errorCode InvalidParams = -32602
errorCode InternalError = -32603

-- pattern-matching on negative numbers doesn't work ATM
parseErrorCode : Float -> Maybe ErrorCode
parseErrorCode code =
  if code == -32700 then Just ParseError else
     if code == -3600 then Just InvalidRequest else
       if code == -3601 then Just MethodNotFound else
         if code == -3602 then Just InvalidParams else
           if code == -3603 then Just InternalError else
             Nothing

data ErrorObject = ErrObj ErrorCode String (Maybe PMJsonValue)

-- not including version here, should always be 2.0 (which is the only
-- supported version, check it on parsing)
data Object : Type where
  Request : (method: String) -> {auto notrpc: isPrefixOf "rpc." method = False} ->
    (params: Maybe PMJsonValue) -> {auto ps: isStructured params = True} ->
    (id: PMJsonValue) -> {auto ci: isValidID id = True} -> Object
  Notification : (method: String) -> {auto notrpc: isPrefixOf "rpc." method = False} ->
    (params: Maybe PMJsonValue) -> {auto ps: isStructured params = True} -> Object
  Result : (result: PMJsonValue) -> (id: PMJsonValue) -> {auto ci: isValidID id = True} -> Object
  Error : ErrorObject -> (id: PMJsonValue) -> {auto ci: isValidID id = True} -> Object

data Packet = Single Object | Batch (List Object)

invalidRequest : Either Object Object
invalidRequest = Left $ Error (ErrObj InvalidRequest "Invalid request" Nothing) JsonNull

parseObject : PMJsonValue -> Either Object Object

-- request
parseObject (j{["id" .a id,
                "jsonrpc" .s "2.0",
                "method" .s method,
                "params" .a params]}) with (inspect (isPrefixOf "rpc." method),
                                            inspect (isStructured (Just params)),
                                            inspect (isValidID id))
  | (wi _ False _, wi _ True _, wi _ True _) = Right $ Request method (Just params) id
  | _ = invalidRequest
parseObject (j{["id" .a id,
                "jsonrpc" .s "2.0",
                "method" .s method]}) with (inspect (isPrefixOf "rpc." method),
                                            inspect (isValidID id))
  | (wi _ False _, wi _ True _) = Right $ Request method Nothing id
  | _ = invalidRequest

-- notification
parseObject (j{["jsonrpc" .s "2.0",
                "method" .s method,
                "params" .a params]}) with (inspect (isPrefixOf "rpc." method),
                                            inspect (isStructured (Just params)))
  | (wi _ False _, wi _ True _) = Right $ Notification method (Just params)
  | _ = invalidRequest
parseObject (j{["jsonrpc" .s "2.0",
                "method" .s method]}) with (inspect (isPrefixOf "rpc." method))
  | (wi _ False _) = Right $ Notification method Nothing
  | _ = invalidRequest

-- result
parseObject (j{["id" .a id,
                "jsonrpc" .s "2.0",
                "result" .a result]}) with (inspect (isValidID id))
  | (wi _ True _) = Right $ Result result id
  | _ = invalidRequest

-- error
parseObject (j{["error" .a j{["code" .f errCode,
                              "message" .s errMessage]},
                "id" .a id,
                "jsonrpc" .s "2.0"]}) with (parseErrorCode errCode,
                                            inspect (isValidID id))
  | (Just ec, wi _ True _) = Right $ Error (ErrObj ec errMessage Nothing) id
  | _ = invalidRequest
parseObject (j{["error" .a j{["code" .f errCode,
                              "data" .a errData,
                              "message" .s errMessage]},
                "id" .a id,
                "jsonrpc" .s "2.0"]}) with (parseErrorCode errCode,
                                            inspect (isValidID id))
  | (Just ec, wi _ True _) = Right $ Error (ErrObj ec errMessage (Just errData)) id
  | _ = invalidRequest

-- unknown
parseObject _ = Left $ Error (ErrObj InvalidRequest "Failed to parse a JSON-RPC 2.0 object" Nothing) JsonNull

parseObjectTest : String -> Either Object Object
parseObjectTest s = do
  case (parse jsonToplevelValue s) of
    (Left str) => Left $ Error (ErrObj ParseError "Object parse error" Nothing) JsonNull
    (Right json) => parseObject $ toPM json

-- parseObjectTest """{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}"""
-- parseObjectTest """{"jsonrpc": "2.0", "method": "update", "params": [1,2,3,4,5]}"""
-- parseObjectTest """{"jsonrpc": "2.0", "result": 19, "id": 1}"""
-- parseObjectTest """{"jsonrpc": "2.0", "error": {"code": -32601, "message": "Method not found"}, "id": "1"}"""
-- parseObjectTest """{"jsonrpc": "2.0", "error": {"code": 0, "message": "test", "data": "data test"}, "id": "1"}"""

composeObject : Object -> PMJsonValue
composeObject (Request method (Just params) id) = j{["id" .a id,
                                                     "jsonrpc" .s "2.0",
                                                     "method" .s method,
                                                     "params" .a params]}
composeObject (Request method Nothing id) = j{["id" .a id,
                                               "jsonrpc" .s "2.0",
                                               "method" .s method]}
composeObject (Notification method (Just params)) = j{["jsonrpc" .s "2.0",
                                                       "method" .s method,
                                                       "params" .a params]}
composeObject (Notification method Nothing) = j{["jsonrpc" .s "2.0",
                                                 "method" .s method]}
composeObject (Result result id) = j{["id" .a id,
                                      "jsonrpc" .s "2.0",
                                      "result" .a result]}
composeObject (Error (ErrObj errCode errMessage (Just errData)) id) =
  j{["error" .a j{["code" .f (errorCode errCode),
                   "message" .s errMessage,
                   "data" .a errData]},
     "id" .a id,
     "jsonrpc" .s "2.0"]}
composeObject (Error (ErrObj errCode errMessage Nothing) id) =
  j{["error" .a j{["code" .f (errorCode errCode),
                   "message" .s errMessage]},
     "id" .a id,
     "jsonrpc" .s "2.0"]}

-- map (show . composeObject) $ parseObjectTest """{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}"""

-- batch

parsePacket : PMJsonValue -> Either Object Packet
parsePacket j[l] = map Batch $ ugh l
  where ugh : List PMJsonValue -> Either Object (List Object)
        ugh [] = return []
        ugh (x::xs) = do
          cur <- parseObject x
          next <- ugh xs
          return (cur::next)
parsePacket o@j{_} = map Single $ parseObject o
parsePacket _ = Left $ Error (ErrObj InvalidRequest "Malformed packet" Nothing) JsonNull

parsePacketTest : String -> Either Object Packet
parsePacketTest s = do
  case (parse jsonToplevelValue s) of
    (Left str) => Left $ Error (ErrObj ParseError "Packet parse error" Nothing) JsonNull
    (Right json) => parsePacket $ toPM json

-- parsePacketTest """{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}"""
-- parsePacketTest """[{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "update", "params": [1,2,3,4,5]}]"""

composePacket : Packet -> PMJsonValue
composePacket (Single o) = composeObject o
composePacket (Batch l) = JsonArray $ map composeObject l

-- map (show . composePacket) $ parsePacketTest """[{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "update", "params": [1,2,3,4,5]}]"""

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
module DepB

import Submodule.DepC

empty : ()
empty = ()

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Equis.Matrix.Algebraic

import Data.Matrix.Algebraic

%access private

||| Retrieves the scalar value from an order-1 square matrix.
|||
||| @x the matrix
export
scalar : (x : Matrix (S Z) (S Z) a) -> a
scalar x = head (head x)

||| Zips two matrices together pairwise.
|||
||| @x the first matrix
||| @y the second matrix
export
zipMatrix : (x : Matrix n m a) -> (y : Matrix n m b) -> Matrix n m (a, b)
zipMatrix [] [] = []
zipMatrix (x :: xs) (y :: ys) = (zip x y) :: (zipMatrix xs ys)

||| Maps a function over a matrix.
|||
||| @f the function
||| @x the matrix
export
mapMatrix : (f : a -> b) -> (x : Matrix n m a) -> Matrix n m b
mapMatrix f x = map (map f) x

||| Generates a matrix of the specified order containing zero-based coordinates along one dimension.
|||
||| @n the first matrix dimension
||| @m the second matrix dimension
coord : (n : Nat) -> (m : Nat) -> Matrix n m (Fin m)
coord Z (S k) = []
coord (S k) m = (fins m) :: (coord k m)

||| Generates a matrix of the specified order containing zero-based coordinates along both dimensions.
|||
||| @n the first matrix dimension
||| @m the second matrix dimension
export
coords : (n : Nat) -> (m : Nat) -> Matrix n m (Fin n, Fin m)
coords n m = zipMatrix (transpose (coord m n)) (coord n m)

max_stars_repo_name: lambdacasserole/equis

max_issues_repo_name: lambdacasserole/equis

max_forks_repo_name: lambdacasserole/equis


text:
module CheckEqDec

data Vect : Nat -> (elem : Type) -> Type where
     Nil : Vect Z elem
     (::) : elem -> Vect n elem -> Vect (1 + n) elem

zeroNotSuc : (0 = S k) -> Void
zeroNotSuc Refl impossible

sucNotZero : (S k = 0) -> Void
sucNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSuc
checkEqNat (S k) Z = No sucNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
                              (Yes prf) => Yes (cong prf)
                              (No contra) => No (noRec contra)

-- Ex 8.3 #1
headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} -> (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} -> (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl

-- Ex 8.3 #2
DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) = case decEq x y of
                                 (Yes prf1) => case decEq xs ys of
                                                   (Yes prf2) => Yes $ rewrite prf1 in rewrite prf2 in Refl
                                                   (No contra2) => No $ tailUnequal contra2
                                 (No contra1) => No $ headUnequal contra1


text:
0
foo : (0 b : Bool) -> Bool
foo b = b

0
bar : Bool
bar = q
  where
    q : Bool
    q = foo True

0
baz : Bool
baz = let q : Bool
          q = foo True in
      q


text:
module Dbcritic.Libpq

import Control.IOExcept
import Data.Vect

%include C "libpq-fe.h"
%lib C "pq"

namespace raw
    connectdb : String -> IO Ptr
    connectdb = foreign FFI_C "PQconnectdb" (String -> IO Ptr)

    errorMessage : Ptr -> IO String
    errorMessage = foreign FFI_C "PQerrorMessage" (Ptr -> IO String)

    exec : Ptr -> String -> IO Ptr
    exec = foreign FFI_C "PQexec" (Ptr -> String -> IO Ptr)

    getisnull : Ptr -> Int -> Int -> IO Int
    getisnull = foreign FFI_C "PQgetisnull" (Ptr -> Int -> Int -> IO Int)

    getvalue : Ptr -> Int -> Int -> IO String
    getvalue = foreign FFI_C "PQgetvalue" (Ptr -> Int -> Int -> IO String)

    nfields : Ptr -> IO Int
    nfields = foreign FFI_C "PQnfields" (Ptr -> IO Int)

    ntuples : Ptr -> IO Int
    ntuples = foreign FFI_C "PQntuples" (Ptr -> IO Int)

    resultErrorMessage : Ptr -> IO String
    resultErrorMessage = foreign FFI_C "PQresultErrorMessage" (Ptr -> IO String)

    status : Ptr -> IO Int
    status = foreign FFI_C "PQstatus" (Ptr -> IO Int)

export
data PgConnection =
    MkPgConnection Ptr

export
data PgResult =
    MkPgResult Ptr

export
pgConnect : String -> IOExcept String PgConnection
pgConnect conninfo = IOM $ do
    conn <- raw.connectdb conninfo
    stat <- raw.status conn
    if stat == 0
        then pure (Right (MkPgConnection conn))
        else Left <$> errorMessage conn

export
pgExecute : PgConnection -> String -> IOExcept String PgResult
pgExecute (MkPgConnection conn) command = IOM $ do
    res <- raw.exec conn command
    err <- resultErrorMessage res
    pure $ if err == "" then Right (MkPgResult res) else Left err

export
pgRows : PgResult -> Int
pgRows (MkPgResult res) = unsafePerformIO $ raw.ntuples res

export
pgCols : PgResult -> Int
pgCols (MkPgResult res) = unsafePerformIO $ raw.nfields res

export
pgCell : PgResult -> Int -> Int -> Maybe String
pgCell (MkPgResult res) row col = unsafePerformIO $ do
    isnull <- raw.getisnull res row col
    if isnull == 1 then pure Nothing
                   else Just <$> raw.getvalue res row col

export
pgRow : PgResult -> Int -> List (Maybe String)
pgRow res row = map (pgCell res row) [0, 1 .. pgCols res - 1]

export
pgGrid : PgResult -> List (List (Maybe String))
pgGrid res = map (pgRow res) [0, 1 .. pgRows res - 1]

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module CLaSH.Default

class Default a where
  def : a

instance Default Int where
  def = 0

instance Default Integer where
  def = 0

max_stars_repo_name: christiaanb/clash-prelude-idris

max_issues_repo_name: christiaanb/clash-prelude-idris

max_forks_repo_name: christiaanb/clash-prelude-idris


text:
module Main

import IdrisScript
import IdrisScript.Objects
import IdrisScript.JSON

main : JS_IO ()
main = do
  let text = "{\"foo\":true,\"bar\":1337}"
  case !(parse text) of
       Just (_ ** obj) =>
         case !(getProperty "bar" obj) of
              Just (_ ** res) => log res
              _               => pure ()
       _               => pure ()

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module FFI.Concurrency

import FFI
import Data.List1
import Data.Vect
import Data.Either
import Data.Promise
import Language.JSON

%default total

concurrency_ffi : String -> String
concurrency_ffi = node_ffi "concurrency"

export
data Future : Type where [external]

%foreign concurrency_ffi "future"
prim__future : (args : String) -> PrimIO Future

export
fork : HasIO io => (args : String) -> io Future
fork args = primIO $ prim__future args

%foreign "node:lambda:(p1,p2)=>Promise.all([p1,p2])"
prim__both : Future -> Future -> PrimIO Future

%foreign "node:lambda:(p)=>Promise.all([p])"
prim__singleton : Future -> PrimIO Future

%foreign "node:lambda:()=>Promise.all([])"
prim__neutral : PrimIO Future

%foreign "node:lambda:(p)=>{return new Promise((onSuccess, onFailure) => p.then(r => onSuccess(r.flat()), onFailure))}"
prim__flatten : Future -> PrimIO Future

all : HasIO io => Foldable t => t Future -> io Future
all xs = foldr both (primIO prim__neutral) xs
  where
    both : Future -> io Future -> io Future
    both x y = do
      x'     <- primIO $ prim__singleton x
      nested <- primIO $ prim__both x' !y
      primIO $ prim__flatten nested

%foreign concurrency_ffi "await_stringify"
prim__awaitStringify : Future -> (onSuccess : String -> PrimIO ()) -> (onError : String -> PrimIO ()) -> PrimIO ()

||| Create a Promise that waits for all the given futures to finish
||| and then processes the result (an array of results) as a list
||| of JSON objects.
export
promiseAll : Foldable t => t Future -> Promise (List JSON)
promiseAll xs =
  do f <- all xs
     str <- promisify $ \ok,err => prim__awaitStringify f (\x => toPrim $ ok x) (\y => toPrim $ err y)
     JArray xs <- either . maybeToEither "Failed to parse JSON from \{str}" $ parse str
       | other => reject "Expected a JSON array from futures but got \{show other}."
     pure xs

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony