text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Builder

import public Text.PrettyPrint.Leijen
import        Options.Applicative.Types
import        Control.Monad.Trans
import        Control.Lens

public export
optRdr : Lens' (Option x a) (OptReader x a)
optRdr (Mor f) = Mor (\a => case a of
      (Opt props rdr) => (Opt props) <$> f rdr
    )

public export
optProps : Lens' (Option x a) (OptProperties)
optProps (Mor f) = Mor (\a => case a of
      (Opt props rdr) => (flip Opt rdr) <$> f props
    )

public export
interface HasMeta d where
  meta : { f : Type -> Type } -> Functor f => LensLike' f d String

public export
HasMeta (OptReader OptionParams a) where
  meta (Mor f) = Mor (\a => case a of
          (OptionReader n p m) => (OptionReader n p) <$> f m
        )

public export
HasMeta (OptReader ArgParams a) where
  meta (Mor f) = Mor (\a => case a of
          (ArgReader p m) => (ArgReader p) <$> f m
        )

public export
HasMeta (OptReader CmdParams a) where
  meta (Mor f) = Mor (\a => case a of
          (CmdReader ps m) => (CmdReader ps) <$> f m
        )

public export
HasMeta (OptReader x a) => HasMeta (Option x a) where
  meta = optRdr . meta

public export
interface HasName d where
  names : { f : Type -> Type } -> Functor f => LensLike' f d (List OptName)

public export
HasName (OptReader OptionParams a) where
  names (Mor f) = Mor (\a => case a of
         (OptionReader n p m) => (\n' => OptionReader n' p m) <$> (f n)
        )

public export
HasName (OptReader FlagParams a) where
  names (Mor f) = Mor (\a => case a of
         (FlagReader n d) => (\n' => FlagReader n' d) <$> f n
        )

public export
HasName (OptReader x a) => HasName (Option x a) where
  names = optRdr . names

public export
short : HasName d => Char -> d -> d
short c = over names (\ns => ShortName c :: ns)

public export
long : HasName d => String -> d -> d
long c = over names (\ns => LongName c :: ns)

public export
interface HasSubCommands (0 d : Type ) a where
  cmds : { f : Type -> Type } -> Functor f => LensLike' f d (List (String, (Parser a)))

public export
HasSubCommands (OptReader CmdParams a) a where
  cmds (Mor f) = Mor (\a => case a of
          (CmdReader ps m) => flip CmdReader m <$> f ps
        )

public export
HasSubCommands (Option CmdParams a) a where
  cmds = optRdr . cmds

public export
cmd : HasSubCommands d a => String -> Parser a -> d -> d
cmd n p = over cmds (\ns => (n,p) :: ns)

public export
interface HasHelp d where
  help : { f : Type -> Type } -> Functor f => LensLike' f d Doc

public export
HasHelp OptProperties where
  help (Mor f) = Mor (\a => case a of
         (MkOptProperties vis hdoc) => MkOptProperties vis <$> f hdoc
       )

public export
HasHelp (Option x a) where
  help = optProps . help

public export
interface HasVisibility d where
  visibility : { f : Type -> Type } -> Functor f => LensLike' f d Visibility

public export
HasVisibility OptProperties where
  visibility (Mor f) = Mor (\a => case a of
         (MkOptProperties vis hdoc) => (\vis' => MkOptProperties vis' hdoc) <$> f vis
        )

public export
HasVisibility (Option x a) where
  visibility = optProps . visibility

public export
hide : HasVisibility d => d -> d
hide d = d |> visibility .~ Hidden

public export
internal : HasVisibility d => d -> d
internal d = d |> visibility .~ Internal

public export
interface HasValue ( 0 d : Type -> Type ) where
  value : { a : Type } -> { b : Type } -> { f : Type -> Type } -> Functor f => LensLike f (d a) (d b) a b

public export
HasValue (OptReader FlagParams) where
  value (Mor f) = Mor (\a => case a of
         (FlagReader n d) => (\d' => FlagReader n d') <$> f d
        )

public export
HasValue (Option FlagParams) where
  value (Mor f) = Mor (\a => case a of
         (Opt props (FlagReader n d)) => (\d' => Opt props $ FlagReader n d') <$> f d
        )

public export
defProps : OptProperties
defProps = MkOptProperties Visible empty

public export
option : (String -> Either ParseError a) -> (Option OptionParams a -> Option OptionParams a) -> Parser a
option rdr f = OptP  (f $ Opt defProps (OptionReader [] rdr "OPT"))

public export
strOption : (Option OptionParams String -> Option OptionParams String) -> Parser String
strOption = option Right

public export
arg : (String -> Either ParseError a) -> (Option ArgParams a -> Option ArgParams a) -> Parser a
arg rdr f = OptP (f $ Opt defProps (ArgReader rdr "ARG"))

public export
strArg : (Option ArgParams String -> Option ArgParams String) -> Parser String
strArg = arg Right

public export
flag : (Option FlagParams Bool -> Option FlagParams a) -> Parser a
flag f = OptP (f $ Opt defProps (FlagReader [] True))

public export
subparser : (Option CmdParams a -> Option CmdParams a) -> Parser a
subparser f = OptP (f $ Opt defProps (CmdReader [] "COMMAND"))

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


text:
fun1 : a -> a
fun1 x = x

{-

allow unclosed comment block at the end of file

{-
fun2 : a -> a
fun2 x = x
-}

-- Before implemneting #2098, this was somehow parsed as a valid source and `fun3` was in scope
--
-- But i don't think that's the supposed behaviour for nested comment blocks?
-- In any case, after the change, `fun3` now is commented out.

fun3 : a -> a
fun3 x = x

ext: idr


text:
data InfIO: Type where
  Do: IO a -> (a -> Inf InfIO) -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever: Fuel
forever = More forever

total
run: Fuel -> InfIO -> IO()
run Dry         y                = putStrLn "Out of fuel"
run (More fuel) (Do action cont) =
  do
    res <- action
    run fuel (cont res)

total
totalRepl : (prompt: String) -> (action: String -> String) -> InfIO
totalRepl prompt action =
  do
    input <- getLine
    putStr ((action input) ++ prompt)
    totalRepl prompt action

partial
main : IO()
main = run forever (totalRepl "\n: " toUpper)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Control.App.Network

import Control.App
import Control.App.Network.Data

data SocketState = Ready | Bound | Listening | Open | Closed

data Socket : SocketState -> Type where
     MkSocket : Int -> Socket s

data NetworkError = Foo

interface Has [Exception NetworkError] e => Network e where
  newSocket : (1 p : (1 s : Socket Ready) -> App e a) -> App e a
  done : (1 s : Socket Closed) -> App e ()

bind : (1 sock : Socket Ready) ->
       (addr : Maybe SocketAddress) -> (port : Port) ->
       Either NetworkError (Socket Bound)

{-
connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode
listen : (sock : Socket) -> IO Int
accept : (sock : Socket) -> IO (Either SocketError (Socket, SocketAddress))
send : (sock : Socket) -> (msg  : String) -> IO (Either SocketError ResultCode)
recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (String, ResultCode))
close : Socket -> IO ()
-}


text:
module Linear

public export
data Usage = Once | Many

public export
data Lin : (Type -> Type) -> Usage -> Type -> Type where
     Pure : (1 x : a) -> Lin m usage a
     Lift : (1 x : m a) -> Lin m Many a
     BindOnce : (1 act : Lin m Once a) ->
                (1 k : (1 x : a) -> Lin m t b) -> Lin m t b
     BindMany : (1 act : Lin m Many a) ->
                (1 k : (x : a) -> Lin m t b) -> Lin m t b

public export
data Unrestricted : Type -> Type where
     MkUn : (x : a) -> Unrestricted a

export
pure : (1 x : a) -> Lin m usage a
pure = Pure

export
lift : (1 x : m a) -> Lin m Many a
lift = Lift

public export
contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
contType m Once q a b = (1 x : a) -> Lin m q b
contType m Many q a b = (x : a) -> Lin m q b

public export
(>>=) : {p : _} ->
        (1 f : Lin m p a) -> (1 k : contType m p q a b) -> Lin m q b
(>>=) {p=Once} = BindOnce
(>>=) {p=Many} = BindMany

export
run : Monad m => Lin m usage t -> m t
run (Pure x) = pure x
run (Lift p) = p
run (BindOnce act k)
    = do act' <- run act
         run (k act')
run (BindMany act k)
    = do act' <- run act
         run (k act')

public export
One : (Type -> Type) -> Type -> Type
One m = Lin m Once

public export
Any : (Type -> Type) -> Type -> Type
Any m = Lin m Many

{-
data DoorState = Closed | Open

data Door : DoorState -> Type where
     MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)

newDoor    : One m (Door Closed)
knock      : (1 d : Door t)      -> One m (Door t)
openDoor   : (1 d : Door Closed) -> One m (Res Bool (\ok => Door (if ok then Open else Closed)))
closeDoor  : (1 d : Door Open)   -> One m (Door Closed)
deleteDoor : (1 d : Door Closed) -> Any m ()

doorProg : Any m ()
doorProg
    = do d <- newDoor
         ok @@ d' <- openDoor d
         d'' <- knock d'
         if ok
            then ?doorOK
            else ?doorBad
            -}


text:
-- ------------------------------------------------------------ [ RoseTree.idr ]
-- Module    : RoseTree.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| Trees with unbounded number of children
module Data.RoseTree

%default total
%access export

||| A RTree.
data RTree : Type -> Type where
  Empty : RTree a
  Node : (value : a) -> (children : List (RTree a)) -> RTree a

contains : Eq a => a -> RTree a -> Bool
contains x Empty       = False
contains x (Node y cs) =
    if x == y
      then True
      else doChildren x cs
  where
    doChildren : Eq a => a -> List (RTree a) -> Bool
    doChildren a Nil     = False
    doChildren a (Empty :: xs)    = doChildren a xs
    doChildren a (Node a' ys::xs) = a == a' || (doChildren a ys || doChildren a xs )

data HasValue : RTree a -> a -> Type where
  DoesHaveValue : HasValue (Node p cs) n

private
noValueEmpty : HasValue (Empty) x -> Void
noValueEmpty DoesHaveValue impossible

||| Insert into a Rose RTree
|||
||| //TODO Make total
partial
insert : Eq a => (value : a) -> (parent : Maybe a) -> (tree : RTree a) -> RTree a
insert x Nothing  (Empty)      = Node x Nil
insert x Nothing  (Node y xs)  = Node y (Node x Nil:: xs)
insert x (Just p) (Empty)      = Node p [Node x Nil]
insert x (Just p) (Node y cs)  =
    if p == y
      then Node y (Node x Nil :: cs)
      else Node y $ map (\y => insert x (Just p) y) cs

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module BoehmBerarducci

%default total

-- NOTE: Issues with scoped implicits:
-- https://github.com/idris-lang/Idris-dev/issues/2346

NatQ : Type
NatQ = {A : Type} -> (A -> A) -> A -> A

unNatQ : {A : Type} -> (A -> A) -> A -> NatQ -> A
unNatQ f a q = q f a

succQ : NatQ -> NatQ
succQ q = \f, a => f (q f a)

zeroQ : NatQ
zeroQ = \f, a => a

fromNatQ : NatQ -> Nat
fromNatQ q = unNatQ S Z q

-- NOTE: Issue #2346 / 1
toNatQ : Nat -> NatQ
toNatQ (S n) = succQ (toNatQ n)
toNatQ Z     = zeroQ

iterated : Nat -> (a -> a) -> a -> a
iterated (S n) f a = f (iterated n f a)
iterated Z f a     = a

test_iterated : (n : Nat) -> iterated n S Z = n
test_iterated (S n) = rewrite test_iterated n in Refl
test_iterated Z     = Refl

-- NOTE: Issue #2346 / 1
-- test_fromNatQ : (n : Nat) -> fromNatQ (iterated n succQ zeroQ) = n
-- test_fromNatQ (S n) = rewrite test_fromNatQ n in Refl
-- test_fromNatQ Z     = Refl

-- TODO: Unknown issue
-- test_toNatQ : (n : Nat) -> toNatQ n = iterated n succQ zeroQ
-- test_toNatQ (S n) = rewrite test_toNatQ n in Refl
-- test_toNatQ Z = Refl

ListQ : Type -> Type
ListQ A = {B : Type} -> (A -> B -> B) -> B -> B

unListQ : {A, B : Type} -> (A -> B -> B) -> B -> ListQ A -> B
unListQ f b q = q f b

consQ : {A : Type} -> A -> ListQ A -> ListQ A
consQ a q = \f, b => f a (q f b)

nilQ : {A : Type} -> ListQ A
nilQ = \f, b => b

fromListQ : {A : Type} -> ListQ A -> List A
fromListQ q = unListQ (::) [] q

-- NOTE: Issue #2346 / 1
toListQ : {A : Type} -> List A -> ListQ A
toListQ (a :: aa) = consQ a (toListQ aa)
toListQ []        = nilQ

max_stars_repo_name: mietek/scott-encoding

max_issues_repo_name: mietek/scott-encoding

max_forks_repo_name: mietek/scott-encoding


text:
module Plugin

import Data.List
import Data.List1
import Data.Ref
import Data.Strings

import System.File
import System

import Language.Reflection

import Libraries.Utils.Hex
import Libraries.Utils.Path

-- A type-checking slowdown happens because of this
-- import vvv
import Core.Core
import Idris.IDEMode.Commands
import Idris.IDEMode.Parser
import Parser.Lexer.Source
import Parser.Support

import Commands
import Foreign

%language ElabReflection

%hide Core.Ref

-- TODO: Move all temporary foreign declaration to vim api module

data Server : Type where
data Client : Type where

public export
data Parameters : Type where
  [noHints] -- Auto search won't be able to construct instances of this type
            -- straight through this constructor anymore
  MkParameters : (sourceDir : String) -> Parameters

namespace Parameters
  public export
  sourceDir : Parameters -> String
  sourceDir (MkParameters srcDir) = srcDir

  public export
  (.sourceDir) : Parameters -> String
  (.sourceDir) = sourceDir

%foreign "s, h => {args={'-p', 'contrib', '-p', 'idris2', '-p', 'network', '--ide-mode-socket', s}, stdio={nil, h, nil}}"
prim__spawnOpts : String -> OpaqueDict -> OpaqueDict

spawnOpts : String
         -> OpaqueDict
         -> Dict [("args", Lua.List [String, String]), ("stdio", Lua.List [OpaqueDict, OpaqueDict, OpaqueDict])]
spawnOpts s h = MkDict $ prim__spawnOpts s h

spawnIdris2 : String -> Int
           -> IO (OpaqueDict, OpaqueDict)
spawnIdris2 host port = do
  stdout <- newPipe
  let opts = spawnOpts (host ++ ":" ++ show port) stdout
  d <- spawn "idris2" opts (\code, signal => nvimCommand $ "echom 'Idris2 process closed with code " ++ show code ++ "'")
  let handle : OpaqueDict = getField d "handle"
  readStart stdout (\msg => nvimCommand $ "echom 'server: " ++ msg ++ "'")
                   (\err => nvimCommand $ "echom 'err: " ++ err ++ "'")
                   (nvimCommand  "echom 'Idris2 stdout closed'")
  pure (handle, stdout)

%foreign "_ => vim.fn.getcurpos()"
getCurPos : PrimIO OpaqueDict

%foreign "pos, _ => vim.fn.setpos('.', pos)"
setCurPos : OpaqueDict -> PrimIO ()

%foreign "idris.support.appendToBuffer|support"
appendLines : Bool -> Bool -> Int -> String -> PrimIO ()

%foreign "l, _ => vim.fn.deletebufline('%', l)"
deleteLine : Int -> PrimIO ()

%foreign "s, _ => vim.fn.line(s)"
line : String -> PrimIO Int

%foreign "_ => vim.fn.strftime('%T')"
currenttime : PrimIO String

%foreign "s, _ => vim.fn.bufwinnr(s)"
bufwinnr : String -> PrimIO Int

%foreign "idris.support.fzfWindowBottom"
fzfWindowBottom : (name : String)
               -> (options : List String)
               -> (fn : String -> IO ())
               -> IO ()

%foreign "idris.support.matchlist"
matchlist : (str : String) -> (pattern : String) -> List String

responseBufferName : String
responseBufferName = "idris-response"

trimNewLineAtEnd : (str : String) -> String
trimNewLineAtEnd str =
  fastPack $ reverse $ dropWhile (== '\n') (reverse (fastUnpack str))

||| Runs a system command to find out where
||| the package source files are located. By default,
||| it uses a subdirectory of the local Idris 2 installation
getSourceDirectory : IO String
getSourceDirectory = do
  let cmd = "idris2 --libdir"
  Right fh <- popen cmd Read
      | Left err => do printLn err
                       exitFailure
  Right output <- fGetLine fh
      | Left err => do printLn err
                       exitFailure
  pclose fh
  let path ::: _ = split (== '\n') output
  let pathWithSuffix = path ++ "-src"
  pure pathWithSuffix

||| Creates a response buffer if absent
createResponseBuffer : IO ()
createResponseBuffer =
  when (not !(bufexists responseBufferName)) $
    do nvimCommand "let prevBuf = bufnr(@#)"
       nvimCommand $ "badd " ++ responseBufferName
       nvimCommand $ "b " ++ responseBufferName
       nvimCommand "set buftype=nofile"
       nvimCommand "b #"
       nvimCommand "let @# = prevBuf"

||| Writes to the response buffer, if loaded in one of the windows
writeToBuffer : Bool -> String -> IO ()
writeToBuffer commented str = do
  createResponseBuffer
  cwid <- primIO $ bufwinnr "."
  rwid <- primIO $ bufwinnr responseBufferName
  when (rwid > 0) $ do
   nvimCommand $ show rwid ++ "wincmd w"
   lastline <- primIO $ line "$"
   primIO $ appendLines commented True lastline str
   nvimCommand "normal! G"
   nvimCommand $ show cwid ++ "wincmd w"

splitMessages : String -> List String -> List String
splitMessages recv acc =
  case fromHex (reverse $ substr 0 6 recv) of
       Just 0 => acc
       Just len => let msg = substr 6 (integerToNat len) recv
                       rest = substr (integerToNat $ 6 + len) (length recv) recv in
                       splitMessages rest (snoc acc msg)
       Nothing => acc

runFind : (installDir : String) -> (searchStr : String) -> IO (List String)
runFind installDir searchStr = do
  let cmd = "fd -p " ++ searchStr ++ " . " ++ installDir
  Right f <- popen cmd Read
    | Left err => do putStrLn (show err)
                     exitFailure
  ret <- rec f []
  pclose f
  pure ret
where
  rec : File -> List String -> IO (List String)
  rec f got = do Right line <- fGetLine f
                   | Left err => do putStrLn (show err)
                                    exitFailure
                 if line == "" || line == "\n"
                   then
                     pure $ reverse got
                   else do
                     let line = trimNewLineAtEnd line
                     rec f (line :: got)

record NamePositionInfo where
  constructor MkNamePositionInfo
  name : String
  filename : String
  startRow : Integer
  startColumn : Integer
  endRow : Integer
  endColumn : Integer

||| Checks if the provided SExp is a valid entry of a name-at output.
||| Parses the entry into a record with info in that case.
validateNameAtEntry : SExp -> Maybe NamePositionInfo
validateNameAtEntry (SExpList [ StringAtom name
                                    , StringAtom filename
                                    , IntegerAtom sr
                                    , IntegerAtom sc
                                    , IntegerAtom er
                                    , IntegerAtom ec]) =
  Just $ MkNamePositionInfo name filename sr sc er ec
validateNameAtEntry _ = Nothing

||| Opens the file in the focused buffer, navigating to the provided row and column
jumpToDef : (filePath : String) -> (row : Integer) -> (col : Integer) -> IO ()
jumpToDef path row col = do
  nvimCommand "write"
  nvimCommand $ "edit " ++ path
  nvimCommand $ "call setpos('.', [0, " ++ show (row + 1) ++ ", " ++ show (col + 1) ++ ", 0])"
  nvimCommand $ "normal! zz"

zipWithIndex : List a -> List (a, Nat)
zipWithIndex xs = zip xs [0 .. length xs `minus` 1]

process : (params : Parameters)
       => IDEResult
       -> IO ()
process (OK idx res) = do
  case !(primIO $ getCmdFromHistory idx) of
    Just (Interpret sel) => do
      let SExpList ((StringAtom ls) :: _) = res
        | x => nvimCommand $ "echom 'Invalid response to Interpret" ++ show res ++ "'"
      writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (LoadFile path _) => do
      writeToBuffer True $ !(primIO currenttime) ++ "\nSuccesfully reloaded " ++ path
      primIO $ deleteCmdInHistory idx
    Just (TypeOf name _) => do

      let SExpList ((StringAtom ls) :: _) = res
        | x => nvimCommand $ "echom 'Invalid response to TypeOf" ++ show res ++ "'"
      writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (NameAt name _) => do
      primIO $ deleteCmdInHistory idx
      let SExpList [SExpList list] = res
        | x => nvimCommand $ "echom 'Invalid response to NameAt" ++ show res ++ "'"
      let Just validated@(first :: rest) = sequence $ map validateNameAtEntry list
        | Just [] => writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n"
                         ++ "Could not find anything on " ++ name
        | Nothing => nvimCommand $ "echom 'Invalid response to NameAt" ++ show res ++ "'"
      case rest of
        [] => do -- exactly one name returned by the IDE
          [fullPath] <- runFind params.sourceDir first.filename -- one candidate found by the finder
            | multiple@(_ :: _) => do
                let relative = filter isRelative multiple --keep only relative paths
                case relative of
                  [] => nvimCommand "echoe \"Can't handle multiple absolute candidates\""
                  [singlePath] =>
                    jumpToDef singlePath first.startRow first.startColumn
                  _ => nvimCommand "echoe \"Can't handle multiple relative candidates\""
            | [] => nvimCommand "echoe 'Candidates not found'"
          jumpToDef fullPath first.startRow first.startColumn
        _ :: _ => do
          let fzfInput = map (\(x, i) => "[" ++ show i ++ "] " ++ x.filename)
                             (zipWithIndex validated)
          -- TODO previews
          fzfWindowBottom name fzfInput \file =>
            -- I (Russoul) don't know why, but the fzf vim plugin calls this callback with the empty string
            -- in addition to a normal call with the supplied choice.
            -- So we have to filter out that empty redundant call here
            when (file /= "") $ do
              nvimCommand $ "echom 'file is: " ++ file ++ "'"
              let _ :: iStr :: _ = matchlist file "\\v\\[([0-9]+)\\].+"
                | _ => nvimCommand $ "echoe 'Bad match while processing name-at'"
              let Just i = parsePositive {a = Nat} iStr
                | _ => nvimCommand $ "echoe 'Bad match while processing name-at'"
              let Just (entry, _) = find (\(_, j) => i == j) (zipWithIndex validated)
                | _ => nvimCommand $ "echoe 'Bad match while processing name-at'"
              nvimCommand $ "echom 'entry filename is: " ++ entry.filename ++ "'"
              candidates <- runFind params.sourceDir entry.filename
              case candidates of
                [] => writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n"
                                 ++ "Could not find anything on " ++ name
                [singlePath] => jumpToDef singlePath entry.startRow entry.startColumn
                many => do
                  -- Prioritise relative paths over absolute ones,
                  -- in case multiple files are found by the find utility
                  let relative = filter isRelative many
                  case relative of
                    [] => nvimCommand "echoe \"Can't handle multiple absolute candidates\""
                    [singlePath] =>
                      jumpToDef singlePath entry.startRow entry.startColumn
                    _ => nvimCommand "echoe \"Can't handle multiple relative candidates\""
    Just (DocsFor name _) => do
      let SExpList ((StringAtom ls) :: _) = res
        | x => nvimCommand $ "echom 'Invalid response to DocsFor" ++ show res ++ "'"
      writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (CaseSplit line col name) => do
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to CaseSplit" ++ show res ++ "'"
      primIO $ deleteLine (cast line)
      primIO $ appendLines False False (cast line - 1) ls
      primIO $ deleteCmdInHistory idx
    Just (AddClause line name) => do
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to AddClause" ++ show res ++ "'"
      primIO $ appendLines False False (cast line) ls
      primIO $ deleteCmdInHistory idx
    Just (ExprSearch line name _ _) => do
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to ExprSearch" ++ show res ++ "'"
      nvimCommand $ "s/" ++ (strCons '?' name) ++ "/" ++ ls ++ "/"
      ignore $ primIO $ putLastSearch ls
      primIO $ deleteCmdInHistory idx
    Just ExprSearchNext => do
      -- TODO: How we rollback?
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to ExprSearch" ++ show res ++ "'"
      writeToBuffer True $ "Inline substitution of next expression search is not available\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (GenerateDef line name) => do
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to GenerateDef" ++ show res ++ "'"
      primIO $ appendLines False False (cast line) ls
      primIO $ deleteCmdInHistory idx
    Just GenerateDefNext => do
      -- TODO: How we rollback?
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to ExprSearch" ++ show res ++ "'"
      writeToBuffer True $ "Inline substitution of next definition is not available\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (MakeLemma line name) => do
      -- TODO: How we find where to put the lemma? (Maybe, go to the previous paragraph and append there)
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to ExprSearch" ++ show res ++ "'"
      writeToBuffer False $ "Inline substitution of make lemma is not available\n" ++ ls
      primIO $ deleteCmdInHistory idx
    Just (MakeCase line name) => do
      -- TODO: Feels like a hack
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to MakeCase" ++ show res ++ "'"
      primIO $ deleteLine (cast line)
      primIO $ appendLines False False (cast line - 1) ls
      primIO $ deleteCmdInHistory idx
    Just (MakeWith line name) => do
      -- TODO: Feels like a hack
      let SExpList [StringAtom ls] = res
        | x => nvimCommand $ "echom 'Invalid response to MakeWith" ++ show res ++ "'"
      primIO $ deleteLine (cast line)
      primIO $ appendLines False False (cast line - 1) ls
      primIO $ deleteCmdInHistory idx
    Just (Metavariables _) => do
      -- let SExpList [StringAtom ls] = res
      --   | x => nvimCommand $ "echom 'Invalid response to Metavariables" ++ show res ++ "'"
      writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n" ++ (show res)
      primIO $ deleteCmdInHistory idx
    Just (BrowseNamespace name) => do
      let SExpList ((StringAtom ls) :: _) = res
        | x => nvimCommand $ "echom 'Invalid response to BrowseNamespace" ++ show res ++ "'"
      writeToBuffer False $ "-- " ++ !(primIO currenttime) ++ "\n" ++ ls
      primIO $ deleteCmdInHistory idx
--     Just (EnableSyntax _) => do
--       let SExpList ((StringAtom ls) :: _) = res
--         | x => nvimCommand $ "echom 'Invalid response to EnableSyntax"++ show res ++ "'"
--       writeToBuffer True $ !(primIO currenttime) ++ "\nServer message: \"" ++ ls ++ "\""
--       primIO $ deleteCmdInHistory idx
    Just GetOptions => do
      writeToBuffer True (show res)
      primIO $ deleteCmdInHistory idx
    x => pure ()
process (Warning idx (SExpList [StringAtom file, start, end, StringAtom msg, _])) = pure () -- TODO: disabled until fix in compiler
process (Error idx (SExpList ((StringAtom ls) :: _))) = do
  writeToBuffer False $ "-- Error " ++ !(primIO currenttime) ++ "\n" ++ ls
  primIO $ deleteCmdInHistory idx
process (WriteString idx res) = do
  let msg = !(primIO currenttime) ++ "\nServer message: \"" ++ res ++ "\""
  writeToBuffer True msg
  primIO $ deleteCmdInHistory idx
process (Output idx res) = primIO $ deleteCmdInHistory idx
process (Version (SExpList [IntegerAtom major, IntegerAtom minor])) = do
  let msg = !(primIO currenttime) ++ "\nIdris2 IDE Mode server version " ++ show major ++ "." ++ show minor
  writeToBuffer True msg
process _ = nvimCommand $ "echom 'Invalid message from the server'"

connectIdris2 : (params : Parameters)
             => String
             -> Int
             -> IO OpaqueDict
connectIdris2 host port = do
  nvimCommand "echom 'Starting connection...'"
  client <- newTCP
  nvimCommand "echom 'Created new tcp socket...'"
  connect client host port
    (do readStart client
          (\recv => do
              let msgs = splitMessages recv []
              for_ msgs $ \msg => do
                let head = substr 0 5 msg
                if (head == "(:out")
                   then nvimCommand $ "echo 'skipped output'"
                   else do let Right sexp = parseSExp msg
                             | Left err => nvimCommand $ "echom 'invalid response: " ++ show err ++ "'"
                           let Just res = getResult sexp
                             | Nothing => nvimCommand $ "echom 'invalid response: " ++ show sexp ++ "'"
                           process res)
          (\err => nvimCommand $ "echom 'read err: " ++ err ++ "'")
          (pure ()))
    (\err => nvimCommand $ "echom 'connect error: " ++ err ++ "'")
  -- write client !(buildCommand $ EnableSyntax False) -- Still not merged
  pure client

quitServer : HasIO io
          => Ref Server (Maybe OpaqueDict)
          => io ()
quitServer = do
  Just handle <- get Server
    | Nothing => pure ()
  sigterm handle
  put Server Nothing

-- TODO: Use IORef instead of an hacky global variable. How we pass it to
--       callbacks without loosing generality?
spawnAndConnectIdris2 : HasIO io
                     => (params : Parameters)
                     => Ref Server (Maybe OpaqueDict)
                     => Ref Client (Maybe OpaqueDict)
                     => (String, Int)
                     -> (String, Int)
                     -> io ()
spawnAndConnectIdris2 (shost, sport) (chost, cport) = do
  Nothing <- get Server
    | Just _ => nvimCommand "echom 'Idris2 process already spawned'"
  stdout <- newPipe
  let opts = spawnOpts (shost ++ ":" ++ show sport) stdout
  d <- spawn "idris2" opts (\code, signal => nvimCommand $ "echom 'Idris2 process closed with code " ++ show code ++ "'")
  let handle : OpaqueDict = getField d "handle"
  put Server (Just handle)
  readStart stdout (\msg => do nvimCommand $ "echom 'server: " ++ msg ++ "'"
                               if trim msg == show sport
                                  then do client <- connectIdris2 chost cport
                                          primIO $ setGlobalClient client -- TODO: can we remove it?
                                          put Client (Just client)
                                          readStop stdout
                                  else do nvimCommand $ "echom 'wrong port " ++ msg ++ "'"
                                          quitServer)
                   (\err => do nvimCommand $ "echom 'err: " ++ err ++ "'"
                               quitServer)
                   (do nvimCommand "echom 'Idris2 stdout closed'"
                       quitServer)

main : IO ()
main = do
  loadCommands

  serverRef <- newRef Server $ the (Maybe OpaqueDict) Nothing
  clientRef <- newRef Client $ the (Maybe OpaqueDict) Nothing

  sourceDir <- getSourceDirectory

  autostart <- getGlobalBoolVar "idris2_autostart" True

  let params = MkParameters sourceDir

  when autostart $ do
    nvimCommand "set maxfuncdepth=10000"
    nvimCommand "echom 'starting idris2 ide mode plugin'"

    externalClientOpt <- getGlobalBoolVar "idris2_external_server" False
    if externalClientOpt
       then do nvimCommand "echom 'starting with external server'"
               host <- getGlobalStringVar "idris2_external_host" "127.0.0.1"
               port <- getGlobalIntVar "idris2_external_port" 38398
               client <- connectIdris2 host port
               primIO $ setGlobalClient client
       else do nvimCommand "echom 'starting server'"
               port <- getGlobalIntVar "idris2_server_port" 38398
               spawnAndConnectIdris2 ("localhost", port) ("127.0.0.1", port)

    -- KEYBINDINGS
    nnoremap !(getGlobalStringVar "idris2_loadCurrent_key" "<LocalLeader>r")
              (commandBinding True `{{loadCurrent}})
    nnoremap !(getGlobalStringVar "idris2_typeOf_key" "<LocalLeader>t")
              (commandBinding True `{{typeOf}})
    nnoremap !(getGlobalStringVar "idris2_typeOfPrompt_key" "<LocalLeader>T")
              (commandBinding True `{{typeOfPrompt}})
    vnoremap !(getGlobalStringVar "idris2_typeOf_key" "<LocalLeader>t")
              (commandBinding True `{{typeOfSel}})
    nnoremap !(getGlobalStringVar "idris2_docOverview_key" "<LocalLeader>d")
              (commandBinding True `{{docOverview}})
    nnoremap !(getGlobalStringVar "idris2_caseSplit_key" "<LocalLeader>c")
              (commandBinding True `{{caseSplit}})
    nnoremap !(getGlobalStringVar "idris2_exprSearch_key" "<LocalLeader>s")
              (commandBinding True `{{exprSearch}})
    nnoremap !(getGlobalStringVar "idris2_exprSearchNext_key" "<LocalLeader>sn")
              (commandBinding True `{{exprSearchNext}})
    nnoremap !(getGlobalStringVar "idris2_addClause_key" "<LocalLeader>a")
              (commandBinding True `{{addClause}})
    nnoremap !(getGlobalStringVar "idris2_generateDef_key" "<LocalLeader>g")
              (commandBinding True `{{generateDef}})
    nnoremap !(getGlobalStringVar "idris2_generateDefNext_key" "<LocalLeader>gn")
              (commandBinding True `{{generateDefNext}})
    nnoremap !(getGlobalStringVar "idris2_makeLemma_key" "<LocalLeader>l")
              (commandBinding True `{{makeLemma}})
    nnoremap !(getGlobalStringVar "idris2_makeCase_key" "<LocalLeader>mc")
              (commandBinding True `{{makeCase}})
    nnoremap !(getGlobalStringVar "idris2_makeWith_key" "<LocalLeader>w")
              (commandBinding True `{{makeWith}})
    nnoremap !(getGlobalStringVar "idris2_jumpTo_key" "<LocalLeader>j")
              (commandBinding True `{{nameAt}})
    nnoremap !(getGlobalStringVar "idris2_jumpToPrompt_key" "<LocalLeader>J")
              (commandBinding True `{{nameAtPrompt}})
    vnoremap !(getGlobalStringVar "idris2_jumpTo_key" "<LocalLeader>j")
              (commandBinding True `{{nameAtSel}})
    vnoremap !(getGlobalStringVar "idris2_interpret_key" "<LocalLeader>e")
              (commandBinding True `{{interpret}}) -- evaluates selected code

    -- AUTOCOMMANDS
    loadOnStart <- getGlobalBoolVar "idris2_load_on_start" True
    when loadOnStart $ do
      nvimCommand "augroup IdrisLoadOnRead"
      nvimCommand " autocmd!"
      nvimCommand $ "autocmd BufNewFile,BufRead *.idr " ++ commandBinding False `{{loadCurrent}}
      nvimCommand "augroup end"
    -- Set up the response buffer
    nvimCommand "augroup IdrisSetBufType"
    nvimCommand $ " autocmd!"
    nvimCommand $ " autocmd BufEnter " ++ responseBufferName ++ " set buftype=nofile|set syntax=idris2"
    nvimCommand "augroup end"

    -- RESPONSE BUFFER
    nvimCommand "vertical rightbelow split"
    nvimCommand "badd idris-response"
    nvimCommand "b idris-response"
    nvimCommand "set buftype=nofile"
    nvimCommand "wincmd h"


text:
module Main

f : Maybe Integer -> Int
f x = 3
f (Just _) = 1
f Nothing = 0

main : IO ()
main = do
    putStrLn $ show $ f (Just 3)
    putStrLn $ show $ f Nothing

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module GameServer.Protocol.Mock

import Data.Buffer
import Data.List
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw
import System

import GameServer.Protocol.Options
import GameServer.Protocol.Messages
import GameServer.Protocol.Binary

%cg chez libidris_net.so

handleClient : Socket -> SocketAddress -> (len_buf : BufPtr) -> IO ()
handleClient socket addr len_buf = do
  putStrLn $ "waiting for input"
  Right res <- recvBuf socket len_buf 8 -- receive 8 bytes representing length of message
    | Left err => do putStrLn ("failed to read length of message " ++ show err) ; close socket
  if res < 0
    then do putStrLn ("error reading message length: " ++ show res) ; close socket
    else do len <- read64be len_buf
            data_buf <- sock_alloc (cast len)
            Right res <- recvBuf socket data_buf (fromInteger len)
              | Left err => do putStrLn ("failed to read message of len " ++ show len ++ ": " ++ show err) ; sock_free data_buf ; close socket
            if res < 0
              then  do putStrLn ("failed to read message " ++ show res) ; sock_free data_buf ; close socket
              else do
                Right msg <- decodeMessage data_buf len
                  | Left err => do putStrLn ("failed to decode message " ++ show err) ; sock_free data_buf
                print msg
                sock_free data_buf
                handleClient socket addr len_buf

serve : Socket -> IO (Either String ())
serve sock = do
  Right (s, addr) <- accept sock
    | Left err => pure (Left $ "Failed to accept on socket with error: " ++ show err)
  pid <- fork $ do
    len_buf <- sock_alloc 8
    handleClient s addr len_buf
  serve sock

export
server : Int -> String -> IO (Either String ())
server port host = do
  Right sock <- socket AF_INET Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- bind sock (Just (Hostname host)) port
  if res /= 0
    then pure (Left $ "Failed to bind socket with error: " ++ show res)
    else do
      res <- listen sock
      if res /= 0
        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
        else serve sock

export
mock : Options -> IO (Either String ())
mock (MkOptions port host MockMode) = server port host
mock _ = pure $ Left "invalid mode for mock server"

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
-- Prototype of RealizedFunction as described in
-- https://blog.singularitynet.io/ai-dsl-toward-a-general-purpose-description-language-for-ai-agents-21459f691b9e

-- List RealizedFunction but only has one attribute which is cost
module SimpleRealizedFunction

public export
record SimpleRealizedFunction f (cost : Integer) (quality : Double) where
  constructor MkSimpleRealizedFunction
  function : f

-- Perform the composition between 2 simple realized functions.  The
-- resulting realized function is formed as follows:
--
-- 1. Composed lifted functions
-- 2. Costs are added
public export
compose : (SimpleRealizedFunction (b -> c) g_cost g_q) ->
          (SimpleRealizedFunction (a -> b) f_cost f_q) ->
          (SimpleRealizedFunction (a -> c) (f_cost + g_cost) (min f_q g_q))
compose rlz_f rlz_g = MkSimpleRealizedFunction rlz_fg where
  rlz_fg : a -> c
  rlz_fg = rlz_f.function . rlz_g.function

-- Perform function application over realized functions.  Maybe we'd
-- want to used some funded data, as defined in FndType.
public export
apply : (SimpleRealizedFunction (a -> b) cost quality) -> a -> b
apply rlz_f = rlz_f.function

max_stars_repo_name: sroberti/ai-dsl

max_issues_repo_name: sroberti/ai-dsl

max_forks_repo_name: sroberti/ai-dsl


text:
module Flexidisc.THList

%default total
%access export

||| `THList` stands for "TagLess Heterogenous list
||| It's a record demoted to an heterogeneous list,
||| where the label are only kept at the type lebvel
public export
data THList : (m : Type -> Type) -> (k : Type) -> (List (k, Type)) -> Type where
  Nil  : THList m k []
  (::) : m a -> THList m k xs -> THList m k ((l, a)::xs)

implementation Eq (THList m k []) where
  (==) x y = True
  (/=) x y = False

implementation (Eq (m t), Eq (THList m k ts)) => Eq (THList m k ((l,t)::ts)) where
  (==) (x :: xs) (y :: ys) = x == y && xs == ys
  (/=) (x :: xs) (y :: ys) = x /= y || xs /= ys

interface Shows t where
  shows : t -> List String

implementation Shows (THList m k []) where
  shows _ = []

implementation (Show k, Show (m t), Shows (THList m k ts)) =>
               Shows (THList m k ((l,t) :: ts)) where
  shows (x::xs) {l} = unwords [show l, ":=", show x] :: shows xs

implementation Shows (THList m k xs) => Show (THList m k xs) where
  show xs = unwords ["[", concat (intersperse ", " (shows xs)), "]"]

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Graph.Core

import Graph.DictStub as D

-- %default total

-- --------------------------------------------------------------------- [Types]
public export
NodeID : Type
NodeID = Int
%name NodeID node

public export
LNode : Type -> Type
LNode a = (NodeID, a)
%name LNode lnode

public export
Edge : Type
Edge = (NodeID, NodeID)
%name Edge edge

public export
LEdge : Type -> Type
LEdge b = (NodeID, NodeID, b)
%name LEdge ledge

public export
Path : Type
Path = List NodeID
%name Path path

public export
Adj : Type -> Type
Adj b = List (b, NodeID)
%name Adj adj

public export
Context : Type -> Type -> Type
Context a b = (Adj b, NodeID, a, Adj b)
%name Context ctxt

public export
MContext : Type -> Type -> Type
MContext a b = Maybe (Context a b)
%name MContext mctxt

NodeMap : Type -> Type
NodeMap = DictStub NodeID

Context' : Type -> Type -> Type
Context' a b = (NodeMap (List b), a, NodeMap (List b))

GraphData : Type -> Type -> Type
GraphData a b = NodeMap (Context' a b)
%name GraphData qdata

export
data Graph a b = MkGraph (GraphData a b)

%name Graph q, q1, q2

public export
Decomp : Type -> Type -> Type
Decomp a b = (MContext a b, Graph a b)
%name Decomp decomp

public export
GDecomp : Type -> Type -> Type
GDecomp a b = (Context a b, Graph a b)
%name GDecomp gdecomp

-- ------------------------------------------------------------------- [Helpers]
addLists : List a -> List a -> List a
addLists [x] ys = x :: ys
addLists xs [y] = y :: xs
addLists xs ys = xs ++ ys

addSucc : GraphData a b -> NodeID -> List (b, NodeID) -> GraphData a b
addSucc qdata _ [] = qdata
addSucc qdata node ((l, node') :: rest) = addSucc qdata' node rest
  where
    qdata' = adjust f node' qdata
    f : Context' a b -> Context' a b
    f (preds, l', succs) = (preds, l', insertWith addLists node [l] succs)

addPred : GraphData a b -> NodeID -> List (b, NodeID) -> GraphData a b
addPred qdata _ [] = qdata
addPred qdata node ((l, node') :: rest) = addPred qdata' node rest
  where
    qdata' = adjust f node' qdata
    f : Context' a b -> Context' a b
    f (preds, l', succs) = (insertWith addLists node [l] preds, l', succs)

fromAdj : Adj b -> NodeMap (List b)
fromAdj = fromListWith addLists . map (\(label, node) => (node, [label]))

toAdj : NodeMap (List b) -> Adj b
toAdj = concatMap expand . toList
  where
    expand : (NodeID, List b) -> List (b, NodeID)
    expand (node, ls) = map ((flip MkPair) node) ls

clearSucc : GraphData a b -> NodeID -> List NodeID -> GraphData a b
clearSucc qdata _ [] = qdata
clearSucc qdata node (p :: rest) = clearSucc qdata' node rest
  where
    qdata' = adjust f p qdata
    f : Context' a b -> Context' a b
    f (preds, l, succs) = (preds, l, delete node succs)

clearPred : GraphData a b -> NodeID -> List NodeID -> GraphData a b
clearPred qdata _ [] = qdata
clearPred qdata node (p :: rest) = clearSucc qdata' node rest
  where
    qdata' = adjust f p qdata
    f : Context' a b -> Context' a b
    f (preds, l, succs) = (delete node preds, l, succs)

-- ---------------------------------------------------------------- [Operations]

infixr 10 & -- TODO choose right fixity

emptyData : GraphData a b
emptyData = D.empty {k = NodeID} {v = Context' a b}

emptyMap : NodeMap (List b)
emptyMap = D.empty {k = NodeID} {v = List b}

export
empty : Graph a b
empty = MkGraph emptyData

export
isEmpty : Graph a b -> Bool
isEmpty (MkGraph c) = case D.toList c of
                            [] => True
                            _ => False

export
embed : Context a b -> Graph a b -> Graph a b
embed (preds, node, label, succs) (MkGraph qdata)
  = let qdata1 = insert node (fromAdj preds, label, fromAdj succs) qdata
        qdata2 = addSucc qdata1 node preds
        qdata3 = addPred qdata2 node succs in
    MkGraph qdata3

export
(&) : Context a b -> Graph a b -> Graph a b
(&) = embed

-- TODO can we statically verify that we match against a node that's in the graph?
export
match : NodeID -> Graph a b -> Decomp a b
match node q@(MkGraph qdata)
  = case D.lookup node qdata of
         Nothing => (Nothing, q)
         Just (preds, label, succs)
           => let qdata1 = delete node qdata
                  preds' = delete node preds
                  succs' = delete node succs
                  qdata2 = clearPred qdata1 node (keys succs')
                  qdata3 = clearSucc qdata2 node (keys preds')
              in (Just (toAdj preds', node, label, toAdj succs), MkGraph qdata3)

-- TODO get rid of ?error by making sure that match always succeed
-- The Edge must find a way to tell that its source (and maybe target)
-- do belong to the graph
insEdge : LEdge b -> Graph a b -> Graph a b
insEdge (source, target, l) graph
  = let (mcxt, graph') = match source graph
        (pr, _, la, su) = fromMaybe ?error mcxt in
    (pr, source, la, (l, target) :: su) & graph'

insEdges : List (LEdge b) -> Graph a b -> Graph a b
insEdges edges graph = foldl (flip insEdge) graph edges

export
mkGraph : List (LNode a) -> List (LEdge b) -> Graph a b
mkGraph nodes edges = insEdges edges (MkGraph (fromList (
                        map (\(node, label) => (node, emptyMap, label, emptyMap)) nodes)))

export
labNodes : Graph a b -> List (LNode a)
labNodes (MkGraph qdata) = [ (node, label) | (node, (_, label, _)) <- toList qdata ]

-- TODO find a way to make sure that you never match on an empty graph
export
matchAny : Graph a b -> GDecomp a b
matchAny g
  = case labNodes g of
         [] => ?empty_graph
         (n, _) :: _ => let (Just ctxt, g') = match n g in (ctxt, g')

export
ufold : (Context a b -> ty_acc -> ty_acc) -> ty_acc -> Graph a b -> ty_acc
ufold f acc g
  = if isEmpty g
       then acc
       else let (ctxt, g') = matchAny g in f ctxt (ufold f acc g')

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
import Data.Vect

%unbound_implicits off

append : forall n, m, a . Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

data Env : forall n . Vect n Type -> Type where
     ENil : Env []
     ECons : forall t, ts . t -> Env ts -> Env (t :: ts)

-- fine because the only name used in bound, and it'll infer types for
-- xs and its indices
len : forall xs . Env xs -> Nat

-- neither of these are fine
len': Env xs -> Nat
append' : Vect n a -> Vect m a -> Vect (n + m) a


text:
module TTImp.ProcessParams

import Core.Context
import Core.Context.Log
import Core.Env
import Core.TT
import Core.Unify
import Core.Metadata
import Core.Normalise

import TTImp.BindImplicits
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.TTImp

import Data.List

%default covering

extend : {extvs : _} ->
         Env Term extvs -> SubVars vs extvs ->
         NestedNames extvs ->
         Term extvs ->
         (vars' ** (SubVars vs vars', Env Term vars', NestedNames vars'))
extend env p nest (Bind _ n b@(Pi fc c pi ty) sc)
    = extend (b :: env) (DropCons p) (weaken nest) sc
extend env p nest tm = (_ ** (p, env, nest))

export
processParams : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                NestedNames vars ->
                Env Term vars ->
                FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> List ImpDecl ->
                Core ()
processParams {vars} {c} {m} {u} nest env fc ps ds
    = do -- Turn the parameters into a function type, (x : ps) -> Type,
         -- then read off the environment from the elaborated type. This way
         -- we'll get all the implicit names we need
         let pty_raw = mkParamTy ps
         pty_imp <- bindTypeNames fc [] vars (IBindHere fc (PI erased) pty_raw)
         log "declare.param" 10 $ "Checking " ++ show pty_imp
         pty <- checkTerm (-1) InType []
                          nest env pty_imp (gType fc)
         let (vs ** (prf, env', nest')) = extend env SubRefl nest pty
         logEnv "declare.param" 5 "Param env" env'

         -- Treat the names in the block as 'nested names' so that we expand
         -- the applications as we need to
         defs <- get Ctxt
         let defNames = definedInBlock (currentNS defs) ds
         names' <- traverse (applyEnv env') defNames
         let nestBlock = record { names $= (names' ++) } nest'
         traverse_ (processDecl [] nestBlock env') ds
  where
    mkParamTy : List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
    mkParamTy [] = IType fc
    mkParamTy ((n, rig, info, ty) :: ps)
       = IPi fc rig info (Just n) ty (mkParamTy ps)

    applyEnv : {vs : _} ->
               Env Term vs -> Name ->
               Core (Name, (Maybe Name, List (Var vs), FC -> NameType -> Term vs))
    applyEnv {vs} env n
          = do n' <- resolveName n -- it'll be Resolved by expandAmbigName
               pure (Resolved n', (Nothing, reverse (allVars env),
                        \fc, nt => applyToFull fc
                               (Ref fc nt (Resolved n')) env))


text:
module NatExtension

%default total
%access public export

zeroYCancel : (x : Nat) -> (y : Nat) -> x + y = 0 -> x = 0
zeroYCancel x Z e = rewrite plusCommutative 0 x in e
zeroYCancel x (S k) e = void $ SIsNotZ (trans (plusCommutative (S k) x) e)

multLeftCancel : (x : Nat) -> (y : Nat) -> (z : Nat) -> S x * y = S x * z -> y = z
multLeftCancel x Z z e = sym (zeroYCancel _ _ (sym (rewrite multCommutative 0 x in e)))
multLeftCancel x y Z e = zeroYCancel _ _ (rewrite multCommutative 0 x in e)
multLeftCancel x (S k) (S j) e = rewrite multLeftCancel x k j _ss3 in Refl
  where
    _ss1 : k + (x + x * k) = j + (x + x * j)
    _ss1 =
        rewrite sym $ multRightSuccPlus x k in
        rewrite sym $ multRightSuccPlus x j in
        succInjective _ _ e

    _ss2 : x + (k + x * k) = x + (j + x * j)
    _ss2 =
        rewrite plusAssociative x k (x * k) in
        rewrite plusAssociative x j (x * j) in
        rewrite plusCommutative x k in
        rewrite plusCommutative x j in
        rewrite sym $ plusAssociative k x (x * k) in
        rewrite sym $ plusAssociative j x (x * j) in
        _ss1

    _ss3 : k + x * k = j + x * j
    _ss3 = plusLeftCancel _ _ _ _ss2

takeY : (x : Nat) -> (y : Nat) -> (z : Nat) -> x * (y * z) = y * x * z
takeY x y z =
        rewrite multAssociative x y z in
        rewrite multCommutative x y in
        Refl


text:
> module SequentialDecisionProblems.OptDefaults

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.Utils

> import Finite.Predicates
> import Finite.Operations
> import Opt.Operations
> import Rel.TotalPreorder

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

We implement |cvalmax|, |cvalargmax|, |cvalmaxSpec| and |cvalargmaxSpec|
by exhaustive search (see |Opt|) if we can show that |LTE| is a total
preorder

> totalPreorderLTE : TotalPreorder SequentialDecisionProblems.CoreTheory.LTE

, that |GoodCtrl t x n| is finite and that, for every |t : Nat|, |x :
State t| such that |Viable (S n) x|, its cardinality is not zero.

In typical applications, finiteness and non-emptyness of |GoodCtrl t x
n| are going to be deduced (see Utils) from finiteness of |All| and
|NotEmpty| (see, for instance, NonDeterministicDefaults), finiteness of
|Viable| (see ViabilityDefaults) and finiteness of controls.

> SequentialDecisionProblems.FullTheory.cvalmax {n} x r v ps =
>  Opt.Operations.max totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.CoreTheory.cvalargmax {n} x r v ps =
>   Opt.Operations.argmax totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalmaxSpec {n} x r v ps =
>   Opt.Operations.maxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalargmaxSpec {n} x r v ps =
>   Opt.Operations.argmaxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Cont.Out

import Control.HigherOrder

import Control.Monad.Free

public export
data Out cnt = MkOut String cnt

public export
Functor Out where
  map f (MkOut x y) = MkOut x (f y)

public export
HOut : (Type -> Type) -> (Type -> Type)
HOut = Lift Out

public export
runOut : Free HOut a -> IO a
runOut (Return x) = pure x
runOut (Op (MkLift (MkOut s p))) =
  putStrLn s `io_bind` \_ => runOut p

public export
out : Inj HOut sig => String -> Free sig ()
out x = inject {sub = HOut} $ MkLift $ MkOut x (return ())


text:
> module Nat.LTEProperties

> import Rel.TotalPreorder

> %default total
> %auto_implicits on
> %access export
> -- %access public export

LTE is unique:

> ||| LTE is unique
> uniqueLTE : (p1 : LTE m n) -> (p2 : LTE m n) -> p1 = p2
> uniqueLTE  LTEZero     LTEZero    = Refl
> uniqueLTE  LTEZero    (LTESucc p) impossible
> uniqueLTE (LTESucc p)  LTEZero    impossible
> uniqueLTE (LTESucc p) (LTESucc q) = cong (uniqueLTE p q)
> %freeze uniqueLTE

LTE is decidable:

> ||| LTE is decidable
> decLTE : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
> --decLTE = lte
> --{-
> decLTE Z _     = Yes LTEZero
> decLTE (S m) Z = No succNotLTEzero
> decLTE (S m) (S n) with (decLTE m n)
>   | (Yes p) = Yes (LTESucc p)
>   | (No contra) = No (\ p => contra (fromLteSucc p))
> ---}
> %freeze decLTE

|LTE| is a total preorder:

> ||| LTE is reflexive
> reflexiveLTE : (n : Nat) -> LTE n n
> reflexiveLTE n = lteRefl {n}

> ||| LTE is transitive
> transitiveLTE : (m : Nat) -> (n : Nat) -> (o : Nat) ->
>                 LTE m n -> LTE n o -> LTE m o
> transitiveLTE  Z       n     o   LTEZero                 nlteo  = LTEZero
> transitiveLTE (S m) (S n) (S o) (LTESucc mlten) (LTESucc nlteo) = LTESucc (transitiveLTE m n o mlten nlteo)
> %freeze transitiveLTE

> ||| LTE is total
> totalLTE : (m : Nat) -> (n : Nat) -> Either (LTE m n) (LTE n m)
> totalLTE  Z    n     = Left LTEZero
> totalLTE (S m) Z     = Right LTEZero
> totalLTE (S m) (S n) with (totalLTE m n)
>   | (Left  p) = Left  (LTESucc p)
>   | (Right p) = Right (LTESucc p)
> %freeze totalLTE

> ||| LTE is a total preorder
> totalPreorderLTE : TotalPreorder LTE
> totalPreorderLTE = MkTotalPreorder LTE reflexiveLTE transitiveLTE totalLTE

Properties of |LTE| and successor:

> |||
> notLTELemma0 : Not (S m `LTE` S n) -> Not (m `LTE` n)
> notLTELemma0 contra = contra . LTESucc
> %freeze notLTELemma0

> |||
> notLTELemma1 : (m : Nat) -> (n : Nat) -> Not (m `LTE` n) -> n `LTE` m
> notLTELemma1  m     Z    p = LTEZero
> notLTELemma1  Z    (S n) p = void (p LTEZero)
> notLTELemma1 (S m) (S n) p = LTESucc (notLTELemma1 m n (notLTELemma0 p))
> %freeze notLTELemma1

> |||
> lteLemma1 : (m : Nat) -> (n : Nat) -> LTE (S m) n -> LTE m n
> lteLemma1  Z     Z             prf  = absurd prf
> lteLemma1  Z    (S n)  LTEZero        impossible
> lteLemma1  Z    (S n) (LTESucc prf) = LTEZero
> lteLemma1 (S m)  Z             prf  = absurd prf
> lteLemma1 (S m) (S n)  LTEZero        impossible
> lteLemma1 (S m) (S n) (LTESucc prf) = LTESucc (lteLemma1 m n prf)
> %freeze lteLemma1

> |||
> idSuccPreservesLTE : (m : Nat) -> (n : Nat) -> m `LTE` n -> m `LTE` (S n)
> idSuccPreservesLTE  Z     n    prf = LTEZero
> idSuccPreservesLTE (S m)  Z    prf = absurd prf
> idSuccPreservesLTE (S m) (S n) prf = LTESucc (idSuccPreservesLTE m n (fromLteSucc prf))
> %freeze idSuccPreservesLTE

Properties of |LTE| and |plus|:

> |||
> elimSuccRightLTEPlus : {a, b, c, d : Nat} -> LTE (a + S b) (c + S d) -> LTE (a + b) (c + d)
> elimSuccRightLTEPlus {a} {b} {c} {d} aSbLTEcSd = s6 where
>   s0 : LTE (a + S b) (c + S d)
>   s0 = aSbLTEcSd
>   s1 : LTE (S b + a) (c + S d)
>   s1 = replace {P = \ ZUZU => LTE ZUZU (c + S d)} (plusCommutative a (S b)) s0
>   s2 : LTE (S b + a) (S d + c)
>   s2 = replace {P = \ ZUZU => LTE (S b + a) ZUZU } (plusCommutative c (S d)) s1
>   s3 : LTE (S (b + a)) (S (d + c))
>   s3 = s2
>   s4 : LTE (b + a) (d + c)
>   s4 = fromLteSucc s3
>   s5 : LTE (a + b) (d + c)
>   s5 = replace {P = \ ZUZU => LTE ZUZU (d + c)} (plusCommutative b a) s4
>   s6 : LTE (a + b) (c + d)
>   s6 = replace {P = \ ZUZU => LTE (a + b) ZUZU}(plusCommutative d c) s5
> %freeze elimSuccRightLTEPlus

> |||
> idAnyPlusPreservsLTE : {a, b, c : Nat} -> LTE a b -> LTE a (c + b)
> idAnyPlusPreservsLTE {a} {b} {c = Z}   aLTEb = aLTEb
> idAnyPlusPreservsLTE {a} {b} {c = S m} aLTEb = idSuccPreservesLTE a (m + b) (idAnyPlusPreservsLTE {a = a} {b = b} {c = m} aLTEb)
> %freeze idAnyPlusPreservsLTE

> |||
> monotoneNatPlusLTE : {a, b, c, d  : Nat} ->
>                      LTE a b -> LTE c d -> LTE (a + c) (b + d)
> monotoneNatPlusLTE {a = Z}   {b = Z}   {c} {d} _           cLTEd =
>   cLTEd
> monotoneNatPlusLTE {a = Z}   {b = S n} {c} {d} _           cLTEd =
>   idAnyPlusPreservsLTE {a = c} {b = d} {c = S n} cLTEd
> monotoneNatPlusLTE {a = S m} {b = Z}   {c} {d} aLTEb       _     =
>   absurd aLTEb
> monotoneNatPlusLTE {a = S m} {b = S n} {c} {d} (LTESucc p) cLTEd =
>   LTESucc (monotoneNatPlusLTE {a = m} {b = n} {c = c} {d = d} p cLTEd)
> %freeze monotoneNatPlusLTE

> |||
> elimRightPlusLTE : {a, b, c, d : Nat} ->
>                    LTE (a + c) (b + d) -> c = d -> LTE a b
> elimRightPlusLTE {a} {b} {c = Z} {d = Z} acLTEbd _ = s2 where
>   s1 : LTE a (b + Z)
>   s1 = replace {P = \ ZUZ => LTE ZUZ (b + Z)} (plusZeroRightNeutral a) acLTEbd
>   s2 : LTE a b
>   s2 = replace {P = \ ZUZ => LTE a ZUZ} (plusZeroRightNeutral b) s1
> elimRightPlusLTE {a} {b} {c = Z} {d = S n} _ ZEQSn = absurd ZEQSn
> elimRightPlusLTE {a} {b} {c = S m} {d = Z} _ SmEQZ = void (SIsNotZ SmEQZ)
> elimRightPlusLTE {a} {b} {c = S m} {d = S n} aSmLTEbSn SmEQSn = s4 where
>   s1 : LTE (a + S m) (b + S n)
>   s1 = aSmLTEbSn
>   s2 : LTE (a + m) (b + n)
>   s2 = elimSuccRightLTEPlus s1
>   s3 : m = n
>   s3 = succInjective m n SmEQSn
>   s4 : LTE a b
>   s4 = elimRightPlusLTE {a = a} {b = b} {c = m} {d = n} s2 s3
> %freeze elimRightPlusLTE

Properties of |LTE| and |mult|:

> |||
> monotoneNatMultLTE : {a, b, c, d  : Nat} ->
>                      LTE a b -> LTE c d -> LTE (a * c) (b * d)
> monotoneNatMultLTE {a = Z}   {b}       {c} {d} _ _ = LTEZero
> monotoneNatMultLTE {a = S m} {b = Z}   {c} {d} aLTEb _ = absurd aLTEb
> monotoneNatMultLTE {a = S m} {b = S n} {c} {d} (LTESucc mLTEn) cLTEd = s3 where
>   s1 : LTE (c + m * c) (d + n * d)
>   s1 = monotoneNatPlusLTE {a = c} {b = d} {c = m * c} {d = n * d}
>        cLTEd (monotoneNatMultLTE {a = m} {b = n} {c = c} {d = d} mLTEn cLTEd)
>   s2 : LTE ((S m) * c) (d + n * d)
>   s2 = replace {P = \ ZUZ => LTE ZUZ (d + n * d)} Refl s1
>   s3 : LTE ((S m) * c) ((S n) * d)
>   s3 = replace {P = \ ZUZ => LTE ((S m) * c) ZUZ} Refl s2
> %freeze monotoneNatMultLTE

> |||
> elimRightMultLTE : {a, b, c, d : Nat} ->
>                    LTE (a * c) (b * d) -> c = d -> Not (c = Z) -> LTE a b
> elimRightMultLTE {a = Z}   {b}       {c}       {d} _       _    _      = LTEZero
> elimRightMultLTE {a = S m} {b = Z}   {c = Z}   {d} _       _    contra = void (contra Refl)
> elimRightMultLTE {a = S m} {b = Z}   {c = S n} {d} acLTEbd _    _      = absurd acLTEbd
> elimRightMultLTE {a = S m} {b = S n} {c}       {d} acLTEbd cEQd ncEQZ  = s6 where
>   s1 : LTE (c + m * c) (d + n * d)
>   s1 = acLTEbd
>   s2 : LTE (m * c + c) (d + n * d)
>   s2 = replace {P = \ ZUZ => LTE ZUZ (d + n * d)} (plusCommutative c (m * c)) s1
>   s3 : LTE (m * c + c) (n * d + d)
>   s3 = replace {P = \ ZUZ => LTE (m * c + c) ZUZ} (plusCommutative d (n * d)) s2
>   s4 : LTE (m * c) (n * d)
>   s4 = elimRightPlusLTE s3 cEQd
>   s5 : LTE m n
>   s5 = elimRightMultLTE s4 cEQd ncEQZ
>   s6 : LTE (S m) (S n)
>   s6 = LTESucc s5
> %freeze elimRightMultLTE

> {-

> ---}


text:
import Data.List.Views

-- total
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (MkPair (snocList input1) (snocList input2))
  isSuffix [] input2 | (Empty, s) = True
  isSuffix input1 [] | (s, Empty) = False
  isSuffix (xs ++ [x]) (ys ++ [y]) | (MkPair (Snoc x xs xsrec) (Snoc y ys ysrec))
     = if x == y
          then isSuffix xs ys | (MkPair xsrec ysrec)
          else False


text:
ff : (a -> b) -> Not (Not a) -> Not (Not b)
ff ab nna nb = nna $ nb . ab

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Control.Linear

%default total

public export
interface Applicative m => LMonad m where
  (>>=) : (1 _ : m a) -> (1 f : ((_ : a) -> m b)) -> m b

export
lfoldlM : (Foldable t, LMonad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
lfoldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)


text:
module Main

import Data.Vect

{-
  This actually won't type check.

  Even though `a` is implementing the Decidable Equality interface,
  at some point the recursion might end up calling `removeElem value []`
  which this function is not defined for (since [] is a Vect Z a).

  So there's really no guarantee that the value will appear in the vector,
  and thus it's possible to reach the end of the vector without ever finding it.

  Some options here would be

  1. to consider the case for `[]`, and change the signature to return
     `Maybe (Vect n a)` -- if we reach the empty case, we might as well return
      Nothing.

  2. Return a dependant pair (length ** Vect lenght a) so we don't make an
     assumption on the length

  3. Have a type-level predicate that ensures that the element is in the vector
-}
removeElem__nope : DecEq a => (value : a) -> (xs : Vect (S n) a) -> Vect n a
removeElem__nope value (x :: xs) = case decEq value x of
                                  Yes prf => xs
                                  No contr => ?x_removeElem_value_xs

{-
  Let's implement option 3 by defining a specific type that tells us that a
  given element is indeed part of the vector

  Elem is actually already part of Data.Vect, so here it's defined as Elem'
  but we'll use Data.Vect.Elem instead
-}

data Elem' : a -> Vect k a -> Type where
  -- x is the first value of the vector
  Here : Elem' x (x :: xs)

  -- if x is in xs, it's also in y :: xs
  There : (later : Elem' x xs) -> Elem' x (y :: xs)

oneInVector : Elem 1 [1,2,3]
oneInVector = Here

somewhereElseInVector : Elem 1 [2,3,1]
somewhereElseInVector = There (There Here)

notInVector : Elem 1 [3,4]
notInVector = There (There ?notInVector_rhs2)

removeElemWithProof : (value : a) ->
                      (xs : Vect (S n) a ) ->
                      (prf : Elem value xs) ->
                      Vect n a
removeElemWithProof value (value :: ys) Here = ys
removeElemWithProof { n = Z } value (y :: []) (There later) = absurd later
removeElemWithProof { n = (S k) } value (y :: ys) (There later) =
  y :: removeElemWithProof value ys later

removeAutoProofed : (value : a) ->
                    (xs : Vect (S n) a) ->
                    {auto prf : Elem value xs} ->
                    Vect n a
removeAutoProofed value xs {prf} = removeElemWithProof value xs prf

removeElem : (value : a) ->
             (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a
removeElem value (value :: ys) { prf = Here  } = ys
removeElem { n = Z } value (y :: []) { prf = There later } = absurd later
removeElem { n = (S k) } value (y :: ys) { prf = There later } =
  y :: removeElem value ys

{-
  Now let's try to make a Letter data type that will only accept being
  constructed with alpha characters
-}

Alphabet : Vect 52 Char
Alphabet = ['a',
           'b',
           'c',
           'd',
           'e',
           'f',
           'g',
           'h',
           'i',
           'j',
           'k',
           'l',
           'm',
           'n',
           'o',
           'p',
           'q',
           'r',
           's',
           't',
           'u',
           'v',
           'w',
           'x',
           'y',
           'z',
           'A',
           'B',
           'C',
           'D',
           'E',
           'F',
           'G',
           'H',
           'I',
           'J',
           'K',
           'L',
           'M',
           'N',
           'O',
           'P',
           'Q',
           'R',
           'S',
           'T',
           'U',
           'V',
           'W',
           'X',
           'Y',
           'Z']

data Letter : Char -> Type where
  MkLetter : (c : Char) -> { auto prf : Elem c Alphabet } -> Letter c

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module TTImp.Elab.ImplicitBind
-- Machinery needed for handling implicit name bindings (either pattern
-- variables or unbound implicits as type variables)

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.UnifyState
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

import Data.List
import Libraries.Data.NameMap

%default covering

-- Make a hole for an unbound implicit in the outer environment
export
mkOuterHole : {vars : _} ->
              {auto e : Ref EST (EState vars)} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              Name -> Env Term vars -> Maybe (Glued vars) ->
              Core (Term vars, Term vars)
mkOuterHole loc rig n topenv (Just expty_in)
    = do est <- get EST
         let sub = subEnv est
         expected <- getTerm expty_in
         case shrinkTerm expected sub of
              -- Can't shrink so rely on unification with expected type later
              Nothing => mkOuterHole loc rig n topenv Nothing
              Just exp' =>
                  do let env = outerEnv est
                     tm <- implBindVar loc rig env n exp'
                     pure (embedSub sub tm, embedSub sub exp')
mkOuterHole loc rig n topenv Nothing
    = do est <- get EST
         let sub = subEnv est
         let env = outerEnv est
         nm <- genName ("type_of_" ++ nameRoot n)
         ty <- metaVar loc erased env nm (TType loc)
         log "elab.implicits" 10 $ "Made metavariable for type of " ++ show n ++ ": " ++ show nm
         put EST (addBindIfUnsolved nm rig Explicit topenv (embedSub sub ty) (TType loc) est)
         tm <- implBindVar loc rig env n ty
         pure (embedSub sub tm, embedSub sub ty)

-- Make a hole standing for the pattern variable, which we'll instantiate
-- with a bound pattern variable later.
-- Returns the hole term, its expected type (this is the type we'll use when
-- we see the name later) and the type the binder will need to be when we
-- instantiate it.
export
mkPatternHole : {vars' : _} ->
                {auto e : Ref EST (EState vars')} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                FC -> RigCount -> Name -> Env Term vars' -> BindMode ->
                Maybe (Glued vars') ->
                Core (Term vars', Term vars', Term vars')
mkPatternHole loc rig n env (PI _) exp
    = do (tm, exp) <- mkOuterHole loc rig n env exp
         pure (tm, exp, exp)
mkPatternHole {vars'} loc rig n topenv imode (Just expty_in)
    = do est <- get EST
         let sub = subEnv est
         let env = outerEnv est
         expected <- getTerm expty_in
         case bindInner topenv expected sub of
              Nothing => mkPatternHole loc rig n topenv imode Nothing
              Just exp' =>
                  do tm <- implBindVar loc rig env n exp'
                     pure (apply loc (embedSub sub tm) (mkArgs sub),
                           expected,
                           embedSub sub exp')
  where
    mkArgs : {vs : _} -> SubVars newvars vs -> List (Term vs)
    mkArgs SubRefl = []
    mkArgs (DropCons p) = Local loc Nothing 0 First :: map weaken (mkArgs p)
    mkArgs _ = []

    -- This is for the specific situation where we're pattern matching on
    -- function types, which is realistically the only time we'll legitimately
    -- encounter a type variable under a binder
    bindInner : {vs : _} ->
                Env Term vs -> Term vs -> SubVars newvars vs ->
                Maybe (Term newvars)
    bindInner env ty SubRefl = Just ty
    bindInner {vs = x :: _} (b :: env) ty (DropCons p)
        = bindInner env (Bind loc x b ty) p
    bindInner _ _ _ = Nothing

mkPatternHole loc rig n env _ _
    = throw (GenericMsg loc ("Unknown type for pattern variable " ++ show n))

-- For any of the 'bindIfUnsolved' - these were added as holes during
-- elaboration, but are as yet unsolved, so create a pattern variable for
-- them and unify.
-- (This is only when we're in a mode that allows unbound implicits)
bindUnsolved : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto e : Ref EST (EState vars)} ->
               {auto u : Ref UST UState} ->
               FC -> ElabMode -> BindMode -> Core ()
bindUnsolved fc elabmode NONE = pure ()
bindUnsolved {vars} fc elabmode _
    = do est <- get EST
         defs <- get Ctxt
         let bifs = bindIfUnsolved est
         log "elab.implicits" 5 $ "Bindable unsolved implicits: " ++ show (map fst bifs)
         traverse_ (mkImplicit defs (outerEnv est) (subEnv est)) (bindIfUnsolved est)
  where
    makeBoundVar : {outer, vs : _} ->
                   Name -> RigCount -> PiInfo (Term vs) -> Env Term outer ->
                   SubVars outer vs -> SubVars outer vars ->
                   Term vs -> Core (Term vs)
    makeBoundVar n rig p env sub subvars expected
        = case shrinkTerm expected sub of
               Nothing => do tmn <- toFullNames expected
                             throw (GenericMsg fc ("Can't bind implicit " ++ show n ++ " of type " ++ show tmn))
               Just exp' =>
                    do impn <- genVarName (nameRoot n)
                       tm <- metaVar fc rig env impn exp'
                       est <- get EST
                       let p' : PiInfo (Term vars) = forgetDef p
                       put EST (record { toBind $= ((impn, NameBinding rig p'
                                                             (embedSub subvars tm)
                                                             (embedSub subvars exp')) ::) } est)
                       pure (embedSub sub tm)

    mkImplicit : {outer : _} ->
                 Defs -> Env Term outer -> SubVars outer vars ->
                 (Name, RigCount, (vars' **
                     (Env Term vars', PiInfo (Term vars'), Term vars', Term vars', SubVars outer vars'))) ->
                 Core ()
    mkImplicit defs outerEnv subEnv (n, rig, (vs ** (env, p, tm, exp, sub)))
        = do Just (Hole _ _) <- lookupDefExact n (gamma defs)
                  | _ => pure ()
             bindtm <- makeBoundVar n rig p outerEnv
                                    sub subEnv
                                    !(normaliseHoles defs env exp)
             logTerm "elab.implicits" 5 ("Added unbound implicit") bindtm
             ignore $ unify (case elabmode of
                         InLHS _ => inLHS
                         _ => inTerm)
                   fc env tm bindtm

swapIsVarH : {idx : Nat} -> (0 p : IsVar nm idx (x :: y :: xs)) ->
             Var (y :: x :: xs)
swapIsVarH First = MkVar (Later First)
swapIsVarH (Later p) = swapP p -- it'd be nice to do this all at the top
                               -- level, but that will need an improvement
                               -- in erasability checking
  where
    swapP : forall name . {idx : _} -> (0 p : IsVar name idx (y :: xs)) ->
            Var (y :: x :: xs)
    swapP First = MkVar First
    swapP (Later x) = MkVar (Later (Later x))

swapIsVar : (vs : List Name) ->
            {idx : Nat} -> (0 p : IsVar nm idx (vs ++ x :: y :: xs)) ->
            Var (vs ++ y :: x :: xs)
swapIsVar [] prf = swapIsVarH prf
swapIsVar (x :: xs) First = MkVar First
swapIsVar (x :: xs) (Later p)
    = let MkVar p' = swapIsVar xs p in MkVar (Later p')

swapVars : {vs : List Name} ->
           Term (vs ++ x :: y :: ys) -> Term (vs ++ y :: x :: ys)
swapVars (Local fc x idx p)
    = let MkVar p' = swapIsVar _ p in Local fc x _ p'
swapVars (Ref fc x name) = Ref fc x name
swapVars (Meta fc n i xs) = Meta fc n i (map swapVars xs)
swapVars {vs} (Bind fc x b scope)
    = Bind fc x (map swapVars b) (swapVars {vs = x :: vs} scope)
swapVars (App fc fn arg) = App fc (swapVars fn) (swapVars arg)
swapVars (As fc s nm pat) = As fc s (swapVars nm) (swapVars pat)
swapVars (TDelayed fc x tm) = TDelayed fc x (swapVars tm)
swapVars (TDelay fc x ty tm) = TDelay fc x (swapVars ty) (swapVars tm)
swapVars (TForce fc r tm) = TForce fc r (swapVars tm)
swapVars (PrimVal fc c) = PrimVal fc c
swapVars (Erased fc i) = Erased fc i
swapVars (TType fc) = TType fc

-- Push an explicit pi binder as far into a term as it'll go. That is,
-- move it under implicit binders that don't depend on it, and stop
-- when hitting any non-implicit binder
push : {vs : _} ->
       FC -> (n : Name) -> Binder (Term vs) -> Term (n :: vs) -> Term vs
push ofc n b tm@(Bind fc (PV x i) (Pi fc' c Implicit ty) sc) -- only push past 'PV's
    = case shrinkTerm ty (DropCons SubRefl) of
           Nothing => -- needs explicit pi, do nothing
                      Bind ofc n b tm
           Just ty' => Bind fc (PV x i) (Pi fc' c Implicit ty')
                            (push ofc n (map weaken b) (swapVars {vs = []} sc))
push ofc n b tm = Bind ofc n b tm

-- Move any implicit arguments as far to the left as possible - this helps
-- with curried applications
-- We only do this for variables named 'PV', since they are the unbound
-- implicits, and we don't want to move any given by the programmer
liftImps : {vars : _} ->
           BindMode -> (Term vars, Term vars) -> (Term vars, Term vars)
liftImps (PI _) (tm, TType fc) = (liftImps' tm, TType fc)
  where
    liftImps' : {vars : _} ->
                Term vars -> Term vars
    liftImps' (Bind fc (PV n i) b@(Pi _ _ Implicit _) sc)
        = Bind fc (PV n i) b (liftImps' sc)
    liftImps' (Bind fc n b@(Pi _ _ _ _) sc)
        = push fc n b (liftImps' sc)
    liftImps' tm = tm
liftImps _ x = x

-- Bind implicit arguments, returning the new term and its updated type
bindImplVars : FC -> BindMode ->
               Defs ->
               Env Term vars ->
               List (Name, ImplBinding vars) ->
               Term vars -> Term vars -> (Term vars, Term vars)
bindImplVars fc NONE gam env imps_in scope scty = (scope, scty)
bindImplVars {vars} fc mode gam env imps_in scope scty
    = let imps = map (\ (x, bind) => (tidyName x, x, bind)) imps_in in
          getBinds imps None scope scty
  where
    -- Turn the pattern variable name into the user's original choice,
    -- now that there's no longer a risk of clash
    tidyName : Name -> Name
    tidyName (NS _ n) = tidyName n
    tidyName (PV n _) = tidyName n
    tidyName (Nested n inner) = tidyName inner
    tidyName n = n

    getBinds : (imps : List (Name, Name, ImplBinding vs)) ->
               Bounds new -> (tm : Term vs) -> (ty : Term vs) ->
               (Term (new ++ vs), Term (new ++ vs))
    getBinds [] bs tm ty = (refsToLocals bs tm, refsToLocals bs ty)
    getBinds {new} ((n, metan, NameBinding c p _ bty) :: imps) bs tm ty
        = let (tm', ty') = getBinds imps (Add n metan bs) tm ty
              bty' = refsToLocals bs bty in
              case mode of
                   PI c =>
                      (Bind fc _ (Pi fc c Implicit bty') tm',
                       TType fc)
                   _ =>
                      (Bind fc _ (PVar fc c (map (weakenNs (sizeOf bs)) p) bty') tm',
                       Bind fc _ (PVTy fc c bty') ty')
    getBinds ((n, metan, AsBinding c _ _ bty bpat) :: imps) bs tm ty
        = let (tm', ty') = getBinds imps (Add n metan bs) tm ty
              bty' = refsToLocals bs bty
              bpat' = refsToLocals bs bpat in
              (Bind fc _ (PLet fc c bpat' bty') tm',
               Bind fc _ (PLet fc c bpat' bty') ty')

normaliseHolesScope : {auto c : Ref Ctxt Defs} ->
                      {vars : _} ->
                      Defs -> Env Term vars -> Term vars -> Core (Term vars)
normaliseHolesScope defs env (Bind fc n b sc)
    = pure $ Bind fc n b
                  !(normaliseHolesScope defs
                   -- use Lam because we don't want it reducing in the scope
                   (Lam fc (multiplicity b) Explicit (binderType b) :: env) sc)
normaliseHolesScope defs env tm = normaliseHoles defs env tm

export
bindImplicits : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
                FC -> BindMode ->
                Defs -> Env Term vars ->
                List (Name, ImplBinding vars) ->
                Term vars -> Term vars -> Core (Term vars, Term vars)
bindImplicits fc NONE defs env hs tm ty = pure (tm, ty)
bindImplicits {vars} fc mode defs env hs tm ty
   = do hs' <- traverse nHoles hs
        pure $ liftImps mode $ bindImplVars fc mode defs env hs' tm ty
  where
    nHoles : (Name, ImplBinding vars) -> Core (Name, ImplBinding vars)
    nHoles (n, NameBinding c p tm ty)
        = pure (n, NameBinding c p tm !(normaliseHolesScope defs env ty))
    nHoles (n, AsBinding c p tm ty pat)
        = pure (n, AsBinding c p tm !(normaliseHolesScope defs env ty) pat)

export
implicitBind : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               Name -> Core ()
implicitBind n
    = do defs <- get Ctxt
         Just (Hole _ _) <- lookupDefExact n (gamma defs)
             | _ => pure ()
         updateDef n (const (Just ImpBind))
         removeHoleName n

-- 'toBind' are the names which are to be implicitly bound (pattern bindings and
-- unbound implicits).
-- Return the names in the order they should be bound: i.e. respecting
-- dependencies between types, and putting @-patterns last because their
-- value is determined from the patterns
export
getToBind : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto e : Ref EST (EState vars)} ->
            {auto u : Ref UST UState} ->
            FC -> ElabMode -> BindMode ->
            Env Term vars -> (excepts : List Name) ->
            Core (List (Name, ImplBinding vars))
getToBind fc elabmode NONE env excepts
    = pure [] -- We should probably never get here, but for completeness...
getToBind {vars} fc elabmode impmode env excepts
    = do solveConstraints (case elabmode of
                                InLHS _ => inLHS
                                _ => inTerm) Normal
         bindUnsolved fc elabmode impmode
         solveConstraints (case elabmode of
                                InLHS _ => inLHS
                                _ => inTerm) Normal
         defs <- get Ctxt
         est <- get EST
         let tob = reverse $ filter (\x => not (fst x `elem` excepts)) $
                             toBind est
         -- Make sure all the hole names are normalised in the implicitly
         -- bound types, because otherwise we'll bind them too
         res <- normImps defs [] tob
         let hnames = map fst res
         -- Return then in dependency order
         let res' = depSort hnames res
         log "elab.implicits" 10 $ "Bound names: " ++ show res
         log "elab.implicits" 10 $ "Sorted: " ++ show res'
         pure res'
  where
    normBindingTy : Defs -> ImplBinding vars -> Core (ImplBinding vars)
    normBindingTy defs (NameBinding c p tm ty)
        = pure $ NameBinding c p tm !(normaliseHoles defs env ty)
    normBindingTy defs (AsBinding c p tm ty pat)
        = pure $ AsBinding c p tm !(normaliseHoles defs env ty)
                                  !(normaliseHoles defs env pat)

    normImps : Defs -> List Name -> List (Name, ImplBinding vars) ->
               Core (List (Name, ImplBinding vars))
    normImps defs ns [] = pure []
    normImps defs ns ((PV n i, bty) :: ts)
        = do logTermNF "elab.implicits" 10 ("Implicit pattern var " ++ show (PV n i)) env
                       (bindingType bty)
             if PV n i `elem` ns
                then normImps defs ns ts
                else do rest <- normImps defs (PV n i :: ns) ts
                        pure ((PV n i, !(normBindingTy defs bty)) :: rest)
    normImps defs ns ((n, bty) :: ts)
        = do tmnf <- normaliseHoles defs env (bindingTerm bty)
             logTerm "elab.implicits" 10 ("Normalising implicit " ++ show n) tmnf
             case getFnArgs tmnf of
                -- n reduces to another hole, n', so treat it as that as long
                -- as it isn't already done
                (Meta _ n' i margs, args) =>
                    do hole <- isCurrentHole i
                       if hole && not (n' `elem` ns)
                          then do rest <- normImps defs (n' :: ns) ts
                                  btynf <- normBindingTy defs bty
                                  pure ((n', btynf) :: rest)
                          else normImps defs ns ts
                _ => -- Unified to something concrete, so drop it
                     normImps defs ns ts

    -- Insert the hole/binding pair into the list before the first thing
    -- which refers to it
    insert : (Name, ImplBinding vars) -> List Name -> List Name ->
             List (Name, ImplBinding vars) ->
             List (Name, ImplBinding vars)
    insert h ns sofar [] = [h]
    insert (hn, bty) ns sofar ((hn', bty') :: rest)
        = let used = filter (\n => elem n ns) (keys (bindingMetas bty')) in
              -- 'used' is to make sure we're only worrying about metavariables
              -- introduced in *this* expression (there may be others unresolved
              -- from elsewhere, for type inference purposes)
              if hn `elem` used
                 then (hn, bty) ::
                      (hn', bty') :: rest
                 else (hn', bty') ::
                          insert (hn, bty) ns (hn' :: sofar) rest

    -- Sort the list of implicits so that each binding is inserted *after*
    -- all the things it depends on (assumes no cycles)
    depSort : List Name -> List (Name, ImplBinding vars) ->
              List (Name, ImplBinding vars)
    depSort hnames [] = []
    depSort hnames (h :: hs) = insert h hnames [] (depSort hnames hs)

export
checkBindVar : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               {auto e : Ref EST (EState vars)} ->
               RigCount -> ElabInfo ->
               NestedNames vars -> Env Term vars ->
               FC -> UserName -> -- username is base of the pattern name
               Maybe (Glued vars) ->
               Core (Term vars, Glued vars)
checkBindVar rig elabinfo nest env fc str topexp
    = do let elabmode = elabMode elabinfo
         -- In types, don't rebind if the name is already in scope;
         -- Below, return True if we don't need to implicitly bind the name
         let False = case implicitMode elabinfo of
                          PI _ => maybe False (const True) (defined (UN str) env)
                          _ => False
               | _ => check rig elabinfo nest env (IVar fc (UN str)) topexp
         est <- get EST
         let n = PV (UN str) (defining est)
         noteLHSPatVar elabmode (UN str)
         notePatVar n
         est <- get EST

         whenJust (isConcreteFC fc) $ \nfc => do
           log "ide-mode.highlight" 7 $ "getNameType is adding Bound: " ++ show n
           addSemanticDecorations [(nfc, Bound, Just n)]

         case lookup n (boundNames est) of
              Nothing =>
                do (tm, exp, bty) <- mkPatternHole fc rig n env
                                              (implicitMode elabinfo)
                                              topexp
                   -- In PI mode, it's invertible like any other pi bound thing
                   case implicitMode elabinfo of
                        PI _ => setInvertible fc n
                        _ => pure ()
                   log "elab.implicits" 5 $ "Added Bound implicit " ++ show (n, (rig, tm, exp, bty))
                   est <- get EST
                   put EST (record { boundNames $= ((n, NameBinding rig Explicit tm exp) ::),
                                     toBind $= ((n, NameBinding rig Explicit tm bty) :: ) } est)

                   log "metadata.names" 7 $ "checkBindVar is adding ↓"
                   addNameType fc (UN str) env exp
                   addNameLoc fc (UN str)

                   checkExp rig elabinfo env fc tm (gnf env exp) topexp
              Just bty =>
                do -- Check rig is consistent with the one in bty, and
                   -- update if necessary
                   combine (UN str) rig (bindingRig bty)
                   let tm = bindingTerm bty
                   let ty = bindingType bty

                   log "metadata.names" 7 $ "checkBindVar is adding ↓"
                   addNameType fc (UN str) env ty
                   addNameLoc fc (UN str)

                   checkExp rig elabinfo env fc tm (gnf env ty) topexp
  where
    updateRig : Name -> RigCount -> List (Name, ImplBinding vars) ->
                List (Name, ImplBinding vars)
    updateRig n c [] = []
    updateRig n c ((bn, r) :: bs)
        = if n == bn
             then case r of
                  NameBinding _ p tm ty => (bn, NameBinding c p tm ty) :: bs
                  AsBinding _ p tm ty pat => (bn, AsBinding c p tm ty pat) :: bs
             else (bn, r) :: updateRig n c bs

    -- Two variables are incompatble if at least one of them appears in a linear position
    -- and their sum is bigger than 1
    isIncompatible : RigCount -> RigCount -> Bool
    isIncompatible l r = (isLinear l || isLinear r) && linear < l |+| r

    combine : Name -> RigCount -> RigCount -> Core ()
    combine n l r = when (isIncompatible l r)
                         (throw (LinearUsed fc 2 n))

checkPolyConstraint :
            {auto c : Ref Ctxt Defs} ->
            PolyConstraint -> Core ()
checkPolyConstraint (MkPolyConstraint fc env arg x y)
    = do defs <- get Ctxt
         -- If 'x' is a metavariable and 'y' is concrete, that means we've
         -- ended up putting something too concrete in for a polymorphic
         -- argument
         xnf <- continueNF defs env x
         case xnf of
              NApp _ (NMeta _ _ _) _ =>
                   do ynf <- continueNF defs env y
                      if !(concrete defs env ynf)
                         then do empty <- clearDefs defs
                                 throw (MatchTooSpecific fc env arg)
                         else pure ()
              _ => pure ()
checkPolyConstraint _ = pure ()

solvePolyConstraint :
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            PolyConstraint -> Core ()
solvePolyConstraint (MkPolyConstraint fc env arg x y)
    = do defs <- get Ctxt
         -- If the LHS of the constraint isn't a metavariable, we can solve
         -- the constraint
         case !(continueNF defs env x) of
              xnf@(NApp _ (NMeta _ _ _) _) => pure ()
              t => do res <- unify inLHS fc env t !(continueNF defs env y)
                      -- If there's any constraints, it just means we didn't
                      -- solve anything and it won't help the check
                      pure ()

export
checkBindHere : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                {auto e : Ref EST (EState vars)} ->
                RigCount -> ElabInfo ->
                NestedNames vars -> Env Term vars ->
                FC -> BindMode -> RawImp ->
                Maybe (Glued vars) ->
                Core (Term vars, Glued vars)
checkBindHere rig elabinfo nest env fc bindmode tm exp
    = do est <- get EST
         let oldenv = outerEnv est
         let oldsub = subEnv est
         let oldbif = bindIfUnsolved est
         let dontbind = map fst (toBind est)
         -- Set the binding environment in the elab state - unbound
         -- implicits should have access to whatever is in scope here
         put EST (updateEnv env SubRefl [] est)
         constart <- getNextEntry
         (tmv, tmt) <- check rig (record { implicitMode = bindmode,
                                           bindingVars = True }
                                         elabinfo)
                             nest env tm exp
         let solvemode = case elabMode elabinfo of
                              InLHS c => inLHS
                              _ => inTerm
         solveConstraints solvemode Normal

         ust <- get UST
         catch (retryDelayed solvemode (delayedElab ust))
               (\err =>
                  do ust <- get UST
                     put UST (record { delayedElab = [] } ust)
                     throw err)

         -- Check all the patterns standing for polymorphic variables are
         -- indeed polymorphic
         ust <- get UST
         let cons = polyConstraints ust
         put UST (record { polyConstraints = [] } ust)
         traverse_ solvePolyConstraint cons
         traverse_ checkPolyConstraint cons

         solveConstraintsAfter constart
                          (case elabMode elabinfo of
                                InLHS c => inLHS
                                _ => inTerm) Defaults
         checkDots -- Check dot patterns unifying with the claimed thing
                   -- before binding names

         logTerm "elab.implicits" 5 "Binding names" tmv
         logTermNF "elab.implicits" 5 "Normalised" env tmv
         argImps <- getToBind fc (elabMode elabinfo)
                              bindmode env dontbind
         clearToBind dontbind
         est <- get EST
         put EST (updateEnv oldenv oldsub oldbif
                     (record { boundNames = [] } est))
         ty <- getTerm tmt
         defs <- get Ctxt
         (bv, bt) <- bindImplicits fc bindmode
                                   defs env argImps
                                   !(normaliseHoles defs env tmv)
                                   !(normaliseHoles defs env ty)
         traverse_ implicitBind (map fst argImps)
         checkExp rig elabinfo env fc bv (gnf env bt) exp


text:
module Doc.Main

import JS
import Doc.Tutorial

main : IO ()
main = runJS Doc.Tutorial.prog


text:
> module Data.Fin.Extensions
> import Data.Fin
> import Data.List
> import Data.List.TypeEnumeration

> embedNatAsFin : (n : Nat) -> (m : Nat) -> {pf: LT m n} -> Fin n
> embedNatAsFin Z _ {pf=_} impossible
> embedNatAsFin (S _) Z {pf = _} = FZ
> embedNatAsFin (S j) (S k) {pf = LTESucc x} = FS (embedNatAsFin j k {pf=x})

> Uninhabited (LT (S j) (S Z)) where
>    uninhabited (LTESucc x) = uninhabited x

> getLesserFins : {n:Nat} -> (f : Fin (S n)) -> List (Fin (S n))
> getLesserFins FZ = FZ :: []
> getLesserFins (FS x) = (FS x) :: (getLesserFins (weaken x))

> getLesserFinsContains : (x : Fin (S k)) -> Elem x (getLesserFins (last {n = k}))
> getLesserFinsContains {k = Z} FZ = ?getLesserFinsContains_rhs_3
> getLesserFinsContains {k = Z} (FS x) impossible
> getLesserFinsContains {k = (S k)} x = ?getLesserFinsContains_rhs_2

> natToListFin' : (n : Nat) -> List (Fin (S n))
> natToListFin' t = natToListFinInternal t t {pf=lteRefl} where
>   natToListFinInternal : (k:Nat) -> (l : Nat) -> {auto pf: LT (k) (S l)} -> List (Fin (S l))
>   natToListFinInternal Z Z {pf = _}= [FZ]
>   natToListFinInternal (S j) Z {pf} = absurd (uninhabited pf)
>   natToListFinInternal (S j) m {pf} =
>       let headVal = (embedNatAsFin (S m) (S j) {pf=pf}) in
>           let tailVal = natToListFinInternal j m {pf = (lteSuccLeft pf)} in
>               headVal :: tailVal

> safeStrengthen : (f : Fin (S n)) -> (contra : (f = last {n=n}) -> Void) -> Fin n
> safeStrengthen {n=Z} FZ contra = absurd (contra Refl)
> safeStrengthen {n=(S k)} FZ contra = FZ
> safeStrengthen {n=(S k)} (FS x) contra = ?ssh_2

> natToListFinIsAll : (n : Nat) -> All (getLesserFins (last {n=n}))
> natToListFinIsAll Z =  ?isAll
> natToListFinIsAll (S k) = \f =>
>   case (decEq f (last {n=(S k)})) of
>       Yes pf => ?isAll1
>       No contra => ?isAll2

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets