text:
module Test.Bits64

import Data.Prim.Bits64
import Data.SOP
import Hedgehog
import Test.RingLaws

allBits64 : Gen Bits64
allBits64 = bits64 (linear 0 0xffffffffffffffff)

gt0 : Gen Bits64
gt0 = bits64 (linear 1 MaxBits64)

gt1 : Gen Bits64
gt1 = bits64 (linear 2 MaxBits64)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allBits64
  (b8 <= MaxBits64) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allBits64
  (b8 >= MinBits64) === True

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allBits64, allBits64]
  toOrdering (comp m n) === compare m n

prop_mod : Property
prop_mod = property $ do
  [n,d] <- forAll $ np [allBits64, gt0]
  compare (n `mod` d) d === LT

prop_div : Property
prop_div = property $ do
  [n,d] <- forAll $ np [gt0, gt1]
  compare (n `div` d) n === LT

prop_divMod : Property
prop_divMod = property $ do
  [n,d] <- forAll $ np [allBits64, gt0]
  let x = n `div` d
      r = n `mod` d
  n === x * d + r

export
props : Group
props = MkGroup "Bits64" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  , ("prop_mod",    prop_mod)
  , ("prop_div",    prop_div)
  , ("prop_divMod", prop_divMod)
  ] ++ ringProps allBits64


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module seL4.seL4Debug

import Prelude.Strings

import seL4.BootinfoTypes
import seL4.Syscalls

%access public export
%default total

(>>) : Monad m => m a -> m b -> m b
m >> k = m >>= \_ => k

mapM_ : (Monad m, Foldable t) => (a -> m b) -> t a -> m ()
mapM_ f xs = foldr ((>>) . f) (pure ()) xs

debugPrint : String -> IO ()
debugPrint str = mapM_ seL4_DebugPutChar (unpack str)

ifdef(`CONFIG_USER_DEBUG_BUILD', `

debugPrintBootInfo : SeL4_BootInfo -> IO ()
debugPrintBootInfo info = do
  debugPrint (show info)

')

ext: idr


text:
data Gnu : Type where [noHints, uniqueSearch]
  ||| Use Bool stop proof search from using constructors
  G : Bool -> Gnu
  N : Bool -> Gnu
  U : Bool -> Gnu

||| Makes interaction a bit nicer
Show Gnu where
  show (G _) = "G"
  show (N _) = "N"
  show (U _) = "U"

FooG : Gnu
FooG = G True

FooN : Gnu
FooN = N True

FooU : Gnu
FooU = U True

||| Curried versions
CooG : Unit -> Gnu
CooG _ = FooG

CooN : Unit -> Gnu
CooN _ = FooN

CooU : Unit -> Gnu
CooU _ = FooU

||| We'll use this to see what proof Idris finds.
Guess : {auto gnu : Gnu} -> String
Guess {gnu} = show gnu

||| Calls `Guess {gnu = gnu}` as expected
TestOK1 : (gnu : Gnu) -> String
TestOK1 gnu = Guess

||| Calls `Guess {gnu = f ()}` as expected
TestOK2 : (f : Unit -> Gnu) -> String
TestOK2 f = Guess

||| This is the meat. I'd expect this function to raise an error
||| because it is ambiguous which local/local function to use.
TestSurprise1 : (gnu1, gnu2 : Gnu) -> String
TestSurprise1 gnu1 gnu2 = Guess

TestSurprise2 : (f,g : Unit -> Gnu) -> String
TestSurprise2 f g = Guess

TestSurprise3 : (Unit -> Gnu, Unit -> Gnu) -> String
TestSurprise3 f = Guess


text:
module sorting_with_proof

import Data.Vect
import Data.Fin
import permutation
import perm_cons

data Finite : Nat -> Type where
    FinZ : (k : Nat) -> (Finite (S k))
    FinS : (k : Nat) -> (Finite k) -> (Finite (S k))

total
Finite_to_Fin : (k : Nat) -> (Finite k) -> (Fin k)
Finite_to_Fin Z a impossible
Finite_to_Fin (S k) (FinZ k) = FZ
Finite_to_Fin (S k) (FinS k nm) = FS (Finite_to_Fin k nm)

total
Fin_to_Finite : (k : Nat) -> (Fin k) -> (Finite k)
Fin_to_Finite Z a impossible
Fin_to_Finite (S k) FZ = FinZ k
Fin_to_Finite (S k) (FS l) = FinS k (Fin_to_Finite k l)

||| Predecessor function for finite
total
predFinite : (k : Nat) -> (Finite k) -> (Finite k)
predFinite Z a impossible
predFinite (S k) (FinZ k) = FinZ k
predFinite (S (S k)) (FinS (S k) (FinZ k)) = FinZ (S k)
predFinite (S (S k)) (FinS (S k) l) = FinS (S k) (predFinite (S k) l)

||| Predecessor function for fin
total
predFin : (n : Nat) -> (Fin n) -> (Fin n)
predFin n a = Finite_to_Fin n ( predFinite n (Fin_to_Finite n a))

||| Type of proofs that a vector is sorted in increasing order.
||| Note that the predecessor function takes care of the first index
total
SortProof : (n : Nat) -> (NatVect n) -> (Fin n) -> Type
SortProof Z v a impossible
SortProof (S k) v l = LTE (Vect.index (pred l) v) (Vect.index l v)

||| Type of the sorted vectors.
SortedVect : Type
SortedVect = (n : Nat ** (v : (NatVect n)  ** ((k : Fin n) -> (SortProof n v k))))


text:
module SimpleData

data Fwd a = FNil | (<|) a (Fwd a)
data Bwd a = BNil | (|>) (Bwd a) a

data Tree n l
  = Leaf l
  | Node (Tree n l) n (Tree n l)


text:
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)
%name Tree tree, tree1, tree2

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node tleft val tright) = case compare x val of
                                        LT => Node (insert x tleft) val tright
                                        EQ => orig
                                        GT => Node tleft val (insert x tright)


text:
module Yaffle.Main

import Parser.Source

import Core.Binary
import Core.Context
import Core.Directory
import Core.Env
import Core.FC
import Core.InitPrimitives
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.TT
import Core.UnifyState
import Libraries.Utils.Path

import TTImp.Parser
import TTImp.ProcessDecls
import TTImp.TTImp

import Yaffle.REPL

import Data.List
import Data.So
import Data.String
import System

%default covering

usage : String
usage = "Usage: yaffle <input file> [--timing]"

processArgs : List String -> Core Bool
processArgs [] = pure False
processArgs ["--timing"] = pure True
processArgs _
    = coreLift $ do ignore $ putStrLn usage
                    exitWith (ExitFailure 1)

HasNames () where
  full _ _ = pure ()
  resolved _ _ = pure ()

export
yaffleMain : String -> List String -> Core ()
yaffleMain sourceFileName args
    = do defs <- initDefs
         c <- newRef Ctxt defs
         t <- processArgs args
         modIdent <- ctxtPathToNS sourceFileName
         m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))
         u <- newRef UST initUState
         setLogTimings t
         addPrimitives
         case extension sourceFileName of
              Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC"
                               ignore $ readFromTTC {extra = ()} True emptyFC True sourceFileName (nsAsModuleIdent emptyNS) emptyNS
                               coreLift_ $ putStrLn "Read TTC"
              _ => do coreLift_ $ putStrLn "Processing as TTImp"
                      ok <- processTTImpFile sourceFileName
                      when ok $
                         do makeBuildDirectory modIdent
                            ttcFileName <- getTTCFileName sourceFileName "ttc"
                            writeToTTC () sourceFileName ttcFileName
                            coreLift_ $ putStrLn "Written TTC"
         ust <- get UST

         repl {c} {u}

ymain : IO ()
ymain
    = do (_ :: fname :: rest) <- getArgs
             | _ => do putStrLn usage
                       exitWith (ExitFailure 1)
         coreRun (yaffleMain fname rest)
               (\err : Error => putStrLn ("Uncaught error: " ++ show err))
               (\res => pure ())


text:
module Main

import System
import System.Directory
import System.File

import Test.Golden

%default covering

------------------------------------------------------------------------
-- Test cases

ttimpTests : TestPool
ttimpTests = MkTestPool "TTImp" [] Nothing
     [ "basic001", "basic002", "basic003", "basic004", "basic005"
     , "basic006"
     , "coverage002"
     , "dot001"
     , "eta001"
     , "lazy001"
     , "nest001", "nest002"
     , "perf001", "perf002", "perf003"
     , "record001", "record002", "record003"
     , "qtt001", "qtt003"
     , "total001", "total002", "total003"
     ]

idrisTestsBasic : TestPool
idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing
      -- Fundamental language features
      ["basic001", "basic002", "basic003", "basic004", "basic005",
       "basic006", "basic007", "basic008", "basic009", "basic010",
       "basic011", "basic012", "basic013", "basic014", "basic015",
       "basic016", "basic017", "basic018", "basic019", "basic020",
       "basic021", "basic022", "basic023", "basic024", "basic025",
       "basic026", "basic027", "basic028", "basic029", "basic030",
       "basic031", "basic032", "basic033", "basic034", "basic035",
       "basic036", "basic037", "basic038", "basic039", "basic040",
       "basic041", "basic042", "basic043", "basic044", "basic045",
       "basic046", "basic047",             "basic049", "basic050",
       "basic051", "basic052", "basic053", "basic054", "basic055",
       "basic056", "basic057", "basic058", "basic059", "basic060",
       "basic061",
       "interpolation001", "interpolation002"]

idrisTestsCoverage : TestPool
idrisTestsCoverage = MkTestPool "Coverage checking" [] Nothing
       -- Coverage checking
      ["coverage001", "coverage002", "coverage003", "coverage004",
       "coverage005", "coverage006", "coverage007", "coverage008",
       "coverage009", "coverage010", "coverage011", "coverage012",
       "coverage013", "coverage014", "coverage015", "coverage016",
       "coverage017", "coverage018", "coverage019"]

idrisTestsCasetree : TestPool
idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
       -- Case tree building
      ["casetree001"]

idrisTestsWarning : TestPool
idrisTestsWarning = MkTestPool "Warnings" [] Nothing
     ["warning001"]

idrisTestsError : TestPool
idrisTestsError = MkTestPool "Error messages" [] Nothing
       -- Error messages
      ["error001", "error002", "error003", "error004", "error005",
       "error006", "error007", "error008", "error009", "error010",
       "error011", "error012", "error013", "error014", "error015",
       "error016", "error017", "error018", "error019", "error020",
       "error021",
       -- Parse errors
       "perror001", "perror002", "perror003", "perror004", "perror005",
       "perror006", "perror007", "perror008", "perror009", "perror010",
       "perror011"]

idrisTestsInteractive : TestPool
idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
       -- Interactive editing support
      ["interactive001", "interactive002", "interactive003", "interactive004",
       "interactive005", "interactive006", "interactive007", "interactive008",
       "interactive009", "interactive010", "interactive011", "interactive012",
       "interactive013", "interactive014", "interactive015", "interactive016",
       "interactive017", "interactive018", "interactive019", "interactive020",
       "interactive021", "interactive022", "interactive023", "interactive024",
       "interactive025", "interactive026", "interactive027", "interactive028",
       "interactive029", "interactive030", "interactive031", "interactive032",
       "interactive033", "interactive034", "interactive035", "interactive036",
       "interactive037"]

idrisTestsInterface : TestPool
idrisTestsInterface = MkTestPool "Interface" [] Nothing
       -- Interfaces
      ["interface001", "interface002", "interface003", "interface004",
       "interface005", "interface006", "interface007", "interface008",
       "interface009", "interface010", "interface011", "interface012",
       "interface013", "interface014", "interface015", "interface016",
       "interface017", "interface018", "interface019", "interface020",
       "interface021", "interface022", "interface023", "interface024",
       "interface025", "interface026", "interface027"]

idrisTestsLinear : TestPool
idrisTestsLinear = MkTestPool "Quantities" [] Nothing
       -- QTT and linearity related
       ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping
        "linear005", "linear006", "linear007", "linear008",
        "linear009", "linear010", "linear011", "linear012",
        "linear013", "linear014"]

idrisTestsLiterate : TestPool
idrisTestsLiterate = MkTestPool "Literate programming" [] Nothing
       -- Literate
      ["literate001", "literate002", "literate003", "literate004",
       "literate005", "literate006", "literate007", "literate008",
       "literate009", "literate010", "literate011", "literate012",
       "literate013", "literate014", "literate015", "literate016"]

idrisTestsPerformance : TestPool
idrisTestsPerformance = MkTestPool "Performance" [] Nothing
       -- Performance: things which have been slow in the past, or which
       -- pose interesting challenges for the elaborator
      ["perf001", "perf002", "perf003", "perf004", "perf005",
       "perf007", "perf008", "perf009"]

idrisTestsRegression : TestPool
idrisTestsRegression = MkTestPool "Various regressions" [] Nothing
       -- Miscellaneous regressions
      ["reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
       "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
       "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
       "reg036", "reg037", "reg038", "reg039", "reg040", "reg041", "reg042",
       "reg043", "reg044", "reg045", "reg046", "reg047", "reg048", "reg049",
       "reg050"]

idrisTestsData : TestPool
idrisTestsData = MkTestPool "Data and record types" [] Nothing
      [-- Data types
       "data001",
       -- Records, access and dependent update
       "record001", "record002", "record003", "record004", "record005",
       "record006", "record007", "record008", "record009"]

idrisTestsBuiltin : TestPool
idrisTestsBuiltin = MkTestPool "Builtin types and functions" [] Nothing
      -- %builtin related tests for the frontend (type-checking)
      ["builtin001", "builtin002", "builtin003", "builtin004", "builtin005",
       "builtin006", "builtin007", "builtin008", "builtin009", "builtin010",
       "builtin011"]

idrisTestsEvaluator : TestPool
idrisTestsEvaluator = MkTestPool "Evaluation" [] Nothing
      [ -- Evaluator
       "evaluator001", "evaluator002", "evaluator003",
       -- Miscellaneous REPL
       "interpreter001", "interpreter002", "interpreter003", "interpreter004",
       "interpreter005", "interpreter006", "interpreter007"]

idrisTestsAllBackends : Requirement -> TestPool
idrisTestsAllBackends cg = MkTestPool
      ("Test across all backends: " ++ show cg ++ " instance")
      [] (Just cg)
      [ -- Evaluator
       "evaluator004",
       -- Unfortunately the behaviour of Double is platform dependent so the
       -- following test is turned off.
       -- "evaluator005",
       "basic048",
       "perf006"]

idrisTestsTotality : TestPool
idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
       -- Positivity checking
      ["positivity001", "positivity002", "positivity003", "positivity004",
       -- Totality checking
       "total001", "total002", "total003", "total004", "total005",
       "total006", "total007", "total008", "total009", "total010",
       "total011", "total012"
      ]

idrisTests : TestPool
idrisTests = MkTestPool "Misc" [] Nothing
       -- Documentation strings
      ["docs001", "docs002", "docs003",
       -- Eta equality
       "eta001",
       -- Modules and imports
       "import001", "import002", "import003", "import004", "import005",
       -- Implicit laziness, lazy evaluation
       "lazy001", "lazy002",
       -- Namespace blocks
       "namespace001", "namespace002",
       -- Parameters blocks
       "params001", "params002", "params003",
       -- Packages and ipkg files
       "pkg001", "pkg002", "pkg003", "pkg004", "pkg005", "pkg006", "pkg007",
       "pkg008", "pkg009", "pkg010",
       -- Larger programs arising from real usage. Typically things with
       -- interesting interactions between features
       "real001", "real002",
       -- Quotation and reflection
       "reflection001", "reflection002", "reflection003", "reflection004",
       "reflection005", "reflection006", "reflection007", "reflection008",
       "reflection009","reflection010",
       -- The 'with' rule
       "with001", "with002", "with004", "with005", "with006",
       -- with-disambiguation
       "with003",
       -- pretty printing
       "pretty001",
       -- golden file testing
       "golden001"]

typeddTests : IO TestPool
typeddTests = testsInDir "typedd-book" (const True) "Type Driven Development" [] Nothing

chezTests : TestPool
chezTests = MkTestPool "Chez backend" [] (Just Chez)
    [ "chez001", "chez002", "chez003", "chez004", "chez005", "chez006"
    , "chez007", "chez008", "chez009", "chez010", "chez011", "chez012"
    , "chez013", "chez014", "chez015", "chez016", "chez017", "chez018"
    , "chez019", "chez020", "chez021", "chez022", "chez023", "chez024"
    , "chez025", "chez026", "chez027", "chez028", "chez029", "chez030"
    , "chez031", "chez032", "chez033", "chez034"
    , "futures001"
    , "bitops"
    , "casts"
    , "memo"
    , "newints"
    , "integers"
    , "semaphores001"
    , "semaphores002"
    , "perf001"
    , "reg001"
    , "channels001", "channels002", "channels003", "channels004", "channels005"
    ]

refcTests : IO TestPool
refcTests = testsInDir "refc" (const True) "Reference counting C backend" [] (Just C)

racketTests : TestPool
racketTests = MkTestPool "Racket backend" [] (Just Racket)
    [ "forkjoin001"
    , "semaphores001", "semaphores002"
    , "futures001"
    , "mutex001", "mutex002", "mutex003", "mutex004", "mutex005"
    , "conditions001" , "conditions002" , "conditions003" , "conditions004"
    , "conditions005"
--    , "conditions006"
--    , "conditions007"
    ]

nodeTests : TestPool
nodeTests = MkTestPool "Node backend" [] (Just Node)
    [ "node001", "node002", "node003", "node004", "node005", "node006"
    , "node007", "node008", "node009", "node011", "node012", "node015"
    , "node017", "node018", "node019", "node021", "node022", "node023"
    , "node024", "node025", "node026"
    , "perf001"
    -- , "node14", "node020"
    , "args"
    , "bitops"
    , "casts"
    , "memo"
    , "newints"
    , "reg001"
    , "stringcast"
    , "syntax001"
    , "tailrec001"
    , "idiom001"
    , "integers"
    , "fix1839"
    , "tailrec_libs"
    ]

vmcodeInterpTests : IO TestPool
vmcodeInterpTests = testsInDir "vmcode" (const True) "VMCode interpreter" [] Nothing

ideModeTests : IO TestPool
ideModeTests = testsInDir "ideMode" (const True) "IDE mode" [] Nothing

preludeTests : IO TestPool
preludeTests = testsInDir "prelude" (const True) "Prelude library" [] Nothing

templateTests : IO TestPool
templateTests = testsInDir "templates" (const True) "Test templates" [] Nothing

-- base library tests are run against
-- each codegen supported and to keep
-- things simple it's all one test group
-- that only runs if all backends are
-- available.
baseLibraryTests : IO TestPool
baseLibraryTests = testsInDir "base" (const True) "Base library" [Chez, Node] Nothing

-- same behavior as `baseLibraryTests`
contribLibraryTests : IO TestPool
contribLibraryTests = testsInDir "contrib" (const True) "Contrib library" [Chez, Node] Nothing

codegenTests : IO TestPool
codegenTests = testsInDir "codegen" (const True) "Code generation" [] Nothing

jvmTests : TestPool
jvmTests = MkTestPool "JVM backend" [] (Just Jvm)
    [ "jvm001", "jvm002", "jvm003", "jvm004", "jvm005", "jvm006",
      "jvm007", "jvm008", "jvm009", "jvm011", "jvm012", -- "jvm014",
      "jvm015", "jvm016", "jvm017", "jvm018", "jvm019", "jvm020",
      "reg001", "tailrec001" --, "concurrency001"
    ]

main : IO ()
main = runner $
  [ testPaths "ttimp" ttimpTests
  , testPaths "idris2" idrisTestsBasic
  , testPaths "idris2" idrisTestsCoverage
  , testPaths "idris2" idrisTestsCasetree
  , testPaths "idris2" idrisTestsError
  , testPaths "idris2" idrisTestsWarning
  , testPaths "idris2" idrisTestsInteractive
  , testPaths "idris2" idrisTestsInterface
  , testPaths "idris2" idrisTestsLiterate
  , testPaths "idris2" idrisTestsLinear
  , testPaths "idris2" idrisTestsPerformance
  , testPaths "idris2" idrisTestsRegression
  , testPaths "idris2" idrisTestsData
  , testPaths "idris2" idrisTestsBuiltin
  , testPaths "idris2" idrisTestsEvaluator
  , testPaths "idris2" idrisTestsTotality
  , testPaths "idris2" idrisTests
  , !typeddTests
  , !ideModeTests
  , !preludeTests
  , !baseLibraryTests
  , !contribLibraryTests
  , testPaths "chez" chezTests
  , !refcTests
  , testPaths "racket" racketTests
  , testPaths "node" nodeTests
  , !vmcodeInterpTests
  , !templateTests
  , !codegenTests
  , testPaths "jvm" jvmTests
  ]
  ++ map (testPaths "allbackends" . idrisTestsAllBackends) [Chez, Node, Racket]

    where

    testPaths : String -> TestPool -> TestPool
    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }


text:
module Inigo.Util.Url.Url

-- TODO: Improve here
public export
record Url where
  constructor MkUrl
  host : String
  path : String

export
fromHostPath : String -> String -> Url
fromHostPath host path =
  MkUrl host path

export
toString : Url -> String
toString url =
  host url ++ path url

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Starknet

export
fib : (i: Felt) -> Felt
fib n = if n == 0 || n == 1
    then n
    else fib (n - 1) + fib (n - 2)

export
main : Cairo ()
main =
  do
     val <- storageRead 123
     storageWrite 123 (val + fib 5)

     topic <- createMemory
     writeMemory 0 123 topic

     value <- createMemory
     writeMemory 0 val value

     emitEvent 1 topic 1 value

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 Data.Fin
import Data.Vect
import Data.Vect.Quantifiers
import Decidable.Equality

Cell : Nat -> Type
Cell n = Maybe (Fin n)

data Board : Nat -> Type where
  MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n

emptyBoard : {n : Nat} -> Board n
emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))

Empty : Cell n -> Type
Empty {n=n} x = (the (Cell n) Nothing) = x

Filled : Cell n -> Type
Filled {n=n} = (\x => Not (Empty x))

FullBoard : Board n -> Type
FullBoard (MkBoard b) = All (All Filled) b

indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)
indexStep = Refl

find : {p : a -> Type} -> ((x : a) -> Dec (p x)) -> (xs : Vect n a)
       -> Either (All (\x => Not (p x)) xs) (y : a ** (p y, (i : Fin n ** y = index i xs)))
find _ Nil = Left Nil
find {p} d (x::xs) with (d x)
  | Yes prf = Right (x ** (prf, (FZ ** Refl)))
  | No prf =
    case find {p} d xs of
      Right (y ** (prf', (i ** prf''))) =>
        Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
      Left prf' => Left (prf::prf')

empty : (cell : Cell n) -> Dec (Empty cell)
empty Nothing = Yes Refl
empty (Just _) = No nothingNotJust

findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
findEmptyInRow xs =
  case find {p=Empty} empty xs of
    Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
    Left p => Left p

getCell : Board n -> (Fin n, Fin n) -> Cell n
getCell (MkBoard b) (x, y) = index x (index y b)

emptyCell : {n : Nat} -> (b : Board n) ->
         Either (FullBoard b) (c : (Fin n, Fin n) ** Empty (getCell b c))
emptyCell (MkBoard rs) =
  case helper rs of
    Left p => Left p
    Right (ri ** (ci ** pf2)) => Right ((ci, ri) ** pf2)
 where
  helper : (rs : Vect m (Vect n (Cell n)))
           -> Either (All (All Filled) rs) (r : Fin m ** (c : Fin n ** Empty (index c (index r rs))))
  helper Nil = Left Nil
  helper (r::rs) =
    case findEmptyInRow r of
      Right (ci ** pf3) => Right (FZ ** (ci ** pf3))
      Left prf =>
        case helper rs of
          Left prf' => Left (prf::prf')
          Right (ri ** (ci ** pf4)) => Right (FS ri ** (ci ** pf4))

main : IO ()
main =
  case emptyCell (emptyBoard {n=0}) of
    Left _ => putStrLn "l"
    Right _ => putStrLn "r"

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.idr ]
-- Module    : Test.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Commons.Options.ArgParse.Test

import Commons.Options.ArgParse
import Commons.Options.ArgParse.Error

import Test.Unit.Assertions

%access private

||| Program Options
record Opts where
  constructor MkOpts
  from    : Maybe String
  verbose : Bool
  help    : Bool
  version : Bool
  args    : List String

Show Opts where
  show (MkOpts f v h ve as) = unwords ["MkOpts", show f, show v, show h, show ve, show as]

Eq Opts where
  (==) (MkOpts a b c d e) (MkOpts a' b' c' d' e') = a == a' && b == b' && c == c' && d' == d' && e == e'

||| Convert Arguments into Options
convOpts : Arg -> Opts -> Maybe Opts
convOpts (File x)     o = Just $ record {args = x :: args o} o
convOpts (KeyValue k v) o =
  case k of
    "from"    => Just $ record {from = Just v} o
    otherwise => Nothing
convOpts (Flag x) o =
  case x of
    "help"    => Just $ record {help = True} o
    "verbose" => Just $ record {verbose = True} o
    "version" => Just $ record {version = True} o
    otherwise => Nothing

defOpts : Opts
defOpts = MkOpts Nothing False False False Nil

test1 : IO ()
test1 =
    case parseArgs defOpts convOpts ["--help", "--verbose"] of
      Left _  => do
        putStrLn "Err"
        pure ()
      Right o => do
        printLn $ !(assertTrue $ verbose o)
        printLn $ !(assertFalse $ help o)
        printLn $ !(assertNothing $ from o)

export
runTests : IO ()
runTests = do
    putStrLn "Testing ArgParse"
    test1
    printLn !(assertRight $ parseArgs defOpts convOpts Nil)

    let res' = parseArgs defOpts convOpts ["exe", "--help", "--verbose", "--from=conv"]
    case res' of
      Left _    => putStrLn "Err"
      Right res => do
        printLn !(assertTrue $ from res == Just "conv")

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Main

import Control.Monad.State

data Tree a = Empty
            | Node (Tree a) a (Tree a)

Show a => Show (Tree a) where
  show Empty = "Empty"
  show (Node left val right) = "(Node " ++ show left ++ " " ++ show val ++ " " ++ show right ++ ")"

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty)
                      "Fred"
                      (Node Empty "Sheila" Empty))
                "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = pure Empty
treeLabelWith (Node left val right) = do
  leftLabelled <- treeLabelWith left
  (this :: rest) <- get
  put rest
  rightLabelled <- treeLabelWith right
  pure (Node leftLabelled (this, val) rightLabelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = evalState (treeLabelWith tree) [1..]

main : IO ()
main = do
  printLn $ flatten (treeLabel testTree)

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
module LowerCaseData

%default total

data TeXNat = zero | succ TeXNat
dts : TeXNat -> String
dts n = case n of
  LowerCaseData.zero   => "zero"
  LowerCaseData.succ _ => "non-zero"

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
natToInt : Nat -> Integer
natToInt Z = 0
natToInt (S k) = 1 + natToInt k

%builtin NaturalToInteger natToInt

intToNat : Integer -> Nat
intToNat i = if i <= 0
    then Z
    else S $ intToNat (i - 1)

%builtin IntegerToNatural intToNat

add : Nat -> Nat -> Nat
add Z y = y
add (S x) y = S (add x y)

%transform "add" add x y = intToNat (prim__add_Integer (natToInt x) (natToInt y))

main : IO ()
main = do
    printLn $ intToNat 3141592
    printLn $ intToNat 12345
    printLn $ add 100 1000
    printLn $ add 9566 7554


text:
module Data.Either

import Data.List1

%default total

--------------------------------------------------------------------------------
-- Checking for a specific constructor

||| Extract the Left value, if possible
public export
getLeft : Either a b -> Maybe a
getLeft (Left a) = Just a
getLeft _ = Nothing

||| Extract the Right value, if possible
public export
getRight : Either a b -> Maybe b
getRight (Right b) = Just b
getRight _ = Nothing

||| True if the argument is Left, False otherwise
public export
isLeft : Either a b -> Bool
isLeft (Left _)  = True
isLeft (Right _) = False

||| True if the argument is Right, False otherwise
public export
isRight : Either a b -> Bool
isRight (Left _)  = False
isRight (Right _) = True

--------------------------------------------------------------------------------
-- Grouping values

||| Compress the list of Lefts and Rights by accumulating
||| all of the lefts and rights into non-empty blocks.
export
compress : List (Either a b) -> List (Either (List1 a) (List1 b))
compress [] = []
compress (Left x :: abs) = compressLefts (singleton x) abs where
  compressLefts : List1 a -> List (Either a b) -> List (Either (List1 a) (List1 b))
  compressLefts acc (Left a :: abs) = compressLefts (cons a acc) abs
  compressLefts acc abs = Left (reverse acc) :: compress abs
compress (Right y :: abs) = compressRights (singleton y) abs where
  compressRights : List1 b -> List (Either a b) -> List (Either (List1 a) (List1 b))
  compressRights acc (Right b :: abs) = compressRights (cons b acc) abs
  compressRights acc abs = Right (reverse acc) :: compress abs

||| Decompress a compressed list. This is the left inverse of `compress` but not its
||| right inverse because nothing forces the input to be maximally compressed!
export
decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)
decompress = concatMap $ \case
  Left  as => map Left  $ forget as
  Right bs => map Right $ forget bs

||| Keep the payloads of all Left constructors in a list of Eithers
public export
lefts : List (Either a b) -> List a
lefts []              = []
lefts (Left  l :: xs) = l :: lefts xs
lefts (Right _ :: xs) = lefts xs

||| Keep the payloads of all Right constructors in a list of Eithers
public export
rights : List (Either a b) -> List b
rights []              = []
rights (Left  _ :: xs) = rights xs
rights (Right r :: xs) = r :: rights xs

||| Split a list of Eithers into a list of the left elements and a list of the right elements
public export
partitionEithers : List (Either a b) -> (List a, List b)
partitionEithers l = (lefts l, rights l)

||| Remove a "useless" Either by collapsing the case distinction
public export
fromEither : Either a a -> a
fromEither (Left l)  = l
fromEither (Right r) = r

||| Right becomes left and left becomes right
public export
mirror : Either a b -> Either b a
mirror (Left  x) = Right x
mirror (Right x) = Left x

--------------------------------------------------------------------------------
-- Bifunctor

export
pushInto : c -> Either a b -> Either (c, a) (c, b)
pushInto c = bimap (\ a => (c, a)) (\ b => (c, b))
  -- ^ not using sections to keep it backwards compatible

--------------------------------------------------------------------------------
-- Conversions
--------------------------------------------------------------------------------

||| Convert a Maybe to an Either by using a default value in case of Nothing
||| @ e the default value
public export
maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
maybeToEither def (Just j) = Right j
maybeToEither def Nothing  = Left  def

||| Convert an Either to a Maybe from Right injection
public export
eitherToMaybe : Either e a -> Maybe a
eitherToMaybe (Left _) = Nothing
eitherToMaybe (Right x) = Just x

-- Injectivity of constructors

||| Left is injective
export
leftInjective : Left x = Left y -> x = y
leftInjective Refl = Refl

||| Right is injective
export
rightInjective : Right x = Right y -> x = y
rightInjective Refl = Refl


text:
module Chapter8

-- import Data.Vect
import Exercises.Chapter7

%access  public export
%default total

-- Exercise 8.1.7.1

same_cons :  {xs : List a} -> {ys : List a}
          -> xs = ys -> x :: xs = x :: ys
same_cons = cong

-- Exercise 8.1.7.2

same_lists :  {xs : List a} -> {ys : List a}
           -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists prf prf' = rewrite prf in rewrite prf' in Refl

-- Exercise 8.1.7.3

data ThreeEq : a -> b -> c -> Type where
  Same : (x : a) -> ThreeEq x x x

-- Exercise 8.1.7.4

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z (Same z) = Same (S z)

-- `allSameS` can be thought of as a proof that if `x`, `y` and `z` are equal,
-- then `S x`, `S y` and `S z` are also equal.

-- Exercise 8.2.6.1

my_plusCommutes : (n, m : Nat) -> n + m = m + n
my_plusCommutes  Z    m = sym (plusZeroRightNeutral m)
my_plusCommutes (S k) m = rewrite my_plusCommutes k m in plusSuccRightSucc m k

-- my_plusCommutes n  Z    = plusZeroRightNeutral n
-- my_plusCommutes n (S k) = rewrite sym (my_plusCommutes n k) in
--                           sym (plusSuccRightSucc n k)

-- Exercise 8.2.6.2

my_reverse : Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n+m) a
    reverse' {n}           acc []      = rewrite plusZeroRightNeutral n in acc
    reverse' {n} {m = S k} acc (y::ys) = rewrite sym (plusSuccRightSucc n k) in
                                         reverse' (y::acc) ys

-- Exercise 8.3.4.1

head : Vect (S n) a -> a
head (x :: _) = x

tail : Vect (S n) a -> Vect n a
tail (_ :: xs) = xs

head_unequal :  DecEq a => {xs : Vect n a} -> {ys : Vect n a}
             -> (contra : Not (x = y))
             -> Not (x :: xs = y :: ys)
head_unequal contra = void . contra . cong {f = head}

tail_unequal :  DecEq a => {xs : Vect n a} -> {ys : Vect n a}
             -> (contra : Not (xs = ys))
             -> Not (x :: xs = y :: ys)
tail_unequal contra = void . contra . cong {f = tail}

-- Exercise 8.3.4.2

namespace MyVect
  implementation DecEq a => DecEq (Vect n a) where
    decEq [] [] = Yes Refl
    decEq (x :: xs) (y :: ys) with (decEq x y)
      | Yes same_head with (decEq xs ys)
        | Yes same_tail = Yes (rewrite same_head in rewrite same_tail in Refl)
        | No  contra    = No  (tail_unequal contra)
      | No contra = No (head_unequal contra)

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Cond

%default total
%access abstract

{-
Usage example:

foo : Int -> String
foo x = cond $ do
  x == 5 ?: "five"
  x == 17 ?: "bigger"
  otherwise "fnord"

• An otherwise at the end is required.
• Note that (?:) is a low-precedence operator and will act as such: parentheses
  may be required in some cases. Note also that otherwise is a function, so ($)
  or parentheses are required for non-simple default expressions.
• The expression for a non-matched clause is not evaluated, so this construct
  can be used to check preconditions on partial functions (but please encode
  these in types instead to make the functions total, if feasible).
-}

infix 0 ?:

data Alt a = Unmatched | Matched (Lazy a)

data Res a = It (Lazy a)

(>>=) : Alt a -> (() -> Res a) -> Res a
(>>=) Unmatched f = f ()
(>>=) (Matched x) f = It x

(?:) : Bool -> Lazy a -> Alt a
(?:) False x = Unmatched
(?:) True x = Matched x

otherwise : Lazy a -> Res a
otherwise x = It x

cond : Res a -> a
cond (It x) = x

max_stars_repo_name: david-christiansen/idris-utils

max_issues_repo_name: david-christiansen/idris-utils

max_forks_repo_name: david-christiansen/idris-utils


text:
module Main

getAnswer : String -> String
getAnswer "four" = "eight"
getAnswer "two" = "four"
getAnswer "one" = "two"
getAnswer "xx" = "XXX danger XXX"
getAnswer "" = "empty"
getAnswer _ = "unknown"

getAnswer' : String -> String
getAnswer' x = if (prim__strHead x) == '-' then "minus" else "plus"

main : IO ()
main = do
  putStrLn (getAnswer' "-")
  putStrLn (getAnswer' "se")
  putStrLn (getAnswer "xxx")
  putStrLn (getAnswer "se")
  putStrLn (getAnswer "")
  putStrLn (getAnswer "four")
  putStrLn (getAnswer "two")
  putStrLn (getAnswer "one")
  putStrLn (getAnswer "two")
  putStrLn (getAnswer "xxx")
  putStrLn (getAnswer "xx")
  putStrLn (getAnswer "x")
  putStrLn (getAnswer "seven")

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Protocol.IDE.Formatting

import Protocol.SExp
import Protocol.IDE.Decoration

import Data.Maybe
import Data.List

%default total

public export
data Formatting : Type where
  Bold      : Formatting
  Italic    : Formatting
  Underline : Formatting

export
Show Formatting where
  show Bold      = "bold"
  show Italic    = "italic"
  show Underline = "underline"

export
SExpable Formatting where
  toSExp format = SExpList [ SymbolAtom "text-formatting"
                           , SymbolAtom (show format)
                           ]
  where
    {- This definition looks like it repeats `Show`, but `display` is part
       of the IDE protocol, whereas the `Show` instance doesn't have to be.
    -}
    display : Formatting -> String
    display Bold      = "bold"
    display Italic    = "italic"
    display Underline = "underline"

export
FromSExpable Formatting where
  fromSExp (SExpList [ SymbolAtom "text-formatting"
                           , SymbolAtom format
                     ]) =
    case format of
       "bold"      => Just Bold
       "italic"    => Just Italic
       "underline" => Just Underline
       _           => Nothing
  fromSExp _ = Nothing

-- At most one decoration & one formatting
-- (We could use `These` to guarantee non-emptiness but I am not
-- convinced this will stay being just 2 fields e.g. the emacs mode
-- has support for tagging things as errors, adding links, etc.)
public export
record Properties where
  constructor MkProperties
  decor  : Maybe Decoration
  format : Maybe Formatting

export
mkDecor : Decoration -> Properties
mkDecor dec = MkProperties (Just dec) Nothing

export
mkFormat : Formatting -> Properties
mkFormat = MkProperties Nothing . Just

export
SExpable Properties where
  toSExp (MkProperties dec form)  = SExpList $ catMaybes
    [ toSExp <$> form
    , toSExp <$> dec
    ]

export
FromSExpable Properties where
  fromSExp (SExpList props) =
    case props of
      []  => Just $ MkProperties {decor = Nothing, format = Nothing}
      [prop] => do
        let Nothing = fromSExp prop
          | Just decor => Just $ mkDecor decor
        format <- fromSExp prop
        pure $ mkFormat format
      [prop1, prop2] => -- assume the same order as in toSExp
                        -- not part of the protocol though
        do let format = Just !(fromSExp prop1)
           let decor  = Just !(fromSExp prop2)
           pure $ MkProperties {format, decor}
      _ => Nothing
  fromSExp _ = Nothing


text:
module Main

main : IO ()
main = do
  printLn "Hello, world!"

max_stars_repo_name: steshaw/idris-elba-example

max_issues_repo_name: steshaw/idris-elba-example

max_forks_repo_name: steshaw/idris-elba-example


text:
module Main

main : IO()
main = putStrLn "hello world!"


text:
module Proofs.OrderTheory

import Common.Abbrev
import Common.Util
import Specifications.Order

%default total
%access export

rewriteReflexive : isReflexive rel -> (a,b : s) -> a = b -> rel a b
rewriteReflexive {rel} spec a b eq = rewriteRelation rel Refl eq (spec a)

orderContra : TotalOrderSpec leq -> (a,b : s) ->
  Not (leq a b) -> (leq b a, Not (a = b))
orderContra spec a b given = (o2, contraposition o3 given) where
  o1 : Either (leq a b) (leq b a)
  o1 = totalOrder spec a b
  o2 : leq b a
  o2 = o1 `butNotLeft` given
  o3 : a = b -> leq a b
  o3 = rewriteReflexive (reflexive (partialOrder spec)) a b

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Streaming.IO

import Streaming

||| A `Stream` of `getLine`s
export
stdinLn : HasIO m => Stream (Of String) m r
stdinLn = unfold (\_ => getLine >>= \line => pure (Right (line :> ()))) ()

||| `putStrLn` for each `String` in `Stream (Of String)`
export
stdoutLn : HasIO m => Stream (Of String) m r -> m r
stdoutLn = mapM_ putStrLn


text:
module Compiler.Scheme.Common

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline

import Core.Context
import Core.Name
import Core.TT

import Data.List
import Data.Vect

import System.Info

%default covering

export
firstExists : List String -> IO (Maybe String)
firstExists [] = pure Nothing
firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs

schString : String -> String
schString s = concatMap okchar (unpack s)
  where
    okchar : Char -> String
    okchar c = if isAlphaNum c || c =='_'
                  then cast c
                  else "C-" ++ show (cast {to=Int} c)

export
schUserName : UserName -> String
schUserName (Basic n) = "u--" ++ schString n
schUserName (Field n) = "rf--" ++ schString n
schUserName Underscore = "u--_"

export
schName : Name -> String
schName (NS ns (UN (Basic n))) = schString (showNSWithSep "-" ns) ++ "-" ++ schString n
schName (UN n) = schUserName n
schName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schName n
schName (MN n i) = schString n ++ "-" ++ show i
schName (PV n d) = "pat--" ++ schName n
schName (DN _ n) = schName n
schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
schName (Resolved i) = "fn--" ++ show i

export
schConstructor : (String -> String) -> Name -> Maybe Int -> List String -> String
schConstructor _ _ (Just t) args
    = "(vector " ++ show t ++ " " ++ showSep " " args ++ ")"
schConstructor schString n Nothing args
    = "(vector " ++ schString (show n) ++ " " ++ showSep " " args ++ ")"

export
schRecordCon : (String -> String) -> Name -> List String -> String
schRecordCon _ _ args = "(vector " ++ showSep " " args ++ ")"

||| Generate scheme for a plain function.
op : String -> List String -> String
op o args = "(" ++ o ++ " " ++ showSep " " args ++ ")"

||| Generate scheme for a boolean operation.
boolop : String -> List String -> String
boolop o args = "(or (and " ++ op o args ++ " 1) 0)"

add : Maybe IntKind -> String -> String -> String
add (Just $ Signed $ P n)   x y = op "bs+" [x, y, show (n-1)]
add (Just $ Unsigned n)     x y = op "bu+" [x, y, show n]
add _                       x y = op "+" [x, y]

sub : Maybe IntKind -> String -> String -> String
sub (Just $ Signed $ P n)   x y = op "bs-" [x, y, show (n-1)]
sub (Just $ Unsigned n)     x y = op "bu-" [x, y, show n]
sub _                       x y = op "-" [x, y]

mul : Maybe IntKind -> String -> String -> String
mul (Just $ Signed $ P n)   x y = op "bs*" [x, y, show (n-1)]
mul (Just $ Unsigned n)     x y = op "bu*" [x, y, show n]
mul _                       x y = op "*" [x, y]

div : Maybe IntKind -> String -> String -> String
div (Just $ Signed Unlimited) x y = op "quotient" [x, y]
div (Just $ Signed $ P n)     x y = op "bs/" [x, y, show (n-1)]
div (Just $ Unsigned n)       x y = op "bu/" [x, y, show n]
div _                         x y = op "/" [x, y]

shl : Maybe IntKind -> String -> String -> String
shl (Just $ Signed $ P n) x y = op "blodwen-bits-shl-signed"
                                   [x, y, show (n-1)]
shl (Just $ Unsigned n)   x y = op "blodwen-bits-shl" [x, y, show n]
shl _                     x y = op "blodwen-shl" [x, y]

constPrimitives : ConstantPrimitives
constPrimitives = MkConstantPrimitives {
    charToInt    = \k     => pure . charTo k
  , intToChar    = \_,x   => pure $ op "cast-int-char" [x]
  , stringToInt  = \k     => pure . strTo k
  , intToString  = \_,x   => pure $ op "number->string" [x]
  , doubleToInt  = \k     => pure . dblTo k
  , intToDouble  = \_,x   => pure $ op "exact->inexact" [x]
  , intToInt     = \k1,k2 => pure . intTo k1 k2
  }
  where charTo : IntKind -> String -> String
        charTo (Signed Unlimited) x = op "char->integer" [x]
        charTo (Signed $ P n)     x = op "cast-char-boundedInt" [x, show (n-1)]
        charTo (Unsigned n)       x = op "cast-char-boundedUInt" [x,show n]

        strTo : IntKind -> String -> String
        strTo (Signed Unlimited) x = op "cast-string-int" [x]
        strTo (Signed $ P n)     x = op "cast-string-boundedInt" [x, show (n-1)]
        strTo (Unsigned n)       x = op "cast-string-boundedUInt" [x,show n]

        dblTo : IntKind -> String -> String
        dblTo (Signed Unlimited) x = op "exact-truncate" [x]
        dblTo (Signed $ P n)     x = op "exact-truncate-boundedInt" [x, show (n-1)]
        dblTo (Unsigned n)       x = op "exact-truncate-boundedUInt" [x,show n]

        intTo : IntKind -> IntKind -> String -> String
        intTo _ (Signed Unlimited) x = x
        intTo (Signed m) (Signed $ P n) x =
          if P n >= m then x else op "blodwen-toSignedInt" [x,show (n-1)]

        -- Only if the precision of the target is greater
        -- than the one of the source, there is no need to cast.
        intTo (Unsigned m) (Signed $ P n) x =
          if n > m then x else op "blodwen-toSignedInt" [x,show (n-1)]

        intTo (Signed _) (Unsigned n) x = op "blodwen-toUnsignedInt" [x,show n]

        intTo (Unsigned m) (Unsigned n) x =
          if n >= m then x else op "blodwen-toUnsignedInt" [x,show n]

||| Generate scheme for a primitive function.
schOp : {0 arity : Nat} -> PrimFn arity -> Vect arity String -> Core String
schOp (Add ty) [x, y] = pure $ add (intKind ty) x y
schOp (Sub ty) [x, y] = pure $ sub (intKind ty) x y
schOp (Mul ty) [x, y] = pure $ mul (intKind ty) x y
schOp (Div ty) [x, y] = pure $ div (intKind ty) x y
schOp (Mod ty) [x, y] = pure $ op "remainder" [x, y]
schOp (Neg ty) [x] = pure $ op "-" [x]
schOp (ShiftL ty) [x, y] = pure $ shl (intKind ty) x y
schOp (ShiftR ty) [x, y] = pure $ op "blodwen-shr" [x, y]
schOp (BAnd ty) [x, y] = pure $ op "blodwen-and" [x, y]
schOp (BOr ty) [x, y] = pure $ op "blodwen-or" [x, y]
schOp (BXOr ty) [x, y] = pure $ op "blodwen-xor" [x, y]
schOp (LT CharType) [x, y] = pure $ boolop "char<?" [x, y]
schOp (LTE CharType) [x, y] = pure $ boolop "char<=?" [x, y]
schOp (EQ CharType) [x, y] = pure $ boolop "char=?" [x, y]
schOp (GTE CharType) [x, y] = pure $ boolop "char>=?" [x, y]
schOp (GT CharType) [x, y] = pure $ boolop "char>?" [x, y]
schOp (LT StringType) [x, y] = pure $ boolop "string<?" [x, y]
schOp (LTE StringType) [x, y] = pure $ boolop "string<=?" [x, y]
schOp (EQ StringType) [x, y] = pure $ boolop "string=?" [x, y]
schOp (GTE StringType) [x, y] = pure $ boolop "string>=?" [x, y]
schOp (GT StringType) [x, y] = pure $ boolop "string>?" [x, y]
schOp (LT ty) [x, y] = pure $ boolop "<" [x, y]
schOp (LTE ty) [x, y] = pure $ boolop "<=" [x, y]
schOp (EQ ty) [x, y] = pure $ boolop "=" [x, y]
schOp (GTE ty) [x, y] = pure $ boolop ">=" [x, y]
schOp (GT ty) [x, y] = pure $ boolop ">" [x, y]
schOp StrLength [x] = pure $ op "string-length" [x]
schOp StrHead [x] = pure $ op "string-ref" [x, "0"]
schOp StrTail [x] = pure $ op "substring" [x, "1", op "string-length" [x]]
schOp StrIndex [x, i] = pure $ op "string-ref" [x, i]
schOp StrCons [x, y] = pure $ op "string-cons" [x, y]
schOp StrAppend [x, y] = pure $ op "string-append" [x, y]
schOp StrReverse [x] = pure $ op "string-reverse" [x]
schOp StrSubstr [x, y, z] = pure $ op "string-substr" [x, y, z]

-- `e` is Euler's number, which approximates to: 2.718281828459045
schOp DoubleExp [x] = pure $ op "flexp" [x] -- Base is `e`. Same as: `pow(e, x)`
schOp DoubleLog [x] = pure $ op "fllog" [x] -- Base is `e`.
schOp DoublePow [x, y] = pure $ op "expt" [x, y]
schOp DoubleSin [x] = pure $ op "flsin" [x]
schOp DoubleCos [x] = pure $ op "flcos" [x]
schOp DoubleTan [x] = pure $ op "fltan" [x]
schOp DoubleASin [x] = pure $ op "flasin" [x]
schOp DoubleACos [x] = pure $ op "flacos" [x]
schOp DoubleATan [x] = pure $ op "flatan" [x]
schOp DoubleSqrt [x] = pure $ op "flsqrt" [x]
schOp DoubleFloor [x] = pure $ op "flfloor" [x]
schOp DoubleCeiling [x] = pure $ op "flceiling" [x]

schOp (Cast DoubleType StringType)  [x] = pure $ op "number->string" [x]
schOp (Cast CharType StringType)    [x] = pure $ op "string" [x]
schOp (Cast StringType DoubleType)  [x] = pure $ op "cast-string-double" [x]

schOp (Cast from to)                [x] = castInt constPrimitives from to x

schOp BelieveMe [_,_,x] = pure x
schOp Crash [_,msg] = pure $ "(blodwen-error-quit (string-append \"ERROR: \" " ++ msg ++ "))"

||| Extended primitives for the scheme backend, outside the standard set of primFn
public export
data ExtPrim = NewIORef | ReadIORef | WriteIORef
             | NewArray | ArrayGet | ArraySet
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
             | OnCollect
             | OnCollectAny
             | MakeFuture
             | Unknown Name

export
Show ExtPrim where
  show NewIORef = "NewIORef"
  show ReadIORef = "ReadIORef"
  show WriteIORef = "WriteIORef"
  show NewArray = "NewArray"
  show ArrayGet = "ArrayGet"
  show ArraySet = "ArraySet"
  show GetField = "GetField"
  show SetField = "SetField"
  show VoidElim = "VoidElim"
  show SysOS = "SysOS"
  show SysCodegen = "SysCodegen"
  show OnCollect = "OnCollect"
  show OnCollectAny = "OnCollectAny"
  show MakeFuture = "MakeFuture"
  show (Unknown n) = "Unknown " ++ show n

||| Match on a user given name to get the scheme primitive
toPrim : Name -> ExtPrim
toPrim pn@(NS _ n)
    = cond [(n == UN (Basic "prim__newIORef"), NewIORef),
            (n == UN (Basic "prim__readIORef"), ReadIORef),
            (n == UN (Basic "prim__writeIORef"), WriteIORef),
            (n == UN (Basic "prim__newArray"), NewArray),
            (n == UN (Basic "prim__arrayGet"), ArrayGet),
            (n == UN (Basic "prim__arraySet"), ArraySet),
            (n == UN (Basic "prim__getField"), GetField),
            (n == UN (Basic "prim__setField"), SetField),
            (n == UN (Basic "void"), VoidElim), -- DEPRECATED. TODO: remove when bootstrap has been updated
            (n == UN (Basic "prim__void"), VoidElim),
            (n == UN (Basic "prim__os"), SysOS),
            (n == UN (Basic "prim__codegen"), SysCodegen),
            (n == UN (Basic "prim__onCollect"), OnCollect),
            (n == UN (Basic "prim__onCollectAny"), OnCollectAny),
            (n == UN (Basic "prim__makeFuture"), MakeFuture)
            ]
           (Unknown pn)
toPrim pn = Unknown pn

export
mkWorld : String -> String
mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes

schConstant : (String -> String) -> Constant -> String
schConstant _ (I x) = show x
schConstant _ (I8 x) = show x
schConstant _ (I16 x) = show x
schConstant _ (I32 x) = show x
schConstant _ (I64 x) = show x
schConstant _ (BI x) = show x
schConstant _ (B8 x) = show x
schConstant _ (B16 x) = show x
schConstant _ (B32 x) = show x
schConstant _ (B64 x) = show x
schConstant schString (Str x) = schString x
schConstant _ (Ch x)
   = if (the Int (cast x) >= 32 && the Int (cast x) < 127)
        then "#\\" ++ cast x
        else "(integer->char " ++ show (the Int (cast x)) ++ ")"
schConstant _ (Db x) = show x
schConstant _ WorldVal = "#f"
schConstant _ IntType = "#t"
schConstant _ Int8Type = "#t"
schConstant _ Int16Type = "#t"
schConstant _ Int32Type = "#t"
schConstant _ Int64Type = "#t"
schConstant _ IntegerType = "#t"
schConstant _ Bits8Type = "#t"
schConstant _ Bits16Type = "#t"
schConstant _ Bits32Type = "#t"
schConstant _ Bits64Type = "#t"
schConstant _ StringType = "#t"
schConstant _ CharType = "#t"
schConstant _ DoubleType = "#t"
schConstant _ WorldType = "#t"

schCaseDef : Maybe String -> String
schCaseDef Nothing = ""
schCaseDef (Just tm) = "(else " ++ tm ++ ")"

export
schArglist : List Name -> String
schArglist [] = ""
schArglist [x] = schName x
schArglist (x :: xs) = schName x ++ " " ++ schArglist xs

mutual
  used : Name -> NamedCExp -> Bool
  used n (NmLocal fc n') = n == n'
  used n (NmRef _ _) = False
  used n (NmLam _ _ sc) = used n sc
  used n (NmLet _ _ v sc) = used n v || used n sc
  used n (NmApp _ f args) = used n f || any (used n) args
  used n (NmCon _ _ _ _ args) = any (used n) args
  used n (NmOp _ _ args) = any (used n) (toList args)
  used n (NmExtPrim _ _ args) = any (used n) args
  used n (NmForce _ _ t) = used n t
  used n (NmDelay _ _ t) = used n t
  used n (NmConCase _ sc alts def)
      = used n sc || any (usedCon n) alts
            || maybe False (used n) def
  used n (NmConstCase _ sc alts def)
      = used n sc || any (usedConst n) alts
            || maybe False (used n) def
  used n _ = False

  usedCon : Name -> NamedConAlt -> Bool
  usedCon n (MkNConAlt _ _ _ _ sc) = used n sc

  usedConst : Name -> NamedConstAlt -> Bool
  usedConst n (MkNConstAlt _ sc) = used n sc

var : NamedCExp -> Bool
var (NmLocal _ _) = True
var _ = False

parameters (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String,
            schString : String -> String)
  showTag : Name -> Maybe Int -> String
  showTag n (Just i) = show i
  showTag n Nothing = schString (show n)

  mutual
    schConAlt : Int -> String -> NamedConAlt -> Core String
    schConAlt i target (MkNConAlt n ci tag args sc)
        = pure $ "((" ++ showTag n tag ++ ") "
                      ++ bindArgs 1 args !(schExp i sc) ++ ")"
      where
        bindArgs : Int -> (ns : List Name) -> String -> String
        bindArgs i [] body = body
        bindArgs i (n :: ns) body
            = if used n sc
                 then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
                    ++ bindArgs (i + 1) ns body ++ ")"
                 else bindArgs (i + 1) ns body

    schConUncheckedAlt : Int -> String -> NamedConAlt -> Core String
    schConUncheckedAlt i target (MkNConAlt n ci tag args sc)
        = pure $ bindArgs 1 args !(schExp i sc)
      where
        bindArgs : Int -> (ns : List Name) -> String -> String
        bindArgs i [] body = body
        bindArgs i (n :: ns) body
            = if used n sc
                 then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
                    ++ bindArgs (i + 1) ns body ++ ")"
                 else bindArgs (i + 1) ns body

    schConstAlt : Int -> String -> NamedConstAlt -> Core String
    schConstAlt i target (MkNConstAlt c exp)
        = pure $ "((equal? " ++ target ++ " " ++ schConstant schString c ++ ") " ++ !(schExp i exp) ++ ")"

    -- oops, no traverse for Vect in Core
    schArgs : Int -> Vect n NamedCExp -> Core (Vect n String)
    schArgs i [] = pure []
    schArgs i (arg :: args) = pure $ !(schExp i arg) :: !(schArgs i args)

    schCaseTree : Int -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp ->
                  Core String
    schCaseTree i sc [] def
        = do tcode <- schExp (i+1) sc
             defc <- maybe (pure "'erased") (schExp i) def
             let n = "sc" ++ show i
             if var sc
                then pure defc
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) "
                             ++ defc ++ ")"
    schCaseTree i sc [alt] Nothing
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             if var sc
                then pure !(schConUncheckedAlt (i+1) tcode alt)
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++
                        !(schConUncheckedAlt (i+1) n alt) ++ ")"
    schCaseTree i sc alts Nothing
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             if var sc
                then pure $ "(case (vector-ref " ++ tcode ++ " 0) "
                       ++ !(showAlts tcode alts) ++
                       ")"
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) "
                       ++ !(showAlts n alts) ++
                       "))"
      where
        showAlts : String -> List NamedConAlt -> Core String
        showAlts n [] = pure ""
        showAlts n [alt]
           = pure $ "(else " ++ !(schConUncheckedAlt (i + 1) n alt) ++ ")"
        showAlts n (alt :: alts)
           = pure $ !(schConAlt (i + 1) n alt) ++ " " ++
                    !(showAlts n alts)
    schCaseTree i sc alts def
        = do tcode <- schExp (i+1) sc
             defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
             let n = "sc" ++ show i
             if var sc
                then pure $ "(case (vector-ref " ++ tcode ++ " 0) "
                               ++ showSep " " !(traverse (schConAlt (i+1) tcode) alts)
                               ++ schCaseDef defc ++ ")"
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (case (vector-ref " ++ n ++ " 0) "
                       ++ showSep " " !(traverse (schConAlt (i+1) n) alts)
                       ++ schCaseDef defc ++ "))"

    schRecordCase : Int -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp ->
                    Core String
    schRecordCase i sc [] _ = pure "#f" -- suggests empty case block!
    schRecordCase i sc (alt :: _) _
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             if var sc
                then getAltCode tcode alt
                else do alt' <- getAltCode n alt
                        pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++
                                     alt' ++ ")"
      where
        bindArgs : Int -> String -> (ns : List Name) -> String ->
                   NamedCExp -> String
        bindArgs i target [] body sc = body
        bindArgs i target (n :: ns) body sc
            = if used n sc
                 then "(let ((" ++ schName n ++ " " ++ "(vector-ref " ++ target ++ " " ++ show i ++ "))) "
                    ++ bindArgs (i + 1) target ns body sc ++ ")"
                 else bindArgs (i + 1) target ns body sc

        getAltCode : String -> NamedConAlt -> Core String
        getAltCode n (MkNConAlt _ _ _ args sc)
            = pure $ bindArgs 0 n args !(schExp i sc) sc

    schListCase : Int -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp ->
                  Core String
    schListCase i sc alts def
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             defc <- maybe (pure Nothing)
                           (\v => pure (Just !(schExp (i + 1) v))) def
             nil <- getNilCode alts
             if var sc
                then do cons <- getConsCode tcode alts
                        pure $ buildCase tcode nil cons defc
                else do cons <- getConsCode n alts
                        pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++
                            buildCase n nil cons defc ++ ")"
      where
        buildCase : String ->
                    Maybe String -> Maybe String -> Maybe String ->
                    String
        buildCase n (Just nil) (Just cons) _
            = "(if (null? " ++ n ++ ") " ++ nil ++ " " ++ cons ++ ")"
        buildCase n (Just nil) Nothing Nothing = nil
        buildCase n Nothing (Just cons) Nothing = cons
        buildCase n (Just nil) Nothing (Just def)
            = "(if (null? " ++ n ++ ") " ++ nil ++ " " ++ def ++ ")"
        buildCase n Nothing (Just cons) (Just def)
            = "(if (null? " ++ n ++ ") " ++ def ++ " " ++ cons ++ ")"
        buildCase n Nothing Nothing (Just def) = def
        buildCase n Nothing Nothing Nothing = "#f"

        getNilCode : List NamedConAlt -> Core (Maybe String)
        getNilCode [] = pure Nothing
        getNilCode (MkNConAlt _ NIL _ _ sc :: _)
            = pure (Just !(schExp (i + 1) sc))
        getNilCode (_ :: xs) = getNilCode xs

        getConsCode : String -> List NamedConAlt -> Core (Maybe String)
        getConsCode n [] = pure Nothing
        getConsCode n (MkNConAlt _ CONS _ [x,xs] sc :: _)
            = do sc' <- schExp (i + 1) sc
                 pure $ Just $ bindArgs [(x, "car"), (xs, "cdr")] sc'
          where
            bindArgs : (ns : List (Name, String)) -> String -> String
            bindArgs [] body = body
            bindArgs ((x, get) :: ns) body
                = if used x sc
                     then "(let ((" ++ schName x ++ " " ++ "(" ++ get ++ " " ++ n ++ "))) "
                        ++ bindArgs ns body ++ ")"
                     else bindArgs ns body
        getConsCode x (_ :: xs) = getConsCode x xs

    schMaybeCase : Int -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp ->
                   Core String
    schMaybeCase i sc alts def
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             defc <- maybe (pure Nothing)
                           (\v => pure (Just !(schExp (i + 1) v))) def
             nothing <- getNothingCode alts
             if var sc
                then do just <- getJustCode tcode alts
                        pure $ buildCase tcode nothing just defc
                else do just <- getJustCode n alts
                        pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) " ++
                            buildCase n nothing just defc ++ ")"
      where
        buildCase : String ->
                    Maybe String -> Maybe String -> Maybe String ->
                    String
        buildCase n (Just nothing) (Just just) _
            = "(if (null? " ++ n ++ ") " ++ nothing ++ " " ++ just ++ ")"
        buildCase n (Just nothing) Nothing Nothing = nothing
        buildCase n Nothing (Just just) Nothing = just
        buildCase n (Just nothing) Nothing (Just def)
            = "(if (null? " ++ n ++ ") " ++ nothing ++ " " ++ def ++ ")"
        buildCase n Nothing (Just just) (Just def)
            = "(if (null? " ++ n ++ ") " ++ def ++ " " ++ just ++ ")"
        buildCase n Nothing Nothing (Just def) = def
        buildCase n Nothing Nothing Nothing = "#f"

        getNothingCode : List NamedConAlt -> Core (Maybe String)
        getNothingCode [] = pure Nothing
        getNothingCode (MkNConAlt _ NOTHING _ _ sc :: _)
            = pure (Just !(schExp (i + 1) sc))
        getNothingCode (_ :: xs) = getNothingCode xs

        getJustCode : String -> List NamedConAlt -> Core (Maybe String)
        getJustCode n [] = pure Nothing
        getJustCode n (MkNConAlt _ JUST _ [x] sc :: _)
            = do sc' <- schExp (i + 1) sc
                 pure $ Just $ bindArg x sc'
          where
            bindArg : Name -> String -> String
            bindArg x body
                = if used x sc
                     then "(let ((" ++ schName x ++ " " ++ "(unbox " ++ n ++ "))) "
                        ++ body ++ ")"
                     else body
        getJustCode x (_ :: xs) = getJustCode x xs

    export
    schExp : Int -> NamedCExp -> Core String
    schExp i (NmLocal fc n) = pure $ schName n
    schExp i (NmRef fc n) = pure $ schName n
    schExp i (NmLam fc x sc)
       = do sc' <- schExp i  sc
            pure $ "(lambda (" ++ schName x ++ ") " ++ sc' ++ ")"
    schExp i (NmLet fc x val sc)
       = do val' <- schExp i val
            sc' <- schExp i sc
            pure $ "(let ((" ++ schName x ++ " " ++ val' ++ ")) " ++ sc' ++ ")"
    schExp i (NmApp fc x [])
        = pure $ "(" ++ !(schExp i x) ++ ")"
    schExp i (NmApp fc x args)
        = pure $ "(" ++ !(schExp i x) ++ " " ++ showSep " " !(traverse (schExp i) args) ++ ")"
    schExp i (NmCon fc _ NIL tag []) = pure $ "'()"
    schExp i (NmCon fc _ NIL tag _) = throw (InternalError "Bad NIL")
    schExp i (NmCon fc _ CONS tag [x, xs])
        = do x' <- schExp i x
             xs' <- schExp i xs
             pure $ "(cons " ++ x' ++ " " ++ xs' ++ ")"
    schExp i (NmCon fc _ CONS tag _) = throw (InternalError "Bad CONS")
    schExp i (NmCon fc _ NOTHING tag []) = pure $ "'()"
    schExp i (NmCon fc _ NOTHING tag _) = throw (InternalError "Bad NOTHING")
    schExp i (NmCon fc _ JUST tag [x])
        = do x' <- schExp i x
             pure $ "(box " ++ x' ++ ")"
    schExp i (NmCon fc _ JUST tag _) = throw (InternalError "Bad JUST")
    schExp i (NmCon fc x RECORD tag args)
        = pure $ schRecordCon schString x !(traverse (schExp i) args)
    schExp i (NmCon fc x ci tag args)
        = pure $ schConstructor schString x tag !(traverse (schExp i) args)
    schExp i (NmOp fc op args)
        = schOp op !(schArgs i args)
    schExp i (NmExtPrim fc p args)
        = schExtPrim i (toPrim p) args
    schExp i (NmForce fc lr t) = pure $ "(" ++ !(schExp i t) ++ ")"
    schExp i (NmDelay fc lr t) = pure $ "(lambda () " ++ !(schExp i t) ++ ")"
    schExp i (NmConCase fc sc alts def)
        = cond [(recordCase alts, schRecordCase i sc alts def),
                (maybeCase alts, schMaybeCase i sc alts def),
                (listCase alts, schListCase i sc alts def)]
                -- probably more to come here...
                (schCaseTree i sc alts def)
      where
        listCase : List NamedConAlt -> Bool
        listCase (MkNConAlt _ NIL _ _ _ :: _) = True
        listCase (MkNConAlt _ CONS _ _ _ :: _) = True
        listCase _ = False

        maybeCase : List NamedConAlt -> Bool
        maybeCase (MkNConAlt _ NOTHING _ _ _ :: _) = True
        maybeCase (MkNConAlt _ JUST _ _ _ :: _) = True
        maybeCase _ = False

        recordCase : List NamedConAlt -> Bool
        recordCase (MkNConAlt _ RECORD _ _ _ :: _) = True
        recordCase _ = False

    schExp i (NmConstCase fc sc alts Nothing)
        = do tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             if var sc
                then pure $ "(cond "
                          ++ !(showConstAlts tcode alts)
                          ++ ")"
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "
                          ++ !(showConstAlts n alts)
                          ++ "))"
      where
        showConstAlts : String -> List NamedConstAlt -> Core String
        showConstAlts n [] = pure ""
        showConstAlts n [MkNConstAlt c exp]
           = pure $ "(else " ++ !(schExp (i + 1) exp) ++ ")"
        showConstAlts n (alt :: alts)
           = pure $ !(schConstAlt (i + 1) n alt) ++ " " ++
                    !(showConstAlts n alts)
    schExp i (NmConstCase fc sc alts def)
        = do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
             tcode <- schExp (i+1) sc
             let n = "sc" ++ show i
             if var sc
                then pure $ "(cond "
                          ++ showSep " " !(traverse (schConstAlt (i+1) tcode) alts)
                          ++ schCaseDef defc ++ ")"
                else pure $ "(let ((" ++ n ++ " " ++ tcode ++ ")) (cond "
                          ++ showSep " " !(traverse (schConstAlt (i+1) n) alts)
                          ++ schCaseDef defc ++ "))"
    schExp i (NmPrimVal fc c) = pure $ schConstant schString c
    schExp i (NmErased fc) = pure "'erased"
    schExp i (NmCrash fc msg) = pure $ "(blodwen-error-quit " ++ show msg ++ ")"

  fileOp : String -> String
  fileOp op = "(blodwen-file-op (lambda () " ++ op ++ "))"

  -- External primitives which are common to the scheme codegens (they can be
  -- overridden)
  export
  schExtCommon : Int -> ExtPrim -> List NamedCExp -> Core String
  schExtCommon i NewIORef [_, val, world]
      = pure $ mkWorld $ "(box " ++ !(schExp i val) ++ ")"
  schExtCommon i ReadIORef [_, ref, world]
      = pure $ mkWorld $ "(unbox " ++ !(schExp i ref) ++ ")"
  schExtCommon i WriteIORef [_, ref, val, world]
      = pure $ mkWorld $ "(set-box! "
                           ++ !(schExp i ref) ++ " "
                           ++ !(schExp i val) ++ ")"
  schExtCommon i NewArray [_, size, val, world]
      = pure $ mkWorld $ "(make-vector " ++ !(schExp i size) ++ " "
                                         ++ !(schExp i val) ++ ")"
  schExtCommon i ArrayGet [_, arr, pos, world]
      = pure $ mkWorld $ "(vector-ref " ++ !(schExp i arr) ++ " "
                                        ++ !(schExp i pos) ++ ")"
  schExtCommon i ArraySet [_, arr, pos, val, world]
      = pure $ mkWorld $ "(vector-set! " ++ !(schExp i arr) ++ " "
                                         ++ !(schExp i pos) ++ " "
                                         ++ !(schExp i val) ++ ")"
  schExtCommon i VoidElim [_, _]
      = pure "(display \"Error: Executed 'void'\")"
  schExtCommon i SysOS []
      = pure $ "(blodwen-os)"
  schExtCommon i (Unknown n) args
      = throw (InternalError ("Can't compile unknown external primitive " ++ show n))
  schExtCommon i prim args
      = throw (InternalError ("Badly formed external primitive " ++ show prim
                                ++ " " ++ show args))

  schDef : {auto c : Ref Ctxt Defs} ->
           Name -> NamedDef -> Core String
  schDef n (MkNmFun [] exp)
     = pure $ "(define " ++ schName !(getFullName n) ++ "(blodwen-lazy (lambda () "
                      ++ !(schExp 0 exp) ++ ")))\n"
  schDef n (MkNmFun args exp)
     = pure $ "(define " ++ schName !(getFullName n) ++ " (lambda (" ++ schArglist args ++ ") "
                      ++ !(schExp 0 exp) ++ "))\n"
  schDef n (MkNmError exp)
     = pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 exp) ++ ")\n"
  schDef n (MkNmForeign _ _ _) = pure "" -- compiled by specific back end
  schDef n (MkNmCon t a _) = pure "" -- Nothing to compile here

-- Convert the name to scheme code
-- (There may be no code generated, for example if it's a constructor)
export
getScheme : {auto c : Ref Ctxt Defs} ->
            (schExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String) ->
            (schString : String -> String) ->
            (Name, FC, NamedDef) -> Core String
getScheme schExtPrim schString (n, fc, d)
    = schDef schExtPrim schString n d


text:
module UnivalenceFromScratch

-- Based on http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html

data Sigma : (x : Type) -> (y : x -> Type) -> Type where
  Pair : (a : x) -> y a -> Sigma x y

-- We need something like --without-K
data Id : {x : Type} -> x -> x -> Type where
  Refl : (a : x) -> Id a a

J : {x : Type} ->
    (alpha : (a, b : x) -> Id a b -> Type) ->
    ((a : x) -> alpha a a (Refl a)) ->
    (a, b : x) -> (p : Id a b) -> alpha a b p
J alpha f b b (Refl b) = f b

isSingleton : Type -> Type
isSingleton x = Sigma x (\a => (b : x) -> Id a b)

fiber : {x, y : Type} -> (x -> y) -> y -> Type
fiber {x} f b = Sigma x (\a => Id (f a) b)

isEquiv : {x, y : Type} -> (x -> y) -> Type
isEquiv {y} f = (b : y) -> isSingleton (fiber f b)

Eq : Type -> Type -> Type
Eq x y = Sigma (x -> y) (\f => isEquiv f)

singletonType : {x : Type} -> x -> Type
singletonType {x} a = Sigma x (\b => Id b a)

eta : {x : Type} -> (a : x) -> singletonType a
eta a = Pair a (Refl a)

singletonTypesAreSingletons : {x : Type} -> (a : x) -> isSingleton (singletonType a)
singletonTypesAreSingletons = h
  where
    alpha : (b, a : x) -> Id b a -> Type
    alpha b a p = Id (eta a) (Pair b p)
    f : (a : x) -> alpha a a (Refl a)
    f a = Refl (eta a)
    phi : (b, a : x) -> (p : Id b a) -> Id (eta a) (Pair b p)
    phi = J alpha f
    g : (a : x) -> (sigma : singletonType a) -> Id (eta a) sigma
    g a (Pair b p) = phi b a p
    h : (a : x) -> Sigma (singletonType a) (\b => (sigma : singletonType a) -> Id b sigma)
    h a = Pair (eta a) (g a)

id : (x : Type) -> x -> x
id x a = a

idIsEquiv : (x : Type) -> isEquiv (id x)
idIsEquiv x = g
 where
  g : (a : x) -> isSingleton (fiber (id x) a)
  g = singletonTypesAreSingletons

IdToEq : (x, y : Type) -> Id x y -> Eq x y
IdToEq = J alpha f
  where
    alpha : (x, y : Type) -> Id x y -> Type
    alpha x y p = Eq x y
    f : (x : Type) -> alpha x x (Refl x)
    f x = Pair (id x) (idIsEquiv x)

isUnivalent : Type
isUnivalent = (x, y : Type) -> isEquiv (IdToEq x y)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module basic025

-- converting data from strings at runtime so as to prevent the
-- compiler of eliding the calls to atan2 via constant folding
input : List (String, String, String)
input = [
  ("atan2", " 1", " 1"),
  ("atan2", "-1", " 1"),
  ("atan2", " 1", "-1"),
  ("atan2", "-1", "-1"),
  ("atan2", " 0", " 1"),
  ("atan2", " 1", " 0")
]

round : Double -> Double
round x = let y = x * 1e10
              z = if y < 0 then (ceiling y) else (floor y)
          in z / 1e10

-- the input file is read at runtime so as to prevent the compiler of
-- eliding the calls to atan2 via constant folding
namespace Main
  main : IO ()
  main = traverse_ evalInput input
    where
      evalInput : (String, String, String) -> IO ()
      evalInput ("atan2", y, x) = printLn $ round $ atan2 (cast y) (cast x)
      evalInput _ = putStrLn $ "Could not eval line"


text:
module Main

main : IO ()
main = putStrLn "Hello, Idris world!"

mainHole : IO ()
mainHole = putStrLn ?greeting

mainConvert : IO ()
mainConvert = putStrLn (cast 'x')

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
-- build instructions:
-- $ cd calc && idris2 --build calc.ipkg && idris2 --install calc.ipkg
-- $ cd .. && idris2 --package calc CalcClient.idr
---
module Main

import Data.Strings
import Calc

%default total

readNum : HasIO io => io (Maybe Int)
readNum = do putStr "Enter a number: "
             ns <- getLine
             case all isDigit (unpack ns) of
                  False => pure Nothing
                  True => pure $ Just (cast ns)

main : HasIO io => io ()
main = do Just n <- readNum
              | Nothing => do putStrLn "Error: first number is invalid"
          Just m <- readNum
              | Nothing => do putStrLn "Error: second number is invalid"
          let sum = addInts n m
          let diff = subInts n m
          let prod = mulInts n m
          let quot = divInts n m
          putStrLn $ "Sum = " ++ show sum
                      ++ ", Diff = " ++ show diff
                      ++ ", Prod = " ++ show prod
                      ++ ", Quot = " ++ show quot

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Test.SemVar.SatTest

import IdrTest.Test
import IdrTest.Expectation

import Data.List
import Data.Maybe
import Extra.List

import SemVar
import SemVar.Data
import SemVar.Parser
import SemVar.Sat

satSpecs : List (String, List (List String, (List (String, (List (List String, String))))), List (List String, String), Either String (List (List String, String)))
satSpecs =
  [
    (
      "Simple Dep Test",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [])]
        )
      ],
      [ (["Dep1"], "^1.2.3")
      , (["Dep2"], "^3.0.0")
      ],
      Right [(["Dep1"], "1.2.3"), (["Dep2"], "3.0.0")]
    ),
    (
      "Simple Sub-Dep Test",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [])]
        )
      ],
      [ (["Dep1"], "^1.2.3")
      ],
      Right [(["Dep1"], "1.2.3"), (["Dep2"], "3.0.0")]
    ),
    (
      "Simple Sub-Sub-Dep Test",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [(["Dep3"], "=5.0.0")])]
        )
      , (["Dep3"],
          [ ("5.0.0", [])]
        )
      ],
      [ (["Dep1"], "^1.2.3")
      ],
      Right [(["Dep1"], "1.2.3"), (["Dep2"], "3.0.0"), (["Dep3"], "5.0.0")]
    ),
    -- This is where we can't just rely on head anymore
    (
      "More complex test where we force Dep2 and have to match Dep1",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [])
          , ("3.1.0", [])
          ]
        )
      ],
      [ (["Dep1"], ">=0")
      , (["Dep2"], "=3.1.0")
      ],
      Right [(["Dep1"], "2.0.0"), (["Dep2"], "3.1.0")]
    ),
    (
      "Mutual constraints",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [(["Dep1"], ">=0")])
          ]
        )
      ],
      [ (["Dep1"], ">=0")
      ],
      Right [(["Dep1"], "1.2.3"), (["Dep2"], "3.0.0")]
    ),
    (
      "Mutual incompatible constraints",
      [ (["Dep1"],
          [ ("1.0.0", [(["Dep2"], "=4.0.0")])
          , ("2.0.0", [(["Dep2"], "=3.0.0")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [(["Dep1"], "=1.0.0")])
          , ("4.0.0", [(["Dep1"], "=2.0.0")])
          ]
        )
      ],
      [ (["Dep1"], ">=0")
      ],
      Left "Package [\"Dep1\"] req =1.0.0 is incompatible"
    ),
    (
      "Simple Failing Dep",
      [ (["Dep1"],
          [ ("1.2.3", [(["Dep2"], "~3.0.0")])
          , ("1.2.4", [(["Dep2"], "~3.0.0")])
          , ("2.0.0", [(["Dep2"], "~3.1")])
          ]
        )
      , (["Dep2"],
          [ ("3.0.0", [])]
        )
      ],
      [ (["Dep1"], "^1.2.3")
      , (["Dep2"], "^4.0.0")
      ],
      Left "Cannot match [\"Dep2\"] req >=4.0.0 <5.0.0"
    )
  ]

mapSnd : (b -> c) -> List (a, b) -> List (a, c)
mapSnd f =
  map (\(x, y) => (x, f y))

liftTuple : (a, Maybe b) -> Maybe (a, b)
liftTuple (a, Just x) = Just (a, x)
liftTuple _ = Nothing

collapseEither : Either a (Maybe b) -> Maybe (Either a b)
collapseEither (Left x) = Just (Left x)
collapseEither (Right (Just y)) = Just (Right y)
collapseEither (Right Nothing) = Nothing

makeVersionNodes : List String -> List (String, List (List String, String)) -> Maybe (List (List String, Version, List (List String, Requirement)))
makeVersionNodes name versions =
  collapse $ map (mkVersion name) versions
  where
    mkVersion : List String -> (String, List (List String, String)) -> Maybe VersionNode
    mkVersion name (versionStr, reqStrList) =
      do
        version <- parseVersion versionStr
        reqs <- collapse $ map liftTuple $ mapSnd parseRequirement reqStrList
        pure (name, version, reqs)

||| TODO: Move to Extra
map2 : Monad m => (a -> b -> c) -> m a -> m b -> m c
map2 f x y =
  join $ map (\x' => map (\y' => f x' y') y) x

map3 : Monad m => (a -> b -> c -> d) -> m a -> m b -> m c -> m d
map3 f x y z =
  (map2 f x y) <*> z

compareBy : Ord b => (a -> b) -> (a -> a -> Ordering)
compareBy f =
  (\x, y => compare (f x) (f y))

export
suite : Test
suite =
  let
    satTests = map (\(name, versionSpec, reqSpec, expSpec) =>
      let
        mVersionNodes : Maybe (List VersionNode)
        mVersionNodes = foldl (\mAcc, (dep, versions) =>
            do
              acc <- mAcc
              x <- makeVersionNodes dep versions
              pure (x ++ acc)
          ) (the (Maybe (List VersionNode)) (Just [])) versionSpec

        mReqs : Maybe (List (List String, Requirement))
        mReqs = collapse $ map (\(dep, reqStr) =>
            map (\req => (dep, req)) $ parseRequirement reqStr
          ) reqSpec

        maybeParseDepReq : (List String, String) -> Maybe (List String, Version)
        maybeParseDepReq (dep, verStr) =
          map (\vers => (dep, vers)) $ parseVersion verStr

        mExp : Either String (Maybe (List (List String, Version)))
        mExp = map collapse (map (map maybeParseDepReq) expSpec)

        sort : Either String (List (List String, Version)) -> Either String (List (List String, Version))
        sort =
          map (sortBy (compareBy fst))
      in
        test name (\_ =>
          let
            t = map3 (\versionNodes, reqs, exp =>
              assertEq (sort $ satisfyAll versionNodes reqs) exp
              ) mVersionNodes mReqs (map sort $ collapseEither mExp)
            in
              fromMaybe (Just "Invalid set-up for test") t
        )
      ) satSpecs
  in
    describe "Sat Tests" satTests


text:
module Greet

%default total

greet : HasIO io => io ()
greet = do putStr "What is your name? "
           name <- getLine
           putStrLn $ "Nice to meet you again, " ++ name


text:
-- ------------------------------------------------------------------------ [  ]
-- Common things
-- --------------------------------------------------------------------- [ EOH ]
module Greeter.Common

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

import System.Protocol

import RFC.Greeter

%access public

GreeterES : List EFFECT
GreeterES = [STDIO, STATE Int]

GreeterFrontend : GreeterProto () -> Type -> Type
GreeterFrontend p t = Process p 'Alice [] GreeterES t

GreeterBackend : GreeterProto () -> Type -> Type
GreeterBackend p t = Process p 'Bob [] GreeterES t

-- --------------------------------------------------------------------- [ 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 Dbcritic.Interface

export
formatMessage : Int -> String -> List String -> List String -> String
formatMessage index description problems solutions =
    "\x1B[34mISSUE #" ++ show index ++ ": " ++ description ++ "\x1B[0m\n" ++
    "\n" ++
    "\x1B[31m  If you do not solve this issue, you will encounter the following problems:\x1B[0m\n" ++
    "\n" ++
    concatMap (\p => "    \x1B[31m• " ++ p ++ "\x1B[0m\n") (problems) ++
    "\n" ++
    "\x1B[32m  You can solve this issue by taking one of the following measures:\x1B[0m\n" ++
    "\n" ++
    concatMap (\p => "    \x1B[32m• " ++ p ++ "\x1B[0m\n") (solutions)

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
-- ------------------------------------------------------------------------ [  ]
-- Client Process
-- --------------------------------------------------------------------- [ EOH ]
module Greeter.Frontend

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

import System.Protocol

import RFC.Greeter
import Greeter.Common

%access public

-- ---------------------------------------------------------- [ Greeter Client ]

||| Get commands from the user.
private
readCmd : { [STDIO] } Eff Command
readCmd = case (process !getStr) of
    Just cmd => return cmd
    Nothing => do
      putStrLn "Bad command"
      putStr "Try again: "
      readCmd
  where
    process : String -> Maybe Command
    process str = case words (trim str) of
      [":greet", str] => Just (GreetMe str)
      [":?"]          => Just Help
      [":help"]       => Just Help
      [":q"]          => Just Quit
      _ => Nothing

||| Process commands and interact with the backend.
private
covering
clientBody : (proc : PID) -> GreeterFrontend (gBody) ()
clientBody proc = do
     setChan 'Bob proc
     putStrLn !(recvFrom 'Bob)
     cmd <- readCmd
     sendTo 'Bob cmd
     case cmd of
       GreetMe str => do
         putStrLn !(recvFrom 'Bob)
         dropChan 'Bob
         rec (clientBody proc)

       Help => do
         putStrLn !(recvFrom 'Bob)
         dropChan 'Bob
         rec (clientBody proc)

       Quit => do
         dropChan 'Bob
         return ()

||| A Client process to perform the client greeter interactions.
covering
greeterClient : (proc : PID) -> GreeterFrontend (greeter gBody) ()
greeterClient proc = do
    setChan 'Bob proc
    sendTo 'Bob "I am a nasty hack"
    dropChan 'Bob
    (clientBody proc)
    return ()

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


text:
module Utils

import Control.ST
import public Data.Vect

%inline
public export
jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

export
debugError : String -> JS_IO a
debugError s = believe_me <$> jscall "throw2(%0)" (String -> JS_IO ()) s

export
setTimeout : JS_IO () -> Int -> JS_IO ()
setTimeout act millis = jscall "setTimeout(%0,%1)" (JsFn (() -> JS_IO ()) -> Int -> JS_IO ()) (MkJsFn (\()=>act)) millis

export
isUndefined : Ptr -> JS_IO Bool
isUndefined x =
  do
    i <- jscall "(%0 == undefined)+0" (Ptr -> JS_IO Int) x
    if i == 0 then
      pure False
      else pure True

export
data JSIORef : (b:Type) -> Type where
  MkJSIORef : Ptr -> JSIORef a

export
newJSIORef : a -> JS_IO (JSIORef a)
newJSIORef x = MkJSIORef <$> jscall "{val: %0}" (Ptr -> JS_IO Ptr) (believe_me x)

export
writeJSIORef : JSIORef a -> a -> JS_IO ()
writeJSIORef (MkJSIORef ctx) z = jscall "%0.val = %1" (Ptr -> Ptr -> JS_IO ()) ctx (believe_me z)

export
readJSIORef : JSIORef a -> JS_IO a
readJSIORef (MkJSIORef ctx) = believe_me <$> jscall "%0.val" ( Ptr -> JS_IO Ptr) ctx

export
modifyJSIORef : JSIORef a -> (a->a) -> JS_IO ()
modifyJSIORef ref f =
  do
    v <- readJSIORef ref
    writeJSIORef ref (f v)

export
random : JS_IO Double
random = jscall "Math.random()" (() -> JS_IO Double) ()

export
randomInt : Int -> JS_IO Int
randomInt x = pure $ cast $ !random * (cast x)

export
randomInteger : Integer -> JS_IO Integer
randomInteger x = pure $ cast $ !random * (cast x)

export
randomNat : Nat -> JS_IO Nat
randomNat x = cast <$> randomInteger (cast x)

export
randomFin : {n: Nat} -> JS_IO (Fin (S n))
randomFin {n} =
  case natToFin !(randomNat (S n)) (S n) of
    Just y => pure y
    Nothing => pure FZ

export total
shuffle : List a -> JS_IO (List a)
shuffle x =
  shuffle' (fromList x) []
  where
    total
    shuffle' : Vect n a -> List a -> JS_IO (List a)
    shuffle' {n = Z} xs ys = pure ys
    shuffle' {n = (S k)} xs ys =
      let pos = !randomFin
      in shuffle' (deleteAt pos xs) (index pos xs :: ys)

export
readJSList : Ptr -> JS_IO (List Ptr)
readJSList x =
  do
    len <- jscall "%0.length" (Ptr -> JS_IO Int) x
    if len > 0 then
      do
        pfirst <- jscall "%0[0]" (Ptr -> JS_IO Ptr) x
        prest <- jscall "%0.slice(1)" (Ptr -> JS_IO Ptr) x
        rest <- readJSList prest
        pure $ pfirst :: rest
      else
          pure []

export
makeJSList : List Ptr -> JS_IO Ptr
makeJSList [] = jscall "[]" (() -> JS_IO Ptr) ()
makeJSList (x::xs) =
  do
    res <- makeJSList xs
    jscall "%1.unshift(%0)" (Ptr -> Ptr -> JS_IO ()) x res
    pure res

export
makeJSObj : List (String, Ptr) -> JS_IO Ptr
makeJSObj [] =
  jscall "{}" (() -> JS_IO Ptr) ()
makeJSObj ((k,v)::xs) =
  do
    o <- makeJSObj xs
    jscall "%2[%0]=%1" (String -> Ptr -> Ptr -> JS_IO ()) k v o
    pure o

export
makeJSNumberObj : List (Double, Ptr) -> JS_IO Ptr
makeJSNumberObj [] =
  jscall "{}" (() -> JS_IO Ptr) ()
makeJSNumberObj ((k,v)::xs) =
  do
    o <- makeJSNumberObj xs
    jscall "%2[%0]=%1" (Double -> Ptr -> Ptr -> JS_IO ()) k v o
    pure o

export
makeJSStringObj : List (String, String) -> JS_IO Ptr
makeJSStringObj xs = makeJSObj $ map (\(x,y)=>(x,believe_me y)) xs

public export
interface Console (m:Type -> Type) where
    consoleLog : String -> STrans m () xs (const xs)

export
implementation Console JS_IO where
  consoleLog s = lift $ jscall "console.log(%0)" (String -> JS_IO ()) s

public export
interface JSRandom (m:Type -> Type) where
  randInt : Int -> STrans m Int xs (const xs)

export
implementation JSRandom JS_IO where
  randInt i = lift $ randomInt i

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module TTImp.BindImplicits

import Core.Context
import Core.Context.Log
import Core.Core
import Core.TT
import TTImp.TTImp
import TTImp.Utils

import Control.Monad.State

import Data.List

%default covering

-- Rename the IBindVars in a term. Anything which appears in the list 'renames'
-- should be renamed, to something which is *not* in the list 'used'
export
renameIBinds : (renames : List String) ->
               (used : List String) ->
               RawImp -> State (List (String, String)) RawImp
renameIBinds rs us (IPi fc c p (Just un@(UN (Basic n))) ty sc)
    = if n `elem` rs
         then let n' = getUnique (rs ++ us) n
                  un' = UN (Basic n')
                  sc' = substNames (map (UN . Basic) (filter (/= n) us))
                                   [(un, IVar fc un')] sc in
             do scr <- renameIBinds rs (n' :: us) sc'
                ty' <- renameIBinds rs us ty
                upds <- get
                put ((n, n') :: upds)
                pure $ IPi fc c p (Just un') ty' scr
         else do scr <- renameIBinds rs us sc
                 ty' <- renameIBinds rs us ty
                 pure $ IPi fc c p (Just un) ty' scr
renameIBinds rs us (IPi fc c p n ty sc)
    = pure $ IPi fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
renameIBinds rs us (ILam fc c p n ty sc)
    = pure $ ILam fc c p n !(renameIBinds rs us ty) !(renameIBinds rs us sc)
renameIBinds rs us (IApp fc fn arg)
    = pure $ IApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IAutoApp fc fn arg)
    = pure $ IAutoApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (INamedApp fc fn n arg)
    = pure $ INamedApp fc !(renameIBinds rs us fn) n !(renameIBinds rs us arg)
renameIBinds rs us (IWithApp fc fn arg)
    = pure $ IWithApp fc !(renameIBinds rs us fn) !(renameIBinds rs us arg)
renameIBinds rs us (IAs fc nameFC s n pat)
    = pure $ IAs fc nameFC s n !(renameIBinds rs us pat)
renameIBinds rs us (IMustUnify fc r pat)
    = pure $ IMustUnify fc r !(renameIBinds rs us pat)
renameIBinds rs us (IDelayed fc r t)
    = pure $ IDelayed fc r !(renameIBinds rs us t)
renameIBinds rs us (IDelay fc t)
    = pure $ IDelay fc !(renameIBinds rs us t)
renameIBinds rs us (IForce fc t)
    = pure $ IForce fc !(renameIBinds rs us t)
renameIBinds rs us (IAlternative fc u alts)
    = pure $ IAlternative fc !(renameAlt u)
                             !(traverse (renameIBinds rs us) alts)
  where
    renameAlt : AltType -> State (List (String, String)) AltType
    renameAlt (UniqueDefault t) = pure $ UniqueDefault !(renameIBinds rs us t)
    renameAlt u = pure u
renameIBinds rs us (IBindVar fc n)
    = if n `elem` rs
         then do let n' = getUnique (rs ++ us) n
                 upds <- get
                 put ((n, n') :: upds)
                 pure $ IBindVar fc n'
         else pure $ IBindVar fc n
renameIBinds rs us tm = pure $ tm

export
doBind : List (String, String) -> RawImp -> RawImp
doBind [] tm = tm
doBind ns (IVar fc nm@(UN (Basic n)))
    = maybe (IVar fc nm)
            (IBindVar fc)
            (lookup n ns)
doBind ns (IPi fc rig p mn aty retty)
    = let ns' = case mn of
                     Just (UN (Basic n)) => filter (\x => fst x /= n) ns
                     _ => ns in
          IPi fc rig p mn (doBind ns' aty) (doBind ns' retty)
doBind ns (ILam fc rig p mn aty sc)
    = let ns' = case mn of
                     Just (UN (Basic n)) => filter (\x => fst x /= n) ns
                     _ => ns in
          ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
doBind ns (IApp fc fn av)
    = IApp fc (doBind ns fn) (doBind ns av)
doBind ns (IAutoApp fc fn av)
    = IAutoApp fc (doBind ns fn) (doBind ns av)
doBind ns (INamedApp fc fn n av)
    = INamedApp fc (doBind ns fn) n (doBind ns av)
doBind ns (IWithApp fc fn av)
    = IWithApp fc (doBind ns fn) (doBind ns av)
doBind ns (IAs fc nameFC s n pat)
    = IAs fc nameFC s n (doBind ns pat)
doBind ns (IMustUnify fc r pat)
    = IMustUnify fc r (doBind ns pat)
doBind ns (IDelayed fc r ty)
    = IDelayed fc r (doBind ns ty)
doBind ns (IDelay fc tm)
    = IDelay fc (doBind ns tm)
doBind ns (IForce fc tm)
    = IForce fc (doBind ns tm)
doBind ns (IQuote fc tm)
    = IQuote fc (doBind ns tm)
doBind ns (IUnquote fc tm)
    = IUnquote fc (doBind ns tm)
doBind ns (IAlternative fc u alts)
    = IAlternative fc (mapAltType (doBind ns) u) (map (doBind ns) alts)
doBind ns tm = tm

export
bindNames : {auto c : Ref Ctxt Defs} ->
            (arg : Bool) -> RawImp -> Core (List Name, RawImp)
bindNames arg tm
    = if !isUnboundImplicits
         then do let ns = nub (findBindableNames arg [] [] tm)
                 log "elab.bindnames" 10 $ "Found names :" ++ show ns
                 pure (map (UN . Basic) (map snd ns), doBind ns tm)
         else pure ([], tm)

-- if the name is part of the using decls, add the relevant binder for it:
-- either an implicit pi binding, if there's a name, or an autoimplicit type
-- binding if the name just appears as part of the type
getUsing : Name -> List (Int, Maybe Name, RawImp) ->
           List (Int, (RigCount, PiInfo RawImp, Maybe Name, RawImp))
getUsing n [] = []
getUsing n ((t, Just n', ty) :: us) -- implicit binder
    = if n == n'
         then (t, (erased, Implicit, Just n, ty)) :: getUsing n us
         else getUsing n us
getUsing n ((t, Nothing, ty) :: us) -- autoimplicit binder
    = let ns = nub (findIBindVars ty) in
          if n `elem` ns
             then (t, (top, AutoImplicit, Nothing, ty)) ::
                      getUsing n us
             else getUsing n us

getUsings : List Name -> List (Int, Maybe Name, RawImp) ->
            List (Int, (RigCount, PiInfo RawImp, Maybe Name, RawImp))
getUsings ns u = concatMap (flip getUsing u) ns

bindUsings : List (RigCount, PiInfo RawImp, Maybe Name, RawImp) -> RawImp -> RawImp
bindUsings [] tm = tm
bindUsings ((rig, p, mn, ty) :: us) tm
    = IPi (getFC ty) rig p mn ty (bindUsings us tm)

addUsing : List (Maybe Name, RawImp) ->
           RawImp -> RawImp
addUsing uimpls tm
    = let ns = nub (findIBindVars tm)
          bs = nubBy (\x, y => fst x == fst y)
                     (getUsings ns (tag 0 uimpls)) in
          bindUsings (map snd bs) tm
  where
    tag : Int -> List a -> List (Int, a) -- to check uniqueness of resulting uimps
    tag t xs = zip (map (+t) [0..cast (length xs)]) xs

export
bindTypeNames : {auto c : Ref Ctxt Defs} ->
                FC -> List (Maybe Name, RawImp) ->
                List Name -> RawImp-> Core RawImp
bindTypeNames fc uimpls env tm
    = if !isUnboundImplicits
             then do ns <- findUniqueBindableNames fc True env [] tm
                     let btm = doBind ns tm
                     pure (addUsing uimpls btm)
             else pure tm

export
bindTypeNamesUsed : {auto c : Ref Ctxt Defs} ->
                    FC -> List String -> List Name -> RawImp -> Core RawImp
bindTypeNamesUsed fc used env tm
    = if !isUnboundImplicits
         then do ns <- findUniqueBindableNames fc True env used tm
                 pure (doBind ns tm)
         else pure tm

export
piBindNames : {auto c : Ref Ctxt Defs} ->
              FC -> List Name -> RawImp -> Core RawImp
piBindNames loc env tm
    = do ns <- findUniqueBindableNames loc True env [] tm
         pure $ piBind (map fst ns) tm
  where
    piBind : List String -> RawImp -> RawImp
    piBind [] ty = ty
    piBind (n :: ns) ty
       = IPi loc erased Implicit (Just (UN $ Basic n)) (Implicit loc False)
       $ piBind ns ty


text:
module Main

-- When generating javasript from idris, it is possible that the same name may appear in
-- different clauses when translating cases from Idris. To avoid a javascript syntax error
-- from occuring due to duplicate declations, each case clause is wrapped in brackets
-- to create unique block scopes.

-- https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Statements/switch

-- Without wrapping in a block, the test error may look like the following:
-- syntax001/build/exec/_tmp_node.js:39
-- const x = ({h:1});
--         ^
-- SyntaxError: Identifier 'x' has already been declared

test : Bool -> Int
test x @ True =
  case x of
    _ => 0
test x @ False =
  case x of
    _ => 1

main : IO ()
main = do
  printLn $ test True
  printLn $ test False


text:
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just prf => Just (cong S prf)


text:
-- Vector.idr
--
-- Working with vectors and length-constraint lists

import Data.Vect

aList : List Int
aList = [1, 2, 3]

addToList : List Int -> Int -> List Int
addToList [] x = []
addToList (y :: ys) x = y + x :: addToList ys x

addToListWrong : List Int -> Int -> List Int
addToListWrong [] x = [0]
addToListWrong (y :: ys) x = y + x :: addToListWrong ys x

aVect : Vect 3 Int
aVect = [1, 2, 3]

addToVect : Vect n Int -> Int -> Vect n Int
addToVect [] x = []
addToVect (y :: ys) x = y + x :: addToVect ys x

addToVectWrong : Vect n Int -> Int -> Vect n Int
addToVectWrong [] x = [0]
addToVectWrong (y :: ys) x = y + x :: addToVectWrong ys x

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
-- Idris2

import System.Concurrency

||| Test basic lock/acquire and unlock/release functionality
main : IO ()
main =
  do m <- makeMutex
     mutexAcquire m
     putStrLn "Mutex acquired"
     mutexRelease m
     putStrLn "Mutex released"