text:
-- examples in "Type-Driven Development with Idris"
-- chapter 11, section 3, part 2

import Data.Primitives.Views
import System

-- check that all functions are total
%default total

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

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound num with (divides num 12)
      bound ((12 * div) + rem) | (DivBy prf) = rem + 1

data LazyFuel = LDry | LMore (Lazy LazyFuel)

partial
forever : LazyFuel
forever = LMore forever

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

(>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
(>>=) = Do

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand (GetLine) = getLine

run : LazyFuel -> ConsoleIO a -> IO (Maybe a)
run _ (Quit value) = pure $ Just value
run LDry (Do act gen) = pure Nothing
run (LMore fuel) (Do act gen) = do res <- runCommand act
                                   run fuel $ gen res

quiz' : Stream Int -> (score : Nat) -> ConsoleIO Nat
quiz'  (num1 :: num2 :: nums) score
 = do PutStr ("Score so far:" ++ show score ++ "\n")
      PutStr (show num1 ++ " * " ++ show num2 ++ "? ")
      answer <- GetLine
      if toLower answer == "quit" then Quit score else
        if cast answer == num1 * num2
          then do PutStr "Correct!\n"
                  quiz' nums (score + 1)
          else do PutStr ("Wrong, the answer is " ++ show (num1 * num2) ++ "\n")
                  quiz' nums score

partial
main' : IO ()
main' = do seed <- time
           Just score <- run forever (quiz' (arithInputs (fromInteger seed)) 0)
              | Nothing => putStrLn "Ran out of fuel"
           putStrLn $ "Final score: " ++ show score

mutual
  correct : Stream Int -> (score : Nat) -> ConsoleIO Nat
  correct nums score
    = do PutStr "Correct!\n"
         quiz nums (score + 1)

  wrong : Stream Int -> Int -> (score : Nat) -> ConsoleIO Nat
  wrong nums ans score
    = do PutStr $ "Wrong, the answer is " ++ show ans ++ "\n"
         quiz nums score

  quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat
  quiz  (num1 :: num2 :: nums) score
  = do PutStr ("Score so far:" ++ show score ++ "\n")
       PutStr (show num1 ++ " * " ++ show num2 ++ "? ")
       answer <- GetLine
       if toLower answer == "quit" then Quit score else
         if cast answer == num1 * num2
           then correct nums score
           else wrong nums (num1 * num2) score

partial
main : IO ()
main = do seed <- time
          Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)
            | Nothing => putStrLn "Ran out of fuel"
          putStrLn $ "Final score: " ++ show score

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Main

pythag : Int -> List (Int, Int, Int)
pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],
                           x*x + y*y == z*z ]

main : IO ()
main = putStrLn (show (pythag 50))

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Core.Hash

import Core.CaseTree
import Core.TT
import Core.CompileExpr

import Data.List
import Data.List1
import Libraries.Data.List.Lazy
import Data.String
import Libraries.Data.String.Iterator
import Data.Vect

%default covering

-- This is so that we can store a hash of the interface in ttc files, to avoid
-- the need for reloading modules when no interfaces have changed in imports.
-- As you can probably tell, I know almost nothing about writing good hash
-- functions, so better implementations will be very welcome...

public export
interface Hashable a where
  hash : a -> Int
  hashWithSalt : Int -> a -> Int

  hash = hashWithSalt 5381
  hashWithSalt h i = h * 33 + hash i

infixl 5 `hashWithSalt`

export
Hashable Int where
  hash = id

export
Hashable Integer where
  hash = fromInteger

export
Hashable Nat where
  hash = cast

export
Hashable Char where
  hash = cast

export
Hashable a => Hashable (Vect n a) where
  hashWithSalt h [] = abs h
  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs

export
Hashable a => Hashable (List a) where
  hashWithSalt h [] = abs h
  hashWithSalt h (x :: xs) = hashWithSalt (h * 33 + hash x) xs

export
Hashable a => Hashable (List1 a) where
  hashWithSalt h xxs = hashWithSalt (h * 33 + hash (head xxs)) (tail xxs)

export
Hashable a => Hashable (Maybe a) where
  hashWithSalt h Nothing = abs h
  hashWithSalt h (Just x) = hashWithSalt h x

export
Hashable a => Hashable b => Hashable (a, b) where
  hashWithSalt h (x, y) = h `hashWithSalt` x `hashWithSalt` y

export
Hashable String where
  hashWithSalt h = String.Iterator.foldl hashWithSalt h

export
Hashable Double where
  hash = hash . show

export
Hashable Namespace where
  hashWithSalt h ns = hashWithSalt h (unsafeUnfoldNamespace ns)

export
Hashable Name where
  hashWithSalt h (MN s _) = hashWithSalt h s
  hashWithSalt h (DN _ n) = hashWithSalt h n
  hashWithSalt h (NS ns n) = hashWithSalt (hashWithSalt h ns) n
  hashWithSalt h (Resolved i) = hashWithSalt h i
  hashWithSalt h n = hashWithSalt h (show n)

export
Hashable RigCount where
  hashWithSalt h = elimSemi
                     (hashWithSalt h 0)
                     (hashWithSalt h 1)
                     (const $ hashWithSalt h 2)

export
Hashable t => Hashable (PiInfo t) where
  hashWithSalt h Implicit = hashWithSalt h 0
  hashWithSalt h Explicit = hashWithSalt h 1
  hashWithSalt h AutoImplicit = hashWithSalt h 2
  hashWithSalt h (DefImplicit t) = h `hashWithSalt` 3 `hashWithSalt` t

export
Hashable ty => Hashable (Binder ty) where
  hashWithSalt h (Lam _ c p ty)
      = h `hashWithSalt` 0 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (Let _ c val ty)
      = h `hashWithSalt` 1 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
  hashWithSalt h (Pi _ c p ty)
      = h `hashWithSalt` 2 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (PVar _ c p ty)
      = h `hashWithSalt` 3 `hashWithSalt` c `hashWithSalt` p `hashWithSalt` ty
  hashWithSalt h (PLet _ c val ty)
      = h `hashWithSalt` 4 `hashWithSalt` c `hashWithSalt` val `hashWithSalt` ty
  hashWithSalt h (PVTy _ c ty)
      = h `hashWithSalt` 5 `hashWithSalt` c `hashWithSalt` ty

Hashable (Var vars) where
  hashWithSalt h (MkVar {i} _) = hashWithSalt h i

mutual
  export
  Hashable (Term vars) where
    hashWithSalt h (Local fc x idx y)
        = h `hashWithSalt` 0 `hashWithSalt` idx
    hashWithSalt h (Ref fc x name)
        = h `hashWithSalt` 1 `hashWithSalt` name
    hashWithSalt h (Meta fc x y xs)
        = h `hashWithSalt` 2 `hashWithSalt` y `hashWithSalt` xs
    hashWithSalt h (Bind fc x b scope)
        = h `hashWithSalt` 3 `hashWithSalt` b `hashWithSalt` scope
    hashWithSalt h (App fc fn arg)
        = h `hashWithSalt` 4 `hashWithSalt` fn `hashWithSalt` arg
    hashWithSalt h (As fc _ nm pat)
        = h `hashWithSalt` 5 `hashWithSalt` nm `hashWithSalt` pat
    hashWithSalt h (TDelayed fc x y)
        = h `hashWithSalt` 6 `hashWithSalt` y
    hashWithSalt h (TDelay fc x t y)
        = h `hashWithSalt` 7 `hashWithSalt` t `hashWithSalt` y
    hashWithSalt h (TForce fc r x)
        = h `hashWithSalt` 8 `hashWithSalt` x
    hashWithSalt h (PrimVal fc c)
        = h `hashWithSalt` 9 `hashWithSalt` (show c)
    hashWithSalt h (Erased fc _)
        = hashWithSalt h 10
    hashWithSalt h (TType fc)
        = hashWithSalt h 11

  export
  Hashable Pat where
    hashWithSalt h (PAs fc nm pat)
        = h `hashWithSalt` 0 `hashWithSalt` nm `hashWithSalt` pat
    hashWithSalt h (PCon fc x tag arity xs)
        = h `hashWithSalt` 1 `hashWithSalt` x `hashWithSalt` xs
    hashWithSalt h (PTyCon fc x arity xs)
        = h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` xs
    hashWithSalt h (PConst fc c)
        = h `hashWithSalt` 3 `hashWithSalt` (show c)
    hashWithSalt h (PArrow fc x s t)
        = h `hashWithSalt` 4 `hashWithSalt` s `hashWithSalt` t
    hashWithSalt h (PDelay fc r t p)
        = h `hashWithSalt` 5 `hashWithSalt` t `hashWithSalt` p
    hashWithSalt h (PLoc fc x)
        = h `hashWithSalt` 6 `hashWithSalt` x
    hashWithSalt h (PUnmatchable fc x)
        = h `hashWithSalt` 7 `hashWithSalt` x

  export
  Hashable (CaseTree vars) where
    hashWithSalt h (Case idx x scTy xs)
        = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs
    hashWithSalt h (STerm _ x)
        = h `hashWithSalt` 1 `hashWithSalt` x
    hashWithSalt h (Unmatched msg)
        = h `hashWithSalt` 2
    hashWithSalt h Impossible
        = h `hashWithSalt` 3

  export
  Hashable (CaseAlt vars) where
    hashWithSalt h (ConCase x tag args y)
        = h `hashWithSalt` 0 `hashWithSalt` x `hashWithSalt` args
            `hashWithSalt` y
    hashWithSalt h (DelayCase t x y)
        = h `hashWithSalt` 2 `hashWithSalt` (show t)
            `hashWithSalt` (show x) `hashWithSalt` y
    hashWithSalt h (ConstCase x y)
        = h `hashWithSalt` 3 `hashWithSalt` (show x) `hashWithSalt` y
    hashWithSalt h (DefaultCase x)
        = h `hashWithSalt` 4 `hashWithSalt` x

export
Hashable CFType where
  hashWithSalt h = \case
    CFUnit =>
      h `hashWithSalt` 0
    CFInt =>
      h `hashWithSalt` 1
    CFUnsigned8 =>
      h `hashWithSalt` 2
    CFUnsigned16 =>
      h `hashWithSalt` 3
    CFUnsigned32 =>
      h `hashWithSalt` 4
    CFUnsigned64 =>
      h `hashWithSalt` 5
    CFString =>
      h `hashWithSalt` 6
    CFDouble =>
      h `hashWithSalt` 7
    CFChar =>
      h `hashWithSalt` 8
    CFPtr =>
      h `hashWithSalt` 9
    CFGCPtr =>
      h `hashWithSalt` 10
    CFBuffer =>
      h `hashWithSalt` 11
    CFWorld =>
      h `hashWithSalt` 12
    CFFun a b =>
      h `hashWithSalt` 13 `hashWithSalt` a `hashWithSalt` b
    CFIORes a =>
      h `hashWithSalt` 14 `hashWithSalt` a
    CFStruct n fs =>
      h `hashWithSalt` 15 `hashWithSalt` n `hashWithSalt` fs
    CFUser n xs =>
      h `hashWithSalt` 16 `hashWithSalt` n `hashWithSalt` xs
    CFInt8 =>
      h `hashWithSalt` 17
    CFInt16 =>
      h `hashWithSalt` 18
    CFInt32 =>
      h `hashWithSalt` 19
    CFInt64 =>
      h `hashWithSalt` 20
    CFForeignObj =>
      h `hashWithSalt` 21
    CFInteger =>
      h `hashWithSalt` 22

export
Hashable Constant where
  hashWithSalt h = \case
    I i =>
      h `hashWithSalt` 0 `hashWithSalt` i
    BI x =>
      h `hashWithSalt` 1 `hashWithSalt` x
    B8 x =>
      h `hashWithSalt` 2 `hashWithSalt` x
    B16 x =>
      h `hashWithSalt` 3 `hashWithSalt` x
    B32 x =>
      h `hashWithSalt` 4 `hashWithSalt` x
    B64 x =>
      h `hashWithSalt` 5 `hashWithSalt` x
    Str x =>
      h `hashWithSalt` 6 `hashWithSalt` x
    Ch x =>
      h `hashWithSalt` 7 `hashWithSalt` x
    Db x =>
      h `hashWithSalt` 8 `hashWithSalt` x

    WorldVal =>
      h `hashWithSalt` 9

    IntType =>
      h `hashWithSalt` 10
    IntegerType =>
      h `hashWithSalt` 11
    Bits8Type =>
      h `hashWithSalt` 12
    Bits16Type =>
      h `hashWithSalt` 13
    Bits32Type =>
      h `hashWithSalt` 14
    Bits64Type =>
      h `hashWithSalt` 15
    StringType =>
      h `hashWithSalt` 16
    CharType =>
      h `hashWithSalt` 17
    DoubleType =>
      h `hashWithSalt` 18
    WorldType =>
      h `hashWithSalt` 19

    I8 x => h `hashWithSalt` 20 `hashWithSalt` x
    I16 x => h `hashWithSalt` 21 `hashWithSalt` x
    I32 x => h `hashWithSalt` 22 `hashWithSalt` x
    I64 x => h `hashWithSalt` 23 `hashWithSalt` x

    Int8Type => h `hashWithSalt` 24
    Int16Type => h `hashWithSalt` 25
    Int32Type => h `hashWithSalt` 26
    Int64Type => h `hashWithSalt` 27

export
Hashable LazyReason where
  hashWithSalt h = \case
    LInf => h `hashWithSalt` 0
    LLazy => h `hashWithSalt` 1
    LUnknown => h `hashWithSalt` 2

export
Hashable (PrimFn arity) where
  hashWithSalt h = \case
    Add ty =>
      h `hashWithSalt` 0 `hashWithSalt` ty
    Sub ty =>
      h `hashWithSalt` 1 `hashWithSalt` ty
    Mul ty =>
      h `hashWithSalt` 2 `hashWithSalt` ty
    Div ty =>
      h `hashWithSalt` 3 `hashWithSalt` ty
    Mod ty =>
      h `hashWithSalt` 4 `hashWithSalt` ty
    Neg ty =>
      h `hashWithSalt` 5 `hashWithSalt` ty
    ShiftL ty =>
      h `hashWithSalt` 6 `hashWithSalt` ty
    ShiftR ty =>
      h `hashWithSalt` 7 `hashWithSalt` ty

    BAnd ty =>
      h `hashWithSalt` 8 `hashWithSalt` ty
    BOr ty =>
      h `hashWithSalt` 9 `hashWithSalt` ty
    BXOr ty =>
      h `hashWithSalt` 10 `hashWithSalt` ty

    LT ty =>
      h `hashWithSalt` 11 `hashWithSalt` ty
    LTE ty =>
      h `hashWithSalt` 12 `hashWithSalt` ty
    EQ ty =>
      h `hashWithSalt` 13 `hashWithSalt` ty
    GTE ty =>
      h `hashWithSalt` 14 `hashWithSalt` ty
    GT ty =>
      h `hashWithSalt` 15 `hashWithSalt` ty

    StrLength =>
      h `hashWithSalt` 16
    StrHead =>
      h `hashWithSalt` 17
    StrTail =>
      h `hashWithSalt` 18
    StrIndex =>
      h `hashWithSalt` 19
    StrCons =>
      h `hashWithSalt` 20
    StrAppend =>
      h `hashWithSalt` 21
    StrReverse =>
      h `hashWithSalt` 22
    StrSubstr =>
      h `hashWithSalt` 23

    DoubleExp =>
      h `hashWithSalt` 24
    DoubleLog =>
      h `hashWithSalt` 25
    DoubleSin =>
      h `hashWithSalt` 26
    DoubleCos =>
      h `hashWithSalt` 27
    DoubleTan =>
      h `hashWithSalt` 28
    DoubleASin =>
      h `hashWithSalt` 29
    DoubleACos =>
      h `hashWithSalt` 30
    DoubleATan =>
      h `hashWithSalt` 31
    DoubleSqrt =>
      h `hashWithSalt` 32
    DoubleFloor =>
      h `hashWithSalt` 33
    DoubleCeiling =>
      h `hashWithSalt` 34

    Cast f t =>
      h `hashWithSalt` 35 `hashWithSalt` f `hashWithSalt` t
    BelieveMe =>
      h `hashWithSalt` 36
    Crash =>
      h `hashWithSalt` 37

    DoublePow =>
      h `hashWithSalt` 38

export
Hashable ConInfo where
  hashWithSalt h = \case
    DATACON => h `hashWithSalt` 0
    TYCON => h `hashWithSalt` 1
    NIL => h `hashWithSalt` 2
    CONS => h `hashWithSalt` 3
    ENUM => h `hashWithSalt` 4
    NOTHING => h `hashWithSalt` 5
    JUST => h `hashWithSalt` 6
    RECORD => h `hashWithSalt` 7
    ZERO => h `hashWithSalt` 8
    SUCC => h `hashWithSalt` 9

mutual
  export
  Hashable NamedCExp where
    hashWithSalt h = \case
      NmLocal fc n =>
        h `hashWithSalt` 0 `hashWithSalt` n
      NmRef fc n =>
        h `hashWithSalt` 1 `hashWithSalt` n
      NmLam fc x rhs =>
        h `hashWithSalt` 2 `hashWithSalt` x `hashWithSalt` rhs
      NmLet fc x val rhs =>
        h `hashWithSalt` 3 `hashWithSalt` x `hashWithSalt` val `hashWithSalt` rhs
      NmApp fc f xs =>
        h `hashWithSalt` 4 `hashWithSalt` f `hashWithSalt` xs
      NmCon fc cn ci t args =>
        h `hashWithSalt` 5 `hashWithSalt` cn `hashWithSalt` ci `hashWithSalt` t `hashWithSalt` args
      NmOp fc fn args =>
        h `hashWithSalt` 6 `hashWithSalt` fn `hashWithSalt` args
      NmExtPrim fc p args =>
        h `hashWithSalt` 7 `hashWithSalt` p `hashWithSalt` args
      NmForce fc r x =>
        h `hashWithSalt` 8 `hashWithSalt` r `hashWithSalt` x
      NmDelay fc r x =>
        h `hashWithSalt` 9 `hashWithSalt` r `hashWithSalt` x
      NmConCase fc sc alts df =>
        h `hashWithSalt` 10 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
      NmConstCase fc sc alts df =>
        h `hashWithSalt` 11 `hashWithSalt` sc `hashWithSalt` alts `hashWithSalt` df
      NmPrimVal fc c =>
        h `hashWithSalt` 12 `hashWithSalt` c
      NmErased fc =>
        h `hashWithSalt` 13
      NmCrash fc msg =>
        h `hashWithSalt` 14 `hashWithSalt` msg

  export
  Hashable NamedConAlt where
    hashWithSalt h (MkNConAlt n ci tag args rhs) =
      h `hashWithSalt` n `hashWithSalt` ci `hashWithSalt` tag `hashWithSalt` args `hashWithSalt` rhs

  export
  Hashable NamedConstAlt where
    hashWithSalt h (MkNConstAlt c rhs) =
      h `hashWithSalt` c `hashWithSalt` rhs

export
Hashable NamedDef where
  hashWithSalt h = \case
    MkNmFun args ce =>
      h `hashWithSalt` 0 `hashWithSalt` args `hashWithSalt` ce
    MkNmCon tag arity nt =>
      h `hashWithSalt` 1 `hashWithSalt` tag `hashWithSalt` arity `hashWithSalt` nt
    MkNmForeign ccs fargs cft =>
      h `hashWithSalt` 2 `hashWithSalt` ccs `hashWithSalt` fargs `hashWithSalt` cft
    MkNmError e =>
      h `hashWithSalt` 3 `hashWithSalt` e


text:
module Hello

%default total

main : IO ()
main = putStrLn "Hello, world!"

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
||| Module    : Action.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
||| In some cases `Maybe` is not sufficient to describe the results of
||| operations. Here we describe a more Generic result data type.
module Commons.Data.Action

%access public export

||| Operations either return a success or some result, we use
||| `ActionTy` to differentiate between the two.
data ActionTy = SUCCESS | RESULT

||| A custom return type for operations.
|||
||| @aty What type of action are we performing.
||| @rty The return type for an action that returns a value.
||| @ety The error type for an action.
|||
data Action : (aty : ActionTy)
           -> (ety : Type)
           -> (rty : Type)
           -> Type
  where
    ||| The operation completed successfully and doesn't return a
    ||| result.
    Success : Action SUCCESS ety rty

    ||| The operation returns a result of type `rty`.
    |||
    ||| @rty The value returned.
    Result : rty -> Action RESULT ety rty

    ||| The operation failed and the given error was produced.
    |||
    ||| @ety The reported error.
    Error : ety -> Action aty ety rty

||| Given an `action` if it was successful return `success` otherwise return `backup`.
success : (backup  : Lazy b)
       -> (success : Lazy b)
       -> (action  : Action SUCCESS ety rty)
       -> b
success _      success Success   = success
success backup _       (Error x) = backup

||| Given an `action` if it was successful apply `transform` otherwise return `backup`.
result : (backup     : Lazy b)
      -> (transform  : Lazy (rty -> b))
      -> (result : Action RESULT ety rty)
      -> b
result _      transform (Result x) = transform x
result backup _         (Error x)  = backup

runEitherIO : IO (Either ety rty) -> IO $ Action RESULT ety rty
runEitherIO func =
  case !func of
    Left err  => pure $ Error  err
    Right res => pure $ Result res

(Show rty, Show ety) => Show (Action ty ety rty) where
  show Success    = "Success"
  show (Result x) = unwords ["Result", show x]
  show (Error  x) = unwords ["Error", show x]

(Eq rty, Eq ety) => Eq (Action aty ety rty) where
  (==) Success    Success    = True
  (==) (Result x) (Result y) = x == y
  (==) (Error x)  (Error y)  = x == y
  (==) _          _          = False

export
Functor (Action aty ety) where
    map f (Error l)  = Error l
    map f Success    = Success
    map f (Result r) = Result (f r)

export
Applicative (Action RESULT ety) where
  pure = Result

  (<*>) (Result f)  (Result x)  = Result (f x)
  (<*>) (Result _)  (Error err) = Error err
  (<*>) (Error err) _           = Error err

combine : Action SUCCESS eTy ()
       -> Action SUCCESS eTy ()
       -> Action SUCCESS eTy ()
combine Success     Success     = Success
combine Success     (Error err) = Error err
combine (Error err) _           = Error err

export
Monad (Action RESULT ety) where
  (>>=) (Result x) f = f x
  (>>=) (Error x)  f = Error x

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Crypto.Hash.MerkleDamgard

import Crypto.Hash.Interfaces
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.List
import Data.Nat
import Data.Nat.Factor
import Data.Vect
import Utils.Misc
import Utils.Bytes
import Data.Stream

public export
record MerkleDamgard (internal_state_nbyte : Nat) (0 block_nbyte : Nat) (0 word_type : Type) where
  constructor MkMerkleDamgard
  hash_values : Vect internal_state_nbyte word_type
  buffer_nbyte : Nat
  buffer_nbyte_constraint : LT buffer_nbyte block_nbyte
  buffer : Vect buffer_nbyte Bits8
  npassed_blocks : Nat

export
mk_merkle_damgard : (init_hash_values : Vect internal_state_nbyte word_type) ->
                    {auto 0 prf : LTE 1 block_nbyte} ->
                    MerkleDamgard internal_state_nbyte block_nbyte word_type
mk_merkle_damgard x {prf = LTESucc prf'} = MkMerkleDamgard x 0 (LTESucc LTEZero) [] 0

public export
pad_lemma : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : Nat}
  -> LTE 1 block_nbyte
  -> (residue_max_nbyte + 1 + length_nbyte = block_nbyte)
  -> LTE residue_nbyte residue_max_nbyte
  -> (plus residue_nbyte (S (plus (minus residue_max_nbyte residue_nbyte) length_nbyte))) = block_nbyte
pad_lemma remilia flandre sakuya =
  rewrite sym flandre in
  rewrite sym $ plusSuccRightSucc residue_nbyte (plus (minus residue_max_nbyte residue_nbyte) length_nbyte) in
  rewrite plusAssociative residue_nbyte (minus residue_max_nbyte residue_nbyte) length_nbyte in
  rewrite plusCommutative residue_nbyte (minus residue_max_nbyte residue_nbyte) in
  rewrite plusMinusLte residue_nbyte residue_max_nbyte sakuya in
  rewrite plusCommutative residue_max_nbyte 1 in
    Refl

public export
pad_over_lemma : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : Nat}
  -> (residue_max_nbyte + 1 + length_nbyte = block_nbyte)
  -> LT residue_nbyte block_nbyte
  -> plus residue_nbyte (S (plus (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte)) = (plus block_nbyte (plus block_nbyte 0))
pad_over_lemma flandre cirno =
  rewrite sym $ plusSuccRightSucc residue_nbyte (plus (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte) in
  rewrite plusAssociative residue_nbyte (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte in
  rewrite plusAssociative residue_nbyte (minus block_nbyte residue_nbyte) residue_max_nbyte in
  rewrite plusCommutative residue_nbyte (minus block_nbyte residue_nbyte) in
  rewrite plusMinusLte residue_nbyte block_nbyte (lteSuccLeft cirno) in
  rewrite sym $ plusAssociative block_nbyte residue_max_nbyte length_nbyte in
  rewrite plusSuccRightSucc block_nbyte (plus residue_max_nbyte length_nbyte) in
  rewrite plusZeroRightNeutral block_nbyte in
  rewrite flandre' in
    Refl
  where
  flandre' : S (plus residue_max_nbyte length_nbyte) = block_nbyte
  flandre' = rewrite sym flandre in rewrite plusCommutative residue_max_nbyte 1 in Refl

public export
pad_residue : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
  -> (0 _ : LTE 1 block_nbyte)
  -> (0 _ : (residue_max_nbyte + 1 + length_nbyte = block_nbyte))
  -> (0 _ : LTE residue_nbyte residue_max_nbyte)
  -> Vect residue_nbyte Bits8
  -> Vect length_nbyte Bits8
  -> Vect block_nbyte Bits8
pad_residue remilia flandre sakuya residue b_length =
   replace_vect (pad_lemma remilia flandre sakuya) $
     residue
     ++ [0b10000000]
     ++ replicate (minus residue_max_nbyte residue_nbyte) 0
     ++ b_length

public export
pad_over_residue : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
  -> (0 _ : LTE 1 block_nbyte)
  -> (0 _ : residue_max_nbyte + 1 + length_nbyte = block_nbyte)
  -> (0 _ : LT residue_max_nbyte residue_nbyte)
  -> (0 _ : LT residue_nbyte block_nbyte)
  -> Vect residue_nbyte Bits8
  -> Vect length_nbyte Bits8
  -> Vect (2 * block_nbyte) Bits8
pad_over_residue remilia flandre rumia cirno residue b_length =
  replace_vect (pad_over_lemma flandre cirno) $
    residue
    ++ [0b10000000]
    ++ replicate (minus block_nbyte residue_nbyte + residue_max_nbyte) 0
    ++ b_length

public export
pad_theorem : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
  -> (0 _ : LTE 1 block_nbyte)
  -> (0 _ : residue_max_nbyte + 1 + length_nbyte = block_nbyte)
  -> (0 _ : LT residue_nbyte block_nbyte)
  -> Vect residue_nbyte Bits8
  -> Vect length_nbyte Bits8
  -> Either (Vect block_nbyte Bits8) (Vect (block_nbyte + block_nbyte) Bits8)
pad_theorem remilia flandre cirno input b_length =
  case isLTE residue_nbyte residue_max_nbyte of
    Yes sakuya => Left $ pad_residue remilia flandre sakuya input b_length
    No rumia => Right $ replace_vect (cong (plus block_nbyte) (plusZeroRightNeutral block_nbyte)) $ pad_over_residue remilia flandre (notLTEImpliesGT rumia) cirno input b_length


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

-- Proves that k and j are the same
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k) -- proving k is the same as itself

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat 0 0 = Just (Same 0)
checkEqNat 0 (S k) = Nothing
checkEqNat (S k) 0 = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)


text:
module IdrisScript.Timer

import IdrisScript

%access public export

export
record Timeout where
  constructor MkTimeout
  unTimeout : Ptr

export
record Interval where
  constructor MkInterval
  unInterval : Ptr

||| Executes a JS_IO action after `millis` milliseconds.
setTimeout : (() -> JS_IO ()) -> (millis : Int) -> JS_IO Timeout
setTimeout f millis = do
  timeout <- jscall "setTimeout(%0, %1)"
                    (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                    (MkJsFn f) millis
  pure $ MkTimeout timeout

||| Clears a timeout.
export
clearTimeout : Timeout -> JS_IO ()
clearTimeout timeout =
  jscall "clearTimeout(%0)" (Ptr -> JS_IO ()) (unTimeout timeout)

||| Periodically executes a JS_IO action after `millis` milliseconds.
setInterval : (() -> JS_IO ()) -> Int -> JS_IO Interval
setInterval f millis = do
  interval <- jscall "setInterval(%0, %1)"
                     (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                     (MkJsFn f) millis
  pure $ MkInterval interval

||| Clears an interval.
export
clearInterval : Interval -> JS_IO ()
clearInterval interval =
  jscall "clearInterval(%0)" (Ptr -> JS_IO ()) (unInterval interval)

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
data Natty : Nat -> Type where
  Z : Natty Z
  S : Natty n -> Natty (S n)

view : (n: Nat) -> Natty n
view Z = Z
view (S n) = S (view n)

id : Nat -> Nat
id n with (view n)
  id _ | Z = Z
  id _ | S n = id _ | n


text:
module Test.Blockchain

import Test.Asserts
import Data.Hash
import Blockchain

%access export

||| Simple tests use Nat type
Hashable Nat where
   saltedHash64 n = saltedHash64 (toIntegerNat n)

||| Simplified test blocks containing integers that can be only placed consecutively
||| on the blockchain `n :: (n - 1) :: ... :: 1 :: 0 :: Genesis`
record TestNatPayload where
       constructor MkTestNatPayload
       payload : Nat

Show TestNatPayload where
   show = show . payload

Cast TestNatPayload Nat where
   cast = payload

||| assumes i can only be linked to (i - 1)
hashPrevNat : Nat -> BlockHash
hashPrevNat Z = GenesisHash
hashPrevNat (S i) = hash . show $ i

||| ignoring serialization
BlockData TestNatPayload where
   serialize = show
   prevHash = hashPrevNat . payload

||| Note this is very tightly typed requiring consecutive numbers so stuff like this
||| ```idris example
|||  natChain1 : HBlockchain [TestNatPayload, TestNatPayload, ()] (blockHash (MkTestNatPayload 1))
|||  natChain1 = exampleMiner (MkTestNatPayload 1) (exampleMiner (MkTestNatPayload 1) (Single Genesis))
||| ```
|||will not compile
natChain : HBlockchain [TestNatPayload, TestNatPayload] (blockHash (MkTestNatPayload 1))
natChain = exampleMiner (MkTestNatPayload 1) (exampleMiner (MkTestNatPayload 0) (Single Block.Genesis))

testNatHashes : IO ()
testNatHashes =
      assertEq ((take 2) . computeHashes $ natChain) (map (hash . show) $ [1,0])

testNatPayloads : IO ()
testNatPayloads =
    assertEq (the (List Nat) (asList $ natChain)) [1,0]

||| Again note this is very tightly typed, for example this will not compile
||| ```idris example
|||  natSimpleChain = (MkTestNatPayload 1) :: (MkTestNatPayload 1) :: SimpleBlockchain.Genesis
||| ```
natSimpleChain : SimpleBlockchain TestNatPayload (blockHash (MkTestNatPayload 1))
natSimpleChain = (MkTestNatPayload 1) :: (MkTestNatPayload 0) :: SimpleBlockchain.Genesis

extractSimpleHash : SimpleBlockchain a hash -> BlockHash
extractSimpleHash {hash} block = hash

testNatSimpleHash : IO ()
testNatSimpleHash =
   assertEq (extractSimpleHash natSimpleChain) (hash . show $ 1)

||| Simplified test msg block
record MsgPayload where
       constructor MkMsgPayload
       prevMsgHash : BlockHash
       msg : String

Show MsgPayload where
   show block = (show . prevMsgHash $ block) ++ ":" ++ (msg block)

BlockData MsgPayload where
   serialize = show
   prevHash = prevMsgHash

||| Attempting to compile the following never returns with Idris 1.2:
||| ```idris example
|||  msgChain : SimpleBlockchain MsgPayload (strHash "16FC397CF62F64D3:Hello")
|||  msgChain = (MkMsgPayload GenesisHash "Hello") :: SimpleBlockchain.Genesis
||| ```
||| I do not expect to have much use of hardcoded values of hash type variable
||| this works
msgSimpleChain1 : (h ** SimpleBlockchain MsgPayload h)
msgSimpleChain1 = (_ ** (MkMsgPayload GenesisHash "Hello") :: SimpleBlockchain.Genesis)

testMsgSimpleChain1Hash : IO()
testMsgSimpleChain1Hash =
   case msgSimpleChain1 of
        (h ** _) => assertEq h (strHash $ (show GenesisHash) ++ ":Hello")

mixedChain : (h ** HBlockchain [MsgPayload, TestNatPayload] h)
mixedChain = (_ ** exampleMiner (MkMsgPayload (strHash "0") "Hello") (exampleMiner (MkTestNatPayload 0) (Single Block.Genesis)))

testMixedChainHash : IO()
testMixedChainHash =
   case mixedChain of
        (h ** _) => assertEq h (strHash (show (strHash "0") ++ ":Hello"))

max_stars_repo_name: rpeszek/idris-chain

max_issues_repo_name: rpeszek/idris-chain

max_forks_repo_name: rpeszek/idris-chain


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

import WebAssembly.Structure

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

public export
data ValidLimits : Limits -> Nat -> Type where
  ||| Proof that a limit wihtout an upper bound is valid for some given k
  |||
  |||    n <= k
  |||----------------
  ||| ⊢ {min n} : k
  |||
  MkValidLowerBound : (mm = Nothing) -> LTE n k -> ValidLimits (MkLimits n mm) k
  ||| Proof that a limit with lower and upper bound is valid for some given k
  |||
  |||   (n <= k)   (m <= k)   (n <= m)
  |||------------------------------------
  |||        ⊢ {min n, max m} : k
  |||
  MkValidLimits     : (mm = Just m)  -> LTE n k -> LTE m k -> LTE n m -> ValidLimits (MkLimits n mm) k

-------------------------------------------------------------------------------
-- Lemmas about limit-type validation
-------------------------------------------------------------------------------

||| If the lower bound of a limit without an upper bound is larger than k, then we the limit is invalid
total lower_bound_invalid_upper_bound_absent : (LTE n k -> Void) -> (ValidLimits (MkLimits n Nothing) k -> Void)
lower_bound_invalid_upper_bound_absent not_n_lte_k (MkValidLowerBound _ n_lte_k) = not_n_lte_k n_lte_k
lower_bound_invalid_upper_bound_absent not_n_lte_k (MkValidLimits _ n_lte_k _ _) = not_n_lte_k n_lte_k

||| If the lower bound of a limit with lower and upper bounds is larger than k, then we the limit is invalid
total lower_bound_invalid_upper_bound_present : (LTE n k -> Void) -> (ValidLimits (MkLimits n (Just m)) k -> Void)
lower_bound_invalid_upper_bound_present _ (MkValidLowerBound Refl _) impossible
lower_bound_invalid_upper_bound_present not_n_lte_k (MkValidLimits Refl n_lte_k _ _) = not_n_lte_k n_lte_k

||| If the upper bound of a limit is larger than k, then the limit is invalid
total upper_bound_invalid : (LTE m k -> Void) -> (ValidLimits (MkLimits n (Just m)) k -> Void)
upper_bound_invalid _ (MkValidLowerBound Refl _) impossible
upper_bound_invalid not_m_lte_k (MkValidLimits Refl _ m_lte_k _) = not_m_lte_k m_lte_k

||| If the lower bound is greater than the upper bound, then the limit is invalid
total lower_bound_greater_than_upper_bound : (LTE n m -> Void) -> (ValidLimits (MkLimits n (Just m)) k -> Void)
lower_bound_greater_than_upper_bound _ (MkValidLowerBound Refl _) impossible
lower_bound_greater_than_upper_bound not_n_lte_m (MkValidLimits Refl _ _ n_lte_m) = not_n_lte_m n_lte_m

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

||| Decide whether a given limit is valid for some given k
total public export
isLimitsValid : (limits : Limits) -> (k : Nat) -> Dec (ValidLimits limits k)
isLimitsValid (MkLimits n Nothing) k =
  case isLTE n k of
    No  contra => No (lower_bound_invalid_upper_bound_absent contra)
    Yes prof   => Yes (MkValidLowerBound Refl prof)
isLimitsValid (MkLimits n (Just m)) k =
  case isLTE n k of
    No  contra => No (lower_bound_invalid_upper_bound_present contra)
    Yes n_lte_k   => case isLTE m k of
      No contra => No (upper_bound_invalid contra)
      Yes m_lte_k  => case isLTE n m of
        No contra => No (lower_bound_greater_than_upper_bound contra)
        Yes n_lte_m  => Yes (MkValidLimits Refl n_lte_k m_lte_k n_lte_m)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Data.Prim.Int8

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Int8) -> Type where
  LT : {0 m,n : Int8} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Int8) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Int8) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Int8) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Int8) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Int8) -> Trichotomy (<) m n
comp m n = case prim__lt_Int8 m n of
  0 => case prim__eq_Int8 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Int8 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Int8`
public export
MinInt8 : Int8
MinInt8 = -0x80

||| Upper bound of `Int8`
public export
MaxInt8 : Int8
MaxInt8 = 0x7f

||| `m >= MinInt8` for all `m` of type `Int8`.
export
0 GTE_MinInt8 : (m : Int8) -> m >= MinInt8
GTE_MinInt8 m = case comp MinInt8 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int8 smaller than \{show MinInt8}"

||| Not value of type `Int8` is less than zero.
export
0 Not_LT_MinInt8 : m < MinInt8 -> Void
Not_LT_MinInt8 = GTE_not_LT (GTE_MinInt8 m)

||| `m <= MaxInt8` for all `m` of type `Int8`.
export
0 LTE_MaxInt8 : (m : Int8) -> m <= MaxInt8
LTE_MaxInt8 m = case comp m MaxInt8 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Int8 greater than \{show MaxInt8}"

||| Not value of type `Int8` is greater than `MaxInt8`.
export
0 Not_GT_MaxInt8 : m > MaxInt8 -> Void
Not_GT_MaxInt8 = LTE_not_GT (LTE_MaxInt8 m)

||| Every value of type `Int8` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Int8) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Int8 (<) where
  wellFounded = accessLT

||| Every value of type `Int8` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Int8) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Int8 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
export %inline
sdiv : (n,d : Int8) -> (0 prf : d /= 0) => Int8
sdiv n d = n `div` d

||| Safe modulo.
export %inline
smod : (n,d : Int8) -> (0 prf : d /= 0) => Int8
smod n d = n `mod` d


text:
module GenFunctor

import MonadFunctor

import Control.Monad.Reader
import Control.Monad.Trans

interface GenFunctor n (0 m : Type -> Type) | m where
  gmap : (n a -> n b) -> m a -> m b

Functor m => GenFunctor Prelude.id m where
  gmap = map

f : List Nat -> List Int
f = gmap cast

MonadFunctor t => Monad m => GenFunctor m (t m) where
  gmap = liftMap

[Trans] MonadReader r m => MonadTrans t => GenFunctor m (t m) => Monad (t m) => MonadReader r (t m) where
  ask   = lift ask
  local = gmap . local

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
data Shape : Type where
  ||| Triangle; Base & Height
  Triangle : Double -> Double -> Shape
  ||| Rectangle; Width & Height
  Rectangle : Double -> Double -> Shape
  ||| Circle; Radius
  Circle : Double -> Shape
%name Shape shape, shape1, shape2

data Picture = Primitive Shape
             | Combine Picture Picture
             | Roatate Double Picture
             | Translate Double Double Picture
%name Picture pic, pic1, pic2

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

myTriangle : Picture
myTriangle = Primitive (Triangle 10 10)

myRect : Picture
myRect = Primitive (Rectangle 20 10)

myCircle : Picture
myCircle = Primitive (Circle 5)

testPic : Picture
testPic = Combine (Translate 5 5 myRect) (Combine (Translate 35 5 myCircle) (Translate 15 25 myTriangle))

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


text:
toBit : Num i => Char -> Maybe i
toBit '0' = Just 0
toBit '1' = Just 1
toBit _ = Nothing

-- Return the number represented in binary as an initial segment of
-- the string (remembering that if a number begins 0, it's zero).
eatBinary : (Eq i, Num i) => String -> i
eatBinary = firstDigit . unpack where

  laterDigit : i -> List Char -> i
  laterDigit n [] = n
  laterDigit n (d :: ds) = let
    f : Maybe i -> i
    f Nothing = n
    f (Just a) = laterDigit (2*n + a) ds
    in f $ toBit d

  firstDigit : List Char -> i
  firstDigit [] = 0
  firstDigit (d :: ds) = let
    f : Maybe i -> i
    f Nothing = 0
    f (Just 0) = 0
    f (Just a) = laterDigit a ds
    in f $ toBit d


text:
module Client.Skeleton.Skeleton

import Client.Skeleton.BaseWithTest.InigoTOML
import Client.Skeleton.BaseWithTest.Package
import Client.Skeleton.BaseWithTest.Test.Suite
import Client.Skeleton.BaseWithTest.Test.Test

public export
data Skeleton : Type where
  BaseWithTest : Skeleton

export
toString : Skeleton -> String
toString BaseWithTest = "BaseWithTest"

export
describe : Skeleton -> String
describe BaseWithTest = "base skeleton with tests"

export
fromString : String -> Maybe Skeleton
fromString "BaseWithTest" = Just BaseWithTest
fromString _ = Nothing

export
getFiles : Skeleton -> (String, String) -> List (List String, String)
getFiles BaseWithTest vars =
  [ ( Client.Skeleton.BaseWithTest.InigoTOML.name vars
    , Client.Skeleton.BaseWithTest.InigoTOML.build vars
    )
  , ( Client.Skeleton.BaseWithTest.Package.name vars
    , Client.Skeleton.BaseWithTest.Package.build vars
    )
  , ( Client.Skeleton.BaseWithTest.Test.Suite.name vars
    , Client.Skeleton.BaseWithTest.Test.Suite.build vars
    )
  , ( Client.Skeleton.BaseWithTest.Test.Test.name vars
    , Client.Skeleton.BaseWithTest.Test.Test.build vars
    )
  ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- ----------------------------------------------------------- [ Structure.idr ]
-- Module    : Structure.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| This section details the check for structural link insertion.
|||
||| Correctness/Soundess Properties of a Structural Link
|||
||| 1. The src and destination must not be the same.
||| 2. A node can only be decomposed once.
||| 3. The decomposition type must be valid for the parent.
||| 4. A parent cannot be contained by its children.
|||
module GRL.Property.Structure

import public Data.AVL.Graph
import public Data.List
import public Data.Stack

import GRL.Model
import GRL.IR
import GRL.Common

%default partial
%access export

-- ----------------------------------------------- [ Structural Link Insertion ]

||| No loops and all different children.
allDiff : GExpr ELEM -> List (GExpr ELEM) -> Bool
allDiff src ds = diffDSTs ds && noLoopBack src ds
  where
    diffDSTs : List (GExpr ELEM) -> Bool
    diffDSTs xs = if length xs == 1
                   then True
                   else not $ and [ eqGExpr x y | x <- xs, y <- xs]

    noLoopBack : GExpr ELEM -> List (GExpr ELEM) -> Bool
    noLoopBack y xs = not $ and $ map (\x => eqGExpr x y) xs

||| Nodes are all valid nodes
validNodes : List (GExpr ELEM) -> GModel -> Bool
validNodes ns m = and $ map (\n => isValid n m) ns
  where
    isValid : GExpr ELEM -> GModel -> Bool
    isValid (Elem ty t s) m = hasGoal t m

||| The node is free to be decomposed, or has been decomposed and are
||| adding the same decomposition.
validDTy : GExpr ELEM -> GStructTy -> GModel -> Bool
validDTy (Elem ty t s) dty m =
  case getGoalByTitle t m of
    Nothing => False
    Just n  => case getStructTy n of
        Nothing  => True
        Just xty => xty == dty

-- -------------------------------------------------------------- [ Evaluation ]
private
record ComputeState where
  constructor MkState
  next : Stack NodeID
  seen : List NodeID

private
defState : List NodeID -> ComputeState
defState is = MkState (pushSThings is mkStack) (List.Nil)

private
cycleCheck : NodeID -> NodeID -> List NodeID -> Bool
cycleCheck id curr seen = elem curr seen || curr == id || elem id seen

partial
private
doComputeSpan : (id    : NodeID)
              -> (model : GModel)
              -> (st    : ComputeState)
              -> Bool
doComputeSpan id g st =
    case popS' (next st) of
      Nothing          => True
      Just (curr, newS) =>  -- TODO
        if cycleCheck id curr (seen st)
          then False
          else let cs = children curr in
              if isNil cs
                then True && doComputeSpan id g
                                 (record { next = newS} st)
                else
                  if elem id cs
                    then False -- If thing is in children
                    else True && doComputeSpan id g
                        (record { seen = curr :: (seen st)
                                , next = newS ++ cs} st)
  where
    children : NodeID -> List NodeID
    children n = map fst $ getDeCompEdges n g

%assert_total
computeSpan : GExpr STRUCT -> GModel -> Bool
computeSpan (SLink ty (Elem ty' t s) ds) m =
    case initID of
      Nothing => False
      Just id => doComputeSpan id m (defState ds')
  where
    initID : Maybe NodeID
    initID = getGoalIDByTitle t m

    ds' : List (NodeID)
    ds' = catMaybes $ map (\x => getGoalIDByTitle (getTitle x) m) ds

partial
checkStructBool : GExpr STRUCT -> GModel -> Bool
checkStructBool l@(SLink ty src ds) m =
    length ds >= 1
    && allDiff src ds
    && validNodes (src :: ds) m
    && validDTy src ty m
    && computeSpan l m

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Compiler.Opts.ConstantFold

import Compiler.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Primitives
import Core.Value
import Data.List
import Data.Vect

findConstAlt : Constant -> List (CConstAlt vars) ->
               Maybe (CExp vars) -> Maybe (CExp vars)
findConstAlt c [] def = def
findConstAlt c (MkConstAlt c' exp :: alts) def = if c == c'
    then Just exp
    else findConstAlt c alts def

foldableOp : PrimFn ar -> Bool
foldableOp BelieveMe = False
foldableOp (Cast from to)
  = fromMaybe False [| intKind from `smaller` intKind to |]
  where
    smaller : IntKind -> IntKind -> Bool
    smaller (Signed x) (Signed y) = x <= y
    smaller (Unsigned x) (Unsigned y) = x <= y
    smaller (Signed x) (Unsigned y) = x < P y
    smaller (Unsigned x) (Signed y) = P x < y
foldableOp _ = True

data Subst : List Name -> List Name -> Type where
  Nil  : Subst [] vars
  (::) : CExp vars -> Subst ds vars -> Subst (d :: ds) vars
  Wk   : SizeOf ws -> Subst ds vars -> Subst (ws ++ ds) (ws ++ vars)

initSubst : (vars : List Name) -> Subst vars vars
initSubst vars
  = rewrite sym $ appendNilRightNeutral vars in
    Wk (mkSizeOf vars) []

wk : SizeOf out -> Subst ds vars -> Subst (out ++ ds) (out ++ vars)
wk sout (Wk {ws, ds, vars} sws rho)
  = rewrite appendAssociative out ws ds in
    rewrite appendAssociative out ws vars in
    Wk (sout + sws) rho
wk ws rho = Wk ws rho

record WkCExp (vars : List Name) where
  constructor MkWkCExp
  {0 outer, supp : List Name}
  size : SizeOf outer
  0 prf : vars === outer ++ supp
  expr : CExp supp

Weaken WkCExp where
  weaken (MkWkCExp s Refl e) = MkWkCExp (suc s) Refl e

lookup : FC -> Var ds -> Subst ds vars -> CExp vars
lookup fc (MkVar p) rho = case go p rho of
    Left (MkVar p') => CLocal fc p'
    Right (MkWkCExp s Refl e) => weakenNs s e

  where

  go : {i : Nat} -> {0 ds, vars : _} -> (0 _ : IsVar n i ds) ->
       Subst ds vars -> Either (Var vars) (WkCExp vars)
  go First     (val :: rho) = Right (MkWkCExp zero Refl val)
  go (Later p) (val :: rho) = go p rho
  go p         (Wk ws  rho) = case sizedView ws of
    Z => go p rho
    S ws' => case i of
      Z => Left (MkVar First)
      S i' => bimap later weaken (go (dropLater p) (Wk ws' rho))

-- constant folding of primitive functions
-- if a primitive function is applied to only constant
-- then replace with the result
-- if there's only 1 constant argument to a commutative function
-- move the constant to the right. This simplifies Compiler.Opts.Identity
constFold : {vars' : _} ->
            Subst vars vars' ->
            CExp vars -> CExp vars'
constFold rho (CLocal fc p) = lookup fc (MkVar p) rho
constFold rho e@(CRef fc x) = CRef fc x
constFold rho (CLam fc x y)
  = CLam fc x $ constFold (wk (mkSizeOf [x]) rho) y
constFold rho (CLet fc x inlineOK y z) =
    let val = constFold rho y
     in case val of
        CPrimVal _ _ => if inlineOK
            then constFold (val :: rho) z
            else CLet fc x inlineOK val (constFold (wk (mkSizeOf [x]) rho) z)
        _ => CLet fc x inlineOK val (constFold (wk (mkSizeOf [x]) rho) z)
constFold rho (CApp fc x xs) = CApp fc (constFold rho x) (constFold rho <$> xs)
constFold rho (CCon fc x y tag xs) = CCon fc x y tag $ constFold rho <$> xs
constFold rho (COp {arity} fc fn xs) =
    let xs' = map (constFold rho) xs
        e = constRight fc fn xs'
     in fromMaybe e $ do
          guard (foldableOp fn)
          nfs <- traverse toNF xs'
          nf <- getOp fn nfs
          fromNF nf
  where
    toNF : CExp vars' -> Maybe (NF vars')
    -- Don't fold `Int` and `Double` because they have varying widths
    toNF (CPrimVal fc (I _)) = Nothing
    toNF (CPrimVal fc (Db _)) = Nothing
    -- Fold the rest
    toNF (CPrimVal fc c) = Just $ NPrimVal fc c
    toNF _ = Nothing

    fromNF : NF vars' -> Maybe (CExp vars')
    fromNF (NPrimVal fc c) = Just $ CPrimVal fc c
    fromNF _ = Nothing

    commutative : Constant -> Bool
    commutative DoubleType = False
    commutative _ = True

    constRight : {ar : _} -> FC -> PrimFn ar ->
                 Vect ar (CExp vars') -> CExp vars'
    constRight fc (Add ty) [x@(CPrimVal _ _), y] =
        if commutative ty
            then COp fc (Add ty) [y, x]
            else COp fc (Add ty) [x, y]
    constRight fc (Mul ty) [x@(CPrimVal _ _), y] =
        if commutative ty
            then COp fc (Mul ty) [y, x]
            else COp fc (Mul ty) [x, y]
    constRight fc fn args = COp fc fn args

constFold rho (CExtPrim fc p xs) = CExtPrim fc p $ constFold rho <$> xs
constFold rho (CForce fc x y) = CForce fc x $ constFold rho y
constFold rho (CDelay fc x y) = CDelay fc x $ constFold rho y
constFold rho (CConCase fc sc xs x)
  = CConCase fc (constFold rho sc) (foldAlt <$> xs) (constFold rho <$> x)
  where
    foldAlt : CConAlt vars -> CConAlt vars'
    foldAlt (MkConAlt n ci t xs e)
      = MkConAlt n ci t xs $ constFold (wk (mkSizeOf xs) rho) e

constFold rho (CConstCase fc sc xs x) =
    let sc' = constFold rho sc
     in case sc' of
        CPrimVal _ val => case findConstAlt val xs x of
            Just exp => constFold rho exp
            Nothing => CConstCase fc (constFold rho sc) (foldAlt <$> xs) (constFold rho <$> x)
        _ => CConstCase fc (constFold rho sc) (foldAlt <$> xs) (constFold rho <$> x)
  where
    foldAlt : CConstAlt vars -> CConstAlt vars'
    foldAlt (MkConstAlt c e) = MkConstAlt c $ constFold rho e
constFold rho (CPrimVal fc v) = CPrimVal fc v
constFold rho (CErased fc) = CErased fc
constFold rho (CCrash fc err) = CCrash fc err

constFoldCDef : CDef -> Maybe CDef
constFoldCDef (MkFun args exp)
  = Just $ MkFun args $ constFold (initSubst args) exp
constFoldCDef _ = Nothing

export
constantFold : Ref Ctxt Defs => Name -> Core ()
constantFold fn = do
    defs <- get Ctxt
    Just (fnIdx, gdef) <- lookupCtxtExactI fn defs.gamma
        | Nothing => pure ()
    let Just cdef = gdef.compexpr
        | Nothing => pure ()
    let Just cdef' = constFoldCDef cdef
        | Nothing => pure ()
    log "compiler.const-fold" 50 $ "constant folding " ++ show !(getFullName fn)
                                 ++ "\n\told def: " ++ show cdef
                                 ++ "\n\tnew def: " ++ show cdef'
    setCompiled (Resolved fnIdx) cdef'


text: -- WIP


text:
module AddAll

-- The idea from Thorsten Altenkirch's "Why Type Theory matters" at Lambda Days 2019 --

public export
data NatFun : a -> Type where
  SZ : NatFun Nat
  SS : NatFun x -> NatFun (Nat -> x)

liftUnary : (Nat -> Nat) -> NatFun a => a -> a
liftUnary f @{SZ}   nf = f nf
liftUnary f @{SS s} nf = liftUnary f . nf

-- You can also lift binary and `const`

export
add : NatFun a => a
add @{SZ}   = 0
add @{SS s} = \n => liftUnary (n+) add

x : Nat
x = add 2 3 4 5

y : Nat
y = add 1 2


text:
module VectorsAndLists

import Data.List
import Data.Vect

%default total

list2vec : (l : List a) -> Vect (length l) a
list2vec [] = []
list2vec (x::xs) = x :: list2vec xs

safeToVec : List a -> Maybe (Vect n a)
safeToVec {n} l = if length l == n
                    then Just $ list2vec l -- need a proof that length l = n
                    else Nothing


text:
> module Listable
> import Functions
> import Data.Fin
> import Data.List
> import Data.List.TypeEnumeration
> import Data.Fin.Extensions

Now we turn to propositions about finiteness. We start with the well-known
Kuratowski finiteness, which we will call `Listable`: a type $t$ is Kuratowski
finite if its elements can be put into a single list. That is, we can find a list
$xs$ satisfying $\texttt{All} \{t\} xs$.

> ||| Proofs that a type `t` can be completely enumerated by a list `xs`.
> ||| Alternatively, this is a definition of a finite type.
> Listable : (t : Type) -> Type
> Listable t = (xs ** (All {t} xs))

An alternative idea is to require a surjection $\texttt{Fin} n \rightarrow t$
for some $n:\texttt{Nat}$:

> FinSurjective : (t: Type) -> Type
> FinSurjective ty = (n:Nat ** (fromFin : (Fin n -> ty) ** (Surjective fromFin)))

These notions are equivalent. We need some helper lemmas... it is quite likely
that these can be cleaned up considerably...

> ||| If we have a proof that `x` is contained in the list `xs`, then we can map
> ||| that proof to a `Fin (length xs)` in the obvious way.
> getIndexOfElem : {x:t} -> Elem x xs -> Fin (length xs)
> getIndexOfElem Here = FZ
> getIndexOfElem (There later) = FS (getIndexOfElem later)

> ||| Given a proof that some `xs : List t` contains all instances of type `t`,
> ||| get the `Fin (length xs)`-valued index of any `x : t`.
> getIndexFromAll : All {t} xs -> t -> Fin (length xs)
> getIndexFromAll {xs = []} pf x = absurd (pf x)
> getIndexFromAll {xs = (y :: xs)} pf x = getIndexOfElem (pf x)

> allFinBijection : {t:Type} -> All {t} xs -> (f:(t-> Fin (length xs)) ** Bijective f)
> allFinBijection pf = ((getIndexFromAll pf) ** (?tvalHole1,?tvalHole2))

> ||| Index into a list `l` with a `Fin (length l).`
> finIndexList : (l:List t) -> Fin (length l) -> t
> finIndexList [] _ impossible
> finIndexList (x :: _) FZ = x
> finIndexList (_ :: xs) (FS y) = finIndexList xs y

> getIndexOfElemLemma : {x:t} -> (pf : Elem x xs) -> finIndexList xs (getIndexOfElem pf) = x
> getIndexOfElemLemma {xs = (x :: ys)} Here = Refl
> getIndexOfElemLemma {xs = (y :: ys)} (There later) = getIndexOfElemLemma later

> getIndexOfAllLemma : (pf : All {t} xs) -> (x : t) -> finIndexList xs (getIndexFromAll pf x) = x
> getIndexOfAllLemma {xs} pf x with (pf x)
>   getIndexOfAllLemma {xs= x :: ys} pf x | Here = getIndexOfElemLemma (pf x)
>   getIndexOfAllLemma {xs= y :: ys} pf x | (There later) = getIndexOfElemLemma (pf x)

> finIndexListSurjectiveIfAll : All {t} xs -> Surjective (finIndexList xs)
> finIndexListSurjectiveIfAll {xs} pf = \y => ((getIndexFromAll pf y) ** (getIndexOfAllLemma pf y))

> indexIntoAll : All {t} xs -> (f : (Fin (length xs) -> t) ** Surjective f)
> indexIntoAll {xs} pf = ((finIndexList xs) ** (finIndexListSurjectiveIfAll pf))

> listableIsFinSurjective : Listable t -> FinSurjective t
> listableIsFinSurjective (xs ** pf) = ((length xs) ** (indexIntoAll pf))

> elemToFinIndex : {t : Type} -> (x:t  ** Elem x xs) -> Fin (length xs)
> elemToFinIndex (_ ** Here) = FZ
> elemToFinIndex ( x ** (There later)) = FS (elemToFinIndex (x ** later))

> elemLemma : {y: t} -> (x ** Data.List.Elem x xs) -> (x ** Data.List.Elem x (y :: xs))
> elemLemma (a ** pf) = (a ** (Data.List.There pf))

> finIndexToElem : (xs : List t) -> (index : Fin (length xs)) -> (x : t ** (Elem x xs))
> finIndexToElem [] _ impossible
> finIndexToElem (x :: xs) FZ = (x ** Here)
> finIndexToElem (b :: bs) (FS j) = elemLemma {y=b} (finIndexToElem bs j)

> elemLemmaLemma : {y:t} -> {xs : List t} -> {e : (x ** Data.List.Elem x xs)} -> (elemToFinIndex e = m) -> (elemToFinIndex (elemLemma e) = FS m)
> elemLemmaLemma {y = y} {e = (x ** pf)} Refl = Refl

> elemToFinIndexLemma : (x : t) -> (xs : List t) -> (y : Fin (length xs)) ->
>                       (subres2 : elemToFinIndex (finIndexToElem xs y) = y) ->
>                       elemToFinIndex (elemLemma (finIndexToElem xs y)) = FS y
> elemToFinIndexLemma x [] y _ impossible
> elemToFinIndexLemma x (z :: xs) y subres2 = elemLemmaLemma {y=z} {xs=(z::xs)} {e=(finIndexToElem(z::xs) y)} subres2

> finIndexElemInverse1 : (xs : List t) -> (index : Fin (length xs)) -> (elemToFinIndex (finIndexToElem xs index) = index)
> finIndexElemInverse1 [] _ impossible
> finIndexElemInverse1 (x :: xs) FZ = Refl
> finIndexElemInverse1 (x :: xs) (FS y) = let subres2 = (finIndexElemInverse1 xs y) in (elemToFinIndexLemma x xs y subres2)

> finIndexElemInverse2 : {x:t} -> (xs : List t) -> (elem : Elem x xs) -> finIndexToElem xs (elemToFinIndex (x**elem)) = (x**elem)
> finIndexElemInverse2 (x::ys) Here = Refl
> finIndexElemInverse2 {x} (y::ys) (There later) = ?finIndexElemInverse2Hole2

> finSurjectiveIsListable : FinSurjective t -> Listable t
> finSurjectiveIsListable (bound ** (surj ** pf)) = ?finSurjectiveIsListable_rhs_2

Listability gives an upper bound on the cardinality of any given type considered
as sets. We can strengthen this by forbidding duplicates:

> ListableNoDuplicate : (t: Type) -> Type
> ListableNoDuplicate t = (xs : List t ** (All {t} xs, NoDupes {t} xs))

Alternatively, we can strengthen FinSurjectivity by requring a bijection:

> FinBijective : (t: Type) -> Type
> FinBijective t  = (n:Nat ** (f : (t -> Fin n) ** Bijective f))

These two notions are equivalent:

> finBijToListNoDupes : {t:Type} -> FinBijective t -> ListableNoDuplicate t

> listNoDupesToFinBij : {t:Type} -> ListableNoDuplicate t -> FinBijective t

Actually, all four notions of finiteness are equivalent. The reason is that
listability implies decidable equality:

> listableToDecEq : {t:Type} -> Listable t -> (x: t) -> (y : t) -> Dec (x = y)
> listableToDecEq (xs **pf) x y = ?listableToDecEq_rhs

With this (along with the implication $\texttt{DecEq} \Rightarrow \texttt{DecIn}$)
we can implement removal of duplicates.

ext: lidr

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
module Dart.FFI.UpcastList

import Dart.Core
import Dart.FFI.Upcast

public export
data UpcastList : Type -> Type where
  MkUpcastList : List elTy -> UpcastList elTy

namespace UpcastList
  %inline
  export
  Nil : UpcastList _
  Nil = MkUpcastList []

  %inline
  export
  (::) : IsAssignableFrom elTy ty => ty -> UpcastList elTy -> UpcastList elTy
  (::) e (MkUpcastList es) = MkUpcastList (upcast e :: es)

  export
  toList : UpcastList elTy -> List elTy
  toList (MkUpcastList es) = es

  export
  into : DartList elTy -> UpcastList elTy -> IO (DartList elTy)
  into result es = do
    traverse (`add` result) (toList es)
    pure result


text:
module Vektoren

import Data.Vect

data Vektor : (n:Nat) -> (a:Type) -> Type where
  Nil : Vektor 0 a
  (::) : a -> Vektor n a -> Vektor (S n) a

concat : Vektor n a -> Vektor m a -> Vektor (n+m) a
concat [] ys = ys
concat (x :: xs) ys = x :: concat xs ys

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts


text:
module WeakenedPredicateError

import Data.Fin

{-
-- Can't do this for some reason
bad1 : { p : {m : Nat} -> Fin (S m) -> a -> Type }
	-> ( (i : Fin predn)
		-> Sigma a (p $ weaken $ FS i)
		-> Sigma a (p $ weaken $ weaken i) )
	-> (i : Fin predn)
	-> Sigma a ((p . weaken) $ FS i)
	-> Sigma a ((p . weaken) $ weaken i)
-}

{-
-- Universe inconsistency when not entered in REPL.
bad2 : ?bad2_ty
bad2_ty = proof
  exact {a : Type} -> { p : {m : Nat} -> Fin (S m) -> a -> Type } -> {predn : Nat} -> _
  exact _ -> _
  exact (i : Fin predn) -> Sigma a (p $ weaken $ FS i) -> Sigma a (p $ weaken $ weaken i)
  exact (i : Fin predn) -> Sigma a _ -> Sigma a _
  exact (p . weaken) $ FS i
  exact (p . weaken) $ weaken i
-}

{-
-- Same as bad1 but with the implicit argument to (p) filled in in each application.
bad3 : { p : {m : Nat} -> Fin (S m) -> a -> Type }
	-> ( (i : Fin predn)
		-> Sigma a (p {m=S predn} $ weaken $ FS i)
		-> Sigma a (p {m=S predn} $ weaken $ weaken i) )
	-> (i : Fin predn)
	-> Sigma a (((p {m=S predn}) . weaken) $ FS i)
	-> Sigma a (((p {m=S predn}) . weaken) $ weaken i)
-}

good1 : (p : {m : Nat} -> Fin m -> a -> Type)
	-> (i : Fin n)
	-> (fn : (x : a) -> (j : Fin n) -> p j x -> p (weaken j) x)
	-> (pr : Sigma a (p i))
	-> Sigma a (p $ weaken i)
good1 = ?good1_pr

good1_pr = proof
  intros
  exact (getWitness pr ** fn (getWitness pr) i (getProof pr))

good2 : (p : {m : Nat} -> Fin m -> a -> Type)
	-> (i : Fin n)
	-> ( fn : (j : Fin n) -> Sigma a (p j) -> Sigma a (p $ weaken j) )
	-> (pr : Sigma a (p i))
	-> Sigma a (p $ weaken i)
good2 = ?good2_pr

good2_pr = proof
  intros
  exact fn i pr

good3 : (n : Nat)
	-> (p : (m : Nat) -> Fin m -> a -> Type)
	-> (i : Fin n)
	-> (fn : (x : a) -> (j : Fin n) -> p n j x -> p (S n) (weaken j) x)
	-> Sigma a (p n i)
	-> Sigma a (p (S n) (weaken i))

-- Same as bad3 but with the first argument of (p) explicit.
good4 : { p : (m : Nat) -> Fin (S m) -> a -> Type }
	-> ( (i : Fin predn)
		-> Sigma a (p (S predn) $ weaken $ FS i)
		-> Sigma a (p (S predn) $ weaken $ weaken i) )
	-> (i : Fin predn)
	-> Sigma a (((p (S predn)) . weaken) $ FS i)
	-> Sigma a (((p (S predn)) . weaken) $ weaken i)

{-
bad4 : { p : {m : Nat} -> Fin (S m) -> a -> Type }
	-> ( (i : Fin predn)
		-> Sigma a (p {m=S predn} $ weaken $ FS i)
		-> Sigma a (p {m=S predn} $ weaken $ weaken i) )
	-> Nat
-}

{-
bad5 : { p : {m : Nat} -> Fin (S m) -> a -> Type }
	-> (i : Fin predn)
	-> Sigma a (((p {m=S predn}) . weaken) $ FS i)
-}

{-
bad6 : ( p : {m : Nat} -> Nat -> a -> Type )
	-> (i : Nat)
	-> Sigma a (p {m=Z} i)
-}

{-
bad7 : ( p : {m : Nat} -> a -> Type )
	-> Sigma a (p {m=Z})
-}

{-
bad8 : (a : Type)
	-> ( p : {m : Nat} -> a -> Type )
	-> Sigma a (p {m=Z})
-}

{-
-- Different error : No such variable (p)
bad9 : (a : Type)
	-> ( p : {m : Nat} -> a -> Type )
	-> (x : a)
	-> (p {m=Z} x)
	-> Sigma a (p {m=Z})
-}

{-
-- No such variable (p)
bad10 : ( p : {m : Nat} -> Type )
	-> Sigma Nat (\n => p {m=n})
-}

{-
-- No such variable (p)
bad11 : ( p : {m : Nat} -> Type )
	-> (p {m=Z})
	-> Sigma Nat Fin
-}

-- For whatever reason, this is fine to declare.
good5 : ( p : {m : Nat} -> Type )
	-> Sigma Nat p
good5 = ?good5_pr

{-
> :prove good5_pr
----------                 Goal:                  ----------
{hole0} : (p : Type) -> Sigma Nat p
-WeakenedPredicateError.good5_pr> intro
----------              Other goals:              ----------
{hole0}
----------              Assumptions:              ----------
 p : Type
----------                 Goal:                  ----------
{hole1} : Sigma Nat p
-WeakenedPredicateError.good5_pr> exact (Z ** _)

----------              Assumptions:              ----------
 p : Type
----------                 Goal:                  ----------
{pf505} : p 0
-}

{-
-- No such variable (p)
bad12 : ( p : {m : Nat} -> Type )
	-> p Z
	-> Sigma Nat p
-}

{-
-- No such variable (p)
bad13 : ( p : {m : Nat} -> Type )
	-> (a : Nat ** p {m=a})
-}

{-
"
When checking argument P to type constructor Builtins.Sigma:
        Type mismatch between
                Type (Type of p)
        and
                Type (Expected type)
"

---

bad14 : ( p : {m : Nat} -> Type )
	-> (a : Nat ** p)
-}


text:
-- Classical propositional logic, PHOAS approach, final encoding

module Pf.Cp

%default total

-- Types

infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty
  (:&&) : Ty -> Ty -> Ty
  (:||) : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 :<=>
(:<=>) : Ty -> Ty -> Ty
(:<=>) a b = (a :=> b) :&& (b :=> a)

NOT : Ty -> Ty
NOT a = a :=> FALSE

TRUE : Ty
TRUE = FALSE :=> FALSE

-- Context and truth judgement

Cx : Type
Cx = Ty -> Type

isTrue : Ty -> Cx -> Type
isTrue a tc = tc a

-- Terms

TmRepr : Type
TmRepr = Cx -> Ty -> Type

infixl 1 :$
class ArrMpTm (tr : TmRepr) where
  var  : isTrue a tc                -> tr tc a
  lam' : (isTrue a tc -> tr tc b)   -> tr tc (a :=> b)
  (:$) : tr tc (a :=> b) -> tr tc a -> tr tc b

lam'' : {tr : TmRepr} -> ArrMpTm tr => (tr tc a -> tr tc b) -> tr tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

syntax "lam" {a} ":=>" [b] = lam'' (\a => b)

class ArrMpTm tr => MpTm (tr : TmRepr) where
  pair  : tr tc a         -> tr tc b -> tr tc (a :&& b)
  fst   : tr tc (a :&& b)            -> tr tc a
  snd   : tr tc (a :&& b)            -> tr tc b
  left  : tr tc a                    -> tr tc (a :|| b)
  right : tr tc b                    -> tr tc (a :|| b)
  case' : tr tc (a :|| b) -> (isTrue a tc -> tr tc c) -> (isTrue b tc -> tr tc c) -> tr tc c

case'' : {tr : TmRepr} -> MpTm tr => tr tc (a :|| b) -> (tr tc a -> tr tc c) -> (tr tc b -> tr tc c) -> tr tc c
case'' xy f g = case' xy (\x => f (var x)) (\y => g (var y))

syntax "["    [a]  ","  [b] "]" = pair a b
syntax "case" [ab] "of" {a} ":=>" [c1] or {b} ":=>" [c2] = case'' ab (\a => c1) (\b => c2)

class MpTm tr => CpTm (tr : TmRepr) where
  abort' : (isTrue (NOT a) tc -> tr tc FALSE) -> tr tc a

abort'' : {tr : TmRepr} -> CpTm tr => (tr tc (NOT a) -> tr tc FALSE) -> tr tc a
abort'' f = abort' $ \na => f (var na)

syntax "abort" {a} ":=>" [b] = abort'' (\a => b)

Thm : Ty -> Type
Thm a = {tr : TmRepr} -> {tc : Cx} -> CpTm tr => tr tc a

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
import Effects
import Effect.StdIO
import Effect.State

-- Local Variables:
-- idris-load-packages: ("contrib" "prelude" "effects" "base")
-- End:

-- this is mostly code from the tutorial on effects
hello : Eff () [STDIO]
hello = putStrLn "hello world!"

data BTree a = Leaf
             | Node (BTree a) a (BTree a)

testTree : BTree String
testTree = Node (Node Leaf "Jim" Leaf)
                "Fred"
                (Node (Node Leaf "Alice" Leaf)
                      "Sheila"
                      (Node Leaf "Bob" Leaf))

treeTagAux : BTree a -> Eff (BTree (Int,a)) [STATE Int]
treeTagAux Leaf = pure Leaf
treeTagAux (Node b1 x b2) = do
                    b1' <- treeTagAux b1
                    i <- get
                    put (i + 1)
                    b2' <- treeTagAux b2
                    pure (Node b1' (i,x) b2')

-- So one of the things that I find super fascinating are the dependent effects
-- obviously such things are needed for the purpose of having things like state that
-- contain dependent types, but it's also just really neat and makes, at least to me,
-- more sense than the simple-type-theory style monadic approach to semantics
-- The way I think I see effects in Idris is that you're essentially creating an internal
-- language of an effect and then you need to give a semantics of the effect in terms of
-- the types that support the operation and *that* is what the handlers are.

-- Let's try making a reader effect, one that has an ask and local operation

data Reader : Effect where
  Ask : Reader a a (\x => a)
  Local : (a -> b) -> Reader c b f -> Reader c a (\x => a)

-- I think that's the right signature, it type checks at least. It's a little more complicated
-- than a normal reader because there could be some kind of dependent type in the reader state
-- such as, I don't know, an environment that's indexed by its length?

-- so what we're trying to do here is
-- run the "local" effect with the resource (f r)
-- get back the value, in this case of type 't' from the local effect action
-- then restore the original state by passing that to the original continuation
-- now where I'm getting stuck, I think, is that, to me, this should clearly be something
-- kinda like
--  handle (f r) loc (\t _ => k t r)

 rhs : (m : Type -> Type) -> (r : res) -> (act : Reader t res resk) -> (k : (x : t) -> resk x -> m a) -> m a
 rhs m r Ask k = k r r
 rhs m r (Local f loc) k = rhs m (f r) loc (\ t,_ => k t r) -- Why did this work but recursion in handle didn't???

 READER : Type -> EFFECT
 READER t = MkEff t Reader -- yeah this part is just like state aren't I clever

instance Handler Reader m where
  handle r act k = rhs m r act k

{-
instance Handler Reader m where
  handle r Ask k = k r r
  handle r (Local f loc) k = handle (f r) loc ?f
-}

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


text:
%default total

record DirEntry where
  constructor MkDirEntry

data Action : Type -> Type where
  ListDirectory : String -> Action (List DirEntry)
  RemoveFile    : String -> Action ()
  RemovePath    : String -> Action ()

data Script : Type -> Type where
  Pure : (val : res) -> Script res
  Bind : (act : Action r1) -> (step : r1 -> Script r2) -> Script r2

Functor Script where
  map f (Pure res) = Pure $ f res
  map f (Bind act step) = Bind act $ \x => f <$> step x

Applicative Script where
  pure = Pure
  (Pure f)        <*> script = f <$> script
  (Bind act step) <*> script = Bind act $ \x => step x <*> script

Monad Script where
  (Pure val)      >>= f = f val
  (Bind act step) >>= f = Bind act $ \x => step x >>= f


text:
module Main

import Data.Vect
import System.REPL
import Data.String

data DataStore : Type where
     MkData    : (size : Nat) ->
                 (items: Vect size String) ->
                 DataStore

-- Store commands
size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items)
    where
        addToData : Vect old String -> Vect (S old) String
        addToData [] = [newitem]
        addToData (item :: items) = item :: addToData items

getItem : Integer -> DataStore -> Maybe (String, DataStore)
getItem i store@(MkData size items) = case integerToFin i size of
                                     Nothing => Just ("Entry not found\n", store)
                                     Just i => Just (index i items ++ "\n", store)

search : String -> DataStore -> Maybe (String, DataStore)
search substr store@(MkData size items) = Just (searchItems items, store) where
                                          searchItems : Vect n String -> String
                                          searchItems [] = "No entries with " ++ substr ++ " found\n"
                                          searchItems (x :: xs) = case isInfixOf substr x of
                                                                        False => searchItems xs
                                                                        True => show (length xs) ++ ": " ++ x ++ "\n"

-- REPL UI

data Command = Add String
             | Get Integer
             | Search String
             | Size
             | Quit

parseCommand : String -> String -> Maybe Command
parseCommand cmd input = case cmd of
                              "add" => Just (Add input)
                              "get" => map (\i => Get i) (parseInteger input)
                              "search" => Just (Search input)
                              "size" => Just Size
                              "quit" => Just Quit
                              _ => Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

processCommand : DataStore -> Command -> Maybe (String, DataStore)
processCommand store (Add str) = Just ("Added ID " ++ show (size store) ++ " to store\n", addToStore store str)
processCommand store (Get i) = getItem i store
processCommand store Size = Just (show (size store) ++ " entries in store\n", store)
processCommand store (Search substr) = search substr store
processCommand _ Quit = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
                                Nothing => Just ("Invalid command\n", store)
                                Just cmd => processCommand store cmd

main : IO ()
main = replWith (MkData _ []) "Command: " processInput


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
module BayesianOptimization.Acquisition

import public Data.Nat
import Distribution
import Tensor
import Data
import Model
import Optimize
import BayesianOptimization.Morphisms
import Error

||| An `Empiric` constructs values from historic data and the model over that data.
|||
||| @features The shape of the feature domain.
||| @out The type of the value constructed by the `Empiric`.
public export 0
Empiric : Distribution targets marginal => (0 features : Shape) -> (0 out : Type) -> Type
Empiric features out = Dataset features targets -> ProbabilisticModel features {marginal} -> out

||| An `Acquisition` function quantifies how useful it would be to query the objective at a given
||| set of points, towards the goal of optimizing the objective.
|||
||| @batch_size The number of points in the feature domain that the `Acquisition` evaluates
|||   at once.
||| @features The shape of the feature domain.
public export 0
Acquisition : (0 batch_size : Nat) -> {auto 0 _ : GT batch_size 0} -> (0 features : Shape) -> Type
Acquisition batch_size features = Tensor (batch_size :: features) Double -> Tensor [] Double

||| Construct the acquisition function that estimates the absolute improvement in the best
||| observation if we were to evaluate the objective at a given point.
|||
||| @model The model over the historic data.
||| @best The current best observation.
export
expectedImprovement : ProbabilisticModel features {marginal=Gaussian [1]} ->
                      (best : Tensor [] Double) -> Acquisition 1 features
expectedImprovement predict best at =
  let marginal = predict at
      best' = broadcast {to=[_, 1]} best
      pdf = pdf marginal best'
      cdf = cdf marginal best'
      mean = squeeze (mean marginal)
      variance = squeeze (variance marginal)
   in (best - mean) * cdf + variance * pdf

||| Build an acquisition function that returns the absolute improvement, expected by the model, in
||| the observation value at each point.
export
expectedImprovementByModel : Empiric features {marginal=Gaussian [1]} $ Acquisition 1 features
expectedImprovementByModel (MkDataset query_points _) predict at =
  let best = squeeze $ reduce_min 0 $ mean $ predict query_points
   in expectedImprovement predict best at

||| Build an acquisition function that returns the probability that any given point will take a
||| value less than the specified `limit`.
export
probabilityOfFeasibility : (limit : Tensor [] Double) -> ClosedFormDistribution [1] d =>
                           Empiric features {marginal=d} $ Acquisition 1 features
probabilityOfFeasibility limit _ predict at = cdf (predict at) $ broadcast {to=[_, 1]} limit

||| Build an acquisition function that returns the negative of the lower confidence bound of the
||| probabilistic model. The variance contribution is weighted by a factor `beta`.
|||
||| @beta The weighting given to the variance contribution. If negative, this function will return
|||   `Nothing`.
export
negativeLowerConfidenceBound : (beta : Double) ->
  Either ValueError $ Empiric features {marginal=Gaussian [1]} $ Acquisition 1 features
negativeLowerConfidenceBound beta =
  if beta < 0
  then Left $ MkValueError $ "beta should be greater than or equal to zero, got " ++ show beta
  else Right $ \_, predict, at =>
    let marginal = predict at
     in squeeze $ mean marginal - const beta * variance marginal

||| Build the expected improvement acquisition function in the context of a constraint on the input
||| domain, where points that do not satisfy the constraint do not offer an improvement. The
||| complete acquisition function is built from a constraint acquisition function, which quantifies
||| whether specified points in the input space satisfy the constraint.
export
expectedConstrainedImprovement : (limit : Tensor [] Double) ->
  Empiric features {marginal=Gaussian [1]} $ (Acquisition 1 features -> Acquisition 1 features)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Examples.CSS.Performance

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

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

-- displays the current sum of clicks
public export
out : ElemRef Div
out = Id Div "performance_sum"

-- text fields where users can enter the number of buttons
public export
natIn : ElemRef Input
natIn = Id Input "performance_numbuttons"

public export
btnRun : ElemRef HTMLButtonElement
btnRun = Id Button "performance_run"

-- where the created buttons go
public export
buttons : ElemRef Div
buttons = Id Div "performance_buttons"

-- displays the time take to create the buttons
public export
time : ElemRef Div
time = Id Div "performance_time"

--------------------------------------------------------------------------------
--          Classes
--------------------------------------------------------------------------------

export
inc : String
inc = "performance_inc"

export
numButtonsLbl : String
numButtonsLbl = "performance_numbuttonslbl"

export
sumLbl : String
sumLbl = "performance_sumlbl"

export
grid : String
grid = "performance_grid"

export
performanceContent : String
performanceContent = "performance_content"

--------------------------------------------------------------------------------
--          Rules
--------------------------------------------------------------------------------

data Tag = LBtn | NBtn | BRun | LSum | OSum | Btns | OTme | Dot

AreaTag Tag where
  showTag LBtn  = "LBtn"
  showTag NBtn  = "NBtn"
  showTag BRun  = "BRun"
  showTag LSum  = "LSum"
  showTag Btns  = "Btns"
  showTag OSum  = "OSum"
  showTag OTme  = "OTme"
  showTag Dot   = "."

export
css : List (Rule 1)
css =
  [ Media "min-width: 300px"
      [ class performanceContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, fr 1, MaxContent]
              [ [LBtn, NBtn, BRun]
              , [LSum, OSum, OSum]
              , [OTme, OTme, OTme]
              , [Btns, Btns, Btns]
              ]
          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , Media "min-width: 800px"
      [ class performanceContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, MaxContent, MaxContent, fr 1]
              [ [LBtn, NBtn, BRun, Btns]
              , [LSum, OSum, OSum, Btns]
              , [OTme, OTme, OTme, Btns]
              , [Dot,  Dot,  Dot,  Btns]
              ]
          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , class numButtonsLbl !! [ GridArea .= LBtn ]

  , idRef natIn !!
      [ GridArea        .= NBtn
      , TextAlign       .= End
      ]

  , idRef btnRun !! [ GridArea .= BRun ]

  , class sumLbl !! [ GridArea .= LSum ]

  , idRef out  !!
      [ GridArea        .= OSum
      , FontSize        .= Large
      ]

  , idRef time  !! [ GridArea .= OTme ]

  , idRef buttons  !!
      [ GridArea        .= Btns
      , BorderStyle     .= Left Solid
      , BorderWidth     .= Left (px 2)
      , BorderColor     .= Left base80
      , Padding         .= Left (px 10)
      ]

  , class grid  !!
      [ Display         .= Flex
      , FlexWrap        .= "wrap"
      ]

  , class inc !!
      [ FlexBasis       .= perc 5
      , FontSize        .= XXSmall
      ]
  ]


text:
module DescribeList

data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
                          Empty => NonEmpty [] x
                          NonEmpty ys y => NonEmpty (x :: ys) y

describeHelper : (input : List Int) -> (form : ListLast input) -> String
describeHelper [] Empty = "Empty it is."
describeHelper (xs ++ [x]) (NonEmpty xs x) = "Empty it is not, initial: " ++ show xs

describeListEnd : List Int -> String
describeListEnd xs = describeHelper xs (listLast xs)

describeListEWith : List Int -> String
describeListEWith xs with (listLast xs)
  describeListEWith [] | Empty = "Empty it is."
  describeListEWith (ys ++ [x]) | (NonEmpty ys x) =  "Empty it is not, initial: " ++ show ys

myReverse : List a -> List a
myReverse xs with (listLast xs)
  myReverse [] | Empty = []
  myReverse (ys ++ [x]) | (NonEmpty ys x) = x :: myReverse ys


text:
module Minecraft.Data.Type.Vtbl

%default total

public export
interface Vtbl (a : Type) where
  vtable : (constraint : Type) -> Maybe constraint

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module CH06.DataStore

import Data.Vect

infixr 5 .+.

data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString   = String
SchemaType SInt      = Int
SchemaType SChar     = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

data DataStore : Type where
  MkData : (schema : Schema)
         -> (size : Nat)
         -> (items : Vect size (SchemaType schema))
         -> DataStore

data Command : Schema -> Type where
  SetSchema : (newschema : Schema)  -> Command schema
  Add  : SchemaType schema -> Command schema
  Get  : Integer -> Command schema
  Size : Command schema
  Quit : Command schema

display : SchemaType schema -> String
display {schema = SString} item             = item
display {schema = SInt} item                = show item
display {schema = SChar} item               = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SChar input                 = case unpack input of
                                            [x]              => Just (x, "")
                                            (x :: ' ' :: xs) => Just (x, ltrim $ pack xs)
                                            _                => Nothing
parsePrefix SString input               = getQuoted (unpack input)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) =
      case span (/= '"') xs of
        (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
        _                     => Nothing
    getQuoted _           = Nothing
parsePrefix SInt input                  = case span isDigit input of
                                          ("", _)     => Nothing
                                          (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) input = do
  (lval, inputl) <- parsePrefix schemal input
  (rval, inputr) <- parsePrefix schemar inputl
  pure ((lval, rval), inputr)

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input =
  case parsePrefix schema input of
    Just (res, "") => Just res
    _              => Nothing

size : DataStore -> Nat
size (MkData schema' size' items') = size'

schema : DataStore -> Schema
schema (MkData schema' size' items') = schema'

items : (store : DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData schema' size' items') = items'

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema' size' store') newitem = MkData schema' _ (addToData store')
  where
    addToData : Vect oldSize (SchemaType schema') -> Vect (S oldSize) (SchemaType schema')
    addToData []        = [newitem]
    addToData (x :: xs) = x :: addToData xs

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                           Z => Just (MkData schema _ [])
                           _ => Nothing

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) =
  case xs of
    [] => Just SString
    _  => do
      schema1 <- parseSchema xs
      Just (SString .+. schema1)
parseSchema ("Char" :: xs)   =
  case xs of
    [] => Just SChar
    _  => do
      schema1 <- parseSchema xs
      Just (SChar .+. schema1)
parseSchema ("Int" :: xs)    =
  case xs of
    [] => Just SInt
    _  => do
      schema1 <- parseSchema xs
      Just (SInt .+. schema1)
parseSchema _                = Nothing

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "schema" rest = SetSchema <$> (parseSchema (words rest))
parseCommand schema "add" val     = Add <$> (parseBySchema schema val)
parseCommand schema "get" val     = if all isDigit (unpack val)
                                    then Nothing
                                    else Just (Get (cast val))
parseCommand schema "quit" ""     = Just Quit
parseCommand schema "size" ""     = Just Size
parseCommand _ _ _                = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                       (cmd, args) => parseCommand schema cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store
                     in case integerToFin pos (size store) of
                          Nothing => Just ("Out of range\n", store)
                          Just id => Just ((display $ index id store_items) ++ "\n", store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input =
  case parse (schema store) input of
    Nothing                  => Just ("Invalid command\n", store)
    Just (SetSchema schema') => case setSchema store schema' of
                                  Nothing     => Just ("Can't update scema\n", store)
                                  Just store' => Just ("OK\n", store')
    Just (Add item)          => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
    Just (Get pos)           => getEntry pos store
    Just Size                => Just("Size " ++ show (size store) ++ "\n", store)
    Just Quit                => Nothing

main : IO ()
main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput


text:
module OddAndEvens

%access export
%default total

public export
data Even : Nat -> Type where
  -- | Zero is even.
  ZeroEven : Even Z
  -- | If n is even, then n+2 is even.
  NextEven : Even n -> Even (S (S n))

public export
data Odd : Nat -> Type where
  -- | One is odd.
  OneOdd : Odd (S Z)
  -- | If n is odd, then n+2 is odd.
  NextOdd : Odd n -> Odd (S (S n))

-- | Proves that if n is even, n+1 is odd.
-- Notice how I use the axioms here.
evenPlusOne : Even n -> Odd (S n)
evenPlusOne  ZeroEven    = OneOdd
evenPlusOne (NextEven x) = NextOdd $ evenPlusOne x

-- | Proves that if n is odd, n+1 is even.
oddPlusOne : Odd n -> Even (S n)
oddPlusOne  OneOdd     = NextEven $ ZeroEven
oddPlusOne (NextOdd x) = NextEven $ oddPlusOne x

-- | Proves even + even = even
evenPlusEven : Even n -> Even m -> Even (n + m)
evenPlusEven  ZeroEven    y = y
evenPlusEven (NextEven x) y = NextEven $ evenPlusEven x y

-- | Proves odd + odd = even
oddPlusOdd : Odd n -> Odd m -> Even (n + m)
oddPlusOdd OneOdd      y = oddPlusOne y
oddPlusOdd (NextOdd x) y = NextEven $ oddPlusOdd x y

-- | Proves even + odd = odd
evenPlusOdd : Even n -> Odd m -> Odd (n + m)
evenPlusOdd ZeroEven     y = y
evenPlusOdd (NextEven x) y = NextOdd $ evenPlusOdd x y

-- | Proves odd + even = odd
oddPlusEven : Odd n -> Even m -> Odd (n + m)
oddPlusEven OneOdd      y = evenPlusOne y
oddPlusEven (NextOdd x) y = NextOdd $ oddPlusEven x y

-- | Proves even * even = even
evenTimesEven : Even n -> Even m -> Even (n * m)
evenTimesEven ZeroEven     _ = ZeroEven
evenTimesEven (NextEven x) y = evenPlusEven y $ evenPlusEven y $ evenTimesEven x y

-- | Proves odd * odd = odd
oddTimesOdd : Odd n -> Odd m -> Odd (n * m)
oddTimesOdd OneOdd {m}  y = rewrite plusZeroRightNeutral m in y
oddTimesOdd (NextOdd x) y = oddPlusEven y $ oddPlusOdd y $ oddTimesOdd x y

-- | Proves even * odd = even
evenTimesOdd : Even n -> Odd m -> Even (n * m)
evenTimesOdd ZeroEven y = ZeroEven
evenTimesOdd (NextEven x) y = oddPlusOdd y $ oddPlusEven y $ evenTimesOdd x y

-- | Proves odd * even = even
oddTimesEven : Odd n -> Even m -> Even (n * m)
oddTimesEven OneOdd {m}  y = rewrite plusZeroRightNeutral m in y
oddTimesEven (NextOdd x) y = evenPlusEven y $ evenPlusEven y $ oddTimesEven x y