text:
module Main

import System

countDown : Int -> IO ()
countDown 0 = putStrLn "\n\n-- Timer Finished --"
countDown n = do putStrLn $ show n
                 secondDelay
                 countDown (n - 1)
              where secondDelay : IO ()
                    secondDelay = usleep 1000000

getCountdownNumIO : IO (Int)
getCountdownNumIO = do putStr "Enter how many seconds you want to set the timer for: "
                       inp <- getLine
                       case inp of
                             "0" => putStrLn "Please input a number greater than zero." >>= \ _ => getCountdownNumIO
                             _ => case (the Int (cast inp)) of
                                       0 => putStrLn "Please input a number." >>= \ _ => getCountdownNumIO
                                       i => pure i

getCountdownNum : (args : List (String)) -> IO Int
getCountdownNum args = case Prelude.List.index' 1 args of
                            Nothing => getCountdownNumIO
                            Just n => if cast n == 0 then getCountdownNumIO else pure $ cast n

getCommandFromFile : IO (String)
getCommandFromFile = do Right cmd <- readFile "command.sh" | Left er => pure ""
                        pure cmd

main : IO ()
main = do
       args <- getArgs
       putStrLn "Welcome to your favorite cli countdown timer!"
       cdNum <- getCountdownNum args
       putStrLn "---\n"
       countDown cdNum
       cmd <- getCommandFromFile
       system cmd
       pure ()

max_stars_repo_name: robkorn/idris-cli-timer

max_issues_repo_name: robkorn/idris-cli-timer

max_forks_repo_name: robkorn/idris-cli-timer


text:
module NCurses.Core

import NCurses.Types

%default total

libncurses : String -> String
libncurses fn = "C:" ++ fn ++ ",libncurses 6"

libhelper : String -> String
libhelper fn = "C:" ++ fn ++ ",libncurses-idris"

%foreign libncurses "cbreak"
prim__cBreak : PrimIO ()

%foreign libncurses "noecho"
prim__noEcho : PrimIO ()

%foreign libncurses "keypad"
prim__keypad : AnyPtr -> Int -> PrimIO ()

%foreign libncurses "nodelay"
prim__noDelay : AnyPtr -> Int -> PrimIO ()

%foreign libncurses "curs_set"
prim__setCursorVisibility : Int -> PrimIO ()

%foreign libncurses "getch"
prim__getCh : PrimIO Int8

%foreign libncurses "start_color"
prim__startColor : PrimIO ()

%foreign libncurses "initscr"
prim__initScr : PrimIO ()

%foreign libncurses "endwin"
prim__endWin : PrimIO ()

%foreign libhelper "std_win"
prim__stdWindow : PrimIO AnyPtr

%foreign libncurses "newwin"
prim__newWindow : Int -> Int -> Int -> Int -> PrimIO AnyPtr

%foreign libncurses "getmaxx"
prim__maxXWindow : AnyPtr -> PrimIO Int

%foreign libncurses "getmaxy"
prim__maxYWindow : AnyPtr -> PrimIO Int

%foreign libncurses "refresh"
prim__refresh : PrimIO ()

%foreign libncurses "wrefresh"
prim__refreshWindow : AnyPtr -> PrimIO ()

%foreign libncurses "clear"
prim__clear : PrimIO ()

%foreign libncurses "wclear"
prim__clearWindow : AnyPtr -> PrimIO ()

%foreign libncurses "waddch"
prim__waddCh : AnyPtr -> Char -> PrimIO ()

%foreign libncurses "addch"
prim__addCh : Char -> PrimIO ()

%foreign libncurses "wvline"
prim__wvline : AnyPtr -> Char -> Int -> PrimIO ()

%foreign libncurses "vline"
prim__vline : Char -> Int -> PrimIO ()

%foreign libncurses "whline"
prim__whline : AnyPtr -> Char -> Int -> PrimIO ()

%foreign libncurses "hline"
prim__hline : Char -> Int -> PrimIO ()

%foreign libncurses "inch"
prim__inch : PrimIO Char

%foreign libncurses "winch"
prim__winch : AnyPtr -> PrimIO Char

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvinch"
prim__mvinch : Int -> Int -> PrimIO Char

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvwinch"
prim__mvwinch : AnyPtr -> Int -> Int -> PrimIO Char

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvwvline"
prim__mvwvline : AnyPtr -> Int -> Int -> Char -> Int -> PrimIO ()

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvvline"
prim__mvvline : Int -> Int -> Char -> Int -> PrimIO ()

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvwhline"
prim__mvwhline : AnyPtr -> Int -> Int -> Char -> Int -> PrimIO ()

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvhline"
prim__mvhline : Int -> Int -> Char -> Int -> PrimIO ()

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvaddch"
prim__mvaddch : Int -> Int -> Char -> PrimIO ()

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
%foreign libncurses "mvwaddch"
prim__mvwaddch : AnyPtr -> Int -> Int -> Char -> PrimIO ()

||| move to row and column given and print
||| the given string.
|||
||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
|||
||| The second to last argument is a format string but
||| its best to just always pass strings ("%s").
%foreign libncurses "mvprintw"
prim__mvPrint : Int -> Int -> String -> String -> PrimIO ()

%foreign libncurses "mvwprintw"
prim__mvPrintWindow : AnyPtr -> Int -> Int -> String -> String -> PrimIO ()

%foreign libncurses "move"
prim__move : Int -> Int -> PrimIO ()

%foreign libncurses "mvchgat"
prim__mvChangeAt : Int -> Int -> Int -> Int -> Int -> AnyPtr -> PrimIO ()

%foreign libncurses "mvwchgat"
prim__mvChangeAtWindow : AnyPtr -> Int -> Int -> Int -> Int -> Int -> AnyPtr -> PrimIO ()

%foreign libncurses "attrset"
prim__setAttr : Int -> PrimIO ()

%foreign libncurses "wattrset"
prim__setAttrWindow : AnyPtr -> Int -> PrimIO ()

%foreign libhelper "normal_attr"
prim__normalAttr : PrimIO Int

%foreign libhelper "underline_attr"
prim__underlineAttr : PrimIO Int

%foreign libhelper "standout_attr"
prim__standoutAttr : PrimIO Int

%foreign libhelper "reverse_attr"
prim__reverseAttr : PrimIO Int

%foreign libhelper "blink_attr"
prim__blinkAttr : PrimIO Int

%foreign libhelper "dim_attr"
prim__dimAttr : PrimIO Int

%foreign libhelper "bold_attr"
prim__boldAttr : PrimIO Int

%foreign libhelper "protected_attr"
prim__protectedAttr : PrimIO Int

%foreign libhelper "invisible_attr"
prim__invisibleAttr : PrimIO Int

%foreign libhelper "color_pair_attr"
prim__colorPairAttr : Int -> PrimIO Int

%foreign libhelper "black_color"
prim__blackColor : PrimIO Int

%foreign libhelper "red_color"
prim__redColor : PrimIO Int

%foreign libhelper "green_color"
prim__greenColor : PrimIO Int

%foreign libhelper "yellow_color"
prim__yellowColor : PrimIO Int

%foreign libhelper "blue_color"
prim__blueColor : PrimIO Int

%foreign libhelper "magenta_color"
prim__magentaColor : PrimIO Int

%foreign libhelper "cyan_color"
prim__cyanColor : PrimIO Int

%foreign libhelper "white_color"
prim__whiteColor : PrimIO Int

%foreign libncurses "init_pair"
prim__initColorPair : Int -> Int -> Int -> PrimIO ()

%foreign libhelper "keyF0"
prim__keyF0 : PrimIO Char

%foreign libhelper "keyF1"
prim__keyF1 : PrimIO Char

%foreign libhelper "keyF2"
prim__keyF2 : PrimIO Char

%foreign libhelper "keyF3"
prim__keyF3 : PrimIO Char

%foreign libhelper "keyF4"
prim__keyF4 : PrimIO Char

%foreign libhelper "keyF5"
prim__keyF5 : PrimIO Char

%foreign libhelper "keyF6"
prim__keyF6 : PrimIO Char

%foreign libhelper "keyF7"
prim__keyF7 : PrimIO Char

%foreign libhelper "keyF8"
prim__keyF8 : PrimIO Char

%foreign libhelper "keyF9"
prim__keyF9 : PrimIO Char

%foreign libhelper "keyF10"
prim__keyF10 : PrimIO Char

%foreign libhelper "keyF11"
prim__keyF11 : PrimIO Char

%foreign libhelper "keyF12"
prim__keyF12 : PrimIO Char

%foreign libhelper "keyUp"
prim__keyUp : PrimIO Char

%foreign libhelper "keyDown"
prim__keyDown : PrimIO Char

%foreign libhelper "keyLeft"
prim__keyLeft : PrimIO Char

%foreign libhelper "keyRight"
prim__keyRight : PrimIO Char

%foreign libhelper "keyBackspace"
prim__keyBackspace : PrimIO Char

||| When you make new windows with @newWindow@
||| this data type stores a reference for you
||| to use with any function that operates on
||| a particular window.
|||
||| Most functions operate on a window even if
||| they don't appear to; you get a default window
||| for free with @initNCurses@. You can request the
||| default window with @stdWindow@.
export
data Window = Win AnyPtr

||| Consider using @withNCurses@ instead.
|||
||| You must call @initNCurses@ before using the other
||| ncurses functions and you must call @deinitNCurses@
||| after you are done (before exiting your program).
|||
||| You will actually see weird behavior in the shell
||| post-exit of your program if you have not deinited
||| ncurses.
export
initNCurses : HasIO io => io ()
initNCurses = primIO $ prim__initScr

||| Consider using @withNCurses@ instead.
|||
||| Must be called after @initNCurses@ and before your
||| program exits.
export
deinitNCurses : HasIO io => io ()
deinitNCurses = primIO $ prim__endWin

||| Calls @initNCurses@, runs the action passed as an argument,
||| and then calls @deiniteNCurses@ before returning the result.
export
withNCurses : HasIO io => io a -> io a
withNCurses ma = do
  initNCurses
  a <- ma
  deinitNCurses
  pure a

||| Begin using color mode.
export
startColor : HasIO io => io ()
startColor = primIO $ prim__startColor

||| Get the default standard ncurses window.
export
stdWindow : HasIO io => io Window
stdWindow = Win <$> (primIO $ prim__stdWindow)

||| Create a new ncurses window.
export
newWindow : HasIO io => (height : Nat) -> (width : Nat) -> (y : Nat) -> (x : Nat) -> io Window
newWindow height width y x = Win <$> (primIO $ prim__newWindow (cast height) (cast width) (cast y) (cast x))

||| As is normal for ncurses, returns (height, width).
export
getMaxSize : HasIO io => Window -> io (Nat, Nat)
getMaxSize (Win win)
  = do y <- primIO (prim__maxYWindow win)
       x <- primIO (prim__maxXWindow win)
       pure (fromInteger (cast y), fromInteger (cast x))

||| Return a window size, using a record with named fields so that it's harder
||| to mistake one dimension for the other
export
getSize : HasIO io => Window -> io Size
getSize win = uncurry MkSize <$> getMaxSize win

||| Refresh the standard window.
|||
||| See @refresh'@ to refresh any other window.
export
refresh : HasIO io => io ()
refresh = primIO $ prim__refresh

||| Refresh a particular window.
export
refresh' : HasIO io => Window -> io ()
refresh' (Win win) = primIO $ prim__refreshWindow win

||| Clear the standard window.
|||
||| See @clear'@ to clear any other window.
export
clear : HasIO io => io ()
clear = primIO $ prim__clear

||| Clear a particular window.
export
clear' : HasIO io => Window -> io ()
clear' (Win win) = primIO $ prim__clearWindow win

export
getChAsInt8 : HasIO io => io Int8
getChAsInt8 = primIO prim__getCh

||| Get a single character immediately.
|||
||| This contrasts with a read from the default shell
||| `stdin` which will wait until a newline to flush
||| its buffer and send input to a program.
export
getCh : HasIO io => io Char
getCh = cast <$> getChAsInt8

||| Switch keyboard input to cbreak mode.
export
cBreak : HasIO io => io ()
cBreak = primIO $ prim__cBreak

||| Switch keyboard input to noecho mode.
export
noEcho : HasIO io => io ()
noEcho = primIO $ prim__noEcho

boolToInt : Bool -> Int
boolToInt False = 0
boolToInt True  = 1

export
noDelay' : HasIO io => Window -> (enable : Bool) -> io ()
noDelay' (Win win) enable = primIO $ prim__noDelay win (boolToInt enable)

export
noDelay : HasIO io => (enable : Bool) -> io ()
noDelay enable = noDelay' !stdWindow enable

||| Turn keypad mode on or off for the given window.
||| When on, function keys (F0, F1, ...) and arrow keys are
||| transformed into single chars that can be compared against
||| the result of passing a particular key to the fnKeyChar
||| function.
export
keypad' : HasIO io => Window -> (enable : Bool) -> io ()
keypad' (Win win) enable = primIO $ prim__keypad win (boolToInt enable)

||| Turn keypad mode on or off for the std window.
||| When on, function keys (F0, F1, ...) and arrow keys are
||| transformed into single chars that can be compared against
||| the result of passing a particular key to the fnKeyChar
||| function.
export
keypad : HasIO io => (enable : Bool) -> io ()
keypad enable = keypad' !stdWindow enable

||| Set the visibility of the cursor.
export
setCursorVisibility : HasIO io => CursorVisibility -> io ()
setCursorVisibility vis = primIO $ prim__setCursorVisibility $
                                     case vis of
                                          CInvisible     => 0
                                          CNormal        => 1
                                          CHighlyVisible => 2

||| Move the cursor in the standard window.
export
nMoveCursor : HasIO io => (row : Nat) -> (col : Nat) -> io ()
nMoveCursor row col = primIO $ prim__move (cast row) (cast col)

||| Move the cursor and print to the standard window.
|||
||| See @mvPrint'@ to print to a particular window.
export
mvPrint : HasIO io => (row, col : Nat) -> String -> io ()
mvPrint row col str = primIO $ prim__mvPrint (cast row) (cast col) "%s" str

||| Move the cursor and print to a window.
export
mvPrint' : HasIO io => Window -> (row, col : Nat) -> String -> io ()
mvPrint' (Win win) row col str
  = primIO $ prim__mvPrintWindow win (cast row) (cast col) "%s" str

||| Move the cursor and print to the standard window.
|||
||| See @nPutStrLn'@ to print to a particular window.
export
nPutStrLn : HasIO io => (row : Nat) -> String -> io ()
nPutStrLn row str = primIO $ prim__mvPrint (cast row) 0 "%s" str

||| Move the cursor and print to the given window.
export
nPutStrLn' : HasIO io => Window -> (row : Nat) -> String -> io ()
nPutStrLn' (Win win) row str = primIO $ prim__mvPrintWindow win (cast row) 0 "%s" str

||| Add a character under the cursor in a given window
export
addCh' : HasIO io => Window -> Char -> io ()
addCh' (Win win) c = primIO $ prim__waddCh win c

||| Add a character under the cursor in the standard window
export
addCh : HasIO io => Char -> io ()
addCh c = primIO $ prim__addCh c

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
export
mvAddCh' : HasIO io => Window -> (row, col : Nat) -> Char -> io ()
mvAddCh' (Win win) row col c
  = primIO $ prim__mvwaddch win (cast row) (cast col) c

||| IMPORTANT: This takes the y-position (the row) before
||| the x-position (the column).
export
mvAddCh : HasIO io => (row, col : Nat) -> Char -> io ()
mvAddCh row col c = primIO $ prim__mvaddch (cast row) (cast col) c

||| Create a vertical line on the standard window
export
vLine : HasIO io => Char -> Nat -> io ()
vLine c n = primIO $ prim__vline c (cast n)

||| Create a vertical line in a given window
export
vLine' : HasIO io => Window -> Char -> Nat -> io ()
vLine' (Win win) c n = primIO $ prim__wvline win c (cast n)

||| Create a horizontal line on the standard window
export
hLine : HasIO io => Char -> Nat -> io ()
hLine c n = primIO $ prim__hline c (cast n)

||| Create a horizontal line in a given window
export
hLine' : HasIO io => Window -> Char -> Nat -> io ()
hLine' (Win win) c n = primIO $ prim__whline win c (cast n)

||| Move the cursor and create a vertical line on the standard window
export
mvVLine : HasIO io => (row, col : Nat) -> Char -> Nat -> io ()
mvVLine row col c n = primIO $ prim__mvvline (cast row) (cast col) c (cast n)

||| Move the cursor and create a vertical line in a given window
export
mvVLine' : HasIO io => Window -> (row, col : Nat) -> Char -> Nat -> io ()
mvVLine' (Win win) col row c n
  = primIO $ prim__mvwvline win (cast row) (cast col) c (cast n)

||| Move the cursor and create a horizontal line on the standard window
export
mvHLine : HasIO io => (row, col : Nat) -> Char -> Nat -> io ()
mvHLine row col c n = primIO $ prim__mvhline (cast row) (cast col) c (cast n)

||| Move the cursor and create a horizontal line in a given window
export
mvHLine' : HasIO io => Window -> (row, col : Nat) -> Char -> Nat -> io ()
mvHLine' (Win win) row col c n
  = primIO $ prim__mvwhline win (cast row) (cast col) c (cast n)

||| Get the character under the cursor in the standard window
export
inCh : HasIO io => io Char
inCh = primIO $ prim__inch

||| Get the character under the cursor in a given window
export
inCh' : HasIO io => Window -> io Char
inCh' (Win win) = primIO $ prim__winch win

||| Move the cursor and get the character under it in the standard window
export
mvInCh : HasIO io => (row, col : Nat) -> io Char
mvInCh row col = primIO $ prim__mvinch (cast row) (cast col)

||| Move the cursor and get the character under it in a given window
export
mvInCh' : HasIO io => Window -> (row, col : Nat) -> io Char
mvInCh' (Win win) row col = primIO $ prim__mvwinch win (cast row) (cast col)

||| Turn a Key into a Char that can be used to compare against
||| the results of getCh. This only applies if you have enabled
||| keypad for the given window.
export
fnKeyChar : HasIO io => Key -> io Char
fnKeyChar F0        = primIO $ prim__keyF0
fnKeyChar F1        = primIO $ prim__keyF1
fnKeyChar F2        = primIO $ prim__keyF2
fnKeyChar F3        = primIO $ prim__keyF3
fnKeyChar F4        = primIO $ prim__keyF4
fnKeyChar F5        = primIO $ prim__keyF5
fnKeyChar F6        = primIO $ prim__keyF6
fnKeyChar F7        = primIO $ prim__keyF7
fnKeyChar F8        = primIO $ prim__keyF8
fnKeyChar F9        = primIO $ prim__keyF9
fnKeyChar F10       = primIO $ prim__keyF10
fnKeyChar F11       = primIO $ prim__keyF11
fnKeyChar F12       = primIO $ prim__keyF12
fnKeyChar Up        = primIO $ prim__keyUp
fnKeyChar Down      = primIO $ prim__keyDown
fnKeyChar Left      = primIO $ prim__keyLeft
fnKeyChar Right     = primIO $ prim__keyRight
fnKeyChar Backspace = primIO $ prim__keyBackspace

firstM : Monad m => (a -> m (Maybe b)) -> List a -> m (Maybe b)
firstM test [] = pure Nothing
firstM test (a :: as)
  = do Nothing <- test a
         | Just b => pure (Just b)
       firstM test as

export
isKey : HasIO io => Char -> io (Maybe Key)
isKey c = firstM (\ k => pure $ k <$ guard (c == !(fnKeyChar k))) allKeys

export
data ColorPair = MkColorPair Nat

public export
Attribute : Type
Attribute = Attribute' ColorPair

export
defaultColorPair : ColorPair
defaultColorPair = MkColorPair 0

getColor : HasIO io => Color -> io Int
getColor color = case color of
                      Black   => primIO $ prim__blackColor
                      Red     => primIO $ prim__redColor
                      Green   => primIO $ prim__greenColor
                      Yellow  => primIO $ prim__yellowColor
                      Blue    => primIO $ prim__blueColor
                      Magenta => primIO $ prim__magentaColor
                      Cyan    => primIO $ prim__cyanColor
                      White   => primIO $ prim__whiteColor

||| Create a new color pair. You must tell it the index to create
||| the color at, which should be a number starting at 0. Some
||| platforms allow you to redefine a color at a given index but this
||| is not universally supported.
|||
||| You might notice that ncurses expects color indices to start at 1 --
||| this function increments the index it is given so that passing 0 to
||| it will use the first available user color pair index of 1.
export
initColorPair : HasIO io => Nat -> (fg : Color) -> (bg : Color) -> io ColorPair
initColorPair idx fg bg =
  do bgColor <- getColor bg
     fgColor <- getColor fg
     let actualIdx = (S idx)
     primIO $ prim__initColorPair (cast actualIdx) fgColor bgColor
     pure (MkColorPair actualIdx)

||| Get the Int representation ncurses cares about for a
||| particular @Attribute@.
getAttribute : HasIO io => Attribute -> io Int
getAttribute attr = case attr of
                         Normal    => primIO $ prim__normalAttr
                         Underline => primIO $ prim__underlineAttr
                         Standout  => primIO $ prim__standoutAttr
                         Reverse   => primIO $ prim__reverseAttr
                         Blink     => primIO $ prim__blinkAttr
                         Dim       => primIO $ prim__dimAttr
                         Bold      => primIO $ prim__boldAttr
                         Protected => primIO $ prim__protectedAttr
                         Invisible => primIO $ prim__invisibleAttr
                         (CP (MkColorPair idx)) => primIO $ prim__colorPairAttr (cast idx)

||| Set an attribute to be applied in the standard window
||| until it is cleared or overwritten.
|||
||| See @nSetAttr'@ for a version that works on
||| any given window.
export
nSetAttr : HasIO io => Attribute -> io ()
nSetAttr attr = do attribute <- getAttribute attr
                   primIO $ prim__setAttr attribute

||| Set an attribute to be applied in the given window
||| until it is cleared or overwritten.
export
nSetAttr' : HasIO io => Window -> Attribute -> io ()
nSetAttr' (Win win) attr = do attribute <- getAttribute attr
                              primIO $ prim__setAttrWindow win attribute

||| Change the attributes at the given position in the standard window.
||| A len of Nothing means "the whole line."
||| A color pair with @defaultColorPair@ offering a sane default.
|||
||| See @nChangeAttr'@ to change attributes in another window.
export
nChangeAttr : HasIO io
           => (row : Nat)
           -> (col : Nat)
           -> (len : Maybe Nat)
           -> Attribute
           -> ColorPair
           -> io ()
nChangeAttr row col len attr (MkColorPair colorIdx) =
  let length = the Int (maybe (-1) cast len)
  in
      do attribute <- getAttribute attr
         primIO $
           prim__mvChangeAt (cast row) (cast col) length attribute (cast colorIdx) prim__getNullAnyPtr

||| Change the attributes at the given position in the given window.
||| A len of Nothing means "the whole line."
||| A color pair with @defaultColorPair@ offering a sane default.
export
nChangeAttr' : HasIO io
            => Window
            -> (row : Nat)
            -> (col : Nat)
            -> (len : Maybe Nat)
            -> Attribute
            -> ColorPair
            -> io ()
nChangeAttr' (Win win) row col len attr (MkColorPair colorIdx) =
  let length = the Int (maybe (-1) cast len)
  in
      do attribute <- getAttribute attr
         primIO $
           prim__mvChangeAtWindow win (cast row) (cast col) length attribute (cast colorIdx) prim__getNullAnyPtr

ext: idr

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
> module Fun.Predicates

> %default total
> %access public export
> %auto_implicits off

> ||| Extensional equality
> ExtEq : {A, B : Type} -> (f : A -> B) -> (g : A -> B) -> Type
> ExtEq {A} {B} f g = (a : A) -> f a = g a

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Flexidisc.Record.Update

import        Flexidisc.RecordContent
import public Flexidisc.Record.Type

%default total
%access export

||| Replace a row, can change its type
|||
||| Complexity is _O(n)_
|||
||| @ xs  the record
||| @ loc the proof that the row is in it
||| @ new the new value for the row
setByLabel : (xs : RecordM m k header) -> (loc : Label query header) ->
             (new : m ty) ->
             RecordM m k (changeType header loc ty)
setByLabel (Rec xs nub) (L loc) new =
  Rec (set xs loc new) (changeValuePreservesNub nub)

||| Update a row, the update can change the row type.
|||
||| Complexity is _O(n)_
|||
||| @ key the row name
||| @ xs    the record
||| @ loc   the proof that the row is in it
||| @ new   the new value for the row
set : (key : k) -> (new : m ty) -> (xs : RecordM m k header) ->
      {auto loc : Label key header} ->
      RecordM m k (changeType header loc ty)
set _ new xs {loc} = setByLabel xs loc new

||| Update a row, the update can change the row type.
|||
||| Complexity is _O(n)_
|||
||| @ query the row name
||| @ xs    the record
||| @ loc   the proof that the row is in it
||| @ new   the new value for the row
setA : Applicative m =>
       (query : k) -> (new : ty) -> (xs : RecordM m k header) ->
       {auto loc : Label query header} ->
       RecordM m k (changeType header loc ty)
setA loc = set loc . pure

||| Update a row at a given `Label`, can change its type.
|||
||| Complexity is _O(n)_
|||
||| @ xs     the record
||| @ loc    the proof that the row is in it
||| @ f      the update function
updateByLabel : (xs : RecordM m k header) -> (loc : Row query a header) ->
                (f : m a -> m b) ->
                RecordM m k (changeType header loc b)
updateByLabel (Rec xs nub) (R loc) f =
  Rec (update xs loc f) (changeValuePreservesNub nub)

||| Update a row at the given key, can change its type.
|||
||| Complexity is _O(n)_
|||
||| @ query  the row name
||| @ xs     the record
||| @ loc    the proof that the row is in it
||| @ f      the update function
update : (query : k) -> (f : m a -> m b) -> (xs : RecordM m k header) ->
         {auto loc : Row query a header} ->
         RecordM m k (changeType header loc b)
update _ f xs {loc} = updateByLabel xs loc f

||| Map at a given `Row`, can change its type.
|||
||| Complexity is _O(n)_
|||
||| @ query  the row name
||| @ xs     the record
||| @ loc    the proof that the row is in it
||| @ f      the update function
mapRow : Functor m =>
         (query : k) -> (f : a -> b) -> (xs : RecordM m k header) ->
         {auto loc : Row query a header} ->
         RecordM m k (changeType header loc b)
mapRow _ f xs {loc} = updateByLabel xs loc (map f)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Util

import Data.Config
import Data.Fuel
import Data.List
import Data.String
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal

%default total

||| Render with or without color based on configuration
export
renderString : Config => Doc AnsiStyle -> String
renderString @{config} =
  renderString . layoutPretty defaultLayoutOptions . if config.colors then id else unAnnotate

export
getManyLines : HasIO io => Fuel -> io (List String)
getManyLines = getMoreLines []
  where
    getMoreLines : (acc : List String) -> Fuel -> io (List String)
    getMoreLines acc Dry = pure (reverse acc)
    getMoreLines acc (More fuel) =
      do line <- trim <$> getLine
         -- stop collecting lines on second blank line.
         case (acc, line) of
              ("" :: rest, "") => pure (reverse rest)
              _                => getMoreLines (line :: acc) fuel

export
parseJiraPrefix : String -> Maybe String
parseJiraPrefix = map (pack . reverse) . guardSuccess . foldl go startOver . unpack
  where
    data Part = Start | Proj | Dash | Num | End

    startOver : (Part, List Char)
    startOver = (Start, [])

    guardSuccess : (Part, List Char) -> Maybe (List Char)
    guardSuccess (Num, y) = Just y
    guardSuccess (End, y) = Just y
    guardSuccess _ = Nothing

    go : (Part, List Char) -> Char -> (Part, List Char)
      -- start off looking for alpha characters that are a Jira Project slug.
    go (Start, cs) c   = if isAlpha c then (Proj, c :: cs) else startOver

      -- if you've found alpha characters, keep an eye out for a dash.
    go (Proj , cs) '-' = (Dash, '-' :: cs)

      -- continue parsing alpha until you find the aforementioned dash.
      -- start over if you find something else.
    go (Proj , cs) c   = if isAlpha c then (Proj, c :: cs) else startOver

      -- we expect a number after a dash or else we start over.
    go (Dash , cs) c   = if isDigit c then (Num, c :: cs) else startOver

      -- now we expect numbers until we reach the end of the prefix.
    go (Num  , cs) c   = if isDigit c then (Num, c :: cs) else (End, cs)

      -- once we are done, we just ignore the remaining characters.
    go (End  , cs) c   = (End, cs)

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
-- Exercise 1
total
same_cons :  {xs : List a}
          -> {ys : List a}
          -> xs = ys
          -> x :: xs = x :: ys
same_cons Refl = Refl

-- Exercise 2
same_list :  {xs : List a}
          -> {ys : List a}
          -> x = y
          -> xs = ys
          -> x :: xs = y :: ys
same_list Refl Refl = Refl

-- Exercise 3
data ThreeEq : a -> b -> c -> Type where
  AllSame : ThreeEq x x x

-- Exercise 4
allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x AllSame = AllSame


text:
module StreamFusion

data TypeT : Type where
  UnitT : TypeT
  IntT : TypeT
  BoolT : TypeT
  ArrayT : TypeT -> TypeT
  VarT : Type -> TypeT -> TypeT
  ArrowT : TypeT -> TypeT -> TypeT

Show TypeT where
  show UnitT = "unit"
  show IntT = "int"
  show BoolT = "bool"
  show (ArrayT typ) = show typ ++ " []"
  show (VarT _ typ) = show typ ++ " ref"
  show (ArrowT arg res) = "(" ++ show arg ++ " -> " ++ show res ++ ")"

interface Symantics (rep : TypeT -> Type) where
  defaultof : rep a
  int : Int -> rep IntT
  bool : Bool -> rep BoolT
  (==) : rep IntT -> rep IntT -> rep BoolT
  (>) : rep IntT -> rep IntT -> rep BoolT
  (<) : rep IntT -> rep IntT -> rep BoolT
  (&&) : rep BoolT -> rep BoolT -> rep BoolT
  (||) : rep BoolT -> rep BoolT -> rep BoolT
  not : rep BoolT -> rep BoolT
  (+) : rep IntT -> rep IntT -> rep IntT
  (*) : rep IntT -> rep IntT -> rep IntT
  ite : rep BoolT -> rep a -> rep a -> rep a
  it : rep BoolT -> rep UnitT -> rep UnitT
  deref : rep (VarT s a) -> rep a
  assign : rep a -> rep (VarT s a) -> rep UnitT
  newVar : rep a -> ({s : Type} -> rep (VarT s a) -> rep b) -> rep b
  letVal : rep a -> (rep a -> rep b) -> rep b
  index : rep IntT -> rep (ArrayT a) -> rep a
  length : rep (ArrayT a) -> rep IntT
  while : rep BoolT -> rep UnitT -> rep UnitT
  seq : rep a -> rep b -> rep b
  seqs : List (rep UnitT) -> rep UnitT
  lam : (rep a -> rep b) -> rep (ArrowT a b)
  app : rep (ArrowT a b) -> rep a -> rep b

data Code : TypeT -> Type where
  C : (Int -> String) -> Code a

Symantics Code where
  defaultof {a = UnitT} = C (\_ => "()")
  defaultof {a = IntT} = C (\_ => "0")
  defaultof {a = BoolT} = C (\_ => "false")
  defaultof {a = (ArrayT x)} = C (\_ => "null")
  defaultof {a = (VarT x y)} = C (\_ => "null")
  defaultof {a = (ArrowT x y)} = C (\_ => "null")
  int x = C (\_ => show x)
  bool x = C (\_ => if x then "true" else "false")
  (==) (C l) (C r) = C (\v => "( " ++ l v ++ " = " ++ r v ++ " )")
  (>) (C l) (C r) = C (\v => "( " ++ l v ++ " > " ++ r v ++ " )")
  (<) (C l) (C r) = C (\v => "( " ++ l v ++ " < " ++ r v ++ " )")
  (&&) (C l) (C r) = C (\v => "( " ++ l v ++ " && " ++ r v ++ " )")
  (||) (C l) (C r) = C (\v => "( " ++ l v ++ " || " ++ r v ++ " )")
  not (C c) = C (\v => "not (" ++ c v ++ " )")
  (+) (C l) (C r) = C (\v => "( " ++ l v ++ " + " ++ r v ++ " )")
  (*) (C l) (C r) = C (\v => "( " ++ l v ++ " * " ++ r v ++ " )")
  ite (C b) (C l) (C r) = C (\v => "(if " ++ b v ++ " then " ++ l v ++ " else " ++ r v ++ ")")
  it (C b) (C t) = C (\v => "(if " ++ b v ++ " then " ++ t v ++ ")")
  deref (C x) = C (\v => "!" ++ x v)
  assign (C val) (C var) = C (\v => var v ++ " := " ++ val v)
  newVar {a} (C s) f = C (\v => let x = "x" ++ show v in
                                let (C c) = f $ the (Code (VarT () a)) (C (\_ => x)) in
                                "let " ++ x ++ " = ref " ++ s v ++ " in " ++ c (v + 1))
  letVal (C s) f = C (\v => let x = "x" ++ show v in
                            let (C c) = f $ C (\_ => x) in
                            "let " ++ x ++ " = " ++ s v ++ " in " ++ c (v + 1))
  index (C i) (C arr) = C (\v => arr v ++ ".[" ++ i v ++ "]")
  length (C arr) = C (\v => arr v ++ ".Length")
  while (C p) (C b) = C (\v => "(while " ++ p v ++ " do " ++ b v ++ ")")
  seq (C fs) (C sn) = C (\v => "(" ++ fs v ++ "; " ++ sn v ++ ")")
  seqs steps = foldr seq defaultof steps
  lam {a} f = C (\v => let x = "x" ++ show v in
                       let (C g) = f (C (\_ => x)) in
                       "(fun (" ++ x ++ " : " ++ show a ++ ") -> " ++ g (v + 1) ++ ")")
  app (C f) (C g) = C (\v => "(" ++ f v ++ " " ++ g v ++ ")")

data Stream : (rep : TypeT -> Type) -> (a : TypeT) -> Type where
  SC : ((s -> rep UnitT) -> rep UnitT) ->
       (s -> rep BoolT) ->
       (s -> (rep a -> rep UnitT) -> rep UnitT) ->
       (s -> rep UnitT) -> Stream rep a

ofArray : Symantics rep => rep (ArrayT a) -> Stream rep a
ofArray arr = SC (init arr) next current reset
  where
    init : rep (ArrayT a) -> ((rep (ArrayT a), DPair Type (\s => rep (VarT s IntT))) -> rep UnitT) -> rep UnitT
    init arr k = newVar (int 0) (\v => k (arr, (_ ** v)))
    next : (rep (ArrayT a), DPair Type (\s => rep (VarT s IntT))) -> rep BoolT
    next (arr, (_ ** v)) = deref v < length arr
    current : (rep (ArrayT a), DPair Type (\s => rep (VarT s IntT))) -> (rep a -> rep UnitT) -> rep UnitT
    current (arr, (_ ** v)) k = letVal (index (deref v) arr) (\x => seqs [k x, assign (deref v + (int 1)) v])
    reset : (rep (ArrayT a), DPair Type (\s => rep (VarT s IntT))) -> rep UnitT
    reset (arr, (_ ** v)) = assign (int 0) v

fold : Symantics rep => (rep a -> rep r -> rep r) -> rep r -> Stream rep a -> rep r
fold f seed stream = newVar seed (\acc => seq (fold' (\x => assign (f x (deref acc)) acc) stream) (deref acc))
  where
    fold' : (rep a -> rep UnitT) -> Stream rep a -> rep UnitT
    fold' k (SC init next current reset) = init (\s => while (next s) (current s k))

count : Symantics rep => Stream rep a -> rep IntT
count = fold (\x, acc => acc + (int 1)) (int 0)

sum : Symantics rep => Stream rep IntT -> rep IntT
sum = fold (\x, acc => x + acc) (int 0)

map : Symantics rep => (rep a -> rep b) -> Stream rep a -> Stream rep b
map f (SC init next current reset) = SC init next (\s, k => current s (\x => letVal x (\x' => k (f x')))) reset

filter : Symantics rep => (rep a -> rep BoolT) -> Stream rep a -> Stream rep a
filter pred (SC init next current reset) = SC init next (\s, k => current s (\x => letVal x (\x' => ite (pred x') (k x') defaultof))) reset

StreamC : (TypeT -> Type) -> Type -> TypeT -> Type
StreamC rep s a = (s, ((s -> rep UnitT) -> rep UnitT), (s -> rep BoolT),
                      (s -> (rep a -> rep UnitT) -> rep UnitT),
                      (s -> rep UnitT))

flatMap : Symantics rep => (rep a -> Stream rep b) -> Stream rep a -> Stream rep b
flatMap f (SC init' next' current' reset') = SC (init f init') next (current current' next') (reset reset')
  where
    init : (rep a -> Stream rep b) -> ((s -> rep UnitT) -> rep UnitT) -> ((s, DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => StreamC rep s' b)) -> rep UnitT) -> rep UnitT
    init f inita k = newVar (bool True) (\b => newVar (bool True) (\b' => newVar defaultof (\v => let (SC initb nextb currentb resetb) = f (deref v) in inita (\st => initb (\st' => k (st, (_ ** b), (_ ** b'), (_ ** v), (_ ** (st', initb, nextb, currentb, resetb))))))))
    next : (s, DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => StreamC rep s' b)) -> rep BoolT
    next (st, _, (_ ** b'), _, (_ ** (st', _, _, _, _))) = deref b'
    current : (s -> (rep a -> rep UnitT) -> rep UnitT) -> (s -> rep BoolT) -> (s, DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => StreamC rep s' b)) -> (rep b -> rep UnitT) -> rep UnitT
    current currenta nexta (st, (_ ** b), (_ ** b'), (_ ** v), (_ ** (st', initb, nextb, currentb, resetb))) k =
      ite (deref b)
          (ite (not (nexta st)) (assign (bool False) b') (seqs [currenta st (\a => seqs [assign a v, assign (bool False) b])]))
          (ite (nextb st') (currentb st' k)
                           (seqs [resetb st', assign (bool True) b]))
    reset : (s -> rep UnitT) -> (s, DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => StreamC rep s' b)) -> rep UnitT
    reset reseta (st, (_ ** b), (_ ** b'), _, (_ ** (st', _, _, _, resetb))) = seqs [assign (bool True) b, assign (bool True) b',reseta st, resetb st']

zipWith : Symantics rep => (rep a -> rep b -> rep c) -> Stream rep a -> Stream rep b -> Stream rep c
zipWith f (SC inita nexta currenta reseta) (SC initb nextb currentb resetb) =
  SC (init inita initb) (next nexta nextb) (current f currenta currentb) (reset reseta resetb)
  where
    init : ((s -> rep UnitT) -> rep UnitT) -> ((s' -> rep UnitT) -> rep UnitT) -> ((s, s', DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => rep (VarT s' b))) -> rep UnitT) -> rep UnitT
    init inita initb k = newVar (bool True) (\b => newVar (bool False) (\b' => newVar defaultof (\v => newVar defaultof (\v' => inita (\s => initb (\s' => k (s, s', (_ ** b), (_ ** b'), (_ ** v), (_ ** v'))))))))
    next : (s -> rep BoolT) -> (s' -> rep BoolT) -> (s, s', DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => rep (VarT s' b))) -> rep BoolT
    next nexta nextb (s, s', _, _, _, _) = nexta s && nextb s'
    current : (rep a -> rep b -> rep c) -> (s -> (rep a -> rep UnitT) -> rep UnitT) -> (s' -> (rep b -> rep UnitT) -> rep UnitT) ->
                                           (s, s', DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => rep (VarT s' b))) ->
                                           (rep c -> rep UnitT) -> rep UnitT
    current f currenta currentb (s, s', (_ ** b), (_ ** b'), (_ ** v), (_ ** v')) k =
      seqs [it (deref b) (currenta s (\x => seqs [assign x v, assign (bool False) b, assign (bool True) b'])),
            it (deref b') (currentb s' (\x => seqs [assign x v', assign (bool False) b'])),
            it (not (deref b) && not (deref b'))
               (seqs [
                  k (f (deref v) (deref v')),
                  assign (bool True) b
                ])]
    reset : (s -> rep UnitT) -> (s' -> rep UnitT) -> (s, s', DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' BoolT)), DPair Type (\s' => rep (VarT s' a)), DPair Type (\s' => rep (VarT s' b))) -> rep UnitT
    reset reseta resetb (s, s', (_ ** b), (_ ** b'), _, _) = seqs [assign (bool True) b, assign (bool False) b', reseta s, resetb s']

example0 : Symantics rep => rep (ArrayT IntT) -> rep IntT
example0 = sum . map (\x => x * (int 2)) . filter (\x => x < (int 3)) . ofArray

example1 : Symantics rep => rep (ArrayT IntT) -> rep IntT
example1 arr = (sum . flatMap (\x => nested1 arr x) . ofArray) arr
  where
    nested2 : rep (ArrayT IntT) -> rep IntT -> Stream rep IntT
    nested2 arr x = (map (\x' => x * x') . ofArray) arr
    nested1 : rep (ArrayT IntT) -> rep IntT -> Stream rep IntT
    nested1 arr x = (flatMap (\x => nested2 arr x) . ofArray) arr

example2 : Symantics rep => rep (ArrayT IntT) -> rep IntT
example2 arr = sum $ zipWith (\x, y => x * y) (nested1 arr) (nested1 arr)
where
  nested1 : rep (ArrayT IntT) -> Stream rep IntT
  nested1 arr = (map (\x => x * (int 2)) . ofArray) arr

example3 : Symantics rep => rep (ArrayT IntT) -> rep (ArrayT IntT) -> rep IntT
example3 arr arr' = sum $ zipWith (\x, y => x * y) (nested1 arr) (nested1 arr')
  where
    nested2 : rep (ArrayT IntT) -> rep IntT -> Stream rep IntT
    nested2 arr x = (filter (\x' => x == x') . ofArray) arr
    nested1 : rep (ArrayT IntT) -> Stream rep IntT
    nested1 arr = (flatMap (\x => nested2 arr x) . ofArray) arr

example4 : Symantics rep => rep (ArrayT IntT) -> rep IntT
example4 arr = sum $ map (\x => x * (int 2)) (nested1 arr)
where
  nested2 : rep (ArrayT IntT) -> rep IntT -> Stream rep IntT
  nested2 arr x = (map (\x' => x * x') . ofArray) arr
  nested1 : rep (ArrayT IntT) -> Stream rep IntT
  nested1 arr = (flatMap (\x => nested2 arr x) . flatMap (\x => nested2 arr x) . ofArray) arr

test0 : Code (ArrowT (ArrayT IntT) IntT)
test0 = lam example0

test3 : Code (ArrowT (ArrayT IntT) (ArrowT (ArrayT IntT) IntT))
test3 = lam (\arr => lam (\arr' => example3 arr arr'))

compile : Code a -> String
compile code = let (C c) = code in c 0

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
foo : String
foo = """a
"""


text:
module BoundAst

%default total
%access public export

mutual
  ||| An unary type operator is a type of kind * -> *
  data UnaryTypeOp
    = TypeclassCtr
    --| TypeCtr String
    | NAryTypeAppl UnaryTypeOp Monotype

  ||| A monotype is a type of kind *
  data Monotype : Type where
    Term : String -> Monotype
    FuncType : Monotype -> Monotype -> Monotype
    TypeFullyApplied : UnaryTypeOp -> Monotype -> Monotype

data Method : (Monotype, Monotype) -> Type where
  Method' : (msig : (Monotype, Monotype)) -> String -> Method msig

||| Monomorphic type constructors
||| (S n) is the arity of the type constructor, except for tuple, in which case
||| it is S (S n)
data MMTypeCtr : (n : Nat) -> Type where
  Regular : (n: Nat) -> String -> MMTypeCtr n
  Tuple   : (n : Nat) -> MMTypeCtr (S n)
  Array   : MMTypeCtr Z
  Appl1   : MMTypeCtr (S n) -> MMTypeCtr n

||| (S n) is the arity of the typeclass
||| The list is the methods that will be used to implement the others. You might
||| also call them abstract or pure virtual in object-oriented terminology.
data Typeclass : Nat -> List (Monotype, Monotype) -> Type where
  TyCl : String -> Typeclass n l

data Methods : List (Monotype, Monotype) -> Type where
  Nil  : Methods []
  (::) : Method msig -> Methods sigs -> Methods (msig :: sigs)

||| TODO Need number of methods to match number of primitive methods in typeclass, and their signatures
data Instance : (tc : Typeclass n l) -> Type where
  Inst : (MMTypeCtr n, Methods l) -> Instance tc

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
module Language.LSP.Message.Implementation

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_implementation
public export
record ImplementationClientCapabilities where
  constructor MkImplementationClientCapabilities
  dynamicRegistration : Maybe Bool
  linkSupport         : Maybe Bool
%runElab deriveJSON defaultOpts `{{ImplementationClientCapabilities}}

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

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

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


text:
main : IO ()
main = printLn "one\ntwo"

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Channel
import Linear

data Cmd = Add | Append

Utils : Protocol ()
Utils
    = do cmd <- Request Cmd
         case cmd of
              Add => do Request (Int, Int)
                        Respond Int
                        Done
              Append => do Request (String, String)
                           Respond String
                           Done

utilServer : (1 chan : Server Utils) -> Any IO ()
utilServer chan
    = do cmd # chan <- recv chan
         case cmd of
              Add => do (x, y) # chan <- recv chan
                        chan <- send chan (x + y)
                        close chan
              Append => do (x, y) # chan <- recv chan
                           chan <- send chan (x ++ y)
                           close chan

MakeUtils : Protocol ()
MakeUtils = do cmd <- Request Bool
               if cmd
                  then do Respond (Client Utils); Loop MakeUtils
                  else Done

sendUtils : (1 chan : Server MakeUtils) -> Any IO ()
sendUtils chan
    = do cmd # chan <- recv chan
         if cmd
            then do cchan <- Channel.fork utilServer
                    chan <- send chan cchan
                    sendUtils chan
            else close chan

getUtilsChan : (1 chan : Client MakeUtils) ->
               One IO (Client Utils, Client MakeUtils)
getUtilsChan chan
    = do chan <- send chan True
         cchan # chan <- recv chan
         pure (cchan, chan)

closeUtilsChan : (1 chan : Client MakeUtils) ->
                 Any IO ()
closeUtilsChan chan
    = do chan <- send chan False
         close chan

doThings : Any IO ()
doThings
    = do -- lift $ printLn "Starting"
         schan <- Channel.fork sendUtils
         res <- getUtilsChan schan
         let (uchan1, schan) = res
         lift $ printLn "Got Chan 1"
         (uchan2, schan) <- getUtilsChan schan
         lift $ printLn "Got Chan 2"
         closeUtilsChan schan

         uchan1 <- send uchan1 Add
         uchan2 <- send uchan2 Append
         uchan2 <- send uchan2 ("aaa", "bbb")
         res # uchan2 <- recv uchan2
         close uchan2
         lift $ printLn res

         uchan1 <- send uchan1 (40, 54)
         res # uchan1 <- recv uchan1
         close uchan1

         lift $ printLn res

main : IO ()
main = run doThings


text:
module Main

data Cat = Cas | Luna | Sherlock

f : (cat: Cat) -> String

getName : (cat: Cat) -> String
getName Cas = "Cas"
getName Luna = "Luna"

plusTwo : (n: Nat) -> Nat
plusTwo n = plus 2 n

g : (n: Nat) -> (b: Bool) -> String
g n b = ?g_rhs

n : Nat
n = ?n_rhs


text:
module Nat

import Basic
import Unit
import Void

public export
data Nat = Z | S Nat

public export
NatInduction : (p : Nat -> Type)
            -> p Z
            -> ((n : Nat) -> p n -> p (S n))
            -> (n : Nat) -> p n
NatInduction _ p0 pn Z = p0
NatInduction p p0 pn (S n) = pn n (NatInduction p p0 pn n)

public export
NatRecursion : (p : Type) -> p -> (Nat -> p -> p) -> Nat -> p
NatRecursion p = NatInduction (const p)

public export
NatIteration : (p : Type) -> p -> (p -> p) -> Nat -> p
NatIteration p p0 f = NatRecursion p p0 (const f)

infixl 5 +
infixl 6 *

public export
(+) : Nat -> Nat -> Nat
Z + k = k
(S n) + k = S (n + k)

public export
(*) : Nat -> Nat -> Nat
Z * k = Z
(S n) * k = k + n * k

infixl 1 <=
infixl 1 >=

namespace NatOrder
  public export
  (<=) : Nat -> Nat -> Type
  Z   <= _   = Unit
  S n <= Z   = Void
  S n <= S k = n <= k

  public export
  (>=) : Nat -> Nat -> Type
  n >= k = Neg (n <= k)

namespace N
  %inline public export
  zero : Nat
  zero = Z

  %inline public export
  one : Nat
  one = S zero

  %inline public export
  two : Nat
  two = S one

  %inline public export
  three : Nat
  three = S two

  %inline public export
  four : Nat
  four = S three


text:
import VISD.Binary

test : Syntax d Nat => d (Nat, Nat) Nat
test = (val 1) <*> item
   <|> (val 2) <*> (val 3)

test2 : Syntax d Bool => d (Nat, Bool) Bool
test2 = (nat BE 4) <*> (val True)
    <|> (nat BE 2) <*> (val False)

partial test3 : Syntax d Bool => d (Bool, List Nat) Bool
test3 = (val True) <*> ((ignore False <$> item) *> (many $ nat BE 4))
    <|> (val False) <*> ((ignore True <$> item) *> (many $ nat LE 3))

test4 : Syntax d Bool => d (Vect 2 Nat, Bool) Bool
test4 = rep 2 (nat LE 4) <*> val True
    <|> rep 2 (nat BE 3) <*> val False

main : IO ()
main = do
  putStrLn $ show $ parse test4 [False, False, True, False, True, False, False] >>= compose test4

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


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

import Data.DList
import GRL.Lang.GLang

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

data Ty = TyITEM | TyTASK

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

data IRes : Ty -> Type where
  IResItem : GLang ELEM -> IRes TyITEM
  IResTask : GLang ELEM -> GLang INTENT -> IRes TyTASK

interpItem : String -> Maybe SValue -> IRes TyITEM
interpItem title Nothing     = IResItem $ mkGoal title
interpItem title (Just sval) = IResItem $ mkSatGoal title sval

interpTask : String -> SValue -> IRes TyITEM -> IRes TyTASK
interpTask t s (IResItem to) = IResTask elem link
  where
    elem : GLang ELEM
    elem = mkSatTask t s

    link : GLang INTENT
    link = (elem ==> to | MAKES)

buildModel : String
          -> List (IRes TyITEM)
          -> List (IRes TyTASK) -> GModel
buildModel n is ts = insertMany tis $ insertMany tes m
  where
    root : GLang ELEM
    root = mkGoal n

    es : List (GLang ELEM)
    es = map (\(IResItem x) => x) is

    toRoot : GLang STRUCT
    toRoot = (root &= es)

    m : GModel
    m = insert toRoot $ insertMany (root::es) emptyModel

    ties : List (GLang ELEM, GLang INTENT)
    ties = map (\(IResTask e i) => (e,i)) ts

    tis : List (GLang ELEM)
    tis = map fst ties

    tes : List (GLang INTENT)
    tes = map snd ties

-- --------------------------------------------------------- [ Data Structures ]

data TODOItem : (ty : Ty) -> IRes ty -> Type where
  Done : (title : String) -> (desc : Maybe String)
      -> TODOItem TyITEM (interpItem title (Just SATISFIED))

  TODO : (title : String) -> (desc : Maybe String)
      -> TODOItem TyITEM (interpItem title Nothing)

  Action : (title : String) -> (desc : Maybe String)
        -> (value : SValue) -> (todo : TODOItem TyITEM e)
        -> TODOItem TyTASK (interpTask title value e)

data TODOList : GModel -> Type where
  MyList : (name : String)
        -> DList (IRes TyITEM) (\res => TODOItem TyITEM res) is
        -> DList (IRes TyTASK) (\res => TODOItem TyTASK res) ts
        -> TODOList (buildModel name is ts)

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Replica.App.Set

import Control.App
import Control.App.Console

import Data.List

import Language.JSON

import Replica.App.FileSystem
import Replica.App.Format
import Replica.App.Log
import Replica.App.Replica
import Replica.Command.Set
import Replica.Core

import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

import System.Path

%default total

export
data HomeDir : Type where

export
data SetContext : Type where

export
updateConfig : List (String, JSON) -> Setter -> JSON
updateConfig = updateConfig' []
  where
    updateConfig' : List (String, JSON) -> List (String, JSON) -> Setter -> JSON
    updateConfig' xs [] (MkSetter key value) = JObject $ reverse $ (key, value) :: xs
    updateConfig' xs (x :: ys) s@(MkSetter key value) = if fst x == key
      then JObject $ reverse xs ++ ((key, value) :: ys)
      else updateConfig' (x :: xs) ys s

export
setReplica :
  FileSystem (FSError :: e) =>
  Has
    [ Console
    , State HomeDir (Maybe String)
    , State SetContext SetCommand
    , State GlobalConfig Global
    , Exception ReplicaError
    ] e => App e ()
setReplica = do
  setCtx <- get SetContext
  debug "Set: \{show setCtx}"
  tgt <- case setCtx.target of
              Local => pure $ "."</> ".replica.json"
              Global => do
                Just hd <- get HomeDir
                  | Nothing => throw $ InvalidJSON ["Can't access global config: No HOME"]
                pure $ hd </> ".replica.json"
  f <- catchNew (readFile tgt)
    (\err : FSError => case err of
                            (MissingFile x) => pure $ show $ JObject []
                            pat => throw $ InvalidJSON ["Error when accessing config"])
  let Just (JObject xs) = JSON.parse f
      | Nothing => throw $ InvalidJSON
         ["Can't parse current config \{show tgt} (either delete the file or fix its content)"]
      | Just _ => throw $ InvalidJSON
         ["Current config \{show tgt} is invalid (object expected) (either delete the file or fix its content)"]
  let newConfig = updateConfig xs !(setter <$> get SetContext)
  catchNew (writeFile tgt $ show newConfig)
    (\err : FSError => throw $ InvalidJSON ["Can't write config"])

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module Prelude.Interpolation

||| Interpolated strings are of the form `"xxxx \{ expr } yyyy"`.
||| In this example the string `"xxxx "` is concatenated with `expr` and
||| `" yyyy"`, since `expr` is not necessarily a string, the generated
||| code looks like this:
||| ```
||| concat [interpolate "xxxx ", interpolate expr, interpolate " yyyy"]
||| ```
||| This allows to customise the interpolation behaviour by providing
||| an instance of `Interpolation` for a type.
public export
interface Interpolation a where
  interpolate : a -> String

||| The interpolation instance for Strings is the identity
export
Interpolation String where
  interpolate x = x


text:
module Uri.Parser

import public Uri.Core
import public Uri.Types
import Data.String
import Debug.Trace
import Uri.Util

%inline
valAlphaNum : Char -> Bool
valAlphaNum c = isAlpha c || isDigit c

%inline
valMark : Char -> Bool
valMark = (`oneOf` "-_.!~*'()")

%inline
valUnreserved : Char -> Bool
valUnreserved c = valAlphaNum c || valMark c

%inline
valReserved : Char -> Bool
valReserved = (`oneOf` ";/?:@&=+$,")

-- Not Escaped
%inline
valUric : Char -> Bool
valUric c = valReserved c || valUnreserved c || (c `oneOf` ";/?:@&=+$,")

-- Not Escaped
%inline
valPchar : Char -> Bool
valPchar c = valUnreserved c || (c `oneOf` ":@&=+$,")

%inline
valPcharColonSlash : Char -> Bool
valPcharColonSlash c = valUnreserved c || c == '/' || c == ';' || (c `oneOf` ":@&=+$,")

%inline
valScheme : Char -> Bool
valScheme c = isAlpha c || isDigit c || (c `oneOf` "+-.")

-- Not Escaped
%inline
valRegNameNoAtColon : Char -> Bool
valRegNameNoAtColon c = valUnreserved c || (c `oneOf` "$,;&=+")

%inline
valUserInfo : Char -> Bool
valUserInfo c = valUnreserved c || (c `oneOf` ";:&=+$,")

%inline
valUricNoSlash : Char -> Bool
valUricNoSlash c = valUnreserved c || (c `oneOf` ";?:@&=+$,")

%inline
valRelSegment : Char -> Bool
valRelSegment c = valUnreserved c || (c `oneOf` ";@&=+$,")

-- Parsers

parseSingleEncode : Parser Int
parseSingleEncode = do
    _     <- chr '%'
    start <- (\str => assert_total (strIndex str 0)) <$> (cut $ is isHexDigit)
    end   <- (\str => assert_total (strIndex str 0)) <$> (cut $ is isHexDigit)
    pure $ (hexDigitToDigit start * 16) + (hexDigitToDigit end)

parseEncode : Parser Cut
parseEncode = (MkLit . hexToStr) <$> (some parseSingleEncode)

parseUricNoSlash : Parser Cut
parseUricNoSlash = cutters ((matchPlus valUricNoSlash) <|> parseEncode)

parseUric : Parser Cut
parseUric = cutters $ (matchPlus valUric) <|> parseEncode

%inline
parseFragment : Parser Cut
parseFragment = match valUric

%inline
parseQuery : Parser Cut
parseQuery = cutters $ (matchPlus valUric) <|> parseEncode

parseParam : Parser Cut
parseParam = cutters $ (matchPlus valPchar) <|> parseEncode

parsePathSegment : Parser Cut
parsePathSegment = (cutters $ (matchPlus valPcharColonSlash) <|> parseEncode) <|> pure (MkLit "")

parseOpaquePart : Parser Cut
parseOpaquePart = is valUricNoSlash <+> match valUric

parseAbsPath : Parser Cut
parseAbsPath = chr '/' <+> parsePathSegment

parsePath : Parser (Maybe Cut)
parsePath = option (parseAbsPath <|> parseOpaquePart)

parseRelPath : Parser Cut
parseRelPath = do
    res <- cutters (matchPlus valRelSegment <|> parseEncode)
    rest <- option parseAbsPath
    case rest of
        Just n => pure (res <+> n)
        Nothing => pure res

parseHost : Parser Cut
parseHost = matchPlus (\c => valAlphaNum c || c == '.')

unsafePort : String -> Int
unsafePort str =
    if str == ""
        then 80
        else assert_total (let (Just n) = parseInteger str in n)

public export
parseServer : Parser Authority
parseServer = do
    userInfo <- option $ cut (match valUserInfo >>| chr '@')
    host     <- cut parseHost
    port     <- option $ unsafePort <$> cut (chr ':' |>> match isDigit)
    pure (MkAuthority userInfo host port)

-- Not implemented "reg_name" rule
parseAuthority : Parser Authority
parseAuthority = parseServer

parseNetPathWithoutPath : Parser Authority
parseNetPathWithoutPath = exact "//" |>> parseAuthority

parseHierPart : Parser (Maybe Authority, Maybe String, Maybe String)
parseHierPart = do
    netPath <- option parseNetPathWithoutPath
    case netPath of
        Just _ => do
            path <- option (cut parseAbsPath)
            query <- option $ cut (chr '?' |>> parseQuery)
            pure (netPath, path, query)
        Nothing => do
            path <- (cut parseAbsPath)
            query <- option $ cut (chr '?' |>> parseQuery)
            pure (netPath, Just path, query)

public export
parseAbsoluteURI : Parser AbsoluteURI
parseAbsoluteURI = do
        scheme <- (cut $ is isAlpha <+> match valScheme)
        _ <- chr ':'
        (authority, path, query) <- (parseHierPart <|> parseOpaque)
        frag <- option $ cut (chr '#' |>> matchPlus valUric)
        pure $ MkAbsURI scheme authority path query frag
    where
        parseOpaque : Parser (Maybe Authority, Maybe String, Maybe String)
        parseOpaque = (\x => (Just (MkAuthority Nothing x Nothing), Nothing, Nothing)) <$> cut parseOpaquePart

-- Will not parse net_path as relative.
public export
parseRelativeURI : Parser RelativeURI
parseRelativeURI = do
    res <- cut (parseAbsPath <|> parseRelPath)
    query <- option $ cut (chr '?' |>> parseQuery)
    pure (MkRelURI res query)

public export
parseURI : Parser URI
parseURI =
        ((Absolute <$> parseAbsoluteURI)
    <|> (Relative <$> parseRelativeURI))
    >>| eof

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
module Data.Matrix.ZZGaussianElimination

import Control.Algebra
import Classes.Verified
import Control.Algebra.VectorSpace -- definition of module

import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.ZZVerified

import Data.Matrix.ZZModuleSpan
import Data.Matrix.LinearCombinations

import Data.Matrix.RowEchelon
import Control.Algebra.ZZDivisors
import Data.Matrix.ZZGaussianEliminationLemmas

import Data.Fin.FinOrdering

import Control.Isomorphism

{-
(bezQTy) is the only thing actually used from here in the proof,
something req.d to potentially generalize to other Bezout domains.

However, the example (bezoutZT) is applied here to give a specific algorithm.
-}
import Control.Algebra.ZZBezoutsIdentity

-- Extension of a GCD operation to any number of arguments arguments
import Control.Algebra.ZZGCDOfVectAlg

-- Dependent pattern matching using (do) notation binds improves clarity
import Control.Monad.Identity

{-
Main elimination algorithms.

Index:

* Template & usage for do notation pattern matching technique
* elimFirstCol
* gaussElimlzIfVectGCD2
* gaussElimlzIfVectGCD
* gaussElimlzIfGCD
* The gaussian elimination instantiation derived from (bezoutZT)
* Appendix Elim.General.Meta
-}

{-
Dependent pattern matching using (do) notation binds improves clarity

---

Template & usage for technique:

> f : (a : ZZ ** a = Pos Z)
> f = runIdentity $ do {
> 		clause <- Id $ 'c'
> 		(s ** s_pr) <- Id $ the (r : ZZ ** r = Pos Z) (Pos 0 ** Refl)
> 		(t ** t_pr) <- Id $ (s ** s_pr)
> 		(a, b, c) <- Id $ ('x', ('y', 'z'))
> 		return $ believe_me "Placeholder for while argument incomplete"
> 		-- return (the ZZ _ ** ?foo)
> 	}

Note that two dependent pattern matches have occurred without nesting (with) blocks.

If we figure out the witness of the dependent pair value, we can test things out
interactively, which is sometimes helpful. Note that (clause) won't get recognized
as being ('c'), it's still only a monadic bind.

> g : (a : ZZ ** a = Pos Z)
> g = runIdentity $ do {
> 		clause <- Id $ 'c'
> 		(s ** s_pr) <- Id $ the (r : ZZ ** r = Pos Z) (Pos 0 ** Refl)
> 		-- return $ believe_me "Placeholder for while argument incomplete"
> 		return (the ZZ (Pos 0) ** ?bar)
> 	}

Likewise, we can't recognize (s_pr) is a proof that (Pos 0 = Pos 0), so it doesn't
match the actual goal. However, we can still change the last line to

> 		return (s ** ?bar)

at which point `s_pr` solves the goal.

While (Reader) without (runReader) can simulate a (parameters) block at the same time,
this adds some plumbing overhead, and (ask) may have to be passed its (MonadReader)
instance explicitly:

> z <- ask @{the (MonadReader ZZ _) %instance}

-}

{-
Main elimination algorithms
-}

parameters (
	gcdOfVectAlg :
		-- Will making argument "k" implicit work?
		(k : Nat)
		-> (x : Vect k ZZ)
		-> ( v : Vect k ZZ **
			( i : Fin k )
			-> (index i x) `quotientOverZZ` (v <:> x) )
	) {

{-
Structure of (elimFirstCol):

succImplWknStep_Qfunclemma => succImplWknStep_stepQfunc => succImplWknStep_unplumbed => succImplWknStep => foldedFully

(mkQfunc, foldedFully) => elimFirstCol (after some work)

---

Better to refine this to a type that depends on (m=S predm) so that the case (m=Z) may also be covered.

Shall start from the bottom of the matrix (last) and work up to row (FS FZ) using a traversal based on (weaken) and a binary map from index (Fin n) and oldvals to newvals.
-}

total
elimFirstCol :
	(xs : Matrix n (S predm) ZZ)
	-> (gexs : Matrix (S n) (S predm) ZZ **
		(downAndNotRightOfEntryImpliesZ gexs FZ FZ
		, gexs `bispanslz` xs))
elimFirstCol [] {predm}
	= ( row {n=S predm} $ neutral ** ( nosuch, ([] ** Refl), ([neutral] ** Refl) ) )
	where
		nosuch : (i : Fin _) -> (j : Fin _)
			-> LTRel Z (finToNat i)
			-> LTERel (finToNat j) Z
			-> indices i j (row {n=S predm} Prelude.Algebra.neutral) = Pos 0
		nosuch FZ FZ _ = either (const Refl) (const Refl)
		nosuch (FS k) FZ _ = absurd k
		nosuch _ (FS k) _ = void . ( either succNotLTEzero SIsNotZ )
elimFirstCol mat {n=S predn} {predm} = runIdentity $ do {

		-- The application of (gcdOfVectAlg) to (mat) column 0.
		(v ** fn) <- Id $ vAndFn

		-- Refines endgoal
		let bisWithGCD = the ( (v<\>mat)::mat `bispanslz` mat )
			(extendSpanningLZsByPreconcatTrivially {zs=[_]} spanslzrefl
			, mergeSpannedLZs spanslzRowTimesSelf spanslzrefl)

		-- ( _ ** forall i. succImplWknProp mat (v<\>mat) _ i endmat_i )
		(endmat ** endmatPropFn)
			<- Id $ foldedFully _ _ mat v $ mkQFunc _ _ v mat fn

		-- (_, danrz endmat_0 0 0, endmat_0 bispans v<\>mat::mat)
		(_, leftColZBelow, endmatBispansMatandgcd) <- Id $ endmatPropFn FZ
		return $ ( index FZ endmat **
			(leftColZBelow
			, endmatBispansMatandgcd `bispanslztrans` bisWithGCD) )
	}
	where
		vAndFn : ( v : Vect (S predn) ZZ **
			( i : Fin (S predn) )
			-> (index i (getCol FZ mat))
				`quotientOverZZ` (v <:> (getCol FZ mat)) )
		vAndFn = gcdOfVectAlg (S predn) (getCol FZ mat)

{- Gaussian elimination for width > 0 -}

total
gaussElimlzIfVectGCD2 :
	(xs : Matrix n (S predm) ZZ)
	-> ( n' : Nat
		** (gexs : Matrix n' (S predm) ZZ
			** (rowEchelonPre gexs, gexs `bispanslz` xs)) )

{-
Suppose case width = 1.

If desired:

gaussElimlzIfVectGCD2 xs {predm=Z} with (elimFirstCol xs)
	| (gexs ** (danrz, bis)) = (_ ** ( gexs ** (echelonPreFromDanrzLast danrz, bis) ))

can't be done, because the typechecker thinks it's a (Vect 1 ZZ = ZZ) situation.

Not fixed if the (danrz, bis) is matched as (danrzAndBis).
Not fixed by passing (S n) into the hole.
-}

gaussElimlzIfVectGCD2 xs {predm=Z} = runIdentity $ do {
		(gexs ** (danrz, bis)) <- Id $ elimFirstCol xs
		return $ (_ ** ( gexs ** (echelonPreFromDanrzLast danrz, bis) ))
	}

{-
Else case width > 1.

We handle recursion in different ways depending on whether the first column is neutral.
Since (with) blocks can't access local functions unless local to the case, and (case)
blocks have totality problems, we write it as a wrapping of a local function which
pattern matches on the equality decision.

The locally scoped functions in question were involved in partially completing the
proof, and this is retained as an artifact to retain compatibility this implementation
tool used.
-}

gaussElimlzIfVectGCD2 xs {predm = S prededm}
	= gaussElimlzIfVectGCD2_gen $ decEq (getCol FZ xs) Algebra.neutral
	where
		gaussElimlzIfVectGCD2_gen :
			Dec (getCol FZ xs = Algebra.neutral)
			-> ( n' : Nat
				** (gexs : Matrix n' (S $ S prededm) ZZ
					** (rowEchelonPre gexs, gexs `bispanslz` xs)) )

		{-
		If first col neutral then we can reduce the process
		to that on the value of (map tail).
		-}

		gaussElimlzIfVectGCD2_gen (Yes prNeut) = runIdentity $ do {
			( nold ** (matold ** (echold, bisold)) )
				<- Id $ gaussElimlzIfVectGCD2 $ map tail xs
			return ( nold **
					(map ((Pos 0)::) matold
					** (echelonPreNullcolExtension echold
					, bispansNullcolExtension prNeut bisold)) )
			}

		{-
		Otherwise it's nonneutral, so we can show that since the elimFirstCol
		is DANRZ FZ FZ, its first row's leading nonzero entry is FZ. This leads
		to promoting the (rowEchelon) of one matrix to one with the same
		first row as the elimFirstCol.

		For a proof, compare with "Appendix Elim.General.Meta"
		-}

		gaussElimlzIfVectGCD2_gen (No prNonneut) = runIdentity $ do {
			-- Perform elimination on the first column.
			(xFCE::xsFCE ** (xnxsFCEdanrz, fceBisxs))
					<- Id $ elimFirstCol xs
			-- Recurse, eliminating the tail.
			(elimLen ** (xselim ** (xselimEch, coltailxsFCEBisElim)))
				<- Id $ gaussElimlzIfVectGCD2 $ map tail xsFCE

			{-
			Add the head of the first-column elimination
			to the tail's elimination to get the final elim.
			-}

			let endmat = xFCE::map ((Pos Z)::) xselim

			-- The final elim is bispannable with the original matrix.
			let xsNullcolextElimBisFCE = bispansNulltailcolExtension
				xnxsFCEdanrz coltailxsFCEBisElim
			-- Bispannability is preserved by consing a common vector
			let endmatBisxnFCE = bispansSamevecExtension
				xsNullcolextElimBisFCE xFCE
			-- This is hence bispannable with the original matrix.
			let endmatBisxs = bispanslztrans endmatBisxnFCE fceBisxs

			{-
			The first column being nonzero is invariant over the
			bispannability class,
			and we assumed (prNonneut) this to hold for (xs),
			thus it holds for (endmat).

			The first column being nonzero and the danrz for (endmat)
			imply (head endmat = xFCE) has (leadingNonzeroNum xFCE = Just 0).
			-}

			let headxFCELeadingNonzero = either
				( void
				. prNonneut
				. spansImpliesSameFirstColNeutrality (fst fceBisxs) )
				id
				$ danrzLeadingZeroAlt xnxsFCEdanrz

			{-
			Thus the hypothesis of (rowEchelonPreExtension) applies,
			and the final elim is row echelon.
			-}

			let endmatEch = rowEchelonPreExtension {x=xFCE}
				headxFCELeadingNonzero xselimEch

			return (_ ** (endmat ** (endmatEch, endmatBisxs)))

			}

{- Gaussian elimination in general -}

total
gaussElimlzIfVectGCD :
	(xs : Matrix n m ZZ)
	-> ( n' : Nat
		** (gexs : Matrix n' m ZZ
			** (rowEchelonPre gexs, gexs `bispanslz` xs)) )
gaussElimlzIfVectGCD {m=Z} xs = (_ ** (Algebra.neutral
	** (rowEchelonPreZeroWidth, bispanslzreflFromEq $ sym $ zeroVecVecId xs)))
gaussElimlzIfVectGCD {m=S predm} xs = gaussElimlzIfVectGCD2 xs

}

{-
Gaussian elimination from a GCD algorithm.
The premise of (gaussElimlzIfVect)s is equivalent to having a GCD.
-}

{- (gaussElimlzIfGCD) parameters -}
parameters (
	gcdAlg : (c, d : ZZ)
		-> ( zpar : (ZZ, ZZ) ** uncurry (bezQTy c d) zpar )
	) {

total
gaussElimlzIfGCD2 :
	(xs : Matrix n m ZZ)
	-> ( n' : Nat
		** (gexs : Matrix n' m ZZ
			** (rowEchelonPre gexs, gexs `bispanslz` xs)) )
gaussElimlzIfGCD2 = gaussElimlzIfVectGCD $ gcdToVectGCD gcdAlg

{- Render proper row echelon property -}

total
gaussElimlzIfGCD :
	(xs : Matrix n m ZZ)
	-> ( n' : Nat
		** (gexs : Matrix n' m ZZ
			** (rowEchelon gexs, gexs `bispanslz` xs)) )
gaussElimlzIfGCD xs = runIdentity $ do {
		(n' ** (gexs ** (echPre, bis))) <- Id $ gaussElimlzIfGCD2 xs
		return $ (n' ** (gexs ** (toRowEchelon echPre, bis)))
	}

} {- (gaussElimlzIfGCD) parameters -}

{-
The gaussian elimination instantiation derived from (bezoutZT)
-}

gaussElimlz :
	(xs : Matrix n m ZZ)
	-> ( n' : Nat
		** (gexs : Matrix n' m ZZ
			** (rowEchelon gexs, gexs `bispanslz` xs)) )
gaussElimlz = gaussElimlzIfGCD bezoutZT

{-

Appendix Elim.General.Meta

Case matrix has height > 0, width > 1 of gaussian elimination.

The following meta-analytic proof translates between the mathematical ideas and the realization in the formal logic.

---

Suppose we are to produce from a given (x::xs) of width > 1 a row-span-equivalent
row echelon matrix, given how to do this for all matrices of lesser height
and (nonzero) width, and given that the first column of (x::xs) is nonzero.

By (rowEchelonPreExtension), (leadingNonzeroNum v = Just FZ) & (rowEchelonPre vs)
--> row echelon v :: 0|vs

Eliminating the first column

	matchbind

converts a y::ys of width > 0 to an equivalent y' :: 0|ys' =: (yy'::yys') :: 0|ys'.

Being of this form is an unspoken equivalence to "danrz" (abbrev.): tautologically,
(downAndNotRightOfEntryImpliesZ (y'::0|ys') 0 0). Whence the type of & intention
behind (elimFirstCol).

	"y::ys === m where (m = y'::0|ys')"
	<==>
	y::ys `bispanslz` m & downAndNotRightOfEntryImpliesZ m 0 0

Since x::xs didn't have a 0 column, & bispannability preserves this (spansImpliesSameFirstColNeutrality), bispannability implies that xx' /= 0:

	"xx' /= 0"
	<==>
	lnzn x' = Just 0,

& the latter is proved through (danrzLeadingZeroAlt):

	danrz (_1::_2) 0 0, getCol 0 (_1::_2) /= 0
	==>	(danrzLeadingZeroAlt)
	(getCol 0 (_1::_2) = 0 | lnzn _1 = Just 0) & getCol 0 (_1::_2) /= 0
	==>
	lnzn _1 = Just 0

Eliminating ys' then gives a matrix equivalent to ys under bispannability

	matchbind

which is preserved (bispansSamevecExtension) by consing a common vector. Thus we can
convert each y::ys of width > 1 to an equivalent y' :: 0|zs =: (yy'::yys') :: 0|zs such
that yy' /= 0 and 0|zs is row echelon.

Sharing the head y' means preserving the leading nonzero of the head, shown to
be (Just 0).

Thus the hypothesis of (rowEchelonPreExtension) applies

	y'_0 /= 0 ==> leadingNonzeroNum y' = Just FZ

& we have that the y'::0|zs equivalent to the original y::ys is row echelon.

Such a matrix with the property of being equivalent to the original but row echelon is
wwtbd.

-}


text:
||| Additional properties and lemmata to do with Vect
module Data.Vect.Properties

import public Data.Vect.Properties.Tabulate
import public Data.Vect.Properties.Index
import public Data.Vect.Properties.Foldr
import public Data.Vect.Properties.Map
import public Data.Vect.Properties.Fin


text:
module Main

import Data.List
import Data.Vect

-- needs to be concretely in IO to test error messages
myPrintLn : String -> IO ()
myPrintLn = printLn

-- add some definition of (>>=) in another namespace
namespace Other
  public export
  (>>=) : IO a -> IO b -> IO b
  (>>=) f x = f *> x


text:
module Language.LSP.CodeAction.MakeCase

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.MakeClause
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Libraries.Data.PosMap
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.CaseSplit

currentLineRange : Int -> String -> Range
currentLineRange i origLine = MkRange (MkPosition i 0) (MkPosition i (cast $ length origLine))

isHole : Defs -> Name -> Core Bool
isHole defs n = do
  Just def <- lookupCtxtExact n (gamma defs)
    | Nothing => pure False
  pure $ case definition def of
    Hole _ _ => True
    _ => False

export
makeCaseKind : CodeActionKind
makeCaseKind = Other "refactor.rewrite.MakeCase"

isAllowed : CodeActionParams -> Bool
isAllowed params =
  maybe True (\filter => (makeCaseKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only

buildCodeAction : URI -> Name -> TextEdit -> CodeAction
buildCodeAction uri name edit =
  MkCodeAction
    { title       = "Make case for hole ?\{show name}"
    , kind        = Just RefactorRewrite
    , diagnostics = Nothing
    , isPreferred = Nothing
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }

export
makeCase : Ref LSPConf LSPConfiguration
        => Ref MD Metadata
        => Ref Ctxt Defs
        => Ref UST UState
        => Ref Syn SyntaxInfo
        => Ref ROpts REPLOpts
        => CodeActionParams -> Core (Maybe CodeAction)
makeCase params = do
  let True = isAllowed params
    | False => logI MakeCase "Skipped" >> pure Nothing
  logI MakeCase "Checking for \{show params.textDocument.uri} at \{show params.range}"

  withSingleLine MakeCase params (pure Nothing) $ \line => do
    withSingleCache MakeCase params MakeCase $ do
      nameLocs <- gets MD nameLocMap
      let col = params.range.start.character
      let Just (loc, name) = findPointInTreeLoc (line, col) nameLocs
        | Nothing => logD MakeCase "No name found at \{show line}:\{show col}}" >> pure Nothing
      logD MakeCase "Found name \{show name}"

      defs <- get Ctxt
      True <- isHole defs name -- should only work on holes
        | _ => logD MakeCase "\{show name} is not a metavariable" >> pure Nothing

      toBrack <- gets Syn (elemBy ((==) `on` dropNS) name . bracketholes)
      Just original <- getSourceLine (line + 1)
        | Nothing => logE MakeCase "Error while fetching the referenced line" >> pure Nothing
      litStyle <- getLitStyle
      let Right l = unlit litStyle original
         | Left err => logE MakeCase "Invalid literate Idris" >> pure Nothing
      let (markM, _) = isLitLine original
      let name' = dropAllNS name
      let caseText = makeCase toBrack (dropAllNS name') original
      let newText = maybe caseText (const (unlines $ map (relit markM) $ lines caseText)) markM
      let edit = MkTextEdit (currentLineRange line original) newText

      pure $ Just (cast loc, buildCodeAction params.textDocument.uri name' edit)


text:
||| The cardinal directions
data Direction = North
               | East
               | South
               | West

total turn : Direction -> Direction
turn North = East
turn East = South
turn South = West
turn West = North

||| A Shape
data Shape = ||| A triangle
             Triangle Double Double
           | ||| A rectangle
             Rectangle Double Double
           | ||| A circle
             Circle Double

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

||| A shape defined as a type function
data Shape' : Type where
  Triangle' : Double -> Double -> Shape'
  Rectangle' : Double -> Double -> Shape'
  Circle' : Double -> Shape'

data Nat = Z | S Nat

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
import Data.Fuel

%default covering -- total

interface X a where
  ls : Fuel -> List a

mutual

  X Nat where
    ls Dry      = []
    ls (More f) = [length $ the (List Bool) $ ls f]

  X Bool where
    ls Dry      = []
    ls (More f) = [null $ the (List Nat) $ ls f]

main : IO Unit
main =
  putStrLn $ show $ the (List Nat) $ ls $ limit 6


text:
module HRAL

-- Based on https://www.cambridge.org/core/services/aop-cambridge-core/content/view/CC82B2E79DC5CCAD57E0AC5DF0D43DEC/S0956796820000064a.pdf/div-class-title-heterogeneous-binary-random-access-lists-div.pdf

data Tree : Type -> Nat -> Type where
  Leaf : a -> Tree a Z
  Node : Tree a n -> Tree a n -> Tree a (S n)

data Path : Nat -> Type where
  Here : Path Z
  Left : Path n -> Path (S n)
  Right : Path n -> Path (S n)

namespace Tree
  lookup : Tree a n -> Path n -> a
  lookup (Leaf x) Here = x
  lookup (Node t1 t2) (Left p) = lookup t1 p
  lookup (Node t1 t2) (Right p) = lookup t2 p

data Bin : Type where
  End : Bin
  One : Bin -> Bin
  Zero : Bin -> Bin

bsucc : Bin -> Bin
bsucc End = One End
bsucc (One b) = Zero (bsucc b)
bsucc (Zero b) = One b

data RAL : Type -> Nat -> Bin -> Type where
  Nil : RAL a n End
  Cons1 : Tree a n -> RAL a (S n) b -> RAL a n (One b)
  Cons0 : RAL a (S n) b -> RAL a n (Zero b)

data Pos : Nat -> Bin -> Type where
  PosHere : Path n -> Pos n (One b)
  There0 : Pos (S n) b -> Pos n (Zero b)
  There1 : Pos (S n) b -> Pos n (One b)

namespace RAL
  lookup : RAL a n b -> Pos n b -> a
  lookup [] (PosHere _) impossible
  lookup [] (There0 _) impossible
  lookup [] (There1 _) impossible
  lookup (Cons1 t r) (PosHere p) = Tree.lookup t p
  lookup (Cons1 t r) (There1 p) = lookup r p
  lookup (Cons0 r) (There0 p) = lookup r p

  consTree : Tree a n -> RAL a n b -> RAL a n (bsucc b)
  consTree t [] = Cons1 t Nil
  consTree t (Cons1 t' r) = Cons0 (consTree (Node t t') r)
  consTree t (Cons0 r) = Cons1 t r

  cons : a -> RAL a Z b -> RAL a Z (bsucc b)
  cons x r = consTree (Leaf x) r

data HTree : Tree Type n -> Type where
  HLeaf : u -> HTree (Leaf u)
  HNode : HTree us -> HTree vs -> HTree (Node us vs)

data HPath : Tree Type n -> Type -> Type where
  HHere : HPath (Leaf u) u
  HLeft : HPath us u -> HPath (Node us vs) u
  HRight : HPath vs u -> HPath (Node us vs) u

namespace HTree
  lookup : HTree us -> HPath us u -> u
  lookup (HLeaf u) HHere = u
  lookup (HNode t1 t2) (HLeft p) = lookup t1 p
  lookup (HNode t1 t2) (HRight p) = lookup t2 p

data HRAL : RAL Type n b -> Type where
  HNil : HRAL Nil
  HCons1 : HTree t -> HRAL r -> HRAL (Cons1 t r)
  HCons0 : HRAL r -> HRAL (Cons0 r)

data HPos : RAL Type n b -> Type -> Type where
  HPosHere : HPath t u -> HPos (Cons1 t r) u
  HThere0 : HPos r u -> HPos (Cons0 r) u
  HThere1 : HPos r u -> HPos (Cons1 t r) u

namespace HRAL
  lookup : HRAL r -> HPos r u -> u
  lookup HNil (HPosHere _) impossible
  lookup HNil (HThere0 _) impossible
  lookup HNil (HThere1 _) impossible
  lookup (HCons1 t r) (HPosHere p) = HTree.lookup t p
  lookup (HCons1 t r) (HThere1 p) = lookup r p
  lookup (HCons0 r) (HThere0 p) = lookup r p

  consTree : HTree t -> HRAL r -> HRAL (RAL.consTree t r)
  consTree t HNil = HCons1 t HNil
  consTree t (HCons1 t' r) = HCons0 (consTree (HNode t t') r)
  consTree t (HCons0 r) = HCons1 t r

  cons : (u : Type) -> HRAL r -> HRAL (RAL.cons Type r)
  cons x r = consTree (HLeaf x) r

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Time

import Data.String
import Data.Nat
import Data.Fin
import Data.List1
import Data.List
import Data.Either
import Data.Maybe

import Text.Parser
import Text.Parser.Util

import System.File

-- HH:MM
record TimeUnit where
  constructor MkTimeUnit
  hours : Integer
  minutes : Integer

-- HH:MM-HH:MM
record TimeInterval where
  constructor MkTimeInterval
  start : TimeUnit
  end : TimeUnit

twoDigitNat : Parser Nat
twoDigitNat = do
  d0 <- digit
  d1 <- digit
  pure (10 * finToNat d0 + finToNat d1)

||| Discards whitespace.
||| N:N
parseTimeUnit : Parser TimeUnit
parseTimeUnit = do
  a <- twoDigitNat
  ignore $ many space
  ignore $ char ':'
  ignore $ many space
  b <- twoDigitNat
  pure (MkTimeUnit (cast a) (cast b))

parseTimeInterval : Parser TimeInterval
parseTimeInterval = do
  s <- parseTimeUnit
  ignore $ many space
  ignore $ char '-'
  ignore $ many space
  e <- parseTimeUnit
  pure (MkTimeInterval s e)

asymmetricDif : Integer -> Integer -> Integer -> (Bool, Integer)
asymmetricDif x y m =
  case (x <= y) of
    True => (True, y - x)
    False => (False, m - (x - y))

intervalDif : (start : TimeInterval) -> TimeUnit
intervalDif (MkTimeInterval (MkTimeUnit sh sm) (MkTimeUnit eh em)) =
  let (v, m) = asymmetricDif sm em 60 in
  let (_, h) = asymmetricDif sh eh 24 in
  MkTimeUnit (abs (h - if v then 0 else 1)) m

sum : TimeUnit -> TimeUnit -> TimeUnit
sum (MkTimeUnit a b) (MkTimeUnit c d) =
  let m = mod (b + d) 60 in
  let d = div (b + d) 60 in
  MkTimeUnit (a + c + d) m

showPadTwo : Integer -> String
showPadTwo x = case (x < 10) of
  True => "0" ++ show x
  False => show x

public export
Show TimeUnit where
  show (MkTimeUnit a b) = showPadTwo a ++ ":" ++ showPadTwo b

public export
Show TimeInterval where
  show (MkTimeInterval a b) = show a ++ "-" ++ show b

eTimeInterval : String -> Either String TimeInterval
eTimeInterval str =
  mapFst (const "Can't parse '\{str}'") (parseFull' parseTimeInterval str)

lineFilter : String -> Bool
lineFilter x = x /= ""
            && x /= "\n"
            && x /= "\r"
            && not (isPrefixOf "//" x)
            && not (isPrefixOf "--" x)

namespace Show
  namespace Str
    public export
    [Id]
    Show String where
      show x = x

  public export
  [NLSepList]
  (inner : Show a) => Show (List a) where
    show []        = ""
    show (x :: xs) = show x ++ show' xs
     where
      show' : List a -> String
      show' []        = ""
      show' (x :: xs) = "\n" ++ show x ++ show' xs

main : IO ()
main = do
  fileName <- getLine
  Right str <- readFile fileName
    | Left err => putStrLn (show err)
  let ls = lines str
  let ls = filter lineFilter ls
  putStrLn $ "Intervals:\n" ++ show @{NLSepList @{Id}} ls
  let ds =
       do ds <- for ls $ \l => do
             i <- eTimeInterval l
             Right (intervalDif i)
          Right $ foldr sum (MkTimeUnit 0 0) ds
  case ds of
    Left x => putStrLn ("Error: " ++ x)
    Right ds => putStrLn ("Total: " ++ show ds)

max_stars_repo_name: Russoul/Time-Interval

max_issues_repo_name: Russoul/Time-Interval

max_forks_repo_name: Russoul/Time-Interval


text:
module ImplicitCatenableDeque

import CatenableDeque

%default total
%access private

public export
interface Sized (d : Type -> Type) where
  size : d a -> Int

mutual
  export
  data ImplicitCatDeque : (Type -> Type) -> Type -> Type where
    Shallow : d a -> ImplicitCatDeque d a
    Deep : d a -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
        -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
        -> ImplicitCatDeque d a

  data CmpdElem : (Type -> Type) -> Type -> Type where
    Simple : d a -> CmpdElem d a
    Cmpd : d a -> Lazy (ImplicitCatDeque d (CmpdElem d a)) -> d a
        -> CmpdElem d a

dappendL : Deque d => d a {- size < 4 -} -> d a -> d a
dappendL d1 d2 =
  if isEmpty d1 then d2 else dappendL (assert_smaller d1 $ init d1) (cons (last d1) d2)

dappendR : Deque d => d a -> d a {- size < 4 -} -> d a
dappendR d1 d2 =
  if isEmpty d2 then d1 else dappendR (snoc d1 (head d2)) (assert_smaller d2 $ tail d2)

replaceHead : Deque d => a -> ImplicitCatDeque d a -> ImplicitCatDeque d a
replaceHead x (Shallow d) = Shallow (cons x (tail d))
replaceHead x (Deep f a m b r) = Deep (cons x (tail f)) a m b r

replaceLast : Deque d => ImplicitCatDeque d a -> a -> ImplicitCatDeque d a
replaceLast (Shallow d) x = Shallow (snoc (init d) x)
replaceLast (Deep f a m b r) x = Deep f a m b (snoc (init r) x)

share : Deque d => d a -> d a -> (d a, d a, d a)
share f r = let m = cons (last f) (cons (head r) empty) in (init f, m, tail r)

mutual
  export
  (Deque d, Sized d) => Deque (ImplicitCatDeque d) where
    empty = Shallow empty
    isEmpty (Shallow d) = isEmpty d
    isEmpty _ = False

    cons x (Shallow d) = Shallow (cons x d)
    cons x (Deep f a m b r) = Deep (cons x f) a m b r

    head (Shallow d) = head d
    head (Deep f a m b r) = head f

    tail (Shallow d) = Shallow (tail d)
    tail (Deep f a m b r) =
      if size f > 3 then Deep (tail f) a m b r
      else if not (isEmpty a) then
        case head a of
          (Simple d) => let f' = dappendL (tail f) d
                        in Deep f' (tail a) m b r
          (Cmpd f' c' r') => let f'' = dappendL (tail f) f'
                                 a'' = c' ++ replaceHead (Simple r') a
                             in Deep f'' a'' m b r
      else if not (isEmpty b) then
        case head b of
          (Simple d) => let f' = dappendL (tail f) m
                        in Deep f' empty d (tail b) r
          (Cmpd f' c' r') => let f'' = dappendL (tail f) m
                                 a'' = cons (Simple f') c'
                             in Deep f'' a'' r' (tail b) r
      else Shallow (dappendL (tail f) m) ++ Shallow r

    snoc (Shallow d) x = Shallow (snoc d x)
    snoc (Deep f a m b r) x = Deep f a m b (snoc r x)

    last (Shallow d) = last d
    last (Deep f a m b r) = last r

    init (Shallow d) = Shallow (init d)
    init (Deep f a m b r) =
      if size r > 3 then Deep f a m b (init r)
      else if not (isEmpty b) then
        case last b of
          (Simple d) => let r' = dappendR d (init r)
                        in Deep f a m (init b) r'
          (Cmpd f' c' r') => let r'' = dappendR r' (init r)
                                 b'' = replaceLast b (Simple f') ++ c'
                             in Deep f a m b'' r''
      else if not (isEmpty a) then
        case last a of
          (Simple d) => let r' = dappendR m (init r)
                        in Deep f (init a) d empty r'
          (Cmpd f' c' r') => let r'' = dappendR m (init r)
                                 b'' = snoc c' (Simple r')
                             in Deep f (init a) f' b'' r''
      else Shallow f ++ Shallow (dappendR m (init r))

  export
  (Deque d, Sized d) => CatenableDeque (ImplicitCatDeque d) where
    (Shallow d1) ++ (Shallow d2) =
      if size d1 < 4 then Shallow (dappendL d1 d2)
      else if size d2 < 4 then Shallow (dappendR d1 d2)
      else let (f, m, r) = share d1 d2 in Deep f empty m empty r
    (Shallow d) ++ (Deep f a m b r) =
      if size d < 4 then Deep (dappendL d f) a m b r
      else Deep d (cons (Simple f) a) m b r
    (Deep f a m b r) ++ (Shallow d) =
      if size d < 4 then Deep f a m b (dappendR r d)
      else Deep f a m (snoc b (Simple r)) d
    (Deep f1 a1 m1 b1 r1) ++ (Deep f2 a2 m2 b2 r2) =
      let (r1', m, f2') = share r1 f2
          a1' = snoc a1 (Cmpd m1 b1 r1')
          b2' = cons (Cmpd f2' a2 m2) b2
      in Deep f1 a1' m b2' r2


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

import Config.JSON

import Lightyear.Testing

%access export

jsonTest1 : TestReport
jsonTest1 = parseTest "JSON Test 1"
                      parseJSONFile
                      """{
          "firstName": "John",
          "lastName": "Smith",
          "isAlive": true,
          "age": 25,
          "height_cm": 167.6,
          "address": {
              "streetAddress": "21 2nd Street",
              "city": "New York",
              "state": "NY",
              "postalCode": "10021-3100"
          },
          "phoneNumbers": [
              {
                  "type": "home",
                  "number": "212 555-1234"
              },
              {
                  "type": "office",
                  "number": "646 555-4567"
              }
          ],
          "children": [],
          "spouse": null
      }
      """

jsonTest2 : TestReport
jsonTest2 = parseTest "JSON Test 2"
                      parseJSONFile
                      """{
        "$schema": "http://json-schema.org/draft-03/schema#",
        "name": "Product",
        "type": "object",
        "properties": {
            "id": {
                "type": "number",
                "description": "Product identifier",
                "required": true
            },
            "name": {
                "type": "string",
                "description": "Name of the product",
                "required": true
            },
            "price": {
                "type": "number",
                "minimum": 0,
                "required": true
            },
            "tags": {
                "type": "array",
                "items": {
                    "type": "string"
                }
            },
            "stock": {
                "type": "object",
                "properties": {
                    "warehouse": {
                        "type": "number"
                    },
                    "retail": {
                        "type": "number"
                    }
                }
            }
        }
    }
    """

jsonTest3 : TestReport
jsonTest3 = parseTest "JSON Test 3"
                      parseJSONFile
                      """{
    "firstName": "John",
    "lastName": "Smith",
    "isAlive": true,
    "age": 25,
    "height_cm": 167.6,
    "address": {
        "streetAddress": "21 2nd Street",
        "city": "New York",
        "state": "NY",
        "postalCode": "10021-3100"
    },
    "phoneNumbers": [
        {
            "type": "home",
            "number": "212 555-1234"
        },
        {
            "type": "office",
            "number": "646 555-4567"
        }
    ],
    "children": [],
    "spouse": null
    }
    """

runTests : IO ()
runTests = Testing.runTests [jsonTest1, jsonTest2, jsonTest3]

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module SqEq0

sqeq0 : (a, b : Nat) -> a*a + b*b = 0 -> (a = 0, b = 0)
sqeq0 0 0 Refl = (Refl, Refl)


text:
module Main

import System

import Task
import Helpers

%default total

-- Tests -----------------------------------------------------------------------
--
-- NOTE: Tasks ending in `'` need user input
--

-- Helpers --

edit : Int -> Task (PRIM INT)
edit = pure

--FIXME: due to some namespacing problem...
del : Nat -> List a -> List a
del = Helpers.delete
rep : Nat -> a -> List a -> List a
rep = Helpers.replace

-- Basics --

fourtytwo : Task (PRIM INT)
fourtytwo = pure 42

hello : Task (PRIM STRING)
hello = pure "Hello"

inc : Int -> Task (PRIM INT)
inc x = pure (x + 1)

add : Int -> Int -> Task (PRIM INT)
add x y = pure (x + y)

append : String -> String -> Task (PRIM STRING)
append x y = pure (x ++ y)

-- Steps --

pureStep : Task (PRIM INT)
pureStep = do
  x <- fourtytwo
  inc x

pureStep' : Task (PRIM INT)
pureStep' = "Hello" # (
    fourtytwo >>? \x =>
    inc x
  )

pureStep'' : Task (PRIM INT)
pureStep'' =
  ("Hello" # fourtytwo) >>? \x =>
  inc x

oneStep : Task (PRIM INT)
oneStep = do
  x <- edit 0
  inc x

oneStep' : Task (PRIM INT)
oneStep' =
  edit 0 >>? \x =>
  inc x

twoSteps : Task (PRIM INT)
twoSteps = do
  x <- edit 1
  y <- edit 2
  add x y

twoSteps' : Task (PRIM INT)
twoSteps' =
  edit 1 >>? \x =>
  edit 2 >>? \y =>
  add x y

-- Parallel --

parallel : Task (PAIR (PRIM INT) (PRIM STRING))
parallel = "Give an integer" # ask (PRIM INT) <&> hello

parallelStep : Task (PRIM STRING)
parallelStep = do
  ( n, m ) <- parallel
  pure (unwords $ replicate (cast n) m)

parallelStep' : Task (PRIM STRING)
parallelStep' =
  parallel >>? \( n, m ) =>
  pure (unwords $ replicate (cast n) m)

-- Normalisation --
--
-- FIXME: should these automatically simplify?

pair : Task (PAIR (PRIM INT) (PRIM INT))
pair = pure 3 <&> pure 8

inner : Task (PRIM INT)
inner = do
  ( x, y ) <- pair
  add x y

inner' : Task (PRIM INT)
inner' =
  pair >>? \( x, y ) =>
  add x y

-- Shared Data --

partial
editList : Task (PAIR (PRIM UNIT) (LIST (PRIM INT)))
editList = do
  l <- ref (LIST (PRIM INT)) []
  start l <&> watch l

where

  delete : Loc (LIST (PRIM INT)) -> Nat -> Task (PRIM UNIT)
  delete l i =
    modify (LIST (PRIM INT)) l (del i)

  replace : Loc (LIST (PRIM INT)) -> Nat -> Task (PRIM UNIT)
  replace l i =
    "Give a new value" # ask (PRIM INT) >>? \x =>
    modify (LIST (PRIM INT)) l (rep i x)

  change : Loc (LIST (PRIM INT)) -> Task (PRIM UNIT)
  change l =
    --NOTE: `deref` should be before the external step,
    --      otherwise we'll end up an a state where we show an editor with the list when the user entered an improper index.
    --      Compare this with iTasks though:
    --      `deref` should be before the external step because you cannot specify the `deref` inside the step list!
    deref (LIST (PRIM INT)) l >>= \xs =>
    "Give an index" # ask (PRIM INT) >>? \n =>
    let i = the Nat (cast n) in
    if i < List.length xs then
      "Delete" # delete l i <?> "Replace" # replace l i
    else
      fail

  prepend : Loc (LIST (PRIM INT)) -> Task (PRIM UNIT)
  prepend l =
    "Give a new value to prepend" # ask (PRIM INT) >>? \x =>
    modify (LIST (PRIM INT)) l ((::) x)

  clear : Loc (LIST (PRIM INT)) -> Task (PRIM UNIT)
  clear l =
    modify (LIST (PRIM INT)) l (const [])

  quit : Task (PRIM UNIT)
  quit = pure ()

  mutual
    partial
    repeat : Loc (LIST (PRIM INT)) -> Task (PRIM UNIT)
    repeat l = do
      "Prepend" # prepend l <?> "Clear" # clear l <?> "Change" # change l
      start l

    partial
    start : Loc (LIST (PRIM INT)) -> Task (PRIM UNIT)
    start l =
      "Edit" # repeat l <?> "Quit" # quit

update1 : Loc (PRIM INT) -> Task (PRIM INT)
update1 l = do
  n <- ask (PRIM INT)
  assign (PRIM INT) l n
  m <- ask (PRIM INT)
  modify (PRIM INT) l ((+) m)
  edit !(deref (PRIM INT) l)

update2 : Loc (PRIM INT) -> Task (PRIM UNIT)
update2 l =
  deref (PRIM INT) l >>= \x =>
  edit (x + 1) >>? \y =>
  assign (PRIM INT) l y >>= \() =>
  deref (PRIM INT) l >>= \u =>
  edit (u + 2) >>? \v =>
  assign (PRIM INT) l v

inspect : Show (typeOf a) => (Loc (PRIM INT) -> Task a) -> Task (PAIR a (PRIM INT))
inspect f = do
  l <- ref (PRIM INT) 0
  f l <&> watch l

-- inspect : Show (typeOf a) => Show (typeOf b) => (Loc b -> Task a) -> Task (PAIR a (PRIM b))
-- inspect {b} f = do
--   l <- init b
--   f l <&> watch l

doubleShared : Task (PAIR (PRIM UNIT) (PRIM INT))
doubleShared = do
  l <- ref (PRIM INT) 0
  m <- ref (PRIM INT) 0
  let t1 = do
    x <- the (Task (PRIM INT)) $ watch m
    if x >= 10 then edit (x * 2) else fail
  let t2 = do
    y <- the (Task (PRIM INT)) $ watch l
    if y >= 5 then assign (PRIM INT) m 12 else fail
  t2 <&> t1

-- Choices --

pick1 : Task (PRIM INT)
pick1 = fail <|> edit 0

pick2 : Task (PRIM INT)
pick2 = edit 1 <|> edit 2

pick3 : Task (PRIM INT)
pick3 = pick2 <|> edit 3

pick1' : Task (PRIM INT)
pick1' = "Fail" # fail <?> "Cont" # edit 0

pick2' : Task (PRIM INT)
pick2' = "Pick one of two" # ("First" # edit 1 <?> "Second" # edit 2)

pick3' : Task (PRIM INT)
pick3' = "Pick one of three" # (pick2' <?> "Third" # edit 3)

-- Guards --

auto : Task (PRIM STRING)
auto = do
  x <- ask (PRIM INT)
  if x >= 10 then pure "large" else fail

actions : Task (PRIM INT)
actions =
  ask (PRIM INT) >>? \x =>
  pick3

actions' : Task (PRIM INT)
actions' =
  ask (PRIM INT) >>? \x =>
  pick3'

guards : Task (PRIM STRING)
guards = do
  x <- ask (PRIM INT)
  "Large" # (if x >= 10 then pure "large" else fail)
    <?>
    "VeryLarge" # (if x >= 100 then pure "very large" else fail)

guards' : Task (PRIM STRING)
guards' = do
  ask (PRIM INT) >>? \x =>
  ("Large" # (if x >= 10 then pure "large" else fail)
    <?>
    "VeryLarge" # (if x >= 100 then pure "very large" else fail))

partial -- due to `mod` on `0`
branch : Task (PRIM STRING)
branch =
  edit 1 >>? \x =>
  if x `mod` 3 == 0 then
    pure "multiple of 3"
  else if x `mod` 5 == 0 then
    pure "multiple of 5"
  else
    fail

-- Empty edit --

empties : Task (PRIM INT)
empties = do
  ( x, y ) <- ask (PRIM INT) <&> ask (PRIM INT)
  pure (x + y)

-- Running ---------------------------------------------------------------------
%default covering

get : IO Input
get = do
  putStr ">> "
  input <- getLine
  case input of
    "quit" => System.exit 0
    _ =>
      case Task.Input.parse (words input) of
        Right event => do
          pure event
        Left msg => do
          putStrLn msg
          get

loop : Show (typeOf a) => Task a -> IO ()
loop task = do
  putStrLn !(Task.ui task)
  putStrLn $ "Possibilities: " ++ show !(Task.inputs task)
  event <- get
  loop !(Task.run task event)

run : Show (typeOf a) => Task a -> IO ()
run task = loop !(Task.initialise task)

main : IO ()
main = run empties

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
import Data.Vect

test : Vect 33 Int -> IO Int
test bytes_list = do
  let int1 = (index 0 bytes_list * 8) +
             (index 1 bytes_list * 4) +
             (index 2 bytes_list * 2) + (index 3 bytes_list)
  let int2 = (index 4 bytes_list * 8) + (index 5 bytes_list * 4) + (index 6 bytes_list * 2) + (index 7 bytes_list)
  let int3 = (index 8 bytes_list * 8) + (index 9 bytes_list * 4) + (index 10 bytes_list * 2) + (index 11 bytes_list)
  let int4 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int5 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int6 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int7 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int8 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int9 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  let int10 = (index 12 bytes_list * 8) + (index 13 bytes_list * 4) + (index 14 bytes_list * 2) + (index 15 bytes_list)
  pure int1