text:
module PLFI.Part1.Isomorphism

import Data.Nat
import Data.Vect
import Syntax.PreorderReasoning
import Syntax.PreorderReasoning.Generic
import Control.Order
import Control.Relation

0
handwaving : {t : Type} -> (a : t) -> (b : t) -> (a = b)
handwaving a b = believe_me (the (a=a) Refl)

namespace Postulate

  export 0
  extensionality : {a,b : Type} -> {f,g : a -> b} -> ((x : a) -> f x = g x) -> f = g
  extensionality _ = handwaving f g

addX : (m,n : Nat) -> Nat
addX m Z = m
addX m (S n) = S (addX m n)

sameAdd : (m, n : Nat) -> addX m n = m + n
sameAdd m n = rewrite plusCommutative m n in helper m n
  where
    helper : (m, n : Nat) -> addX m n = n + m
    helper m 0     = Refl
    helper m (S n) = cong S (helper m n)

add : Nat -> Nat -> Nat
add = (+)

0
same : Isomorphism.addX = Isomorphism.add
same = extensionality (\p => extensionality (\q => sameAdd p q))

namespace Things

  interesting1 : (x : Nat) -> (y : Nat) -> Nat
  interesting1 x y = x + y

  interesting2 : Nat
  interesting2 = interesting1 {y=2} {x=1}

-- infix 0 _≃_
-- record _≃_ (A B : Set) : Set where
--   field
--     to   : A → B
--     from : B → A
--     from∘to : ∀ (x : A) → from (to x) ≡ x
--     to∘from : ∀ (y : B) → to (from y) ≡ y
-- open _≃_

public export
record Iso (a, b : Type) where
  constructor MkIso
  to     : a -> b
  from   : b -> a
  fromTo : (x : a) -> from (to x) === x
  toFrom : (y : b) -> to (from y) === y

-- interface IsoI a b where
--   toI   : a -> b
--   fromI : b -> a
--   fromToI : (x : a) -> fromI (toI x) = x
--   toFromI : (y : b) -> toI (fromI y) = y

-- ≃-refl : ∀ {A : Set}
--     -----
--   → A ≃ A
-- ≃-refl =
--   record
--     { to      = λ{x → x}
--     ; from    = λ{y → y}
--     ; from∘to = λ{x → refl}
--     ; to∘from = λ{y → refl}
--     }

public export
isoRefl : {a : Type} -> Iso a a
isoRefl = MkIso
  { to     = id
  , from   = id
  , fromTo = \x => Refl
  , toFrom = \x => Refl
  }

isoTo : Iso a b -> (a -> b)
isoTo i = i.to

-- ≃-sym : ∀ {A B : Set}
--   → A ≃ B
--     -----
--   → B ≃ A
-- ≃-sym A≃B =
--   record
--     { to      = from A≃B
--     ; from    = to   A≃B
--     ; from∘to = to∘from A≃B
--     ; to∘from = from∘to A≃B
--     }

public export
isoSym : Iso a b -> Iso b a
isoSym (MkIso to from fromTo toFrom) = MkIso from to toFrom fromTo

-- ≃-trans : ∀ {A B C : Set}
--   → A ≃ B
--   → B ≃ C
--     -----
--   → A ≃ C
-- ≃-trans A≃B B≃C =
--   record
--     { to       = to   B≃C ∘ to   A≃B
--     ; from     = from A≃B ∘ from B≃C
--     ; from∘to  = λ{x →
--         begin
--           (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
--         ≡⟨⟩
--           from A≃B (from B≃C (to B≃C (to A≃B x)))
--         ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
--           from A≃B (to A≃B x)
--         ≡⟨ from∘to A≃B x ⟩
--           x
--         ∎}
--     ; to∘from = λ{y →
--         begin
--           (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
--         ≡⟨⟩
--           to B≃C (to A≃B (from A≃B (from B≃C y)))
--         ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
--           to B≃C (from B≃C y)
--         ≡⟨ to∘from B≃C y ⟩
--           y
--         ∎}
--      }

public export
isoTrans : Iso a b -> Iso b c -> Iso a c
isoTrans ab bc = MkIso
  { to     = to bc . to ab
  , from   = from ab . from bc
  , fromTo = \x => Calc $
      |~ (from ab . from bc) ((to bc . to ab) x)
      -- ~~ (from ab . from bc) (to bc (to ab x))  ... (Refl)
      -- ~~ (from ab (from bc (to bc (to ab x))))  ... (Refl)
      ~~ (from ab (to ab x))                    ... (cong ab.from (bc.fromTo (ab.to x)))
      ~~ x                                      ... (ab.fromTo x)
  , toFrom = \y => rewrite ab.toFrom (bc.from y) in bc.toFrom y
--  , toFrom = \y => (?x (bc.toFrom y))
                    -- rewriteP (ab.toFrom (bc.from y)) (bc.toFrom y)

                    -- rewriteP : a = b -> P a -> P b
                    -- rewriteP Refl pa = pa
  }

-- module ≃-Reasoning where

--   infix  1 ≃-begin_
--   infixr 2 _≃⟨_⟩_
--   infix  3 _≃-∎

--   ≃-begin_ : ∀ {A B : Set}
--     → A ≃ B
--       -----
--     → A ≃ B
--   ≃-begin A≃B = A≃B

--   _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
--     → A ≃ B
--     → B ≃ C
--       -----
--     → A ≃ C
--   A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

--   _≃-∎ : ∀ (A : Set)
--       -----
--     → A ≃ A
--   A ≃-∎ = ≃-refl

-- open ≃-Reasoning

public export Reflexive  Type Iso where reflexive = isoRefl
public export Transitive Type Iso where transitive = isoTrans
public export Preorder   Type Iso where

public export
(~~) : (a, b : Type) -> Type
(~~) a b = Iso a b

-- 0
test : {a,b,c : Type} -> Iso a b -> Iso b c -> Iso a c
test ab bc = CalcWith {leq = Iso} $
  |~ a
  <~ b ... (ab)
  <~ c ... (bc)

-- [additive] Semigroup Nat where
--   a <+> b = ?h

-- [multiplicative] Semigroup Nat where
--   a <+> b = ?h2

-- infix 0 _≲_
-- record _≲_ (A B : Set) : Set where
--   field
--     to      : A → B
--     from    : B → A
--     from∘to : ∀ (x : A) → from (to x) ≡ x
-- open _≲_

-- infixr 100 <=

-- %hint -- Would be nice to have
public export
record (<=) (a, b : Type) where
  constructor MkEmb
  to     : a -> b
  from   : b -> a
  -- %hint : Would be nice to have
  fromTo : (x : a) -> from (to x) === x

%hint
fromToX : (ab : (a <= b)) -> (x : a) -> ab.from (ab.to x) === x
fromToX ab x = ab.fromTo x

-- %hint (.to)

-- (<=) : (a,b : Type) -> Type
-- (<=) a b = Emb a b

-- -- A deep question from the audience. :)
-- embIso : {a,b : Type} -> a <= b -> b <= a -> (Iso a b)
-- embIso = ?xembIso

embRefl : {a : Type} -> a <= a
embRefl = MkEmb Prelude.id Prelude.id (\x => Refl)

-- ≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
-- ≲-trans A≲B B≲C =
--   record
--     { to      = λ{x → to   B≲C (to   A≲B x)}
--     ; from    = λ{y → from A≲B (from B≲C y)}
--     ; from∘to = λ{x →
--         begin
--           from A≲B (from B≲C (to B≲C (to A≲B x)))
--         ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
--           from A≲B (to A≲B x)
--         ≡⟨ from∘to A≲B x ⟩
--           x
--         ∎}
--      }

embTrans : {a,b,c : Type} -> a <= b -> b <= c -> a <= c
embTrans ab bc = MkEmb
  { to   = (bc.to . ab.to)
  , from = (ab.from . bc.from)
  , fromTo = \x => Calc $
      |~ ab.from (bc.from (bc.to (ab.to x)))
      ~~ ab.from (ab.to x)
          ... (cong ab.from (bc.fromTo (ab.to x)))
      ~~ x
          ... (ab.fromTo x)
--          ... (fromToX ab x)
  }

-- ≲-antisym : ∀ {A B : Set}
--   → (A≲B : A ≲ B)
--   → (B≲A : B ≲ A)
--   → (to A≲B ≡ from B≲A)
--   → (from A≲B ≡ to B≲A)
--     -------------------
--   → A ≃ B
-- ≲-antisym A≲B B≲A to≡from from≡to =
--   record
--     { to      = to A≲B
--     ; from    = from A≲B
--     ; from∘to = from∘to A≲B
--     ; to∘from = λ{y →
--         begin
--           to A≲B (from A≲B y)
--         ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
--           to A≲B (to B≲A y)
--         ≡⟨ cong-app to≡from (to B≲A y) ⟩
--           from B≲A (to B≲A y)
--         ≡⟨ from∘to B≲A y ⟩
--           y
--         ∎}
--     }

embAntisym
  :  {a,b : Type}
  -> (ab : (a <= b)) -> (ba : (b <= a))
  -> (to ab = from ba) -> (from ab = to ba)
  -> Iso a b
embAntisym (MkEmb t f ft) (MkEmb _ _ ft1) Refl Refl = MkIso t f ft ft1

Reflexive  Type (<=) where reflexive = embRefl
Transitive Type (<=) where transitive = embTrans
Preorder   Type (<=) where

embFromIso : {a,b : Type} -> Iso a b -> (a <= b)
-- Issue in internel meta variable
-- embFromIso (MkIso to from fromTo toFrom) = MkEmb (\{arg:2022} => to arg) from fromTo
embFromIso (MkIso to from fromTo toFrom) = MkEmb to from fromTo

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module Specifications.Monoid

import public Specifications.Semigroup

%default total
%access public export

infixl 8 #

||| specification
isNeutralL : Binop s -> s -> Type
isNeutralL (#) e = (x : _) -> e # x = x

||| specification
isNeutralR : Binop s -> s -> Type
isNeutralR (#) e = (x : _) -> x # e = x

||| composed specification
data MonoidSpec : Binop s -> s -> Type where
  MkMonoid : isAssociative op -> isNeutralL op e -> isNeutralR op e ->
    MonoidSpec op e

||| forget
associative : MonoidSpec op _ -> isAssociative op
associative (MkMonoid g _ _) = g

||| forget
neutralL : MonoidSpec op e -> isNeutralL op e
neutralL (MkMonoid _ l _) = l

||| forget
neutralR : MonoidSpec op e -> isNeutralR op e
neutralR (MkMonoid _ _ r) = r

ext: idr

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Data.GIS.Verified

import Control.Algebra
import Data.GIS

%access public export

interface GIS space ivls => VerifiedGIS space ivls | space where
  conditionA : (r, s, t : space) -> int r s <+> int s t = int r t
  conditionB : (s : space) -> (i : ivls) -> (int s t = i, int s t' = i) -> t = t'

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
module Naperian

-- Naperian Functors, based on https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf

import Data.Vect
import Data.Fin

interface Functor f => Naperian (f : Type -> Type) where
  Log : {f : Type} -> Type
  lookup' : f a -> (Log -> a)
  positions : f Log
  tabulate : (Log -> a) -> f a

  positions = tabulate id

Naperian (Vect n) where
  Log {n} = Fin n

  lookup' [] FZ impossible
  lookup' [] (FS _) impossible
  lookup' (x :: xs) FZ = x
  lookup' (x :: xs) (FS y) = lookup' xs y

  tabulate h = map h positions
    where
      positions = positions' (replicate _ ())
        where
          positions' : Vect n () -> Vect n (Fin n)
          positions' [] = []
          positions' (() :: xs) = FZ :: map FS (positions' xs)

transpose' : (Naperian f, Naperian g) => f (g a) -> g (f a)
transpose' source = (map tabulate . tabulate . flip . lookup' . map lookup') source

example : Vect 2 (Vect 3 Integer)
example = [[1, 2, 3], [4, 5, 6]]

transposedExample : Vect 3 (Vect 2 Integer)
transposedExample = transpose' example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Node.HTTP

export
data HTTP : Type where [external]

%foreign "node:lambda: () => require('http')"
ffi_require : () -> PrimIO HTTP

export
require : HasIO io => io HTTP
require = primIO $ ffi_require ()

namespace Headers

  export
  data Headers : Type where [external]

  %foreign "node:lambda: () => { return {}; }"
  ffi_empty : () -> PrimIO Headers

  export
  empty : HasIO io => io Headers
  empty = primIO $ ffi_empty ()

  %foreign "node:lambda: (name, value) => { const headers = {}; headers[name] = value; return headers; }"
  ffi_singleton : String -> String -> Headers

  export
  singleton : String -> String -> Headers
  singleton name value = ffi_singleton name value

  %foreign "node:lambda: (headers, name, value) => { headers[name] = value; return headers; }"
  ffi_setHeader : Headers -> String -> String -> PrimIO Headers

  export
  (.setHeader) : HasIO io => Headers -> String -> String -> io Headers
  (.setHeader) headers name value = primIO $ ffi_setHeader headers name value

  %foreign "node:lambda: (headers) => __prim_js2idris_array(Object.entries(headers).map(([k,v]) => { return {h:0,a1:k,a2:v}}))"
  export
  (.asList) : Headers -> List (String, String)

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Hardware

import Data.Vect

Gate : Type
Gate = Bool -> Bool -> Bool

nand : Gate
nand True True = False
nand a    b    = True

and : Gate
and a b = nand (nand a b) (nand a b)

or : Gate
or a b = nand (nand a a) (nand b b)

not : Bool -> Bool
not a = nand a a

nor : Gate
nor a b = nand q q
  where
    q = nand (nand a a) (nand b b)

xor : Gate
xor a b = nand d e
  where
    c : Bool
    c = nand a b
    d = nand c a
    e = nand c b

halfAdder : Bool -> Bool -> (Bool, Bool)
halfAdder a b = (xor a b, and a b)

fullAdder : Bool -> Bool -> Bool -> (Bool, Bool)
fullAdder a b c = (xor a (xor b c), or (and a b) (and c (xor a b)))

Word : Nat -> Type
Word n = Vect n Bool

Byte : Type
Byte = Word 8

rippleCarry : Word n -> Word n -> Word n
rippleCarry x y = go False x y
  where
    go : Bool -> Vect n Bool -> Vect n Bool -> Vect n Bool
    go carry [] [] = Data.Vect.Nil
    go carry (a :: as) (b :: bs) =
      let (s, c) = fullAdder a b carry
       in s :: go c as bs

zero' : Byte
zero' = replicate 8 False

zero : Word n
zero {n} = replicate n False

one : Word (S n)
one {n} = True :: replicate n False

two : Byte
two = rippleCarry one one

three : Byte
three = rippleCarry one two

four : Byte
four = rippleCarry one three

max_stars_repo_name: parsonsmatt/hardware

max_issues_repo_name: parsonsmatt/hardware

max_forks_repo_name: parsonsmatt/hardware


text:
module InsertionProof

import Data.Vect
import congruence
import Data.Fin
import Permutation
import PermCons
import Finite
import DecOrderNat
import LTE_Properties
import SortingWithProof
import InsertionSort
import InsertionHelpers
import PermConsProperties

%access public export
%default total

insertProof : (n : Nat) -> (a : Nat) -> (xs : (Vect n Nat)) ->
              (SortedVect n xs) -> (SortedVect (S n) (a :: xs))

insertProof Z a Nil sorted_Nil =
    ( [a] ** ((Idt (S Z) ** (Refl, (insertHelper8 a)))))

insertProof (S Z) a [x] sorted_x = case (decMin a x) of
    (Left pfLTE) => let
        pf = insertHelper8 x
        in
        ( [a, x] ** ((Idt 2) ** (Refl, (insertHelper1 Z a x Nil pfLTE pf))))
    (Right pfLTE) => let
        pf = insertHelper8 a
        in
        ( [x, a] ** ((Swap 2 FZ) ** (Refl, (insertHelper1 Z x a Nil pfLTE pf))))

insertProof (S (S n)) a xs sorted_xs = let
    {-
    (x :: u) = (fst sorted_xs)
    perm_xs = (fst (snd sorted_xs))
    pf_total_xs = (snd (snd sorted_xs))
    pf_perm_xs = fst pf_total_xs  -- perm_xs xs = (x :: u)
    pf_sorted_xs = snd pf_total_xs

    in

    case (decMin a (head (fst sorted_xs))) of

        (Left pfLTE) => let

            perm = includePerm (S (S n)) (fst (snd sorted_xs)) -- perm_xs as a permutation of a :: xs

            pf1_1 = PermC_prp_1 (S (S n)) a xs (fst (snd sorted_xs))
            -- ( (a :: (applyPerm n Nat perm xs)) = (applyPerm (S n) Nat (includePerm n perm) (a :: xs)))

            pf1_2 = congruence (Vect (S (S n)) Nat) (Vect (S (S (S n))) Nat)
                (fst sorted_xs) (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs)
                (\k => (a :: k)) (sym pf_perm_xs)
            -- a :: fst sorted_xs = a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs

            pf1_3 = sym (trans pf1_2 pf1_1)
            -- applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs) = a :: fst sorted_xs

            pf1_5 = (\k => (insertHelper10 (S n) (fst sorted_xs) k (pf_sorted_xs k)))

            pf1_4 = insertHelper1 (S n) a (head (fst sorted_xs)) (tail (fst sorted_xs)) pfLTE pf1_5

            in
            ((a :: (fst sorted_xs)) ** (perm ** (pf1_3, ?rhs)))

        (Right pfLTE) => ?rhs2
      -}

    (x1 :: v1) = (fst sorted_xs)
    x = (head (fst sorted_xs))
    u = (tail (fst sorted_xs))
    perm_xs = (fst (snd sorted_xs))
    pf_total_xs = (snd (snd sorted_xs))
    pf_perm_xs = fst pf_total_xs  -- perm_xs xs = v
    pf_sorted_xs = snd pf_total_xs
    pf1_5 = (\k => (insertHelper10 (S n) (fst sorted_xs) k (pf_sorted_xs k)))

    -- IsSorted (S (S n)) (head (fst sorted_xs) :: tail (fst sorted_xs)) :=

    --  (k16 : Fin (S (S n))) ->
    --      LTE (index (Data.Fin.Fin (S n) implementation of Prelude.Enum, method pred k16)
    --          (head (fst sorted_xs) :: tail (fst sorted_xs)))
    --              (index k16 (head (fst sorted_xs) :: tail (fst sorted_xs)))

    in

    case (decMin a (head (fst sorted_xs))) of

        (Left pfLTE) =>
        let
            perm = includePerm (S (S n)) (fst (snd sorted_xs))

            pf1_1 = PermC_prp_1 (S (S n)) a xs (fst (snd sorted_xs))
            -- a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs =
            --    applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)

            pf1_2 = congruence (Vect (S (S n)) Nat) (Vect (S (S (S n))) Nat)
                (fst sorted_xs) (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs)
                (\k => (a :: k)) (sym pf_perm_xs)
            -- a :: fst sorted_xs = a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs

            pf1_3 = sym (trans pf1_2 pf1_1)
            -- applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs) = a :: fst sorted_xs

            pf1_4 = insertHelper1 (S n) a (head (fst sorted_xs)) (tail (fst sorted_xs)) pfLTE pf1_5 --pf_sorted_xs

            -- IsSorted (S (S (S n))) (a :: (head (fst sorted_xs) :: tail (fst sorted_xs))) :=

            --(k : Fin (S (S (S n)))) ->
            --    LTE (index (Data.Fin.Fin (S n) implementation of Prelude.Enum, method pred k)
            --        (a :: head (fst sorted_xs) :: tail (fst sorted_xs)))
            --            (index k (a :: head (fst sorted_xs) :: tail (fst sorted_xs)))

            pf1_7 = vect_prp1 (S n) (fst sorted_xs)
            -- fst sorted_xs = head (fst sorted_xs) :: tail (fst sorted_xs)

            pf1_8 = congruence (Vect (S (S n)) Nat) (Vect (S (S (S n))) Nat) (fst sorted_xs)
                ((head (fst sorted_xs)) :: (tail (fst sorted_xs))) (\k => (a :: k)) pf1_7
            -- a :: fst sorted_xs = a :: head (fst sorted_xs) :: tail (fst sorted_xs)

            pf1_6 = insertHelper11 (S (S n)) (a :: head (fst sorted_xs) :: tail (fst sorted_xs))
                (a :: (fst sorted_xs)) (sym pf1_8) pf1_4
            -- IsSorted (S (S (S n))) (a :: (fst sorted_xs)) :=

            --(k : Fin (S (S (S n)))) ->
            --    LTE (index (Data.Fin.Fin (S n) implementation of Prelude.Enum, method pred k) (a :: fst sorted_xs))
            --        (index k (a :: fst sorted_xs))

            in
            ( (a :: (fst sorted_xs)) ** (perm ** (pf1_3, pf1_6)))

        (Right pfLTE) =>

        let

            pf2_1 = insertHelper9 (S n) (head (fst sorted_xs)) (tail (fst sorted_xs)) pf1_5
            -- IsSorted (S n) (tail (fst sorted_xs))

            pf2_2 = PermC_prp_2 (S n) (tail (fst sorted_xs))
            -- applyPerm (S n) Nat (Idt (S n)) (tail (fst sorted_xs)) = tail (fst sorted_xs)

            -- (k : Fin (S n)) ->
            --     LTE (index (Data.Fin.Fin (S n) implementation of Prelude.Enum, method pred k) (tail (fst sorted_xs)))
            --         (index k (tail (fst sorted_xs)))

            sorted_a_xs = insertProof (S n) a (tail (fst sorted_xs))
                ((tail (fst sorted_xs)) ** ((Idt (S n)) ** (pf2_2, pf2_1)))

            perm_a_xs = (fst (snd (sorted_a_xs)))

            perm = CPerm (S (S (S n)))
                (CPerm (S (S (S n))) (includePerm (S (S n)) (fst (snd (sorted_a_xs)))) (Swap (S (S (S n))) FZ) )
                (includePerm (S (S n)) (fst (snd (sorted_xs))))

            pf2_3 = PermC_prp_1 (S (S n)) a xs (fst (snd sorted_xs))
            -- a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs =
            --     applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)

            pf2_4 = congruence (Vect (S (S (S n))) Nat) Nat
                    (a :: (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs))
                    (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))
                     (\k => (index FZ k)) pf2_3
            -- a = index FZ (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))

            pf2_5 = PermC_prp_1 (S (S n))

                       (index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))

                       ((index FZ (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))) ::
                        (tail (tail (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))))

                        (fst (snd (insertProof (S n) a
                                                      (tail (fst sorted_xs))
                                                      (tail (fst sorted_xs) **
                                                      (Idt (S n)) **
                                                      ( (PermC_prp_2 (S n) (tail (fst sorted_xs))),
                                                        (insertHelper9 (S n) (head (fst sorted_xs)) (tail (fst sorted_xs)) pf1_5))))))

            -- now want to prove that x = (index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))

            pf2_6 = congruence (Vect (S (S (S n))) Nat) Nat

                        (a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs)

                        (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))

                        (\us => (index (FS FZ) us))

                        pf2_3

            -- index FZ (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs) =
            --     index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))

            pf2_7 = congruence (Vect (S (S n)) Nat) Nat

                    (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs)

                    (fst (sorted_xs))

                    (\us => ((index FZ) us))

                    pf_perm_xs

             -- index FZ (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs) = index FZ (fst sorted_xs)

            pf2_8 = trans (sym pf2_6) pf2_7

            -- index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)) =
            --    index FZ (fst sorted_xs)

            pf2_10 = insertHelper12 (S n) (fst sorted_xs)

            -- ((index FZ (fst (sorted_xs))) = (head (fst sorted_xs)))

            pf2_11 = trans pf2_8 pf2_10

            -- index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)) =
            -- head (fst sorted_xs)

            pf2_9 = congruence Nat (Vect (S (S (S n))) Nat)

                    (index (FS FZ) (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))

                    (head (fst sorted_xs)) --(index FZ (fst sorted_xs))

                    (\z => (z :: (fst (insertProof (S n)
                          a
                         (tail (fst sorted_xs))
                         (tail (fst sorted_xs) **
                          Idt (S n) **
                          (PermC_prp_2 (S n) (tail (fst sorted_xs)), insertHelper9 (S n) (head (fst sorted_xs)) (tail (fst sorted_xs)) pf1_5))))))

                    pf2_11

            -- ||||||||||||   code is running but taking too long

            {-

            pf_sorted_a_xs_total = (snd (snd sorted_a_xs))

            pf_perm_a_xs = (fst pf_sorted_a_xs_total)

            pf2_12 = congruence Nat (Vect (S (S n)) Nat) a

                (index FZ (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))

                (\s => (s :: (tail (fst sorted_xs))))

                pf2_4

            -- a :: tail (fst sorted_xs) =
            -- index FZ (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)) :: tail (fst sorted_xs)

            -- want to prove
            -- (index FZ (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)) ::
            --     tail (tail (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)))) =
            -- (a :: tail (fst sorted_xs))

            -- check pf2_4

            -- want to prove
            -- (tail (fst sorted_xs)) = (tail (tail (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))))

            pf2_13 = PermC_prp_1 (S (S n)) a xs (fst (snd sorted_xs))

            --  a :: applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs =
            -- applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs)

            pf2_14 = insertHelper13 (S (S n)) a (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs)

            pf2_15 = congruence (Vect (S (S (S n))) Nat) (Vect (S (S n)) Nat)
                (a :: (applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs))
                (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))
                (\v => (tail v))
                pf2_13

            -- applyPerm (S (S n)) Nat (fst (snd sorted_xs)) xs =
            -- tail (applyPerm (S (S (S n))) Nat (includePerm (S (S n)) (fst (snd sorted_xs))) (a :: xs))

            pf2_16 = trans (sym pf_perm_xs) pf2_15
            -}

            in
            (((head (fst sorted_xs)) :: (fst sorted_a_xs)) ** (perm ** ((trans (trans (sym pf2_5) ?rhs21) pf2_9), ?rhs22)))


text:
module Replica.TestConfig.Lexer

import public Text.Lexer
import public Text.Parser

import Data.List
import Data.Strings

%default total

public export
data Token
  = Equals
  | Word String
  | Comment String
  | Space
  | Separator String
  | Path String
  | StringLit String

%default total

lineComment : Lexer
lineComment = Text.Lexer.lineComment (exact "--")

%hide Text.Lexer.lineComment

blockComment : Lexer
blockComment = Text.Lexer.blockComment (exact "{-") (exact "-}")

%hide Text.Lexer.blockComment

spacesOrNewlines : Lexer
spacesOrNewlines = some (space <|> newline)

comment : Lexer
comment = lineComment <|> blockComment

equals : Lexer
equals = is '='

letterLike : Lexer
letterLike = pred (> chr 160)

wordChar : Lexer
wordChar = alphaNum <|> letterLike

word : Lexer
word = some wordChar

separator : Lexer
separator = oneOf "/."

rawTokens : TokenMap Token
rawTokens =
  [ (equals, const Equals)
  , (word, Word)
  , (separator, Separator)
  , (spacesOrNewlines, const Space)
  , (comment, Comment)
  , (stringLit, \s => StringLit (pack . removeEscaped . unpack $ stripQuotes s))
  ]
  where

    stripQuotes : (str : String) -> String
    stripQuotes str = substr 1 (length str `minus` 2) str

    removeEscaped : List Char -> List Char
    removeEscaped ('\\' :: '\'' :: xs) = '\'' :: removeEscaped xs
    removeEscaped ('\\' :: '"'  :: xs) = '"' :: removeEscaped xs
    removeEscaped ('\\' :: 't'  :: xs) = '\t' :: removeEscaped xs
    removeEscaped ('\\' :: 'n'  :: xs) = '\n' :: removeEscaped xs
    removeEscaped ('\\' :: 'r'  :: xs) = '\r' :: removeEscaped xs
    removeEscaped ('\\' :: 'b'  :: xs) = '\b' :: removeEscaped xs
    removeEscaped ('\\' :: 'f'  :: xs) = '\f' :: removeEscaped xs
    removeEscaped ('\\' :: 'v'  :: xs) = '\v' :: removeEscaped xs
    removeEscaped (x            :: xs) = x    :: removeEscaped xs
    removeEscaped []                   = []

export
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex str =
  case lexTo (const False) rawTokens str of
       (tokenData, (l, c, "")) =>
         Right $ (filter (useful . tok) tokenData)
       (_, fail) => Left fail
  where
    useful : Token -> Bool
    useful (Comment c) = False
    useful Space       = False
    useful _ = True

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
module GameServer.Protocol.Tester

import Network.Socket
import Network.Socket.Data

import GameServer.Protocol.Options
import GameServer.Protocol.Messages

runTester : (sock : Socket) -> IO (Either String ())
runTester sock = do
  (buf, len) <- prepareMessage ListGames
  Right res <- sendBuf sock buf len
    | Left err => do sock_free buf ; close sock ; pure (Left $ "failed to send message to server: " ++ show err)
  if res < 0
    then do sock_free buf ; close sock ; pure (Left $ "Error code sending message: " ++ show res)
    else do sock_free buf ; close sock ; pure (Right ())

client : Int -> String -> IO (Either String ())
client port host =
  do Right sock <- socket AF_INET Stream 0
           | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
     res <- connect sock (Hostname host) port
     if res /= 0
       then pure (Left $ "Failed to connect socket with error: " ++ show res)
       else runTester sock

export
tester : Options -> IO (Either String ())
tester (MkOptions port host TesterMode) = client port host
tester _ = pure $ Left "invalid mode for mock tester"

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
data DoorState = DoorClosed | DoorOpen

data DoorResult = OK | Jammed

data DoorCmd : (ty : Type) ->
               DoorState ->
               (ty -> DoorState) ->
               Type where
  Open :     DoorCmd DoorResult DoorClosed (\res => case res of
                                                         OK => DoorOpen
                                                         Jammed => DoorClosed)
  Close :    DoorCmd ()         DoorOpen   (const DoorClosed)
  RingBell : DoorCmd ()         DoorClosed (const DoorClosed)

  Display : String -> DoorCmd () state (const state)

  Pure : (res : ty) -> DoorCmd ty (state_fn res) state_fn
  (>>=) : DoorCmd a state1 state2_fn ->
          ((res: a) -> DoorCmd b (state2_fn res) state3_fn) ->
          DoorCmd b state1 state3_fn

logOpen : DoorCmd DoorResult DoorClosed
                             (\res => case res of
                                           OK => DoorOpen
                                           Jammed => DoorClosed)
logOpen = do Display "Trying to open the door"
             OK <- Open | Jammed => do Display "Jammed"
                                       Pure Jammed
             Display "Success"
             Pure OK

doorProg : DoorCmd () DoorClosed (const DoorClosed)
doorProg = do RingBell
              jam <- Open
              Display "Trying to open the door"
              case jam of
                   OK => do Display "Glad To Be Of Service"
                            Close
                   Jammed => Display "Door Jammed"

doorProg2 : DoorCmd () DoorClosed (const DoorClosed)
doorProg2 = do RingBell
               OK <- Open | Jammed => Display "Door Jammed"
               Display "Glad To Be Of Service"
               Close
               OK <- Open | Jammed => Display "Door Jammed"
               Display "Glad To Be Of Service"
               Close


text:
foo : Maybe Int -> Bool -> Int
foo Nothing _ = 42
foo Nothing True = 94
foo (Just x) _ = x
foo Nothing False = 42


text:
module IdrisWeb.CGI.CgiTypes

import Effects
import Decidable.Equality
import IdrisWeb.DB.SQLite.SQLiteNew
import IdrisWeb.Session.Session
%access public
-- Types used by the CGI module

-- Simple type synonym for a list of key value pairs
public
Vars : Type
Vars = List (String, String)

-- CGI Concrete effect sig
public
CGI : Type -> EFFECT

FormHandler : List EFFECT -> Type
FormHandler effs = Eff IO effs ()

public
UserForm : Type

-- Information passed by CGI
public
record CGIInfo : Type where
       CGIInf : (GET : Vars) ->
                (POST : Vars) ->
                (Cookies : Vars) ->
                (UserAgent : String) ->
                (Headers : String) ->
                (Output : String) ->
                (FormNumber : Nat) -> CGIInfo

-- Type of user-defined
public
CGIProg : List EFFECT -> Type -> Type

-- States in the state machine
public
data CGIStep  = Initialised
              | TaskRunning
              | TaskCompleted
              | HeadersWritten
              | ContentWritten
              -- Perhaps another after any cleanup?

-- Data type representing an initialised CGI script
public
data InitialisedCGI : CGIStep -> Type where
  ICgi : CGIInfo -> InitialisedCGI s

{- Serialisable Web Effects -}

data WebEffect = CgiEffect
               | SqliteEffect
               | SessionEffect

cgiNotSqlite : CgiEffect = SqliteEffect -> _|_
cgiNotSqlite refl impossible

cgiNotSession : CgiEffect = SessionEffect -> _|_
cgiNotSession refl impossible

sqliteNotSession : SqliteEffect = SessionEffect -> _|_
sqliteNotSession refl impossible

instance DecEq WebEffect where
  decEq CgiEffect CgiEffect = Yes refl
  decEq SqliteEffect SqliteEffect = Yes refl
  decEq CgiEffect SqliteEffect = No cgiNotSqlite
  decEq SqliteEffect CgiEffect = No (negEqSym cgiNotSqlite)
  decEq CgiEffect SessionEffect = No cgiNotSession
  decEq SessionEffect CgiEffect = No (negEqSym cgiNotSession)
  decEq SessionEffect SessionEffect = Yes refl
  decEq SqliteEffect SessionEffect = No sqliteNotSession
  decEq SessionEffect SqliteEffect = No (negEqSym sqliteNotSession)

instance Eq WebEffect where
  (==) CgiEffect CgiEffect = True
  (==) SqliteEffect SqliteEffect = True
  (==) SessionEffect SessionEffect = True
  (==) _ _ = False

instance Show WebEffect where
  show CgiEffect = "cgi"
  show SqliteEffect = "sqlite"
  show SessionEffect = "session"

total
interpWebEffect : WebEffect -> EFFECT
interpWebEffect CgiEffect = (CGI (InitialisedCGI TaskRunning))
interpWebEffect SqliteEffect = (SQLITE ())
interpWebEffect SessionEffect = (SESSION (SessionRes SessionUninitialised))

interpWebEffects : List WebEffect -> List EFFECT
interpWebEffects [] = []
interpWebEffects (x :: xs) = interpWebEffect x :: interpWebEffects xs

{- Allowed form types -}

data FormTy = FormString
            | FormInt
            | FormBool
            | FormFloat
            | FormList FormTy

total
interpFormTy : FormTy -> Type
interpFormTy FormString = String
interpFormTy FormInt = Int
interpFormTy FormBool = Bool
interpFormTy FormFloat = Float
interpFormTy (FormList a) = List (interpFormTy a)

instance Eq FormTy where
  (==) FormString FormString = True
  (==) FormInt FormInt = True
  (==) FormBool FormBool = True
  (==) FormFloat FormFloat = True
  (==) (FormList a) (FormList b) = (a == b)
  (==) _ _ = False

instance Show FormTy where
  show FormString = "str"
  show FormInt = "int"
  show FormBool = "bool"
  show FormFloat = "float"
  show (FormList a) = "list_" ++ (show a)

formstringNotFormInt : FormString = FormInt -> _|_
formstringNotFormInt refl impossible
formstringNotFormBool : FormString = FormBool -> _|_
formstringNotFormBool refl impossible
formstringNotFormFloat : FormString = FormFloat -> _|_
formstringNotFormFloat refl impossible
formstringNotFormList : FormString = (FormList a) -> _|_
formstringNotFormList refl impossible
formintNotFormBool : FormInt = FormBool -> _|_
formintNotFormBool refl impossible
formintNotFormFloat : FormInt = FormFloat -> _|_
formintNotFormFloat refl impossible
formintNotFormList : FormInt = (FormList a) -> _|_
formintNotFormList refl impossible
formboolNotFormFloat : FormBool = FormFloat -> _|_
formboolNotFormFloat refl impossible
formboolNotFormList : FormBool = (FormList a) -> _|_
formboolNotFormList refl impossible
formfloatNotFormList : FormFloat = (FormList a) -> _|_
formfloatNotFormList refl impossible

lemma_fl_injective : {a : FormTy} -> {b : FormTy} -> (FormList a = FormList b) -> a = b
lemma_fl_injective refl = refl

lemma_a_not_b : {a : FormTy} -> {b : FormTy} -> ((a = b) -> _|_) -> ((FormList a = FormList b) -> _|_)
lemma_a_not_b p h = p (lemma_fl_injective h)

instance DecEq FormTy where
  decEq FormString FormString = Yes refl
  decEq FormString FormInt = No formstringNotFormInt
  decEq FormString FormBool = No formstringNotFormBool
  decEq FormString FormFloat = No formstringNotFormFloat
  decEq FormString (FormList a) = No formstringNotFormList
  decEq FormInt FormString = No (negEqSym formstringNotFormInt)
  decEq FormInt FormInt = Yes refl
  decEq FormInt FormBool = No formintNotFormBool
  decEq FormInt FormFloat = No formintNotFormFloat
  decEq FormInt (FormList a) = No formintNotFormList
  decEq FormBool FormString = No (negEqSym formstringNotFormBool)
  decEq FormBool FormInt = No (negEqSym formintNotFormBool)
  decEq FormBool FormBool = Yes refl
  decEq FormBool FormFloat = No formboolNotFormFloat
  decEq FormBool (FormList a) = No formboolNotFormList
  decEq FormFloat FormString = No (negEqSym formstringNotFormFloat)
  decEq FormFloat FormInt = No (negEqSym formintNotFormFloat)
  decEq FormFloat FormBool = No (negEqSym formboolNotFormFloat)
  decEq FormFloat FormFloat = Yes refl
  decEq FormFloat (FormList a) = No formfloatNotFormList
  decEq (FormList a) FormString = No (negEqSym formstringNotFormList)
  decEq (FormList a) FormInt = No (negEqSym formintNotFormList)
  decEq (FormList a) FormBool = No (negEqSym formboolNotFormList)
  decEq (FormList a) FormFloat = No (negEqSym formfloatNotFormList)
  decEq (FormList a) (FormList b) with (decEq a b)
    decEq (FormList a) (FormList a) | Yes refl = Yes refl
    decEq (FormList a) (FormList b) | No p = No (lemma_a_not_b p)

MkHandlerFnTy : Type
MkHandlerFnTy = (List FormTy, List WebEffect)

mkHandlerFn' : List FormTy -> List WebEffect -> Type
mkHandlerFn' [] effs = FormHandler (interpWebEffects effs)
mkHandlerFn' (x :: xs) effs = Maybe (interpFormTy x) -> mkHandlerFn' xs effs

mkHandlerFn : MkHandlerFnTy -> Type
mkHandlerFn (tys, effs) = mkHandlerFn' tys effs

public
HandlerFn : Type
HandlerFn = (ft ** (mkHandlerFn ft, String))

public
HandlerList : Type
HandlerList = List HandlerFn

using (G : List FormTy, E : List WebEffect)
  data FormRes : List FormTy -> List WebEffect -> Type where
    FR : Nat -> List FormTy -> List WebEffect -> String -> FormRes G E

  data FnElem : mkHandlerFn ((reverse G), E) -> HandlerList -> Type where
       FnHere : {xs : HandlerList, f : mkHandlerFn ((reverse G), E)} ->
              FnElem f ((((reverse G), E) ** (f, fStr)) :: xs)
       FnThere : {xs : HandlerList, f : mkHandlerFn ((reverse G), E)} ->
               FnElem f xs -> FnElem f (x :: xs)

  findFn : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth
  findFn Z ctxt goal = Refine "FnHere" `Seq` Solve
  findFn (S n) ctxt goal = GoalType "FnElem"
            (Try (Refine "FnHere" `Seq` Solve)
                 (Refine "FnThere" `Seq` (Solve `Seq` findFn n ctxt goal)))

  getString' : (f : mkHandlerFn ((reverse G), E)) ->
               (fs : HandlerList) -> FnElem f fs -> String
  getString' f ((_ ** (_, n)) :: _) FnHere = n
  getString' f (_ :: fs) (FnThere p) = getString' f fs p

  data Form : Effect where
    AddTextBox : (label : String) ->
                 (fty : FormTy) ->
                 (Maybe (interpFormTy fty)) ->
                 Form (FormRes G E) (FormRes (fty :: G) E) ()

    AddHidden  : (fty : FormTy) ->
                 (interpFormTy fty) ->
                 Form (FormRes G E) (FormRes (fty :: G) E) ()

    AddSelectionBox : (label : String) ->
                      (fty : FormTy) ->
                      (vals : Vect m (interpFormTy fty)) ->
                      (names : Vect m String) ->
                      Form (FormRes G E) (FormRes (fty :: G) E) ()

    AddRadioGroup : (label : String) ->
                    (fty : FormTy) ->
                    (vals : Vect m (interpFormTy fty)) ->
                    (names : Vect m String) ->
                    (default : Int) ->
                    Form (FormRes G E) (FormRes (fty :: G) E) ()

    AddCheckBoxes : (label : String) ->
                    (fty : FormTy) ->
                    (vals : Vect m (interpFormTy fty)) ->
                    (names : Vect m String) ->
                    (checked_boxes : Vect m Bool) ->
                    Form (FormRes G E) (FormRes ((FormList fty) :: G) E) ()

    UseEffects : (effs : List WebEffect) ->
                 Form (FormRes G E) (FormRes G effs) ()

    Submit : (mkHandlerFn ((reverse G), E)) ->
             String ->
             Form (FormRes G E) (FormRes [] []) String

  FORM : Type -> EFFECT
  FORM t = MkEff t Form

  addTextBox : String ->
               (fty : FormTy) -> -- Data type
               (Maybe (interpFormTy fty)) ->  -- Default data value (optional)
               EffM m [FORM (FormRes G E)] [FORM (FormRes (fty :: G) E)] ()
  addTextBox label ty val = (AddTextBox label ty val)

  addHidden : (fty : FormTy) ->
              (interpFormTy fty) -> -- Default value
              EffM m [FORM (FormRes G E)] [FORM (FormRes (fty :: G) E)] ()
  addHidden ty val = (AddHidden ty val)

  addSelectionBox : String ->
                    (fty : FormTy) ->
                    (vals : Vect j (interpFormTy fty)) ->
                    (names : Vect j String) ->
                    EffM m [FORM (FormRes G E)] [FORM (FormRes (fty :: G) E)] ()
  addSelectionBox label ty vals names = (AddSelectionBox label ty vals names)

  addRadioGroup : String ->
                  (fty : FormTy) ->
                  (vals : Vect j (interpFormTy fty)) ->
                  (names : Vect j String) ->
                  (default : Int) ->
                  EffM m [FORM (FormRes G E)] [FORM (FormRes (fty :: G) E)] ()
  addRadioGroup label ty vals names default = (AddRadioGroup label ty vals names default)

  addCheckBoxes : (label : String) ->
                  (fty : FormTy) ->
                  (vals : Vect j (interpFormTy fty)) ->
                  (names : Vect j String) ->
                  (checked_boxes : Vect j Bool) ->
                  EffM m [FORM (FormRes G E)] [FORM (FormRes ((FormList fty) :: G) E)] ()
  addCheckBoxes label ty vals names checked = (AddCheckBoxes label ty vals names checked)

  addSubmit : (f :  mkHandlerFn ((reverse G), E)) ->
              (fns : HandlerList) ->
              {default tactics { applyTactic findFn 100; solve; }
                prf : FnElem f fns} ->
              EffM m [FORM (FormRes G E)] [FORM (FormRes [] [])] String
  addSubmit f handlers {prf} = (Submit f name)
    where name : String
          name = getString' f handlers prf

  useEffects : (effs : List WebEffect) ->
               EffM m [FORM (FormRes G E)] [FORM (FormRes G effs)] ()
  useEffects effs = (UseEffects effs)

UserForm = Eff id [FORM (FormRes [] [])] String -- Making a form is a pure function (atm)

-- CGI Effect
public
data Cgi : Effect where
  -- Individual functions of the effect

  -- Action retrieval
  GetInfo : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) CGIInfo

  -- Output a string
  OutputData : String -> Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) ()

  -- Retrieve the GET variables
  GETVars : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) Vars

  -- Retrieve the POST variables
  POSTVars : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) Vars

  -- Retrieve the cookie variables
  CookieVars : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) Vars

  -- Lookup a variable in the GET variables
  QueryGetVar : String -> Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) (Maybe String)

  -- Lookup a variable in the POST variables
  QueryPostVar : String -> Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) (Maybe String)

  -- Lookup a cookie from the cookie variables
  QueryCookieVar : String -> Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) (Maybe String)

  -- Retrieves the current output
  GetOutput : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) String

  -- Retrieves the headers
  GetHeaders : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) String

  -- Flushes the headers to StdOut
  FlushHeaders : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) ()

  -- Flushes output to StdOut
  Flush : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) ()

  -- Initialise the internal CGI State
  Init : Cgi () (InitialisedCGI Initialised) ()

  -- Transition to task started state
  StartRun : Cgi (InitialisedCGI Initialised) (InitialisedCGI TaskRunning) ()

  -- Transition to task completed state
  FinishRun : Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskCompleted) ()

  -- Write headers, transition to headers written state
  WriteHeaders : Cgi (InitialisedCGI TaskCompleted) (InitialisedCGI HeadersWritten) ()

  -- Write content, transition to content written state
  WriteContent : Cgi (InitialisedCGI HeadersWritten) (InitialisedCGI ContentWritten) ()

  -- Add cookie
  -- TODO: Add expiry date in here once I've finished the basics
  SetCookie : String -> String -> {- Date -> -}
              Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) ()

  -- Run the user-specified action
  RunAction : Env IO (CGI (InitialisedCGI TaskRunning) :: effs) ->
              CGIProg effs a ->
              Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) a

  -- Write a form to the web page
  AddForm : UserForm ->
            Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) ()

  -- Attempts to handle a form, given a list of available handlers
  HandleForm : HandlerList ->
               Cgi (InitialisedCGI TaskRunning) (InitialisedCGI TaskRunning) Bool

CGI t = MkEff t Cgi

CGIProg effs a = Eff IO (CGI (InitialisedCGI TaskRunning) :: effs) a

interpFnTy : Vect n FormTy -> Type
interpFnTy tys = interpFnTy' (reverse tys)
  where interpFnTy' : Vect n FormTy -> Type
        interpFnTy' [] = () -- TODO: should be form effect stuff here
        interpFnTy' (x :: xs) = interpFormTy x -> interpFnTy' xs

SerialisedForm : Type
SerialisedForm = String

data PopFn : Type where
  PF : (w_effs : List WebEffect) ->
       (effs : List EFFECT) -> (env : Effects.Env IO effs) ->
       Eff IO effs () -> PopFn

{-
test1 : Maybe String -> Maybe Int -> FormHandler [CGI (InitialisedCGI TaskRunning)]
test1 (Just name) (Just age) = do
  --output $ "Your name is " ++ name
  --output $ " and you are " ++ (show age) ++ " years old!"
  pure ()

test2 : Maybe String -> Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning), SQLITE ()]
test2 (Just name) (Just name2) = do
  --output $ "Your name is " ++ name
  --output $ " and your last name is " ++ name2
  pure ()
-}
{-
fnList : HandlerList
fnList = [(([FormString, FormInt], [CgiEffect]) ** (test1, "test1")),
          (([FormString, FormString], [CgiEffect, SqliteEffect]) ** (test2, "test2"))]
-}

-----
----- END NEW STUFF
-----

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
-- -------------------------------------------------------------- [ Freyja.idr ]
-- Module    : Freyja.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Core Data Types.
module Freyja

import public Data.DList

import public GRL.Lang.GLang

import public Edda

import public Freyja.Common

%access public export
-- ----------------------------------------------------------- [ Element Types ]

-- ---------------------------------------------------------------- [ MetaData ]

record Metadata where
  constructor MkMData
  aliases   : List EddaString
  tags      : List EddaString
  authors   : List EddaString
  auditors  : List EddaString
  created   : String
  modified  : String
  evaluated : String
  ident     : String

implementation Show Metadata where
  show (MkMData as bs cs ds e f g i) = unwords
    [ "MkMData", show as, show bs, show cs, show ds
    , show e, show f, show g, show i]

-- ------------------------------------------------------------ [ Requirements ]

record Requirement (x : RTy) where
  constructor MkReq
  ty   : RTy
  name : EddaString
  desc : EddaBody

implementation Show (Requirement ty) where
  show (MkReq typ n d) = unwords
    [ "MkReq", show typ, show n, show d]

-- ---------------------------------------------------------------- [ Problems ]

record Problem where
  constructor MkProblem
  name : EddaString
  desc : EddaBody
  reqs : DList RTy Requirement rs

implementation Show Problem where
  show (MkProblem n d rs) = unwords
    ["MkProblem", show n, show d, showDList show rs]

-- ------------------------------------------------------------------ [ Models ]

record Model (x : MTy) where
  constructor MkModel
  name  : EddaString
  ty    : MTy
  desc  : EddaBody
  model : String

implementation Show (Model ty) where
  show (MkModel n typ d m) = unwords
    ["MkModel", show n, show typ, show d, show m]

-- ----------------------------------------------------------------- [ Affects ]

record Affect where
  constructor MkAffect
  cval : CValue
  req  : Requirement ty
  desc : Maybe (EddaBody)

implementation Show Affect where
  show (MkAffect c r d) = unwords
    ["MkAffect", show c, show r, show d]

-- ------------------------------------------------------------------ [ Traits ]

record Trait (x : TTy) where
  constructor MkTrait
  ty : TTy
  name : EddaString
  desc : EddaBody
  sval : SValue
  affects : List Affect

implementation Show (Trait ty) where
  show (MkTrait typ n d s as) = unwords
    ["MkTrait", show typ, show n, show d, show s, show as]

-- ---------------------------------------------------------------- [ Property ]

record Property where
  constructor MkProperty
  name   : EddaString
  desc   : EddaBody
  traits : DList TTy Trait ts

implementation Show (Property) where
  show (MkProperty n d ts) = unwords
    ["MkProperty", show n, show d, showDList show ts]

-- ---------------------------------------------------------------- [ Solution ]

record Solution where
  constructor MkSolution
  name       : EddaString
  desc       : EddaBody
  models     : DList MTy Model ms
  properties : List Property

implementation Show Solution where
  show (MkSolution n d ms ps) = unwords
    ["MkSolution", show n, show d, showDList show ms, show ps]

-- ----------------------------------------------------------------- [ Context ]

record Context where
  constructor MkContext
  name : EddaString
  desc : EddaBody

implementation Show Context where
  show (MkContext n d) = unwords
    ["MkContext", show n, show d]

-- ------------------------------------------------------------------- [ Study ]

record Study where
  constructor MkStudy
  name : EddaString
  before : EddaBody
  after  : EddaBody

implementation Show Study where
  show (MkStudy n b a) = unwords
    ["MkStudy", show b, show b, show a]

-- ---------------------------------------------------------------- [ Relation ]

record Relation (x : LTy) where
  constructor MkRelation
  ty    : LTy
  ident : String
  desc  : Maybe EddaBody

implementation Show (Relation ty) where
  show (MkRelation typ i d) = unwords
    ["MkRelation", show typ, show i, show d]

-- ------------------------------------------------------------- [ Pattern Doc ]

record PatternDoc where
  constructor MkPDoc
  name      : EddaString
  summary   : EddaBody
  mdata     : Metadata
  context   : Context
  problem   : Problem
  solution  : Solution
  evidence  : EddaBody
  studies   : List Study
  relations : DList LTy Relation ls

implementation Show PatternDoc where
  show (MkPDoc n d m c p s e ss rs) = unwords
      [ "MkPDoc"
      , show n, show d, show m, show c
      , show p, show s, show e, show ss
      , showDList show rs]

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module LinearAlgebra

import MultiSolver
import Data.Matrix.Numeric
import Data.Vect
import Data.Fin
import Data.Matrix
import ZZ
import Rationals

%access public export

-- Some auxillary functions for elementary operations

--Euclid's div
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

--Nat to Fin (modular values)
tofinNat: (a: Nat) -> (n: Nat) -> Fin n
tofinNat Z (S j) = FZ
tofinNat (S k) (S j) = case lte (S k) (S j) of
                True => FS (tofinNat k j)
                False =>  (tofinNat (snd(Eucl (S k) (S j))) (S j))

FST: ZZPair -> ZZ
FST (a, b) = a

Pred: Nat -> Nat
Pred Z = Z
Pred (S k) = k

--Takes the first m elements from a vector
Vecttake : (m:Nat)->Vect n elem->Vect m  elem
Vecttake Z xs = []
Vecttake (S k) (x::xs) = x::(Vecttake k xs)

SimpleCast:  (v1:(Vect (k+ (S Z)) elem)) ->( Vect (S k) elem)  -- necessary for type matching, taken from Shafil's code
SimpleCast {k} v1 = (Vecttake (S k) v1)

RowN: Matrix n n ZZPair -> (k: Nat) -> Vect n ZZPair -- returns the nth row (indexing from 0)
RowN {n} x k = Data.Vect.index (tofinNat k n) x

ij: Matrix n n ZZPair -> (i: Nat) -> (j: Nat) -> ZZPair
ij {n} x i j = Data.Vect.index (tofinNat j n) (RowN x i)

ColumnN: Matrix n n ZZPair -> (k: Nat) -> Vect n ZZPair --returns the nth column (indexing from 0)
ColumnN {n} x k = Data.Vect.index (tofinNat k n) (transpose x)

VectorSubtract: (n: Nat) -> (a: Vect n ZZPair) -> (b: Vect n ZZPair) -> (Vect n ZZPair) --subtracts components
VectorSubtract n a b = a - b

ScaleVect: (n: Nat) -> (Vect n ZZPair) -> (c: ZZPair) -> (Vect n ZZPair) --scales by a rational
ScaleVect n xs c = c <# xs

--returns the row scaled by a constant minus another vector (used in row operations)

axpy: (n: Nat) -> (a: Vect n ZZPair) -> (b: Vect n ZZPair) -> (c: ZZPair) -> (Vect n ZZPair)
axpy n a b c = VectorSubtract (n) (a) (ScaleVect (n) b c)

--Auxillary functions, will be used in the Gauss-Jordan process

First_k_rows: (n: Nat) -> (x: Matrix n n ZZPair) -> (k: Nat) -> Matrix k n ZZPair
First_k_rows n x Z = []
First_k_rows n x (S k) = [RowN x k] ++ (First_k_rows n x k)

Last_k_rows: (n: Nat) -> (x: Matrix n n ZZPair) -> (k: Nat) -> Matrix k n ZZPair
Last_k_rows n x k = reverse (First_k_rows n (reverse x) k)

First_k_rows_from_RowP: (n: Nat) -> (x: Matrix n n ZZPair) -> (p: Nat) -> (k: Nat) -> Matrix k n ZZPair
First_k_rows_from_RowP n x p Z = []
First_k_rows_from_RowP n x p (S k) = SimpleCast ((First_k_rows_from_RowP n x p k) ++ [RowN x (p+k)])

-- A section on elementary operations (to eventually implement the Gauss-Jordan process)

-- Scales a row by dividing it by a rational number.

ScaleRow: (n: Nat) -> Matrix n n ZZPair -> (row_a: Nat) -> (c: ZZPair) -> Matrix n n ZZPair
ScaleRow n x row_a c = replaceAt (tofinNat row_a n) (ScaleVect n (RowN x row_a) c) (x)

-- Swaps two rows in a matrix (indexing from 0)

SwapRows: (n: Nat) -> Matrix n n ZZPair -> (a: Nat) -> (b: Nat) -> Matrix n n ZZPair
SwapRows n x a b = replaceAt (tofinNat b n) (RowN x a) (replaceAt (tofinNat a n) (RowN x b) (x))

-- Performs an elementary row operation, subtracts from row a the row b scaled by c

RowOperation: (n: Nat) -> Matrix n n ZZPair -> (a: Nat) -> (b: Nat) -> (c: ZZPair) -> Matrix n n ZZPair
RowOperation n x a b c = replaceAt (tofinNat a n) (axpy n (RowN x a) (RowN x b) c) (x)

-- Makes the kth number in Row A zero by subtracting a scaling of Row B (for upper triangularizing)
-- As usual, indexing starts from 0

MakeElementZero: (n: Nat) -> (x: Matrix n n ZZPair) -> (row_a : Nat) -> (row_b : Nat) -> (pos : Nat) -> Matrix n n ZZPair
MakeElementZero n x row_a row_b pos = case (FST(ij x row_a pos)) of
                                      (Pos Z) => x
                                      (Pos (S k)) => case ((fst (ij x row_b pos))) of
                                                                          (Pos Z) => (SwapRows n x row_a row_b)
                                                                          (Pos (S k)) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                                                          (NegS k) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                      (NegS k) => case ((fst (ij x row_b pos))) of
                                                                          (Pos Z) => (SwapRows n x row_a row_b)
                                                                          (Pos (S k)) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )
                                                                          (NegS k) => (RowOperation n x row_a row_b (divZZ (ij x row_a pos) (ij x row_b pos)) )

-- Explanation: We want to transform the element x[row_a][pos] into zero by a row operation. There are a few different cases
--              1. If x[row_a][pos] is already zero, nothing needs to be done.
--              2. If not, we scale row_b appropriately and do a row operation (A -> A - cB)
--              3. If x[row_b][pos] is zero, however, no row operation will work. We simply swap the
--                 row_a and row_b here; then, x[row_a][pos] will become zero.

-- This algorithm is important to make a matrix upper-triangular.

MakeColumnZero: (n: Nat) -> (x: Matrix n n ZZPair) -> (col : Nat) -> (iter : Nat) -> Matrix n n ZZPair
MakeColumnZero n x col Z = x
MakeColumnZero n x col (S k) = case (isLTE (S k) col) of
                                   (Yes prf) => x
                                   (No contra) => (MakeColumnZero n (MakeElementZero n x (S k) col col) col k)

-- This function turns a column into what it should be in upper-triangular form by adding in the necessary zeros.
-- iter is a variable to induct on (trick courtesy Sriram)
-- When using this, make sure to set "iter" as n-1 (1 less than the number of rows)

-- The next step here is to use the above function to make a matrix upper triangular. This can be
-- done by inducting on the number of columns.

-- A helper function, which recursively fills zeros into columns.

UpperTriangularize: (x: Matrix n n ZZPair) -> (iter: Nat) -> Matrix n n ZZPair
UpperTriangularize {n} x Z = (MakeColumnZero n x Z (Pred n)) -- Column Zero is the base case
UpperTriangularize {n} x (S k) = (MakeColumnZero n (UpperTriangularize x k) (S k) (Pred n))

-- Enter a matrix, get the upper triangular form.

UpperTriangularForm: (x: Matrix n n ZZPair) -> Matrix n n ZZPair
UpperTriangularForm {n} x = UpperTriangularize x (Pred (Pred n))

-- The function below converts a matrix into a Diagonal Form (note that this is NOT diagonalization!) by converting to upper-triangular
-- form, transposing that (to get a lower triangular matrix) and finding the upper-triangular form of the tranpose. This is going to be useful
-- as it is the next step of the Gauss-Jordan algorithm (what's next: divide out the rows to get an identity matrix; an inverse can be
-- found this way by applying all the above row operations to an identity matrix.

DiagonalForm: (x: Matrix n n ZZPair) -> Matrix n n ZZPair
DiagonalForm {n} x = UpperTriangularForm (transpose (UpperTriangularForm x))

-- once a matrix is in diagonal form, we can convert it to the identity by dividing each row by its only nonzero element

ReduceRow: (x: Matrix n n ZZPair) -> (iter: Nat) -> Matrix n n ZZPair
ReduceRow {n = n} x Z = case (FST(ij x Z Z)) of
                             (Pos Z) => x
                             (Pos (S k)) => ScaleRow n x Z (divZZ (1,1) (ij x 0 0))
                             (NegS k) => ScaleRow n x Z (divZZ (1,1) (ij x 0 0))
ReduceRow {n = n} x (S k) = case ((FST(ij x (S k) (S k)))) of
                                 (Pos Z) => x
                                 (Pos (S k)) => ScaleRow n (ReduceRow x k) (S k) (divZZ (1,1) (ij x (S k) (S k)))
                                 (NegS k) => ScaleRow n (ReduceRow x k) (S k) (divZZ (1,1) (ij x (S k) (S k)))

-- This function converts any matrix into the identity. Applying the row operations which do this to an identity matrix would convert it
-- to an inverse. If we want to solve linear equations, this would be enough (for proof, we would need to prove that AA^-1 = I).
-- Another possibility would be to use back-substitution from the upper-triangular form. This would be simpler because the function
-- GeneralEqSolver from Linear.idr could be modified a bit to solve n successive 1 - variable equations, and generating a proof would
-- be easier.

TotalReduce: (x: Matrix n n ZZPair) -> (Matrix n n ZZPair)
TotalReduce {n} x = ReduceRow (DiagonalForm x) (Pred n)

-- Once we have a matrix in diagonal (or even upper triangular) form, we can calculate the magnitude of its determinant by multiplying
-- the diagonal elements.

DiagonalProductHelper: (x: Matrix n n ZZPair) -> (iter: Nat) -> ZZPair
DiagonalProductHelper x Z = (ij x 0 0)
DiagonalProductHelper x (S k) = (ij x (S k) (S k)) * (DiagonalProductHelper x k)

-- Calculates the determinant up to the sign ( (-1)^n to be implemented later ). Effectively, this calculates the "volume" of n-vectors in
-- n-dimensional Euclidean space.

DetUpToSign: (x: Matrix n n ZZPair) -> ZZPair
DetUpToSign {n} x = simplifyRational (DiagonalProductHelper (DiagonalForm x) (Pred n))

-- I propose a simple way to calculate the sign factor: in the conversion to upper-triangular form, the last column is untouched
-- except for by Row Swapping. The last column in upper - triangular form is thus a permutation of the last column of the original
-- matrix. We just need to check if this is an odd or even permutation (simplification of all elements of the matrices will be
-- necessary to ensure that this can be carried out) and multiply appropriately.

-- A short section consisting of functions used to simplify a matrix of ZZPairs

ChangeElementRow: (n: Nat) -> Vect n ZZPair -> (pos: Nat) -> (new: ZZPair) -> Vect n ZZPair
ChangeElementRow n xs pos new = replaceAt (tofinNat pos n) (new) xs

ChangeElementMatrix: (n: Nat) -> (x: Matrix n n ZZPair) -> (i: Nat) -> (j: Nat) -> (new: ZZPair) -> Matrix n n ZZPair
ChangeElementMatrix n x i j new = replaceAt (tofinNat i n) (ChangeElementRow n (RowN x i) j new) (x)

SimplifyElement: (n: Nat) -> (x: Matrix n n ZZPair) -> (i: Nat) -> (j: Nat) -> Matrix n n ZZPair
SimplifyElement n x i j = ChangeElementMatrix n x i j (simplifyRational (ij x i j))

simplifyRowHelper: (n: Nat) -> (x: Matrix n n ZZPair) -> (row: Nat) -> (iter: Nat) -> Matrix n n ZZPair
simplifyRowHelper n x row Z = SimplifyElement n x row Z
simplifyRowHelper n x row (S k) = SimplifyElement n (simplifyRowHelper n x row k) row (S k)

simplifyRow: (n: Nat) -> (x: Matrix n n ZZPair) -> (row: Nat) -> (Matrix n n ZZPair)
simplifyRow n x row = simplifyRowHelper n x row (Pred n)

simplifyMatrixHelper: (n: Nat) -> (x: Matrix n n ZZPair) -> (iter: Nat) -> Matrix n n ZZPair
simplifyMatrixHelper n x Z = simplifyRow n x Z
simplifyMatrixHelper n x (S k) = simplifyMatrixHelper n (simplifyMatrixHelper n x k) (S k)

simplifyMatrix: (x: Matrix n n ZZPair) -> (Matrix n n ZZPair) -- simplifies all the rationals in the matrix, takes a while to run
simplifyMatrix {n} x = simplifyMatrixHelper n x (Pred n)


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.String
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.ExprSearch
import TTImp.TTImp
import TTImp.TTImp.Functor

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))

buildCodeAction : Name -> URI -> Range -> String -> CodeAction
buildCodeAction name uri range str =
  MkCodeAction
    { title       = "Expression search on \{show $ dropAllNS name} as ~ \{strSubstr 0 50 str} ..."
    , kind        = Just RefactorRewrite
    , diagnostics = Just []
    , isPreferred = Just False
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [MkTextEdit range str])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , 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
  logI ExprSearch "Checking for \{show params.textDocument.uri} at \{show params.range}"
  withSingleLine ExprSearch params (pure []) $ \line => do
    withMultipleCache ExprSearch params ExprSearch $ do

      fuel <- gets LSPConf searchLimit
      nameLocs <- gets MD nameLocMap
      let col = params.range.start.character
      let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
        | Nothing => do logD ExprSearch "No name found at \{show line}:\{show col}}"
                        pure []
      logD ExprSearch "Found name \{show name}"

      defs <- get Ctxt
      let context = defs.gamma
      toBrack <- gets Syn (elemBy (\x, y => dropNS x == dropNS y) name . bracketholes)
      let bracket = the (IPTerm -> IPTerm) $ if toBrack then addBracket replFC else id
      solutions <-
        case !(lookupDefName name context) of
             [(n, nidx, Hole locs _)] =>
               catch (do searchtms <- exprSearchN replFC fuel name []
                         traverse (map (show . bracket) . pterm . map defaultKindedName . dropLams locs) searchtms)
                     (\case Timeout _ => do logI ExprSearch "Timed out"
                                            pure []
                            err => do logC ExprSearch "Unexpected error while searching"
                                      throw err)
             [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] => case holeInfo pi of
               NotHole => do logD ExprSearch "\{show name} is not a metavariable"
                             pure []
               SolvedHole locs => do
                 let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm)
                 itm <- resugar env tm'
                 pure [show $ bracket itm]
             _ => do logD ExprSearch "\{show name} is not a metavariable"
                     pure []

      let range = MkRange (uncurry MkPosition nstart) (uncurry MkPosition nend)
      let actions = buildCodeAction name params.textDocument.uri range <$> solutions
      pure [(cast loc, actions)]


text:
-- -*- idris-interpreter-flags: ("-p" "contrib") -*-

import Data.ZZ
import Data.Vect

data CountChange : ZZ -> Vect n ZZ -> Type where
     C1  : CountChange 0 k        -- 1 way
     C0a : CountChange (NegS a) k -- 0 ways
     C0b : CountChange a []       -- 0 ways
     CC  : CountChange (a - (head k)) k -> CountChange a (tail k) -> CountChange a k -- x + y ways

count : CountChange x y -> Nat
count C1       = 1
count C0a      = 0
count C0b      = 0
count (CC x y) = count x + count y

cc_2_by_1 : CountChange 2 [1]
cc_2_by_1 = CC (CC C1 C0b) C0b

cc_2_by_2_1 : CountChange 2 [2,1]
cc_2_by_2_1 = CC C1 (CC (CC C1 C0b) C0b)

cc_11_by_50_25_10_5_1 : CountChange 11 [50,25,10,5,1]
cc_11_by_50_25_10_5_1 = ?try_it
{- ex 1.14 'tree', generated by 'C-c-a'
cc_11_by_50_25_10_5_1 = CC
                          C0a
                          (CC
                            C0a
                            (CC
                              (CC
                                C0a
                                (CC
                                  C0a
                                  (CC
                                    C1
                                    C0b
                                  )
                                )
                              )
                              (CC
                                (CC
                                  (CC
                                    C0a
                                    (CC
                                      C1
                                      C0b
                                    )
                                  )
                                  (CC
                                    (CC
                                      (CC
                                        (CC
                                          (CC
                                            (CC
                                              C1
                                              C0b
                                            )
                                            C0b
                                          )
                                          C0b
                                        )
                                        C0b
                                      )
                                      C0b
                                    )
                                    C0b
                                  )
                                )
                                (CC
                                  (CC
                                    (CC
                                      (CC
                                        (CC
                                          (CC
                                            (CC
                                              (CC
                                                (CC
                                                  (CC
                                                    (CC
                                                      C1
                                                      C0b
                                                    )
                                                    C0b
                                                  )
                                                  C0b
                                                )
                                                C0b
                                              )
                                              C0b
                                            )
                                            C0b
                                          )
                                          C0b
                                        )
                                        C0b
                                      )
                                      C0b
                                    )
                                    C0b
                                  )
                                  C0b
                                )
                              )
                            )
                          )
-}


text:
module DepSec.Declassification

import DepSec.Labeled

%access export

||| Predicate hatch builder
||| TCB
||| @D data structure type
||| @E element type
||| @d data structure where declassification is allowed from
||| @P predicate
predicateHatch : Poset labelType
             => {l, l' : labelType}
             -> {D, E : Type}
             -> (d : D)
             -> (P : D -> E -> Type)
             -> (d : D ** Labeled l (e : E ** P d e) -> Labeled l' E)
predicateHatch {labelType} {l} {l'} {E} d P = (d ** hatch)
  where
    hatch : Labeled l (e : E ** P d e) -> Labeled l' E
    hatch (MkLabeled (x ** _)) = label x

||| Token hatch builder
||| TCB
||| @E value type
||| @S token type
||| @Q token predicate
tokenHatch : Poset labelType
          => {l, l' : labelType}
          -> {E, S : Type}
          -> (Q : S -> Type) -- 'when'/'who' predicate
          -> (s : S ** Q s) -> Labeled l E -> Labeled l' E
tokenHatch {labelType} {l} {l'} {E} {S} Q = hatch
  where
    hatch : (s : S ** Q s) -> Labeled l E -> Labeled l' E
    hatch _ (MkLabeled x) = label x

||| Generic combined hatch builder
||| TCB
||| @d data structure
||| @Q token predicate
||| @P predicate
hatchBuilder : Poset labelType
            => {l, l' : labelType}
            -> {D, E, S : Type}
            -> (d : D) -- datastructre
            -> (Q : S -> Type) -- 'when'/'who' predicate
            -> (P : D -> E -> Type) -- 'what' predicate
            -> (d : D ** Labeled l (e :  E ** P d e) -> (s : S ** Q s) -> Labeled l' E)
hatchBuilder {labelType} {l} {l'} {E} {S} d Q P =  (d ** hatch)
  where
    hatch : Labeled l (e : E ** P d e) -> (s : S ** Q s) -> Labeled l' E
    hatch (MkLabeled (x ** _)) _ = label x

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Control.Algebra.DiamondInstances

import Control.Algebra
import Classes.Verified -- definition of verified algebras other than modules

%default total

{-
Diamond instances
explicitly referenced for using in treating diamond inheritance problems
* VerifiedGroup a -> Semigroup a
* VerifiedRingWithUnity a -> Semigroup a
* VerifiedRingWithUnity a -> Ring a
-}

vgrpVerifiedMonoid : VerifiedGroup a -> VerifiedMonoid a
vgrpVerifiedMonoid a = %instance

vgrpGroup : VerifiedGroup a -> Group a
vgrpGroup a = %instance

vmonSemigrp : VerifiedMonoid a -> Semigroup a
vmonSemigrp a = %instance

grpSemigrp : Group a -> Semigroup a
grpSemigrp a = %instance

vgrpSemigroupByVMon : VerifiedGroup a -> Semigroup a
vgrpSemigroupByVMon = vmonSemigrp . vgrpVerifiedMonoid

vgrpSemigroupByGrp : VerifiedGroup a -> Semigroup a
vgrpSemigroupByGrp = grpSemigrp . vgrpGroup

vrSemigroupByVMon : VerifiedRing a -> Semigroup a
vrSemigroupByVMon a = vgrpSemigroupByVMon %instance

vrSemigroupByGrp : VerifiedRing a -> Semigroup a
vrSemigroupByGrp a = vgrpSemigroupByGrp %instance

vrwuSemigroupByVMon : VerifiedRingWithUnity a -> Semigroup a
vrwuSemigroupByVMon a = vgrpSemigroupByVMon %instance

vrwuSemigroupByGrp : VerifiedRingWithUnity a -> Semigroup a
vrwuSemigroupByGrp a = vgrpSemigroupByGrp %instance

vrwuVerifiedRing : VerifiedRingWithUnity a -> VerifiedRing a
vrwuVerifiedRing a = %instance

vrwuRingWithUnity : VerifiedRingWithUnity a -> RingWithUnity a
vrwuRingWithUnity a = %instance

vrRing : VerifiedRing a -> Ring a
vrRing a = %instance

rwuRing : RingWithUnity a -> Ring a
rwuRing a = %instance

vrwuRingByVR : VerifiedRingWithUnity a -> Ring a
vrwuRingByVR = vrRing . vrwuVerifiedRing

vrwuRingByRWU : VerifiedRingWithUnity a -> Ring a
vrwuRingByRWU = rwuRing . vrwuRingWithUnity


text:
> module NonNegRational.tests.Main

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Fraction.Fraction
> import Fraction.Predicates
> import Fraction.BasicOperations
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.Positive

> %default total
> %auto_implicits off

> x  : NonNegRational
> x  = fromFraction (2067, Element 616 MkPositive)

> y  : NonNegRational
> y  = fromFraction (32, Element 11 MkPositive)

> z  : NonNegRational
> z  = fromFraction (1, Element 13 MkPositive) -- segfaults with 'Element 12749 MkPositive'

> f1  : Fraction
> f1  = (1, Element 8 MkPositive)
> z1  : NonNegRational
> z1  = fromFraction f1

> f2  : Fraction
> f2  = (3, Element 24 MkPositive)
> z2  : NonNegRational
> z2  = fromFraction f2

> f1Eqf2 : f1 `Eq` f2
> f1Eqf2 = Refl

> z1EQz2 : z1 = z2
> z1EQz2 = fromFractionEqLemma f1 f2 f1Eqf2

> zs : List NonNegRational
> zs = [z1, z2]

> szs : sum zs = z1 + z2
> szs = Refl

> main : IO ()
> main = do putStrLn ("x           = " ++ show x)
>           putStrLn ("y           = " ++ show y)
>           putStrLn ("z           = " ++ show z)
>           putStrLn ("x + y       = " ++ show (x + y))
>           putStrLn ("y + x       = " ++ show (y + x))
>           putStrLn ("x * y       = " ++ show (x * y))
>           putStrLn ("y * x       = " ++ show (y * x))
>           putStrLn ("(x + y) + z = " ++ show ((x + y) + z))
>           putStrLn ("x + (y + z) = " ++ show (x + (y + z)))
>           putStrLn ("(x * y) * z = " ++ show ((x * y) * z))
>           putStrLn ("zs          = " ++ show zs)
>           putStrLn ("sum zs      = " ++ show (sum zs))

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import System

main : IO ()
main = do
  0 <- system "bash zero.sh"
    | r => do putStrLn ("expecting zero, got " ++ (show r))
              exitFailure
  -- `system` returns result of `waitpid` which is not trivial to decode
  let True = !(system "bash seventeen.sh") /= 0
    | False => putStrLn "expecting 17, got zero"
  pure ()


text:
module Data.NFA

%default total
%access public export

record NFA s elem where
  constructor MkNFA
  init       : s
  transition : s -> elem -> List s
  terminal   : s -> Bool

accepts : Eq elem => NFA s elem -> List elem -> Bool
accepts (MkNFA init transition terminal) = any terminal . foldlM transition init

data State : Type -> Type where
  Match  :                                                State elem
  Split  : (left : State elem) -> (right : State elem) -> State elem
  Single : (out  : elem)       -> (next  : State elem) -> State elem

data Expression : Type -> Type where
  ELit : elem                                                                      -> Expression elem
  EUn  : (opname : String) -> (operation : State elem -> State elem)               -> Expression elem
  EBin : (opname : String) -> (operation : State elem -> State elem -> State elem) -> Expression elem

data ExprCompilationError = ECompErr String

private
compErr : String -> Either ExprCompilationError a
compErr = Left . ECompErr

-- compile : List (Expression elem) -> Either ExprCompilationError (State elem)
-- compile xs = go xs [] where
--   go : List (Expression elem) -> List (Frag elem) -> Either ExprCompilationError (State elem)
--   go [] [] = compErr "Nothing to compile"
--   go [] (s :: []) = case state s of
--                       Ready x     => Right x
--                       TempSplit _ =>
--                         compErr "Compilation error, state value not complete. Possibly a bug in the implementation."
--   go [] (s :: ss) = compErr "Compilation error, extra values remaining in stack. Probably a bug in the implementation."
--   go (ELit l :: xs) ys = go xs (MkFrag (Ready $ Single l) Nil :: ys)
--   go (EUn _ op :: xs) (o1 :: ys) = go xs (op o1 :: ys)
--   go (EUn name _ :: xs) ys       = compErr $ "Compilation error: operation [ " ++ name ++ " ] requires an operand."
--   go (EBin _ op :: xs) (o1 :: o2 :: ys) = go xs (op o1 o2 :: ys)
--   go (EBin name _ :: xs) ys = compErr $ "Compilation error: operation [ " ++ name ++ " ] requires two operands."

max_stars_repo_name: jhmcstanton/idris-sandbox

max_issues_repo_name: jhmcstanton/idris-sandbox

max_forks_repo_name: jhmcstanton/idris-sandbox


text:
module Data.Vect.Extras

import Data.Vect
import Data.Vect.Views

%default total
%access export

foldrM :  Monad m => (func : elem -> acc -> m acc) -> (init : acc) -> (input : Vect n elem) -> m acc
foldrM func init input with (snocVect input)
    foldrM _ init [] | Empty = pure init
    foldrM func init (xs ++ [x]) | Snoc rec = foldrM func !(func x init) xs | rec

mapM : Monad m => (func : elem -> m r) -> (input : Vect n elem) -> m (Vect n r)
mapM = helper []
where helper :  Monad m => Vect n r -> (elem -> m r) ->  Vect n' elem -> m (Vect (n + n') r)
      helper {n} acc func [] =
          rewrite plusZeroRightNeutral n in
          pure acc
      helper {n} {n' = S k} acc func (x :: xs) =
          rewrite sym $ plusSuccRightSucc n k in
          do helper (!(func x) :: acc) func xs

max_stars_repo_name: jheiling/idris-extras

max_issues_repo_name: jheiling/idris-extras

max_forks_repo_name: jheiling/idris-extras


text:
module Js

%default total
%access export

infix 6 ===

%inline
js : (fname : String) -> (ty : Type) -> {auto fty : FTy FFI_JS [] ty} -> ty
js fname ty = foreign FFI_JS fname ty

%inline
null : JS_IO Ptr
null = js "null" (JS_IO Ptr)

%inline
undefined : JS_IO Ptr
undefined = js "undefined" (JS_IO Ptr)

%inline
(===) : Ptr -> Ptr -> JS_IO Bool
(===) a b = pure $ !(js "%0 === %1 + 0" (Ptr -> Ptr -> JS_IO Int) a b) /= 0

%inline
isNull : Ptr -> JS_IO Bool
isNull x = pure $ !(js "(%0 === null) + 0" (Ptr -> JS_IO Int) x) /= 0

%inline
isUndefined : Ptr -> JS_IO Bool
isUndefined x = pure $ !(js "(%0 === undefined) + 0" (Ptr -> JS_IO Int) x) /= 0

|||time in ms
%inline
setTimeout : (time : Nat) -> (action : JS_IO ()) -> JS_IO ()
setTimeout time action = assert_total $ js "setTimeout(%1, %0)" (Int -> JsFn (() -> JS_IO ()) -> JS_IO ()) (cast time) $ MkJsFn $ \() => action

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module World

import public Data.SortedMap

%access export

public export
record Entity t where
  constructor MkEntity
  health : t -> Int
  attack : Int -> t -> t

%name Entity i, i', i''

public export
Key : Type
Key = Int

public export
Host : Type
Host = SortedMap Key (t : Type ** (Entity t, t))

%name Host w, w', w''

spawn : Entity t -> Key -> t -> Host -> Host
spawn i k e w = insert k (t ** (i, e)) w

withEntity : Host -> Key -> ((t : Type) -> Entity t -> t -> (t, b)) -> (Host, Maybe b)
withEntity w k f = case lookup k w of
    Nothing             => (w, Nothing)
    Just (t' ** (i, e)) => let (e', x) = f t' i e
                           in (insert k (t' ** (i, e')) w, Just x)

foldWorld : Monoid m => Host -> ((t : Type) -> Entity t -> Key -> t -> m) -> m
foldWorld w f = foldl f' neutral (toList w)
  where f' m (k, (t ** (i, e))) = m <+> f t i k e


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

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

{-
  ported from file ./kernel/libsel4/include/sel4/sel4.h
-}

module seL4.seL4

import public seL4.Syscalls
import public seL4.Arch.Functions
import public seL4.BootinfoTypes
import public seL4.Bootinfo
import public seL4.SharedTypes
import public seL4.seL4Debug
import public seL4.Types

%include C "sel4/sel4.h"


text:
module IndexVector

import Data.Vect

ndx : (Fin 3) -- Bounded naturl number [0 .. n)
ndx = 2

v : Vect 3 Nat -- vector od 3 elements of Nat type (natural number, zero or greater)
v = [0,1,5]

el : Nat
el = index ndx v

el2 : Nat
el2 = index ndx [11, 22, 33]

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
module Streaming.API

import Prelude as P

import public Streaming.Internal as S

import Control.Monad.Trans -- lift

import Data.LazyList

-- import Util

-- slightly more specific version of inspect
export
%inline
next : Monad m => Stream (Of a) m r -> m (Either r (Of a (Stream (Of a) m r)))
next = inspect

export
%inline
cons : Monad m => a -> Stream (Of a) m r -> Stream (Of a) m r
cons x str = wrap (x :> str)
-- cons x str = Build (\r,eff,step => step (x :> streamFold r eff step str))

export
copy : Monad m => Stream (Of a) m r -> Stream (Of a) (Stream (Of a) m) r
copy str = case str of
  (Return x) => Effect . pure . Return $ x
  (Effect x) => Effect . pure . Effect $ copy <$> lift x -- tricky
  (Step (x :> y)) => Effect . pure . Effect $ (Step (x :> Return (Step (x :> copy y))))
  (Build g)  => copy (streamBuild g)

export
store : Monad m => (Stream (Of a) (Stream (Of a) m) r -> t)
     -> Stream (Of a) m r -> t
store f str = f (copy str)

||| Appends two streams keeping the value of the latter, for a version that
||| keeps both results use <+>
export
append : Monad m => Stream (Of a) m r -> Stream (Of a) m r -> Stream (Of a) m r
append s1 s2 = Build
 (\r,eff,step => streamFold (\_ => streamFold r eff step s2) eff step s1)

export
concats : (Functor f, Monad m) => Stream (Stream f m) m r -> Stream f m r
concats str = Build
  (\r,eff,step => streamFold r eff (streamFold id eff step) str)

export
||| strict (left) fold
foldl : Monad m => (b -> a -> b) -> b -> Stream (Of a) m r -> m (Of b r)
foldl f acc (Return r) = pure (acc :> r)
foldl f acc (Effect m) = m >>= foldl f acc
foldl f acc (Step (x :> str)) = foldl f (f acc x) str
foldl f acc (Build g) = foldl f acc (streamBuild g)

export
foldr : Monad m => (a -> b -> b) -> b -> Stream (Of a) m r -> m (Of b r)
foldr f acc = streamFold (\r => pure (acc :> r)) join
               (\(a :> rest) => mapFst (f a) <$> rest)

export
foldr_ : Monad m => (a -> b -> b) -> b -> Stream (Of a) m r -> m b
foldr_ f acc = streamFold (\_ => pure acc) join (\(a :> rest) => f a <$> rest)

foldl_ : Monad m => (b -> a -> b) -> b -> Stream (Of a) m r -> m b
foldl_ f acc (Return r) = pure acc
foldl_ f acc (Effect m) = m >>= foldl_ f acc
foldl_ f acc (Step (x :> str)) = foldl_ f (f acc x) str
foldl_ f acc (Build g) = foldl_ f acc (streamBuild g)

export
foldrM : Monad m => (a -> b -> m b) -> m b -> Stream (Of a) m r -> m (Of b r)
foldrM f acc = streamFold (\r => (:> r) <$> acc) join
                (\(a :> rest) => do
                  (b :> r) <- rest
                  (:> r) <$> f a b)

export -- our fold is foldl so we make a dlist
toList : Monad m => Stream (Of a) m r -> m (Of (List a) r)
toList str = mapFst ($ []) <$> foldl (\diff,a,ls => diff (a :: ls)) id str

||| Run an action on each element of a stream and reyield them, this is quite
||| useful for debug priting of stream values as you work on them.
export
chain : Monad m => (a -> m ()) -> Stream (Of a) m r -> Stream (Of a) m r
chain f str = Build (\r,eff,step => streamFold r eff
  (\(x :> y) => eff $ f x *> pure (step (x :> y))) str)

-- export
-- toList_ : Monad m => Stream (Of a) m r -> m (List a)
-- toList_ = fold_ (::) []

export
length : Monad m => Stream (Of a) m r -> m (Of Int r)
length = foldl (\n,_ => 1 + n) 0

export
length' : Monad m => Stream (Of a) m r -> m (Of Nat r)
length' = foldl (\n,_ => S n) Z

export
length_ : Monad m => Stream (Of a) m r -> m Int
length_ = foldl_ (\n,_ => 1 + n) 0

export
length'_ : Monad m => Stream (Of a) m r -> m Nat
length'_ = foldl_ (\n,_ => S n) Z

export
sum : (Monad m, Num a) => Stream (Of a) m r -> m (Of a r)
sum = foldl (+) 0

export
sum_ : (Monad m, Num a) => Stream (Of a) m r -> m a
sum_ = foldl_ (+) 0

-------------------------------------------------
-- Constructing Streams
-------------------------------------------------

public export -- Might as well be public, it's just constructors.
%inline
||| The empty stream, mostly for convenience.
empty : Stream (Of a) m ()
empty = Return ()

export
||| aka 'single', a stream of one element.
yield : Monad m => a -> Stream (Of a) m ()
yield x = cons x empty

-- Stream (Of )

-- yields : f a -> Stream (Of a) m r

-- 'each' of these could simply be Foldable if Foldable's foldr wasn't so strict

export
||| Preferred method of providing List input to a Stream.
each : Monad m => LazyList a -> Stream (Of a) m ()
each [] = empty
each (x :: xs) = cons x (each xs)

export
||| Turn a (list) stream into our Stream.
each' : Monad m => Stream a -> Stream (Of a) m ()
each' (x :: xs) = cons x (each' xs)

export
||| It's better to use LazyList. List will reside in memory all at once.
each'' : Monad m => List a -> Stream (Of a) m ()
each'' = each . fromList

export
||| You are best to avoid this, foldable's methods are strict, your source will
||| reside in memory all at once. And (for some reason) in a manner worse than
||| plain List.
each''' : (Monad m, Foldable f) => f a -> Stream (Of a) m ()
each''' = foldr cons empty

-------------------------------------------------
-- Splitting Streams
-------------------------------------------------

-- idk how to 'Build' this. specifically to carry the Nat to the next 'step'
export
splitsAt : (Monad m, Functor f) => Int -> Stream f m r -> Stream f m (Stream f m r)
splitsAt 0 str = Return str
splitsAt n str = case str of
  (Return x) => Return (Return x)
  (Effect x) => Effect (splitsAt n <$> x)
  (Step x) => case n of
    0 => Return (Step x)
    k => Step $ splitsAt (k-1) <$> x
  (Build g) => splitsAt n (streamBuild g) -- :(

-- idk how to 'Build' this. specifically to carry the Nat to the next 'step'
export
splitsAt' : (Monad m, Functor f) => Nat -> Stream f m r -> Stream f m (Stream f m r)
splitsAt' Z str = Return str
splitsAt' n str = case str of
  (Return x) => Return (Return x)
  (Effect x) => Effect (splitsAt' n <$> x)
  (Step x) => case n of
    Z => Return (Step x)
    (S k) => Step $ splitsAt' k <$> x
  (Build g) => splitsAt' n (streamBuild g) -- :(

-- idk how to 'Build' this
export
chunksOf : (Monad m, Functor f) => Int -> Stream f m r -> Stream (Stream f m) m r
chunksOf n (Return x) = Return x
chunksOf n (Effect x) = Effect (chunksOf n <$> x)
chunksOf n (Step x)   = Step (Step (map (map (chunksOf n) . splitsAt (n - 1)) x))
chunksOf n (Build g)  = chunksOf n (streamBuild g) -- :(

export
chunksOf' : (Monad m, Functor f) => Nat -> Stream f m r -> Stream (Stream f m) m r
chunksOf' n (Return x) = Return x
chunksOf' n (Effect x) = Effect (chunksOf' n <$> x)
chunksOf' n (Step x)   = Step (Step (map (map (chunksOf' n) . splitsAt' (n`minus`1)) x))
chunksOf' n (Build g)  = chunksOf' n (streamBuild g) -- :(

-- I was able to 'Build' this because it doesn't need to carry state per
-- invocation, it's a constant predicate.
||| `span` streams elements until one fails the condition, returning the remainder
||| span (<3) [1,2,3,4,5] => [3,4,5]
export
span : Monad m => (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m (Stream (Of a) m r)
span p str = Build (\r,eff,step => streamFold (r . Return) eff (spanIt p r eff step) str)
  where
    spanIt : (a -> Bool) -> (Stream (Of a) m r -> b) -> (m b -> b) -> (Of a b -> b) -> Of a b -> b
    spanIt pred r eff step v@(x :> y) = if pred x
      then step v
      else r $ Step (x :> str)

export
take : (Functor f, Monad m) => Int -> Stream f m r -> Stream f m ()
take 0 str = pure ()
take n str = case str of
  (Return x) => Return ()
  (Effect x) => Effect (map (take n) x)
  (Step x) => Step (map (take (n - 1)) x)
  (Build g) => g (const (Return ())) (effect . map (take n)) (wrap . map (take (n - 1)))

-- dunno how to 'Build' this
export
take' : (Functor f, Monad m) => Nat -> Stream f m r -> Stream f m ()
take' Z str = pure ()
take' n@(S k) str = case str of
  (Return x) => Return ()
  (Effect x) => Effect (map (take' n) x)
  (Step x) => Step (map (take' k) x)
  (Build g) => g (const (Return ())) (effect . map (take' n)) (wrap . map (take' k))

export
drop : (Functor f, Monad m) => Int -> Stream f m r -> Stream f m r
drop 0 str = str
drop n str = Build (\r,eff,step => streamFold r eff step (drop (n - 1) str))

export
drop' : (Functor f, Monad m) => Nat -> Stream f m r -> Stream f m r
drop' Z str = str
drop' (S k) str = Build (\r,eff,step => streamFold r eff step (drop' k str))

export
||| `split` aka splitOn/splitBy
||| splits a stream into segments based on a predicate, consumes True results.
split : Monad m => (a -> Bool) -> Stream (Of a) m r -> Stream (Stream (Of a) m) m r
split f (Return y) = Return y
split f (Effect y) = Effect (map (split f) y)
split f (Step (a :> rest)) = if not (f a)
  then Step (Prelude.map (split f) (yield a *> span (not . f) rest))
  else split f rest
split f (Build g) = split f (streamBuild g)

export
filter : Monad m => (a -> Bool) -> Stream (Of a) m r -> Stream (Of a) m r
filter p str = Build (\r,eff,step => streamFold r eff (\(x :> y) => if p x then step (x :> y) else y) str)

export
all : Monad m => (a -> Bool) -> Stream (Of a) m r -> m (Of Bool r)
all p str = foldl (\b,x => p x && b) True str

export
print : (HasIO io, Show a, Show r) => Stream (Of a) io r -> io r
print x = streamFold (\r => printLn r *> pure r) join (\(x :> s) => print x *> s) x <* putStr "\n"

-- infixl 9 `for`
export
-- | @for@ replaces each element of a stream with an associated stream. Note that the
-- associated stream may layer any functor.
for : (Monad m, Functor f) => Stream (Of a) m r -> (a -> Stream f m x) -> Stream f m r
for str act = Build (\r,eff,step => streamFold r eff
  (\(a :> rest) => streamFold r eff step (act a *> for str act)) str)

export
concat : (Foldable f, Monad m) => Stream (Of (f a)) m r -> Stream (Of a) m r
concat str = for str each'''

-- Temporary, this seems like a common pattern somehow, I need to find what
-- fundamental operation subsumes it. a variant of how concat is written perhaps
export
fromList : (Foldable f, Monad m) => m (Of (LazyList a) r) -> Stream (Of a) m r
fromList xs = Effect $ do
  (x :> y) <- xs
  let g = each {m} x
  pure (Build (\r,eff,step => streamFold (\_ => r y) eff step g))

export
fromList' : (Foldable f, Monad m) => m (Of (f a) r) -> Stream (Of a) m r
fromList' xs = Effect $ do
  (x :> y) <- xs
  let g = each''' {m} x
  pure (Build (\r,eff,step => streamFold (\_ => r y) eff step g))

export
zipWith : Monad m => (a -> b -> c) -> Stream (Of a) m r -> Stream (Of b) m r -> Stream (Of c) m r
zipWith f (Return r) str2 = Return r
zipWith f (Effect m) str2 = Effect $ map (\str => zipWith f str str2) m
zipWith f s@(Step (a :> y1)) str2 = case str2 of
  (Return r) => Return r
  (Effect m) => Effect $ map (zipWith f s) m
  (Step (b :> y2)) => Step $ f a b :> zipWith f y1 y2
  (Build g) => g Return Effect (\(b :> y2) => Step $ f a b :> y2)
zipWith f (Build g) str2 = zipWith f (streamBuild g) str2

export
repeat : Monad m => a -> Stream (Of a) m r
repeat x = effect (pure (wrap (x :> repeat x)))

export
replicate : Monad m => Int -> a -> Stream (Of a) m ()
replicate n x = take n (repeat {r=()} x)

-- export
-- replicateM : Monad m => Int -> m a -> Stream (Of a) m ()
-- replicateM n x = take n (repeat x)

export
%inline
zip : Monad m => Stream (Of a) m r -> Stream (Of b) m r -> Stream (Of (a,b)) m r
zip = zipWith MkPair

export
iterate : Monad m => (a -> a) -> a -> Stream (Of a) m r
iterate f x = effect $ pure $ wrap $ x :> iterate f (f x)

-- Helper, I seem to use it a lot but haskell 'streaming' doesn't have it, am I
-- doing something wrong?
-- Not quite sure about its execution complexity with the naive rev style
export
rev : Monad m => Stream (Of a) m r -> Stream (Of a) m r
rev str0 = effect $ do
  Right (x :> str) <- inspect str0
    | Left l => pure . pure $ l
  pure $ rev str <* yield x

||| This is quite strict but it also that way in the haskell implementation
||| because Step is strict there and only lazy in the 2nd field of Of, which we
||| use immediately here, so it's fully strict.
export
effects : Monad m => Stream (Of a) m r -> m r
effects = streamFold pure join sndOf
-- effects (Return x) = pure x
-- effects (Effect x) = x >>= effects
-- effects (Step (x :> y)) = effects y -- too strict
-- effects (Build f) = effects (streamBuild f)

-- drained :: Monad m => Stream (Of a) m (Stream (Of b) m r) -> Stream (Of a) m r
export
drained : (Monad m, Monad (t m), Functor (t m), MonadTrans t)
      => t m (Stream (Of a) m r) -> t m r
drained = join . map (lift . effects)

||| strictly take some of a stream and preserve the return type, it's barely
||| worth it given that it's strict on the whole stream
export -- t is hard to deduce for the compiler so we help it along
take'' : Monad m => Int -> Stream (Of a) m r -> Stream (Of a) m r
take'' n = drained {t=Stream (Of a)} . splitsAt n


text:
module TyTTP.Adapter.Node.Error

import Node.Error
import TyTTP

export
Error NodeError where
  message = Node.Error.message


text:
import Drahko

main : Promise ()
main = do
  hotkey "#z" $ do
    msgBox "Pressed Win+Z"

  hotkey "#t" $ do
    msgBox "Pressed Win+T"

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/idris-autohotkey

max_forks_repo_name: drahko/drahko


text:
module Text.Markup.Edda.CommonMark

import public Text.Markup.Edda.Model
import public Text.Markup.Edda.Walk
import public Text.Markup.Edda.Query

import public Text.Markup.Edda.Reader.CommonMark
import public Text.Markup.Edda.Writer.CommonMark

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
-- Module      : Itea.Html.Events
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Html.Events
import Itea.Utils
import Itea.Javascript.Types

import Control.Monad.Reader
import Control.Monad.Trans
import Data.IORef

%default total
%access public export

||| Internal event queue used for feeding user actions and other events for
||| the main loop to consume.
data EventQueue : Type -> Type where
  MkEVQ : IORef (List a) -> EventQueue a

||| Event handler type
Handler : Type -> Type
Handler a = JsFn (Ptr -> JS_IO ())

||| Event type
data Event : Type -> Type where
  ||| Event constructor
  |||
  ||| @name name of event to fire on
  ||| @handler event hanlder
  ||| @options event options given a raw Javascript pointer with an opaque type
  MkEvent : (name    : String)
         -> (handler : Handler a)
         -> (options : JSRef 'EventOptions)
         -> Event a

HtmlEvent : Type -> Type -> Type
HtmlEvent a b = ReaderT (EventQueue a, Ptr) JS_IO b

||| Place a new event on the event queue
putEvent : EventQueue a -> a -> JS_IO ()
putEvent (MkEVQ queue) value = modifyIORef' queue (value::)

||| Pop the latest event from the event queue
getEvent : EventQueue a -> JS_IO (Maybe a)
getEvent (MkEVQ queue) =
  case !(readIORef' queue) of
       (x :: _) => modifyIORef' queue (drop 1) *> pure (Just x)
       _        => pure Nothing

namespace HtmlEvent

  ||| Place a new event on the queue within the context of a reader monad
  putEvent : a -> HtmlEvent a ()
  putEvent value = asks Prelude.Basics.fst
               >>= lift . flip putEvent value

  ||| Pop the latest event from the queue within the context of a reader monad
  getEvent : HtmlEvent a (Maybe a)
  getEvent = asks Prelude.Basics.fst
         >>= lift . getEvent

||| Construct a new event with the given name, options, handler, and queue
event : (name    : String)
     -> (options : JSRef 'EventOptions)
     -> (handler : HtmlEvent a ())
     -> (queue   : EventQueue a)
     -> Event a
event name options handler e =
  MkEvent name
          (MkJsFn $ \p => runReaderT handler (e,p))
          options

onchange : JSRef 'EventOptions
        -> HtmlEvent a ()
        -> EventQueue a
        -> Event a
onchange = event "change"

onclick : JSRef 'EventOptions
       -> HtmlEvent a ()
       -> EventQueue a
       -> Event a
onclick = event "click"

options : (passive : Bool) -> (once : Bool) -> (capture : Bool) -> JSRef 'EventOptions
options p o c = believe_me
              $ jscall "{'passive': %0, 'once': %1, 'capture': %2}"
                       (Int -> Int -> Int -> JS_IO Ptr)
                       (jsbool p) (jsbool o) (jsbool c)

namespace Default

  ||| Default options for onchange
  onchange : HtmlEvent a () -> EventQueue a -> Event a
  onchange = onchange (options False False False)

  ||| Default options for onclick
  onclick : HtmlEvent a () -> EventQueue a -> Event a
  onclick = onclick (options False False False)

namespace Simple

  ||| Simplified interface for `onchange`
  onchange : a -> EventQueue a -> Event a
  onchange = onchange . putEvent

  ||| Simplified interface for `onclick`
  onclick : a -> EventQueue a -> Event a
  onclick = onclick . putEvent

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module Main

main : IO ()
main = return ()

max_stars_repo_name: pharpend/dudo

max_issues_repo_name: pharpend/dudo

max_forks_repo_name: pharpend/dudo