text:
module Interface

import Data.List
import Data.Maybe
import Data.Version
import Data.String
import System
import System.Console.Extra
import System.Directory
import System.Directory.Extra
import System.File
import System.File.Extra

import Git
import public IdvPaths
import Installed
import Interp

exitError : HasIO io => String -> io a
exitError err = do
  putStrLn ""
  putStrLn err
  putStrLn ""
  exitFailure

exitSuccess : HasIO io => String -> io a
exitSuccess msg = do
  putStrLn ""
  putStrLn msg
  putStrLn ""
  exitSuccess

createVersionsDir : HasIO io => Version -> io ()
createVersionsDir version = do
  Just resolvedVersionsDir <- pathExpansion $ versionPath version
    | Nothing => exitError "Could not resolve install directory for new Idris2 version."
  True <- createDirIfNeeded $ resolvedVersionsDir
    | False => exitError "Could not create install directory for new Idris2 version."
  pure ()

||| Assumes the current working directory is a git repository.
updateMainBranch : HasIO io => io ()
updateMainBranch = do
  True <- checkoutAndPullBranch "main"
    | False => exitError "Could not update Idris2 repository prior to building a new version."
  pure ()

||| Assumes the current working directory is a git repository with a clean target in the Makefile.
clean : HasIO io => io Bool
clean = [ res == 0 | res <- System.system "make clean" ]

||| Builds the current repository _using_ the executable for the
||| given version. This means you must have already installed the
||| given version into the versions folder (possibly as a bootstrap
||| build).
||| Assumes the current working directory is an Idris repository.
build : HasIO io => (idrisExecutable : Version) -> (installedDir : String) -> (buildPrefix : String) -> io Bool
build version installedDir buildPrefix =
  [ res == 0 | res <- System.system "PREFIX=\"\{buildPrefix}\" IDRIS2_BOOT=\"\{installedDir}\" make" ]

||| Assumes the current working directory is an Idris repository.
cleanAndBuild : HasIO io
             => Version
             -> (installedDir : String)
             -> (buildPrefix : String)
             -> io ()
cleanAndBuild version installedDir buildPrefix = do
  True <- clean
    | False => exitError "Could not clean before building."
  True <- build version installedDir buildPrefix
    | False => exitError "Failed to build the current repository with the Idris executable that should have been installed into \{installedIdrisPath version}."
  pure ()

||| Check out the given version if available (in the checkout folder
||| in preparation for building against a particular version of the
||| Idris 2 source code).
checkoutIfAvailable : HasIO io => BuildTarget -> Version -> io (Either String ())
checkoutIfAvailable target version = do
  fromMaybe (Left "Failed to switch to checkout directory.") <$>
    changeDirAndCheckout
      where
        checkoutIdris : io (Either String ())
        checkoutIdris = do
          availableVersions <- listVersions
          case List.find (== version) availableVersions of
               Nothing => pure $ Left "Version \{version} is not one of the available versions: \{availableVersions}."
               (Just resolvedVersion) => do
                 True <- checkout resolvedVersion.tag
                   | False => pure $ Left "Could not check out requested version of Idris2."
                 pure $ Right ()

        checkoutLSP : io (Either String ())
        checkoutLSP = do
          let desiredBranchName = idrisLspBranchName version
          availableBranches <- listBranches
          case List.find (desiredBranchName `isInfixOf`) availableBranches of
               Nothing => pure $ Left "The LSP does not have a branch for version \{version} Available branches: \{availableBranches}."
               (Just resolvedBranch) => do
                 True <- checkout resolvedBranch
                   | False => pure $ Left "Could not check out requested version of the Idris2 LSP."
                 pure $ Right ()

        checkoutTarget : io (Either String ())
        checkoutTarget =
          case target of
               Idris => checkoutIdris
               LSP   => checkoutLSP

        changeDirAndCheckout : io (Maybe (Either String ()))
        changeDirAndCheckout =
          inDir (relativeCheckoutPath target) $ do
            updateMainBranch
            checkoutTarget

||| Assumes the current working directory is an Idris repository.
bootstrapBuild : HasIO io => (resolvedVersion : Version) -> (buildPrefix : String) -> io ()
bootstrapBuild version buildPrefix = do
  True <- go
    | False => exitError "Failed to build Idris2 version \{version}."
  pure ()
    where
      chezExec : io (Maybe String)
      chezExec = pure $ if !(eatOutput True "which chez") then Just "chez" else Nothing

      schemeExec : io (Maybe String)
      schemeExec = pure $ if !(eatOutput True "which scheme") then Just "scheme" else Nothing

      envExec : io (Maybe String)
      envExec = getEnv "SCHEME"

      go : io Bool
      go = do
        Just exec <- pure $ !chezExec <|> !schemeExec <|> !envExec
          | Nothing => do
              putStrLn "Could not find Scheme executable. Specify executable to use with SCHEME environment variable."
              pure False
        putStrLn "Building with Scheme executable: \{exec}"
        res <- System.system "make clean && PREFIX=\"\{buildPrefix}\" SCHEME=\"\{exec}\" make bootstrap"
        pure $ res == 0

||| Assumes the current working directory is an Idris repository.
||| If `installOver` is True, the Idris 2 executable in the versions
||| directory for the version specified will be used (it will be asked
||| for the --libdir which affects where Idris installs the std libraries
||| included).
install : HasIO io
       => (installOver : Bool)
       -> (installedDir : String)
       -> Version
       -> (buildPrefix : String)
       -> io ()
install installOver installedDir version buildPrefix = do
  0 <- installCompiler
    | _ => exitError "Failed to install Idris2 \{version}."
  -- Idris2 v0.4.0 was when install-with-src was added.
  when (version >= (V 0 4 0 Nothing "")) $ do
    0 <- installLibsWithSrc
      | _ => exitError "Failed to install Idris2 libraries \{version}."
    pure ()
  putStrLn ""
  putStrLn "Idris2 version \{version} successfully installed to \{buildPrefix}."
  pure ()

  where
    executableOverride : String
    executableOverride = if installOver
                            then "IDRIS2_BOOT=\"\{installedDir}\""
                            else ""

    installCompiler : io Int
    installCompiler = System.system "PREFIX=\"\{buildPrefix}\" \{executableOverride} make install"

    installLibsWithSrc : io Int
    installLibsWithSrc = System.system "PREFIX=\"\{buildPrefix}\" \{executableOverride} make install-with-src-libs"

buildAndInstall : HasIO io => Version -> (cleanAfter : Bool) -> io ()
buildAndInstall version cleanAfter = do
  let target = Idris
  True <- cloneIfNeeded idrisRepoURL (relativeCheckoutPath target)
    | False => exitError "Failed to clone Idris2 repository into local folder."
  Right _ <- checkoutIfAvailable target version
    | Left err => exitError err
  moveDirRes <- inDir (relativeCheckoutPath target) $ do
    let proposedInstalledDir = installedIdrisPath version
    let proposedBuildPrefix = buildPrefix version
    Just installedDir <- pathExpansion proposedInstalledDir
      | Nothing => exitError "Could not resolve install directory: \{proposedInstalledDir}."
    Just buildPrefix <- pathExpansion proposedBuildPrefix
      | Nothing => exitError "Could not resolve build prefix directory: \{proposedBuildPrefix}."
    -- bootstrap build
    bootstrapBuild version buildPrefix
    install False installedDir version buildPrefix
    -- non-bootstrap build
    cleanAndBuild version installedDir buildPrefix
    install True installedDir version buildPrefix
    when cleanAfter $
      -- clean up
      ignore $ clean
  unless (isJust moveDirRes) $
    exitError "Failed to install version \{version}."

buildAndInstallLsp : HasIO io => (idrisVersion : Version) -> io ()
buildAndInstallLsp version = do
  let target = LSP
  True <- cloneIfNeeded idrisLspRepoURL (relativeCheckoutPath target)
    | False => exitError "Failed to clone Idris 2 LSP repository into local folder."
  Right _ <- checkoutIfAvailable target version
    | Left err => exitError err
  moveDirRes <- inDir (relativeCheckoutPath target) $ do
    let proposedInstalledDir = installedLspPath version
    let proposedBuildPrefix = buildPrefix version
    Just installedDir <- pathExpansion proposedInstalledDir
      | Nothing => exitError "Could not resolve install directory: \{proposedInstalledDir}."
    Just buildPrefix <- pathExpansion proposedBuildPrefix
      | Nothing => exitError "Could not resolve build prefix directory: \{proposedBuildPrefix}."
    0 <- installLsp buildPrefix
      | _ => exitError "Failed to build & install LSP."
    -- clean up
    ignore $ clean
  unless (isJust moveDirRes) $
    exitError "Failed to install LSP for version \{version}."

  where
    installLsp : (buildPrefix : String) -> io Int
    installLsp buildPrefix = System.system "PREFIX=\"\{buildPrefix}\" make install"

||| Uninstall the given version. Assumes that version exists.
uninstall : HasIO io => Version -> io ()
uninstall version = do
  Just installPath <- pathExpansion $ versionPath version
    | Nothing => exitError "Failed to locate an install path for version \{version}."
  putStrLn "uninstalling from \{installPath}..."
  -- TODO: make cross-platform remove recursive. current standard lib options won't do it.
  0 <- System.system $ "rm -rf " ++ installPath
    | _ => exitError "Failed to remove install directory."
  pure ()

||| Assumes the current directory is an Idris 2 repository. Runs only
||| the install of the Idris 2 API.
installApi : HasIO io => Version -> io ()
installApi version = do
  let proposedBuildPrefix = buildPrefix version
  Just buildPrefix <- pathExpansion proposedBuildPrefix
    | Nothing => exitError "Could not resolve build prefix directory: \{proposedBuildPrefix}."
  0 <- System.system "PREFIX=\"\{buildPrefix}\" make install-\{maybeWithSrc}"
    | _ => exitError "Failed to install Idris2 API package."
  putStrLn ""
  putStrLn "Idris2 API package successfully installed."
  ignore $ clean

  where
    -- Idris2 v0.4.0 was when install-with-src was added.
    maybeWithSrc : String
    maybeWithSrc = if version >= (V 0 4 0 Nothing "")
                      then "with-src-api"
                      else "api"

||| Select the given version if it is installed (as in set it as the version used
||| when the `idris2` command is executed). Then checkout that same version in the
||| checkout folder where builds are performed.
selectAndCheckout : HasIO io => (version : Version) -> io Bool
selectAndCheckout version = do
  Right _ <- selectVersion version
    | Left _  => pure False
  Right _ <- checkoutIfAvailable Idris version
    | Left _ => pure False
  pure True

--
-- Commands
--

export
listVersionsCommand : HasIO io => io ()
listVersionsCommand = do
  True <- cloneIfNeeded idrisRepoURL (relativeCheckoutPath Idris)
    | False => exitError "Failed to clone Idris2 repository into local folder."
  Just remoteVersions <- inDir (relativeCheckoutPath Idris) fetchAndListVersions
    | Nothing => exitError "Failed to retrieve remote versions."
  Just installedVersions <- Installed.listVersions
    | Nothing => exitError "Failed to list local versions."
  systemInstall <- getSystemVersion
  selectedVersion <- getSelectedVersion
  let isSystemSelected = isNothing $ (flip find installedVersions) . (==) =<< selectedVersion
  let selectedInstalled = buildSelectedFn selectedVersion
  whenJust systemInstall $ \systemVersion => do
    putStrLn $ (if isSystemSelected then "* " else "  ") ++ "system (installed @ v\{systemVersion})"
  traverse_ putStrLn $ printVersion . selectedInstalled <$> zipMatch installedVersions remoteVersions
    where
      printVersion : (Bool, Maybe Version, Maybe Version) -> String
      printVersion (sel, Just v, Just _)  = (if sel then "* " else "  ") ++ "\{v}  (installed)"
      printVersion (_, Nothing, Just v) = "  " ++ show v
      printVersion (sel, Just v, Nothing) = (if sel then "* " else "  ") ++ "\{v}  (local only)"
      printVersion (_, Nothing, Nothing) = ""

      buildSelectedFn : (selectedVersion : Maybe Version)
                     -> (Maybe Version, Maybe Version)
                     -> (Bool, Maybe Version, Maybe Version)
      buildSelectedFn selectedVersion (l, r) = (l == selectedVersion, l, r)

export
installCommand : HasIO io => (version : Version) -> (cleanAfter : Bool) -> io ()
installCommand version cleanAfter = do
  createVersionsDir version
  buildAndInstall version cleanAfter

export
uninstallCommand : HasIO io => (version : Version) -> io ()
uninstallCommand version =
  case !(isInstalled version) of
       Left err    => exitError err
       Right False => exitError "Version \{version} is not installed."
       Right True  =>
         when !(confirm "Are you sure you want to uninstall version \{version}?") $ do
           uninstall version
           exitSuccess "Uninstalled version \{version}."

export
selectCommand : HasIO io => (version : Version) -> io ()
selectCommand version = do
  Right () <- selectVersion version
    | Left err => exitError err
  exitSuccess "Idris 2 version \{version} selected."

selectSystem : HasIO io => io (Either String ())
selectSystem = do
  Right () <- unselect
    | Left err => pure $ Left err
  let proposedIdrisSymlinked = idrisSymlinkedPath
  Just installedIdris <- systemIdrisPath
    | Nothing => pure $ Left "Could not find system install of Idris 2. You might have to run this command with the IDRIS2 environment variable set to the location of the idris2 binary because it is not located at \{defaultIdris2Location}."
  Just linkedIdris <- pathExpansion proposedIdrisSymlinked
    | Nothing => pure $ Left "Could not resolve symlinked location: \{proposedIdrisSymlinked}."
  True <- symlink installedIdris linkedIdris
    | False => pure $ Left "Failed to create symlink for Idris 2 system install."
  case !systemIdrisLspPath of
       Nothing => pure $ Right ()
       Just installedLsp => do
          let proposedLspSymlinked = idrisLspSymlinkedPath
          Just linkedLsp <- pathExpansion proposedLspSymlinked
            | Nothing => pure $ Left "Could not resolve symlinked LSP location: \{proposedLspSymlinked}."
          True <- symlink installedLsp linkedLsp
            | False => pure $ Left "Failed to create symlink for Idris 2 LSP system install."
          pure $ Right ()

export
selectSystemCommand : HasIO io => io ()
selectSystemCommand = do
  Right () <- selectSystem
    | Left err => exitError err
  exitSuccess "System copy of Idris 2 selected."

||| Select the given version and print messages to the effect of
||| failing to switch _back_ to that version if unsuccessful.
switchBack : HasIO io => (actionMsg : String) -> (prevVersion : Version) -> io (Either String ())
switchBack actionMsg prevVersion = do
  Right True <- isInstalled prevVersion
    | Right False => selectSystem
    | Left err    => pure $ Left err
  Right () <- selectVersion prevVersion
    | Left err => pure $ Left "Successfully \{actionMsg} but failed to switch back to Idris version \{prevVersion} with error: \{err}"
  pure $ Right ()

||| Install the Idris 2 API (and the related version of Idris, if needed).
export
installAPICommand : HasIO io => (version : Version) -> io ()
installAPICommand version = do
  selectedVersion <- getSelectedVersion
  -- we won't reinstall Idris 2 if not needed:
  unless !(selectAndCheckout version) $ do
    installCommand version False
    Right () <- selectVersion version
      | Left err => exitError err
    pure ()
  Just _ <- inDir (relativeCheckoutPath Idris) (installApi version)
    | Nothing => exitError "Failed to switch to checkout branch and install Idris 2 API."
  -- if we know we used to have a different version of Idris selected, switch back.
  whenJust selectedVersion $ \prevVersion =>
    case !(switchBack "installed Idris 2 API version \{version} package" prevVersion) of
         Right () => pure ()
         Left err => exitError err

||| Install the Idris 2 LSP (and the related version of Idris, if needed).
export
installLSPCommand : HasIO io => (version : Version) -> io ()
installLSPCommand version = do
  when (version < (V 0 4 0 Nothing "")) $
    exitError "The Idris 2 LSP is not supported prior to Idris 2 v0.4.0."
  selectedVersion <- getSelectedVersion
  -- don't reinstall Idris 2 and its API unless needed:
  unless !selectIdrisWithAPI $ do
    installAPICommand version
    Right () <- selectVersion version
      | Left err => exitError err
    pure ()
  buildAndInstallLsp version
  whenJust selectedVersion $ \prevVersion =>
    case !(switchBack "installed Idris 2 LSP for version \{version}" prevVersion) of
         Right () => pure ()
         Left err => exitError err

  where
    ||| Select the requested Idris version and verify it has
    ||| the API installed.
    selectIdrisWithAPI : io Bool
    selectIdrisWithAPI = do
      Right () <- selectVersion version
        | _ => do putStrLn "Idris 2 version \{version} will be installed prior to installing the LSP server."
                  pure False
      case !(hasApiInstalled version) of
           Right True => pure True
           _ => do putStrLn "The Idris 2 API for version \{version} will be installed prior to installing the LSP server."
                   pure False

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 13, section 2

import Data.Vect

-- check that all functions are total
%default total

data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd () height (S height)
  Pop : StackCmd Integer (S height) height
  Top : StackCmd Integer (S height) (S height)
  GetStr : StackCmd String height height
  PutStr : String -> StackCmd () height height
  Pure : ty -> StackCmd ty s s
  (>>=) : StackCmd a s1 s2 ->
          (a -> StackCmd b s2 s3) ->
          StackCmd b s1 s3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight ->
           IO (ty, Vect outHeight Integer)
runStack stk (Push x) = pure ((), x :: stk)
runStack (x :: xs) Pop = pure (x, xs)
runStack (x :: xs) Top = pure (x, x :: xs)
runStack stk (Pure x) = pure (x, stk)
runStack stk (x >>= f) = do (res, stk') <- runStack stk x
                            runStack stk' (f res)
runStack stk GetStr = do val <- getLine
                         pure (val, stk)
runStack stk (PutStr val) = do putStr val
                               pure ((), stk)

doBinOp : (Integer -> Integer -> Integer) -> StackCmd () (S (S height)) (S height)
doBinOp op = do val1 <- Pop
                val2 <- Pop
                Push $ op val1 val2

doNegate : StackCmd () (S height) (S height)
doNegate = do val <- Pop
              Push $ -val

doDiscard : StackCmd () (S height) (height)
doDiscard = do val <- Pop
               Pure ()

doDuplicate : StackCmd () (S height) (S (S height))
doDuplicate = do val <- Top
                 Push val

data StackIO : Nat -> Type where
  Do : StackCmd a h1 h2 ->
       (a -> Inf (StackIO h2)) -> StackIO h1

namespace StackDo
  (>>=) : StackCmd a h1 h2 ->
          (a -> Inf (StackIO h2)) -> StackIO h1
  (>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> Vect h Integer -> StackIO h -> IO ()
run (More fuel) stk (Do c f)
  = do (res, stk') <- runStack stk c
       run fuel stk' (f res)
run Dry stk p = pure ()

data StkInput = Number Integer
              | Add
              | Subtract
              | Multiply
              | Negate
              | Discard
              | Duplicate

strToInput : String -> Maybe StkInput
strToInput "" = Nothing
strToInput "add" = Just Add
strToInput "subtract" = Just Subtract
strToInput "multiply" = Just Multiply
strToInput "negate" = Just Negate
strToInput "discard" = Just Discard
strToInput "duplicate" = Just Duplicate
strToInput x = if all isDigit (unpack x)
                then Just (Number (cast x))
                else Nothing

mutual
  tryBinOp : (op : Integer -> Integer -> Integer) -> StackIO h
  tryBinOp {h = (S (S k))} op
    = do (doBinOp op)
         result <- Top
         PutStr (show result ++ "\n")
         stackCalc
  tryBinOp _
    = do PutStr "Fewer than two items on the stack\n"
         stackCalc

  tryNegate : StackIO h
  tryNegate {h = (S k)}
   = do doNegate
        result <- Top
        PutStr (show result ++ "\n")
        stackCalc
  tryNegate
   = do PutStr "Fewer than one item on the stack\n"
        stackCalc

  tryDiscard : StackIO h
  tryDiscard {h = (S k)}
   = do result <- Top
        doDiscard
        PutStr ("Discarded " ++ show result ++ "\n")
        stackCalc
  tryDiscard
   = do PutStr "Fewer than one item on the stack\n"
        stackCalc

  tryDuplicate : StackIO h
  tryDuplicate {h = (S k)}
   = do doDuplicate
        result <- Top
        PutStr ("Duplicated " ++ show result ++ "\n")
        stackCalc
  tryDuplicate
   = do PutStr "Fewer than one item on the stack\n"
        stackCalc

  stackCalc : StackIO h
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                   Nothing => do PutStr "Invalid input\n"
                                 stackCalc
                   Just (Number x) => do Push x
                                         stackCalc
                   Just Add => tryBinOp (+)
                   Just Subtract => tryBinOp (flip (-))
                   Just Multiply => tryBinOp (*)
                   Just Negate => tryNegate
                   Just Discard => tryDiscard
                   Just Duplicate => tryDuplicate

partial
main : IO ()
main = run forever [] stackCalc

ext: idr

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Main

import HTML
import VNode
import Render
import Attributes

Model : Type
Model = Integer

%foreign "browser:lambda: (node, func) => node.onclick = func"
prim__onClick : AnyPtr -> (IO ()) -> PrimIO AnyPtr

initModel : Model
initModel = 0

view : Model -> DOM V
view count =
  div [] [
    h1 [] [text "Count"]
    , span [] [text count]
    , button [Id "inc", Class ["test", "foobar"]] [text "+"]
  ]

update : Model -> IO ()
update model = do
  root <- getRoot "idris-root"
  let model = model + 1
  let html = view model
  live <- render root html
  button <- getRoot "inc"
  _ <- primIO $ prim__onClick button (update model)
  pure ()

main : IO ()
main = do
  update (-1)

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
infix 5 ^

(^) : Nat -> %static Nat -> Nat
(^) x Z = 1
(^) x (S k) = mult x (x ^ k)

powFn : Nat -> Nat
powFn x = (x ^ 2) + 1

calc : Int -> Int
calc x = (x * x) + x

myMap : %static (a -> b) -> List a -> List b
myMap f [] = []
myMap f (x :: xs) = f x :: myMap f xs

doubleAll : List Int -> List Int
doubleAll xs = myMap (* 2) xs


text:
module Extra.String

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Extra.List
import Extra.Op

public export
join : String -> List String -> String
join joiner strs =
  foldl (++) "" (Data.List.intersperse joiner strs)

export
findAll : String -> String -> List Nat
findAll str lookup =
  findAll (unpack str) (unpack lookup)

export
replace : String -> String -> String -> String
replace k v str =
  pack (Extra.List.replace (unpack str) (unpack k) (unpack v))

export
wrap : String -> String -> String
wrap sym str =
  sym ++ str ++ sym

export
filter : (Char -> Bool) -> String -> String
filter test =
  pack . filter test . unpack

export
showList : (a -> String) -> List a -> String
showList f els =
  "[" ++ (join "," (map f els)) ++ "]"

export
listOp : (List Char -> List Char) -> String -> String
listOp op =
  pack . op . unpack

export
split : Char -> String -> List String
split c =
  ( map pack ) . Data.List1.forget . (Data.List.split (== c)) . unpack

export
includesAny : String -> String -> Bool
includesAny search =
  let
    searchChars = unpack search
  in
     any (\c => c `elem` searchChars) . unpack

export
quote : String -> String
quote =
  (wrap "\"")
  . (replace "\n" "\\n")
  . (replace "\"" "\\\"")

export
unquote : String -> String
unquote =
  (replace "\\n" "\n") .
  (listOp (reverse . drop 1 . reverse . drop 1))

export
limit : Nat -> String -> String
limit len str =
  if length str > len then
    (strSubstr 0 (cast len) str) ++ "..."
  else
    str

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Commons.Test.Unit.Lexer

import Text.PrettyPrint.WL

import Text.Lexer

%default total
%access export

data TestReport : Type -> Type where
  ExpectedSuccess : (title : String) -> TestReport a

  Failure : (Eq a, Show a)
         => (title : String)
         -> (input : String)
         -> (lexed : List (TokenData a))
         -> (left  : String)
         -> TestReport a

  FailureCmp : (Eq a, Show a)
            => (title, input : String)
            -> (given, expected : List (TokenData a))
            -> TestReport a

isSuccess : TestReport a -> Bool
isSuccess (ExpectedSuccess _) = True
isSuccess _ = False

data LexResult a = Empty Int Int String
                 | Success (List (TokenData a)) Int Int
                 | Extra   (List (TokenData a)) Int Int String

lexFunc : {a : Type}
       -> (Eq a, Show a)
       => (String -> Pair (List (TokenData a)) (Int, Int, String))
       -> String
       -> LexResult a
lexFunc l i = case l i of
                (Nil, (l,c,str)) => Empty l c str
                (ts , (l,c,""))  => Success ts l c
                (ts , (l,c,str)) => Extra ts l c str

lexerTest : (Eq a, Show a)
         => (title : String)
         -> (lex   : String -> Pair (List (TokenData a)) (Int, Int, String))
         -> (input : String)
         -> TestReport a
lexerTest t l i {a} =
  case lexFunc {a=a} l i of
    Empty _ _ str => Failure t i Nil str
    Success ts _ _ => ExpectedSuccess t
    Extra ts _ _ str => Failure t i ts str

lexerTestNot : (Eq a, Show a)
            => (title : String)
            -> (lex   : String -> Pair (List (TokenData a)) (Int, Int, String))
            -> (input : String)
            -> TestReport a
lexerTestNot t l i =
  case lexFunc l i of
    Success ts _ _ => Failure t i ts ""
    Extra ts _ _ str => Failure t i ts str
    Empty _ _ str => ExpectedSuccess t

lexerTestAssert : (Eq a, Show a)
            => (title : String)
            -> (lex   : String -> Pair (List (TokenData a)) (Int, Int, String))
            -> (input : String)
            -> (expected : List (TokenData a))
            -> TestReport a
lexerTestAssert t l i e =
  case lexFunc l i of
    Success ts _ _ =>
      if map tok ts == map tok e
        then ExpectedSuccess t
        else FailureCmp t i ts e

    Empty _ _ str => Failure t i Nil str
    Extra ts _ _ str => Failure t i ts str

showReport : Show a => TestReport a -> Doc
showReport (ExpectedSuccess t) = text "[PASS]" <+> text t
showReport (Failure t i sofar left) =
  vcat [ text "[FAIL]" <+> text t
       , indent 2 $ text "So far I lexed:"
       , indent 4 $ list (map (text . show . tok) sofar)
       , indent 2 $ text "This was left:"
       , indent 4 $ text left]
showReport (FailureCmp t i g e) =
  vcat [ text "[FAIL]" <+> text t
       , indent 2 $ text "Expected to lex:"
       , indent 4 $ list (map (text . show . tok) e)
       , indent 2 $ text "But gave this:"
       , indent 4 $ list (map (text . show . tok) g)]

runLexTest : Show a => TestReport a -> IO Bool
runLexTest r = do putStrLn ((toString . showReport) r)
                  pure (isSuccess r)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
||| Sets and display version of Idris.
module Idris.Version

import IdrisPaths
import public Libraries.Data.Version

%default total

export
version : Version
version with (idrisVersion)
 version | (s,"") = MkVersion s Nothing
 version | (s,t) = MkVersion s (Just t)


text:
module Main

import Data.String

-- Test, that Scheme-dependent builtins are correctly blacklisted/overridden

main : IO ()
main = do
  putStrLn $ fastPack ['a', 'b', 'c']
  putStrLn $ fastAppend ["first part", "|", "", "|", "END of the string"]
  putStrLn $ fastConcat ["last", "part", "empty", ""]

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Web.Internal.UrlPrim

import JS
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace URL

  export
  %foreign "browser:lambda:(a,b)=> new URL(a,b)"
  prim__new : String -> UndefOr String -> PrimIO URL

  export
  %foreign "browser:lambda:(a)=>URL.createObjectURL(a)"
  prim__createObjectURL : Union2 Blob MediaSource -> PrimIO String

  export
  %foreign "browser:lambda:(a)=>URL.createObjectURL(a)"
  prim__createObjectURL1 : MediaSource -> PrimIO String

  export
  %foreign "browser:lambda:(a)=>URL.revokeObjectURL(a)"
  prim__revokeObjectURL : String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.hash"
  prim__hash : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.hash = v}"
  prim__setHash : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.host"
  prim__host : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.host = v}"
  prim__setHost : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.hostname"
  prim__hostname : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.hostname = v}"
  prim__setHostname : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.href"
  prim__href : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.href = v}"
  prim__setHref : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.origin"
  prim__origin : URL -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.password"
  prim__password : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.password = v}"
  prim__setPassword : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.pathname"
  prim__pathname : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.pathname = v}"
  prim__setPathname : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.port"
  prim__port : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.port = v}"
  prim__setPort : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.protocol"
  prim__protocol : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.protocol = v}"
  prim__setProtocol : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.search"
  prim__search : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.search = v}"
  prim__setSearch : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.searchParams"
  prim__searchParams : URL -> PrimIO URLSearchParams

  export
  %foreign "browser:lambda:x=>x.username"
  prim__username : URL -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.username = v}"
  prim__setUsername : URL -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : URL -> PrimIO String

namespace URLSearchParams

  export
  %foreign "browser:lambda:(a)=> new URLSearchParams(a)"
  prim__new :  UndefOr (Union3 (Array (Array String))
                               (Record String String)
                               String)
            -> PrimIO URLSearchParams

  export
  %foreign "browser:lambda:(x,a,b)=>x.append(a,b)"
  prim__append : URLSearchParams -> String -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.delete(a)"
  prim__delete : URLSearchParams -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getAll(a)"
  prim__getAll : URLSearchParams -> String -> PrimIO (Array String)

  export
  %foreign "browser:lambda:(x,a)=>x.get(a)"
  prim__get : URLSearchParams -> String -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:(x,a)=>x.has(a)"
  prim__has : URLSearchParams -> String -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a,b)=>x.set(a,b)"
  prim__set : URLSearchParams -> String -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sort()"
  prim__sort : URLSearchParams -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.toString()"
  prim__toString : URLSearchParams -> PrimIO String


text:
module Libra.Parser

import Libra.Constants
import Libra.Data

import public Control.Monad.Identity

import public Lightyear
import Lightyear.Char
import Lightyear.Strings

%access export
%default partial

{-
  Parse Combinators
-}

parseName : Parser SExpr
parseName = lexeme (letter >>= \x => commitTo $ do {
                xs <- many alphaNum
                let name = pack (x :: xs)
                pure (MkName name)
            })

parseExpr : Parser SExpr
parseExpr = parseName <|>| ( MkSExpr <$> parens (many parseExpr) )

out : Identity (Result str SExpr) -> Either (List (str, String)) SExpr
out (Id (Failure xs)) = Left xs
out (Id (Success x y)) = Right y

max_stars_repo_name: ostera/libra

max_issues_repo_name: ostera/libra

max_forks_repo_name: ostera/libra


text:
module Examples.ConferenceManager

import DepSec.DIO
import DepSec.Labeled
import DepSec.Ref

import Examples.ConferenceLattice

%default total

-- Examples derived from "Luísa Lourenço and Luís Caires. 2015.
-- Dependent Information Flow Types (POPL '15)"

--------------------------------------------------------------------------------
-- Types
--------------------------------------------------------------------------------
record User where
  constructor MkUser
  uid   : Uid
  name  : Labeled (U uid) String
  univ  : Labeled (U uid) String
  email : Labeled (U uid) String

record Submission where
  constructor MkSubmission
  uid   : Uid
  sid   : Sid
  title : Labeled (A uid sid) String
  abs   : Labeled (A uid sid) String
  paper : Labeled (A uid sid) String

record Review where
  constructor MkReview
  uid     : Uid
  sid     : Sid
  PC_only : Labeled (PC uid sid) String
  review  : Labeled (A Top sid) String
  grade   : Labeled (A Top sid) Integer

Bot' : Compartment
Bot' = Bottom

Users : Type
Users = SecRef Bot' (List (SecRef Bot' User))

Submissions : Type
Submissions = SecRef Bot' (List (SecRef Bot' Submission))

Reviews : Type
Reviews = SecRef Bot' (List (SecRef Bot' Review))

--------------------------------------------------------------------------------
-- Hints
--------------------------------------------------------------------------------
%hint
botFlowsToBot : Bot' `leq` Bot'
botFlowsToBot = reflexive Bot'

implicit
stringToLabeled : Poset labelType => {l : labelType} -> String -> Labeled l String
stringToLabeled = label

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

-- Example 2.1
assignReviewer : Reviews -> Uid -> Sid -> DIO Bot' ()
assignReviewer revRef uid1 sid1 =
  do reviews <- unlabel !(readRef revRef)
     new <- (newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label (MkReview uid1 sid1 "" "" (label 0))))
     let newreviews = label (new :: reviews)
     writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} revRef newreviews

-- Example 2.2
viewAuthorPapers : Submissions
                -> (uid1 : Uid)
                -> DIO Bot' (List (sub : Submission ** uid1 = (uid sub)))
viewAuthorPapers subRef uid1 =
  do submissions <- unlabel !(readRef subRef)
     findPapers submissions
  where
    findPapers : (List (SecRef Bot' Submission))
              -> DIO Bot' (List (sub : Submission ** uid1 = (uid sub)))
    findPapers [] = pure []
    findPapers (x :: xs) =
      do sub <- unlabel !(readRef x)
         case decEq (uid sub) uid1 of
           (Yes prf) => pure $ (sub ** (sym prf)) :: !(findPapers xs)
           (No _) => findPapers xs

-- Example 2.3
viewAssignedPapers : Reviews -> Submissions -> Uid -> DIO Bot' (List (SecRef Bot' Submission))
viewAssignedPapers reviewsRef subsRef id =
  do reviews <- unlabel !(readRef reviewsRef)
     subs <- unlabel !(readRef subsRef)
     sids <- getSids reviews
     findPapers sids subs
  where
  getSids : List (SecRef (U Bot) Review) -> DIO Bot' $ List Sid
  getSids [] = pure []
  getSids (x :: xs) =
    do rev <- unlabel !(readRef x)
       case decEq (uid rev) id of
         (Yes _) => pure $ (sid rev) :: !(getSids xs)
         (No _) => getSids xs

  findPapers : List Sid -> List (SecRef Bot' Submission) -> DIO Bot' (List (SecRef Bot' Submission))
  findPapers xs [] = pure []
  findPapers xs (x :: ys) =
    do sub <- unlabel !(readRef x)
       case elemBy (==) (sid sub) xs of
         True => pure $ x :: !(findPapers xs ys)
         False => findPapers xs ys

-- Example 2.4
emphasizeTitle : Uid -> Sid -> Submissions -> DIO Bot' ()
emphasizeTitle uid1 sid1 subsRef =
  do subs <- unlabel !(readRef subsRef)
     ltitle <- getTitleOfSub subs
     lNewTitle <- appendToTitle "!" ltitle
     searchAndReplaceTitle lNewTitle subs
     pure ()
  where
  searchAndReplaceTitle : Labeled (A uid1 sid1) String -> List (SecRef Bot' Submission) -> DIO Bot' ()
  searchAndReplaceTitle newTitle [] = pure ()
  searchAndReplaceTitle newTitle (x :: xs) =
    do sub <- unlabel !(readRef x)
       case (decEq (uid sub) uid1, decEq (sid sub) sid1) of
         (Yes prf1, Yes prf2) =>
           let abs'= abs sub
               paper' = paper sub
               title' : Labeled (A (uid sub) (sid sub)) String =
                 rewrite prf1 in
                 rewrite prf2 in
                 newTitle
               newSub = MkSubmission (uid sub) (sid sub) title' abs' paper'
               newlsub : Labeled Bot' Submission = label newSub
           in writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} x newlsub
         (_ , _ ) => searchAndReplaceTitle newTitle xs

  getTitleOfSub : List (SecRef Bot' Submission) -> DIO Bot' (Labeled (A uid1 sid1) String)
  getTitleOfSub [] = pure ""
  getTitleOfSub (x :: xs) =
    do sub <- unlabel !(readRef x)
       case (decEq (uid sub) uid1, decEq (sid sub) sid1) of
         (Yes prf1, Yes prf2) =>
           rewrite sym $ prf1 in
           rewrite sym $ prf2 in
           pure $ title sub
         (_,_) => getTitleOfSub xs

  appendToTitle : String -> Labeled (A x y) String -> DIO Bot' (Labeled (A x y) String)
  appendToTitle {x} {y} str lstr =
    do let oldStrDIO : DIO (A x y) String = unlabel {flow = reflexive (A x y)} lstr
       let newStrDIO : DIO (A x y) String = do pure $ (!oldStrDIO ++ str)
       plug newStrDIO

-- Example 2.5
addCommentSubmission : Reviews
                    -> (uid1 : Uid)
                    -> (sid1 : Sid)
                    -> (comment : Labeled (A uid1 sid1) String)
                    -> DIO Bot' ()
addCommentSubmission revsRef uid1 sid1 comment =
  do revs <- unlabel !(readRef revsRef)
     addComment revs
  where
  addComment : List (SecRef (U Bot) Review) -> DIO Bot' ()
  addComment [] = pure ()
  addComment (x :: xs) =
    do rev <- unlabel !(readRef x)
       case (decEq (uid rev) uid1, decEq (sid rev) sid1) of
         (Yes prf1, Yes prf2) =>
           let review' = review rev
               grade' = grade rev
               PC_only' : Labeled (PC (uid rev) (sid rev)) String =
                 rewrite prf1 in
                 rewrite prf2 in relabel {flow=A_leq_PC {uid1}} comment
               newRev = MkReview (uid rev) (sid rev) PC_only' review' grade'
               newlRev : Labeled Bot' Review = label newRev
           in writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} x newlRev
         _ => addComment xs

--------------------------------------------------------------------------------
-- Test data
--------------------------------------------------------------------------------

User1 : User
User1 = MkUser (Nat 1) "Alice" "Foo University" "alice@cs.foo.dk"

User2 : User
User2 = MkUser (Nat 2) "Bob" "Bar University" "bob@cs.bar.dk"

User3 : User
User3 = MkUser (Nat 3) "Chuck" "Baz University" "chuck@cs.baz.dk"

Paper1 : Submission
Paper1 = MkSubmission (Nat 1) (Nat 1) "IFC in Idris" "Dependent types seems good?" "QED"

Paper2 : Submission
Paper2 = MkSubmission (Nat 2) (Nat 2) "Haskell is old fashioned" "Why not more Idris?" "QED"

Paper3 : Submission
Paper3 = MkSubmission (Nat 1) (Nat 3) "Messing with Idris" "Idris is fun!" "QED"

Review1 : Review
Review1 = MkReview (Nat 3) (Nat 1) "Pretty good" "That's okay" (label 12)

Review2 : Review
Review2 = MkReview (Nat 3) (Nat 2) "Yay!" "OK!" (label 12)

initUsers : DIO Bot' Users
initUsers = newRef {flow=reflexive Bot'} {flow'=reflexive Bot'} (label Nil)

initSubmissions : DIO Bot' Submissions
initSubmissions = newRef (label Nil)

initReviews : DIO Bot' Reviews
initReviews = newRef {flow=reflexive Bot'} {flow'=reflexive Bot'} (label Nil)

dummyDB : Users -> Submissions -> Reviews -> DIO Bot' ()
dummyDB users submissions reviews=
  do user1 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label User1)
     user2 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label User2)
     let newusers = label {l=Bot'} [user1, user2]
     writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} users newusers

     sub1 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label Paper1)
     sub2 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label Paper2)
     sub3 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label Paper3)
     let newsubmissions = label {l=Bot'} [sub1, sub2, sub3]
     writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} submissions newsubmissions

     rev1 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label Review1)
     rev2 <- newRef {l = Bot'} {l' = Bot'} {l'' = Bot'} (label Review2)
     let newreviews = label {l=Bot'} [rev1, rev2]
     writeRef {l = Bot'} {l' = Bot'} {l'' = Bot'} reviews newreviews

--------------------------------------------------------------------------------
-- Main
--------------------------------------------------------------------------------
main : IO ()
main =
  do putStrLn "Starting conference manager ..."
     run $
       do users <- initUsers
          submissions <- initSubmissions
          reviews <- initReviews
          dummyDB users submissions reviews

          assignReviewer reviews (Nat 42) (Nat 1)
          addCommentSubmission reviews (Nat 2) (Nat 2) "Cool paper!"

          reviews' <- unlabel !(readRef reviews)
          lift $ putStrLn $ "No. of reviews: " ++ (cast $ length reviews')

          alice <- viewAuthorPapers submissions (Nat 1)
          lift $ putStrLn $ "No. of submissions from Alice: " ++ (cast $ length alice)

          papersToReview <- viewAssignedPapers reviews submissions (Nat 3)
          lift $ putStrLn $ "No. of papers to review Chuck: " ++ (cast $ length papersToReview)

          pure ()
     putStrLn "Shutting down conference manager ..."

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module ProofColDivSeqPostulate

import ProofColDivSeqBase

%default total
%access export

--            from ProofColDivSeqBase
-- ########################################
-- ########################################

--            from ProofColDivSeqMain
-- ########################################
-- ########################################

--            from sub0xxxxx
-- ########################################
-- ########################################


text:
module Compiler.Erlang.Erlang

import Compiler.Common
import Compiler.CompileExpr

import Compiler.Erlang.GlobalOpts
import Compiler.Erlang.ModuleOpts
import Compiler.Erlang.Cmd
import Compiler.Erlang.Name
import Compiler.Erlang.Codegen.NamedCExpToErlExpr
import Compiler.Erlang.Codegen.NamedCExpToErlExpr.RtsSupport
import Compiler.Erlang.Codegen.ErlExprToAbstractFormat
import Compiler.Erlang.Codegen.AbstractFormatToErlangSource
import Compiler.Erlang.Codegen.AbstractFormatToPrimTerm
import Compiler.Erlang.Utils.CompositeString

import Core.Context
import Core.Directory
import Core.Name
import Core.Options
import Core.TT

import Data.NameMap
import Data.List
import Data.SortedMap
import Data.Strings
import Utils.Binary
import Utils.Path
import System
import System.File

%default covering
%hide ErlExpr.Line

findErlangExecutable : IO String
findErlangExecutable = pure "erl"

findErlangCompiler : IO String
findErlangCompiler = pure "erlc"

-- TODO: Ideally, line numbers should be retrieved from the NamedCExp, and not
-- use a default placeholder line number.
defLine : Line
defLine = 4242

groupBy : Ord key => (a -> key) -> (a -> value) -> List a -> SortedMap key (List value)
groupBy _ _ [] = empty
groupBy toKey toValue (x :: xs) = singleton (toKey x) [toValue x] <+> (groupBy toKey toValue xs)

defsPerModule : List (NamespaceInfo, a) -> List (NamespaceInfo, List a)
defsPerModule defs = SortedMap.toList $ groupBy fst snd defs

getExportFunNames : List ModuleOpts -> List (Namespace, Name)
getExportFunNames allModuleOpts = mapMaybe (\mod => (\funName => (mod.ns, funName)) <$> mod.exportFunName) allModuleOpts

getCompileExpr : {auto c : Ref Ctxt Defs} -> Name -> Core NamedDef
getCompileExpr name = do
  defs <- get Ctxt
  Just globalDef <- lookupCtxtExact name (gamma defs)
    | Nothing => throw (InternalError ("Compiling undefined name " ++ show name))
  let Just expr = namedcompexpr globalDef
    | Nothing => throw (InternalError ("No compiled definition for " ++ show name))
  pure expr

genExports : {auto c : Ref Ctxt Defs} -> NamespaceInfo -> Line -> Name -> Core (List ErlFunDecl)
genExports namespaceInfo l name = do
  MkNmFun [] expr <- getCompileExpr name
    | _ => throw (InternalError ("Expected function definition for " ++ show name))
  readExports namespaceInfo l expr

genDeclAbstr : Decl -> CompositeString
genDeclAbstr d =
  Nested [primTermToCS (AbstractFormatToPrimTerm.genDecl d), Str ".\n"]

genDeclErl : Decl -> CompositeString
genDeclErl d =
  Nested [AbstractFormatToErlangSource.genDecl d, Str "\n"]

writeErlangModule : {auto c : Ref Ctxt Defs} -> GlobalOpts -> List ModuleOpts -> (outputDir : String) -> (extension : String) -> (declToCS : Decl -> CompositeString) -> (NamespaceInfo, List ErlFunDecl) -> Core String
writeErlangModule globalOpts allModuleOpts outputDir extension declToCS (namespaceInfo, funDecls) = do
  let currentModuleOpts = case outputBundle namespaceInfo of
        Concat _ => Nothing
        Split _ inNS => find ((== inNS) . ns) allModuleOpts
  exportFunDecls <- maybe (pure []) (genExports namespaceInfo defLine) (currentModuleOpts >>= exportFunName)
  let modName = currentModuleName namespaceInfo
  let moduleInlineSize = currentModuleOpts >>= inlineSize
  let inlineAttrs = if fromMaybe (inlineSize globalOpts) moduleInlineSize > 0
        then [Inline defLine, InlineSize defLine (inlineSize globalOpts)]
        else []
  let module_ = MkModule (MkModuleName defLine modName) (NoAutoImport defLine :: inlineAttrs) (exportFunDecls ++ funDecls)
  let outfile = outputDir </> modName ++ "." ++ extension
  let decls = genErlModule defLine module_
  let content = fastAppend (flatten (Nested (map declToCS decls)))
  Right () <- coreLift $ writeFile outfile content
    | Left err => throw (FileErr outfile err)
  pure outfile

genCompdef : Line -> (NamespaceInfo, (Name, FC, NamedDef)) -> Core (Maybe (NamespaceInfo, ErlFunDecl))
genCompdef l (namespaceInfo, (name, fc, def)) = do
  Just funDecl <- genDef namespaceInfo l name def
    | Nothing => pure Nothing
  pure $ Just (namespaceInfo, funDecl)

concatNamespaceInfo : (ns : String) -> a -> (NamespaceInfo, a)
concatNamespaceInfo ns x =
  (MkNamespaceInfo (Concat ns), x)

splitNamespaceInfo : (prefixStr : String) -> (Name, a) -> (NamespaceInfo, (Name, a))
splitNamespaceInfo prefixStr x@(name, _) =
  let ns = getNamespace name
  in (MkNamespaceInfo (Split prefixStr ns), x)

namespaceInfoToModuleNamePath : (outputDir : String) -> (extension : String) -> NamespaceInfo -> (String, String)
namespaceInfoToModuleNamePath outputDir extension namespaceInfo =
  let modName = currentModuleName namespaceInfo
  in (modName, outputDir </> modName ++ "." ++ extension)

compileMainEntrypointToModules : {auto c : Ref Ctxt Defs} -> GlobalOpts -> ClosedTerm -> (modName : String) -> Core (List (NamespaceInfo, List ErlFunDecl))
compileMainEntrypointToModules globalOpts tm modName = do
  compileData <- getCompileData Cases tm
  compdefs <- traverse (genCompdef defLine . concatNamespaceInfo modName) (namedDefs compileData)
  let namespaceInfo = MkNamespaceInfo (Concat modName)
  lv <- newRef LV (initLocalVars "V")
  mainBody <- genNmExp namespaceInfo empty (forget (mainExpr compileData))
  argsVar <- newLocalVar
  let erlMainFunDecl = MkFunDecl defLine Public "start" [] !(genErlMain defLine mainBody)
  let escriptMainFunDecl = MkFunDecl defLine Public "main" [argsVar] (genEscriptMain defLine mainBody)
  let validCompdefs = (namespaceInfo, erlMainFunDecl) :: (namespaceInfo, escriptMainFunDecl) :: mapMaybe id compdefs
  pure $ defsPerModule validCompdefs

compileLibraryToModules : {auto c : Ref Ctxt Defs} -> GlobalOpts -> List ModuleOpts -> (changedModules : Maybe (List ModuleIdent)) -> Core (List (NamespaceInfo, List ErlFunDecl))
compileLibraryToModules globalOpts allModuleOpts changedModules = do
  let extraNames = filter (shouldCompileName changedModules) (map snd (getExportFunNames allModuleOpts))
  compileData <- getExportedCompileData Cases (shouldCompileName changedModules) extraNames
  compdefs <- traverse (genCompdef defLine . splitNamespaceInfo (prefixStr globalOpts)) (filter (shouldCompileName changedModules . fst) (namedDefs compileData))
  let validCompdefs = mapMaybe id compdefs
  pure $ defsPerModule validCompdefs
    where
      shouldCompileName : Maybe (List ModuleIdent) -> Name -> Bool
      shouldCompileName Nothing _ = True
      shouldCompileName (Just modulesToCompile) n =
        let namespaces = map miAsNamespace modulesToCompile
        in any (`isParentOf` getNamespace n) namespaces

build : {auto c : Ref Ctxt Defs} -> GlobalOpts -> List ModuleOpts -> (tmpDir : String) -> (outputDir : String) -> (modules : List (NamespaceInfo, List ErlFunDecl)) -> Core (List String)
build globalOpts allModuleOpts tmpDir outputDir modules = do
  erl <- coreLift findErlangExecutable
  erlc <- coreLift findErlangCompiler
  case outputFormat globalOpts of
    ErlangSource => do
      traverse_ (writeErlangModule globalOpts allModuleOpts outputDir "erl" genDeclErl) modules
    ErlangSourcePretty => do
      generatedFiles <- traverse (writeErlangModule globalOpts allModuleOpts tmpDir "abstr" genDeclAbstr) modules
      coreLift $ system $ compileAbstrToErlCmd False erl generatedFiles outputDir
      pure ()
    AbstractFormat => do
      traverse_ (writeErlangModule globalOpts allModuleOpts outputDir "abstr" genDeclAbstr) modules
    BeamFromErlangSource => do
      generatedFiles <- traverse (writeErlangModule globalOpts allModuleOpts tmpDir "erl" genDeclErl) modules
      coreLift $ system $ compileErlToBeamCmd erlc generatedFiles outputDir
      pure ()
    BeamFromAbstractFormat => do
      generatedFiles <- traverse (writeErlangModule globalOpts allModuleOpts tmpDir "abstr" genDeclAbstr) modules
      coreLift $ system $ compileAbstrToBeamCmd erl generatedFiles outputDir
      pure ()
  pure $ map (currentModuleName . fst) modules

-- CODEGEN

compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile = do
  ds <- getDirectives (Other "erlang")
  let groupedDirectives = groupBy fst snd ds
  let globalDirectives = fromMaybe [] (lookup emptyNS groupedDirectives) -- TODO: Fix emptyNS
  let globalOpts = parseOpts globalDirectives
  let modName = outfile
  modules <- compileMainEntrypointToModules globalOpts tm modName
  build globalOpts [] tmpDir outputDir modules
  pure (Just outfile)

executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm = do
  let globalOpts = defaultGlobalOpts
  let modName = "main"
  modules <- compileMainEntrypointToModules globalOpts tm modName
  build globalOpts [] tmpDir tmpDir modules
  erl <- coreLift $ findErlangExecutable
  coreLift $ system (executeBeamCmd erl tmpDir modName)
  pure ()

compileLibrary : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> (libName : String) -> (changedModules : Maybe (List ModuleIdent)) -> Core (Maybe (String, List String))
compileLibrary c tmpDir outputDir libName changedModules = do
  ds <- getDirectives (Other "erlang")
  let groupedDirectives = groupBy fst snd ds
  let globalDirectives = fromMaybe [] (lookup emptyNS groupedDirectives) -- TODO: Fix emptyNS
  let moduleDirectives = SortedMap.toList (delete emptyNS groupedDirectives) -- TODO: Fix emptyNS
  let allModuleOpts = map (uncurry parseModuleOpts) moduleDirectives
  let globalOpts = parseOpts globalDirectives
  modules <- compileLibraryToModules globalOpts allModuleOpts changedModules
  generatedModules <- build globalOpts allModuleOpts tmpDir outputDir modules
  pure (Just (libName, generatedModules))

export
codegenErlang : Codegen
codegenErlang = MkCG compileExpr executeExpr compileLibrary


text:
module LispVal

import Prelude.Bool as B
import Prelude.List as L

import Effects
import Effect.Exception
import Effect.State

mutual

  public export
  data LispError = NumArgs Integer (L.List LispVal)
                 | TypeMismatch String LispVal
                 | BadSpecialForm String LispVal
                 | NotFunction String String
                 | UnboundVar String LispVal
                 | Default String
                 | LispErr String

  public export
  EnvCtx : Type
  EnvCtx = L.List (String, LispVal)

  public export
  Eval : Type -> Type
  Eval a = Eff a [STATE EnvCtx, EXCEPTION LispError]

  public export
  record IFunc where
    constructor MkFun
    fn : L.List LispVal -> Eval LispVal

  public export
  data LispVal = Atom String
               | List (L.List LispVal)
               | DottedList (L.List LispVal) LispVal
               | Number Integer
               | Str String
               | Fun IFunc
               | Lambda IFunc EnvCtx
               | Nil
               | Bool B.Bool

mutual
  unwordsList : List LispVal -> String
  unwordsList = unwords . map showVal

  p : Maybe String -> String
  p varargs = case varargs of
                  Nothing => ""
                  Just arg => " . " ++ arg

  export
  showVal : LispVal -> String
  showVal (Atom x) = x
  showVal (List xs) = "(" ++ unwordsList xs ++ ")"
  showVal (DottedList xs x) = "(" ++ unwordsList xs ++ " . " ++ showVal x ++ ")"
  showVal (Number x) = show x
  showVal (Str x) = "\"" ++ x ++ "\""
  showVal (Bool True) = "#t"
  showVal (Bool False) = "#f"
  showVal (Fun _) = "internal function"
  showVal (Lambda _ _) = "lambda function"

export
Show LispVal where
     show = showVal

export
Show LispError where
     show (UnboundVar m v)     = m ++ ": " ++ show v
     show (BadSpecialForm s v) = s ++ " : " ++ show v
     show (NotFunction s f)    = s ++ " : " ++ show f
     show (NumArgs e f)        = "Expected " ++ show e ++ " args; found " ++ (show $ length f)
     show (TypeMismatch e f)   = "Invalid type: expected " ++ e ++ ", found " ++ show f
     show (Default s)          = s
     show (LispErr s)          = s
     show _                    = "Error!!!"


text:
module Uri.Core

import Data.String

public export
oneOf : Char -> String -> Bool
oneOf valid str = oneOf' 0 valid str
    where
        oneOf' : Nat -> Char -> String -> Bool
        oneOf' idx valid input =
            if (cast idx) >= length input then False
            else if assert_total $ strIndex input (cast idx) == valid then True
            else oneOf' (idx+1) valid input

public export
data Parser tok = MkParser ((Int, String) -> Either Int (tok, Int))

public export
run : Parser tok -> (Int, String) -> Either Int (tok, Int)
run (MkParser parserA) input = parserA input

public export
fail : Parser a
fail = MkParser $ \(pos, input) => Left pos

public export
Semigroup tok => Semigroup (Parser tok) where
    (<+>) (MkParser funA) (MkParser funB) = MkParser $ \(pos, input) => do
        (res1, pos')  <- funA (pos, input)
        (res2, pos'') <- funB (pos', input)
        Right (res1 <+> res2, pos'')

public export
Functor (Parser) where
    map func parser = MkParser $ \(pos, input) =>
        case run parser (pos, input) of
            Right (tok, newPos) => Right (func tok, newPos)
            Left err => Left err

public export
Applicative Parser where
    pure a = MkParser $ \(pos,input) => Right (a, pos)
    (MkParser fun) <*> (MkParser entry) = MkParser $ \(pos, input) => do
        (func, pos')  <- fun   (pos, input)
        (res, pos'') <- entry (pos', input)
        Right (func res, pos'')

public export
Alternative Parser where
    empty = ?not_use_it
    (MkParser parserA) <|> (MkParser parserB) = MkParser $ \(pos, input) =>
        case parserA (pos, input) of
            Left err => parserB (pos, input)
            Right (tok, pos') => Right (tok, pos')

public export
Monad Parser where
    join (MkParser res) = MkParser $ \(pos, input) =>
        case res (pos, input) of
            Left err => Left err
            Right (tok, pos') => run tok (pos', input)

-- Cuts

public export
data Cut = MkCut Int Int
         | MkLit String
         | Join Cut Cut

Show Cut where
    show (MkCut a b) = concat ["(", show a, "--", show b ,")"]
    show (MkLit a) = concat ["(", a,")"]
    show (Join a b) = concat ["(", show a, " ", show b,")"]

public export
Semigroup Cut where
    (<+>) (MkCut sc ec) (MkCut sc' ec') = (MkCut sc ec')
    (<+>) (MkLit a) (MkLit b) = (MkLit (a ++ b))
    (<+>) a b = Join a b

Monoid Cut where
    neutral = (MkCut 0 0)

public export
(|>>) : Parser a -> Parser b -> Parser b
(|>>) parserA parserB = do
    _ <- parserA
    parserB

public export
(>>|) : Parser a -> Parser b -> Parser a
(>>|) parserA parserB = do
    res <- parserA
    _  <- parserB
    pure res

infixl 6 |>>
infixl 6 >>|

public export
option : Parser a -> Parser (Maybe a)
option (MkParser parserA) = MkParser $ \(pos, inp) =>
    case parserA (pos, inp) of
        Left err => Right (Nothing, pos)
        Right (tok, pos') => Right (Just tok, pos')

-- I trust you. I know that you will NEVER make an invalid
-- range that will make assert_total just panics.... you, Chiyoku,
-- have a great power and you'll have to use this power in the future
-- to cut strings.

cutBy : Cut -> String -> String
cutBy (MkCut sc ec) inp = assert_total (strSubstr sc (ec - sc) inp)
cutBy (MkLit a) inp = a
cutBy (Join a b) inp = (cutBy a inp) ++ (cutBy b inp)

public export
cut : Parser Cut -> Parser String
cut (MkParser parserCut) = MkParser $ \(pos, inp) =>
    case parserCut (pos, inp) of
        Left err => Left err
        Right (MkCut sc ec, pos') => Right (assert_total (strSubstr sc (ec - sc) inp), pos')
        Right (MkLit a, pos')     => Right (a, pos')
        Right (Join  a b, pos')   => Right ((cutBy a inp) ++ (cutBy b inp), pos')

-- Lexer rules

public export
is : (Char -> Bool) -> Parser Cut
is valid = MkParser $ \(pos, inp) =>
    if cast pos >= length inp
        then Left pos
        else if valid (assert_total $ strIndex inp pos)
                then Right (MkCut pos (pos+1), pos+1)
                else Left pos

%inline
public export
chr : Char -> Parser Cut
chr c = is (== c)

public export
match : (Char -> Bool) -> Parser Cut
match valid = MkParser
    $ \(pos, input) =>
        case match' valid (input, pos) of
            Left err   => Left err
            Right pos' => Right (MkCut pos pos', pos')
    where
        match' : (Char -> Bool) -> (String, Int) -> Either Int Int
        match' valid (input, inpPos) =
                 if (cast inpPos >= length input)
                    then Right inpPos
                    else if valid (assert_total $ strIndex input inpPos)
                            then match' valid (input, inpPos+1)
                            else Right inpPos

public export
matchPlus : (Char -> Bool) -> Parser Cut
matchPlus valid = do
    res <- match valid
    case res of
        (MkCut start end) =>
            if start == end then fail
                            else pure (MkCut start end)
        res => pure res

public export
exact : String -> Parser Cut
exact valid = MkParser
    $ \(pos, input) =>
        case exact' (valid, 0) (input, pos) of
            Left err   => Left err
            Right pos' => Right (MkCut pos pos', pos')
    where
        exact' : (String, Int) -> (String, Int) -> Either Int Int
        exact' (valid, valPos) (input, inpPos) =
                 case (cast valPos >= length valid, cast inpPos >= length input) of
                    (True, _) => Right inpPos -- End of the valid string (probably matched everything)
                    (_, True) => Left  inpPos -- End of the input string gives us an error
                    (False, False) =>
                        let valChar = assert_total $ strIndex valid valPos
                            inpChar = assert_total $ strIndex input inpPos
                        in if valChar /= inpChar
                            then Left inpPos
                            else exact' (valid, valPos+1) (input, inpPos+1)

public export
some : Show a => Parser a -> Parser (List a)
some (MkParser parserA) = MkParser $ \(pos, input) =>
    case parserA (pos, input) of
        Left err => Left err
        Right (tok, pos') =>
            if pos' == pos then Left pos'
            else case run (some (MkParser parserA)) (pos', input) of
                    Left err => Right ([tok], pos')
                    Right (tokens, pos'') => Right (tok :: tokens, pos'')

public export
cutters : Parser Cut -> Parser Cut
cutters parserA = do
    fst <- parserA
    res <- option (cutters parserA)
    case res of
        Just end => pure (fst <+> end)
        Nothing => pure fst

public export
eof : Parser ()
eof = MkParser $ \(pos, input) =>
    if (cast pos) >= (length input)
        then Right ((), pos)
        else Left pos

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
module IdrisJvm.Core.Asm

import Data.SortedMap
import IdrisJvm.IR.Types

%access public export

record JMethodName where
  constructor MkJMethodName
  jmethClsName : String
  jmethName    : String

Eq JMethodName where
  (==) (MkJMethodName c1 m1) (MkJMethodName c2 m2) = c1 == c2 && m1 == m2

Show JMethodName where
  show (MkJMethodName cname mname) = cname ++ "#" ++ mname

Ord JMethodName where
   compare (MkJMethodName c1 m1) (MkJMethodName c2 m2) =
     case c1 `compare` c2 of
       EQ => m1 `compare` m2
       classOrdering => classOrdering

data InferredType = IBool | IByte | IChar | IShort | IInt | ILong | IFloat | IDouble | Ref String
                  | IArray InferredType | IUnknown

InferredTypeStore : Type
InferredTypeStore = SortedMap Int InferredType

record InferredFunctionType where
    constructor MkInferredFunctionType
    functionName : JMethodName
    returnType : InferredType
    locsType : InferredTypeStore
    arity : Nat

rtClass : String -> String
rtClass c = "io/github/mmhelloworld/idrisjvm/runtime/" ++ c

idrisObjectType : String
idrisObjectType = rtClass "IdrisObject"

thunkClass : String
thunkClass = rtClass "Thunk"

objectClass : String
objectClass = "java/lang/Object"

futureClass : String
futureClass = "java/util/concurrent/Future"

inferredObjectType : InferredType
inferredObjectType = Ref "java/lang/Object"

inferredBigIntegerType : InferredType
inferredBigIntegerType = Ref "java/math/BigInteger"

inferredStringType : InferredType
inferredStringType = Ref "java/lang/String"

inferredIdrisObjectType : InferredType
inferredIdrisObjectType = Ref idrisObjectType

record InferenceConfig where
  constructor MkInferenceConfig
  functionName : JMethodName
  functionTypes : SortedMap JMethodName InferredFunctionType

Eq InferredType where
  IBool == IBool = True
  IByte == IByte = True
  IChar == IChar = True
  IShort == IShort = True
  IInt == IInt = True
  ILong == ILong = True
  IFloat == IFloat = True
  IDouble == IDouble = True
  (Ref ty1) == (Ref ty2) = ty1 == ty2
  (IArray elemTy1) == (IArray elemTy2) = elemTy1 == elemTy2
  IUnknown == IUnknown = True
  _ == _ = False

Show InferredType where
    show IBool = "boolean"
    show IByte = "byte"
    show IChar = "char"
    show IShort = "short"
    show IInt = "int"
    show ILong = "long"
    show IFloat = "float"
    show IDouble = "double"
    show (Ref clsName) = clsName
    show (IArray elemTy) = "Array " ++ show elemTy
    show IUnknown = "unknown"

Semigroup InferredType where
  ty1 <+> ty2 = if ty1 == ty2 then ty1 else inferredObjectType

Monoid InferredType where
  neutral = IUnknown

isPrimitive : InferredType -> Bool
isPrimitive IBool = True
isPrimitive IByte = True
isPrimitive IChar = True
isPrimitive IShort = True
isPrimitive IInt = True
isPrimitive ILong = True
isPrimitive IFloat = True
isPrimitive IDouble = True
isPrimitive _ = False

isThunk : InferredType -> Bool
isThunk (Ref ty) = ty == thunkClass
isThunk _ = False

isObject : InferredType -> Bool
isObject (Ref ty) = ty == objectClass
isObject _ = False

getLocTy : InferredTypeStore -> LVar -> InferredType
getLocTy tys (Loc varIndex) = fromMaybe IUnknown $ SortedMap.lookup varIndex tys

ReferenceName : Type
ReferenceName = String

Label : Type
Label = String

Exception : Type
Exception = String

ClassName : Type
ClassName = String

FieldName : Type
FieldName = String

MethodName : Type
MethodName = String

Descriptor : Type
Descriptor = String

Signature : Type
Signature = String

SourceFileName : Type
SourceFileName = String

mutual
  data Annotation = MkAnnotation AnnotationTypeName (List AnnotationProperty)

  data FieldInitialValue = IntField Int | StringField String | DoubleField Double
  data BsmArg = BsmArgGetType Descriptor | BsmArgHandle Handle

  data Constant = DoubleConst Double
                | IntegerConst Int
                | LongConst Bits64
                | StringConst String
                | TypeConst String

  data ReferenceTypeDescriptor = ClassDesc ClassName
                               | InterfaceDesc ClassName
                               | ArrayDesc FieldTypeDescriptor
                               | IdrisExportDesc ClassName

  data FieldTypeDescriptor = FieldTyDescByte
                           | FieldTyDescChar
                           | FieldTyDescShort
                           | FieldTyDescBoolean
                           | FieldTyDescDouble
                           | FieldTyDescFloat
                           | FieldTyDescInt
                           | FieldTyDescLong
                           | FieldTyDescReference ReferenceTypeDescriptor

  data TypeDescriptor = FieldDescriptor FieldTypeDescriptor | VoidDescriptor | ThrowableDescriptor TypeDescriptor

  Eq ReferenceTypeDescriptor where
    (ClassDesc className1          ) == (ClassDesc className2          ) = className1 == className2
    (InterfaceDesc className1      ) == (InterfaceDesc className2      ) = className1 == className2
    (ArrayDesc elemDesc1           ) == (ArrayDesc elemDesc2           ) = elemDesc1 == elemDesc2
    (IdrisExportDesc className1    ) == (IdrisExportDesc className2    ) = className1 == className2
    _                                == _                                = False

  Eq FieldTypeDescriptor where
      FieldTyDescByte                == FieldTyDescByte               = True
      FieldTyDescChar                == FieldTyDescChar               = True
      FieldTyDescShort               == FieldTyDescShort              = True
      FieldTyDescBoolean             == FieldTyDescBoolean            = True
      FieldTyDescDouble              == FieldTyDescDouble             = True
      FieldTyDescFloat               == FieldTyDescFloat              = True
      FieldTyDescInt                 == FieldTyDescInt                = True
      FieldTyDescLong                == FieldTyDescLong               = True
      (FieldTyDescReference refTy1)  == (FieldTyDescReference refTy2) = refTy1 == refTy2
      _                              == _                             = False

  Eq TypeDescriptor where
    (FieldDescriptor fieldTyDesc1) == (FieldDescriptor fieldTyDesc2) = fieldTyDesc1 == fieldTyDesc2
    VoidDescriptor == VoidDescriptor = True
    (ThrowableDescriptor tyDesc1) == (ThrowableDescriptor tyDesc2) = tyDesc1 == tyDesc2
    _ == _ = False

  data MethodDescriptor = MkMethodDescriptor (List FieldTypeDescriptor) TypeDescriptor

  data ClassOpts = ComputeMaxs | ComputeFrames

  data InvocType = InvokeInterface | InvokeSpecial | InvokeStatic | InvokeVirtual

  data FieldInsType = FGetStatic | FPutStatic | FGetField | FPutField

  data FrameType = FFull | FSame | FAppend

  data Access = Private | Public | Static | Synthetic | Final

  Eq Access where
    Private == Private = True
    Public == Public = True
    Static == Static = True
    Synthetic == Synthetic = True
    Final == Final = True
    _ == _ = False

  data AnnotationValue = AnnInt Int
                       | AnnBoolean Bool
                       | AnnByte Bits8
                       | AnnChar Char
                       | AnnShort Bits16
                       | AnnLong Bits64
                       | AnnFloat Double
                       | AnnDouble Double
                       | AnnString String
                       | AnnClass String
                       | AnnEnum String String
                       | AnnArray (List AnnotationValue)
                       | AnnAnnotation Annotation

  data HandleTag = HGetField
                 | HGetStatic
                 | HPutField
                 | HPutStatic
                 | HInvokeVirtual
                 | HInvokeStatic
                 | HInvokeSpecial
                 | HNewInvokeSpecial
                 | HInvokeInterface

  record Handle where
    constructor MkHandle
    tag : HandleTag
    hClassName  : ClassName
    hMethodName : MethodName
    hDescriptor : Descriptor
    isInterface : Bool

  data ReferenceType = RefTyClass | RefTyInterface

  AnnotationProperty : Type
  AnnotationProperty = (String, AnnotationValue)

  AnnotationTypeName : Type
  AnnotationTypeName = String

  Show ReferenceTypeDescriptor where
    show (ClassDesc className) = "ClassDesc " ++ show className
    show (InterfaceDesc className) = "InterfaceDesc " ++ show className
    show (ArrayDesc tyDesc) = "ArrayDesc " ++ show tyDesc
    show (IdrisExportDesc className) = "IdrisExportDesc " ++ show className

  Show FieldTypeDescriptor where
    show FieldTyDescByte = "FieldTyDescByte"
    show FieldTyDescChar = "FieldTyDescChar"
    show FieldTyDescShort = "FieldTyDescShort"
    show FieldTyDescBoolean = "FieldTyDescBoolean"
    show FieldTyDescDouble = "FieldTyDescDouble"
    show FieldTyDescFloat = "FieldTyDescFloat"
    show FieldTyDescInt = "FieldTyDescInt"
    show FieldTyDescLong = "FieldTyDescLong"
    show (FieldTyDescReference referenceTypeDescriptor) = "FieldTyDescReference(" ++ show referenceTypeDescriptor ++ ")"

  Show TypeDescriptor where
    show (FieldDescriptor fieldTypeDescriptor) = "FieldDescriptor(" ++ show fieldTypeDescriptor ++ ")"
    show VoidDescriptor = "VoidDescriptor"
    show (ThrowableDescriptor tyDesc) = "ThrowableDescriptor(" ++ show tyDesc ++ ")"

mutual
    asmRefTyDesc : ReferenceTypeDescriptor -> String
    asmRefTyDesc (ClassDesc c)       = "L" ++ c ++ ";"
    asmRefTyDesc (IdrisExportDesc c) = "L" ++ c ++ ";"
    asmRefTyDesc (InterfaceDesc c)   = "L" ++ c ++ ";"
    asmRefTyDesc (ArrayDesc ty)   = "[" ++ asmFieldTypeDesc ty

    refTyClassName : ReferenceTypeDescriptor -> ClassName
    refTyClassName (ClassDesc c)       = c
    refTyClassName (InterfaceDesc c)   = c
    refTyClassName (IdrisExportDesc c) = c
    refTyClassName arr@(ArrayDesc _)   = asmRefTyDesc arr

    asmFieldTypeDesc : FieldTypeDescriptor -> String
    asmFieldTypeDesc FieldTyDescByte           = "B"
    asmFieldTypeDesc FieldTyDescChar           = "C"
    asmFieldTypeDesc FieldTyDescShort          = "S"
    asmFieldTypeDesc FieldTyDescBoolean        = "Z"
    asmFieldTypeDesc FieldTyDescDouble         = "D"
    asmFieldTypeDesc FieldTyDescFloat          = "F"
    asmFieldTypeDesc FieldTyDescInt            = "I"
    asmFieldTypeDesc FieldTyDescLong           = "J"
    asmFieldTypeDesc (FieldTyDescReference f)  = asmRefTyDesc f

asmTypeDesc : TypeDescriptor -> String
asmTypeDesc (FieldDescriptor t) = asmFieldTypeDesc t
asmTypeDesc VoidDescriptor      = "V"
asmTypeDesc (ThrowableDescriptor tyDesc) = asmTypeDesc tyDesc

asmMethodDesc : MethodDescriptor -> String
asmMethodDesc (MkMethodDescriptor args returns) = "(" ++ asmArgs ++ ")" ++ r where
  asmArgs = concat $ asmFieldTypeDesc <$> args
  r = asmTypeDesc returns

data Asm : Type -> Type where
    Aaload : Asm ()
    Aastore : Asm ()
    Aconstnull : Asm ()
    Aload : Int -> Asm ()
    Anewarray : Descriptor -> Asm ()

    Anewbooleanarray : Asm ()
    Anewbytearray : Asm ()
    Anewchararray : Asm ()
    Anewshortarray : Asm ()
    Anewintarray : Asm ()
    Anewlongarray : Asm ()
    Anewfloatarray : Asm ()
    Anewdoublearray : Asm ()

    Arraylength : Asm ()
    Areturn : Asm ()
    Astore : Int -> Asm ()
    Baload : Asm ()
    Bastore : Asm ()
    Caload : Asm ()
    Castore : Asm ()
    Checkcast : Descriptor -> Asm ()
    ClassCodeStart : Int -> Access -> ClassName -> (Maybe Signature) -> ClassName -> List ClassName -> List Annotation -> Asm ()
    ClassCodeEnd : String -> Asm ()
    CreateClass : ClassOpts -> Asm ()
    CreateField : List Access -> ClassName -> FieldName -> Descriptor -> Maybe Signature -> Maybe FieldInitialValue -> Asm ()
    CreateLabel : String -> Asm Label
    CreateMethod : List Access -> ClassName -> MethodName -> Descriptor -> Maybe Signature ->
                   Maybe (List Exception) -> List Annotation -> List (List Annotation) -> Asm ()
    D2i : Asm ()
    D2f : Asm ()
    Dadd : Asm ()
    Daload : Asm ()
    Dastore : Asm ()
    Dconst : Double -> Asm ()
    Ddiv : Asm ()
    Debug : String -> Asm ()
    Dload : Int -> Asm ()
    Dmul : Asm ()
    Drem : Asm ()
    Dreturn : Asm ()
    Dstore : Int -> Asm ()
    Dsub : Asm ()
    Dup : Asm ()
    Error : String -> Asm ()
    F2d : Asm ()
    Faload : Asm ()
    Fastore : Asm ()
    Fconst : Double -> Asm ()
    Field : FieldInsType -> ClassName -> FieldName -> Descriptor -> Asm ()
    FieldEnd : Asm ()
    Fload : Int -> Asm ()
    Frame : FrameType -> Nat -> (List Signature) -> Nat -> (List Signature) -> Asm ()
    FreshIfIndex : Asm Nat
    FreshLambdaIndex : String -> Asm Nat
    FreshSwitchIndex : Asm Nat
    Freturn : Asm ()
    Fstore : Int -> Asm ()
    GetFunctionName : Asm JMethodName
    GetFunctionLocTypes : Asm InferredTypeStore
    GetFunctionRetType : Asm InferredType
    GetFunctionTypes : Asm (SortedMap JMethodName InferredFunctionType)
    GetLocalVarCount : Asm Nat
    Goto : Label -> Asm ()
    I2b : Asm ()
    I2c : Asm ()
    I2d : Asm ()
    I2l : Asm ()
    I2s : Asm ()
    Iadd : Asm ()
    Iaload : Asm ()
    Iand : Asm ()
    Iastore : Asm ()
    Ior : Asm ()
    Ixor : Asm ()
    Icompl : Asm ()
    Iconst : Int -> Asm ()
    Idiv : Asm ()
    Ifeq : Label -> Asm ()
    Ificmpge : Label -> Asm ()
    Ificmpgt : Label -> Asm ()
    Ificmple : Label -> Asm ()
    Ificmplt : Label -> Asm ()
    Ifnonnull : Label -> Asm ()
    Ifnull : Label -> Asm ()
    Iload : Int -> Asm ()
    Imul : Asm ()
    InstanceOf : ClassName -> Asm ()
    InvokeMethod : InvocType -> ClassName -> MethodName -> Descriptor -> Bool -> Asm ()
    InvokeDynamic : MethodName -> Descriptor -> Handle -> List BsmArg -> Asm ()
    Irem : Asm ()
    Ireturn : Asm ()
    Ishl : Asm ()
    Ishr : Asm ()
    Istore : Int -> Asm ()
    Isub : Asm ()
    Iushr : Asm ()
    L2i : Asm ()
    LabelStart : Label -> Asm ()
    Ladd : Asm ()
    Laload : Asm ()
    Land : Asm ()
    Lastore : Asm ()
    Lor : Asm ()
    Lxor : Asm ()
    Lcompl : Asm ()
    Lconst : Bits64 -> Asm ()
    Ldc : Constant -> Asm ()
    Ldiv : Asm ()
    Lload : Int  -> Asm ()
    Lmul : Asm ()
    LookupSwitch : Label -> List Label -> List Int-> Asm ()
    Lrem : Asm ()
    Lreturn : Asm ()
    Lshl : Asm ()
    Lshr : Asm ()
    Lstore : Int -> Asm ()
    Lsub : Asm ()
    Lushr : Asm ()
    MaxStackAndLocal : Int -> Int -> Asm ()
    MethodCodeStart : Asm ()
    MethodCodeEnd : Asm ()
    Multianewarray : Descriptor -> Nat -> Asm ()
    New : ClassName -> Asm ()
    Pop : Asm ()
    Pop2 : Asm ()
    Return : Asm ()
    Saload : Asm ()
    Sastore : Asm ()
    ShouldDescribeFrame : Asm Bool
    SourceInfo : SourceFileName -> Asm ()
    Subroutine : Asm () -> Asm ()
    UpdateFunctionName : JMethodName -> Asm ()
    UpdateFunctionLocTypes : InferredTypeStore -> Asm ()
    UpdateFunctionRetType : InferredType -> Asm ()
    UpdateFunctionTypes : SortedMap JMethodName InferredFunctionType -> Asm ()
    UpdateLocalVarCount : Nat -> Asm ()
    UpdateShouldDescribeFrame : Bool -> Asm ()
    UpdateSwitchIndex : Nat -> Asm ()
    UpdateIfIndex : Nat -> Asm ()

    Pure : ty -> Asm ty
    Bind : Asm a -> (a -> Asm b) -> Asm b

namespace AsmDo
  (>>=) : Asm a -> (a -> Asm b) -> Asm b
  (>>=) = Bind

Functor Asm where
  map f a = Bind a (\a' => Pure $ f a')

Applicative Asm where
  pure = Pure

  (<*>) f a = Bind f (\f' =>
              Bind a (\a' =>
              Pure (f' a')))

getFunctionType : JMethodName -> Asm (InferredType, InferredTypeStore)
getFunctionType fname =
  maybe (IUnknown, SortedMap.empty) (\fty => (returnType fty, locsType fty))
    . SortedMap.lookup fname <$> GetFunctionTypes

isExportedDesc : FieldTypeDescriptor -> Bool
isExportedDesc (FieldTyDescReference (IdrisExportDesc _)) = True
isExportedDesc _ = False

isExportedReturnDesc : TypeDescriptor -> Bool
isExportedReturnDesc (FieldDescriptor (FieldTyDescReference (IdrisExportDesc _))) = True
isExportedReturnDesc _ = False


text:
module Tail

import Data.String

main : IO ()
main = assert_total $ do
  putStrLn $ strTail ""
  putStrLn $ strTail " Hello World!"


text:
import Aoc
import Data.Vect
%default total

main : IO ()
main = do
  ns <- readIntegerLines {a=Int}
  putStr "*   "; printLn [product c | c <- combinations 2 ns, sum c == 2020]
  putStr "**  "; printLn [product c | c <- combinations 3 ns, sum c == 2020]


text:
module Language.LSP.SignatureHelp

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Data.List
import Data.String
import Idris.Doc.String
import Idris.REPL.Opts
import Idris.Syntax
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Utils
import Server.Log

-- Color codes in JSON messages makes the JSON parser fail, we have to
-- turn temporarly the syntax highlight and coloring off when asking for
-- for documentation.
getNonColoredDocsForName : Ref Ctxt Defs
                        => Ref ROpts REPLOpts
                        => Ref Syn SyntaxInfo
                        => FC -> Name -> Core String
getNonColoredDocsForName fc n = do
  ropts <- get ROpts
  put ROpts (record { color = False, synHighlightOn = False } ropts)
  docs <- getDocsForName fc n
  put ROpts ropts
  pure (show docs)

-- Find the unique Name in the type term for the function return type which represent
-- the datatype. This function should be called only for a closed term of a DCon.
findRefNamesInTerm : Term vars -> List Name
findRefNamesInTerm (Local fc isLet idx p) = []
findRefNamesInTerm (Ref fc x name)        = [name]
findRefNamesInTerm (Meta fc x y xs)       = concatMap findRefNamesInTerm xs
findRefNamesInTerm (Bind fc x b scope)    = findRefNamesInTerm scope
findRefNamesInTerm (App fc fn arg)        = findRefNamesInTerm fn ++ findRefNamesInTerm arg
findRefNamesInTerm (As fc x as pat)       = findRefNamesInTerm as ++ findRefNamesInTerm pat
findRefNamesInTerm (TDelayed fc x y)      = findRefNamesInTerm y
findRefNamesInTerm (TDelay fc x ty arg)   = findRefNamesInTerm ty
findRefNamesInTerm (TForce fc x y)        = findRefNamesInTerm y
findRefNamesInTerm (PrimVal fc c)         = []
findRefNamesInTerm (Erased fc imp)        = []
findRefNamesInTerm (TType fc)             = []

renderDataTypeInfo : Ref Ctxt Defs
                  => Ref ROpts REPLOpts
                  => Ref Syn SyntaxInfo
                  => Name -> Def -> Core (Maybe String)
renderDataTypeInfo n d@(DCon tag arity newtypeArg) = do
  -- Render the related whole data structure information for the selected data constructor.
  -- Helps to understand code, when we have an easy way to look at all the constructors.
  context <- gets Ctxt gamma
  fullName <- getFullName n
  case !(lookupCtxtExact fullName context) of
    Nothing => pure Nothing
    Just df => case findRefNamesInTerm (getFn df.type) of
                [rn] => do
                  fullName <- getFullName rn
                  case !(lookupDefName fullName context) of
                    -- Render the TCon for this DCon
                    [(defName, _, tcon@(TCon _ _ _ _ _ _ _ _))] => renderDataTypeInfo defName tcon
                    _ => pure Nothing
                _ => pure Nothing
renderDataTypeInfo n d@(TCon tag arity parampos detpos flags mutwith datacons detagabbleBy) = do
  -- Render the data structure information for the type.
  context <- gets Ctxt gamma
  constructors <- traverse
                    (\dn => case !(lookupDefName dn context) of
                              [(_, _, DCon _ _ _)] => do
                                fullName <- getFullName dn
                                pure $ Just $ " | " ++ show fullName ++ " ..."
                              _ => pure $ the (Maybe String) Nothing)
                    datacons
  pure $ Just $ String.unlines (show n :: catMaybes constructors)
renderDataTypeInfo n other = pure Nothing

||| Generate the signature help for a callable function. In Idris many many things are
||| callable functions.
export
signatureHelp : Ref Ctxt Defs
             => Ref MD Metadata
             => Ref LSPConf LSPConfiguration
             => Ref ROpts REPLOpts
             => Ref Syn SyntaxInfo
             => SignatureHelpParams -> Core (Maybe SignatureHelp)
signatureHelp params =
  catch (do let line = params.position.line
            let col = params.position.character
            nameLocs <- gets MD nameLocMap
            let Just ((fname, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
              | Nothing => do
                  logString Debug "signatureHelp: didn't find name for \{show (line,col)}"
                  pure Nothing

            -- Check of the name is a local name.
            localResult <- findTypeAt $ anyWithName name $ within (line, col)

            docs <- getNonColoredDocsForName (MkFC fname nstart nend) name

            -- Generate the data type information if it is not in the generated doc already.
            -- When there is no Constructor info, the data structure information is hidden
            -- and only partial information can be retrieved.
            dataTypeInformation <-
              if "Constructors:" `isInfixOf` docs
                then pure []
                else do
                  defs <- lookupDefName name !(gets Ctxt gamma)
                  infos <- traverse
                            (\(n, _, d) => do
                              infoStr <- renderDataTypeInfo n d
                              pure $ map (\str => ("Data structure of", str)) infoStr)
                            defs
                  pure $ catMaybes infos

            -- Use one signature block, as it seems the nvim client doesn't render more than one... :(
            let signatureDocs : List (String, String)
                signatureDocs =
                  case localResult of
                    Just (n,_,t) => [("Local", show n ++ " : " ++ show t), ("Shadowing", docs)]
                    Nothing    => [("Global definition(s)", docs)]

            let signatures =
                  MkSignatureInformation
                    { label = show name
                    , documentation
                        = Just $ make
                        $ concatMap
                            (\(header, body) => "\n" ++ header ++ "\n" ++ body ++ "\n")
                            (signatureDocs ++ dataTypeInformation)
                    , parameters_ = Nothing
                    , activeParameter = Nothing
                    }
            pure $ Just $ MkSignatureHelp
              { signatures = [signatures]
              , activeSignature = Nothing
              , activeParameter = Nothing
              })
  (\err => pure Nothing)


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

export
program : PrintString m => Zippable m => CanSleep m => CanSpawn m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"
  (l, r) <- zip
    (do spawn $ do
          sleepFor 200.millis
          printTime offset "                                          spawned 1, before 500"
          sleepFor 500.millis
          printTime offset "                                          spawned 1, after 500"
        for 5 $ do
          printTime offset "proc 1, before 1000"
          sleepFor 1.seconds
          printTime offset "proc 1, before 2000"
          sleepFor 2.seconds
        pure 4)
    (do spawn $ do
          sleepFor 100.millis
          printTime offset "                                          spawned 2, before 15s"
          sleepFor 15.seconds
          printTime offset "                                          spawned 2, after 15s"
        for 10 $ do
          printTime offset "                     proc 2, before 350"
          sleepFor 350.millis
          printTime offset "                     proc 2, before 750"
          sleepFor 750.millis
        pure "right process")
  printTime offset "end, l: \{show l}, r: \{show r}"


text:
import Data.Vect

data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd () height (S height)
  Pop : StackCmd Integer (S height) height
  Top : StackCmd Integer (S height) (S height)

  GetStr : StackCmd String height height
  PutStr : String -> StackCmd () height height

  Pure : ty -> StackCmd ty height height
  (>>=) : StackCmd a height1 height2 ->
          (a -> StackCmd b height2 height3) ->
          StackCmd b height1 height3

data StackIO : Nat -> Type where
   Do : StackCmd a height1 height2 ->
        (a -> Inf (StackIO height2)) -> StackIO height1

namespace StackDo
  (>>=) : StackCmd a height1 height2 ->
         (a -> Inf (StackIO height2)) -> StackIO height1
  (>>=) = Do

runStack : (stk: Vect inHeight Integer) ->
            StackCmd ty inHeight outHeight ->
            IO (ty, Vect outHeight Integer)
runStack stk (Push val) = pure ((), val :: stk)
runStack (val :: stk) Pop = pure (val, stk)
runStack (val :: stk) Top = pure (val, val :: stk)
runStack stk GetStr = do x <- getLine
                         pure (x, stk)
runStack stk (PutStr x) = do putStr x
                             pure (() , stk)
runStack stk (Pure x) = pure (x, stk)
runStack stk (cmd >>= next)
  = do (cmdRes, newStk) <- runStack stk cmd
       runStack newStk (next cmdRes)

testAdd : StackCmd Integer 0 0
testAdd = do Push 10
             Push 20
             val1 <- Pop
             val2 <- Pop
             Pure (val1 + val2)

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push (val1 + val2)

data Fuel = Dry | More (Lazy Fuel)

forever : Fuel
forever = More forever

run : Fuel -> Vect height Integer -> StackIO height -> IO ()
run Dry stk p = pure ()
run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c
                                  run fuel newStk (f res)

data StkInput = Number Integer
              | Add

strToInput : String -> Maybe StkInput
strToInput "" = Nothing
strToInput "add" = Just Add
strToInput x = if all isDigit (unpack x)
                  then Just (Number (cast x))
                  else Nothing

mutual
  tryAdd : StackIO height
  tryAdd {height = S(S h)}= do doAdd
                               result <- Top
                               PutStr (show result ++ "\n")
                               stackCalc
  tryAdd = do PutStr "Fewer than two items on the stack \n"
              stackCalc

  stackCalc : StackIO height
  stackCalc = do PutStr "> "
                 input <- GetStr
                 case strToInput input of
                      Nothing => do PutStr "Invalid input\n"
                                    stackCalc
                      Just (Number x) => do Push x
                                            stackCalc
                      Just Add => tryAdd

main: IO ()
main = run forever [] stackCalc


text:
module Text.Html.Event

import Data.Maybe

%default total

--------------------------------------------------------------------------------
--          Event Info Types
--------------------------------------------------------------------------------

public export
record MouseInfo where
  constructor MkMouseInfo
  -- buttons
  button  : Int16
  buttons : Bits16

  -- coordinates
  clientX : Int32
  clientY : Int32
  screenX : Int32
  screenY : Int32

  -- keys
  alt     : Bool
  ctrl    : Bool
  meta    : Bool
  shift   : Bool

public export
record InputInfo where
  constructor MkInputInfo
  value   : String
  checked : Bool

public export
record KeyInfo where
  constructor MkKeyInfo
  key         : String
  code        : String
  location    : Bits32
  isComposing : Bool

  -- control keys
  alt         : Bool
  ctrl        : Bool
  meta        : Bool
  shift       : Bool

--------------------------------------------------------------------------------
--          Events
--------------------------------------------------------------------------------

public export
data DOMEvent : Type -> Type where
  -- Mouse clicks
  Click      : (MouseInfo -> Maybe a) -> DOMEvent a
  DblClick   : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseDown  : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseUp    : (MouseInfo -> Maybe a) -> DOMEvent a

  -- Mouse movement
  MouseEnter : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseLeave : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseOver  : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseOut   : (MouseInfo -> Maybe a) -> DOMEvent a
  MouseMove  : (MouseInfo -> Maybe a) -> DOMEvent a

  -- Focus
  Blur       : a -> DOMEvent a
  Focus      : a -> DOMEvent a

  -- Keyboard
  KeyDown    : (KeyInfo -> Maybe a) -> DOMEvent a
  KeyUp      : (KeyInfo -> Maybe a) -> DOMEvent a

  -- Input
  Change     : (InputInfo -> Maybe a) -> DOMEvent a
  Input      : (InputInfo -> Maybe a) -> DOMEvent a

  -- Routing
  HashChange : a -> DOMEvent a