text:
module Bautzen.Game

import public Bautzen.Combats
import public Bautzen.GameUnit
import public Bautzen.Game.Combat
import public Bautzen.Game.Core
import public Bautzen.Game.Move
import public Bautzen.Game.Supply
import public Bautzen.Game.Turn
import public Bautzen.Pos
import public Bautzen.Terrain
import public Bautzen.Game.Map

import Bautzen.SExp

import Data.List.Extra

import Data.Fin
import Data.Nat

export
act : (game : Game) -> Command (curSegment game) -> Either GameError Event
act (MkGame _ (MkGameState _ side Move units) gameMap) (MoveTo unitName to) = moveTo side units gameMap unitName to
act (MkGame _ (MkGameState _ side (Combat NoCombat) units) gameMap) (AttackWith unitNames target) = attackWith side units gameMap unitNames target
act game NextSegment = nextSegment game
act (MkGame _ (MkGameState _ side (Combat (AssignTacticalSupport combatSide combat)) units) gameMap) (TacticalSupport unitNames) =
  supportWith side combatSide units gameMap unitNames combat
act (MkGame _ (MkGameState _ side (Combat (Resolve combat)) units) gameMap) (ResolveCombat combat) =
  resolveCombat side combat
act (MkGame _ (MkGameState _ side (Combat (ApplyLosses lossSide combat)) units) gameMap) (LoseStep unitName) =
  loseStep side lossSide combat unitName

applyTacticalSupportEvent : Side -> CombatState -> List (GameUnit, Pos) -> GameState -> GameState
applyTacticalSupportEvent supportedSide (MkCombatState combatHex attackers defenders losses) units game =
  if side game == supportedSide
  then record { segment = Combat (AssignTacticalSupport (flipSide supportedSide)
                                       (MkCombatState combatHex
                                        (record { tacticalSupport = units } attackers)
                                        defenders
                                        losses)) } game
  else record { segment = Combat (AssignStrategicSupport (flipSide supportedSide)
                                       (MkCombatState combatHex
                                        attackers
                                        (record { tacticalSupport = units } defenders)
                                        losses)) } game

applySupplyColumnUsedEvent :  Side -> CombatState -> Pos -> GameState -> GameState
applySupplyColumnUsedEvent supportedSide (MkCombatState combatHex attackers defenders losses) hex game =
  if side game == supportedSide
  then record { segment = Combat (AssignStrategicSupport supportedSide
                                       (MkCombatState combatHex
                                        (record { strategicSupport $= (+1) } attackers)
                                        defenders
                                        losses)) } game
  else record { segment = Combat (AssignStrategicSupport supportedSide
                                       (MkCombatState combatHex
                                        attackers
                                        (record { strategicSupport $= (+1) } defenders)
                                        losses)) } game

-- TODO handle case where there are more losses to applies than units
applyStepLostEvent :
  Side -> GameUnit -> Losses -> CombatState -> GameState -> GameState
applyStepLostEvent lossSide unit newLosses state game@(MkGameState turn side segment units) =
  record { segment = newSegment, units = reduced } game
  where
    reduced : List (GameUnit, Pos)
    reduced = reduce unit units

    newState : CombatState
    newState = record { losses = Just newLosses } state

    newSegment : GameSegment
    newSegment = case newLosses of
                  (Z /> Z) => Combat NoCombat -- combat is completely resolved
                  (Z /> def) => Combat $ ApplyLosses (flipSide side) newState
                  (atk /> _) => Combat $ ApplyLosses side newState

applyEvent : Event -> GameState -> GameState
applyEvent (Moved unit from to cost) (MkGameState turn side segment units) =
  MkGameState turn side segment (updateMovedUnit unit to (Terrain.toNat cost) units)
applyEvent (CombatEngaged atk def tgt) game =
  record { segment = Combat (AssignTacticalSupport (side game)
                     (MkCombatState tgt
                       (MkEngagedUnits atk [] 0)
                       (MkEngagedUnits def [] 0)
                       Nothing)) } game
applyEvent (TacticalSupportProvided _ units) game =
  case segment game of
    (Combat (AssignTacticalSupport supSide combat)) => applyTacticalSupportEvent supSide combat units game
    _ => game -- TODO make this impossible to happen
applyEvent (SupplyColumnUsed side pos) game =
  case segment game of
    (Combat (AssignStrategicSupport supSide combat)) => applySupplyColumnUsedEvent supSide combat pos game
    _ => game -- TODO make this impossible to happen
applyEvent (CombatResolved state losses) game =
  case segment game of
    (Combat (Resolve _)) => record { segment = (Combat $ ApplyLosses (side game) (record { losses = Just losses } state)) } game
    _ => game -- TODO make this impossible to happen
applyEvent (StepLost unitSide unit newLosses) game =
  case segment game of
    (Combat (ApplyLosses lossSide combatState)) => applyStepLostEvent unitSide unit newLosses combatState game
    _ => game -- TODO make this impossible to happen
applyEvent (SegmentChanged from to) game =
  record { segment = to } game
applyEvent AxisTurnDone game =
  record { side = Allies, segment = Supply } game
applyEvent (TurnEnded n) game =
  record { turn = n, side = Axis, segment = Supply } game
applyEvent GameEnded game =
  record { segment = GameEnd } game

export
apply : Event -> Game -> Game
apply event (MkGame events curState gameMap) =
  MkGame (event :: events) (applyEvent event curState) gameMap

-- Queries

||| Query interface to retrieve information from a `Game`.
|||
||| Queries do not change the state of the game  but provide various
||| information, raw or computed, on its current state, in ways that
||| can be consumed by clients.
|||
||| @result the type of result produced by this instance of `Query`
public export
data Query : (result : Type) -> Type where

  ||| What's the (shortest) supply path for the given `unitName`?
  |||
  ||| Returns a list of `Pos`itions from a `SupplySource` hex to the current
  ||| position of the given unit, if there is one. Returns a `QueryError` if no
  ||| supply path can be drawn for this unit, either because there is none
  ||| or because the unit does not exist.
  ||| @unitName full name of unit to check supply for
  SupplyPath : (unitName : String) -> Query (Either QueryError (List Pos))

  ||| Retrieve the game's `Map`
  TerrainMap : Query Map

  ||| Retrieve positions of all units
  Positions : Query (List (GameUnit, Pos))

  ||| Retrieve the stage (turn, side, segment) the game is currently at
  GameStage : Query (Fin 6, Side, GameSegment)

export
Show (Query a) where
  show (SupplyPath u) = "SupplyPath " ++ show u
  show TerrainMap = "TerrainMap"
  show Positions = "Positions"
  show GameStage = "GameStage"

export
query : (ToSExp result) => (game : Game) -> (qry : Query result) -> result
query (MkGame _ (MkGameState _ side _ units) gameMap) (SupplyPath unitName) =
  case find' (sameName unitName) units of
    Nothing => Left (UnitDoesNotExist unitName)
    (Just (unit, pos)) =>
      case supplyPathTo units gameMap (supplySources (nation unit) gameMap) (unit, pos) of
        [] => Left (NoSupplyPathFor unitName pos)
        x  => Right x
query (MkGame _ (MkGameState _ side _ units) gameMap) TerrainMap = gameMap
query (MkGame _ (MkGameState _ side _ positions) _) Positions = positions
query (MkGame _ (MkGameState turn side segment _) _) GameStage = (turn, side, segment)

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Extra.OpenSSL.Random

import Control.Linear.LIO
import Extra.OpenSSL.FFI
import Extra.C.CPtr

%foreign libcrypto "RAND_bytes"
export
prim__RAND_bytes : Ptr CUInt8 -> CInt -> PrimIO CInt

export
RAND_bytes
  : LinearIO io
  => {length : Nat}
  -> (1 _ : CPtr (Bytes can_free True can_write length))
  -> L io {use=1} (CPtr (Bytes can_free can_write can_write length))
RAND_bytes (MkCPtr ptr) = do
  _ <- liftIO1 $ primIO $ prim__RAND_bytes ptr (cast $ natToInteger length)
  pure1 $ MkCPtr ptr

ext: idr


text:
module Peer

import Util
import System.Concurrency.Channels
import Data.Primitives.Views
import System
import Data.String
import Data.List
import Language.JSON
import public Network.Socket
import Channel

%access public export
%include C "c/ip.h"
%link C "c/ip.o"

record Message where
       constructor MkMsg
       msgId : String
       content : String

record PeerChannels where
       constructor MkPeerChans
       msgQueue : Channel (List Message)
       relayed : Channel (List Message)
       connChan : Channel (List Socket)

data PeerState = Joining
               | Setup
               | Running
               | Ready
               | NotReady

data PeerCmd : (resultType : Type) -> (stateIn : PeerState) ->
     (stateOut : PeerState) -> Type where
     WaitForRelayedMessages : (sock : Socket) -> (relayed : Channel (List Message)) -> PeerCmd () Joining Setup
     ListenForNewClients : (sock : Socket) -> (chans : PeerChannels) -> PeerCmd () Setup Setup
     BroadcastToClients : (chans : PeerChannels) -> PeerCmd () Setup Setup
     RecMessages : (sock : Socket) -> (ip : SocketAddress) -> (chans : PeerChannels) -> PeerCmd () Setup Setup
     ReplStart : (chans : PeerChannels) -> (ip : SocketAddress) -> (port : Int) -> PeerCmd () Setup Running
     Connect : (sock : Socket) -> (ip : SocketAddress) -> (port : Int) -> PeerCmd Int Ready Joining
     CreateSocket : PeerCmd (Either SocketError Socket) NotReady Ready

     Error : (str : String) -> PeerCmd () state Running
     Push : (chan : Channel (List ty)) -> (val : ty) -> PeerCmd () state state
     GetLine : PeerCmd String state state
     PutStrLn : (str : String) -> PeerCmd () state state
     PureCmd : (res : ty) -> PeerCmd ty state state
     (>>=) : PeerCmd a state1 state2 -> (a -> PeerCmd b state2 state3) ->
             PeerCmd b state1 state3

msgToJson : Message -> JSON
msgToJson msg = JObject [("id", JString (msgId msg)), ("content", JString (content msg))]

jsonToMsg : JSON -> Maybe Message
jsonToMsg (JObject [("id", JString msgId), ("content", JString msg)]) = Just (MkMsg msgId msg)
jsonToMsg _ = Nothing

msgListToJson : List Message -> JSON
msgListToJson msgList = JArray (map (\msg => msgToJson msg) msgList)

jsonToMsgList : JSON -> Maybe (List (Maybe Message))
jsonToMsgList (JArray msgs) = Just (map (\msg => jsonToMsg msg) msgs)
jsonToMsgList _ = Nothing

recAll : (sock : Socket) -> IO (Either SocketError String)
recAll sock = recvRec sock [] 64
  where
    partial
    recvRec : Socket -> List String -> ByteLength -> IO (Either SocketError String)
    recvRec sock acc n = do res <- recv sock n
                            case res of
                              Left c => pure (Left c)
                              Right (str, res) => let n' = min (n * 2) 65536 in
                                                  if res < n then pure (Right $ concat $ reverse $ str :: acc)
                                                  else recvRec sock (str :: acc) n'

parseIpAndPort : String -> IO (Maybe(SocketAddress, Port))
parseIpAndPort str =
  let (addrStr, portStr) = span (/= ':') str in
  case parseIPv4 addrStr of
        (IPv4Addr p1 p2 p3 p4) =>
        case parseInteger $ substr 1 (length portStr) portStr of
          Nothing => pure Nothing
          (Just port) => pure $ Just ((IPv4Addr p1 p2 p3 p4), toIntNat (fromIntegerNat port))
        _ => pure Nothing

push : (chan : Channel (List ty)) -> (elem : ty) ->
       ChannelCmd (ResultType (List ty)) (List ty) Unlocked Unlocked
push chan elem = do res <- ReadCmd chan
                    case res of
                        (Correct state) => do WriteCmd chan (elem :: state); PureCmd res
                        _ => do ReleaseLockCmd chan; PureCmd res

pop : (chan : Channel (List ty)) -> ChannelCmd (ResultType (Maybe ty)) (List ty) Unlocked Unlocked
pop chan =
  do res <- ReadCmd chan
     case res of
           (Correct state) =>
             case state of
               [] => do WriteCmd chan []; PureCmd (Correct Nothing)
               (x :: xs) => do WriteCmd chan xs; PureCmd (Correct (Just x))
           (Fatal x) => do ReleaseLockCmd chan; PureCmd (Fatal x)
           (Warning x) => do ReleaseLockCmd chan; PureCmd (Warning x)

peek : (chan : Channel (List ty)) -> ChannelCmd (ResultType (Maybe ty)) (List ty) Unlocked Unlocked
peek chan =
  do res <- ReadOnlyCmd chan
     case res of
           (Correct state) =>
             case state of
               [] => PureCmd (Correct Nothing)
               (x :: xs) => PureCmd (Correct (Just x))
           (Fatal x) => PureCmd (Fatal x)
           (Warning x) => PureCmd (Warning x)

releaseLock : (chan : (Channel (List ty))) ->
              ChannelCmd Bool (List ty) Locked Unlocked
releaseLock chan = ReleaseLockCmd chan

lockChannel : (chan : Channel (List ty)) ->
              ChannelCmd () (List ty) Unlocked Locked
lockChannel chan = do ReadCmd chan
                      PureCmd ()

getListOfChannel : (chan : Channel (List ty)) ->
                   ChannelCmd (ResultType (List ty)) (List ty) Unlocked Unlocked
getListOfChannel chan = ReadOnlyCmd chan

writeToChan : (chan : Channel (List ty)) -> (newList : List ty) -> ChannelCmd () (List ty) Locked Unlocked
writeToChan chan newList = do WriteCmd chan newList
                              PureCmd ()

readFromChan : (chan : Channel (List ty)) -> ChannelCmd (ResultType (List ty)) (List ty) Unlocked Locked
readFromChan chan = ReadCmd chan

getIP : Int -> (IO String)
getIP = foreign FFI_C "getipc" (Int -> (IO String))

parseSingleIp : String -> Maybe SocketAddress
parseSingleIp input = let parsedIp = parseIPv4 input in
                      case parsedIp of
                        (IPv4Addr p1 p2 p3 p4) => Just (IPv4Addr p1 p2 p3 p4)
                        _ => Nothing

getAllIps : Int -> IO (List String)
getAllIps startingInt = do ip <- getIP startingInt
                           if ip == "END"
                            then pure []
                            else do rest <- getAllIps (startingInt + 1)
                                    pure (ip :: rest)

printIpOptions : List (SocketAddress, Nat) -> IO ()
printIpOptions [] = pure ()
printIpOptions ((ip, nr) :: rest) = do putStrLn $ (show ip) ++ "(" ++ (show nr) ++ ")"
                                       printIpOptions rest

removeNothings : List (Maybe ty) -> List ty
removeNothings [] = []
removeNothings (Nothing :: rest) = removeNothings rest
removeNothings (Just elem :: rest) = (elem :: removeNothings rest)

selectIp : IO (SocketAddress)
selectIp = do ips <- getAllIps 0
              parsedIps <- pure (removeNothings (map parseSingleIp ips))
              zippedIps <- pure (zip parsedIps [0..(length parsedIps)])
              printIpOptions zippedIps
              input <- getLine
              case parseInteger input of
                Just option => do Just addr <- pure (index' (fromIntegerNat option) parsedIps) | Nothing => selectIp
                                  pure addr
                Nothing => selectIp

recMessages : (sock : Socket) -> (ip : SocketAddress) ->
              (chans : PeerChannels) -> IO ()
recMessages sock ip chans =
  do Right jsonString <- recAll sock
      | Left err => do if err == 0 then putStrLn $ (show ip) ++ " has lost connection" else putStrLn $ "Recmessages err: " ++ (show err)
     Just json <- pure (parse jsonString)
      | Nothing => putStrLn "The message does not have json structure"
     Just msg <- pure (jsonToMsg json)
      | Nothing => putStrLn "Structure of json was incorrect"
     ok <- run (readFromChan (relayed chans))
     case ok of
           (Fatal err) =>
             do putStrLn err
           (Warning err) =>
             do putStrLn ("Error in recMessages, error is: " ++ err); recMessages sock ip chans
           (Correct seenmsgs) =>
             case isElem (msgId msg) (map (\x => msgId x) seenmsgs) of
               (Yes prf) =>
                 do run (push (msgQueue chans) msg)
                    run (releaseLock (relayed chans))
                    recMessages sock ip chans
               (No contra) =>
                 do run (push (msgQueue chans) msg)
                    putStrLn $ (msgId msg) ++ ": " ++ (content msg)
                    run (releaseLock (relayed chans))
                    recMessages sock ip chans

listenForClients : (listeningSock : Socket) ->
                (chans : PeerChannels) -> IO ()
listenForClients listeningSock chans =
  do Right (newSock, newIp) <- accept listeningSock
      | Left err => do putStrLn $ "ListenForClients error: " ++ (show err)
     putStrLn $ "Socket accepted connection from: " ++ (show newIp)
     run (push (connChan chans) newSock)
     run (lockChannel (msgQueue chans))
     seenMsgs <- run (getListOfChannel (relayed chans))
     case seenMsgs of
      (Fatal x) => do putStrLn $ "listenForClients dead: " ++ x
      (Warning x) =>
        do putStrLn ("Failed to get seenmsgs list from channel, reason : " ++ x)
           listenForClients listeningSock chans
      (Correct seenMsgs) =>
        do Right ok <- send newSock ((format 1 (msgListToJson seenMsgs)))
           | Left err => do putStrLn $ "Could not send seenMsgs, error: " ++ (show err)
           Right str <- recAll newSock | Left err => do putStrLn $ "Failed to recieve the ACK: " ++ (show err)
           if str == "ACK" then
            do spawn (recMessages newSock newIp chans)
               run (releaseLock (msgQueue chans))
               listenForClients listeningSock chans
           else putStrLn $ "Did not recieve ACK but some other msg" ++ str

broadcastInner : (msg : Message) -> (relayed : List Message) ->
                 (connections : List Socket) -> IO ()
broadcastInner msg relayed [] = pure ()
broadcastInner msg relayed (current :: rest) =
  case isElem (msgId msg) (map (\x => msgId x) relayed) of
            (Yes prf) => pure ()
            (No contra) =>
              do Right ok <- send current (format 1 (msgToJson msg))
                  | Left err => if not (err == 32) then putStrLn $ "Could not send message: " ++ (show err) else broadcastInner msg relayed rest
                 broadcastInner msg relayed rest

broadcast : (msg : Message) -> (connChan : Channel (List Socket)) ->
  (relayed : Channel (List Message)) -> IO ()
broadcast msg connChan relayed =
  do connections <- run (readFromChan connChan)
     case connections of
      (Fatal x) => do putStrLn $ "Broadcast dead: " ++ x
                      run (releaseLock connChan)
                      pure ()
      (Warning x) => do run (releaseLock connChan)
                        broadcast msg connChan relayed
                        pure ()
      (Correct connections) =>
        do ok <- run (readFromChan relayed)
           case ok of
              (Fatal x) => do putStrLn $ "Broadcast dead: " ++ x
                              run (releaseLock relayed)
                              run (releaseLock connChan)
                              pure ()
              (Warning x) => do run (releaseLock relayed)
                                run (releaseLock connChan)
                                broadcast msg connChan relayed
                                pure ()
              (Correct relayedmsgs) => do broadcastInner msg relayedmsgs connections
                                          run (releaseLock connChan)
                                          run (writeToChan relayed (msg :: relayedmsgs))
                                          pure ()

broadcastToClients : (chans : PeerChannels) -> IO ()
broadcastToClients chans =
  do msg <- run (pop (msgQueue chans))
     case msg of
       (Fatal err) => do putStrLn $ "BroadCastToClients Dead: " ++ err
       (Warning err) =>
         do putStrLn ("BroadcastToClientsErr " ++ err)
            broadcastToClients chans
       (Correct maybeMsg) =>
         case maybeMsg of
           Nothing =>
             do broadcastToClients chans
           (Just msg) =>
             do broadcast msg (connChan chans) (relayed chans)
                broadcastToClients chans

addSingleMsg : (input : String) -> (msgQueue : Channel (List Message)) -> (msgId : String) -> IO ()
addSingleMsg input msgQueue msgId = do pushedOk <- run (push msgQueue (MkMsg msgId input))
                                       pure ()

generateMsgId : (ip : SocketAddress) -> (port : Int) -> (msgId : Int) -> IO String
generateMsgId ip port msgId = pure $ (show ip) ++ ":" ++ (show port) ++ "-" ++ (show msgId)

repl : (chans : PeerChannels) -> (oldId : Int) ->
  (ip: SocketAddress) -> (port: Int) -> IO ()
repl chans oldId ip port =
  do input <- getLine
     newId <- pure (oldId + 1)
     msgId <- generateMsgId ip port newId
     spawn (addSingleMsg input (msgQueue chans) msgId)
     repl chans newId ip port

addMessagesToChan : (msgs : List (Maybe Message)) -> (relayed : Channel (List Message)) -> IO ()
addMessagesToChan [] relayed = pure ()
addMessagesToChan (Nothing :: rest) relayed = pure ()
addMessagesToChan (Just msg :: rest) relayed =
  do run (push relayed msg)
     addMessagesToChan rest relayed
     putStrLn $ (msgId msg) ++ ": " ++ (content msg)

waitForSeenMsgs : (sock : Socket) -> (relayed : Channel (List Message)) -> IO ()
waitForSeenMsgs sock relayed = do Right jsonString <- recAll sock | Left err => putStrLn (show err)
                                  Just json <- pure (parse jsonString)
                                    | Nothing => putStrLn "The message does not have json structure"
                                  Just msgs <- pure (jsonToMsgList json)
                                    | Nothing => putStrLn "Structure of json was incorrect"
                                  addMessagesToChan msgs relayed
                                  Right ok <- send sock "ACK" | Left err => do putStrLn $ "Could not send ACK " ++ (show err)
                                  pure ()

firstPeer : (chans : PeerChannels) -> (sock : Socket) ->
            (ip : SocketAddress) -> (port : Int) ->
            PeerCmd () Setup Running
firstPeer chans sock ip port =
  do PutStrLn $ "Socket is listening for connections on: " ++ (show ip) ++ ":" ++ (show port)
     ListenForNewClients sock chans
     BroadcastToClients chans
     ReplStart chans ip port

connectingPeer : (chans : PeerChannels) -> (mySock : Socket) ->
                 (myIp : SocketAddress) -> (myPort : Int) ->
                 (newIp : SocketAddress) -> (newPort : Int) ->
                 PeerCmd () NotReady Running
connectingPeer chans mySock myIp myPort newIp newPort =
  do Right newSock <- CreateSocket | Left err => Error (show err)
     ok <- Connect newSock newIp newPort
     if ok == 0 then
      do Push (connChan chans) newSock
         WaitForRelayedMessages newSock (relayed chans)
         PutStrLn $ "Socket is listening for connections on: " ++ (show myIp) ++ ":" ++ (show myPort)
         RecMessages newSock newIp chans
         ListenForNewClients mySock chans
         BroadcastToClients chans
         ReplStart chans myIp myPort
     else Error $ "Something went wrong : error code " ++ (show ok)

run : PeerCmd res inState outState -> IO res
run (WaitForRelayedMessages sock relayed) = waitForSeenMsgs sock relayed
run (ListenForNewClients sock chans) =
  do spawn (listenForClients sock chans )
     pure ()
run (BroadcastToClients chans) =
  do spawn (broadcastToClients chans)
     pure ()
run (RecMessages newSock ip chans) =
  do spawn (recMessages newSock ip chans)
     pure ()
run (ReplStart chans ip port) = repl chans 0 ip port
run (Connect newSock newIp newPort) = connect newSock newIp newPort
run (CreateSocket) = socket AF_INET Stream 0

run (Error str) = putStrLn str
run (Push chan val) =
  do run (push chan val)
     pure ()
run (GetLine) = getLine
run (PutStrLn str) = putStrLn str
run (PureCmd res) = pure res
run (x >>= f) = do x' <- run x
                   run (f x')

peerStart : IO ()
peerStart =
  do Right sock <- socket AF_INET Stream 0
      | Left err => putStr (show err)
     putStrLn "Socket created"
     connChan <- makeChan (the (List Socket) [])
     msgQueue <- makeChan (the (List Message) [])
     relayed <- makeChan (the (List Message) [])
     chans <- pure (MkPeerChans msgQueue relayed connChan)
     putStrLn "Select what ip you want to use, by inputting the number in the parentheses:"
     ip <- selectIp
     seed <- time
     port <- pure (randPort (fromInteger seed))
     ok <- bind sock (Just ip) port
     listeningCode <- listen sock
     if ok == 0 then
       do putStrLn "Press ENTER to start a new network, or input an ip to connect to an existing network"
          ipAndPort <- getLine
          if ipAndPort == "" then
            do run (firstPeer chans sock ip port)
          else
            do Just (newIp, newPort) <- parseIpAndPort ipAndPort
                | Nothing => putStrLn "Failed to parse ip or port"
               run (connectingPeer chans sock ip port newIp newPort)
     else if ok == 13 then
       putStrLn $ "Something went wrong, port is probably already in use. Try again"
     else putStrLn $ "Something went wrong, error code: " ++ (show ok)

main : IO ()
main = peerStart

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module BacktrackSearch

import Data.So

%default total

data X = A | B | C

Eq X where
  A == A = True
  B == B = True
  _ == _ = False

data Statement : Type -> Type where
  MkStmt : (x : X) -> {auto nonA : So (x /= A)} -> Statement X

summon : {auto u : a} -> a
summon {u} = u

u : Statement X
u = MkStmt B

-- works and should
lastOfTwo : Statement X
lastOfTwo = let a = A; b = B in summon

-- works and should
theOnlyGood : Statement X
theOnlyGood = let b = B in summon

-- does not work, but why not? Why it stops searching after finding the first variant?
firstOfTwo : Statement X
firstOfTwo = let b = B; a = A in summon

-- should not work and does not
theOnlyBad : Statement X
theOnlyBad = let a = A in summon

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
-- -------------------------------------------------------------- [ Common.idr ]
-- Module      : Common
-- Description : Common things for advanced crypto
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOF ]
module Crypto.Adv.Common

namespace BPolicy
    data BPolicy : Type where
      Leaf : (value : a) -> BPolicy
      Or   : (l : BPolicy) -> (r : BPolicy) -> BPolicy
      And  : (l : BPolicy) -> (r : BPolicy) -> BPolicy

namespace TPolicy
  data TPolicy : (threshold : Nat) -> (count : Nat) -> Type where
    TLeaf      : (value : a) -> TPolicy 1 1
    NKPolicy   : (k : Nat) -> (children : Vect n (TPolicy t m)) -> TPolicy k n
    OneKPolicy : (children : Vect n (TPolicy t m)) -> TPolicy 1 n
    KKPolicy   : (children : Vect n (TPolicy t m)) -> TPolicy n n

foobar : BPolicy
foobar = Or (And
              (Or (Leaf "a:xxx0") (Leaf "a:xx0x"))
              (Leaf "a:x0xx"))
            (Leaf "a:0xxx")

foobar' : TPolicy 1 2
foobar' = OneKPolicy [KKPolicy
                      [OneKPolicy
                          [TLeaf "a:xx0", TLeaf "a:xx0x"],
                       TLeaf "a:x0xx"],
                      TLeaf "a:0xxx"]
-- 1of2 ( 2of2 ( 1of2 ( a:xxx0 , a:xx0x ) , a:x0xx ) , a:0xxx )

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module WebServer.Format

import WebServer.Requests

%default total

%access public export

data Format
  = Num Format
  | Str Format
  | End
%name Format format

HandlerType : Format -> Type
HandlerType (Num fmt) = Nat -> HandlerType fmt
HandlerType (Str fmt) = String -> HandlerType fmt
HandlerType End = Response
%name HandlerType f

parse : (acc : Format) -> (parts : List String) -> Format
parse acc [] = acc
parse acc (part :: parts) =
  case unpack part of
       (':' :: 'n' :: 'u' :: 'm' :: '.' :: _) =>
         Num (parse acc parts)
       (':' :: _) =>
         Str (parse acc parts)
       _ =>
         parse acc parts

parseFormat : (routePath : String) -> Format
parseFormat routePath = parse End $ (== '/') `split` routePath

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
module Drahko.FFI

%default total
%access public export

mutual
  data AutoHotkeyRaw : Type -> Type where
    MkAutoHotkeyRaw : (x:t) -> AutoHotkeyRaw t
  -- %used MkAutoHotkeyRaw x

  data AHK_FnTypes : Type -> Type where
    AHK_Fn : AHK_Types s -> AHK_FnTypes t -> AHK_FnTypes (s -> t)
    AHK_FnIO : AHK_Types s -> AHK_Types t -> AHK_FnTypes (s -> IO' l t)
    AHK_FnBase : AHK_Types s -> AHK_Types t -> AHK_FnTypes (s -> t)

  data AHK_Types : Type -> Type where
    AHK_Str    : AHK_Types String
    AHK_Int    : AHK_Types Int
    AHK_Float  : AHK_Types Double
    AHK_Bool   : AHK_Types Bool
    AHK_Unit   : AHK_Types ()
    AHK_Raw    : AHK_Types (Raw a)
    AHK_Ptr    : AHK_Types Ptr
    AHK_FnT    : AHK_FnTypes t -> AHK_Types t

  data AHK_Foreign
    = AHK_DotAccess String String
    | AHK_Command String
    | AHK_Function String

  %error_reverse
  FFI_AHK : FFI
  FFI_AHK = MkFFI AHK_Types AHK_Foreign String

  %error_reverse
  Promise : Type -> Type
  Promise = IO' FFI_AHK

  IO : Type -> Type
  IO a = IO' FFI_AHK a

mutual
  -- Translates an AHK-conventions function to an Idris-conventions
  -- one by inserting an additional dummy 'world' argument.
  %inline
  fromAHKFn : AHK_FnTypes a -> a -> a
  fromAHKFn (AHK_Fn s t)     f = \x => fromAHKFn t (f (toAHK s x))
  fromAHKFn (AHK_FnIO s t)   f = \x => pure (fromAHK t (believe_me (f (toAHK s x))))
  fromAHKFn (AHK_FnBase s t) f = \x => fromAHK t (f (toAHK s x))

  %inline
  toAHKFn : AHK_FnTypes a -> a -> a
  toAHKFn (AHK_Fn s t)     f = \x => toAHKFn t (f (fromAHK s x))
  toAHKFn (AHK_FnIO s t)   f = \x => believe_me (toAHK t (unsafePerformIO (f (fromAHK s x))))
  toAHKFn (AHK_FnBase s t) f = \x => toAHK t (f (fromAHK s x))

  %inline
  fromAHK : AHK_Types a -> a -> a
  fromAHK AHK_Str        s = s
  fromAHK AHK_Int        i = i
  fromAHK AHK_Float      f = f
  fromAHK AHK_Bool       b = b
  fromAHK AHK_Unit       u = u
  fromAHK AHK_Raw        a = a
  fromAHK AHK_Ptr        p = p
  fromAHK (AHK_FnT t)    f = fromAHKFn t f
  -- fromAHK (AHK_Pair s t) p = (fromAHK s (fst p), fromAHK t (snd p))
  -- fromAHK (AHK_List s)   l = map (fromAHK s) l

  %inline
  toAHK : AHK_Types a -> a -> a
  toAHK AHK_Str        s = s
  toAHK AHK_Int        i = i
  toAHK AHK_Float      f = f
  toAHK AHK_Bool       b = b
  toAHK AHK_Unit       u = u
  toAHK AHK_Raw        a = a
  toAHK AHK_Ptr        p = p
  toAHK (AHK_FnT t)    f = toAHKFn t f
  -- toAHK (AHK_Pair s t) p = (toAHK s (fst p), toAHK t (snd p))
  -- toAHK (AHK_List s)   l = map (toAHK s) l

%inline
fromAHKFTy : FTy FFI_AHK xs ty -> ty -> ty
fromAHKFTy (FRet t)   f = do x <- f; pure (fromAHK t x)
fromAHKFTy (FFun s t) f = \x => fromAHKFTy t (f (toAHK s x))

||| Call an AutoHotkey function.
%inline
call_function : String -> (ty : Type) -> {auto fty : FTy FFI_AHK [] ty} -> ty
call_function name ty {fty} =
  fromAHKFTy fty (foreign FFI_AHK (AHK_Function name) ty)

||| Call an AutoHotkey command.
%inline
call_command : String -> (ty : Type) -> {auto fty : FTy FFI_AHK [] ty} -> ty
call_command name =
  foreign FFI_AHK (AHK_Command name)

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/drahko

max_forks_repo_name: drahko/drahko


text:
x : Nat
x = 0

add : Nat -> Nat -> Nat
add x y = x + y

main : IO ()
main = printLn "Hello World"


text:
module TicTacToe.Simple

import TicTacToe.GameState
import TicTacToe.Player

import Data.Matrix

%access export
%default total

public export
Grid : Type
Grid = Matrix 3 3 (Maybe Player)

public export
Position : Type
Position = (Fin 3, Fin 3)

namespace Grid
  export
  show : Grid -> String
  show g = unlines . intersperse rule . toList . map row $ g
    where
      row : Vect 3 (Maybe Player) -> String
      row = strCons ' ' . concat . intersperse " | " . map showCell

      rule : String
      rule = pack $ List.replicate 11 '-'
      --rule = pack $ List.replicate (n * 3 + (n `minus` 1)) '-'

public export
emptyGrid : Grid
emptyGrid = replicate _ . replicate _ $ Nothing

public export
get : Position -> Grid -> Maybe Player
get (x, y) = indices x y

public export
set : Player -> Position -> Grid -> Grid
set p (x, y) g = replaceAt x (replaceAt y (Just p) (getRow x g)) g

public export
occupied : Grid -> Nat
occupied = sum . map (DPair.fst . filter isJust)

public export
free : Position -> Grid -> Bool
free (x, y) = isNothing . indices x y

public export
hasWinner : Grid -> Maybe Player
hasWinner g = List.find pred (rows g) >>= Vect.head
  where
    rows : Grid -> List (Vect 3 (Maybe Player))
    rows m = (diag m) :: (diag . reverse $ m) :: toList m ++ (toList $ transpose m)

    pred : Vect 3 (Maybe Player) -> Bool
    pred v = all (== Just Cross) v || all (== Just Nought) v

public export
data IsNothing : Maybe a -> Type where
  ItIsNothing : IsNothing Nothing

public export
Uninhabited (IsNothing (Just v)) where
  uninhabited ItIsNothing impossible

public export
isItNothing : (v : Maybe a) -> Dec (IsNothing v)
isItNothing Nothing = Yes ItIsNothing
isItNothing (Just _) = No absurd

public export
data Empty : (pos : Position) -> (g : Grid) -> Type where
  IsEmpty : {auto prf : IsNothing (get pos g)} -> Empty pos g

public export
isEmptyJust : (contra : IsNothing (get pos g) -> Void) -> Empty pos g -> Void
isEmptyJust contra (IsEmpty {prf}) = contra prf

isEmpty : (pos : Position) -> (g : Grid) -> Dec (Empty pos g)
isEmpty pos g with (isItNothing (get pos g))
  isEmpty _ _ | (Yes prf) = Yes IsEmpty
  isEmpty _ _ | (No contra) = No (isEmptyJust contra)

public export
data Board : (g : Grid) -> (p : Player) -> (turn : Nat) -> Type where
  Start : Board Simple.emptyGrid Cross 0
  Turn  : (pos : Position)
       -> Board g p turn
       -> {auto prf : Empty pos g}
       -> Board (set p pos g) (switch p) (S turn)

Show (Board g p turn) where
  show {g} _ = Grid.show g

public export
status : Board g p turn -> GameState
status {g} {turn} _ = case hasWinner g of
                           Nothing => if turn == 9
                                         then Ended Draw
                                         else InPlay
                           Just winner => Ended (Won winner)

public export
data Game : {g : Grid} -> (b : Board g p turn) -> GameState -> Type where
  MkGame : (b : Board g p turn) -> Game b (status b)

Show (Game b state) where
  show (MkGame {g} _) = Grid.show g

initGame : Game Start InPlay
initGame = MkGame Start

move : {b : Board g p turn}
    -> (pos : Position)
    -> Game b InPlay
    -> {auto prf : Empty pos g}
    -> (st : GameState ** Game (Turn pos b {prf = prf}) st)
move pos _ {b} {prf} = (_ ** MkGame (Turn pos b {prf = prf}))

winner : Game b (Ended (Won p)) -> Player
winner {p} _ = p

currentStatus : Game b st -> GameState
currentStatus {st} _ = st

currentGrid : Game b st -> Grid
currentGrid (MkGame {g} _) = g

currentBoard : {b : Board g p turn} -> Game b st -> Board g p turn
currentBoard (MkGame b) = b

max_stars_repo_name: ShinKage/DT-TicTacToe

max_issues_repo_name: ShinKage/DT-TicTacToe

max_forks_repo_name: ShinKage/DT-TicTacToe


text:
module Main

import Data.Vect

allLengths : Vect len String -> Vect len Nat
allLengths       []  = []
allLengths (x :: xs) = length x :: allLengths xs

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.Time.HighResolution

%access public export
%default total

||| The DOMHighResTimeStamp type is used to store a time value in milliseconds,
||| measured relative from the time origin, global monotonic clock, or a time
||| value that represents a duration between two DOMHighResTimeStamp's.
|||
||| The original specification can be found at
||| https://w3c.github.io/hr-time/#dom-domhighrestimestamp
DOMHighResTimeStamp : Type
DOMHighResTimeStamp = Double

max_stars_repo_name: blau-io/idris-hrTime

max_issues_repo_name: blau-io/idris-hrTime

max_forks_repo_name: blau-io/idris-hrTime


text:
module Control.Monad.Dom.Event

import JS
import Text.Html.Event
import Web.Dom
import Web.Raw.UIEvents

%default total

%foreign "browser:lambda:x=>x.target.value || x.target.innerHTML || ''"
prim__input : Event -> PrimIO String

%foreign "browser:lambda:x=>x.target.checked?1:0"
prim__checked : Event -> PrimIO Bits8

export
mouseInfo : MouseEvent -> JSIO MouseInfo
mouseInfo e =
  [| MkMouseInfo
     (button e)
     (buttons e)
     (clientX e)
     (clientY e)
     (screenX e)
     (screenY e)
     (altKey e)
     (ctrlKey e)
     (metaKey e)
     (shiftKey e)
  |]

export
keyInfo : KeyboardEvent -> JSIO KeyInfo
keyInfo e =
  [| MkKeyInfo
     (key e)
     (code e)
     (location e)
     (isComposing e)
     (altKey e)
     (ctrlKey e)
     (metaKey e)
     (shiftKey e)
  |]

export
inputInfo : InputEvent -> JSIO InputInfo
inputInfo e =
  [| MkInputInfo
       (primIO (prim__input $ up e))
       ((1 ==) <$> primIO (prim__checked $ up e)) |]

export
changeInfo : Event -> JSIO InputInfo
changeInfo e =
  [| MkInputInfo
       (primIO (prim__input e))
       ((1 ==) <$> primIO (prim__checked e)) |]


text:
module TTImp.Elab.App

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

import TTImp.Elab.Check
import TTImp.Elab.Dot
import TTImp.TTImp

import Data.List
import Data.List1
import Data.Maybe

%default covering

checkVisibleNS : {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> Visibility -> Core ()
checkVisibleNS fc (NS ns x) vis
    = if !(isVisible ns)
         then if !isAllPublic
                       || visibleInAny (!getNS :: !getNestedNS) (NS ns x) vis
                 then pure ()
                 else throw $ InvisibleName fc (NS ns x) Nothing
         else throw $ InvisibleName fc (NS ns x) (Just ns)
checkVisibleNS _ _ _ = pure ()

-- Get the type of a variable, assuming we haven't found it in the nested
-- names. Look in the Env first, then the global context.
getNameType : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> Env Term vars ->
              FC -> Name ->
              Core (Term vars, Glued vars)
getNameType rigc env fc x
    = case defined x env of
           Just (MkIsDefined rigb lv) =>
              do rigSafe rigb rigc
                 let binder = getBinder lv env
                 let bty = binderType binder

                 log "metadata.names" 7 $ "getNameType is adding ↓"
                 addNameType fc x env bty

                 when (isLinear rigb) $
                      do est <- get EST
                         put EST
                            (record { linearUsed $= ((MkVar lv) :: ) } est)
                 log "ide-mode.highlight" 8
                     $ "getNameType is trying to add Bound: "
                      ++ show x ++ " (" ++ show fc ++ ")"
                 when (isSourceName x) $
                   whenJust (isConcreteFC fc) $ \nfc => do
                     log "ide-mode.highlight" 7 $ "getNameType is adding Bound: " ++ show x
                     addSemanticDecorations [(nfc, Bound, Just x)]

                 pure (Local fc (Just (isLet binder)) _ lv, gnf env bty)
           Nothing =>
              do defs <- get Ctxt
                 [(pname, i, def)] <- lookupCtxtName x (gamma defs)
                      | [] => undefinedName fc x
                      | ns => throw (AmbiguousName fc (map fst ns))
                 checkVisibleNS fc (fullname def) (visibility def)
                 rigSafe (multiplicity def) rigc
                 let nt = fromMaybe Func (defNameType $ definition def)

                 log "ide-mode.highlight" 8
                     $ "getNameType is trying to add something for: "
                      ++ show def.fullname ++ " (" ++ show fc ++ ")"

                 when (isSourceName def.fullname) $
                   whenJust (isConcreteFC fc) $ \nfc => do
                     let decor = nameDecoration def.fullname nt
                     log "ide-mode.highlight" 7
                       $ "getNameType is adding " ++ show decor ++ ": " ++ show def.fullname
                     addSemanticDecorations [(nfc, decor, Just def.fullname)]

                 pure (Ref fc nt (Resolved i), gnf env (embed (type def)))
  where
    rigSafe : RigCount -> RigCount -> Core ()
    rigSafe lhs rhs = when (lhs < rhs)
                           (throw (LinearMisuse fc !(getFullName x) lhs rhs))

-- Get the type of a variable, looking it up in the nested names first.
getVarType : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto e : Ref EST (EState vars)} ->
             RigCount -> NestedNames vars -> Env Term vars ->
             FC -> Name ->
             Core (Term vars, Nat, Glued vars)
getVarType rigc nest env fc x
    = case lookup x (names nest) of
           Nothing => do (tm, ty) <- getNameType rigc env fc x
                         pure (tm, 0, ty)
           Just (nestn, argns, tmf) =>
              do defs <- get Ctxt
                 let arglen = length argns
                 let n' = fromMaybe x nestn
                 case !(lookupCtxtExact n' (gamma defs)) of
                      Nothing => undefinedName fc n'
                      Just ndef =>
                         let nt = fromMaybe Func (defNameType $ definition ndef)
                             tm = tmf fc nt
                             tyenv = useVars (getArgs tm)
                                             (embed (type ndef)) in
                             do checkVisibleNS fc (fullname ndef) (visibility ndef)
                                logTerm "elab" 5 ("Type of " ++ show n') tyenv
                                logTerm "elab" 5 ("Expands to") tm
                                log "elab" 5 $ "Arg length " ++ show arglen

                                -- Add the type to the metadata
                                log "metadata.names" 7 $ "getVarType is adding ↓"
                                addNameType fc x env tyenv

                                when (isSourceName ndef.fullname) $
                                  whenJust (isConcreteFC fc) $ \nfc => do
                                    let decor = nameDecoration ndef.fullname nt
                                    log "ide-mode.highlight" 7
                                       $ "getNameType is adding "++ show decor ++": "
                                                                 ++ show ndef.fullname
                                    addSemanticDecorations [(nfc, decor, Just ndef.fullname)]

                                pure (tm, arglen, gnf env tyenv)
    where
      useVars : {vars : _} ->
                List (Term vars) -> Term vars -> Term vars
      useVars [] sc = sc
      useVars (a :: as) (Bind bfc n (Pi fc c _ ty) sc)
           = Bind bfc n (Let fc c a ty) (useVars (map weaken as) sc)
      useVars as (Bind bfc n (Let fc c v ty) sc)
           = Bind bfc n (Let fc c v ty) (useVars (map weaken as) sc)
      useVars _ sc = sc -- Can't happen?

isHole : NF vars -> Bool
isHole (NApp _ (NMeta _ _ _) _) = True
isHole _ = False

mutual
  makeImplicit : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RigCount -> RigCount -> ElabInfo ->
                 NestedNames vars -> Env Term vars ->
                 FC -> (fntm : Term vars) ->
                 Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->
                 (argdata : (Maybe Name, Nat)) ->
                 (expargs : List RawImp) ->
                 (autoargs : List RawImp) ->
                 (namedargs : List (Name, RawImp)) ->
                 (knownret : Bool) ->
                 (expected : Maybe (Glued vars)) ->
                 Core (Term vars, Glued vars)
  makeImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
      = do defs <- get Ctxt
           nm <- genMVName x
           empty <- clearDefs defs
           metaty <- quote empty env aty
           metaval <- metaVar fc argRig env nm metaty
           let fntm = App fc tm metaval
           fnty <- sc defs (toClosure defaultOpts env metaval)
           when (bindingVars elabinfo) $
                do est <- get EST
                   put EST (addBindIfUnsolved nm argRig Implicit env metaval metaty est)
           checkAppWith rig elabinfo nest env fc
                        fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

  makeAutoImplicit : {vars : _} ->
                     {auto c : Ref Ctxt Defs} ->
                     {auto m : Ref MD Metadata} ->
                     {auto u : Ref UST UState} ->
                     {auto e : Ref EST (EState vars)} ->
                     RigCount -> RigCount -> ElabInfo ->
                     NestedNames vars -> Env Term vars ->
                     FC -> (fntm : Term vars) ->
                     Name -> Closure vars -> (Defs -> Closure vars -> Core (NF vars)) ->
                     (argpos : (Maybe Name, Nat)) ->
                     (expargs : List RawImp) ->
                     (autoargs : List RawImp) ->
                     (namedargs : List (Name, RawImp)) ->
                     (knownret : Bool) ->
                     (expected : Maybe (Glued vars)) ->
                     Core (Term vars, Glued vars)
  makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc (n, argpos) expargs autoargs namedargs kr expty
  -- on the LHS, just treat it as an implicit pattern variable.
  -- on the RHS, add a searchable hole
      = if metavarImp (elabMode elabinfo)
           then do defs <- get Ctxt
                   nm <- genMVName x
                   empty <- clearDefs defs
                   metaty <- quote empty env aty
                   metaval <- metaVar fc argRig env nm metaty
                   let fntm = App fc tm metaval
                   fnty <- sc defs (toClosure defaultOpts env metaval)
                   est <- get EST
                   put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
                   checkAppWith rig elabinfo nest env fc
                                fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
           else do defs <- get Ctxt
                   nm <- genMVName x
                   -- We need the full normal form to check determining arguments
                   -- so we might as well calculate the whole thing now
                   metaty <- quote defs env aty
                   est <- get EST
                   lim <- getAutoImplicitLimit
                   metaval <- searchVar fc argRig lim (Resolved (defining est))
                                        env nest nm metaty
                   let fntm = App fc tm metaval
                   fnty <- sc defs (toClosure defaultOpts env metaval)
                   checkAppWith rig elabinfo nest env fc
                                fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
    where
      metavarImp : ElabMode -> Bool
      metavarImp (InLHS _) = True
      metavarImp InTransform = True
      metavarImp _ = False

  makeDefImplicit : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    {auto m : Ref MD Metadata} ->
                    {auto u : Ref UST UState} ->
                    {auto e : Ref EST (EState vars)} ->
                    RigCount -> RigCount -> ElabInfo ->
                    NestedNames vars -> Env Term vars ->
                    FC -> (fntm : Term vars) ->
                    Name -> Closure vars -> Closure vars ->
                    (Defs -> Closure vars -> Core (NF vars)) ->
                    (argpos : (Maybe Name, Nat)) ->
                    (expargs : List RawImp) ->
                    (autoargs : List RawImp) ->
                    (namedargs : List (Name, RawImp)) ->
                    (knownret : Bool) ->
                    (expected : Maybe (Glued vars)) ->
                    Core (Term vars, Glued vars)
  makeDefImplicit rig argRig elabinfo nest env fc tm x arg aty sc (n, argpos) expargs autoargs namedargs kr expty
  -- on the LHS, just treat it as an implicit pattern variable.
  -- on the RHS, use the default
      = if metavarImp (elabMode elabinfo)
           then do defs <- get Ctxt
                   nm <- genMVName x
                   empty <- clearDefs defs
                   metaty <- quote empty env aty
                   metaval <- metaVar fc argRig env nm metaty
                   let fntm = App fc tm metaval
                   fnty <- sc defs (toClosure defaultOpts env metaval)
                   est <- get EST
                   put EST (addBindIfUnsolved nm argRig AutoImplicit env metaval metaty est)
                   checkAppWith rig elabinfo nest env fc
                                fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
           else do defs <- get Ctxt
                   empty <- clearDefs defs
                   aval <- quote empty env arg
                   let fntm = App fc tm aval
                   fnty <- sc defs (toClosure defaultOpts env aval)
                   checkAppWith rig elabinfo nest env fc
                                fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
    where
      metavarImp : ElabMode -> Bool
      metavarImp (InLHS _) = True
      metavarImp InTransform = True
      metavarImp _ = False

  -- Defer elaborating anything which will be easier given a known target
  -- type (ambiguity, cases, etc)
  needsDelayExpr : {auto c : Ref Ctxt Defs} ->
                   (knownRet : Bool) -> RawImp ->
                   Core Bool
  needsDelayExpr False _ = pure False
  needsDelayExpr True (IVar fc n)
      = do defs <- get Ctxt
           pure $ case !(lookupCtxtName n (gamma defs)) of
                       (_ :: _ :: _) => True
                       _ => False
  needsDelayExpr True (IApp _ f _) = needsDelayExpr True f
  needsDelayExpr True (IAutoApp _ f _) = needsDelayExpr True f
  needsDelayExpr True (INamedApp _ f _ _) = needsDelayExpr True f
  needsDelayExpr True (ILam _ _ _ _ _ _) = pure True
  needsDelayExpr True (ICase _ _ _ _) = pure True
  needsDelayExpr True (ILocal _ _ _) = pure True
  needsDelayExpr True (IUpdate _ _ _) = pure True
  needsDelayExpr True (IAlternative _ _ _) = pure True
  needsDelayExpr True (ISearch _ _) = pure True
  needsDelayExpr True (IRewrite _ _ _) = pure True
  needsDelayExpr True _ = pure False

  -- On the LHS, for any concrete thing, we need to make sure we know
  -- its type before we proceed so that we can reject it if the type turns
  -- out to be polymorphic
  needsDelayLHS : {auto c : Ref Ctxt Defs} ->
                  RawImp -> Core Bool
  needsDelayLHS (IVar fc n) = pure True
  needsDelayLHS (IApp _ f _) = needsDelayLHS f
  needsDelayLHS (IAutoApp _ f _) = needsDelayLHS f
  needsDelayLHS (INamedApp _ f _ _) = needsDelayLHS f
  needsDelayLHS (IAlternative _ _ _) = pure True
  needsDelayLHS (IAs _ _ _ _ t) = needsDelayLHS t
  needsDelayLHS (ISearch _ _) = pure True
  needsDelayLHS (IPrimVal _ _) = pure True
  needsDelayLHS (IType _) = pure True
  needsDelayLHS (IWithUnambigNames _ _ t) = needsDelayLHS t
  needsDelayLHS _ = pure False

  onLHS : ElabMode -> Bool
  onLHS (InLHS _) = True
  onLHS _ = False

  needsDelay : {auto c : Ref Ctxt Defs} ->
               ElabMode ->
               (knownRet : Bool) -> RawImp ->
               Core Bool
  needsDelay (InLHS _) _ tm = needsDelayLHS tm
  needsDelay _ kr tm = needsDelayExpr kr tm

  checkValidPattern :
    {vars : _} ->
    {auto c : Ref Ctxt Defs} ->
    {auto m : Ref MD Metadata} ->
    {auto u : Ref UST UState} ->
    {auto e : Ref EST (EState vars)} ->
    RigCount -> Env Term vars -> FC ->
    Term vars -> Glued vars ->
    Core (Term vars, Glued vars)
  checkValidPattern rig env fc tm ty
    = do log "elab.app.lhs" 50 $ "Checking that " ++ show tm ++ " is a valid pattern"
         case tm of
           Bind _ _ (Lam _ _ _ _)  _ => registerDot rig env fc NotConstructor tm ty
           _ => pure (tm, ty)

  dotErased : {vars : _} ->
              {auto c : Ref Ctxt Defs} -> (argty : Closure vars) ->
              Maybe Name -> Nat -> ElabMode -> RigCount -> RawImp -> Core RawImp
  dotErased argty mn argpos (InLHS lrig ) rig tm
      = if not (isErased lrig) && isErased rig
          then do
            -- if the argument type aty has a single constructor, there's no need
            -- to dot it
            defs <- get Ctxt
            mconsCount <- countConstructors !(evalClosure defs argty)
            if mconsCount == Just 1 || mconsCount == Just 0
              then pure tm
              else
                -- if argpos is an erased position of 'n', leave it, otherwise dot if
                -- necessary
                do Just gdef <- maybe (pure Nothing) (\n => lookupCtxtExact n (gamma defs)) mn
                        | Nothing => pure (dotTerm tm)
                   if argpos `elem` safeErase gdef
                      then pure tm
                      else pure $ dotTerm tm
          else pure tm
    where
      ||| Count the constructors of a fully applied concrete datatype
      countConstructors : NF vars -> Core (Maybe Nat)
      countConstructors (NTCon _ tycName _ n args) =
        if length args == n
        then do defs <- get Ctxt
                Just gdef <- lookupCtxtExact tycName (gamma defs)
                | Nothing => pure Nothing
                let (TCon _ _ _ _ _ _ datacons _) = gdef.definition
                | _ => pure Nothing
                pure (Just (length datacons))
        else pure Nothing
      countConstructors _ = pure Nothing

      dotTerm : RawImp -> RawImp
      dotTerm tm
          = case tm of
                 IMustUnify _ _ _ => tm
                 IBindVar _ _ => tm
                 Implicit _ _ => tm
                 IAs _ _ _ _ (IBindVar _ _) => tm
                 IAs _ _ _ _ (Implicit _ _) => tm
                 IAs fc nameFC p t arg => IAs fc nameFC p t (IMustUnify fc ErasedArg tm)
                 _ => IMustUnify (getFC tm) ErasedArg tm
  dotErased _ _ _ _ _ tm = pure tm

  -- Check the rest of an application given the argument type and the
  -- raw argument. We choose elaboration order depending on whether we know
  -- the return type now. If we know it, elaborate the rest of the
  -- application first and come back to it, because that might infer types
  -- for implicit arguments, which might in turn help with type-directed
  -- disambiguation when elaborating the argument.
  checkRestApp : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto m : Ref MD Metadata} ->
                 {auto u : Ref UST UState} ->
                 {auto e : Ref EST (EState vars)} ->
                 RigCount -> RigCount -> ElabInfo ->
                 NestedNames vars -> Env Term vars ->
                 FC -> (fntm : Term vars) -> Name ->
                 (aty : Closure vars) -> (sc : Defs -> Closure vars -> Core (NF vars)) ->
                 (argdata : (Maybe Name, Nat)) ->
                 (arg : RawImp) ->
                 (expargs : List RawImp) ->
                 (autoargs : List RawImp) ->
                 (namedargs : List (Name, RawImp)) ->
                 (knownret : Bool) ->
                 (expected : Maybe (Glued vars)) ->
                 Core (Term vars, Glued vars)
  checkRestApp rig argRig elabinfo nest env fc tm x aty sc
               (n, argpos) arg_in expargs autoargs namedargs knownret expty
     = do defs <- get Ctxt
          arg <- dotErased aty n argpos (elabMode elabinfo) argRig arg_in
          kr <- if knownret
                   then pure True
                   else do sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
                           concrete defs env sc'
          -- In theory we can check the arguments in any order. But it turns
          -- out that it's sometimes better to do the rightmost arguments
          -- first to give ambiguity resolution more to work with. So
          -- we do that if the target type is unknown, or if we see that
          -- the raw term is otherwise worth delaying.
          if (isHole !(evalClosure defs aty) && kr) || !(needsDelay (elabMode elabinfo) kr arg_in)
             then handle (checkRtoL kr arg)
                  -- if the type isn't resolved, we might encounter an
                  -- implicit that we can't use yet because we don't know
                  -- about it. In that case, revert to LtoR
                    (\err => if invalidArg err
                                then checkLtoR kr arg
                                else throw err)
             else checkLtoR kr arg
    where
      invalidArg : Error -> Bool
      invalidArg (InvalidArgs{}) = True
      invalidArg _ = False

      checkRtoL : Bool -> -- return type is known
                  RawImp -> -- argument currently being checked
                  Core (Term vars, Glued vars)
      checkRtoL kr arg
        = do defs <- get Ctxt
             nm <- genMVName x
             empty <- clearDefs defs
             metaty <- quote empty env aty
             (idx, metaval) <- argVar (getFC arg) argRig env nm metaty
             let fntm = App fc tm metaval
             logTerm "elab" 10 "...as" metaval
             fnty <- sc defs (toClosure defaultOpts env metaval)
             (tm, gty) <- checkAppWith rig elabinfo nest env fc
                                       fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
             defs <- get Ctxt
             aty' <- nf defs env metaty
             logNF "elab" 10 ("Now trying " ++ show nm ++ " " ++ show arg) env aty'

             -- On the LHS, checking an argument can't resolve its own type,
             -- it must be resolved from elsewhere. Otherwise we might match
             -- on things which are too specific for their polymorphic type.
             when (onLHS (elabMode elabinfo)) $
                case aty' of
                     NApp _ (NMeta _ i _) _ =>
                          do Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
                                  | Nothing => pure ()
                             when (isErased (multiplicity gdef)) $ addNoSolve i
                     _ => pure ()
             res <- check argRig (record { topLevel = False } elabinfo) nest env arg (Just $ glueBack defs env aty')
             when (onLHS (elabMode elabinfo)) $
                case aty' of
                     NApp _ (NMeta _ i _) _ => removeNoSolve i
                     _ => pure ()

             (argv, argt) <-
               if not (onLHS (elabMode elabinfo))
                 then pure res
                 else do let (argv, argt) = res
                         checkValidPattern rig env fc argv argt

             defs <- get Ctxt
             -- If we're on the LHS, reinstantiate it with 'argv' because it
             -- *may* have as patterns in it and we need to retain them.
             -- (As patterns are a bit of a hack but I don't yet see a
             -- better way that leads to good code...)
             logTerm "elab" 10 ("Solving " ++ show metaval ++ " with") argv
             ok <- solveIfUndefined env metaval argv
             -- If there's a constraint, make a constant, but otherwise
             -- just return the term as expected
             tm <- if not ok
                      then do res <- convert fc elabinfo env
                                                 (gnf env metaval)
                                                 (gnf env argv)
                              let [] = constraints res
                                  | cs => do tmty <- getTerm gty
                                             newConstant fc rig env tm tmty cs
                              ignore $ updateSolution env metaval argv
                              pure tm
                      else pure tm
             case elabMode elabinfo of
                  InLHS _ => -- reset hole and redo it with the unexpanded definition
                     do updateDef (Resolved idx) (const (Just (Hole 0 (holeInit False))))
                        ignore $ solveIfUndefined env metaval argv
                  _ => pure ()
             removeHole idx
             pure (tm, gty)

      checkLtoR : Bool -> -- return type is known
                  RawImp -> -- argument currently being checked
                  Core (Term vars, Glued vars)
      checkLtoR kr arg
        = do defs <- get Ctxt
             logNF "elab" 10 ("Full function type") env
                      (NBind fc x (Pi fc argRig Explicit aty) sc)
             logC "elab" 10
                     (do ety <- maybe (pure Nothing)
                                     (\t => pure (Just !(toFullNames!(getTerm t))))
                                     expty
                         pure ("Overall expected type: " ++ show ety))
             res <- check argRig (record { topLevel = False } elabinfo)
                                   nest env arg (Just (glueClosure defs env aty))
             (argv, argt) <-
               if not (onLHS (elabMode elabinfo))
                 then pure res
                 else do let (argv, argt) = res
                         checkValidPattern rig env fc argv argt

             logGlueNF "elab" 10 "Got arg type" env argt
             defs <- get Ctxt
             let fntm = App fc tm argv
             fnty <- sc defs (toClosure defaultOpts env argv)
             checkAppWith rig elabinfo nest env fc
                          fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty

  export
  findNamed : Name -> List (Name, RawImp) -> Maybe ((Name, RawImp), List (Name, RawImp))
  findNamed n l = case partition ((== n) . fst) l of
                       (x :: xs, ys) => Just (x, (xs ++ ys))
                       _ => Nothing

  export
  findBindAllExpPattern : List (Name, RawImp) -> Maybe RawImp
  findBindAllExpPattern = lookup (UN Underscore)

  isImplicitAs : RawImp -> Bool
  isImplicitAs (IAs _ _ UseLeft _ (Implicit _ _)) = True
  isImplicitAs _ = False

  isBindAllExpPattern : Name -> Bool
  isBindAllExpPattern (UN Underscore) = True
  isBindAllExpPattern _ = False

  -- Check an application of 'fntm', with type 'fnty' to the given list
  -- of explicit and implicit arguments.
  -- Returns the checked term and its (weakly) normalised type
  checkAppWith' : {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 -> (fntm : Term vars) -> (fnty : NF vars) ->
                 (argdata : (Maybe Name, Nat)) ->
                      -- function we're applying, and argument position, for
                      -- checking if it's okay to erase against 'safeErase'
                 (expargs : List RawImp) ->
                 (autoargs : List RawImp) ->
                 (namedargs : List (Name, RawImp)) ->
                 (knownret : Bool) -> -- Do we know what the return type is yet?
                              -- if we do, we might be able to use it to work
                              -- out the types of arguments before elaborating them
                 (expected : Maybe (Glued vars)) ->
                 Core (Term vars, Glued vars)
   -- Explicit Pi, we use provided unnamed explicit argument
  checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
               argdata (arg :: expargs') autoargs namedargs kr expty
     = do let argRig = rig |*| rigb
          checkRestApp rig argRig elabinfo nest env fc
                       tm x aty sc argdata arg expargs' autoargs namedargs kr expty
  checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
               argdata [] autoargs namedargs kr expty with (findNamed x namedargs)
   -- We found a compatible named argument
   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
                argdata [] autoargs namedargs kr expty | Just ((_, arg), namedargs')
    = do let argRig = rig |*| rigb
         checkRestApp rig argRig elabinfo nest env fc
                      tm x aty sc argdata arg [] autoargs namedargs' kr expty
   checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Explicit aty) sc)
                argdata [] autoargs namedargs kr expty | Nothing
    = case findBindAllExpPattern namedargs of
           Just arg => -- Bind-all-explicit pattern is present - implicitly bind
             do let argRig = rig |*| rigb
                checkRestApp rig argRig elabinfo nest env fc
                             tm x aty sc argdata arg [] autoargs namedargs kr expty
           _ =>
             do defs <- get Ctxt
                if all isImplicitAs (autoargs
                                      ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))
                                                                    -- Only non-user implicit `as` bindings added by
                                                                    -- the compiler are allowed here
                   then -- We are done
                        checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
                   else -- Some user defined binding is present while we are out of explicit arguments, that's an error
                        throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)
  -- Function type is delayed, so force the term and continue
  checkAppWith' rig elabinfo nest env fc tm (NDelayed dfc r ty@(NBind _ _ (Pi _ _ _ _) sc)) argdata expargs autoargs namedargs kr expty
      = checkAppWith' rig elabinfo nest env fc (TForce dfc r tm) ty argdata expargs autoargs namedargs kr expty
  -- If there's no more arguments given, and the plicities of the type and
  -- the expected type line up, stop
  checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb Implicit aty) sc)
               argdata [] [] [] kr (Just expty_in)
      = do let argRig = rig |*| rigb
           expty <- getNF expty_in
           defs <- get Ctxt
           case expty of
                NBind tfc' x' (Pi _ rigb' Implicit aty') sc'
                   => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
                _ => if not (preciseInf elabinfo)
                        then makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
                        -- in 'preciseInf' mode blunder on anyway, and hope
                        -- that we can resolve the implicits
                        else handle (checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in))
                               (\err => makeImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in))
  -- Same for auto
  checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
               argdata [] [] [] kr (Just expty_in)
      = do let argRig = rig |*| rigb
           expty <- getNF expty_in
           defs <- get Ctxt
           case expty of
                NBind tfc' x' (Pi _ rigb' AutoImplicit aty') sc'
                   => checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
                _ => makeAutoImplicit rig argRig elabinfo nest env fc tm x aty sc argdata [] [] [] kr (Just expty_in)
  -- Same for default
  checkAppWith' rig elabinfo nest env fc tm ty@(NBind tfc x (Pi _ rigb (DefImplicit aval) aty) sc)
               argdata [] [] [] kr (Just expty_in)
      = do let argRig = rigMult rig rigb
           expty <- getNF expty_in
           defs <- get Ctxt
           case expty of
                NBind tfc' x' (Pi _ rigb' (DefImplicit aval') aty') sc'
                   => if !(convert defs env aval aval')
                         then checkExp rig elabinfo env fc tm (glueBack defs env ty) (Just expty_in)
                         else makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)
                _ => makeDefImplicit rig argRig elabinfo nest env fc tm x aval aty sc argdata [] [] [] kr (Just expty_in)

  -- Check next unnamed auto implicit argument
  checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
               argdata expargs (arg :: autoargs') namedargs kr expty
      = checkRestApp rig (rig |*| rigb) elabinfo nest env fc
                         tm x aty sc argdata arg expargs autoargs' namedargs kr expty
  -- Check next named auto implicit argument
  checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb AutoImplicit aty) sc)
               argdata expargs [] namedargs kr expty
      = let argRig = rig |*| rigb in
            case findNamed x namedargs of
                 Just ((_, arg), namedargs') =>
                    checkRestApp rig argRig elabinfo nest env fc
                                 tm x aty sc argdata arg expargs [] namedargs' kr expty
                 Nothing =>
                         makeAutoImplicit rig argRig elabinfo nest env fc tm
                                              x aty sc argdata expargs [] namedargs kr expty
  -- Check next implicit argument
  checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb Implicit aty) sc)
               argdata expargs autoargs namedargs kr expty
      = let argRig = rig |*| rigb in
            case findNamed x namedargs of
               Nothing => makeImplicit rig argRig elabinfo nest env fc tm
                                       x aty sc argdata expargs autoargs namedargs kr expty
               Just ((_, arg), namedargs') =>
                     checkRestApp rig argRig elabinfo nest env fc
                                  tm x aty sc argdata arg expargs autoargs namedargs' kr expty
  -- Check next default argument
  checkAppWith' rig elabinfo nest env fc tm (NBind tfc x (Pi _ rigb (DefImplicit arg) aty) sc)
               argdata expargs autoargs namedargs kr expty
      = let argRig = rigMult rig rigb in
            case findNamed x namedargs of
               Nothing => makeDefImplicit rig argRig elabinfo nest env fc tm
                                          x arg aty sc argdata expargs autoargs namedargs kr expty
               Just ((_, arg), namedargs') =>
                     checkRestApp rig argRig elabinfo nest env fc
                                  tm x aty sc argdata arg expargs autoargs namedargs' kr expty
  -- Invent a function type if we have extra explicit arguments but type is further unknown
  checkAppWith' {vars} rig elabinfo nest env fc tm ty (n, argpos) (arg :: expargs) autoargs namedargs kr expty
      = -- Invent a function type,  and hope that we'll know enough to solve it
        -- later when we unify with expty
        do logNF "elab.with" 10 "Function type" env ty
           logTerm "elab.with" 10 "Function " tm
           argn <- genName "argTy"
           retn <- genName "retTy"
           argTy <- metaVar fc erased env argn (TType fc)
           let argTyG = gnf env argTy
           retTy <- metaVar -- {vars = argn :: vars}
                            fc erased env -- (Pi RigW Explicit argTy :: env)
                            retn (TType fc)
           (argv, argt) <- check rig elabinfo
                                 nest env arg (Just argTyG)
           let fntm = App fc tm argv
           defs <- get Ctxt
           fnty <- nf defs env retTy -- (Bind fc argn (Let RigW argv argTy) retTy)
           let expfnty = gnf env (Bind fc argn (Pi fc top Explicit argTy) (weaken retTy))
           logGlue "elab.with" 10 "Expected function type" env expfnty
           whenJust expty (logGlue "elab.with" 10 "Expected result type" env)
           res <- checkAppWith' rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty
           cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty
           let [] = constraints cres
              | cs => do cty <- getTerm expfnty
                         ctm <- newConstant fc rig env (fst res) cty cs
                         pure (ctm, gnf env retTy)
           pure res
  -- Only non-user implicit `as` bindings are allowed to be present as arguments at this stage
  checkAppWith' rig elabinfo nest env fc tm ty argdata [] autoargs namedargs kr expty
      = do defs <- get Ctxt
           if all isImplicitAs (autoargs ++ map snd (filter (not . isBindAllExpPattern . fst) namedargs))
              then checkExp rig elabinfo env fc tm (glueBack defs env ty) expty
              else throw (InvalidArgs fc env (map (const (UN $ Basic "<auto>")) autoargs ++ map fst namedargs) tm)

  ||| Entrypoint for checkAppWith: run the elaboration first and, if we're
  ||| on the LHS and the result is an under-applied constructor then insist
  ||| that it ought to be forced by another pattern somewhere else in the LHS.
  checkAppWith : {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 -> (fntm : Term vars) -> (fnty : NF vars) ->
                 (argdata : (Maybe Name, Nat)) ->
                      -- function we're applying, and argument position, for
                      -- checking if it's okay to erase against 'safeErase'
                 (expargs : List RawImp) ->
                 (autoargs : List RawImp) ->
                 (namedargs : List (Name, RawImp)) ->
                 (knownret : Bool) -> -- Do we know what the return type is yet?
                              -- if we do, we might be able to use it to work
                              -- out the types of arguments before elaborating them
                 (expected : Maybe (Glued vars)) ->
                 Core (Term vars, Glued vars)
  checkAppWith rig info nest env fc tm ty
    argdata expargs autoargs namedargs knownret expected
    = do res <- checkAppWith' rig info nest env fc tm ty
                   argdata expargs autoargs namedargs knownret expected
         let Just _ = isLHS (elabMode info)
               | Nothing => pure res
         let (Ref _ t _, args) = getFnArgs (fst res)
               | _ => pure res
         let Just (_, a) = isCon t
               | _ => pure res
         if a == length args
           then pure res
           else registerDot rig env fc UnderAppliedCon (fst res) (snd res)

export
checkApp : {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 -> (fn : RawImp) ->
           (expargs : List RawImp) ->
           (autoargs : List RawImp) ->
           (namedargs : List (Name, RawImp)) ->
           Maybe (Glued vars) ->
           Core (Term vars, Glued vars)
checkApp rig elabinfo nest env fc (IApp fc' fn arg) expargs autoargs namedargs exp
   = checkApp rig elabinfo nest env fc' fn (arg :: expargs) autoargs namedargs exp
checkApp rig elabinfo nest env fc (IAutoApp fc' fn arg) expargs autoargs namedargs exp
   = checkApp rig elabinfo nest env fc' fn expargs (arg :: autoargs) namedargs exp
checkApp rig elabinfo nest env fc (INamedApp fc' fn nm arg) expargs autoargs namedargs exp
   = checkApp rig elabinfo nest env fc' fn expargs autoargs ((nm, arg) :: namedargs) exp
checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
   = do (ntm, arglen, nty_in) <- getVarType rig nest env fc' n
        nty <- getNF nty_in
        prims <- getPrimitiveNames
        elabinfo <- updateElabInfo prims (elabMode elabinfo) n expargs elabinfo

        addNameLoc fc' n

        logC "elab" 10
                (do defs <- get Ctxt
                    fnty <- quote defs env nty
                    exptyt <- maybe (pure Nothing)
                                       (\t => do ety <- getTerm t
                                                 etynf <- normaliseHoles defs env ety
                                                 pure (Just !(toFullNames etynf)))
                                       exp
                    pure ("Checking application of " ++ show !(getFullName n) ++
                          " (" ++ show n ++ ")" ++
                          " to " ++ show expargs ++ "\n\tFunction type " ++
                          (show !(toFullNames fnty)) ++ "\n\tExpected app type "
                                ++ show exptyt))
        let fn = case lookup n (names nest) of
                      Just (Just n', _) => n'
                      _ => n
        normalisePrims prims env
           !(checkAppWith rig elabinfo nest env fc ntm nty (Just fn, arglen) expargs autoargs namedargs False exp)
  where

    -- If the term is an application of a primitive conversion (fromInteger etc)
    -- and it's applied to a constant, fully normalise the term.
    normalisePrims : {vs : _} ->
                     List Name -> Env Term vs ->
                     (Term vs, Glued vs) ->
                     Core (Term vs, Glued vs)
    normalisePrims prims env res
        = do tm <- Normalise.normalisePrims (`boundSafe` elabMode elabinfo)
                                            isIPrimVal
                                            (case elabMode elabinfo of
                                                  InLHS _ => True
                                                  _ => False)
                                            prims n expargs (fst res) env
             pure (fromMaybe (fst res) tm, snd res)

      where

        boundSafe : Constant -> ElabMode -> Bool
        boundSafe _ (InLHS _) = True -- always need to expand on LHS
        boundSafe (BI x) _ = abs x < 100 -- only do this for relatively small bounds.
                           -- Once it gets too big, we might be making the term
                           -- bigger than it would have been without evaluating!
        boundSafe _ _ = True

    updateElabInfo : List Name -> ElabMode -> Name ->
                     List RawImp -> ElabInfo -> Core ElabInfo
    -- If it's a primitive function applied to a constant on the LHS, treat it
    -- as an expression because we'll normalise the function away and match on
    -- the result
    updateElabInfo prims (InLHS _) n [IPrimVal fc c] elabinfo =
        do if isPrimName prims !(getFullName n)
              then pure (record { elabMode = InExpr } elabinfo)
              else pure elabinfo
    updateElabInfo _ _ _ _ info = pure info

checkApp rig elabinfo nest env fc fn expargs autoargs namedargs exp
   = do (fntm, fnty_in) <- checkImp rig elabinfo nest env fn Nothing
        fnty <- getNF fnty_in
        checkAppWith rig elabinfo nest env fc fntm fnty (Nothing, 0) expargs autoargs namedargs False exp


text: module PQ.SQL.Table


text:
||| This module implements a relation between a natural number and a list.
||| The relation witnesses the fact the number is the length of the list.
|||
||| It is meant to be used in a runtime-irrelevant fashion in computations
||| manipulating data indexed over lists where the computation actually only
||| depends on the length of said lists.
|||
||| Instead of writing:
||| ```idris example
||| f0 : (xs : List a) -> P xs
||| ```
|||
||| We would write either of:
||| ```idris example
||| f1 : (n : Nat) -> (0 _ : HasLength xs n) -> P xs
||| f2 : (n : Subset n (HasLength xs)) -> P xs
||| ```
|||
||| See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
||| but the udpate to the list (were we to keep it around) an O(n) traversal.

module Data.List.HasLength

import Data.DPair
import Data.List

%default total

------------------------------------------------------------------------
-- Type

||| Ensure that the list's length is the provided natural number
public export
data HasLength : List a -> Nat -> Type where
  Z : HasLength [] Z
  S : HasLength xs n -> HasLength (x :: xs) (S n)

------------------------------------------------------------------------
-- Properties

||| The length is unique
export
hasLengthUnique : HasLength xs m -> HasLength xs n -> m === n
hasLengthUnique Z Z = Refl
hasLengthUnique (S p) (S q) = cong S (hasLengthUnique p q)

||| This specification corresponds to the length function
export
hasLength : (xs : List a) -> HasLength xs (length xs)
hasLength [] = Z
hasLength (_ :: xs) = S (hasLength xs)

export
map : (f : a -> b) -> HasLength xs n -> HasLength (map f xs) n
map f Z = Z
map f (S n) = S (map f n)

||| @sucR demonstrates that snoc only increases the lenght by one
||| So performing this operation while carrying the list around would cost O(n)
||| but relying on n together with an erased HasLength proof instead is O(1)
export
sucR : HasLength xs n -> HasLength (snoc xs x) (S n)
sucR Z = S Z
sucR (S n) = S (sucR n)

------------------------------------------------------------------------
-- Views

namespace SubsetView

  ||| We provide this view as a convenient way to perform nested pattern-matching
  ||| on values of type `Subset Nat (HasLength xs)`. Functions using this view will
  ||| be seen as terminating as long as the index list `xs` is left untouched.
  ||| See e.g. listTerminating below for such a function.
  public export
  data View : (xs : List a) -> Subset Nat (HasLength xs) -> Type where
    Z : View [] (Element Z Z)
    S : (p : Subset Nat (HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))

  ||| This auxiliary function gets around the limitation of the check ensuring that
  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
  viewZ : (0 p : HasLength xs Z) -> View xs (Element Z p)
  viewZ Z = Z

  ||| This auxiliary function gets around the limitation of the check ensuring that
  ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
  viewS : (n : Nat) -> (0 p : HasLength xs (S n)) -> View xs (Element (S n) p)
  viewS n (S p) = S (Element n p)

  ||| Proof that the view covers all possible cases.
  export
  view : (p : Subset Nat (HasLength xs)) -> View xs p
  view (Element Z p) = viewZ p
  view (Element (S n) p) = viewS n p

namespace CurriedView

  ||| We provide this view as a convenient way to perform nested pattern-matching
  ||| on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations
  ||| to the list between recursive calls (e.g. mapping over the list) that prevent
  ||| it from being a valid termination metric, it is best to take the Nat argument
  ||| separately from the HasLength proof and the Subset view is not as useful anymore.
  ||| See e.g. natTerminating below for (a contrived example of) such a function.
  public export
  data View : (xs : List a) -> (n : Nat) -> HasLength xs n -> Type where
    Z : View [] Z Z
    S : (n : Nat) -> (0 p : HasLength xs n) -> View (x :: xs) (S n) (S p)

  ||| Proof that the view covers all possible cases.
  export
  view : (n : Nat) -> (0 p : HasLength xs n) -> View xs n p
  view Z Z = Z
  view (S n) (S p) = S n p

------------------------------------------------------------------------
-- Examples

-- /!\ Do NOT re-export these examples

listTerminating : (p : Subset Nat (HasLength xs)) -> HasLength (xs ++ [x]) (S (fst p))
listTerminating p = case view p of
  Z => S Z
  S p => S (listTerminating p)

data P : List Nat -> Type where
  PNil : P []
  PCon : P (map f xs) -> P (x :: xs)

covering
notListTerminating : (p : Subset Nat (HasLength xs)) -> P xs
notListTerminating p = case view p of
  Z => PNil
  S p => PCon (notListTerminating {xs = map id (tail xs)} ({ snd $= map id } p))

natTerminating : (n : Nat) -> (0 p : HasLength xs n) -> P xs
natTerminating n p = case view n p of
  Z => PNil
  S n p => PCon (natTerminating n (map id p))


text:
Y : Type
X : Type
Term : Type -> Type

erase : Term a -> Y

unc : (x : Term a) -> erase x = y -> (x : Term a ** erase x = y)
unc x p = (x ** p)

f : (x : Term a) -> erase x = y -> X = a -> (x' : Term X ** erase x' = y)
f x h p = rewrite p in unc x h


text:
module Utils.Hex

import Data.List
import Data.Primitives.Views

%default total

hexDigit : Int -> Char
hexDigit 0 = '0'
hexDigit 1 = '1'
hexDigit 2 = '2'
hexDigit 3 = '3'
hexDigit 4 = '4'
hexDigit 5 = '5'
hexDigit 6 = '6'
hexDigit 7 = '7'
hexDigit 8 = '8'
hexDigit 9 = '9'
hexDigit 10 = 'a'
hexDigit 11 = 'b'
hexDigit 12 = 'c'
hexDigit 13 = 'd'
hexDigit 14 = 'e'
hexDigit 15 = 'f'
hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below

||| Convert a positive integer into a list of (lower case) hexadecimal characters
export
asHex : Int -> String
asHex n =
  if n > 0
    then pack $ asHex' n []
    else "0"
  where
    asHex' : Int -> List Char -> List Char
    asHex' 0 hex = hex
    asHex' n hex with (n `divides` 16)
      asHex' (16 * div + rem) hex | DivBy div rem _ =
        asHex' (assert_smaller n div) (hexDigit rem :: hex)

export
leftPad : Char -> Nat -> String -> String
leftPad paddingChar padToLength str =
  if length str < padToLength
    then pack (List.replicate (minus padToLength (length str)) paddingChar) ++ str
    else str

export
fromHexDigit : Char -> Maybe Int
fromHexDigit '0' = Just 0
fromHexDigit '1' = Just 1
fromHexDigit '2' = Just 2
fromHexDigit '3' = Just 3
fromHexDigit '4' = Just 4
fromHexDigit '5' = Just 5
fromHexDigit '6' = Just 6
fromHexDigit '7' = Just 7
fromHexDigit '8' = Just 8
fromHexDigit '9' = Just 9
fromHexDigit 'a' = Just 10
fromHexDigit 'b' = Just 11
fromHexDigit 'c' = Just 12
fromHexDigit 'd' = Just 13
fromHexDigit 'e' = Just 14
fromHexDigit 'f' = Just 15
fromHexDigit _ = Nothing

export
fromHexChars : List Char -> Maybe Int
fromHexChars = fromHexChars' 1
  where
    fromHexChars' : Int -> List Char -> Maybe Int
    fromHexChars' _ [] = Just 0
    fromHexChars' m (d :: ds) = pure $ !(fromHexDigit (toLower d)) * m + !(fromHexChars' (m*16) ds)

export
fromHex : String -> Maybe Int
fromHex = fromHexChars . unpack


text:
module Graphexamples

import Graph
import data.Vect

am1 :(Vect 6 (Vect 6  Nat))
am1 = [[0,1,1,0,0,0],[1,0,1,0,0,0],[1,1,0,0,0,0],[0,0,0,0,1,0],[0,0,0,1,0,1],[0,0,0,0,1,0]]
am2:(Vect 6 (Vect 6  Nat))
am2 = [[0,1,1,0,0,0],[1,0,1,1,0,0],[1,1,0,0,0,1],[0,1,0,0,1,0],[0,0,0,1,0,1],[0,0,1,0,1,0]]
am3:(Vect 6 (Vect 6  Nat))
am3=[[0,1,1,0,0,0],[1,0,1,1,0,0],[1,1,0,0,0,0],[0,1,0,0,1,0],[0,0,0,1,0,0],[0,0,0,0,0,0]]
am4 : (Vect 8 (Vect 8  Nat))
am4 = [[0,1,1,0,0,0,0,0],[1,0,1,0,1,0,0,1],[1,1,0,1,0,0,0,0],[0,0,1,0,1,0,1,0],[0,1,0,1,0,1,1,0],[0,0,0,0,1,0,1,0],[0,0,0,1,1,1,0,0],[0,1,0,0,0,0,0,0]]

ConnectedComponents_of_am1 : List (List Nat )
ConnectedComponents_of_am1 = (ConnectedComponents am1)--[[6,5,4],[3,2,1]]

ConnectedComponents_of_am3 : List (List Nat )
ConnectedComponents_of_am3 = ConnectedComponents am3

Path_am4_2_7:Maybe  ( List Nat)
Path_am4_2_7 = (FindPath am4 2 7 )--Just ([2,1,3,4,7])

Path_am1_2_5:Maybe  ( List Nat)
Path_am1_2_5 = (FindPath am1 2 5 )--Nothing

PathProof_am4_2_7 :Maybe((List Nat),Path am4 2 7 )
PathProof_am4_2_7 = PathWithProof am4 2 7--Returns Path between 2 and 7 and a proof that it is a path.

PathProof_am1_2_5 :Maybe((List Nat),Path am1 2 5 )
PathProof_am1_2_5 = PathWithProof am1 2 5


text:
module Circuits.NetList.Linear.Usage

import Decidable.Equality

import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra

import Circuits.Common

import Circuits.NetList.Types

import public Circuits.NetList.Linear.Usage.DataType
import public Circuits.NetList.Linear.Usage.DataType.Use.Full
import public Circuits.NetList.Linear.Usage.DataType.Use.Partial

import public Circuits.NetList.Linear.Usage.TermType
import public Circuits.NetList.Linear.Usage.TermType.Use.Port
import public Circuits.NetList.Linear.Usage.TermType.Use.Channel

import public Circuits.NetList.Linear.Usage.Item
import public Circuits.NetList.Linear.Usage.Context

%default total

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

main : IO()
main = do
    putStr "Enter your name: "
    x <- getLine
    putStrLn ("Hello " ++ x ++ "!")


text:
> module Main

> import Data.So

> ifTrue        :   So True -> Nat
> ifTrue Oh     =   S Z

> ifFalse       :   So False -> Nat
> ifFalse Oh impossible

> test          :   (f : Nat -> Bool) -> (n : Nat) -> So (f n) -> Nat
> test f n x   with   (f n)
>               |   True     =  ifTrue  x
>               |   False    =  ifFalse x

> main : IO ()
> main = printLn (test ((S 4) ==) 5 Oh)

ext: lidr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module FCTypes

%default total

StringOrInt : Bool -> Type
StringOrInt b = case b of
                     False => String
                     True => Int

getStringOrInt : (b : Bool) -> StringOrInt b
getStringOrInt b = case b of
                        False => "94"
                        True => 94

valToString : (b : Bool) -> StringOrInt b -> String
valToString b val = case b of
                         False => val
                         True => cast val

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Network.Curl.Network

-- Networking via curl


text:
||| Convenience functions for working in Effectful functions.
module XML.DOM.Eff

import Effects
import Effect.Exception

import XML.DOM

%access export

getAttributeE : String
             -> Document ELEMENT
             -> {[EXCEPTION String]} Eff String
getAttributeE id n = case getAttribute id n of
  Just res => pure res
  Nothing  => raise $ "Element does not have: " ++ id

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml