text:
module Dbcritic.Check.PrimaryKeyBigint

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

formatTypeByteSize : String -> String
formatTypeByteSize type =
    case byteSizeOfType type of
        Nothing => "unknown"
        Just byteSize => show byteSize
    where
        byteSizeOfType : String -> Maybe Int
        byteSizeOfType "smallint" = Just 2
        byteSizeOfType "integer" = Just 4
        byteSizeOfType _ = Nothing

mkIssue : String -> String -> String -> String -> Issue
mkIssue schema table column columnType =
    let
        fullTable      = schema ++ "." ++ table
        identifier     = [ schema, table, column ]
        description    = "The table ‘" ++ fullTable ++ "’ primary key (" ++ column ++ ") is "
                         ++ "of type ‘" ++ columnType ++ "’ instead of ‘bigint’."
        columnByteSize = formatTypeByteSize columnType
        problems       = [ "PostgreSQL's " ++ columnType ++ " type is " ++ columnByteSize
                         ++ " bytes. It is relatively easy to run out of values." ]
        solutions      = [ "Change the type of ‘" ++ fullTable ++ "." ++ column ++ "’ to ‘bigint’, "
                         ++ "as well as its associated auto generating sequence if it exists." ]
    in
        MkIssue identifier description problems solutions IsNonEmpty IsNonEmpty IsNonEmpty

export
checkPrimaryKeyBigint : Check
checkPrimaryKeyBigint = MkCheck name help inspect
    where
    name = "primary_key_bigint"
    help = "Check that there are no tables with a smallint or integer primary key."

    inspectRow : List (Maybe String) -> IOExcept String Issue
    inspectRow [Just schema, Just table, Just column, Just columnType] =
                   pure (mkIssue schema table column columnType)
    inspectRow _ = ioe_fail "checkPrimaryKeyBigint: Bad result"

    inspect : PgConnection -> IOExcept String (List Issue)
    inspect conn = do
        res <- pgExecute conn """
            SELECT
                kcu.table_schema as schema_name,
                kcu.table_name as table_name,
                kcu.column_name as column_name,
                c.data_type as column_type
            FROM information_schema.table_constraints tc
            JOIN information_schema.key_column_usage kcu
                ON kcu.constraint_name = tc.constraint_name
                AND kcu.constraint_schema = tc.constraint_schema
                AND kcu.constraint_name = tc.constraint_name
            JOIN information_schema.columns c
                ON c.table_schema = kcu.table_schema
                AND c.table_name = kcu.table_name
                AND c.column_name = kcu.column_name
            WHERE tc.constraint_type = 'PRIMARY KEY'
            AND c.data_type IN ('smallint', 'integer')
            ORDER BY schema_name, table_name
        """
        traverse inspectRow (pgGrid res)

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
module TreeQ2

%default total
%access public export

data Qry : (Type -> Type) -> Type -> Type where
  ||| Pure for monad/applicative: lift a plain value into the tree
  Pure : a -> Qry q a
  ||| Lift a query into the tree
  Lift : q i -> (i -> a) -> Qry q a
  ||| Gives us a monoid operation
  Attach : Qry q a -> q i -> ((a, i) -> b) -> Qry q b

liftQ : q a -> Qry q a
liftQ qry = Lift qry id

infixr 5 ^+^

||| Generalized semigroup operation. Not nearly as simple as the tree version.
||| This does not bode well. Moreover, one wonders what all this extra wrapping
||| will do to F# if translated to it...
(^+^) : Qry q a -> Qry q b -> Qry q (a, b)
(Pure x) ^+^ (Pure y) = Pure (x, y)
(Lift q h) ^+^ (Pure x) = Lift q (\y => (h y, x))
(Attach q r h) ^+^ (Pure x) = Attach q r (\y => (h y, x))
(Pure x) ^+^ (Lift q h) = Lift q (\y => (x, h y))
(Lift q h) ^+^ (Lift r i) = Attach (Lift q h) r (\(x, y) => (x, i y))
(Attach q r h) ^+^ (Lift s i) = Attach (Attach q r h) s (\(x, y) => (x, i y))
(Pure x) ^+^ (Attach q r h) = Attach q r (\y => (x, h y))
(Lift q h) ^+^ (Attach s r i) =
  Attach (Attach s q id) r (\((b, a), c) => (h a, i (b, c)))
(Attach q r h) ^+^ (Attach s t i) =
  Attach (Attach (q ^+^ s) r id) t (\(((a, c), b), d) => (h (a, b), i (c, d)))

||| TODO Now I'm not sure I'm at all careful enough in my implementation. I may
||| accidentally be assuming commutivity of the underlying semigroup.
Semigroup a => Semigroup (Qry q a) where
  (Pure y) <+> (Pure x) = Pure (x <+> y)
  (Lift y f) <+> (Pure x) = Lift y ((<+> x) . f)
  (Attach y z f) <+> (Pure x) = Attach y z ((<+> x) . f)
  (Pure y) <+> (Lift x f) = Lift x ((<+> y) . f)
  (Lift y g) <+> (Lift x f) = Attach (Lift y g) x (uncurry (<+>) . map f)
  (Attach y z g) <+> (Lift x f) =
    Attach (Attach y z g) x (\(a, b) => a <+> f b)
  (Pure z) <+> (Attach x y f) = Attach x y ((<+> z) . f)
  (Lift z g) <+> (Attach x y f) =
    Attach (Attach x y f) z (\(a, b) => a <+> g b)
  (Attach z w g) <+> (Attach x y f) = ?semigroup_huh_6

-- Augh I give up this is madness. If I were to succeed, I can't even imagine
-- how hard it would be to prove this all correct or translate it into anything
-- in F#.

ext: idr


text:
module Command

%default total

public export
data Command : Type where
  TurnLeft : Command
  TurnRight : Command
  Forward : Command

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
module Main

import Data.Strings

%default total

readNum : HasIO io => io (Maybe Nat)
readNum = do putStr "Enter a number: "
             ns <- getLine
             case all isDigit (unpack ns) of
                  False => pure Nothing
                  True => pure $ Just (stringToNatOrZ ns)

addNums : HasIO io => io (Maybe Nat)
addNums = do Just n <- readNum
              | Nothing => do putStrLn "Error: first input is not a number"
                              pure Nothing
             Just m <- readNum
               | Nothing => do putStrLn "Error: second input is not a number"
                               pure Nothing
             pure $ Just (n + m)

main : HasIO io => io ()
main = do Just sum <- addNums
            | Nothing => pure ()
          printLn sum

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module UI.Curses

%include C "curses.h"
%include C "cursesrun.h"
%link C "cursesrun.o"
%lib C "curses"

%access private

||| A window, also known as screen.
|||
||| This is used to interface with certain C functions.
data Window = MkWindow Ptr

||| The modes that `getCh` can use to get characters.
public export
data GetChMode : Type where
  ||| `getCh` waits for the user to press a key, but doesn't affect interrupt
  ||| and control flow characters.
  WaitForever           : GetChMode
  ||| `getCh` waits for the user to press a key, allows the program to determine
  ||| what happens when interrupt or control flow characters are encountered.
  WaitForeverRaw        : GetChMode
  ||| `getCh` waits for a certain amount of time before returning Nothing.
  ||| Doesn't affect interrupt and control flow characters.
  ||| @k tenths of a second `getCh` will wait
  Wait                  : (k : Nat) -> GetChMode
  ||| `getCh` waits for the user to press a key, but the program doesn't
  ||| receive any information about which keys have been pressed until a
  ||| newline character is encountered. Doesn't affect interrupt and control
  ||| flow characters.
  WaitForeverLinebuf    : GetChMode
  ||| `getCh` waits for the user to press a key, but the program doesn't
  ||| receive any information about which keys have been pressed until a newline
  ||| character is encountered. Allows the program to determine what happens
  ||| when interrupt or control flow characters are encountered.
  WaitForeverLinebufRaw : GetChMode

||| These are the color that are defined once curses is initialized.
|||
||| Note that some terminals may display some colors differently.
public export
data Color = Black
           | Red
           | Green
           | Yellow
           | Blue
           | Magenta
           | Cyan
           | White

||| This is necessary to use colors.
public export
data ColorPair : Type where
  ||| Use this constructor to make a ColorPair.
  ||| @i index of the ColorPair
  ||| @foreground foreground color
  ||| @background background color
  MkColorPair : (i : Nat) -> (foreground : Color) -> (background : Color) ->
    ColorPair

||| These are the attributes that can be used to print text in various ways.
|||
||| Note that some terminals may not support all of these attributes.
public export
data Attr : Type where
  ||| Prints text normally.
  Normal      : Attr
  ||| Highlights the printed text.
  Standout    : Attr
  ||| Puts a line under printed text.
  Underline   : Attr
  ||| Reverses the foreground and background colors.
  Reverse     : Attr
  ||| Prints blinking text.
  Blink       : Attr
  ||| Prints half bright text.
  Dim         : Attr
  ||| Prints bold text.
  Bold        : Attr
  ||| Prints with an alternate character set.
  AltCharSet  : Attr
  ||| Prints out invisible text.
  Invis       : Attr
  ||| Protects printed text.
  Protect     : Attr

namespace Cursor
  ||| These are the available cursor states.
  public export
  data CursorState = Invisible
                   | Normal
                   | VeryVisible

||| These are special characters, which can be converted into regular
||| Characters with the function `specialChar`.
public export
data SpecialChar = Escape
                 | Backspace
                 | Up
                 | Down
                 | Left
                 | Right
                 | F1
                 | F2
                 | F3
                 | F4
                 | F5
                 | F6
                 | F7
                 | F8
                 | F9
                 | F10
                 | F11
                 | F12
                 | Insert
                 | Delete
                 | Home
                 | End
                 | PageUp
                 | PageDown
                 | Tab
                 | Enter

||| Converts a `SpecialChar` into a regular `Char`.
public export
specialChar : SpecialChar -> Char
specialChar Escape    = '\ESC'
specialChar Backspace = '\263'
specialChar Up        = '\259'
specialChar Down      = '\258'
specialChar Left      = '\260'
specialChar Right     = '\261'
specialChar F1        = '\410'
specialChar F2        = '\266'
specialChar F3        = '\267'
specialChar F4        = '\268'
specialChar F5        = '\269'
specialChar F6        = '\270'
specialChar F7        = '\271'
specialChar F8        = '\272'
specialChar F9        = '\273'
specialChar F10       = '\274'
specialChar F11       = '\275'
specialChar F12       = '\276'
specialChar Insert    = '\331'
specialChar Delete    = '\330'
specialChar Home      = '\262'
specialChar End       = '\360'
specialChar PageUp    = '\339'
specialChar PageDown  = '\338'
specialChar Tab       = '\t'
specialChar Enter     = '\n'

intToCursorState : Int -> Maybe CursorState
intToCursorState 0 = Just Invisible
intToCursorState 1 = Just Normal
intToCursorState 2 = Just VeryVisible
intToCursorState _ = Nothing

cursorStateToInt : CursorState -> Int
cursorStateToInt Invisible   = 0
cursorStateToInt Normal      = 1
cursorStateToInt VeryVisible = 2

colorToInt : Color -> Int
colorToInt Black   = 0
colorToInt Red     = 1
colorToInt Green   = 2
colorToInt Yellow  = 3
colorToInt Blue    = 4
colorToInt Magenta = 5
colorToInt Cyan    = 6
colorToInt White   = 7

attrToInt : Attr -> Int
attrToInt Normal     = 0
attrToInt Standout   = pow 2 16
attrToInt Underline  = pow 2 17
attrToInt Reverse    = pow 2 18
attrToInt Blink      = pow 2 19
attrToInt Dim        = pow 2 20
attrToInt Bold       = pow 2 21
attrToInt AltCharSet = pow 2 22
attrToInt Invis      = pow 2 23
attrToInt Protect    = pow 2 24

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

idrBool : Int -> Bool
idrBool = (/= 0)

errOkToBool : Int -> Bool
errOkToBool = (/= (-1))

||| Returns the standard window.
stdScr : IO Window
stdScr = map MkWindow $ foreign FFI_C "stdScr" (IO Ptr)

noDelay : Bool -> IO ()
noDelay bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "nodelay" (Ptr -> Int -> IO ()) scr (cBool bf)

halfDelay : Int -> IO ()
halfDelay delay = foreign FFI_C "halfdelay" (Int -> IO ()) delay

||| Enables or disables the reading of function keys, arrow keys, and so on.
||| This is turned on by default.
||| @bf  if `True`, enables reading, if `False`, disables it
export
keypad : (bf : Bool) -> IO ()
keypad bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "keypad" (Ptr -> Int -> IO ()) scr (cBool bf)

meta : Bool -> IO ()
meta bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "meta" (Ptr -> Int -> IO ()) scr (cBool bf)

leaveOk : Bool -> IO Int
leaveOk bf = do
  (MkWindow scr) <- stdScr
  foreign FFI_C "leaveok" (Ptr -> Int -> IO Int) scr (cBool bf)

nl : Bool -> IO ()
nl True  = foreign FFI_C "nl"   (IO ())
nl False = foreign FFI_C "nonl" (IO ())

||| `echo` determines whether a character will be printed when the user presses
||| a key
||| @bf whether or not the echo will be on
export
echo : (bf : Bool) -> IO ()
echo False = foreign FFI_C "noecho" (IO ())
echo True  = foreign FFI_C "echo"   (IO ())

cBreak : Bool -> IO ()
cBreak True  = foreign FFI_C "cbreak"   (IO ())
cBreak False = foreign FFI_C "nocbreak" (IO ())

raw : Bool -> IO ()
raw True  = foreign FFI_C "raw"   (IO ())
raw False = foreign FFI_C "noraw" (IO ())

||| Return `True` if the terminal supports colors, false otherwise. This
||| function may not return correct results if `startCurses` has not been
||| called.
export
hasColors : IO Bool
hasColors = map idrBool $ foreign FFI_C "has_colors" (IO Int)

||| Refreshes the screen. It is unlikely that a program needs to manually
||| call this function.
export
refresh : IO ()
refresh = foreign FFI_C "refresh" (IO ())

||| This function must be called before colors can be used. Note that not all
||| terminals support colors. Use `hasColors` to find out whether the terminal
||| the program runs on supports colors.
export
startColor : IO ()
startColor = refresh *> foreign FFI_C "start_color" (IO ())

initScr : IO Window
initScr = map MkWindow $ foreign FFI_C "initscr" (IO Ptr)

||| Terminates curses. This should *always* be called before the program
||| terminates.
export
endWin : IO ()
endWin = foreign FFI_C "endwin" (IO ())

||| Returns the size of the standard window.
|||
||| The format is `(lines, columns)`.
export
scrSize : IO (Int, Int)
scrSize = [| MkPair (foreign FFI_C "getLines" (IO Int))
                    (foreign FFI_C "getCols"  (IO Int)) |]

||| Initializes a color pair.
initPair : ColorPair -> IO ()
initPair (MkColorPair natIndex colorFG colorBG) =
  foreign FFI_C "init_pair" (Int -> Int -> Int -> IO ()) (i + 1) fg bg
  where
    i : Int
    i = toIntNat natIndex
    fg  : Int
    fg  = colorToInt colorFG
    bg  : Int
    bg  = colorToInt colorBG

setAttr : Int -> IO ()
setAttr a = foreign FFI_C "attrset" (Int -> IO ()) a

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s        the string that will be printed
||| @maxChars specifies the maximum number of characters that will be printed
export
addNStr : (s : String) -> (maxChars : Nat) -> IO ()
addNStr s n = foreign FFI_C "addnstr" (String -> Int -> IO ()) s (toIntNat n)

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s the string that will be printed
export
addStr : (s: String) -> IO ()
addStr s = foreign FFI_C "addstr" (String -> IO ()) s

||| Prints a character to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @c the character that will be printed
export
addCh : (c : Char) -> IO ()
addCh c = foreign FFI_C "addch" (Char -> IO ()) c

||| Clears the screen to the end of the line.
export
clrToEol : IO ()
clrToEol = foreign FFI_C "clrtoeol" (IO ())

||| Moves the cursor to the specified coordinates.
||| Returns `True` if the cursor was moved, `False` otherwise.
||| @y the line to which the cursor will move (counting starts at 0)
||| @x the column to which the cursor will move (counting starts at 0)
export
move : (y : Int) -> (x : Int) -> IO Bool
move y x = map errOkToBool $ foreign FFI_C "move" (Int -> Int -> IO Int) y x

curs_set : Int -> IO Int
curs_set x = foreign FFI_C "curs_set" (Int -> IO Int) x

||| Sets the cursor state. Returns `Nothing`, if the specified cursor state
||| cannot be set, and `Just` the previous cursor state otherwise.
||| @cs the cursor state that will be set
export
cursSet : (cs : CursorState) -> IO $ Maybe CursorState
cursSet Invisible = leaveOk True  *> curs_set 0 >>= pure . intToCursorState
cursSet cs = leaveOk False *> curs_set (cursorStateToInt cs) >>=
  pure . intToCursorState

||| Returns the current cursor position.
||| The format is `(line, column)`.
export
getYX : IO (Int, Int)
getYX = do
  (MkWindow scr) <- stdScr
  [| MkPair (foreign FFI_C "getY" (Ptr -> IO Int) scr)
            (foreign FFI_C "getX" (Ptr -> IO Int) scr) |]

||| Returns the highest line and column the cursor can be at.
||| The format is `(line, column)`.
export
getMaxYX : IO (Int, Int)
getMaxYX = scrSize >>= \(row, col) => pure (row - 1, col - 1)

getch : IO Int
getch = foreign FFI_C "getch" (IO Int)

||| Clears the screen.
export
clear : IO ()
clear = foreign FFI_C "clear" (IO ())

colorPair : Int -> IO Int
colorPair i = foreign FFI_C "COLOR_PAIR" (Int -> IO Int) (i + 1)

||| Sets all given attributes and the specified colors. Note that this function
||| will not affect colors unless the terminal supports colors (which you can
||| check with `hasColors`) and `startColors` has been called.
||| @attrs  the attributes that will be set
||| @colors if this is `Nothing`, the default colors will be used, which are
|||           usually white on black; if this is not `Nothing`, the specified
|||           Pair will be initialized and used - note that if characters on the
|||           screen use the pair with index *i*, and the pair with index *i* is
|||           then reinitialized with different colors, the characters that are
|||           already on the screen will change their color
export
setAttrAndColor : (attrs : List Attr) -> (colors : Maybe ColorPair) -> IO ()
setAttrAndColor as c = do
    refresh
    for_ c initPair
    col <- colorAttr
    setAttr $ combineAttr col as
  where
    combineAttr : Int -> List Attr -> Int
    combineAttr col = foldr prim__orInt col . map attrToInt
    intIndex : ColorPair -> Int
    intIndex (MkColorPair i _ _) = toIntNat i
    colorAttr : IO Int
    colorAttr = maybe (pure 0) (colorPair . intIndex) c

||| Advances the cursor to the next position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
export
moveNextCh : IO Bool
moveNextCh = do
  (maxY, maxX) <- getMaxYX
  (y, x) <- getYX
  let (newY, newX, success) = if x >= maxX
    then if y >= maxY then (maxY, maxX, False) else (y + 1, 0, True)
    else (y, x + 1, True)
  move newY newX
  pure success

||| Moves the cursor to the previous position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
export
movePrevCh : IO Bool
movePrevCh = do
  (maxY, maxX) <- getMaxYX
  (y, x) <- getYX
  let (newY, newX, success) = if x <= 0
    then if y <= 0 then (0, 0, False) else (y - 1, maxX, True)
    else (y, x - 1, True)
  move newY newX
  pure success

||| Returns `Just` a character, or `Nothing` if the `GetChMode` is `Wait k` and
||| the time runs out. See `GetChMode` for more information.
export
getCh : IO $ Maybe Char
getCh = do
  refresh
  c <- getch
  pure $ if c == (-1) then Nothing else pure $ chr c

||| Returns a character once the user presses a key. This function is affected
||| by whether or not the `GetChMode` is a "raw" or a "linebuf" mode.
export
forceCh : IO Char
forceCh = do
  refresh
  c <- getch
  if c == (-1) then forceCh else pure $ chr c

||| Returns a `String` the user enters. This function is affected by whether or
||| not the `GetChMode` is a "raw" mode.
||| @useEcho  if `True`, the user will see the `String` they enter
||| @setEcho  if `True`, echo will be on after the `String` has been returned,
|||             otherwise, echo will be off
export
getStr : (useEcho : Bool) -> (setEcho : Bool) -> IO String
getStr useEcho setEcho = do
    echo useEcho
    (y, x) <- getYX
    str <- map reverse $ getRawStr y x ""
    echo setEcho
    pure str
  where
    mayMovePrev : IO Bool
    mayMovePrev = if useEcho then movePrevCh else pure False
    mayMoveNext : IO Bool
    mayMoveNext = if useEcho then moveNextCh else pure False
    mayMove : Int -> Int -> IO Bool
    mayMove y x = if useEcho then move y x else pure False
    mayAddCh : Char -> IO ()
    mayAddCh c = when useEcho $ addCh c
    safeTail : List a -> List a
    safeTail [] = []
    safeTail (_ :: xs) = xs
    getRawStr : Int -> Int -> String -> IO String
    getRawStr initY initX str = do
      (preY, preX) <- getYX
      c <- forceCh
      (y, x) <- getYX
      case c of
        '\n'   => mayMove preY preX *> pure str
        '\263' => if y <= initY && x < initX
          then mayMove preY preX *> getRawStr initY initX str
          else do if (preY, preX) == (y, x)
                    then mayMovePrev *> mayAddCh ' ' *> mayMovePrev *> pure ()
                    else mayAddCh ' ' *> mayMove y x *> pure ()
                  getRawStr initY initX . pack . safeTail . unpack $ str
        char => getRawStr initY initX $ strCons char str

||| Sets the mode `getCh` will operate in.
export
setGetChMode : GetChMode -> IO ()
setGetChMode WaitForever           = raw False *> cBreak True  *> noDelay False
setGetChMode WaitForeverRaw        = raw True                  *> noDelay False
setGetChMode (Wait Z)              = raw False *> cBreak True  *> noDelay True
setGetChMode (Wait (S k))          = halfDelay (toIntNat k)    *> noDelay False
setGetChMode WaitForeverLinebuf    = raw False *> cBreak False *> noDelay False
setGetChMode WaitForeverLinebufRaw = raw True  *> cBreak False *> noDelay False

||| Use this function to start curses. Note that `endWin` should *always* be
||| called before the program terminates.
||| @getChMode    the mode that `getCh` will use
export
startCurses : (getChMode : GetChMode) -> IO ()
startCurses getChMode = do
  initScr
  nl True
  echo False
  keypad True
  meta True
  leaveOk False
  setGetChMode getChMode

max_stars_repo_name: zenntenn/curses-idris

max_issues_repo_name: zenntenn/curses-idris

max_forks_repo_name: zenntenn/curses-idris


text:
module Main

import Dart.Core
import Dart.FFI

%inline
export
Point : Type
Point = Struct """
Point,
// All foreign names must be fully qualified and
// the following import can always be assumed to exist:
// import 'dart:core' as $;
class Point {
  $.int x;
  $.int y;
  Point({this.x, this.y});
  void moveTo($.int x, $.int y) { this.x = x; this.y = y; }
  static Point from({$.int x, $.int y}) => Point(x: x, y: y);
}
""" [
  ("x", Int),
  ("y", Int)
]

Show Point where
  show pt = show (the Int (getField pt "x"), the Int (getField pt "y"))

namespace Point

  namespace From

    data Tag : Type where

    %inline
    public export
    x : Parameter Tag
    x = MkParameter "x" Int Tag

    %inline
    public export
    y : Parameter Tag
    y = MkParameter "y" Int Tag

  %inline
  public export
  from : Parameters [From.x, From.y] -> IO Point
  from ps = primIO $ prim__dart_invoke "Point.from" [] [] ps

  %inline
  public export
  moveTo : Int -> Int -> Point -> IO ()
  moveTo x y this = primIO $ prim__dart_invoke ".moveTo" [] [this, x, y] none

main : IO ()
main = do
  pt <- Point.from [
    x @= 42,
    y @= 37
  ]
  printLn pt
  moveTo 11 21 pt
  printLn pt


text:
module System.Escape

import Data.List
import Data.String

import System.Info

||| Escape special characters in an Idris string, for use as a string literal
||| in the shell
public export
escapeArg : String -> String
escapeArg cmd = let escapedCmdChars = pack $ unpack cmd >>= escapeArgChar in
    if isWindows
       then escapedCmdChars
       else "\"" ++ escapedCmdChars ++ "\""
  where
    escapeArgChar : Char -> List Char
    escapeArgChar c =
        if isWindows
           then if c == '%'  || c == '^'  || c == '&'  || c == '<'  || c == '>' || c == '|' ||
                   c == '\'' || c == '"'  || c == '`'  ||
                   c == ' '  || c == '\t' || c == '\n' || c == ';' || c == ',' || c == '=' || c == '\x0B' || c == '\x0C' || c == '\xFF' ||
                   c == '('  || c == ')'  || c == '!'
                   then ['^', c]
                   else [c]
           else if c == '$' || c == '`' || c == '\\' || c == '"'
                   then ['\\', c]
                   else [c]

||| Escape special characters in a list of shell arguments, as a single command
||| for the shell.
||| eg. the list ["a", "b", "c d"] is interpreted as the command `a b "c d"`
public export
escapeCmd : List String -> String
escapeCmd cmd = concat $ intersperse " " $ map escapeArg cmd


text:
import System.Directory.Tree
import System.File
import System.Path

main : IO ()
main = do
    Right () <- copyDir (parse "templateDir") (parse "resultDir")
        | Left err => printLn err
    pure ()


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

import XML.DOM

import public XML.XPath.Types
import XML.XPath.Parser

%access export

-- ------------------------------------------------------------------- [ Query ]

public export
data XPathResultTy = NODELIST | VALUE

public export
data XPathResult : NodeTy -> Type where
  Nodes : (prf : ValidNode a)
       -> List (Document a)
       -> XPathResult a
  Empty  : XPathResult a

foldResults : List (XPathResult a) -> XPathResult a
foldResults = foldl merge Empty
  where
    merge : XPathResult a -> XPathResult a -> XPathResult a
    merge Empty y     = y
    merge x     Empty = x
    merge (Nodes prf xs) (Nodes x ys) = Nodes prf (xs ++ ys)

concatMapResults : (Document ELEMENT -> XPathResult ty) -> XPathResult ELEMENT -> XPathResult ty
concatMapResults f (Nodes prf xs) = foldResults $ Functor.map f xs
concatMapResults f Empty = Empty

private
evaluatePath : (q : XPath ty a)
            -> Document ELEMENT
            -> XPathResult ty -- (calcResultTy q)

evaluatePath (Query q) n = evaluatePath q n
evaluatePath (Elem e)  n = Nodes ValidElem $ getChildElementsByName e n
evaluatePath (Any)     n = Nodes ValidElem $ getChildElements n

evaluatePath (Attr a)  n with (getAttribute a n)
  evaluatePath (Attr a)  n | Nothing = Empty
  evaluatePath (Attr a)  n | (Just x) = Nodes ValidText [(mkText x)]

evaluatePath (CData)   n = Nodes ValidCData $ getCData n
evaluatePath (Text)    n = Nodes ValidText  $ getText n
evaluatePath (Comment) n = Nodes ValidDoc   $ getComments n

evaluatePath (Root r)  n with (r)
    | Any    = Nodes ValidElem [n]
    | Elem e = if getTagName n == e then Nodes ValidElem [n] else Empty

evaluatePath (DRoot r) n with (r)
    | Any    = Nodes ValidElem $ getAllChildren n
    | Elem e = Nodes ValidElem $ getElementsByName e n

evaluatePath (PathA p child prf {a}) n = concatMapResults (evaluatePath child) (evaluatePath p n)

evaluatePath (PathD p child prf) n with (child)
  evaluatePath (PathD p child prf) n | Any with (evaluatePath p n)
    evaluatePath (PathD p child prf) n | Any | (Nodes x xs) =
        Nodes ValidElem $ Foldable.concatMap (\x => getAllChildren x) xs
    evaluatePath (PathD p child prf) n | Any | Empty = Empty

  evaluatePath (PathD p child prf) n | (Elem x) with (evaluatePath p n)
    evaluatePath (PathD p child prf) n | (Elem x) | (Nodes ValidElem xs) =
        Nodes ValidElem $ Foldable.concatMap (\e => getElementsByName x e) xs
    evaluatePath (PathD p child prf) n | (Elem x) | Empty = Empty

  evaluatePath (PathD p child prf) n | path with (evaluatePath p n)
    evaluatePath (PathD p child prf) n | path | res =
        concatMapResults (evaluatePath path) res

-- ------------------------------------------------------------------- [ Query ]

export
queryDoc : XPath ty QUERY
        -> Document DOCUMENT
        -> XPathResult ty
queryDoc qstr doc = evaluatePath qstr (getRoot doc)

export
queryElem : XPath ty QUERY
         -> Document ELEMENT
         -> XPathResult ty
queryElem qstr e = evaluatePath qstr e

export
query : XPath qTy QUERY
     -> Document ty
     -> {auto prf : CanQuery ty}
     -> XPathResult qTy
query q x {prf} with (prf)
  query q x {prf = prf} | QueryDoc = queryDoc q x
  query q x {prf = prf} | QueryElem = queryElem q x

-- ------------------------------------------------------------------ [ Parser ]

namespace String
  export
  queryDoc : String
          -> Document DOCUMENT
          -> Either XPathError (ty ** XPathResult ty)
  queryDoc qstr doc =
    case (parseXPathStr qstr) of
      Left err        => Left $ MalformedQuery qstr err
      Right (_ ** q)  => Right $ (_ ** queryDoc q doc)

  export
  queryElem : String
           -> Document ELEMENT
           -> Either XPathError (ty ** XPathResult ty)
  queryElem qstr e = do
    case (parseXPathStr qstr) of
      Left err        => Left $ MalformedQuery qstr err
      Right (_ ** q)  => Right $ (_ ** queryElem q e)

  export
  query : String
       -> Document ty
       -> {auto prf : CanQuery ty}
       -> Either XPathError (ty' ** XPathResult ty')
  query qstr x {prf} with (prf)
    query qstr x {prf = prf} | QueryDoc = queryDoc qstr x
    query qstr x {prf = prf} | QueryElem = queryElem qstr x

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Core.Options

import Core.Core
import Core.Name
import public Core.Options.Log
import Core.TT

import Libraries.Utils.Binary
import Libraries.Utils.Path

import Data.List
import Data.Maybe
import Data.String

import System.Info

%default total

public export
record Dirs where
  constructor MkDirs
  working_dir : String
  source_dir : Maybe String -- source directory, relative to working directory
  build_dir : String -- build directory, relative to working directory
  depends_dir : String -- local dependencies directory, relative to working directory
  output_dir : Maybe String -- output directory, relative to working directory
  prefix_dir : String -- installation prefix, for finding data files (e.g. run time support)
  extra_dirs : List String -- places to look for import files
  package_dirs : List String -- places to look for packages
  lib_dirs : List String -- places to look for libraries (for code generation)
  data_dirs : List String -- places to look for data file

export
execBuildDir : Dirs -> String
execBuildDir d = build_dir d </> "exec"

export
outputDirWithDefault : Dirs -> String
outputDirWithDefault d = fromMaybe (build_dir d </> "exec") (output_dir d)

public export
toString : Dirs -> String
toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs pdirs ldirs ddirs) =
  unlines [ "+ Working Directory      :: " ++ show wdir
          , "+ Source Directory       :: " ++ show sdir
          , "+ Build Directory        :: " ++ show bdir
          , "+ Local Depend Directory :: " ++ show ldir
          , "+ Output Directory       :: " ++ show (outputDirWithDefault d)
          , "+ Installation Prefix    :: " ++ show dfix
          , "+ Extra Directories      :: " ++ show edirs
          , "+ Package Directories    :: " ++ show pdirs
          , "+ CG Library Directories :: " ++ show ldirs
          , "+ Data Directories       :: " ++ show ddirs]

public export
data CG = Chez
        | ChezSep
        | Racket
        | Gambit
        | Node
        | Javascript
        | RefC
        | VMCodeInterp
        | Jvm
        | Other String

export
Eq CG where
  Chez == Chez = True
  ChezSep == ChezSep = True
  Racket == Racket = True
  Gambit == Gambit = True
  Node == Node = True
  Javascript == Javascript = True
  RefC == RefC = True
  VMCodeInterp == VMCodeInterp = True
  Jvm == Jvm = True
  Other s == Other t = s == t
  _ == _ = False

export
Show CG where
  show Chez = "chez"
  show ChezSep = "chez-sep"
  show Racket = "racket"
  show Gambit = "gambit"
  show Node = "node"
  show Javascript = "javascript"
  show RefC = "refc"
  show VMCodeInterp = "vmcode-interp"
  show Jvm = "jvm"
  show (Other s) = s

public export
record PairNames where
  constructor MkPairNs
  pairType : Name
  fstName : Name
  sndName : Name

public export
record RewriteNames where
  constructor MkRewriteNs
  equalType : Name
  rewriteName : Name

public export
record PrimNames where
  constructor MkPrimNs
  fromIntegerName : Maybe Name
  fromStringName : Maybe Name
  fromCharName : Maybe Name
  fromDoubleName : Maybe Name

export
primNamesToList : PrimNames -> List Name
primNamesToList (MkPrimNs i s c d) = catMaybes [i,s,c,d]

public export
data LangExt
     = ElabReflection
     | Borrowing -- not yet implemented

export
Eq LangExt where
  ElabReflection == ElabReflection = True
  Borrowing == Borrowing = True
  _ == _ = False

-- Other options relevant to the current session (so not to be saved in a TTC)
public export
record ElabDirectives where
  constructor MkElabDirectives
  lazyActive : Bool
  unboundImplicits : Bool
  totality : TotalReq
  ambigLimit : Nat
  autoImplicitLimit : Nat
  nfThreshold : Nat
  --
  -- produce traditional (prefix) record projections,
  -- in addition to postfix (dot) projections
  -- default: yes
  prefixRecordProjections : Bool

public export
record Session where
  constructor MkSessionOpts
  noprelude : Bool
  totalReq : TotalReq
  nobanner : Bool
  findipkg : Bool
  codegen : CG
  directives : List String
  searchTimeout : Integer -- maximum number of milliseconds to run
                          -- expression/program search
  ignoreMissingPkg : Bool -- fail silently on missing packages. This is because
          -- while we're bootstrapping, we find modules by a different route
          -- but we still want to have the dependencies listed properly

  -- Troubleshooting
  logEnabled : Bool -- do we check logging flags at all? This is 'False' until
                    -- any logging is enabled.
  logLevel : LogLevels
  logTimings : Bool
  debugElabCheck : Bool -- do conversion check to verify results of elaborator
  dumpcases : Maybe String -- file to output compiled case trees
  dumplifted : Maybe String -- file to output lambda lifted definitions
  dumpanf : Maybe String -- file to output ANF definitions
  dumpvmcode : Maybe String -- file to output VM code definitions
  profile : Bool -- generate profiling information, if supported
  logErrorCount : Nat -- when parsing alternatives fails, how many errors
                      -- should be shown.

  -- Warnings
  warningsAsErrors : Bool
  showShadowingWarning : Bool

  -- Experimental
  checkHashesInsteadOfModTime : Bool
  incrementalCGs : List CG
  wholeProgram : Bool
     -- Use whole program compilation for executables, no matter what
     -- incremental CGs are set (intended for overriding any environment
     -- variables that set incremental compilation)
  caseTreeHeuristics : Bool -- apply heuristics to pick matches for case tree building

public export
record PPrinter where
  constructor MkPPOpts
  showImplicits : Bool
  showFullEnv : Bool
  fullNamespace : Bool

public export
record Options where
  constructor MkOptions
  dirs : Dirs
  printing : PPrinter
  session : Session
  elabDirectives : ElabDirectives
  pairnames : Maybe PairNames
  rewritenames : Maybe RewriteNames
  primnames : PrimNames
  extensions : List LangExt
  additionalCGs : List (String, CG)
  hashFn : Maybe String

export
availableCGs : Options -> List (String, CG)
availableCGs o
    = [("chez", Chez),
       ("chez-sep", ChezSep),
       ("racket", Racket),
       ("node", Node),
       ("javascript", Javascript),
       ("refc", RefC),
       ("gambit", Gambit),
       ("jvm", Jvm),
       ("vmcode-interp", VMCodeInterp)] ++ additionalCGs o

export
getCG : Options -> String -> Maybe CG
getCG o cg = lookup (toLower cg) (availableCGs o)

defaultDirs : Dirs
defaultDirs = MkDirs "." Nothing "build" "depends" Nothing
                     "/usr/local" ["."] [] [] []

defaultPPrint : PPrinter
defaultPPrint = MkPPOpts False True False

export
defaultSession : Session
defaultSession = MkSessionOpts False CoveringOnly False False Jvm [] 1000 False False
                               defaultLogLevel False False Nothing Nothing
                               Nothing Nothing False 1 False True
                               False [] False False

export
defaultElab : ElabDirectives
defaultElab = MkElabDirectives True True CoveringOnly 3 50 50 True

-- FIXME: This turns out not to be reliably portable, since different systems
-- may have tools with the same name but different required arugments. We
-- probably need another way (perhaps our own internal hash function, although
-- that's not going to be as good as sha256).
export
defaultHashFn : Core (Maybe String)
defaultHashFn
    = do Nothing <- coreLift $ pathLookup ["sha256sum", "gsha256sum"]
           | Just p => pure $ Just $ p ++ " --tag"
         Nothing <- coreLift $ pathLookup ["sha256"]
           | Just p => pure $ Just p
         Nothing <- coreLift $ pathLookup ["openssl"]
           | Just p => pure $ Just $ p ++ " sha256"
         pure Nothing

export
defaults : Core Options
defaults
    = do -- hashFn <- defaultHashFn
         -- Temporarily disabling the hash function until we have a more
         -- portable way of working out what to call, and allowing a way for
         -- it to fail gracefully.
         pure $ MkOptions
           defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing
           (MkPrimNs Nothing Nothing Nothing Nothing) [] [] Nothing

-- Reset the options which are set by source files
export
clearNames : Options -> Options
clearNames = record { pairnames = Nothing,
                      rewritenames = Nothing,
                      primnames = MkPrimNs Nothing Nothing Nothing Nothing,
                      extensions = []
                    }

export
setPair : (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
          Options -> Options
setPair ty f s = record { pairnames = Just (MkPairNs ty f s) }

export
setRewrite : (eq : Name) -> (rwlemma : Name) -> Options -> Options
setRewrite eq rw = record { rewritenames = Just (MkRewriteNs eq rw) }

export
setFromInteger : Name -> Options -> Options
setFromInteger n = record { primnames->fromIntegerName = Just n }

export
setFromString : Name -> Options -> Options
setFromString n = record { primnames->fromStringName = Just n }

export
setFromChar : Name -> Options -> Options
setFromChar n = record { primnames->fromCharName = Just n }

export
setFromDouble : Name -> Options -> Options
setFromDouble n = record { primnames->fromDoubleName = Just n }

export
setExtension : LangExt -> Options -> Options
setExtension e = record { extensions $= (e ::) }

export
isExtension : LangExt -> Options -> Bool
isExtension e opts = e `elem` extensions opts

export
addCG : (String, CG) -> Options -> Options
addCG cg = record { additionalCGs $= (cg::) }


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 14

-- check that all functions are total
%default total

--
-- section 14.2
-- see Security.idr
-- see VendingMachine.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
%default total

nice : (x : Bool) -> x === True
nice .(_) = Refl


text:
module Java.Util.Stream

import IdrisJvm.IO
import Java.Lang
import Java.Util.Function

%access public export

namespace Collector
  Collector : Type
  Collector = javaInterface "java/util/stream/Collector"

namespace Collectors
  collectorsClass : String
  collectorsClass = "java/util/stream/Collectors"

  CollectorsClass : JVM_NativeTy
  CollectorsClass = Class "java/util/stream/Collectors"

  Collectors : Type
  Collectors = JVM_Native CollectorsClass

  toList : JVM_IO Collector
  toList = invokeStatic CollectorsClass "toList" (JVM_IO Collector)

namespace JStream
  streamClass : String
  streamClass = "java/util/stream/Stream"

  JStreamInterface : JVM_NativeTy
  JStreamInterface = Interface streamClass

  JStream : Type
  JStream = JVM_Native JStreamInterface

  map : Inherits JStream stream => Function -> stream -> JVM_IO JStream
  map f stream = invokeInstance "map" (JStream -> Function -> JVM_IO JStream) (believe_me stream) f

  filter : Inherits JStream stream => Predicate -> stream -> JVM_IO JStream
  filter predicate stream = invokeInstance "filter" (JStream -> Predicate -> JVM_IO JStream) (believe_me stream) predicate

  collect : (Inherits JStream stream, Inherits Collector collector) => collector -> stream -> JVM_IO Object
  collect collector stream = invokeInstance "collect" (JStream -> Collector -> JVM_IO Object) (believe_me stream) (believe_me collector)

  generate : Inherits Supplier supplier => supplier -> JVM_IO JStream
  generate supplier = invokeStatic JStreamInterface "generate" (Supplier -> JVM_IO JStream) (believe_me supplier)

  limit : Inherits JStream stream => Bits64 -> stream -> JVM_IO JStream
  limit maxSize stream = invokeInstance "limit" (JStream -> Bits64 -> JVM_IO JStream) (believe_me stream) maxSize

namespace IntStream
  IntStreamInterface : JVM_NativeTy
  IntStreamInterface = Interface "java/util/stream/IntStream"

  IntStream : Type
  IntStream = JVM_Native IntStreamInterface

  map : (Inherits IntStream stream, Inherits IntUnaryOperator operator) => operator -> stream -> JVM_IO IntStream
  map operator stream = invokeInstance "map" (IntStream -> IntUnaryOperator -> JVM_IO IntStream) (believe_me stream) (believe_me operator)

  sum : Inherits IntStream stream => stream -> JVM_IO Int
  sum stream = invokeInstance "sum" (IntStream -> JVM_IO Int) (believe_me stream)

  from : JVM_Array Int -> JVM_IO IntStream
  from values = invokeStatic IntStreamInterface "of" (JVM_Array Int -> JVM_IO IntStream) values


text:
module Main

import System

import Sixel

partial
main : IO ()
main = do
  (_ :: filename :: _) <- getArgs
    | (script :: _) => putStrLn ("Usage: " ++ script ++ " <filename>")

  Right encoder <- MkEncoder
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt encoder OptFlagQuality "high"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt encoder OptFlagResampling "hamming"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt encoder OptFlagSelectColor "histogram"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt encoder OptFlagEncodePolicy "size"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- encode encoder filename
    | Left error => putStrLn getAdditionalMessage

  pure ()

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module Bautzen.Game.Map

import Bautzen.Terrain
import Bautzen.GameUnit
import Bautzen.Pos

import Data.Maybe.Extra

import Data.Nat
import Data.Vect

V : Terrain -> Terrain
V = Village

Wd  : Terrain
Wd = Wood

Cl  : Terrain
Cl = Clear

Rg  : Terrain
Rg = Rough

RW  : Terrain
RW = RoughWood

H : Terrain -> Terrain
H = Hill

SA : Terrain -> Terrain
SA = SupplySource Allies

SX : Terrain -> Terrain
SX = SupplySource Axis

T : Terrain
T = Town

N : Terrain
N = Clear

A : Side
A = Allies

terrains : Vect 13 (Vect 23 Terrain)
terrains = [-- 01      02     03          04    05     06     07     08     09      10     11     12     13     14         15     16     17     18      19     20          21    22      23
 {- 01 -}    [ Cl    , Wd   , Cl        , Wd  , Wd   , V Cl , Cl   , Wd    , Cl   , Wd   , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , Wd    , Cl   , SA (V Wd) , Cl   , Wd   , Cl    ]
 {- 02 -}  , [ Wd    , Wd   , Wd        , Wd  , Wd   , Wd   , Wd   , Wd    , Wd   , V Wd , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , V Wd  , Wd   , V Wd      , V Wd , Wd   , Wd    ]
 {- 03 -}  , [ Wd    , Wd   , Wd        , Wd  , Wd   , Cl   , V Wd , Wd    , Wd   , Cl   , Wd   , Wd   , Wd   , Wd       , Wd   , Wd   , Wd   , Wd    , Wd   , Wd        , Wd   , Wd   , Cl    ]
 {- 04 -}  , [ SX Wd , Cl   , Wd        , Wd  , Wd   , Cl   , V Cl , Cl    , Cl   , V Cl , Cl   , Cl   , V Wd , Wd       , V Wd , Wd   , V Wd , Cl    , Cl   , Cl        , V Cl , Cl   , Cl    ]
 {- 05 -}  , [ Cl    , Wd   , Wd        , Cl  , Cl   , Cl   , Cl   , Cl    , Cl   , Cl   , Cl   , Cl   , Cl   , Cl       , Wd   , Wd   , Wd   , Wd    , V Cl , Cl        , Cl   , Cl   , SA Cl ]
 {- 06 -}  , [ Cl    , Wd   , Wd        , Cl  , Cl   , Cl   , V Cl , Cl    , Cl   , H RW , RW   , Wd   , RW   , H (V RW) , Cl   , V Wd , Wd   , Wd    , V Wd , Wd        , Cl   , T    , SA Cl ]
 {- 07 -}  , [ SX Wd , Wd   , V Wd      , H Rg, Cl   , Cl   , H Rg , T     , Cl   , Cl   , RW   , V Cl , Cl   , V Cl     , Wd   , Cl   , Cl   , Wd    , Cl   , Wd        , V Cl , V Cl , Cl    ]
 {- 08 -}  , [ Wd    , RW   , Wd        , RW  , Cl   , Cl   , V Cl , Rg    , V Cl , Cl   , V Cl , Cl   , Cl   , Cl       , Cl   , Cl   , V Cl , Cl    , Cl   , Cl        , V Cl , Cl   , Cl    ]
 {- 09 -}  , [ Cl    , Rg   , Wd        , Rg  , Cl   , Wd   , Cl   , H RW  , Wd   , V Cl , Cl   , V Cl , Cl   , T        , Cl   , Cl   , Cl   , Cl    , V Cl , Cl        , Cl   , Cl   , Cl    ]
 {- 10 -}  , [ SX Wd , V Cl , V Cl      , Wd  , V Cl , Cl   , Wd   , Cl    , V Rg , Rg   , Wd   , Cl   , Cl   , Cl       , T    , Cl   , Cl   , Cl    , V Cl , Cl        , Cl   , Cl   , Cl    ]
 {- 11 -}  , [ Wd    , V Wd , Cl        , Cl  , Wd   , Cl   , Cl   , Cl    , T    , H Rg , Cl   , RW   , RW   , Rg       , Cl   , H RW , RW   , H Rg  , Cl   , Cl        , Cl   , V Cl , Cl    ]
 {- 12 -}  , [ Wd    , Wd   , V Wd      , Wd  , Cl   , Cl   , Rg   , SX Rg , Rg   , Cl   , RW   , Cl   , Rg   , Cl       , RW   , Cl   , Cl   , SX Cl , T    , Cl        , Cl   , Cl   , Cl    ]
 {- 13 -}  , [ T     , N    , SX (V Cl) , N   , Cl   , N    , Cl   , N     , Cl   , N    , Cl   , N    , Cl   , N        , Cl   , N    , Cl   , N     , Cl   , N         , Cl   , N    , Cl    ]
           ]

public export
PartialGameMap : Map
PartialGameMap = MkMap positions []
  where
    positions : List (Pos, Terrain)
    positions = [(Hex 0 0, Clear),
                 (Hex 0 1, Clear),
                 (Hex 0 2, Clear),
                 (Hex 0 3, SupplySource Axis $ Clear),
                 (Hex 0 4, Clear),
                 (Hex 1 0, Clear),
                 (Hex 1 1, Clear),
                 (Hex 1 2, Clear),
                 (Hex 1 3, Clear),
                 (Hex 1 4, Clear),
                 (Hex 2 0, Clear),
                 (Hex 2 1, Clear),
                 (Hex 2 2, Clear),
                 (Hex 2 3, Clear),
                 (Hex 2 4, Clear),
                 (Hex 3 0, Clear),
                 (Hex 3 1, Clear),
                 (Hex 3 2, Clear),
                 (Hex 3 3, Clear),
                 (Hex 3 4, Clear),
                 (Hex 4 0, Clear),
                 (Hex 4 1, Clear),
                 (Hex 4 2, Clear),
                 (Hex 4 3, Clear),
                 (Hex 4 4, Clear)]

public export
FullGameMap : Map
FullGameMap = MkMap positions []
  where
    mkPosition : (c : Nat) -> (r : Nat) -> Maybe ( Pos, Terrain)
    mkPosition c r with (natToFin c 23, natToFin r 13, isLTE c 22, isLTE r 12)
      mkPosition c r | (Just col, Just row, Yes cprf, Yes rprf) =
           let terrain = index col $ index row terrains
           in Just (Hex c r, terrain)
      mkPosition c r | (_, _, _, _) = Nothing

    positions : List (Pos, Terrain)
    positions = catMaybes $ [ mkPosition c r | c <- [ 0 .. 22 ], r <- [ 0 .. 12 ]]

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Postgres

import public Postgres.Data
import public Postgres.DB
import public Postgres.DB.Wait
import public Postgres.Notification
import public Postgres.Exec
import public Postgres.Query
import public Postgres.Result

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
import ArithState
import DataStore
import Record
import State
import StateMonad
import Traverse
import TreeLabel
import TreeLabelState
import TreeLabelType


text:
module Control.MonadRec

import public Control.WellFounded
import Control.Monad.Either
import Control.Monad.Identity
import Control.Monad.Maybe
import Control.Monad.Reader
import Control.Monad.RWS
import Control.Monad.State
import Control.Monad.Writer

import Data.List
import Data.SnocList
import public Data.Fuel
import public Data.Nat

%default total

--------------------------------------------------------------------------------
--          Sized Implementations
--------------------------------------------------------------------------------

public export
Sized Fuel where
  size Dry      = 0
  size (More f) = S $ size f

public export
Sized (SnocList a) where
  size = length

--------------------------------------------------------------------------------
--          Step
--------------------------------------------------------------------------------

||| Single step in a recursive computation.
|||
||| A `Step` is either `Done`, in which case we return the
||| final result, or `Cont`, in which case we continue
||| iterating. In case of a `Cont`, we get a new seed for
||| the next iteration plus an updated state. In addition
||| we proof that the sequence of seeds is related via `rel`.
||| If `rel` is well-founded, the recursion will provably
||| come to an end in a finite number of steps.
public export
data Step :  (rel   : a -> a -> Type)
          -> (seed  : a)
          -> (accum : Type)
          -> (res   : Type)
          -> Type where

  ||| Keep iterating with a new `seed2`, which is
  ||| related to the current `seed` via `rel`.
  ||| `vst` is the accumulated state of the iteration.
  Cont :  (seed2 : a)
       -> (0 prf : rel seed2 seed)
       -> (vst   : st)
       -> Step rel seed st res

  ||| Stop iterating and return the given result.
  Done : (vres : res) -> Step rel v st res

public export
Bifunctor (Step rel seed) where
  bimap f _ (Cont s2 prf st) = Cont s2 prf (f st)
  bimap _ g (Done res)       = Done (g res)

  mapFst f (Cont s2 prf st) = Cont s2 prf (f st)
  mapFst _ (Done res)       = Done res

  mapSnd _ (Cont s2 prf st) = Cont s2 prf st
  mapSnd g (Done res)       = Done (g res)

--------------------------------------------------------------------------------
--          MonadRec
--------------------------------------------------------------------------------

||| Interface for tail-call optimized monadic recursion.
public export
interface Monad m => MonadRec m where
  ||| Implementers mus make sure they implement this function
  ||| in a tail recursive manner.
  ||| The general idea is to loop using the given `step` function
  ||| until it returns a `Done`.
  |||
  ||| To convey to the totality checker that the sequence
  ||| of seeds generated during recursion must come to an
  ||| end after a finite number of steps, this function
  ||| requires an erased proof of accessibility.
  total
  tailRecM :  {0 rel : a -> a -> Type}
           -> (seed  : a)
           -> (ini   : st)
           -> (0 prf : Accessible rel seed)
           -> (step  : (seed2 : a) -> st -> m (Step rel seed2 st b))
           -> m b

public export %inline
||| Monadic tail recursion over a sized structure.
trSized :  MonadRec m
        => (0 _ : Sized a)
        => (seed : a)
        -> (ini  : st)
        -> (step : (v : a) -> st -> m (Step Smaller v st b))
        -> m b
trSized x ini = tailRecM x ini (sizeAccessible x)

--------------------------------------------------------------------------------
--          Base Implementations
--------------------------------------------------------------------------------

public export
MonadRec Identity where
  tailRecM seed st1 (Access rec) f = case f seed st1 of
    Id (Done b)         => Id b
    Id (Cont y prf st2) => tailRecM y st2 (rec y prf) f

public export
MonadRec Maybe where
  tailRecM seed st1 (Access rec) f = case f seed st1 of
    Nothing               => Nothing
    Just (Done b)         => Just b
    Just (Cont y prf st2) => tailRecM y st2 (rec y prf) f

public export
MonadRec (Either e) where
  tailRecM seed st1 (Access rec) f = case f seed st1 of
    Left e                 => Left e
    Right (Done b)         => Right b
    Right (Cont y prf st2) => tailRecM y st2 (rec y prf) f

trIO :  (x : a)
     -> (ini : st)
     -> (0 _ : Accessible rel x)
     -> (f : (v : a) -> st -> IO (Step rel v st b))
     -> IO b
trIO x ini acc f = fromPrim $ run x ini acc
  where run :  (y : a) -> (st1 : st)
            -> (0 _ : Accessible rel y)
            -> (1 w : %World)
            -> IORes b
        run y st1 (Access rec) w = case toPrim (f y st1) w of
          MkIORes (Done b) w2          => MkIORes b w2
          MkIORes (Cont y2 prf st2) w2 => run y2 st2 (rec y2 prf) w2

public export %inline
MonadRec IO where
  tailRecM = trIO

--------------------------------------------------------------------------------
--          Transformer Implementations
--------------------------------------------------------------------------------

---------------------------
-- StateT

%inline
convST :  Functor m
       => (f : (v : a) -> st -> StateT s m (Step rel v st b))
       -> (v : a)
       -> (st,s)
       -> m (Step rel v (st,s) (s,b))
convST f v (st1,s1) =   (\(s2,stp) => bimap (,s2) (s2,) stp)
                    <$> runStateT s1 (f v st1)

public export
MonadRec m => MonadRec (StateT s m) where
  tailRecM x ini acc f =
    ST $ \s1 => tailRecM x (ini,s1) acc (convST f)

---------------------------
-- EitherT

convE :  Functor m
      => (f : (v : a) -> st -> EitherT e m (Step rel v st b))
      -> (v : a)
      -> (ini : st)
      -> m (Step rel v st (Either e b))
convE f v s1 = map conv $ runEitherT (f v s1)
  where conv : Either e (Step rel v st b) -> Step rel v st (Either e b)
        conv (Left err)                = Done (Left err)
        conv (Right $ Done b)          = Done (Right b)
        conv (Right $ Cont v2 prf st2) = Cont v2 prf st2

public export
MonadRec m => MonadRec (EitherT e m) where
  tailRecM x ini acc f =
    MkEitherT $ tailRecM x ini acc (convE f)

---------------------------
-- MaybeT

convM :  Functor m
      => (f : (v : a) -> st -> MaybeT m (Step rel v st b))
      -> (v : a)
      -> (ini : st)
      -> m (Step rel v st (Maybe b))
convM f v s1 = map conv $ runMaybeT (f v s1)
  where conv : Maybe (Step rel v st b) -> Step rel v st (Maybe b)
        conv Nothing                  = Done Nothing
        conv (Just $ Done b)          = Done (Just b)
        conv (Just $ Cont v2 prf st2) = Cont v2 prf st2

public export
MonadRec m => MonadRec (MaybeT m) where
  tailRecM x ini acc f =
    MkMaybeT $ tailRecM x ini acc (convM f)

---------------------------
-- ReaderT

convR :  (f : (v : a) -> st -> ReaderT e m (Step rel v st b))
      -> (env : e)
      -> (v : a)
      -> (ini : st)
      -> m (Step rel v st b)
convR f env v s1 = runReaderT env (f v s1)

public export
MonadRec m => MonadRec (ReaderT e m) where
  tailRecM x ini acc f =
    MkReaderT $ \env => tailRecM x ini acc (convR f env)

---------------------------
-- WriterT

convW :  Functor m
      => (f : (v : a) -> st -> WriterT w m (Step rel v st b))
      -> (v : a)
      -> (st,w)
      -> m (Step rel v (st,w) (b,w))
convW f v (s1,w1) =   (\(stp,w2) => bimap (,w2) (,w2) stp)
                  <$> unWriterT (f v s1) w1

public export
MonadRec m => MonadRec (WriterT w m) where
  tailRecM x ini acc f =
    MkWriterT $ \w1 => tailRecM x (ini,w1) acc (convW f)

---------------------------
-- RWST

convRWS :  Functor m
        => (f : (v : a) -> st -> RWST r w s m (Step rel v st b))
        -> (env : r)
        -> (v : a)
        -> (st,s,w)
        -> m (Step rel v (st,s,w) (b,s,w))
convRWS f env v (st1,s1,w1) =   (\(stp,s2,w2) => bimap (,s2,w2) (,s2,w2) stp)
                            <$> unRWST (f v st1) env s1 w1

public export
MonadRec m => MonadRec (RWST r w s m) where
  tailRecM x ini acc f =
    MkRWST $ \r1,s1,w1 => tailRecM x (ini,s1,w1) acc (convRWS f r1)


text:
module Debug.Trace

import Prelude
import PrimIO

%default total

export
trace : (msg : String) -> (result : a) -> a
trace x val = unsafePerformIO (do putStrLn x; pure val)

%foreign "jvm:toString(java/lang/Object java/lang/String),java/util/Objects"
prim_objectToString : AnyPtr -> PrimIO String

export
toString : a -> String
toString value = unsafePerformIO $ primIO (prim_objectToString (believe_me value))


text:
module Language.LSP.Message.Completion

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

%language ElabReflection
%default total

namespace CompletionItemKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  data CompletionItemKind
    = Text
    | Method
    | Function
    | Constructor
    | Field
    | Variable
    | Class
    | Interface
    | Module
    | Property
    | Unit_
    | Value
    | Enum
    | Keyword
    | Snippet
    | Color
    | File
    | Reference
    | Folder
    | EnumMember
    | Constant
    | Struct
    | Event
    | Operator
    | TypeParameter

export
ToJSON CompletionItemKind where
  toJSON Text          = JNumber 1
  toJSON Method        = JNumber 2
  toJSON Function      = JNumber 3
  toJSON Constructor   = JNumber 4
  toJSON Field         = JNumber 5
  toJSON Variable      = JNumber 6
  toJSON Class         = JNumber 7
  toJSON Interface     = JNumber 8
  toJSON Module        = JNumber 9
  toJSON Property      = JNumber 10
  toJSON Unit_         = JNumber 11
  toJSON Value         = JNumber 12
  toJSON Enum          = JNumber 13
  toJSON Keyword       = JNumber 14
  toJSON Snippet       = JNumber 15
  toJSON Color         = JNumber 16
  toJSON File          = JNumber 17
  toJSON Reference     = JNumber 18
  toJSON Folder        = JNumber 19
  toJSON EnumMember    = JNumber 20
  toJSON Constant      = JNumber 21
  toJSON Struct        = JNumber 22
  toJSON Event         = JNumber 23
  toJSON Operator      = JNumber 24
  toJSON TypeParameter = JNumber 25

export
FromJSON CompletionItemKind where
  fromJSON (JNumber 1)  = pure Text
  fromJSON (JNumber 2)  = pure Method
  fromJSON (JNumber 3)  = pure Function
  fromJSON (JNumber 4)  = pure Constructor
  fromJSON (JNumber 5)  = pure Field
  fromJSON (JNumber 6)  = pure Variable
  fromJSON (JNumber 7)  = pure Class
  fromJSON (JNumber 8)  = pure Interface
  fromJSON (JNumber 9)  = pure Module
  fromJSON (JNumber 10) = pure Property
  fromJSON (JNumber 11) = pure Unit_
  fromJSON (JNumber 12) = pure Value
  fromJSON (JNumber 13) = pure Enum
  fromJSON (JNumber 14) = pure Keyword
  fromJSON (JNumber 15) = pure Snippet
  fromJSON (JNumber 16) = pure Color
  fromJSON (JNumber 17) = pure File
  fromJSON (JNumber 18) = pure Reference
  fromJSON (JNumber 19) = pure Folder
  fromJSON (JNumber 20) = pure EnumMember
  fromJSON (JNumber 21) = pure Constant
  fromJSON (JNumber 22) = pure Struct
  fromJSON (JNumber 23) = pure Event
  fromJSON (JNumber 24) = pure Operator
  fromJSON (JNumber 25) = pure TypeParameter
  fromJSON _ = neutral

namespace CompletionItemTag
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  data CompletionItemTag = Deprecated

export
ToJSON CompletionItemTag where
  toJSON Deprecated = JNumber 1

export
FromJSON CompletionItemTag where
  fromJSON (JNumber 1) = pure Deprecated
  fromJSON _ = neutral

namespace InsertTextMode
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  data InsertTextMode = AsIs | AdjustIndentation

export
ToJSON InsertTextMode where
  toJSON AsIs              = JNumber 1
  toJSON AdjustIndentation = JNumber 2

export
FromJSON InsertTextMode where
  fromJSON (JNumber 1) = pure AsIs
  fromJSON (JNumber 2) = pure AdjustIndentation
  fromJSON _ = neutral

namespace InsertTextFormat
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  data InsertTextFormat = PlainText | Snippet

export
ToJSON InsertTextFormat where
  toJSON PlainText = JNumber 1
  toJSON Snippet   = JNumber 2

export
FromJSON InsertTextFormat where
  fromJSON (JNumber 1) = pure PlainText
  fromJSON (JNumber 2) = pure Snippet
  fromJSON _ = neutral

namespace CompletionItemClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  record CompletionItemTagSupportClientCapabilities where
    constructor MkCompletionItemTagSupportClientCapabilities
    valueSet : List CompletionItemTag
  %runElab deriveJSON defaultOpts `{CompletionItemTagSupportClientCapabilities}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  record CompletionItemResolveSupportClientCapabilities where
    constructor MkCompletionItemResolveSupportClientCapabilities
    properties : List String
  %runElab deriveJSON defaultOpts `{CompletionItemResolveSupportClientCapabilities}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  record InsertTextModeSupport where
    constructor MkInsertTextModeSupport
    valueSet : List InsertTextMode
  %runElab deriveJSON defaultOpts `{InsertTextModeSupport}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  record CompletionItemClientCapabilities where
    constructor MkCompletionItemClientCapabilities
    snippetSupport          : Maybe Bool
    commitCharactersSupport : Maybe Bool
    documentationFormat     : Maybe (List MarkupKind)
    deprecatedSupport       : Maybe Bool
    preselectSupport        : Maybe Bool
    tagSupport              : Maybe CompletionItemTagSupportClientCapabilities
    insertReplaceSupport    : Maybe Bool
    resolveSupport          : Maybe CompletionItemResolveSupportClientCapabilities
    insertTextModeSupport   : Maybe InsertTextModeSupport
  %runElab deriveJSON defaultOpts `{CompletionItemClientCapabilities}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  record CompletionItemKindClientCapabilities where
    constructor MkCompletionItemKindClientCapabilities
    valueSet : Maybe (List CompletionItemKind)
  %runElab deriveJSON defaultOpts `{CompletionItemKindClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionClientCapabilities where
  constructor MkCompletionClientCapabilities
  dynamicRegistration : Maybe Bool
  completionItem      : Maybe CompletionItemClientCapabilities
  completionItemKind  : Maybe CompletionItemKindClientCapabilities
  contextSupport      : Maybe Bool
%runElab deriveJSON defaultOpts `{CompletionClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionOptions where
  constructor MkCompletionOptions
  workDoneProgress    : Maybe Bool
  triggerCharacters   : Maybe (List Char)
  allCommitCharacters : Maybe (List Char)
  resolveProvider     : Maybe Bool
%runElab deriveJSON defaultOpts `{CompletionOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionRegistrationOptions where
  constructor MkCompletionRegistrationOptions
  documentSelector    : (OneOf [DocumentSelector, Null])
  workDoneProgress    : Maybe Bool
  triggerCharacters   : Maybe (List Char)
  allCommitCharacters : Maybe (List Char)
  resolveProvider     : Maybe Bool
%runElab deriveJSON defaultOpts `{CompletionRegistrationOptions}

namespace CompletionTriggerKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
  public export
  data CompletionTriggerKind = Invoked | TriggerCharacter | TriggerForIncompleteCompletions

export
ToJSON CompletionTriggerKind where
  toJSON Invoked                         = JNumber 1
  toJSON TriggerCharacter                = JNumber 2
  toJSON TriggerForIncompleteCompletions = JNumber 3

export
FromJSON CompletionTriggerKind where
  fromJSON (JNumber 1) = pure Invoked
  fromJSON (JNumber 2) = pure TriggerCharacter
  fromJSON (JNumber 3) = pure TriggerForIncompleteCompletions
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionContext where
  constructor MkCompletionContext
  triggerKind      : CompletionTriggerKind
  triggerCharacter : Maybe String
%runElab deriveJSON defaultOpts `{CompletionContext}

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionItem where
  constructor MkCompletionItem
  label               : String
  kind                : Maybe CompletionItemKind
  tags                : Maybe (List CompletionItemTag)
  detail              : Maybe String
  documentation       : Maybe (OneOf [String, MarkupContent])
  deprecated          : Maybe Bool
  preselect           : Maybe Bool
  sortText            : Maybe String
  filterText          : Maybe String
  insertText          : Maybe String
  insertTextFormat    : Maybe InsertTextFormat
  insertTextMode      : Maybe InsertTextMode
  textEdit            : Maybe (OneOf [TextEdit, InsertReplaceEdit])
  additionalTextEdits : Maybe (List TextEdit)
  commitCharacters    : Maybe (List Char)
  command             : Maybe Command
  data_               : Maybe JSON
%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CompletionItem}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_completion
public export
record CompletionList where
  constructor MkCompletionList
  isIncomplete : Bool
  items        : List CompletionItem
%runElab deriveJSON defaultOpts `{CompletionList}


text:
module Idris.DocString

import Core.Context
import Core.Core
import Core.Env
import Core.TT

import Idris.Resugar
import Idris.Syntax

import TTImp.TTImp

import Data.ANameMap
import Data.List
import Data.Maybe
import Data.NameMap
import Data.Strings

-- Add a doc string for a name in the current namespace
export
addDocString : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Name -> String ->
               Core ()
addDocString n_in doc
    = do n <- inCurrentNS n_in
         syn <- get Syn
         put Syn (record { docstrings $= addName n doc,
                           saveDocstrings $= insert n () } syn)

-- Add a doc string for a name, in an extended namespace (e.g. for
-- record getters)
export
addDocStringNS : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Namespace -> Name -> String ->
                 Core ()
addDocStringNS ns n_in doc
    = do n <- inCurrentNS n_in
         let n' = case n of
                       NS old root => NS (old <.> ns) root
                       root => NS ns root
         syn <- get Syn
         put Syn (record { docstrings $= addName n' doc,
                           saveDocstrings $= insert n' () } syn)

export
getDocsFor : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             FC -> Name -> Core (List String)
getDocsFor fc n
    = do syn <- get Syn
         defs <- get Ctxt
         all@(_ :: _) <- lookupCtxtName n (gamma defs)
             | _ => throw (UndefinedName fc n)
         let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn))
                                     (map fst all)
             | [] => pure ["No documentation for " ++ show n]
         traverse showDoc ns
  where
    indent : String -> String
    indent str = unlines $ map ("\t" ++) (lines str)

    showTotal : Name -> Totality -> String
    showTotal n tot
        = case isTerminating tot of
               Unchecked => ""
               _ => "\nTotality: " ++ show tot

    getConstructorDoc : Name -> Core (Maybe String)
    getConstructorDoc con
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact con (gamma defs)
                  | Nothing => pure Nothing
             syn <- get Syn
             let [(n, str)] = lookupName con (docstrings syn)
                  | _ => pure Nothing
             ty <- normaliseHoles defs [] (type def)
             pure (Just (nameRoot n ++ " : " ++ show !(resugar [] ty)
                          ++ "\n" ++ indent str))

    getImplDoc : Name -> Core (Maybe String)
    getImplDoc n
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure Nothing
             ty <- normaliseHoles defs [] (type def)
             pure (Just (indent (show !(resugar [] ty) ++ "\n")))

    getMethDoc : (Name, RigCount, Maybe TotalReq, Bool, RawImp) ->
                 Core (Maybe String)
    getMethDoc (n, c, tot, _, ty)
        = do syn <- get Syn
             let [(n, str)] = lookupName n (docstrings syn)
                  | _ => pure Nothing
             pure (Just (nameRoot n ++ " : " ++ show !(pterm ty)
                          ++ maybe "" (\t => "\n" ++ show t) tot
                          ++ "\n" ++ indent str))

    getIFaceDoc : (Name, IFaceInfo) -> Core String
    getIFaceDoc (n, iface)
        = do let params =
                case params iface of
                     [] => ""
                     ps => "Parameters: " ++ showSep ", " (map show ps) ++ "\n"
             constraints <-
                case parents iface of
                     [] => pure ""
                     ps => do pts <- traverse pterm ps
                              pure ("Constraints: " ++
                                    showSep ", " (map show pts) ++ "\n")
             mdocs <- traverse getMethDoc (methods iface)
             let meths = case mapMaybe id mdocs of
                              [] => ""
                              docs => "\nMethods:\n" ++ concat docs
             sd <- getSearchData fc False n
             idocs <- case hintGroups sd of
                           [] => pure []
                           ((_, tophs) :: _) => traverse getImplDoc tophs
             let insts = case mapMaybe id idocs of
                              [] => ""
                              docs => "\nImplementations:\n" ++ concat docs
             pure (params ++ constraints ++ meths ++ insts)

    getExtra : Name -> GlobalDef -> Core String
    getExtra n d
        = do syn <- get Syn
             let [] = lookupName n (ifaces syn)
                 | [ifacedata] => getIFaceDoc ifacedata
                 | _ => pure "" -- shouldn't happen, we've resolved ambiguity by now
             case definition d of
               PMDef _ _ _ _ _
                   => pure (showTotal n (totality d))
               TCon _ _ _ _ _ _ cons _
                   => do cdocs <- traverse getConstructorDoc
                                           !(traverse toFullNames cons)
                         case mapMaybe id cdocs of
                              [] => pure ""
                              docs => pure $ "\nConstructors:\n" ++ concat docs
               _ => pure ""

    showDoc : (Name, String) -> Core String
    showDoc (n, str)
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => throw (UndefinedName fc n)
             ty <- normaliseHoles defs [] (type def)
             let doc = show !(aliasName n) ++ " : " ++ show !(resugar [] ty)
                              ++ "\n" ++ indent str
             extra <- getExtra n def
             pure (doc ++ extra)

summarise : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Name -> Core String
summarise n -- n is fully qualified
    = do syn <- get Syn
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
             | _ => pure ""
         let doc = case lookupName n (docstrings syn) of
                        [(_, doc)] => case lines doc of
                                           (d :: _) => Just d
                                           _ => Nothing
                        _ => Nothing
         ty <- normaliseHoles defs [] (type def)
         pure (nameRoot n ++ " : " ++ show !(resugar [] ty) ++
                  maybe "" (\d => "\n\t" ++ d) doc)

-- Display all the exported names in the given namespace
export
getContents : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Namespace -> Core (List String)
getContents ns
   = -- Get all the names, filter by any that match the given namespace
     -- and are visible, then display with their type
     do defs <- get Ctxt
        ns <- allNames (gamma defs)
        let allNs = filter inNS ns
        allNs <- filterM (visible defs) allNs
        traverse summarise (sort allNs)
  where
    visible : Defs -> Name -> Core Bool
    visible defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (visibility def /= Private)

    inNS : Name -> Bool
    inNS (NS xns (UN _)) = xns == ns
    inNS _ = False


text:
||| Binary representation of natural numbers
||| See:
||| * [Idris tutorial](https://github.com/idris-lang/idris-tutorial/blob/master/examples/binary.idr)
||| * [Haskell](https://jaspervdj.be/posts/2018-09-04-binomial-heaps-101.html#binomial-forests) Binomial heap
|||   making use of binary numbers
module Data.Binary

import public Data.Nat.Parity

%access public export
%default total

||| Right to left binary representation of numbers.
||| Working with a right-to-left representation makes addition much easier. We
||| can always reconstruct the usual representation through a `Show` instance
||| for example.
|||
||| ```
||| > :x toBinary 12
||| B0 (B0 (B1 (B1 BZero))) : Binary 12
||| ```
data Binary : (value : Nat) -> Type where
  ||| Denote the single 0 number in binary representation
  ||| This is also used to _close_ a sequence of binary digits
  BZero  : Binary Z

  ||| A `0` bit
  ||| Build a binary number equal to 2v. Note that because we don't want to have
  ||| multiple representations for the number 0, eg. `BZero` or an arbitrary
  ||| string of `B0` terminated by `BZero`, we require the next `bin`ary to be
  ||| strictly positive.
  ||| @bin the rest of this binary number
  ||| @n the value of the rest of this binary number.
  B0    : (bin : Binary (S n)) -> Binary ((S n) * 2)

  ||| A `1` bit
  ||| Build a binary number equal to 2v + 1
  ||| @bin the rest of this binary number
  ||| @n the value of the rest of this binary number
  B1    : (bin : Binary n) -> Binary (S (n * 2))

implementation Show (Binary k) where
  show BZero      = "0"
  show (B0 bin)   = show bin ++ "0"
  show (B1 BZero) = "1"
  show (B1 bin)   = show bin ++ "1"

show_test_0 : show BZero = "0"
show_test_0 = Refl

show_test_10 : show (B0 (B1 BZero)) = "10"
show_test_10 = Refl

show_test_1 : show (B1 BZero) = "1"
show_test_1 = Refl

-- there's probably a way to use lemmas from Prelude.Nat about distributivity
-- of multiplication....
distributePlus2 : (k : Nat) -> (S (S (k * 2)) = (k + 1) * 2)
distributePlus2 Z     = Refl
distributePlus2 (S k) =
  let hyp = distributePlus2 k
  in rewrite hyp in Refl

||| Increment given `Binary`
inc : Binary k -> Binary (S k)
inc BZero = B1 BZero
inc (B0 bin) = B1 bin
inc (B1 bin) = B0 (inc bin)

-- we would like to derive a `Num` instance for `Binary` but unfortunately
-- we can't because `Binary` has a type-level argument hence it's not possible
-- to provide meaning to `Num` operations
--
-- We therefore resort to work with specialized functions for casting and
-- operating on binary numbers.
toBinary : (n : Nat) -> Binary n
toBinary Z     = BZero
toBinary (S k) = inc (toBinary k)

lemma1 : (n : Nat) -> toBinary (S n * 2) = B0 (toBinary (S n))
lemma1 Z     = Refl
lemma1 (S k) = rewrite lemma1 k in Refl

lemma2 : (n : Nat) -> (B1 (toBinary n) = inc (toBinary (mult n 2)))
lemma2 Z     = Refl
lemma2 (S k) = rewrite sym (lemma2 k) in Refl

||| A proof that we can convert a `Binary` from a `Nat` and get the
||| same "number".
||| @b a `Binary` number
||| @n a `Nat` representing the same number than b
natIsBinary : (b : Binary n) -> (b = toBinary n)
natIsBinary BZero = Refl
natIsBinary (B0 bin {n}) = rewrite natIsBinary bin in
                           rewrite lemma1 n in Refl
natIsBinary (B1 bin {n}) = rewrite natIsBinary bin in lemma2 n

Zero : Binary 0
Zero = BZero

One : Binary 1
One = toBinary 1

Two : Binary 2
Two = toBinary 2

infixl 6 +.

lemmaB0plusB0 : (m, n : Nat) -> (S (plus n (S m)) * 2) =
       (S (S (plus (mult n 2) (S (S (mult m 2))))))
lemmaB0plusB0 m n =
  rewrite plusCommutative n (S m) in
  rewrite plusCommutative (mult n 2) (S (S (mult m 2))) in
  rewrite multDistributesOverPlusLeft m n 2 in
  Refl

lemmaB1plusB0 : (v, w : Nat) -> (mult (v + S w) 2 = (mult v 2) + (S (S (mult w 2))))
lemmaB1plusB0 v w =
  rewrite multDistributesOverPlusLeft v (S w) 2 in
  Refl

lemmaB0plusB1 : (v, w : Nat) -> (mult (S v + w) 2 = S (plus (mult v 2) (S (mult w 2))))
lemmaB0plusB1 v w =
  rewrite multDistributesOverPlusLeft v w 2 in
  rewrite plusSuccRightSucc (mult v 2) (mult w 2) in
  Refl

lemmaB1plusB1 : (v, w : Nat) -> (S (mult (v + w) 2) = plus (mult v 2) (S (mult w 2)))
lemmaB1plusB1 v w =
  rewrite multDistributesOverPlusLeft v w 2 in
  rewrite plusSuccRightSucc (mult v 2) (mult w 2) in
  Refl

||| Add two binary numbers
|||
||| Unsurprisingly, it returns the sum of the 2 numbers, in binary representation.
||| **Implementation note**: We use `toBinary` to convert the sum of the 2 numbers
||| which is probably very inefficient at runtime, probably in `O(n + m)` whereas
||| standard addition has complexity `O(log(n + m))`. This is left to implement
||| properly later on, using the first implementation provided in the comments
||| below.
|||
||| @x left binary number to add
||| @y right binary number to add
||| @n `Nat` represented by `x`
||| @m `Nat` represented by `y`
add : (x : Binary n) -> (y : Binary m) -> Binary (n + m)
add BZero         y            = y
add (B0 bin {n})  BZero        = rewrite plusZeroRightNeutral (mult n 2) in B0 bin
add (B1 bin {n})  BZero        = rewrite plusZeroRightNeutral (mult n 2) in B1 bin
add (B0 l {n=v})  (B0 r {n=w}) = rewrite sym (lemmaB0plusB0 w v) in B0 (add l r)
add (B1 l {n=v})  (B0 r {n=w}) = rewrite sym (lemmaB1plusB0 v w) in B1 (add l r)
add (B0 l {n=v})  (B1 r {n=w}) = rewrite sym (lemmaB0plusB1 v w) in B1 (add l r)
add (B1 l {n=v})  (B1 r {n=w}) = rewrite sym (lemmaB1plusB1 v w) in B0 (inc (add l r))

(+.) : (x : Binary n) -> (y : Binary m) -> Binary (n + m)
(+.) = add

-- Properties
bZeroRightNeutral : (b : Binary n) -> (add b BZero = b)
bZeroRightNeutral BZero = Refl
bZeroRightNeutral (B0 bin) = ?bZeroRightNeutral_rhs_2
bZeroRightNeutral (B1 bin) = ?bZeroRightNeutral_rhs_3


text:
module TotallyTotal

%default total

zero : Nat
zero = Z


text:
module Minecraft.Core.Univ.Level.Gen

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

%default total

public export
record LevelGen (seed : Bits64) (univ : Univ) (voidBlock : As Block) where
  constructor MkLevelGen
  blockAt : Pos -> As Block

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Toolkit.Text.Parser.Run

import System.File

import Text.Parser
import Text.Lexer

import Data.List1
import Data.String
import Toolkit.Data.Nat
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run

import Toolkit.Text.Parser.Support

%default total

public export
record ParseFailure a where
  constructor MkParseFail
  error    : String
  location : FileContext

public export
data ParseError a = PError (List1 (ParseFailure a))
                  | LError LexError
                  | FError FileError

export
Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
Show a => Show (Run.ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map show err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

convert : (src : Maybe String)
       -> (err : ParsingError a)
              -> ParseFailure a
convert src (Error msg Nothing)
  = MkParseFail msg (record {source = src} emptyFC)

convert src (Error msg (Just loc))
  = let s = startBounds loc in
    let e = endBounds   loc in
    let fc = if s == e
             then newFC src s (mapSnd (+1) e)
             else newFC src s e
    in MkParseFail msg fc

runConvert : Maybe String
          -> List1 (ParsingError a)
          -> ParseError a
runConvert src es = PError (map (convert src) es)

export
parseString : {e     : _}
           -> (lexer : Lexer a)
           -> (rule  : Grammar () (a) e ty)
           -> (str   : String)
                   -> (Either (ParseError a) ty)
parseString lexer rule str =
  case lexString lexer str of
    Left err   => Left (LError err)
    Right toks =>
      case parse rule toks of
        Left err      => Left (runConvert Nothing err)
        Right (val,_) => Right val

export
covering
parseFile : {e     : _}
         -> (lexer : Lexer a)
         -> (rule  : Grammar () a e ty)
         -> (fname : String)
         -> IO $ Either (ParseError a) ty
parseFile lexer grammar fname =
  case !(lexFile lexer fname) of
    Left (LError err) => pure (Left (LError err))
    Left (LIOErr err) => pure (Left (FError err))
    Right toks =>
      case parse grammar toks of
        Left err      => pure (Left (runConvert (Just fname) err))
        Right (val,_) => pure (Right val)

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

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
totalLen : List String -> Nat
totalLen xs = foldr (\str, len => len + length str) 0 xs


text:
totalLen : List String -> Nat
totalLen xs = foldr (\str, len => length str + len) 0 xs