text:
module UnboundImplsWhere

import Data.Vect

xs : Nat
xs = 5

-- Having `xs` above gives us a warning as if `xs` in `x` is a parameter.
-- Turning off unbound implicits in the `where` block moves warning away, but leaves implicits to be turned off after where block.

g : Vect n a -> Nat
g xs = x $ lengthCorrect xs where

--  %unbound_implicits off

  x : length xs = n -> Nat
  x _ = 5

f : List a -> Nat


text:
module Expr

data Expr num = Val num
    | Add (Expr num) (Expr num)
    | Sub (Expr num) (Expr num)
    | Mul (Expr num) (Expr num)

Num ty => Num (Expr ty) where
    (+) = Add
    (*) = Mul
    fromInteger = Val . fromInteger

-- Ex 7.2 #1
Cast ty String => Show (Expr ty) where
    show (Val x) = cast x
    show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
    show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
    show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"

eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y

-- Ex 7.2 #2
(Neg num, Integral num, Eq num) => Eq (Expr num) where
    (==) x y = eval x == eval y

-- Ex 7.2 #3
(Neg num, Integral num) => Cast (Expr num) num where
  cast orig = eval orig

-- Ex 7.3 #1
Functor Expr where
  map func (Val x) = Val (func x)
  map func (Add x y) = Add (map func x) (map func y)
  map func (Sub x y) = Sub (map func x) (map func y)
  map func (Mul x y) = Mul (map func x) (map func y)

-- Ex 7.3 #2
data Vect : (size : Nat) -> (ty : Type) -> Type where
     Nil : Vect Z ty
     (::) : ty -> Vect size ty -> Vect (S size) ty

Eq ty => Eq (Vect n ty) where
  (==) [] [] = True
  (==) (x :: z) (y :: w) = x == y && z == w

Foldable (Vect n) where
  foldr func acc [] = acc
  foldr func acc (x :: xs) = func x (foldr func acc xs)
  foldl func acc [] = acc
  foldl func acc (x :: xs) = func (foldl func acc xs) x

ext: idr


text:
module Collections.BSTree.Map

import Collections.BSTree.Map.Quantifiers
import Collections.Util.Bnd
import Collections.Util.Erased
import Data.Nat
import Data.Nat.Order.Strict
import Decidable.Order.Strict

import public Collections.BSTree.Map.Core

------------------
-- CONSTRUCTION --
------------------

||| The empty tree.
public export
empty : {0 rel : kTy -> kTy -> Type} ->
        {auto pre : StrictPreorder kTy rel} ->
        {auto tot : StrictOrdered kTy rel} ->
        BSTree rel {pre} {tot} vTy
empty = Empty BotLTTop

||| A tree with a single element.
public export
singleton : {0 rel : kTy -> kTy -> Type} ->
            {auto pre : StrictPreorder kTy rel} ->
            {auto tot : StrictOrdered kTy rel} ->
            (k : kTy) ->
            (v : vTy) ->
            BSTree rel {pre} {tot} vTy
singleton k v = Node k v (Empty BotLTMid) (Empty MidLTTop)

---------------
-- INSERTION --
---------------

insertWith' : {0 rel : kTy -> kTy -> Type} ->
              {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              {0 mn,mx : Bnd kTy} ->
              (f : vTy -> vTy -> vTy) ->
              (k : kTy) ->
              (v : vTy) ->
              (0 bnds : (BndLT rel mn (Mid k), BndLT rel (Mid k) mx)) ->
              (t : BST pre tot vTy mn mx) ->
              BST pre tot vTy mn mx
insertWith' f x vX (lx, xu) (Empty _) = Node x vX (Empty lx) (Empty xu)
insertWith' {tot} f x vX (lx, xu) (Node y vY l r) =
  case order (Mid x) (Mid y) of
       DecLT xy   => Node y vY (insertWith' f x vX (lx, xy) l) r
       DecEQ Refl => Node x (f vX vY) l r
       DecGT yx   => Node y vY l (insertWith' f x vX (yx, xu) r)

||| Insert with a function, combining new value and old value. `insertWith f k v m` will insert
||| the pair `(k, v)` into `m` if `k` does not exist in the tree. If the key does exist, the
||| function will insert the pair `(k, f new_v old_v)`.
export
insertWith : {0 rel : kTy -> kTy -> Type} ->
             {pre : StrictPreorder kTy rel} ->
             {tot : StrictOrdered kTy rel} ->
             (f : vTy -> vTy -> vTy) ->
             (k : kTy) ->
             (v : vTy) ->
             BSTree rel {pre} {tot} vTy ->
             BSTree rel {pre} {tot} vTy
insertWith f k v t = insertWith' f k v (BotLTMid, MidLTTop) t

||| Insert a new key and value in the tree. If the key is already present in the tree, the
||| associated value is replaced with the supplied value.
export
insert : {0 rel : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy rel} ->
         {tot : StrictOrdered kTy rel} ->
         (k : kTy) ->
         (v : vTy) ->
         BSTree rel {pre} {tot} vTy ->
         BSTree rel {pre} {tot} vTy
insert = insertWith const

--------------
-- QUERYING --
--------------

||| Is the tree empty?
export
null : BSTree rel {pre} {tot} vTy -> Bool
null (Empty _) = True
null (Node _ _ _ _) = False

size' : Nat -> (t: BST {rel} pre tot vTy mn mx) -> Nat
size' n (Empty _)      = n
size' n (Node _ _ l r) = size' (S (size' n l)) r

||| The number of elements in the tree.
export
size : BSTree rel {pre} {tot} vTy -> Nat
size t = size' 0 t where

member' : {0 rel : kTy -> kTy -> Type} ->
          {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (k : kTy) ->
          (t : BST pre tot vty mn mx) ->
          Bool
member'       k (Empty _)      = False
member' {tot} k (Node x v l r) = case order @{tot} k x of
                                      DecLT _ => member' k l
                                      DecEQ _ => True
                                      DecGT _ => member' k r

||| Is the key a member of the tree?
export
member : {0 rel : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy rel} ->
         {tot : StrictOrdered kTy rel} ->
         (k : kTy) ->
         BSTree rel {pre} {tot} vTy ->
          Bool
member = member'

lookup' : {0 rel : kTy -> kTy -> Type} ->
          {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (k : kTy) ->
          (t : BST pre tot vTy mn mx) ->
          Maybe vTy
lookup'       k (Empty _)      = Nothing
lookup' {tot} k (Node x v l r) = case order @{tot} k x of
                                      DecLT _ => lookup' k l
                                      DecEQ _ => Just v
                                      DecGT _ => lookup' k r

||| Lookup the value at a key in the tree.
export
lookup : {0 rel : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy rel} ->
         {tot : StrictOrdered kTy rel} ->
         (k : kTy) ->
         BSTree rel {pre} {tot} vTy ->
         Maybe vTy
lookup = lookup' where

lookupOr' : {0 rel : kTy -> kTy -> Type} ->
            {pre : StrictPreorder kTy rel} ->
            {tot : StrictOrdered kTy rel} ->
            (def : vTy) ->
            (k : kTy) ->
            (t : BST pre tot vTy mn mx) ->
            vTy
lookupOr'       def k (Empty _)      = def
lookupOr' {tot} def k (Node x v l r) = case order @{tot} k x of
                                            DecLT _ => lookupOr' def k l
                                            DecEQ _ => v
                                            DecGT _ => lookupOr' def k r

||| Returns the value at key `k` or returns default value `def` when the key is not in the tree.
export
lookupOr : {0 rel : kTy -> kTy -> Type} ->
           {pre : StrictPreorder kTy rel} ->
           {tot : StrictOrdered kTy rel} ->
           (def : vTy) ->
           (k : kTy) ->
           BSTree rel {pre} {tot} vTy ->
           vTy
lookupOr = lookupOr'

-----------------------
-- DELETION / UPDATE --
-----------------------

||| Deletes the leftmost element of a tree, returning the key/value of the deleted element,
||| the ordering proof of the key w.r.t. `mn`, and the updated tree.
deleteLeftmost : {0 rel : kTy -> kTy -> Type} ->
                 {pre : StrictPreorder kTy rel} ->
                 {tot : StrictOrdered kTy rel} ->
                 (t : BST pre tot vTy mn mx) ->
                 (prf : NonEmpty t) ->
                 (kv : (kTy, vTy) ** (Erased (BndLT rel mn (Mid (fst kv))),
                                     BST pre tot vTy (Mid (fst kv)) mx))
deleteLeftmost (Node k v (Empty mnk)     (Empty kmx)    ) IsNode =
  ((k, v) ** (MkErased mnk, Empty kmx))
deleteLeftmost (Node k v (Empty mnk)     r@(Node _ _ _ _)) IsNode =
  ((k, v) ** (MkErased mnk, r))
deleteLeftmost (Node k v l@(Node _ _ _ _) r               ) IsNode =
  let ((k', v') ** (mnk, l')) = deleteLeftmost l IsNode in
      ((k', v') ** (mnk, Node k v l' r))

delete' : {0 rel : kTy -> kTy -> Type} ->
          {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (k : kTy) ->
          (t : BST pre tot vTy mn mx) ->
          BST pre tot vTy mn mx
delete' x t@(Empty _) = t
delete' {pre} {tot} x (Node {mn} {mx} k v l r) =
  case order {spo=BndLT rel} (Mid x) (Mid k) of
       DecLT _    => Node k v (delete' x l) r
       DecEQ Refl =>
         case (l, r) of
              (Empty mnx,   Empty xmx      ) =>
                Empty $ transitive {rel=BndLT rel} {x=mn} {y=Mid x} {z=mx} mnx xmx
              (Empty mnx,   Node _ _ _ _     ) => extendMin mnx r
              (Node _ _ _ _, Empty xmx       ) => extendMax xmx l
              (Node _ _ _ _, r@(Node _ _ _ _)) =>
                let ((k', v') ** (MkErased xk, r')) = deleteLeftmost r IsNode in
                    Node k' v' (extendMax xk l) r'
       DecGT _    => Node k v l (delete' x r)

||| Delete a key and its value from the tree. When the key is not a member of the tree, the
||| original tree is returned.
export
delete : {0 rel : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy rel} ->
         {tot : StrictOrdered kTy rel} ->
         (k : kTy) ->
         BSTree rel {pre} {tot} vTy ->
         BSTree rel {pre} {tot} vTy
delete = delete'

adjust' : {0 rel : kTy -> kTy -> Type} ->
          {pre : StrictPreorder kTy rel} ->
          {tot : StrictOrdered kTy rel} ->
          (f : vTy -> vTy) ->
          (k : kTy) ->
          BST pre tot vTy mn mx ->
          BST pre tot vTy mn mx
adjust'       f x t@(Empty _) = t
adjust' {tot} f x (Node k v l r) = case order @{tot} x k of
                                        DecLT _    => Node k v (adjust' f x l) r
                                        DecEQ Refl => Node k (f v) l r
                                        DecGT _    => Node k v l (adjust' f x r)

||| Update a value at a specific key with the result of the provided function. When the key is not
||| a member of the tree, the original tree is returned.
export
adjust : {0 rel : kTy -> kTy -> Type} ->
         {pre : StrictPreorder kTy rel} ->
         {tot : StrictOrdered kTy rel} ->
         (f : vTy -> vTy) ->
         (k : kTy) ->
         BSTree rel {pre} {tot} vTy ->
         BSTree rel {pre} {tot} vTy
adjust = adjust'

-----------
-- TESTS --
-----------

empty_isNull : null (empty {rel=LT} {vTy=Bool}) = True
empty_isNull = Refl

singleton_notNull : null (singleton {rel=LT} 2 False) = False
singleton_notNull = Refl

singleton_equivToInsertEmpty : singleton 5 'a' = insert 5 'a' (empty {rel=LT})
singleton_equivToInsertEmpty = Refl

member_missingKeyLeft_returnsFalse : member 1 (singleton {rel=LT} 2 'a') = False
member_missingKeyLeft_returnsFalse = Refl

member_missingKeyRight_returnsFalse : member 3 (singleton {rel=LT} 2 'a') = False
member_missingKeyRight_returnsFalse = Refl

member_keyInRoot_returnsTrue : member 2 (singleton {rel=LT} 2 'a') = True
member_keyInRoot_returnsTrue = Refl

member_keyInRight_returnsTrue : member 5 (insert 5 True (singleton {rel=LT} 2 False)) = True
member_keyInRight_returnsTrue = Refl

member_keyInLeft_returnsTrue : member 1 (insert 1 True (singleton {rel=LT} 2 False)) = True
member_keyInLeft_returnsTrue = Refl

lookup_keyExists_returnsJust : lookup 2 (insert 5 'b' (singleton {rel=LT} 2 'a')) = Just 'a'
lookup_keyExists_returnsJust = Refl

lookup_keyMissing_returnsNothing : lookup 9 (insert 5 'b' (singleton {rel=LT} 2 'a')) = Nothing
lookup_keyMissing_returnsNothing = Refl

lookupOr_keyExists_returnsValue : lookupOr 'c' 2 (insert 5 'a' (singleton {rel=LT} 2 'b')) = 'b'
lookupOr_keyExists_returnsValue = Refl

lookupOr_keyMissing_returnsDefault : lookupOr 'c' 9 (insert 5 'a' (singleton {rel=LT} 2 'b')) = 'c'
lookupOr_keyMissing_returnsDefault = Refl

delete_keyMissing_treeUnchanged : delete 1 (singleton {rel=LT} 2 'a') = singleton {rel=LT} 2 'a'
delete_keyMissing_treeUnchanged = Refl

delete_keyExists_removesKey : delete 2 (insert 1 'a' (singleton {rel=LT} 2 'b')) = singleton {rel=LT} 1 'a'
delete_keyExists_removesKey = Refl

adjust_keyMissing_treeUnchanged : adjust (\_ => 'b') 1 (singleton {rel=LT} 2 'a') = singleton {rel=LT} 2 'a'
adjust_keyMissing_treeUnchanged = Refl

adjust_keyExists_treeUpdated : adjust (\_ => 'c') 2 (insert 1 'a' (singleton {rel=LT} 2 'b')) =
                                insert 1 'a' (singleton {rel=LT} 2 'c')
adjust_keyExists_treeUpdated = Refl

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
maybeAdd: Num a => Maybe a -> Maybe a -> Maybe a
maybeAdd x y = do
  xVal <- x
  yVal <- y
  Just (xVal + yVal)

occurrences: Eq ty => (item: ty) -> (values: List ty) -> Nat
occurrences item [] = 0
occurrences item (value :: values) =
  case value == item of
    False => occurrences item values
    True  => 1 + occurrences item values

data Matter = Solid | Liquid | Gas

Eq Matter where
  (==) Solid  Solid   = True
  (==) Liquid Liquid  = True
  (==) Gas    Gas     = True
  (==) _      _       = False

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

Eq elem => Eq (Tree elem) where
  (==) Empty Empty = True
  (==) (Node left e right) (Node left' e' right') =
    left == left' && e == e' && right == right'
  (==) _ _ = False

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

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

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

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

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

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

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

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

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

Show Album where
  show (MkAlbum artist title year) =
    title ++ " by " ++ artist ++ " (released " ++ show year ++ ")"

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

Eq Shape where
  (==) (Triangle x z) (Triangle x' z') = x == x' && z == z'
  (==) (Rectangle x z) (Rectangle x' z') = x == x' && z == z'
  (==) (Circle x) (Circle x') = x == x'
  (==) _ _ = False

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

Ord Shape where
  compare x y = let
    xArea = area x
    yArea = area y
  in
    compare xArea yArea

testShapes: List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
-- This test ensures that implicits bound on the RHS of a
-- record update field are correctly bound by the compiler.

record Rec where
    n : Nat

data T : Rec -> Type where
    C : T ({ n := Z } r)

data U : Rec -> Type where
    D : U ({ n $= S } r)


text:
data BSTree elem = Empty
                 | Node (BSTree elem) elem (BSTree elem)

Eq elem => Eq (BSTree elem) where
  (==) Empty Empty = True
  (==) (Node left e right) (Node left' e' right') =
    left == left' && e == e' && right == right'
  (==) _ _ = False

Functor BSTree where
  map func Empty = Empty
  map func (Node left e right) = Node(map func left) (func e) (map func right)

Foldable BSTree where
  foldr func acc Empty = acc
  foldr func acc (Node left e right) =
    let
      leftFold = foldr func acc left
      rightFold = foldr func leftFold right
    in
      func e rightFold


text:
> module LocalEffect.StdIO

> import Effects
> import Effect.StdIO
> import Effect.Exception

> import LocalEffect.Exception
> import BoundedNat.BoundedNat
> import Sigma.Sigma
> import Pairs.Operations

> -- %default total

> %access public export

> |||
> -- %assert_total -- termination not required
> getNat : { [STDIO] } Eff Nat
> getNat =
>   do putStr (" Nat: " )
>      case the (Either String Nat) (run (parseNat (trim !getStr))) of
>           Left err => do putStr (err ++ "\n")
>                          getNat
>           Right n  => do putStr "thanks!\n"
>                          pure n

> |||
> -- %assert_total -- termination not required
> getLTB : (b : Nat) -> { [STDIO] } Eff (LTB b)
> getLTB b =
>   do putStr (" Nat, < " ++ cast {from = Int} (cast b) ++ ": " )
>      case the (Either String (LTB b)) (run (parseLTB b (trim !getStr))) of
>           Left err => do putStr (err ++ "\n")
>                          getLTB b
>           Right n  => do putStr "thanks!\n"
>                          pure n

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- ------------------------------------------------------------------------ [  ]
-- Example innvocations of greeters
-- --------------------------------------------------------------------- [ EOH ]
module Greeter.Example

import Effects
import Effect.StdIO
import Effect.Default
import Effect.State
import Effect.Msg

import System.Protocol

import RFC.Greeter
import Greeter.Common
import Greeter.Frontend
import Greeter.Backend

%access public
-- ------------------------------------------------------------------------- [  ]

||| A Greeter Backend.
covering
exampleGreeterBackend : PID -> GreeterBackend (greeter gBody) ()
exampleGreeterBackend proc = greeterBackend proc (backendBody')

||| Run the Greeter Application.
|||
||| @max The max number of greets to be given.
doGreeterProcess : (max : Int) -> IO ()
doGreeterProcess max = runConc [(),0] (doGreet' max)
  where
    doGreet' : Int -> GreeterFrontend (greeter gBody) ()
    doGreet' max = do
      server <- spawn (exampleGreeterBackend) [(), max]
      greeterClient server

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Toml.Lexer

import Text.Lexer
import Text.Token

import public Toml.Tokens

%default total

stringLitSingle : Lexer
stringLitSingle = quote (is '\'') any

||| Recognise one or more characters that can comprise a keyword
||| /[A-Za-z0-9-_]+/
export
keyword : Lexer
keyword = some (pred (\x => isAlphaNum x || x == '-' || x == '_'))

tomlTokenMap : TokenMap TomlToken
tomlTokenMap = toTokenMap $
  [ (stringLit, StringLit)
  , (stringLitSingle, StringLit)
  , (digits, Number)
  , (keyword, Keyword)
  , (is '.', Dot)
  , (is '=', Equals)
  , (is '[', LeftBracket)
  , (is ']', RightBracket)
  , (is ',', Comma)
  , (is '#' <+> manyUntil newline any, Comment)
  , (spaces, Whitespace)
  ]

public export
lexToml : String -> Maybe (List $ WithBounds TomlToken)
lexToml str
  = case lex tomlTokenMap str of
         (tokens, _, _, "") => Just $ tokens
         _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

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)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

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 _ [])
                              S k => Nothing

data Command : Schema -> Type where
     SetSchema : Schema -> Command schema
     Add : SchemaType schema -> Command schema
     Get : Integer -> Command schema
     All : Command schema
     Quit : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
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 SChar input = case unpack input of
                           [] => Nothing
                           (char :: rest) => Just (char, ltrim (pack rest))
parsePrefix SInt input = case span isDigit input of
                              ("", rest) => Nothing
                              (num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) input = do
          (l_val, input') <- parsePrefix schemal input
          (r_val, input'') <- parsePrefix schemar input'
          pure ((l_val, r_val), input'')

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

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

parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" rest = case parseBySchema schema rest of
                                      Nothing => Nothing
                                      Just restok => Just (Add restok)
parseCommand schema "get" "" = Just All
parseCommand schema "get" val = case all isDigit (unpack val) of
                                    False => Nothing
                                    True => Just (Get (cast val))
parseCommand schema "quit" "" = Just Quit
parseCommand schema "schema" rest
    = case parseSchema (words rest) of
           Nothing => Nothing
           Just schemaok => Just (SetSchema schemaok)
parseCommand _ _ _ = Nothing

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

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

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 (items store)) ++ "\n", store)

getAllEntries : (store : DataStore) -> Maybe (String, DataStore)
getAllEntries store = Just (getEntries 0 (items store), store)
    where getEntries : Integer -> Vect n (SchemaType schema) -> String
          getEntries _ [] = ""
          getEntries index (entry :: rest) = (show index) ++ ": " ++
                        (display entry) ++ "\n" ++ getEntries (index + 1) rest

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

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


text:
||| Properties of the reverse function.
module Data.List.Reverse

import Data.Nat
import Data.List
import Data.List.Equalities

%default total

export
reverseOntoAcc : (xs, ys, zs : List a) ->
  reverseOnto (ys ++ zs) xs = (reverseOnto ys xs) ++ zs
reverseOntoAcc [] _ _ = Refl
reverseOntoAcc (x :: xs) (ys) (zs) = reverseOntoAcc xs (x :: ys) zs

||| Serves as a specification for reverseOnto.
export
reverseOntoSpec : (xs, ys : List a) -> reverseOnto xs ys = reverse ys ++ xs
reverseOntoSpec xs ys = reverseOntoAcc ys [] xs

||| The reverse of an empty list is an empty list.  Together with reverseCons,
||| serves as a specification for reverse.
export
reverseNil : reverse [] = []
reverseNil = Refl

||| The reverse of a cons is the reverse of the tail followed by the head.
||| Together with reverseNil serves as a specification for reverse.
export
reverseCons : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs `snoc` x
reverseCons x xs = reverseOntoSpec [x] xs

||| Reversing an append is appending reversals backwards.
export
reverseAppend : (xs, ys : List a) ->
  reverse (xs ++ ys) = reverse ys ++ reverse xs
reverseAppend [] ys = sym (appendNilRightNeutral (reverse ys))
reverseAppend (x :: xs) ys =
  rewrite reverseCons x (xs ++ ys) in
    rewrite reverseAppend xs ys in
      rewrite reverseCons x xs in
        sym $ appendAssociative (reverse ys) (reverse xs) [x]

||| A slow recursive definition of reverse.
public export
0 slowReverse : List a -> List a
slowReverse [] = []
slowReverse (x :: xs) = slowReverse xs `snoc` x

||| The iterative and recursive defintions of reverse are the same.
export
reverseEquiv : (xs : List a) -> slowReverse xs = reverse xs
reverseEquiv [] = Refl
reverseEquiv (x :: xs) =
  rewrite reverseEquiv xs in
    rewrite reverseAppend [x] xs in
      Refl

||| Reversing a singleton list is a no-op.
export
reverseSingletonId : (x : a) -> reverse [x] = [x]
reverseSingletonId _ = Refl

||| Reversing a reverse gives the original.
export
reverseReverseId : (xs : List a) -> reverse (reverse xs) = xs
reverseReverseId [] = Refl
reverseReverseId (x :: xs) =
  rewrite reverseCons x xs in
    rewrite reverseAppend (reverse xs) [x] in
      rewrite reverseReverseId xs in
        Refl

||| Reversing onto preserves list length.
export
reverseOntoLength : (xs, acc : List a) ->
  length (reverseOnto acc xs) = length acc + length xs
reverseOntoLength [] acc = rewrite plusZeroRightNeutral (length acc) in Refl
reverseOntoLength (x :: xs) acc =
  rewrite reverseOntoLength xs (x :: acc) in
    plusSuccRightSucc (length acc) (length xs)

||| Reversing preserves list length.
export
reverseLength : (xs : List a) -> length (reverse xs) = length xs
reverseLength xs = reverseOntoLength xs []

||| Equal reversed lists are equal.
export
reverseEqual : (xs, ys : List a) -> reverse xs = reverse ys -> xs = ys
reverseEqual xs ys prf =
  rewrite sym $ reverseReverseId xs in
    rewrite prf in
      reverseReverseId ys


text:
import Syntax.PreorderReasoning

-------- some notation ----------
infixr 6 .+.,:+:
infixr 7 .*.,:*:

interface Additive a where
  constructor MkAdditive
  (.+.) : a -> a -> a
  O   : a

interface Additive2 a where
  constructor MkAdditive2
  (:+:) : a -> a -> a
  O2   : a

interface Multiplicative a where
  constructor MkMultiplicative
  (.*.) : a -> a -> a
  I     : a

record MonoidOver U where
  constructor WithStruct
  Unit    : U
  Mult    : U -> U -> U
  lftUnit : (x : U) -> Unit `Mult` x    = x
  rgtUnit : (x : U) -> x    `Mult` Unit = x
  assoc   : (x,y,z : U)
                    -> x `Mult` (y `Mult` z) = (x `Mult` y) `Mult` z

record Monoid where
  constructor MkMonoid
  U : Type
  Struct : MonoidOver U

AdditiveStruct : (m : MonoidOver a) -> Additive a
AdditiveStruct m = MkAdditive (Mult $ m)
                              (Unit $ m)
AdditiveStruct2 : (m : MonoidOver a) -> Additive2 a
AdditiveStruct2 m = MkAdditive2 (Mult $ m)
                                (Unit $ m)
AdditiveStructs : (ma : MonoidOver a) -> (mb : MonoidOver b)
              -> (Additive a, Additive2 b)
AdditiveStructs ma mb = (AdditiveStruct ma, AdditiveStruct2 mb)

getAdditive : (m : Monoid) -> Additive (U m)
getAdditive m = AdditiveStruct (Struct m)

MultiplicativeStruct : (m : Monoid) -> Multiplicative (U m)
MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m)
                                          (Unit $ Struct m)
-----------------------------------------------------

0 Commutative : MonoidOver a -> Type
Commutative m = (x,y : a) -> let _ = AdditiveStruct m in
                x .+. y = y .+. x

0 Commute : (Additive a, Additive2 a) => Type
Commute =
          (x11,x12,x21,x22 : a) ->
          ((x11 :+: x12) .+. (x21 :+: x22))
          =
          ((x11 .+. x21) :+: (x12 .+. x22))

product : (ma, mb : Monoid) -> Monoid
product ma mb =
  let
      %hint aStruct : Additive (U ma)
      aStruct = getAdditive ma
      %hint bStruct : Additive (U mb)
      bStruct = getAdditive mb

  in MkMonoid (U ma, U mb) $ WithStruct
     (O, O)
     (\(x1,y1), (x2, y2)  => (x1 .+. x2, y1 .+. y2))
     (\(x,y) => rewrite lftUnit (Struct ma) x in
                rewrite lftUnit (Struct mb) y in
                Refl)
     (\(x,y) => rewrite rgtUnit (Struct ma) x in
                rewrite rgtUnit (Struct mb) y in
                Refl)
     (\(x1,y1),(x2,y2),(x3,y3) =>
                rewrite assoc (Struct ma) x1 x2 x3 in
                rewrite assoc (Struct mb) y1 y2 y3 in
                Refl)

EckmannHilton : forall a . (ma,mb : MonoidOver a)
             -> let ops = AdditiveStructs ma mb in
                Commute @{ops}
             -> (Commutative ma, (x,y : a) -> x .+. y = x :+: y)
EckmannHilton ma mb prf =
  let %hint first : Additive a
      first = AdditiveStruct ma
      %hint second : Additive2 a
      second = AdditiveStruct2 mb in
  let SameUnits : (the a O === O2)
      SameUnits = Calc $
        |~ O
        ~~  O         .+.         O  ...(sym $ lftUnit ma O)
        ~~ (O :+: O2) .+. (O2 :+: O) ...(sym $ cong2 (.+.)
                                             (rgtUnit mb O)
                                             (lftUnit mb O))
        ~~ (O .+. O2) :+: (O2 .+. O) ...(prf O O2 O2 O)
        ~~        O2  :+:  O2        ...(cong2 (:+:)
                                             (lftUnit ma O2)
                                             (rgtUnit ma O2))
        ~~ O2                        ...(lftUnit mb O2)

      SameMults : (x,y : a) -> (x .+. y) === (x :+: y)
      SameMults x y = Calc $
        |~ x .+. y
        ~~ (x :+: O2) .+. (O2 :+: y) ...(sym $ cong2 (.+.)
                                             (rgtUnit mb x)
                                             (lftUnit mb y))
        ~~ (x .+. O2) :+: (O2 .+. y) ...(prf x O2 O2 y)
        ~~ (x .+. O ) :+: (O  .+. y) ...(cong (\u =>
                                              (x .+. u) :+: (u .+. y))
                                              (sym SameUnits))
        ~~ x :+: y                   ...(cong2 (:+:)
                                              (rgtUnit ma x)
                                              (lftUnit ma y))

      Commutativity : Commutative ma
      Commutativity x y = Calc $
        |~ x .+. y
        ~~ (O2 :+: x) .+. (y :+: O2) ...(sym $ cong2 (.+.)
                                             (lftUnit mb x)
                                             (rgtUnit mb y))
        ~~ (O2 .+. y) :+: (x .+. O2) ...(prf O2 x y O2)
        ~~ (O  .+. y) :+: (x .+. O ) ...(cong (\u =>
                                              (u .+. y) :+: (x .+. u))
                                              (sym SameUnits))
        ~~ y :+: x                   ...(cong2 (:+:)
                                              (lftUnit ma y)
                                              (rgtUnit ma x))
        ~~ y .+. x                   ...(sym $ SameMults y x)
  in (Commutativity, SameMults)