text:
module Idris.REPL

import Compiler.Scheme.Chez
import Compiler.Scheme.Racket
import Compiler.Scheme.Gambit
import Compiler.ES.Node
import Compiler.ES.Javascript
import Compiler.Common

import Core.AutoSearch
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Env
import Core.InitPrimitives
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Termination
import Core.TT
import Core.Unify

import Parser.Unlit

import Idris.Desugar
import Idris.DocString
import Idris.Error
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands
import Idris.IDEMode.MakeClause
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Parser
import Idris.Pretty
import Idris.ProcessIdr
import Idris.Resugar
import public Idris.REPLCommon
import Idris.Syntax
import Idris.Version

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Interactive.CaseSplit
import TTImp.Interactive.ExprSearch
import TTImp.Interactive.GenerateDef
import TTImp.Interactive.MakeLemma
import TTImp.TTImp
import TTImp.ProcessDecls

import Data.List
import Data.Maybe
import Data.NameMap
import Data.Stream
import Data.Strings
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Util
import Text.PrettyPrint.Prettyprinter.Render.Terminal

import System
import System.File

%default covering

showInfo : {auto c : Ref Ctxt Defs} ->
           (Name, Int, GlobalDef) -> Core ()
showInfo (n, idx, d)
    = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++
                              show !(toFullNames (definition d)))
         coreLift $ putStrLn (show (multiplicity d))
         coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d))
         coreLift $ putStrLn ("Detaggable arg types: " ++ show (safeErase d))
         coreLift $ putStrLn ("Specialise args: " ++ show (specArgs d))
         coreLift $ putStrLn ("Inferrable args: " ++ show (inferrable d))
         case compexpr d of
              Nothing => pure ()
              Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr)
         coreLift $ putStrLn ("Refers to: " ++
                               show !(traverse getFullName (keys (refersTo d))))
         coreLift $ putStrLn ("Refers to (runtime): " ++
                               show !(traverse getFullName (keys (refersToRuntime d))))
         coreLift $ putStrLn ("Flags: " ++ show (flags d))
         when (not (isNil (sizeChange d))) $
            let scinfo = map (\s => show (fnCall s) ++ ": " ++
                                    show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
                coreLift $ putStrLn $
                        "Size change: " ++ showSep ", " scinfo

displayType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayType defs (n, i, gdef)
    = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
                pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm))
            (\num => prettyHole defs [] n num (type gdef))
            (isHole gdef)

getEnvTerm : {vars : _} ->
             List Name -> Env Term vars -> Term vars ->
             (vars' ** (Env Term vars', Term vars'))
getEnvTerm (n :: ns) env (Bind fc x b sc)
    = if n == x
         then getEnvTerm ns (b :: env) sc
         else (_ ** (env, Bind fc x b sc))
getEnvTerm _ env tm = (_ ** (env, tm))

displayTerm : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> ClosedTerm ->
              Core (Doc IdrisAnn)
displayTerm defs tm
    = do ptm <- resugar [] !(normaliseHoles defs [] tm)
         pure (prettyTerm ptm)

displayPatTerm : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Defs -> ClosedTerm ->
                 Core String
displayPatTerm defs tm
    = do ptm <- resugarNoPatvars [] !(normaliseHoles defs [] tm)
         pure (show ptm)

displayClause : {auto c : Ref Ctxt Defs} ->
                {auto s : Ref Syn SyntaxInfo} ->
                Defs -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core (Doc IdrisAnn)
displayClause defs (vs ** (env, lhs, rhs))
    = do lhstm <- resugar env !(normaliseHoles defs env lhs)
         rhstm <- resugar env !(normaliseHoles defs env rhs)
         pure (prettyTerm lhstm <++> equals <++> prettyTerm rhstm)

displayPats : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayPats defs (n, idx, gdef)
    = case definition gdef of
           PMDef _ _ _ _ pats
               => do ty <- displayType defs (n, idx, gdef)
                     ps <- traverse (displayClause defs) pats
                     pure (vsep (ty :: ps))
           _ => pure (pretty n <++> reflow "is not a pattern matching definition")

setOpt : {auto c : Ref Ctxt Defs} ->
         {auto o : Ref ROpts REPLOpts} ->
         REPLOpt -> Core ()
setOpt (ShowImplicits t)
    = do pp <- getPPrint
         setPPrint (record { showImplicits = t } pp)
setOpt (ShowNamespace t)
    = do pp <- getPPrint
         setPPrint (record { fullNamespace = t } pp)
setOpt (ShowTypes t)
    = do opts <- get ROpts
         put ROpts (record { showTypes = t } opts)
setOpt (EvalMode m)
    = do opts <- get ROpts
         put ROpts (record { evalMode = m } opts)
setOpt (Editor e)
    = do opts <- get ROpts
         put ROpts (record { editor = e } opts)
setOpt (CG e)
    = do defs <- get Ctxt
         case getCG (options defs) e of
            Just cg => setCG cg
            Nothing => iputStrLn (reflow "No such code generator available")

getOptions : {auto c : Ref Ctxt Defs} ->
         {auto o : Ref ROpts REPLOpts} ->
         Core (List REPLOpt)
getOptions = do
  pp <- getPPrint
  opts <- get ROpts
  pure $ [ ShowImplicits (showImplicits pp), ShowNamespace (fullNamespace pp)
         , ShowTypes (showTypes opts), EvalMode (evalMode opts)
         , Editor (editor opts)
         ]

export
findCG : {auto o : Ref ROpts REPLOpts} ->
         {auto c : Ref Ctxt Defs} -> Core Codegen
findCG
    = do defs <- get Ctxt
         case codegen (session (options defs)) of
              Chez => pure codegenChez
              Racket => pure codegenRacket
              Gambit => pure codegenGambit
              Node => pure codegenNode
              Javascript => pure codegenJavascript
              Other s => case !(getCodegen s) of
                            Just cg => pure cg
                            Nothing => do coreLift $ putStrLn ("No such code generator: " ++ s)
                                          coreLift $ exitWith (ExitFailure 1)

anyAt : (FC -> Bool) -> FC -> a -> Bool
anyAt p loc y = p loc

printClause : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Maybe String -> Nat -> ImpClause ->
              Core String
printClause l i (PatClause _ lhsraw rhsraw)
    = do lhs <- pterm lhsraw
         rhs <- pterm rhsraw
         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
printClause l i (WithClause _ lhsraw wvraw flags csraw)
    = do lhs <- pterm lhsraw
         wval <- pterm wvraw
         cs <- traverse (printClause l (i + 2)) csraw
         pure ((relit l ((pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n")) ++
                 showSep "\n" cs))
printClause l i (ImpossibleClause _ lhsraw)
    = do lhs <- pterm lhsraw
         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

lookupDefTyName : Name -> Context ->
                  Core (List (Name, Int, (Def, ClosedTerm)))
lookupDefTyName = lookupNameBy (\g => (definition g, type g))

public export
data EditResult : Type where
  DisplayEdit : Doc IdrisAnn -> EditResult
  EditError : Doc IdrisAnn -> EditResult
  MadeLemma : Maybe String -> Name -> PTerm -> String -> EditResult
  MadeWith : Maybe String -> List String -> EditResult
  MadeCase : Maybe String -> List String -> EditResult

updateFile : {auto r : Ref ROpts REPLOpts} ->
             (List String -> List String) -> Core EditResult
updateFile update
    = do opts <- get ROpts
         let Just f = mainfile opts
             | Nothing => pure (DisplayEdit emptyDoc) -- no file, nothing to do
         Right content <- coreLift $ readFile f
               | Left err => throw (FileErr f err)
         coreLift $ writeFile (f ++ "~") content
         coreLift $ writeFile f (unlines (update (lines content)))
         pure (DisplayEdit emptyDoc)

rtrim : String -> String
rtrim str = reverse (ltrim (reverse str))

addClause : String -> Nat -> List String -> List String
addClause c Z [] = rtrim c :: []
addClause c Z (x :: xs)
    = if all isSpace (unpack x)
         then rtrim c :: x :: xs
         else x :: addClause c Z xs
addClause c (S k) (x :: xs) = x :: addClause c k xs
addClause c (S k) [] = [c]

caseSplit : String -> Nat -> List String -> List String
caseSplit c Z (x :: xs) = rtrim c :: xs
caseSplit c (S k) (x :: xs) = x :: caseSplit c k xs
caseSplit c _ [] = [c]

proofSearch : Name -> String -> Nat -> List String -> List String
proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs
  where
    replaceStr : String -> String -> String -> String
    replaceStr rep new "" = ""
    replaceStr rep new str
        = if isPrefixOf rep str
             then new ++ pack (drop (length rep) (unpack str))
             else assert_total $ strCons (prim__strHead str)
                          (replaceStr rep new (prim__strTail str))
proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs
proofSearch n res _ [] = []

addMadeLemma : Maybe String -> Name -> String -> String -> Nat -> List String -> List String
addMadeLemma lit n ty app line content
    = addApp lit line [] (proofSearch n app line content)
  where
    -- Put n : ty in the first blank line
    insertInBlank : Maybe String -> List String -> List String
    insertInBlank lit [] = [relit lit $ show n ++ " : " ++ ty ++ "\n"]
    insertInBlank lit (x :: xs)
        = if trim x == ""
             then ("\n" ++ (relit lit $ show n ++ " : " ++ ty ++ "\n")) :: xs
             else x :: insertInBlank lit xs

    addApp : Maybe String -> Nat -> List String -> List String -> List String
    addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest
    addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs
    addApp _ (S k) acc [] = reverse acc

-- Replace a line; works for 'case' and 'with'
addMadeCase : Maybe String -> List String -> Nat -> List String -> List String
addMadeCase lit wapp line content
    = addW line [] content
  where
    addW : Nat -> List String -> List String -> List String
    addW Z acc (_ :: rest) = reverse acc ++ map (relit lit) wapp ++ rest
    addW Z acc [] = [] -- shouldn't happen!
    addW (S k) acc (x :: xs) = addW k (x :: acc) xs
    addW (S k) acc [] = reverse acc

nextProofSearch : {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  Core (Maybe (Name, RawImp))
nextProofSearch
    = do opts <- get ROpts
         let Just (n, res) = psResult opts
              | Nothing => pure Nothing
         Just (res, next) <- nextResult res
              | Nothing =>
                    do put ROpts (record { psResult = Nothing } opts)
                       pure Nothing
         put ROpts (record { psResult = Just (n, next) } opts)
         pure (Just (n, res))

nextGenDef : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto o : Ref ROpts REPLOpts} ->
             (reject : Nat) ->
             Core (Maybe (Int, (FC, List ImpClause)))
nextGenDef reject
    = do opts <- get ROpts
         let Just (line, res) = gdResult opts
              | Nothing => pure Nothing
         Just (res, next) <- nextResult res
              | Nothing =>
                    do put ROpts (record { gdResult = Nothing } opts)
                       pure Nothing
         put ROpts (record { gdResult = Just (line, next) } opts)
         case reject of
              Z => pure (Just (line, res))
              S k => nextGenDef k

dropLams : Nat -> RawImp -> RawImp
dropLams Z tm = tm
dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
dropLams _ tm = tm

dropLamsTm : {vars : _} ->
             Nat -> Env Term vars -> Term vars ->
             (vars' ** (Env Term vars', Term vars'))
dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))

processEdit : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              {auto o : Ref ROpts REPLOpts} ->
              EditCmd -> Core EditResult
processEdit (TypeAt line col name)
    = do defs <- get Ctxt
         glob <- lookupCtxtName name (gamma defs)
         res <- the (Core (Doc IdrisAnn)) $ case glob of
                     [] => pure emptyDoc
                     ts => do tys <- traverse (displayType defs) ts
                              pure (vsep tys)
         Just (n, num, t) <- findTypeAt (\p, n => within (line-1, col-1) p)
            | Nothing => case res of
                              Empty => throw (UndefinedName (MkFC "(interactive)" (0,0) (0,0)) name)
                              _     => pure (DisplayEdit res)
         case res of
            Empty => pure (DisplayEdit $ pretty (nameRoot n) <++> colon <++> !(displayTerm defs t))
            _     => pure (DisplayEdit emptyDoc)  -- ? Why () This means there is a global name and a type at (line,col)
processEdit (CaseSplit upd line col name)
    = do let find = if col > 0
                       then within (line-1, col-1)
                       else onLine (line-1)
         OK splits <- getSplits (anyAt find) name
             | SplitFail err => pure (EditError (pretty $ show err))
         lines <- updateCase splits (line-1) (col-1)
         if upd
            then updateFile (caseSplit (unlines lines) (integerToNat (cast (line - 1))))
            else pure $ DisplayEdit (vsep $ pretty <$> lines)
processEdit (AddClause upd line name)
    = do Just c <- getClause line name
             | Nothing => pure (EditError (pretty name <++> reflow "not defined here"))
         if upd
            then updateFile (addClause c (integerToNat (cast line)))
            else pure $ DisplayEdit (pretty c)
processEdit (ExprSearch upd line name hints)
    = do defs <- get Ctxt
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         case !(lookupDefName name (gamma defs)) of
              [(n, nidx, Hole locs _)] =>
                  do let searchtm = exprSearch replFC name []
                     ropts <- get ROpts
                     put ROpts (record { psResult = Just (name, searchtm) } ropts)
                     defs <- get Ctxt
                     Just (_, restm) <- nextProofSearch
                          | Nothing => pure $ EditError "No search results"
                     let tm' = dropLams locs restm
                     itm <- pterm tm'
                     let itm' : PTerm = if brack then addBracket replFC itm else itm
                     if upd
                        then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))
                        else pure $ DisplayEdit (prettyTerm itm')
              [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>
                  case holeInfo pi of
                       NotHole => pure $ EditError "Not a searchable hole"
                       SolvedHole locs =>
                          do let (_ ** (env, tm')) = dropLamsTm locs [] tm
                             itm <- resugar env tm'
                             let itm' : PTerm = if brack then addBracket replFC itm else itm
                             if upd
                                then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))
                                else pure $ DisplayEdit (prettyTerm itm')
              [] => pure $ EditError $ "Unknown name" <++> pretty name
              _ => pure $ EditError "Not a searchable hole"
processEdit ExprSearchNext
    = do defs <- get Ctxt
         syn <- get Syn
         Just (name, restm) <- nextProofSearch
              | Nothing => pure $ EditError "No more results"
         [(n, nidx, Hole locs _)] <- lookupDefName name (gamma defs)
              | _ => pure $ EditError "Not a searchable hole"
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         let tm' = dropLams locs restm
         itm <- pterm tm'
         let itm' : PTerm = if brack then addBracket replFC itm else itm
         pure $ DisplayEdit (prettyTerm itm')

processEdit (GenerateDef upd line name rej)
    = do defs <- get Ctxt
         Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)
             | Nothing => pure (EditError ("Can't find declaration for" <++> pretty name <++> "on line" <++> pretty line))
         case !(lookupDefExact n' (gamma defs)) of
              Just None =>
                 do let searchdef = makeDefSort (\p, n => onLine (line - 1) p)
                                                16 mostUsed n'
                    ropts <- get ROpts
                    put ROpts (record { gdResult = Just (line, searchdef) } ropts)
                    Just (_, (fc, cs)) <- nextGenDef rej
                         | Nothing => pure (EditError "No search results")
                    let l : Nat =  integerToNat (cast (snd (startPos fc)))
                    Just srcLine <- getSourceLine line
                       | Nothing => pure (EditError "Source line not found")
                    let (markM, srcLineUnlit) = isLitLine srcLine
                    ls <- traverse (printClause markM l) cs
                    if upd
                       then updateFile (addClause (unlines ls) (integerToNat (cast line)))
                       else pure $ DisplayEdit (vsep $ pretty <$> ls)
              Just _ => pure $ EditError "Already defined"
              Nothing => pure $ EditError $ "Can't find declaration for" <++> pretty name
processEdit GenerateDefNext
    = do Just (line, (fc, cs)) <- nextGenDef 0
              | Nothing => pure (EditError "No more results")
         let l : Nat =  integerToNat (cast (snd (startPos fc)))
         Just srcLine <- getSourceLine line
            | Nothing => pure (EditError "Source line not found")
         let (markM, srcLineUnlit) = isLitLine srcLine
         ls <- traverse (printClause markM l) cs
         pure $ DisplayEdit (vsep $ pretty <$> ls)
processEdit (MakeLemma upd line name)
    = do defs <- get Ctxt
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         case !(lookupDefTyName name (gamma defs)) of
              [(n, nidx, Hole locs _, ty)] =>
                  do (lty, lapp) <- makeLemma replFC name locs ty
                     pty <- pterm lty
                     papp <- pterm lapp
                     opts <- get ROpts
                     let pappstr = show (the PTerm (if brack
                                            then addBracket replFC papp
                                            else papp))
                     Just srcLine <- getSourceLine line
                       | Nothing => pure (EditError "Source line not found")
                     let (markM,_) = isLitLine srcLine
                     if upd
                        then updateFile (addMadeLemma markM name (show pty) pappstr
                                                      (max 0 (integerToNat (cast (line - 1)))))
                        else pure $ MadeLemma markM name pty pappstr
              _ => pure $ EditError "Can't make lifted definition"
processEdit (MakeCase upd line name)
    = do litStyle <- getLitStyle
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         Just src <- getSourceLine line
              | Nothing => pure (EditError "Source line not available")
         let Right l = unlit litStyle src
              | Left err => pure (EditError "Invalid literate Idris")
         let (markM, _) = isLitLine src
         let c = lines $ makeCase brack name l
         if upd
            then updateFile (addMadeCase markM c (max 0 (integerToNat (cast (line - 1)))))
            else pure $ MadeCase markM c
processEdit (MakeWith upd line name)
    = do litStyle <- getLitStyle
         Just src <- getSourceLine line
              | Nothing => pure (EditError "Source line not available")
         let Right l = unlit litStyle src
              | Left err => pure (EditError "Invalid literate Idris")
         let (markM, _) = isLitLine src
         let w = lines $ makeWith name l
         if upd
            then updateFile (addMadeCase markM w (max 0 (integerToNat (cast (line - 1)))))
            else pure $ MadeWith markM w

public export
data MissedResult : Type where
  CasesMissing : Name -> List String  -> MissedResult
  CallsNonCovering : Name -> List Name -> MissedResult
  AllCasesCovered : Name -> MissedResult

public export
data REPLResult : Type where
  Done : REPLResult
  REPLError : Doc IdrisAnn -> REPLResult
  Executed : PTerm -> REPLResult
  RequestedHelp : REPLResult
  Evaluated : PTerm -> (Maybe PTerm) -> REPLResult
  Printed : Doc IdrisAnn -> REPLResult
  TermChecked : PTerm -> PTerm -> REPLResult
  FileLoaded : String -> REPLResult
  ModuleLoaded : String -> REPLResult
  ErrorLoadingModule : String -> Error -> REPLResult
  ErrorLoadingFile : String -> FileError -> REPLResult
  ErrorsBuildingFile : String -> List Error -> REPLResult
  NoFileLoaded : REPLResult
  CurrentDirectory : String -> REPLResult
  CompilationFailed: REPLResult
  Compiled : String -> REPLResult
  CompiledLibrary : (String, List String) -> REPLResult
  ProofFound : PTerm -> REPLResult
  Missed : List MissedResult -> REPLResult
  CheckedTotal : List (Name, Totality) -> REPLResult
  FoundHoles : List HoleData -> REPLResult
  OptionsSet : List REPLOpt -> REPLResult
  LogLevelSet : LogLevel -> REPLResult
  ConsoleWidthSet : Maybe Nat -> REPLResult
  ColorSet : Bool -> REPLResult
  VersionIs : Version -> REPLResult
  DefDeclared : REPLResult
  Exited : REPLResult
  Edited : EditResult -> REPLResult

export
execExp : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          PTerm -> Core REPLResult
execExp ctm
    = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
         inidx <- resolveName (UN "[input]")
         (tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
                                 [] ttimp Nothing
         tm_erased <- linearCheck replFC linear True [] tm
         cgExecuteExpr !findCG tm_erased
         pure $ Executed ctm

execDecls : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            List PDecl -> Core REPLResult
execDecls decls = do
  traverse_ execDecl decls
  pure DefDeclared
  where
    execDecl : PDecl -> Core ()
    execDecl decl = do
      i <- desugarDecl [] decl
      traverse_ (processDecl [] (MkNested []) []) i

export
compileExp : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto m : Ref MD Metadata} ->
             {auto o : Ref ROpts REPLOpts} ->
             PTerm -> String -> Core REPLResult
compileExp ctm outfile
    = do inidx <- resolveName (UN "[input]")
         ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
         (tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
                               [] ttimp Nothing
         tm_erased <- linearCheck replFC linear True [] tm
         ok <- cgCompileExpr !findCG tm_erased outfile
         maybe (pure CompilationFailed)
               (pure . Compiled)
               ok

export
compileLib : {auto c : Ref Ctxt Defs} ->
             {auto o : Ref ROpts REPLOpts} ->
             (libName : String) ->
             (changedModules : Maybe (List ModuleIdent)) ->
             Core REPLResult
compileLib libName changedModules = do
  ok <- cgCompileLibrary !findCG libName changedModules
  maybe (pure CompilationFailed)
        (pure . CompiledLibrary)
        ok

export
loadMainFile : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               String -> Core REPLResult
loadMainFile f
    = do resetContext
         Right res <- coreLift (readFile f)
            | Left err => do setSource ""
                             pure (ErrorLoadingFile f err)
         errs <- logTime "+ Build deps" $ buildDeps f
         updateErrorLine errs
         setSource res
         resetProofState
         case errs of
           [] => pure (FileLoaded f)
           _ => pure (ErrorsBuildingFile f errs)

||| Process a single `REPLCmd`
|||
||| Returns `REPLResult` for display by the higher level shell which
||| is invoking this interactive command processing.
export
process : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          REPLCmd -> Core REPLResult
process (NewDefn decls) = execDecls decls
process (Eval itm)
    = do opts <- get ROpts
         case evalMode opts of
            Execute => do execExp itm; pure (Executed itm)
            _ =>
              do ttimp <- desugar AnyExpr [] itm
                 inidx <- resolveName (UN "[input]")
                 -- a TMP HACK to prioritise list syntax for List: hide
                 -- foreign argument lists. TODO: once the new FFI is fully
                 -- up and running we won't need this. Also, if we add
                 -- 'with' disambiguation we can use that instead.
                 catch (do hide replFC (NS primIONS (UN "::"))
                           hide replFC (NS primIONS (UN "Nil")))
                       (\err => pure ())
                 (tm, gty) <- elabTerm inidx (emode (evalMode opts)) [] (MkNested [])
                                       [] ttimp Nothing
                 logTerm "repl.eval" 10 "Elaborated input" tm
                 defs <- get Ctxt
                 opts <- get ROpts
                 let norm = nfun (evalMode opts)
                 ntm <- norm defs [] tm
                 logTermNF "repl.eval" 5 "Normalised" [] ntm
                 itm <- resugar [] ntm
                 if showTypes opts
                    then do ty <- getTerm gty
                            ity <- resugar [] !(norm defs [] ty)
                            pure (Evaluated itm (Just ity))
                    else pure (Evaluated itm Nothing)
  where
    emode : REPLEval -> ElabMode
    emode EvalTC = InType
    emode _ = InExpr

    nfun : {vs : _} ->
           REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
    nfun NormaliseAll = normaliseAll
    nfun _ = normalise
process (Check (PRef fc fn))
    = do defs <- get Ctxt
         case !(lookupCtxtName fn (gamma defs)) of
              [] => throw (UndefinedName fc fn)
              ts => do tys <- traverse (displayType defs) ts
                       pure (Printed $ vsep tys)
process (Check itm)
    = do inidx <- resolveName (UN "[input]")
         ttimp <- desugar AnyExpr [] itm
         (tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
                                  [] ttimp Nothing
         defs <- get Ctxt
         itm <- resugar [] !(normaliseHoles defs [] tm)
         ty <- getTerm gty
         ity <- resugar [] !(normaliseScope defs [] ty)
         pure (TermChecked itm ity)
process (PrintDef fn)
    = do defs <- get Ctxt
         case !(lookupCtxtName fn (gamma defs)) of
              [] => throw (UndefinedName replFC fn)
              ts => do defs <- traverse (displayPats defs) ts
                       pure (Printed $ vsep defs)
process Reload
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => pure NoFileLoaded
              Just f => loadMainFile f
process (Load f)
    = do opts <- get ROpts
         put ROpts (record { mainfile = Just f } opts)
         -- Clear the context and load again
         loadMainFile f
process (ImportMod m)
    = do catch (do addImport (MkImport emptyFC False m (miAsNamespace m))
                   pure $ ModuleLoaded (show m))
               (\err => pure $ ErrorLoadingModule (show m) err)
process (CD dir)
    = do setWorkingDir dir
         workDir <- getWorkingDir
         pure (CurrentDirectory workDir)
process CWD
    = do workDir <- getWorkingDir
         pure (CurrentDirectory workDir)
process Edit
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => pure NoFileLoaded
              Just f =>
                do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
                   coreLift $ system (editor opts ++ " " ++ f ++ line)
                   loadMainFile f
process (Compile ctm outfile)
    = compileExp ctm outfile
process (Exec ctm)
    = execExp ctm
process Help
    = pure RequestedHelp
process (ProofSearch n_in)
    = do defs <- get Ctxt
         [(n, i, ty)] <- lookupTyName n_in (gamma defs)
              | [] => throw (UndefinedName replFC n_in)
              | ns => throw (AmbiguousName replFC (map fst ns))
         tm <- search replFC top False 1000 n ty []
         itm <- resugar [] !(normaliseHoles defs [] tm)
         pure $ ProofFound itm
process (Missing n)
    = do defs <- get Ctxt
         case !(lookupCtxtName n (gamma defs)) of
              [] => throw (UndefinedName replFC n)
              ts => map Missed $ traverse (\fn =>
                                         do tot <- getTotality replFC fn
                                            the (Core MissedResult) $ case isCovering tot of
                                                 MissingCases cs =>
                                                    do tms <- traverse (displayPatTerm defs) cs
                                                       pure $ CasesMissing fn tms
                                                 NonCoveringCall ns_in =>
                                                   do ns <- traverse getFullName ns_in
                                                      pure $ CallsNonCovering fn ns
                                                 _ => pure $ AllCasesCovered fn)
                               (map fst ts)
process (Total n)
    = do defs <- get Ctxt
         case !(lookupCtxtName n (gamma defs)) of
              [] => throw (UndefinedName replFC n)
              ts => map CheckedTotal $
                    traverse (\fn =>
                          do checkTotal replFC fn
                             tot <- getTotality replFC fn >>= toFullNames
                             pure $ (fn, tot))
                               (map fst ts)
process (Doc n)
    = do doc <- getDocsFor replFC n
         pure $ Printed $ vsep $ pretty <$> doc
process (Browse ns)
    = do doc <- getContents ns
         pure $ Printed $ vsep $ pretty <$> doc
process (DebugInfo n)
    = do defs <- get Ctxt
         traverse_ showInfo !(lookupCtxtName n (gamma defs))
         pure Done
process (SetOpt opt)
    = do setOpt opt
         pure Done
process GetOpts
    = do opts <- getOptions
         pure $ OptionsSet opts
process (SetLog lvl)
    = do addLogLevel lvl
         pure $ LogLevelSet lvl
process (SetConsoleWidth n)
    = do setConsoleWidth n
         pure $ ConsoleWidthSet n
process (SetColor b)
    = do setColor b
         pure $ ColorSet b
process Metavars
    = do defs <- get Ctxt
         let ctxt = gamma defs
         ms  <- getUserHoles
         let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
         let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
                                                           pure (n, gdef, args))
                                      globs
         hData <- the (Core $ List HoleData) $
             traverse (\n_gdef_args =>
                        -- Inference can't deal with this for now :/
                        let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
                        holeData defs [] n args (type gdef))
                      holesWithArgs
         pure $ FoundHoles hData

process (Editing cmd)
    = do ppopts <- getPPrint
         -- Since we're working in a local environment, don't do the usual
         -- thing of printing out the full environment for parameterised
         -- calls or calls in where blocks
         setPPrint (record { showFullEnv = False } ppopts)
         res <- processEdit cmd
         setPPrint ppopts
         pure $ Edited res
process (CGDirective str)
    = do setSession (record { directives $= (str::) } !getSession)
         pure Done
process Quit
    = pure Exited
process NOP
    = pure Done
process ShowVersion
    = pure $ VersionIs  version

processCatch : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               REPLCmd -> Core REPLResult
processCatch cmd
    = do c' <- branch
         u' <- get UST
         s' <- get Syn
         o' <- get ROpts
         catch (do r <- process cmd
                   commit
                   pure r)
               (\err => do put Ctxt c'
                           put UST u'
                           put Syn s'
                           put ROpts o'
                           msg <- display err
                           pure $ REPLError msg
                           )

parseEmptyCmd : SourceEmptyRule (Maybe REPLCmd)
parseEmptyCmd = eoi *> (pure Nothing)

parseCmd : SourceEmptyRule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c

export
parseRepl : String -> Either (ParseError Token) (Maybe REPLCmd)
parseRepl inp
    = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
           Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)
           Just cmd => Right $ Just cmd
  where
    -- a right load of hackery - we can't tokenise the filename using the
    -- ordinary parser. There's probably a better way...
    getLoad : Nat -> (String -> REPLCmd) -> String -> Maybe REPLCmd
    getLoad n cmd str = Just (cmd (trim (substr n (length str) str)))

    fnameCmd : List (String, String -> REPLCmd) -> String -> Maybe REPLCmd
    fnameCmd [] inp = Nothing
    fnameCmd ((pre, cmd) :: rest) inp
        = if isPrefixOf pre inp
             then getLoad (length pre) cmd inp
             else fnameCmd rest inp

export
interpret : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            String -> Core REPLResult
interpret inp
    = case parseRepl inp of
           Left err => pure $ REPLError (pretty err)
           Right Nothing => pure Done
           Right (Just cmd) => do
             setCurrentElabSource inp
             processCatch cmd

mutual
  export
  replCmd : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            String -> Core ()
  replCmd "" = pure ()
  replCmd cmd
      = do res <- interpret cmd
           displayResult res

  export
  repl : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} ->
         Core ()
  repl
      = do ns <- getNS
           opts <- get ROpts
           coreLift (putStr (prompt (evalMode opts) ++ show ns ++ "> "))
           inp <- coreLift getLine
           end <- coreLift $ fEOF stdin
           if end
             then do
               -- start a new line in REPL mode (not relevant in IDE mode)
               coreLift $ putStrLn ""
               iputStrLn $ pretty "Bye for now!"
              else do res <- interpret inp
                      handleResult res

    where
      prompt : REPLEval -> String
      prompt EvalTC = "[tc] "
      prompt NormaliseAll = ""
      prompt Execute = "[exec] "

  export
  handleMissing' : MissedResult -> String
  handleMissing' (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
  handleMissing' (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
                                           ++ (case ns of
                                                 [f] => " " ++ show f
                                                 _ => "s: " ++ showSep ", " (map show ns)))
  handleMissing' (AllCasesCovered fn) = show fn ++ ": All cases covered"

  export
  handleMissing : MissedResult -> Doc IdrisAnn
  handleMissing (CasesMissing x xs) = pretty x <+> colon <++> vsep (code . pretty <$> xs)
  handleMissing (CallsNonCovering fn ns) =
    pretty fn <+> colon <++> reflow "Calls non covering"
      <++> (case ns of
                 [f] => "function" <++> code (pretty f)
                 _ => "functions:" <++> concatWith (surround (comma <+> space)) (code . pretty <$> ns))
  handleMissing (AllCasesCovered fn) = pretty fn <+> colon <++> reflow "All cases covered"

  export
  handleResult : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  handleResult Exited = iputStrLn (reflow "Bye for now!")
  handleResult other = do { displayResult other ; repl }

  export
  displayResult : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  displayResult (REPLError err) = printError err
  displayResult (Evaluated x Nothing) = printResult $ prettyTerm x
  displayResult (Evaluated x (Just y)) = printResult (prettyTerm x <++> colon <++> code (prettyTerm y))
  displayResult (Printed xs) = printResult xs
  displayResult (TermChecked x y) = printResult (prettyTerm x <++> colon <++> code (prettyTerm y))
  displayResult (FileLoaded x) = printResult (reflow "Loaded file" <++> pretty x)
  displayResult (ModuleLoaded x) = printResult (reflow "Imported module" <++> pretty x)
  displayResult (ErrorLoadingModule x err) = printResult (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err))
  displayResult (ErrorLoadingFile x err) = printResult (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
  displayResult (ErrorsBuildingFile x errs) = printResult (reflow "Error(s) building file" <++> pretty x) -- messages already displayed while building
  displayResult NoFileLoaded = printError (reflow "No file can be reloaded")
  displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> squotes (pretty dir))
  displayResult CompilationFailed = printError (reflow "Compilation failed")
  displayResult (Compiled f) = printResult (pretty "File" <++> pretty f <++> pretty "written")
  displayResult (CompiledLibrary (libName, files)) = printResult (pretty "Compiled" <++> pretty libName)
  displayResult (ProofFound x) = printResult (prettyTerm x)
  displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
  displayResult (CheckedTotal xs) = printResult (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
  displayResult (FoundHoles []) = printResult (reflow "No holes")
  displayResult (FoundHoles [x]) = printResult (reflow "1 hole" <+> colon <++> pretty x.name)
  displayResult (FoundHoles xs) = do
    let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
    printResult (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
  displayResult (LogLevelSet k) = printResult (reflow "Set loglevel to" <++> pretty k)
  displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)
  displayResult (ConsoleWidthSet Nothing) = printResult (reflow "Set consolewidth to auto")
  displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))
  displayResult (VersionIs x) = printResult (pretty (showVersion True x))
  displayResult (RequestedHelp) = printResult (pretty displayHelp)
  displayResult (Edited (DisplayEdit Empty)) = pure ()
  displayResult (Edited (DisplayEdit xs)) = printResult xs
  displayResult (Edited (EditError x)) = printError x
  displayResult (Edited (MadeLemma lit name pty pappstr)) = printResult $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
  displayResult (Edited (MadeWith lit wapp)) = printResult $ pretty $ showSep "\n" (map (relit lit) wapp)
  displayResult (Edited (MadeCase lit cstr)) = printResult $ pretty $ showSep "\n" (map (relit lit) cstr)
  displayResult (OptionsSet opts) = printResult (vsep (pretty <$> opts))
  displayResult _ = pure ()

  export
  displayHelp : String
  displayHelp =
    showSep "\n" $ map cmdInfo help
    where
      makeSpace : Nat -> String
      makeSpace n = pack $ take n (repeat ' ')

      col : Nat -> Nat -> String -> String -> String -> String
      col c1 c2 l m r =
        l ++ (makeSpace $ c1 `minus` length l) ++
        m ++ (makeSpace $ c2 `minus` length m) ++ r

      cmdInfo : (List String, CmdArg, String) -> String
      cmdInfo (cmds, args, text) = " " ++ col 16 12 (showSep " " cmds) (show args) text

  export
  displayErrors : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  displayErrors (ErrorLoadingFile x err) = printError (reflow "File error in" <++> pretty x <+> colon <++> pretty (show err))
  displayErrors _ = pure ()


text:
module Oyster.Core

import Data.Strings
import Oyster.Helper

%default total

-- the basic parser type

export
data Parser : Type -> Type where
  MkParser : (String -> List (a, String)) -> Parser a

export
parse : Parser a -> String -> List (a, String)
parse (MkParser p) str = p str

-- the primitive parser

||| Parser that consumes a single character
export
item : Parser Char
item = MkParser (\str => case strM str of
                          StrNil => []
                          StrCons c cs => [(c, cs)])

-- make Parser a monad so that we can use the `do`
-- notation (as well as making it fully generic)

export
Functor Parser where
  -- map : (a -> b) -> Parser a -> Parser b
  map f p = MkParser (\str => case parse p str of
                                [(x, rest)] => [(f x, rest)]
                                _ => [])

export
Applicative Parser where
  -- pure : a -> Parser a
  pure x = MkParser (\str => [(x, str)])

  -- (<*>) : Parser (a -> b) -> Parser a -> Parser b
  pf <*> px = MkParser (\str => case parse pf str of
                                  [(f, rest)] => parse (map f px) rest
                                  _ => [])

export
Monad Parser where
  -- (>>=) : Parser a -> (a -> Parser b) -> Parser b
  p >>= f = MkParser (\str => case parse p str of
                                [(x, rest)] => parse (f x) rest
                                _ => [])

-- make the parser into an alternative for choice
-- combination

partial
export
Alternative Parser where
  -- empty : Parser a
  empty = MkParser (\str => [])

  -- (<|>) : Parser a -> Parser a -> Parser a
  p <|> q = MkParser (\str => case parse p str of
                                [] => parse q str
                                [(x, rest)] => [(x, rest)])

mutual
  export partial
  some : Parser a -> Parser (List a)
  some x = pure (::) <*> x <*> many x

  export partial
  many : Parser a -> Parser (List a)
  many x = some x <|> pure []

-- derived primitives

sat : (Char -> Bool) -> Parser Char
sat p = do x <- item
           if p x then pure x else empty

digit : Parser Char
digit = sat isDigit

lower : Parser Char
lower = sat isLower

upper : Parser Char
upper = sat isUpper

letter : Parser Char
letter = sat isAlpha

alphanum : Parser Char
alphanum = sat isAlphaNum

char : Char -> Parser Char
char c = sat (== c)

partial
string : String -> Parser String
string str = stringHelper (strM str) where
  stringHelper : { s : String } -> StrM s -> Parser String
  stringHelper StrNil = pure ""
  stringHelper (StrCons c cs) = do char c
                                   stringHelper (strM cs)
                                   pure (strCons c cs)

export partial
ident : Parser String
ident = do c <- lower
           cs <- many alphanum
           pure (listCharToString (c :: cs))

partial
nat : Parser Nat
nat = do ds <- some digit
         pure (stringToNatOrZ (listCharToString ds))

partial
space : Parser ()
space = do many (sat isSpace)
           pure ()

partial
int : Parser Int
int = do char '-'
         n <- nat
         pure (-(natToInt n))
      <|> do n <- nat
             pure (natToInt n)

export partial
token : Parser a -> Parser a
token p = do space
             v <- p
             space
             pure v

export partial
identifier : Parser String
identifier = token ident

export partial
natural : Parser Nat
natural = token nat

export partial
integer : Parser Int
integer = token int

export partial
symbol : String -> Parser String
symbol s = token (string s)

ext: idr

max_stars_repo_name: timmyjose-compilers/oyster

max_issues_repo_name: timmyjose-compilers/oyster

max_forks_repo_name: timmyjose-compilers/oyster


text:
module Entscheidbar

data Entscheidbar : (behauptung:Type) -> Type where
  Ja : (beweis : behauptung) -> Entscheidbar behauptung
  Nein : (widerspruch : behauptung -> Void) -> Entscheidbar behauptung

NullUngleichNachfolger : Nat -> (Z = S k) -> Void
NullUngleichNachfolger _ Refl impossible

NachfolgerUngleichNull : Nat -> (S k = Z) -> Void
NachfolgerUngleichNull _ Refl impossible

auchNichtGleich : (a = b -> Void) -> (S a = S b) -> Void
auchNichtGleich wid Refl = wid Refl

sindGleich : (n : Nat) -> (m : Nat) -> Entscheidbar (n = m)
sindGleich Z Z = Ja Refl
sindGleich Z (S k) = Nein (NullUngleichNachfolger k)
sindGleich (S k) Z = Nein (NachfolgerUngleichNull k)
sindGleich (S k) (S j) =
  case sindGleich k j of
    Ja prf => Ja (cong prf)
    Nein wid => Nein (auchNichtGleich wid)

sindGleich' : (n : Nat) -> (m : Nat) -> Dec (n = m)
sindGleich' Z Z = Yes Refl
sindGleich' Z (S k) = No (NullUngleichNachfolger k)
sindGleich' (S k) Z = No (NachfolgerUngleichNull k)
sindGleich' (S k) (S j) =
  case sindGleich' k j of
    Yes prf => Yes (cong prf)
    No wid => No (auchNichtGleich wid)


text:
module Main

import Json
import JsonDSL
import AST
import Effects
import Effect.System
import Effect.StdIO
import Effect.State
import IdrisNet.TCP.TCPServer

processReq : List EFFECT -> Type
processReq effects = (String -> Maybe PMJsonValue -> { effects } Eff (Either ErrorCode PMJsonValue))

handleObject : processReq effects -> Object -> { effects } Eff (Maybe Object)
handleObject f (Request method params id) = do
  out <- f method params
  return . Just $ case out of
    (Right result) => Result result id
    (Left InvalidParams) => Error (ErrObj InvalidParams "Invalid params" Nothing) id
    (Left MethodNotFound) => Error (ErrObj MethodNotFound "Method not found" Nothing) id
handleObject f (Notification method params) = do
  _ <- f method params
  return Nothing
handleObject _ _ = return . Just $ Error (ErrObj InvalidRequest "Neither request nor notification" Nothing) JsonNull

handleObjects : processReq effects -> List Object -> { effects } Eff (List Object)
handleObjects _ [] = return []
handleObjects f (x::xs) = do
  obj <- handleObject f x
  case obj of
    Nothing => handleObjects f xs
    Just result => do
      next <- handleObjects f xs
      return $ result :: next

handlePacket : processReq effects -> Packet -> { effects } Eff (Maybe String)
handlePacket f (Single obj) = do
  out <- handleObject f obj
  return $ map (show . composeObject) out
handlePacket f (Batch l) = do
  pl <- handleObjects f l
  return $ case pl of
    [] => Nothing
    l => Just . show . composePacket . Batch $ l

handleStr : processReq effects -> String -> { effects } Eff (Maybe String)
handleStr f s = do
  case (parse jsonToplevelValue s) of
    (Left err) => return . Just . show . composeObject $
      Error (ErrObj ParseError "Packet parse error" Nothing) JsonNull
    (Right json) => do
      case (parsePacket $ toPM json) of
        Left obj => return . Just . show . composeObject $ obj
        Right packet => do
          out <- handlePacket f packet
          return out

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
module counts

export
counts : String -> (Nat, Nat)
counts str =
    let nwords = length (words str)
        nchars = length str in
            (nwords, nchars)

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
module CIL.FFI.Effects

import public CIL.FFI
import public Effects
import Effect.StdIO

%access export

implementation Handler StdIO CIL_IO where
  handle () (PutStr s) k = do putStr' s; k () ()
  handle () GetStr     k = do x <- getLine'; k x ()
  handle () (PutCh c)  k = do Write c; k () ()
  handle () GetCh      k = do x <- Read; k (cast x) ()

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Replica.Command.Set

import Data.List
import Data.String

import Replica.Help
import Replica.Option.Parse
import Replica.Option.Types
import public Replica.Option.Filter
import public Replica.Option.Global
import Replica.Other.Decorated

import Language.JSON

%default total

public export
data TargetConfig = Local | Global

export
Show TargetConfig where
  show Local = "Local"
  show Global = "Global"

export
Eq TargetConfig where
  Local == Local = True
  Global == Global = True
  _ == _ = False

public export
record Setter where
  constructor MkSetter
  key: String
  value: JSON

export
Show Setter where
  show (MkSetter key value) =
    "MkSetter \{show key} \{show value}"

public export
record SetCommand' (f : Type -> Type) where
  constructor MkSetCommand
  target : f TargetConfig
  setter : f Setter

public export
SetCommand : Type
SetCommand = Done SetCommand'

TyMap SetCommand' where
  tyMap func x =
    MkSetCommand (func x.target) (func x.setter)

TyTraversable SetCommand' where
  tyTraverse func x =
    [| MkSetCommand (func x.target) (func x.setter) |]

export
Show SetCommand where
  show x = "MkSetCommand \{show x.target} (\{show x.setter})"

targetPart : Part (Builder SetCommand') TargetConfig
targetPart = inj $ MkOption
  (toList1
    [ MkMod (singleton "local") ['l'] (Left Local)
      "Set a local config value (in `./.replica.json`) (default)"
    , MkMod (singleton "global") ['g'] (Left Global)
      "Set a global config value (in `$HOME/.replica.json`)"
    ])
  Local
  go
  where
    go : TargetConfig -> Builder SetCommand' -> Either String (Builder SetCommand')
    go = ifSame target (\x => record {target = Right $ x})
                       (const $ const "Contradictory target")

setterPart : Part (Builder SetCommand') Setter
setterPart = inj $ MkParam1
  "KEY=VALUE"
  parseKV
  go
  where
    go : Setter -> Builder SetCommand' -> Either String (Builder SetCommand')
    go s x = Right $ record {setter = Right $ s} x

    buildSetter : ConfigValue -> (String, String) -> Maybe Setter
    buildSetter x = map (uncurry MkSetter) . jsonFor x

    validateKV : String -> String -> Maybe Setter
    validateKV x y with (strM x, strM y)
      validateKV "" y | (StrNil, w) = Nothing
      validateKV x (prim__strCons '=' t) | (w, StrCons '=' t) =
        concatMap (flip buildSetter (x, t)) configValues
      validateKV x y | (w, z) = Nothing

    parseKV : String -> Maybe Setter
    parseKV x = uncurry validateKV $ break (== '=') x

optParseSet : OptParse (Builder SetCommand') SetCommand
optParseSet =
    [| MkSetCommand
       (liftAp targetPart)
       (liftAp setterPart)
    |]

defaultSet : Default SetCommand'
defaultSet = MkSetCommand
       (defaultPart targetPart)
       (defaultPart setterPart)

export
parseSet : List1 String -> ParseResult SetCommand
parseSet ("set":::xs) = do
    case parse (initBuilder $ defaultSet) optParseSet xs of
         InvalidMix reason => InvalidMix reason
         InvalidOption ys  => InvalidMix $ "Unknown option: " ++ ys.head
         Done builder      => maybe (InvalidMix "No test file given") Done $ build builder
parseSet xs = InvalidOption xs

export
helpSet : Help
helpSet = record {lastWords = Just footer} baseCommand
  where
    baseCommand : Help
    baseCommand = commandHelp {b = Builder SetCommand'}
      "set" "Set a global configuration for replica commands"
      (optParseSet)
      (Just "KEY=VALUE")
    footer : String
    footer =
      #"""
       Available keys, and description:
         replicaDir (or replica-dir, rDir) where replica stores internal information (default `./.replica`)
         goldenDir  (or golden-dir, gDir) where replica stores golden values (default `./.replica/tests`)
         colour     (or color) do we used colored output or not? (true or false, default `true`)
         ascii      do we keep away emojis or not? (true or false, default `false`)
         diff       command used to display diff
                    (known value: diff, git, native, other strings are considered as custom command)
                    (default: `native`)
         log        log level (default: `none`)
                    (known value: debug, info, warning, critical)
         testFile   (or jsonFile, test) the path of the test file to use (prefer a relative path)
                    (no default)
       """#

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module Decidable.Equality.Indexed

%default total
%access public export

interface DecEq iTy
       => DecEqIdx (iTy : Type)
                   (eTy : iTy -> Type) | eTy
  where
     decEq : {i,j : iTy}
          -> (x : eTy i)
          -> (y : eTy j)
          -> (prf : i = j)
          -> Dec (x = y)


text:
module Simple

x : Int
x = 2

y : Nat
y = 2 + ?a

---------- Proofs ----------

Simple.a = proof
  intro n
  exact 2

max_stars_repo_name: GoPavel/idris-proof

max_issues_repo_name: GoPavel/idris-proof

max_forks_repo_name: GoPavel/idris-proof


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

comp : (a -> b) -> (b -> c) -> a -> c
comp = ?baz

zipWith : (a -> b -> c) -> (1 xs : Vect n a) -> (1 ys : Vect n b) -> Vect n c
zipWith f [] [] = []
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

transposeHelper : Vect m a -> (1 xs_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)
transposeHelper xs ys = zipWith ?foo xs ys


text:
module EnumTypes

data Day = Monday
          | Tuesday
          | Wednesday
          | Thursday
          | Friday
          | Saturday
          | Sunday
%name Day day, day1, day2

nextWeekday : Day -> Day
nextWeekday Monday = Tuesday
nextWeekday Tuesday = Wednesday
nextWeekday Wednesday = Thursday
nextWeekday Thursday = Friday
nextWeekday Friday = Saturday
nextWeekday Saturday = Sunday
nextWeekday Sunday = Monday

testNextWeekday : (nextWeekday (nextWeekday Saturday)) = Monday
testNextWeekday = Refl


text:
interface (.defaultable) a where
  defa : a

(.defaultable) Int where
  defa = 0

f : Num a => a.defaultable => a -> a
f x = x + defa

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Test.Other

import Test.Unit
import Demo.Other

%access export

partial
testHello : IO Bool
testHello = genericTest
  (Just "testHello")
  hello
  "hello"
  (==)

partial
runTest : IO ()
runTest = do
  putStrLn "Testing Other"
  putStrLn infoLine
  NonReporting.runTests [ testHello ]

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
module SkepticLang.Main

import Language.JSON

import ListUtils
import PairUtils
import IOUtils
import JSONUtils

||| Core type representing a power-law equation.
public export
record Zipf where
  ||| Creates a power-law equation.
  |||
  ||| @amp    the scaling factor of the equation
  ||| @alpha  the exponent of the equation
  constructor MkZipf
  amp : Double
  alpha : Double

||| Represents a named power-law equation.
public export
NamedZipf : Type
NamedZipf = (String, Zipf)

||| Represents a group of named power-law equations.
public export
Group : Type
Group = List NamedZipf

||| Represents a named group of named power-law equations.
public export
NamedGroup : Type
NamedGroup = (String, Group)

||| Core type to carry environment (context) state.
public export
record Environment where
  ||| Creates an environment (context).
  |||
  ||| @dir        the path of the current working directory
  ||| @equations  a key-value collection of power-law equations
  ||| @groups     a key-value collection of groups of power-law equations
  constructor MkEnvironment
  dir : String
  equations : List NamedZipf
  groups : List NamedGroup

||| Represents a named slope calculated from a named power-law equation.
public export
NamedSlope : Type
NamedSlope = (String, Double)

||| For a power-law equation, computes y for a given x.
|||
||| @f  the equation
||| @x  the x-value
comp : (f : Zipf) -> (x : Double) -> Double
comp f x = (amp f) * (pow x (alpha f))

||| Computes the average slope of a function between two points.
|||
||| @a  the starting x-value
||| @b  the ending x-value
||| @z  the equation to compute for
slope : (a : Double) -> (b : Double) -> (z : Zipf) -> Double
slope a b z = (abs ((comp z a) - (comp z b))) / (abs (a - b))

||| Computes a named average slope of a named function between two points.
|||
||| @a  the starting x-value
||| @b  the ending x-value
||| @z  the named equation to compute for
namedSlope : (a : Double) -> (b : Double) -> (z : NamedZipf) -> NamedSlope
namedSlope a b (n, f) = (n, slope a b f)

||| Adds a Zipf equation to the environment.
|||
||| @env  the environment to add the equation to
||| @name the name to add the equation under
||| @eq   the equation to add
addZipf : (env : Environment) -> (name : String) -> (eq : Zipf) -> Environment
addZipf env name eq = MkEnvironment (dir env) ((name, eq) :: (equations env)) (groups env)

||| Gets a named Zipf equation from an environment by name.
|||
||| @env  the environment to get the equation from
||| @name the name of the equation to get
getZipf : (env : Environment) -> (name : String) -> Maybe Zipf
getZipf env name = lookup (equations env) name

||| Adds an empty group to an environment.
|||
||| @env  the environment to add the group to
||| @name the name for the new group
addGroup : (env : Environment) -> (name : String) -> Environment
addGroup env name = MkEnvironment (dir env) (equations env) ((name, []) :: (groups env))

||| Gets a group from an envionment by name.
|||
||| @env  the environment to get the group from
||| @name the name of the group to get
getGroup : (env : Environment) -> (name : String) -> Maybe Group
getGroup env name = lookup (groups env) name

||| Adds a named equation to a named group in an environment.
|||
||| @env        the environment to add the equation to
||| @groupName  the name of the group to add the equation to
||| @eq         the equation to add to the group
||| @eqName     the name within the group to bind the equation to
addToGroup : (env : Environment) -> (groupName : String) -> (eq : Zipf) -> (eqName : String) -> Maybe Environment
addToGroup env groupName eq eqName =
  case lookup (groups env) groupName of
    Just group =>
      let newGroup = ((eqName, eq) :: group) in
      Just (MkEnvironment (dir env) (equations env) ((groupName, newGroup) :: (groups env)))
    _ => Nothing

||| Loads a Zipf equation from a file.
|||
||| @path the file from which to load the equation
loadEq : (path : String) -> IO (Maybe Zipf)
loadEq path = do
  txt <- readFile path
  case txt of
    Right txt' => case JSON.parse txt' of
      Just json => case (getObjAttr json "amp", getObjAttr json "alpha") of
        (Just (JNumber amp), Just (JNumber alpha)) => pure (Just (MkZipf amp alpha))
        _ => pure Nothing
      _ => pure Nothing
    _ => pure Nothing

||| Returns a function defining a relation between numbers from a name.
|||
||| @name the name to use for the lookup
getRelation : (name : String) -> Maybe (Double -> Double -> Bool)
getRelation name = case name of
  "shallower" => Just (<)
  "steeper" => Just (>)
  _ => Nothing

||| Ranks equations in a group.
|||
||| @group  the group to rank
||| @a      the starting guess number
||| @b      the ending guess number
printRanked : (group : Group) -> (a : Double) -> (b : Double) -> IO ()
printRanked group a b =
  let vals = map (namedSlope a b) group in -- Equations to values.
  let sorted = sortBy compareSnd vals in -- Sort pairs by values.
  putStrLn (unwords (map (\(name, val) => name ++ ": " ++ cast val ++ "\n") sorted)) -- TODO: Prettier printing.

printRankedAlpha : (group : Group) -> IO ()
printRankedAlpha group =
  let sorted = sortBy (\a, b => compare (alpha (snd a)) (alpha (snd b))) group in -- Sort pairs by values.
  putStrLn (unwords (map (\(name, val) => name) sorted)) -- TODO: Prettier printing.

||| Prints an error message.
|||
||| @line the line number at which the error occurred
||| @msg  the message to show
printError : (line : Nat) -> (msg : String) -> IO ()
printError line msg = putStrLn $ "Error on line " ++ cast line ++ ": " ++ msg

||| Evaluates a tokenized line of Skeptic assertion code.
|||
||| @env    the environment to evaluate in
||| @tokens the tokens to evaluate
skepticEvalLineTokens : (env : Environment) -> (tokens : List String) -> (lnum : Nat) -> IO Environment
skepticEvalLineTokens env tokens lnum =
  case tokens of
  ["zipf", amp, alpha, "as", name] =>
    pure $ addZipf env name $ MkZipf (cast amp) (cast alpha) -- Declare Zipf equation directly.
  ["load", file, "as", name] => do
    eq <- loadEq $ joinPaths (dir env) file
    case eq of
      Just eq' => pure $ addZipf env name eq'
      Nothing => do
        printError lnum $ "Could not load equation file at " ++ file
        pure env
  ["group", name] =>
    pure $ addGroup env name
  ["add", eq, "to", group, "as", name] => do
    case getZipf env eq of
      Just eq' =>
        case addToGroup env group eq' name of
          Just env' =>
            pure env' -- Environment changed.
          _ => do
            printError lnum $ "Group " ++ group ++ " not found."
            pure env -- Environment unchanged.
      _ => do
        printError lnum $ "Equation " ++ eq ++ " not found."
        pure env -- Environment unchanged.
  ["assert", x, r, y] => do
    case (getZipf env x, getZipf env y, getRelation r) of -- Look up equations.
      (Just x', Just y', Just r') =>
        if r' (alpha x') (alpha y') then
          printError lnum $ unwords ["Failed to assert that", x, "is", r, "than", y]
        else
          pure () -- No output means success.
      _ => putStrLn "Equation error."
    pure env
  ["assert", bx, x, r, by, y] => do
    case (getGroup env x, getGroup env y, getRelation r) of -- Look up equations.
      (Just x', Just y', Just r') =>
        case (lookup x' bx, lookup y' by) of
          (Just xx', Just yy') =>
            if r' (alpha xx') (alpha yy') then
              printError lnum $ unwords ["Failed to assert that", bx, x, "is", r, "than", by, y]
            else
              pure () -- No output means success.
          _ => putStrLn "ERR" -- TODO: Opportunity for better error messages.
      _ => putStrLn "Equation error."
    pure env
  ["rank", group] => do
    case getGroup env group of
      Just group' =>
        printRankedAlpha group'
      _ =>
        printError lnum $ "No such group as " ++ group
    pure env
  "say" :: tokens' => do
    putStrLn (unwords tokens')
    pure env
  _ => do
    printError lnum $ "Failed to parse line."
    pure env

||| Remvoes empty strings from a list.
|||
||| @tokens the list to filter
stripEmptyTokens : (tokens : List String) -> List String
stripEmptyTokens tokens = filter (\x => length x > 0) tokens

||| Evaluates a line of Skeptic assertion code.
|||
||| @env  the environment to evaluate in
||| @line the line to evaluate
||| @lineNum  the current line number for reporting purposes
skepticEvalLine : (env : Environment) -> (line : String) -> (lineNum : Nat) -> IO Environment
skepticEvalLine env line lineNum =
  case unpack line of
    ('#' :: _) => pure env -- Ignore comments.
    _ =>
      case stripEmptyTokens (split (== ' ') line) of -- Split along spaces to create token list.
        [] => pure env -- Ignore blank lines.
        tokens => skepticEvalLineTokens env tokens lineNum -- Run line.

||| Evaluates lines of Skeptic assertion code.
|||
||| @env      the envronment to evaluate in
||| @lines    the lines to evaluate
||| @lineNum  the current line number for reporting purposes
skepticEvalLines : (env : Environment) -> (lines : List String) -> (lineNum : Nat) -> IO ()
skepticEvalLines env (line :: lines') lineNum = do
  env' <- skepticEvalLine env line lineNum -- Transform environment with current line.
  skepticEvalLines env' lines' $ lineNum + 1 -- Next line.
skepticEvalLines _ [] _ = pure ()

||| Evaluates a file of Skeptic assertion code.
|||
||| @path the lines to evaluate
skepticEvalFile : (path : String) -> IO ()
skepticEvalFile path = do
  absDirPath <- resolveAbsPath (dirName path) -- Absolute directory path needed.
  lines <- loadLines path -- Load entire source file.
  case lines of
    Just lines' => skepticEvalLines (MkEnvironment absDirPath [] []) lines' 1 -- New environment, start line 1.
    Nothing => putStrLn $ "Error: Could not read file at " ++ path -- File read error.

max_stars_repo_name: sr-lab/skeptic-lang

max_issues_repo_name: sr-lab/skeptic-lang

max_forks_repo_name: sr-lab/skeptic-lang


text:
module Minecraft.Core.Block.Export

import public Minecraft.Core.Block
import public Minecraft.Core.Tangible

%default total

public export
Block b => Tangible b where

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module NatPrimes

import InductiveTypes
import NatUtils
import NatOrder
import NatDivisors
import NatGCD

%default total
%access public export

----------------------------------------------------------------------------------------------

-- Definitions

|||A factorisation for a number
Factorisation : (n : Nat) -> Type
Factorisation n = (a : Nat ** (b : Nat ** ((LT 1 a, LT 1 b), n = a * b)))

|||Type of proof that a number is prime
isPrime : (p : Nat) -> Type
isPrime p = ((LT 1 p), {a : Nat} -> {b : Nat} -> (isDivisible (a * b) p) -> Either (isDivisible a p) (isDivisible b p))

|||Type of proof that a number is irreducible
isIrreducible : (p : Nat) -> Type
isIrreducible p = (a : Nat) -> (b : Nat) -> (p = a * b) -> Either (a = 1) (b = 1)

|||Type of proof that a number is the smallest divisor (greater than 1) of a given number
isMinDivisor : (n : Nat) -> (d : Nat) -> Type
isMinDivisor n d = ((LT 1 d), ((isDivisible n d), {k : Nat} -> (LT 1 k) -> (isDivisible n k) -> (LTE d k)))

-----------------------------------------------------------------------------------------------

--Basic Proofs

|||Proof that 1 < n implies n != 0
ltOneNotZ : {n : Nat} -> (LT 1 n) -> (Not (n = Z))
ltOneNotZ {n} ltProof = gtSuccImpliesNotZ n ltProof

|||Proof that p is irreducible and r < p, r ! = 0 implies r and p are coprime
remainderPrimeCoprime : {p : Nat} -> {r : Nat} ->
				    (isIrreducible p) -> (LNEQ r p) -> (Not (r = Z)) -> (coprime r p)
remainderPrimeCoprime {p} {r} proofIrreducible proofLNEQ rNotZ n (divr, (k ** (proofEq, notZ))) = case (proofIrreducible k n proofEq) of
	(Left kEq1) => void ((leqImpliesNotLNEQ (dividesImpliesGEQ (eqConservesDivisible divr Refl (sym (trans proofEq (trans (cong {f = (\a => a * n)} kEq1) (multOneLeftNeutral n))))) rNotZ)) proofLNEQ)
	(Right nEq1) => nEq1

|||Proof that if an irreducible does not divide a number, it is coprime to the number
irredNotDivIsCoprime : {p : Nat} -> (n : Nat) ->
				   (isIrreducible p) -> (Not (isDivisible n p)) -> (coprime n p)
irredNotDivIsCoprime {p} n proofIrreducible notDiv k (divRight, (l ** (proofEq, notZ))) =
	case (proofIrreducible l k proofEq) of
	(Left lEq1) => void (notDiv (eqConservesDivisible divRight Refl (sym (trans proofEq (trans (cong {f = (\a => a * k)} lEq1) (multOneLeftNeutral k))))))
	(Right kEq1) => kEq1

|||Proof that an irreducible either divides a number or is coprime to it
irreducibleDividesOrCoprime : {p : Nat} -> (n : Nat) -> (isIrreducible p) -> Either (isDivisible n p) (coprime n p)
irreducibleDividesOrCoprime {p} n proofIrreducible =
	case (decDivisible n p) of
		(Yes proofDiv) => (Left proofDiv)
		(No notDiv) => (Right (irredNotDivIsCoprime n proofIrreducible notDiv))

-----------------------------------------------------------------------------------------------

--Equivalence of irreducibility and primality in the naturals

|||Proof that a prime is irreducible
primeIsIrreducible : {p : Nat} -> (isPrime p) -> (isIrreducible p)
primeIsIrreducible {p} (proofLT, proofPrime) a b proofEq =
	case (proofPrime (1 ** ((rewrite (multOneLeftNeutral p) in (sym proofEq)), (ltOneNotZ proofLT)))) of
	(Left dividesA) =>
		case (dividesA) of
		(k ** (proofEq2, notZ)) => Right (sym (multLeftCancel p 1 b notZ (trans (rewrite (multOneRightNeutral p) in proofEq) (cong {f = (\n => n * b)} (multAntiSymmetric proofEq2 (trans proofEq (multCommutative a b)))))))
	(Right dividesB) =>
		case (dividesB) of
		(k ** (proofEq2, notZ)) => Left (sym (multRightCancel 1 a p notZ (trans (rewrite (multOneLeftNeutral p) in proofEq) (cong {f = (\n => a * n)} (multAntiSymmetric proofEq2 proofEq)))))

|||Proof that an irreducible greater than 1 is prime
irreducibleIsPrime : {p : Nat} -> (isIrreducible p) -> (LT 1 p) -> (isPrime p)
irreducibleIsPrime {p} proofIrreducible proofLT = (proofLT, proofPrime) where
	proofPrime : {a : Nat} -> {b : Nat} -> (isDivisible (a * b) p) -> Either (isDivisible a p) (isDivisible b p)
	proofPrime {a} {b} proofDiv =
		case (irreducibleDividesOrCoprime a proofIrreducible) of
		(Left divA) => (Left divA)
		(Right coprimeA) => (Right (coprimeImpliesDiv proofDiv coprimeA))

-----------------------------------------------------------------------------------------------

|||Proof that the smallest divisor is unique
minDivisorUnique : {n : Nat} -> {d1 : Nat} -> {d2 : Nat} ->
			    (isMinDivisor n d1) -> (isMinDivisor n d2) -> (d1 = d2)
minDivisorUnique {n} {d1} {d2} (ltLeft, (divLeft, minDivLeft)) (ltRight, (divRight, minDivRight)) = lteAntiSymmetric (minDivLeft ltRight divRight) (minDivRight ltLeft divLeft)

|||Proof that the smallest divisor of an irreducible is the irreducible itself
minDivOfIrreducible : {p : Nat} -> (LT 1 p) -> (isIrreducible p) -> (isMinDivisor p p)
minDivOfIrreducible {p} proofLT proofIrred = (proofLT, ((divisionReflexive (ltOneNotZ proofLT)), minDiv)) where
	minDiv : {n : Nat} -> (LT 1 n) -> (isDivisible p n) -> (LTE p n)
	minDiv {n} nLT1 (k ** (proofEq, notZ)) =
		case (proofIrred k n proofEq) of
		(Left kEq1) => lteSubstitutes lteRefl (sym (multOneLeftEqual proofEq kEq1)) Refl
		(Right nEq1) => void (succNotLTEzero (fromLteSucc (lteSubstitutes nLT1 Refl nEq1)))

----------------------------------------------------------------------------------------------


text:
import Data.List
import Data.List1
import Data.Vect
import Data.Vect.Elem
import Data.Vect.Extra
import Data.String.Parser

import System.File

Pos : Type
Pos = Vect 3 Integer

addVec : Pos -> Pos -> Pos
addVec [x1,y1,z1] [x2,y2,z2] = [x1+x2,y1+y2,z1+z2]

minVec : Pos -> Pos -> Pos
minVec [x1,y1,z1] [x2,y2,z2] = [x1-x2,y1-y2,z1-z2]

dist : Pos -> Pos -> Integer
dist p1 p2 = sum $ abs <$> minVec p1 p2

rotateVecZ : Vect 3 Integer -> List (Vect 3 Integer)
rotateVecZ [x,y,z] = [[x,y,z],[-y,x,z],[-x,-y,z],[y,-x,z]]

rotateVec3 : Vect 3 Integer -> List (Vect 3 Integer)
rotateVec3 [x,y,z] = join $ rotateVecZ <$> [[x,y,z],[-x,y,-z],[z,y,-x],[-z,y,x],[x,z,-y],[x,-z,y]]

Scanner : Type
Scanner = List Pos

Input : Type
Input = List1 Scanner

posParser : Parser Pos
posParser = do x <- integer
               skip $ char ','
               y <- integer
               skip $ char ','
               z <- integer
               pure [x, y, z]

some1 : Parser a -> Parser (List1 a)
some1 p = do Just s <- fromList <$> some p
               | Nothing => fail "none"
             pure s

scannerParser : Parser Scanner
scannerParser = token "---" *> token "scanner" *> lexeme natural *> token "---" *> some (posParser <* spaces)

parser : Parser Input
parser = some1 (scannerParser <* spaces)

rotateScanner : Scanner -> List Scanner
rotateScanner s = transpose $ rotateVec3 <$> s

moveRel : Scanner -> Pos -> Scanner
moveRel l p = map (addVec p) l

overlaps : Scanner -> Scanner -> Pos -> Bool
overlaps abs rels offset = (count ((flip elem) rels) $ (flip minVec) offset <$> abs) >= 12

overlap : Scanner -> Scanner -> Maybe (Scanner, Pos)
overlap abs rels = map (\f => (union abs $ moveRel rels f, f)) $ find (overlaps abs rels) $ (join $ (\a => minVec a <$> rels) <$> abs)

anyOverlap : Scanner -> List Scanner -> Maybe (Scanner, Pos)
anyOverlap abs [] = Nothing
anyOverlap abs (x :: xs) = overlap abs x <|> anyOverlap abs xs

findOverlap : Scanner -> List (List Scanner) -> Maybe (Scanner, Pos, List (List Scanner))
findOverlap abs [] = Nothing
findOverlap abs (rel :: rels) = case anyOverlap abs rel of
                                     Nothing => do (abs, offset, rels) <- findOverlap abs rels
                                                   pure (abs, offset, rel :: rels)
                                     (Just (abs, offset)) => Just (abs, offset, rels)

overlapall : Scanner -> List (List Scanner) -> IO (Maybe (Scanner, List Pos))
overlapall abs [] = pure $ Just (abs, [])
overlapall abs rels = do Just (abs, offset, rels) <- pure $ findOverlap abs rels
                           | Nothing => pure Nothing
                         putStrLn $ (show $ length rels) ++ "scanners left"
                         Just (all, offsets) <- overlapall abs rels
                           | Nothing => pure Nothing
                         pure $ Just (all, offset :: offsets)

part1and2 : Input -> IO String
part1and2 (x ::: xs) = do Just (bs, offsets) <- overlapall x (rotateScanner <$> xs)
                            | Nothing => pure "no overlap"
                          putStrLn $ show $ length bs
                          pure $ show $ foldl max 0 $ join $ (\o => dist o <$> offsets) <$> offsets

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1and2 a >>= putStrLn


text:
data X = A Int

(.la) : X -> Int
(.la) (A x) = x

f : X -> String
f x = show x.la

-- Projection does not define the usual function.
-- `g` does not typecheck without the `la` definition.
-- Moreover, they may have different implementations.

la : X -> Int
la $ A x = x + 1

g : X -> String
g x = show $ la x


text:
module Data.Functor.Product

import Data.Bifunctor
import Control.Comonad

%access public export

-- | `Product f g` is the product of the two functors `f` and `g`.
data Product : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  MkProduct : (f a, g a) -> Product f g a

--------------------------------------------------------------------------------
-- Functions
--------------------------------------------------------------------------------

product : f a -> g a -> Product f g a
product fa ga = MkProduct (fa, ga)

unwrapProduct : Product f g a -> (f a, g a)
unwrapProduct (MkProduct x) = x

bihoistProduct : (Functor f, Functor g, Functor h, Functor i) =>
                 ({a : Type} -> f a -> h a) ->
                 ({a : Type} -> g a -> i a) ->
                 ({a : Type} -> Product f g a -> Product h i a)
bihoistProduct natF natG (MkProduct e) = MkProduct (bimap natF natG e)

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

(Eq (f a), Eq (g a)) => Eq (Product f g a) where
  (MkProduct x) == (MkProduct y) = x == y

(Ord (f a), Ord (g a)) => Ord (Product f g a) where
  compare (MkProduct (l1, r1)) (MkProduct (l2, r2)) =
    case compare l1 l2 of
      EQ => compare r1 r2
      o => o

(Show (f a), Show (g a)) => Show (Product f g a) where
  show (MkProduct x) = "Product (" <+> show x <+> ")"

(Functor f, Functor g) => Functor (Product f g) where
  map f (MkProduct e) = MkProduct (bimap (map f) (map f) e)

(Applicative f, Applicative g) => Applicative (Product f g) where
  pure x = product (pure x) (pure x)
  (MkProduct (f, g)) <*> (MkProduct (a, b)) = product (f <*> a) (g <*> b)

(Monad f, Monad g) => Monad (Product f g) where
  (MkProduct (fa, ga)) >>= f =
    product (fa >>= fst . unwrapProduct . f) (ga >>= snd . unwrapProduct . f)

(Foldable f, Foldable g) => Foldable (Product f g) where
  foldr f z (MkProduct (fa, ga)) = foldr f (foldr f z ga) fa
  foldl f z (MkProduct (fa, ga)) = foldl f (foldl f z fa) ga

(Traversable f, Traversable g) => Traversable (Product f g) where
  traverse f (MkProduct (fa, ga)) = liftA2 product (traverse f fa) (traverse f ga)

max_stars_repo_name: Risto-Stevcev/idris-functors

max_issues_repo_name: Risto-Stevcev/idris-functors

max_forks_repo_name: Risto-Stevcev/idris-functors


text:
module Data.Group

%default total

%access public export

||| This extends 'Monoid' by defining an inverse for every element.
interface (Monoid t) => Group t where
  inverse : t -> t

||| Stream of elements starting at some given element.
generate : (Group g) => g -> Stream g
generate g1 = h where
  h = assert_total $ neutral :: map (<+> g1) h

||| (Positive) integer exponentiation.
exp : (Group g) => (n : Nat) -> g -> g
exp n g = (head . drop n) (generate g)

||| Whether a group element is idempotent
idempotent : (Eq g, Semigroup g) => g -> Bool
idempotent x = x == (x <+> x)

||| Commutator of two elements.
commutator : (Group g) => g -> g -> g
commutator a b = inverse a <+> inverse b <+> a <+> b

max_stars_repo_name: marcosh/permutations

max_issues_repo_name: marcosh/permutations

max_forks_repo_name: marcosh/permutations


text:
module B

import A


text:
module Idrboot

export
readBootCode : IO (Provider String)
readBootCode =
  case !(readFile "../rosetta-lisp/boot.lisp") of
    Right r => pure $ Provide r
    Left err => pure $ Error $ show err

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Streaming.Char

import Streaming
-- import Streaming.Internal

import Control.Monad.Trans

{- This module eventually provides ways of constructing streams of Char and some
   basic manipulations of them.
-}

export
lines : Monad m => Stream (Of Char) m a -> Stream (Stream (Of Char) m) m a
lines = split (=='\n')

export
words : Monad m => Stream (Of Char) m a -> Stream (Stream (Of Char) m) m a
words = split (==' ')

export
unlines : Monad m => Stream (Stream (Of Char) m) m a -> Stream (Of Char) m a
unlines str = intercalates (yield '\n') str <* yield '\n'

export
unwords : Monad m => Stream (Stream (Of Char) m) m a -> Stream (Of Char) m a
unwords = intercalates (yield ' ')


text:
module Circuits.NetList.Pretty

import System.File

import Data.String

import Data.Fin

import Text.Lexer
import Text.Parser

import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Toolkit.Data.List.DeBruijn
import Toolkit.Data.List.Occurs.Does
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree
import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

import Circuits.Common
import public Circuits.Common.Pretty

import Circuits.NetList.Error
import Circuits.NetList.AST
import Circuits.NetList.Types

import Circuits.NetList.Terms

export
Show AST where
  show (Var (MkRef span get))
    = "(Var \{get})"

  show (Port x y z (MkRef span get) scope)
    = "(Port \{show y} \{show z} \{show get} \{show scope})"

  show (Wire x y (MkRef span get) scope)
    = "(Wire \{show y} \{show get} \{show scope})"

  show (GateDecl x (MkRef span get) z scope)
    = "(Gate \{show get} \{show z} \{show scope})"

  show (Shim x y z)
    = "(Shim \{show y} \{show z})"

  show (Assign x y z w)
    = "(Assign \{show y} \{show z} \{show w})"

  show (Mux x y z w v)
    = "(Mux \{show y} \{show z} \{show w} \{show v})"

  show (GateU x y z w)
    = "(GateU \{show y} \{show z} \{show w})"

  show (GateB x y z w v)
    = "(GateB \{show y} \{show z} \{show w} \{show v})"

  show (Index x k y)
    = "(Index \{show k} \{show y})"

  show (Split x y z w)
    = "(Split \{show y} \{show z} \{show w})"

  show (Collect x y z w)
    = "(Collect \{show y} \{show z} \{show w})"

  show (Stop x)
    = "(Stop)"

toNat : IsVar ctxt type -> Nat
toNat (V pos prf) = pos

Show (Project dir) where
  show WRITE = "Write"
  show READ = "Read"

export
Show (Term ctxt type) where
  show (Var prf)
    = "(Var \{show (toNat prf)})"

  show (Port flow dtype body)
    = "(Port \{show flow} \{show dtype} \{show body})"

  show (Wire x body)
    = "(Wire \{show x} \{show body})"

  show (GateDecl g body)
    = "(Gate \{show g} \{show body})"

  show Stop
    = "Stop"

  show (Assign i o body)
    = "(Assign \{show i} <- \{show o} \{show body})"

  show (Index idir what idx)
    = "(Index \{show idir} \{show what} \{show idx})"

  show (Mux o c l r)
    = "(Mux \{show o} \{show c} \{show l} \{show r})"

  show (GateB x o l r)
    = "(GateB \{show x} \{show o} \{show l} \{show r})"

  show (GateU x o i)
    = "(GateU \{show x} \{show o} \{show i})"

  show (Collect o l r)
    = "(Collect \{show o} \{show l} \{show r})"

  show (Split l r i)
    = "(Split \{show l} \{show r} \{show i})"

  show (Project how what)
    = "(Project \{show how} \{show what})"

  show (Cast dir what)
    = "(Cast \{show dir} \{show what})"

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module TTImp.Impossible

import Core.Context
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import TTImp.TTImp
import TTImp.Elab.App

import Data.List
import Data.List1

%default covering

-- This file contains support for building a guess at the term on the LHS of an
-- 'impossible' case, in order to help build a tree of covered cases for
-- coverage checking. Since the LHS by definition won't be well typed, we are
-- only guessing! But we can still do some type-directed disambiguation of
-- names.
-- Constants (fromInteger/fromString etc) won't be supported, because in general
-- they involve resoling interfaces - they'll just become unmatchable patterns.

match : {auto c : Ref Ctxt Defs} ->
        NF [] -> (Name, Int, ClosedTerm) -> Core Bool
match nty (n, i, rty)
    = do defs <- get Ctxt
         rtynf <- nf defs [] rty
         sameRet nty rtynf
  where
    sameRet : NF [] -> NF [] -> Core Bool
    sameRet _ (NApp _ _ _) = pure True
    sameRet _ (NErased _ _) = pure True
    sameRet (NApp _ _ _) _ = pure True
    sameRet (NErased _ _) _ = pure True
    sameRet (NTCon _ n _ _ _) (NTCon _ n' _ _ _) = pure (n == n')
    sameRet (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
    sameRet (NType _) (NType _) = pure True
    sameRet nf (NBind fc _ (Pi _ _ _ _) sc)
        = do defs <- get Ctxt
             sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             sameRet nf sc'
    sameRet _ _ = pure False

dropNoMatch : {auto c : Ref Ctxt Defs} ->
              Maybe (NF []) -> List (Name, Int, GlobalDef) ->
              Core (List (Name, Int, GlobalDef))
dropNoMatch _ [t] = pure [t]
dropNoMatch Nothing ts = pure ts
dropNoMatch (Just nty) ts
    = -- if the return type of a thing in ts doesn't match nty, drop it
      filterM (match nty . map (map type)) ts

nextVar : {auto q : Ref QVar Int} ->
          FC -> Core (Term [])
nextVar fc
    = do i <- get QVar
         put QVar (i + 1)
         pure (Ref fc Bound (MN "imp" i))

badClause : Term [] -> List RawImp -> List RawImp -> List (Name, RawImp) -> Core a
badClause fn exps autos named
   = throw (GenericMsg (getLoc fn)
            ("Badly formed impossible clause "
               ++ show (fn, exps, autos, named)))

mutual
  processArgs : {auto c : Ref Ctxt Defs} ->
                {auto q : Ref QVar Int} ->
                Term [] -> NF [] ->
                (expargs : List RawImp) ->
                (autoargs : List RawImp) ->
                (namedargs : List (Name, RawImp)) ->
                Core ClosedTerm
  -- unnamed takes priority
  processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
     = do e' <- mkTerm e (Just ty) [] [] []
          defs <- get Ctxt
          processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                      exps autos named
  processArgs fn (NBind fc x (Pi _ _ Explicit ty) sc) [] autos named
     = do defs <- get Ctxt
          case findNamed x named of
            Just ((_, e), named') =>
               do e' <- mkTerm e (Just ty) [] [] []
                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                              [] autos named'
            Nothing => badClause fn [] autos named
  processArgs fn (NBind fc x (Pi _ _ Implicit ty) sc) exps autos named
     = do defs <- get Ctxt
          case findNamed x named of
            Nothing => do e' <- nextVar fc
                          processArgs (App fc fn e')
                                      !(sc defs (toClosure defaultOpts [] e'))
                                      exps autos named
            Just ((_, e), named') =>
               do e' <- mkTerm e (Just ty) [] [] []
                  processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                              exps autos named'
  processArgs fn (NBind fc x (Pi _ _ AutoImplicit ty) sc) exps autos named
     = do defs <- get Ctxt
          case autos of
               (e :: autos') => -- unnamed takes priority
                   do e' <- mkTerm e (Just ty) [] [] []
                      processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                                  exps autos' named
               [] =>
                  case findNamed x named of
                     Nothing =>
                        do e' <- nextVar fc
                           processArgs (App fc fn e')
                                       !(sc defs (toClosure defaultOpts [] e'))
                                       exps [] named
                     Just ((_, e), named') =>
                        do e' <- mkTerm e (Just ty) [] [] []
                           processArgs (App fc fn e') !(sc defs (toClosure defaultOpts [] e'))
                                       exps [] named'
  processArgs fn ty [] [] [] = pure fn
  processArgs fn ty exps autos named
     = badClause fn exps autos named

  buildApp : {auto c : Ref Ctxt Defs} ->
             {auto q : Ref QVar Int} ->
             FC -> Name -> Maybe (Closure []) ->
             (expargs : List RawImp) ->
             (autoargs : List RawImp) ->
             (namedargs : List (Name, RawImp)) ->
             Core ClosedTerm
  buildApp fc n mty exps autos named
      = do defs <- get Ctxt
           prims <- getPrimitiveNames
           when (n `elem` prims) $
               throw (InternalError "Can't deal with constants here yet")

           gdefs <- lookupNameBy id n (gamma defs)
           [(n', i, gdef)] <- dropNoMatch !(traverseOpt (evalClosure defs) mty) gdefs
              | [] => undefinedName fc n
              | ts => throw (AmbiguousName fc (map fst ts))
           tynf <- nf defs [] (type gdef)
           -- #899 we need to make sure that type & data constructors are marked
           -- as such so that the coverage checker actually uses the matches in
           -- `impossible` branches to generate parts of the case tree.
           -- When `head` is `Func`, the pattern will be marked as forced and
           -- the coverage checker will considers that all the cases have been
           -- covered!
           let head = case definition gdef of
                        DCon t a _ => DataCon t a
                        TCon t a _ _ _ _ _ _ => TyCon t a
                        _ => Func
           processArgs (Ref fc head (Resolved i)) tynf exps autos named

  mkTerm : {auto c : Ref Ctxt Defs} ->
           {auto q : Ref QVar Int} ->
           RawImp -> Maybe (Closure []) ->
           (expargs : List RawImp) ->
           (autoargs : List RawImp) ->
           (namedargs : List (Name, RawImp)) ->
           Core ClosedTerm
  mkTerm (IVar fc n) mty exps autos named
     = buildApp fc n mty exps autos named
  mkTerm (IApp fc fn arg) mty exps autos named
     = mkTerm fn mty (arg :: exps) autos named
  mkTerm (IAutoApp fc fn arg) mty exps autos named
     = mkTerm fn mty exps (arg :: autos) named
  mkTerm (INamedApp fc fn nm arg) mty exps autos named
     = mkTerm fn mty exps autos ((nm, arg) :: named)
  mkTerm (IPrimVal fc c) _ _ _ _ = pure (PrimVal fc c)
  mkTerm tm _ _ _ _ = nextVar (getFC tm)

-- Given an LHS that is declared 'impossible', build a term to match from,
-- so that when we build the case tree for checking coverage, we take into
-- account the impossible clauses
export
getImpossibleTerm : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
getImpossibleTerm env nest tm
    = do q <- newRef QVar (the Int 0)
         mkTerm (applyEnv tm) Nothing [] [] []
  where
    addEnv : {vars : _} ->
             FC -> Env Term vars -> List RawImp
    addEnv fc [] = []
    addEnv fc (b :: env) =
       if isLet b
          then addEnv fc env
          else Implicit fc False :: addEnv fc env

    expandNest : RawImp -> RawImp
    expandNest (IVar fc n)
        = case lookup n (names nest) of
               Just (Just n', _, _) => IVar fc n'
               _ => IVar fc n
    expandNest tm = tm

    -- Need to apply the function to the surrounding environment, and update
    -- the name to the proper one from the nested names map
    applyEnv : RawImp -> RawImp
    applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
    applyEnv (IAutoApp fc fn arg) = IAutoApp fc (applyEnv fn) arg
    applyEnv (INamedApp fc fn n arg)
        = INamedApp fc (applyEnv fn) n arg
    applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)