text:
module Main

import Data.Vect

-- Enumerated types - Types defined by giving the possible values directly.

data Direction = North | East | South | West

turnClockwise : Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North

-- Union types - Enumerated types that carries additional data at each values.

||| Shape represent objects from trigonometry.
data Shape = ||| A triangle,  with its base length and height
             Triangle Double Double
           | ||| A rectabgle, with its length and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

%name Shape shape, shape1, shape2

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Shape2 : Type where
  Triangle2 : Double -> Double -> Shape2
  Rectagle2 : Double -> Double -> Shape2
  Circle2   : Double -> Shape2

-- Recursive types - Union types that defined on terms of themselves.

data Picture : Type where
  Primitive : Shape -> Picture
  Combine : Picture -> Picture -> Picture
  Rotate : Double -> Picture -> Picture
  Translate : Double -> Double -> Picture -> Picture

%name Picture pic, pic1, pic2

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture =
    Combine (Translate 5 5 rectangle)
    (Combine (Translate 35 5 circle)
    (Translate 15 25 triangle))

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

-- Generic types - Types that are parametrized over some type

data Tree e
  = Empty
  | Node (Tree e) e (Tree e)

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x node@(Node left val right) = case compare x val of
  LT => Node (insert x left) val right
  EQ => node
  GT => Node left val (insert x right)

data STree : Type -> Type where
  SEmpty : Ord elem => STree elem
  SNode : Ord elem
    => (left : STree elem)
    -> (val : elem)
    -> (right : STree elem)
    -> STree elem

insertS : elem -> STree elem -> STree elem
insertS x SEmpty = SNode SEmpty x SEmpty
insertS x node@(SNode left val right)
  = case compare x val of
      LT => SNode (insertS x left) val right
      EQ => node
      GT => SNode left val (insertS x right)

listTree : Ord a => List a -> Tree a
listTree [] = Empty
listTree (x :: xs) = insert x $ listTree xs

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right

-- Dependent types - Types are computed from some other values

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol

renderVehicle : Vehicle power -> String
renderVehicle Bicycle = "Bicycle"
renderVehicle (Car fuel) = "Car " ++ show fuel
renderVehicle (Bus fuel) = "Bus " ++ show fuel

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel Bicycle impossible

zip2 : Vect n a -> Vect n b -> Vect n (a,b)
zip2 [] [] = []
zip2 (x :: xs) (y :: ys) = (x, y) :: zip2 xs ys

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
  Nothing  => Nothing
  Just idx => Just (index idx xs)

fin : Fin n -> Nat
fin FZ     = 0
fin (FS x) = 1 + fin x

total
vectTake : (fn : Fin n) -> Vect n a -> Vect (fin fn) a
vectTake FZ xs = []
vectTake (FS n) (x :: xs) = x :: vectTake n xs

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} i xs ys = case integerToFin i n of
  Nothing => Nothing
  Just idx => Just $ (index idx xs) + (index idx ys)

main : IO ()
main = do
  printLn "Data types"
  printLn $ pictureArea testPicture
  printLn $ treeToList $ listTree [1,4,3,5,2]
  printLn $ wheels Bicycle
  printLn $ renderVehicle (Bus 10)
  printLn $ zip2 [1,2,3] ['a', 'b', 'c']
  printLn $ Vect.index 3 [1,2,3,4,5]
  printLn $ tryIndex 3 [1,2,3,4,5]
  printLn $ sumEntries 2 [1,2,3,4] [5,6,7,8]


text:
module GRL.Test.Sif

import GRL.Lang.GLang
import GRL.Eval

import GRL.Test.Utils

%default total

g1 : GOAL
g1 = mkGoal "[Goal Requirement: Suitable Security Level Nothing ]"

g2 : TASK
g2 = mkGoal "[Goal Requirement: Data Confidentiality Nothing ]"

g3 : TASK
g3 = mkTask "[Goal Requirement: Recipient Confidentiality Nothing ]"

g4 : TASK
g4 = mkTask "[Goal Requirement: Suitable performance Nothing ]"

g5 : TASK
g5 = mkTask "[Goal Requirement: Minimal Workflow Disruption Nothing ]"

g6 : TASK
g6 = mkTask "[Goal Requirement: Secure Implementation Nothing ]"

g7 : TASK
g7 = mkTask "[Goal Requirement: Comprehensible by Non-Experts Nothing ]"

model : GModel
model = insertMany [g1,g2,g3,g4,g5,g6,g7] emptyModel

t1 : TASK
t1 = mkTask "Task Solution: Public Key Cryptography Nothing"

t2 : TASK
t2 = mkTask "[Task Property: Maths Algorithm Nothing ]"

t3 : TASK
t3 = mkTask "[Task Property: Implementation in Code Nothing ]"

t4 : TASK
t4 = mkTask "[Task Property: Key Pairs Nothing ]"

t5 : TASK
t5 = mkTask "[Task Property: Variable Security Parameters Nothing ]"

t6 : TASK
t6 = mkSatTask "t6" SATISFIED

t7 : TASK
t7 = mkSatTask "[Task Trait Disadvantage: Computationally Expensive Just WEAKDEN ]" WEAKDEN

t12 : TASK
t12 = mkSatTask "[Task Trait Disadvantage: Implementation InSecure Just WEAKDEN ]" WEAKDEN

t13 : TASK
t13 = mkSatTask "[Task Trait Disadvantage: Implementation obfuscates understanding Just WEAKSATIS ]" WEAKSATIS

t16 : TASK
t16 = mkSatTask "[Task Trait Advantage: PublicEnc/PrivateDec Keys Just SATISFIED ]" SATISFIED

t17 : TASK
t17 = mkSatTask "[Task Trait Disadvantage: Key Distribution Just DENIED ]" DENIED

t18 : TASK
t18 = mkSatTask "[Task Trait Disadvantage: Key Management Just DENIED ]" DENIED

t19 : TASK
t19 = mkSatTask "[Task Trait Advantage: Greater Security Just SATISFIED ]" SATISFIED

t20 : TASK
t20 = mkSatTask "[Task Trait Disadvantage: Parameter Selection Just DENIED ]" DENIED

t21 : TASK
t21 = mkSatTask "[Task Trait Disadvantage: Parameter Computation Just DENIED ]" DENIED

decls : (ds ** DList GTy GLang ds)
decls = (_ **
   [ t1,
     mkAnd t1 [ t2, t3 , t4 , t5],
     t2 , t6 , t7 ,
     mkImpacts HELPS t6 g2 ,
     mkImpacts HELPS t6 g3 ,
     mkImpacts HURTS t7 g4 ,
     mkImpacts HURTS t7 g5 ,
     mkAnd t2 [t6 , t7],
     t3 , t12 , t13 ,
     mkImpacts SOMENEG t12 g3 ,
     mkImpacts SOMENEG t12 g2 ,
     mkImpacts UNKNOWN t12 g5 ,
     mkImpacts SOMENEG t12 g6 ,
     mkImpacts HURTS t13 g7 ,
     mkImpacts HURTS t13 g5 ,
     mkAnd t3 [t12 , t13],
     t4 , t16 , t17 , t18 ,
     mkImpacts MAKES t16 g3 ,
     mkImpacts SOMENEG t17 g3 ,
     mkImpacts SOMENEG t17 g5 ,
     mkImpacts SOMENEG t18 g2 ,
     mkAnd t4 [t16 , t17 , t18] ,
     t5 , t19 , t20 , t21 ,
     mkImpacts HELPS t19 g1 ,
     mkImpacts SOMENEG t20 g1 ,
     mkImpacts SOMENEG t20 g6 ,
     mkImpacts HURTS t21 g4 ,
     mkImpacts HURTS t21 g5 ,
     mkAnd t5 [t19 , t20 , t21]
     ])

export
partial
runTest : IO ()
runTest = do
  let (_ ** ds) = groupDecls (snd decls)
  putStrLn "Strategy 1:"
  let m = (insertMany' ds model)
  runEval m Nothing

ext: idr

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Ch05.LambdaCalculusWithArith

import Ch03.Relations

%default total
%access public export

--------------------------------------------------------------------------------
-- The lambda calculus extended by native arithmetic expressions.
--------------------------------------------------------------------------------
--
-- Remark: It kinda sucks to have to repeat the definitions of the lambda
-- calculus and the language of arithmetic expressions. In particular because
-- in the book Pierce doesn't even bother to write down the language and simply
-- waves his hands. So you expect to be able to just formally combine the two
-- languages.
-- However, I don't know a convenient way to do that since Idris has no subtyping.
-- It would be possible to define something like
--
-- data Term = Lambda Ch05.LambdaCalculus.Term
--           | Arith Ch03.Arith.Term
--
-- but that would be kinda awkward.
--
-- TL;DR: I'm just gonna repeat definitions as that seems simpler.
--------------------------------------------------------------------------------

||| The type of variables
Variable : Type
Variable = Nat

-- Pierce doesn't bother to actually define this calculus (neither in the book
-- nor the software available at https://www.cis.upenn.edu/~bcpierce/tapl).
-- So I'm using the simplest, most naive definition I can imagine here.
||| Terms in the lambda calculus extended by arithmetic expressions.
data Term = True
          | False
          | IfThenElse Term Term Term
          | Zero
          | Succ Term
          | Pred Term
          | IsZero Term
          | Var Variable
          | Abs Variable Term
          | App Term Term

||| Convenient infix notation for construction of function application terms
(.) : Term -> Term -> Term
(.) = App

-- TODO: Can we get rid of the argument `n`?
||| Convenience function for constructing lambda terms
lambda : Nat -> (Term -> Term) -> Term
lambda n f = Abs n (f (Var n))

-----------------------------------------------------------------------
-- The stuff below is literally copy pasted from Ch05.LambdaCalculus

--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------

||| The Church boolean true
tru : Term
tru = Abs 1 (Abs 0 (Var 1))

||| The Church boolean false
fls : Term
fls = Abs 1 (Abs 0 (Var 0))

||| Church encoding of the if-then-else operator
test : Term
test = Abs 2 (Abs 1 (Abs 0 (App (App (Var 2) (Var 1)) (Var 0))))

||| Logical AND operator for Church booleans.
and : Term
and = Abs 0 (Abs 1 (App (App (Var 0) (Var 1)) fls))

--------------------------------------------------------------------------------
-- Pairs
--------------------------------------------------------------------------------

||| Church pair constructor
pair : Term
pair = Abs 0 (Abs 1 (Abs 2 (App (App (Var 2) (Var 0)) (Var 1))))

||| Projection onto the first component of a pair
fst : Term
fst = Abs 0 (Abs 1 (Var 0))

||| Projection onto the second component of a pair
snd : Term
snd = Abs 0 (Abs 1 (Var 1))

--------------------------------------------------------------------------------
-- Numerals
--------------------------------------------------------------------------------

||| The Church numeral zero.
church_zero : Term
church_zero = Abs 1 (Abs 0 (Var 0))

||| The Church numeral one.
church_one : Term
church_one = Abs 1 (Abs 0 (App (Var 1) (Var 0)))

||| The Church numeral two.
church_two : Term
church_two = Abs 1 (Abs 0 (App (Var 1) (App (Var 1) (Var 0))))

||| The successors function for Church numerals
scc : Term
scc = Abs 0 (Abs 1 (Abs 2 (App (Var 1) (App (App (Var 0) (Var 1)) (Var 2)))))

||| Addition of Church numerals
plus : Term
plus = Abs 0 (Abs 1 (Abs 2 (Abs 3 ((Var 0) . (Var 2)) . (((Var 1) . (Var 2)) . (Var 3)))))

||| Multiplication of Church numerals
times : Term
times = Abs 0 (Abs 1 ((Var 0) . (plus . (Var 1))) . church_zero)

||| Tests whether a Church numeral is zero or not
iszro : Term
iszro = Abs 0 ((Var 0) . (Abs 0 fls)) . tru

||| The predecessor function on Church numerals
prd : Term
prd = let zz = pair . church_zero . church_zero
          ss = Abs 0 (pair . (snd . (Var 0)) . (scc . (snd . (Var 0)))) in
          Abs 0 (fst . ((Var 0) . ss) . zz)

--------------------------------------------------------------------------------
-- Lists
--------------------------------------------------------------------------------

-- See Ch05.Exercise_5_2_8

--------------------------------------------------------------------------------
-- Self-replicating terms
--------------------------------------------------------------------------------

||| The (?) simplest self-replicating term in the lambda calculus
omega : Term
omega = let x = Var 0
            f = Abs 0 (x . x) in
            f . f

||| The call-by-value version of the fix-point combinator (i.e. Y combinator)
fix : Term
fix = let f = Var 0
          x = Var 1
          y = Var 2
          t = Abs 1 f . (Abs 2 (x . x . y)) in
          Abs 0 (t . t)

-----------------------------------------------------------------------
-- Copy pasted exercises

||| `sub m n` yields the result of subtracting `n` from `m` (Church numerals).
|||
||| More precisely, it yields the smallest church numeral `z` such that
|||
|||     m <= n+z
sub : Term
sub = let m = Var 0
          n = Var 1 in
          Abs 0 (Abs 1 (n . prd) . m)

||| `le m n` tests whether `m` is less than or equal to `n`
le : Term
le = let m = Var 0
         n = Var 1 in
         Abs 0 (Abs 1 (iszro . (sub . m . n)))

||| Test whether two Church numerals are equal
equal : Term
equal = let m = Var 0
            n = Var 1
            m_le_n = le . m . n
            n_le_m = le . n . m in
            Abs 0 (Abs 1 (and . m_le_n . n_le_m))

-----------------------------------------------------------------------
-- Stuff below is lifted wholesale from exercise 5.2.8

-- Lists are represented by their corresponding fold function. That is, a list
-- [x, y, z] is identified with the function
--
--    f |-> ( c |-> f x (f y (f z c))) )
--
-- Where f is any 2-ary function (since the untyped lambda calculus is untyped, of
-- course we can't talk about arities).

||| The term representing the empty list
nil : Term
nil = Abs 0 (Abs 1 (Var 1))--?nil_rhs

||| The term representing the cons combinator
cons : Term
cons = let car = Var 0 -- not to be confused with the car combinator below
           cdr = Var 1 -- --------------------------- cdr ----------------
           f = Var 2
           c = Var 3 in
           Abs 0 (Abs 1 (Abs 2 (Abs 3 (f . car . (cdr . f . c)))))

||| Checks whether a list is nil
isnil : Term
isnil = let l = Var 0
            f = Abs 1 (Abs 2 fls) in
            Abs 0 (l . f . tru)

||| The term representing the "car" combinator
head : Term
head = let l = Var 0 in
           Abs 0 l . fst . nil

||| The term representing the "cdr" combinator
tail : Term
tail = let l = Var 0
           x = Var 1
           y = Var 2
           f = Abs 1 (Abs 2 pair . (snd . y) . (cons . x . (snd . y)))
           c = pair . nil . nil in
           Abs 0 (fst . (l . f . c))

-----------------------------------------------------------------------
-- Stuff below is not copy pasted.

||| Term representing a function converting Church booleans into "real" booleans.
realbool : Term
realbool = lambda 0
                  (\b => b . True . False)

||| Term representing a function converting "real" booleans to Church booleans.
churchbool : Term
churchbool = lambda 0
                    (\b => IfThenElse b tru fls)

||| Term representing a function of two arguments returning a "real" boolean
||| specifying whether they are equal or not, at least if both arguments provided
||| are Church numerals.
realeq : Term
realeq = lambda 0
                (\m => lambda 1
                              (\n => (equal . m . n) . True . False))

||| Term representing a function converting a Church numeral into a primitive natural number
realnat : Term
realnat = lambda 0
                 (\n => n . (lambda 1 (\x => Succ x)) . church_zero) -- TODO: Rename church_zero to c0 etc.

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
longer : String -> String -> Nat
longer word1 word2
	= let len1 = length word1
	      len2 = length word2
      in if len1 > len2 then len1 else len2


text:
module StructuralEquivalents

import Data.DPair
import Data.Nat

namespace Equivalence

  data Singleton : a -> Type where
    Val : (x : a) -> Singleton x

  NonStruct : {a : Type} -> a -> Type
  NonStruct x = Subset a (\y => y = x)

  -- Without respect to zero quantity of the bound
  Rougher : {a : Type} -> a -> Type
  Rougher x = (y : a ** y = x)

namespace BoundedNats

  data Fin : Nat -> Type where
    FZ : Fin n
    FS : Fin n -> Fin $ S n

  NonStruct : Nat -> Type
  NonStruct n = Subset Nat (`LT` n)

  -- Without respect to zero quantity of the bound
  Rougher : Nat -> Type
  Rougher n = (x : Nat ** x `LT` n)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module WebAssembly.Validation.Modules.ElementSegments

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Instructions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#element-segments)
|||
||| ```
||| C.tablex[x] = limits funcref    C ⊢ expr : [i32]    C ⊢ expr const    (C.funcs[y] = functype)*
||| ----------------------------------------------------------------------------------------------
||| C ⊢ {table x, offset expr, init y*} ok
||| ```
public export
data ValidElem : Context -> Elem -> Type where
  MkValidElem  : (c : Context)
              -> (x : TableIdx)
              -> (expr : Expr)
              -> (ys : List FuncIdx)
              -> {auto in_bounds: InBounds x (tables c)}
              -> ValidSequence c expr ([] ->> [TI32])
              -> ConstExpr c expr
              -> (InBounds y ys -> InBounds y (funcs c))
              -> ValidElem c (MkElem x expr ys)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
||| Utilities functions for contitionally delaying values.
module Libraries.Control.Delayed

%default total

||| Type-level function for a conditionally infinite type.
public export
inf : Bool -> Type -> Type
inf False t = t
inf True t = Inf t

||| Type-level function for a conditionally lazy type.
public export
lazy : Bool -> Type -> Type
lazy False t = t
lazy True t = Lazy t


text:
import Data.Vect

proofNil : Vect n elem -> Vect (n + 0) elem
proofNil {n} xs = rewrite plusZeroRightNeutral n in xs

proofNext : Vect (1 + n + k) elem -> Vect (n + (1 + k)) elem
proofNext {n} {k} xs =
  let hypothesis = sym $ plusSuccRightSucc n k
  in rewrite hypothesis
  in xs

go : Vect n elem -> Vect m elem -> Vect (n+m) elem
go acc []        = proofNil acc
go acc (x :: xs) = proofNext (go (x::acc) xs)

total myReverse : Vect len elem -> Vect len elem
myReverse xs = go [] xs

-- total invalidReverseList : List a -> List a
-- invalidReverseList input = []

example: Vect 4 String
example = ["1", "2", "3", "4"]

result: Vect 4 String
result = myReverse example

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module TTImp.Elab.Record

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

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

import Data.List
import Data.Maybe

%default covering

getRecordType : Env Term vars -> NF vars -> Maybe Name
getRecordType env (NTCon _ n _ _ _) = Just n
getRecordType env _ = Nothing

data Rec : Type where
     Field : Maybe Name -> -- implicit argument name, if any
             String -> RawImp -> Rec -- field name on left, value on right
     Constr : Maybe Name -> -- implicit argument name, if any
              Name -> List (String, Rec) -> Rec

Show Rec where
  show (Field mn n ty)
      = "Field " ++ show mn ++ "; " ++ show n ++ " : " ++ show ty
  show (Constr mn n args)
      = "Constr " ++ show mn ++ " " ++ show n ++ " " ++ show args

applyImp : RawImp -> List (Maybe Name, RawImp) -> RawImp
applyImp f [] = f
applyImp f ((Nothing, arg) :: xs)
    = applyImp (IApp (getFC f) f arg) xs
applyImp f ((Just n, arg) :: xs)
    = applyImp (INamedApp (getFC f) f n arg) xs

toLHS' : FC -> Rec -> (Maybe Name, RawImp)
toLHS' loc (Field mn@(Just _) n _)
    = (mn, IAs loc EmptyFC UseRight (UN $ Basic n) (Implicit loc True))
toLHS' loc (Field mn n _) = (mn, IBindVar EmptyFC n)
toLHS' loc (Constr mn con args)
    = let args' = map (toLHS' loc . snd) args in
          (mn, applyImp (IVar loc con) args')

toLHS : FC -> Rec -> RawImp
toLHS fc r = snd (toLHS' fc r)

toRHS' : FC -> Rec -> (Maybe Name, RawImp)
toRHS' loc (Field mn _ val) = (mn, val)
toRHS' loc (Constr mn con args)
    = let args' = map (toRHS' loc . snd) args in
          (mn, applyImp (IVar loc con) args')

toRHS : FC -> Rec -> RawImp
toRHS fc r = snd (toRHS' fc r)

findConName : Defs -> Name -> Core (Maybe Name)
findConName defs tyn
    = case !(lookupDefExact tyn (gamma defs)) of
           Just (TCon _ _ _ _ _ _ [con] _) => pure (Just con)
           _ => pure Nothing

findFields : {auto c : Ref Ctxt Defs} ->
             Defs -> Name ->
             Core (Maybe (List (String, Maybe Name, Maybe Name)))
findFields defs con
    = case !(lookupTyExact con (gamma defs)) of
           Just t => pure (Just !(getExpNames !(nf defs [] t)))
           _ => pure Nothing
  where
    getExpNames : NF [] -> Core (List (String, Maybe Name, Maybe Name))
    getExpNames (NBind fc x (Pi _ _ p ty) sc)
        = do rest <- getExpNames !(sc defs (toClosure defaultOpts [] (Erased fc False)))
             let imp = case p of
                            Explicit => Nothing
                            _ => Just x
             pure $ (nameRoot x, imp, getRecordType [] !(evalClosure defs ty)) :: rest
    getExpNames _ = pure []

genFieldName : {auto u : Ref UST UState} ->
               String -> Core String
genFieldName root
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         pure (root ++ show (nextName ust))

-- There's probably a generic version of this in the prelude isn't
-- there?
replace : String -> Rec ->
          List (String, Rec) -> List (String, Rec)
replace k v [] = []
replace k v ((k', v') :: vs)
    = if k == k'
         then ((k, v) :: vs)
         else ((k', v') :: replace k v vs)

findPath : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           FC -> List String -> List String -> Maybe Name ->
           (String -> RawImp) ->
           Rec -> Core Rec
findPath loc [] full tyn val (Field mn lhs _) = pure (Field mn lhs (val lhs))
findPath loc [] full tyn val rec
   = throw (IncompatibleFieldUpdate loc full)
findPath loc (p :: ps) full Nothing val (Field mn n v)
   = throw (NotRecordField loc p Nothing)
findPath loc (p :: ps) full (Just tyn) val (Field mn n v)
   = do defs <- get Ctxt
        Just con <- findConName defs tyn
             | Nothing => throw (NotRecordType loc tyn)
        Just fs <- findFields defs con
             | Nothing => throw (NotRecordType loc tyn)
        args <- mkArgs fs
        let rec' = Constr mn con args
        findPath loc (p :: ps) full (Just tyn) val rec'
  where
    mkArgs : List (String, Maybe Name, Maybe Name) ->
             Core (List (String, Rec))
    mkArgs [] = pure []
    mkArgs ((p, imp, _) :: ps)
        = do fldn <- genFieldName p
             args' <- mkArgs ps
             -- If it's an implicit argument, leave it as _ by default
             let arg = maybe (IVar EmptyFC (UN $ Basic fldn))
                             (const (Implicit loc False))
                             imp
             pure ((p, Field imp fldn arg) :: args')

findPath loc (p :: ps) full tyn val (Constr mn con args)
   = do let Just prec = lookup p args
                 | Nothing => throw (NotRecordField loc p tyn)
        defs <- get Ctxt
        Just fs <- findFields defs con
             | Nothing => pure (Constr mn con args)
        let Just (imp, mfty) = lookup p fs
                 | Nothing => throw (NotRecordField loc p tyn)
        prec' <- findPath loc ps full mfty val prec
        pure (Constr mn con (replace p prec' args))

getSides : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           FC -> IFieldUpdate -> Name -> RawImp -> Rec ->
           Core Rec
getSides loc (ISetField path val) tyn orig rec
   -- update 'rec' so that 'path' is accessible on the lhs and rhs,
   -- then set the path on the rhs to 'val'
   = findPath loc path path (Just tyn) (const val) rec
getSides loc (ISetFieldApp path val) tyn orig rec
   = findPath loc path path (Just tyn)
      (\n => apply val [IVar EmptyFC (UN $ Basic n)]) rec

getAllSides : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> List IFieldUpdate -> Name ->
              RawImp -> Rec ->
              Core Rec
getAllSides loc [] tyn orig rec = pure rec
getAllSides loc (u :: upds) tyn orig rec
    = getAllSides loc upds tyn orig !(getSides loc u tyn orig rec)

-- Convert the collection of high level field accesses into a case expression
-- which does the updates all in one go
export
recUpdate : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount -> ElabInfo -> FC ->
            NestedNames vars -> Env Term vars ->
            List IFieldUpdate ->
            (rec : RawImp) -> (grecty : Glued vars) ->
            Core RawImp
recUpdate rigc elabinfo iloc nest env flds rec grecty
      = do defs <- get Ctxt
           rectynf <- getNF grecty
           let Just rectyn = getRecordType env rectynf
                    | Nothing => throw (RecordTypeNeeded iloc env)
           fldn <- genFieldName "__fld"
           sides <- getAllSides iloc flds rectyn rec
                                (Field Nothing fldn (IVar vloc (UN $ Basic fldn)))
           pure $ ICase vloc rec (Implicit vloc False) [mkClause sides]
  where
    vloc : FC
    vloc = virtualiseFC iloc

    mkClause : Rec -> ImpClause
    mkClause rec = PatClause vloc (toLHS vloc rec) (toRHS vloc rec)

needType : Error -> Bool
needType (RecordTypeNeeded _ _) = True
needType (InType _ _ err) = needType err
needType (InCon _ _ err) = needType err
needType (InLHS _ _ err) = needType err
needType (InRHS _ _ err) = needType err
needType (WhenUnifying _ _ _ _ _ err) = needType err
needType _ = False

export
checkUpdate : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> ElabInfo ->
              NestedNames vars -> Env Term vars ->
              FC -> List IFieldUpdate -> RawImp -> Maybe (Glued vars) ->
              Core (Term vars, Glued vars)
checkUpdate rig elabinfo nest env fc upds rec expected
    = do recty <- case expected of
                       Just ret => pure ret
                       _ => do (_, ty) <- checkImp rig elabinfo
                                                   nest env rec Nothing
                               pure ty
         let solvemode = case elabMode elabinfo of
                              InLHS c => inLHS
                              _ => inTerm
         delayOnFailure fc rig env (Just recty) needType RecordUpdate $
           \delayed =>
             do solveConstraints solvemode Normal
                exp <- getTerm recty
                -- We can't just use the old NF on the second attempt,
                -- because we might know more now, so recalculate it
                let recty' = if delayed
                                then gnf env exp
                                else recty
                logGlueNF "elab.record" 5 (show delayed ++ " record type " ++ show rec) env recty'
                rcase <- recUpdate rig elabinfo fc nest env upds rec recty'
                log "elab.record" 5 $ "Record update: " ++ show rcase
                check rig elabinfo nest env rcase expected


text:
module Language.LSP.Message.DocumentColor

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

%language ElabReflection
%default total

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor
public export
record DocumentColorOptions where
  constructor MkDocumentColorOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{DocumentColorOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor
public export
record DocumentColorRegistrationOptions where
  constructor MkDocumentColorRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{{DocumentColorRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor
public export
record DocumentColorParams where
  constructor MkDocumentColorParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{{DocumentColorParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor
public export
record Color where
  constructor MkColor
  red   : Double
  green : Double
  blue  : Double
  alpha : Double
%runElab deriveJSON defaultOpts `{{Color}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentColor
public export
record ColorInformation where
  constructor MkColorInformation
  range : Range
  color : Color
%runElab deriveJSON defaultOpts `{{ColorInformation}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_colorPresentation
public export
record ColorPresentationParams where
  constructor MkColorPresentationParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  color              : Color
  range              : Range
%runElab deriveJSON defaultOpts `{{ColorPresentationParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_colorPresentation
public export
record ColorPresentation where
  constructor MkColorPresentation
  label               : String
  textEdit            : Maybe TextEdit
  additionalTextEdits : Maybe (List TextEdit)
%runElab deriveJSON defaultOpts `{{ColorPresentation}}


text:
module Flexidisc.Header.Row

import Flexidisc.Header.Type
import Flexidisc.OrdList
import Flexidisc.OrdList.Row

%default total
%access public export

||| Proof that a key value pair is part of an `OrdList`.  If you don't need the value, use `Label`.
|||
||| @k the inspected key
||| @ty its value
||| @xs the header that contains the information
data Row : (k : l) -> (ty : a) -> (xs : Header' l a) -> Type where
  ||| A wrapper for an OrdList Row
  R : {xs : OrdList l o a} -> OrdRow k ty xs -> Row k ty (H xs)

%name Row lbl, loc, prf, e, elem

||| Map a row and its header simultaneously
mapRow : {xs : Header' k a} -> (f : a -> b) -> (loc : Row l ty xs) -> Row l (f ty) (map f xs)
mapRow f (R loc) = R $ mapRow f loc

||| Given a proof that an element is in a vector, remove it
dropRow : (xs : Header' k a) -> (loc : Row l ty xs) -> Header' k a
dropRow (H xs) (R loc) = H (dropOrdRow xs loc)

||| Update a value in the list given it's location and an update function
changeType : (xs : Header' k a) -> (loc : Row l old xs) ->
             (new : a) -> Header' k a
changeType (H xs) (R loc) = H . changeValue xs loc

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Intro

% access public export

sm : List Nat -> Nat
sm [] = 0
sm (x :: xs) = x + (sm xs)

fct : Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)

fbp : Nat -> (Nat, Nat)
fbp Z = (1, 1)
fbp (S k) = (snd (fbp k), fst (fbp k) + snd (fbp k))

fib : Nat -> Nat
fib n = fst (fbp n)

public export
add : Nat -> Nat -> Nat
add Z j = j
add (S k) j = S (add k j)

mul : Nat -> Nat -> Nat
mul Z j = Z
mul (S k) j = add j (mul k j)

sub : (n: Nat) -> (m : Nat) -> (LTE m n) -> Nat
sub n Z LTEZero = n
sub (S right) (S left) (LTESucc x) = sub right left x

oneLTEFour : LTE 1 4
oneLTEFour = LTESucc LTEZero

fourMinusOne : Nat
fourMinusOne = sub 4 1 oneLTEFour

reflLTE : (n: Nat) -> LTE n n
reflLTE Z = LTEZero
reflLTE (S k) = LTESucc (reflLTE k)

sillyZero: Nat -> Nat
sillyZero n = sub n n (reflLTE n)

idNat : Nat -> Nat
idNat = \x => x

loop: Nat -> Nat
loop k = loop (S k)


text:
-- --------------------------------------------------------------- [ CPTML.idr ]
-- Module    : CPTML.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module GRL.Test.DSML.CPTML

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty

%access public export

data Ty = Cyber | Physical

data MTy = AssTy | MechTy Ty | VulnTy Ty | ThreatTy Ty | ILinkTy | SLinkTy

data CPTML : MTy -> GTy -> Type where
  Asset : String -> CPTML AssTy ELEM

  Mech : (ty : Ty) -> String -> CPTML (MechTy ty) ELEM
  Vuln : (ty : Ty) -> String -> CPTML (VulnTy ty) ELEM
  Threat : (ty : Ty) -> String -> CPTML (ThreatTy ty) ELEM

  HasVuln : CPTML (MechTy ty) ELEM
         -> CPTML (VulnTy ty) ELEM
         -> CPTML SLinkTy STRUCT

  Protects : CPTML (MechTy ty) ELEM
          -> CPTML (AssTy) ELEM
          -> CPTML SLinkTy STRUCT

  Manifest : CPTML (ThreatTy xty) ELEM
          -> CPTML (VulnTy   yty) ELEM
          -> CPTML ILinkTy INTENT

GRL (\x => CPTML ty x) where
  mkElem (Asset t)   = Elem GOALty t Nothing
  mkElem (Mech ty t) = Elem GOALty t Nothing
  mkElem (Vuln ty t) = Elem GOALty t Nothing
  mkElem (Threat ty t)  = Elem TASKty t Nothing

  mkStruct (HasVuln x y)  = SLink IORty (mkElem x) [mkElem y]
  mkStruct (Protects x y) = SLink ANDty (mkElem y) [mkElem x]

  mkIntent (Manifest x y) = ILink IMPACTSty BREAK (mkElem x) (mkElem y)

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


text:
||| Library for termios.h and similar actions in Idris
module Termios.POSIX

import Control.ST
import Control.ST.ImplicitCall
import CFFI
import public Terminos

%include C "sys/ioctl.h"
%include C "signal.h"
%lib C "termios"
%include C "Termios/termios_helper.h"
%link C "Termios/termios_helper.o"

%default total

||| Type alias for IO' FFI_C
public export Cio : Type -> Type
Cio = IO' FFI_C

||| Selects what to do for a given mode, only one option for now
modeSelect : (mode : TerminalMode) -> Type
modeSelect TUI = Termios Cio

||| Implementation of FancyConsole for the standard POSIX IO terminal
public export Termios Cio where
  Status mode = State (modeSelect mode)
  initialize = ?initialize_rhs1 (foreign FFI_C "initialize" (Cio ()))
  cleanup {terminal} = ?cleanup_rhs1 (foreign FFI_C "restore" (Cio ()) )
  getCh = lift $ foreign FFI_C "wgetch" (Cio Char)

-- Reference code to both check that the types are sane, and to run integration tests
using (Termios Cio)
  partial
  runCmd : ST Cio () []
  runCmd = do initialize
              someString1 <- getStr
              someString2 <- Control.ST.getStr
              someChar1 <- getCh
              someChar2 <- Termios.getCh
              putChar someChar2
              Control.ST.putChar someChar1
              putStr someString2
              Control.ST.putStr someString1
              cleanup

partial main : Cio ()
main = run runCmd

max_stars_repo_name: zenntenn/Idris-Termios

max_issues_repo_name: zenntenn/Idris-Termios

max_forks_repo_name: zenntenn/Idris-Termios


text:
module Main

-- base
import Data.List
import System.File

-- contrib
import Text.Parser
import Text.Parser.Core

data Direction = East
               | SouthEast
               | SouthWest
               | West
               | NorthEast
               | NorthWest

Eq Direction where
  (==) East East = True
  (==) SouthEast SouthEast = True
  (==) SouthWest SouthWest = True
  (==) West West = True
  (==) NorthEast NorthEast = True
  (==) NorthWest NorthWest = True
  (==) _ _ = False

Show Direction where
  show East = "East"
  show SouthEast = "SouthEast"
  show SouthWest = "SouthWest"
  show West = "West"
  show NorthEast = "NorthEast"
  show NorthWest = "NorthWest"

namespace Grammar
  eastWestGrammar : Grammar Char True Direction
  eastWestGrammar = terminal "Can't parse East" $ \ x =>
                    case x of
                         'e' => Just East
                         'w' => Just West
                         _ => Nothing

  northGrammar : Grammar Char True Direction
  northGrammar = terminal "Can't parse North" checkN *> terminal "Can't parse North-?" checkEW where
    checkN : Char -> Maybe ()
    checkN 'n' = Just ()
    checkN _ = Nothing

    checkEW : Char -> Maybe Direction
    checkEW 'e' = Just NorthEast
    checkEW 'w' = Just NorthWest
    checkEW _ = Nothing

  southGrammar : Grammar Char True Direction
  southGrammar = terminal "Can't parse South" checkS *> terminal "Can't parse South-?" checkEW where
    checkS : Char -> Maybe ()
    checkS 's' = Just ()
    checkS _ = Nothing

    checkEW : Char -> Maybe Direction
    checkEW 'e' = Just SouthEast
    checkEW 'w' = Just SouthWest
    checkEW _ = Nothing

  directionGrammar : Grammar Char True Direction
  directionGrammar = eastWestGrammar <|> northGrammar <|> southGrammar

  directionsGrammar : Grammar Char True (List Direction)
  directionsGrammar = many directionGrammar <* terminal "Can't parse newline" checkNewline where
    checkNewline : Char -> Maybe ()
    checkNewline '\n' = Just ()
    checkNewline _ = Nothing

  export
  dataGrammar : Grammar Char False (List (List Direction))
  dataGrammar = many directionsGrammar <* eof

record HexVector where
  constructor MkHexVector
  east, southeast, southwest : Integer

Eq HexVector where
  (==) (MkHexVector x y z) (MkHexVector x' y' z') = x == x' && y == y' && z == z'

Show HexVector where
  show (MkHexVector east southeast southwest) = "HexVector " ++ show east ++ " " ++ show southeast ++ " " ++ show southwest

namespace HexVector
  succ : Integer -> Integer
  succ = (+ 1)

  pred : Integer -> Integer
  pred x = x - 1

  export
  toHexVector : List Direction -> HexVector
  toHexVector [] = MkHexVector 0 0 0
  toHexVector (East :: xs) = record { east $= succ } (toHexVector xs)
  toHexVector (SouthEast :: xs) = record { southeast $= succ } (toHexVector xs)
  toHexVector (SouthWest :: xs) = record { southwest $= succ } (toHexVector xs)
  toHexVector (West :: xs) = record { east $= pred } (toHexVector xs)
  toHexVector (NorthEast :: xs) = record { southwest $= pred } (toHexVector xs)
  toHexVector (NorthWest :: xs) = record { southeast $= pred } (toHexVector xs)

record Coordinate where
  constructor MkCoordinate
  xCoord, yCoord : Integer

Eq Coordinate where
  (==) (MkCoordinate x y) (MkCoordinate x' y') = x == x' && y == y'

Show Coordinate where
  show (MkCoordinate x y) = "Coordinate " ++ show x ++ " " ++ show y

toCoordinate : HexVector -> Coordinate
toCoordinate (MkHexVector east southeast southwest) = MkCoordinate x y where
  x : Integer
  x = 2 * east + southeast - southwest
  y : Integer
  y = southeast + southwest

namespace countElements
  -- removes duplicates
  export
  elements : Eq a => List a -> List a -> List a
  elements [] acc = acc
  elements (x :: xs) acc with (find (== x) acc)
    elements (x :: xs) acc | Nothing = elements xs (x :: acc)
    elements (x :: xs) acc | (Just _) = elements xs acc

  occurrences : Eq a => a -> List a -> Nat
  occurrences x [] = Z
  occurrences x (y :: xs) with (x == y)
    occurrences x (y :: xs) | True = S $ occurrences x xs
    occurrences x (y :: xs) | False = occurrences x xs

  export
  countElements : List Coordinate -> List (Coordinate,Nat)
  countElements xs = f <$> elements xs [] where
    f : Coordinate -> (Coordinate,Nat)
    f x = (x,occurrences x xs)

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

adjacentCoordinates : Coordinate -> List Coordinate
adjacentCoordinates (MkCoordinate xCoord yCoord) =
  [ MkCoordinate (xCoord - 2) yCoord
  , MkCoordinate (xCoord + 2) yCoord
  , MkCoordinate (xCoord - 1) (yCoord + 1)
  , MkCoordinate (xCoord - 1) (yCoord - 1)
  , MkCoordinate (xCoord + 1) (yCoord + 1)
  , MkCoordinate (xCoord + 1) (yCoord - 1)
  ]

-- adjacent to: c, list of blacks: cs
countAdjacentBlacks : Coordinate -> List Coordinate -> Nat
countAdjacentBlacks c cs = length $ filter id (f <$> adjacentCoordinates c) where
  f : Coordinate -> Bool
  f adjC = case find (== adjC) cs of
                Nothing => False
                (Just _) => True

blacksToWhites : List Coordinate -> List Coordinate
blacksToWhites blacks = elements (foldr f prepWhites blacks) [] where
  prepWhites : List Coordinate
  prepWhites = concat $ adjacentCoordinates <$> blacks
  f : Coordinate -> List Coordinate -> List Coordinate
  f c cs = filter (/= c) cs

flipOnce : List Coordinate -> List Coordinate
flipOnce blacks = newBlacks where
  whites : List Coordinate
  whites = blacksToWhites blacks
  blacksWithAdjacentBlacks : List (Coordinate,Nat)
  blacksWithAdjacentBlacks = (\ c => (c,countAdjacentBlacks c blacks)) <$> blacks
  whitesWithAdjacentBlacks : List (Coordinate,Nat)
  whitesWithAdjacentBlacks = (\ c => (c,countAdjacentBlacks c blacks)) <$> whites
  newBlacks : List Coordinate
  newBlacks = elements (map fst (filter (\ (_,n) => not (n == 0 || n > 2)) blacksWithAdjacentBlacks ++ filter (\ (_,n) => n == 2) whitesWithAdjacentBlacks)) []

flipTimes : Nat -> List Coordinate -> List Coordinate
flipTimes 0 cs = cs
flipTimes (S n) cs = flipTimes n $ flipOnce cs

main : IO ()
main = do
  inputData <- readFile "./data"
  case inputData of
       Left err => print err
       Right dat => do
         let tokenList = unpack dat
             directions = parse dataGrammar tokenList
         case directions of
              (Left (Error err _)) => putStrLn err
              (Right (ds,cs)) => do
                --print ds
                let vecs = toHexVector <$> ds
                --print vecs
                let coords = toCoordinate <$> vecs
                --print coords
                let counts = countElements coords
                    flips = snd <$> counts
                    countBlacks = length $ filter odd flips
                --print countBlacks
                -- part 2
                let blackCountsOdd = filter (\ (_,c) => odd c) counts
                    blacks = fst <$> blackCountsOdd
                    newBlacks = flipTimes 100 blacks
                    countNewBlacks = length newBlacks
                print countNewBlacks
         pure ()
  pure ()


text:
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016, 2019
module Network.Socket

import public Network.Socket.Data
import Network.Socket.Raw
import Data.List
import Network.FFI

-- ----------------------------------------------------- [ Network Socket API. ]

||| Creates a UNIX socket with the given family, socket type and protocol
||| number. Returns either a socket or an error.
export
socket : HasIO io
      => (fam  : SocketFamily)
      -> (ty   : SocketType)
      -> (pnum : ProtocolNumber)
      -> io (Either SocketError Socket)
socket sf st pn = do
  socket_res <- primIO $ prim__idrnet_socket (toCode sf) (toCode st) pn
  errorNumber <- getErrno
  if errorNumber /= 0
    then pure $ Left errorNumber
    else pure $ Right (MkSocket socket_res sf st pn)

||| Close a socket
export
close : HasIO io => Socket -> io ()
close sock = do _ <- primIO $ prim__idrnet_close $ descriptor sock
                pure ()

||| Binds a socket to the given socket address and port.
||| Returns 0 on success, an error code otherwise.
export
bind : HasIO io
    => (sock : Socket)
    -> (addr : Maybe SocketAddress)
    -> (port : Port)
    -> io Int
bind sock addr port = do
    bind_res <- primIO $ prim__idrnet_bind
                  (descriptor sock)
                  (toCode $ family sock)
                  (toCode $ socketType sock)
                  (saString addr)
                  port

    if bind_res == (-1)
      then getErrno
      else pure 0
  where
    saString : Maybe SocketAddress -> String
    saString (Just sa) = show sa
    saString Nothing   = ""

||| Connects to a given address and port.
||| Returns 0 on success, and an error number on error.
export
connect : HasIO io
       => (sock : Socket)
       -> (addr : SocketAddress)
       -> (port : Port)
       -> io ResultCode
connect sock addr port = do
  conn_res <- primIO $ prim__idrnet_connect
              (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port

  if conn_res == (-1)
    then getErrno
    else pure 0

||| Listens on a bound socket.
|||
||| @sock The socket to listen on.
export
listen : HasIO io => (sock : Socket) -> io Int
listen sock = do
  listen_res <- primIO $ prim__idrnet_listen (descriptor sock) BACKLOG
  if listen_res == (-1)
    then getErrno
    else pure 0

||| Accept a connection on the provided socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success a pairing of:
||| + `Socket`        :: The socket representing the connection.
||| + `SocketAddress` :: The
|||
||| @sock The socket used to establish connection.
export
accept : HasIO io
      => (sock : Socket)
      -> io (Either SocketError (Socket, SocketAddress))
accept sock = do

  -- We need a pointer to a sockaddr structure. This is then passed into
  -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.

  sockaddr_ptr <- primIO prim__idrnet_create_sockaddr

  accept_res <- primIO $ prim__idrnet_accept (descriptor sock) sockaddr_ptr
  errorNumber <- getErrno
  if errorNumber /= 0
    then pure $ Left errorNumber
    else do
      let (MkSocket _ fam ty p_num) = sock
      sockaddr <- getSockAddr (SAPtr sockaddr_ptr)
      sockaddr_free (SAPtr sockaddr_ptr)
      pure $ Right ((MkSocket accept_res fam ty p_num), sockaddr)

||| Send data on the specified socket.
|||
||| Returns on failure a `SocketError`.
||| Returns on success the `ResultCode`.
|||
||| @sock The socket on which to send the message.
||| @msg  The data to send.
export
send : HasIO io
    => (sock : Socket)
    -> (msg  : String)
    -> io (Either SocketError ResultCode)
send sock dat = do
  send_res <- primIO $ prim__idrnet_send (descriptor sock) dat

  if send_res == (-1)
    then map Left getErrno
    else pure $ Right send_res

||| Receive data on the specified socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success a pairing of:
||| + `String`     :: The payload.
||| + `ResultCode` :: The result of the underlying function.
|||
||| @sock The socket on which to receive the message.
||| @len  How much of the data to receive.
export
recv : HasIO io
    => (sock : Socket)
    -> (len : ByteLength)
    -> io (Either SocketError (String, ResultCode))
recv sock len = do
  -- Firstly make the request, get some kind of recv structure which
  -- contains the result of the recv and possibly the retrieved payload
  recv_struct_ptr <- primIO $ prim__idrnet_recv (descriptor sock) len
  recv_res <- primIO $ prim__idrnet_get_recv_res recv_struct_ptr

  if recv_res == (-1)
    then do
      errno <- getErrno
      freeRecvStruct (RSPtr recv_struct_ptr)
      pure $ Left errno
    else
      if recv_res == 0
        then do
           freeRecvStruct (RSPtr recv_struct_ptr)
           pure $ Left 0
        else do
           payload <- primIO $ prim__idrnet_get_recv_payload recv_struct_ptr
           freeRecvStruct (RSPtr recv_struct_ptr)
           pure $ Right (payload, recv_res)

||| Receive all the remaining data on the specified socket.
|||
||| Returns on failure a `SocketError`
||| Returns on success the payload `String`
|||
||| @sock The socket on which to receive the message.
export
recvAll : HasIO io => (sock : Socket) -> io (Either SocketError String)
recvAll sock = recvRec sock [] 64
  where
    partial
    recvRec : Socket -> List String -> ByteLength -> io (Either SocketError String)
    recvRec sock acc n = do res <- recv sock n
                            case res of
                              Left c => pure (Left c)
                              Right (str, res) => let n' = min (n * 2) 65536 in
                                                  if res < n then pure (Right $ concat $ reverse $ str :: acc)
                                                  else recvRec sock (str :: acc) n'

||| Send a message.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @addr Address of the recipient.
||| @port The port on which to send the message.
||| @msg  The message to send.
export
sendTo : HasIO io
      => (sock : Socket)
      -> (addr : SocketAddress)
      -> (port : Port)
      -> (msg  : String)
      -> io (Either SocketError ByteLength)
sendTo sock addr p dat = do
  sendto_res <- primIO $ prim__idrnet_sendto
                (descriptor sock) dat (show addr) p (toCode $ family sock)

  if sendto_res == (-1)
    then map Left getErrno
    else pure $ Right sendto_res

||| Receive a message.
|||
||| Returns on failure a `SocketError`.
||| Returns on success a triple of
||| + `UDPAddrInfo` :: The address of the sender.
||| + `String`      :: The payload.
||| + `Int`         :: Result value from underlying function.
|||
||| @sock The channel on which to receive.
||| @len  Size of the expected message.
|||
export
recvFrom : HasIO io
        => (sock : Socket)
        -> (len  : ByteLength)
        -> io (Either SocketError (UDPAddrInfo, String, ResultCode))
recvFrom sock bl = do
  recv_ptr <- primIO $ prim__idrnet_recvfrom
                       (descriptor sock) bl

  let recv_ptr' = RFPtr recv_ptr
  isNull <- (nullPtr recv_ptr)
  if isNull
    then map Left getErrno
    else do
      result <- primIO $ prim__idrnet_get_recvfrom_res recv_ptr
      if result == -1
        then do
          freeRecvfromStruct recv_ptr'
          map Left getErrno
        else do
          payload <- foreignGetRecvfromPayload recv_ptr'
          port <- foreignGetRecvfromPort recv_ptr'
          addr <- foreignGetRecvfromAddr recv_ptr'
          freeRecvfromStruct recv_ptr'
          pure $ Right (MkUDPAddrInfo addr port, payload, result)


text:
module Shape

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

private
rectangle_area : Double -> Double -> Double
rectangle_area x y = x * y

export
area : Shape -> Double
area (Triangle x y) = 0.5 * rectangle_area x y
area (Rectangle x y) = rectangle_area x y
area (Circle x) = pi * x * x

-- 10.3 Ex # 2
public export
data ShapeView : (s : Shape) -> Type where
     VTri : ShapeView (Triangle base height)
     VRect : ShapeView (Rectangle width height)
     VCirc : ShapeView (Circle r)

shapeView : (s : Shape) -> ShapeView s
shapeView (Triangle x y) = VTri
shapeView (Rectangle x y) = VRect
shapeView (Circle x) = VCirc

narea : Shape -> Double
narea x with (shapeView x)
  narea (Triangle base height) | VTri = 0.5 * base * height
  narea (Rectangle width height) | VRect = width * height
  narea (Circle r) | VCirc = pi * r * r


text:
import Data.Vect

plus' : Nat -> Nat -> Nat
plus' Z m = m
plus' (S k) m = S (plus' k m)

fourEq : 4 = 4
fourEq = Refl

twoPlusTwoEqFour : 2 + 2 = 4
twoPlusTwoEqFour = Refl

plusReducesZ : (m : Nat) -> plus' Z m = m
plusReducesZ m = Refl

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

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

natInduction : (p : Nat -> Type) -> (p Z) -> ((k : Nat) -> p k -> p (S k)) -> (x : Nat) -> p x
natInduction p pZ pS Z = pZ
natInduction p pZ pS (S k) = pS k (natInduction p pZ pS k)

plusInd : Nat -> Nat -> Nat
plusInd n m = natInduction (\x => Nat) m (\k, kRec => S kRec) n

-- plusCommutesZ : m = plus' m 0
-- plusCommutesZ {m = Z} = Refl
-- plusCommutesZ {m = (S k)} =
--     let rec = plusCommutesZ {m = k} in cong rec

-- plusCommutesSk : (k : Nat) -> (m : Nat) -> S (plus' m k) = plus' m (S k)
-- plusCommutesSk k Z = Refl
-- plusCommutesSk k (S j) = cong $ plusCommutesSk k j

-- plusCommutes : (n, m : Nat) -> plus' n m = plus' m n
-- plusCommutes Z m = plusCommutesZ
-- plusCommutes (S k) m = rewrite plusCommutes k m in plusCommutesSk k m

-- plusCommutes : (n, m : Nat) -> plus' n m = plus' m n
-- plusCommutes n m = natInduction (\x => plus' x m = plus' m x) ?rest

plusAssoc : (n, m, p : Nat) -> plus' n (plus' m p) = plus' (plus' n m) p


text:
module SVG

import Js.VirtualDom
import Js.Html
import Js.HtmlStyle
import Data.Vect
import Js.Utils

public export
SVG : Type -> Type
SVG a = Node 'SVG a

export
interface SVGAllAttribute (o : Type) where

export
interface SVGShapeAttribute (o : Type) where

svgNS : String
svgNS = "http://www.w3.org/2000/svg"

xlinkNS : String
xlinkNS = "http://www.w3.org/1999/xlink"

export
svg : List (HtmlAttribute a) -> List (SVG a) -> Html a
svg attrs childs = nodeNS svgNS "svg" attrs (believe_me childs)

export
transform : SVGAllAttribute o => Transform -> Attribute o a
transform x = style $ HtmlStyle.transform x

export
nonSelectable : SVGAllAttribute o => Attribute o a
nonSelectable = style $ userSelect None

export
fill : SVGShapeAttribute o => String -> Attribute o a
fill x = style $ HtmlStyle.fill x

export
stroke : SVGShapeAttribute o => String -> Attribute o a
stroke p = stringAttribute "stroke" p

export
strokeWidth : SVGShapeAttribute o => Double -> Attribute o a
strokeWidth p = stringAttribute "stroke-width" $ show p

namespace Polygon
  export
  implementation SVGAllAttribute 'Polygon where

  export
  implementation SVGShapeAttribute 'Polygon where

  export
  points : List (Double, Double) -> Attribute 'Polygon a
  points pts = stringAttribute "points" $ unwords $ map (\(x,y) => show x ++ " " ++ show y) pts

  export
  polygon : List (Attribute 'Polygon a) -> SVG a
  polygon attrs = nodeNS svgNS "polygon" attrs []

namespace Rect
  export
  implementation SVGAllAttribute 'Rect where

  export
  implementation SVGShapeAttribute 'Rect where

  export
  x : Double -> Attribute 'Rect a
  x p = stringAttribute "x" $ show p

  export
  y : Double -> Attribute 'Rect a
  y p = stringAttribute "y" $ show p

  export
  width : Double -> Attribute 'Rect a
  width p = stringAttribute "width" $ show $ max 0 p

  export
  height : Double -> Attribute 'Rect a
  height p = stringAttribute "height" $ show $ max 0 p

  export
  rect : List (Attribute 'Rect a) -> SVG a
  rect attrs = nodeNS svgNS "rect" (attrs ++ [x (-1), y (-1), width 2, height 2]) []

namespace Image
  export
  implementation SVGAllAttribute 'Image where

  export
  x : Double -> Attribute 'Image a
  x p = stringAttribute "x" $ show p

  export
  y : Double -> Attribute 'Image a
  y p = stringAttribute "y" $ show p

  export
  width : Double -> Attribute 'Image a
  width p = stringAttribute "width" $ show $ max 0 p

  export
  height : Double -> Attribute 'Image a
  height p = stringAttribute "height" $ show $ max 0 p

  export
  image : List (Attribute 'Image a) -> String -> SVG a
  image attrs url =
    nodeNS
      svgNS
      "image"
      ( attrs
      ++ [ stringAttributeNS xlinkNS "xlink:href" url
         , x (-1)
         , y (-1)
         , width 2
         , height 2
         ]
      )
      []

namespace Text
  export
  implementation SVGAllAttribute 'Text where

  export
  x : Double -> Attribute 'Text a
  x p = stringAttribute "x" $ show p

  export
  y : Double -> Attribute 'Text a
  y p = stringAttribute "y" $ show p

  export
  fontSize : Double -> Attribute 'Text a
  fontSize x = stringAttribute "font-size" $ show x

  public export
  data TextAnchor = Start | End | Middle

  anchorToString : TextAnchor -> String
  anchorToString Start = "start"
  anchorToString End = "end"
  anchorToString Middle = "middle"

  export
  textAnchor : TextAnchor -> Attribute 'Text a
  textAnchor p = stringAttribute "text-anchor" $ anchorToString p

  export
  text : List (Attribute 'Text a) -> String -> SVG a
  text opts t = nodeNS svgNS "text" opts [text t]

namespace Circle
  export
  implementation SVGAllAttribute 'Circle where

  export
  implementation SVGShapeAttribute 'Circle where

  export
  r : Double -> Attribute 'Circle a
  r x = stringAttribute "r" $ show x

  export
  cx : Double -> Attribute 'Circle a
  cx x = stringAttribute "cx" $ show x

  export
  cy : Double -> Attribute 'Circle a
  cy x = stringAttribute "cy" $ show x

  export
  circle : List (Attribute 'Circle a) -> SVG a
  circle attrs = nodeNS svgNS "circle" (attrs ++ [r 1]) []

namespace Group
  export
  implementation SVGAllAttribute 'Group where

  export
  g : List (Attribute 'Group a) -> List (SVG a) -> SVG a
  g = nodeNS svgNS "g"

export
onclick : SVGAllAttribute o => a -> Attribute o a
onclick x = eventListenerAttribute "click" (\_ => pure x)

export
onlongpress : SVGAllAttribute o => a -> Attribute o a
onlongpress x = customEventListenerAttribute "longpress" (jscall "$JSLIB$html.addLongPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

export
onshortpress : SVGAllAttribute o => a -> Attribute o a
onshortpress x = customEventListenerAttribute "shortpress" (jscall "$JSLIB$html.addShortPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

export
data FilterRef = MkFilterRef String

public export
data Effect = FeColorMatrix (Vect 4 (Vect 5 Double))

matrixToAttr : Vect n (Vect m Double) -> String
matrixToAttr x =
  unwords $ map (\y=> unwords (map show $ toList y) ) $ toList x

effToSVG : Effect -> SVG a
effToSVG {a} (FeColorMatrix m) =
  nodeNS
    svgNS
    "feColorMatrix"
    (the (List (Attribute 'SVG a)) $ [stringAttribute "type" "matrix", stringAttribute "values" $ matrixToAttr m])
    []

export
filterDef : List Effect -> (FilterRef -> SVG a) -> SVG a
filterDef {a} effs x =
  let
      i = unsafePerformIO $ randomInt 999999999
      i' = "f" ++ show i
      defs = the (SVG a) $
        nodeNS
          svgNS
          "defs"
          (the (List (Attribute 'SVG a)) $ [])
          [ the (SVG a) $ nodeNS svgNS "filter" [the (Attribute 'SVG a) $ stringAttribute "id" i'] (map effToSVG effs)
          ]
  in
    g
      []
      [defs, x $ MkFilterRef i']

export
filter : SVGAllAttribute o => FilterRef -> Attribute o a
filter (MkFilterRef x) = stringAttribute "filter" ("url(#" ++ x ++ ")")

export
Cast (Fin n) Double where
  cast x = cast (the Nat $ cast x)

export
Cast Double Nat where
  cast x = cast (the Integer $ cast x)

public export
record Cell where
  constructor MkCellBase
  cleft : Double
  ctop : Double
  cwidth : Double
  cheight : Double
  cmarginLeft : Double
  cmarginRight : Double
  cmarginTop : Double
  cmarginBottom : Double

export
cbottom : Cell -> Double
cbottom x = ctop x + cheight x

export
cright : Cell -> Double
cright x = cleft x + cwidth x

export
cXcenter : Cell -> Double
cXcenter x = cleft x + cmarginLeft x + (cwidth x - cmarginLeft x - cmarginRight x) /2

export
cYcenter : Cell -> Double
cYcenter x = ctop x + cmarginTop x + (cheight x - cmarginTop x - cmarginBottom x) /2

export
cinnerWidth : Cell -> Double
cinnerWidth x = cwidth x - cmarginLeft x - cmarginRight x

export
cinnerHeigth : Cell -> Double
cinnerHeigth x = cheight x - cmarginTop x - cmarginBottom x

export
fitToCellTransform : Cell -> Transform
fitToCellTransform x = translate (cXcenter x) (cYcenter x) <+> scale (cinnerWidth x / 2) (cinnerHeigth x / 2)

public export
mkCell : Double -> Double -> Double -> Double -> Double -> Cell
mkCell left top width height margin = MkCellBase left top width height margin margin margin margin

public export
Grid : Nat -> Nat -> Type
Grid i j = Fin i -> Fin j -> Cell

public export
Flow : Type
Flow = Nat -> Cell

export total
bestFitFlowCentered : Double -> Double -> Double -> Double -> Double -> Double -> Flow
bestFitFlowCentered cellWidth cellHeight margin top left right z =
  let cols = cast $ ((right - left) / cellHeight) - 1
      leftstart = left + (right - left - (cast $ S cols) * cellWidth)/2
  in mkCell
            (leftstart + (cast $ modNatNZ z (S cols) SIsNotZ) * cellWidth)
            (top + (cast $ divNatNZ z (S cols) SIsNotZ) * cellHeight)
            cellWidth
            cellHeight
            margin

export
centeredSquaresGrid : (i:Nat) -> (j:Nat) -> Double -> Double -> Double -> Double -> Double -> Grid i j
centeredSquaresGrid i j cellMargin left right top bottom =
  let side = min ( (bottom - top ) / cast i ) ( ( right - left) / cast j )
      margin' = if cellMargin * 3 < side then cellMargin else 0.0
      topstart = top + (bottom - top - cast i * side)/2
      leftstart = left + (right - left - cast j * side)/2
  in (\x,y => mkCell (cast y * side + leftstart) (cast x * side + topstart) side side margin')

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
import Data.List.Views

mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) =
    merge (mergeSort lefts | lrec) (mergeSort rights | rrec)


text:
module Flexidisc.Validation

%default total
%access public export

data Validation e a = Error e | Valid a

ValidationL : (e, a :Type) -> Type
ValidationL e a = Validation (List e) a

implementation Functor (Validation e) where
  map func (Error x) = Error x
  map func (Valid x) = Valid (func x)

implementation Semigroup e => Applicative (Validation e) where
  pure x = Valid x
  (<*>) (Error x) (Error y) = Error (x <+> y)
  (<*>) (Error x) (Valid _) = Error x
  (<*>) (Valid _) (Error y) = Error y
  (<*>) (Valid f) (Valid x) = Valid (f x)

implementation (Show e, Show a) => Show (Validation e a) where
  show (Error x) = "❌ " <+> show x
  show (Valid x) = "✅ " <+> show x

export
validate : (a -> e) -> (a -> Bool) -> a -> Validation e a
validate err f x = if f x then Valid x else Error (err x)

export
validateL : (Applicative f, Semigroup (f e)) => (a -> e) -> (a -> Bool) -> a -> Validation (f e) a
validateL err f x = if f x then Valid x else Error (pure (err x))


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

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case m == len of
                                 False => Nothing
                                 True => Just ?exactLength_rhs_2


text:
module adder

adderTy : Nat -> Type
adderTy Z = Nat
adderTy (S k) = Nat -> adderTy k

adder : (k : Nat) -> Nat -> adderTy k
adder Z     acc = acc
adder (S k) acc = \ x => adder k (x + acc)

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Main

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

main : IO ()
main = putStrLn $ show $ even $ sum [1,3,4,5,2]

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Commons.Control.Logging.Log4Idris

import Control.IOExcept
import Control.ST

%default total
%access export

public export
data LogLevel : Type where
  OFF : LogLevel

  ||| A fine-grained debug message, typically capturing the flow through
  ||| the application.
  TRACE : LogLevel

  ||| A general debugging event.
  DEBUG : LogLevel

  |||  An event for informational purposes.
  INFO : LogLevel

  ||| An event that might possible lead to an error.
  WARN : LogLevel

  ||| An error in the application, possibly recoverable.
  ERROR : LogLevel

  ||| A severe error that will prevent the application from continuing.
  FATAL : LogLevel

  ||| All events should be logged.
  ALL : LogLevel

export
Cast LogLevel Nat where
  cast OFF   = 0
  cast TRACE = 10
  cast DEBUG = 20
  cast INFO = 30
  cast WARN = 40
  cast ERROR = 50
  cast FATAL = 60
  cast ALL = 70

export
Eq LogLevel where
  (==) x y = cast {to=Nat} x == cast {to=Nat} y

export
Ord LogLevel where
  compare x y = compare (cast {to=Nat} x) (cast {to=Nat} y)

public export
interface Logging (m : Type -> Type) where
  Logger : Type

  startLogging : (lvl : LogLevel)
              -> ST m (Var) [add Logger]

  setLevel : (logger : Var)
          -> (n : LogLevel)
          -> ST m () [logger ::: Logger]

  log : (logger : Var)
     -> (lvl    : LogLevel)
     -> (msg    : String)
     -> ST m () [logger ::: Logger]

  endLogging : (logger : Var)
            -> ST m () [remove logger Logger]

public export
Logging IO where
  Logger = State LogLevel

  startLogging lvl = do
    logger <- new lvl
    pure logger

  setLevel logger n = write logger n

  log logger lvl msg = do
    curr <- read logger
    case compare lvl curr of
      GT => pure ()
      _  => do
        putStr $ unwords [show (cast {to=Nat} lvl), ":", msg]
        pure ()

  endLogging logger = delete logger

public export
Logging (IOExcept err) where
  Logger = State LogLevel

  startLogging lvl = do
    logger <- new lvl
    pure logger

  setLevel logger new = write logger new

  log logger lvl msg = do
    curr <- read logger
    case compare lvl curr of
      GT => pure ()
      _  => do
        putStr $ unwords [show (cast {to=Nat} lvl), ":", msg]
        pure ()

  endLogging logger = delete logger

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Buffer

import Data.Buffer
import Data.Buffer.Ext

main : IO ()
main = do
  let strings =
    [ "árvíztűrő tükörfúrógép"
    , "明日の待ち合わせは、初めて訪れる場所です。あなたは事前に何をしますか？"
    , """
      А а 	Б б 	В в 	Г г 	Д д 	Е е 	Ё ё 	Ж ж 	З з 	И и 	Й й
      К к 	Л л 	М м 	Н н 	О о 	П п 	Р р 	С с 	Т т 	У у 	Ф ф
      Х х 	Ц ц 	Ч ч 	Ш ш 	Щ щ 	Ъ ъ 	Ы ы 	Ь ь 	Э э 	Ю ю 	Я я
      """
    ]

  for_ strings $ \s =>
    let buffer : Buffer = fromString s
        converted : String = show buffer
    in
      when (s /= converted) $ putStrLn "Original: \{s}\nConverted: \{converted}"

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
||| Tokenise a source line for easier processing
module Idris.IDEMode.TokenLine

import Parser.Lexer.Source
import Text.Lexer

%default total

public export
RawName : Type
RawName = String

public export
data SourcePart
  = Whitespace String
  | Name RawName
  | HoleName String
  | LBrace
  | RBrace
  | Equal
  | Other String

------------------------------------------------------------------------
-- Printer
------------------------------------------------------------------------

export
toString : SourcePart -> String
toString (Whitespace str) = str
toString (Name n) = n
toString (HoleName n) = "?" ++ n
toString LBrace = "{"
toString RBrace = "}"
toString Equal = "="
toString (Other str) = str

------------------------------------------------------------------------
-- Parser
------------------------------------------------------------------------

holeIdent : Lexer
holeIdent = is '?' <+> identNormal

srcTokens : TokenMap SourcePart
srcTokens =
    [(identNormal, Name),
     (holeIdent, \x => HoleName (assert_total (prim__strTail x))),
     (space, Whitespace),
     (is '{', const LBrace),
     (is '}', const RBrace),
     (is '=', const Equal),
     (any, Other)]

export
tokens : String -> List SourcePart
tokens str
    = case lex srcTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (srctoks, (l, c, rest)) =>
              map val srctoks ++ (if rest == "" then [] else [Other rest])


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String

import System.File

data Bracket = P | S | B | L
Eq Bracket where
  P == P = True
  S == S = True
  B == B = True
  L == L = True
  _ == _ = False
data Chunk = Open Bracket | Close Bracket

findCorrupted : List Bracket -> List Chunk -> Maybe Bracket
findCorrupted s [] = Nothing
findCorrupted s ((Open x) :: xs) = findCorrupted (x :: s)  xs
findCorrupted [] ((Close x) :: xs) = Just x
findCorrupted (y :: ys) ((Close x) :: xs) = if x == y
                                       then findCorrupted ys xs
                                       else Just x

score : Bracket -> Nat
score P = 3
score S = 57
score B = 1197
score L = 25137

parseChunk : Char -> Maybe Chunk
parseChunk '(' = Just $ Open P
parseChunk ')' = Just $ Close P
parseChunk '[' = Just $ Open S
parseChunk ']' = Just $ Close S
parseChunk '{' = Just $ Open B
parseChunk '}' = Just $ Close B
parseChunk '<' = Just $ Open L
parseChunk '>' = Just $ Close L
parseChunk _ = Nothing
parseChunks : List Char -> List (Maybe Chunk)
parseChunks l = parseChunk <$> l

run : String -> IO ()
run s = do let l = findCorrupted [] . catMaybes . parseChunks . unpack <$> lines s
           let s = sum $ catMaybes $ (score <$>) <$> l
           putStrLn $ show s

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
-- --------------------------------------------------------------- [ Class.idr ]
-- Module      : UML.Class
-- Description : Class models.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Class

import public UML.Class.Model
import public UML.Class.Parser
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module TTImp.Elab.Delayed

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

import TTImp.Elab.Check
import TTImp.TTImp

import Libraries.Data.IntMap
import Libraries.Data.NameMap
import Data.List

%default covering

-- We run the elaborator in the given environment, but need to end up with a
-- closed term.
mkClosedElab : {vars : _} ->
               FC -> Env Term vars ->
               (Core (Term vars, Glued vars)) ->
               Core ClosedTerm
mkClosedElab fc [] elab
    = do (tm, _) <- elab
         pure tm
mkClosedElab {vars = x :: vars} fc (b :: env) elab
    = mkClosedElab fc env
          (do (sc', _) <- elab
              let b' = newBinder b
              pure (Bind fc x b' sc', gErased fc))
  where
    -- in 'abstractEnvType' we get a Pi binder (so we'll need a Lambda) for
    -- everything except 'Let', so make the appropriate corresponding binder
    -- here
    newBinder : Binder (Term vars) -> Binder (Term vars)
    newBinder b@(Let _ _ _ _) = b
    newBinder b = Lam (binderLoc b) (multiplicity b) Explicit (binderType b)

deeper : {auto e : Ref EST (EState vars)} ->
         Core a -> Core a
deeper elab
    = do est <- get EST
         let d = delayDepth est
         put EST (record { delayDepth = 1 + d } est)
         res <- elab
         est <- get EST
         put EST (record { delayDepth = d } est)
         pure res

-- Try the given elaborator; if it fails, and the error matches the
-- predicate, make a hole and try it again later when more holes might
-- have been resolved
export
delayOnFailure : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 FC -> RigCount -> Env Term vars ->
                 (expected : Maybe (Glued vars)) ->
                 (Error -> Bool) ->
                 (pri : DelayReason) ->
                 (Bool -> Core (Term vars, Glued vars)) ->
                 Core (Term vars, Glued vars)
delayOnFailure fc rig env exp pred pri elab
    = do est <- get EST
         ust <- get UST
         let nos = noSolve ust -- remember the holes we shouldn't solve
         handle (elab False)
          (\err =>
              do est <- get EST
                 expected <- mkExpected exp
                 if pred err
                    then
                      do nm <- genName "delayed"
                         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
                         logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++
                                      " at " ++ show fc ++
                                      " for") env expected
                         log "elab.delay" 10 ("Due to error " ++ show err)
                         ust <- get UST
                         defs <- get Ctxt
                         put UST (record { delayedElab $=
                                 ((pri, ci, localHints defs,
                                   mkClosedElab fc env
                                      (deeper
                                        (do ust <- get UST
                                            let nos' = noSolve ust
                                            put UST (record { noSolve = nos } ust)
                                            res <- elab True
                                            ust <- get UST
                                            put UST (record { noSolve = nos' } ust)
                                            pure res))) :: ) }
                                         ust)
                         pure (dtm, expected)
                    else throw err)
  where
    mkExpected : Maybe (Glued vars) -> Core (Glued vars)
    mkExpected (Just ty) = pure ty
    mkExpected Nothing
        = do nm <- genName "delayTy"
             ty <- metaVar fc erased env nm (TType fc)
             pure (gnf env ty)

export
delayElab : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            FC -> RigCount -> Env Term vars ->
            (expected : Maybe (Glued vars)) ->
            (pri : DelayReason) ->
            Core (Term vars, Glued vars) ->
            Core (Term vars, Glued vars)
delayElab {vars} fc rig env exp pri elab
    = do est <- get EST
         ust <- get UST
         let nos = noSolve ust -- remember the holes we shouldn't solve
         nm <- genName "delayed"
         expected <- mkExpected exp
         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
         logGlueNF "elab.delay" 5 ("Postponing elaborator " ++ show nm ++
                      " for") env expected
         ust <- get UST
         defs <- get Ctxt
         put UST (record { delayedElab $=
                 ((pri, ci, localHints defs, mkClosedElab fc env
                                              (do ust <- get UST
                                                  let nos' = noSolve ust
                                                  put UST (record { noSolve = nos } ust)
                                                  res <- elab
                                                  ust <- get UST
                                                  put UST (record { noSolve = nos' } ust)
                                                  pure res)) :: ) }
                         ust)
         pure (dtm, expected)
  where
    mkExpected : Maybe (Glued vars) -> Core (Glued vars)
    mkExpected (Just ty) = pure ty
    mkExpected Nothing
        = do nm <- genName "delayTy"
             ty <- metaVar fc erased env nm (TType fc)
             pure (gnf env ty)

export
ambiguous : Error -> Bool
ambiguous (AmbiguousElab _ _ _) = True
ambiguous (AmbiguousName _ _) = True
ambiguous (AmbiguityTooDeep _ _ _) = True
ambiguous (InType _ _ err) = ambiguous err
ambiguous (InCon _ _ err) = ambiguous err
ambiguous (InLHS _ _ err) = ambiguous err
ambiguous (InRHS _ _ err) = ambiguous err
ambiguous (WhenUnifying _ _ _ _ _ err) = ambiguous err
ambiguous _ = False

mutual
  mismatchNF : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Defs -> NF vars -> NF vars -> Core Bool
  mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
      = if xn /= yn
           then pure True
           else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
  mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
      = if xt /= yt
           then pure True
           else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
  mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)
  mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y
  mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)
      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
  mismatchNF _ _ _ = pure False

  mismatch : {auto c : Ref Ctxt Defs} ->
             {vars : _} ->
             Defs -> (Closure vars, Closure vars) -> Core Bool
  mismatch defs (x, y)
      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)

contra : {auto c : Ref Ctxt Defs} ->
         {vars : _} ->
         Defs -> NF vars -> NF vars -> Core Bool
-- Unlike 'impossibleOK', any mismatch indicates an unrecoverable error
contra defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
    = if xn /= yn
         then pure True
         else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
contra defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
    = if xt /= yt
         then pure True
         else anyM (mismatch defs) (zipWith (curry $ mapHom snd) xargs yargs)
contra defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)
contra defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
contra defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
contra defs x y = pure False

-- Errors that might be recoverable later if we try again. Generally -
-- ambiguity errors, type inference errors
export
recoverable : {auto c : Ref Ctxt Defs} ->
              Error -> Core Bool
recoverable (CantConvert _ gam env l r)
   = do defs <- get Ctxt
        let defs = record { gamma = gam } defs
        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
recoverable (CantSolveEq _ gam env l r)
   = do defs <- get Ctxt
        let defs = record { gamma = gam } defs
        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
recoverable (UndefinedName _ _) = pure False
recoverable (LinearMisuse _ _ _ _) = pure False
recoverable (InType _ _ err) = recoverable err
recoverable (InCon _ _ err) = recoverable err
recoverable (InLHS _ _ err) = recoverable err
recoverable (InRHS _ _ err) = recoverable err
recoverable (WhenUnifying _ _ _ _ _ err) = recoverable err
recoverable _ = pure True

data RetryError
     = RecoverableErrors
     | AllErrors

Show RetryError where
  show RecoverableErrors = "RecoverableErrors"
  show AllErrors = "AllErrors"

-- Try all the delayed elaborators. If there's a failure, we want to
-- show the ambiguity errors first (since that's the likely cause)
-- Return all the ones that need trying again
retryDelayed' : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                {auto e : Ref EST (EState vars)} ->
                RetryError ->
                (progress : Bool) ->
                List (DelayReason, Int, NameMap (), Core ClosedTerm) ->
                List (DelayReason, Int, NameMap (), Core ClosedTerm) ->
                Core (Bool, List (DelayReason, Int, NameMap (), Core ClosedTerm))
retryDelayed' errmode p acc [] = pure (p, reverse acc)
retryDelayed' errmode p acc (d@(_, i, hints, elab) :: ds)
    = do defs <- get Ctxt
         Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
              | _ => retryDelayed' errmode p acc ds
         handle
           (do est <- get EST
               log "elab.retry" 5 (show (delayDepth est) ++ ": Retrying delayed hole " ++ show !(getFullName (Resolved i)))
               -- elab itself might have delays internally, so keep track of them
               ust <- get UST
               put UST (record { delayedElab = [] } ust)
               defs <- get Ctxt
               put Ctxt (record { localHints = hints } defs)

               tm <- elab
               ust <- get UST
               let ds' = reverse (delayedElab ust) ++ ds

               updateDef (Resolved i) (const (Just
                    (PMDef (MkPMDefInfo NotHole True False)
                           [] (STerm 0 tm) (STerm 0 tm) [])))
               logTerm "elab.update" 5 ("Resolved delayed hole " ++ show i) tm
               logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) [] tm
               removeHole i
               retryDelayed' errmode True acc ds')
           (\err => do log "elab" 5 $ show errmode ++ ":Error in " ++ show !(getFullName (Resolved i))
                                ++ "\n" ++ show err
                       case errmode of
                         RecoverableErrors =>
                            if not !(recoverable err)
                               then throw err
                               else retryDelayed' errmode p (d :: acc) ds
                         AllErrors =>
                            -- we've got an error, but see if we get a more
                            -- helpful one with a later elaborator
                            handle (do ignore $ retryDelayed' errmode p [] ds
                                       throw err)
                               (\err' => throw (better err err')))
  where
    better : Error -> Error -> Error
    better e (GenericMsg _ _) = e
    better (GenericMsg _ _) e = e
    better e _ = e

export
retryDelayed : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               {auto e : Ref EST (EState vars)} ->
               UnifyInfo -> List (DelayReason, Int, NameMap (), Core ClosedTerm) ->
               Core ()
retryDelayed mode ds
    = do est <- get EST
         (p, ds) <- retryDelayed' RecoverableErrors False [] ds -- try everything again
         solveConstraints mode Normal -- maybe we can resolve some interfaces now
         if p
            then retryDelayed mode ds -- progress, go around again
            else ignore $ retryDelayed' AllErrors False [] ds -- fail on all errors

-- Run an elaborator, then all the delayed elaborators arising from it
export
runDelays : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            (DelayReason -> Bool) -> Core a -> Core a
runDelays pri elab
    = do ust <- get UST
         let olddelayed = delayedElab ust
         put UST (record { delayedElab = [] } ust)
         tm <- elab
         ust <- get UST
         log "elab.delay" 2 $ "Rerunning delayed in elaborator"
         handle (do ignore $ retryDelayed' AllErrors False []
                       (reverse (filter hasPri (delayedElab ust))))
                (\err => do put UST (record { delayedElab = olddelayed } ust)
                            throw err)
         ust <- get UST
         put UST (record { delayedElab $= (++ olddelayed) } ust)
         pure tm
  where
    hasPri : (DelayReason, d) -> Bool
    hasPri (n, _) = pri n


text:
module Dbcritic.Check.IndexFkRef

import Control.IOExcept
import Dbcritic.Check
import Dbcritic.Libpq

mkIssue : String -> String -> String -> Issue
mkIssue table fk cols =
    let
        qual        = table ++ "." ++ fk
        identifier  = [ table, fk ]
        description = "The foreign key constraint ‘" ++ qual ++ "’ is missing an index on its referencing side."
        problems    = [ "Updating rows in the referenced table causes a sequential scan on the referencing table."
                      , "Deleting rows from the referenced table causes a sequential scan on the referencing table." ]
        solutions   = [ "Create an index on ‘" ++ table ++ " (" ++ cols ++ ")’." ]
    in
        MkIssue identifier description problems solutions IsNonEmpty IsNonEmpty IsNonEmpty

export
checkIndexFkRef : Check
checkIndexFkRef = MkCheck name help inspect
    where
    name = "index_fk_ref"
    help = "Check that foreign key has an index on its referencing side."

    inspectRow : List (Maybe String) -> IOExcept String Issue
    inspectRow [Just table, Just fk, Just cols] = pure (mkIssue table fk cols)
    inspectRow _ = ioe_fail "checkIndexFkRef: Bad result"

    inspect : PgConnection -> IOExcept String (List Issue)
    inspect conn = do
        res <- pgExecute conn """
            SELECT
                pg_class.relname,
                pg_constraint.conname,
                (
                    SELECT string_agg(pg_attribute.attname, ', ')
                    FROM   pg_attribute
                    WHERE  pg_attribute.attrelid = pg_constraint.conrelid AND
                           ARRAY[pg_attribute.attnum] <@ pg_constraint.conkey
                )
            FROM
                pg_constraint
                JOIN pg_class ON pg_class.oid = pg_constraint.conrelid
            WHERE
                pg_constraint.contype = 'f' AND
                NOT EXISTS (
                    SELECT
                    FROM
                        pg_index
                    WHERE
                        pg_index.indrelid = pg_constraint.conrelid AND
                        ( CAST(pg_index.indkey AS text) || ' ' LIKE
                          array_to_string(pg_constraint.conkey, ' ') || ' %' )
                ) AND
                pg_constraint.connamespace <> regnamespace 'information_schema' AND
                pg_constraint.connamespace <> regnamespace 'pg_catalog'
            ORDER BY
                pg_class.relname,
                pg_constraint.conname
        """
        traverse inspectRow (pgGrid res)

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module BashCompletion

import Data.Config
import Data.List
import Data.String

import Debug.Trace

%default total

allRootCmds : List String
allRootCmds = [
    "assign"
  , "config"
  , "contribute"
  , "graph"
  , "help"
  , "list"
  , "pr"
  , "reflect"
  , "sync"
  ]

-- given a pair of strings, the first representing the word
-- actually being edited, the second representing the word
-- before the one being edited, return a list of possible
-- completions. If the list of completions is empty, bash
-- will perform directory completion.
export
opts : Config => String -> String -> List String
-- first the subcommands available:
opts @{_} "--" "harmony" = allRootCmds
opts @{_} partialCmd "harmony" = filter (isPrefixOf partialCmd) allRootCmds

-- then the config command
opts @{_} "--" "config" = settableProps
opts @{_} partialConfigProp "config" = filter (isPrefixOf partialConfigProp) settableProps

-- then the subcommands that take no arguments
opts @{_} _ "pr"         = []
opts @{_} _ "contribute" = []
opts @{_} _ "sync"       = []
opts @{_} _ "help"       = []
opts @{_} _ "--help"     = []
opts @{_} _ "reflect"    = []

-- then list, which only accepts a single team slug:
opts @{config} "--" "list"   = config.teamSlugs
opts @{config} partialTeamName "list" =
  filter (isPrefixOf partialTeamName) config.teamSlugs

-- finally, everything else (assign, assign --dry) auto-completes with
-- either a team slug or '+' followed by a user login:
opts @{config} "--" _ = config.teamSlugs
opts @{config} partialTeamName _ =
  filter (isPrefixOf partialTeamName) slugsOrLogins
    where
      -- If the word being typed is prefixed with '+' return user logins
      -- but otherwise return team slugs.
      slugsOrLogins : List String
      slugsOrLogins =
        if "+" `isPrefixOf` partialTeamName
          then (strCons '+') <$> config.orgMembers
          else config.teamSlugs

export
script : String
script = """
_harmony()
{
  ED=$([ -z $2 ] && echo "--" || echo $2)
  COMPREPLY=($(harmony --bash-completion $ED $3))
}

complete -F _harmony harmony
"""

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Bad1

data Bad = BadDCon (x : Nat)


text:
-- Tree.idr
--
-- Demonstates generic data types

module Tree

||| A binary tree
public export
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

||| Inserts a new element into a binary search tree
export
insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x (Node left val right) = case compare x val of
                                      LT => Node (insert x left) val right
                                      EQ => Node left val right
                                      GT => Node left val (insert x right)

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
%access public export
Int32 : Type
Int32 = Bits32
Int64 : Type
Int64 = Bits64
Bytes : Type
Bytes = String

max_stars_repo_name: zenhack/idris-protobufs

max_issues_repo_name: zenhack/idris-protobufs

max_forks_repo_name: zenhack/idris-protobufs


text:
module Module'

function' : Int -> Int
function' x = x + 1

main : IO ()
main = printLn . show $ function' 4


text:
module State

import World
import Command

%default total

public export
data State : Type where
  MkState : World.World -> List Command -> State

export
isOver : State -> Bool
isOver (MkState world Nil) = True
isOver (MkState world _) = didWin world

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
module Minecraft.Base.PreClassic.Stone.Block.Export

import public Minecraft.Core.Entity
import public Minecraft.Base.PreClassic.Stone.Block
import public Minecraft.Base.PreClassic.Stone.Item
import public Minecraft.Base.PreClassic.Cobblestone.ItemEntity

%default total

public export
Eq Stone.Block where
  x == y = True

public export
Serialize Stone.Block where
  identifier = "Stone.Block"
  serialize x = JObject [
    ("waterLogged", JBoolean x.base.waterLogged)
  ]

public export
Deserialize Stone.Block where
  deserialize (JObject [
    ("waterLogged", JBoolean waterLogged)
  ]) = Just $ Stone.MkBlock {base = (GenericData.MkBlock {waterLogged = waterLogged})}
  deserialize _ = Nothing

[stoneBlock']
Block Stone.Block where
  id = Item.id {self = Stone.Item}

[breakStone']
Break Stone.Block where
  breakBlk self = [new Cobblestone.ItemEntity Cobblestone.MkItemEntity]

[stoneVtbl']
Vtbl Stone.Block where
  vtable (Block    Stone.Block) = Just stoneBlock
  vtable (Break    Stone.Block) = Just breakStone
  vtable (Tangible Stone.Block) = Just %search
  vtable _ = Nothing

stoneBlock = stoneBlock'
breakStone = breakStone'
stoneVtbl  = stoneVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module StoreL

import Control.App
import Control.App.Console

data Access = LoggedOut | LoggedIn
data Store : Access -> Type where
     MkStore : (secret : String) -> Store a

interface StoreI e where
  connect : (1 prog : (1 d : Store LoggedOut) ->
            App {l} e ()) -> App {l} e ()
  disconnect : (1 d : Store LoggedOut) -> App {l} e ()

Has [Console] e => StoreI e where
  connect f
      = let (>>=) = bindL in
            do putStrLn "Connected"
               f (MkStore "xyzzy")
  disconnect (MkStore _)
      = do putStrLn "Disconnected"
           pure ()

login : (1 s : Store LoggedOut) -> (password : String) ->
        Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
login (MkStore secret) password
    = password == "Mornington Crescent" # MkStore secret

logout : (1 s : Store LoggedIn) -> Store LoggedOut
logout (MkStore secret) = MkStore secret

storeProg : Has [Console, StoreI] e => App e ()
storeProg
    = let (>>=) = bindL in
        do putStr "Password: "
           password <- Console.getStr
           connect $ \s =>
             do let True # s = login s password
                       | False # s => do putStrLn "Incorrect password"
                                         disconnect s
                putStrLn "Door opened"
                let s = logout s
                putStrLn "Door closed"
                disconnect s

foo : IO ()
foo = run storeProg