text:
module Idris.Package

import Compiler.Common

import Core.Context
import Core.Core
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify

import Data.List
import Data.List1
import Data.Maybe
import Data.So
import Data.StringMap
import Data.Strings
import Data.StringTrie
import Data.These

import Parser.Package
import System
import System.Directory
import System.File

import Text.Parser
import Text.PrettyPrint.Prettyprinter
import Utils.Binary
import Utils.String
import Utils.Path

import Idris.CommandLine
import Idris.ModTree
import Idris.ProcessIdr
import Idris.REPL
import Idris.REPLOpts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import IdrisPaths

%default covering

record PkgDesc where
  constructor MkPkgDesc
  name : String
  version : String
  authors : String
  maintainers : Maybe String
  license : Maybe String
  brief   : Maybe String
  readme  : Maybe String
  homepage : Maybe String
  sourceloc : Maybe String
  bugtracker : Maybe String
  depends : List String -- packages to add to search path
  modules : List (ModuleIdent, String) -- modules to install (namespace, filename)
  mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)
  executable : Maybe String -- name of executable
  library : Maybe String -- name of library
  options : Maybe (FC, String)
  sourcedir : Maybe String
  builddir : Maybe String
  outputdir : Maybe String
  prebuild : Maybe (FC, String) -- Script to run before building
  postbuild : Maybe (FC, String) -- Script to run after building
  preinstall : Maybe (FC, String) -- Script to run after building, before installing
  postinstall : Maybe (FC, String) -- Script to run after installing
  preclean : Maybe (FC, String) -- Script to run before cleaning
  postclean : Maybe (FC, String) -- Script to run after cleaning

Show PkgDesc where
  show pkg = "Package: " ++ name pkg ++ "\n" ++
             "Version: " ++ version pkg ++ "\n" ++
             "Authors: " ++ authors pkg ++ "\n" ++
             maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++
             maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++
             maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++
             maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++
             maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++
             maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++
             maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++
             "Depends: " ++ show (depends pkg) ++ "\n" ++
             "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++
             maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++
             maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++
             maybe "" (\m => "Library: " ++ m ++ "\n") (library pkg) ++
             maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++
             maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++
             maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++
             maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++
             maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++
             maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++
             maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++
             maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++
             maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++
             maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)

initPkgDesc : String -> PkgDesc
initPkgDesc pname
    = MkPkgDesc pname "0" "Anonymous" Nothing Nothing
                Nothing Nothing Nothing Nothing Nothing
                [] []
                Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing
                Nothing Nothing Nothing Nothing Nothing

data DescField : Type where
  PVersion     : FC -> String -> DescField
  PAuthors     : FC -> String -> DescField
  PMaintainers : FC -> String -> DescField
  PLicense     : FC -> String -> DescField
  PBrief       : FC -> String -> DescField
  PReadMe      : FC -> String -> DescField
  PHomePage    : FC -> String -> DescField
  PSourceLoc   : FC -> String -> DescField
  PBugTracker  : FC -> String -> DescField
  PDepends     : List String -> DescField
  PModules     : List (FC, ModuleIdent) -> DescField
  PMainMod     : FC -> ModuleIdent -> DescField
  PExec        : String -> DescField
  PLibrary     : String -> DescField
  POpts        : FC -> String -> DescField
  PSourceDir   : FC -> String -> DescField
  PBuildDir    : FC -> String -> DescField
  POutputDir   : FC -> String -> DescField
  PPrebuild    : FC -> String -> DescField
  PPostbuild   : FC -> String -> DescField
  PPreinstall  : FC -> String -> DescField
  PPostinstall : FC -> String -> DescField
  PPreclean    : FC -> String -> DescField
  PPostclean   : FC -> String -> DescField

field : String -> Rule DescField
field fname
      = strField PVersion "version"
    <|> strField PAuthors "authors"
    <|> strField PMaintainers "maintainers"
    <|> strField PLicense "license"
    <|> strField PBrief "brief"
    <|> strField PReadMe "readme"
    <|> strField PHomePage "homepage"
    <|> strField PSourceLoc "sourceloc"
    <|> strField PBugTracker "bugtracker"
    <|> strField POpts "options"
    <|> strField POpts "opts"
    <|> strField PSourceDir "sourcedir"
    <|> strField PBuildDir "builddir"
    <|> strField POutputDir "outputdir"
    <|> strField PPrebuild "prebuild"
    <|> strField PPostbuild "postbuild"
    <|> strField PPreinstall "preinstall"
    <|> strField PPostinstall "postinstall"
    <|> strField PPreclean "preclean"
    <|> strField PPostclean "postclean"
    <|> do exactProperty "depends"
           equals
           ds <- sep packageName
           pure (PDepends ds)
    <|> do exactProperty "modules"
           equals
           ms <- sep (do start <- location
                         m <- moduleIdent
                         end <- location
                         pure (MkFC fname start end, m))
           pure (PModules ms)
    <|> do exactProperty "main"
           equals
           start <- location
           m <- moduleIdent
           end <- location
           pure (PMainMod (MkFC fname start end) m)
    <|> do exactProperty "executable"
           equals
           e <- (stringLit <|> packageName)
           pure (PExec e)
    <|> do exactProperty "library"
           equals
           libName <- (stringLit <|> packageName)
           pure (PLibrary libName)
  where
    strField : (FC -> String -> DescField) -> String -> Rule DescField
    strField fieldConstructor fieldName
        = do start <- location
             exactProperty fieldName
             equals
             str <- stringLit
             end <- location
             pure $ fieldConstructor (MkFC fname start end) str

parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
    = do exactProperty "package"
         name <- packageName
         fields <- many (field fname)
         pure (name, fields)

data ParsedMods : Type where

data MainMod : Type where

addField : {auto c : Ref Ctxt Defs} ->
           {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
           {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
           DescField -> PkgDesc -> Core PkgDesc
addField (PVersion fc n)     pkg = pure $ record { version = n } pkg
addField (PAuthors fc a)     pkg = pure $ record { authors = a } pkg
addField (PMaintainers fc a) pkg = pure $ record { maintainers = Just a } pkg
addField (PLicense fc a)     pkg = pure $ record { license = Just a } pkg
addField (PBrief fc a)       pkg = pure $ record { brief = Just a } pkg
addField (PReadMe fc a)      pkg = pure $ record { readme = Just a } pkg
addField (PHomePage fc a)    pkg = pure $ record { homepage = Just a } pkg
addField (PSourceLoc fc a)   pkg = pure $ record { sourceloc = Just a } pkg
addField (PBugTracker fc a)  pkg = pure $ record { bugtracker = Just a } pkg
addField (PDepends ds)       pkg = pure $ record { depends = ds } pkg
-- we can't resolve source files for modules without knowing the source directory,
-- so we save them for the second pass
addField (PModules ms)       pkg = do put ParsedMods ms
                                      pure pkg
addField (PMainMod loc n)    pkg = do put MainMod (Just (loc, n))
                                      pure pkg
addField (PExec e)           pkg = pure $ record { executable = Just e } pkg
addField (PLibrary e)        pkg = pure $ record { library = Just e } pkg
addField (POpts fc e)        pkg = pure $ record { options = Just (fc, e) } pkg
addField (PSourceDir fc a)   pkg = pure $ record { sourcedir = Just a } pkg
addField (PBuildDir fc a)    pkg = pure $ record { builddir = Just a } pkg
addField (POutputDir fc a)   pkg = pure $ record { outputdir = Just a } pkg
addField (PPrebuild fc e)    pkg = pure $ record { prebuild = Just (fc, e) } pkg
addField (PPostbuild fc e)   pkg = pure $ record { postbuild = Just (fc, e) } pkg
addField (PPreinstall fc e)  pkg = pure $ record { preinstall = Just (fc, e) } pkg
addField (PPostinstall fc e) pkg = pure $ record { postinstall = Just (fc, e) } pkg
addField (PPreclean fc e)    pkg = pure $ record { preclean = Just (fc, e) } pkg
addField (PPostclean fc e)   pkg = pure $ record { postclean = Just (fc, e) } pkg

addFields : {auto c : Ref Ctxt Defs} ->
            List DescField -> PkgDesc -> Core PkgDesc
addFields xs desc = do p <- newRef ParsedMods []
                       m <- newRef MainMod Nothing
                       added <- go {p} {m} xs desc
                       setSourceDir (sourcedir added)
                       ms <- get ParsedMods
                       mmod <- get MainMod
                       pure $ record { modules = !(traverse toSource ms)
                                     , mainmod = !(traverseOpt toSource mmod)
                                     } added
  where
    toSource : (FC, ModuleIdent) -> Core (ModuleIdent, String)
    toSource (loc, ns) = pure (ns, !(nsToSource loc ns))
    go : {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->
         {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->
         List DescField -> PkgDesc -> Core PkgDesc
    go [] dsc = pure dsc
    go (x :: xs) dsc = go xs !(addField x dsc)

runScript : Maybe (FC, String) -> Core ()
runScript Nothing = pure ()
runScript (Just (fc, s))
    = do res <- coreLift $ system s
         when (res /= 0) $
            throw (GenericMsg fc "Script failed")

addDeps : {auto c : Ref Ctxt Defs} ->
          PkgDesc -> Core ()
addDeps pkg
    = do defs <- get Ctxt
         traverse_ addPkg (depends pkg)

processOptions : {auto c : Ref Ctxt Defs} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 Maybe (FC, String) -> Core ()
processOptions Nothing = pure ()
processOptions (Just (fc, opts))
    = do let Right clopts = getOpts (words opts)
                | Left err => throw (GenericMsg fc err)
         preOptions clopts
         pure ()

compileMain : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto o : Ref ROpts REPLOpts} ->
              Name -> String -> String -> Core ()
compileMain mainn mmod exec
    = do m <- newRef MD initMetadata
         u <- newRef UST initUState

         loadMainFile mmod
         compileExp (PRef replFC mainn) exec
         pure ()

compileLibHelper : {auto c : Ref Ctxt Defs} ->
                   {auto s : Ref Syn SyntaxInfo} ->
                   {auto o : Ref ROpts REPLOpts} ->
                   (libName : String) ->
                   (packageNamespaces : List ModuleIdent) ->
                   (changedModules : Maybe (List ModuleIdent)) ->
                   Core ()
compileLibHelper libName packageNamespaces changedModules
    = do m <- newRef MD initMetadata
         u <- newRef UST initUState
         let namespacesToLoad = fromMaybe packageNamespaces changedModules
         loadModules namespacesToLoad
         compileLib libName changedModules
         pure ()

filterChangedModules : (changedModules : List ModuleIdent) ->
                          List BuildMod ->
                          List BuildMod
filterChangedModules changedModules allMods =
  let (changedMods, possiblyChangedMods) = partition (\mod => mod.buildNS `elem` changedModules) allMods
      usedByMods = filterUsedByMods changedModules possiblyChangedMods
  in changedMods ++ usedByMods

prepareCompilation : {auto c : Ref Ctxt Defs} ->
                     {auto s : Ref Syn SyntaxInfo} ->
                     {auto o : Ref ROpts REPLOpts} ->
                     PkgDesc ->
                     List CLOpt ->
                     Core (List Error, Maybe (List ModuleIdent))
prepareCompilation pkg opts =
  do
    defs <- get Ctxt
    addDeps pkg

    processOptions (options pkg)
    preOptions opts

    runScript (prebuild pkg)

    let filesToBuild = maybe (map snd (modules pkg))
                        (\m => snd m :: map snd (modules pkg))
                        (mainmod pkg)
    allMods <- getAllBuildMods filesToBuild
    session <- getSession
    case session.changedModules of
      Just changedModules => do
        let modsToBuild = filterChangedModules (forget changedModules) allMods
        errs <- buildAll modsToBuild
        pure (errs, Just $ map buildNS modsToBuild)
      Nothing => do
        errs <- buildAll allMods
        pure (errs, Nothing)

build : {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core (List Error)
build pkg opts
    = do ([], changedModules) <- prepareCompilation pkg opts
            | (errs, _) => pure errs

         case executable pkg of
              Nothing => pure ()
              Just exec =>
                   do let Just (mainNS, mainFile) = mainmod pkg
                               | Nothing => throw (GenericMsg emptyFC "No main module given")
                      let mainName = NS (miAsNamespace mainNS) (UN "main")
                      compileMain mainName mainFile exec
         case library pkg of
              Nothing => pure ()
              Just libName =>
                let packageNamespaces = map fst (modules pkg)
                in compileLibHelper libName packageNamespaces changedModules
         runScript (postbuild pkg)
         pure []

copyFile : String -> String -> IO (Either FileError ())
copyFile src dest
    = do Right buf <- readFromFile src
             | Left err => pure (Left err)
         writeToFile dest buf

installFrom : {auto c : Ref Ctxt Defs} ->
              String -> String -> String -> ModuleIdent -> Core ()
installFrom pname builddir destdir ns
    = do let ttcfile = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
         let ttcPath = builddir </> "ttc" </> ttcfile <.> "ttc"

         let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns
         let destNest = joinPath modPath
         let destPath = destdir </> destNest
         let destFile = destdir </> ttcfile <.> "ttc"

         Right _ <- coreLift $ mkdirAll $ destNest
             | Left err => throw (InternalError ("Can't make directories " ++ show modPath))
         coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
         Right _ <- coreLift $ copyFile ttcPath destFile
             | Left err => throw (InternalError ("Can't copy file " ++ ttcPath ++ " to " ++ destPath))
         pure ()

-- Install all the built modules in prefix/package/
-- We've already built and checked for success, so if any don't exist that's
-- an internal error.
install : {auto c : Ref Ctxt Defs} ->
          {auto o : Ref ROpts REPLOpts} ->
          PkgDesc ->
          List CLOpt ->
          Core ()
install pkg opts -- not used but might be in the future
    = do defs <- get Ctxt
         let build = build_dir (dirs (options defs))
         runScript (preinstall pkg)
         let toInstall = maybe (map fst (modules pkg))
                               (\ m => fst m :: map fst (modules pkg))
                               (mainmod pkg)
         Just srcdir <- coreLift currentDir
             | Nothing => throw (InternalError "Can't get current directory")
         -- Make the package installation directory
         let installPrefix = prefix_dir (dirs (options defs)) </>
                             "idris2-" ++ showVersion False version
         True <- coreLift $ changeDir installPrefix
             | False => throw (InternalError ("Can't change directory to " ++ installPrefix))
         Right _ <- coreLift $ mkdirAll (name pkg)
             | Left err => throw (InternalError ("Can't make directory " ++ name pkg))
         True <- coreLift $ changeDir (name pkg)
             | False => throw (InternalError ("Can't change directory to " ++ name pkg))

         -- We're in that directory now, so copy the files from
         -- srcdir/build into it
         traverse (installFrom (name pkg)
                               (srcdir </> build)
                               (installPrefix </> name pkg)) toInstall
         coreLift $ changeDir srcdir
         runScript (postinstall pkg)

-- Check package without compiling anything.
check : {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core (List Error)
check pkg opts =
  do
    ([], changedModules) <- prepareCompilation pkg opts
      | (errs, _) => pure errs

    runScript (postbuild pkg)
    pure []

-- Data.These.bitraverse hand specialised for Core
bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d)
bitraverseC f g (This a)   = [| This (f a) |]
bitraverseC f g (That b)   = [| That (g b) |]
bitraverseC f g (Both a b) = [| Both (f a) (g b) |]

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

-- Data.StringTrie.foldWithKeysM hand specialised for Core
foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b
foldWithKeysC {a} {b} fk fv = go []
  where
  go : List String -> StringTrie a -> Core b
  go ks (MkStringTrie nd) =
    map bifold $ bitraverseC
                   (fv ks)
                   (\sm => foldlC
                             (\x, (k, vs) =>
                               do let ks' = ks++[k]
                                  y <- assert_total $ go ks' vs
                                  z <- fk ks'
                                  pure $ x <+> y <+> z)
                             neutral
                             (StringMap.toList sm))
                   nd

clean : {auto c : Ref Ctxt Defs} ->
        {auto o : Ref ROpts REPLOpts} ->
        PkgDesc ->
        List CLOpt ->
        Core ()
clean pkg opts -- `opts` is not used but might be in the future
    = do defs <- get Ctxt
         runScript (preclean pkg)
         let pkgmods = maybe
                         (map fst (modules pkg))
                         (\m => fst m :: map fst (modules pkg))
                         (mainmod pkg)
         let toClean : List (List String, String)
               = mapMaybe (\ mod => case unsafeUnfoldModuleIdent mod of
                                       [] => Nothing
                                       (x :: xs) => Just(xs, x))
                          pkgmods
         Just srcdir <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         let d = dirs (options defs)
         let builddir = srcdir </> build_dir d </> "ttc"
         let outputdir = srcdir </> outputDirWithDefault d
         -- the usual pair syntax breaks with `No such variable a` here for some reason
         let pkgTrie : StringTrie (List String)
                     = foldl (\trie, ksv =>
                                let ks = Builtin.fst ksv
                                    v = Builtin.snd ksv
                                  in
                                insertWith (reverse ks) (maybe [v] (v::)) trie) empty toClean
         foldWithKeysC (deleteFolder builddir)
                       (\ks => map concat . traverse (deleteBin builddir ks))
                       pkgTrie
         deleteFolder builddir []
         maybe (pure ()) (\e => delete (outputdir </> e))
               (executable pkg)
         runScript (postclean pkg)
  where
    delete : String -> Core ()
    delete path = do Right () <- coreLift $ removeFile path
                       | Left err => pure ()
                     coreLift $ putStrLn $ "Removed: " ++ path

    deleteFolder : String -> List String -> Core ()
    deleteFolder builddir ns = delete $ builddir </> joinPath ns

    deleteBin : String -> List String -> String -> Core ()
    deleteBin builddir ns mod
        = do let ttFile = builddir </> joinPath ns </> mod
             delete $ ttFile <.> "ttc"
             delete $ ttFile <.> "ttm"

getParseErrorLoc : String -> ParseError Token -> FC
getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case
getParseErrorLoc fname _ = replFC

-- Just load the given module, if it exists, which will involve building
-- it if necessary
runRepl : {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          Maybe String ->
          Core ()
runRepl fname = do
  u <- newRef UST initUState
  m <- newRef MD initMetadata
  the (Core ()) $
      case fname of
          Nothing => pure ()
          Just fn => do
            errs <- loadMainFile fn
            displayErrors errs
  repl {u} {s}

processPackage : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 PkgCommand ->
                 String ->
                 List CLOpt ->
                 Core ()
processPackage cmd file opts
    =  if not (isSuffixOf ".ipkg" file)
         then do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")
                 coreLift (exitWith (ExitFailure 1))
         else do Right (pname, fs) <- coreLift $ parseFile file
                                          (do desc <- parsePkgDesc file
                                              eoi
                                              pure desc)
                     | Left (FileFail err) => throw (FileErr file err)
                     | Left err => throw (ParseFail (getParseErrorLoc file err) err)
                 pkg <- addFields fs (initPkgDesc pname)
                 maybe (pure ()) setBuildDir (builddir pkg)
                 setOutputDir (outputdir pkg)
                 case cmd of
                      Build => do [] <- build pkg opts
                                     | errs => coreLift (exitWith (ExitFailure 1))
                                  pure ()
                      Install => do [] <- build pkg opts
                                       | errs => coreLift (exitWith (ExitFailure 1))
                                    install pkg opts
                      Typecheck => do
                        [] <- check pkg opts
                          | errs => coreLift (exitWith (ExitFailure 1))
                        pure ()
                      Clean => clean pkg opts
                      REPL => do
                        [] <- build pkg opts
                           | errs => coreLift (exitWith (ExitFailure 1))
                        runRepl (map snd $ mainmod pkg)

record POptsFilterResult where
  constructor MkPFR
  pkgDetails : Maybe (PkgCommand, String)
  oopts : List CLOpt
  hasError : Bool

errorMsg : String
errorMsg = unlines
  [ "Not all command line options can be used to override package options.\n"
  , "Overridable options are:"
  , "    --quiet"
  , "    --verbose"
  , "    --console-width <console width>"
  , "    --color, --colour"
  , "    --no-color, --no-colour"
  , "    --timing"
  , "    --log <log level>"
  , "    --dumpcases <file>"
  , "    --dumplifted <file>"
  , "    --dumpvmcode <file>"
  , "    --debug-elab-check"
  , "    --codegen <cg>"
  , "    --directive <directive>"
  , "    --build-dir <dir>"
  , "    --output-dir <dir>"
  , "    --changed-modules <namespaces>"
  ]

filterPackageOpts : POptsFilterResult -> List CLOpt -> Core (POptsFilterResult)
filterPackageOpts acc Nil                  = pure acc
filterPackageOpts acc (Package cmd f ::xs) = filterPackageOpts (record {pkgDetails = Just (cmd, f)}  acc) xs

filterPackageOpts acc (Quiet         ::xs) = filterPackageOpts (record {oopts $= (Quiet::)}          acc) xs
filterPackageOpts acc (Verbose       ::xs) = filterPackageOpts (record {oopts $= (Verbose::)}        acc) xs
filterPackageOpts acc (ConsoleWidth n::xs) = filterPackageOpts (record {oopts $= (ConsoleWidth n::)} acc) xs
filterPackageOpts acc (Color b       ::xs) = filterPackageOpts (record {oopts $= (Color b::)}        acc) xs
filterPackageOpts acc (Timing        ::xs) = filterPackageOpts (record {oopts $= (Timing::)}         acc) xs
filterPackageOpts acc (Logging l     ::xs) = filterPackageOpts (record {oopts $= (Logging l::)}      acc) xs
filterPackageOpts acc (DumpCases f   ::xs) = filterPackageOpts (record {oopts $= (DumpCases f::)}    acc) xs
filterPackageOpts acc (DumpLifted f  ::xs) = filterPackageOpts (record {oopts $= (DumpLifted f::)}   acc) xs
filterPackageOpts acc (DumpVMCode f  ::xs) = filterPackageOpts (record {oopts $= (DumpVMCode f::)}   acc) xs
filterPackageOpts acc (DebugElabCheck::xs) = filterPackageOpts (record {oopts $= (DebugElabCheck::)} acc) xs
filterPackageOpts acc (SetCG f       ::xs) = filterPackageOpts (record {oopts $= (SetCG f::)}        acc) xs
filterPackageOpts acc (Directive f   ::xs) = filterPackageOpts (record {oopts $= (Directive f::)}    acc) xs
filterPackageOpts acc (BuildDir f    ::xs) = filterPackageOpts (record {oopts $= (BuildDir f::)}     acc) xs
filterPackageOpts acc (OutputDir f   ::xs) = filterPackageOpts (record {oopts $= (OutputDir f::)}    acc) xs
filterPackageOpts acc (ChangedModules ns::xs) = filterPackageOpts (record {oopts $= (ChangedModules ns::)} acc) xs

filterPackageOpts acc (x::xs) = pure (record {hasError = True} acc)

-- If there's a package option, it must be the only option, so reject if
-- it's not
export
processPackageOpts : {auto c : Ref Ctxt Defs} ->
                     {auto s : Ref Syn SyntaxInfo} ->
                     {auto o : Ref ROpts REPLOpts} ->
                     List CLOpt ->
                     Core Bool
processPackageOpts Nil = pure False
processPackageOpts [Package cmd f] = do processPackage cmd f Nil
                                        pure True

processPackageOpts opts
    = do (MkPFR (Just (cmd, f)) opts' err) <- filterPackageOpts (MkPFR Nothing Nil False) opts
             | (MkPFR Nothing opts _) => pure False

         if err
           then do coreLift (putStrLn errorMsg)
                   pure True
           else do processPackage cmd f opts'
                   pure True

-- find an ipkg file in one of the parent directories
-- If it exists, read it, set the current directory to the root of the source
-- tree, and set the relevant command line options before proceeding
export
findIpkg : {auto c : Ref Ctxt Defs} ->
           {auto r : Ref ROpts REPLOpts} ->
           Maybe String -> Core (Maybe String)
findIpkg fname
   = do Just (dir, ipkgn, up) <- coreLift findIpkgFile
             | Nothing => pure fname
        coreLift $ changeDir dir
        setWorkingDir dir
        Right (pname, fs) <- coreLift $ parseFile ipkgn
                                 (do desc <- parsePkgDesc ipkgn
                                     eoi
                                     pure desc)
              | Left (FileFail err) => throw (FileErr ipkgn err)
              | Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err)
        pkg <- addFields fs (initPkgDesc pname)
        maybe (pure ()) setBuildDir (builddir pkg)
        setOutputDir (outputdir pkg)
        processOptions (options pkg)
        loadDependencies (depends pkg)
        case fname of
             Nothing => pure Nothing
             Just srcpath  =>
                do let src' = up </> srcpath
                   setSource src'
                   opts <- get ROpts
                   put ROpts (record { mainfile = Just src' } opts)
                   pure (Just src')
  where
    dropHead : String -> List String -> List String
    dropHead str [] = []
    dropHead str (x :: xs)
        = if x == str then xs else x :: xs
    loadDependencies : List String -> Core ()
    loadDependencies = traverse_ addPkg


text:
module Algebra.Solver.Ring.Sum

import Algebra.Solver.Ring.Expr
import Algebra.Solver.Ring.Prod
import Algebra.Solver.Ring.SolvableRing
import Algebra.Solver.Ring.Util

%default total

||| A single term in a normalized arithmetic expressions.
|||
||| This is a product of all variables each raised to
||| a given power, multiplied with a factors (which is supposed
||| to reduce during elaboration).
public export
record Term (a : Type) (as : List a) where
  constructor T
  factor : a
  prod   : Prod a as

||| Evaluate a term.
public export
eterm : Ring a => {as : List a} -> Term a as -> a
eterm (T f p) = f * eprod p

||| Negate a term.
public export
negTerm : Ring a => Term a as -> Term a as
negTerm (T f p) = T (negate f) p

||| Normalized arithmetic expression in a commutative
||| ring (represented as an (ordered) sum of terms).
public export
data Sum : (a : Type) -> (as : List a) -> Type where
  Nil  : {0 as : List a} -> Sum a as
  (::) : {0 as : List a} -> Term a as -> Sum a as -> Sum a as

||| Evaluate a sum of terms.
public export
esum : Ring a => {as : List a} -> Sum a as -> a
esum []        = 0
esum (x :: xs) = eterm x + esum xs

||| Negate a sum of terms.
public export
negate : Ring a => Sum a as -> Sum a as
negate []       = []
negate (x :: y) = negTerm x :: negate y

--------------------------------------------------------------------------------
--          Normalizer
--------------------------------------------------------------------------------

||| Add two sums of terms.
|||
||| The order of terms will be kept. If two terms have identical
||| products of variables, they will be unified by adding their
||| factors.
public export
add : SolvableRing a => Sum a as -> Sum a as -> Sum a as
add []        ys                = ys
add xs        []                = xs
add (T m x :: xs) (T n y :: ys) = case compProd x y of
  LT => T m x :: add xs (T n y :: ys)
  GT => T n y :: add (T m x :: xs) ys
  EQ => T (m + n) y :: add xs ys

||| Normalize a sum of terms by removing all terms with a
||| `zero` factor.
public export
normSum : SolvableRing a => Sum a as -> Sum a as
normSum []           = []
normSum (T f p :: y) = case isZero f of
  Just refl => normSum y
  Nothing   => T f p :: normSum y

||| Multiplies a single term with a sum of terms.
public export
mult1 : SolvableRing a => Term a as -> Sum a as -> Sum a as
mult1 (T f p) (T g q :: xs) = T (f * g) (mult p q) :: mult1 (T f p) xs
mult1 _       []            = []

||| Multiplies two sums of terms.
public export
mult : SolvableRing a => Sum a as -> Sum a as -> Sum a as
mult []        ys = []
mult (x :: xs) ys = add (mult1 x ys) (mult xs ys)

||| Normalizes an arithmetic expression to a sum of products.
public export
norm : SolvableRing a => {as : List a} -> Expr a as -> Sum a as
norm (Lit n)     = [T n one]
norm (Var x y)   = [T 1 $ fromVar y]
norm (Neg x)     = negate $ norm x
norm (Plus x y)  = add (norm x) (norm y)
norm (Mult x y)  = mult (norm x) (norm y)
norm (Minus x y) = add (norm x) (negate $ norm y)

||| Like `norm` but removes all `zero` terms.
public export
normalize : SolvableRing a => {as : List a} -> Expr a as -> Sum a as
normalize e = normSum (norm e)

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

-- Adding two sums via `add` preserves the evaluation result.
0 padd :  SolvableRing a
       => (x,y : Sum a as)
       -> esum x + esum y === esum (add x y)
padd []            xs = plusZeroLeftNeutral
padd (x :: xs)     [] = plusZeroRightNeutral
padd (T m x :: xs) (T n y :: ys) with (compProd x y) proof eq
  _ | LT = Calc $
    |~ (m * eprod x + esum xs) + (n * eprod y + esum ys)
    ~~ m * eprod x + (esum xs + (n * eprod y + esum ys))
       ..< plusAssociative
    ~~ m * eprod x + esum (add xs (T n y :: ys))
       ... cong (m * eprod x +) (padd xs (T n y :: ys))

  _ | GT = Calc $
    |~ (m * eprod x + esum xs) + (n * eprod y + esum ys)
    ~~ n * eprod y + ((m * eprod x + esum xs) + esum ys)
       ..< p213
    ~~ n * eprod y + esum (add (T m x :: xs) ys)
       ... cong (n * eprod y +) (padd (T m x :: xs) ys)

  _ | EQ = case pcompProd x y eq of
        Refl => Calc $
          |~ (m * eprod x + esum xs) + (n * eprod x + esum ys)
          ~~ (m * eprod x + n * eprod x) + (esum xs + esum ys)
             ... p1324
          ~~ (m + n) * eprod x + (esum xs + esum ys)
             ..< cong (+ (esum xs + esum ys)) rightDistributive
          ~~ (m + n) * eprod x + esum (add xs ys)
             ... cong ((m + n) * eprod x +) (padd xs ys)

-- Small utility lemma
0 psum0 :  SolvableRing a
        => {x,y,z : a}
        -> x === y
        -> x === 0 * z + y
psum0 prf = Calc $
  |~ x
  ~~ y          ... prf
  ~~ 0 + y      ..< plusZeroLeftNeutral
  ~~ 0 * z + y  ..< cong (+ y) multZeroLeftAbsorbs

-- Multiplying a sum with a term preserves the evaluation result.
0 pmult1 :  SolvableRing a
         => (m : a)
         -> (p : Prod a as)
         -> (s : Sum a as)
         -> esum (mult1 (T m p) s) === (m * eprod p) * esum s
pmult1 m p []            = sym multZeroRightAbsorbs
pmult1 m p (T n q :: xs) = Calc $
  |~ (m * n) * (eprod (mult p q)) + esum (mult1 (T m p) xs)
  ~~ (m * n) * (eprod p * eprod q) + esum (mult1 (T m p) xs)
     ... cong (\x => (m*n) * x + esum (mult1 (T m p) xs)) (pmult p q)
  ~~ (m * eprod p) * (n * eprod q) + esum (mult1 (T m p) xs)
     ..< cong (+ esum (mult1 (T m p) xs)) m1324
  ~~ (m * eprod p) * (n * eprod q) + (m * eprod p) * esum xs
     ... cong ((m * eprod p) * (n * eprod q) +) (pmult1 m p xs)
  ~~ (m * eprod p) * (n * eprod q + esum xs)
     ..< leftDistributive

-- Multiplying two sums of terms preserves the evaluation result.
0 pmult :  SolvableRing a
        => (x,y : Sum a as)
        -> esum x * esum y === esum (mult x y)
pmult []            y = multZeroLeftAbsorbs
pmult (T n x :: xs) y = Calc $
  |~ (n * eprod x + esum xs) * esum y
  ~~ (n * eprod x) * esum y + esum xs * esum y
     ... rightDistributive
  ~~ (n * eprod x) * esum y + esum (mult xs y)
     ... cong ((n * eprod x) * esum y +) (pmult xs y)
  ~~ esum (mult1 (T n x) y) + esum (mult xs y)
     ..< cong (+ esum (mult xs y)) (pmult1 n x y)
  ~~ esum (add (mult1 (T n x) y) (mult xs y))
     ... padd (mult1 (T n x) y) (mult xs y)

-- Evaluating a negated term is equivalent to negate the
-- result of evaluating the term.
0 pnegTerm :  SolvableRing a
           => (x : Term a as)
           -> eterm (negTerm x) === neg (eterm x)
pnegTerm (T f p) = multNegLeft

-- Evaluating a negated sum of terms is equivalent to negate the
-- result of evaluating the sum of terms.
0 pneg :  SolvableRing a
       => (x : Sum a as)
       -> esum (negate x) === neg (esum x)
pneg []       = sym $ negZero
pneg (x :: y) = Calc $
  |~ eterm (negTerm x) + esum (negate y)
  ~~ neg (eterm x) + esum (negate y) ... cong (+ esum (negate y)) (pnegTerm x)
  ~~ neg (eterm x) + neg (esum y)    ... cong (neg (eterm x) +) (pneg y)
  ~~ neg (eterm x + esum y)          ..< negDistributes

-- Removing zero values from a sum of terms does not
-- affect the evaluation result.
0 pnormSum :  SolvableRing a
           => (s : Sum a as)
           -> esum (normSum s) === esum s
pnormSum []           = Refl
pnormSum (T f p :: y) with (isZero f)
  _ | Nothing   = Calc $
    |~ f * eprod p + esum (normSum y)
    ~~ f * eprod p + esum y ... cong ((f * eprod p) +) (pnormSum y)

  _ | Just refl = Calc $
    |~ esum (normSum y)
    ~~ esum y               ... pnormSum y
    ~~ 0 + esum y           ..< plusZeroLeftNeutral
    ~~ 0 * eprod p + esum y ..< cong (+ esum y) multZeroLeftAbsorbs
    ~~ f * eprod p + esum y ..< cong (\x => x * eprod p + esum y) refl

-- Evaluating an expression gives the same result as
-- evaluating its normalized form.
0 pnorm :  SolvableRing a
        => (e : Expr a as)
        -> eval e === esum (norm e)
pnorm (Lit n)    = Calc $
  |~ n
  ~~ n * 1                    ..< multOneRightNeutral
  ~~ n * eprod (one {as})     ..< cong (n *) (pone as)
  ~~ n * eprod (one {as}) + 0 ..< plusZeroRightNeutral

pnorm (Var x y)  = Calc $
  |~ x
  ~~ eprod (fromVar y)          ..< pvar as y
  ~~ 1 * eprod (fromVar y)      ..< multOneLeftNeutral
  ~~ 1 * eprod (fromVar y) + 0  ..< plusZeroRightNeutral

pnorm (Neg x) = Calc $
  |~ neg (eval x)
  ~~ neg (esum (norm x))    ... cong neg (pnorm x)
  ~~ esum (negate (norm x)) ..< pneg (norm x)

pnorm (Plus x y) = Calc $
  |~ eval x + eval y
  ~~ esum (norm x) + eval y
     ... cong (+ eval y) (pnorm x)
  ~~ esum (norm x) + esum (norm y)
     ... cong (esum (norm x) +) (pnorm y)
  ~~ esum (add (norm x) (norm y))
     ... padd _ _

pnorm (Mult x y) = Calc $
  |~ eval x * eval y
  ~~ esum (norm x) * eval y
     ... cong (* eval y) (pnorm x)
  ~~ esum (norm x) * esum (norm y)
     ... cong (esum (norm x) *) (pnorm y)
  ~~ esum (mult (norm x) (norm y))
     ... Sum.pmult _ _

pnorm (Minus x y) = Calc $
  |~ eval x - eval y
  ~~ eval x + neg (eval y)
     ... minusIsPlusNeg
  ~~ esum (norm x) + neg (eval y)
     ... cong (+ neg (eval y)) (pnorm x)
  ~~ esum (norm x) + neg (esum (norm y))
     ... cong (\v => esum (norm x) + neg v) (pnorm y)
  ~~ esum (norm x) + esum (negate (norm y))
     ..< cong (esum (norm x) +) (pneg (norm y))
  ~~ esum (add (norm x) (negate (norm y)))
     ... padd _ _

-- Evaluating an expression gives the same result as
-- evaluating its normalized form.
0 pnormalize :  SolvableRing a
             => (e : Expr a as)
             -> eval e === esum (normalize e)
pnormalize e = Calc $
  |~ eval e
  ~~ esum (norm e)           ... pnorm e
  ~~ esum (normSum (norm e)) ..< pnormSum (norm e)

--------------------------------------------------------------------------------
--          Solver
--------------------------------------------------------------------------------

||| Given a list `as` of variables and two arithmetic expressions
||| over these variables, if the expressions are converted
||| to the same normal form, evaluating them gives the same
||| result.
|||
||| This simple fact allows us to conveniently and quickly
||| proof arithmetic equalities required in other parts of
||| our code. For instance:
|||
||| ```idris example
||| 0 binom1 : {x,y : Bits8}
|||          -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
||| binom1 = solve [x,y]
|||                ((x .+. y) * (x .+. y))
|||                (x .*. x + 2 *. x *. y + y .*. y)
||| ```
export
0 solve :  SolvableRing a
        => (as : List a)
        -> (e1,e2 : Expr a as)
        -> (prf : normalize e1 === normalize e2)
        => eval e1 === eval e2
solve _ e1 e2 = Calc $
  |~ eval e1
  ~~ esum (normalize e1) ...(pnormalize e1)
  ~~ esum (normalize e2) ...(cong esum prf)
  ~~ eval e2             ..<(pnormalize e2)

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

0 binom1 : {x,y : Bits8} -> (x + y) * (x + y) === x * x + 2 * x * y + y * y
binom1 = solve [x,y]
               ((x .+. y) * (x .+. y))
               (x .*. x + 2 *. x *. y + y .*. y)

0 binom2 : {x,y : Bits8} -> (x - y) * (x - y) === x * x - 2 * x * y + y * y
binom2 = solve [x,y]
               ((x .-. y) * (x .-. y))
               (x .*. x - 2 *. x *. y + y .*. y)

0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)

ext: idr


text:
module Bounded

import Bits
import Unsigned

%access export
%default total

||| An unsigned number represented bounded within the range [0,`n`], inclusive
data Bounded : (n: Nat) -> Type where
  B : (n:Nat) -> (m:Nat) -> Bounded m

-- We should consider requiring a proof that 0 <= m <= n in this
-- constructor.

||| Show instance for printing `Bounded n`
Show (Bounded n) where
  show (B x n) = "B" ++ show n ++ " " ++ show x

||| Eq instance for equality of `Bounded n`s.
||| Ranges *and* values must be equal.
Eq (Bounded n) where
  (==) (B x n) (B y n) = x==y

||| Ord instance for ordering of `Bounded n`s
Ord (Bounded n) where
 compare (B x n) (B y n) = compare x y

||| MinBound instance for generating extremes of `Signed n`
MinBound (Bounded n) where
  minBound = B 0 n

||| MaxBound instance for generating extremes of `Signed n`
MaxBound (Bounded n) where
  maxBound = B n n

--------------------------------------------------------------------------------
-- Conversion functions
--------------------------------------------------------------------------------

||| Conversion from `Unsigned` to `Bounded`
fromUnsigned : Unsigned n -> Bounded (bitsToMax n)
fromUnsigned {n} x = B (fromInteger $ cast x) (bitsToMax n)

||| Conversion from `Bounded` to `Unsigned`
toUnsigned : Bounded n -> Unsigned (maxToBits n)
toUnsigned (B x _) = saturate (cast x)

||| Generate a `Bounded n` instance of zeros
zeros : Bounded n
zeros = B 0 n

--------------------------------------------------------------------------------
-- Bounded arithmetic functions
--------------------------------------------------------------------------------

||| Add two `Bounded`s
add : Bounded n ->Bounded m -> Bounded (n+m)
add (B x n) (B y m) = B (x+y) (n+m)

||| Multiply two `Bounded`s
mult : Bounded n ->Bounded m -> Bounded (n*m)
mult (B x n) (B y m) = B (x*y) (n*m)

||| Add a `Bounded` to a `Nat`
addConst : Bounded n -> (m: Nat) -> Bounded (n+m)
addConst (B x n) m = B (x+m) (n+m)

||| Multiply a `Bounded` by a `Nat`
mulConst : Bounded n -> (m: Nat) -> Bounded (n*m)
mulConst (B x n) m = B (x*m) (n*m)

-- TODO consider making Bounded just a specialisation of ClosedInt


text:
module Struts

data Rat : Nat -> Nat -> Type where
  MkRat : (a : Nat) -> (b : Nat) -> Rat a b

multRat : Rat a b -> Rat c d -> Rat (a*c) (b*d)
multRat (MkRat a b) (MkRat c d) = MkRat (a*c) (b*d)

divRat : Rat a b -> Rat c d -> Rat (a*d) (b*c)
divRat (MkRat a b) (MkRat c d) = MkRat (a*d) (b*c)

addRat : Rat a b -> Rat c d -> Rat (a*d + b*c) (b*d)
addRat (MkRat a b) (MkRat c d) = MkRat (a*d + b*c) (b*d)

simplify : Rat a b -> Rat (divNat a (gcd a b)) (divNat b (gcd a b))
simplify (MkRat a b) = MkRat (divNat a (gcd a b)) (divNat b (gcd a b))

fromNat : (n : Nat) -> Rat n 1
fromNat n = MkRat n 1

data Pitch = A | B | C | D | E | F | G

data Note : (r : Rat a b) -> Type where
  MkNote : Pitch -> Note r

quarter : Pitch -> Note (MkRat 1 4)
quarter = MkNote

data NoteSequence : (r : Rat a b) -> Type where
  Empty : NoteSequence (fromNat 0)
  Append : Note s -> NoteSequence r -> NoteSequence (addRat s r)

data Measure : (r : Rat a b) -> Type where
  MkMeasure : NoteSequence r -> Measure r

fin : NoteSequence (fromNat 0)
fin = Empty

infixr 10 ~>

(~>) : Note s -> NoteSequence r -> NoteSequence (addRat s r)
(~>) = Append

beatMeasure : Measure (MkRat 1 4)
beatMeasure = MkMeasure (quarter C ~> fin)


text:
module Main
import Cairo

main: Cairo ()
main = output 42

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

import Effects
import Effect.State

main : IO ()
main = putStrLn "CouCou!"

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
-- test that bufferAndBroadcast doesn't block

import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          (MkDPair bc buffer) <- becomeBuffer bcRef
          buffer Broadcast bc [1,2,3]
          putStrLn "Success!"


text:
module LittleLang
-- Warning: only briefly tested, may have bugs

-- a Type, Naturals, Booleans and iterated function types built from these
public export
data Ty : Type where
  NT : Ty
  BT : Ty
  FT : Ty -> Ty -> Ty

-- An expression with type
public export
data Exp : Ty -> Type where
  N : Nat -> Exp NT  -- a literal natural number
  B : Bool -> Exp BT -- a literal boolean
  LTE : Exp NT -> Exp NT -> Exp BT
  EQ : Exp NT -> Exp NT -> Exp BT
  If : {a: Ty} ->  Exp BT -> Exp a -> Exp a -> Exp a -- if expression
  Var : (name: String) -> (type: Ty) -> Exp type -- a variable
  Lam : {domain: Ty} ->  -- a lambda expression defining a function
            {codomain: Ty} -> (var : Exp domain) ->
            (value : Exp codomain) -> Exp (FT domain codomain)
  App : (a: Ty) -> (b: Ty)  ->  -- function application
            (f : Exp (FT a b)) -> (arg: Exp a) -> Exp b
  Sum :  Exp NT -> Exp NT -> Exp NT
  Prod: Exp NT -> Exp NT -> Exp NT
  Pred: Exp NT -> Exp NT -- predecessor of a natural number

-- An example
not: Exp (FT BT BT)
not = Lam (Var "x" BT) (If (Var "x" BT) (B False) (B True))

-- If `a == b` returns an expression of type `a` as one of type `b`
mapTyp : (a : Ty) -> (b: Ty) -> Exp a -> Maybe (Exp b)
mapTyp NT NT x = Just x
mapTyp NT BT x = Nothing
mapTyp NT (FT y z) x = Nothing
mapTyp BT NT x = Nothing
mapTyp BT BT x = Just x
mapTyp BT (FT y z) x = Nothing
mapTyp (FT y z) NT x = Nothing
mapTyp (FT y z) BT x = Nothing
mapTyp (FT y z) (FT w s) (If x t u) =
  case (mapTyp (FT y z) (FT w s) t) of
    Nothing => Nothing
    (Just q) => (case (mapTyp (FT y z) (FT w s) u) of
         Nothing => Nothing
         (Just p) => Just (If x q p))
mapTyp (FT y z) (FT w s) (Var name (FT y z)) =
  if (isJust (mapTyp y w (Var name y))) && (isJust (mapTyp z s (Var name z)))
    then Just(Var name (FT w s)) else Nothing
mapTyp (FT y z) (FT w s) (Lam var value) =
  case (mapTyp y w var) of
      Nothing => Nothing
      (Just x) => (case (mapTyp z s value) of
                        Nothing => Nothing
                        (Just p) => Just (Lam x p))
mapTyp (FT y z) (FT w s) (App a (FT y z) f arg) =
  (case mapTyp (FT a (FT y z)) (FT a (FT w s)) f of
        Nothing => Nothing
        (Just g) =>
          Just(App a (FT w s) g arg)
        )

-- equality of types
export
eqTyp : Ty -> Ty -> Bool
eqTyp x y = isJust (mapTyp x y (Var "test" x))

-- substitute `x` by `y` in `base`
subs: (a: Ty) -> (b: Ty) -> (base: Exp a) -> (x: Exp b) -> (y: Exp b) -> Exp a
subs NT b (N k) x y = N k
subs BT b (B z) x y = B z
subs BT b (LTE z w) x y = LTE (subs NT b z x y) (subs NT b w x y)
subs BT b (EQ z w) x y = EQ (subs NT b z x y) (subs NT b w x y)
subs a b (If z w s) x y =
  If (subs _ _ z x y) (subs _ _ w x y) (subs _ _ s x y)
subs a b (Var name a) (Var other b) y =
  if name == other
    then (case mapTyp b a y of
               Nothing => Var name a
               (Just x) => x)
    else Var name a
subs a b (Var name a) x y = Var name a
subs (FT domain codomain) b (Lam var value) x y =
  Lam (subs domain b var x y) (subs codomain b value x y)
subs a b (App c a f arg) x y =
  App c a (subs _ _ f x y) (subs c b arg x y)
subs NT b (Sum z w) x y = Sum (subs NT b z x y) (subs NT b w x y)
subs NT b (Pred z) x y = Pred (subs NT b z x y)
subs NT b (Prod z w) x y = Prod (subs NT b z x y) (subs NT b w x y)

-- A list of definitions of variables
public export
data Context : Type where
  Empty: Context
  Cons : (name: String) -> (type: Ty) -> (value: Exp type) -> (tail: Context) -> Context

varValue: Context -> (name: String) -> (ty: Ty) -> Maybe (Exp ty)
varValue Empty name ty = Nothing
varValue (Cons x type value tail) name ty =
  if (x==name)
    then (case mapTyp type ty value of
               Nothing => Nothing
               (Just x) => Just x)
    else Nothing

{-
Simplify an expression in context by one step if possible. The simplifications are:
  * if an expression is a variable defined in the context, it is replaced by its value
  * sums, products and predecessors of _literals_ are simplifed, e.g. `Sum (N 2) (N 3)` becomes `N 5`
  * a lambda function `x :-> y` applied to `z` simplifies to the result of subtituting `x` by `z` in `y`.
  * for any other composite term, we simplify the components.
-}
export
simplify : (ctx: Context) -> (a: Ty) -> (exp : Exp a) -> Exp a
simplify ctx NT (N k) = N k
simplify ctx BT (B x) = B x
simplify ctx BT (LTE (N x) (N y)) = B (x <= y)
simplify ctx BT (LTE x y) = LTE (simplify ctx NT x) (simplify ctx NT y)
simplify ctx BT (EQ (N x) (N y)) = B (x == y)
simplify ctx BT (EQ x y) = EQ (simplify ctx NT x) (simplify ctx NT y)
simplify ctx a (If (B True) y z) = y
simplify ctx a (If (B False) y z) = z
simplify ctx a (If x y z) = If (simplify ctx _ x) (simplify ctx _ y) (simplify ctx _ z)
simplify ctx a (Var name a) =
  (case varValue ctx name a of
        Nothing => Var name a
        (Just x) => x)
simplify ctx (FT domain codomain) (Lam var value) = Lam var value
simplify ctx a (App x a (Lam var value) arg) = subs _ _ value var arg
simplify ctx a (App x a f arg) = App x a (simplify ctx _ f) (simplify ctx _ arg)
simplify ctx NT (Sum (N x) (N y)) = N (x + y)
simplify ctx NT (Sum x y) = Sum (simplify ctx NT x) (simplify ctx NT y)
simplify ctx NT (Pred (N x)) = N (pred x)
simplify ctx NT (Pred x) = Pred (simplify ctx NT x)
simplify ctx NT (Prod (N x) (N y)) = N (x * y)
simplify ctx NT (Prod x y) = Prod (simplify ctx NT x) (simplify ctx NT y)

-- repeatedly simplify an expression giving a natural number till we get a literal (or loop forever)
reduce : Context -> Exp NT -> Nat
reduce ctx exp = case (simplify ctx NT exp) of
                  (N k) => k
                  x => reduce ctx x

-- a variable
n: Exp NT
n = Var "n" NT

-- a variable for the factorial function
fac : Exp (FT NT NT)
fac = Var "fac" (FT NT NT)

-- the expression `fac(n - 1)`
prev: Exp NT
prev = Prod (App NT NT fac (Pred n)) n

-- the expression `if n == 0 then 1 else fac(n-1)`
rhs : Exp NT
rhs = If (EQ n (N Z)) (N 1) prev

{- the context with definition:
  fac := n :-> (if (n == 0) then 1 else fac(n - 1)
-}
ctx: Context
ctx = Cons "fac" (FT NT NT) (Lam n rhs) Empty

-- function computing factorial
facFn: Nat -> Nat
facFn n = reduce ctx (App NT NT fac (N n))


text:
module Extra.Parser

import Data.Bits
import Data.DPair
import Data.List
import Debug.Trace
import Data.List1
import Data.String
import Extra.Alternative
import Extra.Applicative
import Extra.String
import Extra.Vect

||| `Stream i e` where `i` is the full type and `e` is the type of a single token
public export
interface Monoid i => Stream i e | i where
  uncons : i -> Maybe (i, e)

export
{0 a : Type} -> Stream (List a) a where
  uncons Nil = Nothing
  uncons (x :: xs) = Just (xs, x)

export
Stream String Char where
  uncons xs = case strM xs of
    StrCons x xs => Just (xs, x)
    StrNil => Nothing

export
data Parser : (input: Type) -> (result : Type) -> Type where
  Done : (leftover : i) -> (result : r) -> Parser i r
  Fail : (msg : String) -> Parser i r
  More : (on_eof : Lazy (Parser i r)) -> (on_feed : (i -> Parser i r)) -> Parser i r

-- core
||| Fail a `Parser`, equivalent to the `Fail` constructor
export
fail : String -> Parser i r
fail = Fail

export
||| Complete a `Parser`, equivalent to the `Done` constructor, arguments:
||| - remaining input
||| - result value
done : i -> r -> Parser i r
done = Done

||| Create a `Parser` handling `feedEof`/`feed` cases, equivalent to the `More` constructor
export
more : (on_eof : Lazy (Parser i r)) -> (on_feed : (i -> Parser i r)) -> Parser i r
more = More

||| Convert a `Parser` into an Either, if the parser is partial, the result is `Left "partial"`
export
toEither : Parser i r -> Either String (i, r)
toEither (Done i r) = Right (i, r)
toEither (Fail msg) = Left msg
toEither (More _ _) = Left "partial"

||| `toEither` but discards the leftover
export
toEither_ : Parser i r -> Either String r
toEither_ = map snd . toEither

||| Feed a parser with inputs into a `Parser`
export
feed : Semigroup i => i -> Parser i r -> Parser i r
feed input (Done leftover result) = Done (leftover <+> input) result
feed input (More _ on_feed) = on_feed input
feed input (Fail msg) = Fail msg

||| Feed an EOF signal into a `Parser`
export
feedEof : Parser i r -> Parser i r
feedEof (Done leftover result) = Done leftover result
feedEof (More on_eof _) = on_eof
feedEof (Fail msg) = Fail msg

infixl 0 <?>

-- TODO: improve quality of labels
||| Labels a parser
export
(<?>) : Parser i r -> String -> Parser i r
(Fail msg') <?> msg = Fail $ msg <+> "." <+> msg'
(Done leftover result) <?> _ = Done leftover result
(More on_eof on_feed) <?> msg = More (on_eof <?> msg) (\i => on_feed i <?> msg)

export
Functor (Parser i) where
  map f (Done leftover result) = Done leftover (f result)
  map f (More on_eof on_feed) = More (map f on_eof) (map f . on_feed)
  map f (Fail msg) = Fail msg

mutual
  export
  Monoid i => LazyApplicative (Parser i) where
    (Done leftover f) <*>| p = map f (feed leftover p)
    (More on_eof_f on_feed_f) <*>| p = More (on_eof_f <*>| p) (\i => on_feed_f i <*>| p)
    (Fail msg) <*>| p = Fail msg

  export
  Monoid i => Applicative (Parser i) where
    pure = Done neutral
    a <*> b = a <*>| b

export
(Monoid i, Applicative (Parser i)) => Monad (Parser i) where
  (Done leftover result) >>= f = feed leftover (f result)
  (More on_eof on_feed) >>= f = More (on_eof >>= f) (\i => on_feed i >>= f)
  (Fail msg) >>= _ = Fail msg

mutual
  export
  (Semigroup i, Applicative (Parser i)) => LazyAlternative (Parser i) where
    (Done leftover result) <|>| p = Done leftover result
    (Fail msg) <|>| p = p
    p1 <|>| p2 = More (feedEof p1 <|>| feedEof p2) (\i => feed i p1 <|>| feed i p2)

  export
  (Semigroup i, Applicative (Parser i)) => Alternative (Parser i) where
    empty = Fail "empty"
    a <|> b = a <|>| b

-- basic

export
anyToken : Stream i e => Parser i e
anyToken = More (Fail "anyToken") $ \i =>
  case uncons i of
    Nothing => anyToken
    Just (i', result) => Done i' result

export
satisfy : Stream i e => (e -> Bool) -> Parser i e
satisfy predicate = More (Fail "satisfy") $ \i =>
  case uncons i of
    Nothing => satisfy predicate
    Just (i', token) => if predicate token then Done i' token else Fail "satisfy"

export
eof : Monoid i => Parser i ()
eof = More (Done neutral ()) (\_ => Fail "eof")

export
token : (Stream i e, Eq e) => e -> Parser i e
token c = satisfy (c ==) <?> "token"

export
string : (Stream i e, Stream i' e) => (Eq e) => i' -> Parser i i'
string xxs = case uncons xxs of
  Nothing => pure xxs -- pure neutral
  Just (xs, x) => token x *> string xs *> pure xxs

export
lookAhead : Stream i e => Parser i e
lookAhead = More (Fail "lookAhead") $ \i =>
  case uncons i of
    Nothing => lookAhead
    Just (xs, x) => Done i x

export
notFollowedBy : Monoid i => Parser i a -> Parser i ()
notFollowedBy = lookAheadNotInto neutral
  where
  lookAheadNotInto : i -> Parser i a -> Parser i ()
  lookAheadNotInto i parser =
    case parser of
      Fail _ => Done i ()
      More on_eof on_feed => More (lookAheadNotInto i on_eof) (\i' => lookAheadNotInto (i <+> i') (on_feed i'))
      Done _ _ => Fail "notFollowedBy"

export
acceptAll : Monoid i => Parser i i
acceptAll = More (pure neutral) $ \i => (<+> i) <$> acceptAll

-- show

export
showWith : Show i => ((i -> Parser i r) -> String) -> (r -> String) -> Parser i r -> String
showWith show_on_feed show_result parser =
  case parser of
    Done i r => "Done " <+> show i <+> " " <+> show_result r
    More on_eof on_feed => "More " <+> show_on_feed on_feed  <+> " or else " <+> showWith show_on_feed show_result on_eof
    Fail msg => "Fail " <+> msg

export
(Show i, Show r) => Show (Parser i r) where
  show = showWith (const "...") show

-- char stuff

export
lower : (Stream i Char) => Parser i Char
lower = satisfy isLower

export
upper : (Stream i Char) => Parser i Char
upper = satisfy isUpper

export
alpha : (Stream i Char) => Parser i Char
alpha = satisfy isAlpha

export
alphaNum : (Stream i Char) => Parser i Char
alphaNum = satisfy isAlphaNum

export
newline : (Stream i Char) => Parser i Char
newline = satisfy isNL

export
space : (Stream i Char) => Parser i Char
space = satisfy isSpace

export
digit : (Stream i Char) => Parser i (Fin 10)
digit = More (Fail "digit") $ \i => case uncons i of
  Nothing => digit
  Just (xs, x) => case x of {
    '0' => Done xs 0; '1' => Done xs 1; '2' => Done xs 2; '3' => Done xs 3; '4' => Done xs 4;
    '5' => Done xs 5; '6' => Done xs 6; '7' => Done xs 7; '8' => Done xs 8; '9' => Done xs 9;
    _ => Fail "digit"
  }

export
hexDigit : (Stream i Char) => Parser i (Fin 16)
hexDigit = More (Fail "digit") $ \i => case uncons i of
  Nothing => hexDigit
  Just (xs, x) => case x of {
    '0' => Done xs 0; '1' => Done xs 1; '2' => Done xs 2; '3' => Done xs 3;
    '4' => Done xs 4; '5' => Done xs 5; '6' => Done xs 6; '7' => Done xs 7;
    '8' => Done xs 8; '9' => Done xs 9; 'A' => Done xs 10; 'B' => Done xs 11;
    'C' => Done xs 12; 'D' => Done xs 13; 'E' => Done xs 14; 'F' => Done xs 15;
    'a' => Done xs 10; 'b' => Done xs 11; 'c' => Done xs 12; 'd' => Done xs 13;
    'e' => Done xs 14; 'f' => Done xs 15;
    _ => Fail "hexDigit"
  }

export
octDigit : (Stream i Char) => Parser i (Fin 8)
octDigit = More (Fail "digit") $ \i => case uncons i of
  Nothing => octDigit
  Just (xs, x) => case x of {
    '0' => Done xs 0; '1' => Done xs 1; '2' => Done xs 2; '3' => Done xs 3;
    '4' => Done xs 4; '5' => Done xs 5; '6' => Done xs 6; '7' => Done xs 7;
    _ => Fail "octDigit"
  }


text:
module Gspider.File.FrequencyFileParsing

%access private

||| Represents a password frequency.
public export
record PasswordFrequency where
  ||| Constructs a password frequency.
  |||
  ||| @ord the guessing order
  ||| @pwd the password
  ||| @freq the frequency
  constructor MkPasswordFrequency
  pwd : String
  freq : Int

||| Attempts to transform a list of fields to a password frequency.
|||
||| @fields the list of fields to attempt to transform
parseFields : (fields : List String) -> Maybe PasswordFrequency
parseFields [] = Nothing
parseFields (key :: []) = Nothing
parseFields (key :: value :: _) = Just (MkPasswordFrequency key (cast value))

||| Attempts to transform a raw data row to a frequency file record.
|||
||| @delim the delimiter that separates fields in the frequency file
||| @row the raw data row to attempt to transform
parseRow : (delim : Char) -> (row : String) -> Maybe PasswordFrequency
parseRow delim row = parseFields (split (== delim) row)

||| Transforms raw frequency file data to a list of password frequencies.
|||
||| @delim the delimiter that separates fields in the frequency file
||| @rows the raw data rows to transform
export
parseRows : (delim : Char) -> (rows : String) -> List PasswordFrequency
parseRows delim rows = catMaybes (map (parseRow delim) (lines rows))

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the echo protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module EchoProtocol

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import RFC.Echo

-- ---------------------------------------------------------- [ Server Process ]

||| Implementation of the Echo Protocol from the Server's perspective.
|||
||| @client The PID of the client process.
covering
echoServer : (client : PID)
           -> Process (echo) 'Server ['Client := client] [STDIO] ()
echoServer client = do
    msg <- recvFrom 'Client
    case msg of
      Just m => do
        sendTo 'Client (m ** Refl)
        rec (echoServer client)

      Nothing => return ()

-- ---------------------------------------------------------- [ Client Process ]

||| Implementation of the Echo Protocol from the Client's perspective.
|||
||| @server The PID of the server process.
covering
echoClient : (server : PID)
           -> Process (echo) 'Client ['Server := server] [STDIO] ()
echoClient server = do
    putStrLn "Enter some text ('q' to quit):"
    msg_raw <- getStr
    case (processMsg (trim msg_raw)) of
      Nothing => do
        sendTo 'Server Nothing
        return ()

      Just m => do
        sendTo 'Server (Just m)
        (resp ** _ ) <- recvFrom 'Server
        putStrLn $ show resp
        rec (echoClient server)

  where
    processMsg : String -> Maybe String
    processMsg msg = case msg == "q" of
                       True => Nothing
                       False => Just msg

-- ------------------------------------------------------ [ Sample Innvocation ]

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
covering
doEchoProcess : IO ()
doEchoProcess = runConc [()] doEcho
  where
    doEcho : Process (echo) 'Client [] [STDIO] ()
    doEcho = do
       server <- spawn (echoServer) [()]
       setChan 'Server server
       echoClient server
       dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doEchoProcess

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Average

import Data.List
import Data.Strings
import System.REPL

average : (str : String) -> Double
average str = let numWords = length (words str)
                  totalLength = sum (allLengths (words str)) in
                  cast totalLength / cast numWords
               where
                 allLengths : List String -> List Nat
                 allLengths strs = map length strs

showAverage : (str : String) -> String
showAverage str = "The average word length is " ++ show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string: " showAverage

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Data.CatList

import Data.CatQueue
import Data.List.Properties
import Interfaces.Verified

%default total
%access public export
%hide Prelude.Stream.(::)

-- | A strict catenable list.
-- |
-- | `CatList` may be empty, represented by `CatNil`.
-- |
-- | `CatList` may be non-empty, represented by `CatCons`. The `CatCons`
-- | data constructor takes the first element of the list and a queue of
-- | `CatList`.
data CatList a = CatNil | CatCons a (CatQueue (CatList a))

data NonEmptyCatList : CatList a -> Type where
  IsNonEmptyCatList : NonEmptyCatList (CatCons a as)

data EmptyCatList : CatList a -> Type where
  IsEmptyCatList : EmptyCatList CatNil

data SingletonCatList : CatList a -> Type where
  IsSingletonCatList : SingletonCatList (CatCons a (MkCatQueue [] []))

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

-- | Create an empty catenable list.
-- |
-- | Running time: `O(1)`
empty : CatList a
empty = CatNil

-- | Test whether a catenable list is empty.
-- |
-- | Running time: `O(1)`
null : CatList a -> Bool
null CatNil = True
null _ = False

-- | Links two catenable lists by making appending the queue in the
-- | first catenable list to the second catenable list. This operation
-- | creates a new catenable list.
-- |
-- | Running time: `O(1)`
link : CatList a -> CatList a -> CatList a
link CatNil cat = cat
link (CatCons a q) cat = CatCons a (snoc q cat)

-- | Append all elements of a catenable list to the end of another
-- | catenable list, create a new catenable list.
-- |
-- | Running time: `O(1)`
append : CatList a -> CatList a -> CatList a
append as CatNil = as
append CatNil as = as
append as bs = link as bs

-- | Append an element to the beginning of the catenable list, creating a new
-- | catenable list.
-- |
-- | Running time: `O(1)`
cons : a -> CatList a -> CatList a
cons a cat = append (CatCons a neutral) cat

-- | Create a catenable list with a single item.
-- |
-- | Running time: `O(1)`
singleton : a -> CatList a
singleton a = cons a CatNil

-- | Append an element to the end of the catenable list, creating a new
-- | catenable list.
-- |
-- | Running time: `O(1)`
snoc : CatList a -> a -> CatList a
snoc cat a = append cat (CatCons a neutral)

-- | Tail recursive version of foldr on `CatList`.
-- |
-- | Ensures foldl on `List` is tail-recursive.
foldr : (CatList a -> CatList a -> CatList a) -> CatList a -> CatQueue (CatList a) -> CatList a
foldr k b q = go q Nil
  where
    foldl : (acc -> e -> acc) -> acc -> List e -> acc
    foldl _ c Nil = c
    foldl k' c (b' :: as) = foldl k' (k' c b') as

    go : CatQueue (CatList a) -> List (CatList a -> CatList a) -> CatList a
    go xs ys = assert_total $ case uncons' xs of
      Nothing => foldl (\x => \i => i x) b ys
      Just (x, rest) => go rest ((k x) :: ys)

-- | Decompose a catenable list into a tuple of the first element and
-- | the rest of the catenable list.
-- |
-- | Running time: `O(1)`
-- |
-- | Note that any single operation may run in `O(n)`.
uncons : (l : CatList a) -> {auto prf : NonEmptyCatList l} -> (a, (CatList a))
uncons (CatCons a q) = (a, (if null q then CatNil else (foldr link CatNil q)))

uncons' : CatList a -> Maybe (a, (CatList a))
uncons' CatNil = Nothing
uncons' (CatCons a q) = Just (a, (if null q then CatNil else (foldr link CatNil q)))

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

Eq l => Eq (CatList l) where
  (==) CatNil CatNil = True
  (==) CatNil (CatCons x y) = False
  (==) (CatCons x z) CatNil = False
  (==) (CatCons x z) (CatCons y w) = x == y && (assert_total (z == w))
  (/=) x y = not (x == y)

Show l => Show (CatList l) where
  show CatNil = "CatNil"
  show (CatCons x y) = "CatCons " <+> show x <+> " " <+> assert_total (show y)

Ord l => Ord (CatList l) where
  compare CatNil CatNil = EQ
  compare CatNil _ = LT
  compare _ CatNil = GT
  compare (CatCons _ z) (CatCons _ w) = assert_total $ compare z w

Semigroup (CatList l) where
  (<+>) xs ys = append xs ys

Monoid (CatList l) where
  neutral = empty

Functor CatList where
  map f CatNil = CatNil
  map f (CatCons x y) = CatCons (f x) (assert_total $ map (\e => map f e) y)

--------------------------------------------------------------------------------
-- Verified implementations
--------------------------------------------------------------------------------

mapDistCons : (Functor m) => (f : a -> b) -> (x : m a) -> (xs : List (m a)) ->
              map (\e => map f e) (x :: xs) = map f x :: map (\e => map f e) xs
mapDistCons f x [] = Refl
mapDistCons f x (y :: xs) = Refl

total
mapFunctorIdentity : (VerifiedFunctor m) => (x : m a) -> (xs : List (m a)) ->
                     map (\e => map Prelude.Basics.id e) (x :: xs) = (x :: xs)
mapFunctorIdentity x [] =
  let verifiedFunctorIdentity = functorIdentity x in
  rewrite verifiedFunctorIdentity in Refl
mapFunctorIdentity x (y :: ys) =
  let verifiedFunctorIdentity = functorIdentity x in
  let inductiveHypothesis = mapFunctorIdentity y ys in
  rewrite verifiedFunctorIdentity in
  rewrite inductiveHypothesis in Refl

VerifiedFunctor CatList where
  functorIdentity CatNil = Refl
  functorIdentity (CatCons x (MkCatQueue [] [])) = Refl
  functorIdentity (CatCons x (MkCatQueue [] (y :: ys))) =
    rewrite assert_total $ mapFunctorIdentity y ys in Refl
  functorIdentity (CatCons x (MkCatQueue (y :: ys) [])) =
    rewrite assert_total $ mapFunctorIdentity y ys in Refl
  functorIdentity (CatCons x (MkCatQueue (y :: ys) (z :: zs))) =
    rewrite assert_total $ mapFunctorIdentity y ys in
    rewrite assert_total $ mapFunctorIdentity z zs in Refl
  functorComposition CatNil g1 g2 = Refl
  functorComposition (CatCons x (MkCatQueue [] [])) g1 g2 = Refl
  functorComposition (CatCons x (MkCatQueue [] (y :: xs))) g1 g2 =
    let ind = functorComposition (y :: xs) (map g1) (map g2) in ?VerifiedFunctor_rhs_4
  functorComposition (CatCons x (MkCatQueue (y :: xs) ys)) g1 g2 = ?VerifiedFunctor_rhs_3

VerifiedSemigroup (CatList a) where
  semigroupOpIsAssociative CatNil CatNil CatNil = Refl
  semigroupOpIsAssociative CatNil CatNil (CatCons x y) = Refl
  semigroupOpIsAssociative CatNil (CatCons x y) CatNil = Refl
  semigroupOpIsAssociative CatNil (CatCons x y) (CatCons z w) = Refl
  semigroupOpIsAssociative (CatCons x y) CatNil CatNil = Refl
  semigroupOpIsAssociative (CatCons x y) CatNil (CatCons z w) = Refl
  semigroupOpIsAssociative (CatCons x y) (CatCons z w) CatNil = Refl
  semigroupOpIsAssociative (CatCons x (MkCatQueue xs ys)) (CatCons z (MkCatQueue zs ws)) (CatCons s (MkCatQueue y w)) = ?VerifiedSemigroup_rhs_3

VerifiedMonoid (CatList a) where
  monoidNeutralIsNeutralL CatNil = Refl
  monoidNeutralIsNeutralL (CatCons x y) = Refl
  monoidNeutralIsNeutralR CatNil = Refl
  monoidNeutralIsNeutralR (CatCons x y) = Refl

-------------------------------------------------------------------------------
-- | Properties
-------------------------------------------------------------------------------

appendEmptyEmpty : (l : CatList a) -> (l' : CatList a) ->
                   {auto prf : EmptyCatList l} -> {auto prf : EmptyCatList l'} ->
                   EmptyCatList (append l l')
appendEmptyEmpty CatNil CatNil = IsEmptyCatList

singletonNonEmpty : SingletonCatList l -> NonEmptyCatList l
singletonNonEmpty IsSingletonCatList = IsNonEmptyCatList

consEmptyNonEmpty : (x : a) -> (l : CatList a) -> {auto prf : EmptyCatList l} -> NonEmptyCatList (cons x l)
consEmptyNonEmpty x CatNil = IsNonEmptyCatList

consEmptySingleton : (x : a) -> (l : CatList a) -> {auto prf : EmptyCatList l} -> SingletonCatList (cons x l)
consEmptySingleton x CatNil = IsSingletonCatList

snocEmptyNonEmpty : (x : a) -> (l : CatList a) -> {auto prf : EmptyCatList l} -> NonEmptyCatList (snoc l x)
snocEmptyNonEmpty x CatNil = IsNonEmptyCatList

snocEmptySingleton : (x : a) -> (l : CatList a) -> {auto prf : EmptyCatList l} -> SingletonCatList (snoc l x)
snocEmptySingleton x CatNil = IsSingletonCatList

appendNilRightNeutralCL : (l : CatList a) -> (l' : CatList a) -> {auto prf : EmptyCatList l'} -> l = append l l'
appendNilRightNeutralCL l CatNil = Refl

appendNilLeftNeutralCL : (l : CatList a) -> (l' : CatList a) -> {auto prf : EmptyCatList l'} -> l = append l' l
appendNilLeftNeutralCL CatNil CatNil = Refl
appendNilLeftNeutralCL (CatCons x y) CatNil = Refl

max_stars_repo_name: Risto-Stevcev/idris-catenatable-lists

max_issues_repo_name: Risto-Stevcev/idris-catenable-lists

max_forks_repo_name: Risto-Stevcev/idris-catenatable-lists


text:
WIP

module Main
import System.File

main : IO ()
main = do myfile <- readFile "in.txt"
          case myfile of
              Right fileContent => putStrLn fileContent
              Left err => printLn err


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the echo protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module EchoProcess

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System
import System.Protocol

import RFC.Echo

-- ---------------------------------------------------------- [ Server Process ]

||| Implementation of the Echo Protocol from the Server's perspective.
|||
||| @client The PID of the client process.
covering
echoServer : (client : PID)
           -> Process (echo) 'Server ['Client := client] [STDIO] ()
echoServer client = do
    msg <- recvFrom 'Client
    case msg of
      Just m => do
        sendTo 'Client (m ** Refl)
        rec (echoServer client)

      Nothing => return ()

-- ---------------------------------------------------------- [ Client Process ]

||| Implementation of the Echo Protocol from the Client's perspective.
|||
||| @server The PID of the server process.
covering
echoClient : Maybe String
           -> (server : PID)
           -> Process (echo) 'Client ['Server := server] [STDIO] ()
echoClient msg server = do
    case msg of
      Nothing => do
        sendTo 'Server Nothing
      Just str => do
        sendTo 'Server (Just str)
        (resp ** _ ) <- recvFrom 'Server
        putStrLn $ show resp
        rec (echoClient Nothing server)

-- ------------------------------------------------------ [ Sample Innvocation ]

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
covering
doEchoProcess : String -> IO ()
doEchoProcess s = runConc [()] (doEcho s)
  where
    doEcho : String -> Process (echo) 'Client [] [STDIO] ()
    doEcho s = do
       server <- spawn (echoServer) [()]
       setChan 'Server server
       echoClient (Just s) server
       dropChan 'Server

processArgs : (List String) -> Maybe String
processArgs [x] = Nothing
processArgs (x::xs) = Just $ unwords xs

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = do
    args <- getArgs
    case processArgs args of
      Just str => doEchoProcess str
      Nothing => doEchoProcess "\n"

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


text:
module Data.CatQueue

import Data.List.Properties
import Interfaces.Verified

%hide Prelude.List.reverse
%hide Prelude.Strings.reverse
%hide Prelude.Strings.null
%hide Prelude.Strings.(++)

%default total
%access public export

data CatQueue a = MkCatQueue (List a) (List a)

data NonEmptyCatQueue : CatQueue a -> Type where
  IsNonEmptyCatQueue : Either (NonEmpty x) (NonEmpty y) ->
                       NonEmptyCatQueue (MkCatQueue x y)

data EmptyCatQueue : CatQueue a -> Type where
  IsEmptyCatQueue : EmptyCatQueue (MkCatQueue [] [])

data SingletonCatQueue : CatQueue a -> Type where
  IsSingletonCatQueueLeft : SingletonCatQueue (MkCatQueue [x] [])
  IsSingletonCatQueueRight : SingletonCatQueue (MkCatQueue [] [x])

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

Uninhabited (NonEmptyCatQueue (MkCatQueue [] [])) where
  uninhabited (IsNonEmptyCatQueue (Left IsNonEmpty)) impossible
  uninhabited (IsNonEmptyCatQueue (Right IsNonEmpty)) impossible

Show q => Show (CatQueue q) where
  show (MkCatQueue xs ys) = "MkCatQueue " <+> show xs <+> " " <+> show ys

Eq q => Eq (CatQueue q) where
  (==) (MkCatQueue xs ys) (MkCatQueue zs ws) =
    xs <+> reverse ys == zs <+> reverse ws
  (/=) x y = not (x == y)

Ord q => Ord (CatQueue q) where
  compare (MkCatQueue [] []) (MkCatQueue [] []) = EQ
  compare (MkCatQueue [] []) _ = LT
  compare _ (MkCatQueue [] []) = GT
  compare (MkCatQueue xs ys) (MkCatQueue zs ws) = compare (xs <+> reverse ys) (zs <+> reverse ws)

Semigroup (CatQueue q) where
  (<+>) (MkCatQueue xs ys) (MkCatQueue zs ws) = MkCatQueue ((xs <+> reverse ys) <+> (zs <+> reverse ws)) []

Monoid (CatQueue q) where
  neutral = MkCatQueue [] []

Functor CatQueue where
  map f (MkCatQueue xs ys) = MkCatQueue (map f xs) (map f ys)

Foldable CatQueue where
  foldr f init (MkCatQueue xs ys) = foldr f init (xs <+> reverse ys)
  foldl f init (MkCatQueue xs ys) = foldl f init (xs <+> reverse ys)

--------------------------------------------------------------------------------
-- Verified implementations
--------------------------------------------------------------------------------

-- TODO: how do I formally write that this is an axiom?
private
axiomCatQueueSame : (xs : List a) -> (ys : List a) -> MkCatQueue xs ys = MkCatQueue (xs <+> reverse ys) []
axiomCatQueueSame xs ys = ?axiomCatQueueSame_rhs

-- However, we can't use this axiom due to some limitations of ITT. Even though we have an axiom saying that these
-- two CatQueues are the same, we can contradict this axiom easily:
private
inconsistentAxiom : MkCatQueue xs ys = MkCatQueue (xs <+> reverse ys) [] -> Void
inconsistentAxiom = case axiomCatQueueSame [] [1] of Refl impossible

-- This could be viewed as a reasonable compromise, since we're only using it internally to prove that other
-- properties hold. But it severely limits the ability to provide proofs for this type of data structure, specifically
-- any data structure where two different constructions are considered equal

VerifiedFunctor CatQueue where
  functorIdentity (MkCatQueue xs ys) =
    rewrite functorIdentity xs in
    rewrite functorIdentity ys in Refl
  functorComposition (MkCatQueue xs ys) g1 g2 =
    rewrite functorComposition xs g1 g2 in
    rewrite functorComposition ys g1 g2 in Refl

VerifiedSemigroup (CatQueue q) where
  semigroupOpIsAssociative (MkCatQueue ls ls') (MkCatQueue cs cs') (MkCatQueue rs rs') =
    rewrite appendAssociative (ls ++ reverse' [] ls') ((cs ++ reverse' [] cs') ++ rs ++ reverse' [] rs') [] in
    rewrite appendNilRightNeutral ((ls ++ reverse' [] ls') ++ cs ++ reverse' [] cs') in
    rewrite appendNilRightNeutral ((ls ++ reverse' [] ls') ++ (cs ++ reverse' [] cs') ++ rs ++ reverse' [] rs') in
    rewrite appendAssociative (ls ++ reverse' [] ls') (cs ++ reverse' [] cs') (rs ++ reverse' [] rs') in
    Refl

VerifiedMonoid (CatQueue q) where
  monoidNeutralIsNeutralL (MkCatQueue xs ys) =
    rewrite appendNilRightNeutral (xs ++ reverse' [] ys) in
    rewrite axiomCatQueueSame xs ys in
    Refl
  monoidNeutralIsNeutralR (MkCatQueue xs ys) =
    rewrite axiomCatQueueSame xs ys in
    Refl

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

-- | Test whether a queue is empty.
-- |
-- | Running time: `O(1)`
null : CatQueue a -> Bool
null (MkCatQueue [] []) = True
null _ = False

-- | Append an element to the end of the queue, creating a new queue.
-- |
-- | Running time: `O(1)`
snoc : CatQueue a -> a -> CatQueue a
snoc (MkCatQueue l r) a = MkCatQueue l (a :: r)

-- | Decompose a queue into a `Tuple` of the first element and the rest of the queue.
-- |
-- | Running time: `O(1)`
-- |
-- | Note that any single operation may run in `O(n)`.
uncons : (q : CatQueue a) -> {auto prf : NonEmptyCatQueue q} -> (a, CatQueue a)
uncons (MkCatQueue [] []) {prf} = absurd prf
uncons (MkCatQueue [] (x :: xs)) = uncons_prf (x :: xs) {prf' = reverseNonEmpty (x :: xs) IsNonEmpty}
  where
    uncons_prf : (l : List a) -> {auto prf : NonEmpty l} -> {prf' : NonEmpty (reverse l)} -> (a, CatQueue a)
    uncons_prf l = assert_total $ uncons (MkCatQueue (reverse l) [])
uncons (MkCatQueue (x :: xs) ys) = (x, (MkCatQueue xs ys))

-- | Decompose a queue into a `Tuple` of the first element and the rest of the queue.
-- |
-- | Running time: `O(1)`
-- |
-- | Note that any single operation may run in `O(n)`.
uncons' : CatQueue a -> Maybe (a, (CatQueue a))
uncons' (MkCatQueue [] []) = Nothing
uncons' (MkCatQueue [] r) = assert_total $ uncons' (MkCatQueue (reverse r) [])
uncons' (MkCatQueue (a :: as) r) = Just (a, (MkCatQueue as r))

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

snocNotEmpty : (x : a) -> (q : CatQueue a) -> {auto prf : EmptyCatQueue q} -> NonEmptyCatQueue (snoc q x)
snocNotEmpty x q@(MkCatQueue [] []) = the (NonEmptyCatQueue (snoc q x)) (IsNonEmptyCatQueue (Right IsNonEmpty))

singletonNonEmpty : SingletonCatQueue q -> NonEmptyCatQueue q
singletonNonEmpty IsSingletonCatQueueLeft = IsNonEmptyCatQueue (Left IsNonEmpty)
singletonNonEmpty IsSingletonCatQueueRight = IsNonEmptyCatQueue (Right IsNonEmpty)

snocEmptySingleton : (x : a) -> (q : CatQueue a) -> {auto prf : EmptyCatQueue q} -> SingletonCatQueue (snoc q x)
snocEmptySingleton x (MkCatQueue [] []) = IsSingletonCatQueueRight

nonEmptyNotNull : (q : CatQueue a) -> {auto prf : NonEmptyCatQueue q} -> null q = False
nonEmptyNotNull (MkCatQueue [] []) {prf} = absurd prf
nonEmptyNotNull (MkCatQueue (x :: xs) []) = Refl
nonEmptyNotNull (MkCatQueue [] (y :: ys)) = Refl
nonEmptyNotNull (MkCatQueue (x :: xs) (y :: ys)) = Refl

Uninhabited (False = True) where
  uninhabited Refl impossible

nullDecidable : (q : CatQueue a) -> Dec (null q = True)
nullDecidable (MkCatQueue [] []) = Yes Refl
nullDecidable (MkCatQueue (x::xs) []) = No uninhabited
nullDecidable (MkCatQueue [] (x::xs)) = No uninhabited
nullDecidable (MkCatQueue (x::xs) (y::ys)) = No uninhabited


text:
module Data.Profunctor

import public Control.Applicative.Const
import public Control.Monad.Identity
import public Data.Morphisms

--------------------------------------------------------------------------------
--          Forget
--------------------------------------------------------------------------------

public export
record Forget (r : Type) (a : Type) (b : Type) where
  constructor MkForget
  fun : a -> Maybe r

public export
Functor (Forget r a) where
  map _ (MkForget fun) = MkForget fun

--------------------------------------------------------------------------------
--          Profunctor
--------------------------------------------------------------------------------

public export
interface (forall a . Functor (p a)) => Profunctor (0 p : Type -> Type -> Type) where
  dimap : (i2 -> i1) -> (o1 -> o2) -> p i1 o1 -> p i2 o2

  lmap : (i2 -> i1) -> p i1 o -> p i2 o
  lmap f = dimap f id

  rmap : (o1 -> o2) -> p i o1 -> p i o2
  rmap = dimap id

public export
Profunctor Morphism where
  dimap f g (Mor fun) = Mor $ g . fun . f

public export
Profunctor (Forget r) where
  dimap f _ (MkForget fun) = MkForget (fun . f)

public export
Functor m => Profunctor (Kleislimorphism m) where
  dimap f g (Kleisli fun) = Kleisli (map g . fun . f)

--------------------------------------------------------------------------------
--          Strong
--------------------------------------------------------------------------------

public export
interface Profunctor p => Strong p where
  first  : p a b -> p (a,c) (b,c)
  second : p a b -> p (c,a) (c,b)

public export
Strong Morphism where
  first  (Mor f) = Mor $ mapFst f
  second (Mor f) = Mor $ mapSnd f

public export
Functor m => Strong (Kleislimorphism m) where
  first  (Kleisli f) = Kleisli $ \(a,c) => (,c) <$> f a
  second (Kleisli f) = Kleisli $ \(c,a) => (c,) <$> f a

public export
Strong (Forget r) where
  first  (MkForget f) = MkForget $ \(a,_) => f a
  second (MkForget f) = MkForget $ \(_,a) => f a

--------------------------------------------------------------------------------
--          Choice
--------------------------------------------------------------------------------

public export
interface Profunctor p => Choice p where
  left  : p a b -> p (Either a c) (Either b c)
  right : p a b -> p (Either c a) (Either c b)

public export
Choice Morphism where
  left  (Mor f) = Mor $ mapFst f
  right (Mor f) = Mor $ mapSnd f

public export
Applicative m => Choice (Kleislimorphism m) where
  left  (Kleisli f) = Kleisli $ bitraverse f pure
  right (Kleisli f) = Kleisli $ bitraverse pure f

public export
Choice (Forget r) where
  left  (MkForget f) = MkForget $ either f (const Nothing)
  right (MkForget f) = MkForget $ either (const Nothing) f


text:
module Trie

import FiniteMap

%default total
%access private

export
data Trie : (Type -> Type) -> Type -> Type -> Type where
  MkTrie : Maybe a -> mk (Trie mk ks a) -> Trie mk ks a

export
FiniteMap m k => FiniteMap (Trie (m k)) (List k) where
  empty = assert_total $ MkTrie Nothing empty

  lookup [] t = assert_total $ case t of
    MkTrie b m => b
  lookup (k :: ks) t = assert_total $ case t of
    MkTrie b m => lookup k m >>= \m' => lookup ks m'

  bind [] x t = assert_total $ case t of
    MkTrie b m => MkTrie (Just x) m
  bind (k :: ks) x t = assert_total $ case t of
    MkTrie b m => let t = fromMaybe empty $ lookup k m
                      t' = bind ks x t
                  in MkTrie b (bind k t' m)


text:
module WebAssembly

import public WebAssembly.Structure
import public WebAssembly.Validation

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module AOC.Day.Three

import Data.Vect
import Data.String
import Decidable.Equality

%default total

data Bit : Type where
  Low : Bit
  High : Bit

Show Bit where
  show Low = "0"
  show High = "1"

Byte : (n : Nat) -> Type
Byte n = Vect n Bit

-- The only problem with this is that I now need to prove that all inputs
-- provided are of the same length. What fun.
data Binary : Nat -> Type where
  BE : Binary Z
  B0 : Binary n -> Binary (S n)
  B1 : Binary n -> Binary (S n)

export
Show (Binary n) where
  show BE = ""
  show (B0 b) = "0" ++ show b
  show (B1 b) = "1" ++ show b

----------------------------------------------------------------------------
-- Code I did not need hooray ----------------------------------------------
----------------------------------------------------------------------------

toBinary' : (s : List Char) -> Maybe (Binary (length s))
toBinary' [] = Just BE
toBinary' ('0' :: str) = (toBinary' str) >>= (\bin => Just $ B0 bin)
toBinary' ('1' :: str) = (toBinary' str) >>= (\bin => Just $ B1 bin)
toBinary' _ = Nothing

-- This works only if the type is unpacked in the type. Otherwise there is a
-- conflict in the length function used.
toBinary : (s : String) -> Maybe (Binary (length (unpack s)))
toBinary s = toBinary' (unpack s)

public export
Eq (Binary n) where
  (==) BE BE = False
  (==) (B0 x) (B0 y) = x == y
  (==) (B0 x) (B1 y) = False
  (==) (B1 x) (B0 y) = False
  (==) (B1 x) (B1 y) = x == y

-- The new Control.Function defines the `Injective` interface, which would make
-- these definitions unnecessary.
B0Injective : (0 left, right : Binary n) -> B0 left = B0 right -> left = right
B0Injective _ _ Refl = Refl

B1Injective : (0 left, right : Binary n) -> B1 left = B1 right -> left = right
B1Injective _ _ Refl = Refl

-- Sweet, I don't actually need this for the exactLength function
public export
DecEq (Binary n) where
  decEq BE BE = Yes Refl
  decEq (B0 x) (B0 y) with (decEq x y)
    decEq (B0 x) (B0 y) | (Yes prf) = Yes (cong B0 prf)
    decEq (B0 x) (B0 y) | (No contra) = No $ \h : (B0 x = B0 y) => contra $ B0Injective x y h
  decEq (B1 x) (B1 y) with (decEq x y)
    decEq (B1 x) (B1 y) | (Yes prf) = Yes (cong B1 prf)
    decEq (B1 x) (B1 y) | (No contra) = No $ \h : (B1 x = B1 y) => contra $ B1Injective x y h
  decEq (B0 x) (B1 y) = No B0B1impossible
    where
      B0B1impossible : (B0 x = B1 y) -> Void
      B0B1impossible Refl impossible
  decEq (B1 x) (B0 y) = No B1B0impossible
    where
      B1B0impossible : (B1 x = B0 y) -> Void
      B1B0impossible Refl impossible

----------------------------------------------------------------------------
-- Proofs required for parsing ---------------------------------------------
----------------------------------------------------------------------------

exactLength : {m : Nat} -> -- expected at run-time
              (len : Nat) -> (xs : Binary m) -> Maybe (Binary len)
exactLength {m} len xs with (decEq m len)
  exactLength {m = m} m xs | (Yes Refl) = Just xs
  exactLength {m = m} len xs | (No contra) = Nothing

-- Stolen from https://github.com/jumper149/AoC2021/blob/main/03/src/Main.idr
exactLengths : (len : Nat) -> Traversable t => t (n ** Binary n) -> Maybe (t (Binary len))
exactLengths len xs = traverse (\ x => exactLength len x.snd) xs

----------------------------------------------------------------------------
-- Actual parsing code -----------------------------------------------------
----------------------------------------------------------------------------

toBinaryDep' : (s : List Char) -> Maybe (n ** Binary n)
toBinaryDep' [] = Just (0 ** BE)
toBinaryDep' ('0' :: str) = (toBinaryDep' str) >>= (\(n ** bin) => Just $ (S n ** B0 bin))
toBinaryDep' ('1' :: str) = (toBinaryDep' str) >>= (\(n ** bin) => Just $ (S n ** B1 bin))
toBinaryDep' _ = Nothing

export
toBinaryDep : (s : String) -> Maybe (n ** Binary n)
toBinaryDep s = toBinaryDep' (unpack s)

export
parseBinary : List (n ** Binary n) -> Maybe (m ** List (Binary m))
parseBinary [] = Just (0 ** [])
parseBinary ((len ** bin) :: ys) = do
    list <- exactLengths len ys
    pure (len ** bin :: list)

  -- Ok, this does not work for some reason or another
  -- Prove that the size of the binary numbers in ys is the same as the size of
  -- bin.

  -- (ys_len ** ys) <- parseBinary ys
  -- bin <- exactLength ys_len bin

  -- -- With the sizes resolved, reconstruct with the dependent pair on the outside
  -- -- of the list.
  -- pure (ys_len ** bin :: ys)

----------------------------------------------------------------------------
-- Implementing Vect like interfaces for Binary ----------------------------
----------------------------------------------------------------------------

-- Most of these functions are just to make it easier to answer the AOC questions, since they involve transforming the individual bits into a

binaryToVect : Binary n -> Vect n Bool
binaryToVect BE = []
binaryToVect (B0 x) = False :: (binaryToVect x)
binaryToVect (B1 x) = True :: (binaryToVect x)

mapBinary : (Bool -> a) -> Binary n -> Vect n a
mapBinary f = map f . binaryToVect

-- day3 : List String -> (Integer, Integer)
-- day3 binary = ?something


text:
module Term

-- Simply-typed lambda calculus with
--   (1) natural numbers as the only base type, and
--   (2) general recursion.
-- This calculus is also referred to as PCF.
--
-- Note that variables in the lambda calculus are not
-- named but identified by their de Bruijn index.

import Data.Fin
import public Data.Vect

%default total
%access public export

---------------------------------------------------
-- Begin: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS

-- Data type 'Ty' represents the types in the
-- simply-typed lambda calculus:
--   (1) Base type 'TyNat' of natural numbers.
--   (2) Type constructor 'TyFun' for forming
--       function types.
data Ty = TyNat | TyFun Ty Ty

-- Simplified syntax for function types:
infixr 10 :->:
(:->:) : Ty -> Ty -> Ty
(:->:) t1 t2 = TyFun t1 t2

-- End: TYPES IN THE SIMPLY-TYPED LAMBDA CALCULUS
-------------------------------------------------

---------------------------------------------------------
-- Begin: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS

Context : Nat -> Type
Context n = Vect n Ty

-- End: CONTEXT FOR TYPING TERMS IN THE LAMBDA CALCULUS
-------------------------------------------------------

-------------------------------------------------
-- Begin: WELL-TYPED TERMS OF THE LAMBDA CALCULUS

-- Data type of well-typed terms in the
-- simply-typed lambda calculus:
data Term : Context n -> Ty -> Type where
  -- Variable:
  -- The data constructor for variables ('Var') takes
  -- as arguments a de Bruijn index ('i') and a proof
  -- ('prf') that the variable at index 'i' in the
  -- context 'ctx' has type 't'.
  TVar  : (i : Fin n) -> {auto prf : index i ctx = t} ->
          Term ctx t
  -- Abstraction:
  -- The data constructor for abstractions ('Abs')
  -- takes as its first (implicit) argument the
  -- type of the variable that is bound by this
  -- abstraction.
  TAbs  : {s : Ty} -> Term (s::ctx) t ->
          Term ctx (s :->: t)
  -- Application:
  TApp  : Term ctx (s :->: t) -> Term ctx s ->
          Term ctx t
  -- Fix-point operator:
  TFix  : Term ctx (t :->: t) ->
          Term ctx t
  -- Constant 'Zero' (natural number):
  TZero : Term ctx TyNat
  -- Successor:
  TSucc : Term ctx TyNat ->
          Term ctx TyNat
  -- Predecessor:
  TPred : Term ctx TyNat ->
          Term ctx TyNat
  -- Test for equality with 'Zero'
  -- (with terms for the "then" and
  -- "else" branches):
  TIfz  : Term ctx TyNat -> Term ctx t -> Term ctx t ->
          Term ctx t

-- End: WELL-TYPED TERMS OF THE LAMBDA CALCULUS
-----------------------------------------------

---------------------------------------
-- Begin: VALUES IN THE LAMBDA CALCULUS

-- The following lambda calculus terms
-- are values (i.e. normal forms for
-- reduction under the "Step" relation):
--   (1) lambda abstractions (that are
--       not applied),
--   (2) the constant 'Zero',
--   (3) the natural number constants
--       (formed by applying 'Succ' to
--       another value).
data Value : Term [] t -> Type where
  VZero : Value TZero
  VSucc : Value e -> Value (TSucc e)
  VAbs  : Value (TAbs e)

valueTerm : {e : Term [] t} -> Value e -> Term [] t
valueTerm {e = e} _ = e

-- End: VALUES IN THE LAMBDA CALCULUS
-------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module EffCont

data Exists : List a -> a -> Type where
    Here : Exists (x :: xs) x
    There : Exists xs x -> Exists (y :: xs) x

data Effect : List (Type -> Type) -> Type -> Type where
  Pure : a -> Effect xs a
  EffectC : {f : Type -> Type} -> Exists xs f -> f a -> Effect xs a

data Eff : List (Type -> Type) -> Type -> Type where
  Cont : ({r : Type} -> (a -> r) -> ({x : Type} -> Effect xs x -> (x -> r) -> r) -> r) -> Eff xs a

pure : a -> Eff xs a
pure x = Cont (\k, imp => imp (Pure x) k)

(>>=) : Eff xs a -> (a -> Eff xs b) -> Eff xs b
(>>=) (Cont g) f = Cont (\k, imp => g (\x => let (Cont g') = f x in g' k imp) imp)

-- State effect
data State : (s : Type) -> Type -> Type where
  Get : State s s
  Put : s -> State s ()

get : {auto e : Exists xs (State s)} -> Eff xs s
get {e} = Cont (\k, imp => imp (EffectC e Get) k)

put : {auto e : Exists xs (State s)} -> s -> Eff xs ()
put {e} s = Cont (\k, imp => imp (EffectC e (Put s)) k)

-- Reader effect
data Reader : (e : Type) -> Type -> Type where
  Ask : Reader e e

ask : {auto e : Exists xs (Reader en)} -> Eff xs en
ask {e} = Cont (\k, imp => imp (EffectC e Ask) k)

-- Interpreters
runPure : Effect [] x -> (x -> r) -> r
runPure (Pure x) k = k x
runPure (EffectC Here _) _ impossible
runPure (EffectC (There _) _) _ impossible

stateImp : State s x -> (x -> s -> r) -> s -> r
stateImp Get k st = k st st
stateImp (Put st') k st = k () st'

runState : (Effect xs x -> (x -> r) -> r) -> Effect (State s :: xs) x -> (x -> s -> r) -> s -> r
runState k (Pure x) k' = k' x
runState k (EffectC Here effect) k' = stateImp effect k'
runState k (EffectC (There xs) fa) k' = \st => k (EffectC xs fa) (\x => k' x st)

readerImp : Reader e x -> (x -> e -> r) -> e -> r
readerImp Ask k e = k e e

runReader : (Effect xs x -> (x -> r) -> r) -> Effect (Reader e :: xs) x -> (x -> e -> r) -> e -> r
runReader k (Pure x) k' = k' x
runReader k (EffectC Here effect) k' = readerImp effect k'
runReader k (EffectC (There xs) fa) k' = \e => k (EffectC xs fa) (\x => k' x e)

run : (a -> r) -> ({x : Type} -> Effect xs x -> (x -> r) -> r) -> Eff xs a -> r
run k imp (Cont f) = f k imp

example : Eff [State Int, Reader Int] Int
example = do s <- get
             put (s + 1)
             s <- get
             a <- ask
             pure (s + a)

test : (Int, Int, Int)
test = let f = run (\x, s, e => (x, s, e)) (\eff, k => runState (runReader runPure) eff k) example in f 1 2

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Minecraft.Server.Main

import public Minecraft.Base.PreClassic

%default total

main : IO ()
main = do
  pure ()

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate