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

import Data.DList
import GRL.Lang.GLang

-- -------------------------------------------------------------- [ Meta Types ]

data Ty = PAPERty | ITEMty | COMPty

data CTy = STy | ATy | BTy

-- ------------------------------------------------------------- [ Interpreter ]

data InterpRes : Ty -> Type where
  ResComp  : GLang ELEM                 -> InterpRes COMPty
  ResPaper : GModel                     -> InterpRes PAPERty
  ResITEM  : GLang ELEM -> GLang INTENT -> InterpRes ITEMty

interpComp : String -> InterpRes COMPty
interpComp t = ResComp $ mkGoal t

interpPaper : String
           -> InterpRes COMPty
           -> InterpRes COMPty
           -> List (InterpRes COMPty)
           -> InterpRes PAPERty
interpPaper s (ResComp a) (ResComp b) es =
    ResPaper $ insert (pelem &= es') m
  where
    pelem : GLang ELEM
    pelem = mkGoal s

    es' : List (GLang ELEM)
    es' = map (\(ResComp e) => e) es

    m : GModel
    m = insertMany (pelem::a::b::es') emptyModel

interpTODO : String
          -> SValue
          -> InterpRes COMPty
          -> InterpRes ITEMty
interpTODO d s (ResComp a) = ResITEM rtask (rtask ==> a | MAKES)
  where
    rtask : GLang ELEM
    rtask = mkSatTask (d ++ getElemTitle a) s

interpTODOS : InterpRes PAPERty
           -> List (InterpRes ITEMty)
           -> GModel
interpTODOS (ResPaper m) es' = insertMany is $ insertMany es m
  where
    is : List (GLang INTENT)
    is = map (\(ResITEM _ i) => i) es'

    es : List (GLang ELEM)
    es = map (\(ResITEM e _) => e) es'

-- ------------------------------------------------------------- [ Definitions ]

data Comp : InterpRes COMPty -> CTy -> Type where
  Sect : (t:String) -> Comp (interpComp t         ) STy
  Abst :               Comp (interpComp "Abstract") ATy
  Bibl :               Comp (interpComp "Biblio"  ) BTy

data Paper : InterpRes PAPERty -> Type where
  MkPaper : (t : String)
         -> Comp a ATy
         -> Comp b BTy
         -> DList (InterpRes COMPty) (\x => Comp x STy) ss
         -> Paper (interpPaper t a b ss)

data TODO : InterpRes ITEMty -> Type where
  Review : (c : Comp a ty)
        -> (s : SValue)
        -> TODO (interpTODO "Review " s a)

  Write  : (c : Comp a ty)
        -> (s : SValue)
        -> TODO (interpTODO "Writing "s a)

data TODOList : GModel -> Type where
  MyList : String
        -> Paper m
        -> DList (InterpRes ITEMty) TODO ts
        -> TODOList (interpTODOS m ts)

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
foo : Int -> Int
foo x = x

bar : Int -> Int
bar x = let y = 42

baz : Int -> Int
baz x = x

ext: idr


text:
{-
[(0, 1), (1, 0), (1, 1), (2, 2)]
-}
module Main

import Data.SortedSet

%hide merge

Cell : Type
Cell = (Int, Int)

Nil : Ord k => SortedSet k
Nil = SortedSet.empty

(::) : Ord k => k -> SortedSet k -> SortedSet k
(::) = insert

Cells : Type
Cells = SortedSet Cell

instance Show Cells where
  show = show . SortedSet.toList

merge : Cells -> Cells -> Cells
merge xs ys = foldl (flip insert) xs ys

main : IO ()
main = printLn $ [(0, 1), (1, 0), (2, 2)] `merge` [(1, 0), (0, 1), (1, 1)]

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
import Package.IkanAst
import Package.IpkgAst
import Control.Monad.Freer
import Debug.Trace
import Control.Monad.Id
import Data.Fin
import Control.Monad.State

build:IkanDataT
build = do
  AddDependencies [""]
  AddSourcepaths [""]

max_stars_repo_name: marcesquerra/ikan

max_issues_repo_name: marcesquerra/ikan

max_forks_repo_name: marcesquerra/ikan


text:
module Data.String

import Data.List
import Data.List1

%default total

export
singleton : Char -> String
singleton c = strCons c ""

||| Create a string by using n copies of a character
export
replicate : Nat -> Char -> String
replicate n c = pack (replicate n c)

||| Indent a given string by `n` spaces.
public export
indent : (n : Nat) -> String -> String
indent n x = replicate n ' ' ++ x

||| Pad a string on the left
export
padLeft : Nat -> Char -> String -> String
padLeft n c str = replicate (minus n (String.length str)) c ++ str

||| Pad a string on the right
export
padRight : Nat -> Char -> String -> String
padRight n c str = str ++ replicate (minus n (String.length str)) c

partial
foldr1 : (a -> a -> a) -> List a -> a
foldr1 _ [x] = x
foldr1 f (x::xs) = f x (foldr1 f xs)

partial
foldl1 : (a -> a -> a) -> List a -> a
foldl1 f (x::xs) = foldl f x xs

-- This uses fastConcat internally so it won't compute at compile time.
export
fastUnlines : List String -> String
fastUnlines = fastConcat . unlines'
  where unlines' : List String -> List String
        unlines' [] = []
        unlines' (x :: xs) = x :: "\n" :: unlines' xs

-- This is a deprecated alias for fastConcat for backwards compatibility
-- (unfortunately, we don't have %deprecated yet).
export
fastAppend : List String -> String
fastAppend = fastConcat

||| Splits a character list into a list of whitespace separated character lists.
|||
||| ```idris example
||| words' (unpack " A B C  D E   ")
||| ```
covering
words' : List Char -> List (List Char)
words' s = case dropWhile isSpace s of
            [] => []
            s' => let (w, s'') = break isSpace s'
                  in w :: words' s''

||| Splits a string into a list of whitespace separated strings.
|||
||| ```idris example
||| words " A B C  D E   "
||| ```
export
covering
words : String -> List String
words s = map pack (words' (unpack s))

||| Joins the character lists by spaces into a single character list.
|||
||| ```idris example
||| unwords' [['A'], ['B', 'C'], ['D'], ['E']]
||| ```
unwords' : List (List Char) -> List Char
unwords' [] = []
unwords' ws = assert_total (foldr1 addSpace ws) where
  addSpace : List Char -> List Char -> List Char
  addSpace w s = w ++ (' ' :: s)

||| Joins the strings by spaces into a single string.
|||
||| ```idris example
||| unwords ["A", "BC", "D", "E"]
||| ```
export
unwords : List String -> String
unwords = pack . unwords' . map unpack

||| Splits a character list into a list of newline separated character lists.
|||
||| ```idris example
||| lines' (unpack "\rA BC\nD\r\nE\n")
||| ```
export
lines' : List Char -> List (List Char)
lines' s = linesHelp [] s
  where linesHelp : List Char -> List Char -> List (List Char)
        linesHelp [] [] = []
        linesHelp acc [] = [reverse acc]
        linesHelp acc ('\n' :: xs) = reverse acc :: linesHelp [] xs
        linesHelp acc ('\r' :: '\n' :: xs) = reverse acc :: linesHelp [] xs
        linesHelp acc ('\r' :: xs) = reverse acc :: linesHelp [] xs
        linesHelp acc (c :: xs) = linesHelp (c :: acc) xs

||| Splits a string into a list of newline separated strings.
|||
||| ```idris example
||| lines  "\rA BC\nD\r\nE\n"
||| ```
export
lines : String -> List String
lines s = map pack (lines' (unpack s))

||| Joins the character lists by a single character list by appending a newline
||| to each line.
|||
||| ```idris example
||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
||| ```
export
unlines' : List (List Char) -> List Char
unlines' [] = []
unlines' (l::ls) = l ++ '\n' :: unlines' ls

||| Joins the strings into a single string by appending a newline to each string.
|||
||| ```idris example
||| unlines ["line", "line2", "ln3", "D"]
||| ```
export
unlines : List String -> String
unlines = pack . unlines' . map unpack

%transform "fastUnlines" unlines = fastUnlines

||| A view checking whether a string is empty
||| and, if not, returning its head and tail
public export
data StrM : String -> Type where
    StrNil : StrM ""
    StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

||| To each string we can associate its StrM view
public export
strM : (x : String) -> StrM x
strM "" = StrNil
strM x
  -- Using primitives, so `assert_total` and `believe_me` needed
    = assert_total $ believe_me $
        StrCons (prim__strHead x) (prim__strTail x)

||| A view of a string as a lazy linked list of characters
public export
data AsList : String -> Type where
  Nil  : AsList ""
  (::) : (c : Char) -> {str : String} -> Lazy (AsList str) -> AsList (strCons c str)

||| To each string we can associate the lazy linked list of characters
||| it corresponds to once unpacked.
public export
asList : (str : String) -> AsList str
asList str with (strM str)
  asList "" | StrNil = []
  asList str@(strCons x xs) | StrCons _ _ = x :: asList (assert_smaller str xs)

||| Trim whitespace on the left of the string
export
ltrim : String -> String
ltrim str with (asList str)
  ltrim ""  | [] = ""
  ltrim str@_ | x :: xs = if isSpace x then ltrim _ | xs else str

||| Trim whitespace on both sides of the string
export
trim : String -> String
trim = ltrim . reverse . ltrim . reverse

||| Splits the string into a part before the predicate
||| returns False and the rest of the string.
|||
||| ```idris example
||| span (/= 'C') "ABCD"
||| ```
||| ```idris example
||| span (/= 'C') "EFGH"
||| ```
export
span : (Char -> Bool) -> String -> (String, String)
span p xs
    = case span p (unpack xs) of
           (x, y) => (pack x, pack y)

||| Splits the string into a part before the predicate
||| returns True and the rest of the string.
|||
||| ```idris example
||| break (== 'C') "ABCD"
||| ```
||| ```idris example
||| break (== 'C') "EFGH"
||| ```
public export
break : (Char -> Bool) -> String -> (String, String)
break p = span (not . p)

||| Splits the string into parts with the predicate
||| indicating separator characters.
|||
||| ```idris example
||| split (== '.') ".AB.C..D"
||| ```
public export
split : (Char -> Bool) -> String -> List1 String
split p xs = map pack (split p (unpack xs))

export
stringToNatOrZ : String -> Nat
stringToNatOrZ = fromInteger . prim__cast_StringInteger

export
toUpper : String -> String
toUpper str = pack (map toUpper (unpack str))

export
toLower : String -> String
toLower str = pack (map toLower (unpack str))

export partial
strIndex : String -> Int -> Char
strIndex = prim__strIndex

export partial
strLength : String -> Int
strLength = prim__strLength

export partial
strSubstr : Int -> Int -> String -> String
strSubstr = prim__strSubstr

export partial
strTail : String -> String
strTail = prim__strTail

export
isPrefixOf : String -> String -> Bool
isPrefixOf a b = isPrefixOf (unpack a) (unpack b)

export
isSuffixOf : String -> String -> Bool
isSuffixOf a b = isSuffixOf (unpack a) (unpack b)

export
isInfixOf : String -> String -> Bool
isInfixOf a b = isInfixOf (unpack a) (unpack b)

parseNumWithoutSign : List Char -> Integer -> Maybe Integer
parseNumWithoutSign []        acc = Just acc
parseNumWithoutSign (c :: cs) acc =
  if (c >= '0' && c <= '9')
  then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
  else Nothing

||| Convert a positive number string to a Num.
|||
||| ```idris example
||| parsePositive "123"
||| ```
||| ```idris example
||| parsePositive {a=Int} " +123"
||| ```
public export
parsePositive : Num a => String -> Maybe a
parsePositive s = parsePosTrimmed (trim s)
  where
    parsePosTrimmed : String -> Maybe a
    parsePosTrimmed s with (strM s)
      parsePosTrimmed ""             | StrNil         = Nothing
      parsePosTrimmed (strCons '+' xs) | (StrCons '+' xs) =
        map fromInteger (parseNumWithoutSign (unpack xs) 0)
      parsePosTrimmed (strCons x xs) | (StrCons x xs) =
        if (x >= '0' && x <= '9')
        then  map fromInteger (parseNumWithoutSign (unpack xs)  (cast (ord x - ord '0')))
        else Nothing

||| Convert a number string to a Num.
|||
||| ```idris example
||| parseInteger " 123"
||| ```
||| ```idris example
||| parseInteger {a=Int} " -123"
||| ```
public export
parseInteger : (Num a, Neg a) => String -> Maybe a
parseInteger s = parseIntTrimmed (trim s)
  where
    parseIntTrimmed : String -> Maybe a
    parseIntTrimmed s with (strM s)
      parseIntTrimmed ""             | StrNil         = Nothing
      parseIntTrimmed (strCons x xs) | (StrCons x xs) =
        if (x == '-')
          then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
          else if (x == '+')
            then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
            else if (x >= '0' && x <= '9')
            then map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
              else Nothing

||| Convert a number string to a Double.
|||
||| ```idris example
||| parseDouble "+123.123e-2"
||| ```
||| ```idris example
||| parseDouble {a=Int} " -123.123E+2"
||| ```
||| ```idris example
||| parseDouble {a=Int} " +123.123"
||| ```
export -- it's a bit too slow at compile time
covering
parseDouble : String -> Maybe Double
parseDouble = mkDouble . wfe . trim
  where
    intPow : Integer -> Integer -> Double
    intPow base exp = assert_total $ if exp > 0 then (num base exp) else 1 / (num base exp)
      where
        num : Integer -> Integer -> Double
        num base 0 = 1
        num base e = if e < 0
                     then cast base * num base (e + 1)
                     else cast base * num base (e - 1)

    natpow : Double -> Nat -> Double
    natpow x Z = 1
    natpow x (S n) = x * (natpow x n)

    mkDouble : Maybe (Double, Double, Integer) -> Maybe Double
    mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
                                Just $ (w * ex + f * ex)
    mkDouble Nothing = Nothing

    wfe : String -> Maybe (Double, Double, Integer)
    wfe cs = case split (== '.') cs of
               (wholeAndExp ::: []) =>
                 case split (\c => c == 'e' || c == 'E') wholeAndExp of
                   (whole:::exp::[]) =>
                     do
                       w <- cast {from=Integer} <$> parseInteger whole
                       e <- parseInteger exp
                       pure (w, 0, e)
                   (whole:::[]) =>
                     do
                       w <- cast {from=Integer} <$> parseInteger whole
                       pure (w, 0, 0)
                   _ => Nothing
               (whole:::fracAndExp::[]) =>
                 case split (\c => c == 'e' || c == 'E') fracAndExp of
                   ("":::exp::[]) => Nothing
                   (frac:::exp::[]) =>
                     do
                       w <- cast {from=Integer} <$> parseInteger whole
                       f <- (/ (natpow 10 (length frac))) <$>
                            (cast <$> parseNumWithoutSign (unpack frac) 0)
                       e <- parseInteger exp
                       pure (w, if w < 0 then (-f) else f, e)
                   (frac:::[]) =>
                     do
                       w <- cast {from=Integer} <$> parseInteger whole
                       f <- (/ (natpow 10 (length frac))) <$>
                            (cast <$> parseNumWithoutSign (unpack frac) 0)
                       pure (w, if w < 0 then (-f) else f, 0)
                   _ => Nothing
               _ => Nothing

public export
null : String -> Bool
null = (== "")


text:
module Main

f : List Integer -> Bool
f [1, 1124000727777607680000] = True
f [1124000727777607680000] = True
f [1124000727777607680001] = True
f [2] = True
f [] = True
f _ = False

ff : Integer -> Maybe Integer
ff 1124000727777607680000 = Just 2003
ff 123123213123123 = Nothing
ff _ = Just 0

main : IO ()
main = do
     putStrLn $ show $ f  [1, product [1..22]]
     putStrLn $ show $ f  [product [1..22] + 1]
     putStrLn $ show $ f  [product [1..22]]
     putStrLn $ show $ f (2 :: [])
     putStrLn $ show $ f [2, 3, 4]
     putStrLn $ show $ f []
     putStrLn $ show $ ff 1124000727777607680000
     putStrLn $ show $ ff 123123213123123
     putStrLn $ show $ ff (-3)

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Data.HashSet

import public Data.Hashable
import Data.HashMap.Internal
import Data.HashMap

||| A hash set.
export
data HashSet : Type -> Type where
    MkHS :
        (eq : k -> k -> Bool) ->
        (hashWithSalt : Salt -> k -> Hash) ->
        HashArrayMapTrie k () ->
        HashSet k

||| Create an empty `HashSet`.
export
empty : Hashable k => Eq k => HashSet k
empty = MkHS (==) hashWithSalt Internal.empty

||| Create a `HashSet` from a single element.
export
singleton : Hashable k => Eq k => k -> HashSet k
singleton k = MkHS (==) hashWithSalt $ Internal.singleton (hashWithSalt defaultSalt k) k ()

||| Returns `True` if the `HashSet` contains provided element.
export
member : k -> HashSet k -> Bool
member k (MkHS eq hws m) = case Internal.lookup eq hws bitMask0 (hws defaultSalt k) k m of
    Nothing => False
    Just _ => True

||| Remove an element from a `HashSet`.
export
delete : k -> HashSet k -> HashSet k
delete k (MkHS eq hws m) = MkHS eq hws $ Internal.delete eq hws bitMask0 (hws defaultSalt k) k m

||| Add an element to a `HashSet`.
export
insert : k -> HashSet k -> HashSet k
insert k (MkHS eq hws m) = MkHS eq hws $ Internal.insert eq hws defaultSalt bitMask0 (hws defaultSalt k) k () m

||| Fold the elements in a `HashSet`
export
foldKeys : (k -> acc -> acc) -> acc -> HashSet k -> acc
foldKeys f z (MkHS _ _ m) = foldWithKey go z m
  where
    go : k -> () -> acc -> acc
    go k _ acc = f k acc

||| Turn a `HashMap` into a `HashSet`
export
keySet : HashMap k v -> HashSet k
keySet m = unsafeFoldHashMap (\eq, hws, m => MkHS eq hws (ignore m)) m


text:
module Postgres.Data

import public Postgres.Data.Conn
import public Postgres.Data.ConnectionStatus
import public Postgres.Data.ResultStatus
import public Postgres.Data.PostgresType

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
import Data.Strings

VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

strToInput : String -> Maybe Input
strToInput "insert" = Just COIN
strToInput "vend" = Just VEND
strToInput "change" = Just CHANGE
strToInput x = if all isDigit (unpack x)
                  then Just (REFILL (stringToNatOrZ x))
                  else Nothing

export
data MachineCmd : Type ->
                  VendState -> VendState ->
                  Type where
  InsertCoin : MachineCmd () (pounds, chocs)     (S pounds, chocs)
  Vend :       MachineCmd () (S pounds, S chocs) (pounds, chocs)
  GetCoins :   MachineCmd () (pounds, chocs)     (Z, chocs)

  Refill : (bars : Nat) ->
           MachineCmd () (Z, chocs) (Z, bars + chocs)

  Display : String -> MachineCmd ()            state state
  GetInput :          MachineCmd (Maybe Input) state state

  Pure : ty -> MachineCmd ty state state
  (>>=) : {state2 : _} ->
          MachineCmd a state1 state2 ->
          (a -> MachineCmd b state2 state3) ->
          MachineCmd b state1 state3

export
data MachineIO : VendState -> Type where
  Do : {state1 : _} ->
       MachineCmd a state1 state2 ->
       (a -> Inf (MachineIO state2)) -> MachineIO state1

runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty
runMachine InsertCoin = putStrLn "Coin inserted"
runMachine Vend = putStrLn "Please take your chocolate"
runMachine {inState = (pounds, _)} GetCoins
     = putStrLn (show pounds ++ " coins returned")
runMachine (Display str) = putStrLn str
runMachine (Refill bars)
     = putStrLn ("Chocolate remaining: " ++ show bars)
runMachine {inState = (pounds, chocs)} GetInput
     = do putStrLn ("Coins: " ++ show pounds ++ "; " ++
                    "Stock: " ++ show chocs)
          putStr "> "
          x <- getLine
          pure (strToInput x)
runMachine (Pure x) = pure x
runMachine (cmd >>= prog) = do x <- runMachine cmd
                               runMachine (prog x)
namespace MachineDo
  export
  (>>=) : {state1 : _} ->
          MachineCmd a state1 state2 ->
          (a -> Inf (MachineIO state2)) -> MachineIO state1
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> MachineIO state -> IO ()
run (More fuel) (Do c f)
     = do res <- runMachine c
          run fuel (f res)
run Dry p = pure ()

mutual
  vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
  vend {pounds = (S p)} {chocs = (S c)} = do Vend
                                             Display "Enjoy!"
                                             machineLoop
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop

  refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _ = do Display "Can't refill: Coins in machine"
                machineLoop

  machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs)
  machineLoop = do Just x <- GetInput
                             | Nothing => do Display "Invalid input"
                                             machineLoop
                   case x of
                        COIN => do InsertCoin
                                   machineLoop
                        VEND => vend
                        CHANGE => do GetCoins
                                     Display "Change returned"
                                     machineLoop
                        REFILL num => refill num

main : IO ()
main = run forever (machineLoop {pounds = 0} {chocs = 1})


text:
module IR

import Control.Monad.Identity
import Data.SortedMap
import Effect.State
import IR.Event
import IR.Lens
import IR.Reader

%default total

record Rectangle : Type where
  MkRectangle : (rectX : Float) ->
                (rectY : Float) ->
                (rectW : Float) ->
                (rectH : Float) ->
                Rectangle

rectX' : Lens Rectangle Float
rectX' = lens (\(MkRectangle x _ _ _) => x) (\x, (MkRectangle _ a b c) => MkRectangle x a b c)

rectY' : Lens Rectangle Float
rectY' = lens (\(MkRectangle _ x _ _) => x) (\x, (MkRectangle a _ b c) => MkRectangle a x b c)

rectW' : Lens Rectangle Float
rectW' = lens (\(MkRectangle _ _ x _) => x) (\x, (MkRectangle a b _ c) => MkRectangle a b x c)

rectH' : Lens Rectangle Float
rectH' = lens (\(MkRectangle _ _ _ x) => x) (\x, (MkRectangle a b c _) => MkRectangle a b c x)

record Stack : Type -> Type where
  MkStack : (stackFocus : wid) ->
            (stackUp : List wid) ->
            (stackDown : List wid) ->
            Stack wid

stackFocus' : Lens (Stack wid) wid
stackFocus' = lens (\(MkStack x _ _) => x) (\x, (MkStack _ a b) => MkStack x a b)

stackUp' : Lens (Stack wid) (List wid)
stackUp' = lens (\(MkStack _ x _) => x) (\x, (MkStack a _ b) => MkStack a x b)

stackDown' : Lens (Stack wid) (List wid)
stackDown' = lens (\(MkStack _ _ x) => x) (\x, (MkStack a b _) => MkStack a b x)

stackLength : Stack wid -> Nat
stackLength (MkStack _ ys zs) = S (length ys + length zs)

LayoutF : Type -> Type
LayoutF wid = Rectangle -> (s : Stack wid) -> Vect (stackLength s) (wid, Rectangle)

record Layout : Type -> Type where
  MkLayout : (layoutPure : LayoutF wid) ->
             (layoutNext : Inf (Layout wid)) ->
             Layout wid

layoutPure' : Lens (Layout wid) (LayoutF wid)
layoutPure' = lens (\(MkLayout x _) => x) (\x, (MkLayout _ a) => MkLayout x a)

layoutNext' : Lens (Layout wid) (Layout wid)
layoutNext' = lens (\(MkLayout _ x) => x) (\x, (MkLayout a _) => MkLayout a x)

record Workspace : Type -> Type where
  MkWorkspace : (workspaceLayout : Layout wid) ->
                (workspaceStack : Maybe (Stack wid)) ->
                Workspace wid

workspaceLayout' : Lens (Workspace wid) (Layout wid)
workspaceLayout' = lens (\(MkWorkspace x _) => x) (\x, (MkWorkspace _ a) => MkWorkspace x a)

workspaceStack' : Lens (Workspace wid) (Maybe (Stack wid))
workspaceStack' = lens (\(MkWorkspace _ x) => x) (\x, (MkWorkspace a _) => MkWorkspace a x)

record Screen : Type -> Type -> Type where
  MkScreen : (screenWorkspace : Workspace wid) ->
             (screenId : sid) ->
             (screenDetail : Rectangle) ->
             Screen wid sid

screenWorkspace' : Lens (Screen wid sid) (Workspace wid)
screenWorkspace' = lens (\(MkScreen x _ _) => x) (\x, (MkScreen _ a b) => MkScreen x a b)

screenDetail' : Lens (Screen wid sid) Rectangle
screenDetail' = lens (\(MkScreen _ _ x) => x) (\x, (MkScreen a b _) => MkScreen a b x)

record StackSet : Type -> Type -> Type where
  MkStackSet : (stackSetCurrent : Screen wid sid) ->
               (stackSetVisible : List (Screen wid sid)) ->
               (stackSetHidden  : List (Workspace wid)) ->
               StackSet wid sid

stackSetCurrent' : Lens (StackSet wid sid) (Screen wid sid)
stackSetCurrent' = lens (\(MkStackSet x _ _) => x) (\x, (MkStackSet _ a b) => MkStackSet x a b)

record IRState : Type -> Type -> Type where
  MkIRState : (irStateStackSet : StackSet wid sid) ->
              IRState wid sid

irStateStackSet' : Lens (IRState wid sid) (StackSet wid sid)
irStateStackSet' = lens (\(MkIRState x) => x) (\x, (MkIRState _) => MkIRState x)

data IREffect : Type -> Type -> Effect where
  GetEvent : { () } (IREffect wid sid) Event
  GetFrames : { () } (IREffect wid sid) (n ** Vect (S n) Rectangle)
  GetWindows : { () } (IREffect wid sid) (List wid)
  GrabKeys : List Key -> { () } (IREffect wid sid) ()
  RefreshState : IRState wid sid -> { () } (IREffect wid sid) (IRState wid sid)
  SetFocus : wid -> { () } (IREffect wid sid) ()
  TileWindow : wid -> Rectangle -> { () } (IREffect wid sid) ()

IR : Type -> Type -> EFFECT
IR wid sid = MkEff () (IREffect wid sid)

record IRConf : Type -> Type -> Type where
  MkIRConf : (irConfKeyActions : SortedMap Key ({ [IR wid sid, STATE (IRState wid sid)] } Eff ())) ->
             IRConf wid sid

irConfKeyActions' : Lens (IRConf wid sid) (SortedMap Key ({ [IR wid sid, STATE (IRState wid sid)] } Eff ()))
irConfKeyActions' = lens (\(MkIRConf x) => x) (\x, (MkIRConf _) => MkIRConf x)

getEvent : { [IR wid sid] } Eff Event
getEvent = call GetEvent

grabKeys : List Key -> { [IR wid sid] } Eff ()
grabKeys k = call (GrabKeys k)

setFocus : wid -> { [IR wid sid] } Eff ()
setFocus wid = call (SetFocus wid)

tileWindow : wid -> Rectangle -> { [IR wid sid] } Eff ()
tileWindow wid rect = call (TileWindow wid rect)

runLayout : { [IR wid sid, STATE (IRState wid sid)] } Eff ()
runLayout = do
  s <- get
  let screen = stackSetCurrent' . irStateStackSet' ^$ s
  let frame : Rectangle = screenDetail' ^$ screen
  -- Idris bug: maybe doesn't work here, have to use fromMaybe
  let maybeStack = workspaceStack' . screenWorkspace' ^$ screen
  let l = layoutPure' . workspaceLayout' . screenWorkspace' ^$ screen
  case maybeStack of
    Just stack => do
      mapVE (uncurry tileWindow) (l frame stack)
      setFocus (stackFocus' ^$ stack)
      return ()
    Nothing => return ()

refresh : { [IR wid sid, STATE (IRState wid sid)] } Eff ()
refresh = do
  s <- get
  s' <- call (RefreshState s)
  put s'
  runLayout

getFrames : { [IR wid sid] } Eff (n ** Vect (S n) Rectangle)
getFrames = call GetFrames

getWindows : { [IR wid sid] } Eff (List wid)
getWindows = call GetWindows

nextLayout : IRState wid sid -> IRState wid sid
nextLayout = workspaceLayout' . screenWorkspace' . stackSetCurrent' . irStateStackSet' ^%= getL layoutNext'

handleEvent : Event -> { [IR wid sid, STATE (IRState wid sid), READER (IRConf wid sid)] } Eff ()
handleEvent RefreshEvent = refresh
handleEvent (KeyEvent key) = do
  conf <- ask
  -- Idris bug: can't inline this let
  let m = lookup key (irConfKeyActions' ^$ conf)
  fromMaybe (return ()) m
  return ()
handleEvent IgnoredEvent = return ()

partial
runIR' : { [IR wid sid, STATE (IRState wid sid), READER (IRConf wid sid)] } Eff ()
runIR' = do
  e <- getEvent
  handleEvent e
  runIR'

partial
runIR : { [IR wid sid, STATE (IRState wid sid), READER (IRConf wid sid)] } Eff ()
runIR = do
  conf <- ask
  grabKeys (map fst (toList (irConfKeyActions' ^$ conf)))
  runLayout
  runIR'

max_stars_repo_name: puffnfresh/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
||| Reexporting `Data.Subset.Interfaces` and `Data.Subset.Predicates`
||| plus some utility functions.
module Data.Subset

import public Data.Subset.Interfaces
import public Data.Subset.Predicates
import public Data.Maybe

%default total

||| Compile time refinement of values
||| If this does not work, the predicate in question
||| might contain a negation. If that's the case, try `refine'`.
public export
refine : (v : t) -> {auto 0 prf : p v} -> Subset t p
refine v = Element v prf

||| Like `Data.Subset.refine` but goes via a propsition's `Predicate`
||| instance. This is necessary for instance for
||| compiletime verification of negations, for which
||| Idris2 is to able to come up with a value otherwise.
public export
refine' :  {0 t : Type} -> {0 p : t -> Type}
        -> Predicate t p
        => (v : t)
        -> {auto prf : IsJust (refineMay {p = p} v)}
        -> Subset t p
refine' v = fromJust (refineMay {p = p} v)

public export
fromInteger :  Num t
            => (v : Integer)
            -> {auto 0 prf : p (fromInteger v)}
            -> Subset t p
fromInteger v = refine (fromInteger v)

public export
fromString :  FromString t
           => (v : String)
           -> {auto 0 prf : p (fromString v)}
           -> Subset t p
fromString v = refine (fromString v)


text:
||| Properties of Fibonacci functions
module Data.Nat.Fib

import Data.Nat

%default total

||| Recursive definition of Fibonacci.
fibRec : Nat -> Nat
fibRec Z = Z
fibRec (S Z) = S Z
fibRec (S (S k)) = fibRec (S k) + fibRec k

||| Accumulator for fibItr.
fibAcc : Nat -> Nat -> Nat -> Nat
fibAcc Z a _ = a
fibAcc (S k) a b = fibAcc k b (a + b)

||| Iterative definition of Fibonacci.
fibItr : Nat -> Nat
fibItr n = fibAcc n 0 1

||| Addend shuffling lemma.
plusLemma : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
plusLemma a b c d =
  rewrite sym $ plusAssociative a b (c + d) in
    rewrite plusAssociative b c d in
      rewrite plusCommutative b c in
        rewrite sym $ plusAssociative c b d in
          plusAssociative a c (b + d)

||| Helper lemma for fibacc.
fibAdd : (n, a, b, c, d : Nat) ->
  fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)
fibAdd Z _ _ _ _ = Refl
fibAdd (S Z) _ _ _ _ = Refl
fibAdd (S (S k)) a b c d =
  rewrite fibAdd k (a + b) (b + (a + b)) (c + d) (d + (c + d)) in
    rewrite plusLemma b (a + b) d (c + d) in
      rewrite plusLemma a b c d in
        Refl

||| Iterative and recursive Fibonacci definitions are equivalent.
fibEq : (n : Nat) -> fibRec n = fibItr n
fibEq Z = Refl
fibEq (S Z) = Refl
fibEq (S (S k)) =
  rewrite fibEq k in
    rewrite fibEq (S k) in
      fibAdd k 1 1 0 1


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Examples
import Control.Lens

--
-- Examples of interactions available with these Lenses
--

Ex1 : Maybe Int
Ex1 = over mapped (+1) (Just 2)

Ex1Proof : Ex1 = Just 3
Ex1Proof = Refl

Ex2 : (Int, Int)
Ex2 = (2,3) |> over both (+1)

Ex2Proof : Ex2 = (3, 4)
Ex2Proof = Refl

Ex3 : (String, String)
Ex3 = ("Hello",2) |> snd_ .~ "World!"

Ex3Proof : Ex3 = ("Hello","World!")
Ex3Proof = Refl

Ex4 : Either String Int
Ex4 = f (Left "hi")
  where f : Either String Int -> Either String Int
        f = over right_ (+1)

Ex4Proof : Ex4 = (Left "hi")
Ex4Proof = Refl

Ex5 : Either String Int
Ex5 = f (Right 4)
  where f : Either String Int -> Either String Int
        f = over right_ (+1)

Ex5Proof : Ex5 = (Right 5)
Ex5Proof = Refl

Ex6 : Either (String, Int) Int
Ex6 = f (Left ("hi", 2))
  where f : Either (String,Int) Int -> Either (String,Int) Int
        f = over (left_ . snd_) (+1)

Ex6Proof : Ex6 = Left ("hi", 3)
Ex6Proof = Refl

-- Ex7 and Ex8 need to use the PlusNatMonoid named instance and I don't know how to do this yet
[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

[PlusNatApplicative] Applicative (Const Nat) using PlusNatMonoid where
  pure _                      = MkConst neutral
  (MkConst f) <*> (MkConst v) = MkConst (f <+> v)

-- f : Either (String, Nat) Int -> Nat
-- f = view @{PlusNatApplicative} (left_ . snd_)

-- Ex7 : Nat
-- Ex7 = f (Left ("hi", 2)) where

-- Ex7Proof : Ex7 = 2
-- Ex7Proof = Refl

-- Ex8 : Nat
-- Ex8 = f (Right 2) where
--   f : Either (String, Additive) Int -> Additive
--   f = view (left_ . snd_)

-- Ex8Proof : Ex8 = 0
-- Ex8Proof = Refl

Ex9 : Maybe String
Ex9 = g ^? right_ . fst_ where
 g : Either String (String, Int)
 g = Right ("x",2)

Ex9Proof : Ex9 = Just "x"
Ex9Proof = Refl

Ex10 : Maybe ()
Ex10 = Just "x" ^? nothing_

Ex10Proof : Ex10 = Nothing
Ex10Proof = Refl

Ex11 : Maybe ()
Ex11 = n ^? nothing_ where
  n : Maybe String
  n = Nothing

Ex11Proof : Ex11 = Just ()
Ex11Proof = Refl

Ex12 : Int
Ex12 = view (to fst) (1,2)

Ex12Proof : Ex12 = 1
Ex12Proof = Refl

Ex13 : Either Int String
Ex13 = the (Either Int String) $ left_ # 4

Ex13Proof : Ex13 = Left 4
Ex13Proof = Refl

Ex14 : Either Int String
Ex14 = the (Either Int String) $ 5 ^.re left_

Ex14Proof : Ex14 = Left 5
Ex14Proof = Refl

sansExample : Maybe Int
sansExample = sans () (Just 4)

fusingExample : Maybe (Int, Int)
fusingExample = Just (2,3) |> over ( fusing (just_ . both)) (+1)

confusingExample : Maybe (Int, Int)
confusingExample = Just (2,3) |> over ( confusing (just_ . both)) (+1)

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


text:
module Data.AVL.Core

import public Data.Tree

%default total
%access export

 -- ------------------------------------------------------------- [ Definitions ]
public export
data Balance : Nat -> Nat -> Type where
  LHeavy   : Balance (S n) n
  RHeavy   : Balance n     (S n)
  Balanced : Balance n     n

%name Balance b, bal

||| Indirection ensures that it reduces to at least S n' without
||| needing to case split on balance.
|||
||| Should make proofs easier.
public export
height : Balance n m -> Nat
height b = S (height' b)
  where
    height' : Balance n m -> Nat
    height' (LHeavy {n}) = S n
    height' (RHeavy {n}) = S n
    height' {n} (Balanced {n}) = n

||| Encoding of the AVL tree height invariants.
|||
||| @height The height of a Tree.
||| @tree   The tree whose height we are capturing.
public export
data AVLInvariant : (height : Nat)
                 -> (tree   : Tree k v)
                 -> Type
  where
    ||| A tree of height zero.
    AVLEmpty : AVLInvariant 0 Empty
    ||| A Balanced tree.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    ||| @b     The encoding of the nodes' balance.
    AVLNode : (left  : AVLInvariant n l)
           -> (right :  AVLInvariant m r)
           -> (b : Balance n m)
           -> AVLInvariant (height b) (Node k v l r)

%name AVLInvariant inv

||| An AVL Tree.
|||
||| Modelled using subset to separate the invariants from the tree
||| implementation itself.
|||
||| @height  The height of the Tree.
||| @keyTy   The type associated with the keys.
||| @valueTy The type associated with the values.
public export
AVLTree : (height  : Nat)
       -> (keyTy   : Type)
       -> (valueTy : Type)
       -> Type
AVLTree n k v = Subset (Tree k v) (AVLInvariant n)

-- --------------------------------------------------------------- [ Rotations ]
public export
data InsertRes : Nat -> (k : Type) -> Type -> Type where
  Same : AVLTree n k v     -> InsertRes n k v
  Grew : AVLTree (S n) k v -> InsertRes n k v

%name InsertRes res, r

||| Process the result of an insertion of a new Key-Value pair into
||| the Tree, returning the new tree and proof of the new tree's
||| height.
|||
||| `InsertRes` is obtained from the result of running `Tree.insert`.
runInsertRes : InsertRes n k v -> (n : Nat ** AVLTree n k v)
runInsertRes (Same t) = (_ ** t)
runInsertRes (Grew t) = (_ ** t)

||| Perform a Left roation.
rotLeft : k
       -> v
       -> AVLTree n k v
       -> AVLTree (S (S n)) k v
       -> InsertRes (S (S n)) k v
-- Impossible because Empty has depth 0 and we know the depth is at least 2 from the type
rotLeft key val l (Element Empty AVLEmpty) impossible

rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr Balanced)) =
    Grew $ Element (Node key' val' (Node key val l rl) rr)
                        (AVLNode (AVLNode invl invrl RHeavy) invrr LHeavy)

rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr LHeavy) invrr LHeavy)) =
    Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr)) -- Needs Checking
                   (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr RHeavy) Balanced)

rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr RHeavy) invrr LHeavy)) =
    Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr))
                   (AVLNode (AVLNode invl invrll LHeavy) (AVLNode invrlr invrr Balanced) Balanced)

rotLeft key val (Element l invl) (Element (Node key' val' (Node key'' val'' rll rlr) rr) (AVLNode (AVLNode invrll invrlr Balanced) invrr LHeavy)) =
    Same $ Element (Node key'' val'' (Node key val l rll) (Node key' val' rlr rr))
                   (AVLNode (AVLNode invl invrll Balanced) (AVLNode invrlr invrr Balanced) Balanced) -- Needs Checking

rotLeft key val (Element l invl) (Element (Node key' val' rl rr) (AVLNode invrl invrr RHeavy)) =
    Same $ Element (Node key' val' (Node key val l rl) rr)
                   (AVLNode (AVLNode invl invrl Balanced) invrr Balanced)

||| Perform a Right rotation.
rotRight : k
        -> v
        -> AVLTree (S (S n)) k v
        -> AVLTree n k v
        -> InsertRes (S (S n)) k v
rotRight key val (Element Empty AVLEmpty) r impossible

rotRight key'' val'' (Element (Node key val ll (Node key' val' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr RHeavy) RHeavy)) (Element r invr) =
  Same $ Element (Node key' val' (Node key val ll lrl) (Node key'' val'' lrr r))
                 (AVLNode (AVLNode invll invlrl LHeavy) (AVLNode invlrr invr Balanced) Balanced)

rotRight key'' val'' (Element (Node key val ll (Node key' val' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr LHeavy) RHeavy)) (Element r invr) =
  Same $ Element (Node key' val' (Node key val ll lrl) (Node key'' val'' lrr r))
                 (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr RHeavy) Balanced)

rotRight key val (Element (Node key' val' ll lr) (AVLNode invll invlr Balanced)) (Element r invr) =
  Grew $ Element (Node key' val' ll (Node key val lr r))
                 (AVLNode invll (AVLNode invlr invr LHeavy) RHeavy)

rotRight key val (Element (Node key' val' ll lr) (AVLNode invll invlr LHeavy)) (Element r invr) =
  Same $ Element (Node key' val' ll (Node key val lr r))
                 (AVLNode invll (AVLNode invlr invr Balanced) Balanced)

rotRight key val (Element (Node key' val' ll (Node key'' val'' lrl lrr))
             (AVLNode invll (AVLNode invlrl invlrr Balanced) RHeavy)) (Element r invr) =
  Same $ Element (Node key'' val'' (Node key' val' ll lrl) (Node key val lrr r))
                 (AVLNode (AVLNode invll invlrl Balanced) (AVLNode invlrr invr Balanced) Balanced)

 --------------------------------------------------------------- [ Insertion ]

||| Perform an insertion into the tree returning the new tree wrapped
||| in a description describing the height change.
doInsert : (Ord k)
         => k
         -> v
         -> AVLTree n k v
         -> InsertRes n k v
doInsert newKey newVal (Element Empty AVLEmpty) = Grew (Element (Node newKey newVal Empty Empty)
                                                              (AVLNode AVLEmpty AVLEmpty Balanced))
doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) with (compare newKey key)
  doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | EQ = Same (Element (Node newKey newVal l r) (AVLNode invl invr b))

  doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | LT with (assert_total $ doInsert newKey newVal (Element l invl))
    -- Totality checker not clever enough to see that this is smaller
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b))        | LT | (Same (Element l' invl'))
                                                                                = Same $ Element (Node key val l' r) (AVLNode invl' invr b)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr LHeavy))   | LT | (Grew (Element l' invl'))
                                                                                = rotRight key val (Element l' invl') (Element r invr)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr Balanced)) | LT | (Grew (Element l' invl'))
                                                                                = Grew $ Element (Node key val l' r) (AVLNode invl' invr LHeavy)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr RHeavy))   | LT | (Grew (Element l' invl'))
                                                                                = Same $ Element (Node key val l' r) (AVLNode invl' invr Balanced)

  doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b)) | GT with (assert_total $ doInsert newKey newVal (Element r invr))
  -- Totality checker not clever enough to see that this is smaller
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr b))        | GT | (Same (Element r' invr'))
                                                                                = Same $ Element (Node key val l r') (AVLNode invl invr' b)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr LHeavy))   | GT | (Grew (Element r' invr'))
                                                                                = Same $ Element (Node key val l r') (AVLNode invl invr' Balanced)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr Balanced)) | GT | (Grew (Element r' invr'))
                                                                                = Grew $ Element (Node key val l r') (AVLNode invl invr' RHeavy)
    doInsert newKey newVal (Element (Node key val l r) (AVLNode invl invr RHeavy))   | GT | (Grew (Element r' invr'))
                                                                                = rotLeft key val (Element l invl) (Element r' invr')

||| Insert a key value pair into the tree, returning a the new tree
||| and possibly its new height.
insert : Ord k => k -> v -> AVLTree n k v -> (n : Nat ** AVLTree n k v)
insert k v t = runInsertRes (doInsert k v t)


text:
module AOC.Solution.IO

import AOC.Solution

import System.File

printSolution : forall a. AOCSolution a -> IO ()
printSolution sol = do
  file <- readFile ("inputs/day-" ++ (show sol.day) ++ ".txt")
  inputString <- case file of
                   Left err => do
                     printLn err
                     pure ""
                   Right x => pure x

  case (sol.parser inputString) of
      Just input => do
        let part1 = sol.part1 input
            part2 = sol.part2 input

        putStrLn $ "Day " ++ show sol.day ++ ":"
        putStrLn $ "Answer 1: " ++ part1
        putStrLn $ "Answer 2: " ++ part2

      Nothing => do
        printLn $ "Could not parse string for day " ++ show sol.day

export
printSolutionDP : (a ** AOCSolution a) -> IO ()
printSolutionDP x = printSolution (x.snd)


text:
module Sortings

import Data.Fin
import Data.Vect
import Data.So

%default total

||| Structural inductive rules for prooving that one vector is a permutation of another.
public export
data Permutation : Vect n a -> Vect n a -> Type where
  EmptyPerm  : Permutation [] []
  InsertPerm : {xs : Vect _ a} -> {lys : Vect lm a} -> {rys : Vect rm a}
            -> Permutation xs (lys ++ rys) -> Permutation (x::xs) (rewrite plusSuccRightSucc lm rm in lys ++ x::rys)

public export
data Sorted : {auto ord : Ord a} -> Vect n a -> Type where
  Empty     : Ord a =>                                             Sorted []
  Singleton : Ord a =>                                             Sorted [x]
  Comp      : {x, y : a} -> Sorted {ord} (x::xs) -> So (y <= x) -> Sorted (y::x::xs)

export
soAbsurd : So b -> So (not b) -> Void
soAbsurd sb snb with (sb)
  | Oh = uninhabited snb

export
soNotToNotSo : So (not b) -> Not (So b)
soNotToNotSo = flip soAbsurd

export
isSorted : Ord a => (xs : Vect n a) -> (s : Bool ** if s then Sorted xs else Not (Sorted xs))
isSorted []  = (True ** Empty)
isSorted [_] = (True ** Singleton)
isSorted (y::x::xs) = case choose (y <= x) of
  Left yx => case isSorted (x::xs) of
    (True  ** prf) => (True ** Comp prf yx)
    (False ** prf) => (False ** \(Comp s _) => prf s)
  Right yxNEq => (False ** \(Comp _ yxEq) => soAbsurd yxEq yxNEq)

public export
sorted : Ord a => Vect n a -> Bool
sorted []         = True
sorted [_]        = True
sorted (y::x::xs) = (y <= x) && sorted (x::xs)

export
total doubleNotDisappears : (b : Bool) -> not (not b) = b
doubleNotDisappears True  = Refl
doubleNotDisappears False = Refl

export
takeSoConjPart : So b -> So (b && c) -> So c
takeSoConjPart sb sbc with (sb)
  takeSoConjPart _ sbc | Oh with (sbc)
    takeSoConjPart _ _ | Oh | Oh = Oh

export
soConjAbsurd : So b -> So (not b && c) -> Void
soConjAbsurd sb sbc with (sb)
  | Oh = uninhabited sbc

export total
splitSoConj : So (b && c) -> (So b, So c)
splitSoConj {b=True} sbc with (sbc)
  | Oh = (Oh, Oh)

namespace SortedProperties
  export
  valueToType : Ord a => So (Sortings.sorted xs) -> Sorted xs
  valueToType {xs=[]}       _  = Empty
  valueToType {xs=[_]}      _  = Singleton
  valueToType {xs=y::x::xs} so = let (soyx, soxxs) = splitSoConj so in
                                 Comp (valueToType soxxs) soyx

  export
  typeToValue : Ord a => Sorted xs -> So (Sortings.sorted xs)
  typeToValue = ?typeToValue_impl

  export
  notValueToNotType : Ord a => So (not $ Sortings.sorted xs) -> Not (Sorted xs)
  notValueToNotType = ?notValueToNotType_impl

  export
  notTypeToNotValue : Ord a => Not (Sorted xs) -> So (not $ Sortings.sorted xs)
  notTypeToNotValue = ?notTypeToNotValue_impl

||| Sorting with direct encoding of first-order logic formulae of sortedness properties
export
sortDirect : Ord a => (v : Vect n a) -> (s : Vect n a ** (v `Permutation` s, Sorted s))
sortDirect = ?sortDirect_impl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Core.Options.Log

import public Data.List
import Data.List1
import public Data.Maybe
import Libraries.Data.StringMap
import Libraries.Data.StringTrie
import Data.String
import Data.These
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.String

%default total

||| Log levels are characterised by two things:
||| * a dot-separated path of ever finer topics of interest e.g. scope.let
||| * a natural number corresponding to the verbosity level e.g. 5
|||
||| If the user asks for some logs by writing
|||
|||     %log scope 5
|||
||| they will get all of the logs whose path starts with `scope` and whose
||| verbosity level is less or equal to `5`. By combining different logging
||| directives, users can request information about everything (with a low
||| level of details) and at the same time focus on a particular subsystem
||| they want to get a lot of information about. For instance:
|||
|||     %log 1
|||     %log scope.let 10
|||
||| will deliver basic information about the various phases the compiler goes
||| through and deliver a lot of information about scope-checking let binders.

----------------------------------------------------------------------------------
-- INDIVIDUAL LOG LEVEL

public export
knownTopics : List (String, Maybe String)
knownTopics = [
    ("auto", Nothing),
    ("builtin.Natural", Nothing),
    ("builtin.Natural.addTransform", Nothing),
    ("builtin.NaturalToInteger", Nothing),
    ("builtin.NaturalToInteger.addTransforms", Nothing),
    ("builtin.IntegerToNatural", Nothing),
    ("builtin.IntegerToNatural.addTransforms", Nothing),
    ("compile.casetree", Nothing),
    ("compile.casetree.clauses", Nothing),
    ("compile.casetree.getpmdef", Nothing),
    ("compile.casetree.intermediate", Nothing),
    ("compile.casetree.measure", Just "Log the node counts of each runtime case tree."),
    ("compile.casetree.pick", Nothing),
    ("compile.casetree.partition", Nothing),
    ("compiler.cse", Nothing),
    ("compiler.identity", Nothing),
    ("compiler.inline.eval", Nothing),
    ("compiler.interpreter", Nothing),
    ("compiler.refc", Nothing),
    ("compiler.refc.cc", Nothing),
    ("compiler.scheme.chez", Nothing),
    ("coverage", Nothing),
    ("coverage.empty", Nothing),
    ("coverage.missing", Nothing),
    ("coverage.recover", Nothing),
    ("declare.data", Nothing),
    ("declare.data.constructor", Nothing),
    ("declare.data.parameters", Nothing),
    ("declare.def", Nothing),
    ("declare.def.clause", Nothing),
    ("declare.def.clause.impossible", Nothing),
    ("declare.def.clause.with", Nothing),
    ("declare.def.impossible", Nothing),
    ("declare.def.lhs", Nothing),
    ("declare.def.lhs.implicits", Nothing),
    ("declare.param", Nothing),
    ("declare.record", Nothing),
    ("declare.record.field", Nothing),
    ("declare.record.projection", Nothing),
    ("declare.record.projection.prefix", Nothing),
    ("declare.type", Nothing),
    ("desugar.idiom", Nothing),
    ("doc.record", Nothing),
    ("doc.module", Nothing),
    ("elab", Nothing),
    ("elab.ambiguous", Nothing),
    ("elab.app.var", Nothing),
    ("elab.app.lhs", Nothing),
    ("elab.as", Nothing),
    ("elab.bindnames", Nothing),
    ("elab.binder", Nothing),
    ("elab.case", Nothing),
    ("elab.def.local", Nothing),
    ("elab.delay", Nothing),
    ("elab.hole", Nothing),
    ("elab.implicits", Nothing),
    ("elab.implementation", Nothing),
    ("elab.interface", Nothing),
    ("elab.interface.default", Nothing),
    ("elab.local", Nothing),
    ("elab.prune", Nothing),
    ("elab.record", Nothing),
    ("elab.retry", Nothing),
    ("elab.rewrite", Nothing),
    ("elab.unify", Nothing),
    ("elab.update", Nothing),
    ("elab.with", Nothing),
    ("eval.casetree", Nothing),
    ("eval.casetree.stuck", Nothing),
    ("eval.eta", Nothing),
    ("eval.stuck", Nothing),
    ("idemode.hole", Nothing),
    ("ide-mode.highlight", Nothing),
    ("ide-mode.highlight.alias", Nothing),
    ("ide-mode.send", Nothing),
    ("import", Nothing),
    ("import.file", Nothing),
    ("interaction.casesplit", Nothing),
    ("interaction.generate", Nothing),
    ("interaction.search", Nothing),
    ("metadata.names", Nothing),
    ("module.hash", Nothing),
    ("quantity", Nothing),
    ("quantity.hole", Nothing),
    ("quantity.hole.update", Nothing),
    ("repl.eval", Nothing),
    ("resugar.var", Nothing),
    ("specialise", Nothing),
    ("totality", Nothing),
    ("totality.positivity", Nothing),
    ("totality.requirement", Nothing),
    ("totality.termination", Nothing),
    ("totality.termination.calc", Nothing),
    ("totality.termination.guarded", Nothing),
    ("totality.termination.sizechange", Nothing),
    ("totality.termination.sizechange.checkCall", Nothing),
    ("totality.termination.sizechange.checkCall.inPath", Nothing),
    ("totality.termination.sizechange.checkCall.inPathNot.restart", Nothing),
    ("totality.termination.sizechange.checkCall.inPathNot.return", Nothing),
    ("totality.termination.sizechange.inPath", Nothing),
    ("totality.termination.sizechange.isTerminating", Nothing),
    ("totality.termination.sizechange.needsChecking", Nothing),
    ("transform.lhs", Nothing),
    ("transform.rhs", Nothing),
    ("ttc.read", Nothing),
    ("ttc.write", Nothing),
    ("typesearch.equiv", Nothing),
    ("unelab.case", Nothing),
    ("unelab.var", Nothing),
    ("unify", Nothing),
    ("unify.application", Nothing),
    ("unify.binder", Nothing),
    ("unify.constant", Nothing),
    ("unify.constraint", Nothing),
    ("unify.delay", Nothing),
    ("unify.equal", Nothing),
    ("unify.head", Nothing),
    ("unify.hole", Nothing),
    ("unify.instantiate", Nothing),
    ("unify.invertible", Nothing),
    ("unify.meta", Nothing),
    ("unify.noeta", Nothing),
    ("unify.postpone", Nothing),
    ("unify.retry", Nothing),
    ("unify.search", Nothing),
    ("unify.unsolved", Nothing)
]

export
helpTopics : String
helpTopics = show $ vcat $ map helpTopic knownTopics

  where

  helpTopic : (String, Maybe String) -> Doc ()
  helpTopic (str, mblurb)
    = let title = "+" <++> pretty str
          blurb = maybe [] ((::[]) . indent 2 . reflow) mblurb
      in vcat (title :: blurb)

public export
KnownTopic : String -> Type
KnownTopic s = IsJust (lookup s knownTopics)

||| An individual log level is a pair of a list of non-empty strings and a number.
||| We keep the representation opaque to force users to call the smart constructor
export
data LogLevel : Type where
  MkLogLevel : List String -> Nat -> LogLevel

||| If we have already processed the input string into (maybe) a non-empty list of
||| non-empty topics we can safely make a `LogLevel`.
export
mkLogLevel' : Maybe (List1 String) -> Nat -> LogLevel
mkLogLevel' ps n = MkLogLevel (maybe [] forget ps) n

||| The smart constructor makes sure that the empty string is mapped to the empty
||| list. This bypasses the fact that the function `split` returns a non-empty
||| list no matter what.
|||
||| However, invoking this function comes without guarantees that
||| the passed string corresponds to a known topic. For this,
||| use `mkLogLevel`.
|||
||| Use this function to create user defined loglevels, for instance, during
||| elaborator reflection.
export
mkUnverifiedLogLevel : (s : String) -> Nat -> LogLevel
mkUnverifiedLogLevel "" = mkLogLevel' Nothing
mkUnverifiedLogLevel ps = mkLogLevel' (Just (split (== '.') ps))

||| Like `mkUnverifiedLogLevel` but with a compile time check that
||| the passed string is a known topic.
export
mkLogLevel : (s : String) -> {auto 0 _ : KnownTopic s} -> Nat -> LogLevel
mkLogLevel s = mkUnverifiedLogLevel s

||| The unsafe constructor should only be used in places where the topic has already
||| been appropriately processed.
export
unsafeMkLogLevel : List String -> Nat -> LogLevel
unsafeMkLogLevel = MkLogLevel

||| The topics attached to a `LogLevel` can be reconstructed from the list of strings.
export
topics : LogLevel -> List String
topics (MkLogLevel ps _) = ps

||| The verbosity is provided by the natural number
export
verbosity : LogLevel -> Nat
verbosity (MkLogLevel _ n) = n

||| When writing generic functions we sometimes want to keep the same topic but
||| change the verbosity.
export
withVerbosity : Nat -> LogLevel -> LogLevel
withVerbosity n (MkLogLevel ps _) = MkLogLevel ps n

||| A log level is show as `P.Q.R:N` where `P`, `Q` and `R` are topics and `N` is
||| a verbosity level. If there are no topics then we simply print `N`.
export
Show LogLevel where

  show (MkLogLevel ps n) = case ps of
    [] => show n
    _  => fastAppend (intersperse "." ps) ++ ":" ++ show n

export
Pretty LogLevel where

  pretty = pretty . show

export
parseLogLevel : String -> Maybe LogLevel
parseLogLevel str = do
  (c, n) <- let nns = split (== ':') str
                n = head nns
                ns = tail nns in
                case ns of
                     [] => pure (MkLogLevel [], n)
                     [ns] => pure (mkUnverifiedLogLevel n, ns)
                     _ => Nothing
  lvl <- parsePositive n
  pure $ c (fromInteger lvl)

----------------------------------------------------------------------------------
-- COLLECTION OF LOG LEVELS

||| We store the requested log levels in a Trie which makes it easy to check
||| whether a given log level is captured by the user's request for information.
export
LogLevels : Type
LogLevels = StringTrie Nat

||| By default we log everything but with very few details (i.e. next to nothing)
export
defaultLogLevel : LogLevels
defaultLogLevel = singleton [] 0

export
insertLogLevel : LogLevel -> LogLevels -> LogLevels
insertLogLevel (MkLogLevel ps n) = insert ps n

----------------------------------------------------------------------------------
-- CHECKING WHETHER TO LOG

||| We keep a log if there is a prefix of its path associated to a larger number
||| in the LogLevels.
export
keepLog : LogLevel -> LogLevels -> Bool
keepLog (MkLogLevel _ Z) _ = True
keepLog (MkLogLevel path n) levels = go path levels where

  go : List String -> StringTrie Nat -> Bool
  go path (MkStringTrie current) = here || there where

    here : Bool
    here = case fromThis current of
      Nothing => False
      Just m  => n <= m

    there : Bool
    there = case path of
      [] => False
      (p :: rest) => fromMaybe False $ do
        assoc <- fromThat current
        next  <- lookup p assoc
        pure $ go rest next


text:
module Main

import Test.Golden

examples : IO TestPool
examples = testsInDir "examples" (const True) "Example code" [] Nothing

main : IO ()
main = runner [!examples]

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


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

%name Vect xs, ys, zs

transpose : {m : Nat} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = ?empties
transpose (x :: xs) = let xs_trans = transpose xs in
                          ?transposeHelper


text:
module Rationals

--Type for divisibility
data isDivisor : Integer -> Integer -> Type where
  AllDivZ : (m : Integer) -> isDivisor m 0
  OneDivAll : (m : Integer) -> isDivisor 1 m
  MulDiv : (c : Integer) -> isDivisor n m -> isDivisor ((\l => l*c) n) ((\l => l*c) m)

isNotZero : Nat -> Bool
isNotZero Z = False
isNotZero (S k) = True

isFactorInt : Integer -> Integer -> Type  --Needed for defining Integer division
isFactorInt m n = (k : Integer ** (m * k = n))

divides : (m: Integer) -> (n: Integer) -> (k: Integer ** (m * k = n)) -> Integer
divides m n k = (fst k)

Pair : Type
Pair = (Integer, Integer)

Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat) --Euclidean algorithm implemented by Chinmaya
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)
{-
gcdab : Nat -> Nat -> Nat -- Produces the GCD of two numbers. This will be useful to produce the simplified form of a rational number.
gcdab b Z = b
gcdab a b = gcdab b (snd (Eucl a b))
-}

--Integer implemetation of gcd
gccd : (Integer, Integer) -> Integer
gccd (a, b) = if (isNotZero (toNat b)) then next else a where
  next = gccd (b, toIntegerNat (modNat (toNat a) (toNat b)))

data NotZero : Integer -> Type where --Proof that a number is not zero, needed to construct Q
  OneNotZero : NotZero 1
  NegativeNotZero : ( n: Integer ) -> NotZero n -> NotZero (-n)
  PositiveNotZero : ( m: Integer ) -> LTE 1 (fromIntegerNat m)  -> NotZero m

--Type for equality of two Rationals
data EqRat : Pair -> Pair -> Type where
  IdEq : (m : Pair) -> EqRat m m
  MulEq : (c : Integer) -> EqRat n m -> EqRat ((fst n)*c,(snd n)*c) m

make_rational : (p: Nat) -> (q: Integer) -> NotZero q -> Pair
make_rational p q x = (toIntegerNat(p), q)

InclusionMap : (n : Nat) -> Pair --Includes the naturals in Q
InclusionMap n = make_rational n 1 OneNotZero

AddRationals : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
AddRationals x a y b = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
MultiplyRationals x a y b =((fst x)*(fst y), (snd x)*(snd y))

--Need proof that MultInverse x * x = 1
MultInverse : (x: Pair) -> NotZero (fst x) -> NotZero (snd x) -> Pair
MultInverse x y z = ((snd x), (fst x))

AddInverse : (x: Pair) -> NotZero (snd x) -> Pair
AddInverse x a = (-(fst x), (snd x))

Subtraction : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
Subtraction x a y b = AddRationals x a (AddInverse y b) b

Division : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (fst y) -> NotZero (snd y) -> Pair
Division x a y b c = MultiplyRationals x a (MultInverse y b c) b

--SimplifyRational : (x: Pair) -> NotZero (snd x) -> Pair
--SimplifyRational x a = (divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x))) ___ (fst x), divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x)) __ (snd x))

--To prove that the SimplifyRational works, we can just check if the output is equal to the input
-- To be done
simplifyRational : (x : Pair) -> Pair
simplifyRational (a, b) = (sa, sb) where
  sa = cast {from=Double} {to=Integer} (da / g) where
    da = cast {from=Integer} {to=Double} a
    g = cast {from=Integer} {to=Double} (gccd (a,b))
  sb = cast {from=Double} {to=Integer} (db / g) where
    db = cast {from=Integer} {to=Double} b
    g = cast {from=Integer} {to=Double} (gccd (a,b))

--Above, I will need to supply a proof that the GCD divides the two numbers. Then, the function defined above will produce the rational in simplified form.


text:
module Career

public export
record Career where
  constructor CreateCareer
  --if no integer then return Career.company
  groupID : Maybe $ Either String Integer
  --if no string then return Career.groupId
  company : Maybe $ Either Integer String
  countryID : Maybe Integer
  --if no integer then return Career.cityName
  cityID : Maybe $ Either String Integer
  --if no string then return Career.cityID
  cityName : Maybe $ Either Integer String
  from : Maybe Integer
  until : Maybe Integer
  position : Maybe String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Main

-- Yeah, this is for windows only
%lib chez "kernel32"

%include chez "(display \"beep\")"

beep : Int -> Int -> IO Int
beep freq dur = foreign FFI_C "Beep" (Int -> Int -> IO Int) freq dur

main : IO ()
main = do
    ok <- beep 1000 1000
    print ok

max_stars_repo_name: melted/idris-chez

max_issues_repo_name: melted/idris-chez

max_forks_repo_name: melted/idris-chez


text:
{-
Extensions for collection interfaces/traits.

Check following std modules as well:
      Prelude.Foldable
    , Prelude.Functor
    , Prelude.Traversable
    , Prelude.WellFounded (Sized)

-}
module Collections

import Data.Vect
import Data.HVect
import Prelude

%hide index
%hide reverse
%access public export

data TypeHolder : Type -> Type where
    MkTypeHolder : (a : Type) -> TypeHolder a

interface StaticSized c where
  typeSize : (TypeHolder c) -> Nat

interface Indexable c i where
  eltype : i -> c -> Type
  index  : (instI: i) -> (instC: c) -> eltype instI instC

interface Reversable c1 c2 | c1 where
   reverse : c1 -> c2

||| implementations for some builtin collection types

implementation StaticSized (Vect n t) where
    typeSize {n} _ = n

implementation Sized (Vect n t) where
     size {n} _ = n

implementation Indexable (Vect n t) (Fin n) where
    eltype {t} _ _ = t
    index FZ (x :: xs) = x
    index (FS k) (x :: xs) = index k xs

-- plusZCommu : (n: Nat) -> n = plus n Z
-- plusZCommu Z = Refl
-- plusZCommu (S k) = cong (plusZCommu k)

-- thanks to ice1000, this is extremely crucial.
appendLast : Vect a n -> n -> Vect (S a) n
appendLast [] x = x :: []
appendLast (y :: xs) x = y :: appendLast xs x

reverseVect : Vect a n -> Vect a n
reverseVect [] = []
reverseVect (x :: xs) = (reverseVect xs) `appendLast` x

implementation Reversable (Vect n t) (Vect n t) where
  reverse = reverseVect

implementation StaticSized (HVect xs) where
  typeSize {xs} _ = size xs

implementation Sized (HVect xs) where
  size {xs} _ = size xs

implementation Indexable (HVect xs) (Fin (size xs)) where
    eltype {xs} fin _ = index fin xs
    index FZ (x::xs) = x
    index (FS k) (x :: xs) = index k xs

popPush : (x: t) -> (ys: Vect n2 t) -> (xs: Vect n1 t) -> xs ++ x :: ys = (xs `appendLast` x) ++ ys
popPush x ys [] = Refl
popPush x ys (y :: xs) = rewrite popPush x ys xs in Refl

vectReverseProp : (x: t) -> (ys: Vect n2 t) -> (xs: Vect n1 t) -> reverseVect xs ++ x :: ys = reverseVect (x :: xs) ++ ys
vectReverseProp x ys xs =
      rewrite popPush x ys (reverseVect xs) in Refl

vectAppendLastProp : (x: t) -> (xs : Vect m t) ->  x :: (xs ++ []) = (x :: xs) ++ []
vectAppendLastProp x xs = Refl

zeroVectCommutativeProp : (vec: Vect n t) -> vec = vec ++ []
zeroVectCommutativeProp [] = Refl
zeroVectCommutativeProp (x::xs) =
  rewrite zeroVectCommutativeProp xs in vectAppendLastProp x xs

-- convert implcit vars into the explicit ones and it works, which
--- is the 2nd suggestion from ice1000.
appendHList : (xs1 : Vect n1 Type) -> (xs2 : Vect n2 Type) ->
              HVect xs1 -> HVect xs2 -> HVect (reverseVect xs1 ++ xs2)
appendHList [] typs [] lst = lst
appendHList (x1::xs1) xs2 (elt1::lst1) lst2 =
    rewrite sym(popPush x1 xs2 (reverseVect xs1)) in
    appendHList xs1 (x1::xs2) lst1 (elt1::lst2)

implementation Reversable (HVect xs) (HVect (reverseVect xs)) where
  reverse {xs} lst =
    rewrite zeroVectCommutativeProp (reverseVect xs) in
    appendHList xs [] lst (with HVect [])

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
module Card

import Data.Vect

public export data Value: Type where
  Pip: (v: Nat) -> Value
  Jack: Value
  Queen: Value
  King: Value
  Ace: Value

public export data Suit = Clubs
  | Spades
  | Hearts
  | Diamonds

public export record Card where
  constructor  MkCard
  value : Value
  suit : Suit

||| proof that the first card is consecutive with the second
||| only valid if the first card is higher
export data ConsecComp: Card -> Card -> Type where
  PipConsec: ConsecComp (MkCard (Pip (S x)) _) (MkCard (Pip x) _)
  JackTen: ConsecComp (MkCard Jack _) (MkCard (Pip 10) _)
  QueenJack: ConsecComp (MkCard Queen _) (MkCard Jack _)
  KingQueen: ConsecComp (MkCard King _) (MkCard Queen _)
  AceKing: ConsecComp (MkCard Ace _) (MkCard King _)

export data Consecutive : Vect n Card -> Type where
  Comp : (x: Card) -> Consecutive (y :: ys) -> ConsecComp x y -> Consecutive (x :: y :: ys)
  ConSingle: (x: Card) -> Consecutive [x]
  ConEmpty : Consecutive []

clubsSpades : (Clubs = Spades) -> Void
clubsSpades Refl impossible

clubsHearts : (Clubs = Hearts) -> Void
clubsHearts Refl impossible

clubsDiamonds : (Clubs = Diamonds) -> Void
clubsDiamonds Refl impossible

spadesClubs : (Spades = Clubs) -> Void
spadesClubs Refl impossible

spadesHearts : (Spades = Hearts) -> Void
spadesHearts Refl impossible

spadesDiamonds : (Spades = Diamonds) -> Void
spadesDiamonds Refl impossible

heartsClubs : (Hearts = Clubs) -> Void
heartsClubs Refl impossible

heartsSpades : (Hearts = Spades) -> Void
heartsSpades Refl impossible

heartsDiamonds : (Hearts = Diamonds) -> Void
heartsDiamonds Refl impossible

diamondsClubs : (Diamonds = Clubs) -> Void
diamondsClubs Refl impossible

diamondsSpades : (Diamonds = Spades) -> Void
diamondsSpades Refl impossible

diamondsHearts : (Diamonds = Hearts) -> Void
diamondsHearts Refl impossible

export DecEq Suit where
  decEq Clubs Clubs = Yes Refl
  decEq Clubs Spades = No clubsSpades
  decEq Clubs Hearts = No clubsHearts
  decEq Clubs Diamonds = No clubsDiamonds
  decEq Spades Clubs = No spadesClubs
  decEq Spades Spades = Yes Refl
  decEq Spades Hearts = No spadesHearts
  decEq Spades Diamonds = No spadesDiamonds
  decEq Hearts Clubs = No heartsClubs
  decEq Hearts Spades = No heartsSpades
  decEq Hearts Hearts = Yes Refl
  decEq Hearts Diamonds = No heartsDiamonds
  decEq Diamonds Clubs = No diamondsClubs
  decEq Diamonds Spades = No diamondsSpades
  decEq Diamonds Hearts = No diamondsHearts
  decEq Diamonds Diamonds = Yes Refl

pipsDontMatch : (contra : (v1 = v2) -> Void) -> (Pip v1 = Pip v2) -> Void
pipsDontMatch contra Refl = contra Refl

pipJack : (Pip v = Jack) -> Void
pipJack Refl impossible

pipQueen : (Pip v = Queen) -> Void
pipQueen Refl impossible

pipKing : (Pip v = King) -> Void
pipKing Refl impossible

pipAce : (Pip v = Ace) -> Void
pipAce Refl impossible

jackPip : (Jack = Pip v) -> Void
jackPip Refl impossible

jackQueen : (Jack = Queen) -> Void
jackQueen Refl impossible

jackKing : (Jack = King) -> Void
jackKing Refl impossible

jackAce : (Jack = Ace) -> Void
jackAce Refl impossible

queenPip : (Queen = Pip v) -> Void
queenPip Refl impossible

queenJack : (Queen = Jack) -> Void
queenJack Refl impossible

queenKing : (Queen = King) -> Void
queenKing Refl impossible

queenAce : (Queen = Ace) -> Void
queenAce Refl impossible

kingPip : (King = Pip v) -> Void
kingPip Refl impossible

kingJack : (King = Jack) -> Void
kingJack Refl impossible

kingQueen : (King = Queen) -> Void
kingQueen Refl impossible

kingAce : (King = Ace) -> Void
kingAce Refl impossible

acePip : (Ace = Pip v) -> Void
acePip Refl impossible

aceJack : (Ace = Jack) -> Void
aceJack Refl impossible

aceQueen : (Ace = Queen) -> Void
aceQueen Refl impossible

aceKing : (Ace = King) -> Void
aceKing Refl impossible

export DecEq Value where
  decEq (Pip v1) (Pip v2) = case decEq v1 v2 of
                                 (Yes prf) => Yes (rewrite prf in Refl)
                                 (No contra) => No (pipsDontMatch contra)
  decEq (Pip v) Jack = No pipJack
  decEq (Pip v) Queen = No pipQueen
  decEq (Pip v) King = No pipKing
  decEq (Pip v) Ace = No pipAce
  decEq Jack (Pip v) = No jackPip
  decEq Jack Jack = Yes Refl
  decEq Jack Queen = No jackQueen
  decEq Jack King = No jackKing
  decEq Jack Ace = No jackAce
  decEq Queen (Pip v) = No queenPip
  decEq Queen Jack = No queenJack
  decEq Queen Queen = Yes Refl
  decEq Queen King = No queenKing
  decEq Queen Ace = No queenAce
  decEq King (Pip v) = No kingPip
  decEq King Jack = No kingJack
  decEq King Queen = No kingQueen
  decEq King King = Yes Refl
  decEq King Ace = No kingAce
  decEq Ace (Pip v) = No acePip
  decEq Ace Jack = No aceJack
  decEq Ace Queen = No aceQueen
  decEq Ace King = No aceKing
  decEq Ace Ace = Yes Refl

export valueToNum : Value -> Nat
valueToNum (Pip v) = v
valueToNum Jack = 11
valueToNum Queen = 12
valueToNum King = 13
valueToNum Ace = 14

export cardValue : Card -> Nat
cardValue (MkCard value suit) = valueToNum value

--=======================================================================================================
-- isConsecutive
--=======================================================================================================
pipsNonConsec : (contra : (v = S k) -> Void) -> ConsecComp (MkCard (Pip v) suit) (MkCard (Pip k) suit1) -> Void
pipsNonConsec contra PipConsec = contra Refl

pipThenJack : ConsecComp (MkCard (Pip v) suit) (MkCard Jack suit1) -> Void
pipThenJack PipConsec impossible
pipThenJack JackTen impossible
pipThenJack QueenJack impossible
pipThenJack KingQueen impossible
pipThenJack AceKing impossible

pipThenQueen : ConsecComp (MkCard (Pip v) suit) (MkCard Queen suit1) -> Void
pipThenQueen PipConsec impossible
pipThenQueen JackTen impossible
pipThenQueen QueenJack impossible
pipThenQueen KingQueen impossible
pipThenQueen AceKing impossible

pipThenKing : ConsecComp (MkCard (Pip v) suit) (MkCard King suit1) -> Void
pipThenKing PipConsec impossible
pipThenKing JackTen impossible
pipThenKing QueenJack impossible
pipThenKing KingQueen impossible
pipThenKing AceKing impossible

pipThenAce : ConsecComp (MkCard (Pip v) suit) (MkCard Ace suit1) -> Void
pipThenAce PipConsec impossible
pipThenAce JackTen impossible
pipThenAce QueenJack impossible
pipThenAce KingQueen impossible
pipThenAce AceKing impossible

jackThenNotTen : (contra : (v = the Nat (fromInteger 10)) -> Void) -> ConsecComp (MkCard Jack suit) (MkCard (Pip v) suit1) -> Void
jackThenNotTen contra JackTen = contra Refl

bothJacks : ConsecComp (MkCard Jack suit) (MkCard Jack suit1) -> Void
bothJacks PipConsec impossible
bothJacks JackTen impossible
bothJacks QueenJack impossible
bothJacks KingQueen impossible
bothJacks AceKing impossible

jackThenQueen : ConsecComp (MkCard Jack suit) (MkCard Queen suit1) -> Void
jackThenQueen PipConsec impossible
jackThenQueen JackTen impossible
jackThenQueen QueenJack impossible
jackThenQueen KingQueen impossible
jackThenQueen AceKing impossible

jackThenKing : ConsecComp (MkCard Jack suit) (MkCard King suit1) -> Void
jackThenKing PipConsec impossible
jackThenKing JackTen impossible
jackThenKing QueenJack impossible
jackThenKing KingQueen impossible
jackThenKing AceKing impossible

jackThenAce : ConsecComp (MkCard Jack suit) (MkCard Ace suit1) -> Void
jackThenAce PipConsec impossible
jackThenAce JackTen impossible
jackThenAce QueenJack impossible
jackThenAce KingQueen impossible
jackThenAce AceKing impossible

queenThenPip : ConsecComp (MkCard Queen suit) (MkCard (Pip v) suit1) -> Void
queenThenPip PipConsec impossible
queenThenPip JackTen impossible
queenThenPip QueenJack impossible
queenThenPip KingQueen impossible
queenThenPip AceKing impossible

queenThenQueen : ConsecComp (MkCard Queen suit) (MkCard Queen suit1) -> Void
queenThenQueen PipConsec impossible
queenThenQueen JackTen impossible
queenThenQueen QueenJack impossible
queenThenQueen KingQueen impossible
queenThenQueen AceKing impossible

queenThenKing : ConsecComp (MkCard Queen suit) (MkCard King suit1) -> Void
queenThenKing PipConsec impossible
queenThenKing JackTen impossible
queenThenKing QueenJack impossible
queenThenKing KingQueen impossible
queenThenKing AceKing impossible

queenThenAce : ConsecComp (MkCard Queen suit) (MkCard Ace suit1) -> Void
queenThenAce PipConsec impossible
queenThenAce JackTen impossible
queenThenAce QueenJack impossible
queenThenAce KingQueen impossible
queenThenAce AceKing impossible

kingThenPip : ConsecComp (MkCard King suit) (MkCard (Pip v) suit1) -> Void
kingThenPip PipConsec impossible
kingThenPip JackTen impossible
kingThenPip QueenJack impossible
kingThenPip KingQueen impossible
kingThenPip AceKing impossible

kingThenJack : ConsecComp (MkCard King suit) (MkCard Jack suit1) -> Void
kingThenJack PipConsec impossible
kingThenJack JackTen impossible
kingThenJack QueenJack impossible
kingThenJack KingQueen impossible
kingThenJack AceKing impossible

kingThenKing : ConsecComp (MkCard King suit) (MkCard King suit1) -> Void
kingThenKing PipConsec impossible
kingThenKing JackTen impossible
kingThenKing QueenJack impossible
kingThenKing KingQueen impossible
kingThenKing AceKing impossible

kingThenAce : ConsecComp (MkCard King suit) (MkCard Ace suit1) -> Void
kingThenAce PipConsec impossible
kingThenAce JackTen impossible
kingThenAce QueenJack impossible
kingThenAce KingQueen impossible
kingThenAce AceKing impossible

aceThenPip : ConsecComp (MkCard Ace suit) (MkCard (Pip v) suit1) -> Void
aceThenPip PipConsec impossible
aceThenPip JackTen impossible
aceThenPip QueenJack impossible
aceThenPip KingQueen impossible
aceThenPip AceKing impossible

aceThenJack : ConsecComp (MkCard Ace suit) (MkCard Jack suit1) -> Void
aceThenJack PipConsec impossible
aceThenJack JackTen impossible
aceThenJack QueenJack impossible
aceThenJack KingQueen impossible
aceThenJack AceKing impossible

aceThenQueen : ConsecComp (MkCard Ace suit) (MkCard Queen suit1) -> Void
aceThenQueen PipConsec impossible
aceThenQueen JackTen impossible
aceThenQueen QueenJack impossible
aceThenQueen KingQueen impossible
aceThenQueen AceKing impossible

aceThenAce : ConsecComp (MkCard Ace suit) (MkCard Ace suit1) -> Void
aceThenAce PipConsec impossible
aceThenAce JackTen impossible
aceThenAce QueenJack impossible
aceThenAce KingQueen impossible
aceThenAce AceKing impossible

isConsecComp: (x:Card) -> (y: Card) -> Dec (ConsecComp x y)
isConsecComp (MkCard (Pip v) _) (MkCard (Pip k) _) = (case decEq v (S k) of
                                                               (Yes prf) => Yes (rewrite prf in PipConsec)
                                                               (No contra) => No (pipsNonConsec contra))
isConsecComp (MkCard (Pip v) _) (MkCard Jack _) = No pipThenJack
isConsecComp (MkCard (Pip v) _) (MkCard Queen _) = No pipThenQueen
isConsecComp (MkCard (Pip v) _) (MkCard King _) = No pipThenKing
isConsecComp (MkCard (Pip v) _) (MkCard Ace _) = No pipThenAce
isConsecComp (MkCard Jack _) (MkCard (Pip v) _) = case decEq v (the Nat 10) of
                                                       (Yes prf) => Yes (rewrite prf in JackTen)
                                                       (No contra) => No (jackThenNotTen contra)
isConsecComp (MkCard Jack _) (MkCard Jack _) = No bothJacks
isConsecComp (MkCard Jack _) (MkCard Queen _) = No jackThenQueen
isConsecComp (MkCard Jack _) (MkCard King _) = No jackThenKing
isConsecComp (MkCard Jack _) (MkCard Ace _) = No jackThenAce
isConsecComp (MkCard Queen _) (MkCard (Pip v) _) = No queenThenPip
isConsecComp (MkCard Queen _) (MkCard Jack _) = Yes QueenJack
isConsecComp (MkCard Queen _) (MkCard Queen _) = No queenThenQueen
isConsecComp (MkCard Queen _) (MkCard King _) = No queenThenKing
isConsecComp (MkCard Queen _) (MkCard Ace _) = No queenThenAce
isConsecComp (MkCard King _) (MkCard (Pip v) _) = No kingThenPip
isConsecComp (MkCard King _) (MkCard Jack _) = No kingThenJack
isConsecComp (MkCard King _) (MkCard Queen _) = Yes KingQueen
isConsecComp (MkCard King _) (MkCard King _) = No kingThenKing
isConsecComp (MkCard King _) (MkCard Ace _) = No kingThenAce
isConsecComp (MkCard Ace _) (MkCard (Pip v) _) = No aceThenPip
isConsecComp (MkCard Ace _) (MkCard Jack _) = No aceThenJack
isConsecComp (MkCard Ace _) (MkCard Queen _) = No aceThenQueen
isConsecComp (MkCard Ace _) (MkCard King _) = Yes AceKing
isConsecComp (MkCard Ace _) (MkCard Ace _) = No aceThenAce

headNotConsec : (contra : ConsecComp x x1 -> Void) -> Consecutive (x :: (x1 :: xs)) -> Void
headNotConsec contra (Comp x y z) = contra z

restIsNotConsec : (contra : Consecutive (x1 :: xs) -> Void) -> Consecutive (x :: (x1 :: xs)) -> Void
restIsNotConsec contra (Comp x y z) = contra y

export isConsecutive: (x:Vect n Card) -> Dec (Consecutive x)
isConsecutive [] = Yes ConEmpty
isConsecutive (x :: []) = Yes (ConSingle x)
isConsecutive (x :: x1 :: xs) = case isConsecComp x x1 of
                                     (Yes consec_prf) => (case isConsecutive (x1::xs) of
                                                               (Yes prf) => Yes (Comp x prf consec_prf)
                                                               (No contra) => No (restIsNotConsec contra))
                                     (No contra) => No (headNotConsec contra)

export Show Value where
  show (Pip v) = show v
  show Jack = "Jack"
  show Queen = "Queen"
  show King = "King"
  show Ace = "Ace"

Show Suit where
  show Clubs = "Clubs"
  show Spades = "Spades"
  show Hearts = "Hearts"
  show Diamonds = "Diamonds"

export Show Card where
  show (MkCard value suit) = "the " ++ (show value) ++ " of " ++ (show suit)


text:
module Control.Comonad.Traced.Traced

import Control.Comonad
import Control.Comonad.Trans
import Control.Monad.Identity

%default total

public export
record TracedT (m : Type) (w : Type -> Type) (a : Type) where
  constructor MkTracedT
  runTracedT : w (m -> a)

public export
Traced : (m : Type) -> (a : Type) -> Type
Traced m = TracedT m Identity

public export %inline
traced : (m -> a) -> Traced m a
traced f = MkTracedT (Id f)

public export %inline
runTraced : Traced m a -> m -> a
runTraced (MkTracedT (Id f)) = f

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export %inline
listen : Functor w => TracedT m w a -> TracedT m w (a, m)
listen = record { runTracedT $= map (\f,m => (f m, m)) }

public export %inline
listens : Functor w => (m -> b) -> TracedT m w a -> TracedT m w (a, b)
listens g = record { runTracedT $= map (\f,m => (f m, g m)) }

public export %inline
censor : Functor w => (m -> m) -> TracedT m w a -> TracedT m w a
censor g = record { runTracedT $= map (. g) }

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

appEnv : (s -> a -> b) -> (s -> a) -> s -> b
appEnv ff fa s = ff s (fa s)

public export %inline
Functor w => Functor (TracedT m w) where
  map f = record { runTracedT $= map (f .) }

public export %inline
Applicative w => Applicative (TracedT m w) where
  pure = MkTracedT . pure . const
  MkTracedT wf <*> MkTracedT wa = MkTracedT (map appEnv wf <*> wa)

public export %inline
(Comonad w, Monoid m) => Comonad (TracedT m w) where
  extract (MkTracedT wf) = extract wf neutral
  extend f =
    record { runTracedT $= extend (\w,m => f (MkTracedT $ map (. (<+> m)) w)) }

public export %inline
(ComonadApply w, Monoid m) => ComonadApply (TracedT m w) where
  MkTracedT wf <@> MkTracedT wa = MkTracedT (map appEnv wf <@> wa)

public export %inline
Monoid m => ComonadTrans (TracedT m) where
  lower = map ($ neutral) . runTracedT


text:
module Data.Nat.Extra

import Data.Nat

public export
(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat
(-) m n {smaller} = minus m n

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module FreeGroup

import Monoid
import Group
import congruence

%access public export

||| The type of free groups generated by elements of a type
data FreeGroup : (typ : Type) -> Type where
    Iden : (typ : Type) -> (FreeGroup typ)
    Incl : typ -> (FreeGroup typ)
    Inv_incl : typ -> (FreeGroup typ)
    (*) : {typ : Type} -> (FreeGroup typ) -> (FreeGroup typ) -> (FreeGroup typ)

{-
data EqFree : {typ : Type} -> (FreeGroup typ) -> (FreeGroup typ) -> Type where
    same : {typ : Type} -> {a : (FreeGroup typ)} -> (EqFree a a)
    inv_eq : {typ : Type} -> {a : typ} -> ( EqFree (Incl a) (Inv_incl a) )
    assoc_eq : {typ : Type} -> (a, b, c : (FreeGroup typ)) -> ( EqFree ((a*b)*c) (a*(b*c)) )

Transport : {typ : Type} -> {P : (FreeGroup typ) -> Type} -> {a, b : (FreeGroup typ)} ->
            (EqFree a b) -> (P a) -> (P b)

Translation : {typ : Type} -> {a, b : (FreeGroup typ)} -> (EqFree a b) -> (a = b)
-}

||| Group axioms
id_eq : {typ : Type} -> (a : (FreeGroup typ)) -> ( a * (Iden typ)= a , (Iden typ) * a = a )
inv_eq : {typ : Type} -> (a : typ) -> ( (Incl a) * (Inv_incl a) = (Iden typ), (Inv_incl a) * (Incl a) = (Iden typ))
assoc_eq : {typ : Type} -> (a, b, c : (FreeGroup typ)) -> ( (a*b)*c  = a*(b*c) )

--total
||| A proof that each element of the free group has an inverse

FreeInverse : (typ : Type) -> (a : (FreeGroup typ)) -> ( b : (FreeGroup typ) ** ((a * b = (Iden typ)) , (b * a = (Iden typ))))
FreeInverse typ (Iden typ) = ((Iden typ) ** (id_eq (Iden typ)))
FreeInverse typ (Incl a) = ((Inv_incl a) ** (inv_eq a))
FreeInverse typ (a * b) = let

    a_inv_pf = FreeInverse typ a
    b_inv_pf = FreeInverse typ b
    a_inv = (fst a_inv_pf)
    b_inv = (fst b_inv_pf)
    a_pf = (snd a_inv_pf)
    b_pf = (snd b_inv_pf)
    pf1 = assoc_eq b b_inv a_inv
    pf2 = congruence (FreeGroup typ) (FreeGroup typ) (b * b_inv) (Iden typ) (\c => (c * a_inv)) (fst b_pf)
    pf3 = (snd (id_eq (a_inv)))
    pf4 = trans pf2 pf3
    pf5 = congruence (FreeGroup typ) (FreeGroup typ) ((b * b_inv) * a_inv) a_inv (\c => (a * c)) pf4
    pf6 = trans pf5 (fst a_pf)
    pf7 = assoc_eq a (b * b_inv) a_inv
    pf8 = assoc_eq a b b_inv
    pf9 = congruence (FreeGroup typ) (FreeGroup typ) ((a * b) * b_inv) (a * (b * b_inv)) (\c => (c * a_inv)) pf8
    pf10 = assoc_eq (a*b) b_inv a_inv
    pf11 = trans (sym pf10) pf9
    pf12 = trans pf11 pf7
    pf13 = trans pf12 pf6

    in
    ((b_inv * a_inv) ** (pf13, ?rhs))

{-
FreeGroup_is_Group : {typ : Type} -> (IsGroup (FreeGroup typ) (*))
FreeGroup_is_Group = ( assoc_eq , ((Iden ** (\b => (id_eq {a = b}))),
                                  ((Iden ** (\b => (id_eq {a = b}))) ** (\b => (?rhs)))))
-}


text:
module permutation_with_constructors

import Data.Vect

--- Goal - To define permutations with constructors

data Perm : Nat -> Type where
    Idt : (n : Nat) -> Perm n -- Identity permutation
    Flip : (n : Nat) -> Perm n -- [1 2 3 ... n]-> [2 1 3 ... n]
    Shift : (n : Nat) -> Perm n -- [1 2 3 .. n] -> [n 1 2 .. (n-1)]
    CPerm : (n : Nat) -> Perm n -> Perm n -> Perm n

total
applyPerm : (n : Nat) -> (t : Type) -> (Perm n) -> (Vect n t) -> (Vect n t)
applyPerm Z typ p v = v
applyPerm (S Z) typ p v = v
applyPerm n typ (Idt n) v = v
applyPerm (S (S k)) t (Flip (S (S k))) v = (index (FS FZ) v) :: ( (index FZ v) :: (tail(tail v)))
applyPerm (S (S k)) t (Shift (S (S k))) v = reverse( (index FZ v) :: (reverse (tail v)))
applyPerm n t (CPerm n f g) v = applyPerm n t f (applyPerm n t g v)


text:
module Utils.String

import Data.Bits
import Data.List
import Data.String

export
tail : String -> String
tail "" = ""
tail str = assert_total (strTail str)

export
splitBy : Char -> String -> (String, String)
splitBy sep = mapSnd tail . break (== sep)

utf8_bytelen : Bits8 -> Maybe (Bits8, Nat)
utf8_bytelen x =
  if (x .&. 0b01111111) == x then Just (x, 0) -- ascii
    else if (shiftR x 5) == 0b110   then Just (x .&. 0b0011111, 1)
    else if (shiftR x 4) == 0b1110  then Just (x .&. 0b0001111, 2)
    else if (shiftR x 3) == 0b11110 then Just (x .&. 0b0000111, 3)
    else Nothing

utf8_unmask : Bits8 -> Maybe Bits8
utf8_unmask x = const (x .&. 0b00111111) <$> guard (shiftR x 6 == 0b10)

utf8_pushbits : Integer -> List Bits8 -> Integer
utf8_pushbits acc [] = acc
utf8_pushbits acc (x::xs) = utf8_pushbits ((shiftL acc 6) .|. (cast x)) xs

public export
utf8_pack : List Bits8 -> Maybe String
utf8_pack = go []
  where
    go : List Char -> List Bits8 -> Maybe String
    go acc [] = Just $ pack $ reverse acc
    go acc (x :: xs) = do
      (x, l) <- utf8_bytelen x
      let (y,ys) = splitAt l xs
      guard (length y == l)
      y <- traverse utf8_unmask y
      let c = utf8_pushbits (cast x) y
      go ((cast c) :: acc) ys

utf8_char_bytelen : Integer -> (Nat, Bits8)
utf8_char_bytelen x =
  if x <= 0x7F then (0, 0)
    else if x <= 0x07FF then (1, 0b11000000)
    else if x <= 0xFFFF then (2, 0b11100000)
    else (3, 0b11110000)

utf8_encode : Integer -> List Bits8
utf8_encode i =
  case utf8_char_bytelen i of
    (0, _) => [ cast i ]
    (n, m) => loop [] i n m where
      loop : List Bits8 -> Integer -> Nat -> Bits8 -> List Bits8
      loop acc i Z mask = (cast i .|. mask) :: acc
      loop acc i (S n) mask =
        let b = cast (i .&. 0b111111) .|. 0b10000000
            i' = shiftR i 6
        in loop (b :: acc) i' n mask

public export
utf8_unpack : String -> List Bits8
utf8_unpack str = unpack str >>= utf8_encode . cast


text:
module Commons.Options.ArgParse.Lexer

import Text.Lexer

import public Commons.Text.Lexer.Run

%default total
%access private

public export
data Token = SFlag   String
           | LFlag   String
           | Equals String
           | Quoted String
           | WS String
           | Arg String
           | Unknown String
           | EndInput

export
Show Token where
  show (LFlag    x) = unwords ["LFlag",   show x]
  show (SFlag    x) = unwords ["SFlag",   show x]
  show (Equals   x) = unwords ["Equals", show x]
  show (Quoted  x) = unwords ["Quoted", show x]
  show (WS      x) = unwords ["WS",     show x]
  show (Arg    x) = unwords ["Arg",     show x]
  show (Unknown x) = unwords ["BAD TOKEN", show x]
  show EndInput = "ENDINPUT"

ch : Lexer
ch = pred (isAlphaNum)

str : Lexer
str = some (pred isAlphaNum)

shortFlag : Lexer
shortFlag = is '-' <+> ch

longFlag : Lexer
longFlag = is '-' <+> is '-' <+> str

equals : Lexer
equals = is '='

arg : Lexer
arg = any <+> manyUntil space any

rawTokens : TokenMap Token
rawTokens =
  [ (space, WS)
  , (stringLit, Quoted)
  , (longFlag, LFlag)
  , (shortFlag, SFlag)
  , (equals, Equals)
  , (arg, Arg)
  , (symbol, Unknown)
  ]

keep : TokenData Token -> Bool
keep t with (tok t)
  keep t | (WS x) = False
  keep t | _      = True

export
ArgParseLexer : Lexer Token
ArgParseLexer = MkLexer rawTokens keep EndInput

export
lexArgParseStr : String -> Either LexError (List (TokenData Token))
lexArgParseStr = lexString ArgParseLexer

export
lexArgParseFile : String -> IO $ Either LexFail (List (TokenData Token))
lexArgParseFile = lexFile ArgParseLexer

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Language.LSP.Message.References

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

%language ElabReflection
%default total

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

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

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
public export
record ReferenceContext where
  constructor MkReferenceContext
  includeDeclaration : Bool
%runElab deriveJSON defaultOpts `{{ReferenceContext}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_references
public export
record ReferenceParams where
  constructor MkReferenceParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
  context            : ReferenceContext
%runElab deriveJSON defaultOpts `{{ReferenceParams}}


text:
module JSArrays

import Types

-- This creates a new normal javascript array for you to use.
createJSArray : IO JSArray
createJSArray = do
  a <- mkForeign (FFun "new Array()" [] FPtr)
  return (MkJSArray a)

-- This pushes a floating point value onto the array
pushFloat : JSArray -> Float -> IO JSArray
pushFloat (MkJSArray x) i = do
  _<- mkForeign (FFun "%0.push(%1)" [FPtr,FFloat] FInt) x i
  return (MkJSArray x)

-- This pushes an integer value onto the array
pushInt : JSArray -> Int -> IO JSArray
pushInt (MkJSArray x) i = do
  _<- mkForeign (FFun "%0.push(%1)" [FPtr,FInt] FInt) x i
  return (MkJSArray x)

-- This creates a javascript array of floats from a List Float
fromFloatList : List Float -> JSArray -> IO JSArray
fromFloatList [] (MkJSArray x) = return (MkJSArray x)
fromFloatList (y :: xs) jsA = do
  njsA <- pushFloat jsA y
  fromFloatList xs njsA

-- This takes a javascript array and attempts to create a specific JS
-- Float32Array.
createF32Array : JSArray -> IO F32Array
createF32Array (MkJSArray xs) = do
  ys <- mkForeign (FFun "new Float32Array(%0)" [FPtr] FPtr) xs
  return (MkF32Array ys)

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Minecraft.Core.Univ.Level

import Data.IOArray
import public Minecraft.Data.Type.As
import public Minecraft.Core.Block.Export
import public Minecraft.Core.Univ
import public Minecraft.Core.Univ.Level.Gen
import public Minecraft.Core.Univ.Level.Pos

%default total

%foreign "C:block_at,level"
block_at : (level_id : String)
        -> (chunk_id : Bits64)
        -> (x : Bits8)
        -> (y : Bits8)
        -> (z : Bits8)
        -> Int -- block data index
%foreign "C:put_block,level"
put_block : (level_id : String)
         -> (chunk_id : Bits64)
         -> (x : Bits8)
         -> (y : Bits8)
         -> (z : Bits8)
         -> (new_val : Int)
         -> Int -- old val
%foreign "C:save_chunk,level"
save_chunk : (level_id : String)
          -> (chunk_id : Bits64)
          -> (identifier : Int -> String)
          -> (serialize : Int -> String)
          -> ()
%foreign "C:save_level,level"
save_level : (level_id : String)
          -> (serialize : Int -> String)
          -> ()
%foreign "C:load_level,level"
load_level : (level_id : String)
          -> (load_blk : (idx : Int) -> (identifier : String) -> (serialized : String) -> ())
          -> ()
-- %foreign "C:load_chunk,level"
-- load_chunk : (level_id : String)
--           -> (chunk_id : Bits64)
--           -> ()

public export
Eq (As Block) where
  x == y = if Block.id @{x.ctx.impl} == Block.id @{y.ctx.impl}
    then (==) @{blkEq x.ctx.impl} x.val (believe_me y.val)
    else False
  where
    blkEq : Block a -> Eq a
    blkEq = %search

find : Eq a => a -> IOArray a -> IO (Maybe Int)
find x xs = find' (integerToNat (cast (max xs))) where
  find' : Nat -> IO (Maybe Int)
  find' Z = pure Nothing
  find' (S n) = do
    y <- readArray xs (cast (S n))
    if Just x == y
      then pure (Just (cast (S n)))
      else find' n

export
record Level where
  constructor MkLevel
  id : String
  seed : Bits64
  univ : Univ
  voidBlock : As Block
  gen : LevelGen seed univ voidBlock
  blocks : IOArray (As Block)
  {auto blocksTop : Int}

-- TODO: dynamic growth logic for level.blocks
export
updateAt : Level -> Pos -> As Block -> IO Level
updateAt level pos blk = do
  idx <- find blk level.blocks
  case idx of
    Just idx => do
      pure $ put_block level.id pos.chunk pos.x pos.y pos.z idx
      pure level
    Nothing  => do
      writeArray level.blocks level.blocksTop blk
      pure $ put_block level.id pos.chunk pos.x pos.y pos.z level.blocksTop
      pure $ record {blocksTop $=(+1)} level

export
blockAt : Level -> Pos -> IO (As Block)
blockAt level pos = do
  case block_at level.id pos.chunk pos.x pos.y pos.z of
    0 => do
      blk <- pure (level.gen.blockAt pos)
      updateAt level pos blk
      pure blk
    n => do
      blk <- readArray level.blocks n
      case blk of
        Just blk => pure blk
        Nothing  => pure level.voidBlock

serializeBlock : (level : Level)
              -> (idx : Int)
              -> String
serializeBlock level idx = case unsafePerformIO (readArray level.blocks idx) of
  Just blk => serialize' blk
  Nothing  => serialize' level.voidBlock
  where
    serialize' : As Block -> String
    serialize' blk = show $ Serialize.serialize @{blockSerialize blk.ctx.impl} blk.val

identifier : (level : Level)
          -> (idx : Int)
          -> String
identifier level idx = case unsafePerformIO (readArray level.blocks idx) of
  Just blk => identifier' blk
  Nothing  => identifier' level.voidBlock
  where
    identifier' : As Block -> String
    identifier' blk = Serialize.identifier @{blockSerialize blk.ctx.impl}

deserializeBlock : (level : Level)
                => (idx : Int)
                -> (identifier : String)
                -> (serialized : String)
                -> ()
deserializeBlock @{level} idx identifier serialized =
  unsafePerformIO $ writeArray level.blocks idx blk
  where
    context : Maybe (Ctx Deserialize)
    context = level.univ.exists identifier

    blk : As Block
    blk = case context of
      Just ctx => case level.univ.reflect ctx.type of
        Just vtbl => case parse serialized of
          Just json => case vtable @{vtbl} (Block ctx.type) of
            Just impl => case Deserialize.deserialize @{ctx.impl} json of
              Just block => new ctx.type block @{impl}
              Nothing => level.voidBlock
            Nothing => level.voidBlock
          Nothing => level.voidBlock
        Nothing => level.voidBlock
      Nothing => level.voidBlock

export
saveChunk : (level : Level)
         -> (chunkId : Bits64)
         -> IO ()
saveChunk level chunkId = do
  pure $ save_chunk level.id chunkId (identifier level) (serializeBlock level)

export
saveLevel : (level : Level) -> IO ()
saveLevel level = pure $ save_level level.id (serializeBlock level)

export
loadLevel : (level : Level) -> IO Level
loadLevel level = do
  pure $ load_level level.id (deserializeBlock @{level})
  pure level

export
level : (id : String)
     -> (seed : Bits64)
     -> (univ : Univ)
     -> (voidBlock : As Block)
     -> (gen : LevelGen seed univ voidBlock)
     -> IO Level
level id seed univ voidBlock gen = do
  blocks <- newArray 256
  writeArray blocks 1 voidBlock
  loadLevel $ MkLevel id seed univ voidBlock gen blocks {blocksTop = 1}

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
import Text.Parser

import Data.Bool

data YamlToken : Type where [external]

Parser : Bool -> Type -> Type
Parser = Grammar (Token YamlToken)

countOcc : {c : Bool} -> Parser c a -> Parser False Nat
countOcc p = rewrite sym $ andFalseFalse (c || False) in
             (S <$ p <*> countOcc p) <|> pure Z