text:
data BSTree : Type -> Type where
    Empty : Ord elem => BSTree elem
    Node : Ord elem => (left : BSTree elem) -> (val : elem) ->
                       (right : BSTree elem) -> BSTree elem

%name BSTree tree, tree1

insert : elem -> BSTree elem -> BSTree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right) = case compare x val of
                                    LT => Node (insert x left) val right
                                    EQ => orig
                                    GT => Node left val (insert x right)

listToTree : Ord a => List a -> BSTree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

treeToList : BSTree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right

ext: idr

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Main
-- Main program. Contains main entry point, event loop, and network / concurrency
-- setup stuff.

import GameState
import GameMessage

import IdrisNet.Socket
import IdrisNet.UDP.UDPServer
import IdrisNet.UDP.UDPClient

import Effects
import Effect.Process
import Effect.SDL
import Effect.State
import Effect.StdIO

import System

CANVAS_WIDTH : Int
CANVAS_WIDTH = 640

CANVAS_HEIGHT : Int
CANVAS_HEIGHT = 480

-- Pong is a type synonym for all the effects we're going to be using within
-- the program.
-- Parameters:
--  s : SDL Surface, should one exist
--  n : UDP state
--  t : Return type
Pong : Type -> Type -> Type
Pong s t = { [ SDL s
               , STATE GameState
               , STDIO
               , UDPCLIENT
               , PROCESS (Running GameMessage)] } Eff t

PongRunning : Type -> Type
PongRunning t = Pong SDLSurface t

-- TODO: Disambiguation more nicely
networkHandlerThread' : (mthread : ProcPID GameMessage) ->
                        RunningProcessM GameMessage
                         [UDPSERVER UDPBound, STDIO]
                         [UDPSERVER (), STDIO]
networkHandlerThread' pid = with Effects do
  UDPSuccess (_, Just (pckt, _)) <- IdrisNet.UDP.UDPServer.udpReadPacket statusUpdate 256
    | UDPSuccess (_, Nothing) => do putStr "Error decoding status packet\n"
                                    networkHandlerThread' pid
    | UDPFailure err => do IdrisNet.UDP.UDPServer.udpFinalise
                           return ()
    | UDPRecoverableError err => do IdrisNet.UDP.UDPServer.udpClose
                                    return ()
  let msg = mkMessage pckt
  sendMessage pid msg
  networkHandlerThread' pid
 -- spawn : Eff

networkHandlerThread : Port ->
                       (mthread : ProcPID GameMessage) ->
                       RunningProcess GameMessage [UDPSERVER (), STDIO]
networkHandlerThread p pid = with Effects do
  putStr $ "Binding to port " ++ (show p) ++ "\n"
  UDPSuccess _ <- udpBind Nothing p
    | UDPFailure err => do putStr $ "Error binding: " ++ (show err)  ++ "\n"
                           return ()
    | UDPRecoverableError err => return ()
  networkHandlerThread' pid

handleNetworkEvents : { [STATE GameState,
                         PROCESS (Running GameMessage)] } Eff ()
handleNetworkEvents = when !hasMessage (do
  st <- get
  case !recvMessage of
    (UpdateRemotePaddle r_up r_down x y) =>
      if (isServer st) then
        put ( record { pongRemotePaddleUp = r_up,
                       pongRemotePaddleDown = r_down,
                       pongRightPaddlePos = (x, y) } st )
      else
        put ( record { pongRemotePaddleUp = r_up,
                       pongRemotePaddleDown = r_down,
                       pongLeftPaddlePos = (x, y) } st )
    (UpdateRemoteBallPos ball) => put ( record { pongBall = ball } st ))

handleKeyEvents : Maybe Event -> { [STATE GameState] } Eff Bool
handleKeyEvents (Just AppQuit) = return False
handleKeyEvents (Just (KeyUp KeyUpArrow)) = do
  put (record { pongIsUpPressed = False, pongIsPaddleChanged = True } !get)
  return True
handleKeyEvents (Just (KeyDown KeyUpArrow)) = do
  put (record { pongIsUpPressed = True, pongIsPaddleChanged = True } !get)
  return True
handleKeyEvents (Just (KeyUp KeyDownArrow)) = do
  put (record { pongIsDownPressed = False, pongIsPaddleChanged = True } !get)
  return True
handleKeyEvents (Just (KeyDown KeyDownArrow)) = do
  put (record { pongIsDownPressed = True, pongIsPaddleChanged = True } !get)
  return True
handleKeyEvents (Just (KeyUp KeySpace)) = do
  put (record { pongToLaunch = True } !get)
  return True
handleKeyEvents _ = return True

draw : PongRunning ()
draw = do
  st <- get
  rectangle white 0 0 (pongWidth st) (pongHeight st)
  drawPaddles
  drawBall
  flip

serverEvents : PongRunning ()
serverEvents = do
  ball_updated <- updateBallServer
  when ball_updated (sendBallUpdate >>= \_ => return ())

-- 2 peers. Both peers update the other on the paddle positions.
-- Server controls ball position and sends this to the remote user
eventLoop : PongRunning ()
eventLoop = do
  st <- get
  handleNetworkEvents
  continue <- handleKeyEvents !poll
  updateRemotePaddlePos
  paddle_updated <- updateLocalPaddlePos
  when paddle_updated (sendPaddleUpdate >>= \_ => return ())
  if (isServer st) then serverEvents else updateBallPos
  draw
  when continue eventLoop

setupUDP : Port -> PongRunning ()
setupUDP p = with Effects do
  pid <- getPID
  spawn GameMessage (networkHandlerThread p pid) [(), ()]
  eventLoop

printUsage : IO ()
printUsage = putStrLn "Usage: ./pong <server | client> <local port> <addr> <port>"

readInt : String -> Int
readInt = cast

modeView : String -> Maybe PongNetworkMode
modeView "client" = Just PongClient
modeView "server" = Just PongServer
modeView _ = Nothing

total
parseArgs : List String -> Maybe (PongNetworkMode, Port, SocketAddress, Port)
parseArgs [_, mode, s_lp, s_a, s_p] with (modeView mode, readInt s_lp, parseIPv4 s_a, readInt s_p)
  | (Just nm, l_p, IPv4Addr i1 i2 i3 i4, p) =
      Just (nm, l_p, (IPv4Addr i1 i2 i3 i4), p)
  | _ = Nothing
parseArgs _ = Nothing

pongMain : Port -> Pong () ()
pongMain p = with Effects do
              st <- get
              initialise (pongWidth st) (pongHeight st)
              setupUDP p
              eventLoop
              quit

main : IO ()
main = do
  args <- getArgs
 -- traverse putStrLn args
  case (parseArgs args) of
         (Just (nm, lp, sa, p)) => do
           let i_st = initState CANVAS_WIDTH CANVAS_HEIGHT nm sa p
           runInit [(), i_st, (), (), initProcess] (pongMain lp)
         Nothing => printUsage


text:
module Main

import System
import System.File
import Control.Monad.Either
import Data.List

import Common
import Parser

import Solutions.Day1
import Solutions.Day2

data Env = Run | Test

-- Read the contents of the input file as a string
getInput : Env -> (day : String) -> EitherT String IO String
getInput env day = do
  let filename = case env of
                      Run  => "./inputs/day" ++ day ++".txt"
                      Test => "./inputs/day" ++ day ++"_test.txt"
  input <- readFile filename
  case input of
    Right output => right output
    Left err => left . show $ "Could not find: \{filename}"

getSolution : (day : String) -> EitherT String IO Solution
getSolution day = case day of
     "1" => right Day1.run
     "2" => right Day2.run
     _ => left "No solution found for this day"

displaySolution : (solution : Either String (String, String)) -> String
displaySolution (Left err) = err
displaySolution (Right (part1, part2)) =
  "\nPart1:\n" ++ part1 ++ "\n\nPart2:\n" ++ part2 ++ "\n"

runProgram : Env -> (day : String) -> EitherT String IO String
runProgram env day = do
  input <- getInput env day
  solution <- getSolution day
  pure . displaySolution . solution $ input

getDayNumber : IO (Maybe String)
getDayNumber = map (tail' >=> head') getArgs

doProgram : Show day => Env -> day -> IO ()
doProgram env day = do
  Right result <- runEitherT (runProgram env (show day))
    | Left err => putStrLn err
  putStr result

-- This is extracted here to make running from the repl easier
run : Show day => day -> IO ()
run = doProgram Run

-- This is extracted here to make running from the repl easier
test : Show day => day -> IO ()
test = doProgram Test

main : IO ()
main = do
  Just day <- getDayNumber
    | Nothing => putStrLn "Please enter a day number"
  run day


text:
module Control.Optics.Either

import public Control.Optics.Prism

export
pleft : Prism (Either a c) (Either b c) a b
pleft = prism Left (either Right (Left . Right))


text:
import Aoc
import Data.List
import Data.List1
import Data.Strings
%default total

Password : Type
Password = String

record Policy where
  constructor MkPolicy
  low, high : Nat
  char : Char

||| Parse a line of input like "1-3 a: abcde".
parse : String -> Maybe (Policy, Password)
parse s =
  case split (not . isAlphaNum) s of
    -- ["1", "3", "a", "", "abcde"]
    (sl:::[sh,sc,"",p]) =>
      case (parsePositive sl, parsePositive sh, unpack sc) of
        (Just l, Just h, [c]) => Just (MkPolicy l h c, p)
        _ => Nothing
    _ => Nothing

||| The * password validity test:
conforms1 : Policy -> Password -> Bool
conforms1 policy pw =
  let n = count (== policy.char) (unpack pw)
  in n >= policy.low && n <= policy.high

||| The ** password validity test:
conforms2 : Policy -> Password -> Bool
conforms2 (MkPolicy (S i) (S j) c) pw =
  count {t=List} ((== Just c) . (`maybeIndex` unpack pw)) [i, j] == 1
conforms2 _ _ = False

main : IO ()
main = do
  pairs <- parseLines parse
  putStr "*   "; printLn $ count (uncurry conforms1) pairs
  putStr "**  "; printLn $ count (uncurry conforms2) pairs


text:
module Compiler.Jvm.Tree

import Data.List
import Data.Strings

public export
data Tree a = Node a (List (Tree a))

export
displayTree : (a -> String) -> Tree a -> String
displayTree show tree = unlines . reverse $ go [] [] 0 tree where
    indent : Nat -> String
    indent level = concat $ replicate level "  "

    showNodeData : Nat -> a -> String
    showNodeData level d = indent level ++ show d

    go : List String -> List (Nat, Tree a) -> Nat -> Tree a -> List String
    go acc [] level (Node d []) = showNodeData level d :: acc
    go acc ((treeLevel, tree) :: nextTree) nodeLevel (Node d []) =
      go (showNodeData nodeLevel d :: acc) nextTree treeLevel tree
    go acc stack level (Node d (child :: children)) =
      let childrenWithLevel = ((\c => (level + 1, c)) <$> children)
      in go (showNodeData level d :: acc) (childrenWithLevel ++ stack) (level + 1) child

implementation Show a => Show (Tree a) where
  show tree = displayTree show tree

export
levelOrder : Tree a -> List (List a)
levelOrder tree = go [] [tree]
  where
    element : Tree b -> b
    element (Node value _) = value

    subtrees : Tree b -> List (Tree b)
    subtrees (Node _ children) = children

    go : List (List b) -> List (Tree b) -> List (List b)
    go acc [] = acc
    go acc trees = go (map element trees :: acc) (concatMap subtrees trees)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


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

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

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

Ord Shape where
  compare x y = compare (area x) (area y)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Language.LSP.DocumentSymbol

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Data.List
import Language.LSP.Message
import Server.Configuration
import Server.Utils
import Server.Log

-- NOTE: Structured information should be rendereded from the actual Term of the expressions
-- in a file, that would give a better high-level overview. For now this is more like a placeholder
-- rather than a useful functionality.

||| Renders all the local names and type declarations from the Metadata of the active file.
export
documentSymbol : Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DocumentSymbolParams -> Core (List DocumentSymbol)
documentSymbol params = do
  Just (uri, _) <- gets LSPConf openFile
    | Nothing => do
        logString Debug "documentSymbol: openFile returned Nothing. Weird."
        pure []
  let True = uri == params.textDocument.uri
      | False => do
          logString Debug "documentSymbol: different URI than expected \{show (uri, params.textDocument.uri)}"
          pure []
  meta <- get MD
  let localDocSymbols
        = map (\((_, (sline,scol), (eline, ecol)), (n,_,_)) =>
                let range = MkRange (MkPosition sline scol) (MkPosition eline ecol)
                    name = show $ dropNS n
                 in ( name
                    , MkDocumentSymbol
                      { name           = name
                      , detail         = Nothing
                      , kind           = Variable
                      , tags           = Nothing
                      , deprecated     = Nothing
                      , range          = range
                      , selectionRange = range
                      , children       = Nothing
                      }
                    ))
              meta.names
  let localTypeDecSymbols
        = map (\((_,(sline,scol),(eline,ecol)), (n,_,_)) =>
                let range = MkRange (MkPosition sline scol) (MkPosition eline ecol)
                    name = show $ dropNS n
                 in ( name
                    , MkDocumentSymbol
                      { name           = name
                      , detail         = Nothing
                      , kind           = Function
                      , tags           = Nothing
                      , deprecated     = Nothing
                      , range          = range
                      , selectionRange = range
                      , children       = Nothing
                      }
                    ))
              meta.tydecls
  pure
    $ map snd
    $ sortBy (\(n1, _), (n2, _) => compare n1 n2)
    $ localDocSymbols ++ localTypeDecSymbols


text:
module Text.Lexer

import Data.Bool.Extra
import Data.List
import Data.Nat

import public Text.Lexer.Core
import public Text.Quantity
import public Text.Token

%default total

export
toTokenMap : List (Lexer, k) -> TokenMap (Token k)
toTokenMap = map $ \(l, kind) => (l, Tok kind)

||| Recognise any character.
||| /./
export
any : Lexer
any = pred (const True)

||| Recognise a lexer or recognise no input. This is not guaranteed
||| to consume input.
||| /`l`?/
export
opt : (l : Lexer) -> Recognise False
opt l = l <|> empty

||| Recognise any character if the sub-lexer `l` fails.
||| /(?!`l`)./
export
non : (l : Lexer) -> Lexer
non l = reject l <+> any

||| Produce recognisers by applying a function to elements of a container, and
||| recognise the first match. Consumes input if the function produces consuming
||| recognisers. Fails if the container is empty.
export
choiceMap : {c : Bool} ->
            Foldable t => (a -> Recognise c) -> t a -> Recognise c
choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
                                               f x <|> acc)
                           fail xs

||| Recognise the first matching recogniser in a container. Consumes input if
||| recognisers in the list consume. Fails if the container is empty.
export
choice : {c : _} ->
         Foldable t => t (Recognise c) -> Recognise c
choice = choiceMap id

||| Sequence a list of recognisers. Guaranteed to consume input if the list is
||| non-empty and the recognisers consume.
export
concat : {c : _} ->
         (xs : List (Recognise c)) -> Recognise (isCons xs && c)
concat = Lexer.Core.concatMap id

||| Recognise a specific character.
||| /[`x`]/
export
is : (x : Char) -> Lexer
is x = pred (==x)

||| Recognise anything but the given character.
||| /[\^`x`]/
export
isNot : (x : Char) -> Lexer
isNot x = pred (/=x)

||| Recognise a specific character (case-insensitive).
||| /[`x`]/i
export
like : (x : Char) -> Lexer
like x = pred (\y => toUpper x == toUpper y)

||| Recognise anything but the given character (case-insensitive).
||| /[\^`x`]/i
export
notLike : (x : Char) -> Lexer
notLike x = pred (\y => toUpper x /= toUpper y)

||| Recognise a specific string.
||| Fails if the string is empty.
||| /`str`/
export
exact : (str : String) -> Lexer
exact str = case unpack str of
                 [] => fail
                 (x :: xs) => concatMap is (x :: xs)

||| Recognise a specific string (case-insensitive).
||| Fails if the string is empty.
||| /`str`/i
export
approx : (str : String) -> Lexer
approx str = case unpack str of
                  [] => fail
                  (x :: xs) => concatMap like (x :: xs)

||| Recognise any of the characters in the given string.
||| /[`chars`]/
export
oneOf : (chars : String) -> Lexer
oneOf chars = pred (\x => x `elem` unpack chars)

||| Recognise a character range. Also works in reverse!
||| /[`start`-`end`]/
export
range : (start : Char) -> (end : Char) -> Lexer
range start end = pred (\x => (x >= min start end)
                           && (x <= max start end))

mutual
  ||| Recognise a sequence of at least one sub-lexers
  ||| /`l`+/
  export
  some : Lexer -> Lexer
  some l = l <+> many l

  ||| Recognise a sequence of at zero or more sub-lexers. This is not
  ||| guaranteed to consume input
  ||| /`l`\*/
  export
  many : Lexer -> Recognise False
  many l = opt (some l)

||| Repeat the sub-lexer `l` zero or more times until the lexer
||| `stopBefore` is encountered. `stopBefore` will not be consumed.
||| Not guaranteed to consume input.
||| /((?!`stopBefore`)`l`)\*/
export
manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
manyUntil stopBefore l = many (reject stopBefore <+> l)

||| Repeat the sub-lexer `l` zero or more times until the lexer
||| `stopAfter` is encountered, and consume it. Guaranteed to
||| consume if `stopAfter` consumes.
||| /`l`\*?`stopAfter`/
export
manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter

||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
||| /`l`{`q`}/
export
count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
count (Qty Z Nothing) l = many l
count (Qty Z (Just Z)) _ = empty
count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l
count (Qty (S min) Nothing) l = l <+> count (atLeast min) l
count (Qty (S min) (Just Z)) _ = fail
count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l

||| Recognise a single digit 0-9
||| /[0-9]/
export
digit : Lexer
digit = pred isDigit

||| Recognise one or more digits
||| /[0-9]+/
export
digits : Lexer
digits = some digit

||| Recognise a single binary digit
||| /[0-1]/
export
binDigit : Lexer
binDigit = pred (\c => c == '0' || c == '1')

||| Recognise one or more binary digits
||| /[0-1]+/
export
binDigits : Lexer
binDigits = some binDigit

||| Recognise a single hexidecimal digit
||| /[0-9A-Fa-f]/
export
hexDigit : Lexer
hexDigit = pred isHexDigit

||| Recognise one or more hexidecimal digits
||| /[0-9A-Fa-f]+/
export
hexDigits : Lexer
hexDigits = some hexDigit

||| Recognise a single octal digit
||| /[0-8]/
export
octDigit : Lexer
octDigit = pred isOctDigit

||| Recognise one or more octal digits
||| /[0-8]+/
export
octDigits : Lexer
octDigits = some octDigit

||| Recognise a single alpha character
||| /[A-Za-z]/
export
alpha : Lexer
alpha = pred isAlpha

||| Recognise one or more alpha characters
||| /[A-Za-z]+/
export
alphas : Lexer
alphas = some alpha

||| Recognise a lowercase alpha character
||| /[a-z]/
export
lower : Lexer
lower = pred isLower

||| Recognise one or more lowercase alpha characters
||| /[a-z]+/
export
lowers : Lexer
lowers = some lower

||| Recognise an uppercase alpha character
||| /[A-Z]/
export
upper : Lexer
upper = pred isUpper

||| Recognise one or more uppercase alpha characters
||| /[A-Z]+/
export
uppers : Lexer
uppers = some upper

||| Recognise an alphanumeric character
||| /[A-Za-z0-9]/
export
alphaNum : Lexer
alphaNum = pred isAlphaNum

||| Recognise one or more alphanumeric characters
||| /[A-Za-z0-9]+/
export
alphaNums : Lexer
alphaNums = some alphaNum

||| Recognise a single whitespace character
||| /\\s/
export
space : Lexer
space = pred isSpace

||| Recognise one or more whitespace characters
||| /\\s+/
export
spaces : Lexer
spaces = some space

||| Recognise a single newline sequence. Understands CRLF, CR, and LF
||| /\\r\\n|[\\r\\n]/
export
newline : Lexer
newline = let crlf = "\r\n" in
              exact crlf <|> oneOf crlf

||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
||| /(\\r\\n|[\\r\\n])+)/
export
newlines : Lexer
newlines = some newline

||| Recognise a single non-whitespace, non-alphanumeric character
||| /[\^\\sA-Za-z0-9]/
export
symbol : Lexer
symbol = pred (\x => not (isSpace x || isAlphaNum x))

||| Recognise one or more non-whitespace, non-alphanumeric characters
||| /[\^\\sA-Za-z0-9]+/
export
symbols : Lexer
symbols = some symbol

||| Recognise a single control character
||| /[\\x00-\\x1f\\x7f-\\x9f]/
export
control : Lexer
control = pred isControl

||| Recognise one or more control characters
||| /[\\x00-\\x1f\\x7f-\\x9f]+/
export
controls : Lexer
controls = some control

||| Recognise zero or more occurrences of a sub-lexer between
||| delimiting lexers
||| /`start`(`l`)\*?`end`/
export
surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
surround start end l = start <+> manyThen end l

||| Recognise zero or more occurrences of a sub-lexer surrounded
||| by the same quote lexer on both sides (useful for strings)
||| /`q`(`l`)\*?`q`/
export
quote : (q : Lexer) -> (l : Lexer) -> Lexer
quote q l = surround q q l

||| Recognise an escape character (often '\\') followed by a sub-lexer
||| /[`esc`]`l`/
export
escape : (esc : Char) -> Lexer -> Lexer
escape esc l = is esc <+> l

||| Recognise a string literal, including escaped characters.
||| (Note: doesn't yet handle escape sequences such as \123)
||| /"(\\\\.|.)\*?"/
export
stringLit : Lexer
stringLit = quote (is '"') (escape '\\' any <|> any)

||| Recognise a character literal, including escaped characters.
||| (Note: doesn't yet handle escape sequences such as \123)
||| /'(\\\\.|[\^'])'/
export
charLit : Lexer
charLit = let q = '\'' in
              is q <+> (escape '\\' (control <|> any) <|> isNot q) <+> is q
  where
    lexStr : List String -> Lexer
    lexStr [] = fail
    lexStr (t :: ts) = exact t <|> lexStr ts

    control : Lexer
    control = lexStr ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",
                      "BS",  "HT",  "LF",  "VT",  "FF",  "CR",  "SO",  "SI",
                      "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",
                      "CAN", "EM",  "SUB", "ESC", "FS",  "GS",  "RS",  "US",
                      "SP",  "DEL"]
                <|> (is 'b' <+> binDigits)
                <|> (is 'x' <+> hexDigits)
                <|> (is 'o' <+> octDigits)
                <|> digits

||| Recognise an integer literal (possibly with a '-' prefix)
||| /-?[0-9]+/
export
intLit : Lexer
intLit = opt (is '-') <+> digits

||| Recognise a binary literal, prefixed by "0b"
||| /0b[0-1]+/
export
binLit : Lexer
binLit = exact "0b" <+> binDigits

||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
||| /0[Xx][0-9A-Fa-f]+/
export
hexLit : Lexer
hexLit = approx "0x" <+> hexDigits

||| Recognise an octal literal, prefixed by "0o"
||| /0o[0-9A-Fa-f]+/
export
octLit : Lexer
octLit = exact "0o" <+> octDigits

||| Recognise `start`, then recognise all input until a newline is encountered,
||| and consume the newline. Will succeed if end-of-input is encountered before
||| a newline.
||| /`start`[\^\\r\\n]+(\\r\\n|[\\r\\n])?/
export
lineComment : (start : Lexer) -> Lexer
lineComment start = start <+> manyUntil newline any <+> opt newline

||| Recognise all input between `start` and `end` lexers.
||| Supports balanced nesting.
|||
||| For block comments that don't support nesting (such as C-style comments),
||| use `surround`
export
blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
blockComment start end = start <+> middle <+> end
  where
    middle : Recognise False
    middle = manyUntil end (blockComment start end <|> any)


text:
import Data.HashMap

main : IO ()
main = go max_n empty
  where
    max_n : Int
    max_n = 10

    go : Int -> HashMap String Int -> IO ()
    go 0 hm = putStrLn "finished"
    go n hm = do
        printLn n
        str <- getLine
        putStrLn str
        let hm' = insert str n hm
        go (n - 1) hm'


text:
VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

data MachineCmd : Type ->
                  VendState ->
                  VendState ->
                  Type where
     InsertCoin : MachineCmd () (pounds, chocs) (S pounds, chocs)
     Vend       : MachineCmd () (S pounds, S chocs) (pounds, chocs)
     GetCoins   : MachineCmd () (pounds, chocs) (Z, chocs)
     Refill     : (bars : Nat) -> MachineCmd () (Z, chocs) (Z, bars + chocs)

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

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

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

namespace MachineDo
  (>>=) : MachineCmd a state1 state2 -> (a -> Inf (MachineIO state2)) ->
          MachineIO state1
  (>>=) = Do

mutual
  vend : MachineIO (pounds, chocs)
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop
  vend {pounds = (S k)} {chocs = (S j)} = do Vend
                                             Display "Enjoy!"
                                             machineLoop

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

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


text:
module Flexidisc.Dec.IsYes

%default total

||| Build at type level the proof that a decidable property is valid
public export
data IsYes : prop -> Type where
  SoTrue : IsYes (Yes prop)

%name IsYes yes, prf, ok

||| Demote a proof from the type level to the value level
export
getProof : {witness : Dec prop} -> IsYes witness -> prop
getProof yes {witness = (Yes prf)} = prf
getProof yes {witness = (No contra)} impossible

||| If I can prove two times that a property doesn't hold,
||| the two proofs are equal
export
uniqueYes : (prop : Dec any) -> (x, y : IsYes prop) -> x = y
uniqueYes (Yes prf) SoTrue SoTrue = Refl
uniqueYes (No _) SoTrue _ impossible

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
{-
foo
bar
baz
'q'
'u'
'x'
-}
module Main

main : IO ()
main = do
  putStrLn . pack $ ['f', 'o', 'o']
  for_ (words "bar baz ") putStrLn
  for_ (unpack "qux") (putStrLn . show)

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Addition.Adhoc

import Common.Abbrev
import Common.Interfaces
import Specifications.Ring
import Proofs.RingTheory

%default total
%access export

adhocIdentity1 : Ringops s => RingSpec {s} (+) Zero Ng (*) -> (b,x,y,z : s) ->
  a = b + c -> x + y * z + y * a = x + y * (z + b + c)
adhocIdentity1 spec {a} b {c} x y z given = o3 where
  o1 : z + a = z + b + c
  o1 = cong given === associative (monoid (group spec)) z b c
  o2 : y * z + y * a = y * (z + b + c)
  o2 = distributativeL spec y z a @== cong o1
  o3 : x + y * z + y * a = x + y * (z + b + c)
  o3 = associative (monoid (group spec)) x _ _ @== cong o2

adhocIdentity2 : Ringops s => RingSpec {s} (+) Zero Ng (*) -> (x,a : s) ->
  x = x + a * Zero
adhocIdentity2 spec x a = sym (o1 === o2) where
  o1 : x + a * Zero = x + Zero
  o1 = cong $ zeroAbsorbsR spec a
  o2 : x + Zero = x
  o2 = neutralR (monoid (group spec)) x

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
module Test.Integer

import Data.Prim.Integer
import Data.SOP
import Hedgehog
import Test.RingLaws

allInteger : Gen Integer
allInteger = integer (linear (-0x8000000000000000) 0xffffffffffffffff)

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allInteger, allInteger]
  toOrdering (comp m n) === compare m n

export
props : Group
props = MkGroup "Int16" $
  [ ("prop_comp",   prop_comp)
  ] ++ ringProps allInteger


text:
module Parser

import Lightyear.Core
import Lightyear.Strings
import Lightyear.Combinators
import Queries

sqltype : Parser SQLiteType
sqltype = the (Parser _) $
          (do token "int"  <|> token "integer"
              pure INTEGER)
      <|> (do token "text" <|> token "string"
              pure TEXT)
      <|> (do token "real" <|> token "float"
              pure REAL)

name : Parser String
name = do n <- many (satisfy (\c => c >= 'a' && c <= 'z' || c >= 'A' && c <= 'Z'))
          return (pack n)

nullable : Parser Bool
nullable = (do token "not"
               token "null"
               return False)
       <|> return True

sqlCol : Parser Attribute
sqlCol = do n <- name
            space
            ty <- sqltype
            null <- nullable
            pure (n:::(if null then NULLABLE ty else ty))

comma : Parser ()
comma = char ','

cols : Parser Schema
cols = do cols <- sepBy sqlCol (space $> comma $> space)
          pure (toSchema cols)
  where toSchema : List Attribute -> Schema
        toSchema [] = []
        toSchema (x::xs) = x :: toSchema xs

table : Parser (String, Schema)
table = do token "create"
           token "table"
           n <- name
           space
           token "("
           cs <- cols
           space
           token ")"
           pure (n,cs)

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
fold_length : (l : List a) -> Nat
fold_length l = foldr (\_, n => S n) 0 l

test_fold_length1 : fold_length [4, 7, 0] = 3
test_fold_length1 = Refl

test_fold_length2 : fold_length [1] = 1
test_fold_length2 = Refl

fold_length_correct : (l : List a) -> fold_length l = length l
fold_length_correct [] = Refl
fold_length_correct (x :: xs) = rewrite fold_length_correct xs in Refl

fold_map : (f : a -> b) -> (l : List a) -> List b
fold_map f l = foldr (\el, acc => f el :: acc) [] l

fold_map_correct : (f : a -> b) -> (l : List a) -> fold_map f l = map f l
fold_map_correct f [] = Refl
fold_map_correct f (x :: xs) = rewrite fold_map_correct f xs in Refl

prod_curry : (f : (a, b) -> c) -> (x : a) -> (y : b) -> c
prod_curry f x y = f (x, y)

prod_uncurry : (f : a -> b -> c) -> (p : (a, b)) -> c
prod_uncurry f (a, b) = f a b

test_map1 : map (+3) [2, 0, 2] = [5, 3, 5]
test_map1 = Refl

uncurry_curry : (f : a -> b -> c) -> (x : a) -> (y : b) -> prod_curry (prod_uncurry f) x y = f x y
uncurry_curry f x y = Refl

curry_uncurry : (f : (a, b) -> c) -> (p : (a, b)) -> prod_uncurry (prod_curry f) p = f p
curry_uncurry f (a, b) = Refl

nth_error : (l : List x) -> (n : Nat) -> Maybe x
nth_error [] n = Nothing
nth_error (h :: l') n =
    if n == 0
        then Just h
        else nth_error l' (pred n)

out_of_bounds_nothing : (n : Nat) -> (l : List a) -> length l = n -> nth_error l n = Nothing
out_of_bounds_nothing (length []) [] Refl = Refl
out_of_bounds_nothing (length (x :: xs)) (x :: xs) Refl =
    rewrite out_of_bounds_nothing (length xs) xs Refl in
        Refl

Church : {x : Type} -> Type
Church {x} = (x -> x) -> x -> x

one : Church
one f x = f x

two : Church
two f x = f $ f x

zero : Church
zero f x = x

three : Church
three f x = f $ f $ f x

succ' : (n : Church {x}) -> Church {x}
succ' n = ?impl

succ1 : succ' zero = one
succ1 = ?succ1_rhs


text:
module Client.Skeleton.BaseWithTest.Test.Suite

import Fmt

export
name : (String, String) -> List String
name = const ["Test", "Suite.idr"]

export
build : (String, String) -> String
build (packageNS, packageName) = fmt """
module Test.Suite

import IdrTest.Test

import Test.%sTest

suite : IO ()
suite = do
  runSuites
    [ Test.%sTest.suite
    ]
""" packageName packageName

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Linear.Types

public export
(-<>) : Type -> Type -> Type
(-<>) a b = (1 x : a) -> b

infixr 0 -<>

public export
void1 : Void -<> a
void1 x impossible

public export
interface LBifunctor f where
  bimap : (a -<> c) -> (b -<> d) -> f a b -<> f c d

namespace LPair

  public export
  0 fst : LPair a b -> a
  fst (x # y) = x

  public export
  0 snd : LPair a b -> b
  snd (x # y) = y

  public export
  0 surjPairing : (w : LPair a b) -> fst w # snd w = w
  surjPairing (x # y) = Refl

public export
LBifunctor LPair where
  bimap f g (x # y) = (f x) # (g y)

public export
data I : Type where
 Star : I

namespace Sigma1
  public export
  data Sigma1 : (a : Type) -> (b : a -> Type) -> Type where
    (#) : (1 x : a) -> (1 y : b x) -> Sigma1 a b

namespace Sigma0
  public export
  data Sigma0 : (a : Type) -> (b : a -> Type) -> Type where
    (#): (0 x : a) -> (1 y : b x) -> Sigma0 a b

  public export
  0 fst : Sigma0 a b -<> a
  fst (x # y) = x

  public export
  snd : (1 x : Sigma0 a b) -> b (fst x)
  snd (x # y) = y

public export
data Sum : (a : Type) -> (b : Type) -> Type where
  Inl : (1 x : a) -> Sum a b
  Inr : (1 y : b) -> Sum a b

public export
Uninhabited (Inl x = Inr y) where
  uninhabited p impossible

public export
LBifunctor Sum where
 bimap f g (Inl x) = Inl $ f x
 bimap f g (Inr y) = Inr $ g y

namespace With
  public export
  0 With : Type -> Type -> Type
  With a b = (1 x : Bool) -> if x then a else b

  public export
  bimap : (a -<> c) -> (b -<> d) -> With a b -<> With c d
  bimap f g x True  = f (x True)
  bimap f g x False = g (x False)

namespace DWith
  public export
  0 DWith : (a : Type) -> (b : a -> Type) -> Type
  DWith a b = Sigma0 a (\x => With (Sigma1 a (\z => z = x)) (b x))

  public export
  fstW : DWith a b -<> a
  fstW (_ # w) = let (z # Refl) = (w True) in z

  public export
  sndW : (1 w : DWith a b) -> b (fstW {b = b} w)
  sndW (x # w) = replace {p = b} (eq (x # w)) (w False)
  where
    eq : (w : DWith a b) -> fst w = fstW {b = b} w
    eq (x # w) with (w True)
      eq (z # w) | (z # Refl) = Refl

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module ViluonsMachine

import Data.Fin
import Data.Vect

data Instr : (nr : Nat) -> (ni : Nat) -> Type where
	IJmp : Fin (S ni) -> Instr nr ni
	IJIZ : Fin nr -> Fin (S ni) -> Instr nr ni
	IIncr : Fin nr -> Instr nr ni
	IDecr : Fin nr -> Instr nr ni

data Prog : (nr : Nat) -> Type where
	MkProg : {ni : Nat} -> Vect ni (Instr nr ni) -> Prog nr

raiseFin : Fin n -> Fin (S n)
raiseFin FZ = FZ
raiseFin (FS f) = FS $ raiseFin f

raiseFin' : Fin n -> Fin (m + n)
raiseFin' {m=Z} f = f
raiseFin' {m=S m} f = raiseFin $ raiseFin' f

incrFin : Fin n -> Fin (m + n)
incrFin {m=Z} f = f
incrFin {m=S m} f = FS $ incrFin f

reduceFin : Fin (S n) -> Maybe (Fin n)
reduceFin {n=Z} f = Nothing
reduceFin {n=S n} FZ = Just FZ
reduceFin {n=S n} (FS f) = map FS $ reduceFin f

mapJumps : (Fin (S n) -> Fin (S m)) -> Instr nr n -> Instr nr m
mapJumps f (IJmp to) = IJmp $ f to
mapJumps f (IJIZ r to) = IJIZ r $ f to
mapJumps f (IIncr r) = IIncr r
mapJumps f (IDecr r) = IDecr r

Semigroup (Prog nr) where
	(MkProg {ni=na} a) <+> (MkProg {ni=nb} b) =
		MkProg $
		map (mapJumps $ replace {P=Fin} (plusCommutative nb (S na)) . raiseFin') a
		++
		map (mapJumps $ replace {P=Fin} (sym $ plusSuccRightSucc na nb) . incrFin) b

Monoid (Prog nr) where
	neutral = MkProg []

MemState : Nat -> Type
MemState nr = Vect nr Nat
ExecState : Nat -> Type
ExecState ni = Fin ni

total
tick : Instr nr ni -> (ExecState ni, MemState nr) -> (ExecState (S ni), MemState nr)
tick (IJmp to) (_, ms) = (to, ms)
tick (IJIZ r to) (es, ms) =
	if index r ms == 0
	then (to, ms)
	else (FS es, ms)
tick (IIncr r) (es, ms) = (FS es, updateAt r S ms)
tick (IDecr r) (es, ms) = (FS es, updateAt r (\a => minus a 1) ms)

total
tick' : Vect ni (Instr nr ni) -> (ExecState ni, MemState nr) -> MemState nr
tick' prog (es, ms) = let
		s' = tick (index es prog) (es, ms)
	in maybe (snd s') (\es'' => assert_total $ tick' prog (es'', snd s')) $ reduceFin $ fst s'

total
exec : Prog nr -> MemState nr -> MemState nr
exec (MkProg {ni=Z} prog) ms = ms
exec (MkProg {ni=S ni} prog) ms = tick' prog (0, ms)

total
reduceFinLast : {n : Nat} -> reduceFin (last {n}) = Nothing
reduceFinLast {n=Z} = Refl
reduceFinLast {n=S n} = replace {P = \l => map FS l = Nothing} (sym $ reduceFinLast {n}) Refl

-- execEndIf :
-- 	(prog : Vect ni (Instr nr ni)) ->
-- 	(es : ExecState ni) ->
-- 	(ms : MemState nr) ->
-- 	fst (tick (index es prog) (es, ms)) = last ->
-- 	tick' prog (es, ms) = snd (tick (index es prog) (es, ms))
-- execEndIf prog es ms prf = ?t

-- execEndIff :
-- 	(prog : Vect ni (Instr nr ni)) ->
--

toZero : Fin nr -> Prog nr
toZero reg = MkProg [
	IJIZ reg 3,
	IDecr reg,
	IJmp 0
]

toZeroZero : index r (exec (toZero r) ms) = 0
-- toZeroZero = ?t

max_stars_repo_name: CoderPuppy/viluons-machine

max_issues_repo_name: CoderPuppy/viluons-machine

max_forks_repo_name: CoderPuppy/viluons-machine


text:
record Votes where
       constructor MkVotes
       upvotes : Integer
       downvotes : Integer

record Article where
       constructor MkArticle
       title : String
       url : String
       score : Votes

initPage : (title : String) -> (url : String) -> Article
initPage title url = MkArticle title url (MkVotes 0 0)

badSite : Article
badSite = MkArticle "Bad Page" "http://example.com/bad" (MkVotes 5 47)

goodSite : Article
goodSite = MkArticle "Good Page" "http://example.com/good" (MkVotes 101 7)

-- Exercise 3

getScore : Article -> Integer
getScore article = upvotes (score article) - downvotes (score article)

-- Exercise 4

addUpvote : Article -> Article
addUpvote = record { score->upvotes $= (+1) }

addDownvote : Article -> Article
addDownvote = record { score->downvotes $= (+1) }


text:
||| Test if the type of variables bound in as patterns is correctly reported
||| by :typeat, both in the pattern and in the right hand side

f : Maybe Nat -> Nat
f x@(Just y@(S _)) = ?rhs1 x y
f _ = ?rhs2


text:
module Core.Core

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

import Data.List
import Data.List1
import Data.String
import Data.Vect

import Libraries.Data.IMaybe
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.Binary

import public Data.IORef
import System
import System.File

%default covering

public export
data TTCErrorMsg
    = Format String Int Int
    | EndOfBuffer String
    | Corrupt String

public export
data CaseError = DifferingArgNumbers
               | DifferingTypes
               | MatchErased (vars ** (Env Term vars, Term vars))
               | NotFullyApplied Name
               | UnknownType

public export
data DotReason = NonLinearVar
               | VarApplied
               | NotConstructor
               | ErasedArg
               | UserDotted
               | UnknownDot
               | UnderAppliedCon

export
Show DotReason where
  show NonLinearVar = "Non linear pattern variable"
  show VarApplied = "Variable applied to arguments"
  show NotConstructor = "Not a constructor application or primitive"
  show ErasedArg = "Erased argument"
  show UserDotted = "User dotted"
  show UnknownDot = "Unknown reason"
  show UnderAppliedCon = "Under-applied constructor"

export
Pretty DotReason where
  pretty NonLinearVar = reflow "Non linear pattern variable"
  pretty VarApplied = reflow "Variable applied to arguments"
  pretty NotConstructor = reflow "Not a constructor application or primitive"
  pretty ErasedArg = reflow "Erased argument"
  pretty UserDotted = reflow "User dotted"
  pretty UnknownDot = reflow "Unknown reason"
  pretty UnderAppliedCon = reflow "Under-applied constructor"

public export
data Warning : Type where
     ParserWarning : FC -> String -> Warning
     UnreachableClause : {vars : _} ->
                         FC -> Env Term vars -> Term vars -> Warning
     ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
     Deprecated : String -> Warning
     GenericWarn : String -> Warning

-- All possible errors, carrying a location
public export
data Error : Type where
     Fatal : Error -> Error -- flag as unrecoverable (so don't postpone awaiting further info)
     CantConvert : {vars : _} ->
                   FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
     CantSolveEq : {vars : _} ->
                   FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error
     PatternVariableUnifies : {vars : _} ->
                              FC -> Env Term vars -> Name -> Term vars -> Error
     CyclicMeta : {vars : _} ->
                  FC -> Env Term vars -> Name -> Term vars -> Error
     WhenUnifying : {vars : _} ->
                    FC -> Context -> Env Term vars -> Term vars -> Term vars -> Error -> Error
     ValidCase : {vars : _} ->
                 FC -> Env Term vars -> Either (Term vars) Error -> Error

     UndefinedName : FC -> Name -> Error
     InvisibleName : FC -> Name -> Maybe Namespace -> Error
     BadTypeConType : FC -> Name -> Error
     BadDataConType : FC -> Name -> Name -> Error
     NotCovering : FC -> Name -> Covering -> Error
     NotTotal : FC -> Name -> PartialReason -> Error
     LinearUsed : FC -> Nat -> Name -> Error
     LinearMisuse : FC -> Name -> RigCount -> RigCount -> Error
     BorrowPartial : {vars : _} ->
                     FC -> Env Term vars -> Term vars -> Term vars -> Error
     BorrowPartialType : {vars : _} ->
                         FC -> Env Term vars -> Term vars -> Error
     AmbiguousName : FC -> List Name -> Error
     AmbiguousElab : {vars : _} ->
                     FC -> Env Term vars -> List (Term vars) -> Error
     AmbiguousSearch : {vars : _} ->
                       FC -> Env Term vars -> Term vars -> List (Term vars) -> Error
     AmbiguityTooDeep : FC -> Name -> List Name -> Error
     AllFailed : List (Maybe Name, Error) -> Error
     RecordTypeNeeded : {vars : _} ->
                        FC -> Env Term vars -> Error
     NotRecordField : FC -> String -> Maybe Name -> Error
     NotRecordType : FC -> Name -> Error
     IncompatibleFieldUpdate : FC -> List String -> Error
     InvalidArgs : {vars : _} ->
                        FC -> Env Term vars -> List Name -> Term vars -> Error
     TryWithImplicits : {vars : _} ->
                        FC -> Env Term vars -> List (Name, Term vars) -> Error
     BadUnboundImplicit : {vars : _} ->
                          FC -> Env Term vars -> Name -> Term vars -> Error
     CantSolveGoal : {vars : _} ->
                     FC -> Context -> Env Term vars -> Term vars ->
                     Maybe Error -> Error
     DeterminingArg : {vars : _} ->
                      FC -> Name -> Int -> Env Term vars -> Term vars -> Error
     UnsolvedHoles : List (FC, Name) -> Error
     CantInferArgType : {vars : _} ->
                        FC -> Env Term vars -> Name -> Name -> Term vars -> Error
     SolvedNamedHole : {vars : _} ->
                       FC -> Env Term vars -> Name -> Term vars -> Error
     VisibilityError : FC -> Visibility -> Name -> Visibility -> Name -> Error
     NonLinearPattern : FC -> Name -> Error
     BadPattern : FC -> Name -> Error
     NoDeclaration : FC -> Name -> Error
     AlreadyDefined : FC -> Name -> Error
     NotFunctionType : {vars : _} ->
                       FC -> Env Term vars -> Term vars -> Error
     RewriteNoChange : {vars : _} ->
                       FC -> Env Term vars -> Term vars -> Term vars -> Error
     NotRewriteRule : {vars : _} ->
                      FC -> Env Term vars -> Term vars -> Error
     CaseCompile : FC -> Name -> CaseError -> Error

     MatchTooSpecific : {vars : _} ->
                        FC -> Env Term vars -> Term vars -> Error
     BadDotPattern : {vars : _} ->
                     FC -> Env Term vars -> DotReason -> Term vars -> Term vars -> Error
     BadImplicit : FC -> String -> Error
     BadRunElab : {vars : _} ->
                  FC -> Env Term vars -> Term vars -> (description : String) -> Error
     GenericMsg : FC -> String -> Error
     TTCError : TTCErrorMsg -> Error
     FileErr : String -> FileError -> Error
     CantFindPackage : String -> Error
     LitFail : FC -> Error
     LexFail : FC -> String -> Error
     ParseFail : List1 (FC, String) -> Error
     ModuleNotFound : FC -> ModuleIdent -> Error
     CyclicImports : List ModuleIdent -> Error
     ForceNeeded : Error
     InternalError : String -> Error
     UserError : String -> Error
     ||| Contains list of specifiers for which foreign call cannot be resolved
     NoForeignCC : FC -> List String -> Error
     BadMultiline : FC -> String -> Error
     Timeout : String -> Error

     InType : FC -> Name -> Error -> Error
     InCon : FC -> Name -> Error -> Error
     InLHS : FC -> Name -> Error -> Error
     InRHS : FC -> Name -> Error -> Error

     MaybeMisspelling : Error -> List1 String -> Error
     WarningAsError : Warning -> Error

export
Show TTCErrorMsg where
  show (Format file ver exp) =
    let age = if ver < exp then "older" else "newer" in
        "TTC data is in an " ++ age ++ " format, file: " ++ file ++ ", expected version: " ++ show exp ++ ", actual version: " ++ show ver
  show (EndOfBuffer when) = "End of buffer when reading " ++ when
  show (Corrupt ty) = "Corrupt TTC data for " ++ ty

-- Simplest possible display - higher level languages should unelaborate names
-- and display annotations appropriately

export
Show Warning where
    show (ParserWarning _ msg) = msg
    show (UnreachableClause _ _ _) = ":Unreachable clause"
    show (ShadowingGlobalDefs _ _) = ":Shadowing names"
    show (Deprecated name) = ":Deprecated " ++ name
    show (GenericWarn msg) = msg

export
Show Error where
  show (Fatal err) = show err
  show (CantConvert fc _ env x y)
      = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y
  show (CantSolveEq fc _ env x y)
      = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
  show (PatternVariableUnifies fc env n x)
      = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
  show (CyclicMeta fc env n tm)
      = show fc ++ ":Cycle detected in metavariable solution " ++ show n
             ++ " = " ++ show tm
  show (WhenUnifying fc _ _ x y err)
      = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
  show (ValidCase fc _ prob)
      = show fc ++ ":" ++
           case prob of
             Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"
             Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)
  show (UndefinedName fc x)
    = show fc ++ ":Undefined name " ++ show x
  show (InvisibleName fc x (Just ns))
       = show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
         show ns ++ " is not explicitly imported"
  show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private"
  show (BadTypeConType fc n)
       = show fc ++ ":Return type of " ++ show n ++ " must be Type"
  show (BadDataConType fc n fam)
       = show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam
  show (NotCovering fc n cov)
       = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
            case cov of
                 IsCovering => "Oh yes it is (Internal error!)"
                 MissingCases cs => "Missing cases:\n\t" ++
                                           showSep "\n\t" (map show cs)
                 NonCoveringCall ns => "Calls non covering function"
                                           ++ (case ns of
                                                   [fn] => " " ++ show fn
                                                   _ => "s: " ++ showSep ", " (map show ns))

  show (NotTotal fc n r)
       = show fc ++ ":" ++ show n ++ " is not total"
  show (LinearUsed fc count n)
      = show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n
  show (LinearMisuse fc n exp ctx)
      = show fc ++ ":Trying to use " ++ showRig exp ++ " name " ++ show n ++
                   " in " ++ showRel ctx ++ " context"
     where
       showRig : RigCount -> String
       showRig = elimSemi
         "linear"
         "irrelevant"
         (const "unrestricted")

       showRel : RigCount -> String
       showRel = elimSemi
         "relevant"
         "irrelevant"
         (const "non-linear")
  show (BorrowPartial fc env t arg)
      = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++
                   " so must be fully applied"
  show (BorrowPartialType fc env t)
      = show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type"

  show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns
  show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts
  show (AmbiguousSearch fc env tgt ts) = show fc ++ ":Ambiguous search " ++ show ts
  show (AmbiguityTooDeep fc n ns)
      = show fc ++ ":Ambiguity too deep in " ++ show n ++ " " ++ show ns
  show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
  show (RecordTypeNeeded fc env)
      = show fc ++ ":Can't infer type of record to update"
  show (NotRecordField fc fld Nothing)
      = show fc ++ ":" ++ fld ++ " is not part of a record type"
  show (NotRecordField fc fld (Just ty))
      = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld
  show (NotRecordType fc ty)
      = show fc ++ ":" ++ show ty ++ " is not a record type"
  show (IncompatibleFieldUpdate fc flds)
      = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
  show (InvalidArgs fc env ns tm)
     = show fc ++ ":" ++ show ns ++ " are not valid arguments in " ++ show tm
  show (TryWithImplicits fc env imps)
     = show fc ++ ":Need to bind implicits "
          ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
          ++ "\n(The front end should probably have done this for you. Please report!)"
  show (BadUnboundImplicit fc env n ty)
      = show fc ++ ":Can't bind name " ++ nameRoot n ++
                   " with type " ++ show ty
  show (CantSolveGoal fc gam env g cause)
      = show fc ++ ":Can't solve goal " ++ assert_total (show g)
  show (DeterminingArg fc n i env g)
      = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++
                " since argument " ++ show n ++ " can't be inferred"
  show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs
  show (CantInferArgType fc env n h ty)
      = show fc ++ ":Can't infer type for " ++ show n ++
                   " (got " ++ show ty ++ " with hole " ++ show h ++ ")"
  show (SolvedNamedHole fc _ h _) = show fc ++ ":Named hole " ++ show h ++ " is solved by unification"
  show (VisibilityError fc vx x vy y)
      = show fc ++ ":" ++ show vx ++ " " ++ show x ++ " cannot refer to "
                       ++ show vy ++ " " ++ show y
  show (NonLinearPattern fc n) = show fc ++ ":Non linear pattern variable " ++ show n
  show (BadPattern fc n) = show fc ++ ":Pattern not allowed here: " ++ show n
  show (NoDeclaration fc x) = show fc ++ ":No type declaration for " ++ show x
  show (AlreadyDefined fc x) = show fc ++ ":" ++ show x ++ " is already defined"
  show (NotFunctionType fc env tm) = show fc ++ ":Not a function type: " ++ show tm
  show (RewriteNoChange fc env rule ty)
      = show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty
  show (NotRewriteRule fc env rule)
      = show fc ++ ":" ++ show rule ++ " is not a rewrite rule type"
  show (CaseCompile fc n DifferingArgNumbers)
      = show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments"
  show (CaseCompile fc n DifferingTypes)
      = show fc ++ ":Patterns for " ++ show n ++ " require matching on different types"
  show (CaseCompile fc n UnknownType)
      = show fc ++ ":Can't infer type to match in " ++ show n
  show (CaseCompile fc n (MatchErased (_ ** (env, tm))))
      = show fc ++ ":Attempt to match on erased argument " ++ show tm ++
                   " in " ++ show n
  show (CaseCompile fc n (NotFullyApplied c))
      = show fc ++ ":Constructor " ++ show c ++ " is not fully applied"
  show (MatchTooSpecific fc env tm)
      = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"
  show (BadDotPattern fc env reason x y)
      = show fc ++ ":Can't match on " ++ show x ++
           " (" ++ show reason ++ ")" ++
           " - it elaborates to " ++ show y
  show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
  show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")"
  show (GenericMsg fc str) = show fc ++ ":" ++ str
  show (TTCError msg) = "Error in TTC file: " ++ show msg
  show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
  show (CantFindPackage fname) = "Can't find package " ++ fname
  show (LitFail fc) = show fc ++ ":Can't parse literate"
  show (LexFail fc err) = show fc ++ ":Lexer error (" ++ show err ++ ")"
  show (ParseFail errs) = "Parse errors (" ++ show errs ++ ")"
  show (ModuleNotFound fc ns)
      = show fc ++ ":" ++ show ns ++ " not found"
  show (CyclicImports ns)
      = "Module imports form a cycle: " ++ showSep " -> " (map show ns)
  show ForceNeeded = "Internal error when resolving implicit laziness"
  show (InternalError str) = "INTERNAL ERROR: " ++ str
  show (UserError str) = "Error: " ++ str
  show (NoForeignCC fc specs) = show fc ++
       ":The given specifier " ++ show specs ++ " was not accepted by any available backend."
  show (BadMultiline fc str) = "Invalid multiline string: " ++ str
  show (Timeout str) = "Timeout in " ++ str

  show (InType fc n err)
       = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
         show err
  show (InCon fc n err)
       = show fc ++ ":When elaborating type of constructor " ++ show n ++ ":\n" ++
         show err
  show (InLHS fc n err)
       = show fc ++ ":When elaborating left hand side of " ++ show n ++ ":\n" ++
         show err
  show (InRHS fc n err)
       = show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++
         show err

  show (MaybeMisspelling err ns)
     = show err ++ "\nDid you mean" ++ case ns of
         (n ::: []) => ": " ++ n ++ "?"
         _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
  show (WarningAsError w) = show w

export
getWarningLoc : Warning -> Maybe FC
getWarningLoc (ParserWarning fc _) = Just fc
getWarningLoc (UnreachableClause fc _ _) = Just fc
getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
getWarningLoc (Deprecated _) = Nothing
getWarningLoc (GenericWarn _) = Nothing

export
getErrorLoc : Error -> Maybe FC
getErrorLoc (Fatal err) = getErrorLoc err
getErrorLoc (CantConvert loc _ _ _ _) = Just loc
getErrorLoc (CantSolveEq loc _ _ _ _) = Just loc
getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
getErrorLoc (CyclicMeta loc _ _ _) = Just loc
getErrorLoc (WhenUnifying loc _ _ _ _ _) = Just loc
getErrorLoc (ValidCase loc _ _) = Just loc
getErrorLoc (UndefinedName loc _) = Just loc
getErrorLoc (InvisibleName loc _ _) = Just loc
getErrorLoc (BadTypeConType loc _) = Just loc
getErrorLoc (BadDataConType loc _ _) = Just loc
getErrorLoc (NotCovering loc _ _) = Just loc
getErrorLoc (NotTotal loc _ _) = Just loc
getErrorLoc (LinearUsed loc _ _) = Just loc
getErrorLoc (LinearMisuse loc _ _ _) = Just loc
getErrorLoc (BorrowPartial loc _ _ _) = Just loc
getErrorLoc (BorrowPartialType loc _ _) = Just loc
getErrorLoc (AmbiguousName loc _) = Just loc
getErrorLoc (AmbiguousElab loc _ _) = Just loc
getErrorLoc (AmbiguousSearch loc _ _ _) = Just loc
getErrorLoc (AmbiguityTooDeep loc _ _) = Just loc
getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
getErrorLoc (AllFailed []) = Nothing
getErrorLoc (RecordTypeNeeded loc _) = Just loc
getErrorLoc (NotRecordField loc _ _) = Just loc
getErrorLoc (NotRecordType loc _) = Just loc
getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
getErrorLoc (InvalidArgs loc _ _ _) = Just loc
getErrorLoc (TryWithImplicits loc _ _) = Just loc
getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
getErrorLoc (CantSolveGoal loc _ _ _ _) = Just loc
getErrorLoc (DeterminingArg loc _ _ _ _) = Just loc
getErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just loc
getErrorLoc (UnsolvedHoles []) = Nothing
getErrorLoc (CantInferArgType loc _ _ _ _) = Just loc
getErrorLoc (SolvedNamedHole loc _ _ _) = Just loc
getErrorLoc (VisibilityError loc _ _ _ _) = Just loc
getErrorLoc (NonLinearPattern loc _) = Just loc
getErrorLoc (BadPattern loc _) = Just loc
getErrorLoc (NoDeclaration loc _) = Just loc
getErrorLoc (AlreadyDefined loc _) = Just loc
getErrorLoc (NotFunctionType loc _ _) = Just loc
getErrorLoc (RewriteNoChange loc _ _ _) = Just loc
getErrorLoc (NotRewriteRule loc _ _) = Just loc
getErrorLoc (CaseCompile loc _ _) = Just loc
getErrorLoc (MatchTooSpecific loc _ _) = Just loc
getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
getErrorLoc (BadImplicit loc _) = Just loc
getErrorLoc (BadRunElab loc _ _ _) = Just loc
getErrorLoc (GenericMsg loc _) = Just loc
getErrorLoc (TTCError _) = Nothing
getErrorLoc (FileErr _ _) = Nothing
getErrorLoc (CantFindPackage _) = Nothing
getErrorLoc (LitFail loc) = Just loc
getErrorLoc (LexFail loc _) = Just loc
getErrorLoc (ParseFail ((loc, _) ::: _)) = Just loc
getErrorLoc (ModuleNotFound loc _) = Just loc
getErrorLoc (CyclicImports _) = Nothing
getErrorLoc ForceNeeded = Nothing
getErrorLoc (InternalError _) = Nothing
getErrorLoc (UserError _) = Nothing
getErrorLoc (NoForeignCC loc _) = Just loc
getErrorLoc (BadMultiline loc _) = Just loc
getErrorLoc (Timeout _) = Nothing
getErrorLoc (InType _ _ err) = getErrorLoc err
getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err
getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
getErrorLoc (WarningAsError warn) = getWarningLoc warn

-- Core is a wrapper around IO that is specialised for efficiency.
export
record Core t where
  constructor MkCore
  runCore : IO (Either Error t)

export
coreRun : Core a ->
          (Error -> IO b) -> (a -> IO b) -> IO b
coreRun (MkCore act) err ok
    = either err ok !act

export
coreFail : Error -> Core a
coreFail e = MkCore (pure (Left e))

export
wrapError : (Error -> Error) -> Core a -> Core a
wrapError fe (MkCore prog) = MkCore $ mapFst fe <$> prog

-- This would be better if we restrict it to a limited set of IO operations
export
%inline
coreLift : IO a -> Core a
coreLift op = MkCore (do op' <- op
                         pure (Right op'))

{- Monad, Applicative, Traversable are specialised by hand for Core.
In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't
specialise interfaces under 'case' expressions, and this has a significant
impact on both compile time and run time.

Of course it would be a good idea to fix this in Idris, but it's not an urgent
thing on the road to self hosting, and we can make sure this isn't a problem
in the next version (i.e., in this project...)! -}

-- Functor (specialised)
export %inline
map : (a -> b) -> Core a -> Core b
map f (MkCore a) = MkCore (map (map f) a)

export %inline
(<$>) : (a -> b) -> Core a -> Core b
(<$>) f (MkCore a) = MkCore (map (map f) a)

export %inline
(<$) : b -> Core a -> Core b
(<$) = (<$>) . const

export %inline
ignore : Core a -> Core ()
ignore = map (\ _ => ())

-- This would be better if we restrict it to a limited set of IO operations
export
%inline
coreLift_ : IO a -> Core ()
coreLift_ op = ignore (coreLift op)

-- Monad (specialised)
export %inline
(>>=) : Core a -> (a -> Core b) -> Core b
(>>=) (MkCore act) f
    = MkCore (act >>=
                   \case
                     Left err => pure $ Left err
                     Right val => runCore $ f val)

export %inline
(>>) : Core () -> Core a -> Core a
ma >> mb = ma >>= const mb

-- Flipped bind
infixr 1 =<<
export %inline
(=<<) : (a -> Core b) -> Core a -> Core b
(=<<) = flip (>>=)

-- Kleisli compose
infixr 1 >=>
export %inline
(>=>) : (a -> Core b) -> (b -> Core c) -> (a -> Core c)
f >=> g = (g =<<) . f

-- Flipped kleisli compose
infixr 1 <=<
export %inline
(<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
(<=<) = flip (>=>)

-- Applicative (specialised)
export %inline
pure : a -> Core a
pure x = MkCore (pure (pure x))

export
(<*>) : Core (a -> b) -> Core a -> Core b
(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]

export
(*>) : Core a -> Core b -> Core b
(*>) (MkCore a) (MkCore b) = MkCore [| a *> b |]

export
(<*) : Core a -> Core b -> Core a
(<*) (MkCore a) (MkCore b) = MkCore [| a <* b |]

export %inline
when : Bool -> Lazy (Core ()) -> Core ()
when True f = f
when False f = pure ()

export %inline
unless : Bool -> Lazy (Core ()) -> Core ()
unless = when . not

export
iwhen : (b : Bool) -> Lazy (Core a) -> Core (IMaybe b a)
iwhen True f = Just <$> f
iwhen False _ = pure Nothing

export
iunless : (b : Bool) -> Lazy (Core a) -> Core (IMaybe (not b) a)
iunless b f = iwhen (not b) f

export %inline
whenJust : Maybe a -> (a -> Core ()) -> Core ()
whenJust (Just a) k = k a
whenJust Nothing k = pure ()

export
iwhenJust : IMaybe b a -> (a -> Core ()) -> Core ()
iwhenJust (Just a) k = k a
iwhenJust Nothing k = pure ()

-- Control.Catchable in Idris 1, just copied here (but maybe no need for
-- it since we'll only have the one instance for Core Error...)
public export
interface Catchable m t | m where
    throw : {0 a : Type} -> t -> m a
    catch : m a -> (t -> m a) -> m a

    breakpoint : m a -> m (Either t a)

export
Catchable Core Error where
  catch (MkCore prog) h
      = MkCore ( do p' <- prog
                    case p' of
                         Left e => let MkCore he = h e in he
                         Right val => pure (Right val))
  breakpoint (MkCore prog) = MkCore (pure <$> prog)
  throw = coreFail

-- Prelude.Monad.foldlM hand specialised for Core
export
foldlC : Foldable t => (a -> b -> Core a) -> a -> t b -> Core a
foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)

-- Traversable (specialised)
traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
traverse' f [] acc = pure (reverse acc)
traverse' f (x :: xs) acc
    = traverse' f xs (!(f x) :: acc)

%inline
export
traverse : (a -> Core b) -> List a -> Core (List b)
traverse f xs = traverse' f xs []

%inline
export
for : List a -> (a -> Core b) -> Core (List b)
for = flip traverse

export
traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b)
traverseList1 f xxs
    = let x = head xxs
          xs = tail xxs in
          [| f x ::: traverse f xs |]

export
traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
traverseVect f [] = pure []
traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]

%inline
export
traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
traverseOpt f Nothing = pure Nothing
traverseOpt f (Just x) = map Just (f x)

export
traversePair : (a -> Core b) -> (w, a) -> Core (w, b)
traversePair f (w, a) = (w,) <$> f a

export
traverse_ : (a -> Core b) -> List a -> Core ()
traverse_ f [] = pure ()
traverse_ f (x :: xs)
    = Core.do ignore (f x)
              traverse_ f xs
%inline
export
for_ : List a -> (a -> Core ()) -> Core ()
for_ = flip traverse_

%inline
export
sequence : List (Core a) -> Core (List a)
sequence (x :: xs)
   = do
        x' <- x
        xs' <- sequence xs
        pure (x' :: xs')
sequence [] = pure []

export
traverseList1_ : (a -> Core b) -> List1 a -> Core ()
traverseList1_ f xxs
    = do let x = head xxs
         let xs = tail xxs
         ignore (f x)
         traverse_ f xs

namespace PiInfo
  export
  traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b)
  traverse f Explicit = pure Explicit
  traverse f Implicit = pure Implicit
  traverse f AutoImplicit = pure AutoImplicit
  traverse f (DefImplicit t) = pure (DefImplicit !(f t))

namespace Binder
  export
  traverse : (a -> Core b) -> Binder a -> Core (Binder b)
  traverse f (Lam fc c p ty) = pure $ Lam fc c !(traverse f p) !(f ty)
  traverse f (Let fc c val ty) = pure $ Let fc c !(f val) !(f ty)
  traverse f (Pi fc c p ty) = pure $ Pi fc c !(traverse f p) !(f ty)
  traverse f (PVar fc c p ty) = pure $ PVar fc c !(traverse f p) !(f ty)
  traverse f (PLet fc c val ty) = pure $ PLet fc c !(f val) !(f ty)
  traverse f (PVTy fc c ty) = pure $ PVTy fc c !(f ty)

export
mapTermM : ({vars : _} -> Term vars -> Core (Term vars)) ->
           ({vars : _} -> Term vars -> Core (Term vars))
mapTermM f = goTerm where

    goTerm : {vars : _} -> Term vars -> Core (Term vars)
    goTerm tm@(Local _ _ _ _) = f tm
    goTerm tm@(Ref _ _ _) = f tm
    goTerm (Meta fc n i args) = f =<< Meta fc n i <$> traverse goTerm args
    goTerm (Bind fc x bd sc) = f =<< Bind fc x <$> traverse goTerm bd <*> goTerm sc
    goTerm (App fc fn arg) = f =<< App fc <$> goTerm fn <*> goTerm arg
    goTerm (As fc u as pat) = f =<< As fc u <$> goTerm as <*> goTerm pat
    goTerm (TDelayed fc la d) = f =<< TDelayed fc la <$> goTerm d
    goTerm (TDelay fc la ty arg) = f =<< TDelay fc la <$> goTerm ty <*> goTerm arg
    goTerm (TForce fc la t) = f =<< TForce fc la <$> goTerm t
    goTerm tm@(PrimVal _ _) = f tm
    goTerm tm@(Erased _ _) = f tm
    goTerm tm@(TType _) = f tm

export
anyM : (a -> Core Bool) -> List a -> Core Bool
anyM f [] = pure False
anyM f (x :: xs)
    = if !(f x)
         then pure True
         else anyM f xs

export
allM : (a -> Core Bool) -> List a -> Core Bool
allM f [] = pure True
allM f (x :: xs)
    = if !(f x)
         then allM f xs
         else pure False

export
filterM : (a -> Core Bool) -> List a -> Core (List a)
filterM p [] = pure []
filterM p (x :: xs)
    = if !(p x)
         then do xs' <- filterM p xs
                 pure (x :: xs')
         else filterM p xs

export
newRef : (x : label) -> t -> Core (Ref x t)
newRef x val
    = do ref <- coreLift (newIORef val)
         pure (MkRef ref)

export %inline
get : (x : label) -> {auto ref : Ref x a} -> Core a
get x {ref = MkRef io} = coreLift (readIORef io)

export %inline
put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
put x {ref = MkRef io} val = coreLift (writeIORef io val)

export %inline
update : (x : label) -> {auto ref : Ref x a} -> (a -> a) -> Core ()
update x f
  = do v <- get x
       put x (f v)

export
wrapRef : (x : label) -> {auto ref : Ref x a} ->
          (a -> Core ()) ->
          Core b ->
          Core b
wrapRef x onClose op
  = do v <- get x
       o <- catch op $ \err =>
              do onClose v
                 put x v
                 throw err
       onClose v
       put x v
       pure o

export
cond : List (Lazy Bool, Lazy a) -> a -> a
cond [] def = def
cond ((x, y) :: xs) def = if x then y else cond xs def

export
condC : List (Core Bool, Core a) -> Core a -> Core a
condC [] def = def
condC ((x, y) :: xs) def
    = if !x then y else condC xs def

export
writeFile : (fname : String) -> (content : String) -> Core ()
writeFile fname content =
  coreLift (writeFile fname content) >>= \case
    Right () => pure ()
    Left err => throw $ FileErr fname err

export
readFile : (fname : String) -> Core String
readFile fname =
  coreLift (readFile fname) >>= \case
    Right content => pure content
    Left err => throw $ FileErr fname err


text:
module Server.Diagnostics

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.FC
import Data.OneOf
import Data.String
import Idris.Pretty
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Parser.Support
import Server.Configuration
import Server.Log
import Server.Utils
import System.File
import System.Path

keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate (Syntax SynKeyword)

buildDiagnostic : Maybe FC -> Doc IdrisAnn -> Maybe (List DiagnosticRelatedInformation) -> Diagnostic
buildDiagnostic loc error related =
  MkDiagnostic
    { range = cast $ fromMaybe replFC loc
    , severity = Just Error
    , code = Nothing
    , codeDescription = Nothing
    , source = Just "idris2"
    , message = renderString $ unAnnotateS $ layoutUnbounded error
    , tags = Nothing
    , relatedInformation = related
    , data_ = Nothing
    }

buildRelatedInformation : URI -> FC -> String -> DiagnosticRelatedInformation
buildRelatedInformation uri fc msg = MkDiagnosticRelatedInformation (MkLocation uri (cast fc)) msg

||| Computes a list of `DiagnosticRelatedInformation` from a compiler error.
|||
||| @uri The URI of the source file.
||| @err The compiler error.
getRelatedErrors : (uri : URI) -> (err : Error) -> List DiagnosticRelatedInformation
getRelatedErrors uri (Fatal err) = getRelatedErrors uri err
getRelatedErrors uri (CantConvert fc _ l r) =
  [ buildRelatedInformation uri (getLoc l) "Mismatched type"
  , buildRelatedInformation uri (getLoc r) "Mismatched type"
  ]
getRelatedErrors uri (CantSolveEq fc _ l r) =
  [ buildRelatedInformation uri (getLoc l) "Can't solve constraint"
  , buildRelatedInformation uri (getLoc r) "Can't solve constraint type"
  ]
getRelatedErrors uri (PatternVariableUnifies fc _ n tm) =
  [ buildRelatedInformation uri (getLoc tm) ("Unifies with pattern variable " ++ show n) ]
getRelatedErrors uri (CyclicMeta fc _ _ _) = []
getRelatedErrors uri (WhenUnifying fc _ x y _) =
  [ buildRelatedInformation uri (getLoc x) "Error while unification"
  , buildRelatedInformation uri (getLoc y) "Error while unification"
  ]
getRelatedErrors uri (ValidCase _ _ (Right err)) = getRelatedErrors uri err
getRelatedErrors uri (InType _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InCon _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InLHS _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InRHS _ _ err) = getRelatedErrors uri err
getRelatedErrors _ _ = []

pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn
pShowMN (Local _ _ _ p) env acc =
  case dropAllNS (nameAt p) of
       MN _ _ => acc <++> parens ("implicitly bound at" <++> pretty (getBinderLoc p env))
       _      => acc
pShowMN _ _ acc = acc

pshow : {vars : _}
     -> Ref Ctxt Defs
     => Ref Syn SyntaxInfo
     => Env Term vars
     -> Term vars
     -> Core (Doc IdrisAnn)
pshow env tm
    = do defs <- get Ctxt
         ntm <- normaliseHoles defs env tm
         itm <- resugar env ntm
         pure (pShowMN ntm env $ prettyTerm itm)

pshowNoNorm : {vars : _}
           -> Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Env Term vars
           -> Term vars
           -> Core (Doc IdrisAnn)
pshowNoNorm env tm
    = do defs <- get Ctxt
         itm <- resugar env tm
         pure (pShowMN tm env $ prettyTerm itm)

ploc : FC -> Doc IdrisAnn
ploc fc = annotate FileCtxt (pretty fc)

pwarning : Ref Ctxt Defs
        => Ref Syn SyntaxInfo
        => Ref ROpts REPLOpts
        => Warning
        -> Core (Doc IdrisAnn)
pwarning (UnreachableClause fc env tm) =
  pure $ errorDesc (reflow "Unreachable clause:" <++> code !(pshow env tm))
pwarning (ShadowingGlobalDefs _ ns) =
  pure $ vcat $
    reflow "We are about to implicitly bind the following lowercase names."
      :: reflow "You may be unintentionally shadowing the associated global definitions:"
      :: map (\ (n, ns) => indent 2 $ hsep $ pretty n
                             :: reflow "is shadowing"
                             :: punctuate comma (map pretty (forget ns)))
             (forget ns)
pwarning (Deprecated s) = pure $ pretty "Deprecation warning:" <++> pretty s
pwarning (GenericWarn s) = pure $ pretty s

perror : Ref Ctxt Defs
      => Ref Syn SyntaxInfo
      => Ref ROpts REPLOpts
      => Error
      -> Core (Doc IdrisAnn)
perror (Fatal err) = perror err
perror (CantConvert fc env l r) =
  pure $ errorDesc (hsep [ reflow "Mismatch between" <+> colon
                         , code !(pshow env l)
                         , "and"
                         , code !(pshow env r) <+> dot
                         ])
perror (CantSolveEq fc env l r) =
  pure $ errorDesc (hsep [ reflow "Can't solve constraint between" <+> colon
                         , code !(pshow env l)
                         , "and"
                         , code !(pshow env r) <+> dot
                         ])
perror (PatternVariableUnifies fc env n tm) =
  pure $ errorDesc (hsep [ reflow "Pattern variable"
                         , code (prettyVar n)
                         , reflow "unifies with" <+> colon
                         , code !(pshow env tm) <+> dot
                         ]) <+> line <+> reflow "Suggestion: Use the same name for both pattern variables, since they unify."
  where
    prettyVar : Name -> Doc IdrisAnn
    prettyVar (PV n _) = prettyVar n
    prettyVar n = pretty n
perror (CyclicMeta fc env n tm)
    = pure $ errorDesc (reflow "Cycle detected in solution of metavariable" <++> meta (pretty !(prettyName n)) <++> equals
        <++> code !(pshow env tm))
perror (WhenUnifying _ env x y err)
    = pure $ errorDesc (reflow "When unifying" <++> code !(pshow env x) <++> "and"
        <++> code !(pshow env y)) <+> dot <+> line <+> !(perror err)
perror (ValidCase fc env (Left tm))
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a valid impossible case.")
perror (ValidCase _ env (Right err))
    = pure $ errorDesc (reflow "Impossible pattern gives an error" <+> colon) <+> line <+> !(perror err)
perror (UndefinedName fc x)
    = pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot)
perror (InvisibleName fc n (Just ns))
     = pure $ errorDesc ("Name" <++> code (pretty n) <++> reflow "is inaccessible since"
         <++> code (pretty ns) <++> reflow "is not explicitly imported.")
         <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
         <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
perror (InvisibleName fc x Nothing)
    = pure $ errorDesc ("Name" <++> code (pretty x) <++> reflow "is private.")
        <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
        <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
perror (BadTypeConType fc n)
    = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be" <++> code "Type" <+> dot)
perror (BadDataConType fc n fam)
    = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be in"
        <++> code (pretty !(toFullNames fam)))
perror (NotCovering fc n IsCovering)
    = pure $ errorDesc (reflow "Internal error" <++> parens (reflow "Coverage of" <++> code (pretty n)))
perror (NotCovering fc n (MissingCases cs))
    = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not covering.")
        <+> line <+> reflow "Missing cases" <+> colon <+> line
        <+> indent 4 (vsep !(traverse (pshow []) cs)) <+> line
perror (NotCovering fc n (NonCoveringCall ns))
    = pure $ errorDesc (pretty !(prettyName n) <++> reflow "is not covering.")
        <+> line <+> reflow "Calls non covering function" <+>
        case ns of
             [fn] => space <+> pretty fn
             _ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
perror (NotTotal fc n r)
    = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not total," <++> pretty r)
perror (LinearUsed fc count n)
    = pure $ errorDesc (reflow "There are" <++> pretty count <++> reflow "uses of linear name"
        <++> code (pretty (sugarName n)) <+> dot)
        <+> line <+> reflow "Suggestion: linearly bounded variables must be used exactly once."
perror (LinearMisuse fc n exp ctx)
    = if isErased exp
         then pure $ errorDesc (code (pretty n) <++> reflow "is not accessible in this context.")
         else pure $ errorDesc (reflow "Trying to use" <++> prettyRig exp <++> "name"
                <++> code (pretty (sugarName n)) <++> "in" <++> prettyRel ctx <++> "context.")
  where
    prettyRig : RigCount -> Doc ann
    prettyRig = elimSemi "irrelevant"
                         "linear"
                         (const "unrestricted")

    prettyRel : RigCount -> Doc ann
    prettyRel = elimSemi "irrelevant"
                         "relevant"
                         (const "non-linear")
perror (BorrowPartial fc env tm arg)
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows argument" <++> code !(pshow env arg)
        <++> reflow "so must be fully applied.")
perror (BorrowPartialType fc env tm)
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows, so must return a concrete type.")
perror (AmbiguousName fc ns)
    = pure $ errorDesc (reflow "Ambiguous name" <++> code (pretty ns))
perror (AmbiguousElab fc env ts)
    = do pp <- getPPrint
         setPPrint (record { fullNamespace = True } pp)
         let res = vsep [ errorDesc (reflow "Ambiguous elaboration. Possible results" <+> colon)
                        , indent 4 (vsep !(traverse (pshow env) ts))
                        ]
         setPPrint pp
         pure res
perror (AmbiguousSearch fc env tgt ts)
    = pure $ vsep [ errorDesc (reflow "Multiple solutions found in search of" <+> colon)
                  , indent 4 !(pshowNoNorm env tgt)
                  , reflow "Possible correct results" <+> colon
                  , indent 4 (vsep !(traverse (pshowNoNorm env) ts))
                  ]
perror (AmbiguityTooDeep fc n ns)
    = pure $ errorDesc (reflow "Maximum ambiguity depth exceeded in" <++> code (pretty !(getFullName n))
        <+> colon) <+> line <+> concatWith (surround (pretty " --> ")) (pretty <$> !(traverse getFullName ns))
        <+> line <+> reflow "Suggestion: the default ambiguity depth limit is 3, the" <++> code "%ambiguity_depth"
        <++> reflow "pragma can be used to extend this limit, but beware compilation times can be severely impacted."
perror (AllFailed ts)
    = case allUndefined ts of
           Just e => perror e
           _ => pure $ errorDesc (reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon) <+> line
                  <+> vsep !(traverse pAlterror ts)
  where
    pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn)
    pAlterror (Just n, err)
       = pure $ "If" <++> code (pretty !(aliasName !(getFullName n))) <+> colon <++> !(perror err)
    pAlterror (Nothing, err)
       = pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perror err)

    allUndefined : List (Maybe Name, Error) -> Maybe Error
    allUndefined [] = Nothing
    allUndefined [(_, UndefinedName loc e)] = Just (UndefinedName loc e)
    allUndefined ((_, UndefinedName _ e) :: es) = allUndefined es
    allUndefined _ = Nothing
perror (RecordTypeNeeded fc _)
    = pure $ errorDesc (reflow "Can't infer type for this record update.")
perror (NotRecordField fc fld Nothing)
    = pure $ errorDesc (code (pretty fld) <++> reflow "is not part of a record type.")
perror (NotRecordField fc fld (Just ty))
    = pure $ errorDesc (reflow "Record type" <++> code (pretty !(getFullName ty)) <++> reflow "has no field"
        <++> code (pretty fld) <+> dot)
perror (NotRecordType fc ty)
    = pure $ errorDesc (code (pretty !(getFullName ty)) <++> reflow "is not a record type.")
perror (IncompatibleFieldUpdate fc flds)
    = pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds)
             <++> reflow "not compatible with other updates at" <+> colon <+> line <+> ploc fc
perror (InvalidArgs fc env [n] tm)
    = pure $ errorDesc (code (pretty n) <++> reflow "is not a valid argument in" <++> !(pshow env tm)
        <+> dot)
perror (InvalidArgs fc env ns tm)
    = pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns)
        <++> reflow "are not valid arguments in" <++> !(pshow env tm) <+> dot)
perror (TryWithImplicits fc env imps)
    = pure $ errorDesc (reflow "Need to bind implicits"
        <++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) <+> dot)
  where
    tshow : {vars : _} ->
            Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn)
    tshow env (n, ty) = pure $ pretty n <++> colon <++> code !(pshow env ty)
perror (BadUnboundImplicit fc env n ty)
    = pure $ errorDesc (reflow "Can't bind name" <++> code (pretty (nameRoot n)) <++> reflow "with type" <++> code !(pshow env ty)
        <+> colon) <+> line <+> reflow "Suggestion: try an explicit bind."
perror (CantSolveGoal fc env g)
    = let (_ ** (env', g')) = dropEnv env g in
          pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g') <+> dot)
  where
    -- For display, we don't want to see the full top level type; just the
    -- return type
    dropEnv : {vars : _} ->
              Env Term vars -> Term vars ->
              (ns ** (Env Term ns, Term ns))
    dropEnv env (Bind _ n b@(Pi _ _ _ _) sc) = dropEnv (b :: env) sc
    dropEnv env (Bind _ n b@(Let _ _ _ _) sc) = dropEnv (b :: env) sc
    dropEnv env tm = (_ ** (env, tm))

perror (DeterminingArg fc n i env g)
    = pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env g) <+> line
        <+> reflow "since I can't infer a value for argument" <++> code (pretty n) <+> dot)
perror (UnsolvedHoles hs)
    = pure $ errorDesc (reflow "Unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
  where
    prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn)
    prettyHoles [] = pure emptyDoc
    prettyHoles ((fc, n) :: hs)
        = pure $ meta (pretty n) <++> reflow "introduced at:" <++> ploc fc <+> !(prettyHoles hs)
perror (CantInferArgType fc env n h ty)
    = pure $ errorDesc (reflow "Can't infer type for argument" <++> code (pretty n)) <+> line
        <+> "Got" <++> code !(pshow env ty) <++> reflow "with hole" <++> meta (pretty h) <+> dot
perror (SolvedNamedHole fc env h tm)
    = pure $ errorDesc (reflow "Named hole" <++> meta (pretty h) <++> reflow "has been solved by unification.") <+> line
        <+> "Result" <+> colon <++> code !(pshow env tm)
perror (VisibilityError fc vx x vy y)
    = pure $ errorDesc (keyword (pretty vx) <++> code (pretty (sugarName !(toFullNames x)))
        <++> reflow "cannot refer to" <++> keyword (pretty vy) <++> code (pretty (sugarName !(toFullNames y))))
perror (NonLinearPattern fc n)
    = pure $ errorDesc (reflow "Non linear pattern" <++> code (pretty (sugarName n)) <+> dot)
perror (BadPattern fc n)
    = pure $ errorDesc (reflow "Pattern not allowed here" <+> colon <++> code (pretty n) <+> dot)
perror (NoDeclaration fc n)
    = pure $ errorDesc (reflow "No type declaration for" <++> code (pretty n) <+> dot)
perror (AlreadyDefined fc n)
    = pure $ errorDesc (code (pretty n) <++> reflow "is already defined.")
perror (NotFunctionType fc env tm)
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a function type.")
perror (RewriteNoChange fc env rule ty)
    = pure $ errorDesc (reflow "Rewriting by" <++> code !(pshow env rule)
        <++> reflow "did not change type" <++> code !(pshow env ty) <+> dot)
perror (NotRewriteRule fc env rule)
    = pure $ errorDesc (code !(pshow env rule) <++> reflow "is not a rewrite rule type.")
perror (CaseCompile fc n DifferingArgNumbers)
    = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "have differing numbers of arguments.")
perror (CaseCompile fc n DifferingTypes)
    = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "require matching on different types.")
perror (CaseCompile fc n UnknownType)
    = pure $ errorDesc (reflow "Can't infer type to match in" <++> code (pretty !(prettyName n)) <+> dot)
perror (CaseCompile fc n (NotFullyApplied cn))
    = pure $ errorDesc (pretty "Constructor" <++> code (pretty !(toFullNames cn)) <++> reflow "is not fully applied.")
perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
    = pure $ errorDesc (reflow "Attempt to match on erased argument" <++> code !(pshow env tm) <++> pretty "in"
        <++> code (pretty !(prettyName n)) <+> dot)
perror (BadDotPattern fc env reason x y)
    = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env x)
        <++> parens (pretty reason) <+> dot)
perror (MatchTooSpecific fc env tm)
    = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm)
        <++> reflow "as it has a polymorphic type.")
perror (BadImplicit fc str)
    = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot)
        <+> line <+> reflow "Suggestion: try making it a bound implicit."
perror (BadRunElab fc env script desc)
    = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <++> parens (pretty desc) <+> dot)
perror (GenericMsg fc str) = pure $ pretty str
perror (TTCError msg)
    = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> pretty (show msg))
        <++> parens (pretty "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files")
perror (FileErr fname err)
    = pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err)
perror (CantFindPackage fname)
    = pure $ errorDesc ("Can't find package" <++> pretty fname)
perror (LitFail _)
    = pure $ errorDesc (reflow "Can't parse literate.")
perror (LexFail _ msg)
    = pure $ errorDesc (pretty msg)
perror (ParseFail msg)
    = pure $ errorDesc (pretty msg)
perror (ModuleNotFound fc ns)
    = pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty ns) <++> reflow "not found")
perror (CyclicImports ns)
    = pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str
perror (NoForeignCC fc specs) = do
    let cgs = fst <$> availableCGs (options !(get Ctxt))
    let res = vsep [ errorDesc (reflow ("The given specifier '" ++ show specs ++ "' was not accepted by any backend. Available backends") <+> colon)
                   , indent 2 (concatWith (\ x, y => x <+> ", " <+> y) (map reflow cgs))
                   , reflow "Some backends have additional specifier rules, refer to their documentation."
                   ]
    pure res
perror (BadMultiline _ str)
    = pure $ errorDesc (reflow "Invalid multiline string" <++> colon <++> line <++> pretty str)

perror (InType fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InCon fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing constructor" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InLHS fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing left hand side of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InRHS fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing right hand side of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (MaybeMisspelling err ns) = pure $ !(perror err) <++> case ns of
  (n ::: []) => reflow "Did you mean:" <++> pretty n <+> "?"
  _ => let (xs, x) = unsnoc ns in
       reflow "Did you mean any of:"
       <++> concatWith (surround (comma <+> space)) (map pretty xs)
       <+> comma <++> reflow "or" <++> pretty x <+> "?"
perror (WarningAsError warn) = pwarning warn
perror (Timeout str) = pure $ errorDesc (reflow "Timeout in" <++> pretty str)

||| Computes a LSP `Diagnostic` from a compiler error.
|||
||| @caps The client capabilities related to diagnostics
||| @uri The URI of the source file.
||| @err The compiler error.
export
toDiagnostic : Ref Ctxt Defs
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => (caps : Maybe PublishDiagnosticsClientCapabilities)
            -> (uri : URI)
            -> (error : Error)
            -> Core Diagnostic
toDiagnostic caps uri err = do
  defs <- get Ctxt
  error <- perror err
  let loc = getErrorLoc err
  let wdir = defs.options.dirs.working_dir
  p <- maybe (pure uri.path) (pure . (wdir </>) <=< nsToSource replFC)
         ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc)
  if uri.path == p
     then do let related = (flip toMaybe (getRelatedErrors uri err) <=< relatedInformation) =<< caps
             pure $ buildDiagnostic loc error related
     else pure $ buildDiagnostic (toStart <$> loc) ("In" <++> pretty p <+> colon <++> error) Nothing


text:
||| Note: The difference to a 'strict' RWST implementation is
||| that accumulation of values does not happen in the
||| Applicative and Monad instances but when invoking `Writer`-specific
||| functions like `writer` or `listen`.
module Control.Monad.RWS.CPS

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

%default total

||| A monad transformer adding reading an environment of type `r`,
||| collecting an output of type `w` and updating a state of type `s`
||| to an inner monad `m`.
public export
record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
  constructor MkRWST
  unRWST : r -> s -> w -> m (a, s, w)

||| Unwrap an RWST computation as a function. (The inverse of `rwsT`.)
public export %inline
runRWST : Monoid w => RWST r w s m a -> r -> s -> m (a, s, w)
runRWST m r s = unRWST m r s neutral

||| Construct an RWST computation from a function. (The inverse of `runRWST`.)
public export %inline
rwsT : (Functor m, Semigroup w) => (r -> s -> m (a, s, w)) -> RWST r w s m a
rwsT f = MkRWST $ \r,s,w => (\(a,s',w') => (a,s',w <+> w')) <$> f r s

||| Evaluate a computation with the given initial state and environment,
||| returning the final value and output, discarding the final state.
public export %inline
evalRWST : (Functor m, Monoid w) => RWST r w s m a -> r -> s -> m (a,w)
evalRWST m r s = (\(a,_,w) => (a,w)) <$> runRWST m r s

||| Evaluate a computation with the given initial state and environment,
||| returning the final state and output, discarding the final value.
public export %inline
execRWST : (Functor m, Monoid w) => RWST r w s m a -> r -> s -> m (s,w)
execRWST m r s = (\(_,s',w) => (s',w)) <$> runRWST m r s

||| Map the inner computation using the given function.
public export %inline
mapRWST : (Functor n, Monoid w, Semigroup w')
        => (m (a, s, w) -> n (b, s, w')) -> RWST r w s m a -> RWST r w' s n b
mapRWST f m = MkRWST $ \r,s,w =>
                (\(a,s',w') => (a,s',w <+> w')) <$> f (runRWST m r s)

||| `withRWST f m` executes action `m` with an initial environment
||| and state modified by applying `f`.
public export %inline
withRWST : (r' -> s -> (r, s)) -> RWST r w s m a -> RWST r' w s m a
withRWST f m = MkRWST $ \r,s => uncurry (unRWST m) (f r s)

--------------------------------------------------------------------------------
--          RWS Functions
--------------------------------------------------------------------------------

||| A monad containing an environment of type `r`, output of type `w`
||| and an updatable state of type `s`.
public export
RWS : (r : Type) -> (w : Type) -> (s : Type) -> (a : Type) -> Type
RWS r w s = RWST r w s Identity

||| Unwrap an RWS computation as a function. (The inverse of `rws`.)
public export %inline
runRWS : Monoid w => RWS r w s a -> r -> s -> (a, s, w)
runRWS m r s = runIdentity (runRWST m r s)

||| Construct an RWS computation from a function. (The inverse of `runRWS`.)
public export %inline
rws : Semigroup w => (r -> s -> (a, s, w)) -> RWS r w s a
rws f = MkRWST $ \r,s,w => let (a, s', w') = f r s
                           in Id (a, s', w <+> w')

||| Evaluate a computation with the given initial state and environment,
||| returning the final value and output, discarding the final state.
public export %inline
evalRWS : Monoid w => RWS r w s a -> r -> s -> (a,w)
evalRWS m r s = let (a,_,w) = runRWS m r s
                 in (a,w)

||| Evaluate a computation with the given initial state and environment,
||| returning the final state and output, discarding the final value.
public export %inline
execRWS : Monoid w => RWS r w s a -> r -> s -> (s,w)
execRWS m r s = let (_,s1,w) = runRWS m r s
                 in (s1,w)

||| Map the return value, final state and output of a computation using
||| the given function.
public export %inline
mapRWS :  (Monoid w, Semigroup w')
       => ((a, s, w) -> (b, s, w')) -> RWS r w s a -> RWS r w' s b
mapRWS f = mapRWST $ \(Id p) => Id (f p)

||| `withRWS f m` executes action `m` with an initial environment
||| and state modified by applying `f`.
public export %inline
withRWS : (r' -> s -> (r, s)) -> RWS r w s a -> RWS r' w s a
withRWS = withRWST

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
Functor m => Functor (RWST r w s m) where
  map f m = MkRWST $ \r,s,w => (\(a,s',w') => (f a,s',w')) <$> unRWST m r s w

public export %inline
Monad m => Applicative (RWST r w s m) where
  pure a = MkRWST $ \_,s,w => pure (a,s,w)
  MkRWST mf <*> MkRWST mx =
    MkRWST $ \r,s,w => do (f,s1,w1) <- mf r s w
                          (a,s2,w2) <- mx r s1 w1
                          pure (f a,s2,w2)

public export %inline
(Monad m, Alternative m) => Alternative (RWST r w s m) where
  empty = MkRWST $ \_,_,_ => empty
  MkRWST m <|> mn = MkRWST $ \r,s,w => m r s w <|> unRWST mn r s w

public export %inline
Monad m => Monad (RWST r w s m) where
  m >>= k = MkRWST $ \r,s,w => do (a,s1,w1) <- unRWST m r s w
                                  unRWST (k a) r s1 w1

public export %inline
MonadTrans (RWST r w s) where
  lift m = MkRWST $ \_,s,w => map (\a => (a,s,w)) m

public export %inline
HasIO m => HasIO (RWST r w s m) where
  liftIO = lift . liftIO